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.
[ 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].
∀A:Type.associative (list A) (append A).
#A; #l1; #l2; #l3; nelim l1; nnormalize; //; nqed.
+(* deleterio per auto
ntheorem cons_append_commute:
∀A:Type.∀l1,l2:list A.∀a:A.
a :: (l1 @ l2) = (a :: l1) @ l2.
-//; nqed.
+//; nqed. *)
ntheorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
-/2/; nqed.
+#A; #a; #l; #l1; napply sym_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)].