X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ftechnicalities%2Fsetoids.ma;h=fd1fb0037a1cff7c0525e3f88ed185df9b5eba08;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=4374ab113d3037c91161d5420bcbf99f8a844a8d;hpb=afcc82e79c1ebddaaed0fe9e83cfcea79493701c;p=helm.git diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma index 4374ab113..fd1fb0037 100644 --- a/helm/software/matita/library/technicalities/setoids.ma +++ b/helm/software/matita/library/technicalities/setoids.ma @@ -15,9 +15,8 @@ (* Code ported from the Coq theorem prover by Claudio Sacerdoti Coen *) (* Original author: Claudio Sacerdoti Coen. for the Coq system *) -set "baseuri" "cic:/matita/technicalities/setoids". - include "datatypes/constructors.ma". +include "logic/coimplication.ma". include "logic/connectives2.ma". (* DEFINITIONS OF Relation_Class AND n-ARY Morphism_Theory *) @@ -51,59 +50,30 @@ inductive Areflexive_Relation_Class : Type := | AAsymmetric : ∀A.∀Aeq : relation A. Areflexive_Relation_Class. definition relation_class_of_argument_class : Argument_Class → Relation_Class. - intro; - unfold in a ⊢ %; - elim a; + intros (a); cases a; [ apply (SymmetricReflexive ? ? ? H H1) | apply (AsymmetricReflexive ? something ? ? H) | apply (SymmetricAreflexive ? ? ? H) | apply (AsymmetricAreflexive ? something ? r) - | apply (Leibniz ? T1) + | apply (Leibniz ? T) ] qed. definition carrier_of_relation_class : ∀X. X_Relation_Class X → Type. - intros; - elim x; - [1,2,3,4,5: exact T1] + 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; - elim R 0; - simplify; - [1,2: intros 4; apply r - |3,4: intros 3; apply r - | intros 1 (T1); apply (eq T1). - (* this eta expansion is needed to avoid a universe inconsistency *) - ] -qed. - -definition relation_of_relation_classCOQ: - ∀X,R. carrier_of_relation_class X R → carrier_of_relation_class X R → Prop. - intros 2; - exact ( - match - R - return - (λ x.carrier_of_relation_class X x -> carrier_of_relation_class X x -> Prop) -with [ - SymmetricReflexive A Aeq _ _ => Aeq -| AsymmetricReflexive _ A Aeq _ => Aeq -| SymmetricAreflexive A Aeq _ => Aeq -| AsymmetricAreflexive _ A Aeq => Aeq -| Leibniz T => 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; - elim R; - reflexivity. - qed. +intro; cases R; reflexivity. +qed. inductive nelistT (A : Type) : Type := singl : A → nelistT A @@ -113,11 +83,10 @@ definition Arguments := nelistT Argument_Class. definition function_type_of_morphism_signature : Arguments → Relation_Class → Type. - intros (In Out); - elim In - [ exact (carrier_of_relation_class ? t → carrier_of_relation_class ? Out) - | exact (carrier_of_relation_class ? t → T) - ] + intros (In Out); elim In; + [ exact (carrier_of_relation_class ? a → carrier_of_relation_class ? Out) + | exact (carrier_of_relation_class ? a → T) + ] qed. definition make_compatibility_goal_aux: @@ -128,31 +97,26 @@ definition make_compatibility_goal_aux: generalize in match f; clear f; [ elim a; simplify in f f1; [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2)) - | elim t; + | cases x; [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2)) | exact (∀x1,x2. r x2 x1 → relation_of_relation_class ? Out (f x1) (f1 x2)) ] | exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2)) - | elim t; + | cases x; [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2)) | exact (∀x1,x2. r x2 x1 → relation_of_relation_class ? Out (f x1) (f1 x2)) ] | exact (∀x. relation_of_relation_class ? Out (f x) (f1 x)) ] | change with - ((carrier_of_relation_class ? t → function_type_of_morphism_signature n Out) → - (carrier_of_relation_class ? t → function_type_of_morphism_signature n Out) → + ((carrier_of_relation_class ? a → function_type_of_morphism_signature n Out) → + (carrier_of_relation_class ? a → function_type_of_morphism_signature n Out) → Prop). - elim t; simplify in f f1; - [ exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2)) - | elim t1; - [ exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2)) - | exact (∀x1,x2. r x2 x1 → R (f x1) (f1 x2)) - ] - | exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2)) - | elim t1; - [ exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2)) - | exact (∀x1,x2. r x2 x1 → R (f x1) (f1 x2)) + elim a; simplify in f f1; + [1,3: exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2)) + |2,4: cases x; + [1,3: exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2)) + |2,4: exact (∀x1,x2. r x2 x1 → R (f x1) (f1 x2)) ] | exact (∀x. R (f x) (f1 x)) ] @@ -170,8 +134,8 @@ record Morphism_Theory (In: Arguments) (Out: Relation_Class) : Type := definition list_of_Leibniz_of_list_of_types: nelistT Type → Arguments. intro; elim n; - [ apply (singl ? (Leibniz ? t)) - | apply (cons ? (Leibniz ? t) a) + [ apply (singl ? (Leibniz ? a)) + | apply (cons ? (Leibniz ? a) a1) ] qed. @@ -184,14 +148,12 @@ 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; - simplify; - intros; - whd; + whd; intros; reflexivity | simplify; intro; @@ -239,13 +201,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. @@ -256,14 +234,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. @@ -276,11 +273,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. @@ -293,11 +296,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. @@ -321,9 +330,8 @@ definition morphism_theory_of_predicate : | generalize in match f; clear f; unfold In'; clear In'; elim In; - [ reduce; + [ normalize; intro; - alias id "iff_refl" = "cic:/matita/logic/coimplication/iff_refl.con". apply iff_refl | simplify; intro x; @@ -338,7 +346,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 @@ -356,9 +365,9 @@ definition variance_of_argument_class : Argument_Class → option variance. intros; elim a; [ apply None - | apply (Some ? t) + | apply (Some ? x) | apply None - | apply (Some ? t) + | apply (Some ? x) | apply None ] qed. @@ -558,14 +567,14 @@ in F0. definition product_of_arguments : Arguments → Type. intro; elim a; - [ apply (carrier_of_relation_class ? t) - | apply (Prod (carrier_of_relation_class ? t) T) + [ apply (carrier_of_relation_class ? a1) + | apply (Prod (carrier_of_relation_class ? a1) T) ] 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 *) @@ -600,16 +609,16 @@ definition relation_of_product_of_arguments: elim In 0; [ simplify; intro; - exact (directed_relation_of_argument_class (get_rewrite_direction r t) t) + exact (directed_relation_of_argument_class (get_rewrite_direction r a) a) | 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; + change in p with (Prod (carrier_of_relation_class variance a) (product_of_arguments n)); + change in p1 with (Prod (carrier_of_relation_class variance a) (product_of_arguments n)); + 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 a) a c c1) + | exact (R p2 p3) ] ] qed. @@ -620,10 +629,10 @@ definition apply_morphism: intro; elim In; [ exact (f p) - | change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n)); + | change in p with (Prod (carrier_of_relation_class variance a) (product_of_arguments n)); elim p; - change in f1 with (carrier_of_relation_class variance t → function_type_of_morphism_signature n Out); - exact (f ? (f1 t1) t2) + change in f1 with (carrier_of_relation_class variance a → function_type_of_morphism_signature n Out); + exact (f ? (f1 a1) b) ] qed. @@ -640,33 +649,28 @@ theorem apply_morphism_compatibility_Right2Left: [ simplify in m1 m2 args1 args2 ⊢ %; change in H1 with (directed_relation_of_argument_class - (get_rewrite_direction Right2Left t) t args1 args2); + (get_rewrite_direction Right2Left a) a args1 args2); generalize in match H1; clear H1; generalize in match H; clear H; generalize in match args2; clear args2; generalize in match args1; clear args1; generalize in match m2; clear m2; generalize in match m1; clear m1; - elim t 0; + elim a 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; @@ -676,31 +680,32 @@ theorem apply_morphism_compatibility_Right2Left: exact H1 ] | change in m1 with - (carrier_of_relation_class variance t → + (carrier_of_relation_class variance a → function_type_of_morphism_signature n Out); change in m2 with - (carrier_of_relation_class variance t → + (carrier_of_relation_class variance a → function_type_of_morphism_signature n Out); change in args1 with - ((carrier_of_relation_class ? t) × (product_of_arguments n)); + ((carrier_of_relation_class ? a) × (product_of_arguments n)); change in args2 with - ((carrier_of_relation_class ? t) × (product_of_arguments n)); + ((carrier_of_relation_class ? a) × (product_of_arguments n)); 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 b b1); 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)); + (relation_of_relation_class unit Out (apply_morphism n Out (m1 a2) b1) + (apply_morphism n Out (m2 a1) b)); generalize in match H3; clear H3; - generalize in match t3; clear t3; - generalize in match t1; clear t1; + generalize in match a1; clear a1; + generalize in match a2; clear a2; generalize in match H1; clear H1; generalize in match m2; clear m2; generalize in match m1; clear m1; - elim t 0; + elim a 0; [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3); simplify in H3; change in H1 with @@ -761,23 +766,19 @@ 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); + (get_rewrite_direction Left2Right a) a args1 args2); generalize in match H1; clear H1; generalize in match H; clear H; generalize in match args2; clear args2; generalize in match args1; clear args1; generalize in match m2; clear m2; generalize in match m1; clear m1; - elim t 0; + elim a 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); @@ -802,33 +803,32 @@ theorem apply_morphism_compatibility_Left2Right: exact H1 ] | change in m1 with - (carrier_of_relation_class variance t → + (carrier_of_relation_class variance a → function_type_of_morphism_signature n Out); change in m2 with - (carrier_of_relation_class variance t → + (carrier_of_relation_class variance a → function_type_of_morphism_signature n Out); change in args1 with - ((carrier_of_relation_class ? t) × (product_of_arguments n)); + ((carrier_of_relation_class ? a) × (product_of_arguments n)); change in args2 with - ((carrier_of_relation_class ? t) × (product_of_arguments n)); + ((carrier_of_relation_class ? a) × (product_of_arguments n)); 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 b b1); 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)); + (relation_of_relation_class unit Out (apply_morphism n Out (m1 a1) b) + (apply_morphism n Out (m2 a2) b1)); generalize in match H3; clear H3; - generalize in match t3; clear t3; - generalize in match t1; clear t1; + generalize in match a2; clear a2; + generalize in match a1; clear a1; generalize in match H1; clear H1; generalize in match m2; clear m2; generalize in match m1; clear m1; - elim t 0; + elim a 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; @@ -897,7 +897,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 @@ -928,7 +928,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 @@ -1017,39 +1017,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. *)