CoRN.reals.fast.CRGroupOps


Require Export CRmetric.
Require Import QMinMax.
Require Import COrdAbs.
Require Import Qordfield.
Require Import Qmetric.
Require Import CornTac.
Require Import ProductMetric.
Require Import stdlib_omissions.Pair.
Require Import canonical_names.

Set Implicit Arguments.
Set Automatic Introduction.

Opaque CR Qmin Qmax.

Open Local Scope Q_scope.
Open Local Scope uc_scope.

Instance CR0: Zero CR := cast Q CR 0.
Notation "0" := (inject_Q_CR 0) : CR_scope.

Instance CR1: One CR := cast Q CR 1.
Notation "1" := (inject_Q_CR 1) : CR_scope.

Addition

Lifting addition over Q by one parameter yields a rational translation function.
Lemma Qtranslate_uc_prf (a:Q) : is_UniformlyContinuousFunction (fun b:QS ⇒ (a[+]b):QS) Qpos2QposInf.
Proof.
 intros e b0 b1 H.
 simpl in ×.
 unfold Qball in ×.
 stepr (b0-b1).
  assumption.
 simpl; ring.
Qed.

Definition Qtranslate_uc (a:Q_as_MetricSpace) : Q_as_MetricSpace --> Q_as_MetricSpace :=
Build_UniformlyContinuousFunction (Qtranslate_uc_prf a).

Definition translate (a:Q) : CR --> CR := Cmap QPrelengthSpace (Qtranslate_uc a).

Lemma translate_ident : ∀ x:CR, (translate 0 x==x)%CR.
Proof.
 intros x.
 unfold translate.
 assert (H:st_eq (Qtranslate_uc 0) (uc_id _)).
  intros a.
  simpl.
  ring.
 simpl.
 rewrite → H.
 rewrite → Cmap_fun_correct.
 apply: MonadLaw1.
Qed.

Lifting translate yields binary addition over CR.
Lemma Qplus_uc_prf : is_UniformlyContinuousFunction Qtranslate_uc Qpos2QposInf.
Proof.
 intros e a0 a1 H b.
 simpl in ×.
 repeat rewrite → (fun x ⇒ Qplus_comm x b).
 apply Qtranslate_uc_prf.
 assumption.
Qed.

Definition Qplus_uc : Q_as_MetricSpace --> Q_as_MetricSpace --> Q_as_MetricSpace :=
Build_UniformlyContinuousFunction Qplus_uc_prf.


Finally, CRplus:

Definition CRplus_uc : CR --> CR --> CR := Cmap2 QPrelengthSpace QPrelengthSpace Qplus_uc.
Instance CRplus: Plus CR := ucFun2 CRplus_uc.
Notation "x + y" := (ucFun2 CRplus_uc x y) : CR_scope.

But here, too having CRplus as a CR-->CR-->CR does not show that it is uniformly continuous in both arguments. This time we can get the uncurried version just by lifting the uncurried uniformly continuous Qplus:

Local Notation CRCR := (ProductMS CR CR).


Uniform continuity of the uncurried original then follows from extentionality:


Lemma CRplus_translate : ∀ (a:Q) (y:CR), (' a + y == translate a y)%CR.
Proof.
 intros a y.
 unfold ucFun2, CRplus.
 unfold Cmap2.
 unfold inject_Q_CR.
 simpl.
 do 2 rewrite → Cmap_fun_correct.
 rewrite → Cap_fun_correct.
 rewrite → MonadLaw3.
 rewrite → StrongMonadLaw1.
 reflexivity.
Qed.

Hint Rewrite CRplus_translate : CRfast_compute.

Lemma translate_Qplus : ∀ a b:Q, (translate a ('b)=='(a+b)%Q)%CR.
Proof.
 intros a b.
 unfold translate, Cmap.
 simpl.
 rewrite → Cmap_fun_correct.
 apply: MonadLaw3.
Qed.

Hint Rewrite translate_Qplus : CRfast_compute.

Negation

Lifting negation on Q yields negation on CR.
Lemma Qopp_uc_prf : is_UniformlyContinuousFunction Qopp Qpos2QposInf.
Proof.
 intros e a b H.
 simpl in ×.
 unfold Qball in ×.
 stepr (b - a).
  apply AbsSmall_minus.
  assumption.
 simpl. ring.
Qed.

Definition Qopp_uc : Q_as_MetricSpace --> Q_as_MetricSpace :=
Build_UniformlyContinuousFunction Qopp_uc_prf.

Instance CRopp: Negate CR := Cmap QPrelengthSpace Qopp_uc.

Notation "- x" := (CRopp x) : CR_scope.

Subtraction

There is no subtraction on CR. It is simply notation for adding a negated quantity. This way all lemmas about addition automatically apply to subtraction.
Notation "x - y" := (x + (- y))%CR : CR_scope.

Inequality

First a predicate for nonnegative numbers is defined.
Definition CRnonNeg (x:CR) := ∀ e:Qpos, (-e) ≤ (approximate x e).
And similarly for nonpositive.
Definition CRnonPos (x:CR) := ∀ e:Qpos, (approximate x e) ≤ e.
Inequality is defined in terms of nonnegativity.
Instance CRle: Le CR := λ x y, (CRnonNeg (y - x))%CR.
Infix "≤" := CRle : CR_scope.

Basic properties of inequality
Lemma CRle_refl : ∀ x, (x ≤ x)%CR.
Proof.
 intros x e.
 simpl.
 unfold Cap_raw.
 simpl.
 rewrite → Qle_minus_iff.
 ring_simplify.
 apply Qpos_nonneg.
Qed.

Lemma CRle_def : ∀ x y, (x==y ↔ (x ≤ y ∧ y ≤ x))%CR.
Proof.
 intros x y.
 split;[intros H;rewrite → H;split; apply CRle_refl|].
 intros [H1 H2].
 rewrite <- (doubleSpeed_Eq x).
 rewrite <- (doubleSpeed_Eq y).
 apply: regFunEq_e.
 intros e.
 apply ball_weak.
 split;[apply H2|].
 apply: inv_cancel_leEq;simpl.
 stepr (approximate y ((1 # 2) × e)%Qpos - approximate x ((1 # 2) × e)%Qpos); [| simpl; ring].
 apply H1.
Qed.

Lemma CRle_trans : ∀ x y z, (x ≤ y → y ≤ z → x ≤ z)%CR.
Proof.
 intros x y z H1 H2.
 unfold CRle.
 rewrite <- (doubleSpeed_Eq (z-x)%CR).
 intros e.
 assert (H1':=H1 ((1#2)*e)%Qpos).
 assert (H2':=H2 ((1#2)*e)%Qpos).
 clear H1 H2.
 simpl in ×.
 unfold Cap_raw in ×.
 simpl in ×.
 stepr ((approximate z ((1 # 2) × ((1 # 2) × e))%Qpos
   - approximate y ((1 # 2) × ((1 # 2) × e))%Qpos + (approximate y ((1 # 2) × ((1 # 2) × e))%Qpos
     - approximate x ((1 # 2) × ((1 # 2) × e))%Qpos))); [| simpl; ring].
 stepl (-(1#2)×e + - (1#2)×e); [| simpl; ring].
 destruct (Qpos_as_positive_ratio e).
 subst.
 apply Qplus_le_compat; assumption.
Qed.

Maximum

QboundBelow ensures that a real number is at least some fixed rational number. It is the lifting of the first parameter of Qmax.
Lemma QboundBelow_uc_prf (a:Q) : is_UniformlyContinuousFunction (fun b:QS ⇒ (Qmax a b):QS) Qpos2QposInf.
Proof.
 intros e b0 b1 H.
 simpl in ×.
 assert (X:∀ a b0 b1, Qball e b0 b1 → b0 ≤ a ≤ b1 → Qball e a b1).
  clear a b0 b1 H.
  intros a b0 b1 H [H1 H2].
  unfold Qball in ×.
  unfold AbsSmall in ×.
  split.
   apply Qle_trans with (b0-b1).
    tauto.
   apply (minus_resp_leEq _ b0).
   assumption.
  apply Qle_trans with 0.
   apply (shift_minus_leEq _ a).
   stepr b1.
    assumption.
   simpl; ring.
  apply Qpos_nonneg.
 do 2 apply Qmax_case; intros H1 H2.
    apply: ball_refl.
   eapply X.
    apply H.
   tauto.
  apply: ball_sym.
  apply X with b1.
   apply: ball_sym.
   apply H.
  tauto.
 assumption.
Qed.

Definition QboundBelow_uc (a:Q_as_MetricSpace) : Q_as_MetricSpace --> Q_as_MetricSpace :=
Build_UniformlyContinuousFunction (QboundBelow_uc_prf a).

Definition boundBelow (a:Q) : CR --> CR := Cmap QPrelengthSpace (QboundBelow_uc a).

CRmax is the lifting of QboundBelow.
Lemma Qmax_uc_prf : is_UniformlyContinuousFunction QboundBelow_uc Qpos2QposInf.
Proof.
 intros e a0 a1 H b.
 simpl in ×.
 repeat rewrite → (fun x ⇒ Qmax_comm x b).
 apply QboundBelow_uc_prf.
 assumption.
Qed.

Definition Qmax_uc : Q_as_MetricSpace --> Q_as_MetricSpace --> Q_as_MetricSpace :=
Build_UniformlyContinuousFunction Qmax_uc_prf.

Definition CRmax : CR --> CR --> CR := Cmap2 QPrelengthSpace QPrelengthSpace Qmax_uc.

Lemma CRmax_boundBelow : ∀ (a:Q) (y:CR), (CRmax (' a) y == boundBelow a y)%CR.
Proof.
 intros a y.
 unfold ucFun2, CRmax.
 unfold Cmap2.
 unfold inject_Q_CR.
 simpl.
 do 2 rewrite → Cmap_fun_correct.
 rewrite → Cap_fun_correct.
 rewrite → MonadLaw3.
 rewrite → StrongMonadLaw1.
 reflexivity.
Qed.
Basic properties of CRmax.
Lemma CRmax_ub_l : ∀ x y, (x ≤ CRmax x y)%CR.
Proof.
 intros x y e.
 simpl.
 unfold Cap_raw.
 simpl.
 unfold Cap_raw.
 simpl.
 rewrite → Qmax_plus_distr_l.
 eapply Qle_trans;[|apply Qmax_ub_l].
 cut (AbsSmall (e:Q) (approximate x ((1 # 2) × ((1 # 2) × e))%Qpos +
   - approximate x ((1 # 2) × e)%Qpos));[unfold AbsSmall;tauto|].
 change (ball e (approximate x ((1 # 2) × ((1 # 2) × e))%Qpos) (approximate x ((1 # 2) × e)%Qpos)).
 eapply ball_weak_le;[|apply regFun_prf].
 autorewrite with QposElim.
 rewrite → Qle_minus_iff.
 ring_simplify.
 apply: mult_resp_nonneg.
  discriminate.
 apply Qpos_nonneg.
Qed.

Lemma CRmax_ub_r : ∀ x y, (y ≤ CRmax x y)%CR.
Proof.
 intros y x e.
 simpl.
 unfold Cap_raw.
 simpl.
 unfold Cap_raw.
 simpl.
 rewrite → Qmax_plus_distr_l.
 eapply Qle_trans;[|apply Qmax_ub_r].
 cut (AbsSmall (e:Q) (approximate x ((1 # 2) × ((1 # 2) × e))%Qpos +
   - approximate x ((1 # 2) × e)%Qpos));[unfold AbsSmall;tauto|].
 change (ball e (approximate x ((1 # 2) × ((1 # 2) × e))%Qpos) (approximate x ((1 # 2) × e)%Qpos)).
 eapply ball_weak_le;[|apply regFun_prf].
 autorewrite with QposElim.
 rewrite → Qle_minus_iff.
 ring_simplify.
 apply: mult_resp_nonneg.
  discriminate.
 apply Qpos_nonneg.
Qed.

Lemma CRmax_lub: ∀ x y z : CR, (x ≤ z → y ≤ z → CRmax x y ≤ z)%CR.
Proof.
 intros x y z Hx Hy.
 rewrite <- (doubleSpeed_Eq z) in × |- ×.
 intros e.
 assert (Hx':=Hx ((1#2)*e)%Qpos).
 assert (Hy':=Hy ((1#2)*e)%Qpos).
 clear Hx Hy.
 simpl in ×.
 unfold Cap_raw in ×.
 simpl in ×.
 unfold Cap_raw.
 simpl.
 stepl ((-(1#2)×e) + (- (1#2)×e)); [| simpl; ring].
 stepr ((approximate z ((1#2)*((1 # 2) × e))%Qpos +
   - approximate z ((1#2)*((1 # 2) × ((1 # 2) × e)))%Qpos) +
     (approximate z ((1#2)*((1 # 2) × ((1 # 2) × e)))%Qpos
       - Qmax (approximate x ((1 # 2) × ((1 # 2) × e))%Qpos)
         (approximate y ((1 # 2) × ((1 # 2) × e))%Qpos))); [|simpl; ring].
 destruct (Qpos_as_positive_ratio e) as [[n d] E].
 simpl in E.
 set (n # d)%Qpos in E.
 subst.
 rename q into e.
 apply Qplus_le_compat;[|apply Qmax_case;intro;assumption].
 cut (ball ((1#2)*e)%Qpos (approximate z ((1#2)*((1 # 2) × e))%Qpos)
   (approximate z ((1#2)*((1 # 2) × ((1 # 2) × e)))%Qpos));[intros [A B]; assumption|].
 apply: ball_weak_le;[|apply regFun_prf].
 rewrite → Qle_minus_iff.
 autorewrite with QposElim.
 ring_simplify.
 apply: mult_resp_nonneg.
  discriminate.
 apply Qpos_nonneg.
Qed.

Minimum

QboundAbove ensures that a real number is at most some fixed rational number. It is the lifting of the first parameter of Qmin.
Lemma QboundAbove_uc_prf (a:Q) : is_UniformlyContinuousFunction (fun b:QS ⇒ (Qmin a b):QS) Qpos2QposInf.
Proof.
 intros e b0 b1 H.
 simpl in ×.
 unfold Qball.
 stepr ((Qmax (- a) (-b1)) - (Qmax (-a) (-b0))).
  apply QboundBelow_uc_prf.
  apply Qopp_uc_prf.
  apply ball_sym.
  assumption.
 unfold Qminus.
 simpl.
 rewrite → Qmin_max_de_morgan.
 rewrite → Qmax_min_de_morgan.
 repeat rewrite → Qopp_involutive.
 ring.
Qed.

Definition QboundAbove_uc (a:Q_as_MetricSpace) : Q_as_MetricSpace --> Q_as_MetricSpace :=
Build_UniformlyContinuousFunction (QboundAbove_uc_prf a).

Definition boundAbove (a:Q) : CR --> CR := Cmap QPrelengthSpace (QboundAbove_uc a).

CRmin is the lifting of QboundAbove.
Lemma Qmin_uc_prf : is_UniformlyContinuousFunction QboundAbove_uc Qpos2QposInf.
Proof.
 intros e a0 a1 H b.
 simpl in ×.
 repeat rewrite → (fun x ⇒ Qmin_comm x b).
 apply QboundAbove_uc_prf.
 assumption.
Qed.

Definition Qmin_uc : Q_as_MetricSpace --> Q_as_MetricSpace --> Q_as_MetricSpace :=
Build_UniformlyContinuousFunction Qmin_uc_prf.

Definition CRmin : CR --> CR --> CR := Cmap2 QPrelengthSpace QPrelengthSpace Qmin_uc.

Lemma CRmin_boundAbove : ∀ (a:Q) (y:CR), (CRmin (' a) y == boundAbove a y)%CR.
Proof.
 intros a y.
 unfold ucFun2, CRmin.
 unfold Cmap2.
 unfold inject_Q_CR.
 simpl.
 do 2 rewrite → Cmap_fun_correct.
 rewrite → Cap_fun_correct.
 rewrite → MonadLaw3.
 rewrite → StrongMonadLaw1.
 reflexivity.
Qed.

Basic properties of CRmin.
Lemma CRmin_lb_l : ∀ x y, (CRmin x y ≤ x)%CR.
Proof.
 intros x y e.
 simpl.
 unfold Cap_raw.
 simpl.
 unfold Cap_raw.
 simpl.
 rewrite → Qmin_max_de_morgan.
 rewrite → Qmax_plus_distr_r.
 eapply Qle_trans;[|apply Qmax_ub_l].
 cut (AbsSmall (e:Q) (approximate x ((1 # 2) × e)%Qpos +
   - approximate x ((1 # 2) × ((1 # 2) × e))%Qpos));[unfold AbsSmall;tauto|].
 change (ball e (approximate x ((1 # 2) × e)%Qpos) (approximate x ((1 # 2) × ((1 # 2) × e))%Qpos)).
 eapply ball_weak_le;[|apply regFun_prf].
 autorewrite with QposElim.
 rewrite → Qle_minus_iff.
 ring_simplify.
 apply: mult_resp_nonneg.
  discriminate.
 apply Qpos_nonneg.
Qed.

Lemma CRmin_lb_r : ∀ x y, (CRmin x y ≤ y)%CR.
Proof.
 intros y x e.
 simpl.
 unfold Cap_raw.
 simpl.
 unfold Cap_raw.
 simpl.
 rewrite → Qmin_max_de_morgan.
 rewrite → Qmax_plus_distr_r.
 eapply Qle_trans;[|apply Qmax_ub_r].
 cut (AbsSmall (e:Q) (approximate x ((1 # 2) × e)%Qpos +
   - approximate x ((1 # 2) × ((1 # 2) × e))%Qpos));[unfold AbsSmall;tauto|].
 change (ball e (approximate x ((1 # 2) × e)%Qpos) (approximate x ((1 # 2) × ((1 # 2) × e))%Qpos)).
 eapply ball_weak_le;[|apply regFun_prf].
 autorewrite with QposElim.
 rewrite → Qle_minus_iff.
 ring_simplify.
 apply: mult_resp_nonneg.
  discriminate.
 apply Qpos_nonneg.
Qed.

Lemma CRmin_glb: ∀ x y z : CR, (z ≤ x → z ≤ y → z ≤ CRmin x y)%CR.
Proof.
 intros x y z Hx Hy.
 rewrite <- (doubleSpeed_Eq z) in × |- ×.
 intros e.
 assert (Hx':=Hx ((1#2)*e)%Qpos).
 assert (Hy':=Hy ((1#2)*e)%Qpos).
 clear Hx Hy.
 simpl in ×.
 unfold Cap_raw in ×.
 simpl in ×.
 unfold Cap_raw.
 simpl.
 stepl ((-(1#2)×e) + (- (1#2)×e)); [| simpl; ring].
 stepr ((approximate z ((1#2)*((1 # 2) × ((1 # 2) × e)))%Qpos +
   - approximate z ((1#2)*((1 # 2) × e))%Qpos) + (Qmin (approximate x ((1 # 2) × ((1 # 2) × e))%Qpos)
     (approximate y ((1 # 2) × ((1 # 2) × e))%Qpos) +
       - approximate z ((1#2)*((1 # 2) × ((1 # 2) × e)))%Qpos)); [| simpl; ring].
 destruct (Qpos_as_positive_ratio e) as [[n d] E].
 simpl in E.
 set (n # d)%Qpos in E.
 subst.
 rename q into e.
 apply Qplus_le_compat;[|apply Qmin_case;intro;assumption].
 cut (ball ((1#2)*e)%Qpos (approximate z ((1#2)*((1 # 2) × ((1 # 2) × e)))%Qpos)
   (approximate z ((1#2)*((1 # 2) × e))%Qpos));[intros [A B]; assumption|].
 apply: ball_weak_le;[|apply regFun_prf].
 rewrite → Qle_minus_iff.
 autorewrite with QposElim.
 ring_simplify.
 apply: mult_resp_nonneg.
  discriminate.
 apply Qpos_nonneg.
Qed.