X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ftechnicalities%2Fsetoids.ma;h=4c51d3a448e15a900e8b28f2118cb480139614fd;hb=347b0f483245bd0295f95f99742e23484c331312;hp=362b9fb5b740abc924761aa1159b3ebbb12ad640;hpb=9fe4caa4ba466250017b5ac1b36fc6e94d7e3860;p=helm.git diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma index 362b9fb5b..4c51d3a44 100644 --- a/helm/software/matita/library/technicalities/setoids.ma +++ b/helm/software/matita/library/technicalities/setoids.ma @@ -18,8 +18,8 @@ set "baseuri" "cic:/matita/technicalities/setoids". include "datatypes/constructors.ma". -include "logic/connectives2.ma". include "logic/coimplication.ma". +include "logic/connectives2.ma". (* DEFINITIONS OF Relation_Class AND n-ARY Morphism_Theory *) @@ -150,8 +150,8 @@ definition morphism_theory_of_function : Morphism_Theory In' Out'. intros; apply (mk_Morphism_Theory ? ? f); - unfold In' in f; clear In'; - unfold Out' in f; clear Out'; + unfold In' in f ⊢ %; clear In'; + unfold Out' in f ⊢ %; clear Out'; generalize in match f; clear f; elim In; [ unfold make_compatibility_goal; @@ -203,13 +203,29 @@ definition equality_morphism_of_symmetric_areflexive_transitive_relation: apply mk_Morphism_Theory; [ exact Aeq | unfold make_compatibility_goal; - simplify; + simplify; unfold ASetoidClass; simplify; intros; split; unfold transitive in H; unfold symmetric in sym; intro; - auto new + [ apply (H x2 x1 x3 ? ?); + [apply (sym x1 x2 ?). + apply (H1). + |apply (H x1 x x3 ? ?); + [apply (H3). + |apply (H2). + ] + ] + | apply (H x1 x3 x ? ?); + [apply (H x1 x2 x3 ? ?); + [apply (H1). + |apply (H3). + ] + |apply (sym x x3 ?). + apply (H2). + ] + ] ]. qed. @@ -220,14 +236,33 @@ definition equality_morphism_of_symmetric_reflexive_transitive_relation: (Morphism_Theory (cons ? ASetoidClass (singl ? ASetoidClass)) Iff_Relation_Class). intros; apply mk_Morphism_Theory; - reduce; + normalize; [ exact Aeq | intros; split; intro; unfold transitive in H; unfold symmetric in sym; - auto depth=4. + [ apply (H x2 x1 x3 ? ?); + [apply (sym x1 x2 ?). + apply (H1). + |apply (H x1 x x3 ? ?); + [apply (H3). + |apply (H2). + ] + ] + | apply (H x1 x2 x ? ?); + [apply (H1). + |apply (H x2 x3 x ? ?); + [apply (H3). + |apply (sym x x3 ?). + apply (H x x3 x3 ? ?); + [apply (H2). + |apply (refl x3). + ] + ] + ] + ] ] qed. @@ -240,11 +275,17 @@ definition equality_morphism_of_asymmetric_areflexive_transitive_relation: apply mk_Morphism_Theory; [ simplify; apply Aeq - | simplify; + | simplify; unfold ASetoidClass1; simplify; unfold ASetoidClass2; simplify; intros; whd; intros; - auto + apply (H x2 x1 x3 ? ?); + [apply (H1). + |apply (H x1 x x3 ? ?); + [apply (H3). + |apply (H2). + ] + ] ]. qed. @@ -257,11 +298,17 @@ definition equality_morphism_of_asymmetric_reflexive_transitive_relation: apply mk_Morphism_Theory; [ simplify; apply Aeq - | simplify; + | simplify; unfold ASetoidClass1; simplify; unfold ASetoidClass2; simplify; intros; whd; intro; - auto + apply (H x2 x1 x3 ? ?); + [apply (H1). + |apply (H x1 x x3 ? ?); + [apply (H3). + |apply (H2). + ] + ] ]. qed. @@ -285,7 +332,7 @@ definition morphism_theory_of_predicate : | generalize in match f; clear f; unfold In'; clear In'; elim In; - [ reduce; + [ normalize; intro; apply iff_refl | simplify; @@ -301,7 +348,8 @@ theorem impl_trans: transitive ? impl. whd; unfold impl; intros; - auto. + apply (H1 ?).apply (H ?).apply (H2). + autobatch. qed. (*DA PORTARE: Add Relation Prop impl @@ -646,9 +694,10 @@ theorem apply_morphism_compatibility_Right2Left: generalize in match H2; clear H2; elim args2 0; clear args2; elim args1; clear args1; + simplify in H2; + change in H2:(? ? %) with + (relation_of_product_of_arguments Right2Left n t2 t4); elim H2; clear H2; - change in H4 with - (relation_of_product_of_arguments Right2Left n t2 t4); change with (relation_of_relation_class unit Out (apply_morphism n Out (m1 t3) t4) (apply_morphism n Out (m2 t1) t2)); @@ -768,9 +817,9 @@ theorem apply_morphism_compatibility_Left2Right: generalize in match H2; clear H2; elim args2 0; clear args2; elim args1; clear args1; + simplify in H2; change in H2:(? ? %) with + (relation_of_product_of_arguments Left2Right n t2 t4); elim H2; clear H2; - change in H4 with - (relation_of_product_of_arguments Left2Right n t2 t4); change with (relation_of_relation_class unit Out (apply_morphism n Out (m1 t1) t2) (apply_morphism n Out (m2 t3) t4)); @@ -850,7 +899,7 @@ definition interp : rewrite < (about_carrier_of_relation_class_and_relation_class_of_argument_class S); exact c1 - | split; + | simplify;split; [ rewrite < (about_carrier_of_relation_class_and_relation_class_of_argument_class S); exact c1 @@ -881,7 +930,7 @@ definition interp_relation_class_list : rewrite < (about_carrier_of_relation_class_and_relation_class_of_argument_class S); exact c1 - | split; + | simplify; split; [ rewrite < (about_carrier_of_relation_class_and_relation_class_of_argument_class S); exact c1 @@ -970,39 +1019,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. *)