From Stdlib Require Import Utf8 Arith.
Require Import Init.Nat.
Require Import Core.
Require Import Misc.

Class excl_midd := { em_prop : ∀ P, P + notT P }.

Definition forall_or_exists_not {T} (P : T → Prop) :=
  {∀ x, P x} + {∃ x, ¬ P x}.

Theorem rl_forall_or_exists_not {em : excl_midd} {T} :
  ∀ (P : T → Prop), forall_or_exists_not P.

Theorem rl_not_forall_exists {em : excl_midd} {T} :
  ∀ (P : T → Prop), ¬ (∀ x, ¬ P x) → ∃ x, P x.

Section a.

Context {T : Type}.
Context {ro : ring_like_op T}.
Context {rp : ring_like_prop T}.
Context {em : excl_midd}.


Definition is_bound (le : T → T → Prop) (P : T → Type) c :=
  rl_forall_or_exists_not (λ x : T, P x → le x c).

Arguments is_bound le P c%_L.

Definition is_upper_bound := is_bound (λ a b, (a ≤ b)%L).
Definition is_lower_bound := is_bound (λ a b, (b ≤ a)%L).

Definition is_extremum le (Q : T → Type) c :=
  bool_of_sumbool (is_bound le Q c) = true ∧
  ∀ c', if is_bound le Q c' then le c c' else True.

Definition is_supremum := is_extremum (λ a b, (a ≤ b)%L).
Definition is_infimum := is_extremum (λ a b, (b ≤ a)%L).

Arguments is_extremum le Q c%_L.
Arguments is_supremum Q c%_L.
Arguments is_infimum Q c%_L.

Fixpoint bisection (P : T → bool) lb ub n :=
  match n with
  | 0 ⇒ lb
  | S n' ⇒
      let x := ((lb + ub) / 2)%L in
      if P x then bisection P x ub n'
      else bisection P lb x n'
  end.

Fixpoint AnBn (P : T → Type) (an bn : T) n :=
  match n with
  | 0 ⇒ (an, bn)
  | S n' ⇒
      let a := ((an + bn) / 2)%L in
      if is_upper_bound P a then AnBn P an a n'
      else AnBn P a bn n'
  end.

Theorem rngl_middle_in_middle :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a ≤ b → a ≤ (a + b) / 2 ≤ b)%L.
Theorem AnBn_interval :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a ≤ b)%L →
  ∀ P n an bn,
  AnBn P a b n = (an, bn)
  → (a ≤ an ≤ bn ≤ b)%L ∧
    bn = (an + (b - a) / 2 ^ n)%L.
Theorem AnBn_le :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a ≤ b)%L →
  ∀ P p q ap bp aq bq,
  p ≤ q
  → AnBn P a b p = (ap, bp)
  → AnBn P a b q = (aq, bq)
  → (ap ≤ aq ∧ bq ≤ bp)%L.
Theorem rngl_abs_AnBn_sub_AnBn_le :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a ≤ b)%L →
  ∀ P p q, p ≤ q →
  ∀ ap bp aq bq,
  AnBn P a b p = (ap, bp)
  → AnBn P a b q = (aq, bq)
  → (rngl_abs (ap - aq) ≤ (b - a) / 2 ^ p)%L ∧
    (rngl_abs (bp - bq) ≤ (b - a) / 2 ^ p)%L.
Context {Hop : rngl_has_opp T = true}.
Context {Hor : rngl_is_ordered T = true}.

Definition rngl_distance :=
  {| d_dist := rngl_dist; d_prop := rngl_dist_is_dist Hop Hor |}.

Theorem An_Bn_are_Cauchy_sequences :
  rngl_has_inv T = true →
  rngl_is_archimedean T = true →
  ∀ P a b, (a ≤ b)%L →
  is_Cauchy_sequence rngl_dist (λ n : nat, fst (AnBn P a b n)) ∧
  is_Cauchy_sequence rngl_dist (λ n : nat, snd (AnBn P a b n)).
Theorem rngl_abs_An_Bn_le :
  rngl_has_inv T = true →
  ∀ a b, (a ≤ b)%L →
  ∀ P n an bn,
  AnBn P a b n = (an, bn)
  → (rngl_abs (an - bn) ≤ (b - a) / 2 ^ n)%L.

Theorem limit_opp :
  ∀ u lim,
  is_limit_when_seq_tends_to_inf rngl_dist u lim
  → is_limit_when_seq_tends_to_inf rngl_dist (λ n, (- u n)%L) (- lim)%L.

Theorem gen_limit_ext_in :
  ∀ {A} (da : A → A → T) u v lim,
  (∀ n, u n = v n)
  → is_limit_when_seq_tends_to_inf da u lim
  → is_limit_when_seq_tends_to_inf da v lim.

Theorem limit_between_An_and_Bn :
  rngl_has_inv T = true →
  ∀ a b lim P,
  (a ≤ b)%L
  → is_limit_when_seq_tends_to_inf rngl_dist (λ n, fst (AnBn P a b n)) lim
  → is_limit_when_seq_tends_to_inf rngl_dist (λ n, snd (AnBn P a b n)) lim
  → ∀ n an bn, AnBn P a b n = (an, bn) → (an ≤ lim ≤ bn)%L.
Theorem AnBn_exists_P :
  ∀ (P : _ → Prop) a b x,
  (∀ x : T, P x → (x ≤ b)%L)
  → (a ≤ x)%L
  → P x
  → ∀ n an bn,
  AnBn P a b n = (an, bn)
  → ∃ y, (an ≤ y ≤ bn)%L ∧ P y.
Theorem in_AnBn :
  ∀ (P : _ → Prop) a b,
  P a
  → (∀ x, P x → (x ≤ b)%L)
  → ∀ n an bn,
  AnBn P a b n = (an, bn)
  → ∃ y : T, (an ≤ y ≤ bn)%L ∧ P y.

Theorem AnBn_not_P :
  ∀ (P : _ → Prop) a b n an bn,
  (∀ x : T, P x → (x ≤ b)%L)
  → AnBn P a b n = (an, bn)
  → ∀ y, (bn < y → ¬ P y)%L.
Theorem after_AnBn :
  ∀ (P : _ → Prop) a b,
  P a
  → (∀ x : T, P x → (x ≤ b)%L)
  → ∀ n an bn,
  AnBn P a b n = (an, bn)
  → ∀ y, (bn < y)%L
  → ¬ P y.

Theorem intermediate_value_prop_1 :
  rngl_has_inv T = true →
  ∀ f,
  is_continuous rngl_le rngl_dist rngl_dist f →
  ∀ a b c u,
  (a < b)%L
  → (f a < u)%L
  → (∀ x, (a ≤ x ≤ b)%L ∧ (f x < u)%L → (x ≤ c)%L)
  → c ≠ a.

Theorem intermediate_value_prop_2 :
  rngl_has_inv T = true →
  ∀ f, is_continuous rngl_le rngl_dist rngl_dist f →
  ∀ a b c u,
  (a < b)%L
  → (u < f b)%L
  → (∀ c',
       if is_upper_bound (λ x : T, (a ≤ x ≤ b)%L ∧ (f x < u)%L) c' then
         (c ≤ c')%L
       else True)
  → c ≠ b.

Theorem rngl_not_le_le : ∀ a b, ¬ (a ≤ b)%L → (b ≤ a)%L.

Theorem exists_supremum :
  rngl_has_inv T = true →
  rngl_is_archimedean T = true →
  is_complete T rngl_dist →
  ∀ (P : T → Prop) a b,
  P a
  → (∀ x, P x → (x ≤ b)%L)
  → ∃ c, is_supremum P c ∧ (c ≤ b)%L ∧
    is_limit_when_seq_tends_to_inf rngl_dist (λ n, fst (AnBn P a b n)) c ∧
    is_limit_when_seq_tends_to_inf rngl_dist (λ n, snd (AnBn P a b n)) c.
Theorem intermediate_value_le :
  rngl_has_inv T = true →
  rngl_is_archimedean T = true →
  is_complete T rngl_dist →
  ∀ f, is_continuous rngl_le rngl_dist rngl_dist f
  → ∀ a b u, (a ≤ b)%L
  → (f a ≤ u ≤ f b)%L
  → ∃ c : T, (a ≤ c ≤ b)%L ∧ f c = u.
Theorem supremum_opp :
  ∀ (P Q : _ → Prop) c,
  (∀ x, P x ↔ Q (- x)%L)
  → is_supremum P c
  → is_infimum Q (- c).


Theorem upper_bound_property :
  rngl_has_inv T = true →
  rngl_is_archimedean T = true →
  is_complete T rngl_dist →
  ∀ (P : T → Prop) a b,
  P a
  → (∀ x, P x → (x ≤ b)%L)
  → ∃ c, is_supremum P c ∧ (c ≤ b)%L.

Theorem lower_bound_property :
  rngl_has_inv T = true →
  rngl_is_archimedean T = true →
  is_complete T rngl_dist →
  ∀ (P : T → Prop) a b,
  P b
  → (∀ x, P x → (a ≤ x)%L)
  → ∃ c, is_infimum P c ∧ (a ≤ c)%L.

Theorem intermediate_value :
  rngl_has_inv T = true →
  rngl_is_archimedean T = true →
  is_complete T rngl_dist →
  ∀ f, is_continuous rngl_le rngl_dist rngl_dist f
  → ∀ a b u, (a ≤ b)%L
  → (rngl_min (f a) (f b) ≤ u ≤ rngl_max (f a) (f b))%L
  → ∃ c, (a ≤ c ≤ b)%L ∧ f c = u.

End a.

Arguments is_infimum {T ro em} Q c%_L.
Arguments is_lower_bound {T ro em} P c%_L.
Arguments upper_bound_property {T ro rp} _ Hop Hor Hiv Har Hco P (a b)%_L.