New Verilog and Coq sample files added

New Verilog examples and Coq examples for additional training have
been added since linguist is currently failing Coq/Verilog recognition
tasks (see #201). In case it wasn't obvious, linguist will not
currently pass these new, added test cases.

samples/coq/Basics.v

@@ -0,0 +1,707 @@
+Inductive day : Type :=
+| monday : day
+| tuesday : day
+| wednesday : day
+| thursday : day
+| friday : day
+| saturday : day
+| sunday : day.
+
+Definition next_weekday (d:day) : day :=
+  match d with
+  | monday => tuesday
+  | tuesday => wednesday
+  | wednesday => thursday
+  | thursday => friday
+  | friday => monday
+  | saturday => monday
+  | sunday => monday
+  end.
+
+Example test_next_weekday:
+(next_weekday (next_weekday saturday)) = tuesday.
+
+Proof. simpl. reflexivity. Qed.
+
+Inductive bool : Type :=
+	| true : bool
+	| false : bool.
+
+Definition negb (b:bool) : bool :=
+													 match b with
+																			 | true => false
+																			 | false => true
+													 end.
+
+Definition andb (b1:bool) (b2:bool) : bool :=
+		match b1 with
+		 | true => b2
+		 | false => false
+	  end.
+
+Definition orb (b1:bool) (b2:bool) : bool :=
+		match b1 with
+		  | true => true
+		  | false => b2
+		end.
+
+Example test_orb1: (orb true false) = true.
+Proof. simpl. reflexivity. Qed.
+
+Example test_orb2: (orb false false) = false.
+Proof. simpl. reflexivity. Qed.
+
+Example test_orb3: (orb false true) = true.
+Proof. simpl. reflexivity. Qed.
+
+Example test_orb4: (orb true true) = true.
+Proof. simpl. reflexivity. Qed.
+
+Definition nandb (b1: bool) (b2:bool) : bool :=
+	match b1 with
+		| true => match b2 with
+										| false => true
+										| true => false
+							end
+		| false => true
+	end.
+
+Example test_nandb1: (nandb true false) = true.
+Proof. simpl. reflexivity. Qed.
+Example test_nandb2: (nandb false false) = true.
+Proof. simpl. reflexivity. Qed.
+Example test_nandb3: (nandb false true) = true.
+Proof. simpl. reflexivity. Qed.
+Example test_nandb4: (nandb true true) = false.
+Proof. simpl. reflexivity. Qed.
+
+Definition andb3 (b1: bool) (b2:bool) (b3:bool) : bool :=
+	match b1 with
+    | false => false
+		| true => match b2 with
+								| false => false
+								| true => b3
+							end
+	end.
+
+Example test_andb31: (andb3 true true true) = true.
+Proof. simpl. reflexivity. Qed.
+Example test_andb32: (andb3 false true true) = false.
+Proof. simpl. reflexivity. Qed.
+Example test_andb33: (andb3 true false true) = false.
+Proof. simpl. reflexivity. Qed.
+Example test_andb34: (andb3 true true false) = false.
+Proof. simpl. reflexivity. Qed.
+
+Module Playground1.
+
+Inductive nat : Type :=
+	| O : nat
+	| S : nat -> nat.
+
+Definition pred (n : nat) : nat :=
+	match n with
+		| O => O
+		| S n' => n'
+	end.
+
+Definition minustwo (n : nat) : nat :=
+	match n with
+		| O => O
+		| S O => O
+		| S (S n') => n'
+	end.
+
+Fixpoint evenb (n : nat) : bool :=
+	match n with
+		| O => true
+		| S O => false
+		| S (S n') => evenb n'
+	end.
+
+Definition oddb (n : nat) : bool := negb (evenb n).
+
+Example test_oddb1: (oddb (S O)) = true.
+Proof. reflexivity. Qed.
+Example test_oddb2: (oddb (S (S (S (S O))))) = false.
+Proof. reflexivity. Qed.
+
+Fixpoint plus (n : nat) (m : nat) : nat :=
+	match n with
+		| O => m
+		| S n' => S (plus n' m)
+	end.
+
+Fixpoint mult (n m : nat) : nat :=
+	match n with
+		| O => O
+		| S n' => plus m (mult n' m)
+	end.
+
+Fixpoint minus (n m : nat) : nat :=
+	match n, m with
+		| O, _ => n
+		| S n', O => S n'
+		| S n', S m' => minus n' m'
+	end.
+
+Fixpoint exp (base power : nat) : nat :=
+	match power with
+		| O => S O
+		| S p => mult base (exp base p)
+	end.
+
+Fixpoint factorial (n : nat) : nat :=
+	match n with
+		| O => S O
+		| S n' => mult n (factorial n')
+	end.
+
+Example test_factorial1: (factorial (S (S (S O)))) = (S (S (S (S (S (S O)))))).
+Proof. simpl. reflexivity. Qed.
+
+Notation "x + y" := (plus x y) (at level 50, left associativity) : nat_scope.
+Notation "x - y" := (minus x y) (at level 50, left associativity) : nat_scope.
+Notation "x * y" := (mult x y) (at level 40, left associativity) : nat_scope.
+
+Fixpoint beq_nat (n m : nat) : bool :=
+	match n with
+		| O => match m with
+						| O => true
+						| S m' => false
+					 end
+		| S n' => match m with
+							| O => false
+							| S m' => beq_nat n' m'
+							end
+	end.
+
+Fixpoint ble_nat (n m : nat) : bool :=
+	match n with
+		| O => true
+		| S n' => 
+				match m with
+					| O => false
+					| S m' => ble_nat n' m'
+				end
+	end.
+
+Example test_ble_nat1: (ble_nat (S (S O)) (S (S O))) = true.
+Proof. simpl. reflexivity. Qed.
+Example test_ble_nat2: (ble_nat (S (S O)) (S (S (S (S O))))) = true.
+Proof. simpl. reflexivity. Qed.
+Example test_ble_nat3: (ble_nat (S (S (S (S O)))) (S (S O))) = false.
+Proof. simpl. reflexivity. Qed.
+
+Definition blt_nat (n m : nat) : bool :=
+		(andb (negb (beq_nat n m)) (ble_nat n m)).
+
+Example test_blt_nat1: (blt_nat (S (S O)) (S (S O))) = false.
+Proof. simpl. reflexivity. Qed.
+Example test_blt_nat3: (blt_nat (S (S (S (S O)))) (S (S O))) = false.
+Proof. simpl. reflexivity. Qed.
+Example test_blt_nat2 : (blt_nat (S (S O)) (S (S (S (S O))))) = true.
+Proof. simpl. reflexivity. Qed.
+
+Theorem plus_O_n : forall n : nat, O + n = n.
+Proof.
+	simpl. reflexivity. Qed.
+
+Theorem plus_O_n' : forall n : nat, O + n = n.
+Proof.
+	reflexivity. Qed.
+
+Theorem plus_O_n'' : forall n : nat, O + n = n.
+Proof.
+	intros n. reflexivity. Qed.
+
+Theorem plus_1_1 : forall n : nat, (S O) + n = S n.
+Proof.
+	intros n. reflexivity. Qed.
+
+Theorem mult_0_1: forall n : nat, O * n = O.
+Proof.
+	intros n. reflexivity. Qed.
+
+Theorem plus_id_example : forall n m:nat,
+	n = m -> n + n = m + m.
+Proof.
+	intros n m.
+	intros H.
+	rewrite -> H.
+	reflexivity. Qed.
+
+Theorem plus_id_exercise : forall n m o: nat,
+	n = m -> m = o -> n + m = m + o.
+Proof.
+	intros n m o.
+	intros H.
+	intros H'.
+	rewrite -> H.
+	rewrite <- H'.
+	reflexivity.
+	Qed.
+
+Theorem mult_0_plus : forall n m : nat,
+				(O + n) * m = n * m.
+Proof.
+	intros n m.
+	rewrite -> plus_O_n.
+	reflexivity. Qed.
+
+Theorem mult_1_plus : forall n m: nat,
+	((S O) + n) * m = m + (n * m).
+Proof.
+	intros n m.
+	rewrite -> plus_1_1.
+	reflexivity.
+	Qed.
+
+Theorem mult_1 : forall n : nat,
+				n * (S O) = n.
+Proof.
+	intros n.
+	induction n as [| n'].
+	reflexivity.
+	simpl.
+	rewrite -> IHn'.
+	reflexivity.
+	Qed.
+
+Theorem plus_1_neq_0 : forall n : nat,
+				beq_nat (n + (S O)) O = false.
+Proof.
+	intros n.
+	destruct n as [| n'].
+	reflexivity.
+	reflexivity.
+	Qed.
+
+Theorem zero_nbeq_plus_1 : forall n : nat,
+				beq_nat O (n + (S O)) = false.
+Proof.
+	intros n.
+	destruct n.
+	reflexivity.
+	reflexivity.
+Qed.
+
+Require String. Open Scope string_scope.
+
+Ltac move_to_top x :=
+match reverse goal with
+| H : _ |- _ => try move x after H
+end.
+
+Tactic Notation "assert_eq" ident(x) constr(v) :=
+	let H := fresh in
+	assert (x = v) as H by reflexivity;
+	clear H.
+
+	Tactic Notation "Case_aux" ident(x) constr(name) :=
+		first [
+		set (x := name); move_to_top x
+		| assert_eq x name; move_to_top x
+		| fail 1 "because we are working on a different case" ].
+
+		Ltac Case name := Case_aux Case name.
+		Ltac SCase name := Case_aux SCase name.
+		Ltac SSCase name := Case_aux SSCase name.
+		Ltac SSSCase name := Case_aux SSSCase name.
+		Ltac SSSSCase name := Case_aux SSSSCase name.
+		Ltac SSSSSCase name := Case_aux SSSSSCase name.
+		Ltac SSSSSSCase name := Case_aux SSSSSSCase name.
+		Ltac SSSSSSSCase name := Case_aux SSSSSSSCase name.
+
+Theorem andb_true_elim1 : forall b c : bool,
+				andb b c = true -> b = true.
+Proof.
+	intros b c H.
+	destruct b.
+	Case "b = true".
+		reflexivity.
+	Case "b = false".
+		rewrite <- H. reflexivity. Qed.
+
+Theorem plus_0_r : forall n : nat, n + O = n.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = 0". reflexivity.
+	Case "n = S n'". simpl. rewrite -> IHn'. reflexivity. Qed.
+
+Theorem minus_diag : forall n,
+				minus n n = O.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = 0".
+		simpl. reflexivity.
+	Case "n = S n'".
+		simpl. rewrite -> IHn'. reflexivity. Qed.
+
+
+Theorem mult_0_r : forall n:nat,
+				n * O = O.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = 0".
+		reflexivity.
+	Case "n = S n'".
+		simpl. rewrite -> IHn'. reflexivity. Qed.
+
+Theorem plus_n_Sm : forall n m : nat,
+				S (n + m) = n + (S m).
+Proof.
+	intros n m. induction n as [| n'].
+	Case "n = 0".
+		reflexivity.
+	Case "n = S n'".
+		simpl. rewrite -> IHn'. reflexivity. Qed.
+
+Theorem plus_assoc : forall n m p : nat,
+					n + (m + p) = (n + m) + p.
+Proof.
+	intros n m p.
+	induction n as [| n'].
+	reflexivity.
+	simpl.
+	rewrite -> IHn'.
+	reflexivity. Qed.
+
+Theorem plus_distr : forall n m: nat, S (n + m) = n + (S m).
+Proof.
+	intros n m.  induction n as [| n'].
+	Case "n = 0".
+		reflexivity.
+	Case "n = S n'".
+		simpl. rewrite -> IHn'. reflexivity. Qed.
+
+Theorem mult_distr : forall n m: nat, n * ((S O) + m) = n * (S m).
+Proof.
+	intros n m.
+	induction n as [| n'].
+	reflexivity.
+	reflexivity.
+	Qed.
+
+Theorem plus_comm : forall n m : nat,
+	n + m = m + n.
+Proof.
+	intros n m.
+	induction n as [| n'].
+	Case "n = 0".
+		simpl.
+		rewrite -> plus_0_r.
+		reflexivity.
+	Case "n = S n'".
+		simpl.
+		rewrite -> IHn'.
+		rewrite -> plus_distr.
+		reflexivity. Qed.
+
+Fixpoint double (n:nat) :=
+	match n with
+		| O => O
+		| S n' => S (S (double n'))
+	end.
+
+Lemma double_plus : forall n, double n = n + n.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = 0".
+		reflexivity.
+	Case "n = S n'".
+		simpl. rewrite -> IHn'.
+		rewrite -> plus_distr. reflexivity.
+		Qed.
+
+Theorem beq_nat_refl : forall n : nat,
+	true = beq_nat n n.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = 0".
+		reflexivity.
+	Case "n = S n".
+		simpl. rewrite <- IHn'.
+		reflexivity. Qed.
+
+Theorem plus_rearrange: forall n m p q : nat,
+				(n + m) + (p + q) = (m + n) + (p + q).
+Proof.
+	intros n m p q.
+	assert(H: n + m = m + n).
+		Case "Proof by assertion".
+		rewrite -> plus_comm. reflexivity.
+	rewrite -> H. reflexivity. Qed.
+
+Theorem plus_swap : forall n m p: nat,
+				n + (m + p) = m + (n + p).
+Proof.
+	intros n m p.
+	rewrite -> plus_assoc.
+	assert(H: m + (n + p) = (m + n) + p).
+	rewrite -> plus_assoc.
+	reflexivity.
+	rewrite -> H.
+	assert(H2: m + n = n + m).
+	rewrite -> plus_comm.
+	reflexivity.
+	rewrite -> H2.
+	reflexivity.
+	Qed.
+
+Theorem plus_swap' : forall n m p: nat,
+				n + (m + p) = m + (n + p).
+Proof.
+	intros n m p.
+	rewrite -> plus_assoc.
+	assert(H: m + (n + p) = (m + n) + p).
+	rewrite -> plus_assoc.
+	reflexivity.
+	rewrite -> H.
+	replace (m + n) with (n + m).
+	rewrite -> plus_comm.
+	reflexivity.
+	rewrite -> plus_comm.
+	reflexivity.
+	Qed.
+
+Theorem mult_1_distr: forall m n: nat,
+				n * ((S O) + m) = n * (S O) + n * m.
+Proof.
+	intros n m.
+	rewrite -> mult_1.
+	rewrite -> plus_1_1.
+	simpl.
+	induction m as [|m'].
+	simpl.
+	reflexivity.
+	simpl.
+	rewrite -> plus_swap.
+	rewrite <- IHm'.
+	reflexivity.
+	Qed.
+
+Theorem mult_comm: forall m n : nat,
+				m * n = n * m.
+Proof.
+	intros m n.
+	induction n as [| n'].
+	Case "n = 0".
+		simpl.
+		rewrite -> mult_0_r.
+		reflexivity.
+	Case "n = S n'".
+		simpl.
+		rewrite <- mult_distr.
+		rewrite -> mult_1_distr.
+		rewrite -> mult_1.
+		rewrite -> IHn'.
+		reflexivity.
+		Qed.
+
+Theorem evenb_next : forall n : nat,
+				evenb n = evenb (S (S n)).
+Proof.
+	intros n.
+Admitted.
+
+Theorem negb_negb : forall n : bool,
+				n = negb (negb n).
+Proof.
+	intros n.
+	destruct n.
+	reflexivity.
+	reflexivity.
+	Qed.
+
+Theorem evenb_n_oddb_Sn : forall n : nat,
+				evenb n = negb (evenb (S n)).
+Proof.
+	intros n.
+	induction n as [|n'].
+	reflexivity.
+	assert(H: evenb n' = evenb (S (S n'))).
+	reflexivity.
+	rewrite <- H.
+	rewrite -> IHn'.
+	rewrite <- negb_negb.
+	reflexivity.
+	Qed.
+
+(*Fixpoint bad (n : nat) : bool :=
+	match n with
+		| O => true
+		| S O => bad (S n)
+		| S (S n') => bad n'
+	end.*)
+
+Theorem ble_nat_refl : forall n:nat,
+				true = ble_nat n n.
+Proof.
+	intros n.
+	induction n as [|n'].
+	Case "n = 0".
+		reflexivity.
+	Case "n = S n".
+		simpl.
+		rewrite <- IHn'.
+		reflexivity.
+	Qed.
+
+Theorem zero_nbeq_S : forall n: nat,
+				beq_nat O (S n) = false.
+Proof.
+	intros n.
+	reflexivity.
+	Qed.
+
+Theorem andb_false_r : forall b : bool,
+				andb b false = false.
+Proof.
+	intros b.
+	destruct b.
+	reflexivity.
+	reflexivity.
+	Qed.
+
+Theorem plus_ble_compat_1 : forall n m p : nat,
+				ble_nat n m = true -> ble_nat (p + n) (p + m) = true.
+Proof.
+	intros n m p.
+	intros H.
+	induction p.
+	Case "p = 0".
+		simpl.
+		rewrite -> H.
+		reflexivity.
+	Case "p = S p'".
+		simpl.
+		rewrite -> IHp.
+		reflexivity.
+		Qed.
+
+Theorem S_nbeq_0 : forall n:nat,
+				beq_nat (S n) O = false.
+Proof.
+	intros n.
+	reflexivity.
+	Qed.
+
+Theorem mult_1_1 : forall n:nat, (S O) * n = n.
+Proof.
+	intros n.
+	simpl.
+	rewrite -> plus_0_r.
+	reflexivity. Qed.
+
+Theorem all3_spec : forall b c : bool,
+	orb (andb b c)
+			(orb (negb b)
+			 		 (negb c))
+	= true.
+Proof.
+	intros b c.
+	destruct b.
+	destruct c.
+	reflexivity.
+	reflexivity.
+	reflexivity.
+	Qed.
+
+Lemma mult_plus_1 : forall n m : nat,
+			S(m + n) = m + (S n).
+Proof.
+	intros n m.
+	induction m.
+	reflexivity.
+	simpl.
+	rewrite -> IHm.
+	reflexivity.
+	Qed.
+
+Theorem mult_mult : forall n m : nat,
+	n * (S m) = n * m + n.
+Proof.
+	intros n m.
+	induction n.
+	reflexivity.
+	simpl.
+	rewrite -> IHn.
+	rewrite -> plus_assoc.
+	rewrite -> mult_plus_1.
+	reflexivity.
+	Qed.
+
+Theorem mult_plus_distr_r : forall n m p:nat,
+				(n + m) * p = (n * p) + (m * p).
+Proof.
+	intros n m p.
+	induction p.
+	rewrite -> mult_0_r.
+	rewrite -> mult_0_r.
+	rewrite -> mult_0_r.
+	reflexivity.
+	rewrite -> mult_mult.
+	rewrite -> mult_mult.
+	rewrite -> mult_mult.
+	rewrite -> IHp.
+	assert(H1: ((n * p) + n) + (m * p + m) = (n * p) + (n + (m * p + m))).
+	rewrite <- plus_assoc.
+	reflexivity.
+	rewrite -> H1.
+	assert(H2: (n + (m * p + m)) = (m * p + (n + m))).
+	rewrite -> plus_swap.
+	reflexivity.
+	rewrite -> H2.
+	assert(H3: (n * p) + (m * p + (n + m)) = ((n * p ) + (m * p)) + (n + m)).
+	rewrite -> plus_assoc.
+	reflexivity.
+	rewrite -> H3.
+	reflexivity.
+	Qed.
+
+Theorem mult_assoc : forall n m p : nat,
+				n * (m * p) = (n * m) * p.
+Proof.
+	intros n m p.
+	induction n.
+	simpl.
+	reflexivity.
+	simpl.
+	rewrite -> mult_plus_distr_r.
+	rewrite -> IHn.
+	reflexivity.
+	Qed.
+
+Inductive bin : Type :=
+	| BO : bin
+	| D : bin -> bin
+	| M : bin -> bin.
+
+Fixpoint incbin (n : bin) : bin :=
+	match n with
+		| BO => M (BO)
+		| D n' => M n'
+		| M n' => D (incbin n')
+	end.
+
+Fixpoint bin2un (n : bin) : nat :=
+	match n with
+		| BO => O
+		| D n' => double (bin2un n')
+		| M n' => S (double (bin2un n'))
+	end.
+
+Theorem bin_comm : forall n : bin,
+				bin2un(incbin n) = S (bin2un n).
+Proof.
+	intros n.
+	induction n.
+		reflexivity.
+		reflexivity.
+		simpl.
+		rewrite -> IHn.
+		reflexivity.
+	Qed.
+
+End Playground1.

samples/coq/Heap.v

@@ -0,0 +1,300 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** This file is deprecated, for a tree on list, use [Mergesort.v]. *)
+
+(** A development of Treesort on Heap trees. It has an average
+    complexity of O(n.log n) but of O(n²) in the worst case (e.g. if
+    the list is already sorted) *)
+
+(* G. Huet 1-9-95 uses Multiset *)
+
+Require Import List Multiset PermutSetoid Relations Sorting.
+
+Section defs.
+
+  (** * Trees and heap trees *)
+
+  (** ** Definition of trees over an ordered set *)
+
+  Variable A : Type.
+  Variable leA : relation A.
+  Variable eqA : relation A.
+
+  Let gtA (x y:A) := ~ leA x y.
+
+  Hypothesis leA_dec : forall x y:A, {leA x y} + {leA y x}.
+  Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+  Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y.
+  Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z.
+  Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y.
+
+  Hint Resolve leA_refl.
+  Hint Immediate eqA_dec leA_dec leA_antisym.
+
+  Let emptyBag := EmptyBag A.
+  Let singletonBag := SingletonBag _ eqA_dec.
+
+  Inductive Tree :=
+    | Tree_Leaf : Tree
+    | Tree_Node : A -> Tree -> Tree -> Tree.
+
+  (** [a] is lower than a Tree [T] if [T] is a Leaf
+      or [T] is a Node holding [b>a] *)
+
+  Definition leA_Tree (a:A) (t:Tree) :=
+    match t with
+      | Tree_Leaf => True
+      | Tree_Node b T1 T2 => leA a b
+    end.
+
+  Lemma leA_Tree_Leaf : forall a:A, leA_Tree a Tree_Leaf.
+  Proof.
+    simpl; auto with datatypes.
+  Qed.
+
+  Lemma leA_Tree_Node :
+    forall (a b:A) (G D:Tree), leA a b -> leA_Tree a (Tree_Node b G D).
+  Proof.
+    simpl; auto with datatypes.
+  Qed.
+
+
+  (** ** The heap property *)
+
+  Inductive is_heap : Tree -> Prop :=
+    | nil_is_heap : is_heap Tree_Leaf
+    | node_is_heap :
+      forall (a:A) (T1 T2:Tree),
+        leA_Tree a T1 ->
+        leA_Tree a T2 ->
+        is_heap T1 -> is_heap T2 -> is_heap (Tree_Node a T1 T2).
+
+  Lemma invert_heap :
+    forall (a:A) (T1 T2:Tree),
+      is_heap (Tree_Node a T1 T2) ->
+      leA_Tree a T1 /\ leA_Tree a T2 /\ is_heap T1 /\ is_heap T2.
+  Proof.
+    intros; inversion H; auto with datatypes.
+  Qed.
+
+  (* This lemma ought to be generated automatically by the Inversion tools *)
+  Lemma is_heap_rect :
+    forall P:Tree -> Type,
+      P Tree_Leaf ->
+      (forall (a:A) (T1 T2:Tree),
+	leA_Tree a T1 ->
+	leA_Tree a T2 ->
+	is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
+      forall T:Tree, is_heap T -> P T.
+  Proof.
+    simple induction T; auto with datatypes.
+    intros a G PG D PD PN.
+    elim (invert_heap a G D); auto with datatypes.
+    intros H1 H2; elim H2; intros H3 H4; elim H4; intros.
+    apply X0; auto with datatypes.
+  Qed.
+
+  (* This lemma ought to be generated automatically by the Inversion tools *)
+  Lemma is_heap_rec :
+    forall P:Tree -> Set,
+      P Tree_Leaf ->
+      (forall (a:A) (T1 T2:Tree),
+	leA_Tree a T1 ->
+	leA_Tree a T2 ->
+	is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
+      forall T:Tree, is_heap T -> P T.
+  Proof.
+    simple induction T; auto with datatypes.
+    intros a G PG D PD PN.
+    elim (invert_heap a G D); auto with datatypes.
+    intros H1 H2; elim H2; intros H3 H4; elim H4; intros.
+    apply X; auto with datatypes.
+  Qed.
+
+  Lemma low_trans :
+    forall (T:Tree) (a b:A), leA a b -> leA_Tree b T -> leA_Tree a T.
+  Proof.
+    simple induction T; auto with datatypes.
+    intros; simpl; apply leA_trans with b; auto with datatypes.
+  Qed.
+
+  (** ** Merging two sorted lists *)
+
+  Inductive merge_lem (l1 l2:list A) : Type :=
+    merge_exist :
+    forall l:list A,
+      Sorted leA l ->
+      meq (list_contents _ eqA_dec l)
+      (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) ->
+      (forall a, HdRel leA a l1 -> HdRel leA a l2 -> HdRel leA a l) ->
+      merge_lem l1 l2.
+  Require Import Morphisms.
+  
+  Instance: Equivalence (@meq A).
+  Proof. constructor; auto with datatypes. red. apply meq_trans. Defined.
+
+  Instance: Proper (@meq A ++> @meq _ ++> @meq _) (@munion A).
+  Proof. intros x y H x' y' H'. now apply meq_congr. Qed.
+  
+  Lemma merge :
+    forall l1:list A, Sorted leA l1 ->
+    forall l2:list A, Sorted leA l2 -> merge_lem l1 l2.
+  Proof.
+    fix 1; intros; destruct l1.
+    apply merge_exist with l2; auto with datatypes.
+    rename l1 into l.
+    revert l2 H0. fix 1. intros.
+    destruct l2 as [|a0 l0]. 
+    apply merge_exist with (a :: l); simpl; auto with datatypes. 
+    elim (leA_dec a a0); intros.
+
+    (* 1 (leA a a0) *)
+    apply Sorted_inv in H. destruct H.
+    destruct (merge l H (a0 :: l0) H0).
+    apply merge_exist with (a :: l1). clear merge merge0.
+      auto using cons_sort, cons_leA with datatypes.
+    simpl. rewrite m. now rewrite munion_ass. 
+    intros. apply cons_leA. 
+    apply (@HdRel_inv _ leA) with l; trivial with datatypes.
+
+    (* 2 (leA a0 a) *)
+    apply Sorted_inv in H0. destruct H0.
+    destruct (merge0 l0 H0). clear merge merge0.  
+    apply merge_exist with (a0 :: l1); 
+      auto using cons_sort, cons_leA with datatypes.
+    simpl; rewrite m. simpl. setoid_rewrite munion_ass at 1. rewrite munion_comm.
+    repeat rewrite munion_ass. setoid_rewrite munion_comm at 3. reflexivity.
+    intros. apply cons_leA. 
+    apply (@HdRel_inv _ leA) with l0; trivial with datatypes.
+  Qed.
+
+  (** ** From trees to multisets *)
+
+  (** contents of a tree as a multiset *)
+
+  (** Nota Bene : In what follows the definition of SingletonBag
+      in not used. Actually, we could just take as postulate:
+      [Parameter SingletonBag : A->multiset].  *)
+
+  Fixpoint contents (t:Tree) : multiset A :=
+    match t with
+      | Tree_Leaf => emptyBag
+      | Tree_Node a t1 t2 =>
+	munion (contents t1) (munion (contents t2) (singletonBag a))
+    end.
+
+
+  (** equivalence of two trees is equality of corresponding multisets *)
+  Definition equiv_Tree (t1 t2:Tree) := meq (contents t1) (contents t2).
+
+
+
+  (** * From lists to sorted lists *)
+
+  (** ** Specification of heap insertion *)
+
+  Inductive insert_spec (a:A) (T:Tree) : Type :=
+    insert_exist :
+    forall T1:Tree,
+      is_heap T1 ->
+      meq (contents T1) (munion (contents T) (singletonBag a)) ->
+      (forall b:A, leA b a -> leA_Tree b T -> leA_Tree b T1) ->
+      insert_spec a T.
+
+
+  Lemma insert : forall T:Tree, is_heap T -> forall a:A, insert_spec a T.
+  Proof.
+    simple induction 1; intros.
+    apply insert_exist with (Tree_Node a Tree_Leaf Tree_Leaf);
+      auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
+    simpl; unfold meq, munion; auto using node_is_heap with datatypes.
+    elim (leA_dec a a0); intros.
+    elim (X a0); intros.
+    apply insert_exist with (Tree_Node a T2 T0);
+      auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
+    simpl; apply treesort_twist1; trivial with datatypes.
+    elim (X a); intros T3 HeapT3 ConT3 LeA.
+    apply insert_exist with (Tree_Node a0 T2 T3);
+      auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
+    apply node_is_heap; auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
+    apply low_trans with a; auto with datatypes.
+    apply LeA; auto with datatypes.
+    apply low_trans with a; auto with datatypes.
+    simpl; apply treesort_twist2; trivial with datatypes.
+  Qed.
+
+
+  (** ** Building a heap from a list *)
+
+  Inductive build_heap (l:list A) : Type :=
+    heap_exist :
+    forall T:Tree,
+      is_heap T ->
+      meq (list_contents _ eqA_dec l) (contents T) -> build_heap l.
+
+  Lemma list_to_heap : forall l:list A, build_heap l.
+  Proof.
+    simple induction l.
+    apply (heap_exist nil Tree_Leaf); auto with datatypes.
+    simpl; unfold meq; exact nil_is_heap.
+    simple induction 1.
+    intros T i m; elim (insert T i a).
+    intros; apply heap_exist with T1; simpl; auto with datatypes.
+    apply meq_trans with (munion (contents T) (singletonBag a)).
+    apply meq_trans with (munion (singletonBag a) (contents T)).
+    apply meq_right; trivial with datatypes.
+    apply munion_comm.
+    apply meq_sym; trivial with datatypes.
+  Qed.
+
+
+  (** ** Building the sorted list *)
+
+  Inductive flat_spec (T:Tree) : Type :=
+    flat_exist :
+    forall l:list A,
+      Sorted leA l ->
+      (forall a:A, leA_Tree a T -> HdRel leA a l) ->
+      meq (contents T) (list_contents _ eqA_dec l) -> flat_spec T.
+
+  Lemma heap_to_list : forall T:Tree, is_heap T -> flat_spec T.
+  Proof.
+    intros T h; elim h; intros.
+    apply flat_exist with (nil (A:=A)); auto with datatypes.
+    elim X; intros l1 s1 i1 m1; elim X0; intros l2 s2 i2 m2.
+    elim (merge _ s1 _ s2); intros.
+    apply flat_exist with (a :: l); simpl; auto with datatypes.
+    apply meq_trans with
+      (munion (list_contents _ eqA_dec l1)
+	(munion (list_contents _ eqA_dec l2) (singletonBag a))).
+    apply meq_congr; auto with datatypes.
+    apply meq_trans with
+      (munion (singletonBag a)
+	(munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2))).
+    apply munion_rotate.
+    apply meq_right; apply meq_sym; trivial with datatypes.
+  Qed.
+
+
+  (** * Specification of treesort *)
+
+  Theorem treesort :
+    forall l:list A,
+    {m : list A | Sorted leA m & permutation _ eqA_dec l m}.
+  Proof.
+    intro l; unfold permutation.
+    elim (list_to_heap l).
+    intros.
+    elim (heap_to_list T); auto with datatypes.
+    intros.
+    exists l0; auto with datatypes.
+    apply meq_trans with (contents T); trivial with datatypes.
+  Qed.
+
+End defs.

samples/coq/Lists.v

@@ -0,0 +1,591 @@
+Require Export Basics.
+Module NatList.
+Import Playground1.
+
+Inductive natprod : Type :=
+	pair : nat -> nat -> natprod.
+
+Definition fst (p : natprod) : nat :=
+	match p with
+		| pair x y => x
+	end.
+
+Definition snd (p : natprod) : nat :=
+	match p with
+		| pair x y => y
+	end.
+
+Notation "( x , y )" := (pair x y).
+
+Definition swap_pair (p : natprod) : natprod :=
+	match p with
+			| (x, y) => (y, x)
+	end.
+
+Theorem surjective_pairing' : forall (n m : nat),
+	(n, m) = (fst (n, m), snd (n, m)).
+Proof.
+	reflexivity.  Qed.
+
+Theorem surjective_pairing : forall (p : natprod),
+	p = (fst p, snd p).
+Proof.
+	intros p.
+	destruct p as (n, m).
+	simpl.
+	reflexivity.
+	Qed.
+
+Theorem snd_fst_is_swap : forall (p : natprod),
+	(snd p, fst p) = swap_pair p.
+Proof.
+	intros p.
+	destruct p.
+	reflexivity.
+	Qed.
+
+Theorem fst_swap_is_snd : forall (p : natprod),
+	 fst (swap_pair p) = snd p.
+Proof.
+	intros p.
+	destruct p.
+	reflexivity.
+	Qed.
+
+Inductive natlist : Type :=
+	| nil : natlist
+	| cons : nat -> natlist -> natlist.
+
+Definition l_123 := cons (S O) (cons (S (S O)) (cons (S (S (S O))) nil)).
+
+Notation "x :: l" := (cons x l) (at level 60, right associativity).
+Notation "[ ]" := nil.
+Notation "[]" := nil.
+Notation "[ x , .. , y ]" := (cons x .. (cons y nil) ..).
+
+Fixpoint repeat (n count : nat) : natlist :=
+	match count with
+		| O => nil
+		| S count' => n :: (repeat n count')
+	end.
+
+Fixpoint length (l:natlist) : nat :=
+	match l with
+		| nil => O
+		| h :: t => S (length t)
+	end.
+
+Fixpoint app (l1 l2 : natlist) : natlist :=
+	match l1 with
+		| nil => l2
+		| h :: t => h :: (app t l2)
+	end.
+
+Notation "x ++ y" := (app x y) (right associativity, at level 60).
+
+(*
+Example test_app1: [1,2,3] ++ [4,5] = [1,2,3,4,5].
+Proof. reflexivity. Qed.
+Example test_app2: nil ++ [4,5] = [4,5].
+Proof. reflexivity. Qed.
+Example test_app3: [1,2,3] ++ [] = [1,2,3].
+Proof. reflexivity. Qed.
+*)
+
+Definition head (l : natlist) : nat :=
+	match l with
+		| nil => O
+		| h :: t => h
+	end.
+
+Definition tl (l : natlist) : natlist :=
+	match l with
+		| nil => nil
+		| h :: t => t
+	end.
+
+			(*
+Example test_tl: tl [1,2,3] = [2,3].
+Proof. reflexivity. Qed.
+*)
+
+Fixpoint nonzeros (l:natlist) : natlist :=
+	match l with
+		| nil => nil
+		| O :: r => nonzeros r
+		| n :: r => n :: (nonzeros r)
+	end.
+
+Example test_nonzeros: nonzeros [O,S O,O,S (S O), S (S (S O)),O,O] = [S O,S (S O), S (S (S O))].
+Proof. reflexivity. Qed.
+
+Fixpoint oddmembers (l:natlist) : natlist :=
+	match l with
+		| nil => nil
+		| n :: r => match (oddb n) with
+										| true => n :: (oddmembers r)
+										| false => oddmembers r
+								end
+	end.
+
+Example test_oddmembers: oddmembers [O, S O, O, S (S O), S (S (S O)), O, O] = [S O, S (S (S O))].
+Proof. reflexivity. Qed.
+
+Fixpoint countoddmembers (l:natlist) : nat :=
+		length (oddmembers l).
+
+Example test_countoddmembers2: countoddmembers [O, S (S O), S (S (S (S O)))] = O.
+Proof. reflexivity. Qed.
+
+Example test_countoddmembers3: countoddmembers [] = O.
+Proof. reflexivity. Qed.
+
+Fixpoint alternate (l1 l2 : natlist) : natlist :=
+		match l1 with
+				| nil => l2
+				| a :: r1 => match l2 with
+											| nil => l1
+											| b :: r2 => a :: b :: (alternate r1 r2)
+										end
+		end.
+
+Example test_alternative1: alternate [S O, S (S O), S (S (S O))] [S (S (S (S O))), S (S (S (S (S O)))), S (S (S (S (S (S O)))))] =
+		[S O, S (S (S (S O))), S (S O), S (S (S (S (S O)))), S (S (S O)), S (S (S (S (S (S O)))))].
+Proof. reflexivity. Qed.
+
+Definition bag := natlist.
+
+Fixpoint count (v : nat) (s: bag) : nat :=
+	match s with
+		| nil => O
+		| v' :: r => match (beq_nat v' v) with
+										| true => S (count v r)
+										| false => count v r
+								 end
+	end.
+
+Example test_count1: count (S O) [S O, S (S O), S (S (S O)), S O, S (S (S (S O))), S O] = S (S (S O)).
+Proof. reflexivity. Qed.
+
+Definition sum : bag -> bag -> bag := app.
+
+Example test_sum1: count (S O) (sum [S O, S (S O), S (S (S O))] [S O, S (S (S (S O))), S O]) = S (S (S O)).
+Proof. reflexivity. Qed.
+
+Definition add (v:nat) (s:bag) : bag := v :: s.
+
+Example test_add1: count (S O) (add (S O) [S O, S (S (S (S O))), S O]) = S (S (S O)).
+Proof. reflexivity. Qed.
+
+Definition member (v:nat) (s:bag) : bool :=
+	ble_nat (S O) (count v s).
+
+Example test_member1: member (S O) [S O, S (S (S (S O))), S O] = true.
+Proof. reflexivity. Qed.
+
+Example test_member2: member (S (S O)) [S O, S (S (S (S O))), S O] = false.
+Proof. reflexivity. Qed.
+
+Fixpoint remove_one (v:nat) (s:bag) : bag :=
+	match s with
+		| nil => nil
+		| v' :: r => match (beq_nat v v') with
+									| true => r
+									| false => v' :: (remove_one v r)
+								 end
+	end.
+
+Example test_remove_one1: count (S (S (S (S (S O)))))
+																(remove_one (S (S (S (S (S O)))))
+																[S (S O), S O, S (S (S (S (S O)))), S (S (S (S O))), S O]) = O.
+Proof. reflexivity. Qed.
+
+Fixpoint remove_all (v:nat) (s:bag) : bag :=
+	match s with
+		| nil => nil
+		| v' :: r => match (beq_nat v v') with
+										| true => remove_all v r
+										| false => v' :: (remove_all v r)
+								 end
+	end.
+
+Example test_remove_all1: count (S (S (S (S (S O)))))
+																(remove_all (S (S (S (S (S O)))))
+																[S (S O), S O, S (S (S (S (S O)))), S (S (S (S O))), S O]) = O.
+Proof. reflexivity. Qed.
+
+Fixpoint subset (s1:bag) (s2:bag) : bool :=
+		match s1 with
+			| nil => true
+			| v :: r => andb (member v s2)
+											 (subset r (remove_one v s2))
+		end.
+
+Definition test_subset1: subset [S O, S (S O)] [S (S O), S O, S (S (S (S O))), S O] = true.
+Proof. reflexivity. Qed.
+Definition test_subset2: subset [S O, S (S O), S (S O)] [S (S O), S O, S (S (S (S O))), S O] = false.
+Proof. reflexivity. Qed.
+
+Theorem bag_count_add : forall n t: nat, forall s : bag,
+				count n s = t -> count n (add n s) = S t.
+Proof.
+	intros n t s.
+	intros H.
+	induction s.
+	simpl.
+	rewrite <- beq_nat_refl.
+	rewrite <- H.
+	reflexivity.
+	rewrite <- H.
+	simpl.
+	rewrite <- beq_nat_refl.
+	reflexivity.
+Qed.
+
+Theorem nil_app : forall l:natlist,
+	[] ++ l = l.
+Proof.
+	reflexivity. Qed.
+
+Theorem tl_length_pred : forall l:natlist,
+	pred (length l) = length (tl l).
+Proof.
+	intros l. destruct l as [| n l'].
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons n l'".
+		reflexivity. Qed.
+
+Theorem app_ass:forall l1 l2 l3 : natlist,
+	(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
+Proof.
+	intros l1 l2 l3. induction l1 as [| n l1'].
+	Case "l1 = nil".
+		reflexivity.
+	Case "l1 = cons n l1'".
+		simpl. rewrite -> IHl1'. reflexivity. Qed.
+
+Theorem app_length: forall l1 l2 : natlist,
+	length (l1 ++ l2) = (length l1) + (length l2).
+Proof.
+	intros l1 l2. induction l1 as [| n l1'].
+	Case "l1 = nil".
+		reflexivity.
+	Case "l1 = cons".
+		simpl. rewrite -> IHl1'. reflexivity. Qed.
+
+Fixpoint snoc (l:natlist) (v:nat) : natlist :=
+	match l with
+		| nil => [v]
+		| h :: t => h :: (snoc t v)
+	end.
+
+Fixpoint rev (l:natlist) : natlist :=
+	match l with
+		| nil => nil
+		| h :: t => snoc (rev t) h
+	end.
+
+Example test_rev1: rev [S O, S (S O), S (S (S O))] = [S (S (S O)), S (S O), S O].
+Proof. reflexivity. Qed.
+
+Theorem length_snoc : forall n : nat, forall l : natlist,
+	length (snoc l n) = S (length l).
+Proof.
+	intros n l. induction l as [| n' l'].
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons n' l'".
+		simpl. rewrite -> IHl'. reflexivity. Qed.
+
+Theorem rev_length : forall l : natlist,
+	length (rev l) = length l.
+Proof.
+	intros l. induction l as [| n l'].
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons".
+		simpl. rewrite -> length_snoc.
+		rewrite -> IHl'. reflexivity. Qed.
+
+Theorem app_nil_end : forall l :natlist,
+	l ++ [] = l.
+Proof.
+	intros l.
+	induction l.
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons".
+		simpl. rewrite -> IHl. reflexivity. Qed.
+
+
+
+Theorem rev_snoc : forall l: natlist, forall n : nat,
+	rev (snoc l n) = n :: (rev l).
+Proof.
+	intros l n.
+	induction l.
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons".
+		simpl.
+		rewrite -> IHl.
+		reflexivity.
+		Qed.
+
+Theorem rev_involutive : forall l : natlist,
+	rev (rev l) = l.
+Proof.
+	intros l.
+	induction l.
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons".
+		simpl.
+		rewrite -> rev_snoc.
+		rewrite -> IHl.
+		reflexivity.
+		Qed.
+
+Theorem app_ass4 : forall l1 l2 l3 l4 : natlist,
+	l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
+Proof.
+	intros l1 l2 l3 l4.
+	rewrite -> app_ass.
+	rewrite -> app_ass.
+	reflexivity.
+	Qed.
+
+Theorem snoc_append : forall (l : natlist) (n : nat),
+	snoc l n = l ++ [n].
+Proof.
+	intros l n.
+	induction l.
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons".
+		simpl.
+		rewrite -> IHl.
+		reflexivity.
+		Qed.
+
+Theorem nonzeros_length : forall l1 l2 : natlist,
+	nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
+Proof.
+	intros l1 l2.
+	induction l1.
+	Case "l1 = nil".
+		reflexivity.
+	Case "l1 = cons".
+		simpl.
+		rewrite -> IHl1.
+		destruct n.
+		reflexivity.
+		reflexivity.
+		Qed.
+
+Theorem distr_rev : forall l1 l2 : natlist,
+	rev (l1 ++ l2) = (rev l2) ++ (rev l1).
+Proof.
+	intros l1 l2.
+	induction l1.
+	Case "l1 = nil".
+		simpl.
+		rewrite -> app_nil_end.
+		reflexivity.
+	Case "l1 = cons".
+		simpl.
+		rewrite -> IHl1.
+		simpl.
+		rewrite -> snoc_append.
+		rewrite -> snoc_append.
+		rewrite -> app_ass.
+		reflexivity.
+		Qed.
+
+Theorem count_number_nonzero : forall (s : bag),
+	ble_nat O (count (S O) (S O :: s)) = true.
+Proof.
+	intros s.
+	induction s.
+		reflexivity.
+		reflexivity.
+		Qed.
+
+Theorem ble_n_Sn : forall n,
+	ble_nat n (S n) = true.
+Proof.
+	intros n. induction n as [| n'].
+	Case "0".
+		simpl. reflexivity.
+	Case "S n'".
+		simpl. rewrite -> IHn'. reflexivity. Qed.
+
+Theorem remove_decreases_count: forall (s : bag),
+	ble_nat (count O (remove_one O s)) (count O s) = true.
+Proof.
+	intros s.
+	induction s.
+	Case "s = nil".
+		reflexivity.
+	Case "s = cons".
+		simpl.
+		induction n.
+		SCase "n = O".
+			simpl.  rewrite -> ble_n_Sn.
+			reflexivity.
+		SCase "n = S n'".
+			simpl.
+			rewrite -> IHs.
+			reflexivity.
+			Qed.
+
+Inductive natoption : Type :=
+	| Some : nat -> natoption
+	| None : natoption.
+
+Fixpoint index (n:nat) (l:natlist) : natoption :=
+	match l with
+		| nil => None
+		| a :: l' => if beq_nat n O then Some a else index (pred n) l'
+  end.
+
+Definition option_elim (o : natoption) (d : nat) : nat :=
+	match o with
+		| Some n' => n'
+		| None => d
+	end.
+
+Definition hd_opt (l : natlist) : natoption :=
+	match l with
+		| nil => None
+		| v :: r => Some v
+	end.
+
+Example test_hd_opt1 : hd_opt [] = None.
+Proof. reflexivity. Qed.
+Example test_hd_opt2 : hd_opt [S O] = Some (S O).
+Proof. reflexivity. Qed.
+
+Theorem option_elim_hd : forall l:natlist,
+	head l = option_elim (hd_opt l) O.
+Proof.
+	intros l.
+	destruct l.
+	reflexivity.
+	reflexivity.
+	Qed.
+
+Fixpoint beq_natlist (l1 l2 : natlist) : bool :=
+	match l1 with
+		| nil => match l2 with
+							| nil => true
+							| _ => false
+						 end
+		| v1 :: r1 => match l2 with
+									 | nil => false
+									 | v2 :: r2 => if beq_nat v1 v2 then beq_natlist r1 r2
+																 else false
+									end
+	end.
+
+Example test_beq_natlist1 : (beq_natlist nil nil = true).
+Proof. reflexivity. Qed.
+Example test_beq_natlist2 : (beq_natlist [S O, S (S O), S (S (S O))]
+																				 [S O, S (S O), S (S (S O))] = true).
+Proof. reflexivity. Qed.
+
+Theorem beq_natlist_refl : forall l:natlist,
+	beq_natlist l l = true.
+Proof.
+	intros l.
+	induction l.
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons".
+		simpl.
+		rewrite <- beq_nat_refl.
+		rewrite -> IHl.
+		reflexivity.
+	Qed.
+
+Theorem silly1 : forall (n m o p : nat),
+	n = m -> [n, o] = [n, p] -> [n, o] = [m, p].
+Proof.
+	intros n m o p eq1 eq2.
+	rewrite <- eq1.
+	apply eq2. Qed.
+
+Theorem silly2a : forall (n m : nat),
+	(n,n) = (m,m) ->
+		(forall (q r : nat), (q, q) = (r, r) -> [q] = [r]) ->
+			[n] = [m].
+Proof.
+	intros n m eq1 eq2.
+	apply eq2.
+	apply eq1.
+	Qed.
+
+Theorem silly_ex :
+	(forall n, evenb n = true -> oddb (S n) = true) ->
+	evenb (S (S (S O))) = true ->
+	oddb (S (S (S (S O)))) = true.
+Proof.
+	intros eq1 eq2.
+	apply eq1.
+	apply eq2.
+	Qed.
+
+Theorem silly3 : forall (n : nat),
+	true = beq_nat n (S (S (S (S (S O))))) ->
+	beq_nat (S (S n)) (S (S (S (S (S (S (S O))))))) = true.
+Proof.
+	intros n H.
+	symmetry.
+	apply H.
+	Qed.
+
+Theorem rev_exercise : forall (l l' : natlist),
+	l = rev l' -> l' = rev l.
+Proof.
+	intros l l' H.
+	rewrite -> H.
+	rewrite -> rev_involutive.
+	reflexivity.
+	Qed.
+
+Theorem beq_nat_sym : forall (n m:nat), forall (b: bool),
+	beq_nat n m = b -> beq_nat m n = b.
+Proof.
+	intros n.
+	induction n as [| n'].
+	Case "n = O".
+		intros m b eq1.
+		induction m.
+		SCase "m = 0".
+			apply eq1.
+		SCase "m = S m'".
+			apply eq1.
+	Case "n = S n'".
+		induction m.
+		SCase "m = 0".
+			intros b eq1.
+			apply eq1.
+		SCase "m = S m'".
+			intros b eq1.
+			apply IHn'.
+			apply eq1.
+		Qed.
+
+Theorem app_ass' : forall l1 l2 l3 : natlist,
+	(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
+Proof.
+	intros l1. induction l1 as [ | n l1'].
+	reflexivity.
+	simpl.
+	intros l2 l3.
+	rewrite -> IHl1'.
+	reflexivity.
+	Qed.
+
+End NatList.

samples/coq/PermutSetoid.v

@@ -0,0 +1,547 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import Omega Relations Multiset SetoidList.
+
+(** This file is deprecated, use [Permutation.v] instead.
+
+    Indeed, this file defines a notion of permutation based on
+    multisets (there exists a permutation between two lists iff every
+    elements have the same multiplicity in the two lists) which
+    requires a more complex apparatus (the equipment of the domain
+    with a decidable equality) than [Permutation] in [Permutation.v].
+
+    The relation between the two relations are in lemma
+    [permutation_Permutation].
+
+    File [Permutation] concerns Leibniz equality : it shows in particular
+    that [List.Permutation] and [permutation] are equivalent in this context.
+*)
+
+Set Implicit Arguments.
+
+Local Notation "[ ]" := nil.
+Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..).
+
+Section Permut.
+
+(** * From lists to multisets *)
+
+Variable A : Type.
+Variable eqA : relation A.
+Hypothesis eqA_equiv : Equivalence eqA.
+Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+
+Let emptyBag := EmptyBag A.
+Let singletonBag := SingletonBag _ eqA_dec.
+
+(** contents of a list *)
+
+Fixpoint list_contents (l:list A) : multiset A :=
+  match l with
+  | [] => emptyBag
+  | a :: l => munion (singletonBag a) (list_contents l)
+  end.
+
+Lemma list_contents_app :
+  forall l m:list A,
+    meq (list_contents (l ++ m)) (munion (list_contents l) (list_contents m)).
+Proof.
+  simple induction l; simpl; auto with datatypes.
+  intros.
+  apply meq_trans with
+    (munion (singletonBag a) (munion (list_contents l0) (list_contents m)));
+    auto with datatypes.
+Qed.
+
+(** * [permutation]: definition and basic properties *)
+
+Definition permutation (l m:list A) := meq (list_contents l) (list_contents m).
+
+Lemma permut_refl : forall l:list A, permutation l l.
+Proof.
+  unfold permutation; auto with datatypes.
+Qed.
+
+Lemma permut_sym :
+  forall l1 l2 : list A, permutation l1 l2 -> permutation l2 l1.
+Proof.
+  unfold permutation, meq; intros; symmetry; trivial.
+Qed.
+
+Lemma permut_trans :
+  forall l m n:list A, permutation l m -> permutation m n -> permutation l n.
+Proof.
+  unfold permutation; intros.
+  apply meq_trans with (list_contents m); auto with datatypes.
+Qed.
+
+Lemma permut_cons_eq :
+  forall l m:list A,
+    permutation l m -> forall a a', eqA a a' -> permutation (a :: l) (a' :: m).
+Proof.
+  unfold permutation; simpl; intros.
+  apply meq_trans with (munion (singletonBag a') (list_contents l)).
+  apply meq_left, meq_singleton; auto.
+  auto with datatypes.
+Qed.
+
+Lemma permut_cons :
+  forall l m:list A,
+    permutation l m -> forall a:A, permutation (a :: l) (a :: m).
+Proof.
+  unfold permutation; simpl; auto with datatypes.
+Qed.
+
+Lemma permut_app :
+  forall l l' m m':list A,
+    permutation l l' -> permutation m m' -> permutation (l ++ m) (l' ++ m').
+Proof.
+  unfold permutation; intros.
+  apply meq_trans with (munion (list_contents l) (list_contents m));
+    auto using permut_cons, list_contents_app with datatypes.
+  apply meq_trans with (munion (list_contents l') (list_contents m'));
+    auto using permut_cons, list_contents_app with datatypes.
+  apply meq_trans with (munion (list_contents l') (list_contents m));
+    auto using permut_cons, list_contents_app with datatypes.
+Qed.
+
+Lemma permut_add_inside_eq :
+  forall a a' l1 l2 l3 l4, eqA a a' ->
+    permutation (l1 ++ l2) (l3 ++ l4) ->
+    permutation (l1 ++ a :: l2) (l3 ++ a' :: l4).
+Proof.
+  unfold permutation, meq in *; intros.
+  specialize H0 with a0.
+  repeat rewrite list_contents_app in *; simpl in *.
+  destruct (eqA_dec a a0) as [Ha|Ha]; rewrite H in Ha;
+    decide (eqA_dec a' a0) with Ha; simpl; auto with arith.
+  do 2 rewrite <- plus_n_Sm; f_equal; auto.
+Qed.
+
+Lemma permut_add_inside :
+  forall a l1 l2 l3 l4,
+    permutation (l1 ++ l2) (l3 ++ l4) ->
+    permutation (l1 ++ a :: l2) (l3 ++ a :: l4).
+Proof.
+  unfold permutation, meq in *; intros.
+  generalize (H a0); clear H.
+  do 4 rewrite list_contents_app.
+  simpl.
+  destruct (eqA_dec a a0); simpl; auto with arith.
+  do 2 rewrite <- plus_n_Sm; f_equal; auto.
+Qed.
+
+Lemma permut_add_cons_inside_eq :
+  forall a a' l l1 l2, eqA a a' ->
+    permutation l (l1 ++ l2) ->
+    permutation (a :: l) (l1 ++ a' :: l2).
+Proof.
+  intros;
+  replace (a :: l) with ([] ++ a :: l); trivial;
+    apply permut_add_inside_eq; trivial.
+Qed.
+
+Lemma permut_add_cons_inside :
+  forall a l l1 l2,
+    permutation l (l1 ++ l2) ->
+    permutation (a :: l) (l1 ++ a :: l2).
+Proof.
+  intros;
+    replace (a :: l) with ([] ++ a :: l); trivial;
+	apply permut_add_inside; trivial.
+Qed.
+
+Lemma permut_middle :
+  forall (l m:list A) (a:A), permutation (a :: l ++ m) (l ++ a :: m).
+Proof.
+  intros; apply permut_add_cons_inside; auto using permut_sym, permut_refl.
+Qed.
+
+Lemma permut_sym_app :
+  forall l1 l2, permutation (l1 ++ l2) (l2 ++ l1).
+Proof.
+  intros l1 l2;
+    unfold permutation, meq;
+	intro a; do 2 rewrite list_contents_app; simpl;
+	  auto with arith.
+Qed.
+
+Lemma permut_rev :
+  forall l, permutation l (rev l).
+Proof.
+  induction l.
+  simpl; trivial using permut_refl.
+  simpl.
+  apply permut_add_cons_inside.
+  rewrite <- app_nil_end. trivial.
+Qed.
+
+(** * Some inversion results. *)
+Lemma permut_conv_inv :
+  forall e l1 l2, permutation (e :: l1) (e :: l2) -> permutation l1 l2.
+Proof.
+  intros e l1 l2; unfold permutation, meq; simpl; intros H a;
+    generalize (H a); apply plus_reg_l.
+Qed.
+
+Lemma permut_app_inv1 :
+  forall l l1 l2, permutation (l1 ++ l) (l2 ++ l) -> permutation l1 l2.
+Proof.
+  intros l l1 l2; unfold permutation, meq; simpl;
+    intros H a; generalize (H a); clear H.
+  do 2 rewrite list_contents_app.
+  simpl.
+  intros; apply plus_reg_l with (multiplicity (list_contents l) a).
+  rewrite plus_comm; rewrite H; rewrite plus_comm.
+  trivial.
+Qed.
+
+(** we can use [multiplicity] to define [InA] and [NoDupA]. *)
+
+Fact if_eqA_then : forall a a' (B:Type)(b b':B),
+ eqA a a' -> (if eqA_dec a a' then b else b') = b.
+Proof.
+  intros. destruct eqA_dec as [_|NEQ]; auto.
+  contradict NEQ; auto.
+Qed.
+
+Lemma permut_app_inv2 :
+  forall l l1 l2, permutation (l ++ l1) (l ++ l2) -> permutation l1 l2.
+Proof.
+  intros l l1 l2; unfold permutation, meq; simpl;
+    intros H a; generalize (H a); clear H.
+  do 2 rewrite list_contents_app.
+  simpl.
+  intros; apply plus_reg_l with (multiplicity (list_contents l) a).
+  trivial.
+Qed.
+
+Lemma permut_remove_hd_eq :
+  forall l l1 l2 a b, eqA a b ->
+    permutation (a :: l) (l1 ++ b :: l2) -> permutation l (l1 ++ l2).
+Proof.
+  unfold permutation, meq; simpl; intros l l1 l2 a b Heq H a0.
+  specialize H with a0.
+  rewrite list_contents_app in *; simpl in *.
+  apply plus_reg_l with (if eqA_dec a a0 then 1 else 0).
+  rewrite H; clear H.
+  symmetry; rewrite plus_comm, <- ! plus_assoc; f_equal.
+  rewrite plus_comm.
+  destruct (eqA_dec a a0) as [Ha|Ha]; rewrite Heq in Ha;
+    decide (eqA_dec b a0) with Ha; reflexivity.
+Qed.
+
+Lemma permut_remove_hd :
+  forall l l1 l2 a,
+    permutation (a :: l) (l1 ++ a :: l2) -> permutation l (l1 ++ l2).
+Proof.
+  eauto using permut_remove_hd_eq, Equivalence_Reflexive.
+Qed.
+
+Fact if_eqA_else : forall a a' (B:Type)(b b':B),
+ ~eqA a a' -> (if eqA_dec a a' then b else b') = b'.
+Proof.
+  intros. decide (eqA_dec a a') with H; auto.
+Qed.
+
+Fact if_eqA_refl : forall a (B:Type)(b b':B),
+ (if eqA_dec a a then b else b') = b.
+Proof.
+  intros; apply (decide_left (eqA_dec a a)); auto with *.
+Qed.
+
+(** PL: Inutilisable dans un rewrite sans un change prealable. *)
+
+Global Instance if_eqA (B:Type)(b b':B) :
+ Proper (eqA==>eqA==>@eq _) (fun x y => if eqA_dec x y then b else b').
+Proof.
+ intros x x' Hxx' y y' Hyy'.
+ intros; destruct (eqA_dec x y) as [H|H];
+  destruct (eqA_dec x' y') as [H'|H']; auto.
+ contradict H'; transitivity x; auto with *; transitivity y; auto with *.
+ contradict H; transitivity x'; auto with *; transitivity y'; auto with *.
+Qed.
+
+Fact if_eqA_rewrite_l : forall a1 a1' a2 (B:Type)(b b':B),
+ eqA a1 a1' -> (if eqA_dec a1 a2 then b else b') =
+               (if eqA_dec a1' a2 then b else b').
+Proof.
+ intros; destruct (eqA_dec a1 a2) as [A1|A1];
+  destruct (eqA_dec a1' a2) as [A1'|A1']; auto.
+ contradict A1'; transitivity a1; eauto with *.
+ contradict A1; transitivity a1'; eauto with *.
+Qed.
+
+Fact if_eqA_rewrite_r : forall a1 a2 a2' (B:Type)(b b':B),
+ eqA a2 a2' -> (if eqA_dec a1 a2 then b else b') =
+               (if eqA_dec a1 a2' then b else b').
+Proof.
+ intros; destruct (eqA_dec a1 a2) as [A2|A2];
+  destruct (eqA_dec a1 a2') as [A2'|A2']; auto.
+ contradict A2'; transitivity a2; eauto with *.
+ contradict A2; transitivity a2'; eauto with *.
+Qed.
+
+
+Global Instance multiplicity_eqA (l:list A) :
+ Proper (eqA==>@eq _) (multiplicity (list_contents l)).
+Proof.
+  intros x x' Hxx'.
+  induction l as [|y l Hl]; simpl; auto.
+  rewrite (@if_eqA_rewrite_r y x x'); auto.
+Qed.
+
+Lemma multiplicity_InA :
+  forall l a, InA eqA a l <-> 0 < multiplicity (list_contents l) a.
+Proof.
+  induction l.
+  simpl.
+  split; inversion 1.
+  simpl.
+  intros a'; split; intros H. inversion_clear H.
+  apply (decide_left (eqA_dec a a')); auto with *.
+  destruct (eqA_dec a a'); auto with *. simpl; rewrite <- IHl; auto.
+  destruct (eqA_dec a a'); auto with *. right. rewrite IHl; auto.
+Qed.
+
+Lemma multiplicity_InA_O :
+  forall l a, ~ InA eqA a l -> multiplicity (list_contents l) a = 0.
+Proof.
+  intros l a; rewrite multiplicity_InA;
+    destruct (multiplicity (list_contents l) a); auto with arith.
+  destruct 1; auto with arith.
+Qed.
+
+Lemma multiplicity_InA_S :
+  forall l a, InA eqA a l -> multiplicity (list_contents l) a >= 1.
+Proof.
+  intros l a; rewrite multiplicity_InA; auto with arith.
+Qed.
+
+Lemma multiplicity_NoDupA : forall l,
+  NoDupA eqA l <-> (forall a, multiplicity (list_contents l) a <= 1).
+Proof.
+  induction l.
+  simpl.
+  split; auto with arith.
+  split; simpl.
+  inversion_clear 1.
+  rewrite IHl in H1.
+  intros; destruct (eqA_dec a a0) as [EQ|NEQ]; simpl; auto with *.
+  rewrite <- EQ.
+  rewrite multiplicity_InA_O; auto.
+  intros; constructor.
+  rewrite multiplicity_InA.
+  specialize (H a).
+  rewrite if_eqA_refl in H.
+  clear IHl; omega.
+  rewrite IHl; intros.
+  specialize (H a0). omega.
+Qed.
+
+(** Permutation is compatible with InA. *)
+Lemma permut_InA_InA :
+  forall l1 l2 e, permutation l1 l2 -> InA eqA e l1 -> InA eqA e l2.
+Proof.
+  intros l1 l2 e.
+  do 2 rewrite multiplicity_InA.
+  unfold permutation, meq.
+  intros H;rewrite H; auto.
+Qed.
+
+Lemma permut_cons_InA :
+  forall l1 l2 e, permutation (e :: l1) l2 -> InA eqA e l2.
+Proof.
+  intros; apply (permut_InA_InA (e:=e) H); auto with *.
+Qed.
+
+(** Permutation of an empty list. *)
+Lemma permut_nil :
+  forall l, permutation l [] -> l = [].
+Proof.
+  intro l; destruct l as [ | e l ]; trivial.
+  assert (InA eqA e (e::l)) by (auto with *).
+  intro Abs; generalize (permut_InA_InA Abs H).
+  inversion 1.
+Qed.
+
+(** Permutation for short lists. *)
+
+Lemma permut_length_1:
+  forall a b, permutation [a] [b] -> eqA a b.
+Proof.
+  intros a b; unfold permutation, meq.
+  intro P; specialize (P b); simpl in *.
+  rewrite if_eqA_refl in *.
+  destruct (eqA_dec a b); simpl; auto; discriminate.
+Qed.
+
+Lemma permut_length_2 :
+  forall a1 b1 a2 b2, permutation [a1; b1] [a2; b2] ->
+    (eqA a1 a2) /\ (eqA b1 b2) \/ (eqA a1 b2) /\ (eqA a2 b1).
+Proof.
+  intros a1 b1 a2 b2 P.
+  assert (H:=permut_cons_InA P).
+  inversion_clear H.
+  left; split; auto.
+  apply permut_length_1.
+  red; red; intros.
+  specialize (P a). simpl in *.
+  rewrite (@if_eqA_rewrite_l a1 a2 a) in P by auto. omega.
+  right.
+  inversion_clear H0; [|inversion H].
+  split; auto.
+  apply permut_length_1.
+  red; red; intros.
+  specialize (P a); simpl in *.
+  rewrite (@if_eqA_rewrite_l a1 b2 a) in P by auto. omega.
+Qed.
+
+(** Permutation is compatible with length. *)
+Lemma permut_length :
+  forall l1 l2, permutation l1 l2 -> length l1 = length l2.
+Proof.
+  induction l1; intros l2 H.
+  rewrite (permut_nil (permut_sym H)); auto.
+  assert (H0:=permut_cons_InA H).
+  destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))).
+  subst l2.
+  rewrite app_length.
+  simpl; rewrite <- plus_n_Sm; f_equal.
+  rewrite <- app_length.
+  apply IHl1.
+  apply permut_remove_hd with b.
+  apply permut_trans with (a::l1); auto.
+  revert H1; unfold permutation, meq; simpl.
+  intros; f_equal; auto.
+  rewrite (@if_eqA_rewrite_l a b a0); auto.
+Qed.
+
+Lemma NoDupA_equivlistA_permut :
+  forall l l', NoDupA eqA l -> NoDupA eqA l' ->
+    equivlistA eqA l l' -> permutation l l'.
+Proof.
+  intros.
+  red; unfold meq; intros.
+  rewrite multiplicity_NoDupA in H, H0.
+  generalize (H a) (H0 a) (H1 a); clear H H0 H1.
+  do 2 rewrite multiplicity_InA.
+  destruct 3; omega.
+Qed.
+
+End Permut.
+
+Section Permut_map.
+
+Variables A B : Type.
+
+Variable eqA : relation A.
+Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+Hypothesis eqA_equiv : Equivalence eqA.
+
+Variable eqB : B->B->Prop.
+Hypothesis eqB_dec : forall x y:B, { eqB x y }+{ ~eqB x y }.
+Hypothesis eqB_trans : Transitive eqB.
+
+(** Permutation is compatible with map. *)
+
+Lemma permut_map :
+  forall f,
+    (Proper (eqA==>eqB) f) ->
+    forall l1 l2, permutation _ eqA_dec l1 l2 ->
+      permutation _ eqB_dec (map f l1) (map f l2).
+Proof.
+  intros f; induction l1.
+  intros l2 P; rewrite (permut_nil eqA_equiv (permut_sym P)); apply permut_refl.
+  intros l2 P.
+  simpl.
+  assert (H0:=permut_cons_InA eqA_equiv P).
+  destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))).
+  subst l2.
+  rewrite map_app.
+  simpl.
+  apply permut_trans with (f b :: map f l1).
+  revert H1; unfold permutation, meq; simpl.
+  intros; f_equal; auto.
+  destruct (eqB_dec (f b) a0) as [H2|H2];
+    destruct (eqB_dec (f a) a0) as [H3|H3]; auto.
+  destruct H3; transitivity (f b); auto with *.
+  destruct H2; transitivity (f a); auto with *.
+  apply permut_add_cons_inside.
+  rewrite <- map_app.
+  apply IHl1; auto.
+  apply permut_remove_hd with b; trivial.
+  apply permut_trans with (a::l1); auto.
+  revert H1; unfold permutation, meq; simpl.
+  intros; f_equal; auto.
+  rewrite (@if_eqA_rewrite_l _ _ eqA_equiv eqA_dec a b a0); auto.
+Qed.
+
+End Permut_map.
+
+Require Import Permutation.
+
+Section Permut_permut.
+
+Variable A : Type.
+
+Variable eqA : relation A.
+Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+Hypothesis eqA_equiv : Equivalence eqA.
+
+Lemma Permutation_impl_permutation : forall l l',
+  Permutation l l' -> permutation _ eqA_dec l l'.
+Proof.
+  induction 1.
+    apply permut_refl.
+    apply permut_cons; auto using Equivalence_Reflexive.
+    change (x :: y :: l) with ([x] ++ y :: l);
+      apply permut_add_cons_inside; simpl;
+      apply permut_cons_eq; auto using Equivalence_Reflexive, permut_refl.
+    apply permut_trans with l'; trivial.
+Qed.
+
+Lemma permut_eqA : forall l l', Forall2 eqA l l' -> permutation _ eqA_dec l l'.
+Proof.
+  induction 1.
+    apply permut_refl.
+    apply permut_cons_eq; trivial.
+Qed.
+
+Lemma permutation_Permutation : forall l l',
+  permutation _ eqA_dec l l' <->
+  exists l'', Permutation l l'' /\ Forall2 eqA l'' l'.
+Proof.
+  split; intro H.
+  (* -> *)
+  induction l in l', H |- *.
+    exists []; apply permut_sym, permut_nil in H as ->; auto using Forall2.
+    pose proof H as H'.
+    apply permut_cons_InA, InA_split in H
+      as (l1 & y & l2 & Heq & ->); trivial.
+    apply permut_remove_hd_eq, IHl in H'
+      as (l'' & IHP & IHA); clear IHl; trivial.
+    apply Forall2_app_inv_r in IHA as (l1'' & l2'' & Hl1 & Hl2 & ->).
+    exists (l1'' ++ a :: l2''); split.
+      apply Permutation_cons_app; trivial.
+      apply Forall2_app, Forall2_cons; trivial.
+  (* <- *)
+  destruct H as (l'' & H & Heq).
+  apply permut_trans with l''.
+    apply Permutation_impl_permutation; trivial.
+    apply permut_eqA; trivial.
+Qed.
+
+End Permut_permut.
+
+(* begin hide *)
+(** For compatibilty *)
+Notation permut_right := permut_cons (only parsing).
+Notation permut_tran := permut_trans (only parsing).
+(* end hide *)

samples/coq/Permutation.v

@@ -0,0 +1,644 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*********************************************************************)
+(** * List permutations as a composition of adjacent transpositions  *)
+(*********************************************************************)
+
+(* Adapted in May 2006 by Jean-Marc Notin from initial contents by
+   Laurent Théry (Huffmann contribution, October 2003) *)
+
+Require Import List Setoid Compare_dec Morphisms.
+Import ListNotations. (* For notations [] and [a;b;c] *)
+Set Implicit Arguments.
+
+Section Permutation.
+
+Variable A:Type.
+
+Inductive Permutation : list A -> list A -> Prop :=
+| perm_nil: Permutation [] []
+| perm_skip x l l' : Permutation l l' -> Permutation (x::l) (x::l')
+| perm_swap x y l : Permutation (y::x::l) (x::y::l)
+| perm_trans l l' l'' :
+    Permutation l l' -> Permutation l' l'' -> Permutation l l''.
+
+Local Hint Constructors Permutation.
+
+(** Some facts about [Permutation] *)
+
+Theorem Permutation_nil : forall (l : list A), Permutation [] l -> l = [].
+Proof.
+  intros l HF.
+  remember (@nil A) as m in HF.
+  induction HF; discriminate || auto.
+Qed.
+
+Theorem Permutation_nil_cons : forall (l : list A) (x : A),
+ ~ Permutation nil (x::l).
+Proof.
+  intros l x HF.
+  apply Permutation_nil in HF; discriminate.
+Qed.
+
+(** Permutation over lists is a equivalence relation *)
+
+Theorem Permutation_refl : forall l : list A, Permutation l l.
+Proof.
+  induction l; constructor. exact IHl.
+Qed.
+
+Theorem Permutation_sym : forall l l' : list A,
+ Permutation l l' -> Permutation l' l.
+Proof.
+  intros l l' Hperm; induction Hperm; auto.
+  apply perm_trans with (l':=l'); assumption.
+Qed.
+
+Theorem Permutation_trans : forall l l' l'' : list A,
+ Permutation l l' -> Permutation l' l'' -> Permutation l l''.
+Proof.
+  exact perm_trans.
+Qed.
+
+End Permutation.
+
+Hint Resolve Permutation_refl perm_nil perm_skip.
+
+(* These hints do not reduce the size of the problem to solve and they
+   must be used with care to avoid combinatoric explosions *)
+
+Local Hint Resolve perm_swap perm_trans.
+Local Hint Resolve Permutation_sym Permutation_trans.
+
+(* This provides reflexivity, symmetry and transitivity and rewriting
+   on morphims to come *)
+
+Instance Permutation_Equivalence A : Equivalence (@Permutation A) | 10 := {
+  Equivalence_Reflexive := @Permutation_refl A ;
+  Equivalence_Symmetric := @Permutation_sym A ;
+  Equivalence_Transitive := @Permutation_trans A }.
+
+Instance Permutation_cons A :
+ Proper (Logic.eq ==> @Permutation A ==> @Permutation A) (@cons A) | 10.
+Proof.
+  repeat intro; subst; auto using perm_skip.
+Qed.
+
+Section Permutation_properties.
+
+Variable A:Type.
+
+Implicit Types a b : A.
+Implicit Types l m : list A.
+
+(** Compatibility with others operations on lists *)
+
+Theorem Permutation_in : forall (l l' : list A) (x : A),
+ Permutation l l' -> In x l -> In x l'.
+Proof.
+  intros l l' x Hperm; induction Hperm; simpl; tauto.
+Qed.
+
+Global Instance Permutation_in' :
+ Proper (Logic.eq ==> @Permutation A ==> iff) (@In A) | 10.
+Proof.
+  repeat red; intros; subst; eauto using Permutation_in.
+Qed.
+
+Lemma Permutation_app_tail : forall (l l' tl : list A),
+ Permutation l l' -> Permutation (l++tl) (l'++tl).
+Proof.
+  intros l l' tl Hperm; induction Hperm as [|x l l'|x y l|l l' l'']; simpl; auto.
+  eapply Permutation_trans with (l':=l'++tl); trivial.
+Qed.
+
+Lemma Permutation_app_head : forall (l tl tl' : list A),
+ Permutation tl tl' -> Permutation (l++tl) (l++tl').
+Proof.
+  intros l tl tl' Hperm; induction l;
+   [trivial | repeat rewrite <- app_comm_cons; constructor; assumption].
+Qed.
+
+Theorem Permutation_app : forall (l m l' m' : list A),
+ Permutation l l' -> Permutation m m' -> Permutation (l++m) (l'++m').
+Proof.
+  intros l m l' m' Hpermll' Hpermmm';
+   induction Hpermll' as [|x l l'|x y l|l l' l''];
+    repeat rewrite <- app_comm_cons; auto.
+  apply Permutation_trans with (l' := (x :: y :: l ++ m));
+   [idtac | repeat rewrite app_comm_cons; apply Permutation_app_head]; trivial.
+  apply Permutation_trans with (l' := (l' ++ m')); try assumption.
+  apply Permutation_app_tail; assumption.
+Qed.
+
+Global Instance Permutation_app' :
+ Proper (@Permutation A ==> @Permutation A ==> @Permutation A) (@app A) | 10.
+Proof.
+  repeat intro; now apply Permutation_app.
+Qed.
+
+Lemma Permutation_add_inside : forall a (l l' tl tl' : list A),
+  Permutation l l' -> Permutation tl tl' ->
+  Permutation (l ++ a :: tl) (l' ++ a :: tl').
+Proof.
+  intros; apply Permutation_app; auto.
+Qed.
+
+Lemma Permutation_cons_append : forall (l : list A) x,
+  Permutation (x :: l) (l ++ x :: nil).
+Proof. induction l; intros; auto. simpl. rewrite <- IHl; auto. Qed.
+Local Hint Resolve Permutation_cons_append.
+
+Theorem Permutation_app_comm : forall (l l' : list A),
+  Permutation (l ++ l') (l' ++ l).
+Proof.
+  induction l as [|x l]; simpl; intro l'.
+  rewrite app_nil_r; trivial. rewrite IHl.
+  rewrite app_comm_cons, Permutation_cons_append.
+  now rewrite <- app_assoc.
+Qed.
+Local Hint Resolve Permutation_app_comm.
+
+Theorem Permutation_cons_app : forall (l l1 l2:list A) a,
+  Permutation l (l1 ++ l2) -> Permutation (a :: l) (l1 ++ a :: l2).
+Proof.
+  intros l l1 l2 a H. rewrite H.
+  rewrite app_comm_cons, Permutation_cons_append.
+  now rewrite <- app_assoc.
+Qed.
+Local Hint Resolve Permutation_cons_app.
+
+Theorem Permutation_middle : forall (l1 l2:list A) a,
+  Permutation (a :: l1 ++ l2) (l1 ++ a :: l2).
+Proof.
+  auto.
+Qed.
+Local Hint Resolve Permutation_middle.
+
+Theorem Permutation_rev : forall (l : list A), Permutation l (rev l).
+Proof.
+  induction l as [| x l]; simpl; trivial. now rewrite IHl at 1.
+Qed.
+
+Global Instance Permutation_rev' :
+ Proper (@Permutation A ==> @Permutation A) (@rev A) | 10.
+Proof.
+  repeat intro; now rewrite <- 2 Permutation_rev.
+Qed.
+
+Theorem Permutation_length : forall (l l' : list A),
+ Permutation l l' -> length l = length l'.
+Proof.
+  intros l l' Hperm; induction Hperm; simpl; auto. now transitivity (length l').
+Qed.
+
+Global Instance Permutation_length' :
+ Proper (@Permutation A ==> Logic.eq) (@length A) | 10.
+Proof.
+  exact Permutation_length.
+Qed.
+
+Theorem Permutation_ind_bis :
+ forall P : list A -> list A -> Prop,
+   P [] [] ->
+   (forall x l l', Permutation l l' -> P l l' -> P (x :: l) (x :: l')) ->
+   (forall x y l l', Permutation l l' -> P l l' -> P (y :: x :: l) (x :: y :: l')) ->
+   (forall l l' l'', Permutation l l' -> P l l' -> Permutation l' l'' -> P l' l'' -> P l l'') ->
+   forall l l', Permutation l l' -> P l l'.
+Proof.
+  intros P Hnil Hskip Hswap Htrans.
+  induction 1; auto.
+  apply Htrans with (x::y::l); auto.
+  apply Hswap; auto.
+  induction l; auto.
+  apply Hskip; auto.
+  apply Hskip; auto.
+  induction l; auto.
+  eauto.
+Qed.
+
+Ltac break_list l x l' H :=
+  destruct l as [|x l']; simpl in *;
+  injection H; intros; subst; clear H.
+
+Theorem Permutation_nil_app_cons : forall (l l' : list A) (x : A),
+ ~ Permutation nil (l++x::l').
+Proof.
+  intros l l' x HF.
+  apply Permutation_nil in HF. destruct l; discriminate.
+Qed.
+
+Theorem Permutation_app_inv : forall (l1 l2 l3 l4:list A) a,
+  Permutation (l1++a::l2) (l3++a::l4) -> Permutation (l1++l2) (l3 ++ l4).
+Proof.
+  intros l1 l2 l3 l4 a; revert l1 l2 l3 l4.
+  set (P l l' :=
+       forall l1 l2 l3 l4, l=l1++a::l2 -> l'=l3++a::l4 ->
+       Permutation (l1++l2) (l3++l4)).
+  cut (forall l l', Permutation l l' -> P l l').
+  intros H; intros; eapply H; eauto.
+  apply (Permutation_ind_bis P); unfold P; clear P.
+  - (* nil *)
+    intros; now destruct l1.
+  - (* skip *)
+    intros x l l' H IH; intros.
+    break_list l1 b l1' H0; break_list l3 c l3' H1.
+    auto.
+    now rewrite H.
+    now rewrite <- H.
+    now rewrite (IH _ _ _ _ eq_refl eq_refl).
+  - (* swap *)
+    intros x y l l' Hp IH; intros.
+    break_list l1 b l1' H; break_list l3 c l3' H0.
+    auto.
+    break_list l3' b l3'' H.
+    auto.
+    constructor. now rewrite Permutation_middle.
+    break_list l1' c l1'' H1.
+    auto.
+    constructor. now rewrite Permutation_middle.
+    break_list l3' d l3'' H; break_list l1' e l1'' H1.
+    auto.
+    rewrite perm_swap. constructor. now rewrite Permutation_middle.
+    rewrite perm_swap. constructor. now rewrite Permutation_middle.
+    now rewrite perm_swap, (IH _ _ _ _ eq_refl eq_refl).
+  - (*trans*)
+    intros.
+    destruct (In_split a l') as (l'1,(l'2,H6)).
+    rewrite <- H.
+    subst l.
+    apply in_or_app; right; red; auto.
+    apply perm_trans with (l'1++l'2).
+    apply (H0 _ _ _ _ H3 H6).
+    apply (H2 _ _ _ _ H6 H4).
+Qed.
+
+Theorem Permutation_cons_inv l l' a :
+ Permutation (a::l) (a::l') -> Permutation l l'.
+Proof.
+  intro H; exact (Permutation_app_inv [] l [] l' a H).
+Qed.
+
+Theorem Permutation_cons_app_inv l l1 l2 a :
+ Permutation (a :: l) (l1 ++ a :: l2) -> Permutation l (l1 ++ l2).
+Proof.
+  intro H; exact (Permutation_app_inv [] l l1 l2 a H).
+Qed.
+
+Theorem Permutation_app_inv_l : forall l l1 l2,
+ Permutation (l ++ l1) (l ++ l2) -> Permutation l1 l2.
+Proof.
+  induction l; simpl; auto.
+  intros.
+  apply IHl.
+  apply Permutation_cons_inv with a; auto.
+Qed.
+
+Theorem Permutation_app_inv_r : forall l l1 l2,
+ Permutation (l1 ++ l) (l2 ++ l) -> Permutation l1 l2.
+Proof.
+  induction l.
+  intros l1 l2; do 2 rewrite app_nil_r; auto.
+  intros.
+  apply IHl.
+  apply Permutation_app_inv with a; auto.
+Qed.
+
+Lemma Permutation_length_1_inv: forall a l, Permutation [a] l -> l = [a].
+Proof.
+  intros a l H; remember [a] as m in H.
+  induction H; try (injection Heqm as -> ->; clear Heqm);
+    discriminate || auto.
+  apply Permutation_nil in H as ->; trivial.
+Qed.
+
+Lemma Permutation_length_1: forall a b, Permutation [a] [b] -> a = b.
+Proof.
+  intros a b H.
+  apply Permutation_length_1_inv in H; injection H as ->; trivial.
+Qed.
+
+Lemma Permutation_length_2_inv :
+  forall a1 a2 l, Permutation [a1;a2] l -> l = [a1;a2] \/ l = [a2;a1].
+Proof.
+  intros a1 a2 l H; remember [a1;a2] as m in H.
+  revert a1 a2 Heqm.
+  induction H; intros; try (injection Heqm; intros; subst; clear Heqm);
+    discriminate || (try tauto).
+  apply Permutation_length_1_inv in H as ->; left; auto.
+  apply IHPermutation1 in Heqm as [H1|H1]; apply IHPermutation2 in H1 as ();
+    auto.
+Qed.
+
+Lemma Permutation_length_2 :
+  forall a1 a2 b1 b2, Permutation [a1;a2] [b1;b2] ->
+    a1 = b1 /\ a2 = b2 \/ a1 = b2 /\ a2 = b1.
+Proof.
+  intros a1 b1 a2 b2 H.
+  apply Permutation_length_2_inv in H as [H|H]; injection H as -> ->; auto.
+Qed.
+
+Let in_middle l l1 l2 (a:A) : l = l1 ++ a :: l2 ->
+ forall x, In x l <-> a = x \/ In x (l1++l2).
+Proof.
+ intros; subst; rewrite !in_app_iff; simpl. tauto.
+Qed.
+
+Lemma NoDup_cardinal_incl (l l' : list A) : NoDup l -> NoDup l' ->
+  length l = length l' -> incl l l' -> incl l' l.
+Proof.
+ intros N. revert l'. induction N as [|a l Hal Hl IH].
+ - destruct l'; now auto.
+ - intros l' Hl' E H x Hx.
+   assert (Ha : In a l') by (apply H; simpl; auto).
+   destruct (in_split _ _ Ha) as (l1 & l2 & H12). clear Ha.
+   rewrite in_middle in Hx; eauto.
+   destruct Hx as [Hx|Hx]; [left|right]; auto.
+   apply (IH (l1++l2)); auto.
+   * apply NoDup_remove_1 with a; rewrite <- H12; auto.
+   * apply eq_add_S.
+     simpl in E; rewrite E, H12, !app_length; simpl; auto with arith.
+   * intros y Hy. assert (Hy' : In y l') by (apply H; simpl; auto).
+     rewrite in_middle in Hy'; eauto.
+     destruct Hy'; auto. subst y; intuition.
+Qed.
+
+Lemma NoDup_Permutation l l' : NoDup l -> NoDup l' ->
+  (forall x:A, In x l <-> In x l') -> Permutation l l'.
+Proof.
+ intros N. revert l'. induction N as [|a l Hal Hl IH].
+ - destruct l'; simpl; auto.
+   intros Hl' H. exfalso. rewrite (H a); auto.
+ - intros l' Hl' H.
+   assert (Ha : In a l') by (apply H; simpl; auto).
+   destruct (In_split _ _ Ha) as (l1 & l2 & H12).
+   rewrite H12.
+   apply Permutation_cons_app.
+   apply IH; auto.
+   * apply NoDup_remove_1 with a; rewrite <- H12; auto.
+   * intro x. split; intros Hx.
+     + assert (Hx' : In x l') by (apply H; simpl; auto).
+       rewrite in_middle in Hx'; eauto.
+       destruct Hx'; auto. subst; intuition.
+     + assert (Hx' : In x l') by (rewrite (in_middle l1 l2 a); eauto).
+       rewrite <- H in Hx'. destruct Hx'; auto.
+       subst. destruct (NoDup_remove_2 _ _ _ Hl' Hx).
+Qed.
+
+Lemma NoDup_Permutation_bis l l' : NoDup l -> NoDup l' ->
+  length l = length l' -> incl l l' -> Permutation l l'.
+Proof.
+ intros. apply NoDup_Permutation; auto.
+ split; auto. apply NoDup_cardinal_incl; auto.
+Qed.
+
+Lemma Permutation_NoDup l l' : Permutation l l' -> NoDup l -> NoDup l'.
+Proof.
+ induction 1; auto.
+ * inversion_clear 1; constructor; eauto using Permutation_in.
+ * inversion_clear 1 as [|? ? H1 H2]. inversion_clear H2; simpl in *.
+   constructor. simpl; intuition. constructor; intuition.
+Qed.
+
+Global Instance Permutation_NoDup' :
+ Proper (@Permutation A ==> iff) (@NoDup A) | 10.
+Proof.
+  repeat red; eauto using Permutation_NoDup.
+Qed.
+
+End Permutation_properties.
+
+Section Permutation_map.
+
+Variable A B : Type.
+Variable f : A -> B.
+
+Lemma Permutation_map l l' :
+  Permutation l l' -> Permutation (map f l) (map f l').
+Proof.
+ induction 1; simpl; eauto.
+Qed.
+
+Global Instance Permutation_map' :
+  Proper (@Permutation A ==> @Permutation B) (map f) | 10.
+Proof.
+  exact Permutation_map.
+Qed.
+
+End Permutation_map.
+
+Section Injection.
+
+Definition injective {A B} (f : A->B) :=
+ forall x y, f x = f y -> x = y.
+
+Lemma injective_map_NoDup {A B} (f:A->B) (l:list A) :
+ injective f -> NoDup l -> NoDup (map f l).
+Proof.
+ intros Hf. induction 1 as [|x l Hx Hl IH]; simpl; constructor; trivial.
+ rewrite in_map_iff. intros (y & Hy & Hy'). apply Hf in Hy. now subst.
+Qed.
+
+Lemma injective_bounded_surjective n f :
+ injective f ->
+ (forall x, x < n -> f x < n) ->
+ (forall y, y < n -> exists x, x < n /\ f x = y).
+Proof.
+ intros Hf H.
+ set (l := seq 0 n).
+ assert (P : incl (map f l) l).
+ { intros x. rewrite in_map_iff. intros (y & <- & Hy').
+   unfold l in *. rewrite in_seq in *. simpl in *.
+   destruct Hy' as (_,Hy'). auto with arith. }
+ assert (P' : incl l (map f l)).
+ { unfold l.
+   apply NoDup_cardinal_incl; auto using injective_map_NoDup, seq_NoDup.
+   now rewrite map_length. }
+ intros x Hx.
+ assert (Hx' : In x l) by (unfold l; rewrite in_seq; auto with arith).
+ apply P' in Hx'.
+ rewrite in_map_iff in Hx'. destruct Hx' as (y & Hy & Hy').
+ exists y; split; auto. unfold l in *; rewrite in_seq in Hy'.
+ destruct Hy'; auto with arith.
+Qed.
+
+Lemma nat_bijection_Permutation n f :
+ injective f -> (forall x, x < n -> f x < n) ->
+ let l := seq 0 n in Permutation (map f l) l.
+Proof.
+ intros Hf BD.
+ apply NoDup_Permutation_bis; auto using injective_map_NoDup, seq_NoDup.
+ * now rewrite map_length.
+ * intros x. rewrite in_map_iff. intros (y & <- & Hy').
+   rewrite in_seq in *. simpl in *.
+   destruct Hy' as (_,Hy'). auto with arith.
+Qed.
+
+End Injection.
+
+Section Permutation_alt.
+Variable A:Type.
+Implicit Type a : A.
+Implicit Type l : list A.
+
+(** Alternative characterization of permutation
+    via [nth_error] and [nth] *)
+
+Let adapt f n :=
+ let m := f (S n) in if le_lt_dec m (f 0) then m else pred m.
+
+Let adapt_injective f : injective f -> injective (adapt f).
+Proof.
+ unfold adapt. intros Hf x y EQ.
+ destruct le_lt_dec as [LE|LT]; destruct le_lt_dec as [LE'|LT'].
+ - now apply eq_add_S, Hf.
+ - apply Lt.le_lt_or_eq in LE.
+   destruct LE as [LT|EQ']; [|now apply Hf in EQ'].
+   unfold lt in LT. rewrite EQ in LT.
+   rewrite <- (Lt.S_pred _ _ LT') in LT.
+   elim (Lt.lt_not_le _ _ LT' LT).
+ - apply Lt.le_lt_or_eq in LE'.
+   destruct LE' as [LT'|EQ']; [|now apply Hf in EQ'].
+   unfold lt in LT'. rewrite <- EQ in LT'.
+   rewrite <- (Lt.S_pred _ _ LT) in LT'.
+   elim (Lt.lt_not_le _ _ LT LT').
+ - apply eq_add_S, Hf.
+   now rewrite (Lt.S_pred _ _ LT), (Lt.S_pred _ _ LT'), EQ.
+Qed.
+
+Let adapt_ok a l1 l2 f : injective f -> length l1 = f 0 ->
+ forall n, nth_error (l1++a::l2) (f (S n)) = nth_error (l1++l2) (adapt f n).
+Proof.
+ unfold adapt. intros Hf E n.
+ destruct le_lt_dec as [LE|LT].
+ - apply Lt.le_lt_or_eq in LE.
+   destruct LE as [LT|EQ]; [|now apply Hf in EQ].
+   rewrite <- E in LT.
+   rewrite 2 nth_error_app1; auto.
+ - rewrite (Lt.S_pred _ _ LT) at 1.
+   rewrite <- E, (Lt.S_pred _ _ LT) in LT.
+   rewrite 2 nth_error_app2; auto with arith.
+   rewrite <- Minus.minus_Sn_m; auto with arith.
+Qed.
+
+Lemma Permutation_nth_error l l' :
+ Permutation l l' <->
+  (length l = length l' /\
+   exists f:nat->nat,
+    injective f /\ forall n, nth_error l' n = nth_error l (f n)).
+Proof.
+ split.
+ { intros P.
+   split; [now apply Permutation_length|].
+   induction P.
+   - exists (fun n => n).
+     split; try red; auto.
+   - destruct IHP as (f & Hf & Hf').
+     exists (fun n => match n with O => O | S n => S (f n) end).
+     split; try red.
+     * intros [|y] [|z]; simpl; now auto.
+     * intros [|n]; simpl; auto.
+   - exists (fun n => match n with 0 => 1 | 1 => 0 | n => n end).
+     split; try red.
+     * intros [|[|z]] [|[|t]]; simpl; now auto.
+     * intros [|[|n]]; simpl; auto.
+   - destruct IHP1 as (f & Hf & Hf').
+     destruct IHP2 as (g & Hg & Hg').
+     exists (fun n => f (g n)).
+     split; try red.
+     * auto.
+     * intros n. rewrite <- Hf'; auto. }
+ { revert l. induction l'.
+   - intros [|l] (E & _); now auto.
+   - intros l (E & f & Hf & Hf').
+     simpl in E.
+     assert (Ha : nth_error l (f 0) = Some a)
+      by (symmetry; apply (Hf' 0)).
+     destruct (nth_error_split l (f 0) Ha) as (l1 & l2 & L12 & L1).
+     rewrite L12. rewrite <- Permutation_middle. constructor.
+     apply IHl'; split; [|exists (adapt f); split].
+     * revert E. rewrite L12, !app_length. simpl.
+       rewrite <- plus_n_Sm. now injection 1.
+     * now apply adapt_injective.
+     * intro n. rewrite <- (adapt_ok a), <- L12; auto.
+       apply (Hf' (S n)). }
+Qed.
+
+Lemma Permutation_nth_error_bis l l' :
+ Permutation l l' <->
+  exists f:nat->nat,
+    injective f /\
+    (forall n, n < length l -> f n < length l) /\
+    (forall n, nth_error l' n = nth_error l (f n)).
+Proof.
+ rewrite Permutation_nth_error; split.
+ - intros (E & f & Hf & Hf').
+   exists f. do 2 (split; trivial).
+   intros n Hn.
+   destruct (Lt.le_or_lt (length l) (f n)) as [LE|LT]; trivial.
+   rewrite <- nth_error_None, <- Hf', nth_error_None, <- E in LE.
+   elim (Lt.lt_not_le _ _ Hn LE).
+ - intros (f & Hf & Hf2 & Hf3); split; [|exists f; auto].
+   assert (H : length l' <= length l') by auto with arith.
+   rewrite <- nth_error_None, Hf3, nth_error_None in H.
+   destruct (Lt.le_or_lt (length l) (length l')) as [LE|LT];
+    [|apply Hf2 in LT; elim (Lt.lt_not_le _ _ LT H)].
+   apply Lt.le_lt_or_eq in LE. destruct LE as [LT|EQ]; trivial.
+   rewrite <- nth_error_Some, Hf3, nth_error_Some in LT.
+   destruct (injective_bounded_surjective Hf Hf2 LT) as (y & Hy & Hy').
+   apply Hf in Hy'. subst y. elim (Lt.lt_irrefl _ Hy).
+Qed.
+
+Lemma Permutation_nth l l' d :
+ Permutation l l' <->
+  (let n := length l in
+   length l' = n /\
+   exists f:nat->nat,
+    (forall x, x < n -> f x < n) /\
+    (forall x y, x < n -> y < n -> f x = f y -> x = y) /\
+    (forall x, x < n -> nth x l' d = nth (f x) l d)).
+Proof.
+ split.
+ - intros H.
+   assert (E := Permutation_length H).
+   split; auto.
+   apply Permutation_nth_error_bis in H.
+   destruct H as (f & Hf & Hf2 & Hf3).
+   exists f. split; [|split]; auto.
+   intros n Hn. rewrite <- 2 nth_default_eq. unfold nth_default.
+    now rewrite Hf3.
+ - intros (E & f & Hf1 & Hf2 & Hf3).
+   rewrite Permutation_nth_error.
+   split; auto.
+   exists (fun n => if le_lt_dec (length l) n then n else f n).
+   split.
+   * intros x y.
+     destruct le_lt_dec as [LE|LT];
+      destruct le_lt_dec as [LE'|LT']; auto.
+     + apply Hf1 in LT'. intros ->.
+       elim (Lt.lt_irrefl (f y)). eapply Lt.lt_le_trans; eauto.
+     + apply Hf1 in LT. intros <-.
+       elim (Lt.lt_irrefl (f x)). eapply Lt.lt_le_trans; eauto.
+   * intros n.
+     destruct le_lt_dec as [LE|LT].
+     + assert (LE' : length l' <= n) by (now rewrite E).
+       rewrite <- nth_error_None in LE, LE'. congruence.
+     + assert (LT' : n < length l') by (now rewrite E).
+       specialize (Hf3 n LT). rewrite <- 2 nth_default_eq in Hf3.
+       unfold nth_default in Hf3.
+       apply Hf1 in LT.
+       rewrite <- nth_error_Some in LT, LT'.
+       do 2 destruct nth_error; congruence.
+Qed.
+
+End Permutation_alt.
+
+(* begin hide *)
+Notation Permutation_app_swap := Permutation_app_comm (only parsing).
+(* end hide *)

samples/coq/Poly.v

@@ -0,0 +1,875 @@
+Require Export Lists.
+Require Export Basics.
+
+Import Playground1.
+
+Inductive list (X : Type) : Type :=
+	| nil : list X
+	| cons : X -> list X -> list X.
+
+Fixpoint length (X:Type) (l:list X) : nat :=
+	match l with
+		| nil => O
+		| cons h t => S (length X t)
+	end.
+
+Fixpoint app (X : Type) (l1 l2 : list X)
+										: (list X) :=
+	match l1 with
+		| nil => l2
+		| cons h t => cons X h (app X t l2)
+	end.
+
+Fixpoint snoc (X:Type) (l:list X) (v:X) : (list X) :=
+	match l with
+		| nil => cons X v (nil X)
+		| cons h t => cons X h (snoc X t v)
+	end.
+
+Fixpoint rev (X:Type) (l:list X) : list X :=
+	match l with
+		| nil => nil X
+		| cons h t => snoc X (rev X t) h
+	end.
+
+
+Implicit Arguments nil [[X]].
+Implicit Arguments cons [[X]].
+Implicit Arguments length [[X]].
+Implicit Arguments app [[X]].
+Implicit Arguments rev [[X]].
+Implicit Arguments snoc [[X]].
+
+Definition list123 := cons 1 (cons 2 (cons 3 (nil))).
+
+Notation "x :: y" := (cons x y) (at level 60, right associativity).
+Notation "[]" := nil.
+Notation "[ x , .. , y ]" := (cons x .. (cons y []) ..).
+Notation "x ++ y" := (app x y) (at level 60, right associativity).
+
+Fixpoint repeat (X : Type) (n : X) (count : nat) : list X :=
+	match count with
+		| O => nil
+		| S count' => n :: (repeat _ n count')
+	end.
+
+Example test_repeat1:
+	repeat bool true (S (S O)) = [true, true].
+Proof. reflexivity. Qed.
+
+Theorem nil_app : forall X:Type, forall l:list X,
+	app [] l = l.
+Proof.
+	reflexivity.
+	Qed.
+
+Theorem rev_snoc : forall X : Type,
+									 forall v : X,
+									 forall s : list X,
+	rev (snoc s v) = v :: (rev s).
+Proof.
+	intros X v s.
+	induction s.
+		reflexivity.
+		simpl.
+		rewrite -> IHs.
+		reflexivity.
+		Qed.
+
+Theorem snoc_with_append : forall X : Type,
+													 forall l1 l2 : list X,
+													 forall v : X,
+	snoc (l1 ++ l2) v = l1 ++ (snoc l2 v).
+Proof.
+	intros X l1 l2 v.
+	induction l1.
+		reflexivity.
+		simpl.
+		rewrite -> IHl1.
+		reflexivity.
+		Qed.
+
+Inductive prod (X Y : Type) : Type :=
+	pair : X -> Y -> prod X Y.
+
+Implicit Arguments pair [X Y].
+
+Notation "( x , y )" := (pair x y).
+Notation "X * Y" := (prod X Y) : type_scope.
+
+Definition fst (X Y : Type) (p : X * Y) : X :=
+	match p with (x,y) => x end.
+Definition snd (X Y : Type) (p : X * Y) : Y :=
+	match p with (x,y) => y end.
+
+Fixpoint combine (X Y : Type) (lx : list X) (ly : list Y)
+			: list (X * Y) :=
+	match lx, ly with
+		| [], _ => []
+		| _,[] => []
+		| x::tx, y::ty => (x,y) :: (combine _ _ tx ty)
+	end.
+
+Implicit Arguments combine [X Y].
+
+Fixpoint split {X Y: Type} (s : list (X * Y)) : (list X)*(list Y) :=
+	match s with
+		| nil => (nil, nil)
+		| (x,y) :: tp => match split tp with
+											| (lx, ly) => (x :: lx, y :: ly)
+										 end
+	end.
+
+Inductive option (X : Type) : Type :=
+	| Some : X -> option X
+	| None : option X.
+
+Implicit Arguments Some [X].
+Implicit Arguments None [X].
+
+Fixpoint index (X : Type) (n : nat)
+							 (l : list X) : option X :=
+	match n with
+		| O => match l with
+								| nil => None
+								| x :: xs => Some x
+					 end
+		| S n' => match l with
+									| nil => None
+									| x :: xs => index X n' xs
+							end
+	end.
+
+Definition hd_opt (X : Type) (l : list X) : option X :=
+		match l with
+			| nil => None
+			| x :: xs => Some x
+		end.
+
+Implicit Arguments hd_opt [X].
+
+Example test_hd_opt1 : hd_opt [S O, S (S O)] = Some (S O).
+Proof. reflexivity. Qed.
+Example test_hd_opt2 : hd_opt [[S O], [S (S O)]] = Some [S O].
+Proof. reflexivity. Qed.
+
+Definition plus3 := plus (S (S (S O))).
+
+Definition prod_curry {X Y Z : Type}
+		(f : X * Y -> Z) (x : X) (y : Y) : Z := f (x,y).
+
+Definition prod_uncurry {X Y Z : Type}
+	(f : X -> Y -> Z) (p : X * Y) : Z :=
+	f (fst X Y p) (snd X Y p).
+
+Theorem uncurry_uncurry : forall (X Y Z : Type) (f : X -> Y -> Z) x y,
+				prod_curry (prod_uncurry f) x y = f x y.
+Proof.
+	reflexivity.
+Qed.
+
+Theorem curry_uncurry : forall (X Y Z : Type) (f : (X * Y) -> Z)
+	(p : X * Y),
+		prod_uncurry (prod_curry f) p = f p.
+Proof.
+	destruct p.
+	reflexivity.
+	Qed.
+
+Fixpoint filter (X : Type) (test : X -> bool) (l:list X)
+				: (list X) :=
+		match l with
+			| [] => []
+		  | h :: t => if test h then h :: (filter _ test t)
+									else filter _ test t
+		end.
+
+Definition countoddmembers' (l:list nat) : nat :=
+	length (filter _ oddb l).
+
+Definition partition (X : Type) (test : X -> bool) (l : list X)
+							: list X * list X :=
+	(filter _ test l, filter _ (fun el => negb (test el)) l).
+
+Example test_partition1: partition _ oddb [S O, S (S O), S (S (S O)), S (S (S (S O))), S (S (S (S (S O))))] = ([S O, S (S (S O)), S (S (S (S (S O))))], [S (S O), S (S (S (S O)))]).
+Proof. reflexivity. Qed.
+
+Fixpoint map {X Y : Type} (f : X -> Y) (l : list X) : (list Y ) :=
+		match l with
+			| [] => []
+			| h :: t => (f h) :: (map f t)
+		end.
+
+Example test_map1: map (plus (S (S (S O)))) [S (S O), O, S (S O)] = [S (S (S (S (S O)))), S (S (S O)), S (S (S (S (S O))))].
+Proof. reflexivity. Qed.
+
+ Theorem map_rev_1 : forall (X Y: Type) (f: X -> Y) (l : list X) (x : X),
+ 		map f (snoc l x) = snoc (map f l) (f x).
+Proof.
+	intros X Y f l x.
+	induction l.
+	reflexivity.
+	simpl.
+	rewrite -> IHl.
+	reflexivity.
+	Qed.
+
+Theorem map_rev : forall (X Y : Type) (f : X -> Y) (l : list X),
+				map f (rev l) = rev (map f l).
+Proof.
+	intros X Y f l.
+	induction l.
+		reflexivity.
+		simpl.
+		rewrite <- IHl.
+		rewrite -> map_rev_1.
+		reflexivity.
+		Qed.
+
+Fixpoint flat_map {X Y : Type} (f : X -> list Y) (l : list X)
+			: (list Y) :=
+	match l with
+		| [] => []
+		| x :: xs => (f x) ++ (flat_map f xs)
+	end.
+
+Definition map_option {X Y : Type} (f : X -> Y) (xo : option X)
+		: option Y :=
+	match xo with
+		| None => None
+		| Some x => Some (f x)
+	end.
+
+Fixpoint fold {X Y: Type} (f: X -> Y -> Y) (l:list X) (b:Y) : Y :=
+	match l with
+		| nil => b
+		| h :: t => f h (fold f t b)
+	end.
+
+Example fold_example : fold andb [true, true, false, true] true = false.
+Proof. reflexivity. Qed.
+
+Definition constfun {X : Type} (x: X) : nat -> X :=
+	fun (k:nat) => x.
+
+Definition ftrue := constfun true.
+Example constfun_example : ftrue O = true.
+Proof. reflexivity. Qed.
+
+Definition override {X : Type} (f: nat -> X) (k:nat) (x:X) : nat->X :=
+	fun (k':nat) => if beq_nat k k' then x else f k'.
+
+Definition fmostlytrue := override (override ftrue (S O) false) (S (S (S O))) false.
+
+Example override_example1 : fmostlytrue O = true.
+Proof. reflexivity. Qed.
+Example override_example2 : fmostlytrue (S O) = false.
+Proof. reflexivity. Qed.
+Example override_example3 : fmostlytrue (S (S O)) = true.
+Proof. reflexivity. Qed.
+Example override_example4 : fmostlytrue (S (S (S O))) = false.
+Proof. reflexivity. Qed.
+
+Theorem override_example : forall (b: bool),
+	(override (constfun b) (S (S (S O))) true) (S (S O)) = b.
+Proof.
+	reflexivity.
+Qed.
+
+Theorem unfold_example_bad : forall m n,
+	(S (S (S O))) + n = m ->
+	plus3 n = m.
+Proof.
+	intros m n H.
+	unfold plus3.
+	rewrite -> H.
+	reflexivity.
+	Qed.
+
+Theorem override_eq : forall {X : Type} x k (f : nat -> X),
+	(override f k x) k = x.
+Proof.
+	intros X x k f.
+	unfold override.
+	rewrite <- beq_nat_refl.
+	reflexivity.
+	Qed.
+
+Theorem override_neq : forall {X : Type} x1 x2 k1 k2 (f : nat->X),
+	f k1 = x1 ->
+		beq_nat k2 k1 = false ->
+			(override f k2 x2) k1 = x1.
+Proof.
+	intros X x1 x2 k1 k2 f eq1 eq2.
+	unfold override.
+	rewrite -> eq2.
+	rewrite -> eq1.
+	reflexivity.
+Qed.
+
+Theorem eq_add_S : forall (n m : nat),
+	S n = S m ->
+		n = m.
+Proof.
+	intros n m eq.
+	inversion eq.
+	reflexivity.
+Qed.
+
+Theorem silly4 : forall (n m : nat),
+	[n] = [m] ->
+		n = m.
+Proof.
+	intros n o eq.
+	inversion eq.
+	reflexivity.
+Qed.
+
+Theorem silly5 : forall (n m o : nat),
+	[n,m] = [o,o] ->
+		[n] = [m].
+Proof.
+	intros n m o eq.
+	inversion eq.
+	reflexivity.
+Qed.
+
+Theorem sillyex1 : forall (X : Type) (x y z : X) (l j : list X),
+	x :: y :: l = z :: j ->
+		y :: l = x :: j ->
+			x = y.
+Proof.
+	intros X x y z l j.
+	intros eq1 eq2.
+	inversion eq1.
+	inversion eq2.
+	symmetry.
+	rewrite -> H0.
+	reflexivity.
+Qed.
+
+Theorem silly6 : forall (n : nat),
+	S n = O ->
+		(S (S O)) + (S (S O)) = (S (S (S (S (S O))))).
+Proof.
+	intros n contra.
+	inversion contra.
+Qed.
+
+Theorem silly7 : forall (n m : nat),
+				false = true ->
+					[n] = [m].
+Proof.
+	intros n m contra.
+	inversion contra.
+Qed.
+
+Theorem sillyex2 : forall (X : Type) (x y z : X) (l j : list X),
+	x :: y :: l = [] ->
+		y :: l = z :: j ->
+			x = z.
+Proof.
+	intros X x y z l j contra.
+	inversion contra.
+	Qed.
+
+Theorem beq_nat_eq : forall n m,
+	true = beq_nat n m -> n = m.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = O".
+		intros m. destruct m as [| m'].
+		SCase "m = 0". reflexivity.
+		SCase "m = S m'". simpl. intros contra. inversion contra.
+	Case "n = S n'".
+		intros m. destruct m as [| m'].
+		SCase "m = 0". simpl. intros contra. inversion contra.
+		SCase "m = S m'". simpl. intros H.
+			assert(n' = m') as Hl.
+				SSCase "Proof of assertion". apply IHn'. apply H.
+			rewrite -> Hl. reflexivity.
+Qed.
+
+Theorem beq_nat_eq' : forall m n,
+				beq_nat n m = true -> n = m.
+Proof.
+	intros m. induction m as [| m'].
+	Case "m = O".
+		destruct n.
+		SCase "n = O".
+			reflexivity.
+		SCase "n = S n'".
+			simpl. intros contra. inversion contra.
+	Case "m = S m'".
+		simpl.
+		destruct n.
+		SCase "n = O".
+			simpl. intros contra. inversion contra.
+		SCase "n = S n'".
+			simpl. intros H.
+			assert (n = m') as Hl.
+				apply IHm'.
+				apply H.
+			rewrite -> Hl.
+			reflexivity.
+Qed.
+
+Theorem length_snoc' : forall (X : Type) (v : X)
+(l : list X) (n : nat),
+	length l = n ->
+	length (snoc l v) = S n.
+	Proof.
+	intros X v l. induction l as [| v' l'].
+	Case "l = []". intros n eq. rewrite <- eq. reflexivity.
+	Case "l = v' :: l'". intros n eq. simpl. destruct n as [| n'].
+	SCase "n = 0". inversion eq.
+	SCase "n = S n'".
+	assert (length (snoc l' v) = S n').
+	SSCase "Proof of assertion". apply IHl'.
+	inversion eq. reflexivity.
+	rewrite -> H. reflexivity.
+	Qed.
+
+	Theorem beq_nat_O_l : forall n,
+	true = beq_nat O n -> O = n.
+	Proof.
+	intros n. destruct n.
+	reflexivity.
+	simpl.
+	intros contra.
+	inversion contra.
+	Qed.
+
+Theorem beq_nat_O_r : forall n,
+	true = beq_nat n O -> O = n.
+Proof.
+	intros n.
+	induction n.
+	Case "n = O".
+		reflexivity.
+	Case "n = S n'".
+		simpl.
+		intros contra.
+		inversion contra.
+	Qed.
+
+Theorem double_injective : forall n m,
+	double n = double m ->
+		n = m.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = O".
+		simpl. intros m eq.
+		destruct m as [|m'].
+		SCase "m = O". reflexivity.
+		SCase "m = S m'". inversion eq.
+	Case "n = S n'". intros m eq. destruct m as [| m'].
+		SCase "m = O". inversion eq.
+		SCase "m = S m'".
+			assert(n' = m') as H.
+				SSCase "Proof of assertion". apply IHn'. inversion eq. reflexivity.
+			rewrite -> H. reflexivity.
+Qed.
+
+Theorem silly3' : forall (n : nat),
+	(beq_nat n (S (S (S (S (S O))))) = true ->
+	 	beq_nat (S (S n)) (S (S (S (S (S (S (S O))))))) = true) ->
+		true = beq_nat n (S (S (S (S (S O))))) ->
+			true = beq_nat (S (S n)) (S (S (S (S (S (S (S O))))))).
+Proof.
+	intros n eq H.
+	symmetry in H.
+	apply eq in H.
+	symmetry in H.
+	apply H.
+Qed.
+
+Theorem plus_n_n_injective : forall n m,
+					n + n = m + m ->
+						n = m.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = O".
+		simpl. intros m.
+		destruct m.
+			SCase "m = O".
+			reflexivity.
+			SCase "m = S m'".
+			simpl.
+			intros contra.
+			inversion contra.
+	Case "n = S n".
+		intros m.
+		destruct m.
+			SCase "m = O".
+			intros contra.
+			inversion contra.
+			SCase "m = S m'".
+			intros eq.
+			inversion eq.
+			rewrite <- plus_n_Sm in H0.
+			rewrite <- plus_n_Sm in H0.
+			inversion H0.
+			apply IHn' in H1.
+			rewrite -> H1.
+			reflexivity.
+	Qed.
+
+Theorem override_shadow : forall {X : Type} x1 x2 k1 k2 (f : nat -> X),
+	(override (override f k1 x2) k1 x1) k2 = (override f k1 x1) k2.
+Proof.
+	intros X x1 x2 k1 k2 f.
+	unfold override.
+	destruct (beq_nat k1 k2).
+	reflexivity.
+	reflexivity.
+	Qed.
+
+Theorem combine_split : forall (X : Type) (Y : Type) (l : list (X * Y)) (l1: list X) (l2: list Y),
+				split l = (l1, l2) -> combine l1 l2 = l.
+Proof.
+	intros X Y l.
+	induction l as [| x y].
+	Case "l = nil".
+		intros l1 l2.
+		intros eq.
+		simpl.
+		simpl in eq.
+		inversion eq.
+		reflexivity.
+	Case "l = ::".
+		intros l1 l2.
+		simpl.
+		destruct x.
+		destruct (split y).
+		simpl.
+		destruct l1.
+		SCase "l1 = []".
+			simpl.
+			induction l2.
+			SSCase "l2 = []".
+				intros contra.
+				inversion contra.
+			SSCase "l2 = ::".
+				intros contra.
+				inversion contra.
+		SCase "l1 = ::".
+			induction l2.
+			SSCase "l2 = []".
+				simpl.
+				intros contra.
+				inversion contra.
+			SSCase "l2 = ::".
+				simpl.
+				intros eq.
+				inversion eq.
+				simpl.
+				rewrite IHy.
+				reflexivity.
+				simpl.
+				rewrite H1.
+				rewrite H3.
+				reflexivity.
+Qed.
+
+Theorem split_combine : forall (X : Type) (Y : Type) (l1: list X) (l2: list Y),
+				length l1 = length l2 -> split (combine l1 l2) = (l1, l2).
+Proof.
+intros X Y.
+intros l1.
+induction l1.
+simpl.
+intros l2.
+induction l2.
+reflexivity.
+
+intros contra.
+inversion contra.
+
+destruct l2.
+simpl.
+intros contra.
+inversion contra.
+
+simpl.
+intros eq.
+inversion eq.
+apply IHl1 in H0.
+rewrite H0.
+reflexivity.
+Qed.
+
+Definition sillyfun1 (n : nat) : bool :=
+	 if beq_nat n (S (S (S O))) then true
+	 else if beq_nat n (S (S (S (S (S O))))) then true
+				else false.
+
+Theorem beq_equal : forall (a b : nat),
+		beq_nat a b = true ->
+			a = b.
+Proof.
+intros a.
+induction a.
+destruct b.
+reflexivity.
+
+intros contra.
+inversion contra.
+
+destruct b.
+intros contra.
+inversion contra.
+
+simpl.
+intros eq.
+apply IHa in eq.
+rewrite eq.
+reflexivity.
+Qed.
+
+Theorem override_same : forall {X : Type} x1 k1 k2 (f : nat->X),
+	f k1 = x1 ->
+		(override f k1 x1) k2 = f k2.
+Proof.
+	intros X x1 k1 k2 f eq.
+	unfold override.
+	remember (beq_nat k1 k2) as a.
+	destruct a.
+	rewrite <- eq.
+	symmetry in Heqa.
+	apply beq_equal in Heqa.
+	rewrite -> Heqa.
+	reflexivity.
+	reflexivity.
+	Qed.
+
+
+Theorem filter_exercise : forall (X : Type) (test : X -> bool)
+	(x : X) (l lf : list X),
+	filter _ test l = x :: lf ->
+		test x = true.
+Proof.
+intros X.
+intros test.
+intros x.
+induction l.
+simpl.
+intros lf.
+intros contra.
+inversion contra.
+
+simpl.
+remember (test x0) as a.
+destruct a.
+simpl.
+intros lf.
+intros eq.
+rewrite Heqa.
+inversion eq.
+reflexivity.
+
+intros lf.
+intros eq.
+apply IHl in eq.
+rewrite eq.
+reflexivity.
+Qed.
+
+Theorem trans_eq : forall {X:Type} (n m o : X),
+				n = m -> m = o -> n = o.
+Proof.
+	intros X n m o eq1 eq2. rewrite -> eq1. rewrite -> eq2.
+	reflexivity.
+Qed.
+
+Example trans_eq_example' : forall (a b c d e f : nat),
+				[a,b] = [c,d] ->
+				[c,d] = [e,f] ->
+				[a,b] = [e,f].
+Proof.
+	intros a b c d e f eq1 eq2.
+	apply trans_eq with (m := [c,d]). apply eq1. apply eq2.
+	Qed.
+
+Theorem trans_eq_exercise : forall (n m o p : nat),
+		m = (minustwo o) ->
+		(n + p) = m ->
+		(n + p) = (minustwo o).
+Proof.
+intros n m o p.
+intros eq1 eq2.
+rewrite eq2.
+rewrite <- eq1.
+reflexivity.
+Qed.
+
+Theorem beq_nat_trans : forall n m p,
+				true = beq_nat n m ->
+				true = beq_nat m p ->
+				true = beq_nat n p.
+Proof.
+intros n m p.
+intros eq1 eq2.
+symmetry  in eq1.
+symmetry  in eq2.
+apply beq_equal in eq1.
+apply beq_equal in eq2.
+rewrite eq1.
+rewrite <- eq2.
+apply beq_nat_refl.
+Qed.
+
+Theorem override_permute : forall {X:Type} x1 x2 k1 k2 k3 (f : nat->X),
+	false = beq_nat k2 k1 ->
+	(override (override f k2 x2) k1 x1) k3 = (override (override f k1 x1) k2 x2) k3.
+Proof.
+intros X x1 x2 k1 k2 k3 f.
+simpl.
+unfold override.
+remember (beq_nat k1 k3).
+remember (beq_nat k2 k3).
+destruct b.
+destruct b0.
+symmetry  in Heqb.
+symmetry  in Heqb0.
+apply beq_equal in Heqb.
+apply beq_equal in Heqb0.
+rewrite <- Heqb in Heqb0.
+assert (k2 = k1 -> true = beq_nat k2 k1).
+destruct k2.
+destruct k1.
+reflexivity.
+
+intros contra.
+inversion contra.
+
+destruct k1.
+intros contra.
+inversion contra.
+
+simpl.
+intros eq.
+inversion eq.
+symmetry .
+symmetry .
+apply beq_nat_refl.
+
+apply H in Heqb0.
+rewrite <- Heqb0.
+intros contra.
+inversion contra.
+
+intros eq.
+reflexivity.
+
+destruct b0.
+intros eq.
+reflexivity.
+
+intros eq.
+reflexivity.
+
+Qed.
+
+Definition fold_length {X : Type} (l : list X) : nat :=
+	fold (fun _ n => S n) l O.
+
+Example test_fold_length1 : fold_length [S (S (S (S O))), S (S (S (S (S (S (S O)))))), O] = S (S (S O)).
+Proof. reflexivity. Qed.
+
+Theorem fold_length_correct : forall X (l :list X),
+	fold_length l = length l.
+Proof.
+	intros X l.
+	unfold fold_length.
+	induction l.
+	Case "l = O".
+		reflexivity.
+	Case "l = ::".
+		simpl.
+		rewrite IHl.
+		reflexivity.
+	Qed.
+
+Definition fold_map {X Y: Type} (f : X -> Y) (l : list X) : list Y :=
+	fold (fun x total => (f x) :: total) l [].
+
+Theorem fold_map_correct : forall (X Y: Type) (f : X -> Y) (l : list X),
+	fold_map f l = map f l.
+Proof.
+	intros X Y f l.
+	unfold fold_map.
+	induction l.
+	reflexivity.
+	  
+	simpl.
+	rewrite IHl.
+	reflexivity.
+	Qed.
+
+Fixpoint forallb {X : Type} (f : X -> bool) (l : list X) :=
+	match l with
+		| nil => true
+		| x :: xs => andb (f x) (forallb f xs)
+	end.
+
+Fixpoint existsb {X : Type} (f : X -> bool) (l : list X) :=
+	match l with
+		| nil => false
+		| x :: xs => orb (f x) (existsb f xs)
+	end.
+
+Definition existsb2 {X : Type} (f: X -> bool) (l : list X) :=
+	negb (forallb (fun x => negb (f x)) l).
+
+Theorem existsb_correct : forall (X : Type) (f : X -> bool) (l : list X),
+		existsb f l = existsb2 f l.
+Proof.
+intros X f l.
+induction l.
+reflexivity.
+
+simpl.
+rewrite IHl.
+unfold existsb2.
+simpl.
+destruct (forallb (fun x0 : X => negb (f x0)) l).
+simpl.
+destruct (f x).
+reflexivity.
+
+reflexivity.
+
+destruct (f x).
+reflexivity.
+
+reflexivity.
+
+Qed.
+
+Theorem index_okx : forall (X:Type) (l : list X) (n : nat),
+		length l = n -> index X (S n) l = None.
+Proof.
+	intros X l.
+	induction l.
+	reflexivity.
+
+	intros n.
+	destruct n.
+	intros contra.
+	inversion contra.
+
+	intros eq.
+	inversion eq.
+	apply IHl.
+	reflexivity.
+Qed.
+
+Inductive mumble : Type :=
+  | a : mumble
+	| b : mumble -> nat -> mumble
+	| c : mumble.
+Inductive grumble (X:Type) : Type :=
+ | d : mumble -> grumble X
+ | e : X -> grumble X.
+

samples/coq/Rel.v

@@ -0,0 +1,312 @@
+Require Export Logic.
+Import Playground1.
+
+Definition relation (X:Type) := X -> X -> Prop.
+
+Definition partial_function {X:Type} (R: relation X) :=
+	forall x y1 y2 : X, R x y1 -> R x y2 -> y1 = y2.
+
+Theorem next_nat_partial_function :
+	partial_function next_nat.
+Proof.
+	unfold partial_function.
+	intros x y1 y2 P Q.
+	inversion P.
+	inversion Q.
+	reflexivity.
+Qed.
+
+Theorem le_not_a_partial_function :
+	~ (partial_function le).
+Proof.
+	unfold not.
+	unfold partial_function.
+	intros H.
+	assert (O = S O) as Nonsense.
+		Case "Proof of assertion.".
+		apply H with O.
+		apply le_n.
+
+		apply le_S.
+		apply le_n.
+
+	inversion Nonsense.
+Qed.
+
+Theorem total_relation_not_partial_function :
+	~ (partial_function total_relation).
+Proof.
+	unfold not.
+	unfold partial_function.
+	intros H.
+	assert (O = S O) as Nonsense.
+	apply H with O.
+	apply total_relation1.
+
+	apply total_relation1.
+
+	inversion Nonsense.
+Qed.
+
+Theorem empty_relation_not_partial_funcion :
+	partial_function empty_relation.
+Proof.
+	unfold partial_function.
+	intros x y1 y2.
+	intros H.
+	inversion H.
+Qed.
+
+Definition reflexive {X:Type} (R: relation X) :=
+	forall a : X, R a a.
+
+Theorem le_reflexive :
+	reflexive le.
+Proof.
+	unfold reflexive.
+	intros n. apply le_n.
+Qed.
+
+Definition transitive {X:Type} (R: relation X) :=
+	forall a b c : X, (R a b) -> (R b c) -> (R a c).
+
+Theorem le_trans:
+	transitive le.
+Proof.
+	intros n m o Hnm Hmo.
+	induction Hmo.
+	Case "le_n". apply Hnm.
+	Case "le_S". apply le_S. apply IHHmo.
+Qed.
+
+Theorem lt_trans:
+	transitive lt.
+Proof.
+	unfold lt. unfold transitive.
+	intros n m o Hnm Hmo.
+	apply le_S in Hnm.
+	apply le_trans with (a := (S n)) (b := (S m)) (c := o).
+	apply Hnm.
+	apply Hmo.
+Qed.
+
+Theorem lt_trans' :
+	transitive lt.
+Proof.
+	unfold lt. unfold transitive.
+	intros n m o Hnm Hmo.
+	induction Hmo as [| m' Hm'o].
+	apply le_S.
+	apply Hnm.
+
+	apply le_S.
+	apply IHHm'o.
+Qed.
+
+Theorem le_Sn_le: forall n m, S n <= m -> n <= m.
+Proof.
+	intros n m H. apply le_trans with (S n).
+	apply le_S. apply le_n.
+	apply H. Qed.
+
+Theorem le_S_n : forall n m,
+	(S n <= S m) -> (n <= m).
+Proof.
+intros n m H.
+apply Sn_le_Sm__n_le_m.
+apply H.
+Qed.
+
+Theorem le_Sn_n : forall n,
+	~ (S n <= n).
+Proof.
+induction n.
+intros H.
+inversion H.
+
+unfold not in IHn.
+intros H.
+apply le_S_n in H.
+apply IHn.
+apply H.
+Qed.
+
+(*
+ TODO
+Theorem lt_trans'' :
+	transitive lt.
+Proof.
+	unfold lt. unfold transitive.
+	intros n m o Hnm Hmo.
+	induction o as [| o'].
+	*)
+
+Definition symmetric {X: Type} (R: relation X) :=
+	forall a b : X, (R a b) -> (R b a).
+
+Definition antisymmetric {X : Type} (R: relation X) :=
+	forall a b : X, (R a b) -> (R b a) -> a = b.
+
+Theorem le_antisymmetric :
+	antisymmetric le.
+Proof.
+intros a b.
+generalize dependent a.
+induction b.
+intros a.
+intros H.
+intros H1.
+inversion H.
+reflexivity.
+
+intros a H1 H2.
+destruct a.
+inversion H2.
+
+apply Sn_le_Sm__n_le_m in H1.
+apply Sn_le_Sm__n_le_m in H2.
+apply IHb in H1.
+rewrite H1 in |- *.
+reflexivity.
+
+apply H2.
+Qed.
+
+(*
+ TODO
+Theorem le_step : forall n m p,
+	n < m ->
+	n <= S p ->
+	n <= p.
+Proof.
+*)
+
+Definition equivalence {X:Type} (R: relation X) :=
+	(reflexive R) /\ (symmetric R) /\ (transitive R).
+
+Definition order {X:Type} (R: relation X) :=
+	(reflexive R) /\ (antisymmetric R) /\ (transitive R).
+
+Definition preorder {X:Type} (R: relation X) :=
+	(reflexive R) /\ (transitive R).
+
+Theorem le_order :
+	order le.
+Proof.
+	unfold order. split.
+	Case "refl". apply le_reflexive.
+	split.
+		Case "antisym". apply le_antisymmetric.
+		Case "transitive". apply le_trans. Qed.
+
+Inductive clos_refl_trans {A:Type} (R: relation A) : relation A :=
+	| rt_step : forall x y, R x y -> clos_refl_trans R x y
+	| rt_refl : forall x, clos_refl_trans R x x
+	| rt_trans : forall x y z,
+		clos_refl_trans R x y -> clos_refl_trans R y z -> clos_refl_trans R x z.
+
+Theorem next_nat_closure_is_le : forall n m,
+	(n <= m) <-> ((clos_refl_trans next_nat) n m).
+Proof.
+intros n m.
+split.
+intro H.
+induction H.
+apply rt_refl.
+
+apply rt_trans with m.
+apply IHle.
+
+apply rt_step.
+apply nn.
+
+intro H.
+induction H.
+inversion H.
+apply le_S.
+apply le_n.
+
+apply le_n.
+
+apply le_trans with y.
+apply IHclos_refl_trans1.
+
+apply IHclos_refl_trans2.
+Qed.																    
+
+Inductive refl_step_closure {X : Type} (R: relation X)
+											: X -> X -> Prop :=
+	| rsc_refl : forall (x : X), refl_step_closure R x x
+	| rsc_step : forall (x y z : X), R x y ->
+								refl_step_closure R y z ->
+								refl_step_closure R x z.
+
+Tactic Notation "rt_cases" tactic(first) ident(c) :=
+	first;
+	[ Case_aux c "rt_step" | Case_aux c "rt_refl" | Case_aux c "rt_trans" ].
+
+Tactic Notation "rsc_cases" tactic(first) ident(c) :=
+	  first;
+		  [ Case_aux c "rsc_refl" | Case_aux c "rsc_step" ].
+
+Theorem rsc_R : forall (X:Type) (R:relation X) (x y:X),
+				R x y -> refl_step_closure R x y.
+Proof.
+intros X R x y r.
+apply rsc_step with y.
+ apply r.
+  
+  apply rsc_refl.
+Qed.
+
+Theorem rsc_trans :
+	forall (X : Type) (R : relation X) (x y z : X),
+		refl_step_closure R x y ->
+			refl_step_closure R y z ->
+				refl_step_closure R x z.
+Proof.
+intros X.
+intros R x y z.
+intros H.
+induction H.
+intros H1.
+apply H1.
+
+intros H1.
+apply IHrefl_step_closure in H1.
+apply rsc_step with y.
+apply H.
+
+apply H1.
+Qed.
+
+Theorem rtc_rsc_coincide:
+	forall (X:Type) (R: relation X) (x y : X),
+		clos_refl_trans R x y <-> refl_step_closure R x y.
+Proof.
+intros X R x y.
+split.
+intros H.
+induction H.
+apply rsc_step with y.
+apply H.
+
+apply rsc_refl.
+
+apply rsc_refl.
+
+apply rsc_trans with y.
+apply IHclos_refl_trans1.
+
+apply IHclos_refl_trans2.
+
+intros H1.
+induction H1.
+apply rt_refl.
+
+apply rt_trans with y.
+apply rt_step.
+apply H.
+
+apply IHrefl_step_closure.
+Qed.

samples/coq/Smallstep.v

@@ -0,0 +1,701 @@
+Require Export Imp.
+Require Export Relations.
+
+Inductive tm : Type :=
+   | tm_const : nat -> tm
+   | tm_plus : tm -> tm -> tm.
+
+Tactic Notation "tm_cases" tactic(first) ident(c) :=
+   first;
+   [ Case_aux c "tm_const" | Case_aux c "tm_plus" ].
+
+Module SimpleArith0.
+
+Fixpoint eval (t : tm) : nat :=
+   match t with
+      | tm_const n => n
+      | tm_plus a1 a2 => eval a1 + eval a2
+   end.
+
+End SimpleArith0.
+
+Module SimpleArith1.
+
+Reserved Notation " t '===>' n " (at level 50, left associativity).
+
+Inductive eval : tm -> nat -> Prop :=
+   | E_Const : forall n,
+                  tm_const n ===> n
+   | E_Plus : forall t1 t2 n1 n2,
+                  t1 ===> n1 ->
+                  t2 ===> n2 ->
+                  tm_plus t1 t2 ===> plus n1 n2
+
+     where " t '===>' n " := (eval t n).
+
+End SimpleArith1.
+
+Reserved Notation " t '===>' t' " (at level 50, left associativity).
+
+Inductive eval : tm -> tm -> Prop :=
+   | E_Const : forall n1,
+      tm_const n1 ===> tm_const n1
+   | E_Plus : forall t1 n1 t2 n2,
+      t1 ===> tm_const n1 ->
+      t2 ===> tm_const n2 ->
+         tm_plus t1 t2 ===> tm_const (plus n1 n2)
+   where " t '===>' t' " := (eval t t').
+
+Tactic Notation "eval_cases" tactic(first) ident(c) :=
+   first;
+   [ Case_aux c "E_Const" | Case_aux c "E_Plus" ].
+
+Module SimpleArith2.
+
+Reserved Notation " t '=>' t' " (at level 40).
+
+Inductive step : tm -> tm -> Prop :=
+   | ST_PlusConstConst : forall n1 n2,
+      tm_plus (tm_const n1) (tm_const n2) => tm_const (plus n1 n2)
+   | ST_Plus1 : forall t1 t1' t2,
+      t1 => t1' ->
+         tm_plus t1 t2 => tm_plus t1' t2
+   | ST_Plus2 : forall n1 t2 t2',
+      t2 => t2' ->
+      tm_plus (tm_const n1) t2 => tm_plus (tm_const n1) t2'
+
+   where " t '=>' t' " := (step t t').
+
+Tactic Notation "step_cases" tactic(first) ident(c) :=
+   first;
+   [ Case_aux c "ST_PlusConstConst"
+   | Case_aux c "ST_Plus1" | Case_aux c "ST_Plus2" ].
+
+Example test_step_1 : 
+      tm_plus 
+        (tm_plus (tm_const 0) (tm_const 3))
+        (tm_plus (tm_const 2) (tm_const 4))
+      =>
+      tm_plus 
+        (tm_const (plus 0 3))
+        (tm_plus (tm_const 2) (tm_const 4)).
+Proof.
+  apply ST_Plus1. apply ST_PlusConstConst. Qed.
+
+Example test_step_2 : 
+      tm_plus 
+        (tm_const 0)
+        (tm_plus 
+          (tm_const 2) 
+          (tm_plus (tm_const 0) (tm_const 3)))
+      =>
+      tm_plus 
+        (tm_const 0)
+        (tm_plus 
+          (tm_const 2) 
+          (tm_const (plus 0 3))).
+Proof.
+apply ST_Plus2.
+simpl.
+apply ST_Plus2.
+apply ST_PlusConstConst.
+Qed.
+
+Theorem step_deterministic:
+  partial_function step.
+Proof.
+  unfold partial_function. intros x y1 y2 Hy1 Hy2.
+  generalize dependent y2.
+  step_cases (induction Hy1) Case; intros y2 Hy2.
+    Case "ST_PlusConstConst". step_cases (inversion Hy2) SCase.
+      SCase "ST_PlusConstConst". reflexivity.
+      SCase "ST_Plus1". inversion H2.
+      SCase "ST_Plus2". inversion H2.
+    Case "ST_Plus1". step_cases (inversion Hy2) SCase.
+      SCase "ST_PlusConstConst". rewrite <- H0 in Hy1. inversion Hy1.
+      SCase "ST_Plus1".
+        rewrite <- (IHHy1 t1'0).
+        reflexivity. assumption.
+      SCase "ST_Plus2". rewrite <- H in Hy1. inversion Hy1.
+    Case "ST_Plus2". step_cases (inversion Hy2) SCase.
+      SCase "ST_PlusConstConst". rewrite <- H1 in Hy1. inversion Hy1.
+      SCase "ST_Plus1". inversion H2.
+      SCase "ST_Plus2".
+        rewrite <- (IHHy1 t2'0).
+        reflexivity. assumption. Qed.
+
+End SimpleArith2.
+
+Inductive value : tm -> Prop :=
+   v_const: forall n, value (tm_const n).
+
+Reserved Notation " t '=>' t' " (at level 40).
+
+Inductive step : tm -> tm -> Prop :=
+   | ST_PlusConstConst : forall n1 n2,
+      tm_plus (tm_const n1) (tm_const n2)
+         => tm_const (plus n1 n2)
+   | ST_Plus1 : forall t1 t1' t2,
+      t1 => t1' ->
+         tm_plus t1 t2 => tm_plus t1' t2
+   | ST_Plus2 : forall v1 t2 t2',
+      value v1 ->
+         t2 => t2' ->
+            tm_plus v1 t2 => tm_plus v1 t2'
+
+   where " t '=>' t' " := (step t t').
+
+Tactic Notation "step_cases" tactic(first) ident(c) :=
+   first;
+   [ Case_aux c "ST_PlusConstConst"
+      | Case_aux c "ST_Plus1" | Case_aux c "ST_Plus2" ].
+
+Theorem step_deterministic :
+   partial_function step.
+Proof.
+unfold partial_function.
+intros x y1 y2 Hy1 Hy2.
+generalize dependent y2.
+step_cases (induction Hy1) Case; intros y2 Hy2.
+ step_cases (inversion Hy2) SCase.
+  reflexivity.
+  
+  inversion H2.
+  
+  inversion Hy2.
+   subst.
+   assumption.
+   
+   subst.
+   inversion H3.
+   
+   subst.
+   inversion H3.
+   
+ step_cases (inversion Hy2) SCase.
+  rewrite <- H0 in Hy1.
+  inversion Hy1.
+  
+  rewrite <- (IHHy1 t1'0).
+   reflexivity.
+   
+   assumption.
+   
+  rewrite <- H in Hy1.
+  rewrite <- H in H1.
+  subst.
+  inversion H1.
+  subst.
+  inversion Hy1.
+  
+ step_cases (inversion Hy2) SCase.
+  subst.
+  inversion Hy1.
+  
+  subst.
+  inversion H.
+  subst.
+  inversion H3.
+  
+  subst.
+  inversion H2.
+  subst.
+  rewrite <- (IHHy1 t2'0).
+   reflexivity.
+   
+   assumption.
+Qed.
+
+Theorem strong_progress : forall t,
+        value t \/ (exists t', t => t').
+Proof.
+   tm_cases (induction t) Case.
+      Case "tm_const". left. apply v_const.
+      Case "tm_plus". right. inversion IHt1.
+         SCase "l". inversion IHt2.
+            SSCase "l". inversion H. inversion H0.
+               exists (tm_const (plus n n0)).
+               apply ST_PlusConstConst.
+            SSCase "r". inversion H0 as [t' H1].
+               exists (tm_plus t1 t').
+               apply ST_Plus2. apply H. apply H1.
+         SCase "r". inversion H as [t' H0].
+            exists (tm_plus t' t2).
+            apply ST_Plus1. apply H0. Qed.
+
+Definition normal_form {X:Type} (R: relation X) (t: X) : Prop :=
+    ~ (exists t', R t t'). 
+
+Lemma value_is_nf: forall t,
+      value t -> normal_form step t.
+Proof.
+   unfold normal_form. intros t H. inversion H.
+   intros contra. inversion contra. inversion H1.
+   Qed.
+
+Lemma nf_is_value: forall t,
+      normal_form step t -> value t.
+Proof.
+   unfold normal_form. intros t H.
+   assert (G: value t \/ (exists t', t => t')).
+      SCase "Proof of assertion". apply strong_progress.
+   inversion G.
+      SCase "l". assumption.
+      SCase "r". apply ex_falso_quodlibet. apply H. assumption. Qed.
+
+Corollary nf_same_as_value : forall t,
+            normal_form step t <-> value t.
+Proof.
+   split. apply nf_is_value. apply value_is_nf.
+Qed.
+
+Module Temp1.
+
+Inductive value : tm -> Prop :=
+| v_const : forall n, value (tm_const n)
+| v_funny : forall t1 n2, (* <---- *)
+              value (tm_plus t1 (tm_const n2)).
+
+Reserved Notation " t '=>' t' " (at level 40).
+
+Inductive step : tm -> tm -> Prop :=
+  | ST_PlusConstConst : forall n1 n2,
+      tm_plus (tm_const n1) (tm_const n2) => tm_const (plus n1 n2)
+  | ST_Plus1 : forall t1 t1' t2,
+      t1 => t1' ->
+      tm_plus t1 t2 => tm_plus t1' t2
+  | ST_Plus2 : forall v1 t2 t2',
+      value v1 ->
+      t2 => t2' ->
+      tm_plus v1 t2 => tm_plus v1 t2'
+
+  where " t '=>' t' " := (step t t').
+
+Lemma value_not_same_as_normal_form:
+   exists t, value t /\ ~ normal_form step t.
+Proof.
+intros.
+unfold normal_form.
+exists (tm_plus (tm_plus (tm_const 1) (tm_const 2)) (tm_const 2)).
+split.
+ apply v_funny.
+ 
+ unfold not.
+ intros.
+ apply H.
+ exists (tm_plus (tm_const (1 + 2)) (tm_const 2)).
+ apply ST_Plus1.
+ apply ST_PlusConstConst.
+Qed.
+
+End Temp1.
+
+Module Temp2.
+
+Inductive value : tm -> Prop :=
+   | v_const : forall n, value (tm_const n).
+
+(*Reserved Notation " t '===>' t' " (at level 40).*)
+
+Inductive step : tm -> tm -> Prop :=
+  | ST_Funny : forall n, (* <---- *)
+      tm_const n ===> tm_plus (tm_const n) (tm_const 0)
+  | ST_PlusConstConst : forall n1 n2,
+      tm_plus (tm_const n1) (tm_const n2) ===> tm_const (plus n1 n2)
+  | ST_Plus1 : forall t1 t1' t2,
+      t1 ===> t1' ->
+      tm_plus t1 t2 ===> tm_plus t1' t2
+  | ST_Plus2 : forall v1 t2 t2',
+      value v1 ->
+      t2 ===> t2' ->
+      tm_plus v1 t2 ===> tm_plus v1 t2'
+
+  where " t '===>' t' " := (step t t').
+
+Lemma value_not_same_as_normal_form :
+  exists t, value t /\ ~ normal_form step t.
+Proof.
+exists (tm_const 0).
+split.
+ apply v_const.
+ 
+ unfold normal_form.
+ unfold not.
+ intro H.
+ apply H.
+ exists (tm_plus (tm_const 0) (tm_const 0)).
+ apply ST_Funny.
+Qed.
+
+End Temp2.
+
+Module Temp3.
+
+Inductive value : tm -> Prop :=
+  | v_const : forall n, value (tm_const n).
+
+(*Reserved Notation " t '===>' t' " (at level 40).*)
+
+Inductive step : tm -> tm -> Prop :=
+  | ST_PlusConstConst : forall n1 n2,
+      tm_plus (tm_const n1) (tm_const n2) ===> tm_const (plus n1 n2)
+  | ST_Plus1 : forall t1 t1' t2,
+      t1 ===> t1' ->
+      tm_plus t1 t2 ===> tm_plus t1' t2
+
+  where " t '===>' t' " := (step t t').
+
+Lemma value_not_same_as_normal_form:
+   exists t, ~ value t /\ normal_form step t.
+Proof.
+exists (tm_plus (tm_const 1) (tm_plus (tm_const 0) (tm_const 0))).
+split.
+ intros H.
+ inversion H.
+ 
+ unfold normal_form.
+ intros H.
+ inversion H.
+ inversion H0.
+ inversion H4.
+Qed.
+
+End Temp3.
+
+Module Temp4.
+Inductive tm : Type :=
+   | tm_true : tm
+   | tm_false : tm
+   | tm_if : tm -> tm -> tm -> tm.
+
+Inductive value : tm -> Prop :=
+   | v_true : value tm_true
+   | v_false : value tm_false.
+
+Inductive step : tm -> tm -> Prop :=
+   | ST_IfTrue : forall t1 t2,
+      tm_if tm_true t1 t2 ===> t1
+   | ST_IfFalse : forall t1 t2,
+      tm_if tm_false t1 t2 ===> t2
+   | ST_If : forall t1 t1' t2 t3,
+      t1 ===> t1' ->
+         tm_if t1 t2 t3 ===> tm_if t1' t2 t3
+
+   where " t '===>' t' " := (step t t').
+
+Example bool_step_prop3 :
+     tm_if
+       (tm_if tm_true tm_true tm_true)
+       (tm_if tm_true tm_true tm_true)
+       tm_false
+   ===>
+     tm_if
+       tm_true
+       (tm_if tm_true tm_true tm_true)
+       tm_false.
+Proof.
+apply ST_If.
+apply ST_IfTrue.
+Qed.
+
+Theorem strong_progress: forall t,
+        value t \/ (exists t', t ===> t').
+Proof.
+induction t.
+ left.
+ constructor.
+ 
+ left.
+ constructor.
+ 
+ right.
+ inversion IHt1.
+  inversion H.
+   exists t2.
+   apply ST_IfTrue.
+   
+   exists t3.
+   apply ST_IfFalse.
+   
+  inversion H.
+  exists (tm_if x t2 t3).
+  apply ST_If.
+  assumption.
+Qed.
+
+Theorem step_deterministic :
+  partial_function step.
+Proof.
+unfold partial_function.
+intros x y1 y2 Hy1 Hy2.
+generalize dependent y2.
+induction Hy1.
+ intros.
+ inversion Hy2.
+  reflexivity.
+  
+  subst.
+  inversion H3.
+  
+ intros.
+ inversion Hy2.
+  reflexivity.
+  
+  inversion H3.
+  
+ intros.
+ inversion Hy2.
+  subst.
+  inversion Hy1.
+  
+  subst.
+  inversion Hy1.
+  
+  subst.
+  apply IHHy1 in H3.
+  subst.
+  reflexivity.
+Qed.
+
+Module Temp5.
+
+
+Inductive step : tm -> tm -> Prop :=
+   | ST_IfTrue : forall t1 t2,
+      tm_if tm_true t1 t2 ===> t1
+   | ST_IfFalse : forall t1 t2,
+      tm_if tm_false t1 t2 ===> t2
+   | ST_If : forall t1 t1' t2 t3,
+      t1 ===> t1' ->
+         tm_if t1 t2 t3 ===> tm_if t1' t2 t3
+   | ST_ShortCut : forall v t,
+      value v ->
+         tm_if t v v ===> v
+
+   where " t '===>' t' " := (step t t').
+
+Definition bool_step_prop4 :=
+         tm_if
+            (tm_if tm_true tm_true tm_true)
+            tm_false
+            tm_false
+     ===>
+         tm_false.
+
+Example bool_step_prop4_holds : 
+  bool_step_prop4.
+Proof.
+   unfold bool_step_prop4.
+   apply ST_ShortCut.
+   constructor.
+Qed.
+
+Theorem strong_progress: forall t,
+        value t \/ (exists t', t ===> t').
+Proof.
+   induction t.
+ left.
+ constructor.
+ 
+ left.
+ constructor.
+ 
+ inversion IHt1.
+  right.
+  inversion H.
+   exists t2.
+   constructor.
+   
+   exists t3.
+   constructor.
+   
+  right.
+  inversion H.
+  exists (tm_if x t2 t3).
+  apply ST_If.
+  assumption.
+Qed.
+
+End Temp5.
+End Temp4.
+
+Definition stepmany := refl_step_closure step.
+
+Notation " t '===>*' t' " := (stepmany t t') (at level 40).
+
+Lemma test_stepmany_1:
+   tm_plus
+      (tm_plus (tm_const 0) (tm_const 3))
+      (tm_plus (tm_const 2) (tm_const 4))
+      ===>*
+         tm_const (plus (plus 0 3) (plus 2 4)).
+Proof.
+   eapply rsc_step. apply ST_Plus1. apply ST_PlusConstConst.
+  eapply rsc_step. apply ST_Plus2. apply v_const.
+  apply ST_PlusConstConst.
+  eapply rsc_step. apply ST_PlusConstConst.
+  apply rsc_refl. Qed.
+
+Lemma test_stepmany_2:
+   tm_const 3 ===>* tm_const 3.
+Proof.
+   eapply rsc_refl.
+Qed.
+
+Lemma test_stepmany_3:
+   tm_plus (tm_const 0) (tm_const 3)
+      ===>*
+   tm_plus (tm_const 0) (tm_const 3).
+Proof.
+   eapply rsc_refl.
+Qed.
+
+Lemma test_stepmany_4:
+   tm_plus
+      (tm_const 0)
+      (tm_plus
+         (tm_const 2)
+         (tm_plus (tm_const 0) (tm_const 3)))
+   ===>*
+      tm_plus
+         (tm_const 0)
+         (tm_const (plus 2 (plus 0 3))).
+Proof.
+eapply rsc_step.
+ apply ST_Plus2.
+  apply v_const.
+  
+  apply ST_Plus2.
+   apply v_const.
+   
+   apply ST_PlusConstConst.
+   
+ eapply rsc_step.
+  apply ST_Plus2.
+   apply v_const.
+   
+   apply ST_PlusConstConst.
+   
+  eapply rsc_refl.
+Qed.
+
+Definition step_normal_form := normal_form step.
+
+Definition normal_form_of (t t' : tm) :=
+  (t ===>* t' /\ step_normal_form t').
+
+   (*
+Theorem normal_forms_unique:
+   partial_function normal_form_of.
+Proof.
+   unfold partial_function. unfold normal_form_of. intros x y1 y2 P1 P2.
+   destruct P1 as [P11 P12]. destruct P2 as [P21 P22].
+   generalize dependent y2.
+
+   unfold step_normal_form in P12.
+   unfold step_normal_form.
+   unfold normal_form.
+   unfold normal_form in P12.
+   induction x.
+   intros.
+   unfold stepmany.
+   inversion P11.
+   subst.
+   inversion P21.
+   subst.
+   reflexivity.
+
+   subst.
+   inversion P21.
+   reflexivity.
+
+   subst.
+   inversion H1.
+
+   inversion H.
+   *)
+
+Definition normalizing {X:Type} (R:relation X) :=
+     forall t, exists t',
+         (refl_step_closure R) t t' /\ normal_form R t'.
+
+Lemma stepmany_congr_1 : forall t1 t1' t2,
+      t1 ===>* t1' ->
+         tm_plus t1 t2 ===>* tm_plus t1' t2.
+Proof.
+intros t1 t1' t2 H.
+rsc_cases (induction H) Case.
+ apply rsc_refl.
+  
+  apply rsc_step with (tm_plus y t2).
+    apply ST_Plus1.
+      apply H.
+        
+        apply IHrefl_step_closure.
+Qed.
+
+Lemma stepmany_congr2 : forall t1 t2 t2',
+      value t1 ->
+         t2 ===>* t2' ->
+            tm_plus t1 t2 ===>* tm_plus t1 t2'.
+Proof.
+intros t1 t2 t2'.
+intros H1.
+intros H2.
+induction H2.
+ apply rsc_refl.
+  
+  apply rsc_step with (tm_plus t1 y).
+    apply ST_Plus2.
+       assumption.
+          
+          assumption.
+             
+            assumption.
+Qed.
+
+Theorem step_normalizing :
+  normalizing step.
+Proof.
+  unfold normalizing.
+  tm_cases (induction t) Case.
+    Case "tm_const".
+      exists (tm_const n).
+      split.
+      SCase "l". apply rsc_refl.
+      SCase "r".
+        (* We can use rewrite with "iff" statements, not
+           just equalities: *)
+        rewrite nf_same_as_value. apply v_const.
+    Case "tm_plus".
+      destruct IHt1 as [t1' H1]. destruct IHt2 as [t2' H2].
+      destruct H1 as [H11 H12]. destruct H2 as [H21 H22].
+      rewrite nf_same_as_value in H12. rewrite nf_same_as_value in H22.
+      inversion H12 as [n1]. inversion H22 as [n2].
+      rewrite <- H in H11.
+      rewrite <- H0 in H21.
+      exists (tm_const (plus n1 n2)).
+      split.
+        SCase "l".
+          apply rsc_trans with (tm_plus (tm_const n1) t2).
+          apply stepmany_congr_1. apply H11.
+          apply rsc_trans with 
+             (tm_plus (tm_const n1) (tm_const n2)).
+          apply stepmany_congr2. apply v_const. apply H21.
+          apply rsc_R. apply ST_PlusConstConst.
+        SCase "r".
+          rewrite nf_same_as_value. apply v_const. Qed.
+          
+ Lemma eval__value : forall t1 t2,
+      eval t1 t2 ->
+      value t2.
+ Proof.
+   intros t1 t2 HE.
+   eval_cases (inversion HE) Case; apply v_const. Qed.
+   
+
+   (*
+Theorem eval__stepmany: forall t v,
+  eval t v -> t ===>* v.
+Proof.   
+*)

samples/coq/Sorting.v

@@ -0,0 +1,10 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Export Sorted.
+Require Export Mergesort.

samples/coq/Stlc.v

@@ -0,0 +1,733 @@
+
+Require Export SfLib.
+
+Module STLC.
+
+Inductive ty : Type :=
+   | ty_Bool : ty
+   | ty_arrow : ty -> ty -> ty.
+
+Inductive tm : Type :=
+   | tm_var : id -> tm
+   | tm_app : tm -> tm -> tm
+   | tm_abs : id -> ty -> tm -> tm
+   | tm_true : tm
+   | tm_false : tm
+   | tm_if : tm -> tm -> tm -> tm.
+
+Tactic Notation "tm_cases" tactic(first) ident(c) :=
+  first;
+  [ Case_aux c "tm_var" | Case_aux c "tm_app" 
+  | Case_aux c "tm_abs" | Case_aux c "tm_true" 
+  | Case_aux c "tm_false" | Case_aux c "tm_if" ].
+  
+Notation a := (Id 0).
+Notation b := (Id 1).
+Notation c := (Id 2).
+
+Notation idB :=
+   (tm_abs a ty_Bool (tm_var a)).
+   
+Notation idBB :=
+   (tm_abs a (ty_arrow ty_Bool ty_Bool) (tm_var a)).
+   
+Notation idBBBB :=
+   (tm_abs a (ty_arrow (ty_arrow ty_Bool ty_Bool) 
+                         (ty_arrow ty_Bool ty_Bool)) 
+       (tm_var a)).
+       
+Notation k := (tm_abs a ty_Bool (tm_abs b ty_Bool (tm_var a))).
+
+Inductive value : tm -> Prop :=
+  | v_abs : forall x T t,
+      value (tm_abs x T t)
+  | t_true : 
+      value tm_true
+  | t_false : 
+      value tm_false.
+
+Hint Constructors value.
+
+Fixpoint subst (s:tm) (x:id) (t:tm) : tm :=
+   match t with
+   | tm_var x' => if beq_id x x' then s else t
+   | tm_abs x' T t1 => tm_abs x' T (if beq_id x x' then t1 else (subst s x t1))
+   | tm_app t1 t2 => tm_app (subst s x t1) (subst s x t2)
+   | tm_true => tm_true
+   | tm_false => tm_false
+   | tm_if t1 t2 t3 => tm_if (subst s x t1) (subst s x t2) (subst s x t3)
+end.
+
+Reserved Notation "t1 '==>' t2" (at level 40).
+
+Inductive step : tm -> tm -> Prop :=
+ | ST_AppAbs : forall x T t12 v2,
+        value v2 ->
+        (tm_app (tm_abs x T t12) v2) ==> (subst v2 x t12)
+ | ST_App1 : forall t1 t1' t2,
+        t1 ==> t1' ->
+        tm_app t1 t2 ==> tm_app t1' t2
+ | ST_App2 : forall v1 t2 t2',
+        value v1 ->
+        t2 ==> t2' ->
+        tm_app v1 t2 ==> tm_app v1 t2'
+ | ST_IfTrue : forall t1 t2,
+     (tm_if tm_true t1 t2) ==> t1
+ | ST_IfFalse : forall t1 t2,
+     (tm_if tm_false t1 t2) ==> t2
+ | ST_If : forall t1 t1' t2 t3,
+     t1 ==> t1' ->
+     (tm_if t1 t2 t3) ==> (tm_if t1' t2 t3)
+
+where "t1 '==>' t2" := (step t1 t2).
+
+Tactic Notation "step_cases" tactic(first) ident(c) :=
+ first;
+ [ Case_aux c "ST_AppAbs" | Case_aux c "ST_App1" 
+ | Case_aux c "ST_App2" | Case_aux c "ST_IfTrue" 
+ | Case_aux c "ST_IfFalse" | Case_aux c "ST_If" ].
+
+Notation stepmany := (refl_step_closure step).
+Notation "t1 '==>*' t2" := (stepmany t1 t2) (at level 40).
+
+Hint Constructors step.
+
+Lemma step_example3 :
+       (tm_app (tm_app idBBBB idBB) idB)
+  ==>* idB.
+Proof.
+ eapply rsc_step.
+ apply ST_App1.
+ apply ST_AppAbs.
+ apply v_abs.
+ 
+ simpl.
+ eapply rsc_step.
+  apply ST_AppAbs.
+  apply v_abs.
+  
+  simpl.
+  apply rsc_refl.
+Qed.
+
+Definition context := partial_map ty.
+Module Context.
+
+Definition partial_map (A:Type) := id -> option A.
+Definition empty {A:Type} : partial_map A := (fun _ => None).
+Definition extend {A:Type} (Gamma : partial_map A) (x:id) (T : A) :=
+   fun x' => if beq_id x x' then Some T else Gamma x'.
+   
+Lemma extend_eq : forall A (ctxt: partial_map A) x T,
+   (extend ctxt x T) x = Some T.
+Proof.
+   intros. unfold extend. rewrite <- beq_id_refl. auto.
+Qed.
+
+Lemma extend_neq : forall A (ctxt: partial_map A) x1 T x2,
+   beq_id x2 x1 = false ->
+      (extend ctxt x2 T) x1 = ctxt x1.
+Proof.
+intros. unfold extend. rewrite H. auto.
+Qed.
+
+End Context.
+
+Inductive has_type : context -> tm -> ty -> Prop :=
+   | T_Var : forall Gamma x T,
+      Gamma x = Some T ->
+         has_type Gamma (tm_var x) T
+   | T_Abs : forall Gamma x T11 T12 t12,
+      has_type (extend Gamma x T11) t12 T12 ->
+         has_type Gamma (tm_abs x T11 t12) (ty_arrow T11 T12)
+   | T_App : forall T11 T12 Gamma t1 t2,
+      has_type Gamma t1 (ty_arrow T11 T12) ->
+         has_type Gamma t2 T11 ->
+            has_type Gamma (tm_app t1 t2) T12
+   | T_True : forall Gamma,
+      has_type Gamma tm_true ty_Bool
+   | T_False : forall Gamma,
+      has_type Gamma tm_false ty_Bool
+   | T_If : forall t1 t2 t3 T Gamma,
+      has_type Gamma t1 ty_Bool ->
+      has_type Gamma t2 T ->
+      has_type Gamma t3 T ->
+      has_type Gamma (tm_if t1 t2 t3) T.
+      
+Tactic Notation "has_type_cases" tactic(first) ident(c) :=
+  first;
+  [ Case_aux c "T_Var" | Case_aux c "T_Abs" 
+  | Case_aux c "T_App" | Case_aux c "T_True" 
+  | Case_aux c "T_False" | Case_aux c "T_If" ].
+
+Hint Constructors has_type.
+
+Hint Unfold beq_id beq_nat extend.
+
+Example typing_example_2_full :
+  has_type empty
+    (tm_abs a ty_Bool
+       (tm_abs b (ty_arrow ty_Bool ty_Bool)
+          (tm_app (tm_var b) (tm_app (tm_var b) (tm_var a)))))
+    (ty_arrow ty_Bool (ty_arrow (ty_arrow ty_Bool ty_Bool) ty_Bool)).
+Proof.
+apply T_Abs.
+apply T_Abs.
+apply T_App with (T11 := ty_Bool).
+ apply T_Var.
+ unfold extend.
+ simpl.
+ reflexivity.
+ 
+ apply T_App with (T11 := ty_Bool).
+  apply T_Var.
+  unfold extend.
+  simpl.
+  reflexivity.
+  
+  apply T_Var.
+  unfold extend.
+  simpl.
+  reflexivity.
+Qed.
+
+Example typing_example_3 :
+  exists T, 
+    has_type empty
+      (tm_abs a (ty_arrow ty_Bool ty_Bool)
+         (tm_abs b (ty_arrow ty_Bool ty_Bool)
+            (tm_abs c ty_Bool
+               (tm_app (tm_var b) (tm_app (tm_var a) (tm_var c))))))
+      T.
+
+Proof with auto.
+exists
+ (ty_arrow (ty_arrow ty_Bool ty_Bool)
+    (ty_arrow (ty_arrow ty_Bool ty_Bool) (ty_arrow ty_Bool ty_Bool))).
+apply T_Abs.
+apply T_Abs.
+apply T_Abs.
+apply T_App with (T11 := ty_Bool).
+ apply T_Var.
+ unfold extend.
+ simpl.
+ reflexivity.
+ 
+ apply T_App with (T11 := ty_Bool).
+  auto.
+  
+  auto.
+Qed.
+
+
+Theorem coiso : forall a b e,
+   a ==>* b ->
+      tm_app a e ==>* tm_app b e.
+Proof.
+intros.
+induction H.
+ apply rsc_refl.
+ 
+ apply rsc_step with (tm_app y e).
+  apply ST_App1.
+  assumption.
+  
+  assumption.
+Qed.
+
+Theorem reptrans : forall a b c,
+   a ==>* b ->
+      b ==>* c ->
+         a ==>* c.
+Proof.
+
+intros a b c H.
+induction H.
+ intros.
+ assumption.
+ 
+ intros H1.
+ apply IHrefl_step_closure in H1.
+ apply rsc_step with y.
+  assumption.
+  
+  assumption.
+Qed.
+
+(* TODO
+Example typing_nonexample_3 :
+  ~ (exists S, exists T,
+        has_type empty 
+          (tm_abs a S
+             (tm_app (tm_var a) (tm_var a)))
+          T).
+Proof.
+*)
+
+Inductive appears_free_in : id -> tm -> Prop :=
+  | afi_var : forall x,
+      appears_free_in x (tm_var x)
+  | afi_app1 : forall x t1 t2,
+      appears_free_in x t1 -> appears_free_in x (tm_app t1 t2)
+  | afi_app2 : forall x t1 t2,
+      appears_free_in x t2 -> appears_free_in x (tm_app t1 t2)
+  | afi_abs : forall x y T11 t12,
+      y <> x ->
+      appears_free_in x t12 ->
+      appears_free_in x (tm_abs y T11 t12)
+  | afi_if1 : forall x t1 t2 t3,
+      appears_free_in x t1 ->
+      appears_free_in x (tm_if t1 t2 t3)
+  | afi_if2 : forall x t1 t2 t3,
+      appears_free_in x t2 ->
+      appears_free_in x (tm_if t1 t2 t3)
+  | afi_if3 : forall x t1 t2 t3,
+      appears_free_in x t3 ->
+      appears_free_in x (tm_if t1 t2 t3).
+      
+Tactic Notation "afi_cases" tactic(first) ident(c) :=
+  first;
+  [ Case_aux c "afi_var"
+  | Case_aux c "afi_app1" | Case_aux c "afi_app2" 
+  | Case_aux c "afi_abs" 
+  | Case_aux c "afi_if1" | Case_aux c "afi_if2" 
+  | Case_aux c "afi_if3" ].
+
+Hint Constructors appears_free_in.
+
+Definition closed (t:tm) :=
+  forall x, ~ appears_free_in x t.
+  
+Lemma free_in_context : forall x t T Gamma,
+  appears_free_in x t ->
+  has_type Gamma t T ->
+  exists T', Gamma x = Some T'.
+Proof.
+  intros. generalize dependent Gamma. generalize dependent T.
+  afi_cases (induction H) Case; 
+         intros; try solve [inversion H0; eauto].
+  Case "afi_abs".
+    inversion H1; subst.
+    apply IHappears_free_in in H7.
+    apply not_eq_beq_id_false in H.
+    rewrite extend_neq in H7; assumption.
+Qed.
+
+Corollary typable_empty__closed : forall t T, 
+    has_type empty t T ->
+    closed t.
+Proof.
+intros t T H x H1.
+remember (@empty ty) as Gamma.
+assert (exists t' : _, Gamma x = Some t').
+ apply free_in_context with (t := t) (T := T).
+  assumption.
+  
+  assumption.
+  
+ inversion H0.
+ rewrite HeqGamma in H2.
+ inversion H2.
+Qed.
+
+Lemma context_invariance : forall Gamma Gamma' t S,
+     has_type Gamma t S ->
+     (forall x, appears_free_in x t -> Gamma x = Gamma' x) ->
+     has_type Gamma' t S.
+Proof with auto.
+intros.
+generalize dependent Gamma'.
+has_type_cases (induction H) Case; intros; auto.
+ apply T_Var.
+ rewrite <- H0...
+ 
+ apply T_Abs.
+ apply IHhas_type.
+ intros x0 Hafi.
+ unfold extend.
+ remember (beq_id x x0) as e.
+ destruct e.
+  reflexivity.
+  
+  auto.
+  apply H0.
+  apply afi_abs.
+   auto.
+   eauto   .
+   apply beq_id_false_not_eq.
+   rewrite Heqe.
+   reflexivity.
+   
+   assumption.
+   
+ apply T_App with T11.
+  auto.
+  
+  auto.
+Qed.
+
+Lemma substitution_preserves_typing : forall Gamma x U v t T,
+   has_type (extend Gamma x U) t T ->
+      has_type empty v U ->
+         has_type Gamma (subst v x t) T.
+Proof with eauto.
+   intros Gamma x U v t T Ht Hv.
+   generalize dependent Gamma.
+   generalize dependent T.
+   tm_cases (induction t) Case; intros T Gamma H; inversion H; subst; simpl...
+   Case "tm_var".
+       rename i into y. remember (beq_id x y) as e. destruct e.
+       SCase "x=y".
+         apply beq_id_eq in Heqe. subst.
+         rewrite extend_eq in H2.
+         inversion H2; subst.
+         clear H2.
+           eapply context_invariance...
+           intros x Hcontra.
+           destruct (free_in_context _ _ T empty Hcontra) as (T', HT')...
+           inversion HT'.
+
+           apply T_Var.
+           rewrite extend_neq in H2.
+            assumption.
+
+            rewrite Heqe.
+            reflexivity.
+
+          rename i into y.
+          apply T_Abs.
+          remember (beq_id x y) as e.
+          destruct e.
+           eapply context_invariance...
+           apply beq_id_eq in Heqe.
+           subst.
+           intros x Hafi.
+           unfold extend.
+           destruct (beq_id y x).
+            reflexivity.
+
+            reflexivity.
+
+           apply IHt.
+           eapply context_invariance...
+           intros x0 Hafi.
+           unfold extend.
+           remember (beq_id y x0) as Coiso1.
+           remember (beq_id x x0) as Coiso2.
+           destruct Coiso1.
+            auto.
+            eauto   .
+            destruct Coiso2.
+             eauto   .
+             auto.
+             apply beq_id_eq in HeqCoiso1.
+             apply beq_id_eq in HeqCoiso2.
+             subst.
+             assert (x0 <> x0).
+              apply beq_id_false_not_eq.
+              rewrite Heqe.
+              auto.
+
+              apply ex_falso_quodlibet.
+              apply H0.
+              reflexivity.
+
+             reflexivity.
+
+            destruct Coiso2.
+             auto.
+
+             auto.
+Qed.
+
+Theorem preservation : forall t t' T,
+     has_type empty t T ->
+     t ==> t' ->
+     has_type empty t' T.
+Proof.
+remember (@empty ty) as Gamma.
+intros t t' T HT.
+generalize dependent t'.
+induction HT.
+ intros t' H1.
+ inversion H1.
+ 
+ intros t' H1.
+ inversion H1.
+ 
+ intros t' H1.
+ inversion H1.
+  apply substitution_preserves_typing with T11.
+   subst.
+   inversion HT1.
+   subst.
+   apply H2.
+   
+   subst.
+   assumption.
+   
+  subst.
+  apply T_App with T11.
+   apply IHHT1.
+    reflexivity.
+    
+    assumption.
+    
+   assumption.
+   
+  subst.
+  apply T_App with T11.
+   assumption.
+   
+   apply IHHT2.
+    reflexivity.
+    
+    assumption.
+    
+ intros t' H.
+ inversion H.
+ 
+ intros t' H.
+ inversion H.
+ 
+ intros t' H.
+ inversion H.
+  subst.
+  assumption.
+  
+  subst.
+  assumption.
+  
+  subst.
+  apply T_If.
+   apply IHHT1.
+    reflexivity.
+    
+    assumption.
+    
+   assumption.
+   
+   assumption.
+Qed.
+
+Theorem progress : forall t T,
+     has_type empty t T ->
+     value t \/ exists t', t ==> t'.
+Proof.
+intros t T.
+intros H.
+remember (@empty ty) as Gamma.
+induction H.
+ rewrite HeqGamma in H.
+ unfold empty in H.
+ inversion H.
+ 
+ left.
+ apply v_abs.
+ 
+ right.
+ assert (value t1 \/ (exists t' : tm, t1 ==> t')).
+  apply IHhas_type1.
+  assumption.
+  
+  assert (value t2 \/ (exists t' : tm, t2 ==> t')).
+   apply IHhas_type2.
+   assumption.
+   
+   inversion H1.
+    inversion H2.
+     inversion H3.
+      subst.
+      exists (subst t2 x t).
+      apply ST_AppAbs.
+      assumption.
+      
+      subst.
+      inversion H.
+      
+      subst.
+      inversion H.
+      
+     inversion H4.
+     exists (tm_app t1 x).
+     apply ST_App2.
+      assumption.
+      
+      assumption.
+      
+    inversion H3.
+    exists (tm_app x t2).
+    apply ST_App1.
+    assumption.
+    
+ left.
+ auto.
+ 
+ left.
+ auto.
+ 
+ right.
+ assert (value t1 \/ (exists t' : tm, t1 ==> t')).
+  apply IHhas_type1.
+  assumption.
+  
+  inversion H2.
+   inversion H3.
+    subst.
+    inversion H.
+    
+    subst.
+    exists t2.
+    apply ST_IfTrue.
+    
+    subst.
+    exists t3.
+    apply ST_IfFalse.
+    
+   inversion H3.
+   exists (tm_if x t2 t3).
+   apply ST_If.
+   assumption.
+Qed.
+
+Theorem progress' : forall t T,
+     has_type empty t T ->
+     value t \/ exists t', t ==> t'.
+Proof.
+intros t.
+tm_cases (induction t) Case; intros T Ht; auto.
+ inversion Ht.
+ inversion H1.
+ 
+ right.
+ inversion Ht.
+ subst.
+ assert (value t1 \/ (exists t' : tm, t1 ==> t')).
+  apply IHt1 with (T := ty_arrow T11 T).
+  assumption.
+  
+  assert (value t2 \/ (exists t' : tm, t2 ==> t')).
+   apply IHt2 with T11.
+   assumption.
+   
+   inversion H.
+    inversion H1.
+     subst.
+     inversion H0.
+      exists (subst t2 x t).
+      apply ST_AppAbs.
+      assumption.
+      
+      inversion H3.
+      exists (tm_app (tm_abs x T0 t) x0).
+      apply ST_App2.
+       assumption.
+       
+       assumption.
+       
+     subst.
+     inversion H2.
+     
+     subst.
+     inversion H2.
+     
+    inversion H1.
+    exists (tm_app x t2).
+    apply ST_App1.
+    assumption.
+    
+ right.
+ inversion Ht.
+ subst.
+ assert (value t1 \/ (exists t' : tm, t1 ==> t')).
+  apply IHt1 with ty_Bool.
+  assumption.
+  
+  assert (value t2 \/ (exists t' : tm, t2 ==> t')).
+   apply IHt2 with T.
+   assumption.
+   
+   assert (value t3 \/ (exists t' : tm, t3 ==> t')).
+    apply IHt3 with T.
+    assumption.
+    
+    inversion H.
+     inversion H2.
+      subst.
+      inversion H3.
+      
+      subst.
+      subst.
+      exists t2.
+      apply ST_IfTrue.
+      
+      exists t3.
+      apply ST_IfFalse.
+      
+     inversion H2.
+     exists (tm_if x t2 t3).
+     apply ST_If.
+     assumption.
+Qed.
+
+Theorem types_unique : forall t T Gamma,
+   has_type Gamma t T ->
+      (forall T', has_type Gamma t T' -> T' = T).
+Proof.
+intros t T Gamma H.
+induction H.
+ intros T'.
+ intros H1.
+ inversion H1.
+ subst.
+ subst.
+ auto.
+ eauto   .
+ inversion H1.
+ subst.
+ assert (Some T = Some T').
+  rewrite <- H3.
+  rewrite <- H.
+  reflexivity.
+  
+  inversion H0.
+  reflexivity.
+  
+ intros T'.
+ intros H1.
+ inversion H1.
+ subst.
+ assert (T1 = T12).
+  apply IHhas_type.
+  assumption.
+  
+  rewrite H0.
+  reflexivity.
+  
+ intros T' H1.
+ subst.
+ inversion H1.
+ subst.
+ assert (ty_arrow T0 T' = ty_arrow T11 T12).
+  apply IHhas_type1.
+  assumption.
+  
+  inversion H2.
+  reflexivity.
+  
+ intros T'.
+ intros H.
+ inversion H.
+ reflexivity.
+ 
+ intros.
+ inversion H.
+ reflexivity.
+ 
+ intros T'.
+ intros H2.
+ inversion H2.
+ subst.
+ apply IHhas_type2.
+ assumption.
+Qed.

samples/verilog/button_debounce.v

@@ -0,0 +1,94 @@
+////////////////////////////////////////////////////////////////////////////////
+// Original Author: Schuyler Eldridge
+// Contact Point: Schuyler Eldridge (schuyler.eldridge@gmail.com)
+// button_debounce.v
+// Created: 10/10/2009
+// Modified: 3/20/2012
+//
+// Counter based debounce circuit originally written for EC551 (back
+// in the day) and then modified (i.e. chagned entirely) into 3 always
+// block format. This debouncer generates a signal that goes high for
+// 1 clock cycle after the clock sees an asserted value on the button
+// line. This action is then disabled until the counter hits a
+// specified count value that is determined by the clock frequency and
+// desired debounce frequency. An alternative implementation would not
+// use a counter, but would use the shift register approach, looking
+// for repeated matches (say 5) on the button line.
+// 
+// Copyright (C) 2012 Schuyler Eldridge, Boston University
+//
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU General Public License as published by
+// the Free Software Foundation, either version 3 of the License.
+//
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+// GNU General Public License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+////////////////////////////////////////////////////////////////////////////////
+`timescale 1ns / 1ps
+module button_debounce
+  (
+   input      clk,     // clock
+   input      reset_n, // asynchronous reset 
+   input      button,  // bouncy button
+   output reg debounce // debounced 1-cycle signal
+   );
+  
+  parameter
+    CLK_FREQUENCY  = 66000000,
+    DEBOUNCE_HZ    = 2;
+  // These parameters are specified such that you can choose any power
+  // of 2 frequency for a debouncer between 1 Hz and
+  // CLK_FREQUENCY. Note, that this will throw errors if you choose a
+  // non power of 2 frequency (i.e. count_value evaluates to some
+  // number / 3 which isn't interpreted as a logical right shift). I'm
+  // assuming this will not work for DEBOUNCE_HZ values less than 1,
+  // however, I'm uncertain of the value of a debouncer for fractional
+  // hertz button presses.
+  localparam
+    COUNT_VALUE  = CLK_FREQUENCY / DEBOUNCE_HZ,
+    WAIT         = 0,
+    FIRE         = 1,
+    COUNT        = 2;
+
+  reg [1:0]   state, next_state;
+  reg [25:0]  count;
+  
+  always @ (posedge clk or negedge reset_n)
+    state <= (!reset_n) ? WAIT : next_state;
+
+  always @ (posedge clk or negedge reset_n) begin
+    if (!reset_n) begin
+      debounce <= 0;
+      count    <= 0;
+    end
+    else begin
+      debounce <= 0;
+      count    <= 0;
+      case (state)
+        WAIT: begin
+        end
+        FIRE: begin
+          debounce <= 1;
+        end
+        COUNT: begin
+          count <= count + 1;
+        end
+      endcase 
+    end
+  end
+
+  always @ * begin
+    case (state)
+      WAIT:    next_state = (button)                  ? FIRE : state;
+      FIRE:    next_state = COUNT;
+      COUNT:   next_state = (count > COUNT_VALUE - 1) ? WAIT : state;
+      default: next_state = WAIT;
+    endcase
+  end
+
+endmodule

samples/verilog/control.v

@@ -0,0 +1,155 @@
+`timescale 1ns / 1ps
+// Copyright (C) 2008 Schuyler Eldridge, Boston University
+//
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU General Public License as published by
+// the Free Software Foundation, either version 3 of the License.
+//
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+// GNU General Public License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+module control(clk,en,dsp_sel,an);
+        input clk, en;
+        output [1:0]dsp_sel;
+        output [3:0]an;
+        wire a,b,c,d,e,f,g,h,i,j,k,l;
+        
+        assign an[3] = a;
+        assign an[2] = b;
+        assign an[1] = c;
+        assign an[0] = d;
+        
+        assign dsp_sel[1] = e;
+        
+        assign dsp_sel[0] = i;
+        
+        
+                FDRSE #(
+                .INIT(1'b0) // Initial value of register (1'b0 or 1'b1)
+                ) DFF3(
+                .Q(a), // Data output
+                .C(clk), // Clock input
+                .CE(en), // Clock enable input
+                .D(d), // Data input
+                .R(1'b0), // Synchronous reset input
+                .S(1'b0) // Synchronous set input
+                );
+                FDRSE #(
+                .INIT(1'b1) // Initial value of register (1'b0 or 1'b1)
+                ) DFF2(
+                .Q(b), // Data output
+                .C(clk), // Clock input
+                .CE(en), // Clock enable input
+                .D(a), // Data input
+                .R(1'b0), // Synchronous reset input
+                .S(1'b0) // Synchronous set input
+                );
+                FDRSE #(
+                .INIT(1'b1) // Initial value of register (1'b0 or 1'b1)
+                ) DFF1(
+                .Q(c), // Data output
+                .C(clk), // Clock input
+                .CE(en), // Clock enable input
+                .D(b), // Data input
+                .R(1'b0), // Synchronous reset input
+                .S(1'b0) // Synchronous set input
+                );
+                FDRSE #(
+                .INIT(1'b1) // Initial value of register (1'b0 or 1'b1)
+                ) DFF0(
+                .Q(d), // Data output
+                .C(clk), // Clock input
+                .CE(en), // Clock enable input
+                .D(c), // Data input
+                .R(1'b0), // Synchronous reset input
+                .S(1'b0) // Synchronous set input
+                );
+                
+                
+                FDRSE #(
+                .INIT(1'b1) // Initial value of register (1'b0 or 1'b1)
+                ) DFF7(
+                .Q(e), // Data output
+                .C(clk), // Clock input
+                .CE(en), // Clock enable input
+                .D(h), // Data input
+                .R(1'b0), // Synchronous reset input
+                .S(1'b0) // Synchronous set input
+                );
+                FDRSE #(
+                .INIT(1'b1) // Initial value of register (1'b0 or 1'b1)
+                ) DFF6(
+                .Q(f), // Data output
+                .C(clk), // Clock input
+                .CE(en), // Clock enable input
+                .D(e), // Data input
+                .R(1'b0), // Synchronous reset input
+                .S(1'b0) // Synchronous set input
+                );              
+                FDRSE #(
+                .INIT(1'b0) // Initial value of register (1'b0 or 1'b1)
+                ) DFF5(
+                .Q(g), // Data output
+                .C(clk), // Clock input
+                .CE(en), // Clock enable input
+                .D(f), // Data input
+                .R(1'b0), // Synchronous reset input
+                .S(1'b0) // Synchronous set input
+                );
+                FDRSE #(
+                .INIT(1'b0) // Initial value of register (1'b0 or 1'b1)
+                ) DFF4(
+                .Q(h), // Data output
+                .C(clk), // Clock input
+                .CE(en), // Clock enable input
+                .D(g), // Data input
+                .R(1'b0), // Synchronous reset input
+                .S(1'b0) // Synchronous set input
+                );
+                
+                
+                FDRSE #(
+                .INIT(1'b1) // Initial value of register (1'b0 or 1'b1)
+                ) DFF11(
+                .Q(i), // Data output
+                .C(clk), // Clock input
+                .CE(en), // Clock enable input
+                .D(l), // Data input
+                .R(1'b0), // Synchronous reset input
+                .S(1'b0) // Synchronous set input
+                );
+                FDRSE #(
+                .INIT(1'b0) // Initial value of register (1'b0 or 1'b1)
+                ) DFF10(
+                .Q(j), // Data output
+                .C(clk), // Clock input
+                .CE(en), // Clock enable input
+                .D(i), // Data input
+                .R(1'b0), // Synchronous reset input
+                .S(1'b0) // Synchronous set input
+                );              
+                FDRSE #(
+                .INIT(1'b1) // Initial value of register (1'b0 or 1'b1)
+                ) DFF9(
+                .Q(k), // Data output
+                .C(clk), // Clock input
+                .CE(en), // Clock enable input
+                .D(j), // Data input
+                .R(1'b0), // Synchronous reset input
+                .S(1'b0) // Synchronous set input
+                );
+                FDRSE #(
+                .INIT(1'b0) // Initial value of register (1'b0 or 1'b1)
+                ) DFF8(
+                .Q(l), // Data output
+                .C(clk), // Clock input
+                .CE(en), // Clock enable input
+                .D(k), // Data input
+                .R(1'b0), // Synchronous reset input
+                .S(1'b0) // Synchronous set input
+                );
+endmodule

samples/verilog/hex_display.v

@@ -0,0 +1,54 @@
+/*
+ *  Copyright (c) 2009  Zeus Gomez Marmolejo <zeus@opencores.org>
+ *
+ *  This file is part of the Zet processor. This processor is free
+ *  hardware; you can redistribute it and/or modify it under the terms of
+ *  the GNU General Public License as published by the Free Software
+ *  Foundation; either version 3, or (at your option) any later version.
+ *
+ *  Zet is distrubuted in the hope that it will be useful, but WITHOUT
+ *  ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+ *  or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
+ *  License for more details.
+ *
+ *  You should have received a copy of the GNU General Public License
+ *  along with Zet; see the file COPYING. If not, see
+ *  <http://www.gnu.org/licenses/>.
+ */
+
+module hex_display (
+    input  [15:0] num,
+    input         en,
+
+    output [6:0] hex0,
+    output [6:0] hex1,
+    output [6:0] hex2,
+    output [6:0] hex3
+  );
+
+  // Module instantiations
+  seg_7 hex_group0 (
+    .num (num[3:0]),
+    .en  (en),
+    .seg (hex0)
+  );
+
+  seg_7 hex_group1 (
+    .num (num[7:4]),
+    .en  (en),
+    .seg (hex1)
+  );
+
+  seg_7 hex_group2 (
+    .num (num[11:8]),
+    .en  (en),
+    .seg (hex2)
+  );
+
+  seg_7 hex_group3 (
+    .num (num[15:12]),
+    .en  (en),
+    .seg (hex3)
+  );
+
+endmodule

samples/verilog/mux.v

@@ -0,0 +1,45 @@
+`timescale 1ns / 1ps
+// Copyright (C) 2008 Schuyler Eldridge, Boston University
+//
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU General Public License as published by
+// the Free Software Foundation, either version 3 of the License.
+//
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+// GNU General Public License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+module mux(opA,opB,sum,dsp_sel,out);
+	input [3:0] opA,opB;
+	input [4:0] sum;
+	input [1:0] dsp_sel;
+	output [3:0] out;
+	
+	reg cout;
+	
+	always @ (sum)
+		begin
+			if (sum[4] == 1)
+				cout <= 4'b0001;
+			else
+				cout <= 4'b0000;
+		end
+	
+	reg out;
+	
+	always @(dsp_sel,sum,cout,opB,opA)
+		begin
+			if (dsp_sel == 2'b00)
+				out <= sum[3:0];
+			else if (dsp_sel == 2'b01)
+				out <= cout;
+			else if (dsp_sel == 2'b10)
+				out <= opB;
+			else if (dsp_sel == 2'b11)
+				out <= opA;
+		end
+
+endmodule

samples/verilog/pipeline_registers.v

@@ -0,0 +1,82 @@
+////////////////////////////////////////////////////////////////////////////////
+// Original Author: Schuyler Eldridge
+// Contact Point: Schuyler Eldridge (schuyler.eldridge@gmail.com)
+// pipeline_registers.v
+// Created: 4.4.2012
+// Modified: 4.4.2012
+//
+// Implements a series of pipeline registers specified by the input
+// parameters BIT_WIDTH and NUMBER_OF_STAGES. BIT_WIDTH determines the
+// size of the signal passed through each of the pipeline
+// registers. NUMBER_OF_STAGES is the number of pipeline registers
+// generated. This accepts values of 0 (yes, it just passes data from
+// input to output...) up to however many stages specified.
+// Copyright (C) 2012 Schuyler Eldridge, Boston University
+//
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU General Public License as published by
+// the Free Software Foundation, either version 3 of the License.
+//
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+// GNU General Public License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+////////////////////////////////////////////////////////////////////////////////
+`timescale 1ns / 1ps
+module pipeline_registers
+  (
+   input                      clk,
+   input                      reset_n,
+   input [BIT_WIDTH-1:0]      pipe_in,
+   output reg [BIT_WIDTH-1:0] pipe_out
+   );
+
+  // WARNING!!! THESE PARAMETERS ARE INTENDED TO BE MODIFIED IN A TOP
+  // LEVEL MODULE. LOCAL CHANGES HERE WILL, MOST LIKELY, BE
+  // OVERWRITTEN!
+  parameter 
+    BIT_WIDTH         = 10,
+    NUMBER_OF_STAGES  = 5;
+
+  // Main generate function for conditional hardware instantiation
+  generate
+    genvar                                 i;
+    // Pass-through case for the odd event that no pipeline stages are
+    // specified.
+    if (NUMBER_OF_STAGES == 0) begin
+      always @ *
+        pipe_out = pipe_in;
+    end
+    // Single flop case for a single stage pipeline
+    else if (NUMBER_OF_STAGES == 1) begin
+      always @ (posedge clk or negedge reset_n)
+        pipe_out <= (!reset_n) ? 0 : pipe_in;
+    end
+    // Case for 2 or more pipeline stages
+    else begin
+      // Create the necessary regs
+      reg [BIT_WIDTH*(NUMBER_OF_STAGES-1)-1:0] pipe_gen;
+      // Create logic for the initial and final pipeline registers
+      always @ (posedge clk or negedge reset_n) begin
+        if (!reset_n) begin
+          pipe_gen[BIT_WIDTH-1:0] <= 0;
+          pipe_out                <= 0;
+        end
+        else begin
+          pipe_gen[BIT_WIDTH-1:0] <= pipe_in;
+          pipe_out                <= pipe_gen[BIT_WIDTH*(NUMBER_OF_STAGES-1)-1:BIT_WIDTH*(NUMBER_OF_STAGES-2)];
+        end
+      end
+      // Create the intermediate pipeline registers if there are 3 or
+      // more pipeline stages
+      for (i = 1; i < NUMBER_OF_STAGES-1; i = i + 1) begin : pipeline
+        always @ (posedge clk or negedge reset_n)
+          pipe_gen[BIT_WIDTH*(i+1)-1:BIT_WIDTH*i] <= (!reset_n) ? 0 : pipe_gen[BIT_WIDTH*i-1:BIT_WIDTH*(i-1)];
+      end
+    end
+  endgenerate
+  
+endmodule

samples/verilog/ps2_mouse.v

@@ -0,0 +1,175 @@
+/*
+ *  PS2 Mouse Interface
+ *  Copyright (C) 2010  Donna Polehn <dpolehn@verizon.net>
+ *
+ *  This file is part of the Zet processor. This processor is free
+ *  hardware; you can redistribute it and/or modify it under the terms of
+ *  the GNU General Public License as published by the Free Software
+ *  Foundation; either version 3, or (at your option) any later version.
+ *
+ *  Zet is distrubuted in the hope that it will be useful, but WITHOUT
+ *  ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+ *  or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
+ *  License for more details.
+ *
+ *  You should have received a copy of the GNU General Public License
+ *  along with Zet; see the file COPYING. If not, see
+ *  <http://www.gnu.org/licenses/>.
+ */
+
+module ps2_mouse (
+    input clk,                // Clock Input
+    input reset,              // Reset Input
+    inout ps2_clk,            // PS2 Clock, Bidirectional
+    inout ps2_dat,            // PS2 Data, Bidirectional
+
+    input  [7:0] the_command,        // Command to send to mouse
+    input        send_command,       // Signal to send
+    output       command_was_sent,   // Signal command finished sending
+    output       error_communication_timed_out,
+
+    output [7:0] received_data,        // Received data
+    output       received_data_en,     // If 1 - new data has been received
+    output       start_receiving_data,
+    output       wait_for_incoming_data
+  );
+
+  // --------------------------------------------------------------------
+  // Internal wires and registers Declarations
+  // --------------------------------------------------------------------
+  wire            ps2_clk_posedge;        // Internal Wires
+  wire            ps2_clk_negedge;
+
+  reg    [7:0]    idle_counter;            // Internal Registers
+  reg             ps2_clk_reg;
+  reg             ps2_data_reg;
+  reg             last_ps2_clk;
+
+  reg    [2:0]    ns_ps2_transceiver;        // State Machine Registers
+  reg    [2:0]    s_ps2_transceiver;
+
+  // --------------------------------------------------------------------
+  // Constant Declarations
+  // --------------------------------------------------------------------
+  localparam  PS2_STATE_0_IDLE            = 3'h0,        // states
+              PS2_STATE_1_DATA_IN         = 3'h1,
+              PS2_STATE_2_COMMAND_OUT     = 3'h2,
+              PS2_STATE_3_END_TRANSFER    = 3'h3,
+              PS2_STATE_4_END_DELAYED     = 3'h4;
+
+  // --------------------------------------------------------------------
+  // Finite State Machine(s)
+  // --------------------------------------------------------------------
+  always @(posedge clk) begin
+    if(reset == 1'b1) s_ps2_transceiver <= PS2_STATE_0_IDLE;
+    else              s_ps2_transceiver <= ns_ps2_transceiver;
+  end
+
+  always @(*) begin
+    ns_ps2_transceiver = PS2_STATE_0_IDLE;        // Defaults
+
+    case (s_ps2_transceiver)
+    PS2_STATE_0_IDLE:
+        begin
+            if((idle_counter == 8'hFF) && (send_command == 1'b1))
+                ns_ps2_transceiver = PS2_STATE_2_COMMAND_OUT;
+            else if ((ps2_data_reg == 1'b0) && (ps2_clk_posedge == 1'b1))
+                ns_ps2_transceiver = PS2_STATE_1_DATA_IN;
+            else ns_ps2_transceiver = PS2_STATE_0_IDLE;
+        end
+    PS2_STATE_1_DATA_IN:
+        begin
+            // if((received_data_en == 1'b1)  && (ps2_clk_posedge == 1'b1))
+            if((received_data_en == 1'b1))   ns_ps2_transceiver = PS2_STATE_0_IDLE;
+            else                             ns_ps2_transceiver = PS2_STATE_1_DATA_IN;
+        end
+    PS2_STATE_2_COMMAND_OUT:
+        begin
+            if((command_was_sent == 1'b1) || (error_communication_timed_out == 1'b1))
+                ns_ps2_transceiver = PS2_STATE_3_END_TRANSFER;
+            else ns_ps2_transceiver = PS2_STATE_2_COMMAND_OUT;
+        end
+    PS2_STATE_3_END_TRANSFER:
+        begin
+            if(send_command == 1'b0) ns_ps2_transceiver = PS2_STATE_0_IDLE;
+            else if((ps2_data_reg == 1'b0) && (ps2_clk_posedge == 1'b1))
+                ns_ps2_transceiver = PS2_STATE_4_END_DELAYED;
+            else ns_ps2_transceiver = PS2_STATE_3_END_TRANSFER;
+        end
+    PS2_STATE_4_END_DELAYED:
+        begin
+            if(received_data_en == 1'b1) begin
+                if(send_command == 1'b0) ns_ps2_transceiver = PS2_STATE_0_IDLE;
+                else                     ns_ps2_transceiver = PS2_STATE_3_END_TRANSFER;
+            end
+            else ns_ps2_transceiver = PS2_STATE_4_END_DELAYED;
+        end
+
+    default:
+            ns_ps2_transceiver = PS2_STATE_0_IDLE;
+    endcase
+  end
+
+  // --------------------------------------------------------------------
+  // Sequential logic
+  // --------------------------------------------------------------------
+  always @(posedge clk) begin
+    if(reset == 1'b1)     begin
+        last_ps2_clk    <= 1'b1;
+        ps2_clk_reg     <= 1'b1;
+        ps2_data_reg    <= 1'b1;
+    end
+    else begin
+        last_ps2_clk    <= ps2_clk_reg;
+        ps2_clk_reg     <= ps2_clk;
+        ps2_data_reg    <= ps2_dat;
+    end
+  end
+
+  always @(posedge clk) begin
+    if(reset == 1'b1) idle_counter <= 6'h00;
+    else if((s_ps2_transceiver == PS2_STATE_0_IDLE) && (idle_counter != 8'hFF))
+        idle_counter <= idle_counter + 6'h01;
+    else if (s_ps2_transceiver != PS2_STATE_0_IDLE)
+        idle_counter <= 6'h00;
+  end
+
+  // --------------------------------------------------------------------
+  // Combinational logic
+  // --------------------------------------------------------------------
+  assign ps2_clk_posedge = ((ps2_clk_reg == 1'b1) && (last_ps2_clk == 1'b0)) ? 1'b1 : 1'b0;
+  assign ps2_clk_negedge = ((ps2_clk_reg == 1'b0) && (last_ps2_clk == 1'b1)) ? 1'b1 : 1'b0;
+
+  assign start_receiving_data      = (s_ps2_transceiver == PS2_STATE_1_DATA_IN);
+  assign wait_for_incoming_data    = (s_ps2_transceiver == PS2_STATE_3_END_TRANSFER);
+
+  // --------------------------------------------------------------------
+  // Internal Modules
+  // --------------------------------------------------------------------
+  ps2_mouse_cmdout mouse_cmdout (
+    .clk                           (clk),            // Inputs
+    .reset                         (reset),
+    .the_command                   (the_command),
+    .send_command                  (send_command),
+    .ps2_clk_posedge               (ps2_clk_posedge),
+    .ps2_clk_negedge               (ps2_clk_negedge),
+    .ps2_clk                       (ps2_clk),        // Bidirectionals
+    .ps2_dat                       (ps2_dat),
+    .command_was_sent              (command_was_sent),    // Outputs
+    .error_communication_timed_out (error_communication_timed_out)
+  );
+
+  ps2_mouse_datain mouse_datain (
+    .clk                    (clk),        // Inputs
+    .reset                  (reset),
+    .wait_for_incoming_data (wait_for_incoming_data),
+    .start_receiving_data   (start_receiving_data),
+    .ps2_clk_posedge        (ps2_clk_posedge),
+    .ps2_clk_negedge        (ps2_clk_negedge),
+    .ps2_data               (ps2_data_reg),
+    .received_data          (received_data),   // Outputs
+    .received_data_en       (received_data_en)
+  );
+
+endmodule
+

samples/verilog/sign_extender.v

@@ -0,0 +1,49 @@
+////////////////////////////////////////////////////////////////////////////////
+// Original Author: Schuyler Eldridge
+// Contact Point: Schuyler Eldridge (schuyler.eldridge@gmail.com)
+// sign_extender.v
+// Created: 5.16.2012
+// Modified: 5.16.2012
+//
+// Generic sign extension module
+//
+// Copyright (C) 2012 Schuyler Eldridge, Boston University
+//
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU General Public License as published by
+// the Free Software Foundation, either version 3 of the License.
+//
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+// GNU General Public License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+////////////////////////////////////////////////////////////////////////////////
+`timescale 1ns/1ps
+module sign_extender
+  #(
+    parameter
+    INPUT_WIDTH = 8,
+    OUTPUT_WIDTH = 16
+    )
+  (
+   input [INPUT_WIDTH-1:0] original,
+   output reg [OUTPUT_WIDTH-1:0] sign_extended_original
+   );
+
+  wire [OUTPUT_WIDTH-INPUT_WIDTH-1:0] sign_extend;
+
+  generate
+    genvar                           i;
+    for (i = 0; i < OUTPUT_WIDTH-INPUT_WIDTH; i = i + 1) begin : gen_sign_extend
+      assign sign_extend[i]  = (original[INPUT_WIDTH-1]) ? 1'b1 : 1'b0;
+    end
+  endgenerate
+
+  always @ * begin
+    sign_extended_original  = {sign_extend,original};
+  end
+
+endmodule

samples/verilog/sqrt_pipelined.v

@@ -0,0 +1,154 @@
+////////////////////////////////////////////////////////////////////////////////
+// Original Author: Schuyler Eldridge
+// Contact Point: Schuyler Eldridge (schuyler.eldridge@gmail.com)
+// sqrt_pipelined.v
+// Created: 4.2.2012
+// Modified: 4.5.2012
+//
+// Implements a fixed-point parameterized pipelined square root
+// operation on an unsigned input of any bit length. The number of
+// stages in the pipeline is equal to the number of output bits in the
+// computation. This pipelien sustains a throughput of one computation
+// per clock cycle.
+// 
+// Copyright (C) 2012 Schuyler Eldridge, Boston University
+//
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU General Public License as published by
+// the Free Software Foundation, either version 3 of the License.
+//
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+// GNU General Public License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+////////////////////////////////////////////////////////////////////////////////
+`timescale 1ns / 1ps
+module sqrt_pipelined
+  (
+   input                        clk,        // clock
+   input                        reset_n,    // asynchronous reset
+   input                        start,      // optional start signal
+   input [INPUT_BITS-1:0]       radicand,   // unsigned radicand
+   output reg                   data_valid, // optional data valid signal
+   output reg [OUTPUT_BITS-1:0] root        // unsigned root 
+   );
+
+  // WARNING!!! THESE PARAMETERS ARE INTENDED TO BE MODIFIED IN A TOP
+  // LEVEL MODULE. LOCAL CHANGES HERE WILL, MOST LIKELY, BE
+  // OVERWRITTEN!
+  parameter
+    INPUT_BITS   = 16; // number of input bits (any integer)
+  localparam
+    OUTPUT_BITS  = INPUT_BITS / 2 + INPUT_BITS % 2; // number of output bits
+  
+  reg [OUTPUT_BITS-1:0]         start_gen; // valid data propagation
+  reg [OUTPUT_BITS*INPUT_BITS-1:0] root_gen; // root values
+  reg [OUTPUT_BITS*INPUT_BITS-1:0] radicand_gen; // radicand values
+  wire [OUTPUT_BITS*INPUT_BITS-1:0] mask_gen; // mask values
+
+  // This is the first stage of the pipeline.
+  always @ (posedge clk or negedge reset_n) begin
+    if (!reset_n) begin
+      start_gen[0]                 <= 0;
+      radicand_gen[INPUT_BITS-1:0] <= 0;
+      root_gen[INPUT_BITS-1:0]     <= 0;
+    end
+    else begin
+      start_gen[0] <= start;
+      if ( mask_gen[INPUT_BITS-1:0] <= radicand ) begin
+        radicand_gen[INPUT_BITS-1:0] <= radicand - mask_gen[INPUT_BITS-1:0];
+        root_gen[INPUT_BITS-1:0] <= mask_gen[INPUT_BITS-1:0];
+      end
+      else begin
+        radicand_gen[INPUT_BITS-1:0] <= radicand;
+        root_gen[INPUT_BITS-1:0] <= 0;
+      end
+    end
+  end
+
+  // Main generate loop to create the masks and pipeline stages.
+  generate
+    genvar i;
+    // Generate all the mask values. These are built up in the
+    // following fashion:
+    // LAST MASK:  0x00...001 
+    //             0x00...004  Increasing # OUTPUT_BITS
+    //             0x00...010          |
+    //             0x00...040          v
+    //                 ...
+    // FIRST MASK: 0x10...000  # masks == # OUTPUT_BITS
+    // 
+    // Note that the first mask used can either be of the 0x1... or
+    // 0x4... variety. This is purely determined by the number of
+    // computation stages. However, the last mask used will always be
+    // 0x1 and the second to last mask used will always be 0x4.
+    for (i = 0; i < OUTPUT_BITS; i = i + 1) begin: mask_4
+      if (i % 2) // i is odd, this is a 4 mask
+        assign mask_gen[INPUT_BITS*(OUTPUT_BITS-i)-1:INPUT_BITS*(OUTPUT_BITS-i-1)]  = 4 << 4 * (i/2);
+      else // i is even, this is a 1 mask
+        assign mask_gen[INPUT_BITS*(OUTPUT_BITS-i)-1:INPUT_BITS*(OUTPUT_BITS-i-1)]  = 1 << 4 * (i/2);
+    end
+    // Generate all the pipeline stages to compute the square root of
+    // the input radicand stream. The general approach is to compare
+    // the current values of the root plus the mask to the
+    // radicand. If root/mask sum is greater than the radicand,
+    // subtract the mask and the root from the radicand and store the
+    // radicand for the next stage. Additionally, the root is
+    // increased by the value of the mask and stored for the next
+    // stage. If this test fails, then the radicand and the root
+    // retain their value through to the next stage. The one weird
+    // thing is that the mask indices appear to be incremented by one
+    // additional position. This is not the case, however, because the
+    // first mask is used in the first stage (always block after the
+    // generate statement).
+    for (i = 0; i < OUTPUT_BITS - 1; i = i + 1) begin: pipeline
+      always @ (posedge clk or negedge reset_n) begin : pipeline_stage
+        if (!reset_n) begin
+          start_gen[i+1]                                    <= 0;
+          radicand_gen[INPUT_BITS*(i+2)-1:INPUT_BITS*(i+1)] <= 0;
+          root_gen[INPUT_BITS*(i+2)-1:INPUT_BITS*(i+1)]     <= 0;
+        end
+        else begin
+          start_gen[i+1] <= start_gen[i];
+          if ((root_gen[INPUT_BITS*(i+1)-1:INPUT_BITS*i] + 
+               mask_gen[INPUT_BITS*(i+2)-1:INPUT_BITS*(i+1)]) <= radicand_gen[INPUT_BITS*(i+1)-1:INPUT_BITS*i]) begin
+	    radicand_gen[INPUT_BITS*(i+2)-1:INPUT_BITS*(i+1)] <= radicand_gen[INPUT_BITS*(i+1)-1:INPUT_BITS*i] - 
+                                                                 mask_gen[INPUT_BITS*(i+2)-1:INPUT_BITS*(i+1)] - 
+                                                                 root_gen[INPUT_BITS*(i+1)-1:INPUT_BITS*i];
+	    root_gen[INPUT_BITS*(i+2)-1:INPUT_BITS*(i+1)] <= (root_gen[INPUT_BITS*(i+1)-1:INPUT_BITS*i] >> 1) + 
+                                                             mask_gen[INPUT_BITS*(i+2)-1:INPUT_BITS*(i+1)];
+          end
+          else begin
+	    radicand_gen[INPUT_BITS*(i+2)-1:INPUT_BITS*(i+1)] <= radicand_gen[INPUT_BITS*(i+1)-1:INPUT_BITS*i];
+	    root_gen[INPUT_BITS*(i+2)-1:INPUT_BITS*(i+1)]     <= root_gen[INPUT_BITS*(i+1)-1:INPUT_BITS*i] >> 1;
+          end
+        end
+      end
+    end
+  endgenerate
+
+  // This is the final stage which just implements a rounding
+  // operation. This stage could be tacked on as a combinational logic
+  // stage, but who cares about latency, anyway? This is NOT a true
+  // rounding stage. In order to add convergent rounding, you need to
+  // increase the input bit width by 2 (increase the number of
+  // pipeline stages by 1) and implement rounding in the module that
+  // instantiates this one. 
+  always @ (posedge clk or negedge reset_n) begin
+    if (!reset_n) begin
+      data_valid <= 0;
+      root       <= 0;
+    end
+    else begin
+      data_valid <= start_gen[OUTPUT_BITS-1];
+      if (root_gen[OUTPUT_BITS*INPUT_BITS-1:OUTPUT_BITS*INPUT_BITS-INPUT_BITS] > root_gen[OUTPUT_BITS*INPUT_BITS-1:OUTPUT_BITS*INPUT_BITS-INPUT_BITS])
+        root <= root_gen[OUTPUT_BITS*INPUT_BITS-1:OUTPUT_BITS*INPUT_BITS-INPUT_BITS] + 1;
+      else
+        root  <= root_gen[OUTPUT_BITS*INPUT_BITS-1:OUTPUT_BITS*INPUT_BITS-INPUT_BITS];
+    end
+  end
+
+endmodule

samples/verilog/t_button_debounce.v

@@ -0,0 +1,70 @@
+////////////////////////////////////////////////////////////////////////////////
+// Original Author: Schuyler Eldridge
+// Contact Point: Schuyler Eldridge (schuyler.eldridge@gmail.com)
+// button_debounce.v
+// Created:  4.5.2012
+// Modified: 4.5.2012
+//
+// Testbench for button_debounce.v.
+// 
+// Copyright (C) 2012 Schuyler Eldridge, Boston University
+//
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU General Public License as published by
+// the Free Software Foundation, either version 3 of the License.
+//
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+// GNU General Public License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+////////////////////////////////////////////////////////////////////////////////
+`timescale 1ns / 1ps
+module t_button_debounce();
+
+  parameter
+    CLK_FREQUENCY  = 66000000,
+    DEBOUNCE_HZ    = 2;
+
+  reg clk, reset_n, button;
+  wire debounce;
+  
+  button_debounce
+    #(
+      .CLK_FREQUENCY(CLK_FREQUENCY),
+      .DEBOUNCE_HZ(DEBOUNCE_HZ)
+      )
+  button_debounce
+    (
+     .clk(clk),
+     .reset_n(reset_n),
+     .button(button),
+     .debounce(debounce)
+     );
+
+  initial begin
+    clk          = 1'bx; reset_n = 1'bx; button = 1'bx;
+    #10 reset_n  = 1;
+    #10 reset_n  = 0; clk = 0;
+    #10 reset_n  = 1;
+    #10 button   = 0;
+  end
+
+  always
+    #5 clk  = ~clk;
+
+  always begin
+    #100 button  = ~button;
+    #0.1 button  = ~button;
+    #0.1 button  = ~button;
+    #0.1 button  = ~button;
+    #0.1 button  = ~button;
+    #0.1 button  = ~button;
+    #0.1 button  = ~button;
+    #0.1 button  = ~button;
+    #0.1 button  = ~button;
+  end
+  
+endmodule

samples/verilog/t_div_pipelined.v

@@ -0,0 +1,75 @@
+////////////////////////////////////////////////////////////////////////////////
+// Original Author: Schuyler Eldridge
+// Contact Point: Schuyler Eldridge (schuyler.eldridge@gmail.com)
+// div_pipelined.v
+// Created: 4.3.2012
+// Modified: 4.5.2012
+//
+// Testbench for div_pipelined.v
+//
+// Copyright (C) 2012 Schuyler Eldridge, Boston University
+//
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU General Public License as published by
+// the Free Software Foundation, either version 3 of the License.
+//
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+// GNU General Public License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+////////////////////////////////////////////////////////////////////////////////
+`timescale 1ns / 1ps
+module t_div_pipelined();
+
+  reg clk, start, reset_n;
+  reg [7:0] dividend, divisor;
+  wire      data_valid, div_by_zero;
+  wire [7:0] quotient, quotient_correct;
+
+  parameter
+    BITS  = 8;
+
+  div_pipelined
+    #(
+      .BITS(BITS)
+      )
+  div_pipelined
+    (
+     .clk(clk),
+     .reset_n(reset_n),
+     .dividend(dividend),
+     .divisor(divisor),
+     .quotient(quotient),
+     .div_by_zero(div_by_zero),
+     //     .quotient_correct(quotient_correct),
+     .start(start),
+     .data_valid(data_valid)
+     );
+
+  initial begin
+    #10 reset_n  = 0;
+    #50 reset_n  = 1;
+    #1
+    clk          = 0;
+    dividend     = -1;
+    divisor      = 127;
+    #1000 $finish;
+  end
+
+//  always
+//    #20 dividend  = dividend + 1;
+
+  always begin
+    #10 divisor  = divisor - 1; start = 1;
+    #10 start    = 0;
+  end
+
+  always
+    #5 clk  = ~clk;
+
+  
+endmodule
+  

samples/verilog/t_sqrt_pipelined.v

@@ -0,0 +1,77 @@
+////////////////////////////////////////////////////////////////////////////////
+// Original Author: Schuyler Eldridge
+// Contact Point: Schuyler Eldridge (schuyler.eldridge@gmail.com)
+// t_sqrt_pipelined.v
+// Created: 4.2.2012
+// Modified: 4.5.2012
+//
+// Testbench for generic sqrt operation
+// 
+// Copyright (C) 2012 Schuyler Eldridge, Boston University
+//
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU General Public License as published by
+// the Free Software Foundation, either version 3 of the License.
+//
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+// GNU General Public License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+////////////////////////////////////////////////////////////////////////////////
+`timescale 1ns / 1ps
+module t_sqrt_pipelined();
+
+  parameter 
+    INPUT_BITS  = 4;
+  localparam
+    OUTPUT_BITS  = INPUT_BITS / 2 + INPUT_BITS % 2;
+  
+  reg [INPUT_BITS-1:0] radicand;
+  reg                  clk, start, reset_n;
+
+  wire [OUTPUT_BITS-1:0] root;
+  wire                   data_valid;
+//  wire [7:0] root_good;
+
+  sqrt_pipelined 
+    #(
+      .INPUT_BITS(INPUT_BITS)
+      )
+    sqrt_pipelined 
+      (
+       .clk(clk),
+       .reset_n(reset_n),
+       .start(start),
+       .radicand(radicand), 
+       .data_valid(data_valid),
+       .root(root)
+       );
+
+  initial begin
+    radicand     = 16'bx; clk = 1'bx; start = 1'bx; reset_n = 1'bx;;
+    #10 reset_n  = 0; clk = 0;
+    #50 reset_n  = 1; radicand = 0;
+//    #40 radicand  = 81; start = 1;
+//    #10 radicand  = 16'bx; start = 0;
+    #10000 $finish;
+  end
+
+  always
+    #5 clk = ~clk;
+
+  always begin
+    #10 radicand  = radicand + 1; start = 1;
+    #10 start     = 0;
+  end
+  
+
+//  always begin
+//    #80 start  = 1;
+//    #10 start  = 0;
+//  end
+
+endmodule
+

samples/verilog/vga.v

@@ -0,0 +1,313 @@
+/*
+ *  VGA top level file
+ *  Copyright (C) 2010  Zeus Gomez Marmolejo <zeus@aluzina.org>
+ *
+ *  This file is part of the Zet processor. This processor is free
+ *  hardware; you can redistribute it and/or modify it under the terms of
+ *  the GNU General Public License as published by the Free Software
+ *  Foundation; either version 3, or (at your option) any later version.
+ *
+ *  Zet is distrubuted in the hope that it will be useful, but WITHOUT
+ *  ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+ *  or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
+ *  License for more details.
+ *
+ *  You should have received a copy of the GNU General Public License
+ *  along with Zet; see the file COPYING. If not, see
+ *  <http://www.gnu.org/licenses/>.
+ */
+
+module vga (
+    // Wishbone signals
+    input         wb_clk_i,     // 25 Mhz VDU clock
+    input         wb_rst_i,
+    input  [15:0] wb_dat_i,
+    output [15:0] wb_dat_o,
+    input  [16:1] wb_adr_i,
+    input         wb_we_i,
+    input         wb_tga_i,
+    input  [ 1:0] wb_sel_i,
+    input         wb_stb_i,
+    input         wb_cyc_i,
+    output        wb_ack_o,
+
+    // VGA pad signals
+    output [ 3:0] vga_red_o,
+    output [ 3:0] vga_green_o,
+    output [ 3:0] vga_blue_o,
+    output        horiz_sync,
+    output        vert_sync,
+
+    // CSR SRAM master interface
+    output [17:1] csrm_adr_o,
+    output [ 1:0] csrm_sel_o,
+    output        csrm_we_o,
+    output [15:0] csrm_dat_o,
+    input  [15:0] csrm_dat_i
+  );
+
+
+  // Registers and nets
+  //
+  // csr address
+  reg  [17:1] csr_adr_i;
+  reg         csr_stb_i;
+
+  // Config wires
+  wire [15:0] conf_wb_dat_o;
+  wire        conf_wb_ack_o;
+
+  // Mem wires
+  wire [15:0] mem_wb_dat_o;
+  wire        mem_wb_ack_o;
+
+  // LCD wires
+  wire [17:1] csr_adr_o;
+  wire [15:0] csr_dat_i;
+  wire        csr_stb_o;
+  wire        v_retrace;
+  wire        vh_retrace;
+  wire        w_vert_sync;
+
+  // VGA configuration registers
+  wire        shift_reg1;
+  wire        graphics_alpha;
+  wire        memory_mapping1;
+  wire [ 1:0] write_mode;
+  wire [ 1:0] raster_op;
+  wire        read_mode;
+  wire [ 7:0] bitmask;
+  wire [ 3:0] set_reset;
+  wire [ 3:0] enable_set_reset;
+  wire [ 3:0] map_mask;
+  wire        x_dotclockdiv2;
+  wire        chain_four;
+  wire [ 1:0] read_map_select;
+  wire [ 3:0] color_compare;
+  wire [ 3:0] color_dont_care;
+
+  // Wishbone master to SRAM
+  wire [17:1] wbm_adr_o;
+  wire [ 1:0] wbm_sel_o;
+  wire        wbm_we_o;
+  wire [15:0] wbm_dat_o;
+  wire [15:0] wbm_dat_i;
+  wire        wbm_stb_o;
+  wire        wbm_ack_i;
+
+  wire        stb;
+
+  // CRT wires
+  wire [ 5:0] cur_start;
+  wire [ 5:0] cur_end;
+  wire [15:0] start_addr;
+  wire [ 4:0] vcursor;
+  wire [ 6:0] hcursor;
+  wire [ 6:0] horiz_total;
+  wire [ 6:0] end_horiz;
+  wire [ 6:0] st_hor_retr;
+  wire [ 4:0] end_hor_retr;
+  wire [ 9:0] vert_total;
+  wire [ 9:0] end_vert;
+  wire [ 9:0] st_ver_retr;
+  wire [ 3:0] end_ver_retr;
+
+  // attribute_ctrl wires
+  wire [3:0] pal_addr;
+  wire       pal_we;
+  wire [7:0] pal_read;
+  wire [7:0] pal_write;
+
+  // dac_regs wires
+  wire       dac_we;
+  wire [1:0] dac_read_data_cycle;
+  wire [7:0] dac_read_data_register;
+  wire [3:0] dac_read_data;
+  wire [1:0] dac_write_data_cycle;
+  wire [7:0] dac_write_data_register;
+  wire [3:0] dac_write_data;
+
+  // Module instances
+  //
+  vga_config_iface config_iface (
+    .wb_clk_i (wb_clk_i),
+    .wb_rst_i (wb_rst_i),
+    .wb_dat_i (wb_dat_i),
+    .wb_dat_o (conf_wb_dat_o),
+    .wb_adr_i (wb_adr_i[4:1]),
+    .wb_we_i  (wb_we_i),
+    .wb_sel_i (wb_sel_i),
+    .wb_stb_i (stb & wb_tga_i),
+    .wb_ack_o (conf_wb_ack_o),
+
+    .shift_reg1       (shift_reg1),
+    .graphics_alpha   (graphics_alpha),
+    .memory_mapping1  (memory_mapping1),
+    .write_mode       (write_mode),
+    .raster_op        (raster_op),
+    .read_mode        (read_mode),
+    .bitmask          (bitmask),
+    .set_reset        (set_reset),
+    .enable_set_reset (enable_set_reset),
+    .map_mask         (map_mask),
+    .x_dotclockdiv2   (x_dotclockdiv2),
+    .chain_four       (chain_four),
+    .read_map_select  (read_map_select),
+    .color_compare    (color_compare),
+    .color_dont_care  (color_dont_care),
+
+    .pal_addr  (pal_addr),
+    .pal_we    (pal_we),
+    .pal_read  (pal_read),
+    .pal_write (pal_write),
+
+    .dac_we                  (dac_we),
+    .dac_read_data_cycle     (dac_read_data_cycle),
+    .dac_read_data_register  (dac_read_data_register),
+    .dac_read_data           (dac_read_data),
+    .dac_write_data_cycle    (dac_write_data_cycle),
+    .dac_write_data_register (dac_write_data_register),
+    .dac_write_data          (dac_write_data),
+
+    .cur_start  (cur_start),
+    .cur_end    (cur_end),
+    .start_addr (start_addr),
+    .vcursor    (vcursor),
+    .hcursor    (hcursor),
+
+    .horiz_total  (horiz_total),
+    .end_horiz    (end_horiz),
+    .st_hor_retr  (st_hor_retr),
+    .end_hor_retr (end_hor_retr),
+    .vert_total   (vert_total),
+    .end_vert     (end_vert),
+    .st_ver_retr  (st_ver_retr),
+    .end_ver_retr (end_ver_retr),
+
+    .v_retrace  (v_retrace),
+    .vh_retrace (vh_retrace)
+  );
+
+  vga_lcd lcd (
+    .clk (wb_clk_i),
+    .rst (wb_rst_i),
+
+    .shift_reg1     (shift_reg1),
+    .graphics_alpha (graphics_alpha),
+
+    .pal_addr  (pal_addr),
+    .pal_we    (pal_we),
+    .pal_read  (pal_read),
+    .pal_write (pal_write),
+
+    .dac_we                  (dac_we),
+    .dac_read_data_cycle     (dac_read_data_cycle),
+    .dac_read_data_register  (dac_read_data_register),
+    .dac_read_data           (dac_read_data),
+    .dac_write_data_cycle    (dac_write_data_cycle),
+    .dac_write_data_register (dac_write_data_register),
+    .dac_write_data          (dac_write_data),
+
+    .csr_adr_o (csr_adr_o),
+    .csr_dat_i (csr_dat_i),
+    .csr_stb_o (csr_stb_o),
+
+    .vga_red_o   (vga_red_o),
+    .vga_green_o (vga_green_o),
+    .vga_blue_o  (vga_blue_o),
+    .horiz_sync  (horiz_sync),
+    .vert_sync   (w_vert_sync),
+
+    .cur_start  (cur_start),
+    .cur_end    (cur_end),
+    .vcursor    (vcursor),
+    .hcursor    (hcursor),
+
+    .horiz_total  (horiz_total),
+    .end_horiz    (end_horiz),
+    .st_hor_retr  (st_hor_retr),
+    .end_hor_retr (end_hor_retr),
+    .vert_total   (vert_total),
+    .end_vert     (end_vert),
+    .st_ver_retr  (st_ver_retr),
+    .end_ver_retr (end_ver_retr),
+
+    .x_dotclockdiv2 (x_dotclockdiv2),
+
+    .v_retrace  (v_retrace),
+    .vh_retrace (vh_retrace)
+  );
+
+  vga_cpu_mem_iface cpu_mem_iface (
+    .wb_clk_i (wb_clk_i),
+    .wb_rst_i (wb_rst_i),
+
+    .wbs_adr_i (wb_adr_i),
+    .wbs_sel_i (wb_sel_i),
+    .wbs_we_i  (wb_we_i),
+    .wbs_dat_i (wb_dat_i),
+    .wbs_dat_o (mem_wb_dat_o),
+    .wbs_stb_i (stb & !wb_tga_i),
+    .wbs_ack_o (mem_wb_ack_o),
+
+    .wbm_adr_o (wbm_adr_o),
+    .wbm_sel_o (wbm_sel_o),
+    .wbm_we_o  (wbm_we_o),
+    .wbm_dat_o (wbm_dat_o),
+    .wbm_dat_i (wbm_dat_i),
+    .wbm_stb_o (wbm_stb_o),
+    .wbm_ack_i (wbm_ack_i),
+
+    .chain_four       (chain_four),
+    .memory_mapping1  (memory_mapping1),
+    .write_mode       (write_mode),
+    .raster_op        (raster_op),
+    .read_mode        (read_mode),
+    .bitmask          (bitmask),
+    .set_reset        (set_reset),
+    .enable_set_reset (enable_set_reset),
+    .map_mask         (map_mask),
+    .read_map_select  (read_map_select),
+    .color_compare    (color_compare),
+    .color_dont_care  (color_dont_care)
+  );
+
+  vga_mem_arbitrer mem_arbitrer (
+    .clk_i (wb_clk_i),
+    .rst_i (wb_rst_i),
+
+    .wb_adr_i (wbm_adr_o),
+    .wb_sel_i (wbm_sel_o),
+    .wb_we_i  (wbm_we_o),
+    .wb_dat_i (wbm_dat_o),
+    .wb_dat_o (wbm_dat_i),
+    .wb_stb_i (wbm_stb_o),
+    .wb_ack_o (wbm_ack_i),
+
+    .csr_adr_i (csr_adr_i),
+    .csr_dat_o (csr_dat_i),
+    .csr_stb_i (csr_stb_i),
+
+    .csrm_adr_o (csrm_adr_o),
+    .csrm_sel_o (csrm_sel_o),
+    .csrm_we_o  (csrm_we_o),
+    .csrm_dat_o (csrm_dat_o),
+    .csrm_dat_i (csrm_dat_i)
+  );
+
+  // Continous assignments
+  assign wb_dat_o  = wb_tga_i ? conf_wb_dat_o : mem_wb_dat_o;
+  assign wb_ack_o  = wb_tga_i ? conf_wb_ack_o : mem_wb_ack_o;
+  assign stb       = wb_stb_i & wb_cyc_i;
+  assign vert_sync = ~graphics_alpha ^ w_vert_sync;
+
+  // Behaviour
+  // csr_adr_i
+  always @(posedge wb_clk_i)
+    csr_adr_i <= wb_rst_i ? 17'h0 : csr_adr_o + start_addr[15:1];
+
+  // csr_stb_i
+  always @(posedge wb_clk_i)
+    csr_stb_i <= wb_rst_i ? 1'b0 : csr_stb_o;
+
+endmodule