2 (* congettura, come si fa? *)
3 include "num/exadecim.ma".
4 include "num/exadecim_lemmas.ma".
6 nlemma decidable_ex_aux1 : ∀x.∀H:x0 = x.(x0 = x) ∨ (x0 ≠ x).
8 ##[ ##1: #H; napply (or_introl … H)
9 ##| ##*: #H; nelim (exadecim_destruct … H)
12 nlemma decidable_ex0 : ∀x:exadecim.decidable (x0 = x).
16 napply (Or_ind (x0=x) (x0≠x) ? ? …);
17 ##[ ##1: napply (or_introl (x0 = x0) (x0 ≠ x0) (refl_eq …))
23 ##[ ##1: napply (or_introl (? = ?) (? ≠ ?) (refl_eq …))
26 (*include "utility/utility.ma".
28 nlemma fold_right_neList2_aux3 :
29 \forall T. \forall h,h',t,t'.len_neList T (h§§t) = len_neList T (h'§§t') → len_neList T t = len_neList T t'.
31 napply (ne_list_ind T ??? t);
32 napply (ne_list_ind T ??? t');
33 ##[ ##1: nnormalize; #x; #y; #H; napply (refl_eq ??)
34 ##| ##2: #a; #l'; #H; #x; #H1;
35 nchange in H1:(%) with ((S (len_neList T «£x»)) = (S (len_neList T (a§§l'))));
36 nrewrite > (nat_destruct_S_S ?? H1);
38 ##| ##3: #x; #a; #l'; #H; #H1;
39 nchange in H1:(%) with ((S (len_neList T (a§§l')))= (S (len_neList T «£x»)));
40 nrewrite > (nat_destruct_S_S ?? H1);
42 ##| ##4: #a; #l; #H; #a1; #l1; #H1; #H2;
43 (* sarebbe nchange in H2:(%) with ((S (len_neList T (a1§§l1))) = (S (len_neList T (a§§l)))); *)
44 (* ma fa passare il seguente errato ... *)
45 nchange in H2:(%) with ((S (len_neList T (a§§l1))) = (S (len_neList T (a§§l))));
48 (*include "freescale/byte8_lemmas.ma".
50 nlemma associative_plusb8_aux
51 : \forall e1,e2,e3,e4.
52 match plus_ex_d_dc e2 e4 with
53 [ pair l c ⇒ 〈plus_ex_dc_d e1 e3 c,l〉 ] =
54 〈plus_ex_dc_d e1 e3 (snd ?? (plus_ex_d_dc e2 e4)),(fst ?? (plus_ex_d_dc e2 e4))〉.
56 (* anche qui appare un T1 *)
57 ncases (plus_ex_d_dc e2 e4);
62 nlemma associative_plusb8
63 : \forall b1,b2,b3.(plus_b8_d_d (plus_b8_d_d b1 b2) b3) = (plus_b8_d_d b1 (plus_b8_d_d b2 b3)).
64 #b1; ncases b1; #e1; #e2;
65 #b2; ncases b2; #e3; #e4;
66 #b3; ncases b3; #e5; #e6;
68 (* perche' volendo posso introdurre anche 2 premesse diverse con lo stesso nome? tipo #e2; #e2 *)
71 match plus_ex_d_dc (b8l (match plus_ex_d_dc e2 e4 with
72 [ pair l1 c1 ⇒ 〈plus_ex_dc_d e1 e3 c1,l1〉 ])) e6 with
73 [ pair l2 c2 ⇒ 〈plus_ex_dc_d (b8h (match plus_ex_d_dc e2 e4 with
74 [ pair l3 c3 ⇒ 〈plus_ex_dc_d e1 e3 c3,l3〉 ])) e5 c2,l2〉 ] =
75 match plus_ex_d_dc e2 (b8l (match plus_ex_d_dc e4 e6 with
76 [ pair l4 c4 ⇒ 〈plus_ex_dc_d e3 e5 c4,l4〉 ])) with
77 [ pair l5 c5 ⇒ 〈plus_ex_dc_d e1 (b8h (match plus_ex_d_dc e4 e6 with
78 [ pair l6 c6 ⇒ 〈plus_ex_dc_d e3 e5 c6,l6〉 ])) c5,l5〉 ]);
80 (* gia' qua ci sono T1, T2 che appaiono dal nulla al posto delle variabili *)
82 nrewrite > (associative_plusb8_aux e1 e2 e3 e4);
83 nrewrite > (associative_plusb8_aux e3 e4 e5 e6);
84 nrewrite > (plusex_d_dc_to_d_c e2 e4);
85 nrewrite > (plusex_d_dc_to_d_d e2 e4);
86 nrewrite > (plusex_d_dc_to_d_c e4 e6);
88 (* nel visualizzatore era (snd ?? (plus_ex_d_dc e5 T2)) ma ha accettato la versione corretta *)
90 nrewrite > (plusex_d_dc_to_d_d e4 e6);
95 (*include "compiler/ast_type_lemmas.ma".
97 nlemma symmetric_eqasttype_aux1
98 : ∀x1,x2,y2.eq_nat (len_neList ast_type («£x1»)) (len_neList ast_type (x2§§y2)) = false.
99 #x1; #x2; #y2; ncases y2; nnormalize;
100 ##[ ##1: #t; napply (refl_eq ??)
101 ##| ##2: #t; #l; napply (refl_eq ??)
105 nlemma symmetric_eqasttype_aux2
106 : ∀x1,y1,x2.eq_nat (len_neList ast_type (x1§§y1)) (len_neList ast_type («£x2»)) = false.
107 #x1; #y1; #x2; ncases y1; nnormalize;
108 ##[ ##1: #t; napply (refl_eq ??)
109 ##| ##2: #t; #l; napply (refl_eq ??)
113 ndefinition symmetric_eqasttype_aux3 ≝
114 λnelSubType1,nelSubType2:ne_list ast_type.
115 match eq_nat (len_neList ast_type nelSubType1) (len_neList ast_type nelSubType2)
116 return λx.eq_nat (len_neList ast_type nelSubType1) (len_neList ast_type nelSubType2) = x → bool
118 [ true ⇒ λp:(eq_nat (len_neList ast_type nelSubType1) (len_neList ast_type nelSubType2) = true).
119 fold_right_neList2 ?? (λx1,x2,acc.(eq_ast_type x1 x2)⊗acc)
120 true nelSubType1 nelSubType2
121 (eqnat_to_eq (len_neList ? nelSubType1) (len_neList ? nelSubType2) p)
122 | false ⇒ λp:(eq_nat (len_neList ast_type nelSubType1) (len_neList ast_type nelSubType2) = false).false
123 ] (refl_eq ? (eq_nat (len_neList ast_type nelSubType1) (len_neList ast_type nelSubType2))).
125 nlemma symmetric_eqasttype : symmetricT ast_type bool eq_ast_type.
127 napply (ast_type_ind ????? t1);
128 ##[ ##1: #b1; #t2; ncases t2;
129 ##[ ##1: #b2; nchange with ((eq_ast_base_type b1 b2) = (eq_ast_base_type b2 b1));
130 nrewrite > (symmetric_eqastbasetype b1 b2);
132 ##| ##2: #tt; #n; nnormalize; napply (refl_eq ??)
133 ##| ##3: #l; nnormalize; napply (refl_eq ??)
135 ##| ##2: #tt1; #n1; #H; #t2; ncases t2;
136 ##[ ##2: #tt2; #n2; nchange with (((eq_ast_type tt1 tt2)⊗(eq_nat n1 n2)) = ((eq_ast_type tt2 tt1)⊗(eq_nat n2 n1)));
138 nrewrite > (symmetric_eqnat n1 n2);
140 ##| ##1: #b2; nnormalize; napply (refl_eq ??)
141 ##| ##3: #l; nnormalize; napply (refl_eq ??)
143 ##| ##3: #tt1; #H; #t2; ncases t2;
144 ##[ ##3: #l; ncases l;
145 ##[ ##1: #tt2; nnormalize; nrewrite > (H tt2); napply (refl_eq ??)
148 (match eq_nat (len_neList ast_type «£tt1») (len_neList ast_type (tt2§§l1))
149 return λx.eq_nat (len_neList ast_type «£tt1») (len_neList ast_type (tt2§§l1)) = x → bool
151 [ true ⇒ λp:(eq_nat (len_neList ast_type «£tt1») (len_neList ast_type (tt2§§l1)) = true).
152 fold_right_neList2 ?? (λx1,x2,acc.(eq_ast_type x1 x2)⊗acc)
153 true «£tt1» (tt2§§l1)
154 (eqnat_to_eq (len_neList ? «£tt1») (len_neList ? (tt2§§l1)) p)
155 | false ⇒ λp:(eq_nat (len_neList ast_type «£tt1») (len_neList ast_type (tt2§§l1)) = false).false
156 ] (refl_eq ? (eq_nat (len_neList ast_type «£tt1») (len_neList ast_type (tt2§§l1))))) = ?);
158 (* eseguendo questa sequenza e' ok *)
159 nrewrite > (symmetric_eqasttype_aux1 tt1 tt2 l1);
161 false = (match eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1»)
162 return λx.eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = x → bool
164 [ true ⇒ λp:(eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = true).
165 fold_right_neList2 ?? (λx1,x2,acc.(eq_ast_type x1 x2)⊗acc)
166 true (tt2§§l1) «£tt1»
167 (eqnat_to_eq (len_neList ? (tt2§§l1)) (len_neList ? «£tt1») p)
168 | false ⇒ λp:(eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = false).false
169 ] (refl_eq ? (eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1»)))));
170 nrewrite > (symmetric_eqasttype_aux2 tt2 l1 tt1);
173 (* se commentiamo invece la prima sequenza ed eseguiamo questa *)
174 (* come e' possibile che rigetti la seconda rewrite? *)
176 ? = (match eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1»)
177 return λx.eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = x → bool
179 [ true ⇒ λp:(eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = true).
180 fold_right_neList2 ?? (λx1,x2,acc.(eq_ast_type x1 x2)⊗acc)
181 true (tt2§§l1) «£tt1»
182 (eqnat_to_eq (len_neList ? (tt2§§l1)) (len_neList ? «£tt1») p)
183 | false ⇒ λp:(eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = false).false
184 ] (refl_eq ? (eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1»)))));
185 nrewrite > (symmetric_eqasttype_aux1 tt1 tt2 l1);
186 nrewrite > (symmetric_eqasttype_aux2 tt2 l1 tt1);