interpretation "nil" 'nil = (nil ?).
interpretation "cons" 'cons hd tl = (cons ? hd tl).
-definition not_nil: ∀A:Type[0].list A → Prop ≝
+definition is_nil: ∀A:Type[0].list A → Prop ≝
λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
theorem nil_cons:
∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
- #A #l #a @nmk #Heq (change with (not_nil ? (a::l))) >Heq //
+ #A #l #a @nmk #Heq (change with (is_nil ? (a::l))) >Heq //
qed.
(*
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.associative (list A) (append A).
#A #l1 #l2 #l3 (elim l1) normalize // qed.
-(* deleterio per auto
-ntheorem cons_append_commute:
- ∀A:Type.∀l1,l2:list A.∀a:A.
- a :: (l1 @ l2) = (a :: l1) @ l2.
-//; nqed. *)
-
theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
#A #a #l #l1 >associative_append // qed.
#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 ≝
theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
#A #B #f #g #l #eqfg (elim l) normalize // qed.
-let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝
-match l1 with
- [ nil ⇒ nil ?
- | cons a tl ⇒ (map ??(mk_Sig ?? a) (g a)) @ dprodl A f tl g
- ].
+(**************************** reverse *****************************)
+let rec rev_append S (l1,l2:list S) on l1 ≝
+ match l1 with
+ [ nil ⇒ l2
+ | cons a tl ⇒ rev_append S tl (a::l2)
+ ]
+.
+
+definition reverse ≝λS.λl.rev_append S l [].
+
+lemma reverse_single : ∀S,a. reverse S [a] = [a].
+// qed.
+
+lemma rev_append_def : ∀S,l1,l2.
+ rev_append S l1 l2 = (reverse S l1) @ l2 .
+#S #l1 elim l1 normalize //
+qed.
+
+lemma reverse_cons : ∀S,a,l. reverse S (a::l) = (reverse S l)@[a].
+#S #a #l whd in ⊢ (??%?); //
+qed.
+
+lemma reverse_append: ∀S,l1,l2.
+ reverse S (l1 @ l2) = (reverse S l2)@(reverse S l1).
+#S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >reverse_cons
+>reverse_cons // qed.
+
+lemma reverse_reverse : ∀S,l. reverse S (reverse S l) = l.
+#S #l elim l // #a #tl #Hind >reverse_cons >reverse_append
+normalize // qed.
+
+(* an elimination principle for lists working on the tail;
+useful for strings *)
+lemma list_elim_left: ∀S.∀P:list S → Prop. P (nil S) →
+(∀a.∀tl.P tl → P (tl@[a])) → ∀l. P l.
+#S #P #Pnil #Pstep #l <(reverse_reverse … l)
+generalize in match (reverse S l); #l elim l //
+#a #tl #H >reverse_cons @Pstep //
+qed.
(**************************** length ******************************)
[ nil ⇒ 0
| cons a tl ⇒ S (length A tl)].
-notation "|M|" non associative with precedence 60 for @{'norm $M}.
+notation "|M|" non associative with precedence 65 for @{'norm $M}.
interpretation "norm" 'norm l = (length ? l).
+lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
+#A #l elim l //
+qed.
+
lemma length_append: ∀A.∀l1,l2:list A.
|l1@l2| = |l1|+|l2|.
#A #l1 elim l1 // normalize /2/
qed.
+lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
+#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.