(*

Midland Graduate School 2008: COQ

*)

Section inductive.

(*
Inductive Nat:Set :=
| zero : Nat
| succ : Nat -> Nat.

Check Nat.
Check succ.
*)

Check 7.

Fixpoint my_add (m n : nat) {struct m} : nat :=
  match m with
  | 0 => n
  | S m' => S (my_add m' n)
  end.

Eval compute in (my_add 7 3).

Require Import List.

Definition l1 : list nat := 1 :: 2 :: 3 :: nil.

Eval compute in l1++l1.

Variable A:Set.

Set Implicit Arguments.

Fixpoint snoc (l : list A) (a:A) := 
   match l with
   | nil => a::nil
   | b::l' => b::(snoc l' a)
   end.   

Fixpoint rev (l : list A) :=
  match l with 
  | nil => nil
  | a :: l' => snoc (rev l') a
  end.

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

Lemma rev_lem : forall l:list A, rev( rev l) = l.
intros.
induction l.
auto.
simpl.
rewrite snoc_lem.
rewrite IHl.
auto.
Qed.



End inductive.

Check rev.

Eval compute in (rev (rev l1)).