(** Mathematics for Computer Scientists 2 (G52MC2)
    Thorsten Altenkirch

    L13 (lists)

    The material in this file contains coq proofs
    which can be read and animated with coqide or xemacs+proofgeneral.

**)

Section l13.

Set Implicit Arguments.
Require Import Coq.Lists.List.

Check (nil : list nat).
Definition l23 : list nat
  := 2 :: 3 :: nil.

Definition l123 : list nat
  := 1 :: l23.

Eval compute in l123.
Eval compute in 1 :: l123.

Definition ll1 : list (list nat) 
  := l23 :: l123 :: nil.

Eval compute in ll1.

Eval compute in nil :: ll1.

Definition hd (ns : list nat) : nat :=
  match ns with
  | nil => 0
  | n :: ns' => n
  end.

Eval compute in hd l123.


Definition hd' (A : Set)(bs : list A) 
  : unit + A :=
  match bs with
  | nil => inl A tt
  | a :: as' => inr unit a
  end.

Eval compute in hd' l123.
Eval compute in hd' (nil : list nat).
Eval compute in hd' ll1.

Fixpoint length 
   (A:Set)(l:list A){struct l} : nat :=
  match l with
  | nil => 0
  | a :: m => S (length m)
  end.

Eval compute in (length l123).
Eval compute in (length ll1).

Fixpoint app (A : Set)(l m:list A) {struct l} : list A :=
  match l with
  | nil => m
  | cons a l' => cons a (app l' m)
  end. 

(* ++ = app, defined in the library. *)

Eval compute in (l123 ++ l23).
Eval compute in (l23 ++ l123).

Lemma nilApp : forall (A:Set)(l:list A), 
  nil ++ l = l.
intros.
simpl.
reflexivity.
Qed.

Lemma appNil : forall (A:Set)(l:list A), 
  l ++ nil = l.
intros.
induction l.
simpl.
reflexivity.
simpl.
rewrite IHl.
reflexivity.
Qed.


Lemma assocApp : forall (A:Set)(l1 l2 l3:list A), 
  (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
induction l1.
simpl.
intros.
reflexivity.
intros.
simpl.
rewrite IHl1.
reflexivity.
Qed.

Fixpoint snoc (A:Set)
  (l : list A)(a : A) {struct l} : list A
  := match l with
     | nil => a :: nil
     | b :: m => b :: (snoc m a)
     end.

Eval compute in (snoc l123 4).

Fixpoint rev 
  (A:Set)(l : list A) {struct l} : list A :=
  match l with
  | nil => nil
  | a :: m => snoc (rev m) a 
  end.

Eval compute in rev l123.
Eval compute in rev (rev l123).

Lemma revsnoc : forall (A:Set)(l:list A)(a:A),
  rev (snoc l a) = a :: (rev l).
intros.
induction l.
simpl.
reflexivity.
simpl.
rewrite IHl.
simpl.
reflexivity.
Qed.

Lemma revrev :  
  forall (A:Set)(l:list A),rev (rev l) = l.
intros.
induction l.
simpl.
reflexivity.
simpl.
rewrite revsnoc.
rewrite IHl.
reflexivity.
Qed.