X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ftechnicalities%2Fsetoids.ma;h=35f3b0920cba32c03d5887e149a592bda7207999;hb=76ccef4bc06a1cc4634c9261d65e2462a016ecde;hp=e589a33d047e65a16aa02e5a47469ecd193fe022;hpb=ccd879c23e341fe287f8fd1078c4cef459cf24f5;p=helm.git

diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma
index e589a33d0..35f3b0920 100644
--- a/helm/software/matita/library/technicalities/setoids.ma
+++ b/helm/software/matita/library/technicalities/setoids.ma
@@ -18,8 +18,8 @@
 set "baseuri" "cic:/matita/technicalities/setoids".
 
 include "datatypes/constructors.ma".
-include "logic/connectives2.ma".
 include "logic/coimplication.ma".
+include "logic/connectives2.ma".
 
 (* DEFINITIONS OF Relation_Class AND n-ARY Morphism_Theory *)
 
@@ -62,19 +62,19 @@ definition relation_class_of_argument_class : Argument_Class → Relation_Class.
 qed.
 
 definition carrier_of_relation_class : ∀X. X_Relation_Class X → Type.
- intros (X x); cases x; clear x; [2,4:clear x1] clear X; assumption.
+ 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; cases R; simplify; [1,2,3,4: assumption | apply (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; cases R; reflexivity.
+intro; cases R; reflexivity.
 qed.
 
 inductive nelistT (A : Type) : Type :=
@@ -86,8 +86,8 @@ 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)
+  [ exact (carrier_of_relation_class ? a → carrier_of_relation_class ? Out)
+  | exact (carrier_of_relation_class ? a → T)
   ]
 qed. 
 
@@ -99,24 +99,24 @@ 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))
-     | cases 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))
-     | cases 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;
+    elim a; simplify in f f1;
      [1,3: exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
-     |2,4: cases t1;
+     |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))
         ]
@@ -136,8 +136,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.
 
@@ -150,14 +150,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;
@@ -205,13 +203,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.
 
@@ -222,14 +236,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.
 
@@ -242,11 +275,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.
 
@@ -259,11 +298,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.
 
@@ -287,7 +332,7 @@ definition morphism_theory_of_predicate :
   | generalize in match f; clear f;
     unfold In'; clear In';
     elim In;
-     [ reduce;
+     [ normalize;
        intro;
        apply iff_refl
      | simplify;
@@ -303,7 +348,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
@@ -321,9 +367,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.
@@ -523,14 +569,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 *)
@@ -565,16 +611,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. 
@@ -585,10 +631,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.
 
@@ -605,33 +651,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;
@@ -641,31 +682,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
@@ -726,23 +768,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);
@@ -767,33 +805,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;
@@ -862,7 +899,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
@@ -893,7 +930,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
@@ -982,39 +1019,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.
 
 *)