Aggiornamento alla negazione.

[helm.git] / helm / software / matita / nlibrary / basics / list.ma

diff --git a/helm/software/matita/nlibrary/basics/list.ma b/helm/software/matita/nlibrary/basics/list.ma
index 62210608a5005d79cf8d0c4fae550feda7104cad..d30ed7dfc2a4833f503224f940b7d37c2a866392 100644 (file)
--- a/helm/software/matita/nlibrary/basics/list.ma
+++ b/helm/software/matita/nlibrary/basics/list.ma
@@ -39,7 +39,7 @@ ndefinition not_nil: ∀A:Type.list A → Prop ≝
 
 ntheorem nil_cons:
   ∀A:Type.∀l:list A.∀a:A. a::l ≠ [].
-  #A; #l; #a; #Heq; nchange with (not_nil ? (a::l));
+  #A; #l; #a; napply nmk; #Heq; nchange with (not_nil ? (a::l));
   nrewrite > Heq; //;
 nqed.
 
@@ -54,7 +54,12 @@ nlet rec append A (l1: list A) l2 on l1 :=
   [ nil ⇒  l2
   | cons hd tl ⇒  hd :: append A tl l2 ].
 
-ndefinition tail := λA:Type.λl: list A.
+ndefinition hd ≝ λA:Type.λl: list A.λd:A.
+  match l with 
+  [ nil ⇒ d
+  | cons a _ ⇒ a].
+
+ndefinition tail ≝  λA:Type.λl: list A.
   match l with
   [ nil ⇒  []
   | cons hd tl ⇒  tl].
@@ -74,7 +79,22 @@ ntheorem cons_append_commute:
 //; nqed.
 
 ntheorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
-/2/; nqed.
+#A; #a; #l; #l1; napply symmetric_eq.
+napply associative_append.
+(* /2/; *) nqed.
+
+ntheorem nil_append_elim: ∀A.∀l1,l2: list A.∀P: list A → list A → Prop. 
+  l1@l2 = [] → P (nil A) (nil A) → P l1 l2.
+#A;#l1; #l2; #P; ncases l1; nnormalize;//;
+#a; #l3; #heq; ndestruct;
+nqed.
+
+ntheorem nil_to_nil:  ∀A.∀l1,l2:list A.
+  l1@l2 = [] → l1 = [] ∧ l2 = [].
+#A; #l1; #l2; #isnil; napply (nil_append_elim A l1 l2);/2/;
+nqed.
+
+(* ierators *)
 
 nlet rec map (A,B:Type) (f: A → B) (l:list A) on l: list B ≝
  match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].