Return Styles: Pseud0ch, Terminal, Valhalla, NES, Geocities, Blue Moon. Entire thread

Produce [1..n] in Coq

Name: Anonymous 2015-03-28 10:42

I'm reading Coq in a Hurry.
https://cel.archives-ouvertes.fr/file/index/docid/459139/filename/coq-hurry.pdf
On page 8 there is the following exercise
Exercise on lists, map, and app. (app is like ++ in Haskell)
Define a function that takes as input a number n and returns a list with n elements, from 0 to n − 1.

I have written the following code.
Fixpoint ex2 (n : nat) :=
match n with
0 => (nil : list nat)
| S p => n :: ex2 p
end.
This produces the list in reverse order (nevermind it is [1..n], not [0..n-1]). Is there any functional way to produce a list in increasing order without using reverse? Keep in mind this is page 8 and I think I am not supposed to use auxiliary functions (or maybe I am?).

Name: Anonymous 2015-03-28 12:27

use a difference list

Fixpoint iota (n : nat) (acc : list nat -> list nat) :=
match n with
| O => acc nil
| S m => iota m (fun xs => acc (cons n xs))
end.

Name: Anonymous 2015-03-28 13:08

apping in Coq!

Name: Anonymous 2015-03-28 13:32

We need a tutorial for creating a website with Coq in 3 hours.

Name: Anonymous 2015-03-28 13:33

JACKSON 5 GET

Name: Anonymous 2015-03-28 13:38

>>4
Coq-Driven Web Design: The Definitive Guide

Name: Anonymous 2015-03-28 17:27

>>2
Cool, thank you. More Coq code to come tomorrow! (gotta sleepzzzzzzzzzzzzz)

Name: Anonymous 2015-03-29 10:44

>>7
I'm eagerly waiting for your Coq.

Name: Anonymous 2015-03-29 18:47

>>8
Blegh, here are some exercises from Chapter 2. Coq feels a bit like Haskell (not that I know Haskell tho). I might read some of Chapter 3 now, but god damn it I'm tired.

Require Import List.
Require Import Bool.
Require Import Arith.

Definition ex3_1 (l : list nat) :=
match l with
nil => true
| x::nil => true
| x::y::xs => leb x y
end.

Fixpoint ex3_2 (l : list nat) :=
match l with
nil => true
| x::xs => andb (ex3_1 l) (ex3_2 xs)
end.

Fixpoint ex4_help (n : nat) (l : list nat) (count : nat) :=
match l with
nil => count
| x::xs => ex4_help n xs count + (if (beq_nat n x) then 1 else 0)
end.

Definition ex4 (n : nat) (l : list nat) :=
ex4_help n l 0.

Eval compute in ex3_2 (1::2::4::3::nil).

Eval compute in ex4 3 (1::3::3::1::3::nil).

Name: Anonymous 2015-03-29 19:40

>>9
ex3_2 returns true if the list is sorted, false otherwise
ex4 counts the number of occurences of its first argument in the second argument (list).

Name: Anonymous 2015-03-30 20:19

CHECKEMMMMMMMMMMMMMMMMMMM

Name: Anonymous 2015-03-30 21:38

Definition dubs : nat -> Prop :=
fun n => exists x, exists y, n = x + 10*x + 100*y.

Theorem check_11 : dubs 11.
Proof.
unfold dubs.
exists 1; exists 0.
compute.
reflexivity.
Qed.

(* Nice dubs *)

Name: Anonymous 2015-03-31 7:55

>>12
Thanks! Cool.

Name: Anonymous 2017-05-19 20:04

Good exercise for the brain.

Name: Anonymous 2017-05-25 15:28

>>1
from 0 to n − 1.
0-based crap does not belong in a programming book. Your program shows one reason why 1 to n is more natural.

Name: Anonymous 2017-05-25 16:18

>>14
Yeah, all these C programmers are wasting away their brain potential instead of doing coqs. We should show them our powerful coq code. Convert them to the coqdom.
Newer Posts
Don't change these.
Name: Email:
Entire Thread Thread List
All trademarks and copyrights on this site are owned by their respective parties. All comments and posts are the responsibility of their own posters.
- Tinychan + 2ch Mode + RSS -