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 :
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.
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.
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)).
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.
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)).
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.
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)).
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.
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.
#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.
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.
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.
#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.
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.
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).
#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.
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.