# Library Kildall.lists.lists

Ltac CaseEq f:=generalize (refl_equal f); pattern f at -1 in |- *; case f.

Section lists.

Require Export List.
Require Export Arith.
Variable A : Set.

Fixpoint split_k_elements (k : nat) (l : list A) {struct l} : option (list A * list A) :=
match l, k with
| _, 0 => Some (nil,l)
| h :: t, S k' =>
match split_k_elements k' t with
| Some (l', r') => Some ((h :: l'), r')
| None => None
end
| _, _ => None
end.

Lemma split_k_elements_ok : forall (k : nat) (l lk lr: list A),
split_k_elements k l = Some (lk, lr) -> l = lk ++ lr.
Proof.
intros k l; generalize k; clear k.
induction l; simpl.
destruct k; intros lk lr H; inversion H.
simpl; trivial.
destruct k; intros lk lr.
intro H; inversion H; simpl; trivial.
generalize (IHl k); destruct (split_k_elements k l).
destruct p as [lk' lr'].
intro H; cut (l = lk'++lr').
intro; subst l.
intro H'; inversion H'; simpl; trivial.
apply (H lk' lr'); trivial.
intros H H'; inversion H'.
Qed.

Lemma split_k_elements_length : forall (k : nat) (l lk lr : list A),
split_k_elements k l = Some (lk, lr) -> length lk = k.
Proof.
intros k l; generalize k; clear k; induction l; intros k lk lr; simpl.
destruct k; intro H; inversion H.
simpl; trivial.
destruct k.
intro H; inversion H; simpl; trivial.
simpl; generalize (IHl k); clear IHl; intro IHl.
destruct (split_k_elements k l).
destruct p.
intro h; inversion h; subst lk; subst lr.
simpl; generalize (IHl l0 l1).
auto with arith.
intro h; inversion h.
Qed.

Lemma split_k_elements_some : forall (k : nat) (l lk lr : list A),
split_k_elements k l = Some (lk, lr) -> k <= length l.
Proof.
intros k l; generalize k; clear k; induction l.
intros k lk lr H; cut (length lk = k); [intro Hlen | generalize H; apply split_k_elements_length].
simpl in H; destruct k.
simpl; auto with arith.
inversion H.
intros k lk lr H; destruct k; simpl.
auto with arith.
simpl in H; generalize H; clear H.
CaseEq (split_k_elements k l); simpl.
intros p case; destruct p as [lk' lr'].
intro H; inversion H; subst.
cut (k <= length l); [auto with arith | apply (IHl k lk' lr)].
assumption.
intros dd F; inversion F.
Qed.

Lemma split_k_elements_none : forall (k : nat) (l : list A),
split_k_elements k l = None -> length l < k.
Proof.
intros k l; generalize k; clear k; induction l.
intro k; destruct k; simpl.
intro H; inversion H.
auto with arith.
intro k; destruct k; simpl.
intro H; inversion H.
CaseEq (split_k_elements k l).
intros p case; destruct p as [lk lr].
intro F; inversion F.
intros case dd; clear dd; cut (length l < k); [auto with arith | apply IHl; auto].
Qed.

Fixpoint element_at_list (l : list A) (k : nat) {struct l} : option A :=
match l with
| nil => None
| h :: t =>
match k with
| 0 => Some h
| S k' => element_at_list t k'
end
end.

Notation "l '[' k ']'" := (element_at_list l k) (at level 50).

Lemma element_at_list_some : forall (l : list A) (k : nat) (e : A),
l[k] = Some e -> k < length l.
Proof.
induction l; simpl; intros k e H.
inversion H.
destruct k.
inversion H; subst a.
auto with arith.
cut (k < length l); [auto with arith | CaseEq (l[k])].
intros a0 He.
rewrite He in H; inversion H; subst a0.
apply (IHl k e); auto.
intro He; rewrite He in H; inversion H.
Qed.

Lemma element_at_list_none : forall (l : list A) (k : nat),
l[k] = None -> k >= length l.
Proof.
induction l; simpl; intros k H.
auto with arith.
destruct k.
inversion H.
cut (k >= length l); [auto with arith | CaseEq (l[k])].
intros ao Ha0.
rewrite Ha0 in H; inversion H.
apply IHl.
Qed.

Lemma element_at_list_in : forall (l : list A) (k : nat) (e : A),
l[k] = Some e -> In e l.
Proof.
induction l; simpl; intros k e H.
inversion H.
destruct k.
inversion H; left; trivial.
right; generalize H; clear H; CaseEq (l[k]).
intros a0 case_a0 H; inversion H; subst; apply (IHl k); trivial.
intros dd F; inversion F.
Qed.

Lemma element_at_list_concat : forall (l l' : list A) (k : nat),
(l++l')[length l + k] = l'[k].
Proof.
induction l.
simpl; trivial.
intros l' k.
simpl.
rewrite (IHl l' k).
destruct (l'[k]); simpl; trivial.
Qed.

Lemma element_at_list_concat' : forall (l l' : list A) (k : nat),
k < length l -> l[k] = (l++l')[k].
Proof.
induction l; simpl.
intros l' k Ck; inversion Ck.
intros l' k Ck; destruct k.
trivial.
cut (k < length l); [intro C | generalize Ck; auto with arith].
rewrite (IHl l' k C).
trivial.
Qed.

Remark list_concat_cons : forall (l l' : list A) (t : A),
l ++ (t :: l') = (l ++ (t::nil)) ++ l'.
Proof.
induction l; simpl.
trivial.
intros l' t'; rewrite <- IHl.
trivial.
Qed.

Lemma list_tail : forall (l : list A), l <> nil ->
ex (fun (t : A) => ex (fun (l' : list A) => l = l' ++ (t::nil))).
Proof.
induction l as [|t l IHl].
intro F; elim F; trivial.
intro H.
destruct l as [|t' l']; simpl.
exists t; exists (nil (A := A)).
simpl; trivial.
clear H.
cut (t' :: l' <> nil); [intro h; generalize (IHl h); clear h IHl | intro F; inversion F].
intro h; elim h; clear h; intros t1 h; elim h; clear h; intros l1 h.
rewrite h.
exists t1.
exists (t :: l1).
simpl; trivial.
Qed.

Remark list_concat_nil : forall (l : list A), l ++ nil = l.
Proof.
induction l; simpl; trivial.
rewrite IHl; trivial.
Qed.

Fixpoint push_list (l stack : list A) {struct l} : list A :=
match l with
| nil => stack
| h :: t => push_list t (h :: stack)
end.

Lemma push_list_is_app_rev : forall (l stack : list A),
push_list l stack = (rev l) ++ stack.
Proof.
intro l; induction l as [ | h t IHl]; simpl; intro stack.
trivial.
rewrite (IHl (h :: stack)).
apply list_concat_cons.
Qed.

Definition rev_lin (l : list A) := push_list l nil.

Lemma rev_lin_is_rev : forall (l : list A), rev_lin l = rev l.
Proof.
intro l; unfold rev_lin; rewrite push_list_is_app_rev.
apply list_concat_nil.
Qed.

Fact rev_length : forall (l : list A), length (rev l) = length l.
Proof.
induction l; simpl; trivial.
rewrite <- IHl.
clear IHl; induction (rev l); simpl; trivial.
rewrite IHl0; trivial.
Qed.

Lemma element_at_list_rev : forall (l : list A) (k : nat),
k < length l -> l[k] = (rev l)[length l - (S k)].
Proof.
induction l; simpl.
trivial.
intros k Ck.
destruct k.
simpl.
clear IHl.
generalize (element_at_list_concat (rev l) (a::nil) 0).
replace (length (rev l) + 0) with (length l - 0).
intro H; rewrite H.
simpl; trivial.
rewrite plus_comm; simpl.
rewrite <- minus_n_O.
symmetry; apply rev_length.
cut (k < length l); [intro C | generalize Ck; auto with arith].
rewrite (IHl k C).
rewrite (element_at_list_concat' (rev l) (a::nil) (length l - S k)).
destruct ((rev l ++ a :: nil)[length l - S k]); simpl; trivial.
clear Ck.
rewrite rev_length.
auto with arith.
Qed.

Lemma concat_length : forall (l l' : list A), length (l++l') = length l + length l'.
Proof.
induction l; simpl.
trivial.
intro l'; rewrite (IHl l').
trivial.
Qed.

Lemma map_id : forall (l : list A),
map (fun e : A => e) l = l.
Proof.
induction l.
trivial.
simpl; rewrite IHl; trivial.
Qed.

Fact cons_eq : forall (h h' : A) (t t' : list A),
h :: t = h' :: t' -> h = h' /\ t = t'.
Proof.
intros h h' t t' H; inversion H; split; trivial.
Qed.

Lemma map_unchanged_elements : forall (f : A -> A) (l : list A),
map f l = l <-> (forall (a : A), In a l -> f a = a).
Proof.
intro f; split.
induction l as [ | h t IHl].
intros Hmap a a_in_nil; inversion a_in_nil.
simpl; intros Hmap a Ha.
elim (cons_eq _ _ _ _ Hmap); intros H1 H2.
elim Ha; clear Ha; intro Ha.
subst h; trivial.
apply IHl; trivial.
induction l as [ | h t IHl].
simpl; trivial.
intro Helems; simpl.
rewrite (Helems h); try left; trivial.
rewrite IHl; trivial.
intros a a_in_t; apply Helems; try right; trivial.
Qed.

End lists.

Implicit Arguments split_k_elements [A].
Implicit Arguments element_at_list [A].
Implicit Arguments push_list [A].
Implicit Arguments rev_lin [A].
Implicit Arguments map_unchanged_elements [A f].

Notation "l '[' k ']'" := (element_at_list l k) (at level 50).

Section fold_bool.

Require Export Bool.
Variable A : Set.
Variable f : A -> bool.

Lemma fold_bool_and_first_false : forall (l : list A),
fold_left (fun (p : bool) (a : A) => p && (f a)) l false = false.
Proof.
induction l as [ | h t IHl]; simpl; trivial.
Qed.

Lemma fold_bool_and_false : forall (l : list A),
fold_left (fun (p : bool) (a : A) => p && (f a)) l true = false <-> ex (fun (a : A) => In a l /\ f a = false).
Proof.
intro l; split.
induction l as [ | h t IHl]; simpl.
intro H; inversion H.
CaseEq (f h); intro case_f_h; simpl.
intro Hfold; elim (IHl Hfold); intros a Ha; elim Ha; clear Ha; intros a_in_t f_a_false.
exists a; split; trivial.
right; assumption.
intro; exists h; split; trivial.
left; trivial.
induction l as [ | h t IHl]; simpl.
intro H; elim H; clear H; intros a Ha; elim Ha; intro F; inversion F.
intro Ha; elim Ha; clear Ha; intros a Ha.
elim Ha; clear Ha; intros Ha f_a_false.
elim Ha; clear Ha; intro Ha.
subst a.
rewrite f_a_false; apply fold_bool_and_first_false.
destruct (f h).
apply IHl; exists a; split; trivial.
apply fold_bool_and_first_false.
Qed.

Lemma fold_bool_and_true : forall (l : list A),
fold_left (fun (p : bool) (a : A) => p && (f a)) l true = true <-> forall (a : A), In a l -> f a = true.
Proof.
split.
induction l as [ | h t IHl]; simpl.
intros dd a F; inversion F.
CaseEq (f h); intro case_f_h; simpl.
intros Hfold a H; elim H; clear H; intro H.
subst a; assumption.
apply (IHl Hfold a H).
intro H; rewrite fold_bool_and_first_false in H.
inversion H.
induction l as [ | h t IHl]; simpl.
trivial.
intro H; assert (H' : forall a : A, In a t -> f a = true).
intros a a_in_t; apply H; right; assumption.
rewrite (H h).
apply IHl; trivial.
left; trivial.
Qed.

Lemma fold_bool_or_first_true : forall (l : list A),
fold_left (fun (p : bool) (a : A) => p || (f a)) l true = true.
Proof.
induction l as [ | h t IHl]; simpl; trivial.
Qed.

Lemma fold_bool_or_false : forall (l : list A),
fold_left (fun (p : bool) (a : A) => p || (f a)) l false = false <-> forall (a : A), In a l -> f a = false.
Proof.
split.
induction l as [ | h t IHl]; simpl.
intros dd a F; inversion F.
CaseEq (f h); intro case_f_h; simpl.
intros Hfold; rewrite fold_bool_or_first_true in Hfold; inversion Hfold.
intros Hfold a Ha; elim Ha; clear Ha; intro Ha.
subst a; assumption.
apply (IHl Hfold a Ha).
induction l as [ | h t IHl]; simpl.
trivial.
intro H; assert (H' : forall a : A, In a t -> f a = false).
intros a a_in_t; apply H; right; assumption.
rewrite (H h).
apply IHl; trivial.
left; trivial.
Qed.

Lemma fold_bool_or_true : forall (l : list A),
fold_left (fun (p : bool) (a : A) => p || (f a)) l false = true <-> ex (fun (a : A) => In a l /\ f a = true).
Proof.
split.
induction l as [ | h t IHl]; simpl.
intro H; inversion H.
CaseEq (f h); intro case_f_h; simpl.
intro; exists h; split; trivial.
left; trivial.
intro Hfold; elim (IHl Hfold); intros a Ha; elim Ha; clear Ha; intros a_in_t f_a_false.
exists a; split; trivial.
right; assumption.
induction l as [ | h t IHl]; simpl.
intro H; elim H; clear H; intros a Ha; elim Ha; intro F; inversion F.
intro Ha; elim Ha; clear Ha; intros a Ha.
elim Ha; clear Ha; intros Ha f_a_false.
elim Ha; clear Ha; intro Ha.
subst a.
rewrite f_a_false; apply fold_bool_or_first_true.
destruct (f h).
apply fold_bool_or_first_true.
apply IHl; exists a; split; trivial.
Qed.

End fold_bool.

Implicit Arguments fold_bool_and_first_false [A f].
Implicit Arguments fold_bool_and_false [A f].
Implicit Arguments fold_bool_and_true [A f].
Implicit Arguments fold_bool_or_first_true [A f].
Implicit Arguments fold_bool_or_false [A f].
Implicit Arguments fold_bool_or_true [A f].

Lemma map_length : forall (A B : Set) (f : A -> B) (l : list A),
length l = length (map f l).
Proof.
induction l; simpl; trivial.
rewrite IHl; trivial.
Qed.

Lemma element_at_list_map : forall (A B : Set) (l : list A) (f : A->B) (k : nat) (e : A),
l[k] = Some e ->
(map f l)[k] = Some (f e).
Proof.
induction l; simpl.
intros f k e F; inversion F.
intros f k e; destruct k.
intro H; inversion H; trivial.
CaseEq (l[k]).
intros a0 case_a0 H; inversion H; subst; clear H.
rewrite (IHl f k e case_a0); trivial.
intros dd F; inversion F.
Qed.

Lemma element_at_list_map' : forall (A B : Set) (l : list A) (f : A->B) (k : nat) (fe : B),
(map f l)[k] = Some fe -> ex (fun (e : A) => l[k] = Some e /\ fe = f e).
Proof.
induction l; simpl.
intros f k e F; inversion F.
intros f k fe; destruct k.
intro H; inversion H; exists a; split; trivial.
CaseEq ((map f l)[k]).
intros b case_b H; inversion H; subst; clear H.
elim (IHl f k fe case_b); intros e He.
elim He; clear He; intros He1 he2.
subst; exists e; rewrite He1; split; trivial.
intros dd F; inversion F.
Qed.

Lemma map_to_elements : forall (A B : Set) (f g : A -> B) (l : list A),
(forall (a: A), In a l -> f a = g a) <-> map f l = map g l.
Proof.
intros A B f g l; split.
induction l as [ | h t IHl]; intro Helems.
simpl; trivial.
simpl.
rewrite IHl.
rewrite Helems; try left; trivial.
intros a a_in_t; apply Helems; right; trivial.
induction l as [ | h t IHl]; intro Hmap.
intros a a_in_nil; inversion a_in_nil.
intros a Ha; simpl in Hmap; elim (cons_eq _ _ _ _ _ Hmap); intros H1 H2.
elim Ha; clear Ha; intro Ha.
subst; trivial.
apply IHl; trivial.
Qed.

Fact In_concat : forall (A : Set) (l l' : list A) (e : A),
In e (l++l') -> In e l \/ In e l'.
Proof.
induction l; simpl; intros l' e Hincat.
right; trivial.
elim Hincat; clear Hincat; intro Hincat.
subst; left; left; trivial.
elim (IHl l' e Hincat); intro H.
left; right; trivial.
right; trivial.
Qed.

Fact In_rev : forall (A : Set) (l : list A) (e : A),
In e (rev l) -> In e l.
Proof.
induction l; simpl; intros e Hinrev.
trivial.
elim (In_concat A (rev l) (a::nil) e Hinrev); clear Hinrev; intro Hinrev.
right; apply IHl; trivial.
inversion Hinrev.
left; trivial.
inversion H.
Qed.

Fact concat_In : forall (A : Set) (l l' : list A) (e : A),
In e l \/ In e l' -> In e (l++l').
Proof.
induction l; simpl; intros l' e Hincat.
elim Hincat; clear Hincat; intro Hincat.
inversion Hincat.
assumption.
elim Hincat; clear Hincat; intro Hincat.
elim Hincat; clear Hincat; intro Hincat.
left; trivial.
right; apply IHl.
left; trivial.
right; apply IHl.
right; trivial.
Qed.

Lemma tail_neq : forall (A : Set) (l : list A) (e : A), l <> e :: l.
Proof.
induction l; simpl; intros e H; inversion H.
apply (IHl e); trivial.
Qed.

Lemma In_mapped : forall (A B : Set) (fcn : A -> B) (l : list A) (e : B),
In e (map fcn l) -> ex (fun (e' : A) => In e' l /\ e = fcn e').
Proof.
induction l; simpl; intros e Hin.
inversion Hin.
elim Hin; clear Hin; intro Hin.
exists a.
split.
left; trivial.
symmetry; trivial.
elim (IHl e Hin).
intros x Hx; elim Hx; clear Hx; intros Hx1 Hx2.
exists x.
split.
right; assumption.
assumption.
Qed.

Lemma concat_map : forall (A B : Set) (f : A -> B) (l l' : list A),
map f (l++l') = (map f l)++(map f l').
Proof.
induction l.
simpl; trivial.
intro l'; simpl.
rewrite (IHl l'); trivial.
Qed.

Lemma map_rev_commut : forall (A B : Set) (f : A -> B) (l : list A),
map f (rev l) = rev (map f l).
Proof.
induction l; simpl; trivial.
rewrite <- IHl.
rewrite concat_map; simpl; trivial.
Qed.

Lemma rev_map : forall (A B : Set) (f g : A -> B) (l l' : list A),
map f (rev l) = map g (rev l') -> map f l = map g l'.
Proof.
intros A B f g l l' H.
assert (H' : rev (map f l) = rev (map g l')).
rewrite <- map_rev_commut.
rewrite <- map_rev_commut.
assumption.
generalize (map f l) (map g l') H'; clear H H' l l'; intros l l' H.
rewrite <- rev_involutive.
rewrite <- (rev_involutive l).
generalize (rev l) (rev l') H; intros L L' H'; subst; trivial.
Qed.

Lemma compose_map : forall (A B C : Set) (f : A -> B) (g : B -> C) (l : list A),
map g (map f l) = map (fun (a : A) => g (f a )) l.
Proof.
induction l as [ | h t IHl].
simpl; trivial.
simpl; rewrite IHl; trivial.
Qed.