1) \ldots here and there

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / word32_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/word32_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/word32_lemmas.ma
index b35e68f9fb96b5e29f6a390a5b98e51fcf9cba3d..dd9a394d38524f9a50287179fb72879f0d7b4fb2 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/word32_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/word32_lemmas.ma
@@ -34,7 +34,7 @@ nlemma word32_destruct_1 :
  nchange with (match mk_word32 x2 y2 with [ mk_word32 a _ ⇒ x1 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma word32_destruct_2 :
@@ -44,7 +44,7 @@ nlemma word32_destruct_2 :
  nchange with (match mk_word32 x2 y2 with [ mk_word32 _ b ⇒ y1 = b ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_eqw32 : symmetricT word32 bool eq_w32.
@@ -55,7 +55,7 @@ nlemma symmetric_eqw32 : symmetricT word32 bool eq_w32.
  nchange with (((eq_w16 w3 w1)⊗(eq_w16 w4 w2)) = ((eq_w16 w1 w3)⊗(eq_w16 w2 w4)));
  nrewrite > (symmetric_eqw16 w1 w3);
  nrewrite > (symmetric_eqw16 w2 w4);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_andw32 : symmetricT word32 word32 and_w32.
@@ -66,7 +66,7 @@ nlemma symmetric_andw32 : symmetricT word32 word32 and_w32.
  nchange with ((mk_word32 (and_w16 w3 w1) (and_w16 w4 w2)) = (mk_word32 (and_w16 w1 w3) (and_w16 w2 w4)));
  nrewrite > (symmetric_andw16 w1 w3);
  nrewrite > (symmetric_andw16 w2 w4);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma associative_andw32 : ∀dw1,dw2,dw3.(and_w32 (and_w32 dw1 dw2) dw3) = (and_w32 dw1 (and_w32 dw2 dw3)).
@@ -81,7 +81,7 @@ nlemma associative_andw32 : ∀dw1,dw2,dw3.(and_w32 (and_w32 dw1 dw2) dw3) = (an
   mk_word32 (and_w16 w1 (and_w16 w3 w5)) (and_w16 w2 (and_w16 w4 w6)));
  nrewrite < (associative_andw16 w1 w3 w5);
  nrewrite < (associative_andw16 w2 w4 w6);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_orw32 : symmetricT word32 word32 or_w32.
@@ -92,7 +92,7 @@ nlemma symmetric_orw32 : symmetricT word32 word32 or_w32.
  nchange with ((mk_word32 (or_w16 w3 w1) (or_w16 w4 w2)) = (mk_word32 (or_w16 w1 w3) (or_w16 w2 w4)));
  nrewrite > (symmetric_orw16 w1 w3);
  nrewrite > (symmetric_orw16 w2 w4);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma associative_orw32 : ∀dw1,dw2,dw3.(or_w32 (or_w32 dw1 dw2) dw3) = (or_w32 dw1 (or_w32 dw2 dw3)).
@@ -107,7 +107,7 @@ nlemma associative_orw32 : ∀dw1,dw2,dw3.(or_w32 (or_w32 dw1 dw2) dw3) = (or_w3
   mk_word32 (or_w16 w1 (or_w16 w3 w5)) (or_w16 w2 (or_w16 w4 w6)));
  nrewrite < (associative_orw16 w1 w3 w5);
  nrewrite < (associative_orw16 w2 w4 w6);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_xorw32 : symmetricT word32 word32 xor_w32.
@@ -118,7 +118,7 @@ nlemma symmetric_xorw32 : symmetricT word32 word32 xor_w32.
  nchange with ((mk_word32 (xor_w16 w3 w1) (xor_w16 w4 w2)) = (mk_word32 (xor_w16 w1 w3) (xor_w16 w2 w4)));
  nrewrite > (symmetric_xorw16 w1 w3);
  nrewrite > (symmetric_xorw16 w2 w4);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma associative_xorw32 : ∀dw1,dw2,dw3.(xor_w32 (xor_w32 dw1 dw2) dw3) = (xor_w32 dw1 (xor_w32 dw2 dw3)).
@@ -133,7 +133,7 @@ nlemma associative_xorw32 : ∀dw1,dw2,dw3.(xor_w32 (xor_w32 dw1 dw2) dw3) = (xo
   mk_word32 (xor_w16 w1 (xor_w16 w3 w5)) (xor_w16 w2 (xor_w16 w4 w6)));
  nrewrite < (associative_xorw16 w1 w3 w5);
  nrewrite < (associative_xorw16 w2 w4 w6);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_plusw32_dc_dc : ∀dw1,dw2,c.plus_w32_dc_dc dw1 dw2 c = plus_w32_dc_dc dw2 dw1 c.
@@ -145,20 +145,20 @@ nlemma symmetric_plusw32_dc_dc : ∀dw1,dw2,c.plus_w32_dc_dc dw1 dw2 c = plus_w3
  nchange with (
   match plus_w16_dc_dc w2 w4 c with
    [ pair l c ⇒ match plus_w16_dc_dc w1 w3 c with
-    [ pair h c' ⇒ pair ?? 〈h.l〉 c' ]] =
+    [ pair h c' ⇒ pair … 〈h.l〉 c' ]] =
   match plus_w16_dc_dc w4 w2 c with
    [ pair l c ⇒ match plus_w16_dc_dc w3 w1 c with
-    [ pair h c' ⇒ pair ?? 〈h.l〉 c' ]]);
+    [ pair h c' ⇒ pair … 〈h.l〉 c' ]]);
  nrewrite > (symmetric_plusw16_dc_dc w4 w2 c);
  ncases (plus_w16_dc_dc w2 w4 c);
  #w5; #c1;
  nchange with (
   match plus_w16_dc_dc w1 w3 c1 with
-   [ pair h c' ⇒ pair ?? 〈h.w5〉 c' ] =
+   [ pair h c' ⇒ pair … 〈h.w5〉 c' ] =
   match plus_w16_dc_dc w3 w1 c1 with
-   [ pair h c' ⇒ pair ?? 〈h.w5〉 c' ]);
+   [ pair h c' ⇒ pair … 〈h.w5〉 c' ]);
  nrewrite > (symmetric_plusw16_dc_dc w1 w3 c1);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_plusw32_dc_d : ∀dw1,dw2,c.plus_w32_dc_d dw1 dw2 c = plus_w32_dc_d dw2 dw1 c.
@@ -177,7 +177,7 @@ nlemma symmetric_plusw32_dc_d : ∀dw1,dw2,c.plus_w32_dc_d dw1 dw2 c = plus_w32_
  #w5; #c1;
  nchange with (〈plus_w16_dc_d w1 w3 c1.w5〉 = 〈plus_w16_dc_d w3 w1 c1.w5〉);
  nrewrite > (symmetric_plusw16_dc_d w1 w3 c1);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_plusw32_dc_c : ∀dw1,dw2,c.plus_w32_dc_c dw1 dw2 c = plus_w32_dc_c dw2 dw1 c.
@@ -191,7 +191,7 @@ nlemma symmetric_plusw32_dc_c : ∀dw1,dw2,c.plus_w32_dc_c dw1 dw2 c = plus_w32_
   plus_w16_dc_c w3 w1 (plus_w16_dc_c w4 w2 c));
  nrewrite > (symmetric_plusw16_dc_c w4 w2 c);
  nrewrite > (symmetric_plusw16_dc_c w3 w1 (plus_w16_dc_c w2 w4 c));
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_plusw32_d_dc : ∀dw1,dw2.plus_w32_d_dc dw1 dw2 = plus_w32_d_dc dw2 dw1.
@@ -203,20 +203,20 @@ nlemma symmetric_plusw32_d_dc : ∀dw1,dw2.plus_w32_d_dc dw1 dw2 = plus_w32_d_dc
  nchange with (
   match plus_w16_d_dc w2 w4 with
    [ pair l c ⇒ match plus_w16_dc_dc w1 w3 c with
-    [ pair h c' ⇒ pair ?? 〈h.l〉 c' ]] =
+    [ pair h c' ⇒ pair … 〈h.l〉 c' ]] =
   match plus_w16_d_dc w4 w2 with
    [ pair l c ⇒ match plus_w16_dc_dc w3 w1 c with
-    [ pair h c' ⇒ pair ?? 〈h.l〉 c' ]]);
+    [ pair h c' ⇒ pair … 〈h.l〉 c' ]]);
  nrewrite > (symmetric_plusw16_d_dc w4 w2);
  ncases (plus_w16_d_dc w2 w4);
  #w5; #c;
  nchange with (
   match plus_w16_dc_dc w1 w3 c with
-   [ pair h c' ⇒ pair ?? 〈h.w5〉 c' ] =
+   [ pair h c' ⇒ pair … 〈h.w5〉 c' ] =
   match plus_w16_dc_dc w3 w1 c with
-   [ pair h c' ⇒ pair ?? 〈h.w5〉 c' ]);
+   [ pair h c' ⇒ pair … 〈h.w5〉 c' ]);
  nrewrite > (symmetric_plusw16_dc_dc w1 w3 c);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_plusw32_d_d : ∀dw1,dw2.plus_w32_d_d dw1 dw2 = plus_w32_d_d dw2 dw1.
@@ -235,7 +235,7 @@ nlemma symmetric_plusw32_d_d : ∀dw1,dw2.plus_w32_d_d dw1 dw2 = plus_w32_d_d dw
  #w5; #c;
  nchange with (〈plus_w16_dc_d w1 w3 c.w5〉 = 〈plus_w16_dc_d w3 w1 c.w5〉);
  nrewrite > (symmetric_plusw16_dc_d w1 w3 c);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_plusw32_d_c : ∀dw1,dw2.plus_w32_d_c dw1 dw2 = plus_w32_d_c dw2 dw1.
@@ -249,7 +249,7 @@ nlemma symmetric_plusw32_d_c : ∀dw1,dw2.plus_w32_d_c dw1 dw2 = plus_w32_d_c dw
   plus_w16_dc_c w3 w1 (plus_w16_d_c w4 w2));
  nrewrite > (symmetric_plusw16_d_c w4 w2);
  nrewrite > (symmetric_plusw16_dc_c w3 w1 (plus_w16_d_c w2 w4));
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_mulw16 : symmetricT word16 word32 mul_w16.
@@ -296,7 +296,7 @@ nlemma symmetric_mulw16 : symmetricT word16 word32 mul_w16.
  nchange with ((plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:b7〉.〈b8:〈x0,x0〉〉〉 〈〈〈x0,x0〉:b9〉.〈b10:〈x0,x0〉〉〉) 〈〈b11:b12〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉) =
   (plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:b9〉.〈b10:〈x0,x0〉〉〉 〈〈〈x0,x0〉:b7〉.〈b8:〈x0,x0〉〉〉) 〈〈b11:b12〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉));
  nrewrite > (symmetric_plusw32_d_d 〈〈〈x0,x0〉:b7〉.〈b8:〈x0,x0〉〉〉 〈〈〈x0,x0〉:b9〉.〈b10:〈x0,x0〉〉〉);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma eqw32_to_eq : ∀dw1,dw2:word32.(eq_w32 dw1 dw2 = true) → (dw1 = dw2).
@@ -306,9 +306,9 @@ nlemma eqw32_to_eq : ∀dw1,dw2:word32.(eq_w32 dw1 dw2 = true) → (dw1 = dw2).
  #w1; #w2; #w3; #w4;
  nchange in ⊢ (% → ?) with (((eq_w16 w3 w1)⊗(eq_w16 w4 w2)) = true);
  #H;
- nrewrite < (eqw16_to_eq ?? (andb_true_true_l ?? H));
- nrewrite < (eqw16_to_eq ?? (andb_true_true_r ?? H));
- napply (refl_eq ??).
+ nrewrite < (eqw16_to_eq … (andb_true_true_l … H));
+ nrewrite < (eqw16_to_eq … (andb_true_true_r … H));
+ napply refl_eq.
 nqed.
 
 nlemma eq_to_eqw32 : ∀dw1,dw2.dw1 = dw2 → eq_w32 dw1 dw2 = true.
@@ -317,11 +317,11 @@ nlemma eq_to_eqw32 : ∀dw1,dw2.dw1 = dw2 → eq_w32 dw1 dw2 = true.
  nelim dw2;
  #w1; #w2; #w3; #w4;
  #H;
- nrewrite < (word32_destruct_1 ???? H);
- nrewrite < (word32_destruct_2 ???? H);
+ nrewrite < (word32_destruct_1 … H);
+ nrewrite < (word32_destruct_2 … H);
  nchange with (((eq_w16 w3 w3)⊗(eq_w16 w4 w4)) = true);
- nrewrite > (eq_to_eqw16 w3 w3 (refl_eq ??));
- nrewrite > (eq_to_eqw16 w4 w4 (refl_eq ??)); 
+ nrewrite > (eq_to_eqw16 w3 w3 (refl_eq …));
+ nrewrite > (eq_to_eqw16 w4 w4 (refl_eq …)); 
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.