1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "num/byte8.ma".
29 nrecord word24 : Type ≝
37 notation "〈x;y;z〉" non associative with precedence 80
38 for @{ 'mk_word24 $x $y $z }.
39 interpretation "mk_word24" 'mk_word24 x y z = (mk_word24 x y z).
43 λw1,w2.(eqc ? (w24x w1) (w24x w2)) ⊗
44 (eqc ? (w24h w1) (w24h w2)) ⊗
45 (eqc ? (w24l w1) (w24l w2)).
47 nlemma word24_destruct_1 :
49 mk_word24 x1 y1 z1 = mk_word24 x2 y2 z2 → x1 = x2.
50 #x1; #x2; #y1; #y2; #z1; #z2; #H;
51 nchange with (match mk_word24 x2 y2 z2 with [ mk_word24 a _ _ ⇒ x1 = a ]);
57 nlemma word24_destruct_2 :
59 mk_word24 x1 y1 z1 = mk_word24 x2 y2 z2 → y1 = y2.
60 #x1; #x2; #y1; #y2; #z1; #z2; #H;
61 nchange with (match mk_word24 x2 y2 z2 with [ mk_word24 _ a _ ⇒ y1 = a ]);
67 nlemma word24_destruct_3 :
69 mk_word24 x1 y1 z1 = mk_word24 x2 y2 z2 → z1 = z2.
70 #x1; #x2; #y1; #y2; #z1; #z2; #H;
71 nchange with (match mk_word24 x2 y2 z2 with [ mk_word24 _ _ a ⇒ z1 = a ]);
77 nlemma symmetric_eqw24 : symmetricT word24 bool eq_w24.
78 #b1; nelim b1; #e1; #e2; #e3;
79 #b2; nelim b2; #e4; #e5; #e6;
80 nchange with (((eqc ? e1 e4)⊗(eqc ? e2 e5)⊗(eqc ? e3 e6)) = ((eqc ? e4 e1)⊗(eqc ? e5 e2)⊗(eqc ? e6 e3)));
81 nrewrite > (symmetric_eqc ? e1 e4);
82 nrewrite > (symmetric_eqc ? e2 e5);
83 nrewrite > (symmetric_eqc ? e3 e6);
87 nlemma eqw24_to_eq : ∀b1,b2.(eq_w24 b1 b2 = true) → (b1 = b2).
88 #b1; nelim b1; #e1; #e2; #e3;
89 #b2; nelim b2; #e4; #e5; #e6;
90 nchange in ⊢ (% → ?) with (((eqc ? e1 e4)⊗(eqc ? e2 e5)⊗(eqc ? e3 e6)) = true);
92 nrewrite < (eqc_to_eq … (andb_true_true_r … H));
93 nrewrite < (eqc_to_eq … (andb_true_true_r … (andb_true_true_l … H)));
94 nrewrite < (eqc_to_eq … (andb_true_true_l … (andb_true_true_l … H)));
98 nlemma eq_to_eqw24 : ∀b1,b2.(b1 = b2) → (eq_w24 b1 b2 = true).
99 #b1; nelim b1; #e1; #e2; #e3;
100 #b2; nelim b2; #e4; #e5; #e6;
102 nchange with (((eqc ? e1 e4)⊗(eqc ? e2 e5)⊗(eqc ? e3 e6)) = true);
103 nrewrite < (word24_destruct_1 … H);
104 nrewrite < (word24_destruct_2 … H);
105 nrewrite < (word24_destruct_3 … H);
106 nrewrite > (eq_to_eqc ? e1 e1 (refl_eq …));
107 nrewrite > (eq_to_eqc ? e2 e2 (refl_eq …));
108 nrewrite > (eq_to_eqc ? e3 e3 (refl_eq …));
113 nlemma decidable_w24_aux1 :
114 ∀e1,e2,e3,e4,e5,e6.e1 ≠ e4 → (mk_word24 e1 e2 e3) ≠ (mk_word24 e4 e5 e6).
115 #e1; #e2; #e3; #e4; #e5; #e6;
117 napply (H (word24_destruct_1 … H1)).
120 nlemma decidable_w24_aux2 :
121 ∀e1,e2,e3,e4,e5,e6.e2 ≠ e5 → (mk_word24 e1 e2 e3) ≠ (mk_word24 e4 e5 e6).
122 #e1; #e2; #e3; #e4; #e5; #e6;
124 napply (H (word24_destruct_2 … H1)).
127 nlemma decidable_w24_aux3 :
128 ∀e1,e2,e3,e4,e5,e6.e3 ≠ e6 → (mk_word24 e1 e2 e3) ≠ (mk_word24 e4 e5 e6).
129 #e1; #e2; #e3; #e4; #e5; #e6;
131 napply (H (word24_destruct_3 … H1)).
134 nlemma decidable_w24 : ∀b1,b2:word24.(decidable (b1 = b2)).
135 #b1; nelim b1; #e1; #e2; #e3;
136 #b2; nelim b2; #e4; #e5; #e6;
138 napply (or2_elim (e1 = e4) (e1 ≠ e4) ? (decidable_c ? e1 e4) …);
139 ##[ ##2: #H; napply (or2_intro2 … (decidable_w24_aux1 e1 e2 e3 e4 e5 e6 H))
140 ##| ##1: #H; napply (or2_elim (e2 = e5) (e2 ≠ e5) ? (decidable_c ? e2 e5) …);
141 ##[ ##2: #H1; napply (or2_intro2 … (decidable_w24_aux2 e1 e2 e3 e4 e5 e6 H1))
142 ##| ##1: #H1; napply (or2_elim (e3 = e6) (e3 ≠ e6) ? (decidable_c ? e3 e6) …);
143 ##[ ##2: #H2; napply (or2_intro2 … (decidable_w24_aux3 e1 e2 e3 e4 e5 e6 H2))
144 ##| ##1: #H2; nrewrite > H; nrewrite > H1; nrewrite > H2;
145 napply (or2_intro1 … (refl_eq ? (mk_word24 e4 e5 e6)))
151 nlemma neqw24_to_neq : ∀b1,b2.(eq_w24 b1 b2 = false) → (b1 ≠ b2).
152 #b1; nelim b1; #e1; #e2; #e3;
153 #b2; nelim b2; #e4; #e5; #e6;
155 nchange in H:(%) with (((eqc ? e1 e4)⊗(eqc ? e2 e5)⊗(eqc ? e3 e6)) = false);
157 nrewrite > (word24_destruct_1 … H1) in H:(%);
158 nrewrite > (word24_destruct_2 … H1);
159 nrewrite > (word24_destruct_3 … H1);
160 nrewrite > (eq_to_eqc ? e4 e4 (refl_eq …));
161 nrewrite > (eq_to_eqc ? e5 e5 (refl_eq …));
162 nrewrite > (eq_to_eqc ? e6 e6 (refl_eq …));
166 nlemma word24_destruct :
168 ((mk_word24 e1 e2 e3) ≠ (mk_word24 e4 e5 e6)) →
169 (Or3 (e1 ≠ e4) (e2 ≠ e5) (e3 ≠ e6)).
170 #e1; #e2; #e3; #e4; #e5; #e6;
172 napply (or2_elim (e1 = e4) (e1 ≠ e4) ? (decidable_c ? e1 e4) …);
173 ##[ ##2: #H1; napply (or3_intro1 … H1)
174 ##| ##1: #H1; napply (or2_elim (e2 = e5) (e2 ≠ e5) ? (decidable_c ? e2 e5) …);
175 ##[ ##2: #H2; napply (or3_intro2 … H2)
176 ##| ##1: #H2; napply (or2_elim (e3 = e6) (e3 ≠ e6) ? (decidable_c ? e3 e6) …);
177 ##[ ##2: #H3; napply (or3_intro3 … H3)
178 ##| ##1: #H3; nrewrite > H1 in H:(%);
179 nrewrite > H2; nrewrite > H3;
180 #H; nelim (H (refl_eq …))
186 nlemma neq_to_neqw24 : ∀b1,b2.((b1 ≠ b2) → (eq_w24 b1 b2 = false)).
187 #b1; nelim b1; #e1; #e2; #e3;
188 #b2; nelim b2; #e4; #e5; #e6;
189 #H; nchange with (((eqc ? e1 e4)⊗(eqc ? e2 e5)⊗(eqc ? e3 e6)) = false);
190 napply (or3_elim (e1 ≠ e4) (e2 ≠ e5) (e3 ≠ e6) ? (word24_destruct e1 e2 e3 e4 e5 e6 … H) …);
191 ##[ ##1: #H1; nrewrite > (neq_to_neqc ? e1 e4 H1); nnormalize; napply refl_eq
192 ##| ##2: #H1; nrewrite > (neq_to_neqc ? e2 e5 H1);
193 nrewrite > (symmetric_andbool (eqc ? e1 e4) …);
194 nnormalize; napply refl_eq
195 ##| ##3: #H1; nrewrite > (neq_to_neqc ? e3 e6 H1);
196 nrewrite > (symmetric_andbool ((eqc ? e1 e4)⊗(eqc ? e2 e5)) …);
197 nnormalize; napply refl_eq
201 nlemma word24_is_comparable : comparable.
203 ##[ napply (mk_word24 (zeroc ?) (zeroc ?) (zeroc ?))
204 ##| napply (λP.forallc ?
207 (λl.P (mk_word24 x h l)))))
209 ##| napply eqw24_to_eq
210 ##| napply eq_to_eqw24
211 ##| napply neqw24_to_neq
212 ##| napply neq_to_neqw24
213 ##| napply decidable_w24
214 ##| napply symmetric_eqw24
218 unification hint 0 ≔ ⊢ carr word24_is_comparable ≡ word24.