From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 21 Nov 2011 09:41:59 +0000 (+0000)
Subject: {pattern} => in pattern;
X-Git-Tag: make_still_working~2077
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e28ee799d0281fb76d484d9b4c01d8bed4716bbe;p=helm.git

{pattern} => in pattern;
---

diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma
index 5e34160fe..826c6a8b2 100644
--- a/matita/matita/lib/arithmetics/bigops.ma
+++ b/matita/matita/lib/arithmetics/bigops.ma
@@ -141,7 +141,7 @@ a ≤ b → b ≤ c →
   op (\big[op,nil]_{i ∈ [b,c[ |p i}(f i)) 
       \big[op,nil]_{i ∈ [a,b[ |p i}(f i).
 #a #b # c #p #B #nil #op #f #leab #lebc 
->(plus_minus_m_m (c-a) (b-a)) {⊢ (??%?)} /2/
+>(plus_minus_m_m (c-a) (b-a)) in ⊢ (??%?); /2/
 >minus_plus >(commutative_plus a) <plus_minus_m_m //
 >bigop_sum (cut (∀i. b -a ≤ i → i+a = i-(b-a)+b))
   [#i #lei >plus_minus // <plus_minus1 
@@ -173,11 +173,11 @@ theorem bigop_prod: ∀k1,k2,p1,p2,B.∀nil.∀op:Aop B nil.∀f: nat →nat →
 #n #Hind cases(true_or_false (p1 n)) #Hp1
   [>bigop_Strue // >Hind >bigop_sum @same_bigop
    #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/
-   #eqi [|#H] >eqi {⊢ (???%)}
+   #eqi [|#H] >eqi in ⊢ (???%);
      >div_plus_times /2/ >Hp1 >(mod_plus_times …) /2/ normalize //
   |>bigop_Sfalse // >Hind >(pad_bigop (S n*k2)) // @same_bigop
    #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/
-   #eqi >eqi {⊢ (???%)} >div_plus_times /2/ 
+   #eqi >eqi in ⊢ (???%); >div_plus_times /2/ 
   ]
 qed.
 
@@ -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 //
-   normalize <assoc <assoc {⊢ (???%)} @eq_f >assoc >comm {⊢ (??(????%?)?)}
+   normalize <assoc <assoc in ⊢ (???%); @eq_f >assoc >comm in ⊢ (??(????%?)?);
    <assoc @eq_f @Hind
   |>bigop_Sfalse // >bigop_Sfalse // >bigop_Sfalse //
   ]
@@ -263,7 +263,7 @@ theorem bigop_iso: ∀n1,n2,p1,p2,B.∀nil.∀op:ACop B nil.∀f1,f2.
   iso B (mk_range B f1 n1 p1) (mk_range B f2 n2 p2) →
   \big[op,nil]_{i<n1|p1 i}(f1 i) = \big[op,nil]_{i<n2|p2 i}(f2 i).
 #n1 #n2 #p1 #p2 #B #nil #op #f1 #f2 * #h * #k * * #same
-@(le_gen ? n1) #i generalize {match p2} (elim i) 
+@(le_gen ? n1) #i lapply p2 (elim i) 
   [(elim n2) // #m #Hind #p2 #_ #sub1 #sub2
    >bigop_Sfalse 
     [@(Hind ? (le_O_n ?)) [/2/ | @(transitive_sub … (sub_lt …) sub2) //]
@@ -280,7 +280,7 @@ theorem bigop_iso: ∀n1,n2,p1,p2,B.∀nil.∀op:ACop B nil.∀f1,f2.
       |#j #ltj #p2j (cases (sub2 j ltj (andb_true_r …p2j))) * 
        #ltkj #p1kj #eqj % // % // 
        (cases (le_to_or_lt_eq …(le_S_S_to_le …ltkj))) //
-       #eqkj @False_ind generalize {match p2j} @eqb_elim 
+       #eqkj @False_ind lapply p2j @eqb_elim 
        normalize /2/
       ]
     |>bigop_Sfalse // @(Hind ? len) 
@@ -298,7 +298,7 @@ qed.
 record Dop (A:Type[0]) (nil:A): Type[0] ≝
   {sum : ACop A nil; 
    prod: A → A →A;
-   null: ∀a. prod a nil = nil; 
+   null: \forall a. prod a nil = nil; 
    distr: ∀a,b,c:A. prod a (sum b c) = sum (prod a b) (prod a c)
   }.
   
diff --git a/matita/matita/lib/arithmetics/binomial.ma b/matita/matita/lib/arithmetics/binomial.ma
index 7ab00d499..a8b1cef79 100644
--- a/matita/matita/lib/arithmetics/binomial.ma
+++ b/matita/matita/lib/arithmetics/binomial.ma
@@ -44,12 +44,12 @@ theorem bc2 : ∀n.
      cut (m-(m-(S c)) = S c) [@plus_to_minus @plus_minus_m_m //] #eqSc     
      lapply (Hind c (le_S_S_to_le … lec)) #Hc
      lapply (Hind (m - (S c)) ?) [@le_plus_to_minus //] >eqSc #Hmc
-     >(plus_minus_m_m m c) {⊢ (??(??(?%)))} [|@le_S_S_to_le //]
+     >(plus_minus_m_m m c) in ⊢ (??(??(?%))); [|@le_S_S_to_le //]
      >commutative_plus >(distributive_times_plus ? (S c))
      @divides_plus
       [>associative_times >(commutative_times (S c))
        <associative_times @divides_times //
-      |<(fact_minus …ltcm) {⊢ (?(??%)?)}
+      |<(fact_minus …ltcm) in ⊢ (?(??%)?);
        <associative_times @divides_times //
        >commutative_times @Hmc
       ]
@@ -61,18 +61,18 @@ qed.
 theorem bc1: ∀n.∀k. k < n → 
   bc (S n) (S k) = (bc n k) + (bc n (S k)).
 #n #k #ltkn > bceq >(bceq n) >(bceq n (S k))
->(div_times_times ?? (S k)) {⊢ (???(?%?))}
+>(div_times_times ?? (S k)) in ⊢ (???(?%?));
   [|>(times_n_O 0) @lt_times // | //]
->associative_times {⊢ (???(?(??%)?))}
->commutative_times {⊢ (???(?(??(??%))?))}
-<associative_times {⊢ (???(?(??%)?))}
->(div_times_times ?? (n - k)) {⊢ (???(??%))}
+>associative_times in ⊢ (???(?(??%)?));
+>commutative_times in ⊢ (???(?(??(??%))?));
+<associative_times in ⊢ (???(?(??%)?));
+>(div_times_times ?? (n - k)) in ⊢ (???(??%)) ; 
   [|>(times_n_O 0) @lt_times // 
    |@(le_plus_to_le_r k ??) <plus_minus_m_m /2/]
->associative_times {⊢ (???(??(??%)))}
+>associative_times in ⊢ (???(??(??%)));
 >fact_minus // <plus_div 
   [<distributive_times_plus
-   >commutative_plus {⊢ (???%)} <plus_n_Sm <plus_minus_m_m [|/2/] @refl
+   >commutative_plus in ⊢ (???%); <plus_n_Sm <plus_minus_m_m [|/2/] @refl
   |<fact_minus // <associative_times @divides_times // @(bc2 n (S k)) //
   |>associative_times >(commutative_times (S k))
    <associative_times @divides_times // @bc2 /2/
diff --git a/matita/matita/lib/arithmetics/chinese_reminder.ma b/matita/matita/lib/arithmetics/chinese_reminder.ma
index 77c0c7959..ec20f30da 100644
--- a/matita/matita/lib/arithmetics/chinese_reminder.ma
+++ b/matita/matita/lib/arithmetics/chinese_reminder.ma
@@ -118,7 +118,7 @@ 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)
-  [whd {match (cr_pair m n a b)} @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 // <(lt_to_eq_mod …ltbn) //
diff --git a/matita/matita/lib/arithmetics/congruence.ma b/matita/matita/lib/arithmetics/congruence.ma
index 2a9e06b0f..d9792b5eb 100644
--- a/matita/matita/lib/arithmetics/congruence.ma
+++ b/matita/matita/lib/arithmetics/congruence.ma
@@ -37,7 +37,7 @@ theorem le_to_mod: ∀n,m:nat. n < m → n = n \mod m.
 qed.
 
 theorem mod_mod : ∀n,p:nat. O<p → n \mod p = (n \mod p) \mod p.
-#n #p #posp >(div_mod (n \mod p) p) {⊢ (? ? % ?) }
+#n #p #posp >(div_mod (n \mod p) p) in ⊢ (? ? % ?); 
 >(eq_div_O ? p) // @lt_mod_m_m //
 qed.
 
@@ -79,8 +79,8 @@ qed.
 theorem congruent_to_divides: ∀n,m,p:nat.O < p → 
   n ≅_{p} m → p ∣ (n - m).
 #n #m #p #posp #congnm @(quotient ? ? ((n / p)-(m / p)))
->commutative_times >(div_mod n p) {⊢ (??%?)}
->(div_mod m p) {⊢ (??%?)} <(commutative_plus (m \mod p))
+>commutative_times >(div_mod n p) in ⊢ (??%?);
+>(div_mod m p) in ⊢ (??%?); <(commutative_plus (m \mod p))
 <congnm <(minus_plus ? (n \mod p)) <minus_plus_m_m //
 qed.
 
diff --git a/matita/matita/lib/arithmetics/div_and_mod.ma b/matita/matita/lib/arithmetics/div_and_mod.ma
index 6932a86e0..44b796e6b 100644
--- a/matita/matita/lib/arithmetics/div_and_mod.ma
+++ b/matita/matita/lib/arithmetics/div_and_mod.ma
@@ -178,7 +178,7 @@ theorem or_div_mod: ∀n,q. O < q →
 #n #q #posq 
 (elim (le_to_or_lt_eq ?? (lt_mod_m_m n q posq))) #H
   [%2 % // applyS eq_f // 
-  |%1 % // /demod/ <H {⊢(? ? ? (? % ?))} @eq_f//
+  |%1 % // /demod/ <H in ⊢(? ? ? (? % ?)); @eq_f//
   ]
 qed.
 
@@ -210,13 +210,13 @@ definition n_divides \def \lambda n,m:nat.n_divides_aux n n m O. *)
 
 theorem lt_div_S: ∀n,m. O < m → n < S(n / m)*m.
 #n #m #posm (change with (n < m +(n/m)*m))
->(div_mod n m) {⊢ (? % ?)} >commutative_plus 
+>(div_mod n m) in ⊢ (? % ?); >commutative_plus 
 @monotonic_lt_plus_l @lt_mod_m_m // 
 qed.
 
 theorem le_div: ∀n,m. O < n → m/n ≤ m.
 #n #m #posn
->(div_mod m n) {⊢ (? ? %)} @(transitive_le ? (m/n*n)) /2/
+>(div_mod m n) in ⊢ (? ? %); @(transitive_le ? (m/n*n)) /2/
 qed.
 
 theorem le_plus_mod: ∀m,n,q. O < q →
@@ -228,9 +228,9 @@ theorem le_plus_mod: ∀m,n,q. O < q →
      @(div_mod_spec_to_eq2 … (m/q + n/q) ? (div_mod_spec_div_mod … posq)).
      @div_mod_spec_intro
       [@not_le_to_lt //
-      |>(div_mod n q) {⊢ (? ? (? ? %) ?)}
+      |>(div_mod n q) in ⊢ (? ? (? ? %) ?);
        (applyS (eq_f … (λx.plus x (n \mod q))))
-       >(div_mod m q) {⊢ (? ? (? % ?) ?)}
+       >(div_mod m q) in ⊢ (? ? (? % ?) ?);
        (applyS (eq_f … (λx.plus x (m \mod q)))) //
       ]
   ]
@@ -241,10 +241,10 @@ theorem le_plus_div: ∀m,n,q. O < q →
 #m #n #q #posq @(le_times_to_le … posq)
 @(le_plus_to_le_r ((m+n) \mod q))
 (* bruttino *)
->commutative_times {⊢ (? ? %)} <div_mod
->(div_mod m q) {⊢ (? ? (? % ?))} >(div_mod n q) {⊢ (? ? (? ? %))}
->commutative_plus {⊢ (? ? (? % ?))} >associative_plus {⊢ (? ? %)}
-<associative_plus {⊢ (? ? (? ? %))} (applyS monotonic_le_plus_l) /2/
+>commutative_times in ⊢ (? ? %); <div_mod
+>(div_mod m q) in ⊢ (? ? (? % ?)); >(div_mod n q) in ⊢ (? ? (? ? %));
+>commutative_plus in ⊢ (? ? (? % ?)); >associative_plus in ⊢ (? ? %);
+<associative_plus in ⊢ (? ? (? ? %)); (applyS monotonic_le_plus_l) /2/
 qed.
 
 theorem le_times_to_le_div: ∀a,b,c:nat. 
diff --git a/matita/matita/lib/arithmetics/exp.ma b/matita/matita/lib/arithmetics/exp.ma
index 2c3b12d07..654185c89 100644
--- a/matita/matita/lib/arithmetics/exp.ma
+++ b/matita/matita/lib/arithmetics/exp.ma
@@ -113,7 +113,7 @@ theorem injective_exp_r: ∀b:nat. 1 < b →
 #b #lt1b @nat_elim2 normalize 
   [#n #H @sym_eq @(exp_to_eq_O b n lt1b) //
   |#n #H @False_ind @(absurd (1 < 1) ? (not_le_Sn_n 1))
-   <H {⊢ (??%)} @(lt_to_le_to_lt ? (1*b)) //
+   <H in ⊢ (??%); @(lt_to_le_to_lt ? (1*b)) //
    @le_times // @lt_O_exp /2/
   |#n #m #Hind #H @eq_f @Hind @(injective_times_l … H) /2/
   ]
diff --git a/matita/matita/lib/arithmetics/factorial.ma b/matita/matita/lib/arithmetics/factorial.ma
index d2c716d70..a95eaaef1 100644
--- a/matita/matita/lib/arithmetics/factorial.ma
+++ b/matita/matita/lib/arithmetics/factorial.ma
@@ -55,8 +55,8 @@ theorem fact_to_exp1: ∀n.O<n →
    @(transitive_le ? ((2^(pred (2*n))) * n! * n! *(2*(S n))*(2*(S n))))
     [@le_times[@le_times //]//
     (* we generalize to hide the computational content *)
-    |normalize {match ((S n)!)} generalize {match (S n)}
-     #Sn generalize {match 2} #two //
+    |normalize in match ((S n)!); generalize in match (S n);
+     #Sn generalize in match 2; #two //
     ]
   ]
 qed.  
@@ -72,8 +72,8 @@ theorem exp_to_fact1: ∀n.O < n →
 #n #posn #Hind (cut (∀i.2*(S i) = S(S(2*i)))) [//] #H
 cut (2^(2*(S n)) = 2^(2*n)*2*2) [>H //] #H1 >H1
 @(le_to_lt_to_lt ? (2^(2*n)*n!*n!*(2*(S n))*(2*(S n))))
-  [normalize {match ((S n)!)} generalize {match (S n)} #Sn
-   generalize {match 2} #two //
+  [normalize in match ((S n)!); generalize in match (S n); #Sn
+   generalize in match 2; #two //
   |cut ((S(2*(S n)))! = (S(2*n))!*(S(S(2*n)))*(S(S(S(2*n)))))
    [>H //] #H2 >H2 @lt_to_le_to_lt_times
      [@lt_to_le_to_lt_times //|>H // | //]
diff --git a/matita/matita/lib/arithmetics/gcd.ma b/matita/matita/lib/arithmetics/gcd.ma
index 8b496e9c5..1fe651915 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 whd {⊢ (??%?)}
+#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 whd {⊢ (??%?)} >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 →
@@ -182,13 +182,13 @@ theorem eq_minus_gcd_aux: ∀p,m,n.O < n → n ≤ m →  n ≤ p →
       [(* first case *)
        <H @(ex_intro ?? (b+a*(m / n))) @(ex_intro ?? a) %2
        <commutative_plus >distributive_times_plus_r 
-       >(div_mod m n) {⊢(? ? (? % ?) ?)}
+       >(div_mod m n) in ⊢(? ? (? % ?) ?);
        >associative_times <commutative_plus >distributive_times_plus
        <minus_plus <commutative_plus <plus_minus //
       |(* second case *)
         <H @(ex_intro ?? (b+a*(m / n))) @(ex_intro ?? a) %1
         >distributive_times_plus_r
-        >(div_mod m n) {⊢ (? ? (? ? %) ?)}
+        >(div_mod m n) in ⊢ (? ? (? ? %) ?);
         >distributive_times_plus >associative_times
         <minus_plus <commutative_plus <plus_minus //
       ]
@@ -367,7 +367,7 @@ qed.
 theorem gcd_1_to_divides_times_to_divides: ∀p,n,m:nat. O < p →
 gcd p n = 1 → p ∣ (n*m) → p ∣ m.
 #p #m #n #posn #gcd1 * #c #nm
-cases(eq_minus_gcd m p) #a * #b * #H >gcd1 {H} #H 
+cases(eq_minus_gcd m p) #a * #b * #H >gcd1 in H; #H 
   [@(quotient ?? (a*n-c*b)) >distributive_times_minus <associative_times 
    <associative_times <nm >(commutative_times m) >commutative_times
    >associative_times <distributive_times_minus //
@@ -398,7 +398,7 @@ qed.
 
 theorem divides_to_divides_times: ∀p,q,n. prime p  → p ∤ q →
  p ∣ n → q ∣ n → p*q ∣ n.
-#p #q #n #primep #notdivpq #divpn * #b #eqn (>eqn {divpn})
+#p #q #n #primep #notdivpq #divpn * #b #eqn >eqn in divpn;
 #divpn cases(divides_times_to_divides ??? primep divpn) #H
   [@False_ind /2/ 
   |cases H #c #eqb @(quotient ?? c) >eqb <associative_times //
diff --git a/matita/matita/lib/arithmetics/minimization.ma b/matita/matita/lib/arithmetics/minimization.ma
index 143104c50..35f177331 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 normalize {Hind} >Hind //
+#m #Hind #ext normalize >ext normalize in Hind; >Hind //
 #i #ltim @ext /2/
 qed.