diff --git a/samples/coq/Basics.v b/samples/coq/Basics.v new file mode 100755 index 00000000..054fcbd8 --- /dev/null +++ b/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. diff --git a/samples/coq/Heap.v b/samples/coq/Heap.v new file mode 100755 index 00000000..8653640d --- /dev/null +++ b/samples/coq/Heap.v @@ -0,0 +1,300 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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. diff --git a/samples/coq/Imp.v b/samples/coq/Imp.v new file mode 100755 index 00000000..36689234 --- /dev/null +++ b/samples/coq/Imp.v @@ -0,0 +1,1558 @@ + +Require Export SfLib. + +Module AExp. + +Inductive aexp : Type := + | ANum : nat -> aexp + | APlus : aexp -> aexp -> aexp + | AMinus : aexp -> aexp -> aexp + | AMult : aexp -> aexp -> aexp. + +Inductive bexp : Type := + | BTrue : bexp + | BFalse : bexp + | BEq : aexp -> aexp -> bexp + | BLe : aexp -> aexp -> bexp + | BNot : bexp -> bexp + | BAnd : bexp -> bexp -> bexp. + +Fixpoint aeval (e: aexp) : nat := + match e with + | ANum n => n + | APlus a1 a2 => (aeval a1) + (aeval a2) + | AMinus a1 a2 => (aeval a1) - (aeval a2) + | AMult a1 a2 => (aeval a1) * (aeval a2) + end. + +Example test_aeval1: + aeval (APlus (ANum 2) (ANum 2)) = 4. +Proof. reflexivity. Qed. + +Fixpoint beval (e: bexp) : bool := + match e with + | BTrue => true + | BFalse => false + | BEq a1 a2 => beq_nat (aeval a1) (aeval a2) + | BLe a1 a2 => ble_nat (aeval a1) (aeval a2) + | BNot b1 => negb (beval b1) + | BAnd b1 b2 => andb (beval b1) (beval b2) + end. + +Fixpoint optimize_0plus (a:aexp) : aexp := + match a with + | ANum n => ANum n + | APlus (ANum 0) e2 => optimize_0plus e2 + | APlus e1 e2 => APlus (optimize_0plus e1) (optimize_0plus e2) + | AMinus e1 e2 => AMinus (optimize_0plus e1) (optimize_0plus e2) + | AMult e1 e2 => AMult (optimize_0plus e1) (optimize_0plus e2) + end. + +Example test_optimize_0plus: + optimize_0plus (APlus (ANum 2) + (APlus (ANum 0) + (APlus (ANum 0) (ANum 1)))) = + APlus (ANum 2) (ANum 1). +Proof. reflexivity. Qed. + +Theorem optimize_0plus_sound: forall e, + aeval (optimize_0plus e) = aeval e. +Proof. +intros e. induction e. + Case "ANum". reflexivity. + Case "APlus". destruct e1. + SCase "e1 = ANum n". destruct n. + SSCase "n = 0". simpl. apply IHe2. + SSCase "n <> 0". simpl. rewrite IHe2. reflexivity. + SCase "e1 = APlus e1_1 e1_2". + simpl. simpl in IHe1. rewrite IHe1. rewrite IHe2. reflexivity. + SCase "e1 = AMinus e1_1 e1_2". + simpl. simpl in IHe1. rewrite IHe1. rewrite IHe2. reflexivity. + SCase "e1 = AMult e1_1 e1_2". + simpl. simpl in IHe1. rewrite IHe1. rewrite IHe2. reflexivity. + Case "AMinus". + simpl. rewrite IHe1. rewrite IHe2. reflexivity. + Case "AMult". + simpl. rewrite IHe1. rewrite IHe2. reflexivity. Qed. + +Theorem optimize_0plus_sound': forall e, + aeval (optimize_0plus e) = aeval e. +Proof. + intros e. + induction e; + try (simpl; rewrite IHe1; rewrite IHe2; reflexivity). + Case "ANum". reflexivity. + Case "APlus". + destruct e1; + try (simpl; simpl in IHe1; rewrite IHe1; rewrite IHe2; reflexivity). + SCase "e1 = ANum n". destruct n; + simpl; rewrite IHe2; reflexivity. Qed. + +Theorem optimize_0plus_sound'': forall e, + aeval (optimize_0plus e) = aeval e. +Proof. + intros e. + induction e; + try (simpl; rewrite IHe1; rewrite IHe2; reflexivity); + try reflexivity. + Case "APlus". + destruct e1; + try (simpl; simpl in IHe1; rewrite IHe1; rewrite IHe2; reflexivity). + SCase "e1 = ANum n". destruct n; + simpl; rewrite IHe2; reflexivity. Qed. + +Tactic Notation "simpl_and_try" tactic(c) := + simpl; + try c. + +Tactic Notation "aexp_cases" tactic(first) ident(c) := + first; + [ Case_aux c "ANum" | Case_aux c "APlus" + | Case_aux c "AMinus" | Case_aux c "AMult" ]. + +Theorem optimize_0plus_sound''': forall e, + aeval (optimize_0plus e) = aeval e. +Proof. + intros e. + aexp_cases (induction e) Case; + try (simpl; rewrite IHe1; rewrite IHe2; reflexivity); + try reflexivity. + + Case "APlus". + aexp_cases (destruct e1) SCase; + try (simpl; simpl in IHe1; rewrite IHe1; rewrite IHe2; reflexivity). + SCase "ANum". destruct n; + simpl; rewrite IHe2; reflexivity. Qed. + + +Fixpoint optimize_0plus_all (b:bexp) : bexp := + match b with + | BTrue => BTrue + | BFalse => BFalse + | BEq a1 a2 => BEq (optimize_0plus a1) (optimize_0plus a2) + | BLe a1 a2 => BLe (optimize_0plus a1) (optimize_0plus a2) + | BNot b1 => BNot b1 + | BAnd b1 b2 => BAnd b1 b2 + end. + +Tactic Notation "bexp_cases" tactic(first) ident(c) := + first; + [ Case_aux c "BTrue" | Case_aux c "BFalse" + | Case_aux c "BEq" | Case_aux c "BLe" | Case_aux c "BNot" + | Case_aux c "BAnd" ]. + +Theorem optimize_0plus_all_sound: forall (e:bexp), + beval (optimize_0plus_all e) = beval e. +Proof. + intros e. + bexp_cases (destruct e) Case; + try (simpl; rewrite optimize_0plus_sound; rewrite optimize_0plus_sound); + try reflexivity. +Qed. + +Fixpoint optimize_and (b: bexp): bexp := + match b with + | BTrue => BTrue + | BFalse => BFalse + | BEq a1 a2 => BEq a1 a2 + | BLe a1 a2 => BLe a1 a2 + | BNot a1 => BNot (optimize_and a1) + | BAnd BFalse a2 => BFalse + | BAnd a1 a2 => BAnd (optimize_and a1) (optimize_and a2) + end. + +Theorem optimize_and_sound: forall (e:bexp), + beval (optimize_and e) = beval e. +Proof. + intros e. + bexp_cases (induction e) Case; + try (simpl; rewrite IHe); + try reflexivity. + Case "BAnd". simpl. + bexp_cases (destruct e1) SCase; + try reflexivity; + try (simpl; rewrite IHe2; reflexivity); + try (simpl; simpl in IHe1; rewrite IHe2; rewrite IHe1; reflexivity). +Qed. + +Module aevalR_first_try. + +Inductive aevalR : aexp -> nat -> Prop := + | E_Anum : forall (n : nat), + aevalR (ANum n) n + | E_APlus : forall (e1 e2 : aexp) (n1 n2 : nat), + aevalR e1 n1 -> aevalR e2 n2 -> aevalR (APlus e1 e2) (n1 + n2) + | E_AMinus: forall (e1 e2 : aexp) (n1 n2 : nat), + aevalR e1 n1 -> aevalR e2 n2 -> aevalR (AMinus e1 e2) (n1 - n2) + | E_AMult : forall (e1 e2 : aexp) (n1 n2 : nat), + aevalR e1 n1 -> aevalR e2 n2 -> aevalR (AMult e1 e2) (n1 * n2). + +Notation "e '==>' n" := (aevalR e n) (at level 40). + +End aevalR_first_try. + +Reserved Notation "e '==>' n" (at level 40). + +Inductive aevalR : aexp -> nat -> Prop := + | E_ANum : forall (n : nat), (ANum n) ==> n + | E_APlus : forall (e1 e2 : aexp) (n1 n2 : nat), + (e1 ==> n1) -> (e2 ==> n2) -> (APlus e1 e2) ==> (n1 + n2) + | E_AMinus : forall (e1 e2 : aexp) (n1 n2 : nat), + (e1 ==> n1) -> (e2 ==> n2) -> (AMinus e1 e2) ==> (n1 - n2) + | E_AMult : forall (e1 e2 : aexp) (n1 n2 : nat), + (e1 ==> n1) -> (e2 ==> n2) -> (AMult e1 e2) ==> (n1 * n2) +where "e '==>' n" := (aevalR e n). + +Inductive bevalR : bexp -> bool -> Prop := + | E_BTrue : bevalR (BTrue) true + | E_BFalse : bevalR (BFalse) false + | E_BEq : forall (e1 e2: aexp) (n1 n2 : nat), + aevalR e1 n1 -> aevalR e2 n2 -> bevalR (BEq e1 e2) (beq_nat n1 n2) + | E_BLe : forall (e1 e2 : aexp) (n1 n2 : nat), + aevalR e1 n1 -> aevalR e2 n2 -> bevalR (BLe e1 e2) (ble_nat n1 n2) + | E_BNot : forall (e1 : bexp) (b : bool), + bevalR e1 b -> bevalR (BNot e1) (negb b) + | E_BAnd : forall (e1 e2 : bexp) (b1 b2 : bool), + bevalR e1 b1 -> bevalR e2 b2 -> bevalR (BAnd e1 e2) (andb b1 b2). + +Tactic Notation "aevalR_cases" tactic(first) ident(c) := + first; + [ Case_aux c "E_Anum" | Case_aux c "E_APlus" + | Case_aux c "E_AMinus" | Case_aux c "E_AMult" ]. + +Theorem aeval_iff_aevalR : forall a n, + (a ==> n) <-> aeval a = n. +Proof. + split. + Case "->". + intros H; induction H; subst; reflexivity; + Case "<-". + generalize dependent n. + induction a; simpl; intros; subst; constructor; + try apply IHa1; try apply IHa2; reflexivity. +Qed. + +Tactic Notation "bevalR_cases" tactic(first) ident(c) := + first; + [ Case_aux c "E_BTrue" | Case_aux c "E_BFalse" + | Case_aux c "E_BEq" | Case_aux c "E_BLe" | Case_aux c "E_BNot" + | Case_aux c "E_BAnd" ]. + +Theorem beval_iff_bevalR : forall a b, + bevalR a b <-> beval a = b. +Proof. +split. +intros H. +induction H. +simpl in |- *. +reflexivity. + +simpl in |- *. +reflexivity. + +simpl in |- *. +apply aeval_iff_aevalR in H. +apply aeval_iff_aevalR in H0. +subst. +reflexivity. + +simpl in |- *. +apply aeval_iff_aevalR in H0. +apply aeval_iff_aevalR in H. +subst. +reflexivity. + +simpl in |- *. +rewrite IHbevalR in |- *. +reflexivity. + +simpl in |- *. +rewrite IHbevalR1 in |- *. +rewrite IHbevalR2 in |- *. +reflexivity. +generalize dependent b. +induction a. +intros b H. subst. constructor. +intros b H. +subst. +constructor. + +intros b H. +rewrite <- H in |- *. +constructor. +simpl in H. +remember (aeval a)as A in *. +assert (aeval a = A). +subst. +reflexivity. + +apply aeval_iff_aevalR in H0. +apply H0. + +remember (aeval a0)as A in *. +assert (aeval a0 = A). +subst. +reflexivity. + +apply aeval_iff_aevalR in H0. +apply H0. + +intros b. +intros H. +simpl in H. +rewrite <- H in |- *. +simpl in |- *. +constructor. +remember (aeval a)as A in *. +assert (aeval a = A). +subst. +reflexivity. + +apply aeval_iff_aevalR in H0. +apply H0. + +remember (aeval a0)as A in *. +assert (aeval a0 = A). +subst. +reflexivity. + +apply aeval_iff_aevalR in H0. +apply H0. + +intros b. +intros H. +simpl in |- *. +simpl in H. +rewrite <- H in |- *. +constructor. +apply IHa. +reflexivity. + +intros b. +simpl in |- *. +intros H. +rewrite <- H in |- *. +constructor. +apply IHa1. +reflexivity. + +apply IHa2. +reflexivity. +Qed. + +End AExp. + +Example silly_presburger_formula : forall m n o p, + m + n <= n + o /\ o + 3 = p + 3 -> + m <= p. +Proof. + intros. omega. +Qed. + +Module Id. + +Inductive id : Type := + Id : nat -> id. + +Definition beq_id id1 id2 := + match (id1, id2) with + (Id n1, Id n2) => beq_nat n1 n2 + end. + +Theorem beq_id_refl : forall i, + true = beq_id i i. +Proof. + intros. destruct i. + apply beq_nat_refl. Qed. + +Theorem beq_id_eq : forall i1 i2, + true = beq_id i1 i2 -> i1 = i2. +Proof. +intros i1 i2. +destruct i1. +destruct i2. +unfold beq_id in |- *. +intros H. +apply beq_nat_eq in H. +subst. +reflexivity. +Qed. + +Theorem beq_id_false_not_eq : forall i1 i2, + beq_id i1 i2 = false -> i1 <> i2. +Proof. +intros i1 i2. +destruct i1. +destruct i2. +unfold beq_id in |- *. +intros H. +intros C. +unfold beq_id in |- *. +assert (false = beq_nat n n0). +subst. +rewrite <- H in |- *. +reflexivity. + +apply beq_false_not_eq in H0. +apply H0. +subst. +inversion C. +reflexivity. +Qed. + +Theorem not_eq_beq_id_false : forall i1 i2, + i1 <> i2 -> beq_id i1 i2 = false. +Proof. + intros i1 i2. + destruct i1. destruct i2. + unfold beq_id in |- *. + intros H. + apply not_eq_beq_false. + intros C. + apply H. + subst. + 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 beq_id_sym : forall i1 i2, + beq_id i1 i2 = beq_id i2 i1. +Proof. + intros i1 i2. + destruct i1. destruct i2. + unfold beq_id. + apply beq_nat_sym. + reflexivity. +Qed. + +End Id. + +Definition state := id -> nat. +Definition empty_state : state := fun _ => 0. +Definition update (st : state) (V:id) (n:nat) : state := + fun V' => if beq_id V V' then n else st V'. + +Theorem update_eq : forall n V st, + (update st V n) V = n. +Proof. +intros n V st. +unfold update. +rewrite <- beq_id_refl. +reflexivity. +Qed. + +Theorem update_neq : forall V2 V1 n st, + beq_id V2 V1 = false -> + (update st V2 n) V1 = (st V1). +Proof. +intros V2 V1 n st. +intros H. +unfold update. +rewrite H. +reflexivity. +Qed. + +Theorem update_example : forall (n:nat), + (update empty_state (Id 2) n) (Id 3) = 0. +Proof. +unfold update. +intros n. +simpl. +unfold empty_state. +reflexivity. +Qed. + +Theorem update_shadow : forall x1 x2 k1 k2 (f:state), + (update (update f k2 x1) k2 x2) k1 = (update f k2 x2) k1. +Proof. +intros x1 x2 k1 k2 f. +unfold update in |- *. +destruct (beq_id k2 k1); + reflexivity. +Qed. + +Theorem update_same : forall x1 k1 k2 (f : state), + f k1 = x1 -> + (update f k1 x1) k2 = f k2. +Proof. +unfold update in |- *. +intros x1 k1 k2 f. +remember (beq_id k1 k2)as A in *. +destruct A. +apply beq_id_eq in HeqA. +subst. +intros H. +subst. +reflexivity. + +intros H. +reflexivity. +Qed. + + +Theorem update_permute : forall x1 x2 k1 k2 k3 f, + beq_id k2 k1 = false -> + (update (update f k2 x1) k1 x2) k3 = (update (update f k1 x2) k2 x1) k3. +Proof. +intros x1 x2 k1 k2 k3 f. +intros H. +unfold update in |- *. +remember (beq_id k1 k3)as A1 in *. +destruct A1. +apply beq_id_eq in HeqA1. +rewrite HeqA1 in H. +destruct (beq_id k2 k3). +inversion H. + +reflexivity. + +remember (beq_id k2 k3)as B in *. +destruct B; +try reflexivity. +Qed. + +Inductive aexp : Type := + | ANum : nat -> aexp + | AId : id -> aexp (* <----- NEW *) + | APlus : aexp -> aexp -> aexp + | AMinus : aexp -> aexp -> aexp + | AMult : aexp -> aexp -> aexp. + +Tactic Notation "aexp_cases" tactic(first) ident(c) := + first; + [ Case_aux c "ANum" | Case_aux c "AId" | Case_aux c "APlus" + | Case_aux c "AMinus" | Case_aux c "AMult" ]. + +Definition X : id := Id 0. +Definition Y : id := Id 1. +Definition Z : id := Id 2. + +Inductive bexp : Type := + | BTrue : bexp + | BFalse : bexp + | BEq : aexp -> aexp -> bexp + | BLe : aexp -> aexp -> bexp + | BNot : bexp -> bexp + | BAnd : bexp -> bexp -> bexp. + +Tactic Notation "bexp_cases" tactic(first) ident(c) := + first; + [ Case_aux c "BTrue" | Case_aux c "BFalse" | Case_aux c "BEq" + | Case_aux c "BLe" | Case_aux c "BNot" | Case_aux c "BAnd" ]. + +Fixpoint aeval (st : state) (e : aexp) : nat := + match e with + | ANum n => n + | AId i => st i (* <----- NEW *) + | APlus a1 a2 => (aeval st a1) + (aeval st a2) + | AMinus a1 a2 => (aeval st a1) - (aeval st a2) + | AMult a1 a2 => (aeval st a1) * (aeval st a2) + end. + +Fixpoint beval (st : state) (e : bexp) : bool := + match e with + | BTrue => true + | BFalse => false + | BEq a1 a2 => beq_nat (aeval st a1) (aeval st a2) + | BLe a1 a2 => ble_nat (aeval st a1) (aeval st a2) + | BNot b1 => negb (beval st b1) + | BAnd b1 b2 => andb (beval st b1) (beval st b2) + end. + +Example aexp1 : + aeval (update empty_state X 5) + (APlus (ANum 3) (AMult (AId X) (ANum 2))) + = 13. +Proof. reflexivity. Qed. + +Example bexp1 : + beval (update empty_state X 5) + (BAnd BTrue (BNot (BLe (AId X) (ANum 4)))) + = true. +Proof. reflexivity. Qed. + +Inductive com : Type := + | CSkip : com + | CAss : id -> aexp -> com + | CSeq : com -> com -> com + | CIf : bexp -> com -> com -> com + | CWhile : bexp -> com -> com. + +Tactic Notation "com_cases" tactic(first) ident(c) := + first; + [ Case_aux c "SKIP" | Case_aux c "::=" | Case_aux c ";" + | Case_aux c "IFB" | Case_aux c "WHILE" ]. + +Notation "'SKIP'" := + CSkip. +Notation "l '::=' a" := + (CAss l a) (at level 60). +Notation "c1 ; c2" := + (CSeq c1 c2) (at level 80, right associativity). +Notation "'WHILE' b 'DO' c 'END'" := + (CWhile b c) (at level 80, right associativity). +Notation "'IFB' e1 'THEN' e2 'ELSE' e3 'FI'" := + (CIf e1 e2 e3) (at level 80, right associativity). + +Definition plus2 : com := + X ::= (APlus (AId X) (ANum 2)). + +Definition XtimesYinZ : com := + Z ::= (AMult (AId X) (AId Y)). + +Definition subtract_slowly_body : com := + Z ::= AMinus (AId Z) (ANum 1); + X ::= AMinus (AId X) (ANum 1). + +Definition subtract_slowly : com := + WHILE BNot (BEq (AId X) (ANum 0)) DO + subtract_slowly_body + END. + +Definition subtract_3_from_5_slowly : com := + X ::= ANum 3 ; + Z ::= ANum 5 ; + subtract_slowly. + +Definition loop : com := + WHILE BTrue DO + SKIP + END. + +Definition fact_body : com := + Y ::= AMult (AId Y) (AId Z) ; + Z ::= AMinus (AId Z) (ANum 1). + +Definition fact_loop : com := + WHILE BNot (BEq (AId Z) (ANum 0)) DO + fact_body + END. + +Definition fact_com : com := + Z ::= AId X ; + Y ::= ANum 1 ; + fact_loop. + +Fixpoint ceval_step1 (st:state) (c:com) : state := + match c with + | SKIP => st + | l ::= a1 => + update st l (aeval st a1) + | c1 ; c2 => + let st' := ceval_step1 st c1 in + ceval_step1 st' c2 + | IFB b THEN c1 ELSE c2 FI => + if (beval st b) then ceval_step1 st c1 else ceval_step1 st c2 + | WHILE b1 DO c1 END => + st (* bogus *) + end. + +Fixpoint ceval_step2 (st: state) (c:com) (i:nat) : state := + match i with + | O => empty_state + | S i' => + match c with + | SKIP => st + | l ::= a1 => + update st l (aeval st a1) + | c1 ; c2 => let st' := ceval_step2 st c1 i' in + ceval_step2 st' c2 i' + | IFB b THEN c1 ELSE c2 FI => + if (beval st b) then ceval_step2 st c1 i' else ceval_step2 st c2 i' + | WHILE b1 DO c1 END => + if (beval st b1) + then let st' := ceval_step2 st c1 i' in + ceval_step2 st' c i' + else st + end + end. + +Fixpoint ceval_step3 (st: state) (c:com) (i:nat) : option state := + match i with + | O => None + | S i' => + match c with + | SKIP => Some st + | l ::= a1 => + Some (update st l (aeval st a1)) + | c1 ; c2 => match (ceval_step3 st c1 i') with + | Some st' => ceval_step3 st' c2 i' + | None => None + end + | IFB b THEN c1 ELSE c2 FI => + if (beval st b) then ceval_step3 st c1 i' else ceval_step3 st c2 i' + | WHILE b1 DO c1 END => + if (beval st b1) + then match (ceval_step3 st c1 i') with + | Some st' => ceval_step3 st' c i' + | None => None + end + else Some st + end + end. + +Definition bind_option {X Y : Type} (xo : option X) (f : X -> option Y) : option Y := + match xo with + | None => None + | Some x => f x + end. + +Fixpoint ceval_step (st: state) (c:com) (i:nat) : option state := + match i with + | O => None + | S i' => + match c with + | SKIP => Some st + | l ::= a1 => + Some (update st l (aeval st a1)) + | c1 ; c2 => bind_option (ceval_step st c1 i') + (fun st' => ceval_step st' c2 i') + | IFB b THEN c1 ELSE c2 FI => + if (beval st b) then ceval_step st c1 i' else ceval_step st c2 i' + | WHILE b1 DO c1 END => + if (beval st b1) + then bind_option (ceval_step st c1 i') + (fun st' => ceval_step st' c i') + else Some st + end + end. + +Definition test_ceval (st:state) (c:com) := + match ceval_step st c 500 with + | None => None + | Some st => Some (st X, st Y, st Z) + end. + +Definition pup_to_n: com := + (Y ::= (ANum 0) ; + WHILE (BLe (ANum 1) (AId X)) DO + Y ::= (APlus (AId X) (AId Y)) ; + X ::= (AMinus (AId X) (ANum 1)) + END) . + +Example pup_to_n_1 : + test_ceval (update empty_state X 5) pup_to_n + = Some (0, 15, 0). +Proof. reflexivity. Qed. + +Definition ceval_even : com := + WHILE (BLe (ANum 2) (AId X)) DO + X ::= (AMinus (AId X) (ANum 2)) + END ; + Z ::= (AId X). + +Example ceval_even_test1 : + test_ceval (update empty_state X 20) ceval_even + = Some (0, 0, 0). +Proof. reflexivity. Qed. + +Example ceval_even_test2 : + test_ceval (update empty_state X 21) ceval_even + = Some (1, 0, 1). +Proof. reflexivity. Qed. + +Example ceval_even_test3 : + test_ceval (update empty_state X 2) ceval_even + = Some (0, 0, 0). +Proof. reflexivity. Qed. + +Example ceval_even_test4 : + test_ceval (update empty_state X 1) ceval_even + = Some (1, 0, 1). +Proof. reflexivity. Qed. + +Example ceval_even_test5 : + test_ceval (update empty_state X 0) ceval_even + = Some (0, 0, 0). +Proof. reflexivity. Qed. + +Reserved Notation "cl '/' st '==>' st'" (at level 40, st at level 39). + +Inductive ceval : com -> state -> state -> Prop := + | E_Skip : forall st, + SKIP / st ==> st + | E_Ass : forall st al n l, + aeval st al = n -> + (l ::= al) / st ==> (update st l n) + | E_Seq : forall c1 c2 st st' st'', + c1 / st ==> st' -> + c2 / st' ==> st'' -> + (c1 ; c2) / st ==> st'' + | E_IfTrue : forall st st' b1 c1 c2, + beval st b1 = true -> + c1 / st ==> st' -> + (IFB b1 THEN c1 ELSE c2 FI) / st ==> st' + | E_IfFalse : forall st st' b1 c1 c2, + beval st b1 = false -> + c2 / st ==> st' -> + (IFB b1 THEN c1 ELSE c2 FI) / st ==> st' + | E_WhileEnd : forall b1 st c1, + beval st b1 = false -> + (WHILE b1 DO c1 END) / st ==> st + | E_WhileLoop : forall st st' st'' b1 c1, + beval st b1 = true -> + c1 / st ==> st' -> + (WHILE b1 DO c1 END) / st' ==> st'' -> + (WHILE b1 DO c1 END) / st ==> st'' + + where "c1 '/' st '==>' st'" := (ceval c1 st st'). + +Tactic Notation "ceval_cases" tactic(first) ident(c) := + first; + [ Case_aux c "E_Skip" | Case_aux c "E_Ass" | Case_aux c "E_Seq" + | Case_aux c "E_IfTrue" | Case_aux c "E_IfFalse" + | Case_aux c "E_WhileEnd" | Case_aux c "E_WhileLoop" ]. + +Example ceval_example1 : + (X ::= ANum 2; + IFB BLe (AId X) (ANum 1) + THEN Y ::= ANum 3 + ELSE Z ::= ANum 4 + FI) + / empty_state ==> (update (update empty_state X 2) Z 4). +Proof. +(* We must supply the intermediate state *) + apply E_Seq with (update empty_state X 2). + Case "assignment command". + apply E_Ass. reflexivity. + Case "if command". + apply E_IfFalse. + reflexivity. + apply E_Ass. reflexivity. Qed. + +Example ceval_example2: + (X ::= ANum 0; Y ::= ANum 1; Z ::= ANum 2) / empty_state ==> + (update (update (update empty_state X 0) Y 1) Z 2). +Proof. +apply E_Seq with (update empty_state X 0); +try (apply E_Ass; reflexivity). + +apply E_Seq with (update (update empty_state X 0) Y 1); +try (apply E_Ass; reflexivity). +Qed. + +Theorem ceval_step__ceval : forall c st st', + (exists i, ceval_step st c i = Some st') -> + c / st ==> st'. +Proof. +intros c st st' H. +inversion H as (i, E). +clear H. +generalize dependent st'. +generalize dependent st. +generalize dependent c. +induction i as [| i']. + intros c st st' H. + inversion H. + + intros c st st' H. + com_cases (destruct c) SCase; simpl in H; inversion H; subst; clear H. + apply E_Skip. + + apply E_Ass. + reflexivity. + + remember (ceval_step st c1 i')as r1 in *. + destruct r1. + apply E_Seq with s. + apply IHi'. + rewrite Heqr1 in |- *. + reflexivity. + + apply IHi'. + simpl in H1. + assumption. + + inversion H1. + + remember (beval st b)as r in *. + destruct r. + apply E_IfTrue. + rewrite Heqr in |- *. + reflexivity. + + apply IHi'. + assumption. + + apply E_IfFalse. + rewrite Heqr in |- *. + reflexivity. + + apply IHi'. + assumption. + + remember (beval st b)as r in *. + destruct r. + remember (ceval_step st c i')as r1 in *. + destruct r1. + apply E_WhileLoop with s. + rewrite Heqr in |- *. + reflexivity. + + apply IHi'. + rewrite Heqr1 in |- *. + reflexivity. + + apply IHi'. + simpl in H1. + assumption. + + inversion H1. + + inversion H1. + apply E_WhileEnd. + rewrite Heqr in |- *. + subst. + reflexivity. +Qed. + +Theorem ceval_step_more: forall i1 i2 st st' c, + i1 <= i2 -> ceval_step st c i1 = Some st' -> + ceval_step st c i2 = Some st'. +Proof. +induction i1 as [| i1']; intros i2 st st' c Hle Hceval. +inversion Hceval. + +destruct i2 as [| i2']. +inversion Hle. + +assert (i1' <= i2') as Hle' by complete omega. +com_cases (destruct c) SCase. +SCase "SKIP". +simpl in Hceval. +inversion Hceval. +reflexivity. + +SCase "::=". +simpl in Hceval. +inversion Hceval. +reflexivity. + +SCase ";". +simpl in Hceval. +simpl in |- *. +remember (ceval_step st c1 i1')as st1'o in *. +destruct st1'o. +SSCase "st1'o = Some". +symmetry in Heqst1'o. +apply (IHi1' i2') in Heqst1'o; try assumption. +rewrite Heqst1'o in |- *. +simpl in |- *. +simpl in Hceval. +apply (IHi1' i2') in Hceval; try assumption. + +inversion Hceval. + +SCase "IFB". +simpl in Hceval. +simpl in |- *. +remember (beval st b)as bval in *. +destruct bval; apply (IHi1' i2') in Hceval; assumption. + +SCase "WHILE". +simpl in Hceval. +simpl in |- *. +destruct (beval st b); try assumption. +remember (ceval_step st c i1')as st1'o in *. +destruct st1'o. +SSCase "st1'o = Some". +symmetry in Heqst1'o. +apply (IHi1' i2') in Heqst1'o; try assumption. +rewrite Heqst1'o in |- *. +simpl in |- *. +simpl in Hceval. +apply (IHi1' i2') in Hceval; try assumption. + +SSCase "i1'o = None". +simpl in Hceval. +inversion Hceval. +Qed. + +Theorem ceval__ceval_step : forall c st st', + c / st ==> st' -> + exists i, ceval_step st c i = Some st'. +Proof. + intros c st st' Hce. + ceval_cases (induction Hce) Case. + exists 1%nat. + simpl in |- *. + reflexivity. + + simpl in |- *. + exists 1%nat. + simpl in |- *. + rewrite H in |- *. + reflexivity. + inversion IHHce1 as (x1). + inversion IHHce2 as (x2). + exists (S (x1 + x2)). + simpl in |- *. + assert (ceval_step st c1 (x1 + x2) = Some st'). + apply ceval_step_more with x1. + omega. + + assumption. + + rewrite H1 in |- *. + simpl in |- *. + apply ceval_step_more with x2. + omega. + + assumption. + + inversion IHHce. + exists (S x). + simpl in |- *. + simpl in |- *. + rewrite H in |- *. + apply H0. + + inversion IHHce. + exists (S x). + simpl in |- *. + simpl in |- *. + rewrite H in |- *. + assumption. + + exists 1%nat. + simpl in |- *. + rewrite H in |- *. + reflexivity. + + inversion IHHce1. + simpl in |- *. + inversion IHHce2. + exists (S (x + x0)). + simpl in |- *. + simpl in |- *. + rewrite H in |- *. + assert (ceval_step st c1 (x + x0) = Some st'). + apply ceval_step_more with x. + omega. + + assumption. + + rewrite H2 in |- *. + simpl in |- *. + apply ceval_step_more with x0. + omega. + + assumption. +Qed. + +Theorem ceval_and_ceval_step_coincide: forall c st st', + c / st ==> st' <-> exists i, ceval_step st c i = Some st'. +Proof. + intros c st st'. + split. apply ceval__ceval_step. apply ceval_step__ceval. +Qed. + +Theorem ceval_deterministic : forall c st st1 st2, + c / st ==> st1 -> + c / st ==> st2 -> + st1 = st2. +Proof. +intros c st st1 st2 He1 He2. +apply ceval__ceval_step in He1. +apply ceval__ceval_step in He2. +inversion He1 as (i1, E1). +inversion He2 as (i2, E2). +apply ceval_step_more with (i2 := i1 + i2) in E1. +apply ceval_step_more with (i2 := i1 + i2) in E2. +rewrite E1 in E2. +inversion E2. +reflexivity. + +omega. + +omega. +Qed. + +Theorem plus2_spec : forall st n st', + st X = n -> + plus2 / st ==> st' -> + st' X = n + 2. +Proof. +intros st n st' HX Heval. +inversion Heval. +subst. +apply update_eq. +Qed. + + +Theorem XtimesYinZ_spec : forall st nx ny st', + st X = nx -> + st Y = ny -> + XtimesYinZ / st ==> st' -> + st' Z = nx * ny. +Proof. +intros st nx ny st' H1 H2 Heval. +inversion Heval. +subst. simpl. +apply update_eq. +Qed. + +Theorem loop_never_stops : forall st st', + ~(loop / st ==> st'). +Proof. + intros st st' contra. unfold loop in contra. + remember (WHILE BTrue DO SKIP END) as loopdef. + induction contra. + simpl in Heqloopdef. + inversion Heqloopdef. + + inversion Heqloopdef. + + inversion Heqloopdef. + + inversion Heqloopdef. + + inversion Heqloopdef. + + inversion Heqloopdef. + subst. + simpl in H. + inversion H. + + inversion Heqloopdef. + subst. + inversion contra1. + subst. + apply IHcontra2. + reflexivity. +Qed. + +Fixpoint no_whiles (c : com) : bool := + match c with + | SKIP => true + | _ ::= _ => true + | c1 ; c2 => andb (no_whiles c1) (no_whiles c2) + | IFB _ THEN ct ELSE cf FI => andb (no_whiles ct) (no_whiles cf) + | WHILE _ DO _ END => false + end. + +Inductive no_Whiles : com -> Prop := + | noWhilesSKIP : no_Whiles (SKIP) + | noWhilesAss : forall a1 a2, no_Whiles (a1 ::= a2) + | noWhilesSeq : forall (a1 a2 : com), no_Whiles a1 -> no_Whiles a2 -> no_Whiles (a1 ; a2) + | noWhilesIf : forall (b : bexp) (a1 a2 : com), + no_Whiles a1 -> no_Whiles a2 -> + no_Whiles (IFB b THEN a1 ELSE a2 FI). + +Theorem no_whiles_eqv: + forall c, no_whiles c = true <-> no_Whiles c. +Proof. +split. +induction c. +intros H. +apply noWhilesSKIP. + +simpl in |- *. +intros H. +apply noWhilesAss. + +intros H. +apply noWhilesSeq. +apply IHc1. +simpl in H. +simpl in H. +auto. +eauto . +apply andb_true_elim1 in H. +apply H. + +apply IHc2. +simpl in H. +apply andb_true_elim2 in H. +assumption. + +simpl in |- *. +intros H. +apply noWhilesIf. +apply andb_true_elim1 in H. +apply IHc1. +assumption. + +apply IHc2. +apply andb_true_elim2 in H. +assumption. + +simpl in |- *. +intros contra. +inversion contra. + +intros H. +induction H. +simpl in |- *. +reflexivity. + +reflexivity. + +simpl in |- *. +assert (no_whiles a1 = true /\ no_whiles a2 = true). +split. +assumption. + +assumption. + +eauto . +auto. +apply andb_true_intro. +apply H1. + +simpl in |- *. +assert (no_whiles a1 = true /\ no_whiles a2 = true). +split. +assumption. + +assumption. + +apply andb_true_intro. +assumption. +Qed. + +Theorem no_whiles_terminate : forall (c : com) (st:state), + no_whiles c = true -> + exists i, exists st', ceval_step st c i = Some st'. +Proof. +induction c. +intros st. +simpl in |- *. +intros H. +exists 1%nat. +exists st. +reflexivity. + +simpl in |- *. +intros st. +intros H. +exists 1%nat. +simpl in |- *. +exists (update st i (aeval st a)). +reflexivity. + +intros st. +intros H. +inversion H. +assert (no_whiles c1 = true). +apply andb_true_elim1 in H1. +assumption. + +assert (no_whiles c2 = true). +apply andb_true_elim2 in H1. +assumption. + +apply IHc1 with st in H0. +inversion H0. +inversion H3. +apply IHc2 with x0 in H2. +inversion H2. +inversion H5. +exists (S (x + x1)). +exists x2. +simpl in |- *. +remember (ceval_step st c1 (x + x1))as r in *. +destruct r. +symmetry in Heqr. +assert (x <= x + x1). +omega. + +simpl in |- *. +apply ceval_step_more with x1. +omega. + +apply ceval_step_more with (i2 := x + x1) in H4. +assert (Some x0 = Some s). +auto. +eauto . +rewrite <- Heqr in |- *. +rewrite <- H4 in |- *. +reflexivity. + +inversion H8. +rewrite <- H10 in |- *. +assumption. + +omega. + +simpl in |- *. +assert (x <= x + x1). +omega. + +apply ceval_step_more with (i2 := x + x1) in H4. +rewrite H4 in Heqr. +inversion Heqr. + +omega. + +intros st. +simpl in |- *. +intros H1. +simpl in |- *. +assert (no_whiles c1 = true). +apply andb_true_elim1 in H1. +assumption. + +assert (no_whiles c2 = true). +apply andb_true_elim2 in H1. +assumption. + +apply IHc1 with st in H. +apply IHc2 with st in H0. +inversion H. +inversion H0. +exists (S (x + x0)). +simpl in |- *. +destruct (beval st b). +inversion H2. +exists x1. +apply ceval_step_more with x. +omega. + +assumption. + +inversion H3. +exists x1. +apply ceval_step_more with x0. +omega. + +assumption. + +intros st H. +inversion H. +Qed. + +Fixpoint beval_short_circuit (st : state) (e: bexp) : bool := + match e with + | BTrue => true + | BFalse => false + | BEq a1 a2 => beq_nat (aeval st a1) (aeval st a2) + | BLe a1 a2 => ble_nat (aeval st a1) (aeval st a2) + | BNot b1 => negb (beval_short_circuit st b1) + | BAnd b1 b2 => match (beval_short_circuit st b1) with + | true => (beval st b2) + | false => false + end + end. + +Theorem beval_short_circuit_eqv : forall (e : bexp) (st : state), + beval st e = beval_short_circuit st e. +Proof. +induction e. +intros st. +simpl in |- *. +reflexivity. + +reflexivity. + +simpl in |- *. +reflexivity. + +reflexivity. + +intros st. +simpl in |- *. +rewrite IHe in |- *. +reflexivity. + +simpl in |- *. +intros st. +rewrite IHe1 in |- *. +rewrite IHe2 in |- *. +destruct (beval_short_circuit st e1). +simpl in |- *. +reflexivity. + +reflexivity. +Qed. + +Inductive sinstr : Type := + | SPush : nat -> sinstr + | SLoad : id -> sinstr + | SPlus : sinstr + | SMinus : sinstr + | SMult : sinstr. + +Fixpoint s_execute (st : state) (stack : list nat) (prog : list sinstr) + : list nat := +match ( prog ) with +| [] =>stack +|a :: l + => match (a) with + | SPush n => s_execute st (cons n stack) l + | SLoad i => s_execute st (cons (st i) stack) l + | SPlus => match stack with + |[]=>nil + |a :: al'=> match al' with + |[]=>nil + |b :: bl'=>s_execute st (cons (a+b) bl') l + end + end + | SMinus => match stack with + |[]=>nil + |a :: al'=> match al' with + |[]=>nil + |b :: bl'=>s_execute st (cons (b-a) bl') l + end + end + | SMult => match stack with + |[]=>nil + |a :: al'=> match al' with + |[]=>nil + |b :: bl'=>s_execute st (cons (a*b) bl') l + end + end + end +end. + +Example s_execute1 : + s_execute empty_state [] [SPush 5, SPush 3, SPush 1, SMinus] = [2, 5]. +Proof. reflexivity. Qed. + +Example s_execute2: + s_execute (update empty_state X 3) [3,4] [SPush 4, SLoad X, SMult, SPlus ] + = [15, 4]. +Proof. reflexivity. Qed. + +Fixpoint s_compile (e : aexp) : list sinstr := + match e with + | ANum v => [SPush v] + | AId i => [SLoad i] + | APlus a1 a2 => (s_compile a1) ++ (s_compile a2) ++ [SPlus] + | AMinus a1 a2 => (s_compile a1) ++ (s_compile a2) ++ [SMinus] + | AMult a1 a2 => (s_compile a1) ++ (s_compile a2) ++ [SMult] + end. + +Example s_compile1 : + s_compile (AMinus (AId X) (AMult (ANum 2) (AId Y))) = + [SLoad X, SPush 2, SLoad Y, SMult, SMinus]. +Proof. reflexivity. Qed. + +Theorem execute_theorem : forall (e : aexp) (st : state) (s1 : list nat) (other : list sinstr), + s_execute st s1 (s_compile e ++ other) = + s_execute st ((aeval st e) :: s1) other. +Proof. +induction e; try reflexivity. +simpl in |- *. +intros st s1 other. +assert +((s_compile e1 ++ s_compile e2 ++ [SPlus]) ++ other = + s_compile e1 ++ s_compile e2 ++ [SPlus] ++ other). +rewrite -> app_ass. +rewrite -> app_ass. +reflexivity. + +rewrite H in |- *. +assert +(s_execute st s1 (s_compile e1 ++ s_compile e2 ++ SPlus :: other) = + s_execute st (aeval st e1 :: s1) (s_compile e2 ++ SPlus :: other)). +apply IHe1. + +simpl in |- *. +rewrite H0 in |- *. +assert +(s_execute st (aeval st e1 :: s1) (s_compile e2 ++ SPlus :: other) = + s_execute st (aeval st e2 :: aeval st e1 :: s1) (SPlus :: other)). +apply IHe2. + +rewrite H1 in |- *. +simpl in |- *. +rewrite plus_comm in |- *. +reflexivity. + +intros st s1 other. +assert +(s_execute st s1 (s_compile e1 ++ s_compile e2 ++ SMinus :: other) = + s_execute st (aeval st e1 :: s1) (s_compile e2 ++ SMinus :: other)). +apply IHe1. + +simpl in |- *. +assert +((s_compile e1 ++ s_compile e2 ++ [SMinus]) ++ other = + s_compile e1 ++ s_compile e2 ++ [SMinus] ++ other). +rewrite -> app_ass. +rewrite -> app_ass. +reflexivity. + +simpl in |- *. +rewrite H0 in |- *. +simpl in |- *. +rewrite H in |- *. +assert +(s_execute st (aeval st e1 :: s1) (s_compile e2 ++ SMinus :: other) = + s_execute st (aeval st e2 :: aeval st e1 :: s1) (SMinus :: other)). +apply IHe2. + +rewrite H1 in |- *. +simpl in |- *. +reflexivity. + +intros st s1 other. +simpl in |- *. +simpl in |- *. +assert +((s_compile e1 ++ s_compile e2 ++ [SMult]) ++ other = + s_compile e1 ++ s_compile e2 ++ [SMult] ++ other). +rewrite -> app_ass. +rewrite -> app_ass. +reflexivity. + +rewrite H in |- *. +simpl in |- *. +assert +(s_execute st s1 (s_compile e1 ++ s_compile e2 ++ SMult :: other) = + s_execute st (aeval st e1 :: s1) (s_compile e2 ++ SMult :: other)). +apply IHe1. + +rewrite H0 in |- *. +assert +(s_execute st (aeval st e1 :: s1) (s_compile e2 ++ SMult :: other) = + s_execute st (aeval st e2 :: aeval st e1 :: s1) (SMult :: other)). +apply IHe2. + +rewrite H1 in |- *. +simpl in |- *. +rewrite mult_comm in |- *. +reflexivity. +Qed. + +Theorem s_compile_correct : forall (st : state) (e : aexp), + s_execute st [] (s_compile e) = [ aeval st e]. +Proof. +intros st e. +assert ([aeval st e] = s_execute st [aeval st e] []). +simpl in |- *. +reflexivity. + +rewrite H in |- *. +assert (s_compile e ++ [] = s_compile e). +simpl in |- *. +rewrite -> app_nil_end. +reflexivity. + +rewrite <- H0 in |- *. +apply execute_theorem. +Qed. + diff --git a/samples/coq/Lists.v b/samples/coq/Lists.v new file mode 100755 index 00000000..f09112ab --- /dev/null +++ b/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. diff --git a/samples/coq/PermutSetoid.v b/samples/coq/PermutSetoid.v new file mode 100755 index 00000000..aed7150c --- /dev/null +++ b/samples/coq/PermutSetoid.v @@ -0,0 +1,547 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 *) diff --git a/samples/coq/Permutation.v b/samples/coq/Permutation.v new file mode 100755 index 00000000..eb769b77 --- /dev/null +++ b/samples/coq/Permutation.v @@ -0,0 +1,644 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 *) diff --git a/samples/coq/Poly.v b/samples/coq/Poly.v new file mode 100755 index 00000000..63968cf3 --- /dev/null +++ b/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. + diff --git a/samples/coq/Rel.v b/samples/coq/Rel.v new file mode 100755 index 00000000..9449cbff --- /dev/null +++ b/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. diff --git a/samples/coq/Smallstep.v b/samples/coq/Smallstep.v new file mode 100755 index 00000000..b59bdd42 --- /dev/null +++ b/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. +*) diff --git a/samples/coq/Sorting.v b/samples/coq/Sorting.v new file mode 100755 index 00000000..22e56592 --- /dev/null +++ b/samples/coq/Sorting.v @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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. \ No newline at end of file diff --git a/samples/verilog/button_debounce.v b/samples/verilog/button_debounce.v new file mode 100755 index 00000000..7803828b --- /dev/null +++ b/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 . +//////////////////////////////////////////////////////////////////////////////// +`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 diff --git a/samples/verilog/control.v b/samples/verilog/control.v new file mode 100755 index 00000000..1dd5ca9c --- /dev/null +++ b/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 . +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 diff --git a/samples/verilog/hex_display.v b/samples/verilog/hex_display.v new file mode 100755 index 00000000..49331a9c --- /dev/null +++ b/samples/verilog/hex_display.v @@ -0,0 +1,54 @@ +/* + * Copyright (c) 2009 Zeus Gomez Marmolejo + * + * 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 + * . + */ + +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 diff --git a/samples/verilog/mux.v b/samples/verilog/mux.v new file mode 100755 index 00000000..1e9ce53a --- /dev/null +++ b/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 . +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 diff --git a/samples/verilog/pipeline_registers.v b/samples/verilog/pipeline_registers.v new file mode 100755 index 00000000..72970d16 --- /dev/null +++ b/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 . +//////////////////////////////////////////////////////////////////////////////// +`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 diff --git a/samples/verilog/ps2_mouse.v b/samples/verilog/ps2_mouse.v new file mode 100755 index 00000000..17c83a0d --- /dev/null +++ b/samples/verilog/ps2_mouse.v @@ -0,0 +1,175 @@ +/* + * PS2 Mouse Interface + * Copyright (C) 2010 Donna Polehn + * + * 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 + * . + */ + +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 + diff --git a/samples/verilog/sign_extender.v b/samples/verilog/sign_extender.v new file mode 100755 index 00000000..21944ccb --- /dev/null +++ b/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 . +//////////////////////////////////////////////////////////////////////////////// +`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 diff --git a/samples/verilog/sqrt_pipelined.v b/samples/verilog/sqrt_pipelined.v new file mode 100755 index 00000000..9ceff573 --- /dev/null +++ b/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 . +//////////////////////////////////////////////////////////////////////////////// +`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 diff --git a/samples/verilog/t_button_debounce.v b/samples/verilog/t_button_debounce.v new file mode 100755 index 00000000..0dfc0c04 --- /dev/null +++ b/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 . +//////////////////////////////////////////////////////////////////////////////// +`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 diff --git a/samples/verilog/t_div_pipelined.v b/samples/verilog/t_div_pipelined.v new file mode 100755 index 00000000..e4aa301e --- /dev/null +++ b/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 . +//////////////////////////////////////////////////////////////////////////////// +`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 + \ No newline at end of file diff --git a/samples/verilog/t_sqrt_pipelined.v b/samples/verilog/t_sqrt_pipelined.v new file mode 100755 index 00000000..c6652234 --- /dev/null +++ b/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 . +//////////////////////////////////////////////////////////////////////////////// +`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 + diff --git a/samples/verilog/vga.v b/samples/verilog/vga.v new file mode 100755 index 00000000..81298a98 --- /dev/null +++ b/samples/verilog/vga.v @@ -0,0 +1,313 @@ +/* + * VGA top level file + * Copyright (C) 2010 Zeus Gomez Marmolejo + * + * 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 + * . + */ + +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