CoRN.model.structures.QnnInf

Require QnonNeg.
Import QnonNeg.notations.

Require Import QposInf.

Inductive T: Set := Infinite | Finite (q: QnonNeg).

Definition eq (x y: T): Prop :=
  match x, y with
  | Finite x', Finite y' ⇒ (x' == y')%Qnn
  | Infinite, Infinite ⇒ True
  | _, _ ⇒ False
  end.

Global Instance: Equivalence eq.
Proof with intuition.
 unfold eq.
 split; repeat intro.
   destruct x...
  destruct x, y...
 destruct x, y, z...
 transitivity q0...
Qed.

Local Infix "==" := eq.

Definition bind (x: T) (f: QnonNeg → T): T :=
  match x with
  | Finite x' ⇒ f x'
  | Infinite ⇒ Infinite
  end.

Section liftM2.

  Context
    (f: QnonNeg → QnonNeg → QnonNeg)
    {p: Proper (QnonNeg.eq ==> QnonNeg.eq ==> QnonNeg.eq) f}.

  Definition liftM2 (x y: T): T := bind x (fun x' ⇒ bind y (fun y' ⇒ Finite (f x' y'))).

  Global Instance liftM2_Proper: Proper (eq ==> eq ==> eq) liftM2.
  Proof with intuition. intros [] [] ? [] [] ?... simpl. apply p... Qed.

  Lemma assoc:
    (∀ x y z, f x (f y z) == f (f x y) z)%Qnn →
    (∀ x y z, liftM2 x (liftM2 y z) == liftM2 (liftM2 x y) z).
  Proof. intros H [] [] []; simpl; auto. Qed.

  Lemma comm:
    (∀ x y, f x y == f y x)%Qnn →
    (∀ x y, liftM2 x y == liftM2 y x).
  Proof. intros H [] []; simpl; auto. Qed.

End liftM2.

Definition mult := liftM2 QnonNeg.mult.
Definition plus := liftM2 QnonNeg.plus.

Local Infix "+" := plus.
Local Infix "×" := mult.

Lemma plus_comm: ∀ x y, x + y == y + x.
Proof comm QnonNeg.plus QnonNeg.plus_comm.
Lemma mult_comm: ∀ x y, x × y == y × x.
Proof comm QnonNeg.mult QnonNeg.mult_comm.
Lemma plus_assoc: ∀ x y z, x + (y + z) == (x + y) + z.
Proof assoc QnonNeg.plus QnonNeg.plus_assoc.
Lemma mult_assoc: ∀ x y z, x × (y × z) == (x × y) × z.
Proof assoc QnonNeg.mult QnonNeg.mult_assoc.

Global Instance: Proper (eq ==> eq ==> eq) plus.
Proof liftM2_Proper _.

Global Instance: Proper (eq ==> eq ==> eq) mult.
Proof liftM2_Proper _.

Definition le (x y: T): Prop :=
  match y with
  | Infinite ⇒ True
  | Finite y' ⇒
    match x with
    | Infinite ⇒ False
    | Finite x' ⇒ (x' ≤ y')
    end
  end.

Global Instance: Proper (eq ==> eq ==> iff) le.
Proof with intuition.
 unfold eq, QnonNeg.eq, le.
 repeat intro.
 destruct x0, y0, y, x...
  rewrite <- H.
  rewrite <- H0...
 unfold QnonNeg.to_Q.
 rewrite H.
 rewrite H0...
Qed.

Global Program Coercion from_QposInf (q: QposInf): T :=
  match q with
  | Qpos2QposInf q' ⇒ Finite q'
  | QposInfinity ⇒ Infinite
  end.

Global Coercion Finite: QnonNeg >-> T.

Global Instance Finite_Proper: Proper (QnonNeg.eq ==> eq) Finite.
Proof. repeat intro. assumption. Qed.

Module notations.

  Delimit Scope QnnInf_scope with QnnInf.

  Global Infix "==" := eq: QnnInf_scope.
  Global Infix "≤" := le: QnnInf_scope.
  Global Infix "+" := plus: QnnInf_scope.
  Global Infix "×" := mult: QnnInf_scope.
  Global Notation QnnInf := T.

End notations.