(**************************************************************)
(*   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.

Section fin_reif.

  Variable (X : Type) (R : nat -> X -> Prop).

  Fact fin_reif n : (forall i, i < n -> exists x, R i x)
                 -> exists s, forall i (Hi : i < n), R i (s i Hi).
  Proof.
(* Goal: forall _ : forall (i : nat) (_ : lt i n), @ex X (fun x : X => R i x), @ex (forall (x : nat) (_ : lt x n), X) (fun s : forall (x : nat) (_ : lt x n), X => forall (i : nat) (Hi : lt i n), R i (s i Hi)) *)
    revert R; induction n as [ | n IHn ]; intros R HR.
    + assert (s : forall x, x < 0 -> X) by (intros; omega).
(* Goal: @ex (forall (x : nat) (_ : lt x O), X) (fun s : forall (x : nat) (_ : lt x O), X => forall (i : nat) (Hi : lt i O), R i (s i Hi)) *)
      exists s; intros; omega.
    + destruct (HR 0) as (x & Hx); try omega.
(* Goal: @ex (forall (x : nat) (_ : lt x (S n)), X) (fun s : forall (x : nat) (_ : lt x (S n)), X => forall (i : nat) (Hi : lt i (S n)), R i (s i Hi)) *)
      destruct IHn with (R := fun i x => R (S i) x) as (s & Hs).
(* Goal: forall (i : nat) (_ : lt i n), @ex X (fun x : X => R (S i) x) *)
(* Goal: @ex (forall (x : nat) (_ : lt x (S n)), X) (fun s : forall (x : nat) (_ : lt x (S n)), X => forall (i : nat) (Hi : lt i (S n)), R i (s i Hi)) *)
      { intros; apply HR; omega. }
(* Goal: @ex (forall (x : nat) (_ : lt x (S n)), X) (fun s : forall (x : nat) (_ : lt x (S n)), X => forall (i : nat) (Hi : lt i (S n)), R i (s i Hi)) *)
      exists (fun i => match i with 0 => fun _ => x | S i => fun Hi => s i (lt_S_n i n Hi) end).
(* Goal: forall (i : nat) (Hi : lt i (S n)), R i (match i as i0 return (forall _ : lt i0 (S n), X) with | O => fun _ : lt O (S n) => x | S i0 => fun Hi0 : lt (S i0) (S n) => s i0 (lt_S_n i0 n Hi0) end Hi) *)
      intros [ | i ] Hi; simpl; auto.
  Qed.

End fin_reif.

Fact fin_reif_nat (R : nat -> nat -> Prop) n :
         (forall i, i < n -> ex (R i)) -> exists s, forall i, i < n -> R i (s i).
Proof.
(* Goal: forall _ : forall (i : nat) (_ : lt i n), @ex nat (R i), @ex (forall _ : nat, nat) (fun s : forall _ : nat, nat => forall (i : nat) (_ : lt i n), R i (s i)) *)
  intros HR.
(* Goal: @ex (forall _ : nat, nat) (fun s : forall _ : nat, nat => forall (i : nat) (_ : lt i n), R i (s i)) *)
  apply fin_reif in HR.
(* Goal: @ex (forall _ : nat, nat) (fun s : forall _ : nat, nat => forall (i : nat) (_ : lt i n), R i (s i)) *)
  destruct HR as (s & Hs).
(* Goal: @ex (forall _ : nat, nat) (fun s : forall _ : nat, nat => forall (i : nat) (_ : lt i n), R i (s i)) *)
  exists (fun i => match le_lt_dec n i with left _ => 0 | right H => s _ H end).
(* Goal: forall (i : nat) (_ : lt i n), R i match le_lt_dec n i with | left l => O | right H => s i H end *)
  intros i Hi; destruct (le_lt_dec n i); auto; omega.
Qed.

Section bounded_search.

  Theorem bounded_search m (P : nat -> Type) :
        (forall n, n < m -> P n + (P n -> False))
     -> { n : nat & (n < m) * P n }%type + { forall n, n < m -> P n -> False }.
  Proof.
(* Goal: forall _ : forall (n : nat) (_ : lt n m), sum (P n) (forall _ : P n, False), sumor (@sigT nat (fun n : nat => prod (lt n m) (P n))) (forall (n : nat) (_ : lt n m) (_ : P n), False) *)
    revert P; induction m as [ | m IHm ]; intros P HP.
    + right; intros; omega.
    + destruct (HP 0) as [ H0 | H0 ]; try omega.
      * left; exists 0; split; auto; omega.
      * destruct IHm with (P := fun n => P (S n)) as [ (n & H1 & H2) | H1 ].
        - intros; apply HP; omega.
        - left; exists (S n); split; auto; omega.
        - right; intros [ | n ] Hn; auto.
(* Goal: forall _ : P (S n), False *)
          apply H1; omega.
  Qed.

  Lemma bounded_min (P : nat -> Prop) : 
        (forall x, P x \/ ~ P x) 
     -> forall n, (exists k, k < n /\ P k /\ forall i, i < k -> ~ P i) \/ forall k, k < n -> ~ P k.
  Proof.
(* Goal: forall (_ : forall x : nat, or (P x) (not (P x))) (n : nat), or (@ex nat (fun k : nat => and (lt k n) (and (P k) (forall (i : nat) (_ : lt i k), not (P i))))) (forall (k : nat) (_ : lt k n), not (P k)) *)
    intros HP.
(* Goal: forall n : nat, or (@ex nat (fun k : nat => and (lt k n) (and (P k) (forall (i : nat) (_ : lt i k), not (P i))))) (forall (k : nat) (_ : lt k n), not (P k)) *)
    induction n as [ | n IHn ].
    + right; intros; omega.
    + destruct IHn as [ (k & H1 & H2 & H3) | H ].
      * left; exists k; repeat split; auto; omega.
      * destruct (HP n).
        - left; exists n; repeat split; auto.
        - right; intros k Hk.
(* Goal: not (P k) *)
          destruct (eq_nat_dec k n); subst; auto. 
(* Goal: not (P k) *)
          apply H; omega.
  Qed.

  Lemma minimize (P : nat -> Prop) : (forall x, P x \/ ~ P x) -> (exists n, P n) -> exists n, P n /\ forall i, i < n -> ~ P i.
  Proof.
(* Goal: forall (_ : forall x : nat, or (P x) (not (P x))) (_ : @ex nat (fun n : nat => P n)), @ex nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i))) *)
    intros HP (n & Hn).
(* Goal: @ex nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i))) *)
    destruct (@bounded_min _ HP (S n)) as [ (k & H1 & H2 & H3) | H ].
    + exists k; split; auto.
    + exfalso; apply H with n; auto.
  Qed.
   
  Lemma first_non_zero (f : nat -> nat) n : f 0 = 0 -> f n <> 0 -> exists i, i < n /\ (forall k, k <= i -> f k = 0) /\ f (i+1) <> 0.
  Proof.
(* Goal: forall (_ : @eq nat (f O) O) (_ : not (@eq nat (f n) O)), @ex nat (fun i : nat => and (lt i n) (and (forall (k : nat) (_ : le k i), @eq nat (f k) O) (not (@eq nat (f (Init.Nat.add i (S O))) O)))) *)
    intros H0 H1.
(* Goal: @ex nat (fun i : nat => and (lt i n) (and (forall (k : nat) (_ : le k i), @eq nat (f k) O) (not (@eq nat (f (Init.Nat.add i (S O))) O)))) *)
    destruct (@minimize (fun i => f i <> 0)) as (i & H2 & H3).
    + intro; destruct (eq_nat_dec (f x) 0); omega.
    + exists n; auto.
    + assert (i <> 0) as Hi by (intro; subst; destruct H2; auto).
      exists (i-1); split; [ | split ].
      * destruct (le_lt_dec i n) as [ | H4 ]; try omega.
(* Goal: lt (Init.Nat.sub i (S O)) n *)
        apply H3 in H4; destruct H4; auto.
      * intros k Hk; generalize (H3 k); intros; omega.
      * replace (i-1+1) with i by omega; auto.
  Qed.

End bounded_search.

Fact interval_dec a b i : { a <= i < b } + { i < a \/ b <= i }.
Proof.
(* Goal: sumbool (and (le a i) (lt i b)) (or (lt i a) (le b i)) *)
  destruct (le_lt_dec b i).
(* Goal: sumbool (and (le a i) (lt i b)) (or (lt i a) (le b i)) *)
  right; omega.
(* Goal: sumbool (and (le a i) (lt i b)) (or (lt i a) (le b i)) *)
  destruct (le_lt_dec a i).
(* Goal: sumbool (and (le a i) (lt i b)) (or (lt i a) (le b i)) *)
(* Goal: sumbool (and (le a i) (lt i b)) (or (lt i a) (le b i)) *)
  left; omega.
(* Goal: sumbool (and (le a i) (lt i b)) (or (lt i a) (le b i)) *)
  right; omega.
Qed.

(* Fact interval_dec a b n : { a <= n < b } + { ~ a <= n < b }.
Proof.
  destruct (le_lt_dec a n).
(* Goal: sumbool (and (le a i) (lt i b)) (or (lt i a) (le b i)) *)
  2: right; omega.
  destruct (le_lt_dec b n).
(* Goal: sumbool (and (le a i) (lt i b)) (or (lt i a) (le b i)) *)
  1: right; omega.
(* Goal: sumbool (and (le a i) (lt i b)) (or (lt i a) (le b i)) *)
(* Goal: sumbool (and (le a i) (lt i b)) (or (lt i a) (le b i)) *)
  left; omega.
Qed. *)


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

Fact lmax_spec l x : lmax l <= x <-> Forall (fun y => y <= x) l.
Proof.
(* Goal: iff (le (lmax l) x) (@Forall nat (fun y : nat => le y x) l) *)
  revert x; induction l as [ | y l IHl ]; simpl.
  + split; auto; try omega.
  + intros x; rewrite Forall_cons_inv, <- IHl, Nat.max_lub_iff; tauto.
Qed.

Fact lsum_app l r : lsum (l++r) = lsum l+lsum r.
Proof.
(* Goal: @eq nat (lsum (@app nat l r)) (Init.Nat.add (lsum l) (lsum r)) *)
  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.
(* Goal: nat_sorted (nat_sort l) *)
      induction l as [ | x l IHl ].
(* Goal: forall (x : nat) (_ : @In nat x (@nil nat)), lt x (nat_new (@nil nat)) *)
(* Goal: forall (x0 : nat) (_ : @In nat x0 (@cons nat x l)), lt x0 (nat_new (@cons nat x l)) *)
(* Goal: not (@In nat (nat_new l) l) *)
      intros _ [].
      intros y [ [] | Hy ]; apply le_n_S;
        [ apply le_max_l | ].
(* Goal: le y (lmax (@cons nat x l)) *)
(* Goal: not (@In nat (nat_new l) l) *)
      apply IHl, le_S_n in Hy.
(* Goal: le y (lmax (@cons nat x l)) *)
(* Goal: not (@In nat (nat_new l) l) *)
      apply le_trans with (1 := Hy), le_max_r.
(* Goal: not (@In nat (nat_new l) l) *)
    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.
(* Goal: let (p, b) := div2 n in if b then @eq nat n (Init.Nat.add (Init.Nat.mul (S (S O)) p) (S O)) else @eq nat n (Init.Nat.mul (S (S O)) p) *)
  induction n as [ [ | [ | n ] ] IHn ] using (well_founded_induction lt_wf); simpl; auto.
(* Goal: let (p, b) := let (p, b) := div2 n in @pair nat bool (S p) b in if b then @eq nat (S (S n)) (Init.Nat.add (Init.Nat.add p (Init.Nat.add p O)) (S O)) else @eq nat (S (S n)) (Init.Nat.add p (Init.Nat.add p O)) *)
  specialize (IHn n).
  destruct (div2 n) as (p,[]); simpl in * |- *; omega.
Qed.

Fixpoint div2_2p1 p : div2 (2*p+1) = (p,One).
Proof.
(* Goal: @eq (prod nat bool) (div2 (Init.Nat.mul (S (S O)) p)) (@pair nat bool p false) *)
  destruct p as [ | p ].
(* Goal: @eq (prod nat bool) (div2 (Init.Nat.mul (S (S O)) O)) (@pair nat bool O false) *)
(* Goal: @eq (prod nat bool) (div2 (Init.Nat.mul (S (S O)) (S p))) (@pair nat bool (S p) false) *)
  simpl; auto.
  replace (2*S p+1) with (S (S (2*p+1))) by omega.
(* Goal: @eq (prod nat bool) (div2 (S (S (Init.Nat.add (Init.Nat.mul (S (S O)) p) (S O))))) (@pair nat bool (S p) true) *)
  unfold div2; fold div2; rewrite div2_2p1; auto.
Qed.

Fixpoint div2_2p0 p : div2 (2*p) = (p,Zero).
Proof.
(* Goal: @eq (prod nat bool) (div2 (Init.Nat.mul (S (S O)) p)) (@pair nat bool p false) *)
  destruct p as [ | p ].
(* Goal: @eq (prod nat bool) (div2 (Init.Nat.mul (S (S O)) O)) (@pair nat bool O false) *)
(* Goal: @eq (prod nat bool) (div2 (Init.Nat.mul (S (S O)) (S p))) (@pair nat bool (S p) false) *)
  simpl; auto.
  replace (2*S p) with (S (S (2*p))) by omega.
(* Goal: @eq (prod nat bool) (div2 (S (S (Init.Nat.mul (S (S O)) p)))) (@pair nat bool (S p) false) *)
  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.
(* Goal: forall (x : nat) (_ : lt x n), lt x (pow2 (S (loop x n))) *)
    induction n as [ | n IHn ]; intros x Hx.
(* Goal: False *)
    omega.
(* Goal: lt x (pow2 (S (loop x (S n)))) *)
    unfold loop; fold loop.
(* Goal: lt x (pow2 (S (let (p, _) := div2 x in match p with | O => O | S n0 => S (loop p n) end))) *)
    generalize (div2_spec x).
(* Goal: forall _ : let (p, b) := div2 x in if b then @eq nat x (Init.Nat.add (Init.Nat.mul (S (S O)) p) (S O)) else @eq nat x (Init.Nat.mul (S (S O)) p), lt x (pow2 (S (let (p, _) := div2 x in match p with | O => O | S n0 => S (loop p n) end))) *)
    destruct (div2 x) as ([ | p ],[]); intros H.
(* Goal: False *)
    simpl; omega.
(* Goal: False *)
    simpl; omega.
(* Goal: lt x (pow2 (S (S (loop (S p) n)))) *)
    specialize (IHn (S p)); spec in IHn.
(* Goal: False *)
    omega.
    simpl in IHn |- *; omega.
(* Goal: lt x (pow2 (S (S (loop (S p) n)))) *)
    specialize (IHn (S p)); spec in IHn.
(* Goal: False *)
    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.
(* Goal: le x (pow2 (find_pow2 x)) *)
    unfold find_pow2; destruct x.
(* Goal: False *)
    simpl; omega.
(* Goal: le (S x) (pow2 (S (loop (Init.Nat.pred (S x)) (S x)))) *)
    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.
(* Goal: forall (_ : lt x y) (_ : nat_sorted (@cons nat y ll)), nat_sorted (@cons nat x (@cons nat y ll)) *)
    intros H1 H2 l a m b r H3.
(* Goal: lt a b *)
    destruct l as [ | u l ].
(* Goal: lt a b *)
    inversion H3; subst.
(* Goal: lt a b *)
(* Goal: lt a b *)
    destruct m as [ | v m ].
(* Goal: lt a b *)
(* Goal: lt a b *)
(* Goal: lt a b *)
    inversion H4; subst; auto.
(* Goal: lt a b *)
(* Goal: lt a b *)
    inversion H4; subst.
(* Goal: lt a b *)
(* Goal: lt a b *)
    apply lt_trans with (1 := H1), (H2 nil _ m _ r); auto.
(* Goal: lt a b *)
    inversion H3; subst.
(* Goal: lt a b *)
    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.
(* Goal: forall (_ : @Forall nat (lt x) ll) (_ : nat_sorted ll), nat_sorted (@cons nat x ll) *)
    induction 1 as [ | y ll Hll IHl ].
(* Goal: forall _ : nat_sorted (@nil nat), nat_sorted (@cons nat x (@nil nat)) *)
(* Goal: forall _ : nat_sorted (@cons nat y l), nat_sorted (if Nat.ltb x y then @cons nat x (@cons nat y l) else if Nat.ltb y x then @cons nat y (nat_list_insert x l) else @cons nat y l) *)
    intro; apply in_nat_sorted_1.
(* Goal: forall _ : @ex nat (fun x : nat => P x), @sig nat (fun m : nat => and (P m) (forall (x : nat) (_ : lt x m), not (P x))) *)
    intros H.
(* Goal: nat_sorted (@cons nat x (@cons nat y ll)) *)
    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. 
(* Goal: forall _ : nat_sorted (@cons nat x ll), @Forall nat (lt x) ll *)
    rewrite Forall_forall; intros H y Hy.
(* Goal: lt x y *)
    apply in_split in Hy.
(* Goal: lt x y *)
    destruct Hy as (l & r & ?); subst.
(* Goal: lt x y *)
    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.
(* Goal: forall _ : nat_sorted l, P l *)
    induction l as [ [ | x [ | y l ] ] IHl ] using (measure_rect (@length _)).
(* Goal: forall _ : nat_sorted (@nil nat), P (@nil nat) *)
(* Goal: forall _ : nat_sorted (@cons nat x (@nil nat)), P (@cons nat x (@nil nat)) *)
(* Goal: forall _ : nat_sorted (@cons nat x (@cons nat y l)), P (@cons nat x (@cons nat y l)) *)
    intro; apply HP0.
(* Goal: forall _ : nat_sorted (@cons nat x (@nil nat)), P (@cons nat x (@nil nat)) *)
(* Goal: forall _ : nat_sorted (@cons nat x (@cons nat y l)), P (@cons nat x (@cons nat y l)) *)
    intro; apply HP1.
(* Goal: forall _ : nat_sorted (@cons nat x (@cons nat y l)), P (@cons nat x (@cons nat y l)) *)
    intros H; apply HP2. 
(* Goal: lt x y *)
(* Goal: P (@cons nat y l) *)
    revert H; apply nat_sorted_head_inv.
(* Goal: P (@cons nat y l) *)
    apply IHl.
(* Goal: False *)
    rew length; omega.
(* Goal: nat_sorted (@cons nat y l) *)
    revert H; apply nat_sorted_cons_inv.
  Qed.
  
End nat_sorted.

Fact nat_sorted_injective ll : nat_sorted ll -> list_injective ll.
Proof.
(* Goal: False *)
  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.
(* Goal: forall _ : nat_sorted l, nat_sorted (nat_list_insert x l) *)
  induction l as [ | y l IHl ]; simpl.
(* Goal: False *)
  omega.
(* Goal: False *)
  destruct (x <? y); simpl; try omega.
(* Goal: False *)
  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. 
  
(* Goal: forall _ : nat_sorted l, nat_sorted (nat_list_insert x l) *)
  induction l as [ | y l IHl ]; simpl.
  intro; auto.
  destruct (x <? y); destruct (y <? x).
  intro; auto.
  intro; auto.
(* Goal: @eq (prod nat bool) (div2 (Init.Nat.mul (S (S O)) O)) (@pair nat bool O false) *)
(* Goal: @eq (prod nat bool) (div2 (Init.Nat.mul (S (S O)) (S p))) (@pair nat bool (S p) false) *)
  intros ? [ [] | H ]; simpl; auto.
  apply IHl in H; simpl in H; tauto.
  intro; simpl; tauto.

(* Goal: forall _ : nat_sorted l, nat_sorted (nat_list_insert x l) *)
  induction l as [ | y l IHl ]; simpl.
  intro; auto.
(* Goal: nat_sorted (if Nat.ltb x y then @cons nat x (@cons nat y l) else if Nat.ltb y x then @cons nat y (nat_list_insert x l) else @cons nat y l) *)
  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.
(* Goal: forall (_ : P x) (_ : @Forall nat P l), @Forall nat P (nat_list_insert x l) *)
  do 2 rewrite Forall_forall; intros H1 H2 y Hy.
(* Goal: P y *)
  apply nat_list_insert_incl in Hy.
(* Goal: P y *)
  destruct Hy; subst; auto.
Qed.
  
Fact nat_list_insert_sorted x l : nat_sorted l -> nat_sorted (nat_list_insert x l).
Proof.
(* Goal: forall _ : nat_sorted l, nat_sorted (nat_list_insert x l) *)
  induction l as [ | y l IHl ]; simpl.
(* Goal: forall _ : nat_sorted (@nil nat), nat_sorted (@cons nat x (@nil nat)) *)
(* Goal: forall _ : nat_sorted (@cons nat y l), nat_sorted (if Nat.ltb x y then @cons nat x (@cons nat y l) else if Nat.ltb y x then @cons nat y (nat_list_insert x l) else @cons nat y l) *)
  intro; apply in_nat_sorted_1.
(* Goal: forall _ : @ex nat (fun x : nat => P x), @sig nat (fun m : nat => and (P m) (forall (x : nat) (_ : lt x m), not (P x))) *)
  intros H.
(* Goal: nat_sorted (if Nat.ltb x y then @cons nat x (@cons nat y l) else if Nat.ltb y x then @cons nat y (nat_list_insert x l) else @cons nat y l) *)
  generalize (Nat.ltb_lt x y) (Nat.ltb_lt y x).
(* Goal: forall (_ : iff (@eq bool (Nat.ltb x y) true) (lt x y)) (_ : iff (@eq bool (Nat.ltb y x) true) (lt y x)), nat_sorted (if Nat.ltb x y then @cons nat x (@cons nat y l) else if Nat.ltb y x then @cons nat y (nat_list_insert x l) else @cons nat y l) *)
  destruct (x <? y); destruct (y <? x); intros H1 H2.
(* Goal: nat_sorted (@cons nat x (@cons nat y l)) *)
(* Goal: nat_sorted (@cons nat x (@cons nat y l)) *)
(* Goal: nat_sorted (@cons nat y (nat_list_insert x l)) *)
(* Goal: nat_sorted (@cons nat y l) *)
  apply proj1 in H1; spec in H1; auto.
(* Goal: nat_sorted (@cons nat x (@cons nat y l)) *)
(* Goal: nat_sorted (@cons nat x (@cons nat y l)) *)
(* Goal: nat_sorted (@cons nat y (nat_list_insert x l)) *)
(* Goal: nat_sorted (@cons nat y l) *)
  apply proj1 in H2; spec in H2; auto.
(* Goal: False *)
  omega.
(* Goal: nat_sorted (@cons nat x (@cons nat y l)) *)
(* Goal: nat_sorted (@cons nat y (nat_list_insert x l)) *)
(* Goal: nat_sorted (@cons nat y l) *)
  apply in_nat_sorted_2; auto; tauto.
(* Goal: nat_sorted (@cons nat y (nat_list_insert x l)) *)
(* Goal: nat_sorted (@cons nat y l) *)
  apply in_nat_sorted_3.
(* Goal: @Forall nat (lt y) (nat_list_insert x l) *)
(* Goal: nat_sorted (nat_list_insert x l) *)
(* Goal: nat_sorted (@cons nat y l) *)
  apply nat_list_insert_Forall.
(* Goal: lt y x *)
(* Goal: @Forall nat (lt y) l *)
(* Goal: nat_sorted (nat_list_insert x l) *)
(* Goal: nat_sorted (@cons nat y l) *)
  tauto.
(* Goal: @Forall nat (lt y) l *)
(* Goal: nat_sorted (nat_list_insert x l) *)
(* Goal: nat_sorted (@cons nat y l) *)
  apply nat_sorted_Forall; auto.
(* Goal: nat_sorted (@cons nat y l) *)
  apply IHl; revert H; apply nat_sorted_cons_inv.
(* Goal: nat_sorted (@cons nat y l) *)
  auto.
Qed.

Definition nat_sort := fold_right (nat_list_insert) nil.

Fact nat_sort_length l : length (nat_sort l) <= length l.
Proof.
(* Goal: le (@length nat (nat_sort l)) (@length nat l) *)
  induction l as [ | x l IHl ]; simpl.
(* Goal: False *)
  omega.
(* Goal: False *)
  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.
(* Goal: nat_sorted (@cons nat y l) *)
  induction l as [ | x l IHl ]; simpl; split; intros y Hy; auto.
(* Goal: @In nat y (@cons nat x l) *)
(* Goal: @In nat y (nat_list_insert x (nat_sort l)) *)
  apply nat_list_insert_incl in Hy; simpl.
(* Goal: nat_sorted (@cons nat y l) *)
  destruct Hy as [ | Hy ]; auto; right; apply IHl; auto.
(* Goal: @In nat y (nat_list_insert x (nat_sort l)) *)
  apply nat_list_insert_incl.
(* Goal: nat_sorted (@cons nat y l) *)
  destruct Hy; [ left | right ]; auto.
(* Goal: nat_sorted (@cons nat y l) *)
  apply IHl; auto.
Qed.

Fact nat_sort_sorted l : nat_sorted (nat_sort l).
Proof.
(* Goal: nat_sorted (nat_sort l) *)
  induction l as [ | x l IHl ].
(* Goal: nat_sorted (nat_sort (@nil nat)) *)
(* Goal: nat_sorted (nat_sort (@cons nat x l)) *)
  apply in_nat_sorted_0.
(* Goal: nat_sorted (@cons nat y l) *)
  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.
(* Goal: forall (_ : forall (x : nat) (_ : and (le a x) (lt x b)), lt (f x) (f (S x))) (x y : nat) (_ : and (and (le a x) (lt x y)) (le y b)), lt (f x) (f y) *)
  intros H1.
  assert (forall n m, n <= m <= b - a -> f (a+n) <= f (a+m)) as H2.
(* Goal: forall (n m : nat) (_ : and (le n m) (le m (Init.Nat.sub b a))), le (f (Init.Nat.add a n)) (f (Init.Nat.add a m)) *)
(* Goal: forall (x y : nat) (_ : and (and (le a x) (lt x y)) (le y b)), lt (f x) (f y) *)
    intros n m (H2 & H3); revert H2 H3.
(* Goal: nat_sorted (@cons nat y l) *)
    induction 1 as [ | m Hm IH ]; auto.
(* Goal: False *)
    intros H. spec in IH. omega.
(* Goal: le (f (Init.Nat.add a n)) (f (Init.Nat.add a (S m))) *)
(* Goal: forall (x y : nat) (_ : and (and (le a x) (lt x y)) (le y b)), lt (f x) (f y) *)
    apply le_trans with (1 := IH).
    replace (a+S m) with (S (a+m)) by omega.
(* Goal: False *)
    apply lt_le_weak, H1; omega.
  assert (forall n m, n < m <= b - a -> f (a+n) < f (a+m)) as H3.
(* Goal: forall (n m : nat) (_ : and (lt n m) (le m (Init.Nat.sub b a))), lt (f (Init.Nat.add a n)) (f (Init.Nat.add a m)) *)
(* Goal: forall (x y : nat) (_ : and (and (le a x) (lt x y)) (le y b)), lt (f x) (f y) *)
    unfold lt at 1; intros n m H.
    specialize (H1 (a+n)).
(* Goal: lt (f (Init.Nat.add a n)) (f (Init.Nat.add a m)) *)
(* Goal: forall (x y : nat) (_ : and (and (le a x) (lt x y)) (le y b)), lt (f x) (f y) *)
    spec in H1.
(* Goal: False *)
    omega.
(* Goal: lt (f (Init.Nat.add a n)) (f (Init.Nat.add a m)) *)
(* Goal: forall (x y : nat) (_ : and (and (le a x) (lt x y)) (le y b)), lt (f x) (f y) *)
    apply lt_le_trans with (1 := H1).
    replace (S (a+n)) with (a+S n) by omega.
(* Goal: nat_sorted (@cons nat y l) *)
    apply H2; auto.
(* Goal: forall (x y : nat) (_ : and (and (le a x) (lt x y)) (le y b)), lt (f x) (f y) *)
  intros x y H4.
  replace x with (a+(x-a)) by omega.
  replace y with (a+(y-a)) by omega.
(* Goal: lt (f (Init.Nat.add a (Init.Nat.sub x a))) (f (Init.Nat.add a (Init.Nat.sub y a))) *)
  apply H3.
(* Goal: False *)
  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.
(* Goal: forall (_ : forall (x y : nat) (_ : and (and (le a x) (lt x y)) (le y b)), lt (f x) (f y)) (x y : nat) (_ : and (le a x) (le x b)) (_ : and (le a y) (le y b)) (_ : @eq nat (f x) (f y)), @eq nat x y *)
  intros H0 x y Hx Hy.
(* Goal: forall _ : @eq nat (f x) (f y), @eq nat x y *)
  destruct Hx; destruct Hy.
(* Goal: nat_sorted (@cons nat y l) *)
  destruct (lt_eq_lt_dec x y) as [ [ ? | ? ] | ? ]; auto.
(* Goal: forall _ : @eq nat (f x) (f y), @eq nat x y *)
(* Goal: forall _ : @eq nat (f x) (f y), @eq nat x y *)
  specialize (H0 x y).
(* Goal: False *)
  spec in H0; repeat split; auto; intro; omega.
(* Goal: forall _ : @eq nat (f x) (f y), @eq nat x y *)
  specialize (H0 y x).
(* Goal: False *)
  spec in H0; repeat split; auto; intro; omega.
Qed.

Theorem nat_rev_ind (P : nat -> Prop) (HP : forall n, P (S n) -> P n) x y : x <= y -> P y -> P x.
Proof. induction 1; auto. Qed.

Section nat_rev_bounded_ind.

  Variables (k : nat) (P : nat -> Prop) (HP : forall n, S n <= k -> P (S n) -> P n).
  
  Fact nat_rev_bounded_ind x y : x <= y <= k -> P y -> P x.
  Proof.
(* Goal: forall (_ : and (le x y) (le y k)) (_ : P y), P x *)
    intros H1 H2.
(* Goal: P x *)
    refine (proj1 (@nat_rev_ind (fun n => P n /\ n <= k) _ x y _ _)).
(* Goal: False *)
    clear x y H1 H2; intros n (H1 & H2); split; auto;omega.
(* Goal: False *)
    omega.
(* Goal: False *)
    split; auto; omega.
  Qed.

End nat_rev_bounded_ind.

Section nat_minimize.

  Variable P : nat -> Prop.
  Hypothesis HP : forall n, { P n } + { ~ P n }.

  Local Inductive bar_min (n : nat) : Prop :=
    | in_bar_min_0 : P n -> bar_min n
    | in_bar_min_1 : bar_min (S n) -> bar_min n.

  Section nat_min.

(* Goal: forall (i : nat) (_ : lt i n), @ex X (fun x : X => R (S i) x) *)
(* Goal: @ex (forall (x : nat) (_ : lt x (S n)), X) (fun s : forall (x : nat) (_ : lt x (S n)), X => forall (i : nat) (Hi : lt i (S n)), R i (s i Hi)) *)
    Let min_rec : forall n, bar_min n -> { m | P m /\ forall x, P x -> x < n \/ m <= x }.
    Proof.
      refine (fix loop n Hn := match HP n with
        | left H  => exist _ n _
        | right H => match loop (S n) _ with
          | exist _ m Hm => exist _ m _
        end
      end).
      * split; auto; intros; omega.
      * destruct Hn; auto; destruct H; auto.
      * destruct Hm as [ H1 H2 ]; split; auto.
(* Goal: forall (x : nat) (_ : P x), or (lt x n) (le m x) *)
        intros x Hx; specialize (H2 x Hx).
(* Goal: or (lt x n) (le m x) *)
        destruct (eq_nat_dec x n).
        - subst; tauto.
        - omega.
    Qed.

(* Goal: forall (i : nat) (_ : lt i n), @ex X (fun x : X => R (S i) x) *)
(* Goal: @ex (forall (x : nat) (_ : lt x (S n)), X) (fun s : forall (x : nat) (_ : lt x (S n)), X => forall (i : nat) (Hi : lt i (S n)), R i (s i Hi)) *)
    Definition min_dec : (exists n, P n) -> { m | P m /\ forall x, P x -> m <= x }.
    Proof.
(* Goal: forall _ : @ex nat (fun x : nat => P x), @sig nat (fun m : nat => and (P m) (forall (x : nat) (_ : lt x m), not (P x))) *)
      intros H.
(* Goal: @sig nat (fun m : nat => and (P m) (forall (x : nat) (_ : P x), le m x)) *)
      destruct (@min_rec 0) as (m & H1 & H2).
      * destruct H as (n & Hn).
(* Goal: bar_min O *)
        apply in_bar_min_0 in Hn.
(* Goal: bar_min O *)
        revert Hn; apply nat_rev_ind.
(* Goal: forall (n : nat) (_ : bar_min (S n)), bar_min n *)
(* Goal: le O n *)
        apply in_bar_min_1.
(* Goal: False *)
        omega.
      * exists m; split; auto.
(* Goal: False *)
        intros x Hx; specialize (H2 _ Hx); omega.
    Defined.

  End nat_min.

(* Goal: forall (i : nat) (_ : lt i n), @ex X (fun x : X => R (S i) x) *)
(* Goal: @ex (forall (x : nat) (_ : lt x (S n)), X) (fun s : forall (x : nat) (_ : lt x (S n)), X => forall (i : nat) (Hi : lt i (S n)), R i (s i Hi)) *)
  Fact first_which : (exists x, P x) -> { m | P m /\ forall x, x < m -> ~ P x }.
  Proof.
(* Goal: forall _ : @ex nat (fun x : nat => P x), @sig nat (fun m : nat => and (P m) (forall (x : nat) (_ : lt x m), not (P x))) *)
    intros H.
(* Goal: @sig nat (fun m : nat => and (P m) (forall (x : nat) (_ : lt x m), not (P x))) *)
    destruct (min_dec H) as (m & H1 & H2).
(* Goal: nat_sorted (@cons nat y l) *)
    exists m; split; auto.
(* Goal: forall (x : nat) (_ : lt x m), not (P x) *)
    intros x Hx H3.
(* Goal: False *)
    apply H2 in H3.
(* Goal: False *)
    omega.
  Qed.

End nat_minimize.

Section first_which_ni.

  Variable P : nat -> Prop.

  Fact bounded_search_ni n : (forall i, i < n -> P i \/ ~ P i) -> (forall i, i < n -> ~ P i) \/ exists i, i < n /\ P i /\ forall j, j < i -> ~ P j.
  Proof.
(* Goal: forall _ : forall (i : nat) (_ : lt i n), or (P i) (not (P i)), or (forall (i : nat) (_ : lt i n), not (P i)) (@ex nat (fun i : nat => and (lt i n) (and (P i) (forall (j : nat) (_ : lt j i), not (P j))))) *)
    revert P; induction n as [ | n IHn ]; intros P HP.
    + left; intros; omega.
    + destruct (HP 0) as [ H | H ]; try omega.
      - right; exists 0; split; try omega; split; auto; intros; omega.
      - destruct IHn with (P := fun n => P (S n)) as [ H1 | (x & H1 & H2 & H3) ].
        * intros; apply HP; omega.
        * left; intros [] ?; auto; apply H1; omega.
        * right; exists (S x); split; try omega; split; auto.
(* Goal: False *)
          intros [] ?; auto; apply H3; omega.
  Qed.
  
  Hypothesis HP : forall n, P n \/ ~ P n.

  Fact first_which_ni : (exists x, P x) -> exists m, P m /\ forall x, x < m -> ~ P x.
  Proof.
(* Goal: forall _ : @ex nat (fun x : nat => P x), @ex nat (fun m : nat => and (P m) (forall (x : nat) (_ : lt x m), not (P x))) *)
    intros (n & Hn).
(* Goal: @ex nat (fun m : nat => and (P m) (forall (x : nat) (_ : lt x m), not (P x))) *)
    destruct (@bounded_search_ni (S n)) as [ H1 | (m & H1 & H2 & H3) ].
    + intros; auto.
    + contradict Hn; apply H1; omega.
    + exists m; auto.
  Qed.

End first_which_ni.
