X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ftechnicalities%2Fsetoids.ma;h=cde3485c895a85d648dce985b7cf72c7921ccccc;hb=54d09097e4ddbf7383d47ff0df4f1d9e14ea50fc;hp=a931d692ec093840d13a9e145b3d69cb8be4a862;hpb=4c2efa45d1b98541e7a68bb4ef676f5a9788a9eb;p=helm.git

diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma
index a931d692e..cde3485c8 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 *)
 
@@ -107,8 +107,8 @@ definition make_compatibility_goal_aux:
  ∀In,Out.∀f,g:function_type_of_morphism_signature In Out.Prop.
  intros 2; 
  elim In (a); simplify in f f1;
- generalize in match f; clear f;
  generalize in match f1; clear f1;
+ 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;
@@ -145,99 +145,152 @@ 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 new
+  ].
 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;
+    unfold symmetric in sym;
+    auto depth=4.
+  ]
 qed.
 
 definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
- ∀(A: Type)(Aeq: relation A)(trans: transitive ? Aeq).
-  let ASetoidClass1 := AsymmetricAreflexive Contravariant Aeq in
-  let ASetoidClass2 := AsymmetricAreflexive Covariant Aeq in
-   (Morphism_Theory (cons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
- intros.
- exists Aeq.
- unfold make_compatibility_goal; simpl; unfold impl; eauto.
+ ∀A: Type.∀Aeq: relation A.∀trans: transitive ? Aeq.
+  let ASetoidClass1 := AsymmetricAreflexive ? Contravariant ? Aeq in
+  let ASetoidClass2 := AsymmetricAreflexive ? Covariant ? Aeq in
+   (Morphism_Theory (cons ? ASetoidClass1 (singl ? ASetoidClass2)) Impl_Relation_Class).
+ intros;
+ apply mk_Morphism_Theory;
+ [ simplify;
+   apply Aeq
+ | simplify;
+   intros;
+   whd;
+   intros;
+   auto
+ ].
 qed.
 
 definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
- ∀(A: Type)(Aeq: relation A)(refl: reflexive ? Aeq)(trans: transitive ? Aeq).
-  let ASetoidClass1 := AsymmetricReflexive Contravariant refl in
-  let ASetoidClass2 := AsymmetricReflexive Covariant refl in
-   (Morphism_Theory (cons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
- intros.
- exists Aeq.
- unfold make_compatibility_goal; simpl; unfold impl; eauto.
+ ∀A: Type.∀Aeq: relation A.∀refl: reflexive ? Aeq.∀trans: transitive ? Aeq.
+  let ASetoidClass1 := AsymmetricReflexive ? Contravariant ? ? refl in
+  let ASetoidClass2 := AsymmetricReflexive ? Covariant ? ? refl in
+   (Morphism_Theory (cons ? ASetoidClass1 (singl ? ASetoidClass2)) Impl_Relation_Class).
+ intros;
+ apply mk_Morphism_Theory;
+ [ simplify;
+   apply Aeq
+ | simplify;
+   intros;
+   whd;
+   intro;
+   auto
+ ].
 qed.
 
 (* iff AS A RELATION *)
 
-Add Relation Prop iff
+(*DA PORTARE:Add Relation Prop iff
  reflexivity proved by iff_refl
  symmetry proved by iff_sym
  transitivity proved by iff_trans
- as iff_relation.
+ as iff_relation.*)
 
 (* every predicate is  morphism from Leibniz+ to Iff_Relation_Class *)
 definition morphism_theory_of_predicate :
@@ -245,33 +298,44 @@ definition morphism_theory_of_predicate :
   let In' := list_of_Leibniz_of_list_of_types In in
    function_type_of_morphism_signature In' Iff_Relation_Class →
     Morphism_Theory In' Iff_Relation_Class.
-  intros.
-  exists X.
-  induction In;  unfold make_compatibility_goal; simpl.
-    intro; apply iff_refl.
-    intro; apply (IHIn (X x)).
+  intros;
+  apply mk_Morphism_Theory;
+  [ apply f
+  | generalize in match f; clear f;
+    unfold In'; clear In';
+    elim In;
+     [ reduce;
+       intro;
+       alias id "iff_refl" = "cic:/matita/logic/coimplication/iff_refl.con".
+       apply iff_refl
+     | simplify;
+       intro x;
+       apply (H (f1 x))
+     ]
+  ].
 qed.
 
 (* impl AS A RELATION *)
 
-Theorem impl_trans: transitive ? impl.
- hnf; unfold impl; tauto.
-Qed.
+theorem impl_trans: transitive ? impl.
+ whd;
+ unfold impl;
+ intros;
+ auto.
+qed.
 
-Add Relation Prop impl
+(*DA PORTARE: Add Relation Prop impl
  reflexivity proved by impl_refl
  transitivity proved by impl_trans
- as impl_relation.
+ as impl_relation.*)
 
 (* THE CIC PART OF THE REFLEXIVE TACTIC (SETOID REWRITE) *)
 
 inductive rewrite_direction : Type :=
-   Left2Right
- | Right2Left.
+   Left2Right: rewrite_direction
+ | Right2Left: rewrite_direction.
 
-Implicit Type dir: rewrite_direction.
-
-definition variance_of_argument_class : Argument_Class → option variance.
+(*definition variance_of_argument_class : Argument_Class → option variance.
  destruct 1.
  exact None.
  exact (Some v).
@@ -629,15 +693,6 @@ Theorem setoid_rewrite:
      exact H1.
 Qed.
 
-(* BEGIN OF UTILITY/BACKWARD COMPATIBILITY PART *)
-
-record Setoid_Theory  (A: Type) (Aeq: relation A) : Prop := 
-  {Seq_refl : ∀x:A. Aeq x x;
-   Seq_sym : ∀x y:A. Aeq x y → Aeq y x;
-   Seq_trans : ∀x y z:A. Aeq x y → Aeq y z → Aeq x z}.
-
-(* END OF UTILITY/BACKWARD COMPATIBILITY PART *)
-
 (* A FEW EXAMPLES ON iff *)
 
 (* impl IS A MORPHISM *)
@@ -678,31 +733,4 @@ Add Morphism not with signature impl -→ impl as Not_Morphism2.
  unfold impl; tauto.
 Qed.
 
-(* FOR BACKWARD COMPATIBILITY *)
-Implicit Arguments Setoid_Theory [].
-Implicit Arguments Seq_refl [].
-Implicit Arguments Seq_sym [].
-Implicit Arguments Seq_trans [].
-
-
-(* Some tactics for manipulating Setoid Theory not officially 
-   declared as Setoid. *)
-
-Ltac trans_st x := match goal with 
-  | H : Setoid_Theory ? ?eqA |- ?eqA ? ? => 
-     apply (Seq_trans ? ? H) with x; auto
- end.
-
-Ltac sym_st := match goal with 
-  | H : Setoid_Theory ? ?eqA |- ?eqA ? ? => 
-     apply (Seq_sym ? ? H); auto
- end.
-
-Ltac refl_st := match goal with 
-  | H : Setoid_Theory ? ?eqA |- ?eqA ? ? => 
-     apply (Seq_refl ? ? H); auto
- end.
-
-definition gen_st : ∀A : Set. Setoid_Theory ? (@eq A).
-Proof. constructor; congruence. Qed.
-
+*)
\ No newline at end of file