Library list_ex_answers

Programming and proving with lists

Inductive natlist : Set :=
| nil : natlist
| cons : nat -> natlist -> natlist.

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.

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.
induction l.
- simpl. auto.
- simpl. rewrite IHl. auto.
Qed.

Lemma append_nil_l : forall l, append nil l = l.
Proof.
simpl.
auto.
Qed.

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.
induction l.
- intros k m. simpl. auto.
- intros k m. simpl. rewrite IHl. auto.
Qed.

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

Fixpoint list_sum (l: natlist) {struct l} : nat :=
  match l with
  | nil => 0
  | cons x xs => plus x (list_sum xs)
  end.

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) {struct l} : natlist :=
  match l with
  | nil => nil
  | cons x xs => cons (f x) (list_map f xs)
  end.

reversing a list, using append

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.
intro l.
induction l.
- simpl. intro m.
  rewrite append_nil_r. auto.
- intro m. simpl.
  rewrite IHl.
  rewrite append_assoc.
  auto.
Qed.

Lemma reverse_length : forall l,
  length l = length (reverse l).
Proof.
induction l.
- simpl;auto.
- simpl.
  rewrite IHl.
  simpl.
  rewrite append_length.
  simpl.
  auto.

Alternative 1: First prove a separate
Lemma help : forall n: nat, S n = n + 1.
and then apply help
The shortest solution is to invoke lia, which add all kinds of automation regarding a.o. arithmetic
It is actually "not done" to Import such a file inside a proof: do it in at teh beginning of your file

Require Import Lia.
lia.
Qed.

Alternative 2: reverse the lemma append_length

Axiom append_length' : forall l m,
  length (append l m) = length m + length l.

Lemma reverse_length' : forall l,
  length l = length (reverse l).
Proof.
induction l.
- simpl;auto.
- simpl.
  rewrite IHl.
  simpl.
  rewrite append_length'.
  simpl.
  auto.
Qed.

Lemma reverse_double : forall l, reverse (reverse l) = l.
Proof.
intro l.
induction l.
- simpl. reflexivity.
- simpl.
  rewrite reverse_append.
  simpl.
  rewrite IHl.
  auto.
Qed.

Pretty printing of lists in the standard library

Require Import List.

Check list.
Print list.

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.

Rocq prints the list back in its own sugared notation

And there is notation for append

Definition example_list' := example_list ++ example_list.

Here is how you compute with the Rocq functions

Eval compute in example_list'.