Require Import Reals.
Require Import mathcomp.ssreflect.ssreflect.
Require Import Rcomplements.

Open Scope R_scope.

Inductive Rbar :=
  | Finite : R → Rbar
  | p_infty : Rbar
  | m_infty : Rbar.
Definition real (x : Rbar) :=
  match x with
    | Finite x ⇒ x
    | _ ⇒ 0
  end.
Coercion Finite : R >-> Rbar.
Coercion real : Rbar >-> R.

Definition is_finite (x : Rbar) := Finite (real x) = x.
Lemma is_finite_correct (x : Rbar) :
  is_finite x ↔ ∃ y : R, x = Finite y.

Definition Rbar_lt (x y : Rbar) : Prop :=
  match x,y with
    | p_infty, _ | _, m_infty ⇒ False
    | m_infty, _ | _, p_infty ⇒ True
    | Finite x, Finite y ⇒ Rlt x y
  end.

Definition Rbar_le (x y : Rbar) : Prop :=
  match x,y with
    | m_infty, _ | _, p_infty ⇒ True
    | p_infty, _ | _, m_infty ⇒ False
    | Finite x, Finite y ⇒ Rle x y
  end.

Definition Rbar_opp (x : Rbar) :=
  match x with
    | Finite x ⇒ Finite (-x)
    | p_infty ⇒ m_infty
    | m_infty ⇒ p_infty
  end.

Definition Rbar_plus' (x y : Rbar) :=
  match x,y with
    | p_infty, m_infty | m_infty, p_infty ⇒ None
    | p_infty, _ | _, p_infty ⇒ Some p_infty
    | m_infty, _ | _, m_infty ⇒ Some m_infty
    | Finite x', Finite y' ⇒ Some (Finite (x' + y'))
  end.
Definition Rbar_plus (x y : Rbar) :=
  match Rbar_plus' x y with Some z ⇒ z | None ⇒ Finite 0 end.
Definition is_Rbar_plus (x y z : Rbar) : Prop :=
  Rbar_plus' x y = Some z.
Definition ex_Rbar_plus (x y : Rbar) : Prop :=
  match Rbar_plus' x y with Some _ ⇒ True | None ⇒ False end.

Lemma is_Rbar_plus_unique (x y z : Rbar) :
  is_Rbar_plus x y z → Rbar_plus x y = z.
Lemma Rbar_plus_correct (x y : Rbar) :
  ex_Rbar_plus x y → is_Rbar_plus x y (Rbar_plus x y).

Definition Rbar_minus (x y : Rbar) := Rbar_plus x (Rbar_opp y).
Definition is_Rbar_minus (x y z : Rbar) : Prop :=
  is_Rbar_plus x (Rbar_opp y) z.
Definition ex_Rbar_minus (x y : Rbar) : Prop :=
  ex_Rbar_plus x (Rbar_opp y).

Definition Rbar_inv (x : Rbar) : Rbar :=
  match x with
    | Finite x ⇒ Finite (/x)
    | _ ⇒ Finite 0
  end.

Definition Rbar_mult' (x y : Rbar) :=
  match x with
    | Finite x ⇒ match y with
      | Finite y ⇒ Some (Finite (x × y))
      | p_infty ⇒ match (Rle_dec 0 x) with
        | left H ⇒ match Rle_lt_or_eq_dec _ _ H with left _ ⇒ Some p_infty | right _ ⇒ None end
        | right _ ⇒ Some m_infty
      end
      | m_infty ⇒ match (Rle_dec 0 x) with
        | left H ⇒ match Rle_lt_or_eq_dec _ _ H with left _ ⇒ Some m_infty | right _ ⇒ None end
        | right _ ⇒ Some p_infty
      end
    end
    | p_infty ⇒ match y with
      | Finite y ⇒ match (Rle_dec 0 y) with
        | left H ⇒ match Rle_lt_or_eq_dec _ _ H with left _ ⇒ Some p_infty | right _ ⇒ None end
        | right _ ⇒ Some m_infty
      end
      | p_infty ⇒ Some p_infty
      | m_infty ⇒ Some m_infty
    end
    | m_infty ⇒ match y with
      | Finite y ⇒ match (Rle_dec 0 y) with
        | left H ⇒ match Rle_lt_or_eq_dec _ _ H with left _ ⇒ Some m_infty | right _ ⇒ None end
        | right _ ⇒ Some p_infty
      end
      | p_infty ⇒ Some m_infty
      | m_infty ⇒ Some p_infty
    end
  end.
Definition Rbar_mult (x y : Rbar) :=
  match Rbar_mult' x y with Some z ⇒ z | None ⇒ Finite 0 end.

Definition is_Rbar_mult (x y z : Rbar) : Prop :=
  Rbar_mult' x y = Some z.
Definition ex_Rbar_mult (x y : Rbar) : Prop :=
  match x with
    | Finite x ⇒ match y with
      | Finite y ⇒ True
      | p_infty ⇒ x ≠ 0
      | m_infty ⇒ x ≠ 0
    end
    | p_infty ⇒ match y with
      | Finite y ⇒ y ≠ 0
      | p_infty ⇒ True
      | m_infty ⇒ True
    end
    | m_infty ⇒ match y with
      | Finite y ⇒ y ≠ 0
      | p_infty ⇒ True
      | m_infty ⇒ True
    end
  end.

Definition Rbar_mult_pos (x : Rbar) (y : posreal) :=
  match x with
    | Finite x ⇒ Finite (x×y)
    | _ ⇒ x
  end.

Lemma is_Rbar_mult_unique (x y z : Rbar) :
  is_Rbar_mult x y z → Rbar_mult x y = z.
Lemma Rbar_mult_correct (x y : Rbar) :
  ex_Rbar_mult x y → is_Rbar_mult x y (Rbar_mult x y).
Lemma Rbar_mult_correct' (x y z : Rbar) :
  is_Rbar_mult x y z → ex_Rbar_mult x y.

Definition Rbar_div (x y : Rbar) : Rbar :=
  Rbar_mult x (Rbar_inv y).
Definition is_Rbar_div (x y z : Rbar) : Prop :=
  is_Rbar_mult x (Rbar_inv y) z.
Definition ex_Rbar_div (x y : Rbar) : Prop :=
  ex_Rbar_mult x (Rbar_inv y).
Definition Rbar_div_pos (x : Rbar) (y : posreal) :=
  match x with
    | Finite x ⇒ Finite (x/y)
    | _ ⇒ x
  end.

Lemma Rbar_finite_eq (x y : R) :
  Finite x = Finite y ↔ x = y.
Lemma Rbar_finite_neq (x y : R) :
  Finite x ≠ Finite y ↔ x ≠ y.

Lemma Rbar_lt_not_eq (x y : Rbar) :
  Rbar_lt x y → x≠y.

Lemma Rbar_not_le_lt (x y : Rbar) :
  ¬ Rbar_le x y → Rbar_lt y x.

Lemma Rbar_lt_not_le (x y : Rbar) :
  Rbar_lt y x → ¬ Rbar_le x y.

Lemma Rbar_not_lt_le (x y : Rbar) :
  ¬ Rbar_lt x y → Rbar_le y x.

Lemma Rbar_le_not_lt (x y : Rbar) :
  Rbar_le y x → ¬ Rbar_lt x y.

Lemma Rbar_le_refl :
  ∀ x : Rbar, Rbar_le x x.

Lemma Rbar_lt_le :
  ∀ x y : Rbar,
  Rbar_lt x y → Rbar_le x y.

Lemma Rbar_total_order (x y : Rbar) :
  {Rbar_lt x y} + {x = y} + {Rbar_lt y x}.

Lemma Rbar_eq_dec (x y : Rbar) :
  {x = y} + {x ≠ y}.

Lemma Rbar_lt_dec (x y : Rbar) :
  {Rbar_lt x y} + {¬Rbar_lt x y}.

Lemma Rbar_lt_le_dec (x y : Rbar) :
  {Rbar_lt x y} + {Rbar_le y x}.

Lemma Rbar_le_dec (x y : Rbar) :
  {Rbar_le x y} + {¬Rbar_le x y}.

Lemma Rbar_le_lt_dec (x y : Rbar) :
  {Rbar_le x y} + {Rbar_lt y x}.

Lemma Rbar_le_lt_or_eq_dec (x y : Rbar) :
  Rbar_le x y → { Rbar_lt x y } + { x = y }.

Lemma Rbar_lt_trans (x y z : Rbar) :
  Rbar_lt x y → Rbar_lt y z → Rbar_lt x z.

Lemma Rbar_lt_le_trans (x y z : Rbar) :
  Rbar_lt x y → Rbar_le y z → Rbar_lt x z.

Lemma Rbar_le_lt_trans (x y z : Rbar) :
  Rbar_le x y → Rbar_lt y z → Rbar_lt x z.

Lemma Rbar_le_trans (x y z : Rbar) :
  Rbar_le x y → Rbar_le y z → Rbar_le x z.

Lemma Rbar_le_antisym (x y : Rbar) :
  Rbar_le x y → Rbar_le y x → x = y.

Lemma Rbar_opp_involutive (x : Rbar) : (Rbar_opp (Rbar_opp x)) = x.

Lemma Rbar_opp_lt (x y : Rbar) : Rbar_lt (Rbar_opp x) (Rbar_opp y) ↔ Rbar_lt y x.

Lemma Rbar_opp_le (x y : Rbar) : Rbar_le (Rbar_opp x) (Rbar_opp y) ↔ Rbar_le y x.

Lemma Rbar_opp_eq (x y : Rbar) : (Rbar_opp x) = (Rbar_opp y) ↔ x = y.

Lemma Rbar_opp_real (x : Rbar) : real (Rbar_opp x) = - real x.

Lemma Rbar_plus'_comm :
  ∀ x y, Rbar_plus' x y = Rbar_plus' y x.

Lemma ex_Rbar_plus_comm :
  ∀ x y,
  ex_Rbar_plus x y → ex_Rbar_plus y x.

Lemma ex_Rbar_plus_opp (x y : Rbar) :
  ex_Rbar_plus x y → ex_Rbar_plus (Rbar_opp x) (Rbar_opp y).

Lemma Rbar_plus_0_r (x : Rbar) : Rbar_plus x (Finite 0) = x.
Lemma Rbar_plus_0_l (x : Rbar) : Rbar_plus (Finite 0) x = x.

Lemma Rbar_plus_comm (x y : Rbar) : Rbar_plus x y = Rbar_plus y x.

Lemma Rbar_plus_lt_compat (a b c d : Rbar) :
  Rbar_lt a b → Rbar_lt c d → Rbar_lt (Rbar_plus a c) (Rbar_plus b d).

Lemma Rbar_plus_le_compat (a b c d : Rbar) :
  Rbar_le a b → Rbar_le c d → Rbar_le (Rbar_plus a c) (Rbar_plus b d).

Lemma Rbar_plus_opp (x y : Rbar) :
  Rbar_plus (Rbar_opp x) (Rbar_opp y) = Rbar_opp (Rbar_plus x y).

Lemma Rbar_minus_eq_0 (x : Rbar) : Rbar_minus x x = 0.
Lemma Rbar_opp_minus (x y : Rbar) :
  Rbar_opp (Rbar_minus x y) = Rbar_minus y x.

Lemma Rbar_inv_opp (x : Rbar) :
  x ≠ 0 → Rbar_inv (Rbar_opp x) = Rbar_opp (Rbar_inv x).

Lemma Rbar_mult'_comm (x y : Rbar) :
  Rbar_mult' x y = Rbar_mult' y x.

Lemma Rbar_mult'_opp_r (x y : Rbar) :
  Rbar_mult' x (Rbar_opp y) = match Rbar_mult' x y with Some z ⇒ Some (Rbar_opp z) | None ⇒ None end.

Lemma Rbar_mult_comm (x y : Rbar) :
  Rbar_mult x y = Rbar_mult y x.
Lemma Rbar_mult_opp_r (x y : Rbar) :
  Rbar_mult x (Rbar_opp y) = (Rbar_opp (Rbar_mult x y)).
Lemma Rbar_mult_opp_l (x y : Rbar) :
  Rbar_mult (Rbar_opp x) y = Rbar_opp (Rbar_mult x y).
Lemma Rbar_mult_opp (x y : Rbar) :
  Rbar_mult (Rbar_opp x) (Rbar_opp y) = Rbar_mult x y.
Lemma Rbar_mult_0_l (x : Rbar) : Rbar_mult 0 x = 0.
Lemma Rbar_mult_0_r (x : Rbar) : Rbar_mult x 0 = 0.

Lemma Rbar_mult_eq_0 (y x : Rbar) :
  Rbar_mult x y = 0 → x = 0 ∨ y = 0.

Lemma ex_Rbar_mult_sym (x y : Rbar) :
  ex_Rbar_mult x y → ex_Rbar_mult y x.
Lemma ex_Rbar_mult_opp_l (x y : Rbar) :
  ex_Rbar_mult x y → ex_Rbar_mult (Rbar_opp x) y.
Lemma ex_Rbar_mult_opp_r (x y : Rbar) :
  ex_Rbar_mult x y → ex_Rbar_mult x (Rbar_opp y).

Lemma is_Rbar_mult_sym (x y z : Rbar) :
  is_Rbar_mult x y z → is_Rbar_mult y x z.
Lemma is_Rbar_mult_opp_l (x y z : Rbar) :
  is_Rbar_mult x y z → is_Rbar_mult (Rbar_opp x) y (Rbar_opp z).
Lemma is_Rbar_mult_opp_r (x y z : Rbar) :
  is_Rbar_mult x y z → is_Rbar_mult x (Rbar_opp y) (Rbar_opp z).

Lemma is_Rbar_mult_p_infty_pos (x : Rbar) :
  Rbar_lt 0 x → is_Rbar_mult p_infty x p_infty.
Lemma is_Rbar_mult_p_infty_neg (x : Rbar) :
  Rbar_lt x 0 → is_Rbar_mult p_infty x m_infty.
Lemma is_Rbar_mult_m_infty_pos (x : Rbar) :
  Rbar_lt 0 x → is_Rbar_mult m_infty x m_infty.
Lemma is_Rbar_mult_m_infty_neg (x : Rbar) :
  Rbar_lt x 0 → is_Rbar_mult m_infty x p_infty.

Lemma is_Rbar_div_p_infty (x : R) :
  is_Rbar_div x p_infty 0.
Lemma is_Rbar_div_m_infty (x : R) :
  is_Rbar_div x m_infty 0.

Lemma Rbar_mult_pos_eq (x y : Rbar) (z : posreal) :
  x = y ↔ (Rbar_mult_pos x z) = (Rbar_mult_pos y z).

Lemma Rbar_mult_pos_lt (x y : Rbar) (z : posreal) :
  Rbar_lt x y ↔ Rbar_lt (Rbar_mult_pos x z) (Rbar_mult_pos y z).

Lemma Rbar_mult_pos_le (x y : Rbar) (z : posreal) :
  Rbar_le x y ↔ Rbar_le (Rbar_mult_pos x z) (Rbar_mult_pos y z).

Lemma Rbar_div_pos_eq (x y : Rbar) (z : posreal) :
  x = y ↔ (Rbar_div_pos x z) = (Rbar_div_pos y z).

Lemma Rbar_div_pos_lt (x y : Rbar) (z : posreal) :
  Rbar_lt x y ↔ Rbar_lt (Rbar_div_pos x z) (Rbar_div_pos y z).

Lemma Rbar_div_pos_le (x y : Rbar) (z : posreal) :
  Rbar_le x y ↔ Rbar_le (Rbar_div_pos x z) (Rbar_div_pos y z).

Definition Rbar_min (x y : Rbar) : Rbar :=
  match x, y with
  | z, p_infty | p_infty, z ⇒ z
  | _ , m_infty | m_infty, _ ⇒ m_infty
  | Finite x, Finite y ⇒ Rmin x y
  end.

Lemma Rbar_lt_locally (a b : Rbar) (x : R) :
  Rbar_lt a x → Rbar_lt x b →
  ∃ delta : posreal,
    ∀ y, Rabs (y - x) < delta → Rbar_lt a y ∧ Rbar_lt y b.

Lemma Rbar_min_comm (x y : Rbar) : Rbar_min x y = Rbar_min y x.

Lemma Rbar_min_r (x y : Rbar) : Rbar_le (Rbar_min x y) y.

Lemma Rbar_min_l (x y : Rbar) : Rbar_le (Rbar_min x y) x.

Lemma Rbar_min_case (x y : Rbar) (P : Rbar → Type) :
  P x → P y → P (Rbar_min x y).
Lemma Rbar_min_case_strong (r1 r2 : Rbar) (P : Rbar → Type) :
  (Rbar_le r1 r2 → P r1) → (Rbar_le r2 r1 → P r2)
    → P (Rbar_min r1 r2).

Definition Rbar_abs (x : Rbar) :=
  match x with
    | Finite x ⇒ Finite (Rabs x)
    | _ ⇒ p_infty
  end.

Lemma Rbar_abs_lt_between (x y : Rbar) :
  Rbar_lt (Rbar_abs x) y ↔ (Rbar_lt (Rbar_opp y) x ∧ Rbar_lt x y).

Lemma Rbar_abs_opp (x : Rbar) :
  Rbar_abs (Rbar_opp x) = Rbar_abs x.

Lemma Rbar_abs_pos (x : Rbar) :
  Rbar_le 0 x → Rbar_abs x = x.
Lemma Rbar_abs_neg (x : Rbar) :
  Rbar_le x 0 → Rbar_abs x = Rbar_opp x.