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: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "utility/utility.ma".
29 nlemma nelist_destruct_nil_nil : ∀T.∀x1,x2:T.ne_nil T x1 = ne_nil T x2 → x1 = x2.
31 nchange with (match ne_nil T x2 with [ ne_cons _ _ ⇒ False | ne_nil a ⇒ x1 = a ]);
37 nlemma nelist_destruct_cons_cons_1 : ∀T.∀x1,x2:T.∀y1,y2:ne_list T.ne_cons T x1 y1 = ne_cons T x2 y2 → x1 = x2.
38 #T; #x1; #x2; #y1; #y2; #H;
39 nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ False | ne_cons a _ ⇒ x1 = a ]);
45 nlemma nelist_destruct_cons_cons_2 : ∀T.∀x1,x2:T.∀y1,y2:ne_list T.ne_cons T x1 y1 = ne_cons T x2 y2 → y1 = y2.
46 #T; #x1; #x2; #y1; #y2; #H;
47 nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ False | ne_cons _ b ⇒ y1 = b ]);
53 nlemma nelist_destruct_cons_nil : ∀T.∀x1,x2:T.∀y1:ne_list T.ne_cons T x1 y1 = ne_nil T x2 → False.
54 #T; #x1; #x2; #y1; #H;
55 nchange with (match ne_cons T x1 y1 with [ ne_nil _ ⇒ True | ne_cons a b ⇒ False ]);
61 nlemma nelist_destruct_nil_cons : ∀T.∀x1,x2:T.∀y2:ne_list T.ne_nil T x1 = ne_cons T x2 y2 → False.
62 #T; #x1; #x2; #y2; #H;
63 nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ True | ne_cons a b ⇒ False ]);
69 nlemma symmetric_eqlenlist : ∀T.∀l1,l2:list T.len_list T l1 = len_list T l2 → len_list T l2 = len_list T l1.
72 ##[ ##1: #l2; ncases l2; nnormalize;
73 ##[ ##1: #H; napply refl_eq
74 ##| ##2: #h; #t; #H; nelim (nat_destruct_0_S ? H)
76 ##| ##2: #h; #l2; ncases l2; nnormalize;
77 ##[ ##1: #H; #l; #H1; nrewrite < H1; napply refl_eq
78 ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply refl_eq
83 nlemma symmetric_foldrightlist2_aux
84 : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:list T1.
85 ∀H1:len_list T1 l1 = len_list T1 l2.∀H2:len_list T1 l2 = len_list T1 l1.
86 (∀x,y,z.f x y z = f y x z) →
87 fold_right_list2 T1 T2 f acc l1 l2 H1 = fold_right_list2 T1 T2 f acc l2 l1 H2.
88 #T1; #T2; #f; #acc; #l1;
90 ##[ ##1: #l2; ncases l2;
91 ##[ ##1: nnormalize; #H1; #H2; #H3; napply refl_eq
92 ##| ##2: #h; #l; #H1; #H2; #H3;
93 nchange in H1:(%) with (O = (S (len_list ? l)));
94 nelim (nat_destruct_0_S ? H1)
96 ##| ##2: #h3; #l3; #H; #l2; ncases l2;
97 ##[ ##1: #H1; #H2; #H3; nchange in H1:(%) with ((S (len_list ? l3)) = O);
98 nelim (nat_destruct_S_0 ? H1)
99 ##| ##2: #h4; #l4; #H1; #H2; #H3;
100 nchange in H1:(%) with ((S (len_list ? l3)) = (S (len_list ? l4)));
101 nchange in H2:(%) with ((S (len_list ? l4)) = (S (len_list ? l3)));
102 nchange with ((f h3 h4 (fold_right_list2 T1 T2 f acc l3 l4 (fold_right_list2_aux3 T1 h3 h4 l3 l4 ?))) =
103 (f h4 h3 (fold_right_list2 T1 T2 f acc l4 l3 (fold_right_list2_aux3 T1 h4 h3 l4 l3 ?))));
104 nrewrite < (H l4 (fold_right_list2_aux3 T1 h3 h4 l3 l4 H1) (fold_right_list2_aux3 T1 h4 h3 l4 l3 H2) H3);
105 nrewrite > (H3 h3 h4 (fold_right_list2 T1 T2 f acc l3 l4 ?));
111 nlemma symmetric_foldrightlist2
112 : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:list T1.∀H:len_list T1 l1 = len_list T1 l2.
113 (∀x,y,z.f x y z = f y x z) →
114 fold_right_list2 T1 T2 f acc l1 l2 H = fold_right_list2 T1 T2 f acc l2 l1 (symmetric_eqlenlist T1 l1 l2 H).
115 #T1; #T2; #f; #acc; #l1; #l2; #H; #H1;
116 nrewrite > (symmetric_foldrightlist2_aux T1 T2 f acc l1 l2 H (symmetric_eqlenlist T1 l1 l2 H) H1);
120 nlemma symmetric_bfoldrightlist2
121 : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
122 (∀x,y.f x y = f y x) →
123 bfold_right_list2 T1 f l1 l2 = bfold_right_list2 T1 f l2 l1.
126 ##[ ##1: #l2; ncases l2;
127 ##[ ##1: #H; nnormalize; napply refl_eq
128 ##| ##2: #hh2; #ll2; #H; nnormalize; napply refl_eq
130 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
131 ##[ ##1: #H1; nnormalize; napply refl_eq
132 ##| ##2: #hh2; #ll2; #H1; nnormalize;
133 nrewrite > (H ll2 H1);
134 nrewrite > (H1 hh1 hh2);
140 nlemma bfoldrightlist2_to_eq
141 : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
142 (∀x,y.(f x y = true → x = y)) →
143 (bfold_right_list2 T1 f l1 l2 = true → l1 = l2).
146 ##[ ##1: #l2; ncases l2;
147 ##[ ##1: #H; #H1; napply refl_eq
148 ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; napply (bool_destruct … H1)
150 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
151 ##[ ##1: #H1; nnormalize; #H2; napply (bool_destruct … H2)
152 ##| ##2: #hh2; #ll2; #H1; #H2;
153 nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = true);
154 nrewrite > (H1 hh1 hh2 (andb_true_true_l … H2));
155 nrewrite > (H ll2 H1 (andb_true_true_r … H2));
161 nlemma eq_to_bfoldrightlist2
162 : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
163 (∀x,y.(x = y → f x y = true)) →
164 (l1 = l2 → bfold_right_list2 T1 f l1 l2 = true).
167 ##[ ##1: #l2; ncases l2;
168 ##[ ##1: #H; #H1; nnormalize; napply refl_eq
169 ##| ##2: #hh2; #ll2; #H; #H1; nelim (list_destruct_nil_cons ??? H1)
171 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
172 ##[ ##1: #H1; #H2; nelim (list_destruct_cons_nil ??? H2)
173 ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize;
174 nrewrite > (list_destruct_1 … H2);
175 nrewrite > (H1 hh2 hh2 (refl_eq …));
177 nrewrite > (H ll2 H1 (list_destruct_2 … H2));
183 nlemma symmetric_eqlennelist : ∀T.∀l1,l2:ne_list T.len_neList T l1 = len_neList T l2 → len_neList T l2 = len_neList T l1.
186 ##[ ##1: #h; #l2; ncases l2; nnormalize;
187 ##[ ##1: #H; #H1; napply refl_eq
188 ##| ##2: #h; #t; #H; nrewrite > H; napply refl_eq
190 ##| ##2: #h; #l2; ncases l2; nnormalize;
191 ##[ ##1: #h1; #H; #l; #H1; nrewrite < H1; napply refl_eq
192 ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply refl_eq
197 nlemma symmetric_foldrightnelist2_aux
198 : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:ne_list T1.
199 ∀H1:len_neList T1 l1 = len_neList T1 l2.∀H2:len_neList T1 l2 = len_neList T1 l1.
200 (∀x,y,z.f x y z = f y x z) →
201 fold_right_neList2 T1 T2 f acc l1 l2 H1 = fold_right_neList2 T1 T2 f acc l2 l1 H2.
202 #T1; #T2; #f; #acc; #l1;
204 ##[ ##1: #h; #l2; ncases l2;
205 ##[ ##1: #h1; nnormalize; #H1; #H2; #H3; nrewrite > (H3 h h1 acc); napply refl_eq
206 ##| ##2: #h1; #l; ncases l;
207 ##[ ##1: #h3; #H1; #H2; #H3;
208 nchange in H1:(%) with ((S O) = (S (S O)));
209 nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
210 ##| ##2: #h3; #l3; #H1; #H2; #H3;
211 nchange in H1:(%) with ((S O) = (S (S (len_neList ? l3))));
212 nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
215 ##| ##2: #h3; #l3; #H; #l2; ncases l2;
216 ##[ ##1: #h4; ncases l3;
217 ##[ ##1: #h5; #H1; #H2; #H3;
218 nchange in H1:(%) with ((S (S O)) = (S O));
219 nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
220 ##| ##2: #h5; #l5; #H1; #H2; #H3;
221 nchange in H1:(%) with ((S (S (len_neList ? l5))) = (S O));
222 nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
224 ##| ##2: #h4; #l4; #H1; #H2; #H3;
225 nchange in H1:(%) with ((S (len_neList ? l3)) = (S (len_neList ? l4)));
226 nchange in H2:(%) with ((S (len_neList ? l4)) = (S (len_neList ? l3)));
227 nchange with ((f h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 ?))) =
228 (f h4 h3 (fold_right_neList2 T1 T2 f acc l4 l3 (fold_right_neList2_aux3 T1 h4 h3 l4 l3 ?))));
229 nrewrite < (H l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 H1) (fold_right_neList2_aux3 T1 h4 h3 l4 l3 H2) H3);
230 nrewrite > (H3 h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 ?));
236 nlemma symmetric_foldrightnelist2
237 : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:ne_list T1.∀H:len_neList T1 l1 = len_neList T1 l2.
238 (∀x,y,z.f x y z = f y x z) →
239 fold_right_neList2 T1 T2 f acc l1 l2 H = fold_right_neList2 T1 T2 f acc l2 l1 (symmetric_eqlennelist T1 l1 l2 H).
240 #T1; #T2; #f; #acc; #l1; #l2; #H; #H1;
241 nrewrite > (symmetric_foldrightnelist2_aux T1 T2 f acc l1 l2 H (symmetric_eqlennelist T1 l1 l2 H) H1);
245 nlemma symmetric_bfoldrightnelist2
246 : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
247 (∀x,y.f x y = f y x) →
248 bfold_right_neList2 T1 f l1 l2 = bfold_right_neList2 T1 f l2 l1.
251 ##[ ##1: #hh1; #l2; ncases l2;
252 ##[ ##1: #hh2; #H; nnormalize; nrewrite > (H hh1 hh2); napply refl_eq
253 ##| ##2: #hh2; #ll2; #H; nnormalize; napply refl_eq
255 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
256 ##[ ##1: #hh2; #H1; nnormalize; napply refl_eq
257 ##| ##2: #hh2; #ll2; #H1; nnormalize;
258 nrewrite > (H ll2 H1);
259 nrewrite > (H1 hh1 hh2);
265 nlemma bfoldrightnelist2_to_eq
266 : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
267 (∀x,y.(f x y = true → x = y)) →
268 (bfold_right_neList2 T1 f l1 l2 = true → l1 = l2).
271 ##[ ##1: #hh1; #l2; ncases l2;
272 ##[ ##1: #hh2; #H; #H1; nnormalize in H1:(%); nrewrite > (H hh1 hh2 H1); napply refl_eq
273 ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; napply (bool_destruct … H1)
275 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
276 ##[ ##1: #hh2; #H1; nnormalize; #H2; napply (bool_destruct … H2)
277 ##| ##2: #hh2; #ll2; #H1; #H2;
278 nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = true);
279 nrewrite > (H1 hh1 hh2 (andb_true_true_l … H2));
280 nrewrite > (H ll2 H1 (andb_true_true_r … H2));
286 nlemma eq_to_bfoldrightnelist2
287 : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
288 (∀x,y.(x = y → f x y = true)) →
289 (l1 = l2 → bfold_right_neList2 T1 f l1 l2 = true).
292 ##[ ##1: #hh1; #l2; ncases l2;
293 ##[ ##1: #hh2; #H; #H1; nnormalize;
294 nrewrite > (H hh1 hh2 (nelist_destruct_nil_nil … H1));
296 ##| ##2: #hh2; #ll2; #H; #H1; nelim (nelist_destruct_nil_cons ???? H1)
298 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
299 ##[ ##1: #hh2; #H1; #H2; nelim (nelist_destruct_cons_nil ???? H2)
300 ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize;
301 nrewrite > (nelist_destruct_cons_cons_1 … H2);
302 nrewrite > (H1 hh2 hh2 (refl_eq …));
304 nrewrite > (H ll2 H1 (nelist_destruct_cons_cons_2 … H2));
310 nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l.
314 ##[ ##1: #H; napply I
315 ##| ##2: #x; #l; #H; napply (bool_destruct … H)
319 nlemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l.
323 ##[ ##1: #H; napply (bool_destruct … H)
324 ##| ##2: #x; #l; #H; napply I
332 nlemma iszerob_to_iszero : ∀n.isZerob n = true → isZero n.
335 ##[ ##1: nnormalize; #H; napply I
336 ##| ##2: #n1; nnormalize; #H; napply (bool_destruct … H)