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.
71 napply (list_ind ???? 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;
89 napply (list_ind ???? 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_eqlennelist : ∀T.∀l1,l2:ne_list T.len_neList T l1 = len_neList T l2 → len_neList T l2 = len_neList T l1.
122 napply (ne_list_ind ???? l1);
123 ##[ ##1: #h; #l2; ncases l2; nnormalize;
124 ##[ ##1: #H; #H1; napply (refl_eq ??)
125 ##| ##2: #h; #t; #H; nrewrite > H; napply (refl_eq ??)
127 ##| ##2: #h; #l2; ncases l2; nnormalize;
128 ##[ ##1: #h1; #H; #l; #H1; nrewrite < H1; napply (refl_eq ??)
129 ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply (refl_eq ??)
134 nlemma symmetric_foldrightnelist2_aux
135 : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:ne_list T1.
136 ∀H1:len_neList T1 l1 = len_neList T1 l2.∀H2:len_neList T1 l2 = len_neList T1 l1.
137 (∀x,y,z.f x y z = f y x z) →
138 fold_right_neList2 T1 T2 f acc l1 l2 H1 = fold_right_neList2 T1 T2 f acc l2 l1 H2.
139 #T1; #T2; #f; #acc; #l1;
140 napply (ne_list_ind ???? l1);
141 ##[ ##1: #h; #l2; ncases l2;
142 ##[ ##1: #h1; nnormalize; #H1; #H2; #H3; nrewrite > (H3 h h1 acc); napply (refl_eq ??)
143 ##| ##2: #h1; #l; ncases l;
144 ##[ ##1: #h3; #H1; #H2; #H3;
145 nchange in H1:(%) with ((S O) = (S (S O)));
146 nelim (nat_destruct_0_S ? (nat_destruct_S_S ?? H1))
147 ##| ##2: #h3; #l3; #H1; #H2; #H3;
148 nchange in H1:(%) with ((S O) = (S (S (len_neList ? l3))));
149 nelim (nat_destruct_0_S ? (nat_destruct_S_S ?? H1))
152 ##| ##2: #h3; #l3; #H; #l2; ncases l2;
153 ##[ ##1: #h4; ncases l3;
154 ##[ ##1: #h5; #H1; #H2; #H3;
155 nchange in H1:(%) with ((S (S O)) = (S O));
156 nelim (nat_destruct_S_0 ? (nat_destruct_S_S ?? H1))
157 ##| ##2: #h5; #l5; #H1; #H2; #H3;
158 nchange in H1:(%) with ((S (S (len_neList ? l5))) = (S O));
159 nelim (nat_destruct_S_0 ? (nat_destruct_S_S ?? H1))
161 ##| ##2: #h4; #l4; #H1; #H2; #H3;
162 nchange in H1:(%) with ((S (len_neList ? l3)) = (S (len_neList ? l4)));
163 nchange in H2:(%) with ((S (len_neList ? l4)) = (S (len_neList ? l3)));
164 nchange with ((f h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 ?))) =
165 (f h4 h3 (fold_right_neList2 T1 T2 f acc l4 l3 (fold_right_neList2_aux3 T1 h4 h3 l4 l3 ?))));
166 nrewrite < (H l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 H1) (fold_right_neList2_aux3 T1 h4 h3 l4 l3 H2) H3);
167 nrewrite > (H3 h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 ?));
173 nlemma symmetric_foldrightnelist2
174 : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:ne_list T1.∀H:len_neList T1 l1 = len_neList T1 l2.
175 (∀x,y,z.f x y z = f y x z) →
176 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).
177 #T1; #T2; #f; #acc; #l1; #l2; #H; #H1;
178 nrewrite > (symmetric_foldrightnelist2_aux T1 T2 f acc l1 l2 H (symmetric_eqlennelist T1 l1 l2 H) H1);
182 nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l.
186 ##[ ##1: #H; napply I
187 ##| ##2: #x; #l; #H; napply (bool_destruct ??? H)
191 nlemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l.
195 ##[ ##1: #H; napply (bool_destruct ??? H)
196 ##| ##2: #x; #l; #H; napply I
204 nlemma iszerob_to_iszero : ∀n.isZerob n = true → isZero n.
207 ##[ ##1: nnormalize; #H; napply I
208 ##| ##2: #n1; nnormalize; #H; napply (bool_destruct ??? H)