Library list_ex
appending two lists by recursion over the first input list
Fixpoint append (l m : natlist) {struct l} : natlist :=
match l with
| nil => m
| cons x xs => cons x (append xs m)
end.
match l with
| nil => m
| cons x xs => cons x (append xs m)
end.
one of the following lemma's has a simple proof, without induction
which? why?
Lemma append_nil_r : forall l, append l nil = l.
Proof.
Admitted.
Lemma append_nil_l : forall l, append nil l = l.
Proof.
Admitted.
in the following lemma: think about what variable to do induction over
Lemma append_assoc : forall l k m ,
append l (append k m) = append (append l k) m.
Proof.
Admitted.
Fixpoint length (l : natlist) : nat :=
match l with
| nil => 0
| cons a k => S(length k)
end.
Lemma append_length : forall l m,
length (append l m) = length l + length m.
Proof.
Admitted.
append l (append k m) = append (append l k) m.
Proof.
Admitted.
Fixpoint length (l : natlist) : nat :=
match l with
| nil => 0
| cons a k => S(length k)
end.
Lemma append_length : forall l m,
length (append l m) = length l + length m.
Proof.
Admitted.
Exercise 1: define a function list_sum : natlist -> nat that sums up
all elements in a list
Exercise 2: define a function list_map :(nat->nat) -> natlist -> natlist
that applies a function f to all elements in a list
Fixpoint list_map (f : nat -> nat)(l: natlist) := ....
reversing a list, using append
Fixpoint list_map (f : nat -> nat)(l: natlist) := ....
Fixpoint reverse (l : natlist) : natlist :=
match l with
| nil => nil
| cons a k => append (reverse k) (cons a nil)
end.
Lemma reverse_append : forall l m,
reverse (append l m) = append (reverse m) (reverse l).
Proof.
Admitted.
Lemma reverse_length : forall l,
length l = length (reverse l).
Proof.
Admitted.
Lemma reverse_double : forall l, reverse (reverse l) = l.
Proof.
Admitted.
match l with
| nil => nil
| cons a k => append (reverse k) (cons a nil)
end.
Lemma reverse_append : forall l m,
reverse (append l m) = append (reverse m) (reverse l).
Proof.
Admitted.
Lemma reverse_length : forall l,
length l = length (reverse l).
Proof.
Admitted.
Lemma reverse_double : forall l, reverse (reverse l) = l.
Proof.
Admitted.
Pretty printing of lists in the standard library
the list type is defined parametrically over the carrier type A
Check cons.
Check nil.
Definition example_list := cons 1 (cons 2 (cons 3 (cons 4 nil))).
Print example_list.
Check nil.
Definition example_list := cons 1 (cons 2 (cons 3 (cons 4 nil))).
Print example_list.
Rocq prints the list back in its own sugared notation
And there is notation for append
Here is how you compute with the Rocq functions