(**************************************************************)
(*   Copyright Dominique Larchey-Wendling *                 *)
(*                                                            *)
(*                             * Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

Require Import List Arith Max Omega Wellfounded Bool.

Require Import list_focus utils_tac utils_list.

Set Implicit Arguments.

Fact interval_dec a b i : { a <= i < b } + { i < a \/ b <= i }.
Proof.
  destruct (le_lt_dec b i).
  right; omega.
  destruct (le_lt_dec a i).
  left; omega.
  right; omega.
Qed.

Definition lsum := fold_right plus 0.
Definition lmax := fold_right max 0.

Fact lsum_app l r : lsum (l++r) = lsum l+lsum r.
Proof.
  induction l as [ | x l IHl ]; simpl; auto; rewrite IHl; omega.
Qed.

Section new.

  Definition nat_new l := S (lmax l).

  Fact nat_new_spec l : ~ In (nat_new l) l.
  Proof.
    assert (forall x, In x l -> x < nat_new l) as H.
      induction l as [ | x l IHl ].
      intros _ [].
      intros y [ [] | Hy ]; apply le_n_S;
        [ apply le_max_l | ].
      apply IHl, le_S_n in Hy.
      apply le_trans with (1 := Hy), le_max_r.
    intros C; apply H in C; omega.
  Qed.

End new.

Local Notation Zero := false.
Local Notation One := true.

Fixpoint div2 n : nat * bool :=
  match n with
    | 0 => (0,Zero)
    | 1 => (0,One)
    | S (S n) => let (p,b) := div2 n in (S p,b)
  end.

Fact div2_spec n : match div2 n with
                     | (p,One) => n = 2*p+1
                     | (p,Zero) => n = 2*p
                   end.
Proof.
  induction n as [ [ | [ | n ] ] IHn ] using (well_founded_induction lt_wf); simpl; auto.
  specialize (IHn n).
  destruct (div2 n) as (p,[]); simpl in * |- *; omega.
Qed.

Fixpoint div2_2p1 p : div2 (2*p+1) = (p,One).
Proof.
  destruct p as [ | p ].
  simpl; auto.
  replace (2*S p+1) with (S (S (2*p+1))) by omega.
  unfold div2; fold div2; rewrite div2_2p1; auto.
Qed.

Fixpoint div2_2p0 p : div2 (2*p) = (p,Zero).
Proof.
  destruct p as [ | p ].
  simpl; auto.
  replace (2*S p) with (S (S (2*p))) by omega.
  unfold div2; fold div2; rewrite div2_2p0; auto.
Qed.

Fixpoint pow2 p :=
  match p with
    | 0 => 1
    | S p => 2*pow2 p
  end.

Section pow2_bound.

  Let loop := fix loop x n :=
    match n with
      | 0 => 0
      | S n => match div2 x with
                 | (0,_) => 0
                 | (p,_) => S (loop p n)
               end
    end.

  Let loop_prop n : forall x, x < n -> x < pow2 (S (loop x n)).
  Proof.
    induction n as [ | n IHn ]; intros x Hx.
    omega.
    unfold loop; fold loop.
    generalize (div2_spec x).
    destruct (div2 x) as ([ | p ],[]); intros H.
    simpl; omega.
    simpl; omega.
    specialize (IHn (S p)); spec in IHn.
    omega.
    simpl in IHn |- *; omega.
    specialize (IHn (S p)); spec in IHn.
    omega.
    simpl in IHn |- *; omega.
  Qed.

  Definition find_pow2 x := S (loop (pred x) x).

  Fact find_pow2_geq x : 1 <= find_pow2 x.
  Proof. unfold find_pow2; omega. Qed.

  Fact find_pow2_prop x : x <= pow2 (find_pow2 x).
  Proof.
    unfold find_pow2; destruct x.
    simpl; omega.
    apply loop_prop; auto.
  Qed.

End pow2_bound.

Section nat_sorted.

  Definition nat_sorted ll := forall l a m b r, ll = l ++ a :: m ++ b :: r -> a < b.

  Fact in_nat_sorted_0 : nat_sorted nil.
  Proof. intros [] ? ? ? ? ?; discriminate. Qed.

  Fact in_nat_sorted_1 x : nat_sorted (x::nil).
  Proof. intros [ | ? [] ] ? [] ? ? ?; discriminate. Qed.

  Fact in_nat_sorted_2 x y ll : x < y -> nat_sorted (y::ll) -> nat_sorted (x::y::ll).
  Proof.
    intros H1 H2 l a m b r H3.
    destruct l as [ | u l ].
    inversion H3; subst.
    destruct m as [ | v m ].
    inversion H4; subst; auto.
    inversion H4; subst.
    apply lt_trans with (1 := H1), (H2 nil _ m _ r); auto.
    inversion H3; subst.
    apply (H2 l _ m _ r); auto.
  Qed.

  Fact in_nat_sorted_3 x ll : Forall (lt x) ll -> nat_sorted ll -> nat_sorted (x::ll).
  Proof.
    induction 1 as [ | y ll Hll IHl ].
    intro; apply in_nat_sorted_1.
    intros H.
    apply in_nat_sorted_2; auto.
  Qed.

  Fact nat_sorted_cons_inv x ll : nat_sorted (x::ll) -> nat_sorted ll.
  Proof. intros H l a m b r ?; apply (H (x::l) _ m _ r); subst; solve list eq. Qed.

  Fact nat_sorted_Forall x ll : nat_sorted (x::ll) -> Forall (lt x) ll.
  Proof.
    rewrite Forall_forall; intros H y Hy.
    apply in_split in Hy.
    destruct Hy as (l & r & ?); subst.
    apply (H nil _ l _ r); auto.
  Qed.

  Fact nat_sorted_head_inv x y ll : nat_sorted (x::y::ll) -> x < y.
  Proof. intros H; apply (H nil _ nil _ ll); solve list eq. Qed.

  Variable P : list nat -> Type.

  Hypothesis (HP0 : P nil).
  Hypothesis (HP1 : forall x, P (x::nil)).
  Hypothesis (HP2 : forall x y l, x < y -> P (y::l) -> P (x::y::l)).

  Theorem nat_sorted_rect l : nat_sorted l -> P l.
  Proof.
    induction l as [ [ | x [ | y l ] ] IHl ] using (measure_rect (@length _)).
    intro; apply HP0.
    intro; apply HP1.
    intros H; apply HP2.
    revert H; apply nat_sorted_head_inv.
    apply IHl.
    rew length; omega.
    revert H; apply nat_sorted_cons_inv.
  Qed.

End nat_sorted.

Fact nat_sorted_injective ll : nat_sorted ll -> list_injective ll.
Proof.
  intros H l a m b r E; generalize (H _ _ _ _ _ E); omega.
Qed.

Fixpoint nat_list_insert x l :=
  match l with
    | nil => x::nil
    | y::l => if x <? y then x::y::l else
              if y <? x then y::nat_list_insert x l else y::l
  end.

Fact nat_list_insert_length x l : length (nat_list_insert x l) <= S (length l).
Proof.
  induction l as [ | y l IHl ]; simpl.
  omega.
  destruct (x <? y); simpl; try omega.
  destruct (y <? x); simpl; omega.
Qed.

Fact nat_list_insert_incl x l : incl (nat_list_insert x l) (x::l)
                             /\ incl (x::l) (nat_list_insert x l).
Proof.
  split.

  induction l as [ | y l IHl ]; simpl.
  intro; auto.
  destruct (x <? y); destruct (y <? x).
  intro; auto.
  intro; auto.
  intros ? [ [] | H ]; simpl; auto.
  apply IHl in H; simpl in H; tauto.
  intro; simpl; tauto.

  induction l as [ | y l IHl ]; simpl.
  intro; auto.
  generalize (Nat.ltb_lt x y) (Nat.ltb_lt y x).
  destruct (x <? y); destruct (y <? x); intros H1 H2 z; auto.
  intros [ Hz | [ Hz | Hz ] ]; subst.
  right; apply IHl; left; auto.
  left; auto.
  right; apply IHl; right; auto.
  destruct (lt_eq_lt_dec x y) as [ [ H | ] | H ].
  apply H1 in H; discriminate.
  2: apply H2 in H; discriminate.
  intros [ Hz | [ Hz | Hz ] ]; subst; auto.
  left; auto.
  left; auto.
  right; auto.
Qed.

Fact nat_list_insert_Forall (P : nat -> Prop) x l :
      P x -> Forall P l -> Forall P (nat_list_insert x l).
Proof.
  do 2 rewrite Forall_forall; intros H1 H2 y Hy.
  apply nat_list_insert_incl in Hy.
  destruct Hy; subst; auto.
Qed.

Fact nat_list_insert_sorted x l : nat_sorted l -> nat_sorted (nat_list_insert x l).
Proof.
  induction l as [ | y l IHl ]; simpl.
  intro; apply in_nat_sorted_1.
  intros H.
  generalize (Nat.ltb_lt x y) (Nat.ltb_lt y x).
  destruct (x <? y); destruct (y <? x); intros H1 H2.
  apply proj1 in H1; spec in H1; auto.
  apply proj1 in H2; spec in H2; auto.
  omega.
  apply in_nat_sorted_2; auto; tauto.
  apply in_nat_sorted_3.
  apply nat_list_insert_Forall.
  tauto.
  apply nat_sorted_Forall; auto.
  apply IHl; revert H; apply nat_sorted_cons_inv.
  auto.
Qed.

Definition nat_sort := fold_right (nat_list_insert) nil.

Fact nat_sort_length l : length (nat_sort l) <= length l.
Proof.
  induction l as [ | x l IHl ]; simpl.
  omega.
  apply le_trans with (1 := nat_list_insert_length _ _); omega.
Qed.

Fact nat_sort_eq l : incl (nat_sort l) l /\ incl l (nat_sort l).
Proof.
  induction l as [ | x l IHl ]; simpl; split; intros y Hy; auto.
  apply nat_list_insert_incl in Hy; simpl.
  destruct Hy as [ | Hy ]; auto; right; apply IHl; auto.
  apply nat_list_insert_incl.
  destruct Hy; [ left | right ]; auto.
  apply IHl; auto.
Qed.

Fact nat_sort_sorted l : nat_sorted (nat_sort l).
Proof.
  induction l as [ | x l IHl ].
  apply in_nat_sorted_0.
  simpl; apply nat_list_insert_sorted; auto.
Qed.

Fact nat_sinc (f : nat -> nat) a b :
      (forall x, a <= x < b -> f x < f (S x))
   -> (forall x y, a <= x < y /\ y <= b -> f x < f y).
Proof.
  intros H1.
  assert (forall n m, n <= m <= b - a -> f (a+n) <= f (a+m)) as H2.
    intros n m (H2 & H3); revert H2 H3.
    induction 1 as [ | m Hm IH ]; auto.
    intros H. spec in IH. omega.
    apply le_trans with (1 := IH).
    replace (a+S m) with (S (a+m)) by omega.
    apply lt_le_weak, H1; omega.
  assert (forall n m, n < m <= b - a -> f (a+n) < f (a+m)) as H3.
    unfold lt at 1; intros n m H.
    specialize (H1 (a+n)).
    spec in H1.
    omega.
    apply lt_le_trans with (1 := H1).
    replace (S (a+n)) with (a+S n) by omega.
    apply H2; auto.
  intros x y H4.
  replace x with (a+(x-a)) by omega.
  replace y with (a+(y-a)) by omega.
  apply H3.
  omega.
Qed.

Fact nat_sinc_inj f a b :
      (forall x y, a <= x < y /\ y <= b -> f x < f y)
   -> (forall x y, a <= x <= b -> a <= y <= b -> f x = f y -> x = y).
Proof.
  intros H0 x y Hx Hy.
  destruct Hx; destruct Hy.
  destruct (lt_eq_lt_dec x y) as [ [ ? | ? ] | ? ]; auto.
  specialize (H0 x y).
  spec in H0; repeat split; auto; intro; omega.
  specialize (H0 y x).
  spec in H0; repeat split; auto; intro; omega.
Qed.