(* Exercise coq_list_01 *)

(* In exercises coq_nat_* we were dealing with natural 
   numbers. Not let us define lists of natural numbers.
   Such a list is either empty, 'nil', or it is a natural
   number 'a' followed by a list 'l' - 'cons a l'. *)
Inductive natlist : Set :=
  | nil : natlist
  | cons : nat -> natlist -> natlist.

(* Remark: lists are defined in the standard library of
   Coq but that definition is polymorphic, ie. for every
   type 'A', 'list A' gives a type of lists with elements
   of type 'A'. *)

(* Now let us define some operations on such lists. 
   Let's start with an append function that given two lists
   concatenates them. *)
Fixpoint append (l m : natlist) {struct l} : natlist :=
  match l with
  | nil => m
  | cons x xs => cons x (append xs m)
  end.
  
(* Now let us prove how append works with empty lists *)

Lemma append_nil_l : forall l, append nil l = l.

Proof.
induction l.
- simpl. auto.
- simpl. auto.
Qed.

(* But note that, as append is defined by recursion 
   over the first argument, we can even do without an induction,
   as append nil l = l by a computation step
   So we also have: *)

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

Lemma append_nil_r : forall l, append l nil = l.

Proof.
induction l.
- simpl; auto.
- simpl; auto. rewrite IHl. reflexivity.
Qed.