Minor changes because of the new, weaker (but much faster) delift.

diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma
index 03db53f7d5ff0f9863abaeba9cfe10f5bd681a33..6bcd62a653b38465021da0bb395700089e4afd70 100644 (file)
--- a/matita/matita/lib/arithmetics/bigops.ma
+++ b/matita/matita/lib/arithmetics/bigops.ma
@@ -192,7 +192,7 @@ op (\big[op,nil]_{i<k|p i}(f i)) (\big[op,nil]_{i<k|p i}(g i)) =
 #k #p #B #nil #op #f #g (elim k) [normalize @nill]
 -k #k #Hind (cases (true_or_false (p k))) #H
   [>bigop_Strue // >bigop_Strue // >bigop_Strue //
-   <assoc <assoc in ⊢ (???%) @eq_f >assoc >comm in ⊢ (??(????%?)?) 
+   normalize <assoc <assoc in ⊢ (???%) @eq_f >assoc >comm in ⊢ (??(????%?)?) 
    <assoc @eq_f @Hind
   |>bigop_Sfalse // >bigop_Sfalse // >bigop_Sfalse //
   ]
@@ -209,7 +209,7 @@ lemma bigop_diff: ∀p,B.∀nil.∀op:ACop B nil.∀f:nat → B.∀i,n.
       [>(not_eq_to_eqb_false … (lt_to_not_eq … Hi)) //] #Hcut
      cases (true_or_false (p n)) #pn 
       [>bigop_Strue // >bigop_Strue //
-       >assoc >(comm ?? op (f i) (f n)) <assoc >Hind //
+       normalize >assoc >(comm ?? op (f i) (f n)) <assoc >Hind //
       |>bigop_Sfalse // >bigop_Sfalse // >Hind //  
       ]
     |<Hi >bigop_Strue // @eq_f >bigop_Sfalse  

diff --git a/matita/matita/lib/arithmetics/chinese_reminder.ma b/matita/matita/lib/arithmetics/chinese_reminder.ma
index 0837e429e2eb4e97d0d558934eea16e5db98dd30..b327c341387c6276e3b4ad5ebbed7e7aa253faaa 100644 (file)
--- a/matita/matita/lib/arithmetics/chinese_reminder.ma
+++ b/matita/matita/lib/arithmetics/chinese_reminder.ma
@@ -118,9 +118,9 @@ theorem mod_cr_pair : ∀m,n,a,b. a < m → b < n → gcd n m = 1 →
 #m #n #a #b #ltam #ltbn #pnm 
 cut (andb (eqb ((cr_pair m n a b) \mod m) a) 
          (eqb ((cr_pair m n a b) \mod n) b) = true)
-  [@f_min_true cases(congruent_ab_lt m n a b ?? pnm)
+  [whd in match (cr_pair m n a b) @f_min_true cases(congruent_ab_lt m n a b ?? pnm)
     [#x * * #cxa #cxb #ltx @(ex_intro ?? x) % /2/
-     >eq_to_eqb_true 
+     >eq_to_eqb_true
       [>eq_to_eqb_true // <(lt_to_eq_mod …ltbn) //
       |<(lt_to_eq_mod …ltam) //
       ]

diff --git a/matita/matita/lib/arithmetics/gcd.ma b/matita/matita/lib/arithmetics/gcd.ma
index 104b598626cd73e3dc3d43c56c5eed86e3fed2ae..1490a626e336db7cc42c65f804e9e3b66b15e078 100644 (file)
--- a/matita/matita/lib/arithmetics/gcd.ma
+++ b/matita/matita/lib/arithmetics/gcd.ma
@@ -54,7 +54,7 @@ qed.
 
 lemma divides_to_gcd_aux: ∀p,m,n. O < p → O < n →n ∣ m → 
   gcd_aux p m n = n.
-#p #m #n #posp @(lt_O_n_elim … posp) #l #posn #divnm normalize 
+#p #m #n #posp @(lt_O_n_elim … posp) #l #posn #divnm whd in ⊢ (??%?)
 >divides_to_dividesb_true normalize //
 qed.
 
@@ -69,7 +69,7 @@ qed.
 
 lemma not_divides_to_gcd_aux: ∀p,m,n. 0 < n → n ∤ m → 
   gcd_aux (S p) m n = gcd_aux p n (m \mod n).
-#p #m #n #lenm #divnm normalize >not_divides_to_dividesb_false
+#p #m #n #lenm #divnm whd in ⊢ (??%?) >not_divides_to_dividesb_false
 normalize // qed.
 
 theorem divides_gcd_aux_mn: ∀p,m,n. O < n → n ≤ m → n ≤ p →

diff --git a/matita/matita/lib/arithmetics/minimization.ma b/matita/matita/lib/arithmetics/minimization.ma
index eda9d016618d1031be5b126b65b35ca105b9ee11..4c55ea6beb9b37a91e752913a0338786cea24952 100644 (file)
--- a/matita/matita/lib/arithmetics/minimization.ma
+++ b/matita/matita/lib/arithmetics/minimization.ma
@@ -122,7 +122,7 @@ qed.
 theorem max_f_g: ∀f,g,n.(∀i. i < n → f i = g i) → 
   max n f = max n g.
 #f #g #n (elim n) //
-#m #Hind #ext normalize >ext >Hind //
+#m #Hind #ext normalize >ext normalize in Hind >Hind //
 #i #ltim @ext /2/
 qed.
 

diff --git a/matita/matita/lib/arithmetics/primes.ma b/matita/matita/lib/arithmetics/primes.ma
index 71e372f96722f893ebd3889a0b78eaf59f37d1fb..3898105c6aaac49345f32c6ea925e52daf0029ed 100644 (file)
--- a/matita/matita/lib/arithmetics/primes.ma
+++ b/matita/matita/lib/arithmetics/primes.ma
@@ -361,7 +361,7 @@ qed.
 
 theorem primeb_false_to_not_prime : ∀n:nat.
   primeb n = false → ¬ (prime n).
-#n #H cut ((leb 2 n ∧ (eqb (smallest_factor n) n)) = false) [>H //] 
+#n #H cut ((leb 2 n ∧ (eqb (smallest_factor n) n)) = false) [@H] 
 @leb_elim 
   [#_ #H1 @(not_to_not … (prime_to_smallest_factor … ))
    @eqb_false_to_not_eq @H1
@@ -465,7 +465,7 @@ qed.
 theorem prime_nth_prime : ∀n:nat.prime (nth_prime n).
 #n (cases n) 
   [@primeb_true_to_prime //
-  |#m >nth_primeS @primeb_true_to_prime @f_min_true
+  |#m >nth_primeS @primeb_true_to_prime check f_min_true @(f_min_true primeb)
    @(ex_intro nat ? (smallest_factor (S (nth_prime m)!)))
    % [% // @le_S_S @(transitive_le … (le_smallest_factor_n …))
       <plus_n_Sm @le_plus_n_r

diff --git a/matita/matita/lib/basics/list.ma b/matita/matita/lib/basics/list.ma
index 21dd7e3d1aa57597da06b06b7ba2c1c192b84be2..e4bdcb8aa0a8fbd38f94ac930d4a9392507908de 100644 (file)
--- a/matita/matita/lib/basics/list.ma
+++ b/matita/matita/lib/basics/list.ma
@@ -211,8 +211,9 @@ lemma lhd_cons_ltl: ∀A,n,l. lhd A l n @ ltl A l n = l.
 #A #n elim n -n //
 #n #IHn #l elim l normalize //
 qed.
-
+(*
 lemma length_ltl: ∀A,n,l. |ltl A l n| = |l| - n.
 #A #n elim n -n /2/
 #n #IHn * normalize /2/
 qed.
+*)
\ No newline at end of file

diff --git a/matita/matita/lib/lambda/ext.ma b/matita/matita/lib/lambda/ext.ma
index 7e64aba31ff7d40ca240c63052a2c0769fffa7f3..d07234a71190f9ce6a14eea84c380039d90657b0 100644 (file)
--- a/matita/matita/lib/lambda/ext.ma
+++ b/matita/matita/lib/lambda/ext.ma
@@ -52,11 +52,11 @@ let rec all (A:Type[0]) (P:A→Prop) l on l ≝ match l with
    ].
 
 lemma all_hd: ∀A:Type[0]. ∀P:A→Prop. ∀a. P a → ∀l. all … P l → P (hd … l a).
-#A #P #a #Ha #l elim l -l [ #_ @Ha | #b #l #_ #Hl elim Hl -Hl // ]
+#A #P #a #Ha #l elim l -l [ #_ @Ha | #b #l #_ #Hl elim Hl -Hl; normalize // ]
 qed.
 
 lemma all_tl: ∀A:Type[0]. ∀P:A→Prop. ∀l. all … P l →  all … P (tail … l).
-#A #P #l elim l -l // #b #l #IH #Hl elim Hl -Hl //
+#A #P #l elim l -l // #b #l #IH #Hl elim Hl -Hl; normalize //
 qed.
 
 lemma all_nth: ∀A:Type[0]. ∀P:A→Prop. ∀a. P a → ∀i,l. all … P l → P (nth i … l a).
@@ -87,14 +87,14 @@ lemma all2_hd: ∀A,B:Type[0]. ∀P:A→B→Prop. ∀a,b. P a b →
                ∀l1,l2. all2 … P l1 l2 → P (hd … l1 a) (hd … l2 b).
 #A #B #P #a #b #Hab #l1 elim l1 -l1 [ #l2 #H2 >H2 @Hab ]
 #x1 #l1 #_ #l2 elim l2 -l2 [ #false elim false ]
-#x2 #l2 #_ #H elim H -H //
+#x2 #l2 #_ #H elim H -H; normalize //
 qed.
 
 lemma all2_tl: ∀A,B:Type[0]. ∀P:A→B→Prop.
                ∀l1,l2. all2 … P l1 l2 →  all2 … P (tail … l1) (tail … l2).
 #A #B #P #l1 elim l1 -l1 [ #l2 #H >H // ]
 #x1 #l1 #_ #l2 elim l2 -l2 [ #false elim false ]
-#x2 #l2 #_ #H elim H -H // 
+#x2 #l2 #_ #H elim H -H; normalize // 
 qed.
 
 lemma all2_nth: ∀A,B:Type[0]. ∀P:A→B→Prop. ∀a,b. P a b →