summaryrefslogtreecommitdiff
path: root/test-suite/modules/Przyklad.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/modules/Przyklad.v')
-rw-r--r--test-suite/modules/Przyklad.v226
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.
-
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-09 21:47:19 +0000