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 ndefinition succ_w24 ≝
48 λw.match eqc ? (predc ? (zeroc ?)) (w24l w) with
49 [ true ⇒ match eqc ? (predc ? (zeroc ?)) (w24h w) with
50 [ true ⇒ 〈(succc ? (w24x w));(succc ? (w24h w));(succc ? (w24l w))〉
51 | false ⇒ 〈(w24x w);(succc ? (w24h w));(succc ? (w24l w))〉 ]
52 | false ⇒ 〈(w24x w);(w24h w);(succc ? (w24l w))〉 ].
54 nlemma word24_destruct_1 :
56 mk_word24 x1 y1 z1 = mk_word24 x2 y2 z2 → x1 = x2.
57 #x1; #x2; #y1; #y2; #z1; #z2; #H;
58 nchange with (match mk_word24 x2 y2 z2 with [ mk_word24 a _ _ ⇒ x1 = a ]);
64 nlemma word24_destruct_2 :
66 mk_word24 x1 y1 z1 = mk_word24 x2 y2 z2 → y1 = y2.
67 #x1; #x2; #y1; #y2; #z1; #z2; #H;
68 nchange with (match mk_word24 x2 y2 z2 with [ mk_word24 _ a _ ⇒ y1 = a ]);
74 nlemma word24_destruct_3 :
76 mk_word24 x1 y1 z1 = mk_word24 x2 y2 z2 → z1 = z2.
77 #x1; #x2; #y1; #y2; #z1; #z2; #H;
78 nchange with (match mk_word24 x2 y2 z2 with [ mk_word24 _ _ a ⇒ z1 = a ]);
84 nlemma symmetric_eqw24 : symmetricT word24 bool eq_w24.
85 #b1; nelim b1; #e1; #e2; #e3;
86 #b2; nelim b2; #e4; #e5; #e6;
87 nchange with (((eqc ? e1 e4)⊗(eqc ? e2 e5)⊗(eqc ? e3 e6)) = ((eqc ? e4 e1)⊗(eqc ? e5 e2)⊗(eqc ? e6 e3)));
88 nrewrite > (symmetric_eqc ? e1 e4);
89 nrewrite > (symmetric_eqc ? e2 e5);
90 nrewrite > (symmetric_eqc ? e3 e6);
94 nlemma eqw24_to_eq : ∀b1,b2.(eq_w24 b1 b2 = true) → (b1 = b2).
95 #b1; nelim b1; #e1; #e2; #e3;
96 #b2; nelim b2; #e4; #e5; #e6;
97 nchange in ⊢ (% → ?) with (((eqc ? e1 e4)⊗(eqc ? e2 e5)⊗(eqc ? e3 e6)) = true);
99 nrewrite < (eqc_to_eq … (andb_true_true_r … H));
100 nrewrite < (eqc_to_eq … (andb_true_true_r … (andb_true_true_l … H)));
101 nrewrite < (eqc_to_eq … (andb_true_true_l … (andb_true_true_l … H)));
105 nlemma eq_to_eqw24 : ∀b1,b2.(b1 = b2) → (eq_w24 b1 b2 = true).
106 #b1; nelim b1; #e1; #e2; #e3;
107 #b2; nelim b2; #e4; #e5; #e6;
109 nchange with (((eqc ? e1 e4)⊗(eqc ? e2 e5)⊗(eqc ? e3 e6)) = true);
110 nrewrite < (word24_destruct_1 … H);
111 nrewrite < (word24_destruct_2 … H);
112 nrewrite < (word24_destruct_3 … H);
113 nrewrite > (eq_to_eqc ? e1 e1 (refl_eq …));
114 nrewrite > (eq_to_eqc ? e2 e2 (refl_eq …));
115 nrewrite > (eq_to_eqc ? e3 e3 (refl_eq …));
120 nlemma decidable_w24_aux1 :
121 ∀e1,e2,e3,e4,e5,e6.e1 ≠ e4 → (mk_word24 e1 e2 e3) ≠ (mk_word24 e4 e5 e6).
122 #e1; #e2; #e3; #e4; #e5; #e6;
124 napply (H (word24_destruct_1 … H1)).
127 nlemma decidable_w24_aux2 :
128 ∀e1,e2,e3,e4,e5,e6.e2 ≠ e5 → (mk_word24 e1 e2 e3) ≠ (mk_word24 e4 e5 e6).
129 #e1; #e2; #e3; #e4; #e5; #e6;
131 napply (H (word24_destruct_2 … H1)).
134 nlemma decidable_w24_aux3 :
135 ∀e1,e2,e3,e4,e5,e6.e3 ≠ e6 → (mk_word24 e1 e2 e3) ≠ (mk_word24 e4 e5 e6).
136 #e1; #e2; #e3; #e4; #e5; #e6;
138 napply (H (word24_destruct_3 … H1)).
141 nlemma decidable_w24 : ∀b1,b2:word24.(decidable (b1 = b2)).
142 #b1; nelim b1; #e1; #e2; #e3;
143 #b2; nelim b2; #e4; #e5; #e6;
145 napply (or2_elim (e1 = e4) (e1 ≠ e4) ? (decidable_c ? e1 e4) …);
146 ##[ ##2: #H; napply (or2_intro2 … (decidable_w24_aux1 e1 e2 e3 e4 e5 e6 H))
147 ##| ##1: #H; napply (or2_elim (e2 = e5) (e2 ≠ e5) ? (decidable_c ? e2 e5) …);
148 ##[ ##2: #H1; napply (or2_intro2 … (decidable_w24_aux2 e1 e2 e3 e4 e5 e6 H1))
149 ##| ##1: #H1; napply (or2_elim (e3 = e6) (e3 ≠ e6) ? (decidable_c ? e3 e6) …);
150 ##[ ##2: #H2; napply (or2_intro2 … (decidable_w24_aux3 e1 e2 e3 e4 e5 e6 H2))
151 ##| ##1: #H2; nrewrite > H; nrewrite > H1; nrewrite > H2;
152 napply (or2_intro1 … (refl_eq ? (mk_word24 e4 e5 e6)))
158 nlemma neqw24_to_neq : ∀b1,b2.(eq_w24 b1 b2 = false) → (b1 ≠ b2).
159 #b1; nelim b1; #e1; #e2; #e3;
160 #b2; nelim b2; #e4; #e5; #e6;
162 nchange in H:(%) with (((eqc ? e1 e4)⊗(eqc ? e2 e5)⊗(eqc ? e3 e6)) = false);
164 nrewrite > (word24_destruct_1 … H1) in H:(%);
165 nrewrite > (word24_destruct_2 … H1);
166 nrewrite > (word24_destruct_3 … H1);
167 nrewrite > (eq_to_eqc ? e4 e4 (refl_eq …));
168 nrewrite > (eq_to_eqc ? e5 e5 (refl_eq …));
169 nrewrite > (eq_to_eqc ? e6 e6 (refl_eq …));
173 nlemma word24_destruct :
175 ((mk_word24 e1 e2 e3) ≠ (mk_word24 e4 e5 e6)) →
176 (Or3 (e1 ≠ e4) (e2 ≠ e5) (e3 ≠ e6)).
177 #e1; #e2; #e3; #e4; #e5; #e6;
179 napply (or2_elim (e1 = e4) (e1 ≠ e4) ? (decidable_c ? e1 e4) …);
180 ##[ ##2: #H1; napply (or3_intro1 … H1)
181 ##| ##1: #H1; napply (or2_elim (e2 = e5) (e2 ≠ e5) ? (decidable_c ? e2 e5) …);
182 ##[ ##2: #H2; napply (or3_intro2 … H2)
183 ##| ##1: #H2; napply (or2_elim (e3 = e6) (e3 ≠ e6) ? (decidable_c ? e3 e6) …);
184 ##[ ##2: #H3; napply (or3_intro3 … H3)
185 ##| ##1: #H3; nrewrite > H1 in H:(%);
186 nrewrite > H2; nrewrite > H3;
187 #H; nelim (H (refl_eq …))
193 nlemma neq_to_neqw24 : ∀b1,b2.((b1 ≠ b2) → (eq_w24 b1 b2 = false)).
194 #b1; nelim b1; #e1; #e2; #e3;
195 #b2; nelim b2; #e4; #e5; #e6;
196 #H; nchange with (((eqc ? e1 e4)⊗(eqc ? e2 e5)⊗(eqc ? e3 e6)) = false);
197 napply (or3_elim (e1 ≠ e4) (e2 ≠ e5) (e3 ≠ e6) ? (word24_destruct e1 e2 e3 e4 e5 e6 … H) …);
198 ##[ ##1: #H1; nrewrite > (neq_to_neqc ? e1 e4 H1); nnormalize; napply refl_eq
199 ##| ##2: #H1; nrewrite > (neq_to_neqc ? e2 e5 H1);
200 nrewrite > (symmetric_andbool (eqc ? e1 e4) …);
201 nnormalize; napply refl_eq
202 ##| ##3: #H1; nrewrite > (neq_to_neqc ? e3 e6 H1);
203 nrewrite > (symmetric_andbool ((eqc ? e1 e4)⊗(eqc ? e2 e5)) …);
204 nnormalize; napply refl_eq
208 nlemma word24_is_comparable : comparable.
210 ##[ napply (mk_word24 (zeroc ?) (zeroc ?) (zeroc ?))
211 ##| napply (λP.forallc ?
214 (λl.P (mk_word24 x h l)))))
216 ##| napply eqw24_to_eq
217 ##| napply eq_to_eqw24
218 ##| napply neqw24_to_neq
219 ##| napply neq_to_neqw24
220 ##| napply decidable_w24
221 ##| napply symmetric_eqw24
225 unification hint 0 ≔ ⊢ carr word24_is_comparable ≡ word24.