Scripts fixed because of:

a) reduce got rid of
b) different behaviour of reduction w.r.t. zeta-reduction

diff --git a/helm/software/matita/library/algebra/CoRN/Setoids.ma b/helm/software/matita/library/algebra/CoRN/Setoids.ma
index 30c8c8bd5d128ebefbfc2d212f5e7ac75f8927ac..ddbb807a85643681b923fc6ee91afb367b0d6c50 100644 (file)
--- a/helm/software/matita/library/algebra/CoRN/Setoids.ma
+++ b/helm/software/matita/library/algebra/CoRN/Setoids.ma
@@ -1115,7 +1115,7 @@ intros.
 unfold.unfold.intros 2.elim x 2.elim y 2.
 simplify.
 intro.
-reduce in H2.
+normalize in H2.
 apply (un_op_wd_unfolded ? f ? ? H2).
 qed.
 
@@ -1123,7 +1123,7 @@ lemma restr_un_op_strext : \forall S:CSetoid. \forall P: S \to Prop.
 \forall f: CSetoid_un_op S. \forall pr: un_op_pres_pred S P f.  
 un_op_strext (mk_SubCSetoid S P) (restr_un_op S P f pr).
 intros.unfold.unfold. intros 2.elim y 2. elim x 2.
-intros.reduce in H2.
+intros.normalize in H2.
 apply (cs_un_op_strext ? f ? ? H2).
 qed.
 
@@ -1182,8 +1182,8 @@ intros.
 unfold.unfold.intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2.
 simplify.
 intros.
-reduce in H4.
-reduce in H5.
+normalize in H4.
+normalize in H5.
 apply (cs_bin_op_wd ? f ? ? ? ? H4 H5).
 qed.
 
@@ -1192,7 +1192,7 @@ lemma restr_bin_op_strext : \forall S:CSetoid. \forall P: S \to Prop.
 bin_op_strext (mk_SubCSetoid S P) (restr_bin_op S P f pr).
 intros.unfold.unfold. intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2.
 simplify.intros.
-reduce in H4.
+normalize in H4.
 apply (cs_bin_op_strext ? f ? ? ? ? H4).
 qed.
 

diff --git a/helm/software/matita/library/decidable_kit/fintype.ma b/helm/software/matita/library/decidable_kit/fintype.ma
index 9223400e7a418c842df929e71340f5e1c931a6d6..6bfa6969f1d38e223c1542b744990e82607e5bf6 100644 (file)
--- a/helm/software/matita/library/decidable_kit/fintype.ma
+++ b/helm/software/matita/library/decidable_kit/fintype.ma
@@ -106,8 +106,8 @@ cut (∀x:fsort. count fsort (cmp fsort x) enum = (S O));
          fold simplify (sort nat_eqType); (* CANONICAL?! *)
          cases (in_sub_eq nat_eqType (λx:nat_eqType.ltb x bound) w);
          simplify; [2: reflexivity]
-         generalize in match H1; clear H1; cases s; clear s; intros (H1);
-         unfold segment; simplify; simplify in H1; rewrite > H1;
+         generalize in match H1; clear H1; cases s (r Pr); clear s; intros (H1);
+         unfold fsort; unfold segment; simplify; simplify in H1; rewrite > H1;
          rewrite > iota_ltb in Hw; apply (p2bF ? ? (eqP nat_eqType ? ?));
          unfold Not; intros (Enw); rewrite > Enw in Hw; 
          rewrite > ltb_refl in Hw; destruct Hw]

diff --git a/helm/software/matita/library/nat/generic_iter_p.ma b/helm/software/matita/library/nat/generic_iter_p.ma
index 5f15bddc93e86a452497614bae6fc236d1ebf9a7..4796ec10b2e14c1829daefba403a11b34e98e38d 100644 (file)
--- a/helm/software/matita/library/nat/generic_iter_p.ma
+++ b/helm/software/matita/library/nat/generic_iter_p.ma
@@ -1571,7 +1571,10 @@ apply (trans_eq ? ?
                 [ assumption
                 | assumption
                 ]
-              | rewrite > H14.
+              | unfold ha.
+                unfold ha12.
+                unfold ha22.
+                rewrite > H14.
                 rewrite > H13.
                 apply sym_eq.
                 apply div_mod.
@@ -1618,18 +1621,23 @@ apply (trans_eq ? ?
                 rewrite > Hcut.
                 assumption
               ] 
-            | rewrite > Hcut1.
+            | unfold ha.
+              unfold ha12.
+              rewrite > Hcut1.
               rewrite > Hcut.
               assumption
             ]
-          | rewrite > Hcut1.
+          | unfold ha.
+            unfold ha22.
+            rewrite > Hcut1.
             rewrite > Hcut.
             assumption            
           ]
         | cut(O \lt m1)
           [ cut(O \lt n1)      
             [ apply (lt_to_le_to_lt ? ((h11 i j)*m1 + m1) )
-              [ apply (lt_plus_r).
+              [ unfold ha.
+                apply (lt_plus_r).
                 assumption
               | rewrite > sym_plus.
                 rewrite > (sym_times (h11 i j) m1).
@@ -1755,7 +1763,4 @@ apply (iter_p_gen_2_eq A baseA plusA H H1 H2 (\lambda x,y. g x y) (\lambda x,y.y
     |assumption
     ]
   ]
-qed.
-
-
-
+qed.
\ No newline at end of file

diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma
index d9fd301fcf2e9f075596c455a20e72db2a2d4c6b..f9c5e878bf1490346d82810827c2aea0d9470f36 100644 (file)
--- a/helm/software/matita/library/technicalities/setoids.ma
+++ b/helm/software/matita/library/technicalities/setoids.ma
@@ -150,8 +150,8 @@ 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;
@@ -203,7 +203,7 @@ 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;
@@ -236,7 +236,7 @@ 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;
@@ -275,7 +275,7 @@ 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;
@@ -298,7 +298,7 @@ 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;
@@ -332,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;