diff options
Diffstat (limited to 'test-suite/modules/Przyklad.v')
-rw-r--r-- | test-suite/modules/Przyklad.v | 226 |
1 files changed, 110 insertions, 116 deletions
diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v index 4f4c2066..014f6c60 100644 --- a/test-suite/modules/Przyklad.v +++ b/test-suite/modules/Przyklad.v @@ -1,38 +1,40 @@ -Definition ifte := [T:Set][A:Prop][B:Prop][s:(sumbool A B)][th:T][el:T] - if s then [_]th else [_]el. +Definition ifte (T : Set) (A B : Prop) (s : {A} + {B}) + (th el : T) := if s then th else el. -Implicits ifte. +Implicit Arguments ifte. -Lemma Reflexivity_provable : - (A:Set)(a:A)(s:{a=a}+{~a=a})(EXT x| s==(left ? ? x)). -Intros. -Elim s. -Intro x. -Split with x; Reflexivity. +Lemma Reflexivity_provable : + forall (A : Set) (a : A) (s : {a = a} + {a <> a}), + exists x : _, s = left _ x. +intros. +elim s. +intro x. +split with x; reflexivity. -Intro. -Absurd a=a; Auto. +intro. + absurd (a = a); auto. -Save. +Qed. -Lemma Disequality_provable : - (A:Set)(a,b:A)(~a=b)->(s:{a=b}+{~a=b})(EXT x| s==(right ? ? x)). -Intros. -Elim s. -Intro. -Absurd a=a; Auto. +Lemma Disequality_provable : + forall (A : Set) (a b : A), + a <> b -> forall s : {a = b} + {a <> b}, exists x : _, s = right _ x. +intros. +elim s. +intro. + absurd (a = a); auto. -Intro. -Split with b0; Reflexivity. +intro. +split with b0; reflexivity. -Save. +Qed. Module Type ELEM. Parameter T : Set. - Parameter eq_dec : (a,a':T){a=a'}+{~ a=a'}. + Parameter eq_dec : forall a a' : T, {a = a'} + {a <> a'}. End ELEM. -Module Type SET[Elt : ELEM]. +Module Type SET (Elt: ELEM). Parameter T : Set. Parameter empty : T. Parameter add : Elt.T -> T -> T. @@ -40,56 +42,52 @@ Module Type SET[Elt : ELEM]. (* Axioms *) - Axiom find_empty_false : - (e:Elt.T) (find e empty) = false. + Axiom find_empty_false : forall e : Elt.T, find e empty = false. - Axiom find_add_true : - (s:T) (e:Elt.T) (find e (add e s)) = true. + Axiom find_add_true : forall (s : T) (e : Elt.T), find e (add e s) = true. - Axiom find_add_false : - (s:T) (e:Elt.T) (e':Elt.T) ~(e=e') -> - (find e (add e' s))=(find e s). + Axiom + find_add_false : + forall (s : T) (e e' : Elt.T), e <> e' -> find e (add e' s) = find e s. End SET. -Module FuncDict[E : ELEM]. +Module FuncDict (E: ELEM). Definition T := E.T -> bool. - Definition empty := [e':E.T] false. - Definition find := [e':E.T] [s:T] (s e'). - Definition add := [e:E.T][s:T][e':E.T] - (ifte (E.eq_dec e e') true (find e' s)). + Definition empty (e' : E.T) := false. + Definition find (e' : E.T) (s : T) := s e'. + Definition add (e : E.T) (s : T) (e' : E.T) := + ifte (E.eq_dec e e') true (find e' s). - Lemma find_empty_false : (e:E.T) (find e empty) = false. - Auto. + Lemma find_empty_false : forall e : E.T, find e empty = false. + auto. Qed. - Lemma find_add_true : - (s:T) (e:E.T) (find e (add e s)) = true. + Lemma find_add_true : forall (s : T) (e : E.T), find e (add e s) = true. - Intros. - Unfold find add. - Elim (Reflexivity_provable ? ? (E.eq_dec e e)). - Intros. - Rewrite H. - Auto. + intros. + unfold find, add in |- *. + elim (Reflexivity_provable _ _ (E.eq_dec e e)). + intros. + rewrite H. + auto. Qed. Lemma find_add_false : - (s:T) (e:E.T) (e':E.T) ~(e=e') -> - (find e (add e' s))=(find e s). - Intros. - Unfold add find. - Cut (EXT x:? | (E.eq_dec e' e)==(right ? ? x)). - Intros. - Elim H0. - Intros. - Rewrite H1. - Unfold ifte. - Reflexivity. - - Apply Disequality_provable. - Auto. + forall (s : T) (e e' : E.T), e <> e' -> find e (add e' s) = find e s. + intros. + unfold add, find in |- *. + cut (exists x : _, E.eq_dec e' e = right _ x). + intros. + elim H0. + intros. + rewrite H1. + unfold ifte in |- *. + reflexivity. + + apply Disequality_provable. + auto. Qed. @@ -99,84 +97,81 @@ Module F : SET := FuncDict. Module Nat. - Definition T:=nat. - Lemma eq_dec : (a,a':T){a=a'}+{~ a=a'}. - Decide Equality. + Definition T := nat. + Lemma eq_dec : forall a a' : T, {a = a'} + {a <> a'}. + decide equality. Qed. End Nat. -Module SetNat:=F Nat. +Module SetNat := F Nat. -Lemma no_zero_in_empty:(SetNat.find O SetNat.empty)=false. -Apply SetNat.find_empty_false. -Save. +Lemma no_zero_in_empty : SetNat.find 0 SetNat.empty = false. +apply SetNat.find_empty_false. +Qed. (***************************************************************************) -Module Lemmas[G:SET][E:ELEM]. +Module Lemmas (G: SET) (E: ELEM). - Module ESet:=G E. + Module ESet := G E. - Lemma commute : (S:ESet.T)(a1,a2:E.T) - let S1 = (ESet.add a1 (ESet.add a2 S)) in - let S2 = (ESet.add a2 (ESet.add a1 S)) in - (a:E.T)(ESet.find a S1)=(ESet.find a S2). + Lemma commute : + forall (S : ESet.T) (a1 a2 : E.T), + let S1 := ESet.add a1 (ESet.add a2 S) in + let S2 := ESet.add a2 (ESet.add a1 S) in + forall a : E.T, ESet.find a S1 = ESet.find a S2. - Intros. - Unfold S1 S2. - Elim (E.eq_dec a a1); Elim (E.eq_dec a a2); Intros H1 H2; - Try Rewrite <- H1; Try Rewrite <- H2; - Repeat - (Try (Rewrite ESet.find_add_true; Auto); - Try (Rewrite ESet.find_add_false; Auto); - Auto). - Save. + intros. + unfold S1, S2 in |- *. + elim (E.eq_dec a a1); elim (E.eq_dec a a2); intros H1 H2; + try rewrite <- H1; try rewrite <- H2; + repeat + (try ( rewrite ESet.find_add_true; auto); + try ( rewrite ESet.find_add_false; auto); auto). + Qed. End Lemmas. -Inductive list [A:Set] : Set := nil : (list A) - | cons : A -> (list A) -> (list A). +Inductive list (A : Set) : Set := + | nil : list A + | cons : A -> list A -> list A. -Module ListDict[E : ELEM]. - Definition T := (list E.T). +Module ListDict (E: ELEM). + Definition T := list E.T. Definition elt := E.T. - Definition empty := (nil elt). - Definition add := [e:elt][s:T] (cons elt e s). - Fixpoint find [e:elt; s:T] : bool := - Cases s of - nil => false - | (cons e' s') => (ifte (E.eq_dec e e') - true - (find e s')) - end. - - Definition find_empty_false := [e:elt] (refl_equal bool false). - - Lemma find_add_true : - (s:T) (e:E.T) (find e (add e s)) = true. - Intros. - Simpl. - Elim (Reflexivity_provable ? ? (E.eq_dec e e)). - Intros. - Rewrite H. - Auto. + Definition empty := nil elt. + Definition add (e : elt) (s : T) := cons elt e s. + Fixpoint find (e : elt) (s : T) {struct s} : bool := + match s with + | nil => false + | cons e' s' => ifte (E.eq_dec e e') true (find e s') + end. + + Definition find_empty_false (e : elt) := refl_equal false. + + Lemma find_add_true : forall (s : T) (e : E.T), find e (add e s) = true. + intros. + simpl in |- *. + elim (Reflexivity_provable _ _ (E.eq_dec e e)). + intros. + rewrite H. + auto. Qed. Lemma find_add_false : - (s:T) (e:E.T) (e':E.T) ~(e=e') -> - (find e (add e' s))=(find e s). - Intros. - Simpl. - Elim (Disequality_provable ? ? ? H (E.eq_dec e e')). - Intros. - Rewrite H0. - Simpl. - Reflexivity. - Save. + forall (s : T) (e e' : E.T), e <> e' -> find e (add e' s) = find e s. + intros. + simpl in |- *. + elim (Disequality_provable _ _ _ H (E.eq_dec e e')). + intros. + rewrite H0. + simpl in |- *. + reflexivity. + Qed. End ListDict. @@ -190,4 +185,3 @@ Module L : SET := ListDict. - |