From 31e8729021717072f88d250ef41527da3488289e Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 6 Jun 2011 21:46:32 +0000
Subject: [PATCH] Minor changes because of the new, weaker (but much faster)
 delift.

---
 matita/matita/lib/arithmetics/bigops.ma           | 4 ++--
 matita/matita/lib/arithmetics/chinese_reminder.ma | 4 ++--
 matita/matita/lib/arithmetics/gcd.ma              | 4 ++--
 matita/matita/lib/arithmetics/minimization.ma     | 2 +-
 matita/matita/lib/arithmetics/primes.ma           | 4 ++--
 matita/matita/lib/basics/list.ma                  | 3 ++-
 matita/matita/lib/lambda/ext.ma                   | 8 ++++----
 7 files changed, 15 insertions(+), 14 deletions(-)

diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma
index 03db53f7d..6bcd62a65 100644
--- 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 0837e429e..b327c3413 100644
--- 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 104b59862..1490a626e 100644
--- 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 eda9d0166..4c55ea6be 100644
--- 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 71e372f96..3898105c6 100644
--- 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 21dd7e3d1..e4bdcb8aa 100644
--- 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 7e64aba31..d07234a71 100644
--- 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 →
-- 
2.39.2