Require Export List.
Require Export tactics.
Require Export Coqlib.

Load param.

Lemma list_inj : forall A (a : A) a' b b', a::b = a'::b' -> (a=a' /\ b=b').
injection 1; auto.
Qed.

Open Scope nat_scope.

Section List_addons.

Variable A : Set.

(** *** List membership. *)

Inductive member
 (e : A) :
list A -> Prop := 
| member_head
    (l : list A) :
  member e (cons e l)
| member_tail
   (l : list A)
   (_ : member e l)
   (a : A) :
  member e (cons a l)
.

Hint Constructors member.

Lemma member_nil : forall x, member x nil -> False.

Proof.
inversion 1.
Qed.

Hint Resolve member_nil.

Lemma member_step : forall x a, x <> a ->
forall l, member x (a::l) -> member x l.
Proof.
intros until 1.
inversion 1 ; subst ; eauto.
contradiction (refl_equal a).
Qed.

Inductive find_in_list : list A -> nat -> A -> Prop :=
| find_in_list_O : forall a l, find_in_list (a::l) O a
| find_in_list_S : forall l n r, find_in_list l n r -> forall a, find_in_list (a::l) (S n) r
.

Hint Constructors find_in_list.

Lemma find_in_list_member : forall l n a,
find_in_list l n a -> member a l.
induction 1; eauto.
Qed.

Lemma member_find_in_list : forall l a, member a l ->
  exists n, find_in_list l n a.
Proof.
induction 1.
esplit.
eauto.
invall.
esplit.
eauto.
Qed.


Section Member_dec.
Hypothesis eq_A_dec : forall x y : A, {x = y} + {x <> y}.

Lemma member_dec : 
forall l x, {member x l} + {member x l -> False}.

Proof.
intros.
induction l.
 right.
 intro Hm ; inversion Hm.
destruct (eq_A_dec x a).
 subst.
 left ; auto.
destruct IHl.
 left ; auto.
 right.
 intro Hm ; inversion Hm ; subst ; [contradiction (refl_equal a) | auto].
Defined.

Lemma member_which_dec :
forall a l x, member x (a::l) -> {x = a} + {member x l}.
Proof.
intros a l x.
destruct (eq_A_dec x a).
auto.
intros Hx.
right.
inversion Hx.
contradiction.
eauto.
Defined.

Definition member_rect_2 : forall (e : A) (P : list A -> Type),
 (forall l : list A, P (e :: l)) ->
       (forall l : list A, member e l -> P l -> forall a : A, P (a :: l)) ->
       forall l : list A, member e l -> P l.
intros e P Hhead Htail.
induction l.
intro Hmem.
apply False_rect.
inversion Hmem.
intro Hmem.
destruct (member_which_dec Hmem).
subst.
apply Hhead.
apply Htail.
trivial.
auto.
Defined.

Definition member_rect : forall (e : A) (P : list A -> Type),
 (forall l, P (e :: l)) ->
       (forall l, member e l -> P l -> forall a, P (a :: l)) ->
       forall l, member e l -> P l.
intros e P Hhead Htail.
induction l.
intro Hmem.
apply False_rect.
inversion Hmem.
intro Hmem.
destruct (member_which_dec Hmem).
subst.
apply Hhead.
eapply Htail.
eassumption.
eauto.
Defined.

Definition find_in_list_constr : forall l e, member e l -> 
{n | find_in_list l n e}.
Proof.
induction 1 using member_rect.
esplit.
eauto.
destruct IHmember.
esplit.
eauto.
Defined.
 

End Member_dec.

(** *** Universal property on all items of a list. *)

Section List_forall.

Variable P : A -> Prop.

Inductive list_forall : list A -> Prop :=
| list_forall_nil : list_forall nil
| list_forall_cons
   (a : A)
   (l : list A) 
   (_ : P a)
   (_ : list_forall l) :
  list_forall (a::l)
.

Hint Constructors list_forall.

Theorem list_forall_correct : forall l,
list_forall l -> forall x, member x l -> P x.

Proof.
induction 1 ; inversion 1 ; auto.
Qed.

Theorem list_forall_complete : forall l,
(forall x, member x l -> P x) -> list_forall l.

Proof.
induction l ; auto.
Qed.

End List_forall.

Hint Constructors list_forall.

Section List_suffix.

Inductive is_suffix_of : list A -> list A -> Prop :=
| is_suffix_of_id : forall l, is_suffix_of l l
| is_suffix_of_cons : forall l m,
  is_suffix_of l m -> forall a,
  is_suffix_of l (a::m)
.

Hint Constructors is_suffix_of.

Lemma suffix_of_nil : forall l, is_suffix_of l nil -> l = nil.

Proof.
inversion 1 ; auto.
Qed.

Lemma suffix_cons : forall l a s, is_suffix_of (a::s) l -> is_suffix_of s l.

Proof.
induction l.
 inversion 1 ; discriminate.
inversion 1 ; subst ; auto.
apply is_suffix_of_cons ; eapply IHl ; eauto.
Qed.

Lemma suffix_refl : forall l, is_suffix_of l l.

Proof is_suffix_of_id.

Lemma suffix_trans : forall s l, is_suffix_of s l -> forall t, is_suffix_of t s -> is_suffix_of t l.

Proof.
 induction 1 ; auto.
Qed.

Lemma suffix_nil_min : forall l, is_suffix_of nil l.

Proof.
induction l ; auto.
Qed.

Lemma suffix_length : forall s l, is_suffix_of s l -> length s <= length l.

Proof.
induction 1 ; simpl ; auto with arith.
Qed.

Lemma suffix_member : forall s l, is_suffix_of s l -> forall m, member m s -> member m l.

Proof.
induction 1 ; auto.
Qed.

End List_suffix.

Hint Constructors is_suffix_of.

(** *** No duplicates

 A list not containing twice the same item. *)

Section List_no_duplicates.

Inductive no_duplicates : list A -> Prop :=
| no_duplicates_nil : no_duplicates nil
| no_duplicates_cons : forall a l,
  (member a l -> False) ->
  no_duplicates l ->
  no_duplicates (cons a l)
.

Hint Constructors no_duplicates.

Lemma no_duplicates_tail : forall a l, 
no_duplicates (a::l) -> no_duplicates l.

Proof.
inversion 1 ; auto.
Qed.

Hint Resolve no_duplicates_tail.

Lemma no_duplicate_suffix : forall s l,
is_suffix_of s l ->
no_duplicates l -> no_duplicates s.

Proof.
induction 1 ; auto.
inversion 1 ; auto.
Qed.

Lemma no_duplicates_correct : forall l,
no_duplicates l -> forall a m,
is_suffix_of (cons a m) l ->
member a m ->
False.

Proof.
intros.
generalize (no_duplicate_suffix H0 H).
intros.
inversion H2.
contradiction.
Qed.

Lemma no_duplicates_complete : forall l,
(forall a m, is_suffix_of (cons a m) l -> member a m -> False) ->
no_duplicates l.

Proof.
induction l ; auto.
intros ; apply no_duplicates_cons ; auto.
 (* member a l -> False *)
apply H ; auto.
apply IHl ; auto.
intros ; apply H with a0 m ; auto.
Qed.

Lemma no_duplicates_base : forall a l,
no_duplicates (a::l) ->
member a l -> False.

Proof.
intros.
eapply no_duplicates_correct ; eauto.
Qed.

End List_no_duplicates.

Fixpoint repeat n (a : A) := match n with O => nil | S n' => a::(@repeat n' a) end.

End List_addons.

Hint Constructors member find_in_list list_forall is_suffix_of no_duplicates.
Hint Resolve member_nil.
Hint Resolve no_duplicates_tail no_duplicates_base.



Ltac automem :=
match goal with
| [ H: member _ nil |- _ ] => apply False_rect ; inversion H
| _ => idtac
end.



Lemma member_map : forall (A : Set) l x, member x l -> forall (B : Set) (f : A -> B),
member (f x) (map f l).
Proof.
induction 1 ; simpl ; auto.
Qed.

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

(* Equations with ++ (app) *)

Section App_facts.
Variable A : Set.

Require Import Arith.

Lemma app_fix_left : forall (l l0 : list A), l = l ++ l0 -> l0 = nil.
Proof.
induction l.
simpl.
auto.
simpl.
intros l0 H.
injection H.
intros.
auto.
Qed.

Lemma app_fix_right : forall (l l0 : list A), l = l0 ++ l -> l0 = nil.
Proof.
intros l l0 Hll0.
generalize (app_length l0 l).
rewrite <- Hll0.
rewrite plus_comm.
pattern (length l) at 1.
rewrite <- (plus_0_r (length l)).
intro Hlength.
generalize (plus_reg_l _ _ _ Hlength).
case l0.
auto.
simpl.
discriminate 1.
Qed.

Lemma app_reg_l : forall l l1 l2 : list A, l ++ l1 = l ++ l2 -> l1 = l2.
Proof.
induction l.
simpl.
auto.
simpl.
injection 1.
auto.
Qed.

Lemma rev_inj : forall l1 l2 : list A, rev l1 = rev l2 -> l1 = l2.
Proof.
intros.
rewrite <- (rev_involutive l1).
rewrite <- (rev_involutive l2).
f_equal.
auto.
Qed.

Lemma app_reg_r : forall l l1 l2 : list A, l1 ++ l = l2 ++ l -> l1 = l2.
Proof.
introvars.
rewrite <- (rev_involutive (l1 ++ l)).
rewrite <- (rev_involutive (l2 ++ l)).
rewrite distr_rev.
rewrite (distr_rev l2).
intro H.
generalize (rev_inj H).
intros.
apply rev_inj.
eapply app_reg_l.
eauto.
Qed.

Lemma member_or : forall l1 l2 (b : A), member b (l1 ++ l2) -> member b l1 \/ member b l2.
Proof.
induction l1; simpl.
intros; right; auto.
inversion 1.
left; auto.
subst.
destruct (IHl1 _ _  H1) ; auto.
Qed.

Lemma member_app_left : forall l1 (b : A), member b l1 -> forall l2, member b (l1 ++ l2).
Proof.
induction 1;simpl;auto.
Qed.

Lemma member_app_right : forall l1 l2 (b : A), member b l2 -> member b (l1 ++ l2).
Proof.
induction l1; simpl; auto.
Qed.

Lemma no_duplicates_no_member_app : forall l1 l2, no_duplicates (l1 ++ l2) -> forall x : A, member x l1 -> member x l2 -> False.
Proof.
induction l1; simpl.
 inversion 2.
inversion 1.
subst.
inversion 1.
 subst.
 intros.
 apply H2.
 apply member_app_right.
 assumption.
subst.
eauto.
Qed.

Lemma member_extract : forall l (b : A), member b l -> exists l1, exists l2, l = l1 ++ (b :: l2).
Proof.
induction 1.
exists (@nil A).
simpl.
exists l.
trivial.
destruct IHmember as [l1 [l2 Hl]].
exists (a::l1).
exists (l2).
simpl.
congruence.
Qed.

Fixpoint flatten l :=
  match l with
    | nil => nil (A := A)
    | a::b => a ++ flatten b
  end.

Lemma member_flatten_elim : forall l a, member a (flatten l) ->
  exists l0, member l0 l /\ member a l0.
Proof.
induction l; simpl.
 inversion 1.
intros a0 Ha0.
generalize (member_or Ha0).
simple inversion 1.
 intros.
 esplit.
 split.
  eapply member_head.
 assumption.
intro HIH.
generalize (IHl _ HIH).
intros [l0 [Hl0 Ha0l0]].
esplit.
split.
 eapply member_tail.
 eassumption.
assumption.
Qed.

Lemma member_flatten_intro : forall l0  l,
  member l0 l -> forall a, member a l0 -> member a (flatten l).
Proof.
induction 1; simpl; intros.
 eapply member_app_left; eauto.
eapply member_app_right; eauto.
Qed.

Hypothesis eq_A_dec : forall a b : A, {a = b} + {a <> b}.

Let md := member_rect eq_A_dec.

Lemma member_extract_dec :
forall l (b : A), member b l -> {l1 : _ & {l2 | l = l1 ++ (b :: l2)}}.
Proof.
induction l.
intros b Hb; apply False_rect; inversion Hb.
intros b Hb.
destruct (member_which_dec eq_A_dec Hb).
subst.
exists (@nil A).
simpl.
exists l.
trivial.
destruct (IHl _ m) as [l1 [l2 Hl]].
exists (a::l1).
exists (l2).
simpl.
congruence.
Qed.

End App_facts.

Section Sorted.
Variable A : Set.
Variable ord : A -> A -> Prop.

Inductive sorted : list A -> Prop := 
| sorted_O: sorted nil
| sorted_1: forall x, sorted (cons x nil)
| sorted_S: forall x y, ord x y -> forall l, sorted (cons y l) -> sorted (cons x (cons y l)).

Hint Constructors sorted.

Lemma sorted_tail : forall a l, sorted (a::l) -> sorted l.
Proof.
 inversion 1.
  auto.
 auto.
Qed.

Hypothesis eq_A_dec : forall a b : A, {a = b} + {a <> b}.

Fixpoint occur a l {struct l} := match l with
| nil => O
| cons b m => match eq_A_dec a b with
  | left _ => S (@occur a m)
  | right _ => @occur a m
  end
end.

Lemma occur_member : forall l a n, occur a l = S n -> member a l.
Proof.
induction l.
simpl.
discriminate 1.
simpl.
intros a0 n.
destruct (eq_A_dec a0 a); subst; eauto.
Qed.

Lemma occur_not_member : forall l a, occur a l = O -> member a l -> False.
Proof.
induction l.
inversion 2.
simpl.
intros a0.
destruct (eq_A_dec a0 a).
discriminate 1.
inversion 2.
contradiction.
subst; eauto.
Qed.

Inductive bisimilar l1 l2 : Prop :=
| bisimilar_intro : (forall a, occur a l1 = occur a l2) -> @bisimilar l1 l2.

Hint Constructors bisimilar.

Lemma bisimilar_member l1 l2 : bisimilar l1 l2 -> forall c, member c l1 -> member c l2.
Proof.
inversion 1 as [Hbis].
intros c Hc.
case_eq (occur c l1).
intros Ho.
destruct (occur_not_member Ho Hc).
rewrite Hbis.
apply occur_member.
Qed.

Hypothesis ord_dec : forall a b, {ord a b} + {ord a b -> False}.

Hypothesis ord_total : forall a b, ord a b \/ ord b a.

Hypothesis ord_trans : forall a b, ord a b -> forall c, ord b c -> ord a c.

Lemma head_minimal : forall l, sorted l -> forall c l', l = c::l' -> forall d, member d l' -> ord c d.
Proof.
induction 1.
discriminate 1.
injection 1.
intros until 2.
subst.
inversion 1.
injection 1.
intros until 2.
subst.
inversion 1.
auto.
subst.
eapply ord_trans; eauto.
Qed.


Lemma sorted_app : forall l1 l2, sorted (l1 ++ l2) -> forall a1, member a1 l1 ->
forall a2, member a2 l2 -> ord a1 a2.
Proof.
induction l1.
 inversion 2.
simpl.
inversion 2.
 subst.
 intros.
 eapply head_minimal.
  eexact H.
 reflexivity.
 apply member_app_right.
 assumption.
subst.
apply IHl1.
eapply sorted_tail.
eassumption.
assumption.
Qed.

Lemma sorted_app_left : forall l1 l2, sorted (l1 ++ l2) -> sorted l1.
Proof.
induction l1.
auto.
simpl.
inversion 1.
subst.
replace l1 with (@nil A).
apply sorted_1.
destruct l1; auto; simpl in H2; discriminate.
subst.
destruct l1; auto.
simpl in *.
apply sorted_S.
 congruence.
eapply IHl1.
rewrite H1 in H3.
eassumption.
Qed.

Lemma sorted_app_right : forall l1 l2, sorted (l1 ++ l2) -> sorted l2.
Proof.
induction l1; auto.
simpl.
 inversion 1.
 replace l2 with (@nil A).
 auto.
 destruct l2; auto; destruct l1; simpl in H2; discriminate.
subst.
rewrite H1 in H3.
eauto.
Qed.

Definition sort_insert l : sorted l -> forall b, {l' | sorted l' /\ bisimilar l' (b::l)}.
Proof.
induction l.
intros.
exists (cons b nil).
auto.
intros Hal b.
case (ord_dec b a).
intros Hba.
exists (b::a::l).
auto.
intros.
assert (sorted l) as Hl.
 inversion Hal; auto.
destruct (IHl Hl b) as [l' Hl'].
exists (a::l').
inversion Hl' as [Hl'sorted Hl'bis].
split.
case_eq l'.
auto.
intros a0 l'0 ?.
subst.
apply sorted_S.
destruct (eq_A_dec a0 b).
subst.
destruct (ord_total a b).
auto.
contradiction.
eapply head_minimal.
apply Hal.
reflexivity.
eapply member_step.
eauto.
eapply bisimilar_member.
apply Hl'bis.
auto.
auto.
inversion Hl'bis as [Hl'ter].
apply bisimilar_intro.
intro a0.
simpl.
destruct (eq_A_dec a0 a).
subst.
rewrite Hl'ter.
simpl.
destruct (eq_A_dec a b); auto.
rewrite Hl'ter.
simpl.
auto.
Defined.

Definition sort l : {l' | sorted l' /\ bisimilar l' l}.
Proof.
induction l.
exists (@nil A).
auto.
destruct IHl as [l' Hl'].
assert (sorted l') as Hl'2.
 inversion Hl'; auto.
destruct (sort_insert Hl'2 a) as [l'0 Hl'0].
exists l'0.
inversion Hl'0 as [Hl'1 [Hl'3]].
split.
auto.
inversion_clear Hl' as [_ [Hl'4]].
apply bisimilar_intro.
intros a0.
rewrite Hl'3.
simpl.
destruct (eq_A_dec a0 a); auto.
Defined.

End Sorted.
Hint Constructors sorted.

Section Member_strong_list.

Variable A : Set.

Let f (l : list A) (a : A) (mh : {m | member m l}) :=
 match mh with
 | exist m h => exist (fun m0 => member m0 (a::l)) m (member_tail h a)
end.

Implicit Arguments f [].

Definition member_weak_list : forall l, list {m : A | member m l} ->
forall a, list {m | member m (a::l)}.
Proof.
intros l l' a.
exact (List.map (f l a) l').
Defined.

Definition member_strong_list : forall l, list {m : A | member m l}.
Proof.
induction l.
exact (@nil {m | member m nil}).
refine (exist _ a _ :: _).
auto.
exact (member_weak_list IHl a).
Defined.

Lemma member_strong_list_nil : member_strong_list nil = nil.
auto.
Qed.

Lemma member_strong_list_cons : forall a l, member_strong_list (a::l) =
(exist _ a (member_head a l)) :: (member_weak_list (member_strong_list l) a).
auto.
Qed.

Theorem member_strong : forall l m (H : member m l), member (exist _ m H) (member_strong_list l).
intros l m H.
generalize H.
induction H as [| ? H0].
intros H.
rewrite member_strong_list_cons.
rewrite (proof_irrelevance _ H (member_head m l)).
auto.
rewrite member_strong_list_cons.
intros H.
apply member_tail.
rewrite (proof_irrelevance _ H (member_tail H0 a)).
unfold member_weak_list.
change (exist (fun m0 => member m0 (a::l)) m (member_tail H0 a)) with
 (f l a (exist _ m H0)).
apply member_map.
auto.
Qed.

Lemma member_strong_length : forall l, length l = length (member_strong_list l).
Proof.
induction l; auto.
rewrite member_strong_list_cons.
simpl.
f_equal.
unfold member_weak_list.
rewrite <- map_length.
auto.
Qed.

Definition erase (P : A -> Prop) (m : {m | P m}) :=
match m with exist m0 _ => m0 end.

Definition erase_list (P : A -> Prop) (l : list {m | P m}) := map (@erase P) l.

Lemma erase_f : forall l a m, erase m = erase (f l a m).
Proof.
destruct m; simpl; auto.
Qed.

Lemma erase_f_map : forall l a l', erase_list l' = erase_list (map (f l a) l').
induction l' ; simpl ; auto.
destruct a0.
simpl.
f_equal.
auto.
Qed.

Lemma weaken_strong : forall l, erase_list (member_strong_list l) = l.
Proof.
induction l; auto.
simpl.
f_equal.
unfold member_weak_list.
eapply trans_equal.
symmetry.
eapply erase_f_map.
auto.
Qed.

(* Starting from a list l, construct the list l' of the elements of l along with
their proofs that they belong to l *)

End Member_strong_list.

Extract Inductive list => "list" [ "[]" "( :: )" ].

(* Recursive Extraction member_strong_list.
 this gives the identity on lists, written in a particular way *)


(* Recursive Extraction sort. *)