From 5a6acf3de6134e81ae2e263b5228e80da38f9816 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Fri, 10 Dec 2021 14:13:28 +0100
Subject: [PATCH] Replace Q with rat, R+ with {nonneg R}...
---
RminStruct.v | 61 ++++++------
backlogged_period.v | 12 +--
cumulative_curves.v | 6 +-
deviations.v | 16 ++--
fifo.v | 4 +-
minerve/PA.v | 136 +++++++++++++--------------
minerve/PA_refinement.v | 56 +++++------
minerve/UPP.v | 180 ++++++++++++++++++------------------
minerve/UPP_PA.v | 58 ++++++------
minerve/UPP_PA_refinement.v | 16 ++--
minerve/ratdiv.v | 86 ++++++++---------
minerve/tactic.v | 2 +-
services.v | 6 +-
static_priority.v | 10 +-
usual_functions.v | 4 +-
15 files changed, 322 insertions(+), 331 deletions(-)
diff --git a/RminStruct.v b/RminStruct.v
index 9aca8f0f..bf2565f1 100644
--- a/RminStruct.v
+++ b/RminStruct.v
@@ -12,10 +12,6 @@ Require Import nngenum.
(* Dioid instances used in network calculus. *)
(* *)
(* * number dioids *)
-(* R+ == {nonneg R} *)
-(* Q == rat *)
-(* Q+ == {nonneg Q} *)
-(* Q+* == {posnum Q} *)
(* \bar R and {nonnege R} are equipped with a complete lattice canonical *)
(* structure, first law is min, second law is addition, zero element is +oo *)
(* and unit element is 0. *)
@@ -59,8 +55,6 @@ Import Order.Theory GRing.Theory Num.Theory DualAddTheory.
library thanks to mathcomp.analysis.Rstruct) *)
Parameter R : realType.
-Notation "'R+'" := {nonneg (R : Type)}.
-
(* a few things about rationals *)
Lemma ratr_ge0 (F : numFieldType) (x : {nonneg rat}) : 0 <= @ratr F x%:nngnum.
@@ -69,9 +63,6 @@ Canonical ratr_nngnum (R' : numFieldType) (x : {nonneg rat}) :=
Nonneg.NngNum (ratr x%:nngnum) (ratr_ge0 R' x).
Notation toR := (@ratr R).
-Notation Q := rat.
-Notation "'Q+'" := {nonneg Q}.
-Notation "'Q+*'" := {posnum Q}.
Lemma toR0 : toR 0 = 0.
Proof. exact: rmorph0. Qed.
@@ -151,13 +142,13 @@ Proof. by []. Qed.
Definition Rbar_dioidE :=
(Rbar_dioid_addE, Rbar_dioid_mulE, Rbar_dioid_set_addE).
-(* (barR+, Order.min, adde) is a comCompleteDioidType *)
+(* ({nonnege R}, Order.min, adde) is a comCompleteDioidType *)
-Notation "'barR+'" := {nonnege R}.
+Notation "'{nonnege R}'" := {nonnege R}.
HB.instance Definition _ :=
WrapChoice_of_TYPE.Build
- barR+ (Nonnege.nngenum_eqMixin R) (Nonnege.nngenum_choiceMixin R).
+ {nonnege R} (Nonnege.nngenum_eqMixin R) (Nonnege.nngenum_choiceMixin R).
Lemma nnRbar_semiring_closed : semiring_closed (@Nonnege.nonNegativeEReal R).
Proof.
@@ -175,21 +166,21 @@ Canonical nnRbar_keyed := KeyedQualifier nnRbar_key.
Canonical nnRbar_addPred := AddPred nnRbar_semiring_closed.
Canonical nnRbar_semiringPred := SemiRingPred nnRbar_semiring_closed.
-Definition nnRbar_semiRing := Eval hnf in [SemiRing of barR+ by <:].
-HB.instance (barR+) nnRbar_semiRing.
-Definition nnRbar_comSemiRing := Eval hnf in [ComSemiRing of barR+ by <:].
-HB.instance (barR+) nnRbar_comSemiRing.
+Definition nnRbar_semiRing := Eval hnf in [SemiRing of {nonnege R} by <:].
+HB.instance ({nonnege R}) nnRbar_semiRing.
+Definition nnRbar_comSemiRing := Eval hnf in [ComSemiRing of {nonnege R} by <:].
+HB.instance ({nonnege R}) nnRbar_comSemiRing.
Definition nnRbar_porderMixin :
- Order.LePOrderMixin.of_ (@Equality.clone (barR+) _ _ id id) :=
+ Order.LePOrderMixin.of_ (@Equality.clone ({nonnege R}) _ _ id id) :=
@Order.SubOrder.sub_POrderMixin _ dual_ereal_porderType _ _.
Canonical nnRbar_porderType :=
Order.POrder.pack (Order.dual_display dioid_display) id nnRbar_porderMixin.
HB.instance Definition _ :=
- WrapPOrder_of_WrapChoice.Build (barR+) nnRbar_porderMixin.
+ WrapPOrder_of_WrapChoice.Build ({nonnege R}) nnRbar_porderMixin.
-Definition nnRbar_dioid := Eval hnf in [Dioid of barR+ by <:].
-HB.instance (barR+) nnRbar_dioid.
+Definition nnRbar_dioid := Eval hnf in [Dioid of {nonnege R} by <:].
+HB.instance ({nonnege R}) nnRbar_dioid.
Definition nnRbar_latticeMixin :
Order.Lattice.mixin_of (@Order.POrder.class _ nnRbar_porderType) :=
@@ -198,7 +189,7 @@ Definition nnRbar_latticeMixin :
_ (dual_orderType [orderType of \bar R]) _ _).
Canonical nnRbar_latticeType := Order.Lattice.pack id nnRbar_latticeMixin.
HB.instance Definition _ :=
- WrapLattice_of_WrapPOrder.Build (barR+) nnRbar_latticeMixin.
+ WrapLattice_of_WrapPOrder.Build ({nonnege R}) nnRbar_latticeMixin.
Lemma nnRbar_set_join_closed : set_join_closed (@Nonnege.nonNegativeEReal R).
Proof. move=> S HS; exact/lb_ereal_inf/HS. Qed.
@@ -206,15 +197,15 @@ Proof. move=> S HS; exact/lb_ereal_inf/HS. Qed.
Canonical nnRbar_setJoinPred := SetJoinPred nnRbar_set_join_closed.
Definition nnRbar_completeLattice :=
- Eval hnf in [CompleteLattice of barR+ by <:].
-HB.instance (barR+) nnRbar_completeLattice.
+ Eval hnf in [CompleteLattice of {nonnege R} by <:].
+HB.instance ({nonnege R}) nnRbar_completeLattice.
-Definition nnRbar_completeDioid := Eval hnf in [CompleteDioid of barR+ by <:].
-HB.instance (barR+) nnRbar_completeDioid.
+Definition nnRbar_completeDioid := Eval hnf in [CompleteDioid of {nonnege R} by <:].
+HB.instance ({nonnege R}) nnRbar_completeDioid.
(* (F, F_min, F_min_conv) is a comCompleteDioidType *)
-Definition F := R+ -> \bar R.
+Definition F := {nonneg R} -> \bar R.
Definition F_eqMixin := @gen_eqMixin F.
Canonical F_eqType := Eval hnf in EqType F F_eqMixin.
@@ -305,7 +296,7 @@ Definition F_min_conv (f g : F) : F :=
fun t =>
ereal_inf
[set (f uv.1 + g uv.2)%dE
- | uv in [set uv : R+ * R+ | uv.1%:nngnum + uv.2%:nngnum = t%:nngnum]].
+ | uv in [set uv : {nonneg R} * {nonneg R} | uv.1%:nngnum + uv.2%:nngnum = t%:nngnum]].
Definition F_zero : F := fun=> +oo%E.
@@ -471,7 +462,7 @@ Definition F_dioidE :=
(F_dioid_addE, F_dioid_mulE, F_dioid_set_addE, F_dioid_oneE, F_dioid_zeroE,
F_dioid_leE).
-Lemma alt_def_F_min_conv (f g : F) (t : R+) :
+Lemma alt_def_F_min_conv (f g : F) (t : {nonneg R}) :
F_min_conv f g t
= ereal_inf [set (f u + g (insubd 0%:nng (t%:nngnum - u%:nngnum))%R)%dE
| u in [set u | u <= t]].
@@ -1051,11 +1042,11 @@ Canonical F0up_choiceType := ChoiceType F0up F0up_choiceMixin.
(** *** Somes properties *)
-Program Definition Fplus_shift_l (f : Fup) (d : R+) :=
+Program Definition Fplus_shift_l (f : Fup) (d : {nonneg R}) :=
Build_Fplus (fun t => f (t%:nngnum + d%:nngnum)%:nng) _.
Next Obligation. by apply/leFP => t. Qed.
-Program Definition Fup_shift_l (f : Fup) (d : R+) :=
+Program Definition Fup_shift_l (f : Fup) (d : {nonneg R}) :=
Build_Fup (Fplus_shift_l f d) _.
Next Obligation.
apply/non_decr_closureP => x y; rewrite /= leEsub /= -(ler_add2r d%:nngnum).
@@ -1063,10 +1054,10 @@ exact/ndFP.
Qed.
(*definiton 20 p 68 *)
-Definition pseudo_inv_inf_nnR (f : Fup) (y : barR+) : barR+ :=
+Definition pseudo_inv_inf_nnR (f : Fup) (y : {nonnege R}) : {nonnege R} :=
(ereal_inf [set x%:nngnum%:E | x in [set x | y%:nngenum <= f x]])%:nnge%E.
-Lemma non_decr_recipr (f : Fup) (x y : R+) : (f x < f y)%E -> x < y.
+Lemma non_decr_recipr (f : Fup) (x y : {nonneg R}) : (f x < f y)%E -> x < y.
Proof.
move=> Hfxy; rewrite ltNge; apply/negP => Hxy.
move: Hfxy; apply/negP; rewrite -leNgt.
@@ -1086,7 +1077,7 @@ by exists 0%:E; rewrite lte_ninfty lte_pinfty.
Qed.
(* Réécriture du Lemma 8 : page 68 *)
-Lemma alt_def_pseudo_inv_inf_nnR (f : Fup) (y : barR+) :
+Lemma alt_def_pseudo_inv_inf_nnR (f : Fup) (y : {nonnege R}) :
((pseudo_inv_inf_nnR f y)%:nngenum
= Order.max
0%:E (ereal_sup [set x%:nngnum%:E | x in [set x | (f x < y%:nngenum)%E]]))%E.
@@ -1109,7 +1100,7 @@ apply/le_anti/andP; split; last first.
by apply: (@non_decr_recipr f); move: Hx; apply: lt_le_trans. }
rewrite leNgt; apply/negP => Hlb.
have [m /andP[Hml Hmb]] := ex_el_between Hlb.
-have [m' Hm'] : exists m' : R+, m'%:nngnum%:E = m.
+have [m' Hm'] : exists m' : {nonneg R}, m'%:nngnum%:E = m.
{ have Hm_pos : (0%:E <= m)%E.
{ by move: Hml => /ltW; apply: le_trans. }
move: Hmb Hm_pos.
@@ -1132,7 +1123,7 @@ rewrite -!Rbar_dioidE -complete_dioid.set_addU.
by rewrite -image_setU setDE -setIUr setUCr setIT.
Qed.
-Lemma Rbar_inf_split_range y y' x z (f : R+ -> \bar R) :
+Lemma Rbar_inf_split_range y y' x z (f : {nonneg R} -> \bar R) :
x <= y -> y <= y' -> y' <= z ->
ereal_inf [set f u | u in [set u | x <= u%:nngnum <= z]]
= Order.min
diff --git a/backlogged_period.v b/backlogged_period.v
index abf01727..5c06c873 100644
--- a/backlogged_period.v
+++ b/backlogged_period.v
@@ -29,10 +29,10 @@ Local Open Scope ring_scope.
Import Order.Theory GRing.Theory Num.Theory DualAddTheory.
Definition backlogged_period (A D : F) (u v : R) :=
- u <= v /\ forall x : R+, u < x%:nngnum <= v -> (D x < A x)%E.
+ u <= v /\ forall x : {nonneg R}, u < x%:nngnum <= v -> (D x < A x)%E.
-Lemma start_proof (A D : F) (t : R+) :
- { y : R+ | y%:nngnum%:E
+Lemma start_proof (A D : F) (t : {nonneg R}) :
+ { y : {nonneg R} | y%:nngnum%:E
= Order.max
0%:E
(ereal_sup [set u%:nngnum%:E | u in [set u | u <= t /\ D u = A u]])}.
@@ -55,7 +55,7 @@ have Hy : [set (u)%:nngnum%:E | u in s] (y)%:nngnum%:E; [by exists y|].
by exfalso; move: E => /ereal_sup_ninfty /(_ y%:nngnum%:E Hy).
Qed.
-Definition start (A D : F) (t : R+) : R+ := proj1_sig (start_proof A D t).
+Definition start (A D : F) (t : {nonneg R}) : {nonneg R} := proj1_sig (start_proof A D t).
Lemma start_non_decr (A D : flow_cc) : {homo (start A D) : x y / x <= y }.
Proof.
@@ -76,7 +76,7 @@ apply: ub_ereal_sup => _ [z' [Hz' H'z'] <-].
by apply: ereal_sup_ub; exists z' => //; split=> //; move: Hxy; apply: le_trans.
Qed.
-Lemma start_eq (A D : flow_cc) (t : R+) : A (start A D t) = D (start A D t).
+Lemma start_eq (A D : flow_cc) (t : {nonneg R}) : A (start A D t) = D (start A D t).
Proof.
set s := start _ _ _.
case (@eqP _ s 0%:nng) => [-> | /eqP Hs]; [by rewrite !flow_cc0|].
@@ -135,7 +135,7 @@ move: (Heta _ H''z) => /andP[+ _].
by rewrite -fin_flow_ccE /eps/= -daddEFin subKr fin_flow_ccE.
Qed.
-Lemma start_le (A D : F) (t : R+) : (start A D t)%:nngnum <= t%:nngnum.
+Lemma start_le (A D : F) (t : {nonneg R}) : (start A D t)%:nngnum <= t%:nngnum.
Proof.
rewrite /= -lee_fin /start; case: start_proof => _ ->.
rewrite le_maxl lee_fin Nonneg.nngnum_ge0 /=.
diff --git a/cumulative_curves.v b/cumulative_curves.v
index f7796cc9..66d0d6fb 100644
--- a/cumulative_curves.v
+++ b/cumulative_curves.v
@@ -91,7 +91,7 @@ Lemma flow_cc_fin (f : flow_cc) t : f t \is a fin_num.
Proof. by case: f => f /= /andP[_ /asboolP]. Qed.
Lemma fin_flow_cc_prop (f : flow_cc) :
- { ff : R+ -> R+ | forall t, f t = (ff t)%:nngnum%:E }.
+ { ff : {nonneg R} -> {nonneg R} | forall t, f t = (ff t)%:nngnum%:E }.
Proof.
apply: constructive_indefinite_description.
case: f => f /= /andP[_ /asboolP finf].
@@ -101,12 +101,12 @@ exists (fun t => Nonneg.NngNum _ (nngfine t)) => t /=.
by case: (f t) (finf t).
Qed.
-Definition fin_flow_cc (f : flow_cc) : R+ -> R+ :=
+Definition fin_flow_cc (f : flow_cc) : {nonneg R} -> {nonneg R} :=
proj1_sig (fin_flow_cc_prop f).
Notation "f '%:fcc'" := (fin_flow_cc f).
-Lemma fin_flow_ccE (f : flow_cc) : forall t : R+, (f%:fcc t)%:nngnum%:E = f t.
+Lemma fin_flow_ccE (f : flow_cc) : forall t : {nonneg R}, (f%:fcc t)%:nngnum%:E = f t.
Proof. by move=> t; rewrite /fin_flow_cc; case: (fin_flow_cc_prop f). Qed.
Lemma flow_cc0 (f : flow_cc) : f 0%:nng = 0%:E.
diff --git a/deviations.v b/deviations.v
index abbb8fb0..484656e3 100644
--- a/deviations.v
+++ b/deviations.v
@@ -35,14 +35,14 @@ Import Order.Theory GRing.Theory Num.Theory DualAddTheory.
(* Def 5 p 32 *)
(* Final Def 1.5 p10 *)
(** *** Horizontal and vertical deviations **)
-Definition hDev_at (f g : F) (t : R+) : barR+ :=
+Definition hDev_at (f g : F) (t : {nonneg R}) : {nonnege R} :=
(ereal_inf [set d%:nngnum%:E | d in [set d
| f t <= g (t%:nngnum + d%:nngnum)%R%:nng]])%:nnge%E.
-Definition vDev_at (f g : F) (t : R+) : \bar R := ((f t) - (g t))%dE.
+Definition vDev_at (f g : F) (t : {nonneg R}) : \bar R := ((f t) - (g t))%dE.
(** Worst Case hDev and vDev **)
-Program Definition hDev (f g : F) : barR+ :=
+Program Definition hDev (f g : F) : {nonnege R} :=
Nonnege.NngeNum (ereal_sup [set (hDev_at f g t)%:nngenum%E | t in setT]) _.
Next Obligation.
apply: (@le_trans _ _ (hDev_at f g 0%R%:nng)%:nngenum%E) => //.
@@ -54,9 +54,9 @@ Definition vDev (f g : F) : \bar R := ereal_sup [set vDev_at f g t | t in setT].
(* Def 3 p30 *)
(* Final Def 1.3 p8 *)
(** *** Delay and Backlog **)
-Definition delay_at (A D : F) (t : R+) : barR+ := hDev_at A D t.
+Definition delay_at (A D : F) (t : {nonneg R}) : {nonnege R} := hDev_at A D t.
-Definition backlog_at (A D : flow_cc) t : R+ :=
+Definition backlog_at (A D : flow_cc) t : {nonneg R} :=
insubd 0%:nng ((A%:fcc t)%:nngnum - (D%:fcc t)%:nngnum).
Lemma backlog_atE A D t (S : partial_server) :
@@ -71,9 +71,9 @@ Qed.
(* Def 4 p 31 *)
(* Final Def 1.4 p9 *)
(** Worst Case - backlog - delay **)
-Definition delay (A D : F) : barR+ := hDev A D.
+Definition delay (A D : F) : {nonnege R} := hDev A D.
-Program Definition backlog (A D : flow_cc) : barR+ :=
+Program Definition backlog (A D : flow_cc) : {nonnege R} :=
Nonnege.NngeNum (ereal_sup [set (backlog_at A D t)%:nngnum%:E | t in setT]) _.
Next Obligation.
apply: (@le_trans _ _ (backlog_at A D 0%:nng)%:nngnum%:E).
@@ -151,7 +151,7 @@ case: (A t) HA => [a | |//] _; case: (D t) HD => [d | // |] _;
move=> _; exact: lee_pinfty.
Qed.
-Lemma hDev_suff (A : Fup) (D : F) (d : barR+) :
+Lemma hDev_suff (A : Fup) (D : F) (d : {nonnege R}) :
((A * delta d%:nngenum)%F <= D)%O -> ((hDev A D)%:nngenum <= d%:nngenum)%E.
Proof.
case: nngenumP => [d' |] Hd; [|by rewrite lee_pinfty].
diff --git a/fifo.v b/fifo.v
index 8d736667..c71e43e7 100644
--- a/fifo.v
+++ b/fifo.v
@@ -29,7 +29,7 @@ Import Order.Theory GRing.Theory Num.Theory DualAddTheory.
(* def 44 p183 *)
(* Final : def 7.7 p164 *)
Definition FIFO_service_policy n (S : n.+1.-server ) :=
- forall A D, S A D -> forall i j, forall t u : R+,
+ forall A D, S A D -> forall i j, forall t u : {nonneg R},
((A i) u < (D i) t -> (A j) u <= (D j) t)%E.
Lemma FIFO_one_server (S : 1.-server) : FIFO_service_policy S.
@@ -39,7 +39,7 @@ Proof. move=> A D HAD i j t u; rewrite !ord1; exact: ltW. Qed.
(* Final : Lem 7.2 p 165 *)
Lemma FIFO_aggregate_server n (S : n.+1.-server) :
FIFO_service_policy S ->
- forall A D, S A D -> forall t u : R+,
+ forall A D, S A D -> forall t u : {nonneg R},
(((\sum_i A i) u <= (\sum_i D i) t)%C <-> forall i, (A i) u <= (D i) t)%E.
Proof.
move=> fifo_server A D hAD t u; split; last first.
diff --git a/minerve/PA.v b/minerve/PA.v
index 657d9478..0d1be5f3 100644
--- a/minerve/PA.v
+++ b/minerve/PA.v
@@ -14,14 +14,14 @@ Local Open Scope ring_scope.
Import Order.Theory GRing.Theory Num.Theory DualAddTheory.
-Definition eq_point (f : F) (x : Q+) (y : \bar Q) :=
+Definition eq_point (f : F) (x : {nonneg rat}) (y : \bar rat) :=
f (toR x%:nngnum)%:nng = er_map toR y.
-Definition affine_on (f : F) (rs : Q * \bar Q) (x y : {nonneg rat}) :=
- forall t : R+, toR x%:nngnum < t%:nngnum < toR y%:nngnum ->
+Definition affine_on (f : F) (rs : rat * \bar rat) (x y : {nonneg rat}) :=
+ forall t : {nonneg R}, toR x%:nngnum < t%:nngnum < toR y%:nngnum ->
f t = ((toR rs.1 * (t%:nngnum - toR x%:nngnum))%R%:E + er_map toR rs.2)%dE.
-Definition JS_of a (f : F) (l : Q+) :=
+Definition JS_of a (f : F) (l : {nonneg rat}) :=
let fix aux x y rho_sigma a' :=
eq_point f x y /\
match a' with
@@ -34,7 +34,7 @@ Definition JS_of a (f : F) (l : Q+) :=
| (x, (y, rho_sigma)) :: a' => (x < l)%O /\ aux x y rho_sigma a'
end.
-Fixpoint JS_of' a (f : F) (l : Q+) :=
+Fixpoint JS_of' a (f : F) (l : {nonneg rat}) :=
match a with
| [::] => False
| xyrs :: a =>
@@ -68,20 +68,20 @@ split; [|by repeat split].
move: Hx'l; exact: lt_trans.
Qed.
-Lemma eq_point_eq (f f' : F) (x : Q+) y :
+Lemma eq_point_eq (f f' : F) (x : {nonneg rat}) y :
f (toR x%:nngnum)%:nng = f' (toR x%:nngnum)%:nng ->
eq_point f x y -> eq_point f' x y.
Proof. by move=> Hff'; case: y => [y | |] Hf; rewrite /eq_point -Hff'. Qed.
-Lemma affine_on_eq f f' rs (x y : Q+) :
- (forall t : R+, toR x%:nngnum <= t%:nngnum < toR y%:nngnum -> f t = f' t) ->
+Lemma affine_on_eq f f' rs (x y : {nonneg rat}) :
+ (forall t : {nonneg R}, toR x%:nngnum <= t%:nngnum < toR y%:nngnum -> f t = f' t) ->
affine_on f rs x y -> affine_on f' rs x y.
Proof.
by move=> Hff'; case: rs => r [s| |] H t /[dup] /andP[/ltW Ht' Ht''] Ht;
rewrite -Hff' ?H // Ht' Ht''.
Qed.
-Lemma JS_of_eq a f f' (l : Q+) :
+Lemma JS_of_eq a f f' (l : {nonneg rat}) :
sorted <%R (map fst a) ->
(forall t, toR (head_JS a).1%:nngnum <= t%:nngnum < toR l%:nngnum ->
f t = f' t) ->
@@ -102,7 +102,7 @@ move=> t /andP[Ht Ht']; apply: Hff'; rewrite Ht' andbT.
by apply: le_trans Ht; rewrite ler_rat -leEsub ltW //; move: Hs => /andP[].
Qed.
-Fixpoint F_of_JS_def (a : seq (Q * (\bar Q * (Q * \bar Q)))) (t : R+) :=
+Fixpoint F_of_JS_def (a : seq (rat * (\bar rat * (rat * \bar rat)))) (t : {nonneg R}) :=
match a with
| [::] => +oo%E
| (x, (y, (r, s))) :: a =>
@@ -118,7 +118,7 @@ Fixpoint F_of_JS_def (a : seq (Q * (\bar Q * (Q * \bar Q)))) (t : R+) :=
Definition F_of_JS (a : seq JS_elem) :=
F_of_JS_def [seq (xyrs.1%:nngnum, xyrs.2) | xyrs <- a].
-Lemma F_of_JS_correct (a : JS) (l : Q+) :
+Lemma F_of_JS_correct (a : JS) (l : {nonneg rat}) :
(last_JS a).1 < l -> JS_of a (F_of_JS a) l.
Proof.
case: a => /= -[//|[x [y [r s]]] a] _ Hh0 Hs Hl; split.
@@ -140,7 +140,7 @@ move=> Hs Hl; split; [|split; [|split]].
{ by move=> t /andP[Ht Ht']; rewrite /F_of_JS /= leNgt Ht Ht'. }
set f := (F_of_JS [:: (x, (y, (r, s))), (x', (y', (r', s'))) & a]).
pattern f; set aux := fun _ => _; rewrite {}/f.
-have H : forall f f', (forall t : R+, toR x'%:nngnum <= t%:nngnum -> f t = f' t) ->
+have H : forall f f', (forall t : {nonneg R}, toR x'%:nngnum <= t%:nngnum -> f t = f' t) ->
aux f -> aux f'.
{ move=> f f'; rewrite {}/aux.
elim: a x' y' r' s' Hs {IH Hl} => [|[x'' [y'' [r'' s'']]] a IH] x' y' r' s' Hs Hff'.
@@ -210,7 +210,7 @@ move=> -[Hfx [Hx'l [Hfrs H]]].
exact: IH.
Qed.
-Lemma eq_point_in_itv f rho_sigma (x x' x'' : Q+) :
+Lemma eq_point_in_itv f rho_sigma (x x' x'' : {nonneg rat}) :
x < x'' < x' ->
affine_on f rho_sigma x x' ->
eq_point f x'' (shift_rho_sigma rho_sigma (x''%:nngnum - x%:nngnum)).2.
@@ -222,7 +222,7 @@ case: rho_sigma => r [s|//|//] /=.
by rewrite rmorphD rmorphM rmorphB (addrC (toR s)).
Qed.
-Lemma affine_on_subitv f (rho_sigma : Q * \bar Q) (x y x' y' : Q+) :
+Lemma affine_on_subitv f (rho_sigma : rat * \bar rat) (x y x' y' : {nonneg rat}) :
x <= x' -> y' <= y ->
affine_on f rho_sigma x y ->
affine_on f (shift_rho_sigma rho_sigma (x'%:nngnum - x%:nngnum)) x' y'.
@@ -236,7 +236,7 @@ rewrite rmorphD rmorphM rmorphB -!daddEFin addrCA (addrC (toR s)).
by rewrite -mulrDr subrKA.
Qed.
-Lemma affine_on_prefix f (rho_sigma : Q * \bar Q) (x y y' : Q+) :
+Lemma affine_on_prefix f (rho_sigma : rat * \bar rat) (x y y' : {nonneg rat}) :
y' <= y -> affine_on f rho_sigma x y -> affine_on f rho_sigma x y'.
Proof.
move=> Hy'y H.
@@ -253,7 +253,7 @@ case: (filter _ _) => [|x' a'].
move=> /allP /=; apply; exact: mem_last.
Qed.
-Lemma JS_below_spec f (a : JS) (l' : Q+*) (l : Q+) :
+Lemma JS_below_spec f (a : JS) (l' : {posnum rat}) (l : {nonneg rat}) :
l'%:num <= l%:nngnum -> JS_of a f l -> JS_of (JS_below a l') f l'%:num%:nng.
Proof.
move=> Hl'l.
@@ -628,7 +628,7 @@ exact: IH.
Qed.
Definition JS_min_def (a a' : JS) l :=
- let fix aux x y rs y' rs' (a : seq (Q+ * _)) :=
+ let fix aux x y rs y' rs' (a : seq ({nonneg rat} * _)) :=
let (x', a) :=
match a with
| [::] => (l, [::])
@@ -658,7 +658,7 @@ Definition JS_min_def (a a' : JS) l :=
| (x, ((y, rs), (y', rs'))) :: a => aux x y rs y' rs' a
end.
-Program Definition JS_min (a a' : JS) (l : Q+) : JS :=
+Program Definition JS_min (a a' : JS) (l : {nonneg rat}) : JS :=
Build_JS (JS_min_def a a' l) _ _ _.
Next Obligation.
rewrite /JS_min_def /=.
@@ -761,7 +761,7 @@ have Hpoint : forall x y y',
{ by rewrite !ltEereal /= ltr_rat; case: ltP. }
{ by rewrite !lte_pinfty. }
by rewrite !lte_ninfty. }
-have Hleft : forall (x x' x'' : Q+) r s r' s',
+have Hleft : forall (x x' x'' : {nonneg rat}) r s r' s',
affine_on f (r, s%:E) x x' ->
affine_on f' (r', s'%:E) x x' ->
r <> r' ->
@@ -788,7 +788,7 @@ have Hleft : forall (x x' x'' : Q+) r s r' s',
rewrite ler_subr_addl.
apply: (le_trans Hx'').
by rewrite ltW // -nnQ2nnRE; apply/RltP. }
-have Hleft0 : forall (x x' : Q+) r s r' s',
+have Hleft0 : forall (x x' : {nonneg rat}) r s r' s',
affine_on f (r, s%:E) x x' ->
affine_on f' (r', s'%:E) x x' ->
r <> r' ->
@@ -798,7 +798,7 @@ have Hleft0 : forall (x x' : Q+) r s r' s',
{ move=> x x' r s r' s' Hfrs Hf'rs' Hrr' Hx'' Hr'r.
rewrite -(shift_rho_sigma_0 (r, s%:E)) -(subrr x%:nngnum).
move: (le_refl x) Hx'' Hr'r; exact: Hleft. }
-have Hleft' : forall (x x' x'' : Q+) r s r' s',
+have Hleft' : forall (x x' x'' : {nonneg rat}) r s r' s',
affine_on f (r, s%:E) x x' ->
affine_on f' (r', s'%:E) x x' ->
x <= x'' ->
@@ -823,7 +823,7 @@ have Hleft' : forall (x x' x'' : Q+) r s r' s',
rewrite ler_subr_addl.
apply: (le_trans Hx'').
by rewrite ltW // -nnQ2nnRE; apply/RltP. }
-have Hleft'0 : forall (x x' : Q+) r s r' s',
+have Hleft'0 : forall (x x' : {nonneg rat}) r s r' s',
affine_on f (r, s%:E) x x' ->
affine_on f' (r', s'%:E) x x' ->
x%:nngnum + (s' - s) / (r - r') <= x%:nngnum ->
@@ -832,7 +832,7 @@ have Hleft'0 : forall (x x' : Q+) r s r' s',
{ move=> x x' r s r' s' Hfrs Hf'rs' Hx'' Hr'r.
rewrite -(shift_rho_sigma_0 (r', s'%:E)) -(subrr x%:nngnum).
move: (le_refl x) Hx'' Hr'r; exact: Hleft'. }
-have Hright : forall (x x' : Q+) r s r' s',
+have Hright : forall (x x' : {nonneg rat}) r s r' s',
affine_on f (r, s%:E) x x' ->
affine_on f' (r', s'%:E) x x' ->
r <> r' ->
@@ -851,7 +851,7 @@ have Hright : forall (x x' : Q+) r s r' s',
rewrite ler_subl_addr addrC.
move: Hx''; apply: le_trans.
by rewrite ltW //; move: Ht => /andP[]. }
-have Hright' : forall (x x' : Q+) r s r' s',
+have Hright' : forall (x x' : {nonneg rat}) r s r' s',
affine_on f (r, s%:E) x x' ->
affine_on f' (r', s'%:E) x x' ->
x'%:nngnum <= x%:nngnum + (s' - s) / (r - r') ->
@@ -868,7 +868,7 @@ have Hright' : forall (x x' : Q+) r s r' s',
rewrite ler_subl_addr addrC.
move: Hx''; apply: le_trans.
by rewrite ltW //; move: Ht => /andP[]. }
-have Hmiddle_eq : forall (x x' : Q+) r s r' s',
+have Hmiddle_eq : forall (x x' : {nonneg rat}) r s r' s',
r <> r' ->
s + r * (x%:nngnum + (s' - s) / (r - r') - x%:nngnum)
= s' + r' * (x%:nngnum + (s' - s) / (r - r') - x%:nngnum).
@@ -879,7 +879,7 @@ have Hmiddle_eq : forall (x x' : Q+) r s r' s',
rewrite (addrC _ r) mulVr.
{ by rewrite mulr1 -opprB addrC subrr. }
by rewrite /mem /in_mem /= subr_eq0; apply/eqP. }
-have Hmiddle : forall (x x' : Q+) r s r' s',
+have Hmiddle : forall (x x' : {nonneg rat}) r s r' s',
affine_on f (r, s%:E) x x' ->
affine_on f' (r', s'%:E) x x' ->
r <> r' ->
@@ -900,7 +900,7 @@ have Hmiddle : forall (x x' : Q+) r s r' s',
have H : le = ri.
{ by rewrite /le /ri addrC [RHS]addrC Hmiddle_eq. }
by rewrite H minxx; do 2 apply: f_equal; rewrite -H /le addrC. }
-have Hmiddle' : forall (x x' : Q+) r s r' s',
+have Hmiddle' : forall (x x' : {nonneg rat}) r s r' s',
affine_on f (r, s%:E) x x' ->
affine_on f' (r', s'%:E) x x' ->
r <> r' ->
@@ -1042,7 +1042,7 @@ move: Hx''x => /ltW; rewrite {1}(_ : _ + _ = xs%:nngnum) ?[RHS]insubdK //.
exact: Hleft'.
Qed.
-Fixpoint JS_max_val a (l : Q+) :=
+Fixpoint JS_max_val a (l : {nonneg rat}) :=
match a with
| [::] => -oo%E
| (x, (y, (r, s))) :: a =>
@@ -1070,7 +1070,7 @@ Proof. by rewrite er_map_toR_max le_maxr. Qed.
Lemma JS_max_val_correct a f l :
JS_of a f l -> sorted <%O (map fst a) ->
- forall t : R+, toR (head_JS a).1%:nngnum <= t%:nngnum < toR l%:nngnum ->
+ forall t : {nonneg R}, toR (head_JS a).1%:nngnum <= t%:nngnum < toR l%:nngnum ->
(f t <= er_map toR (JS_max_val a l))%dE.
Proof.
move=> + Hs t Ht.
@@ -1107,7 +1107,7 @@ apply/orP; right.
by apply: IH => //=; rewrite Hx't Ht'.
Qed.
-Fixpoint JS_min_val a (l : Q+) :=
+Fixpoint JS_min_val a (l : {nonneg rat}) :=
match a with
| [::] => +oo%E
| (x, (y, (r, s))) :: a =>
@@ -1135,7 +1135,7 @@ Proof. by rewrite er_map_toR_min le_minl. Qed.
Lemma JS_min_val_correct a f l :
JS_of a f l -> sorted <%O (map fst a) ->
- forall t : R+, toR (head_JS a).1%:nngnum <= t%:nngnum < toR l%:nngnum ->
+ forall t : {nonneg R}, toR (head_JS a).1%:nngnum <= t%:nngnum < toR l%:nngnum ->
(er_map toR (JS_min_val a l) <= f t)%E.
Proof.
move=> + Hs t Ht.
@@ -1172,7 +1172,7 @@ apply/orP; right.
by apply: IH => //=; rewrite Hx't Ht'.
Qed.
-Fixpoint JS_eval a (l : Q+) :=
+Fixpoint JS_eval a (l : {nonneg rat}) :=
match a with
| [::] => +oo%E
| (x, (y, (r, s))) :: a =>
@@ -1185,7 +1185,7 @@ Fixpoint JS_eval a (l : Q+) :=
end
end.
-Lemma JS_eval_correct (a : JS) f (l l': Q+) :
+Lemma JS_eval_correct (a : JS) f (l l': {nonneg rat}) :
l < l' -> JS_of a f l' -> f (toR l%:nngnum)%:nng = er_map toR (JS_eval a l).
Proof.
move=> Hl Ha.
@@ -1211,10 +1211,10 @@ case: ltP => Hlx'.
exact: IH.
Qed.
-Program Definition JS_affine (r s : Q) : JS :=
+Program Definition JS_affine (r s : rat) : JS :=
Build_JS ([:: (0%:nng, (s%:E, (r, s%:E)))]) _ _ _.
-Lemma JS_affine_correct (r s : Q) (l : Q+*) :
+Lemma JS_affine_correct (r s : rat) (l : {posnum rat}) :
JS_of (JS_affine r s) (fun t => (toR r * t%:nngnum + toR s)%:E) l%:num%:nng.
Proof.
split; [|split].
@@ -1224,9 +1224,9 @@ by move=> t Ht; rewrite /= rmorph0 subr0.
Qed.
Definition JS_of_inf a f l :=
- JS_of a f l /\ (forall t : R+, toR l%:nngnum <= t%:nngnum -> f t = +oo%E).
+ JS_of a f l /\ (forall t : {nonneg R}, toR l%:nngnum <= t%:nngnum -> f t = +oo%E).
-Program Definition JS_point (x : Q+) y : JS :=
+Program Definition JS_point (x : {nonneg rat}) y : JS :=
Build_JS
(if x == 0%:nng then [:: (x, (y, (0, +oo%E)))]
else [:: (0%:nng ,(+oo, (0%R, +oo))%E); (x, (y, (0, +oo%E)))]) _ _ _.
@@ -1238,10 +1238,10 @@ apply/andP; split=> //.
by rewrite lt_def Hx leEsub /=.
Qed.
-Lemma JS_point_spec (x : Q+) y f (l: Q+) :
+Lemma JS_point_spec (x : {nonneg rat}) y f (l: {nonneg rat}) :
JS_of_inf (JS_point x y) f l ->
(f (toR x%:nngnum)%:nng = er_map toR y
- /\ (forall t : R+, t%:nngnum != toR x%:nngnum -> f t = +oo%E) /\ x < l).
+ /\ (forall t : {nonneg R}, t%:nngnum != toR x%:nngnum -> f t = +oo%E) /\ x < l).
Proof.
move=> [Hf Hf'].
split; [|split].
@@ -1279,7 +1279,7 @@ Qed.
Definition min_conv_point x y x' y' :=
JS_point (x%:nngnum + x'%:nngnum)%:nng (y + y')%dE.
-Lemma min_conv_point_spec (x x' : Q+) l l' y y' f f' :
+Lemma min_conv_point_spec (x x' : {nonneg rat}) l l' y y' f f' :
JS_of_inf (JS_point x y) f l ->
JS_of_inf (JS_point x' y') f' l' ->
JS_of (min_conv_point x y x' y') (f * f') (l%:nngnum + l'%:nngnum)%:nng.
@@ -1303,7 +1303,7 @@ have Hff' : (f * f')%F (toR (x%:nngnum + x'%:nngnum))%:nng = er_map toR (y + y')
have -> : v = (toR x'%:nngnum)%:nng; [exact: val_inj|].
by rewrite Hfxy Hfx'y er_map_toR_add. }
by rewrite Hfxy' //= lee_pinfty. }
-have Hff'' : forall t : R+, t != (toR (x%:nngnum + x'%:nngnum))%:nng ->
+have Hff'' : forall t : {nonneg R}, t != (toR (x%:nngnum + x'%:nngnum))%:nng ->
(f * f')%F t = +oo%E.
{ move=> t Ht'.
apply/le_anti; rewrite lee_pinfty /=.
@@ -1344,7 +1344,7 @@ apply: Hff''.
by move: Ht; rewrite lt_def => /andP [].
Qed.
-Program Definition JS_segment (x : Q+) y r s (l : Q+) : JS :=
+Program Definition JS_segment (x : {nonneg rat}) y r s (l : {nonneg rat}) : JS :=
Build_JS
(if l <= x then JS_zero : seq _
else if x == 0%R%:nng then [:: (x, (y, (r, s))); (l, (+oo, (0%R, +oo))%E)]
@@ -1360,13 +1360,13 @@ rewrite andbC /= lt_def; apply/andP; split.
by rewrite leEsub /=.
Qed.
-Lemma JS_segment_spec (x : Q+) y r s f (l l'': Q+) :
+Lemma JS_segment_spec (x : {nonneg rat}) y r s f (l l'': {nonneg rat}) :
x < l ->
JS_of_inf (JS_segment x y r s l) f l'' <->
(l < l''
- /\ (forall t : R+, t%:nngnum < toR x%:nngnum -> f t = +oo%E)
+ /\ (forall t : {nonneg R}, t%:nngnum < toR x%:nngnum -> f t = +oo%E)
/\ eq_point f x y /\ affine_on f (r, s) x l
- /\ (forall t : R+, toR l%:nngnum <= t%:nngnum -> f t = +oo%E)).
+ /\ (forall t : {nonneg R}, toR l%:nngnum <= t%:nngnum -> f t = +oo%E)).
Proof.
move=> Hxl.
split.
@@ -1426,13 +1426,13 @@ move=> [Hll'' [Hf0x [Hfx [Hfxl Hfl]]]]; split.
by move=> t Ht; apply: Hfl; apply: le_trans Ht; rewrite ler_rat -leEsub ltW.
Qed.
-Lemma JS_segment_spec_open (x : Q+) r s f (l l'': Q+) :
+Lemma JS_segment_spec_open (x : {nonneg rat}) r s f (l l'': {nonneg rat}) :
x < l ->
JS_of_inf (JS_segment x +oo%E r s l) f l'' <->
(l < l''
- /\ (forall t : R+, t%:nngnum <= toR x%:nngnum -> f t = +oo%E)
+ /\ (forall t : {nonneg R}, t%:nngnum <= toR x%:nngnum -> f t = +oo%E)
/\ affine_on f (r, s) x l
- /\ (forall t : R+, toR l%:nngnum <= t%:nngnum -> f t = +oo%E)).
+ /\ (forall t : {nonneg R}, toR l%:nngnum <= t%:nngnum -> f t = +oo%E)).
Proof.
move=> Hxl; rewrite (JS_segment_spec _ _ _ _ _ Hxl); split.
{ move=> [Hll'' [Hf0x [Hfx [Hfxl Hfl]]]].
@@ -1445,7 +1445,7 @@ split=> [//|]; split; [|split; [|by split]].
by rewrite /eq_point /= Hf0x.
Qed.
-Lemma JS_segment_to_point_open_segment x y r s (l : Q+) f (l'' : Q+) :
+Lemma JS_segment_to_point_open_segment x y r s (l : {nonneg rat}) f (l'' : {nonneg rat}) :
x < l ->
JS_of_inf (JS_segment x y r s l) f l'' ->
exists f' f'', f = F_min f' f'' /\ JS_of_inf (JS_point x y) f' l''
@@ -1496,8 +1496,8 @@ Definition min_conv_point_open_segment x y x' r' s' l' :=
JS_segment (x%:nngnum + x'%:nngnum)%:nng +oo%E r' (s' + y)%dE
(x%:nngnum + l'%:nngnum)%:nng.
-Lemma min_conv_point_open_segment_spec (x : Q+) (y : \bar Q) x' r' s'
- (l' : Q+) f f' (l'' l''' : Q+) :
+Lemma min_conv_point_open_segment_spec (x : {nonneg rat}) (y : \bar rat) x' r' s'
+ (l' : {nonneg rat}) f f' (l'' l''' : {nonneg rat}) :
x' < l' ->
JS_of_inf (JS_point x y) f l'' ->
JS_of_inf (JS_segment x' +oo%E r' s' l') f' l''' ->
@@ -1714,15 +1714,15 @@ by case: ltP => _ /=; rewrite andbT !ltEsub /= addrC ?ltr_add2l ?ltr_add2r
apply/andP; (split; [apply/eqP|]).
Qed.
-Lemma min_conv_open_segment_spec x r s (l : Q+) x' r' s' (l' : Q+)
- f f' (l'' l''' : Q+) :
+Lemma min_conv_open_segment_spec x r s (l : {nonneg rat}) x' r' s' (l' : {nonneg rat})
+ f f' (l'' l''' : {nonneg rat}) :
x < l -> x' < l' ->
JS_of_inf (JS_segment x +oo%E r s l) f l'' ->
JS_of_inf (JS_segment x' +oo%E r' s' l') f' l''' ->
JS_of (min_conv_open_segment x r s l x' r' s' l') (f * f')
(l''%:nngnum + l'''%:nngnum)%:nng.
Proof.
-suff: forall f f' (x x' l l' : Q+) r r' s s' l'' l''',
+suff: forall f f' (x x' l l' : {nonneg rat}) r r' s s' l'' l''',
r <= r' -> x < l -> x' < l' ->
JS_of_inf (JS_segment x +oo r s l) f l'' ->
JS_of_inf (JS_segment x' +oo r' s' l') f' l''' ->
@@ -1914,7 +1914,7 @@ have Hxx'x'l : forall t,
{ rewrite /in_mem /= subr_ge0.
by apply: le_trans (ltW Ht); rewrite ler_addr. }
rewrite FDioid.F_min_convC alt_def_F_min_conv.
- rewrite /F_min_conv (Rbar_inf_split [set v : R+ |
+ rewrite /F_min_conv (Rbar_inf_split [set v : {nonneg R} |
(toR x%:nngnum < t%:nngnum - v%:nngnum < toR l%:nngnum)
&& (toR x'%:nngnum < v%:nngnum < toR l'%:nngnum)]).
rewrite minEle ifT; last first.
@@ -2034,7 +2034,7 @@ have Hx'lll' : affine_on (f * f')
{ rewrite /in_mem /= subr_ge0.
by apply: le_trans (ltW Ht); rewrite ler_addr. }
rewrite alt_def_F_min_conv.
- rewrite /F_min_conv (Rbar_inf_split [set u : R+ |
+ rewrite /F_min_conv (Rbar_inf_split [set u : {nonneg R} |
(toR x%:nngnum < u%:nngnum < toR l%:nngnum)
&& (toR x'%:nngnum < t%:nngnum - u%:nngnum < toR l'%:nngnum)]).
rewrite minEle ifT; last first.
@@ -2204,7 +2204,7 @@ apply: JS_min_correct.
exact/(JS_below_spec H2li)/min_conv_open_segment_spec.
Qed.
-Definition cutting_below (f : F) (l : Q+) : F :=
+Definition cutting_below (f : F) (l : {nonneg rat}) : F :=
fun t => if t%:nngnum < toR l%:nngnum then f t else +oo%E.
Lemma cutting_below_comp f l l' :
@@ -2278,11 +2278,11 @@ Qed.
Lemma JS_of_first_segment x y r s x' y' r' s' (a : seq JS_elem) f l :
sorted <%R (map fst ((x, (y, (r, s))) :: (x', (y', (r', s'))) :: a)) ->
- (forall t : R+, t%:nngnum < toR x%:nngnum -> f t = +oo%E) ->
+ (forall t : {nonneg R}, t%:nngnum < toR x%:nngnum -> f t = +oo%E) ->
JS_of ((x, (y, (r, s))) :: (x', (y', (r', s'))) :: a) f l ->
exists f' f'', f = F_min f' f'' /\ JS_of_inf (JS_segment x y r s x') f' l
/\ JS_of ((x', (y', (r', s'))) :: a) f'' l
- /\ forall t : R+, t%:nngnum < toR x'%:nngnum -> f'' t = +oo%E.
+ /\ forall t : {nonneg R}, t%:nngnum < toR x'%:nngnum -> f'' t = +oo%E.
Proof.
move=> Hs Hf0x [Hxl [Hfx [Hx'l [Hfxx' Haux]]]].
exists (cutting_below f x').
@@ -2305,7 +2305,7 @@ split; [|split; [|split]].
by move=> t Ht; rewrite leNgt Ht.
Qed.
-Fixpoint min_conv_segment_JS x y r s l (a : seq JS_elem) (l' : Q+*) : JS :=
+Fixpoint min_conv_segment_JS x y r s l (a : seq JS_elem) (l' : {posnum rat}) : JS :=
match a with
| [::] => JS_zero
| (x', (y', (r', s'))) :: a' =>
@@ -2318,7 +2318,7 @@ Fixpoint min_conv_segment_JS x y r s l (a : seq JS_elem) (l' : Q+*) : JS :=
end
end.
-Lemma min_conv_segment_JS_spec x y r s (l : Q+) (a : JS) f f' li (l'' : Q+*) :
+Lemma min_conv_segment_JS_spec x y r s (l : {nonneg rat}) (a : JS) f f' li (l'' : {posnum rat}) :
x < l -> l''%:num <= li%:nngnum ->
JS_of_inf (JS_segment x y r s l) f li ->
JS_of_inf a f' l''%:num%:nng ->
@@ -2326,7 +2326,7 @@ Lemma min_conv_segment_JS_spec x y r s (l : Q+) (a : JS) f f' li (l'' : Q+*) :
Proof.
move=> Hxl Hli Hf Hf'.
case: a Hf' => a /= Hne /eqP H0 Hs Hf'.
-have {H0}: forall t : R+, t%:nngnum < toR (head_JS a).1%:nngnum -> f' t = +oo%E.
+have {H0}: forall t : {nonneg R}, t%:nngnum < toR (head_JS a).1%:nngnum -> f' t = +oo%E.
{ by move=> t; rewrite H0 /= rmorph0 nngnum_lt0. }
elim: a x y r s l f f' Hxl Hf Hf' Hne Hs =>
[// | [x' [y' [r' s']]] a IH] x y r s l f f' Hxl Hf Hf' _ Hs.
@@ -2354,7 +2354,7 @@ move=> t Ht; apply/le_anti; rewrite lee_pinfty /= -(proj2 Hf' t Ht).
by rewrite Hf'12 /F_min /= le_minl lexx orbT.
Qed.
-Fixpoint JS_min_conv (a b : seq JS_elem) (l'' : Q+*) : JS :=
+Fixpoint JS_min_conv (a b : seq JS_elem) (l'' : {posnum rat}) : JS :=
match a with
| [::] => JS_zero
| (x, (y, (r, s))) :: a' =>
@@ -2367,7 +2367,7 @@ Fixpoint JS_min_conv (a b : seq JS_elem) (l'' : Q+*) : JS :=
end
end.
-Lemma JS_min_conv_correct (a a' : JS) f f' (l'' : Q+*) :
+Lemma JS_min_conv_correct (a a' : JS) f f' (l'' : {posnum rat}) :
JS_of a f l''%:num%:nng -> JS_of a' f' l''%:num%:nng ->
JS_of (JS_min_conv a a' l'') (f * f') l''%:num%:nng.
Proof.
@@ -2376,7 +2376,7 @@ rewrite -JS_of_cutting_below => /JS_of_inf_cutting_below Hf'.
rewrite -JS_of_cutting_below cutting_below_conv JS_of_cutting_below.
move: (cutting_below f _) (cutting_below f' _) Hf Hf' => {}f {}f' {}Hf {}Hf'.
case: a Hf Hf' => a /= Hne /eqP H0 Hs Hf Hf'.
-have {H0}: forall t : R+, t%:nngnum < toR (head_JS a).1%:nngnum -> f t = +oo%E.
+have {H0}: forall t : {nonneg R}, t%:nngnum < toR (head_JS a).1%:nngnum -> f t = +oo%E.
{ by move=> t; rewrite H0 /= rmorph0 nngnum_lt0. }
elim: a f Hne Hs Hf => [// | [x [y [r s]]] a IH] f _ Hs Hf.
case: a IH Hs Hf => [_ _ | [x' [y' [r' s']]] a IH Hs] Hf H'f.
@@ -2417,11 +2417,11 @@ Qed.
Lemma JS_eq (a : JS) f f' l :
JS_of a f l -> JS_of a f' l ->
- forall t : R+, t%:nngnum < toR l%:nngnum -> f t = f' t.
+ forall t : {nonneg R}, t%:nngnum < toR l%:nngnum -> f t = f' t.
Proof.
case: a => a /= _ /eqP H0 Hs.
move=> Hf Hf'.
-suff: forall t : R+, toR (head_JS a).1%:nngnum <= t%:nngnum < toR l%:nngnum ->
+suff: forall t : {nonneg R}, toR (head_JS a).1%:nngnum <= t%:nngnum < toR l%:nngnum ->
f t = f' t.
{ by move=> H t Ht; apply H; apply/andP; split=> [|//]; rewrite H0 /= toR0. }
move: Hf Hf'.
@@ -2454,7 +2454,7 @@ Definition JS_eqb a a' :=
== JS_normalize [seq (x.1, x.2.2) | x <- a''].
Lemma JS_eqb_correct (a a' : JS) f f' l : JS_of a f l -> JS_of a' f' l ->
- JS_eqb a a' -> forall t : R+, t%:nngnum < toR l%:nngnum -> f t = f' t.
+ JS_eqb a a' -> forall t : {nonneg R}, t%:nngnum < toR l%:nngnum -> f t = f' t.
Proof.
move=> Hf Hf' /eqP H.
move: (JS_merge_correct Hf Hf') => [].
diff --git a/minerve/PA_refinement.v b/minerve/PA_refinement.v
index e29f7e10..c8b720ca 100644
--- a/minerve/PA_refinement.v
+++ b/minerve/PA_refinement.v
@@ -377,30 +377,30 @@ Parametricity seqjs_eqb.
Section theory.
-Definition rnnQ : Q+ -> Q -> Type := fun e1 e2 => Nonneg.num_of_nng e1 = e2.
+Definition rnnQ : {nonneg rat} -> rat -> Type := fun e1 e2 => Nonneg.num_of_nng e1 = e2.
-Definition rposQ : Q+* -> Q -> Type := fun e1 e2 => num_of_pos e1 = e2.
+Definition rposQ : {posnum rat} -> rat -> Type := fun e1 e2 => num_of_pos e1 = e2.
Definition Rseqjse :
- (Q+ * (\bar Q * (Q * \bar Q))) ->
- (Q * (\bar Q * (Q * \bar Q))) -> Type :=
+ ({nonneg rat} * (\bar rat * (rat * \bar rat))) ->
+ (rat * (\bar rat * (rat * \bar rat))) -> Type :=
prod_R rnnQ eq.
Definition Rseqjse2 :
- (Q+ * ((\bar Q * (Q * \bar Q)) * (\bar Q * (Q * \bar Q)))) ->
- (Q * ((\bar Q * (Q * \bar Q)) * (\bar Q * (Q * \bar Q)))) ->
+ ({nonneg rat} * ((\bar rat * (rat * \bar rat)) * (\bar rat * (rat * \bar rat)))) ->
+ (rat * ((\bar rat * (rat * \bar rat)) * (\bar rat * (rat * \bar rat)))) ->
Type :=
prod_R rnnQ eq.
-Definition Rseqjs : JS -> @seqjs Q -> Type := list_R Rseqjse.
+Definition Rseqjs : JS -> @seqjs rat -> Type := list_R Rseqjse.
Definition Rseqjs' :
- seq (Q+ * (\bar Q * (Q * \bar Q))) -> @seqjs Q -> Type :=
+ seq ({nonneg rat} * (\bar rat * (rat * \bar rat))) -> @seqjs rat -> Type :=
list_R Rseqjse.
Definition Rseqjs2' :
- seq (Q+ * ((\bar Q * (Q * \bar Q)) * (\bar Q * (Q * \bar Q)))) ->
- @seqjs2 Q -> Type :=
+ seq ({nonneg rat} * ((\bar rat * (rat * \bar rat)) * (\bar rat * (rat * \bar rat)))) ->
+ @seqjs2 rat -> Type :=
list_R Rseqjse2.
Local Instance zero_rat : zero_of rat := 0%R.
@@ -415,20 +415,20 @@ Local Instance eq_rat : eq_of rat := eqtype.eq_op.
Local Instance lt_rat : lt_of rat := Num.lt.
Local Instance le_rat : leq_of rat := Num.le.
-Local Instance Req_Q (x : Q) : refines eq x x.
+Local Instance Req_Q (x : rat) : refines eq x x.
Proof. by rewrite refinesE. Qed.
-Local Instance Req_Qbar (x : \bar Q) : refines eq x x.
+Local Instance Req_Qbar (x : \bar rat) : refines eq x x.
Proof. by rewrite refinesE. Qed.
-Local Instance rnnQ_nngnum (x : Q+) : refines rnnQ x x%:nngnum%R.
+Local Instance rnnQ_nngnum (x : {nonneg rat}) : refines rnnQ x x%:nngnum%R.
Proof. by rewrite refinesE. Qed.
Local Instance rnnQ_add x y :
refines rnnQ (x%:nngnum + y%:nngnum)%:nng%R (x%:nngnum%R + y%:nngnum%R)%C.
Proof. by rewrite refinesE. Qed.
-Local Instance rposQ_num (x : Q+*) : refines rposQ x x%:num%R.
+Local Instance rposQ_num (x : {posnum rat}) : refines rposQ x x%:num%R.
Proof. by rewrite refinesE. Qed.
Local Instance Rseqjs_Rseqjs' x y : refines Rseqjs x y -> refines Rseqjs' x y.
@@ -554,7 +554,7 @@ by constructor; [|constructor].
Qed.
Local Instance Rseqjs_er_opp :
- refines (@eq (\bar Q) ==> eq)%rel oppe seqjs_er_opp.
+ refines (@eq (\bar rat) ==> eq)%rel oppe seqjs_er_opp.
Proof.
rewrite refinesE => x _ <-; case: x => //= x.
by rewrite /sub_op /sub_rat GRing.add0r.
@@ -570,7 +570,7 @@ constructor=> //; apply: f_equal2; [|apply: f_equal2];
Qed.
Local Instance Rseqjs_add_cst :
- refines (@eq (\bar Q) ==> Rseqjs ==> Rseqjs)%rel JS_add_cst seqjs_add_cst.
+ refines (@eq (\bar rat) ==> Rseqjs ==> Rseqjs)%rel JS_add_cst seqjs_add_cst.
Proof.
rewrite refinesE => c _ <- a1 a2 ra.
rewrite /Rseqjs /= /seqjs_add_cst.
@@ -620,7 +620,7 @@ by constructor.
Qed.
Local Instance Rseqjs_er_add :
- refines (@eq (\bar Q) ==> eq ==> eq)%rel dual_adde seqjs_er_add.
+ refines (@eq (\bar rat) ==> eq ==> eq)%rel dual_adde seqjs_er_add.
Proof. by rewrite refinesE => x _ <- x' _ <-. Qed.
Local Instance Rseqjs_add :
@@ -800,7 +800,7 @@ by constructor; [|apply: f_equal2].
Qed.
Local Instance Rseqjs_point :
- refines (rnnQ ==> @eq (\bar Q) ==> Rseqjs)%rel JS_point seqjs_point.
+ refines (rnnQ ==> @eq (\bar rat) ==> Rseqjs)%rel JS_point seqjs_point.
Proof.
rewrite refinesE /Rseqjs /seqjs_point => x _ <- y _ <- /=.
rewrite /eq_op /eq_rat /zero_op /zero_rat nng_eq0.
@@ -810,7 +810,7 @@ Qed.
Local Instance Rseqjs_min_conv_point :
refines
- (rnnQ ==> @eq (\bar Q) ==> rnnQ ==> @eq (\bar Q) ==> Rseqjs)%rel
+ (rnnQ ==> @eq (\bar rat) ==> rnnQ ==> @eq (\bar rat) ==> Rseqjs)%rel
min_conv_point seqjs_min_conv_point.
Proof.
rewrite refinesE => x _ <- y _ <- x' _ <- y' _ <-.
@@ -820,7 +820,7 @@ Qed.
Local Instance Rseqjs_segment :
refines
- (rnnQ ==> @eq (\bar Q) ==> @eq Q ==> @eq (\bar Q) ==> rnnQ ==> Rseqjs)%rel
+ (rnnQ ==> @eq (\bar rat) ==> @eq rat ==> @eq (\bar rat) ==> rnnQ ==> Rseqjs)%rel
JS_segment seqjs_segment.
Proof.
rewrite refinesE => x _ <- y _ <- r _ <- s _ <- l _ <-.
@@ -833,7 +833,7 @@ Qed.
Local Instance Rseqjs_min_conv_point_open_segment :
refines
- (rnnQ ==> @eq (\bar Q) ==> rnnQ ==> @eq Q ==> @eq (\bar Q) ==> rnnQ ==>
+ (rnnQ ==> @eq (\bar rat) ==> rnnQ ==> @eq rat ==> @eq (\bar rat) ==> rnnQ ==>
Rseqjs)%rel
min_conv_point_open_segment seqjs_min_conv_point_open_segment.
Proof.
@@ -844,8 +844,8 @@ Qed.
Local Instance Rseqjs_min_conv_open_segment :
refines
- (rnnQ ==> @eq Q ==> @eq (\bar Q) ==> rnnQ ==>
- rnnQ ==> @eq Q ==> @eq (\bar Q) ==> rnnQ ==>
+ (rnnQ ==> @eq rat ==> @eq (\bar rat) ==> rnnQ ==>
+ rnnQ ==> @eq rat ==> @eq (\bar rat) ==> rnnQ ==>
Rseqjs)%rel
min_conv_open_segment seqjs_min_conv_open_segment.
Proof.
@@ -863,8 +863,8 @@ Qed.
Local Instance Rseqjs_min_conv_segment :
refines
- (rnnQ ==> @eq (\bar Q) ==> @eq Q ==> @eq (\bar Q) ==> rnnQ ==>
- rnnQ ==> @eq (\bar Q) ==> @eq Q ==> @eq (\bar Q) ==> rnnQ ==>
+ (rnnQ ==> @eq (\bar rat) ==> @eq rat ==> @eq (\bar rat) ==> rnnQ ==>
+ rnnQ ==> @eq (\bar rat) ==> @eq rat ==> @eq (\bar rat) ==> rnnQ ==>
rposQ ==> Rseqjs)%rel
min_conv_segment seqjs_min_conv_segment.
Proof.
@@ -876,7 +876,7 @@ Qed.
Local Instance Rseqjs_min_conv_segment_seqjs :
refines
- (rnnQ ==> @eq (\bar Q) ==> @eq Q ==> @eq (\bar Q) ==> rnnQ ==>
+ (rnnQ ==> @eq (\bar rat) ==> @eq rat ==> @eq (\bar rat) ==> rnnQ ==>
Rseqjs' ==> rposQ ==> Rseqjs)%rel
min_conv_segment_JS seqjs_min_conv_segment_seqjs.
Proof.
@@ -916,7 +916,7 @@ by move=> _ _ [x _ <- + _ <-] => -[y rs]; split=> [/=|//].
Qed.
Local Instance Rseqjs_er_eq :
- refines (@eq (\bar Q) ==> eq ==> bool_R)%rel eqtype.eq_op seqjs_er_eq.
+ refines (@eq (\bar rat) ==> eq ==> bool_R)%rel eqtype.eq_op seqjs_er_eq.
Proof.
rewrite refinesE => x _ <- x' _ <-; case: x => [x| |]; case: x' => [x'| |] //=.
exact: bool_Rxx.
@@ -972,7 +972,7 @@ Context `{!spec_of C rat}.
Context `{!refines (eq ==> rratC)%rel spec spec_id}.
Definition rratCe :
- (Q * (\bar Q * (Q * \bar Q))) ->
+ (rat * (\bar rat * (rat * \bar rat))) ->
(C * (\bar C * (C * \bar C))) -> Type :=
prod_R rratC (prod_R (extended_R rratC) (prod_R rratC (extended_R rratC))).
diff --git a/minerve/UPP.v b/minerve/UPP.v
index 38c5143e..fead9b15 100644
--- a/minerve/UPP.v
+++ b/minerve/UPP.v
@@ -18,28 +18,28 @@ Section UPP.
Record F_UPP := {
F_UPP_val :> F;
- F_UPP_T : Q+;
- F_UPP_d : Q+*;
- F_UPP_c : Q;
- _ : forall t : R+, toR F_UPP_T%:nngnum <= t%:nngnum ->
+ F_UPP_T : {nonneg rat};
+ F_UPP_d : {posnum rat};
+ F_UPP_c : rat;
+ _ : forall t : {nonneg R}, toR F_UPP_T%:nngnum <= t%:nngnum ->
(F_UPP_val (t%:nngnum + toR F_UPP_d%:num)%R%:nng
= F_UPP_val t + (toR F_UPP_c)%:E)%dE
}.
Arguments Build_F_UPP : clear implicits.
Lemma F_UPP_prop (f : F_UPP) :
- forall t : R+, toR (F_UPP_T f)%:nngnum <= t%:nngnum ->
+ forall t : {nonneg R}, toR (F_UPP_T f)%:nngnum <= t%:nngnum ->
(f (t%:nngnum + toR (F_UPP_d f)%:num)%R%:nng = f t + (toR (F_UPP_c f))%:E)%dE.
Proof. by case f. Qed.
-Definition F_UPP_of_F_def (f : F) (T d c : Q) :=
- fun (t : R+) =>
+Definition F_UPP_of_F_def (f : F) (T d c : rat) :=
+ fun (t : {nonneg R}) =>
if t%:nngnum < toR (T + d) then f t else
let n := (floor ((t%:nngnum - toR T) / toR d))%:~R in
let t' := insubd 0%:nng (t%:nngnum - toR (n * d)) in
(f t' + (toR (n * c))%R%:E)%dE.
-Program Definition F_UPP_of_F (f : F) (T : Q+) (d : Q+*) (c : Q) :=
+Program Definition F_UPP_of_F (f : F) (T : {nonneg rat}) (d : {posnum rat}) (c : rat) :=
Build_F_UPP (F_UPP_of_F_def f T%:nngnum d%:num c) T d c _.
Next Obligation.
rewrite /F_UPP_of_F_def rmorphD /= ltr_add2r ltNge H /= !rmorphM /= !ratr_int.
@@ -65,9 +65,9 @@ rewrite mulrDl mul1r (addrC (_ * _) (toR d%:num)) addrKA.
by rewrite [X in X%:E]mulrDl mul1r -daddeA -daddEFin.
Qed.
-Lemma UPP_extension_prop (f : F_UPP) (k : nat) (T' : Q+) :
+Lemma UPP_extension_prop (f : F_UPP) (k : nat) (T' : {nonneg rat}) :
F_UPP_T f <= T' ->
- forall t : R+, toR T'%:nngnum <= t%:nngnum ->
+ forall t : {nonneg R}, toR T'%:nngnum <= t%:nngnum ->
f (t%:nngnum + toR (k%:R * (F_UPP_d f)%:num))%:nng
= (f t + (toR (k%:R * (F_UPP_c f)))%R%:E)%dE.
Proof.
@@ -85,7 +85,7 @@ by apply: (le_trans Ht); rewrite ler_addl rmorphM; apply: mulr_ge0.
Qed.
Program Definition UPP_extension
- (f : F_UPP) (k : nat) (T' : Q+) (HTT' : F_UPP_T f <= T') : F_UPP :=
+ (f : F_UPP) (k : nat) (T' : {nonneg rat}) (HTT' : F_UPP_T f <= T') : F_UPP :=
Build_F_UPP
f
T'
@@ -111,14 +111,14 @@ Program Definition F_UPP_add (f f' : F_UPP) : F_UPP :=
Build_F_UPP
(F_plus f f')
(Order.max (F_UPP_T f)%:nngnum (F_UPP_T f')%:nngnum)%:nng
- (lcm_posQ (F_UPP_d f) (F_UPP_d f'))
- ((lcm_posQ (F_UPP_d f) (F_UPP_d f'))%:num
+ (lcm_pos_rat (F_UPP_d f) (F_UPP_d f'))
+ ((lcm_pos_rat (F_UPP_d f) (F_UPP_d f'))%:num
* (F_UPP_c f / (F_UPP_d f)%:num + F_UPP_c f' / (F_UPP_d f')%:num))
_.
Next Obligation.
move: H.
set tilde_T := Order.max _ _ => Ht.
-set tilde_d := lcm_posQ _ _.
+set tilde_d := lcm_pos_rat _ _.
rewrite /F_plus.
move: (dvdq_lcml (F_UPP_d f) (F_UPP_d f')) => /= [k Hk].
move: (dvdq_lcmr (F_UPP_d f) (F_UPP_d f')) => /= [k' Hk'].
@@ -138,7 +138,7 @@ rewrite mulrAC -mulrA divrK; [|exact: posnum_neq0].
by rewrite rmorphD /= addrC.
Qed.
-Lemma F_UPP_min_aux (t : R) (T : Q+) (d : Q+*) :
+Lemma F_UPP_min_aux (t : R) (T : {nonneg rat}) (d : {posnum rat}) :
toR T%:nngnum <= t ->
exists k : nat,
toR T%:nngnum <= t - toR (k%:R * d%:num) < toR (T%:nngnum + d%:num).
@@ -165,10 +165,10 @@ Let cd f := c f / (d f)%:num.
Definition hypotheses_UPP_min f f' M m :=
cd f < cd f'
- /\ (forall t : R+,
+ /\ (forall t : {nonneg R},
toR (T f)%:nngnum <= t%:nngnum < toR ((T f)%:nngnum + (d f)%:num) ->
(f t <= (toR M + toR (cd f) * t%:nngnum)%R%:E)%dE)
- /\ (forall t : R+,
+ /\ (forall t : {nonneg R},
toR (T f')%:nngnum <= t%:nngnum < toR ((T f')%:nngnum + (d f')%:num) ->
((toR m + toR (cd f') * t%:nngnum)%R%:E <= f' t)%dE).
@@ -182,11 +182,11 @@ Definition tilde_T_min f f' M m :=
((insubd 0%:nng (M - m))%:nngnum / (insubd 0%:nng (cd f - cd f'))%:nngnum)%:nng)%:nngnum)%:nng.
Definition tilde_d_min f f' :=
- if cd f == cd f' then lcm_posQ (d f) (d f')
+ if cd f == cd f' then lcm_pos_rat (d f) (d f')
else if cd f < cd f' then d f else d f'.
Definition tilde_c_min f f' :=
- if cd f == cd f' then (lcm_posQ (d f) (d f'))%:num * cd f
+ if cd f == cd f' then (lcm_pos_rat (d f) (d f'))%:num * cd f
else if cd f < cd f' then c f else c f'.
Lemma tilde_T_minC f f' M m : tilde_T_min f f' M m = tilde_T_min f' f M m.
@@ -201,7 +201,7 @@ Qed.
Lemma tilde_d_minC : commutative tilde_d_min.
Proof.
move=> f f'.
-rewrite /tilde_d_min lcm_posQC eq_sym.
+rewrite /tilde_d_min lcm_pos_ratC eq_sym.
case: eqP => [//|] /eqP Hcd.
rewrite lt_def Hcd /= leNgt.
by case: ltP.
@@ -210,13 +210,13 @@ Qed.
Lemma tilde_c_minC : commutative tilde_c_min.
Proof.
move=> f f'.
-rewrite /tilde_c_min lcm_posQC eq_sym.
+rewrite /tilde_c_min lcm_pos_ratC eq_sym.
case: eqP => [-> //|] /eqP Hcd.
rewrite lt_def Hcd /= leNgt.
by case: ltP.
Qed.
-Program Definition F_UPP_min (f f' : F_UPP) (M m : Q) : _ -> F_UPP :=
+Program Definition F_UPP_min (f f' : F_UPP) (M m : rat) : _ -> F_UPP :=
fun _ : (cd f = cd f'
\/ hypotheses_UPP_min f f' M m \/ hypotheses_UPP_min f' f M m) =>
Build_F_UPP
@@ -228,7 +228,7 @@ Next Obligation.
move: f f' M m H t H0.
suff : forall f f' M m,
(cd f = cd f' \/ hypotheses_UPP_min f f' M m) ->
- forall t : R+, toR (tilde_T_min f f' M m)%:nngnum <= t%:nngnum ->
+ forall t : {nonneg R}, toR (tilde_T_min f f' M m)%:nngnum <= t%:nngnum ->
F_min f f' (t%:nngnum + toR (tilde_d_min f f')%:num)%:nng
= (F_min f f' t + (toR (tilde_c_min f f'))%:E)%dE.
{ move=> H f f' M m [|[]] H' t Ht.
@@ -263,7 +263,7 @@ move: Hmin (H't) => -[Hcd [HM Hm]].
have Hcd' : cd f == cd f' = false.
{ by apply/negbTE; move: Hcd; rewrite eq_sym lt_def => /andP []. }
rewrite /tilde_T_min /tilde_d_min /tilde_c_min Hcd' Hcd /F_min => Ht.
-have {}HM : forall t : R+, toR (T f)%:nngnum <= t%:nngnum ->
+have {}HM : forall t : {nonneg R}, toR (T f)%:nngnum <= t%:nngnum ->
(f t <= (toR M + toR (cd f) * t%:nngnum)%R%:E)%dE.
{ move=> t' Ht'.
have PTf : 0 <= toR (T f)%:nngnum; [by rewrite -toR0 ler_rat|].
@@ -276,7 +276,7 @@ have {}HM : forall t : R+, toR (T f)%:nngnum <= t%:nngnum ->
rewrite (_ : toR (cd f) * toR (k%:R * _) = toR (k%:R * F_UPP_c f)).
2:{ rewrite /cd -rmorphM /= mulrCA divrK //; exact: posnum_neq0. }
by apply/lee_dadd2r/HM; rewrite Hk Hk'. }
-have {}Hm : forall t : R+, toR (T f')%:nngnum <= t%:nngnum ->
+have {}Hm : forall t : {nonneg R}, toR (T f')%:nngnum <= t%:nngnum ->
((toR m + toR (cd f') * t%:nngnum)%R%:E <= f' t)%dE.
{ move=> t' Ht'.
have PTf' : 0 <= toR (T f')%:nngnum; [by rewrite -toR0 ler_rat|].
@@ -290,7 +290,7 @@ have {}Hm : forall t : R+, toR (T f')%:nngnum <= t%:nngnum ->
rewrite (_ : toR (cd f') * toR (k%:R * _) = toR (k%:R * F_UPP_c f')).
2:{ rewrite /cd -rmorphM /= mulrCA divrK //; exact: posnum_neq0. }
by apply/lee_dadd2r/Hm; rewrite Hk Hk'. }
-have HMm : forall t : R+, toR (tilde_T_min f f' M m)%:nngnum <= t%:nngnum ->
+have HMm : forall t : {nonneg R}, toR (tilde_T_min f f' M m)%:nngnum <= t%:nngnum ->
toR M + toR (cd f) * t%:nngnum <= toR m + toR (cd f') * t%:nngnum.
{ move=> t'.
rewrite /tilde_T_min Hcd' Hcd => Ht'.
@@ -311,7 +311,7 @@ have HT_tilde_T : T f <= tilde_T_min f f' M m.
{ by rewrite leEsub /tilde_T_min !le_maxr lexx. }
have HT'_tilde_T : T f' <= tilde_T_min f f' M m.
{ by rewrite leEsub /tilde_T_min !le_maxr lexx orbT. }
-have Hf_le_f' : forall t : R+, toR (tilde_T_min f f' M m)%:nngnum <= t%:nngnum -> (f t <= f' t)%E.
+have Hf_le_f' : forall t : {nonneg R}, toR (tilde_T_min f f' M m)%:nngnum <= t%:nngnum -> (f t <= f' t)%E.
{ move=> t' Ht'.
refine (le_trans (HM _ _) _).
{ by move: Ht'; apply: le_trans; rewrite ler_rat -leEsub. }
@@ -337,7 +337,7 @@ Program Definition F_UPP_conv_f1_f1' (f f' : F_UPP) d11 c11 : F_UPP :=
c11
_.
Next Obligation.
-suff : forall t : R+, toR ((T f)%:nngnum + (T f')%:nngnum) <= t%:nngnum ->
+suff : forall t : {nonneg R}, toR ((T f)%:nngnum + (T f')%:nngnum) <= t%:nngnum ->
(f1 f * f1 f')%F t = +oo%E.
{ move=> H'; rewrite !H' //.
by apply: (le_trans H); rewrite -leEsub leEsub /= ler_addl. }
@@ -359,11 +359,11 @@ Program Definition F_UPP_conv_f1_f2' (f f' : F_UPP) : F_UPP :=
(c f')
_.
Next Obligation.
-have Hut : forall u : R+, u%:nngnum <= toR (T f)%:nngnum -> u <= t.
+have Hut : forall u : {nonneg R}, u%:nngnum <= toR (T f)%:nngnum -> u <= t.
{ move=> u /= Hu; rewrite leEsub /=.
move: H; apply/le_trans/(le_trans Hu).
by rewrite rmorphD /= ler_addl. }
-have Hutd' : forall u : R+, u%:nngnum <= toR (T f)%:nngnum ->
+have Hutd' : forall u : {nonneg R}, u%:nngnum <= toR (T f)%:nngnum ->
u%:nngnum <= t%:nngnum + toR (d f')%:num.
{ move=> u /= Hu.
move: (Hut _ Hu); rewrite leEsub /= => H'; apply: (le_trans H').
@@ -387,7 +387,7 @@ apply: (@eq_trans _ _ (ereal_inf
case: (leP u%:nngnum (toR (T f)%:nngnum)) => HuT; [by exists u|].
exists (toR (T f)%:nngnum)%:nng => //.
by rewrite /f1 ltxx ltNge ltW. }
-have Hf2 : forall u : R+, u%:nngnum <= toR (T f)%:nngnum ->
+have Hf2 : forall u : {nonneg R}, u%:nngnum <= toR (T f)%:nngnum ->
(f2 f' (insubd 0%:nng (t%:nngnum + toR (d f')%:num - u%:nngnum))%R
= f2 f' (insubd 0%:nng (t%:nngnum - u%:nngnum))%R + (toR (c f'))%:E)%dE.
{ move=> u Hu; rewrite /f2.
@@ -420,13 +420,13 @@ Qed.
Program Definition F_UPP_conv_f2_f2' (f f' : F_UPP) : F_UPP :=
Build_F_UPP
(f2 f * f2 f')
- ((T f)%:nngnum + (T f')%:nngnum + (lcm_posQ (d f) (d f'))%:num)%:nng
- (lcm_posQ (d f) (d f'))
- ((lcm_posQ (d f) (d f'))%:num * Order.min (cd f) (cd f'))
+ ((T f)%:nngnum + (T f')%:nngnum + (lcm_pos_rat (d f) (d f'))%:num)%:nng
+ (lcm_pos_rat (d f) (d f'))
+ ((lcm_pos_rat (d f) (d f'))%:num * Order.min (cd f) (cd f'))
_.
Next Obligation.
move: H; rewrite 2!rmorphD /= => H.
-have Hconv : forall t : R+,
+have Hconv : forall t : {nonneg R},
(f2 f * f2 f')%F t
= ereal_inf [set (f2 f u + f2 f' (insubd 0%:nng (t%:nngnum - u%:nngnum))%R)%dE
| u in [set u | toR (T f)%:nngnum <= u%:nngnum <= t%:nngnum - toR (T f')%:nngnum]].
@@ -446,7 +446,7 @@ have Hconv : forall t : R+,
move=> [u /= Hu <-]; exists u; split=> //=.
move: Hu => /andP[_]; rewrite ler_subr_addr leEsub /=; apply: le_trans.
by rewrite ler_addl. }
-have Hconv' : forall t : R+,
+have Hconv' : forall t : {nonneg R},
(f2 f * f2 f')%F t
= ereal_inf [set (f2 f (insubd 0%:nng (t%:nngnum - v%:nngnum))%R + f2 f' v)%dE
| v in [set v | toR (T f')%:nngnum <= v%:nngnum <= t%:nngnum - toR (T f)%:nngnum]].
@@ -469,7 +469,7 @@ have Hconv' : forall t : R+,
by rewrite daddeC. }
rewrite Hconv.
rewrite (@Rbar_inf_split_range
- (toR (T f)%:nngnum + toR (lcm_posQ (d f) (d f'))%:num)
+ (toR (T f)%:nngnum + toR (lcm_pos_rat (d f) (d f'))%:num)
(t%:nngnum - toR (T f')%:nngnum)); last first.
{ by rewrite -addrA ler_add2l ler_subr_addl subrr. }
{ by rewrite ler_subr_addl addrCA addrA. }
@@ -477,11 +477,11 @@ rewrite (@Rbar_inf_split_range
set inf1 := ereal_inf _.
set inf2 := ereal_inf _.
have -> : inf2
- = ereal_inf [set (f2 f (insubd 0%:nng (t%:nngnum + toR (lcm_posQ (d f) (d f'))%:num - v%:nngnum))%R + f2 f' v)%dE
+ = ereal_inf [set (f2 f (insubd 0%:nng (t%:nngnum + toR (lcm_pos_rat (d f) (d f'))%:num - v%:nngnum))%R + f2 f' v)%dE
| v in [set v | toR (T f')%:nngnum <= v%:nngnum <= t%:nngnum - toR (T f)%:nngnum]].
{ apply: f_equal; rewrite predeqP => x; split;
move=> [u /= /andP[Hu Hu'] <-];
- exists (insubd 0%:nng (t%:nngnum + toR (lcm_posQ (d f) (d f'))%:num - u%:nngnum)).
+ exists (insubd 0%:nng (t%:nngnum + toR (lcm_pos_rat (d f) (d f'))%:num - u%:nngnum)).
{ rewrite insubdK.
2:{ rewrite /in_mem /=.
by rewrite subr_ge0; apply: (le_trans Hu'); rewrite ger_addl oppr_le0. }
@@ -508,7 +508,7 @@ rewrite minr_rat (_ : (Order.min ?[a] ?[b])%:E = Order.min ?a%:E ?b%:E).
rewrite minC daddeC RbarDioid.mulDl; apply: f_equal2.
{ rewrite Hconv' RbarDioid.set_mulDl; apply: f_equal.
rewrite image_comp /comp; apply: eq_imagel => t' /andP[Ht' H't'].
- have P1 : t%:nngnum + toR (lcm_posQ (d f) (d f'))%:num - t'%:nngnum \in >= 0.
+ have P1 : t%:nngnum + toR (lcm_pos_rat (d f) (d f'))%:num - t'%:nngnum \in >= 0.
{ rewrite /in_mem /= subr_ge0.
apply: (le_trans H't'); rewrite ler_add2l.
by apply: (@le_trans _ _ 0); [rewrite oppr_le0|]. }
@@ -531,7 +531,7 @@ rewrite minC daddeC RbarDioid.mulDl; apply: f_equal2.
by rewrite Hk daddeC /cd mulrAC mulrA divrK //; apply: lt0r_neq0. }
rewrite Hconv RbarDioid.set_mulDl; apply: f_equal.
rewrite image_comp /comp; apply: eq_imagel => t' /andP[Ht' H't'].
-have P1 : ((t%:nngnum + toR (lcm_posQ (d f) (d f'))%:num)%:nng)%:nngnum
+have P1 : ((t%:nngnum + toR (lcm_pos_rat (d f) (d f'))%:num)%:nng)%:nngnum
- t'%:nngnum \in >= 0.
{ rewrite /in_mem /= subr_ge0.
apply: (le_trans H't'); rewrite ler_add2l.
@@ -590,21 +590,21 @@ Definition hypotheses_UPP_conv f f' M m :=
Definition tilde_T_conv f f' M m :=
(Order.max
- ((T f)%:nngnum + (T f')%:nngnum + (lcm_posQ (d f) (d f'))%:num)
+ ((T f)%:nngnum + (T f')%:nngnum + (lcm_pos_rat (d f) (d f'))%:num)
(if cd f == cd f' then 0%:nng
else if cd f < cd f' then
((insubd 0%:nng (M - m))%:nngnum / (insubd 0%:nng (cd f' - cd f))%:nngnum)%:nng
else (* cd f' < cd f *)
((insubd 0%:nng (M - m))%:nngnum / (insubd 0%:nng (cd f - cd f'))%:nngnum)%:nng)%:nngnum)%:nng.
-Definition tilde_d_conv f f' := lcm_posQ (d f) (d f').
+Definition tilde_d_conv f f' := lcm_pos_rat (d f) (d f').
Definition tilde_c_conv f f' :=
(tilde_d_conv f f')%:num * Order.min (cd f) (cd f').
Lemma tilde_T_convC f f' M m : tilde_T_conv f f' M m = tilde_T_conv f' f M m.
Proof.
-rewrite /tilde_T_conv eq_sym lcm_posQC.
+rewrite /tilde_T_conv eq_sym lcm_pos_ratC.
apply: f_equal2 => [].
{ by apply/val_inj; rewrite /= (addrC (T f)%:nngnum). }
case: eqP => [//|] /eqP Hcd.
@@ -613,12 +613,12 @@ by case: ltP.
Qed.
Lemma tilde_d_convC : commutative tilde_d_conv.
-Proof. by move=> f f'; rewrite /tilde_d_conv lcm_posQC. Qed.
+Proof. by move=> f f'; rewrite /tilde_d_conv lcm_pos_ratC. Qed.
Lemma tilde_c_convC : commutative tilde_c_conv.
Proof. by move=> f f'; rewrite /tilde_c_conv tilde_d_convC minC. Qed.
-Program Definition F_UPP_conv (f f' : F_UPP) (M m : Q) : _ -> F_UPP :=
+Program Definition F_UPP_conv (f f' : F_UPP) (M m : rat) : _ -> F_UPP :=
fun _ : (cd f = cd f'
\/ hypotheses_UPP_conv f f' M m \/ hypotheses_UPP_conv f' f M m) =>
Build_F_UPP
@@ -630,7 +630,7 @@ Next Obligation.
move: f f' M m H t H0.
suff : forall f f' M m,
(cd f = cd f' \/ hypotheses_UPP_conv f f' M m) ->
- forall t : R+,
+ forall t : {nonneg R},
toR (tilde_T_conv f f' M m)%:nngnum <= (t)%:nngnum ->
(f * f')%F ((t)%:nngnum + toR (tilde_d_conv f f')%:num)%:nng =
((f * f')%F t + (toR (tilde_c_conv f f'))%:E)%dE.
@@ -663,15 +663,15 @@ have Hdf1f2' : d f1f2' = d f'; [by []|].
have Hcf1f2' : c f1f2' = c f'; [by []|].
have Hcdf1f2' : cd f1f2' = cd f'; [by []|].
have HTf2f2' : T f2f2' = ((T f)%:nngnum + (T f')%:nngnum
- + (lcm_posQ (d f) (d f'))%:num)%:nng; [by []|].
-have Hdf2f2' : d f2f2' = lcm_posQ (d f) (d f'); [by []|].
+ + (lcm_pos_rat (d f) (d f'))%:num)%:nng; [by []|].
+have Hdf2f2' : d f2f2' = lcm_pos_rat (d f) (d f'); [by []|].
have Hcf2f2' : c f2f2' = (d f2f2')%:num * Order.min (cd f) (cd f'); [by []|].
have Hcdf2f2' : cd f2f2' = Order.min (cd f) (cd f').
-{ rewrite /cd /= -[lcm_posQ _ _]/(d f2f2') mulrC mulrA mulVr ?mul1r //.
+{ rewrite /cd /= -[lcm_pos_rat _ _]/(d f2f2') mulrC mulrA mulVr ?mul1r //.
exact: lt0r_neq0. }
have Hmax : Num.max ((T f)%:nngnum + (T f')%:nngnum)
- ((T f)%:nngnum + (T f')%:nngnum + (lcm_posQ (d f) (d f'))%:num)
- = (T f)%:nngnum + (T f')%:nngnum + (lcm_posQ (d f) (d f'))%:num.
+ ((T f)%:nngnum + (T f')%:nngnum + (lcm_pos_rat (d f) (d f'))%:num)
+ = (T f)%:nngnum + (T f')%:nngnum + (lcm_pos_rat (d f) (d f'))%:num.
{ by apply/max_idPr; rewrite ler_addl. }
move=> [Hcd|Hconv] t Ht.
{ have Hmin1 : cd f1f2' = cd f2f2'
@@ -680,15 +680,15 @@ move=> [Hcd|Hconv] t Ht.
{ by left; rewrite Hcdf1f2' Hcdf2f2' -Hcd minxx. }
rewrite -[F_min f1f2' f2f2']/(F_UPP_min Hmin1 : F).
have HTmin1 : T (F_UPP_min Hmin1)
- = ((T f)%:nngnum + (T f')%:nngnum + (lcm_posQ (d f) (d f'))%:num)%:nng.
+ = ((T f)%:nngnum + (T f')%:nngnum + (lcm_pos_rat (d f) (d f'))%:num)%:nng.
{ rewrite /T /= /tilde_T_min Hcdf1f2' Hcdf2f2' -Hcd minxx eqxx.
by apply: val_inj; rewrite /= maxEge max_ge0. }
- have Hdmin1 : d (F_UPP_min Hmin1) = lcm_posQ (d f) (d f').
+ have Hdmin1 : d (F_UPP_min Hmin1) = lcm_pos_rat (d f) (d f').
{ rewrite /d /= /tilde_d_min Hcdf1f2' Hcdf2f2' Hcd minxx eqxx.
- by rewrite Hdf1f2' Hdf2f2' lcm_posQC -lcm_posQA lcm_posQ_xx. }
- have Hcmin1 : c (F_UPP_min Hmin1) = (lcm_posQ (d f) (d f'))%:num * cd f.
+ by rewrite Hdf1f2' Hdf2f2' lcm_pos_ratC -lcm_pos_ratA lcm_pos_rat_xx. }
+ have Hcmin1 : c (F_UPP_min Hmin1) = (lcm_pos_rat (d f) (d f'))%:num * cd f.
{ rewrite /c /= /tilde_c_min Hcdf1f2' Hcdf2f2' Hcd minxx eqxx.
- by rewrite Hdf1f2' Hdf2f2' lcm_posQC -lcm_posQA lcm_posQ_xx. }
+ by rewrite Hdf1f2' Hdf2f2' lcm_pos_ratC -lcm_pos_ratA lcm_pos_rat_xx. }
have Hcdmin1 : cd (F_UPP_min Hmin1) = cd f.
{ rewrite /cd Hcmin1 Hdmin1.
rewrite mulrC mulrA mulVr ?mul1r //; exact: lt0r_neq0. }
@@ -697,15 +697,15 @@ move=> [Hcd|Hconv] t Ht.
\/ hypotheses_UPP_min (F_UPP_min Hmin1) f1'f2 M m.
{ by left; rewrite Hcdmin1. }
rewrite -[F_min f1'f2 _]/(F_UPP_min Hmin2 : F).
- have HTmin2 : T (F_UPP_min Hmin2) = ((T f)%:nngnum + (T f')%:nngnum + (lcm_posQ (d f) (d f'))%:num)%:nng.
+ have HTmin2 : T (F_UPP_min Hmin2) = ((T f)%:nngnum + (T f')%:nngnum + (lcm_pos_rat (d f) (d f'))%:num)%:nng.
{ rewrite /T /= /tilde_T_min Hcdf1'f2 Hcdmin1 eqxx.
by rewrite HTf1'f2 HTmin1; apply/val_inj; rewrite /= maxEge ifT ?Hmax. }
- have Hdmin2 : d (F_UPP_min Hmin2) = lcm_posQ (d f) (d f').
+ have Hdmin2 : d (F_UPP_min Hmin2) = lcm_pos_rat (d f) (d f').
{ rewrite /d /= /tilde_d_min Hcdf1'f2 Hcdmin1 eqxx.
- by rewrite Hdf1'f2 Hdmin1 lcm_posQA lcm_posQ_xx. }
- have Hcmin2 : c (F_UPP_min Hmin2) = (lcm_posQ (d f) (d f'))%:num * cd f.
+ by rewrite Hdf1'f2 Hdmin1 lcm_pos_ratA lcm_pos_rat_xx. }
+ have Hcmin2 : c (F_UPP_min Hmin2) = (lcm_pos_rat (d f) (d f'))%:num * cd f.
{ rewrite /c /= /tilde_c_min Hcdf1'f2 Hcdmin1 eqxx.
- by rewrite Hdf1'f2 Hdmin1 lcm_posQA lcm_posQ_xx. }
+ by rewrite Hdf1'f2 Hdmin1 lcm_pos_ratA lcm_pos_rat_xx. }
have Hcdmin2 : cd (F_UPP_min Hmin2) = cd f.
{ rewrite /cd Hcmin2 Hdmin2.
rewrite mulrC mulrA mulVr ?mul1r //; exact: lt0r_neq0. }
@@ -714,15 +714,15 @@ move=> [Hcd|Hconv] t Ht.
\/ hypotheses_UPP_min (F_UPP_min Hmin2) f1f1' M m.
{ by left; rewrite Hcdf1f1' Hcdmin2. }
rewrite -[F_min _ _]/(F_UPP_min Hmin3 : F).
- have HTmin3 : T (F_UPP_min Hmin3) = ((T f)%:nngnum + (T f')%:nngnum + (lcm_posQ (d f) (d f'))%:num)%:nng.
+ have HTmin3 : T (F_UPP_min Hmin3) = ((T f)%:nngnum + (T f')%:nngnum + (lcm_pos_rat (d f) (d f'))%:num)%:nng.
{ rewrite /T /= /tilde_T_min Hcdf1f1' Hcdmin2 eqxx.
by rewrite HTf1f1' HTmin2; apply/val_inj; rewrite /= maxEge ifT ?Hmax. }
- have Hdmin3 : d (F_UPP_min Hmin3) = lcm_posQ (d f) (d f').
+ have Hdmin3 : d (F_UPP_min Hmin3) = lcm_pos_rat (d f) (d f').
{ rewrite /d /= /tilde_d_min Hcdf1f1' Hcdmin2 eqxx.
- by rewrite Hdf1f1' Hdmin2 lcm_posQA lcm_posQ_xx. }
- have Hcmin3 : c (F_UPP_min Hmin3) = (lcm_posQ (d f) (d f'))%:num * cd f.
+ by rewrite Hdf1f1' Hdmin2 lcm_pos_ratA lcm_pos_rat_xx. }
+ have Hcmin3 : c (F_UPP_min Hmin3) = (lcm_pos_rat (d f) (d f'))%:num * cd f.
{ rewrite /c /= /tilde_c_min Hcdf1f1' Hcdmin2 eqxx.
- by rewrite Hdf1f1' Hdmin2 lcm_posQA lcm_posQ_xx. }
+ by rewrite Hdf1f1' Hdmin2 lcm_pos_ratA lcm_pos_rat_xx. }
have Hcdmin3 : cd (F_UPP_min Hmin3) = cd f.
{ rewrite /cd Hcmin3 Hdmin3.
rewrite mulrC mulrA mulVr ?mul1r //; exact: lt0r_neq0. }
@@ -740,9 +740,9 @@ have PT : 0 <= toR (T f)%:nngnum; [by []|].
have PT' : 0 <= toR (T f')%:nngnum; [by []|].
have Pd : 0 < (d f)%:num; [by []|].
have Pd' : 0 < (d f')%:num; [by []|].
-have HMf2f2' : forall t : R+,
- toR (T f)%:nngnum + toR (T f')%:nngnum + toR (lcm_posQ (d f) (d f'))%:num <= t%:nngnum
- < toR (T f)%:nngnum + toR (T f')%:nngnum + toR (lcm_posQ (d f) (d f'))%:num + toR (lcm_posQ (d f) (d f'))%:num ->
+have HMf2f2' : forall t : {nonneg R},
+ toR (T f)%:nngnum + toR (T f')%:nngnum + toR (lcm_pos_rat (d f) (d f'))%:num <= t%:nngnum
+ < toR (T f)%:nngnum + toR (T f')%:nngnum + toR (lcm_pos_rat (d f) (d f'))%:num + toR (lcm_pos_rat (d f) (d f'))%:num ->
((f2 f * f2 f')%F t <= (toR M + toR (cd f) * t%:nngnum)%R%:E)%dE.
{ move=> t' /andP[Ht' H'T'].
have Ht'mT' : (insubd 0%:nng (t'%:nngnum - toR (T f')%:nngnum))%:nngnum
@@ -778,7 +778,7 @@ have HMf2f2' : forall t : R+,
rewrite mulrN opprK mulrC !rmorphM /=.
rewrite mulrAC -mulrA -(mulrA (toR (c f))).
by rewrite -rmorphM mulVf /= ?rmorph1 ?mulr1. }
-have Hmf1f2' : forall t : R+,
+have Hmf1f2' : forall t : {nonneg R},
toR (T f)%:nngnum + toR (T f')%:nngnum <= t%:nngnum
< toR (T f)%:nngnum + toR (T f')%:nngnum + toR (d f')%:num ->
((toR m + toR (cd f') * t%:nngnum)%R%:E <= (f1 f * f2 f')%F t)%dE.
@@ -821,14 +821,14 @@ have Hmin1 : cd f1f2' = cd f2f2'
exact: Hmf1f2'. }
rewrite -[F_min f1f2' f2f2']/(F_UPP_min Hmin1 : F).
have HTmin1 : T (F_UPP_min Hmin1)
- = (Order.max ((T f)%:nngnum + (T f')%:nngnum + (lcm_posQ (d f) (d f'))%:num)
+ = (Order.max ((T f)%:nngnum + (T f')%:nngnum + (lcm_pos_rat (d f) (d f'))%:num)
((insubd 0%:nng (M - m))%:nngnum / (insubd 0%:nng (cd f' - cd f))%:nngnum))%:nng.
{ apply/val_inj; rewrite /= Hmax; apply: f_equal.
by rewrite Hcdf1f2' Hcdf2f2' minEle Hcd_le Hcd_neq ltNge Hcd_le. }
-have Hdmin1 : d (F_UPP_min Hmin1) = lcm_posQ (d f) (d f').
+have Hdmin1 : d (F_UPP_min Hmin1) = lcm_pos_rat (d f) (d f').
{ rewrite /d /= /tilde_d_min Hcdf1f2' Hcdf2f2'.
by rewrite minElt Hcd Hcd_neq ltNge Hcd_le. }
-have Hcmin1 : c (F_UPP_min Hmin1) = (lcm_posQ (d f) (d f'))%:num * cd f.
+have Hcmin1 : c (F_UPP_min Hmin1) = (lcm_pos_rat (d f) (d f'))%:num * cd f.
{ rewrite /c /= /tilde_c_min Hcdf1f2' Hcdf2f2'.
by rewrite minElt Hcd Hcd_neq ltNge Hcd_le /= minElt Hcd. }
have Hcdmin1 : cd (F_UPP_min Hmin1) = cd f.
@@ -840,18 +840,18 @@ have Hmin2 : cd f1'f2 = cd (F_UPP_min Hmin1)
{ by left; rewrite Hcdmin1. }
rewrite -[F_min f1'f2 _]/(F_UPP_min Hmin2 : F).
have HTmin2 : T (F_UPP_min Hmin2)
- = (Order.max ((T f)%:nngnum + (T f')%:nngnum + (lcm_posQ (d f) (d f'))%:num)
+ = (Order.max ((T f)%:nngnum + (T f')%:nngnum + (lcm_pos_rat (d f) (d f'))%:num)
((insubd 0%:nng (M - m))%:nngnum / (insubd 0%:nng (cd f' - cd f))%:nngnum))%:nng.
{ apply/val_inj; rewrite /= Hmax maxA (addrC (T f')%:nngnum) Hmax -maxA.
apply: f_equal.
rewrite Hcdf1f2' Hcdf2f2' minEle Hcd_le Hcd_neq ltNge Hcd_le /=.
by rewrite Hcdf1'f2 Hcdmin1 eqxx maxEge /= ifT. }
-have Hdmin2 : d (F_UPP_min Hmin2) = lcm_posQ (d f) (d f').
+have Hdmin2 : d (F_UPP_min Hmin2) = lcm_pos_rat (d f) (d f').
{ rewrite /d /= /tilde_d_min Hcdf1'f2 Hcdmin1 eqxx.
- by rewrite Hdf1'f2 Hdmin1 lcm_posQA lcm_posQ_xx. }
-have Hcmin2 : c (F_UPP_min Hmin2) = (lcm_posQ (d f) (d f'))%:num * cd f.
+ by rewrite Hdf1'f2 Hdmin1 lcm_pos_ratA lcm_pos_rat_xx. }
+have Hcmin2 : c (F_UPP_min Hmin2) = (lcm_pos_rat (d f) (d f'))%:num * cd f.
{ rewrite /c /= /tilde_c_min Hcdf1'f2 Hcdmin1 eqxx.
- by rewrite Hdf1'f2 Hdmin1 lcm_posQA lcm_posQ_xx. }
+ by rewrite Hdf1'f2 Hdmin1 lcm_pos_ratA lcm_pos_rat_xx. }
have Hcdmin2 : cd (F_UPP_min Hmin2) = cd f.
{ rewrite /cd Hcmin2 Hdmin2.
rewrite mulrC mulrA mulVr ?mul1r //; exact: lt0r_neq0. }
@@ -861,18 +861,18 @@ have Hmin3 : cd f1f1' = cd (F_UPP_min Hmin2)
{ by left; rewrite Hcdf1f1' Hcdmin2. }
rewrite -[F_min _ _]/(F_UPP_min Hmin3 : F).
have HTmin3 : T (F_UPP_min Hmin3)
- = (Order.max ((T f)%:nngnum + (T f')%:nngnum + (lcm_posQ (d f) (d f'))%:num)
+ = (Order.max ((T f)%:nngnum + (T f')%:nngnum + (lcm_pos_rat (d f) (d f'))%:num)
((insubd 0%:nng (M - m))%:nngnum / (insubd 0%:nng (cd f' - cd f))%:nngnum))%:nng.
{ apply/val_inj; rewrite /= Hmax (addrC (T f')%:nngnum) !maxA.
rewrite maxxx Hmax -!maxA; apply: f_equal.
rewrite Hcdf1f2' Hcdf2f2' minElt Hcd Hcd_neq ltNge Hcd_le /=.
by rewrite Hcdf1'f2 Hcdmin1 eqxx Hcdf1f1' Hcdmin2 eqxx /= maxxx maxEge ifT. }
-have Hdmin3 : d (F_UPP_min Hmin3) = lcm_posQ (d f) (d f').
+have Hdmin3 : d (F_UPP_min Hmin3) = lcm_pos_rat (d f) (d f').
{ rewrite /d /= /tilde_d_min Hcdf1f1' Hcdmin2 eqxx.
- by rewrite Hdf1f1' Hdmin2 lcm_posQA lcm_posQ_xx. }
-have Hcmin3 : c (F_UPP_min Hmin3) = (lcm_posQ (d f) (d f'))%:num * cd f.
+ by rewrite Hdf1f1' Hdmin2 lcm_pos_ratA lcm_pos_rat_xx. }
+have Hcmin3 : c (F_UPP_min Hmin3) = (lcm_pos_rat (d f) (d f'))%:num * cd f.
{ rewrite /c /= /tilde_c_min Hcdf1f1' Hcdmin2 eqxx.
- by rewrite Hdf1f1' Hdmin2 lcm_posQA lcm_posQ_xx. }
+ by rewrite Hdf1f1' Hdmin2 lcm_pos_ratA lcm_pos_rat_xx. }
have Hcdmin3 : cd (F_UPP_min Hmin3) = cd f.
{ rewrite /cd Hcmin3 Hdmin3.
rewrite mulrC mulrA mulVr ?mul1r //; exact: posnum_neq0. }
@@ -886,11 +886,11 @@ rewrite -[F_UPP_c _]/(c (F_UPP_min Hmin3)) Hcmin3.
by rewrite /tilde_c_conv minElt Hcd.
Qed.
-Program Definition UPP_change_d_c (f : F_UPP) (d : Q+*) (c : Q)
- (H : (forall t : R+, toR (F_UPP_T f)%:nngnum <= t%:nngnum
+Program Definition UPP_change_d_c (f : F_UPP) (d : {posnum rat}) (c : rat)
+ (H : (forall t : {nonneg R}, toR (F_UPP_T f)%:nngnum <= t%:nngnum
< toR ((F_UPP_T f)%:nngnum + (F_UPP_d f)%:num) ->
f t = +oo%E)
- \/ (forall t : R+, toR (F_UPP_T f)%:nngnum <= t%:nngnum
+ \/ (forall t : {nonneg R}, toR (F_UPP_T f)%:nngnum <= t%:nngnum
< toR ((F_UPP_T f)%:nngnum + (F_UPP_d f)%:num) ->
f t = -oo%E)) : F_UPP :=
Build_F_UPP
@@ -921,7 +921,7 @@ Qed.
Lemma UPP_same_d_c_equality (f f' : F_UPP) :
F_UPP_d f = F_UPP_d f' -> F_UPP_c f = F_UPP_c f' ->
let l := Order.max (F_UPP_T f)%:nngnum (F_UPP_T f')%:nngnum + (F_UPP_d f)%:num in
- (forall t : R+, t%:nngnum < toR l -> f t = f' t) ->
+ (forall t : {nonneg R}, t%:nngnum < toR l -> f t = f' t) ->
forall t, f t = f' t.
Proof.
set theta := Order.max _ _.
@@ -957,8 +957,8 @@ Qed.
Lemma UPP_equality (f f' : F_UPP) :
F_UPP_c f / (F_UPP_d f)%:num = F_UPP_c f' / (F_UPP_d f')%:num ->
let l := Order.max (F_UPP_T f)%:nngnum (F_UPP_T f')%:nngnum
- + (lcm_posQ (F_UPP_d f) (F_UPP_d f'))%:num in
- (forall t : R+, t%:nngnum < toR l -> f t = f' t) ->
+ + (lcm_pos_rat (F_UPP_d f) (F_UPP_d f'))%:num in
+ (forall t : {nonneg R}, t%:nngnum < toR l -> f t = f' t) ->
forall t, f t = f' t.
Proof.
set theta := Order.max _ _.
diff --git a/minerve/UPP_PA.v b/minerve/UPP_PA.v
index 4324e4f2..2d0677d6 100644
--- a/minerve/UPP_PA.v
+++ b/minerve/UPP_PA.v
@@ -29,7 +29,7 @@ Lemma F_UPP_PA_prop (f : F_UPP_PA) :
JS_of (F_UPP_PA_JS f) f ((F_UPP_T f)%:nngnum + (F_UPP_d f)%:num)%:nng.
Proof. by case: f. Qed.
-Program Definition F_UPP_PA_of_JS (a : JS) (T : Q+) (d : Q+*) (c : Q)
+Program Definition F_UPP_PA_of_JS (a : JS) (T : {nonneg rat}) (d : {posnum rat}) (c : rat)
(H : (last_JS a).1%:nngnum < T%:nngnum + d%:num) : F_UPP_PA :=
Build_F_UPP_PA (F_UPP_of_F (F_of_JS a) T d c) a _.
Next Obligation.
@@ -39,7 +39,7 @@ apply: (@JS_of_eq _ (F_of_JS a)).
exact: F_of_JS_correct.
Qed.
-Lemma eq_point_UPP (f : F_UPP) (x : Q+) (y : \bar Q) :
+Lemma eq_point_UPP (f : F_UPP) (x : {nonneg rat}) (y : \bar rat) :
F_UPP_T f <= x -> eq_point f x y ->
eq_point f (x%:nngnum + (F_UPP_d f)%:num)%:nng (y + (F_UPP_c f)%:E)%dE.
Proof.
@@ -54,7 +54,7 @@ case: y => /= [y| |] H.
by rewrite Hxpd F_UPP_prop /= ?ler_rat // H.
Qed.
-Lemma eq_point_UPP_n (f : F_UPP) (x : Q+) (y : \bar Q) (n : nat) :
+Lemma eq_point_UPP_n (f : F_UPP) (x : {nonneg rat}) (y : \bar rat) (n : nat) :
F_UPP_T f <= x -> eq_point f x y ->
eq_point
f (x%:nngnum + n%:R * (F_UPP_d f)%:num)%:nng
@@ -77,25 +77,25 @@ apply: eq_point_UPP.
exact: IH.
Qed.
-Lemma affine_on_UPP (f : F_UPP) rs (x y : Q+) :
+Lemma affine_on_UPP (f : F_UPP) rs (x y : {nonneg rat}) :
F_UPP_T f <= x -> affine_on f rs x y ->
affine_on
f (rs.1, (rs.2 + (F_UPP_c f)%:E)%dE)
(x%:nngnum + (F_UPP_d f)%:num)%:nng (y%:nngnum + (F_UPP_d f)%:num)%:nng.
Proof.
move=> Hx.
-have Ht' : forall t : R+,
+have Ht' : forall t : {nonneg R},
toR (x%:nngnum + (F_UPP_d f)%:num) < t%:nngnum ->
toR (F_UPP_T f)%:nngnum <= t%:nngnum - toR (F_UPP_d f)%:num.
{ move=> t Ht.
rewrite ler_subr_addr; move: (ltW Ht); apply: le_trans.
by rewrite rmorphD /= ler_add2r ler_rat -leEsub. }
-have Ht'' : forall t : R+,
+have Ht'' : forall t : {nonneg R},
toR (x%:nngnum + (F_UPP_d f)%:num) < t%:nngnum ->
0 <= t%:nngnum - toR (F_UPP_d f)%:num.
{ move=> t Ht.
by move: (Ht' t Ht); apply: le_trans. }
-have Htmd : forall t : R+,
+have Htmd : forall t : {nonneg R},
toR (x%:nngnum + (F_UPP_d f)%:num) < t%:nngnum ->
t = ((insubd 0%:nng (t%:nngnum - toR (F_UPP_d f)%:num))%:nngnum
+ toR (F_UPP_d f)%:num)%:nng.
@@ -120,7 +120,7 @@ apply/f_equal/f_equal.
by rewrite /= insubdK // rmorphD /= opprD addrA subrK addrAC.
Qed.
-Lemma affine_on_UPP_n (f : F_UPP) rs (x y : Q+) (n : nat) :
+Lemma affine_on_UPP_n (f : F_UPP) rs (x y : {nonneg rat}) (n : nat) :
F_UPP_T f <= x -> affine_on f rs x y ->
affine_on
f (rs.1, (rs.2 + (n%:R * F_UPP_c f)%R%:E)%dE)
@@ -152,7 +152,7 @@ apply: affine_on_UPP.
exact: IH.
Qed.
-Definition shift_period (a : seq JS_elem) (d : Q+*) (c : Q) (n : nat) :=
+Definition shift_period (a : seq JS_elem) (d : {posnum rat}) (c : rat) (n : nat) :=
let shift xyrs :=
let x := (xyrs.1%:nngnum + n%:R * d%:num)%:nng in
let y := (xyrs.2.1 + (n%:R * c)%R%:E)%dE in
@@ -190,7 +190,7 @@ apply: IH => //.
move: Hxx' => /ltW; exact: le_trans.
Qed.
-Definition F_UPP_PA_JS_upto_def (f : F_UPP_PA) (l : Q+*) :=
+Definition F_UPP_PA_JS_upto_def (f : F_UPP_PA) (l : {posnum rat}) :=
let suf := JS_above (F_UPP_PA_JS f) (F_UPP_T f) in
let fix aux (n n' : nat) :=
match n with
@@ -201,7 +201,7 @@ Definition F_UPP_PA_JS_upto_def (f : F_UPP_PA) (l : Q+*) :=
/ (F_UPP_d f)%:num)) in
F_UPP_PA_JS f ++ aux n 1%nat.
-Program Definition F_UPP_PA_JS_upto_def' f (l : Q+*) :=
+Program Definition F_UPP_PA_JS_upto_def' f (l : {posnum rat}) :=
JS_below (Build_JS (F_UPP_PA_JS_upto_def f l) _ _ _) l.
Next Obligation. by rewrite /F_UPP_PA_JS_upto_def JS_head_behead. Qed.
Next Obligation. by rewrite /F_UPP_PA_JS_upto_def JS_head_behead JS_head. Qed.
@@ -229,7 +229,7 @@ apply/andP; split.
case: (JS_above _ _ : seq _) => [//|h t] /= ->.
rewrite Hl' /= /shift_period.
set shift := fun x => _.
- pose def := (F_UPP_T f, (+oo%E : \bar Q, (0 : Q, +oo%E : \bar Q))).
+ pose def := (F_UPP_T f, (+oo%E : \bar rat, (0 : rat, +oo%E : \bar rat))).
rewrite -{1}[F_UPP_T f]/def.1 path_map.
rewrite -[(_ + _)%:nng]/(shift def).1.
rewrite !path_map; apply: sub_path => x y /= Hxy.
@@ -307,7 +307,7 @@ Definition is_ultimately_affine (f : F_UPP_PA) : bool :=
Lemma is_ultimately_affine_correct f :
is_ultimately_affine f ->
let: (x, (_, (r, s))) := last_JS (F_UPP_PA_JS f) in
- forall t : R+, toR (F_UPP_T f)%:nngnum <= t%:nngnum ->
+ forall t : {nonneg R}, toR (F_UPP_T f)%:nngnum <= t%:nngnum ->
(f t = (toR r * (t%:nngnum - toR x%:nngnum))%:E + er_map toR s)%dE.
Proof.
have PTf : 0 <= toR (F_UPP_T f)%:nngnum; [by []|].
@@ -355,7 +355,7 @@ case: (F_UPP_PA_JS f) JS_f => [a + + a_sorted].
rewrite /JS_seq !(JS_of_JS_of' _ _ a_sorted).
case: a a_sorted => [//|[x [y [r s]]] a /=] + _ _.
have Hlast: forall x r s,
- (forall t : R+, toR (F_UPP_T f)%:nngnum <= t%:nngnum ->
+ (forall t : {nonneg R}, toR (F_UPP_T f)%:nngnum <= t%:nngnum ->
f t
= ((toR r * (t%:nngnum - toR x%:nngnum))%:E
+ er_map toR s)%dE) ->
@@ -406,7 +406,7 @@ Proof. by []. Qed.
Program Definition F_UPP_PA_add (f f' : F_UPP_PA) : F_UPP_PA :=
let l :=
@PosNum _ ((Order.max (F_UPP_T f)%:nngnum (F_UPP_T f')%:nngnum)
- + (lcm_posQ (F_UPP_d f) (F_UPP_d f'))%:num) _ in
+ + (lcm_pos_rat (F_UPP_d f) (F_UPP_d f'))%:num) _ in
Build_F_UPP_PA
(F_UPP_add f f')
(JS_add (F_UPP_PA_JS_upto f l) (F_UPP_PA_JS_upto f' l))
@@ -443,7 +443,7 @@ have Hfmcd : JS_of JSfmcd ffmcd ((T f)%:nngnum + (d f)%:num)%:nng.
by rewrite /ffmcd /F_plus /=; case: (f t). }
apply: JS_add_correct.
{ exact: F_UPP_PA_prop. }
- have -> : (fun t : R+ => (- (toR (cd f) * t%:nngnum))%:E)
+ have -> : (fun t : {nonneg R} => (- (toR (cd f) * t%:nngnum))%:E)
= (fun t => (toR (- (cd f)) * t%:nngnum + toR 0)%:E).
{ apply/funext => t; apply: f_equal.
by rewrite toR0 addr0 rmorphN /= mulNr. }
@@ -458,7 +458,7 @@ have Hfmcd' : JS_of JSfmcd' ffmcd' ((T f')%:nngnum + (d f')%:num)%:nng.
by rewrite /ffmcd' /F_plus /=; case: (f' t). }
apply: JS_add_correct.
{ exact: F_UPP_PA_prop. }
- have -> : (fun t : R+ => (- (toR (cd f') * t%:nngnum))%:E)
+ have -> : (fun t : {nonneg R} => (- (toR (cd f') * t%:nngnum))%:E)
= (fun t => (toR (- (cd f')) * t%:nngnum + toR 0)%:E).
{ apply/funext => t; apply: f_equal.
by rewrite toR0 addr0 rmorphN /= mulNr. }
@@ -602,7 +602,7 @@ have Hfmcd : JS_of JSfmcd ffmcd ((T f)%:nngnum + (d f)%:num)%:nng.
by rewrite /ffmcd /F_plus /=; case: (f t). }
apply: JS_add_correct.
{ exact: F_UPP_PA_prop. }
- have -> : (fun t : R+ => (- (toR (cd f) * (t%:nngnum + toR (T f')%:nngnum)))%:E)
+ have -> : (fun t : {nonneg R} => (- (toR (cd f) * (t%:nngnum + toR (T f')%:nngnum)))%:E)
= (fun t => (toR (- (cd f)) * t%:nngnum + toR (- (cd f) * (T f')%:nngnum))%:E).
{ apply/funext => t; apply: f_equal.
by rewrite [in RHS]rmorphM /= -mulrDr rmorphN /= mulNr. }
@@ -617,7 +617,7 @@ have Hfmcd'' : JS_of JSfmcd'' ffmcd'' ((T f')%:nngnum + (d f')%:num)%:nng.
by rewrite /ffmcd'' /F_plus /=; case: (f' t). }
apply: JS_add_correct.
{ exact: F_UPP_PA_prop. }
- have -> : (fun t : R+ => (- (toR (cd f') * t%:nngnum))%:E)
+ have -> : (fun t : {nonneg R} => (- (toR (cd f') * t%:nngnum))%:E)
= (fun t => (toR (- (cd f')) * t%:nngnum + toR 0)%:E).
{ apply/funext => t; apply: f_equal.
by rewrite toR0 addr0 rmorphN /= mulNr. }
@@ -643,7 +643,7 @@ split=> [//|]; split.
by rewrite ltEsub /= ltr_addl. }
rewrite -[(toR m)%:E]/(er_map toR m%:E) -Hm.
case: eqP => [|/eqP] HT.
-{ have -> : [set t : R+ | t%:nngnum < toR (T f)%:nngnum] = set0.
+{ have -> : [set t : {nonneg R} | t%:nngnum < toR (T f)%:nngnum] = set0.
{ rewrite predeqP => t; split=> [/= | //].
by rewrite HT rmorph0 nngnum_lt0. }
rewrite (_ : [set _ | t in set0] = set0); last first.
@@ -658,7 +658,7 @@ have Hfmcd' : JS_of JSfmcd' ffmcd' (T f)%:nngnum%:nng.
apply: JS_add_correct.
{ rewrite HT'; apply: JS_below_spec (F_UPP_PA_prop f).
by rewrite insubdK ?ler_addl // /in_mem /= lt_def HT /=. }
- have -> : (fun t : R+ => (- (toR (cd f') * t%:nngnum))%:E)
+ have -> : (fun t : {nonneg R} => (- (toR (cd f') * t%:nngnum))%:E)
= (fun t => (toR (- (cd f')) * t%:nngnum + toR 0)%:E).
{ apply/funext => t; apply: f_equal.
by rewrite toR0 addr0 rmorphN /= mulNr. }
@@ -777,7 +777,7 @@ case: (JS_below _ _) last_bf JS_bf => [a + + a_sorted].
rewrite /JS_seq !(JS_of_JS_of' _ _ a_sorted).
case: a a_sorted => [//|[x [y [r s]]] a /=] + _ _.
move=> pa xltTmdd0 [fx Ha]; split=> [//|].
-have Hlast : forall x (y : \bar Q) r s,
+have Hlast : forall x (y : \bar rat) r s,
x < ((T f)%:nngnum + Num.min (F_UPP_d f)%:num d0%:num)%:nng ->
affine_on f (r, s) x ((T f)%:nngnum + Num.min (F_UPP_d f)%:num d0%:num)%:nng ->
affine_on f (r, s) x ((T f)%:nngnum + d0%:num)%:nng.
@@ -840,10 +840,10 @@ Definition is_infinite_on_period (f : F_UPP_PA) : bool :=
Lemma is_infinite_on_period_correct f :
is_infinite_on_period f ->
- ((forall t : R+, toR (F_UPP_T f)%:nngnum <= t%:nngnum
+ ((forall t : {nonneg R}, toR (F_UPP_T f)%:nngnum <= t%:nngnum
< toR ((F_UPP_T f)%:nngnum + (F_UPP_d f)%:num) ->
f t = +oo%E)
- \/ (forall t : R+, toR (F_UPP_T f)%:nngnum <= t%:nngnum
+ \/ (forall t : {nonneg R}, toR (F_UPP_T f)%:nngnum <= t%:nngnum
< toR ((F_UPP_T f)%:nngnum + (F_UPP_d f)%:num) ->
f t = -oo%E)).
Proof.
@@ -922,7 +922,7 @@ Program Definition F_UPP_PA_eqb (f f' : F_UPP_PA) : bool :=
(cd f == cd f')
&& let l :=
@PosNum _ ((Order.max (F_UPP_T f)%:nngnum (F_UPP_T f')%:nngnum)
- + (lcm_posQ (F_UPP_d f) (F_UPP_d f'))%:num) _ in
+ + (lcm_pos_rat (F_UPP_d f) (F_UPP_d f'))%:num) _ in
JS_eqb (F_UPP_PA_JS_upto f l) (F_UPP_PA_JS_upto f' l).
Next Obligation. exact: ltr_paddl. Qed.
@@ -963,7 +963,7 @@ move: E => /F_UPP_PA_min'_correct -> ->.
by apply/leFP => t; rewrite /F_min le_minl lexx orbT.
Qed.
-Program Definition F_UPP_PA_0 (d' : Q+*) :=
+Program Definition F_UPP_PA_0 (d' : {posnum rat}) :=
@F_UPP_PA_of_JS JS_0 0%:nng d' 0 _.
Next Obligation. by rewrite ltr_addl. Qed.
@@ -976,7 +976,7 @@ case: ltP => Ht; rewrite /F_of_JS /=.
by case: leP => _; rewrite rmorph0 !dadde0 // mul0r.
Qed.
-Program Definition F_UPP_PA_delta (d : Q) (d' : Q+*) :=
+Program Definition F_UPP_PA_delta (d : rat) (d' : {posnum rat}) :=
let nngd := insubd 0%:nng d in
let js :=
if d < 0 then [:: (0%:nng, (+oo%E, (0, +oo%E)))]
@@ -1063,7 +1063,7 @@ rewrite !(F_UPP_PA_opp_correct, E) F_UPP_PA_0_correct.
by rewrite non_decr_closure_F_min_conv_F_0.
Qed.
-Definition F_UPP_PA_hDev_bounded (f f' : F_UPP_PA) (d : \bar Q) :=
+Definition F_UPP_PA_hDev_bounded (f f' : F_UPP_PA) (d : \bar rat) :=
match d with
| +oo%E => true | -oo%E => false
| d%:E =>
@@ -1181,7 +1181,7 @@ apply: JS_max_val_correct.
by rewrite JS_head /= rmorph0 insubdK // Pt'.
Qed.
-Definition F_UPP_PA_vDev_bounded (f f' : F_UPP_PA) (b : \bar Q) :=
+Definition F_UPP_PA_vDev_bounded (f f' : F_UPP_PA) (b : \bar rat) :=
F_UPP_PA_never_ninfty f && F_UPP_PA_never_pinfty f'
&& F_UPP_PA_leb f (F_UPP_PA_add_cst b f').
diff --git a/minerve/UPP_PA_refinement.v b/minerve/UPP_PA_refinement.v
index 2307aee9..b2b545d5 100644
--- a/minerve/UPP_PA_refinement.v
+++ b/minerve/UPP_PA_refinement.v
@@ -378,7 +378,7 @@ Local Instance ceil_rat : ceil_of rat :=
fun x => ssrint.absz (mathcomp_complements.ceilq x).
Local Existing Instance max_rat.
Local Existing Instance min_rat.
-Local Instance lcm_rat : lcm_of rat := lcm_Q.
+Local Instance lcm_rat : lcm_of rat := lcm_rat.
Local Existing Instance eq_rat.
Local Existing Instance lt_rat.
Local Existing Instance le_rat.
@@ -841,9 +841,9 @@ case: eqP => Hcd.
by rewrite refinesE /rposQ /= Hcd eqxx max_l //= /tilde_d_conv unlock. }
by rewrite refinesE /rposQ /= Hcd eqxx max_l //= /tilde_d_conv unlock. }
have PT : (0 <= (F_UPP_T f)%:nngnum + (F_UPP_T f')%:nngnum
- + lcm_Q (F_UPP_d f)%:num (F_UPP_d f')%:num)%R.
+ + lcm_rat (F_UPP_d f)%:num (F_UPP_d f')%:num)%R.
{ apply: addr_ge0 => //.
- rewrite (_ : lcm_Q ?[a]%:num ?[b]%:num = (lcm_posQ ?a ?b)%:num)%R //.
+ rewrite (_ : lcm_rat ?[a]%:num ?[b]%:num = (lcm_pos_rat ?a ?b)%:num)%R //.
by rewrite unlock. }
case (ltP (F_UPP_c f / (F_UPP_d f)%:num)%R (F_UPP_c f' / (F_UPP_d f')%:num)%R).
{ move=> Hcd'; rewrite Hcd'.
@@ -869,7 +869,7 @@ case (ltP (F_UPP_c f / (F_UPP_d f)%:num)%R (F_UPP_c f' / (F_UPP_d f')%:num)%R).
have HT :
(Num.max
((F_UPP_T f)%:nngnum + (F_UPP_T f')%:nngnum +
- (lcm_posQ (F_UPP_d f) (F_UPP_d f'))%:num)
+ (lcm_pos_rat (F_UPP_d f) (F_UPP_d f'))%:num)
((insubd 0%:nng (rM1 - rm1))%:nngnum
/ (insubd 0%:nng (F_UPP_c f' / (F_UPP_d f')%:num
- F_UPP_c f / (F_UPP_d f)%:num))%:nngnum)
@@ -932,7 +932,7 @@ rewrite Hm1.
have HT :
(Num.max
((F_UPP_T f)%:nngnum + (F_UPP_T f')%:nngnum +
- (lcm_posQ (F_UPP_d f) (F_UPP_d f'))%:num)
+ (lcm_pos_rat (F_UPP_d f) (F_UPP_d f'))%:num)
((insubd 0%:nng (rM1 - rm1))%:nngnum
/ (insubd 0%:nng (F_UPP_c f / (F_UPP_d f)%:num
- F_UPP_c f' / (F_UPP_d f')%:num))%:nngnum)
@@ -1079,7 +1079,7 @@ apply: andb_R.
by rewrite /eq_op /eq_rat /div_op /div_rat /=; case: eqP. }
have H :
(Num.max (F_UPP_T a1)%:nngnum (F_UPP_T a1')%:nngnum
- + (lcm_posQ (F_UPP_d a1) (F_UPP_d a1'))%:num)%R
+ + (lcm_pos_rat (F_UPP_d a1) (F_UPP_d a1'))%:num)%R
= (max_op (sequpp_T a2) (sequpp_T a2') + lcm_op (sequpp_d a2) (sequpp_d a2'))%C.
{ by rewrite unlock; apply: f_equal2; (apply: f_equal2; [case: ra|case: ra']). }
eapply refinesP.
@@ -1410,7 +1410,7 @@ Fact hDev_bounded_key : unit. Proof. by []. Qed.
Definition hDev_bounded := locked_with hDev_bounded_key hDev_bounded_def.
Canonical hDev_bounded_unlockable := [unlockable fun hDev_bounded].
-Global Instance RsequppC_hDev_obounded a1 a2 a1' a2' (b1 : Q) b2 :
+Global Instance RsequppC_hDev_obounded a1 a2 a1' a2' (b1 : rat) b2 :
refines (or_None RsequppC) a1 a2 -> refines (or_None RsequppC) a1' a2' ->
refines rratC b1 b2 ->
refines
@@ -1440,7 +1440,7 @@ Fact vDev_bounded_key : unit. Proof. by []. Qed.
Definition vDev_bounded := locked_with vDev_bounded_key vDev_bounded_def.
Canonical vDev_bounded_unlockable := [unlockable fun vDev_bounded].
-Global Instance RsequppC_vDev_obounded a1 a2 a1' a2' (b1 : Q) b2 :
+Global Instance RsequppC_vDev_obounded a1 a2 a1' a2' (b1 : rat) b2 :
refines (or_None RsequppC) a1 a2 -> refines (or_None RsequppC) a1' a2' ->
refines rratC b1 b2 ->
refines
diff --git a/minerve/ratdiv.v b/minerve/ratdiv.v
index bab7c31f..213ae875 100644
--- a/minerve/ratdiv.v
+++ b/minerve/ratdiv.v
@@ -10,43 +10,43 @@ Unset Printing Implicit Defensive.
Local Open Scope ring_scope.
-Definition lcm_Q (d d' : Q) : Q :=
+Definition lcm_rat (d d' : rat) : rat :=
fracq (lcmz (numq d * (lcmz (denq d) (denq d') %/ denq d)%Z)
(numq d' * (lcmz (denq d) (denq d') %/ denq d')%Z),
lcmz (denq d) (denq d')).
-Lemma lcm_posQ_aux1 (a : int) (b c : nat) :
+Lemma lcm_pos_rat_aux1 (a : int) (b c : nat) :
a%:Q * (lcmz b.+1 c.+1 %/ b.+1)%Z%:Q = a%:Q / b.+1%:R * (lcmz b.+1 c.+1)%:Q.
Proof.
rewrite -GRing.mulrA; apply f_equal2 => [//|].
-have H_b_unit : (b.+1%:~R : Q) \is a GRing.unit.
+have H_b_unit : (b.+1%:~R : rat) \is a GRing.unit.
{ by rewrite /= /in_mem /mem /= intq_eq0. }
move: (GRing.mulIr H_b_unit); apply.
rewrite -intrM divzK ?dvdz_lcml //.
by rewrite GRing.mulrC GRing.mulrA GRing.mulrV // GRing.mul1r.
Qed.
-Lemma lcm_posQ_aux2 (d d' : Q) :
+Lemma lcm_pos_rat_aux2 (d d' : rat) :
(numq d)%:Q * (lcmz (denq d) (denq d') %/ denq d)%Z%:Q
= d * (lcmz (denq d) (denq d'))%:Q.
Proof.
-by case: ratP => a b Hab; case: ratP => a' b' Hab'; rewrite lcm_posQ_aux1.
+by case: ratP => a b Hab; case: ratP => a' b' Hab'; rewrite lcm_pos_rat_aux1.
Qed.
-Program Definition lcm_posQ_def (d d' : Q+*) : Q+* :=
- @PosNumDef _ (Phant Q) (lcm_Q d%:num d'%:num) _.
+Program Definition lcm_pos_rat_def (d d' : {posnum rat}) : {posnum rat} :=
+ @PosNumDef _ (Phant rat) (lcm_rat d%:num d'%:num) _.
Next Obligation.
-rewrite /lcm_Q fracqE /=.
+rewrite /lcm_rat fracqE /=.
apply Num.Theory.mulr_gt0.
{ rewrite -[0]/(0%:~R) ltr_int.
rewrite Order.POrderTheory.lt_def lcmz_ge0 andbC /=.
rewrite lcmz_neq0; apply/andP; split.
{ apply/eqP => /(f_equal (fun x => x%:Q)).
- rewrite intrM lcm_posQ_aux2.
+ rewrite intrM lcm_pos_rat_aux2.
apply/eqP/GRing.mulf_neq0 => //.
by rewrite intr_eq0 lcmz_neq0 !denq_neq0. }
apply/eqP => /(f_equal (fun x => x%:Q)).
- rewrite intrM lcmzC lcm_posQ_aux2.
+ rewrite intrM lcmzC lcm_pos_rat_aux2.
apply/eqP/GRing.mulf_neq0 => //.
by rewrite intr_eq0 lcmz_neq0 !denq_neq0. }
rewrite Num.Theory.invr_gt0.
@@ -54,20 +54,20 @@ rewrite -[0]/(0%:~R) ltr_int.
rewrite Order.POrderTheory.lt_def lcmz_ge0 andbC /=.
by rewrite lcmz_neq0 !denq_neq0.
Qed.
-Fact lcm_posQ_key : unit. Proof. by []. Qed.
-Definition lcm_posQ := locked_with lcm_posQ_key lcm_posQ_def.
-Canonical lcm_posQ_unlockable := [unlockable fun lcm_posQ].
+Fact lcm_pos_rat_key : unit. Proof. by []. Qed.
+Definition lcm_pos_rat := locked_with lcm_pos_rat_key lcm_pos_rat_def.
+Canonical lcm_pos_rat_unlockable := [unlockable fun lcm_pos_rat].
-Lemma lcm_posQC : commutative lcm_posQ.
+Lemma lcm_pos_ratC : commutative lcm_pos_rat.
Proof.
move=> d d'; apply/val_inj.
-by rewrite unlock /= /lcm_Q /= lcmzC (lcmzC (denq d%:num)).
+by rewrite unlock /= /lcm_rat /= lcmzC (lcmzC (denq d%:num)).
Qed.
-Lemma dvdq_lcml (d d' : Q+*) :
- exists k : nat, (lcm_posQ d d')%:num = k%:R * d%:num.
+Lemma dvdq_lcml (d d' : {posnum rat}) :
+ exists k : nat, (lcm_pos_rat d d')%:num = k%:R * d%:num.
Proof.
-rewrite unlock /= /lcm_Q /=.
+rewrite unlock /= /lcm_rat /=.
set x := _ * _.
set y := _ * _.
move: (dvdn_lcml (absz x) (absz y)) => /dvdnP [k Hk]; rewrite {1}/lcmz Hk.
@@ -76,43 +76,43 @@ have Hx : 0 <= x.
{ apply Num.Theory.mulr_ge0.
{ by rewrite numq_ge0. }
by rewrite lez_divRL // GRing.mul0r lcmz_ge0. }
-rewrite PoszM gez0_abs // fracqE /= /x 2!intrM lcm_posQ_aux2.
-have H_lcmdd'_unit : (intr (lcmz (denq d%:num) (denq d'%:num)) : Q) \is a GRing.unit.
+rewrite PoszM gez0_abs // fracqE /= /x 2!intrM lcm_pos_rat_aux2.
+have H_lcmdd'_unit : (intr (lcmz (denq d%:num) (denq d'%:num)) : rat) \is a GRing.unit.
{ by rewrite /in_mem /mem /= intq_eq0 lcmz_neq0 /= !denq_neq0. }
by rewrite -!GRing.mulrA GRing.mulrV // GRing.mulr1.
Qed.
-Lemma dvdq_lcmr (d d' : Q+*) :
- exists k : nat, (lcm_posQ d d')%:num = k%:R * d'%:num.
-Proof. by rewrite lcm_posQC; apply dvdq_lcml. Qed.
+Lemma dvdq_lcmr (d d' : {posnum rat}) :
+ exists k : nat, (lcm_pos_rat d d')%:num = k%:R * d'%:num.
+Proof. by rewrite lcm_pos_ratC; apply dvdq_lcml. Qed.
-Lemma dvdq_lcm (d d' : Q+*) (m : Q) (k k' : nat) :
+Lemma dvdq_lcm (d d' : {posnum rat}) (m : rat) (k k' : nat) :
m = k%:R * d%:num -> m = k'%:R * d'%:num ->
- exists k'' : nat, m = k''%:R * (lcm_posQ d d')%:num.
+ exists k'' : nat, m = k''%:R * (lcm_pos_rat d d')%:num.
Proof.
move=> Hd Hd'.
-rewrite unlock /= /lcm_Q /=.
+rewrite unlock /= /lcm_rat /=.
set ldd' := lcmz (denq _) _.
set x := _ * _.
set y := _ * _.
have Hx : m * ldd'%:Q = (k%:Z * x)%:Q.
-{ by rewrite Hd -GRing.mulrA -lcm_posQ_aux2 !intrM. }
+{ by rewrite Hd -GRing.mulrA -lcm_pos_rat_aux2 !intrM. }
have Hy : m * ldd'%:Q = (k'%:Z * y)%:Q.
-{ by rewrite Hd' -GRing.mulrA /ldd' lcmzC -lcm_posQ_aux2 lcmzC !intrM. }
-have H_ldd'_unit : (intr ldd' : Q) \is a GRing.unit.
+{ by rewrite Hd' -GRing.mulrA /ldd' lcmzC -lcm_pos_rat_aux2 lcmzC !intrM. }
+have H_ldd'_unit : (intr ldd' : rat) \is a GRing.unit.
{ by rewrite /in_mem /mem /= intq_eq0 lcmz_neq0 /= !denq_neq0. }
have Px : 0 <= x.
-{ rewrite -(@ler_int rat_numDomainType) /x intrM lcm_posQ_aux2.
+{ rewrite -(@ler_int rat_numDomainType) /x intrM lcm_pos_rat_aux2.
apply Num.Theory.mulr_ge0 => //.
by rewrite -[0]/(intr 0) ler_int lcmz_ge0. }
have Py : 0 <= y.
-{ rewrite -(@ler_int rat_numDomainType) /y intrM /ldd' lcmzC lcm_posQ_aux2.
+{ rewrite -(@ler_int rat_numDomainType) /y intrM /ldd' lcmzC lcm_pos_rat_aux2.
apply Num.Theory.mulr_ge0 => //.
by rewrite -[0]/(intr 0) ler_int lcmz_ge0. }
have : (lcmn (absz x) (absz y) %| k * absz x)%nat.
{ rewrite dvdn_lcm dvdn_mull //=.
apply/dvdnP; exists k'.
- suff: intr (k%:Z * absz x) = intr (k'%:Z * absz y) :> Q.
+ suff: intr (k%:Z * absz x) = intr (k'%:Z * absz y) :> rat.
{ by move=> /eqP; rewrite eqr_int -!PoszM => /eqP []. }
by rewrite !gez0_abs // -Hx -Hy. }
move=> /dvdnP [k'' Hk''].
@@ -123,9 +123,9 @@ rewrite -!GRing.mulrA GRing.mulVr // GRing.mulr1.
by rewrite -[k''%:R]/(k''%:~R) -intrM -PoszM -Hk'' PoszM gez0_abs.
Qed.
-Lemma dvdq_ge_lcm (d d' m : Q+*) (k k' : nat) :
+Lemma dvdq_ge_lcm (d d' m : {posnum rat}) (k k' : nat) :
m%:num = k%:R * d%:num -> m%:num = k'%:R * d'%:num ->
- (lcm_posQ d d')%:num <= m%:num.
+ (lcm_pos_rat d d')%:num <= m%:num.
Proof.
move=> Hd Hd'.
move: (dvdq_lcm Hd Hd') => [] [|k'' ->].
@@ -134,36 +134,36 @@ rewrite -addn1 GRing.natrD GRing.mulrDl GRing.mul1r.
by rewrite Num.Theory.ler_addr; apply Num.Theory.mulr_ge0.
Qed.
-Lemma lcm_posQA : associative lcm_posQ.
+Lemma lcm_pos_ratA : associative lcm_pos_rat.
Proof.
move=> a b c.
apply/Order.POrderTheory.le_anti/andP; split.
-{ move: (dvdq_lcml (lcm_posQ a b) c) => [k].
- set m := lcm_posQ (lcm_posQ a b) c => Hab.
+{ move: (dvdq_lcml (lcm_pos_rat a b) c) => [k].
+ set m := lcm_pos_rat (lcm_pos_rat a b) c => Hab.
move: (dvdq_lcml a b) (Hab) => [k' ->].
rewrite GRing.mulrA -GRing.natrM => Ha.
move: (dvdq_lcmr a b) (Hab) => [k'' ->].
rewrite GRing.mulrA -GRing.natrM => Hb.
- move: (dvdq_lcmr (lcm_posQ a b) c) => [k'''].
+ move: (dvdq_lcmr (lcm_pos_rat a b) c) => [k'''].
rewrite -/m => Hc.
move: (dvdq_lcm Hb Hc) => [k''''].
move: Ha; apply dvdq_ge_lcm. }
-move: (dvdq_lcmr a (lcm_posQ b c)) => [k].
-set m := lcm_posQ a (lcm_posQ b c) => Hbc.
+move: (dvdq_lcmr a (lcm_pos_rat b c)) => [k].
+set m := lcm_pos_rat a (lcm_pos_rat b c) => Hbc.
move: (dvdq_lcml b c) (Hbc) => [k' ->].
rewrite GRing.mulrA -GRing.natrM => Hb.
move: (dvdq_lcmr b c) (Hbc) => [k'' ->].
rewrite GRing.mulrA -GRing.natrM => Hc.
-move: (dvdq_lcml a (lcm_posQ b c)) => [k'''].
+move: (dvdq_lcml a (lcm_pos_rat b c)) => [k'''].
rewrite -/m => Ha.
move: (dvdq_lcm Ha Hb) Hc => [k''''].
apply dvdq_ge_lcm.
Qed.
-Lemma lcm_posQ_xx : idempotent lcm_posQ.
+Lemma lcm_pos_rat_xx : idempotent lcm_pos_rat.
Proof.
move=> x; apply/val_inj => /=.
-rewrite unlock /=/ lcm_Q /lcmz /= !Order.NatDvd.lcmnn.
+rewrite unlock /=/ lcm_rat /lcmz /= !Order.NatDvd.lcmnn.
rewrite (@gez0_abs (denq x%:num)) ?denq_ge0 //.
rewrite divzz denq_eq0 /= GRing.mulr1.
move: (posnum_gt0 x); rewrite -numq_gt0.
diff --git a/minerve/tactic.v b/minerve/tactic.v
index 5ae61081..b8ddbb5f 100644
--- a/minerve/tactic.v
+++ b/minerve/tactic.v
@@ -100,7 +100,7 @@ Global Instance refine_ratBigQ_lcm :
refines (r_ratBigQ ==> r_ratBigQ ==> r_ratBigQ)%rel lcm_rat lcm_op.
Proof.
rewrite refinesE => x1 x2 /r_ratBigQ_red rx y1 y2 /r_ratBigQ_red ry.
-rewrite /lcm_rat /ratdiv.lcm_Q fracqE.
+rewrite /lcm_rat /ratdiv.lcm_rat fracqE.
case: (ratP x1) rx => nx1 dx1 _ rx {x1}.
case: (ratP y1) ry => ny1 dy1 _ ry {y1}.
rewrite /mathcomp_complements.lcmz !abszM /= !mul1n.
diff --git a/services.v b/services.v
index a0dd3623..2c5a32bc 100644
--- a/services.v
+++ b/services.v
@@ -45,7 +45,7 @@ Definition is_min_service S beta := forall A, is_min_service_for S beta A.
(* Final : def 5.5 p108 *)
Definition is_strict_min_service (S : flow_cc -> flow_cc -> Prop) (beta : F) :=
forall A D, S A D ->
- forall u v : R+, backlogged_period A D u%:nngnum v%:nngnum ->
+ forall u v : {nonneg R}, backlogged_period A D u%:nngnum v%:nngnum ->
(beta (insubd 0%:nng (v%:nngnum - u%:nngnum))%R <= D v - D u)%dE.
(** Max service *)
@@ -159,7 +159,7 @@ Qed.
(* Th 16 p 163 *)
(* Final Th 6.2 p 143 *)
(** *** Server as a Jitter *)
-Theorem Server_as_a_jitter_min (A D : flow_cc) (S : partial_server) (dm : R+) :
+Theorem Server_as_a_jitter_min (A D : flow_cc) (S : partial_server) (dm : {nonneg R}) :
S A D ->
(dm%:nngnum%R%:E <= ereal_inf [set (delay_at A D t)%:nngenum | t in setT])%E ->
D <= ((A : F) * (delta dm%:nngnum%R%:E))%D :> F.
@@ -206,7 +206,7 @@ Qed.
(* Th 16 p 163 *)
(* Final Th 6.2 p 143 *)
(** *** Server as a Jitter *)
-Theorem Server_as_a_jitter_max (A D : flow_cc) (S : partial_server) (dM : barR+) :
+Theorem Server_as_a_jitter_max (A D : flow_cc) (S : partial_server) (dM : {nonnege R}) :
S A D -> ((delay A D)%:nngenum <= dM%:nngenum)%E ->
((A : F) * delta dM%:nngenum)%D <= D.
Proof.
diff --git a/static_priority.v b/static_priority.v
index 907e0a70..f3868722 100644
--- a/static_priority.v
+++ b/static_priority.v
@@ -78,7 +78,7 @@ Lemma backlogged_period_server_cond n (S : (n.+1).-server) A D (s t : R)
(P : pred 'I_n.+1):
S A D ->
(s <= t
- /\ forall u : R+, s < u%:nngnum <= t -> exists i, P i /\ ((D i) u < (A i) u)%E)
+ /\ forall u : {nonneg R}, s < u%:nngnum <= t -> exists i, P i /\ ((D i) u < (A i) u)%E)
<-> backlogged_period (\sum_(i | P i) A i)%C (\sum_(i | P i) D i)%C s t.
Proof.
move=> Hs; split.
@@ -104,7 +104,7 @@ Qed.
(* Lemma 25 page 175 without condition *)
Lemma backlogged_period_eqv n (S : (n.+1).-server) A D (s t : R) :
S A D ->
- (s <= t /\ forall u : R+, s < u%:nngnum <= t -> exists i, ((D i) u < (A i) u)%E)
+ (s <= t /\ forall u : {nonneg R}, s < u%:nngnum <= t -> exists i, ((D i) u < (A i) u)%E)
<-> backlogged_period (\sum_i A i)%C (\sum_i D i)%C s t.
Proof.
move=> HS; split.
@@ -135,7 +135,7 @@ Qed.
Definition preemptive_SP n (S : (n.+1).-server) (prior : 'I_n.+1 -> nat) :=
forall A D,
S A D ->
- forall i, forall s t : R+,
+ forall i, forall s t : {nonneg R},
backlogged_period
(\sum_(j < n.+1 | (prior j < prior i)%nat) A j)%C
(\sum_(j < n.+1 | (prior j < prior i)%nat) D j)%C
@@ -168,7 +168,7 @@ have Hpu : p <= u; [exact: start_le|].
move: (@start_t_is_a_backlogged_period
_ _ _ u (aggregate_server_prop_cond HAD (fun j => prior j < prior i)%nat)).
rewrite -/sum_A_higher_i -/sum_D_higher_i -/p => Hpu_backl.
-suff: forall w : R+, p <= w <= v ->
+suff: forall w : {nonneg R}, p <= w <= v ->
(beta (insubd 0%:nng (w%:nngnum - p%:nngnum))%R
- sum_alpha_higher_i (insubd 0%:nng (w%:nngnum - p%:nngnum))%R
<= D i w - D i p)%dE.
@@ -250,7 +250,7 @@ rewrite [in X in _ + X] (bigID (fun j0 => (prior j0 <= prior i)%nat)) /=.
under [in X in - (_ + X)] eq_bigl => k do rewrite -ltnNge.
rewrite le_eqVlt; apply/orP; left; apply/eqP.
have H_D_after_i :
- forall w : R+, p <= w <= u ->
+ forall w : {nonneg R}, p <= w <= u ->
(\sum_(j | (prior i < prior j)%nat) D j)%C p
= (\sum_(j | (prior i < prior j)%nat) D j)%C w.
{ move=> w' /andP[Hw'p Hw'u].
diff --git a/usual_functions.v b/usual_functions.v
index a7f265ad..901ab096 100644
--- a/usual_functions.v
+++ b/usual_functions.v
@@ -47,7 +47,7 @@ Proof. by apply/val_inj/val_inj/funext => t /=; rewrite lee_pinfty. Qed.
(* Prop 12 p.62 *)
(* Final Prop 3.2 p40 *)
-Lemma delta_prop_conv (f : Fup) (d : R+) t :
+Lemma delta_prop_conv (f : Fup) (d : {nonneg R}) t :
(f * (delta d%:nngnum%:E))%F t = f (insubd 0%:nng (t%:nngnum - d%:nngnum)).
Proof.
case: (leP 0 (t%:nngnum - d%:nngnum)) => S_t_d.
@@ -77,7 +77,7 @@ by rewrite ler_addr.
Qed.
(** *** Token bucket *)
-Program Definition gamma_h (r b : R+) :=
+Program Definition gamma_h (r b : {nonneg R}) :=
Build_Fup
(Build_Fplus (fun t => ((r%:nngnum * t%:nngnum) + b%:nngnum)%:E) _) _.
Next Obligation. by apply/leFP => t; rewrite lee_fin. Qed.
--
GitLab