X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Flibrary%2Ftechnicalities%2Fsetoids.ma;h=bb8aacac69d4d929ce27f00665348004b349f54e;hb=936f80cf031a7b034dd70fef49abb90e69f2e680;hp=e589a33d047e65a16aa02e5a47469ecd193fe022;hpb=37bbd741fbba797bc7c64318f13edce28131cd91;p=helm.git diff --git a/matita/library/technicalities/setoids.ma b/matita/library/technicalities/setoids.ma index e589a33d0..bb8aacac6 100644 --- a/matita/library/technicalities/setoids.ma +++ b/matita/library/technicalities/setoids.ma @@ -62,19 +62,19 @@ definition relation_class_of_argument_class : Argument_Class → Relation_Class. qed. definition carrier_of_relation_class : ∀X. X_Relation_Class X → Type. - intros (X x); cases x; clear x; [2,4:clear x1] clear X; assumption. + intros (X x); cases x (A o o o o A o o A o o o A o A); exact A. qed. definition relation_of_relation_class: ∀X,R. carrier_of_relation_class X R → carrier_of_relation_class X R → Prop. - intros 2; cases R; simplify; [1,2,3,4: assumption | apply (eq T) ] +intros 2; cases R; simplify; [1,2,3,4: assumption | apply (eq T) ] qed. lemma about_carrier_of_relation_class_and_relation_class_of_argument_class : ∀R. carrier_of_relation_class ? (relation_class_of_argument_class R) = carrier_of_relation_class ? R. - intro; cases R; reflexivity. +intro; cases R; reflexivity. qed. inductive nelistT (A : Type) : Type := @@ -155,9 +155,7 @@ definition morphism_theory_of_function : generalize in match f; clear f; elim In; [ unfold make_compatibility_goal; - simplify; - intros; - whd; + whd; intros; reflexivity | simplify; intro; @@ -211,7 +209,7 @@ definition equality_morphism_of_symmetric_areflexive_transitive_relation: unfold transitive in H; unfold symmetric in sym; intro; - auto new + autobatch new ]. qed. @@ -229,7 +227,7 @@ definition equality_morphism_of_symmetric_reflexive_transitive_relation: intro; unfold transitive in H; unfold symmetric in sym; - auto depth=4. + autobatch depth=4. ] qed. @@ -246,7 +244,7 @@ definition equality_morphism_of_asymmetric_areflexive_transitive_relation: intros; whd; intros; - auto + autobatch ]. qed. @@ -263,7 +261,7 @@ definition equality_morphism_of_asymmetric_reflexive_transitive_relation: intros; whd; intro; - auto + autobatch ]. qed. @@ -303,7 +301,7 @@ theorem impl_trans: transitive ? impl. whd; unfold impl; intros; - auto. + autobatch. qed. (*DA PORTARE: Add Relation Prop impl @@ -530,7 +528,7 @@ qed. definition get_rewrite_direction: rewrite_direction → Argument_Class → rewrite_direction. intros (dir R); - cases (variance_of_argument_class R); + cases (variance_of_argument_class R) (a); [ exact dir | cases a; [ exact dir (* covariant *) @@ -569,12 +567,12 @@ definition relation_of_product_of_arguments: | intros; change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n)); change in p1 with (Prod (carrier_of_relation_class variance t) (product_of_arguments n)); - cases p; - cases p1; + cases p (c p2); + cases p1 (c1 p3); apply And; [ exact - (directed_relation_of_argument_class (get_rewrite_direction r t) t a a1) - | exact (R b b1) + (directed_relation_of_argument_class (get_rewrite_direction r t) t c c1) + | exact (R p2 p3) ] ] qed. @@ -612,26 +610,21 @@ theorem apply_morphism_compatibility_Right2Left: generalize in match args1; clear args1; generalize in match m2; clear m2; generalize in match m1; clear m1; - elim t 0; + elim t 0; simplify; [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1); - simplify in H; - simplify in H1; - simplify; apply H; exact H1 | intros 8 (v T1 r Hr m1 m2 args1 args2); - cases v; + cases v; + simplify; intros (H H1); - simplify in H1; - apply H; - exact H1 + apply (H ? ? H1); | intros; apply H1; exact H2 | intros 7 (v); - cases v; + cases v; simplify; intros (H H1); - simplify in H1; apply H; exact H1 | intros; @@ -726,10 +719,9 @@ theorem apply_morphism_compatibility_Left2Right: directed_relation_of_relation_class Left2Right ? (apply_morphism ? ? m1 args1) (apply_morphism ? ? m2 args2). - intro; - elim In; - [ simplify in m1 m2 args1 args2 ⊢ %; - change in H1 with + intro; + elim In 0; simplify; intros; + [ change in H1 with (directed_relation_of_argument_class (get_rewrite_direction Left2Right t) t args1 args2); generalize in match H1; clear H1; @@ -738,11 +730,8 @@ theorem apply_morphism_compatibility_Left2Right: generalize in match args1; clear args1; generalize in match m2; clear m2; generalize in match m1; clear m1; - elim t 0; + elim t 0; simplify; [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1); - simplify in H; - simplify in H1; - simplify; apply H; exact H1 | intros 8 (v T1 r Hr m1 m2 args1 args2); @@ -793,7 +782,6 @@ theorem apply_morphism_compatibility_Left2Right: generalize in match m1; clear m1; elim t 0; [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3); - simplify in H3; change in H1 with (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2)); | intro v; @@ -982,39 +970,39 @@ Qed. (* impl IS A MORPHISM *) Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism. -unfold impl; tauto. +unfold impl; tautobatch. Qed. (* and IS A MORPHISM *) Add Morphism and with signature iff ==> iff ==> iff as And_Morphism. - tauto. + tautobatch. Qed. (* or IS A MORPHISM *) Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism. - tauto. + tautobatch. Qed. (* not IS A MORPHISM *) Add Morphism not with signature iff ==> iff as Not_Morphism. - tauto. + tautobatch. Qed. (* THE SAME EXAMPLES ON impl *) Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2. - unfold impl; tauto. + unfold impl; tautobatch. Qed. Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2. - unfold impl; tauto. + unfold impl; tautobatch. Qed. Add Morphism not with signature impl -→ impl as Not_Morphism2. - unfold impl; tauto. + unfold impl; tautobatch. Qed. *)