X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcommon%2Flist_utility.ma;h=154d85d36f2794c7984c9d07b0aa8f9dff33eae8;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=3ffd1d3c5df48cd6f91116570aa2b1f7cc3c45ca;hpb=3819ff5482f28f3bb9be822513c7bd73c47a46e0;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/common/list_utility.ma b/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
index 3ffd1d3c5..154d85d36 100755
--- a/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
@@ -15,8 +15,8 @@
 (* ********************************************************************** *)
 (*                          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                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -95,7 +95,7 @@ nlemma fold_right_list2_aux1 :
  #T; #h; #t;
  nnormalize;
  #H;
- napply (nat_destruct_0_S ? H).
+ ndestruct (*napply (nat_destruct_0_S ? H)*).
 nqed.
 
 nlemma fold_right_list2_aux2 :
@@ -103,7 +103,7 @@ 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 :
@@ -114,10 +114,10 @@ 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)));
@@ -162,7 +162,7 @@ nlet rec nth_list (T:Type) (l:list T) (n:nat) on 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.
@@ -188,7 +188,7 @@ nlet rec abs_list (T:Type) (l:list T) on l ≝
 
 (* 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 ≝
@@ -241,8 +241,8 @@ nlemma fold_right_neList2_aux1 :
  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.
 
@@ -252,8 +252,8 @@ nlemma fold_right_neList2_aux2 :
  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.
 
@@ -316,13 +316,11 @@ nlet rec nth_neList (T:Type) (nl:ne_list T) (n:nat) on nl ≝
 
 (* 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