(* ********************************************************************** *)
(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
(* *)
(* ********************************************************************** *)
#T; #h; #t;
nnormalize;
#H;
- napply (nat_destruct_0_S ? H).
+ ndestruct (*napply (nat_destruct_0_S ? H)*).
nqed.
nlemma fold_right_list2_aux2 :
#T; #h; #t;
nnormalize;
#H;
- napply (nat_destruct_S_0 ? H).
+ ndestruct (*napply (nat_destruct_S_0 ? H)*).
nqed.
nlemma fold_right_list2_aux3 :
##[ ##1: nnormalize; #H; napply refl_eq
##| ##2: #a; #l'; #H; #H1;
nchange in H1:(%) with ((S O) = (S (S (len_list T l'))));
- nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
+ ndestruct (*nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))*)
##| ##3: #a; #l'; #H; #H1;
nchange in H1:(%) with ((S (S (len_list T l'))) = (S O));
- nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
+ ndestruct (*nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))*)
##| ##4: #a; #l; #H; #a1; #l1; #H1; #H2;
nchange in H2:(%) with ((S (S (len_list T l1))) = (S (S (len_list T l))));
nchange with ((S (len_list T l1)) = (S (len_list T l)));
(* abs elem *)
ndefinition abs_list_aux1 : ∀T:Type.∀n.((len_list T []) > n) = true → False.
- #T; nnormalize; #n; #H; napply (bool_destruct … H). nqed.
+ #T; nnormalize; #n; #H; ndestruct (*napply (bool_destruct … H)*). nqed.
ndefinition abs_list_aux2 : ∀T:Type.∀h:T.∀t:list T.∀n.((len_list T (h::t)) > (S n) = true) → ((len_list T t) > n) = true.
#T; #h; #t; #n; nnormalize; #H; napply H. nqed.
(* listlen *)
nlet rec len_neList (T:Type) (nl:ne_list T) on nl ≝
- match nl with [ ne_nil _ ⇒ 1 | ne_cons _ t ⇒ S (len_neList T t) ].
+ match nl with [ ne_nil _ ⇒ (S O) | ne_cons _ t ⇒ S (len_neList T t) ].
(* reverse *)
nlet rec reverse_neList (T:Type) (nl:ne_list T) on nl ≝
nnormalize;
ncases t';
nnormalize;
- ##[ ##1: #x; #H; nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))
- ##| ##2: #x; #l; #H; nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))
+ ##[ ##1: #x; #H; ndestruct (*nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))*)
+ ##| ##2: #x; #l; #H; ndestruct (*nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))*)
##]
nqed.
nnormalize;
ncases t;
nnormalize;
- ##[ ##1: #x; #H; nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))
- ##| ##2: #x; #l; #H; nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))
+ ##[ ##1: #x; #H; ndestruct (*nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))*)
+ ##| ##2: #x; #l; #H; ndestruct (*nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))*)
##]
nqed.
(* abs elem *)
ndefinition abs_neList_aux1 : ∀T:Type.∀h:T.∀n.((len_neList T («£h»)) > (S n)) = true → False.
- #T; #h; #n; nnormalize; #H; napply (bool_destruct … H). nqed.
+ #T; #h; #n; nnormalize; #H; ndestruct (*napply (bool_destruct … H)*). nqed.
ndefinition abs_neList_aux2 : ∀T:Type.∀h:T.∀t:ne_list T.∀n.((len_neList T (h§§t)) > (S n) = true) → ((len_neList T t) > n) = true.
#T; #h; #t; #n; nnormalize; #H; napply H. nqed.
-naxiom daemon : False.
-
nlet rec abs_neList (T:Type) (l:ne_list T) on l ≝
match l
return λl.Πn.(((len_neList T l) > n) = true) → T