From: Cosimo Oliboni <??>
Date: Tue, 4 Aug 2009 22:12:22 +0000 (+0000)
Subject:  freescale porting, work in progress
X-Git-Tag: make_still_working~3570
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3819ff5482f28f3bb9be822513c7bd73c47a46e0;p=helm.git

 freescale porting, work in progress
---

diff --git a/helm/software/matita/contribs/ng_assembly/common/list_utility.ma b/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
new file mode 100755
index 000000000..3ffd1d3c5
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
@@ -0,0 +1,350 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(*                          Progetto FreeScale                            *)
+(*                                                                        *)
+(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
+(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*                                                                        *)
+(* ********************************************************************** *)
+
+include "common/list.ma".
+include "common/option.ma".
+include "common/nat_lemmas.ma".
+
+(* *************** *)
+(* LISTE GENERICHE *)
+(* *************** *)
+
+(* listlen *)
+nlet rec len_list (T:Type) (l:list T) on l ≝
+ match l with [ nil ⇒ O | cons _ t ⇒ S (len_list T t) ].
+
+(* vuota? *)
+ndefinition is_empty_list ≝
+λT:Type.λl:list T.match l with [ nil ⇒ True | cons _ _ ⇒ False ].
+
+ndefinition isb_empty_list ≝
+λT:Type.λl:list T.match l with [ nil ⇒ true | cons _ _ ⇒ false ].
+
+ndefinition isnot_empty_list ≝
+λT:Type.λl:list T.match l with [ nil ⇒ False | cons _ _ ⇒ True ].
+
+ndefinition isnotb_empty_list ≝
+λT:Type.λl:list T.match l with [ nil ⇒ false | cons _ _ ⇒ true ].
+
+(* reverse *)
+nlet rec reverse_list (T:Type) (l:list T) on l ≝
+ match l with
+  [ nil ⇒ nil T
+  | cons h t ⇒ (reverse_list T t)@[h]
+  ].
+
+(* getFirst *)
+ndefinition get_first_list ≝
+λT:Type.λl:list T.match l with
+ [ nil ⇒ None ?
+ | cons h _ ⇒ Some ? h ].
+
+(* getLast *)
+ndefinition get_last_list ≝
+λT:Type.λl:list T.match reverse_list T l with
+ [ nil ⇒ None ?
+ | cons h _ ⇒ Some ? h ].
+
+(* cutFirst *)
+ndefinition cut_first_list ≝
+λT:Type.λl:list T.match l with
+ [ nil ⇒ nil T
+ | cons _ t ⇒ t ].
+
+(* cutLast *)
+ndefinition cut_last_list ≝
+λT:Type.λl:list T.match reverse_list T l with
+ [ nil ⇒ nil T
+ | cons _ t ⇒ reverse_list T t ].
+
+(* apply f *)
+nlet rec apply_f_list (T1,T2:Type) (l:list T1) (f:T1 → T2) on l ≝
+match l with
+ [ nil ⇒ nil T2
+ | cons h t ⇒ cons T2 (f h) (apply_f_list T1 T2 t f) ].
+
+(* fold right *)
+nlet rec fold_right_list (T1,T2:Type) (f:T1 → T2 → T2) (acc:T2) (l:list T1) on l ≝
+  match l with
+   [ nil ⇒ acc
+   | cons h t ⇒ f h (fold_right_list T1 T2 f acc t)
+   ].
+
+(* double fold right *)
+nlemma fold_right_list2_aux1 :
+∀T.∀h,t.len_list T [] = len_list T (h::t) → False.
+ #T; #h; #t;
+ nnormalize;
+ #H;
+ napply (nat_destruct_0_S ? H).
+nqed.
+
+nlemma fold_right_list2_aux2 :
+∀T.∀h,t.len_list T (h::t) = len_list T [] → False.
+ #T; #h; #t;
+ nnormalize;
+ #H;
+ napply (nat_destruct_S_0 ? H).
+nqed.
+
+nlemma fold_right_list2_aux3 :
+∀T.∀h,h',t,t'.len_list T (h::t) = len_list T (h'::t') → len_list T t = len_list T t'.
+ #T; #h; #h'; #t; #t';
+ nelim t;
+ nelim t';
+ ##[ ##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))
+ ##| ##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))
+ ##| ##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)));
+          nrewrite > (nat_destruct_S_S … H2);
+          napply refl_eq
+ ##]
+nqed.
+
+nlet rec fold_right_list2 (T1,T2:Type) (f:T1 → T1 → T2 → T2) (acc:T2) (l1:list T1) on l1 ≝
+ match l1
+  return λl1.Πl2.len_list T1 l1 = len_list T1 l2 → T2
+ with
+  [ nil ⇒ λl2.match l2 return λl2.len_list T1 [] = len_list T1 l2 → T2 with
+   [ nil ⇒ λp:len_list T1 [] = len_list T1 [].acc
+   | cons h t ⇒ λp:len_list T1 [] = len_list T1 (h::t).
+    False_rect_Type0 ? (fold_right_list2_aux1 T1 h t p)
+   ]
+  | cons h t ⇒ λl2.match l2 return λl2.len_list T1 (h::t) = len_list T1 l2 → T2 with
+   [ nil ⇒ λp:len_list T1 (h::t) = len_list T1 [].
+    False_rect_Type0 ? (fold_right_list2_aux2 T1 h t p)
+   | cons h' t' ⇒ λp:len_list T1 (h::t) = len_list T1 (h'::t').
+    f h h' (fold_right_list2 T1 T2 f acc t t' (fold_right_list2_aux3 T1 h h' t t' p))
+   ]
+  ].
+
+nlet rec bfold_right_list2 (T1:Type) (f:T1 → T1 → bool) (l1,l2:list T1) on l1 ≝
+ match l1 with
+  [ nil ⇒ match l2 with
+   [ nil ⇒ true | cons h t ⇒ false ]
+  | cons h t ⇒ match l2 with
+   [ nil ⇒ false | cons h' t' ⇒ (f h h') ⊗ (bfold_right_list2 T1 f t t')
+   ]
+  ].
+
+(* nth elem *)
+nlet rec nth_list (T:Type) (l:list T) (n:nat) on l ≝
+ match l with
+  [ nil ⇒ None ?
+  | cons h t ⇒ match n with
+   [ O ⇒ Some ? h | S n' ⇒ nth_list T t n' ]
+  ].
+
+(* abs elem *)
+ndefinition abs_list_aux1 : ∀T:Type.∀n.((len_list T []) > n) = true → False.
+ #T; nnormalize; #n; #H; 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.
+
+nlet rec abs_list (T:Type) (l:list T) on l ≝
+ match l
+  return λl.Πn.(((len_list T l) > n) = true) → T
+ with
+  [ nil ⇒ λn.λp:(((len_list T []) > n) = true).False_rect_Type0 ? (abs_list_aux1 T n p)
+  | cons h t ⇒ λn.
+   match n with
+    [ O ⇒ λp:(((len_list T (h::t)) > O) = true).h
+    | S n' ⇒ λp:(((len_list T (h::t)) > (S n')) = true).
+     abs_list T t n' (abs_list_aux2 T h t n' p)
+    ]
+  ].
+
+(* esempio: abs_list ? [ 1; 2; 3; 4 ] 2 (refl_eq …) = 0. *)
+
+(* ************** *)
+(* NON-EMPTY LIST *)
+(* ************** *)
+
+(* 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) ].
+
+(* reverse *)
+nlet rec reverse_neList (T:Type) (nl:ne_list T) on nl ≝
+ match nl with
+  [ ne_nil h ⇒ ne_nil T h
+  | ne_cons h t ⇒ (reverse_neList T t)&(ne_nil T h)
+  ].
+
+(* getFirst *)
+ndefinition get_first_neList ≝
+λT:Type.λnl:ne_list T.match nl with
+ [ ne_nil h ⇒ h
+ | ne_cons h _ ⇒ h ].
+
+(* getLast *)
+ndefinition get_last_neList ≝
+λT:Type.λnl:ne_list T.match reverse_neList T nl with
+ [ ne_nil h ⇒ h
+ | ne_cons h _ ⇒ h ].
+
+(* cutFirst *)
+ndefinition cut_first_neList ≝
+λT:Type.λnl:ne_list T.match nl with
+ [ ne_nil h ⇒ ne_nil T h
+ | ne_cons _ t ⇒ t ].
+
+(* cutLast *)
+ndefinition cut_last_neList ≝
+λT:Type.λnl:ne_list T.match reverse_neList T nl with
+ [ ne_nil h ⇒ ne_nil T h
+ | ne_cons _ t ⇒ reverse_neList T t ].
+
+(* apply f *)
+nlet rec apply_f_neList (T1,T2:Type) (nl:ne_list T1) (f:T1 → T2) on nl ≝
+match nl with
+ [ ne_nil h ⇒ ne_nil T2 (f h)
+ | ne_cons h t ⇒ ne_cons T2 (f h) (apply_f_neList T1 T2 t f) ].
+
+(* fold right *)
+nlet rec fold_right_neList (T1,T2:Type) (f:T1 → T2 → T2) (acc:T2) (nl:ne_list T1) on nl ≝
+  match nl with
+   [ ne_nil h ⇒ f h acc
+   | ne_cons h t ⇒ f h (fold_right_neList T1 T2 f acc t)
+   ].
+
+(* double fold right *)
+nlemma fold_right_neList2_aux1 :
+∀T.∀h,h',t'.len_neList T «£h» = len_neList T (h'§§t') → False.
+ #T; #h; #h'; #t';
+ 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))
+ ##]
+nqed.
+
+nlemma fold_right_neList2_aux2 :
+∀T.∀h,h',t.len_neList T (h§§t) = len_neList T «£h'» → False.
+ #T; #h; #h'; #t;
+ 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))
+ ##]
+nqed.
+
+nlemma fold_right_neList2_aux3 :
+∀T.∀h,h',t,t'.len_neList T (h§§t) = len_neList T (h'§§t') → len_neList T t = len_neList T t'.
+ #T; #h; #h'; #t; #t';
+ nelim t;
+ nelim t';
+ ##[ ##1: nnormalize; #x; #y; #H; napply refl_eq
+ ##| ##2: #a; #l'; #H; #x; #H1;
+          nchange in H1:(%) with ((S (len_neList T «£x»)) = (S (len_neList T (a§§l'))));
+          nrewrite > (nat_destruct_S_S … H1);
+          napply refl_eq
+ ##| ##3: #x; #a; #l'; #H; #H1;
+          nchange in H1:(%) with ((S (len_neList T (a§§l')))= (S (len_neList T «£x»)));
+          nrewrite > (nat_destruct_S_S … H1);
+          napply refl_eq
+ ##| ##4: #a; #l; #H; #a1; #l1; #H1; #H2;
+          nchange in H2:(%) with ((S (len_neList T (a1§§l1))) = (S (len_neList T (a§§l))));
+          nrewrite > (nat_destruct_S_S … H2);
+          napply refl_eq
+ ##]
+nqed.
+
+nlet rec fold_right_neList2 (T1,T2:Type) (f:T1 → T1 → T2 → T2) (acc:T2) (l1:ne_list T1) on l1 ≝
+ match l1
+  return λl1.Πl2.len_neList T1 l1 = len_neList T1 l2 → T2
+ with
+  [ ne_nil h ⇒ λl2.match l2 return λl2.len_neList T1 «£h» = len_neList T1 l2 → T2 with
+   [ ne_nil h' ⇒ λp:len_neList T1 «£h» = len_neList T1 «£h'».
+    f h h' acc
+   | ne_cons h' t' ⇒ λp:len_neList T1 «£h» = len_neList T1 (h'§§t').
+    False_rect_Type0 ? (fold_right_neList2_aux1 T1 h h' t' p)
+   ]
+  | ne_cons h t ⇒ λl2.match l2 return λl2.len_neList T1 (h§§t) = len_neList T1 l2 → T2 with
+   [ ne_nil h' ⇒ λp:len_neList T1 (h§§t) = len_neList T1 «£h'».
+    False_rect_Type0 ? (fold_right_neList2_aux2 T1 h h' t p)
+   | ne_cons h' t' ⇒ λp:len_neList T1 (h§§t) = len_neList T1 (h'§§t').
+    f h h' (fold_right_neList2 T1 T2 f acc t t' (fold_right_neList2_aux3 T1 h h' t t' p))
+   ]
+  ].
+
+nlet rec bfold_right_neList2 (T1:Type) (f:T1 → T1 → bool) (l1,l2:ne_list T1) on l1 ≝
+ match l1 with
+  [ ne_nil h ⇒ match l2 with
+   [ ne_nil h' ⇒ f h h' | ne_cons h' t' ⇒ false ]
+  | ne_cons h t ⇒ match l2 with
+   [ ne_nil h' ⇒ false | ne_cons h' t' ⇒ (f h h') ⊗ (bfold_right_neList2 T1 f t t')
+   ]
+  ].
+
+(* nth elem *)
+nlet rec nth_neList (T:Type) (nl:ne_list T) (n:nat) on nl ≝
+ match nl with
+  [ ne_nil h ⇒ match n with
+   [ O ⇒ Some ? h | S _ ⇒ None ? ]
+  | ne_cons h t ⇒ match n with
+   [ O ⇒ Some ? h | S n' ⇒ nth_neList T t n' ]
+  ].
+
+(* 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.
+
+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
+ with
+  [ ne_nil h ⇒ λn.
+   match n
+    return λn.(((len_neList T (ne_nil T h)) > n) = true) → T
+   with
+    [ O ⇒ λp:(((len_neList T (ne_nil T h)) > O) = true).h
+    | S n' ⇒ λp:(((len_neList T (ne_nil T h)) > (S n')) = true).
+     False_rect_Type0 ? (abs_neList_aux1 T h n' p)
+    ]
+  | ne_cons h t ⇒ λn.
+   match n with
+    [ O ⇒ λp:(((len_neList T (ne_cons T h t)) > O) = true).h
+    | S n' ⇒ λp:(((len_neList T (ne_cons T h t)) > (S n')) = true).
+     abs_neList T t n' (abs_neList_aux2 T h t n' p)
+    ]
+  ].
+
+(* esempio: abs_neList ? « 1; 2; 3 £ 4 » 0 (refl_eq …) = 0. *)
+
+(* conversione *)
+nlet rec neList_to_list (T:Type) (nl:ne_list T) on nl : list T ≝
+ match nl with [ ne_nil h ⇒ [h] | ne_cons h t ⇒ [h]@(neList_to_list T t) ].
diff --git a/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma
new file mode 100755
index 000000000..5ae7fce81
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma
@@ -0,0 +1,291 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(*                          Progetto FreeScale                            *)
+(*                                                                        *)
+(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
+(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*                                                                        *)
+(* ********************************************************************** *)
+
+include "common/list_utility.ma".
+include "common/list_lemmas.ma".
+
+(* *************** *)
+(* LISTE GENERICHE *)
+(* *************** *)
+
+nlemma symmetric_lenlist : ∀T.∀l1,l2:list T.len_list T l1 = len_list T l2 → len_list T l2 = len_list T l1.
+ #T; #l1;
+ nelim l1;
+ ##[ ##1: #l2; ncases l2; nnormalize;
+          ##[ ##1: #H; napply refl_eq
+          ##| ##2: #h; #t; #H; nelim (nat_destruct_0_S ? H)
+          ##]
+ ##| ##2: #h; #l2; ncases l2; nnormalize;
+          ##[ ##1: #H; #l; #H1; nrewrite < H1; napply refl_eq
+          ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply refl_eq
+          ##]
+ ##]
+nqed.
+
+nlemma symmetric_foldrightlist2_aux
+ : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:list T1.
+   ∀H1:len_list T1 l1 = len_list T1 l2.∀H2:len_list T1 l2 = len_list T1 l1.
+  (∀x,y,z.f x y z = f y x z) →
+  fold_right_list2 T1 T2 f acc l1 l2 H1 = fold_right_list2 T1 T2 f acc l2 l1 H2.
+ #T1; #T2; #f; #acc; #l1;
+ nelim l1;
+ ##[ ##1: #l2; ncases l2;
+          ##[ ##1: nnormalize; #H1; #H2; #H3; napply refl_eq
+          ##| ##2: #h; #l; #H1; #H2; #H3;
+                   nchange in H1:(%) with (O = (S (len_list ? l)));
+                   nelim (nat_destruct_0_S ? H1)
+          ##]
+ ##| ##2: #h3; #l3; #H; #l2; ncases l2;
+          ##[ ##1: #H1; #H2; #H3; nchange in H1:(%) with ((S (len_list ? l3)) = O);
+                   nelim (nat_destruct_S_0 ? H1)
+          ##| ##2: #h4; #l4; #H1; #H2; #H3;
+                   nchange in H1:(%) with ((S (len_list ? l3)) = (S (len_list ? l4)));
+                   nchange in H2:(%) with ((S (len_list ? l4)) = (S (len_list ? l3)));
+                   nchange with ((f h3 h4 (fold_right_list2 T1 T2 f acc l3 l4 (fold_right_list2_aux3 T1 h3 h4 l3 l4 ?))) =
+                                 (f h4 h3 (fold_right_list2 T1 T2 f acc l4 l3 (fold_right_list2_aux3 T1 h4 h3 l4 l3 ?))));
+                   nrewrite < (H l4 (fold_right_list2_aux3 T1 h3 h4 l3 l4 H1) (fold_right_list2_aux3 T1 h4 h3 l4 l3 H2) H3);
+                   nrewrite > (H3 h3 h4 (fold_right_list2 T1 T2 f acc l3 l4 ?));
+                   napply refl_eq
+          ##]
+ ##]
+nqed.
+
+nlemma symmetric_foldrightlist2
+ : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:list T1.∀H:len_list T1 l1 = len_list T1 l2.
+  (∀x,y,z.f x y z = f y x z) →
+  fold_right_list2 T1 T2 f acc l1 l2 H = fold_right_list2 T1 T2 f acc l2 l1 (symmetric_lenlist T1 l1 l2 H).
+ #T1; #T2; #f; #acc; #l1; #l2; #H; #H1;
+ nrewrite > (symmetric_foldrightlist2_aux T1 T2 f acc l1 l2 H (symmetric_lenlist T1 l1 l2 H) H1);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_bfoldrightlist2
+ : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
+  (∀x,y.f x y = f y x) →
+  bfold_right_list2 T1 f l1 l2 = bfold_right_list2 T1 f l2 l1.
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #l2; ncases l2;
+          ##[ ##1: #H; nnormalize; napply refl_eq
+          ##| ##2: #hh2; #ll2; #H; nnormalize; napply refl_eq
+          ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+          ##[ ##1: #H1; nnormalize; napply refl_eq
+          ##| ##2: #hh2; #ll2; #H1; nnormalize;
+                   nrewrite > (H ll2 H1);
+                   nrewrite > (H1 hh1 hh2);
+                   napply refl_eq
+          ##]
+ ##]
+nqed.
+
+nlemma bfoldrightlist2_to_eq
+ : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
+   (∀x,y.(f x y = true → x = y)) →
+   (bfold_right_list2 T1 f l1 l2 = true → l1 = l2).
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #l2; ncases l2;
+          ##[ ##1: #H; #H1; napply refl_eq
+          ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; napply (bool_destruct … H1)
+          ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+          ##[ ##1: #H1; nnormalize; #H2; napply (bool_destruct … H2)
+          ##| ##2: #hh2; #ll2; #H1; #H2;
+                   nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = true);
+                   nrewrite > (H1 hh1 hh2 (andb_true_true_l … H2));
+                   nrewrite > (H ll2 H1 (andb_true_true_r … H2));
+                   napply refl_eq
+          ##]
+ ##]
+nqed.
+
+nlemma eq_to_bfoldrightlist2
+ : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
+   (∀x,y.(x = y → f x y = true)) →
+   (l1 = l2 → bfold_right_list2 T1 f l1 l2 = true).
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #l2; ncases l2;
+          ##[ ##1: #H; #H1; nnormalize; napply refl_eq
+          ##| ##2: #hh2; #ll2; #H; #H1; nelim (list_destruct_nil_cons ??? H1)
+          ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+          ##[ ##1: #H1; #H2; nelim (list_destruct_cons_nil ??? H2)
+          ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize;
+                   nrewrite > (list_destruct_1 … H2);
+                   nrewrite > (H1 hh2 hh2 (refl_eq …));
+                   nnormalize;
+                   nrewrite > (H ll2 H1 (list_destruct_2 … H2));
+                   napply refl_eq
+          ##]
+ ##]
+nqed.
+
+(* ************** *)
+(* NON-EMPTY LIST *)
+(* ************** *)
+
+nlemma symmetric_lennelist : ∀T.∀l1,l2:ne_list T.len_neList T l1 = len_neList T l2 → len_neList T l2 = len_neList T l1.
+ #T; #l1;
+ nelim l1;
+ ##[ ##1: #h; #l2; ncases l2; nnormalize;
+          ##[ ##1: #H; #H1; napply refl_eq
+          ##| ##2: #h; #t; #H; nrewrite > H; napply refl_eq
+          ##]
+ ##| ##2: #h; #l2; ncases l2; nnormalize;
+          ##[ ##1: #h1; #H; #l; #H1; nrewrite < H1; napply refl_eq
+          ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply refl_eq
+          ##]
+ ##]
+nqed.
+
+nlemma symmetric_foldrightnelist2_aux
+ : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:ne_list T1.
+   ∀H1:len_neList T1 l1 = len_neList T1 l2.∀H2:len_neList T1 l2 = len_neList T1 l1.
+  (∀x,y,z.f x y z = f y x z) →
+  fold_right_neList2 T1 T2 f acc l1 l2 H1 = fold_right_neList2 T1 T2 f acc l2 l1 H2.
+ #T1; #T2; #f; #acc; #l1;
+ nelim l1;
+ ##[ ##1: #h; #l2; ncases l2;
+          ##[ ##1: #h1; nnormalize; #H1; #H2; #H3; nrewrite > (H3 h h1 acc); napply refl_eq
+          ##| ##2: #h1; #l; ncases l;
+                   ##[ ##1: #h3; #H1; #H2; #H3;
+                            nchange in H1:(%) with ((S O) = (S (S O)));
+                            nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
+                   ##| ##2: #h3; #l3; #H1; #H2; #H3;
+                            nchange in H1:(%) with ((S O) = (S (S (len_neList ? l3))));
+                            nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
+                   ##]                   
+          ##]
+ ##| ##2: #h3; #l3; #H; #l2; ncases l2;
+          ##[ ##1: #h4; ncases l3;
+                   ##[ ##1: #h5; #H1; #H2; #H3;
+                            nchange in H1:(%) with ((S (S O)) = (S O));
+                            nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
+                   ##| ##2: #h5; #l5; #H1; #H2; #H3;
+                            nchange in H1:(%) with ((S (S (len_neList ? l5))) = (S O));
+                            nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
+                   ##]
+          ##| ##2: #h4; #l4; #H1; #H2; #H3;
+                   nchange in H1:(%) with ((S (len_neList ? l3)) = (S (len_neList ? l4)));
+                   nchange in H2:(%) with ((S (len_neList ? l4)) = (S (len_neList ? l3)));
+                   nchange with ((f h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 ?))) =
+                                 (f h4 h3 (fold_right_neList2 T1 T2 f acc l4 l3 (fold_right_neList2_aux3 T1 h4 h3 l4 l3 ?))));
+                   nrewrite < (H l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 H1) (fold_right_neList2_aux3 T1 h4 h3 l4 l3 H2) H3);
+                   nrewrite > (H3 h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 ?));
+                   napply refl_eq
+          ##]
+ ##]
+nqed.
+
+nlemma symmetric_foldrightnelist2
+ : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:ne_list T1.∀H:len_neList T1 l1 = len_neList T1 l2.
+  (∀x,y,z.f x y z = f y x z) →
+  fold_right_neList2 T1 T2 f acc l1 l2 H = fold_right_neList2 T1 T2 f acc l2 l1 (symmetric_lennelist T1 l1 l2 H).
+ #T1; #T2; #f; #acc; #l1; #l2; #H; #H1;
+ nrewrite > (symmetric_foldrightnelist2_aux T1 T2 f acc l1 l2 H (symmetric_lennelist T1 l1 l2 H) H1);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_bfoldrightnelist2
+ : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
+  (∀x,y.f x y = f y x) →
+  bfold_right_neList2 T1 f l1 l2 = bfold_right_neList2 T1 f l2 l1.
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #hh1; #l2; ncases l2;
+          ##[ ##1: #hh2; #H; nnormalize; nrewrite > (H hh1 hh2); napply refl_eq
+          ##| ##2: #hh2; #ll2; #H; nnormalize; napply refl_eq
+          ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+          ##[ ##1: #hh2; #H1; nnormalize; napply refl_eq
+          ##| ##2: #hh2; #ll2; #H1; nnormalize;
+                   nrewrite > (H ll2 H1);
+                   nrewrite > (H1 hh1 hh2);
+                   napply refl_eq
+          ##]
+ ##]
+nqed.
+
+nlemma bfoldrightnelist2_to_eq
+ : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
+   (∀x,y.(f x y = true → x = y)) →
+   (bfold_right_neList2 T1 f l1 l2 = true → l1 = l2).
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #hh1; #l2; ncases l2;
+          ##[ ##1: #hh2; #H; #H1; nnormalize in H1:(%); nrewrite > (H hh1 hh2 H1); napply refl_eq
+          ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; napply (bool_destruct … H1)
+          ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+          ##[ ##1: #hh2; #H1; nnormalize; #H2; napply (bool_destruct … H2)
+          ##| ##2: #hh2; #ll2; #H1; #H2;
+                   nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = true);
+                   nrewrite > (H1 hh1 hh2 (andb_true_true_l … H2));
+                   nrewrite > (H ll2 H1 (andb_true_true_r … H2));
+                   napply refl_eq
+          ##]
+ ##]
+nqed.
+
+nlemma eq_to_bfoldrightnelist2
+ : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
+   (∀x,y.(x = y → f x y = true)) →
+   (l1 = l2 → bfold_right_neList2 T1 f l1 l2 = true).
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #hh1; #l2; ncases l2;
+          ##[ ##1: #hh2; #H; #H1; nnormalize;
+                   nrewrite > (H hh1 hh2 (nelist_destruct_nil_nil … H1));
+                   napply refl_eq
+          ##| ##2: #hh2; #ll2; #H; #H1; nelim (nelist_destruct_nil_cons ???? H1)
+          ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+          ##[ ##1: #hh2; #H1; #H2; nelim (nelist_destruct_cons_nil ???? H2)
+          ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize;
+                   nrewrite > (nelist_destruct_cons_cons_1 … H2);
+                   nrewrite > (H1 hh2 hh2 (refl_eq …));
+                   nnormalize;
+                   nrewrite > (H ll2 H1 (nelist_destruct_cons_cons_2 … H2));
+                   napply refl_eq
+          ##]
+ ##]
+nqed.
+
+nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l.
+ #T; #l;
+ ncases l;
+ nnormalize;
+ ##[ ##1: #H; napply I
+ ##| ##2: #x; #l; #H; napply (bool_destruct … H)
+ ##]
+nqed.
+
+nlemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l.
+ #T; #l;
+ ncases l;
+ nnormalize;
+ ##[ ##1: #H; napply (bool_destruct … H)
+ ##| ##2: #x; #l; #H; napply I
+ ##]
+nqed.
diff --git a/helm/software/matita/contribs/ng_assembly/common/nat.ma b/helm/software/matita/contribs/ng_assembly/common/nat.ma
index 874ab7d8c..7e9ec23e4 100755
--- a/helm/software/matita/contribs/ng_assembly/common/nat.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/nat.ma
@@ -49,6 +49,20 @@ nlet rec le_nat n m ≝
    [ O ⇒ false | (S q) ⇒ le_nat p q ]
   ].
 
+interpretation "natural 'less or equal to'" 'leq x y = (le_nat x y).
+
+ndefinition lt_nat ≝ λn1,n2:nat.(le_nat n1 n2) ⊗ (⊖ (eq_nat n1 n2)).
+
+interpretation "natural 'less than'" 'lt x y = (lt_nat x y).
+
+ndefinition ge_nat ≝ λn1,n2:nat.(⊖ (le_nat n1 n2)) ⊕ (eq_nat n1 n2).
+
+interpretation "natural 'greater or equal to'" 'geq x y = (ge_nat x y).
+
+ndefinition gt_nat ≝ λn1,n2:nat.⊖ (le_nat n1 n2).
+
+interpretation "natural 'greater than'" 'gt x y = (gt_nat x y).
+
 nlet rec plus (n1,n2:nat) on n1 ≝ 
  match n1 with
   [ O ⇒ n2
diff --git a/helm/software/matita/contribs/ng_assembly/common/string.ma b/helm/software/matita/contribs/ng_assembly/common/string.ma
new file mode 100644
index 000000000..8763ec8fc
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/common/string.ma
@@ -0,0 +1,52 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(*                          Progetto FreeScale                            *)
+(*                                                                        *)
+(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
+(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*                                                                        *)
+(* ********************************************************************** *)
+
+include "common/ascii.ma".
+include "common/list_utility.ma".
+
+(* ************************ *)
+(* MANIPOLAZIONE DI STRINGA *)
+(* ************************ *)
+
+(* tipo pubblico *)
+ndefinition aux_str_type ≝ list ascii.
+
+(* strcmp *)
+ndefinition eq_str ≝
+ bfold_right_list2 ascii (λx,y.eq_ascii x y).
+
+(* ************ *)
+(* STRINGA + ID *)
+(* ************ *)
+
+(* tipo pubblico *)
+nrecord strId : Type ≝
+ {
+ str_elem: aux_str_type;
+ id_elem: nat
+ }.
+
+(* confronto *)
+ndefinition eq_strId ≝
+λsid,sid':strId.
+ (eq_str (str_elem sid) (str_elem sid'))⊗
+ (eq_nat (id_elem sid) (id_elem sid')).
diff --git a/helm/software/matita/contribs/ng_assembly/common/string_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/string_lemmas.ma
new file mode 100755
index 000000000..67590ae1e
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/common/string_lemmas.ma
@@ -0,0 +1,101 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(*                          Progetto FreeScale                            *)
+(*                                                                        *)
+(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
+(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*                                                                        *)
+(* ********************************************************************** *)
+
+include "common/string.ma".
+include "common/ascii_lemmas2.ma".
+include "common/list_utility_lemmas.ma".
+
+(* ************************ *)
+(* MANIPOLAZIONE DI STRINGA *)
+(* ************************ *)
+
+nlemma symmetric_eqstr : symmetricT (list ascii) bool eq_str.
+ #s1; #s2;
+ napply (symmetric_bfoldrightlist2 ascii eq_ascii s1 s2 symmetric_eqascii).
+nqed.
+
+nlemma eqstr_to_eq : ∀s,s'.eq_str s s' = true → s = s'.
+ #s1; #s2;
+ napply (bfoldrightlist2_to_eq ascii eq_ascii s1 s2 eqascii_to_eq).
+nqed.
+
+nlemma eq_to_eqstr : ∀s,s'.s = s' → eq_str s s' = true.
+ #s1; #s2;
+ napply (eq_to_bfoldrightlist2 ascii eq_ascii s1 s2 eq_to_eqascii).
+nqed.
+
+(* ************ *)
+(* STRINGA + ID *)
+(* ************ *)
+
+nlemma strid_destruct_1 : ∀x1,x2,y1,y2.mk_strId x1 y1 = mk_strId x2 y2 → x1 = x2.
+ #x1; #x2; #y1; #y2; #H;
+ nchange with (match mk_strId x2 y2 with [ mk_strId a _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma strid_destruct_2 : ∀x1,x2,y1,y2.mk_strId x1 y1 = mk_strId x2 y2 → y1 = y2.
+ #x1; #x2; #y1; #y2; #H;
+ nchange with (match mk_strId x2 y2 with [ mk_strId _ b ⇒ y1 = b ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_eqstrid : symmetricT strId bool eq_strId.
+ #si1; #si2;
+ nchange with (
+  ((eq_str (str_elem si1) (str_elem si2))⊗(eq_nat (id_elem si1) (id_elem si2))) =
+  ((eq_str (str_elem si2) (str_elem si1))⊗(eq_nat (id_elem si2) (id_elem si1))));
+ nrewrite > (symmetric_eqstr (str_elem si1) (str_elem si2));
+ nrewrite > (symmetric_eqnat (id_elem si1) (id_elem si2));
+ napply refl_eq.
+nqed. 
+
+nlemma eqstrid_to_eq : ∀s,s'.eq_strId s s' = true → s = s'.
+ #si1; #si2;
+ nelim si1;
+ #l1; #n1;
+ nelim si2;
+ #l2; #n2; #H;
+ nchange in H:(%) with (((eq_str l1 l2)⊗(eq_nat n1 n2)) = true);
+ nrewrite > (eqstr_to_eq l1 l2 (andb_true_true_l … H));
+ nrewrite > (eqnat_to_eq n1 n2 (andb_true_true_r … H));
+ napply refl_eq.
+nqed.
+
+nlemma eq_to_eqstrid : ∀s,s'.s = s' → eq_strId s s' = true.
+ #si1; #si2;
+ nelim si1;
+ #l1; #n1;
+ nelim si2;
+ #l2; #n2; #H;
+ nchange with (((eq_str l1 l2)⊗(eq_nat n1 n2)) = true);
+ nrewrite > (strid_destruct_1 … H);
+ nrewrite > (strid_destruct_2 … H);
+ nrewrite > (eq_to_eqstr l2 l2 (refl_eq …));
+ nrewrite > (eq_to_eqnat n2 n2 (refl_eq …));
+ nnormalize;
+ napply refl_eq.
+nqed.
diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends
index e9d1d4c63..adad69897 100644
--- a/helm/software/matita/contribs/ng_assembly/depends
+++ b/helm/software/matita/contribs/ng_assembly/depends
@@ -9,10 +9,12 @@ common/ascii_lemmas1.ma common/ascii.ma
 num/word16_lemmas.ma num/byte8_lemmas.ma num/word16.ma
 common/prod.ma num/bool.ma
 common/ascii_lemmas2.ma common/ascii_lemmas1.ma num/bool_lemmas.ma
+common/list_utility_lemmas.ma common/list_lemmas.ma common/list_utility.ma
+common/string_lemmas.ma common/ascii_lemmas2.ma common/list_utility_lemmas.ma common/string.ma
 num/bool_lemmas.ma num/bool.ma
 common/nat_lemmas.ma common/nat.ma num/bool_lemmas.ma
-num/exadecim_lemmas.ma num/bool_lemmas.ma num/exadecim.ma
 common/option_lemmas.ma common/option.ma num/bool_lemmas.ma
+num/exadecim_lemmas.ma num/bool_lemmas.ma num/exadecim.ma
 num/exadecim.ma common/prod.ma num/bool.ma num/oct.ma num/quatern.ma
 common/theory.ma 
 num/quatern.ma num/bool.ma
@@ -24,6 +26,8 @@ common/option.ma num/bool.ma
 common/prod_lemmas.ma common/prod.ma num/bool_lemmas.ma
 num/bool.ma common/theory.ma
 num/word16.ma num/byte8.ma
+common/string.ma common/ascii.ma common/list_utility.ma
 common/ascii.ma num/bool.ma
 common/list.ma common/theory.ma
+common/list_utility.ma common/list.ma common/nat_lemmas.ma common/option.ma
 num/bitrigesim_lemmas.ma num/bitrigesim.ma num/bool_lemmas.ma