CoRN.model.structures.QposInf
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+∞.
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.
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.
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.
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.
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.
Addition
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.
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.
Multiplication
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.
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.
Order
Definition QposInf_le (x y: Q+∞) : Prop :=
match y with
| ∞ ⇒ True
| Qpos2QposInf y' ⇒
match x with
| ∞ ⇒ False
| Qpos2QposInf x' ⇒ x' ≤ y'
end
end.
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.
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.
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.