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 bb08b8038bf51c37d533a0889c2493fd04fdc810..5afc3e5dc29d7db0f45e812d244f6cd72e4ff7f6 100644 (file)
--- 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 (file)
index 0000000..fcc29e8
--- /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 a931d692ec093840d13a9e145b3d69cb8be4a862..d730d06de6a60386a43b28c2132dbcdcb0b2568a 100644 (file)
--- 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: