X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Fcompiler%2Futility.ma;h=c67298d390673fe02d0519d1241ed2e84a389133;hb=aba1baf85bb8e6b3ea3e66a8c2d07601066d26bc;hp=4352dc426ce24939cf091534d25c48979e514d83;hpb=21f1fb39b5e1187ef87387f20522e60abe4f7c19;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/compiler/utility.ma b/helm/software/matita/contribs/assembly/compiler/utility.ma
index 4352dc426..c67298d39 100755
--- a/helm/software/matita/contribs/assembly/compiler/utility.ma
+++ b/helm/software/matita/contribs/assembly/compiler/utility.ma
@@ -40,7 +40,7 @@ notation "hvbox(hd break §§ tl)"
   right associative with precedence 46
   for @{'ne_cons $hd $tl}.
 
-notation "« y £ break list0 x sep ; »"
+notation "« list0 x sep ; break £ y break »"
   non associative with precedence 90
   for ${fold right @{'ne_nil $y } rec acc @{'ne_cons $x $acc}}.
 
@@ -61,18 +61,14 @@ let rec neList_to_list (T:Type) (p_l:ne_list T) on p_l ≝
  match p_l with [ ne_nil h ⇒ [h] | ne_cons h t ⇒ [h]@neList_to_list T t ].
 
 let rec list_to_neList (T:Type) (p_l:list T) on p_l ≝
- match p_l with [ nil ⇒ None (ne_list T) | cons h t ⇒ match list_to_neList T t with [ None ⇒ Some ? «h£» | Some t' ⇒ Some ? («h£»&t') ]].
+ match p_l with [ nil ⇒ None (ne_list T) | cons h t ⇒ match list_to_neList T t with [ None ⇒ Some ? «£h» | Some t' ⇒ Some ? («£h»&t') ]].
 
 (* listlen *)
-let rec len_list_aux (T:Type) (p_l:list T) (c:nat) on p_l ≝
- match p_l with [ nil ⇒ c | cons _ t ⇒ len_list_aux T t (S c) ].
+let rec len_list (T:Type) (p_l:list T) on p_l ≝
+ match p_l with [ nil ⇒ O | cons _ t ⇒ S (len_list T t) ].
 
-definition len_list ≝ λT:Type.λl:list T.len_list_aux T l O.
-
-let rec len_neList_aux (T:Type) (p_l:ne_list T) (c:nat) on p_l ≝
- match p_l with [ ne_nil _ ⇒ (S c) | ne_cons _ t ⇒ len_neList_aux T t (S c) ].
-
-definition len_neList ≝ λT:Type.λl:ne_list T.len_neList_aux T l O.
+let rec len_neList (T:Type) (p_l:ne_list T) on p_l ≝
+ match p_l with [ ne_nil _ ⇒ 1 | ne_cons _ t ⇒ S (len_neList T t) ].
 
 (* nth elem *)
 let rec nth_list (T:Type) (l:list T) (n:nat) on l ≝
@@ -134,6 +130,28 @@ definition cut_last_neList ≝
  [ ne_nil h ⇒ ne_nil T h
  | ne_cons _ t ⇒ reverse_neList T t ].
 
+(* getFirst *)
+definition get_first_list ≝
+λT:Type.λl:list T.match l with
+ [ nil ⇒ None ?
+ | cons h _ ⇒ Some ? h ].
+
+definition get_first_neList ≝
+λT:Type.λl:ne_list T.match l with
+ [ ne_nil h ⇒ h
+ | ne_cons h _ ⇒ h ].
+
+(* cutFirst *)
+definition cut_first_list ≝
+λT:Type.λl:list T.match l with
+ [ nil ⇒ nil T
+ | cons _ t ⇒ t ].
+
+definition cut_first_neList ≝
+λT:Type.λl:ne_list T.match l with
+ [ ne_nil h ⇒ ne_nil T h
+ | ne_cons _ t ⇒ t ].
+
 (* apply f *)
 let rec apply_f_list (T1,T2:Type) (l:list T1) (f:T1 → T2) on l ≝
 match l with
@@ -180,6 +198,22 @@ lemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empt
    normalize; autobatch ]
 qed.
 
+lemma isempty_to_eq : ∀T,l.isb_empty_list T l = true → l = [].
+ do 2 intro;
+ elim l 0;
+ [ 1: intro; reflexivity
+ | 2: intros; normalize in H1:(%); destruct H1
+ ].
+qed.
+
+lemma eq_to_isempty : ∀T,l.l = [] → isb_empty_list T l = true.
+ do 2 intro;
+ elim l 0;
+ [ 1: intro; reflexivity
+ | 2: intros; destruct H1
+ ]
+qed. 
+
 (* ******** *)
 (* naturali *)
 (* ******** *)