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-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).

Newer Posts
Don't change these.
Name: Email:
Entire Thread Thread List