CoRN (new version) has been committed by Andrea in library/algebra/CoRN.

[helm.git] / helm / software / matita / library / technicalities / setoids.ma

diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma
index c440795ffc2a099ee041fbe8039bc5f20bf478f3..cde3485c895a85d648dce985b7cf72c7921ccccc 100644 (file)
--- a/helm/software/matita/library/technicalities/setoids.ma
+++ b/helm/software/matita/library/technicalities/setoids.ma
@@ -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;
@@ -228,7 +228,7 @@ definition equality_morphism_of_symmetric_areflexive_transitive_relation:
     unfold transitive in H;
     unfold symmetric in sym;
     intro;
-    auto
+    auto new
   ].
 qed.
 
@@ -246,37 +246,51 @@ definition equality_morphism_of_symmetric_reflexive_transitive_relation:
     intro;
     unfold transitive in H;
     unfold symmetric in sym;
-    auto.
+    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 :
@@ -284,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).
@@ -668,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 *)
@@ -717,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