Require Export QArith.
Require Export Qpossec.
Require Import QposMinMax.


Set Implicit Arguments.

Open Local Scope Q_scope.
Open Local Scope Qpos_scope.

Inductive Q⁺_∞ : Set :=
| Qpos2QposInf : Qpos → Q⁺_∞
| ∞ : Q⁺_∞.

Bind Scope QposInf_scope with Q⁺_∞.
Delimit Scope QposInf_scope with Q⁺_∞.

Coercion Qpos2QposInf : Qpos >-> Q⁺_∞.

Definition QposInf_bind (f : Qpos → Q⁺_∞) (x:Q⁺_∞) :=
 match x with
 | Qpos2QposInf x' ⇒ f x'
 | ∞ ⇒ ∞
 end.

Lemma QposInf_bind_id : ∀ x, QposInf_bind (fun e ⇒ e) x = x.
Proof.
 intros [x|]; reflexivity.
Qed.

Definition QposInfEq (a b:Q⁺_∞) :=
 match a, b with
 | Qpos2QposInf x, Qpos2QposInf y ⇒ Qeq x y
 | ∞, ∞ ⇒ True
 | _, _ ⇒ False
 end.

Lemma QposInfEq_refl x : QposInfEq x x.
Proof.
  destruct x as [x|]. apply Qeq_refl.
  simpl. trivial.
Qed.

Lemma QposInfEq_sym x y : QposInfEq x y → QposInfEq y x.
Proof.
  destruct x as [x|], y as [y|]; simpl; trivial. apply Qeq_sym.
Qed.

Lemma QposInfEq_trans x y z : QposInfEq x y → QposInfEq y z → QposInfEq x z.
Proof.
  destruct x as [x|], y as [y|], z as [z|]; simpl; try tauto. apply Qeq_trans.
Qed.

Add Relation Q⁺_∞ QposInfEq
 reflexivity proved by QposInfEq_refl
 symmetry proved by QposInfEq_sym
 transitivity proved by QposInfEq_trans as QposInfSetoid.

Instance: Proper (QposEq ==> QposInfEq) Qpos2QposInf.
Proof. firstorder. Qed.

Instance QposInf_bind_wd (f : Qpos → Q⁺_∞) {f_wd : Proper (QposEq ==> QposInfEq) f} :
  Proper (QposInfEq ==> QposInfEq) (QposInf_bind f).
Proof.
  intros [x|] [y|] E; simpl; auto.
   destruct E.
  destruct E.
Qed.

Definition QposInf_plus (x y : Q⁺_∞) : Q⁺_∞ :=
QposInf_bind (fun x' ⇒ QposInf_bind (fun y' ⇒ x'+y') y) x.

Instance: Proper (QposInfEq ==> QposInfEq ==> QposInfEq) QposInf_plus.
Proof with auto.
  intros [x1|] [y1|] E1 [x2|] [y2|] E2; simpl...
  apply Qplus_comp...
Qed.

Definition QposInf_mult (x y : Q⁺_∞) : Q⁺_∞ :=
QposInf_bind (fun x' ⇒ QposInf_bind (fun y' ⇒ x'×y') y) x.

Instance: Proper (QposInfEq ==> QposInfEq ==> QposInfEq) QposInf_mult.
Proof with auto.
  intros [x1|] [y1|] E1 [x2|] [y2|] E2; simpl...
  apply Qmult_comp...
Qed.

Definition QposInf_le (x y: Q⁺_∞) : Prop :=
match y with
| ∞ ⇒ True
| Qpos2QposInf y' ⇒
 match x with
 | ∞ ⇒ False
 | Qpos2QposInf x' ⇒ x' ≤ y'
 end
end.

Definition QposInf_min (x y : Q⁺_∞) : Q⁺_∞ :=
match x with
| ∞ ⇒ y
| Qpos2QposInf x' ⇒
 match y with
 | ∞ ⇒ x'
 | Qpos2QposInf y' ⇒ Qpos2QposInf (Qpos_min x' y')
 end
end.

Instance: Proper (QposInfEq ==> QposInfEq ==> QposInfEq) QposInf_min.
Proof with intuition.
  intros [x1|] [y1|] E1 [x2|] [y2|] E2; simpl in ×...
  apply Qpos_min_compat_Proper...
Qed.

Lemma QposInf_min_lb_l : ∀ x y, QposInf_le (QposInf_min x y) x.
Proof.
 intros [x|] [y|]; simpl; try auto.
  apply Qpos_min_lb_l.
 apply Qle_refl.
Qed.

Lemma QposInf_min_lb_r : ∀ x y, QposInf_le (QposInf_min x y) y.
Proof.
 intros [x|] [y|]; simpl; try auto.
  apply Qpos_min_lb_r.
 apply Qle_refl.
Qed.

Infix "+" := QposInf_plus : QposInf_scope.
Infix "×" := QposInf_mult : QposInf_scope.