definition tail ≝ λA.λl: list A.
match l with [ nil ⇒ [] | cons hd tl ⇒ tl].
+
+definition option_hd ≝
+ λA.λl:list A. match l with
+ [ nil ⇒ None ?
+ | cons a _ ⇒ Some ? a ].
interpretation "append" 'append l1 l2 = (append ? l1 l2).
#A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /2/
qed.
+lemma cons_injective_l : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → a1 = a2.
+#A #a1 #a2 #l1 #l2 #Heq destruct //
+qed.
+
+lemma cons_injective_r : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → l1 = l2.
+#A #a1 #a2 #l1 #l2 #Heq destruct //
+qed.
+
(**************************** iterators ******************************)
let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
#A #B #l #f elim l // #a #tl #Hind normalize //
qed.
+lemma length_reverse: ∀A.∀l:list A.
+ |reverse A l| = |l|.
+#A #l elim l // #a #l0 #IH >reverse_cons >length_append normalize //
+qed.
+
+(****************** traversing two lists in parallel *****************)
+lemma list_ind2 :
+ ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.
+ length ? l1 = length ? l2 →
+ (P [] []) →
+ (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) →
+ P l1 l2.
+#T1 #T2 #l1 #l2 #P #Hl #Pnil #Pcons
+generalize in match Hl; generalize in match l2;
+elim l1
+[#l2 cases l2 // normalize #t2 #tl2 #H destruct
+|#t1 #tl1 #IH #l2 cases l2
+ [normalize #H destruct
+ |#t2 #tl2 #H @Pcons @IH normalize in H; destruct // ]
+]
+qed.
+
+lemma list_cases2 :
+ ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:Prop.
+ length ? l1 = length ? l2 →
+ (l1 = [] → l2 = [] → P) →
+ (∀hd1,hd2,tl1,tl2.l1 = hd1::tl1 → l2 = hd2::tl2 → P) → P.
+#T1 #T2 #l1 #l2 #P #Hl @(list_ind2 … Hl)
+[ #Pnil #Pcons @Pnil //
+| #tl1 #tl2 #hd1 #hd2 #IH1 #IH2 #Hp @Hp // ]
+qed.
+
+(*********************** properties of append ***********************)
+lemma append_l1_injective :
+ ∀A.∀l1,l2,l3,l4:list A. |l1| = |l2| → l1@l3 = l2@l4 → l1 = l2.
+#a #l1 #l2 #l3 #l4 #Hlen @(list_ind2 … Hlen) //
+#tl1 #tl2 #hd1 #hd2 #IH normalize #Heq destruct @eq_f /2/
+qed.
+
+lemma append_l2_injective :
+ ∀A.∀l1,l2,l3,l4:list A. |l1| = |l2| → l1@l3 = l2@l4 → l3 = l4.
+#a #l1 #l2 #l3 #l4 #Hlen @(list_ind2 … Hlen) normalize //
+#tl1 #tl2 #hd1 #hd2 #IH normalize #Heq destruct /2/
+qed.
+
+lemma append_l1_injective_r :
+ ∀A.∀l1,l2,l3,l4:list A. |l3| = |l4| → l1@l3 = l2@l4 → l1 = l2.
+#a #l1 #l2 #l3 #l4 #Hlen #Heq lapply (eq_f … (reverse ?) … Heq)
+>reverse_append >reverse_append #Heq1
+lapply (append_l2_injective … Heq1) [ // ] #Heq2
+lapply (eq_f … (reverse ?) … Heq2) //
+qed.
+
+lemma append_l2_injective_r :
+ ∀A.∀l1,l2,l3,l4:list A. |l3| = |l4| → l1@l3 = l2@l4 → l3 = l4.
+#a #l1 #l2 #l3 #l4 #Hlen #Heq lapply (eq_f … (reverse ?) … Heq)
+>reverse_append >reverse_append #Heq1
+lapply (append_l1_injective … Heq1) [ // ] #Heq2
+lapply (eq_f … (reverse ?) … Heq2) //
+qed.
+
+lemma length_rev_append: ∀A.∀l,acc:list A.
+ |rev_append ? l acc| = |l|+|acc|.
+#A #l elim l // #a #tl #Hind normalize
+#acc >Hind normalize //
+qed.
+
+(****************************** mem ********************************)
+let rec mem A (a:A) (l:list A) on l ≝
+ match l with
+ [ nil ⇒ False
+ | cons hd tl ⇒ a=hd ∨ mem A a tl
+ ].
+
+(***************************** split *******************************)
+let rec split_rev A (l:list A) acc n on n ≝
+ match n with
+ [O ⇒ 〈acc,l〉
+ |S m ⇒ match l with
+ [nil ⇒ 〈acc,[]〉
+ |cons a tl ⇒ split_rev A tl (a::acc) m
+ ]
+ ].
+
+definition split ≝ λA,l,n.
+ let 〈l1,l2〉 ≝ split_rev A l [] n in 〈reverse ? l1,l2〉.
+
+lemma split_rev_len: ∀A,n,l,acc. n ≤ |l| →
+ |\fst (split_rev A l acc n)| = n+|acc|.
+#A #n elim n // #m #Hind *
+ [normalize #acc #Hfalse @False_ind /2/
+ |#a #tl #acc #Hlen normalize >Hind
+ [normalize // |@le_S_S_to_le //]
+ ]
+qed.
+
+lemma split_len: ∀A,n,l. n ≤ |l| →
+ |\fst (split A l n)| = n.
+#A #n #l #Hlen normalize >(eq_pair_fst_snd ?? (split_rev …))
+normalize >length_reverse >(split_rev_len … [ ] Hlen) normalize //
+qed.
+
+lemma split_rev_eq: ∀A,n,l,acc. n ≤ |l| →
+ reverse ? acc@ l =
+ reverse ? (\fst (split_rev A l acc n))@(\snd (split_rev A l acc n)).
+ #A #n elim n //
+ #m #Hind *
+ [#acc whd in ⊢ ((??%)→?); #False_ind /2/
+ |#a #tl #acc #Hlen >append_cons <reverse_single <reverse_append
+ @(Hind tl) @le_S_S_to_le @Hlen
+ ]
+qed.
+
+lemma split_eq: ∀A,n,l. n ≤ |l| →
+ l = (\fst (split A l n))@(\snd (split A l n)).
+#A #n #l #Hlen change with ((reverse ? [ ])@l) in ⊢ (??%?);
+>(split_rev_eq … Hlen) normalize
+>(eq_pair_fst_snd ?? (split_rev A l [] n)) %
+qed.
+
+lemma split_exists: ∀A,n.∀l:list A. n ≤ |l| →
+ ∃l1,l2. l = l1@l2 ∧ |l1| = n.
+#A #n #l #Hlen @(ex_intro … (\fst (split A l n)))
+@(ex_intro … (\snd (split A l n))) % /2/
+qed.
+
(****************************** nth ********************************)
let rec nth n (A:Type[0]) (l:list A) (d:A) ≝
match n with
qed.
lemma length_ltl: ∀A,n,l. |ltl A l n| = |l| - n.
-#A #n elim n -n /2/
+#A #n elim n -n //
#n #IHn *; normalize /2/
qed.