1) \ldots here and there

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/word16_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/word16_lemmas.ma
index 7b556c439fdf9db40d6ff66bcbef9d7ee44d3be3..826bd8f897570ab924e7297810b01db5cdaf7711 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/word16_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/word16_lemmas.ma
@@ -34,7 +34,7 @@ nlemma word16_destruct_1 :
  nchange with (match mk_word16 x2 y2 with [ mk_word16 a _ ⇒ x1 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma word16_destruct_2 :
@@ -44,7 +44,7 @@ nlemma word16_destruct_2 :
  nchange with (match mk_word16 x2 y2 with [ mk_word16 _ b ⇒ y1 = b ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_eqw16 : symmetricT word16 bool eq_w16.
@@ -55,7 +55,7 @@ nlemma symmetric_eqw16 : symmetricT word16 bool eq_w16.
  nchange with (((eq_b8 b3 b1)⊗(eq_b8 b4 b2)) = ((eq_b8 b1 b3)⊗(eq_b8 b2 b4)));
  nrewrite > (symmetric_eqb8 b1 b3);
  nrewrite > (symmetric_eqb8 b2 b4);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_andw16 : symmetricT word16 word16 and_w16.
@@ -66,7 +66,7 @@ nlemma symmetric_andw16 : symmetricT word16 word16 and_w16.
  nchange with ((mk_word16 (and_b8 b3 b1) (and_b8 b4 b2)) = (mk_word16 (and_b8 b1 b3) (and_b8 b2 b4)));
  nrewrite > (symmetric_andb8 b1 b3);
  nrewrite > (symmetric_andb8 b2 b4);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma associative_andw16 : ∀w1,w2,w3.(and_w16 (and_w16 w1 w2) w3) = (and_w16 w1 (and_w16 w2 w3)).
@@ -81,7 +81,7 @@ nlemma associative_andw16 : ∀w1,w2,w3.(and_w16 (and_w16 w1 w2) w3) = (and_w16
   mk_word16 (and_b8 b1 (and_b8 b3 b5)) (and_b8 b2 (and_b8 b4 b6)));
  nrewrite < (associative_andb8 b1 b3 b5);
  nrewrite < (associative_andb8 b2 b4 b6);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_orw16 : symmetricT word16 word16 or_w16.
@@ -92,7 +92,7 @@ nlemma symmetric_orw16 : symmetricT word16 word16 or_w16.
  nchange with ((mk_word16 (or_b8 b3 b1) (or_b8 b4 b2)) = (mk_word16 (or_b8 b1 b3) (or_b8 b2 b4)));
  nrewrite > (symmetric_orb8 b1 b3);
  nrewrite > (symmetric_orb8 b2 b4);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma associative_orw16 : ∀w1,w2,w3.(or_w16 (or_w16 w1 w2) w3) = (or_w16 w1 (or_w16 w2 w3)).
@@ -107,7 +107,7 @@ nlemma associative_orw16 : ∀w1,w2,w3.(or_w16 (or_w16 w1 w2) w3) = (or_w16 w1 (
   mk_word16 (or_b8 b1 (or_b8 b3 b5)) (or_b8 b2 (or_b8 b4 b6)));
  nrewrite < (associative_orb8 b1 b3 b5);
  nrewrite < (associative_orb8 b2 b4 b6);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_xorw16 : symmetricT word16 word16 xor_w16.
@@ -118,7 +118,7 @@ nlemma symmetric_xorw16 : symmetricT word16 word16 xor_w16.
  nchange with ((mk_word16 (xor_b8 b3 b1) (xor_b8 b4 b2)) = (mk_word16 (xor_b8 b1 b3) (xor_b8 b2 b4)));
  nrewrite > (symmetric_xorb8 b1 b3);
  nrewrite > (symmetric_xorb8 b2 b4);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma associative_xorw16 : ∀w1,w2,w3.(xor_w16 (xor_w16 w1 w2) w3) = (xor_w16 w1 (xor_w16 w2 w3)).
@@ -133,7 +133,7 @@ nlemma associative_xorw16 : ∀w1,w2,w3.(xor_w16 (xor_w16 w1 w2) w3) = (xor_w16
   mk_word16 (xor_b8 b1 (xor_b8 b3 b5)) (xor_b8 b2 (xor_b8 b4 b6)));
  nrewrite < (associative_xorb8 b1 b3 b5);
  nrewrite < (associative_xorb8 b2 b4 b6);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_plusw16_dc_dc : ∀w1,w2,c.plus_w16_dc_dc w1 w2 c = plus_w16_dc_dc w2 w1 c.
@@ -145,20 +145,20 @@ nlemma symmetric_plusw16_dc_dc : ∀w1,w2,c.plus_w16_dc_dc w1 w2 c = plus_w16_dc
  nchange with (
   match plus_b8_dc_dc b2 b4 c with
    [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with
-    [ pair h c' ⇒ pair ?? 〈h:l〉 c' ]] =
+    [ pair h c' ⇒ pair … 〈h:l〉 c' ]] =
   match plus_b8_dc_dc b4 b2 c with
    [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with
-    [ pair h c' ⇒ pair ?? 〈h:l〉 c' ]]);
+    [ pair h c' ⇒ pair … 〈h:l〉 c' ]]);
  nrewrite > (symmetric_plusb8_dc_dc b4 b2 c);
  ncases (plus_b8_dc_dc b2 b4 c);
  #b5; #c1;
  nchange with (
   match plus_b8_dc_dc b1 b3 c1 with
-   [ pair h c' ⇒ pair ?? 〈h:b5〉 c' ] =
+   [ pair h c' ⇒ pair … 〈h:b5〉 c' ] =
   match plus_b8_dc_dc b3 b1 c1 with
-   [ pair h c' ⇒ pair ?? 〈h:b5〉 c' ]);
+   [ pair h c' ⇒ pair … 〈h:b5〉 c' ]);
  nrewrite > (symmetric_plusb8_dc_dc b1 b3 c1);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_plusw16_dc_d : ∀w1,w2,c.plus_w16_dc_d w1 w2 c = plus_w16_dc_d w2 w1 c.
@@ -177,7 +177,7 @@ nlemma symmetric_plusw16_dc_d : ∀w1,w2,c.plus_w16_dc_d w1 w2 c = plus_w16_dc_d
  #b5; #c1;
  nchange with (〈plus_b8_dc_d b1 b3 c1:b5〉 = 〈plus_b8_dc_d b3 b1 c1:b5〉);
  nrewrite > (symmetric_plusb8_dc_d b1 b3 c1);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_plusw16_dc_c : ∀w1,w2,c.plus_w16_dc_c w1 w2 c = plus_w16_dc_c w2 w1 c.
@@ -191,7 +191,7 @@ nlemma symmetric_plusw16_dc_c : ∀w1,w2,c.plus_w16_dc_c w1 w2 c = plus_w16_dc_c
   plus_b8_dc_c b3 b1 (plus_b8_dc_c b4 b2 c));
  nrewrite > (symmetric_plusb8_dc_c b4 b2 c);
  nrewrite > (symmetric_plusb8_dc_c b3 b1 (plus_b8_dc_c b2 b4 c));
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_plusw16_d_dc : ∀w1,w2.plus_w16_d_dc w1 w2 = plus_w16_d_dc w2 w1.
@@ -203,20 +203,20 @@ nlemma symmetric_plusw16_d_dc : ∀w1,w2.plus_w16_d_dc w1 w2 = plus_w16_d_dc w2
  nchange with (
   match plus_b8_d_dc b2 b4 with
    [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with
-    [ pair h c' ⇒ pair ?? 〈h:l〉 c' ]] =
+    [ pair h c' ⇒ pair … 〈h:l〉 c' ]] =
   match plus_b8_d_dc b4 b2 with
    [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with
-    [ pair h c' ⇒ pair ?? 〈h:l〉 c' ]]);
+    [ pair h c' ⇒ pair … 〈h:l〉 c' ]]);
  nrewrite > (symmetric_plusb8_d_dc b4 b2);
  ncases (plus_b8_d_dc b2 b4);
  #b5; #c;
  nchange with (
   match plus_b8_dc_dc b1 b3 c with
-   [ pair h c' ⇒ pair ?? 〈h:b5〉 c' ] =
+   [ pair h c' ⇒ pair … 〈h:b5〉 c' ] =
   match plus_b8_dc_dc b3 b1 c with
-   [ pair h c' ⇒ pair ?? 〈h:b5〉 c' ]);
+   [ pair h c' ⇒ pair … 〈h:b5〉 c' ]);
  nrewrite > (symmetric_plusb8_dc_dc b1 b3 c);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_plusw16_d_d : ∀w1,w2.plus_w16_d_d w1 w2 = plus_w16_d_d w2 w1.
@@ -235,7 +235,7 @@ nlemma symmetric_plusw16_d_d : ∀w1,w2.plus_w16_d_d w1 w2 = plus_w16_d_d w2 w1.
  #b5; #c;
  nchange with (〈plus_b8_dc_d b1 b3 c:b5〉 = 〈plus_b8_dc_d b3 b1 c:b5〉);
  nrewrite > (symmetric_plusb8_dc_d b1 b3 c);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_plusw16_d_c : ∀w1,w2.plus_w16_d_c w1 w2 = plus_w16_d_c w2 w1.
@@ -249,7 +249,7 @@ nlemma symmetric_plusw16_d_c : ∀w1,w2.plus_w16_d_c w1 w2 = plus_w16_d_c w2 w1.
   plus_b8_dc_c b3 b1 (plus_b8_d_c b4 b2));
  nrewrite > (symmetric_plusb8_d_c b4 b2);
  nrewrite > (symmetric_plusb8_dc_c b3 b1 (plus_b8_d_c b2 b4));
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_mulb8 : symmetricT byte8 word16 mul_b8.
@@ -296,7 +296,7 @@ nlemma symmetric_mulb8 : symmetricT byte8 word16 mul_b8.
  nchange with ((plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,e7〉:〈e8,x0〉〉 〈〈x0,e9〉:〈e10,x0〉〉) 〈〈e11,e12〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉) =
   (plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,e9〉:〈e10,x0〉〉 〈〈x0,e7〉:〈e8,x0〉〉) 〈〈e11,e12〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉));
  nrewrite > (symmetric_plusw16_d_d 〈〈x0,e7〉:〈e8,x0〉〉 〈〈x0,e9〉:〈e10,x0〉〉);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma eqw16_to_eq : ∀w1,w2:word16.(eq_w16 w1 w2 = true) → (w1 = w2).
@@ -306,9 +306,9 @@ nlemma eqw16_to_eq : ∀w1,w2:word16.(eq_w16 w1 w2 = true) → (w1 = w2).
  #b1; #b2; #b3; #b4;
  nchange in ⊢ (% → ?) with (((eq_b8 b3 b1)⊗(eq_b8 b4 b2)) = true);
  #H;
- nrewrite < (eqb8_to_eq ?? (andb_true_true_l ?? H));
- nrewrite < (eqb8_to_eq ?? (andb_true_true_r ?? H));
- napply (refl_eq ??).
+ nrewrite < (eqb8_to_eq … (andb_true_true_l … H));
+ nrewrite < (eqb8_to_eq … (andb_true_true_r … H));
+ napply refl_eq.
 nqed.
 
 nlemma eq_to_eqw16 : ∀w1,w2.w1 = w2 → eq_w16 w1 w2 = true.
@@ -317,11 +317,11 @@ nlemma eq_to_eqw16 : ∀w1,w2.w1 = w2 → eq_w16 w1 w2 = true.
  nelim w2;
  #b1; #b2; #b3; #b4;
  #H;
- nrewrite < (word16_destruct_1 ???? H);
- nrewrite < (word16_destruct_2 ???? H);
+ nrewrite < (word16_destruct_1 … H);
+ nrewrite < (word16_destruct_2 … H);
  nchange with (((eq_b8 b3 b3)⊗(eq_b8 b4 b4)) = true);
- nrewrite > (eq_to_eqb8 b3 b3 (refl_eq ??));
- nrewrite > (eq_to_eqb8 b4 b4 (refl_eq ??)); 
+ nrewrite > (eq_to_eqb8 b3 b3 (refl_eq …));
+ nrewrite > (eq_to_eqb8 b4 b4 (refl_eq …)); 
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.