CoRN.model.structures.QposInf

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

Open Local Scope Q_scope.
Open Local Scope Qpos_scope.

Qpos

We choose to define Q⁺_∞ as the disjoint union of Qpos and an Infinity token.

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

Delimit Scope QposInf_scope with Q⁺_∞.

Qpos2QposInf is an injection from Qpos to Q⁺_∞ that we declare as a coercion.

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

This bind operation is useful for lifting operations to work on Q⁺_∞. It will map ∞ to ∞.

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

Lemma QposInf_bind_id : forall x, QposInf_bind (fun e => e) x = x.

Equality

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.

Lemma QposInfEq_sym x y : QposInfEq x y -> QposInfEq y x.

Lemma QposInfEq_trans x y z : QposInfEq x y -> QposInfEq y z -> QposInfEq x z.

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.

Instance QposInf_bind_wd (f : Qpos -> Q⁺_∞) {f_wd : Proper (QposEq ==> QposInfEq) f} :
Proper (QposInfEq ==> QposInfEq) (QposInf_bind f).

Addition

Multiplication

Order

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

Minimum

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.

Lemma QposInf_min_lb_l : forall x y, QposInf_le (QposInf_min x y) x.

Lemma QposInf_min_lb_r : forall x y, QposInf_le (QposInf_min x y) y.

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