From: Claudio Sacerdoti Coen Date: Wed, 27 Sep 2006 15:56:51 +0000 (+0000) Subject: More work on the translation of technicalities/setoids.ma. X-Git-Tag: make_still_working~6844 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c48de1fba2742df0d3ab42d69e758ae2859316d0;p=helm.git More work on the translation of technicalities/setoids.ma. --- diff --git a/helm/software/matita/library/logic/connectives.ma b/helm/software/matita/library/logic/connectives.ma index bb08b8038..5afc3e5dc 100644 --- a/helm/software/matita/library/logic/connectives.ma +++ b/helm/software/matita/library/logic/connectives.ma @@ -82,3 +82,5 @@ interpretation "exists" 'exists \eta.x = inductive ex2 (A:Type) (P,Q:A \to Prop) : Prop \def ex_intro2: \forall x:A. P x \to Q x \to ex2 A P Q. +definition iff := + \lambda A,B. (A -> B) \land (B -> A). \ No newline at end of file diff --git a/helm/software/matita/library/logic/connectives2.ma b/helm/software/matita/library/logic/connectives2.ma new file mode 100644 index 000000000..fcc29e81a --- /dev/null +++ b/helm/software/matita/library/logic/connectives2.ma @@ -0,0 +1,44 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/logic/connectives2". + +include "higher_order_defs/relations.ma". + +theorem reflexive_iff: reflexive ? iff. + unfold reflexive; + intro; + split; + intro; + assumption. +qed. + +theorem symmetric_iff: symmetric ? iff. + unfold symmetric; + intros; + elim H; + split; + assumption. +qed. + +theorem transitive_iff: transitive ? iff. + unfold transitive; + intros; + elim H; + elim H1; + split; + intro; + auto. +qed. + diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma index a931d692e..d730d06de 100644 --- a/helm/software/matita/library/technicalities/setoids.ma +++ b/helm/software/matita/library/technicalities/setoids.ma @@ -17,8 +17,8 @@ set "baseuri" "cic:/matita/technicalities/setoids". -include "higher_order_defs/relations.ma". include "datatypes/constructors.ma". +include "logic/connectives2.ma". (* DEFINITIONS OF Relation_Class AND n-ARY Morphism_Theory *) @@ -145,70 +145,108 @@ qed. definition make_compatibility_goal := λIn,Out,f. make_compatibility_goal_aux In Out f f. -record Morphism_Theory In Out : Type := +record Morphism_Theory (In: Arguments) (Out: Relation_Class) : Type := { Function : function_type_of_morphism_signature In Out; Compat : make_compatibility_goal In Out Function }. definition list_of_Leibniz_of_list_of_types: nelistT Type → Arguments. - induction 1. - exact (singl (Leibniz ? a)). - exact (cons (Leibniz ? a) IHX). + intro; + elim n; + [ apply (singl ? (Leibniz ? t)) + | apply (cons ? (Leibniz ? t) a) + ] qed. (* every function is a morphism from Leibniz+ to Leibniz *) definition morphism_theory_of_function : - ∀(In: nelistT Type) (Out: Type). + ∀In: nelistT Type.∀Out: Type. let In' := list_of_Leibniz_of_list_of_types In in let Out' := Leibniz ? Out in function_type_of_morphism_signature In' Out' → Morphism_Theory In' Out'. - intros. - exists X. - induction In; unfold make_compatibility_goal; simpl. - reflexivity. - intro; apply (IHIn (X x)). + intros; + apply (mk_Morphism_Theory ? ? f); + 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; + reflexivity + | simplify; + intro; + unfold In' in f; + unfold Out' in f; + exact (H (f1 x)) + ] qed. (* THE iff RELATION CLASS *) definition Iff_Relation_Class : Relation_Class. - eapply (@SymmetricReflexive unit ? iff). - exact iff_sym. - exact iff_refl. + apply (SymmetricReflexive unit ? iff); + [ exact symmetric_iff + | exact reflexive_iff + ] qed. (* THE impl RELATION CLASS *) -definition impl (A B: Prop) := A → B. +definition impl \def \lambda A,B:Prop. A → B. -Theorem impl_refl: reflexive ? impl. - hnf; unfold impl; tauto. -Qed. +theorem impl_refl: reflexive ? impl. + unfold reflexive; + intros; + unfold impl; + intro; + assumption. +qed. definition Impl_Relation_Class : Relation_Class. - eapply (@AsymmetricReflexive unit tt ? impl). + unfold Relation_Class; + apply (AsymmetricReflexive unit something ? impl); exact impl_refl. qed. (* UTILITY FUNCTIONS TO PROVE THAT EVERY TRANSITIVE RELATION IS A MORPHISM *) definition equality_morphism_of_symmetric_areflexive_transitive_relation: - ∀(A: Type)(Aeq: relation A)(sym: symmetric ? Aeq)(trans: transitive ? Aeq). - let ASetoidClass := SymmetricAreflexive ? sym in - (Morphism_Theory (cons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class). - intros. - exists Aeq. - unfold make_compatibility_goal; simpl; split; eauto. + ∀A: Type.∀Aeq: relation A.∀sym: symmetric ? Aeq.∀trans: transitive ? Aeq. + let ASetoidClass := SymmetricAreflexive ? ? ? sym in + (Morphism_Theory (cons ? ASetoidClass (singl ? ASetoidClass)) + Iff_Relation_Class). + intros; + apply mk_Morphism_Theory; + [ exact Aeq + | unfold make_compatibility_goal; + simplify; + intros; + split; + unfold transitive in H; + unfold symmetric in sym; + intro; + auto + ]. qed. definition equality_morphism_of_symmetric_reflexive_transitive_relation: - ∀(A: Type)(Aeq: relation A)(refl: reflexive ? Aeq)(sym: symmetric ? Aeq) - (trans: transitive ? Aeq). let ASetoidClass := SymmetricReflexive ? sym refl in - (Morphism_Theory (cons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class). - intros. - exists Aeq. - unfold make_compatibility_goal; simpl; split; eauto. + ∀A: Type.∀Aeq: relation A.∀refl: reflexive ? Aeq.∀sym: symmetric ? Aeq. + ∀trans: transitive ? Aeq. + let ASetoidClass := SymmetricReflexive ? ? ? sym refl in + (Morphism_Theory (cons ? ASetoidClass (singl ? ASetoidClass)) Iff_Relation_Class). + intros; + apply mk_Morphism_Theory; + reduce; + [ exact Aeq + | intros; + split; + intro; + unfold transitive in H; + auto + ] qed. definition equality_morphism_of_asymmetric_areflexive_transitive_relation: