right associative with precedence 46
for @{'ne_cons $hd $tl}.
-notation "« y break £ list0 x sep ; break »"
+notation "« list0 x sep ; break £ y break »"
non associative with precedence 90
for ${fold right @{'ne_nil $y } rec acc @{'ne_cons $x $acc}}.
right associative with precedence 47
for @{'ne_append $l1 $l2 }.
-interpretation "ne_nil" 'ne_nil hd = (ne_nil _ hd).
-interpretation "ne_cons" 'ne_cons hd tl = (ne_cons _ hd tl).
-interpretation "ne_append" 'ne_append l1 l2 = (ne_append _ l1 l2).
+interpretation "ne_nil" 'ne_nil hd = (ne_nil ? hd).
+interpretation "ne_cons" 'ne_cons hd tl = (ne_cons ? hd tl).
+interpretation "ne_append" 'ne_append l1 l2 = (ne_append ? l1 l2).
(* ************ *)
(* List Utility *)
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 ≝
normalize; autobatch ]
qed.
+definition isnot_empty_list ≝
+λT:Type.λl:list T.match l with [ nil ⇒ False | cons _ _ ⇒ True ].
+
+definition isnotb_empty_list ≝
+λT:Type.λl:list T.match l with [ nil ⇒ false | cons _ _ ⇒ true ].
+
+lemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l.
+ unfold isnotb_empty_list;
+ unfold isnot_empty_list;
+ intros;
+ elim l;
+ [ normalize; autobatch |
+ 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 *)
(* ******** *)