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 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 include "common/list.ma".
24 include "common/nat_lemmas.ma".
25 include "common/prod.ma".
27 nlet rec nmember_natList (elem:nat) (l:ne_list nat) on l ≝
29 [ ne_nil h ⇒ ⊖(eq_nat elem h)
30 | ne_cons h t ⇒ match eq_nat elem h with
31 [ true ⇒ false | false ⇒ nmember_natList elem t ]
34 (* elem presente una ed una sola volta in l *)
35 nlet rec member_natList (elem:nat) (l:ne_list nat) on l ≝
37 [ ne_nil h ⇒ eq_nat elem h
38 | ne_cons h t ⇒ match eq_nat elem h with
39 [ true ⇒ nmember_natList elem t | false ⇒ member_natList elem t ]
42 (* costruttore di un sottouniverso:
43 S_EL cioe' uno qualsiasi degli elementi del sottouniverso
45 ninductive S_UN (l:ne_list nat) : Type ≝
46 S_EL : Πx:nat.((member_natList x l) = true) → S_UN l.
48 ndefinition getelem : ∀l.∀e:S_UN l.nat.
54 ndefinition eq_SUN ≝ λl.λx,y:S_UN l.eq_nat (getelem ? x) (getelem ? y).
56 ndefinition getdim : ∀l.∀e:S_UN l.member_natList (getelem ? e) l = true.
63 : ∀l.∀e1,e2.∀dim1,dim2.S_EL l e1 dim1 = S_EL l e2 dim2 → e1 = e2.
64 #l; #e1; #e2; #dim1; #dim2; #H;
65 nchange with (match S_EL l e2 dim2 with [ S_EL a _ ⇒ e1 = a ]);
71 (* destruct universale *)
72 ndefinition SUN_destruct : ∀l.∀x,y:S_UN l.∀P:Prop.x = y → match eq_SUN l x y with [ true ⇒ P → P | false ⇒ P ].
78 nchange with (? → (match eq_nat u1 u2 with [ true ⇒ P → P | false ⇒ P ]));
80 nrewrite > (SUN_destruct_1 l … H);
81 nrewrite > (eq_to_eqnat u2 u2 (refl_eq …));
86 (* eq_to_eqxx universale *)
87 nlemma eq_to_eqSUN : ∀l.∀x,y:S_UN l.x = y → eq_SUN l x y = true.
92 nchange with (? → eq_nat u1 u2 = true);
93 #H; napply (eq_to_eqnat u1 u2);
94 napply (SUN_destruct_1 l … H).
97 (* neqxx_to_neq universale *)
98 nlemma neqSUN_to_neq : ∀l.∀x,y:S_UN l.eq_SUN l x y = false → x ≠ y.
100 napply (not_to_not (n1 = n2) (eq_SUN l n1 n2 = true) …);
101 ##[ ##1: napply (eq_to_eqSUN l n1 n2)
102 ##| ##2: napply (eqfalse_to_neqtrue … H)
106 (* perche' non si riesce a dimstrare ??? *
109 ∀dim1,dim2:(member_natList u l = true).
110 ((S_EL l u dim1) = (S_EL l u dim2)).
111 #l; #u; #dim1; #dim2;
112 nchange with (S_EL l u dim1 = S_EL l u dim1);
118 ∀dim1,dim2:(member_natList u l = true).
119 ((S_EL l u dim1) = (S_EL l u dim2)).
121 nlemma eqgetelem_to_eq : ∀l.∀x,y:S_UN l.(getelem ? x) = (getelem ? y) → x = y.
126 nchange with (u1 = u2 → ?);
128 nrewrite > H in dim1:(%) ⊢ %;
130 napply (SUN_construct l u2 dim1 dim2).
133 (* eqxx_to_eq universale *)
134 nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = y.
139 nchange with ((eq_nat u1 u2 = true) → ?);
141 nrewrite > (eqgetelem_to_eq l (S_EL l u1 dim1) (S_EL l u2 dim2) (eqnat_to_eq u1 u2 H));
145 (* neq_to_neqxx universale *)
146 nlemma neq_to_neqSUN : ∀l.∀x,y:S_UN l.x ≠ y → eq_SUN l x y = false.
148 napply (neqtrue_to_eqfalse (eq_SUN l n1 n2));
149 napply (not_to_not (eq_SUN l n1 n2 = true) (n1 = n2) ? H);
150 napply (eqSUN_to_eq l n1 n2).
153 (* decidibilita' universale *)
154 nlemma decidable_SUN : ∀l.∀x,y:S_UN l.decidable (x = y).
155 #l; #x; #y; nnormalize;
156 napply (or2_elim (eq_SUN l x y = true) (eq_SUN l x y = false) ? (decidable_bexpr ?));
157 ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqSUN_to_eq l … H))
158 ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqSUN_to_neq l … H))
162 (* simmetria di uguaglianza universale *)
163 nlemma symmetric_eqSUN : ∀l.symmetricT (S_UN l) bool (eq_SUN l).
165 napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_SUN l n1 n2));
166 ##[ ##1: #H; nrewrite > H; napply refl_eq
167 ##| ##2: #H; nrewrite > (neq_to_neqSUN l n1 n2 H);
168 napply (symmetric_eq ? (eq_SUN l n2 n1) false);
169 napply (neq_to_neqSUN l n2 n1 (symmetric_neq ? n1 n2 H))
173 (* scheletro di funzione generica ad 1 argomento *)
174 nlet rec farg1_auxT (T:Type) (l:ne_list nat) on l ≝
177 | ne_cons _ t ⇒ ProdT T (farg1_auxT T t)
180 nlemma farg1_auxDim : ∀h,t,x.eq_nat x h = false → member_natList x (h§§t) = true → member_natList x t = true.
182 nnormalize in H1:(%);
183 nrewrite > H in H1:(%);
188 nlet rec farg1 (T:Type) (l:ne_list nat) on l ≝
190 [ ne_nil h ⇒ λarg:farg1_auxT T «£h».λx:S_UN «£h».arg
191 | ne_cons h t ⇒ λarg:farg1_auxT T (h§§t).λx:S_UN (h§§t).
192 match eq_nat (getelem ? x) h
193 return λy.eq_nat (getelem ? x) h = y → ?
195 [ true ⇒ λp:(eq_nat (getelem ? x) h = true).fst … arg
196 | false ⇒ λp:(eq_nat (getelem ? x) h = false).
199 (S_EL t (getelem ? x) (farg1_auxDim h t (getelem ? x) p (getdim ? x)))
200 ] (refl_eq ? (eq_nat (getelem ? x) h))
203 (* scheletro di funzione generica a 2 argomenti *)
204 nlet rec farg2 (T:Type) (l,lfix:ne_list nat) on l ≝
206 [ ne_nil h ⇒ λarg:farg1_auxT (farg1_auxT T lfix) «£h».λx:S_UN «£h».farg1 T lfix arg
207 | ne_cons h t ⇒ λarg:farg1_auxT (farg1_auxT T lfix) (h§§t).λx:S_UN (h§§t).
208 match eq_nat (getelem ? x) h
209 return λy.eq_nat (getelem ? x) h = y → ?
211 [ true ⇒ λp:(eq_nat (getelem ? x) h = true).farg1 T lfix (fst … arg)
212 | false ⇒ λp:(eq_nat (getelem ? x) h = false).
215 (S_EL t (getelem ? x) (farg1_auxDim h t (getelem ? x) p (getdim ? x)))
216 ] (refl_eq ? (eq_nat (getelem ? x) h))
219 (* esempio0: universo ottale *)
220 ndefinition oct0 ≝ O.
221 ndefinition oct1 ≝ S O.
222 ndefinition oct2 ≝ S (S O).
223 ndefinition oct3 ≝ S (S (S O)).
224 ndefinition oct4 ≝ S (S (S (S O))).
225 ndefinition oct5 ≝ S (S (S (S (S O)))).
226 ndefinition oct6 ≝ S (S (S (S (S (S O))))).
227 ndefinition oct7 ≝ S (S (S (S (S (S (S O)))))).
229 ndefinition oct_UN ≝ « oct0 ; oct1 ; oct2 ; oct3 ; oct4 ; oct5 ; oct6 £ oct7 ».
231 ndefinition uoct0 ≝ S_EL oct_UN oct0 (refl_eq …).
232 ndefinition uoct1 ≝ S_EL oct_UN oct1 (refl_eq …).
233 ndefinition uoct2 ≝ S_EL oct_UN oct2 (refl_eq …).
234 ndefinition uoct3 ≝ S_EL oct_UN oct3 (refl_eq …).
235 ndefinition uoct4 ≝ S_EL oct_UN oct4 (refl_eq …).
236 ndefinition uoct5 ≝ S_EL oct_UN oct5 (refl_eq …).
237 ndefinition uoct6 ≝ S_EL oct_UN oct6 (refl_eq …).
238 ndefinition uoct7 ≝ S_EL oct_UN oct7 (refl_eq …).
240 (* esempio1: NOT ottale *)
242 farg1 (S_UN oct_UN) oct_UN
243 (pair … uoct7 (pair … uoct6 (pair … uoct5 (pair … uoct4 (pair … uoct3 (pair … uoct2 (pair … uoct1 uoct0))))))).
245 (* esempio2: AND ottale *)
246 ndefinition octAND0 ≝ pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 uoct0)))))).
247 ndefinition octAND1 ≝ pair … uoct0 (pair … uoct1 (pair … uoct0 (pair … uoct1 (pair … uoct0 (pair … uoct1 (pair … uoct0 uoct1)))))).
248 ndefinition octAND2 ≝ pair … uoct0 (pair … uoct0 (pair … uoct2 (pair … uoct2 (pair … uoct0 (pair … uoct0 (pair … uoct2 uoct2)))))).
249 ndefinition octAND3 ≝ pair … uoct0 (pair … uoct1 (pair … uoct2 (pair … uoct3 (pair … uoct0 (pair … uoct1 (pair … uoct2 uoct3)))))).
250 ndefinition octAND4 ≝ pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct4 (pair … uoct4 (pair … uoct4 uoct4)))))).
251 ndefinition octAND5 ≝ pair … uoct0 (pair … uoct1 (pair … uoct0 (pair … uoct1 (pair … uoct4 (pair … uoct5 (pair … uoct4 uoct5)))))).
252 ndefinition octAND6 ≝ pair … uoct0 (pair … uoct0 (pair … uoct2 (pair … uoct2 (pair … uoct4 (pair … uoct4 (pair … uoct6 uoct6)))))).
253 ndefinition octAND7 ≝ pair … uoct0 (pair … uoct1 (pair … uoct2 (pair … uoct3 (pair … uoct4 (pair … uoct5 (pair … uoct6 uoct7)))))).
256 farg2 (S_UN oct_UN) oct_UN oct_UN
257 (pair … octAND0 (pair … octAND1 (pair … octAND2 (pair … octAND3 (pair … octAND4 (pair … octAND5 (pair … octAND6 octAND7))))))).
259 (* ora e' possibile fare