clutch.base_logic.error_credits_mult
This file implements multiplicative error credits
From Stdlib Require Import Reals RIneq Psatz.
From Coquelicot Require Import Lim_seq.
From clutch.prelude Require Export base classical Reals_ext NNRbar.
From iris.prelude Require Import options.
From iris.proofmode Require Import proofmode.
From iris.algebra Require Export auth numbers.
From iris.base_logic.lib Require Import iprop own.
Import uPred.
Canonical Structure nonnegrealO : ofe := leibnizO nonnegreal.
From Coquelicot Require Import Lim_seq.
From clutch.prelude Require Export base classical Reals_ext NNRbar.
From iris.prelude Require Import options.
From iris.proofmode Require Import proofmode.
From iris.algebra Require Export auth numbers.
From iris.base_logic.lib Require Import iprop own.
Import uPred.
Canonical Structure nonnegrealO : ofe := leibnizO nonnegreal.
Section nonnegreal.
Global Instance R_inhabited : Inhabited R := populate (1%R).
Global Instance nonnegreal_inhabited : Inhabited nonnegreal := populate (nnreal_one).
#[local] Open Scope R.
#[local] Open Scope NNR.
#[local] Instance nonnegreal_valid_instance : Valid (nonnegreal) := λ r, True.
#[local] Instance nonnegreal_validN_instance : ValidN (nonnegreal) := λ _ r, True.
#[local] Instance nonnegreal_pcore_instance : PCore (nonnegreal) := λ _, Some 0.
#[local] Instance nonnegreal_op_instance : Op (nonnegreal) := λ x y, (x + y).
#[local] Instance nonnegreal_equiv : Equiv nonnegreal := λ x y, x = y.
Definition nonnegreal_op (x y : nonnegreal) : x ⋅ y = x + y := eq_refl.
#[local] Lemma Rle_0_le_minus (x y : R) : x <= y → 0 <= y - x.
Proof. lra. Qed.
Lemma nonnegreal_included (x y : nonnegreal) : x ≼ y ↔ x <= y.
Proof.
split; intros.
- destruct x, y => /=.
destruct H as ((z & Hz) & H).
rewrite nonnegreal_op /nnreal_plus in H.
inversion H. lra.
- destruct x as (x & Hx), y as (y & Hy).
simpl in H.
eexists ({| nonneg := y - x ; cond_nonneg := Rle_0_le_minus x y H |}).
rewrite nonnegreal_op /= /equiv/nonnegreal_equiv /=.
apply nnreal_ext => /=. lra.
Qed.
Lemma nonnegreal_ra_mixin : RAMixin nonnegreal.
Proof.
apply ra_total_mixin; try by eauto.
- solve_proper.
- intros ? ? ?.
rewrite /equiv/nonnegreal_equiv.
apply nnreal_ext; simpl; lra.
- intros ? ?.
rewrite /equiv/nonnegreal_equiv.
apply nnreal_ext; simpl; lra.
- intros ?.
rewrite /equiv/nonnegreal_equiv.
apply nnreal_ext; simpl; lra.
- intros ? ? ?.
apply nonnegreal_included; simpl; lra.
Qed.
Canonical Structure nonnegrealR : cmra := discreteR nonnegreal nonnegreal_ra_mixin.
Global Instance nonnegreal_cmra_discrete : CmraDiscrete nonnegrealR.
Proof. apply discrete_cmra_discrete. Qed.
Local Instance nonnegreal_unit_instance : Unit nonnegreal := nnreal_zero.
Lemma nonnegreal_ucmra_mixin : UcmraMixin nonnegreal.
Proof.
split.
- rewrite /valid.
rewrite /nonnegreal_valid_instance.
simpl. lra.
- rewrite /LeftId.
intro.
rewrite /equiv/nonnegreal_equiv/op/nonnegreal_op_instance/=.
apply nnreal_ext; simpl; lra.
- rewrite /pcore/nonnegreal_pcore_instance; auto.
Qed.
Canonical Structure nonnegrealUR : ucmra := Ucmra nonnegreal nonnegreal_ucmra_mixin.
Lemma nonnegreal_add_cancel_l (x y z : nonnegreal) :
z + x = z + y ↔ x = y.
Proof.
rewrite /nnreal_plus.
split; intro H.
- apply nnreal_ext. simplify_eq. lra.
- simplify_eq; auto.
Qed.
Global Instance nonnegreal_cancelable (x : nonnegreal) : Cancelable x.
Proof. by intros ???? ?%nonnegreal_add_cancel_l. Qed.
Lemma nonnegreal_local_update (x y x' y' : nonnegreal) :
y' <= y → x + y' = x' + y → (x,y) ~l~> (x',y').
Proof.
intros ??; apply (local_update_unital_discrete x y x' y') => z H1 H2.
compute in H2; simplify_eq; simpl.
destruct y, x', y', z; simplify_eq; simpl.
split => //.
compute.
apply nnreal_ext; simpl in *; lra.
Qed.
Global Instance nonnegreal_is_op (n1 n2 : nonnegreal) : IsOp (n1 + n2) n1 n2.
Proof. done. Qed.
End nonnegreal.
Class ecmGpreS (Σ : gFunctors) := EcmGpreS {
ecmGpreS_inG :: inG Σ (authR nonnegrealUR)
}.
Class ecmGS (Σ : gFunctors) := EcmGS {
ecmGS_inG : inG Σ (authR nonnegrealUR);
ecmGS_name : gname;
}.
Global Hint Mode ecmGS - : typeclass_instances.
Local Existing Instances ecmGS_inG ecmGpreS_inG.
Definition ecmΣ := #[GFunctor (authR (nonnegrealUR))].
Global Instance subG_ecmΣ {Σ} : subG ecmΣ Σ → ecmGpreS Σ.
Proof. solve_inG. Qed.
Global Instance R_inhabited : Inhabited R := populate (1%R).
Global Instance nonnegreal_inhabited : Inhabited nonnegreal := populate (nnreal_one).
#[local] Open Scope R.
#[local] Open Scope NNR.
#[local] Instance nonnegreal_valid_instance : Valid (nonnegreal) := λ r, True.
#[local] Instance nonnegreal_validN_instance : ValidN (nonnegreal) := λ _ r, True.
#[local] Instance nonnegreal_pcore_instance : PCore (nonnegreal) := λ _, Some 0.
#[local] Instance nonnegreal_op_instance : Op (nonnegreal) := λ x y, (x + y).
#[local] Instance nonnegreal_equiv : Equiv nonnegreal := λ x y, x = y.
Definition nonnegreal_op (x y : nonnegreal) : x ⋅ y = x + y := eq_refl.
#[local] Lemma Rle_0_le_minus (x y : R) : x <= y → 0 <= y - x.
Proof. lra. Qed.
Lemma nonnegreal_included (x y : nonnegreal) : x ≼ y ↔ x <= y.
Proof.
split; intros.
- destruct x, y => /=.
destruct H as ((z & Hz) & H).
rewrite nonnegreal_op /nnreal_plus in H.
inversion H. lra.
- destruct x as (x & Hx), y as (y & Hy).
simpl in H.
eexists ({| nonneg := y - x ; cond_nonneg := Rle_0_le_minus x y H |}).
rewrite nonnegreal_op /= /equiv/nonnegreal_equiv /=.
apply nnreal_ext => /=. lra.
Qed.
Lemma nonnegreal_ra_mixin : RAMixin nonnegreal.
Proof.
apply ra_total_mixin; try by eauto.
- solve_proper.
- intros ? ? ?.
rewrite /equiv/nonnegreal_equiv.
apply nnreal_ext; simpl; lra.
- intros ? ?.
rewrite /equiv/nonnegreal_equiv.
apply nnreal_ext; simpl; lra.
- intros ?.
rewrite /equiv/nonnegreal_equiv.
apply nnreal_ext; simpl; lra.
- intros ? ? ?.
apply nonnegreal_included; simpl; lra.
Qed.
Canonical Structure nonnegrealR : cmra := discreteR nonnegreal nonnegreal_ra_mixin.
Global Instance nonnegreal_cmra_discrete : CmraDiscrete nonnegrealR.
Proof. apply discrete_cmra_discrete. Qed.
Local Instance nonnegreal_unit_instance : Unit nonnegreal := nnreal_zero.
Lemma nonnegreal_ucmra_mixin : UcmraMixin nonnegreal.
Proof.
split.
- rewrite /valid.
rewrite /nonnegreal_valid_instance.
simpl. lra.
- rewrite /LeftId.
intro.
rewrite /equiv/nonnegreal_equiv/op/nonnegreal_op_instance/=.
apply nnreal_ext; simpl; lra.
- rewrite /pcore/nonnegreal_pcore_instance; auto.
Qed.
Canonical Structure nonnegrealUR : ucmra := Ucmra nonnegreal nonnegreal_ucmra_mixin.
Lemma nonnegreal_add_cancel_l (x y z : nonnegreal) :
z + x = z + y ↔ x = y.
Proof.
rewrite /nnreal_plus.
split; intro H.
- apply nnreal_ext. simplify_eq. lra.
- simplify_eq; auto.
Qed.
Global Instance nonnegreal_cancelable (x : nonnegreal) : Cancelable x.
Proof. by intros ???? ?%nonnegreal_add_cancel_l. Qed.
Lemma nonnegreal_local_update (x y x' y' : nonnegreal) :
y' <= y → x + y' = x' + y → (x,y) ~l~> (x',y').
Proof.
intros ??; apply (local_update_unital_discrete x y x' y') => z H1 H2.
compute in H2; simplify_eq; simpl.
destruct y, x', y', z; simplify_eq; simpl.
split => //.
compute.
apply nnreal_ext; simpl in *; lra.
Qed.
Global Instance nonnegreal_is_op (n1 n2 : nonnegreal) : IsOp (n1 + n2) n1 n2.
Proof. done. Qed.
End nonnegreal.
Class ecmGpreS (Σ : gFunctors) := EcmGpreS {
ecmGpreS_inG :: inG Σ (authR nonnegrealUR)
}.
Class ecmGS (Σ : gFunctors) := EcmGS {
ecmGS_inG : inG Σ (authR nonnegrealUR);
ecmGS_name : gname;
}.
Global Hint Mode ecmGS - : typeclass_instances.
Local Existing Instances ecmGS_inG ecmGpreS_inG.
Definition ecmΣ := #[GFunctor (authR (nonnegrealUR))].
Global Instance subG_ecmΣ {Σ} : subG ecmΣ Σ → ecmGpreS Σ.
Proof. solve_inG. Qed.
The internal authoritative part of the credit ghost state,
tracking how many credits are available in total.
Users should not directly interface with this.
Local Definition ecm_supply_def `{!ecmGS Σ} (ε : nonnegreal) : iProp Σ := own ecmGS_name (● ε).
Local Definition ecm_supply_aux : seal (@ecm_supply_def). Proof. by eexists. Qed.
Definition ecm_supply := ecm_supply_aux.(unseal).
Local Definition ecm_supply_unseal :
@ecm_supply = @ecm_supply_def := ecm_supply_aux.(seal_eq).
Global Arguments ecm_supply {Σ _} ε.
Local Definition ecm_supply_aux : seal (@ecm_supply_def). Proof. by eexists. Qed.
Definition ecm_supply := ecm_supply_aux.(unseal).
Local Definition ecm_supply_unseal :
@ecm_supply = @ecm_supply_def := ecm_supply_aux.(seal_eq).
Global Arguments ecm_supply {Σ _} ε.
The user-facing error resource, denoting ownership of ε error credits.
Local Definition ecm_def `{!ecmGS Σ} (ε : nonnegreal) : iProp Σ := own ecmGS_name (◯ ε).
Local Definition ecm_aux : seal (@ecm_def). Proof. by eexists. Qed.
Definition ecm := ecm_aux.(unseal).
Local Definition ecm_unseal :
@ecm = @ecm_def := ecm_aux.(seal_eq).
Global Arguments ecm {Σ _} ε.
Notation "'↯m' ε" := (∃ (x : nonnegreal), ⌜x.(nonneg) = ε%R⌝ ∗ ecm x)%I
(at level 1).
Section error_credit_theory.
Context `{!ecmGS Σ}.
Implicit Types (P Q : iProp Σ).
#[local] Open Scope R.
Local Definition ecm_aux : seal (@ecm_def). Proof. by eexists. Qed.
Definition ecm := ecm_aux.(unseal).
Local Definition ecm_unseal :
@ecm = @ecm_def := ecm_aux.(seal_eq).
Global Arguments ecm {Σ _} ε.
Notation "'↯m' ε" := (∃ (x : nonnegreal), ⌜x.(nonneg) = ε%R⌝ ∗ ecm x)%I
(at level 1).
Section error_credit_theory.
Context `{!ecmGS Σ}.
Implicit Types (P Q : iProp Σ).
#[local] Open Scope R.
Error credit rules
Lemma ecm_split (ε1 ε2 : R) :
0 <= ε1 →
0 <= ε2 →
↯m (ε1 + ε2) ⊢ ↯m ε1 ∗ ↯m ε2.
Proof.
iIntros (Hx1 Hx2) "(%x & %Hx & Hx)".
rewrite ecm_unseal /ecm_def.
set (x1' := mknonnegreal _ Hx1).
set (x2' := mknonnegreal _ Hx2).
assert (x = (x1' + x2')%NNR) as -> by apply nnreal_ext => //=.
rewrite auth_frag_op own_op.
iDestruct (own_op with "Hx") as "[Hx1 Hx2]".
iSplitL "Hx1"; by iExists _; iFrame.
Qed.
Lemma ecm_split_le (r1 r2 : R) :
0 <= r1 <= r2 →
↯m r2 ⊢ ↯m r1 ∗ ↯m (r2 - r1).
Proof.
iIntros (?).
assert (r2 = (r1 + (r2 - r1))%R) as Hr2 by lra.
rewrite {1}Hr2.
apply ecm_split; lra.
Qed.
Lemma ecm_combine (r1 r2 : R) :
↯m r1 ∗ ↯m r2 ⊢ ↯m (r1 + r2).
Proof.
iIntros "[(%x1 & <- & Hr1) (%x2 & <- & Hr2)]".
rewrite ecm_unseal /ecm_def.
iExists (x1 + x2)%NNR.
iSplit; [done|].
rewrite auth_frag_op own_op.
iFrame.
Qed.
Lemma ecm_zero : ⊢ |==> ↯m 0.
Proof.
rewrite ecm_unseal /ecm_def.
iExists nnreal_zero.
iMod own_unit as "H".
iModIntro. iSplit; done.
Qed.
Lemma ecm_supply_bound (ε1 : R) (ε2 : nonnegreal) :
ecm_supply ε2 -∗ ↯m ε1 -∗ ⌜ε1 <= ε2⌝.
Proof.
rewrite ecm_unseal /ecm_def ecm_supply_unseal /ecm_supply_def.
iIntros "H1 (%r & <- & H2)".
iDestruct (own_valid_2 with "H1 H2") as "%Hop".
by eapply auth_both_valid_discrete in Hop as [Hlt%nonnegreal_included ?].
Qed.
Lemma ecm_supply_ecm_inv r1 x2 :
ecm_supply x2 -∗ ↯m r1 -∗ ∃ x1 x3, ⌜x2 = (x1 + x3)%NNR⌝ ∗ ⌜x1.(nonneg) = r1⌝.
Proof.
iIntros "Hx2 Hr1".
iDestruct (ecm_supply_bound with "Hx2 Hr1") as %Hb.
iDestruct "Hr1" as (x1) "[<- Hx1]".
set (x3 := nnreal_minus x2 x1 Hb).
iExists _, x3. iSplit; [|done].
iPureIntro. apply nnreal_ext=>/=; lra.
Qed.
0 <= ε1 →
0 <= ε2 →
↯m (ε1 + ε2) ⊢ ↯m ε1 ∗ ↯m ε2.
Proof.
iIntros (Hx1 Hx2) "(%x & %Hx & Hx)".
rewrite ecm_unseal /ecm_def.
set (x1' := mknonnegreal _ Hx1).
set (x2' := mknonnegreal _ Hx2).
assert (x = (x1' + x2')%NNR) as -> by apply nnreal_ext => //=.
rewrite auth_frag_op own_op.
iDestruct (own_op with "Hx") as "[Hx1 Hx2]".
iSplitL "Hx1"; by iExists _; iFrame.
Qed.
Lemma ecm_split_le (r1 r2 : R) :
0 <= r1 <= r2 →
↯m r2 ⊢ ↯m r1 ∗ ↯m (r2 - r1).
Proof.
iIntros (?).
assert (r2 = (r1 + (r2 - r1))%R) as Hr2 by lra.
rewrite {1}Hr2.
apply ecm_split; lra.
Qed.
Lemma ecm_combine (r1 r2 : R) :
↯m r1 ∗ ↯m r2 ⊢ ↯m (r1 + r2).
Proof.
iIntros "[(%x1 & <- & Hr1) (%x2 & <- & Hr2)]".
rewrite ecm_unseal /ecm_def.
iExists (x1 + x2)%NNR.
iSplit; [done|].
rewrite auth_frag_op own_op.
iFrame.
Qed.
Lemma ecm_zero : ⊢ |==> ↯m 0.
Proof.
rewrite ecm_unseal /ecm_def.
iExists nnreal_zero.
iMod own_unit as "H".
iModIntro. iSplit; done.
Qed.
Lemma ecm_supply_bound (ε1 : R) (ε2 : nonnegreal) :
ecm_supply ε2 -∗ ↯m ε1 -∗ ⌜ε1 <= ε2⌝.
Proof.
rewrite ecm_unseal /ecm_def ecm_supply_unseal /ecm_supply_def.
iIntros "H1 (%r & <- & H2)".
iDestruct (own_valid_2 with "H1 H2") as "%Hop".
by eapply auth_both_valid_discrete in Hop as [Hlt%nonnegreal_included ?].
Qed.
Lemma ecm_supply_ecm_inv r1 x2 :
ecm_supply x2 -∗ ↯m r1 -∗ ∃ x1 x3, ⌜x2 = (x1 + x3)%NNR⌝ ∗ ⌜x1.(nonneg) = r1⌝.
Proof.
iIntros "Hx2 Hr1".
iDestruct (ecm_supply_bound with "Hx2 Hr1") as %Hb.
iDestruct "Hr1" as (x1) "[<- Hx1]".
set (x3 := nnreal_minus x2 x1 Hb).
iExists _, x3. iSplit; [|done].
iPureIntro. apply nnreal_ext=>/=; lra.
Qed.
The statement of this lemma is a bit convoluted, because only implicitly (by validity and
unfolding) can we conclude that 0 <= r1 <= x2 so thus that x2 - r1 is nonnegative
Lemma ecm_supply_decrease (r1 : R) (x2 : nonnegreal) :
ecm_supply x2 -∗ ↯m r1 -∗ |==> ∃ x1 x3, ⌜(x2 = x3 + x1)%NNR⌝ ∗ ⌜x1.(nonneg) = r1⌝ ∗ ecm_supply x3.
Proof.
iIntros "Hx2 Hr1".
iDestruct (ecm_supply_ecm_inv with "Hx2 Hr1") as %(x1 & x3 & -> & <-).
iDestruct "Hr1" as (x1') "[% Hx1]".
rewrite ecm_unseal /ecm_def ecm_supply_unseal /ecm_supply_def.
iMod (own_update_2 with "Hx2 Hx1") as "Hown".
{ eapply (auth_update_dealloc _ _ x3), nonnegreal_local_update.
- apply cond_nonneg.
- apply nnreal_ext =>/=. lra. }
iModIntro.
iExists _, _. iFrame. iSplit; [|done].
iPureIntro. apply nnreal_ext=>/=; lra.
Qed.
Lemma ecm_supply_increase (ε1 ε2 : nonnegreal) :
(* ε1 + ε2 < 1 → *)
ecm_supply ε1 -∗ |==> ecm_supply (ε1 + ε2)%NNR ∗ ↯m ε2.
Proof.
rewrite ecm_unseal /ecm_def.
rewrite ecm_supply_unseal /ecm_supply_def.
iIntros (* (?) *) "H".
iMod (own_update with "H") as "[$ $]"; [|done].
eapply auth_update_alloc.
apply (local_update_unital_discrete _ _ _ _) => z H1 H2.
split; [done|].
apply nnreal_ext. simpl.
rewrite Rplus_comm.
apply Rplus_eq_compat_l.
rewrite H2 /=. lra.
Qed.
Lemma ecm_weaken (r1 r2 : R) :
0 <= r2 <= r1 → ↯m r1 -∗ ↯m r2.
Proof.
iIntros (?) "Hr1".
assert (r1 = (r1 - r2) + r2) as -> by lra.
iDestruct (ecm_split with "Hr1") as "[? $]"; lra.
Qed.
Lemma ecm_eq x1 x2 :
x1 = x2 → ↯m x1 -∗ ↯m x2.
Proof. iIntros (->) "$". Qed.
Lemma ecm_supply_eq x1 x2 :
(x1.(nonneg) = x2.(nonneg)) → ecm_supply x1 -∗ ecm_supply x2.
Proof.
iIntros (?) "?".
replace x1 with x2; [iFrame|by apply nnreal_ext].
Qed.
(* Lemma ec_contradict (ε : R) :
1 <= ε → ↯ ε ⊢ False.
Proof.
iIntros (Hge1) "(?*)
Lemma ecm_valid (ε : R) : ↯m ε -∗ ⌜(0<=ε(* <1 *))%R⌝.
Proof.
iIntros "(%&<-&H)".
rewrite ecm_unseal /ecm_def.
iDestruct (own_valid with "H") as %?%auth_frag_valid_1.
destruct x. compute in H. simpl in *. iPureIntro. lra.
Qed.
#[local] Lemma err_amp_power ε k :
0 < ε →
1 < k →
∃ n, 1 <= ε * k ^ n.
Proof.
intros Hε Hk.
destruct (Lim_seq.is_lim_seq_geom_p k Hk (λ r, / ε <= r)) as [n Hn] => /=.
- exists (/ ε). real_solver.
- exists n.
apply (Rmult_le_reg_l (/ ε)).
+ apply Rinv_0_lt_compat, Hε.
+ rewrite -Rmult_assoc Rinv_l; [|lra].
rewrite Rmult_1_l Rmult_1_r. by apply Hn.
Qed.
#[local] Lemma err_amp_mult ε ε' k :
0 < ε →
ε <= ε' ->
1 < k →
(exists n:nat, 1 <= n*(k-1)*ε + ε').
Proof.
intros Hε Hleq Hk.
edestruct (Rcomplements.nfloor_ex (1/((k-1)*ε))) as [n [Hn1 Hn2]].
- apply Rmult_le_pos; [lra|].
left.
apply Rinv_0_lt_compat.
real_solver.
- exists (S n).
rewrite S_INR.
transitivity ((1 / ((k - 1) * ε)) * (k - 1) * ε + ε').
+ rewrite Rmult_assoc.
rewrite /Rdiv Rmult_1_l.
rewrite Rinv_l; [lra |].
assert (0<(k-1)*ε); real_solver.
+ apply Rplus_le_compat_r.
apply Rmult_le_compat_r; [lra|].
apply Rmult_le_compat_r; lra.
Qed.
(* Lemma ec_ind_amp_external (ε k : R) P :
0 < ε →
1 < k →
(∀ (ε' : R), 0 < ε' → □ (↯ (k * ε') -∗ P) ∗ ↯ ε' ⊢ P) →
(↯ ε ⊢ P).
Proof.
iIntros (Hε Hk Hamp) "Herr".
destruct (err_amp_power ε k) as n Hn; done|done|.
iInduction n as |m "IH" forall (ε Hε Hn Hk) "Herr".
- iDestruct (ec_contradict with "Herr") as *)
(* [local] Lemma ec_ind_simpl_external_aux (ε ε' k : R) P : 0 < ε → ε <= ε' -> 1 < k → ((↯ (k * ε) -∗ P) ∗ ↯ ε ⊢ P) → (↯ ε' ⊢ P). Proof. iIntros (Hε Hleq Hk Hamp) "Herr". destruct (err_amp_mult ε ε' k) as [n Hn]; auto. iInduction n as [|m] "IH" forall (ε ε' Hε Hleq Hn Hk Hamp) "Herr". - iDestruct (ec_contradict with "Herr") as %[]. simpl in Hn. lra. - replace (ε') with (ε + (ε' - ε)) by lra. iDestruct (ec_split with "Herr") as "[Herr1 Herr2]"; [lra | lra |]. iApply (Hamp with "[$Herr1 Herr2]"). iIntros "Herr". assert (k * ε = (k-1)*ε + ε) as ->; [lra |]. iDestruct (ec_split with "Herr") as "[Herr3 Herr4]"; [ real_solver | lra |]. iDestruct (ec_combine with "[$Herr2 $Herr3]") as "Herr". iDestruct (ec_combine with "[$Herr $Herr4]") as "Herr". iApply ("IH" $! ε with "[] [] [] [] [] Herr"); auto. + iPureIntro. replace (ε' - ε + (k-1) * ε + ε) with (ε' + (k-1) * ε) by lra. rewrite <- (Rplus_0_r ε) at 1. apply Rplus_le_compat; auto. apply Rmult_le_pos; lra. + iPureIntro. replace (ε' - ε + (k - 1) * ε + ε) with (ε' + (k - 1) * ε) by lra. replace (m * (k - 1) * ε + (ε' + (k - 1) * ε)) with ((m + 1) * (k - 1) * ε + ε') by lra. etrans; eauto. rewrite S_INR //. Qed. *)
(* Lemma ec_ind_simpl_external (ε k : R) P :
0 < ε →
1 < k →
((↯ (k * ε) -∗ P) ∗ ↯ ε ⊢ P) →
(↯ ε ⊢ P).
Proof.
iIntros (Hε HK Hamp).
eapply ec_ind_simpl_external_aux; eauto.
lra.
Qed. *)
(* [local] Lemma ec_ind_simpl_aux (ε ε' k : R) P : 0 < ε → ε <= ε' -> 1 < k → □ ((↯ (k * ε) -∗ P) ∗ ↯ ε -∗ P) ⊢ (↯ ε' -∗ P). Proof. iIntros (Hε Hleq Hk) "Hamp Herr".
destruct (err_amp_mult ε ε' k) as n Hn; auto.
iInduction n as |m "IH" forall (ε ε' Hε Hleq Hn Hk) "Hamp Herr".
- iDestruct (ec_contradict with "Herr") as *)
(* Lemma ec_ind_simpl (ε k : R) P :
0 < ε →
1 < k →
□((↯ (k * ε) -∗ P) ∗ ↯ ε -∗ P) ⊢
(↯ ε -∗ P).
Proof.
iIntros (Hε Hk) "Hamp Herr". iApply ec_ind_simpl_aux; eauto. lra. Qed. *)
(* Lemma ec_ind_incr (ε ε' k : R) P :
0 < ε →
ε < ε' →
1 < k →
□((↯ ε' -∗ P) ∗ ↯ ε -∗ P) ⊢
(↯ ε -∗ P).
Proof.
iIntros (Hε Hε' Hk) "Hamp Herr". iApply (ec_ind_simpl ε (ε'/ε) with "[Hamp]"); auto. - apply Rcomplements.Rlt_div_r; lra. - iModIntro. iIntros "(H & Herr)". iApply ("Hamp" with "[H $Herr]"). iIntros "Herr". iApply "H". rewrite /Rdiv Rmult_assoc Rinv_l; [|lra]. rewrite Rmult_1_r. iFrame. Qed. *)
(* (* TODO: can ec_ind_amp be derived from ec_ind_amp_external ? *)
Lemma ec_ind_amp (ε k : R) P :
0 < ε →
1 < k →
□ (∀ (ε' : R), ⌜0 < ε'⌝ -∗ □ (↯ (k * ε') -∗ P) -∗ ↯ ε' -∗ P) ⊢
(↯ ε -∗ P).
Proof.
iIntros (Hpos Hgt1) "Hamp Herr". destruct (err_amp_power ε k) as [n Hn]; [done|done|]. iInduction n as [|m] "IH" forall (ε Hpos Hn Hgt1) "Herr". - iDestruct (ec_contradict with "Herr") as %[]. simpl in Hn. lra. - iApply ("Hamp" with "[//] [] Herr"). iIntros "! Herr".
iApply ("IH" with " // Herr"); iPureIntro.
+ real_solver.
+ simpl in Hn. lra.
Qed. *)
Global Instance ecm_timeless r : Timeless (↯m r).
Proof. rewrite ecm_unseal /ecm_def. apply _. Qed.
Global Instance from_sep_ecm_combine r1 r2 :
FromSep (↯m (r1 + r2)) (↯m r1) (↯m r2) | 0.
Proof. rewrite /FromSep ecm_combine //. Qed.
Global Instance into_sep_ecm_add r1 r2 :
0 <= r1 → 0 <= r2 →
IntoSep (↯m (r1 + r2)) (↯m r1) (↯m r2) | 0.
Proof. rewrite /IntoSep. apply ecm_split. Qed.
Global Instance combine_sep_as_ecm_add r1 r2 :
CombineSepAs (↯m r1) (↯m r2) (↯m (r1 + r2)) | 0.
Proof. rewrite /CombineSepAs ecm_combine //. Qed.
End error_credit_theory.
Lemma ecm_alloc `{!ecmGpreS Σ} (n : nonnegreal) :
(* (n < 1)*) ⊢ |==> ∃ _ : ecmGS Σ, ecm_supply n ∗ ↯m n.
Proof.
(* iIntros (?). *)
rewrite ecm_unseal /ecm_def ecm_supply_unseal /ecm_supply_def.
iMod (own_alloc (● n ⋅ ◯ n)) as (γECM) "[H● H◯]".
- apply auth_both_valid_2.
+ compute. destruct n; simpl in *. lra.
+ apply nonnegreal_included; lra.
- pose (C := EcmGS _ _ γECM).
iModIntro. iExists C. by iFrame.
Qed.
#[global] Hint Resolve cond_nonneg : core.
ecm_supply x2 -∗ ↯m r1 -∗ |==> ∃ x1 x3, ⌜(x2 = x3 + x1)%NNR⌝ ∗ ⌜x1.(nonneg) = r1⌝ ∗ ecm_supply x3.
Proof.
iIntros "Hx2 Hr1".
iDestruct (ecm_supply_ecm_inv with "Hx2 Hr1") as %(x1 & x3 & -> & <-).
iDestruct "Hr1" as (x1') "[% Hx1]".
rewrite ecm_unseal /ecm_def ecm_supply_unseal /ecm_supply_def.
iMod (own_update_2 with "Hx2 Hx1") as "Hown".
{ eapply (auth_update_dealloc _ _ x3), nonnegreal_local_update.
- apply cond_nonneg.
- apply nnreal_ext =>/=. lra. }
iModIntro.
iExists _, _. iFrame. iSplit; [|done].
iPureIntro. apply nnreal_ext=>/=; lra.
Qed.
Lemma ecm_supply_increase (ε1 ε2 : nonnegreal) :
(* ε1 + ε2 < 1 → *)
ecm_supply ε1 -∗ |==> ecm_supply (ε1 + ε2)%NNR ∗ ↯m ε2.
Proof.
rewrite ecm_unseal /ecm_def.
rewrite ecm_supply_unseal /ecm_supply_def.
iIntros (* (?) *) "H".
iMod (own_update with "H") as "[$ $]"; [|done].
eapply auth_update_alloc.
apply (local_update_unital_discrete _ _ _ _) => z H1 H2.
split; [done|].
apply nnreal_ext. simpl.
rewrite Rplus_comm.
apply Rplus_eq_compat_l.
rewrite H2 /=. lra.
Qed.
Lemma ecm_weaken (r1 r2 : R) :
0 <= r2 <= r1 → ↯m r1 -∗ ↯m r2.
Proof.
iIntros (?) "Hr1".
assert (r1 = (r1 - r2) + r2) as -> by lra.
iDestruct (ecm_split with "Hr1") as "[? $]"; lra.
Qed.
Lemma ecm_eq x1 x2 :
x1 = x2 → ↯m x1 -∗ ↯m x2.
Proof. iIntros (->) "$". Qed.
Lemma ecm_supply_eq x1 x2 :
(x1.(nonneg) = x2.(nonneg)) → ecm_supply x1 -∗ ecm_supply x2.
Proof.
iIntros (?) "?".
replace x1 with x2; [iFrame|by apply nnreal_ext].
Qed.
(* Lemma ec_contradict (ε : R) :
1 <= ε → ↯ ε ⊢ False.
Proof.
iIntros (Hge1) "(?*)
Lemma ecm_valid (ε : R) : ↯m ε -∗ ⌜(0<=ε(* <1 *))%R⌝.
Proof.
iIntros "(%&<-&H)".
rewrite ecm_unseal /ecm_def.
iDestruct (own_valid with "H") as %?%auth_frag_valid_1.
destruct x. compute in H. simpl in *. iPureIntro. lra.
Qed.
#[local] Lemma err_amp_power ε k :
0 < ε →
1 < k →
∃ n, 1 <= ε * k ^ n.
Proof.
intros Hε Hk.
destruct (Lim_seq.is_lim_seq_geom_p k Hk (λ r, / ε <= r)) as [n Hn] => /=.
- exists (/ ε). real_solver.
- exists n.
apply (Rmult_le_reg_l (/ ε)).
+ apply Rinv_0_lt_compat, Hε.
+ rewrite -Rmult_assoc Rinv_l; [|lra].
rewrite Rmult_1_l Rmult_1_r. by apply Hn.
Qed.
#[local] Lemma err_amp_mult ε ε' k :
0 < ε →
ε <= ε' ->
1 < k →
(exists n:nat, 1 <= n*(k-1)*ε + ε').
Proof.
intros Hε Hleq Hk.
edestruct (Rcomplements.nfloor_ex (1/((k-1)*ε))) as [n [Hn1 Hn2]].
- apply Rmult_le_pos; [lra|].
left.
apply Rinv_0_lt_compat.
real_solver.
- exists (S n).
rewrite S_INR.
transitivity ((1 / ((k - 1) * ε)) * (k - 1) * ε + ε').
+ rewrite Rmult_assoc.
rewrite /Rdiv Rmult_1_l.
rewrite Rinv_l; [lra |].
assert (0<(k-1)*ε); real_solver.
+ apply Rplus_le_compat_r.
apply Rmult_le_compat_r; [lra|].
apply Rmult_le_compat_r; lra.
Qed.
(* Lemma ec_ind_amp_external (ε k : R) P :
0 < ε →
1 < k →
(∀ (ε' : R), 0 < ε' → □ (↯ (k * ε') -∗ P) ∗ ↯ ε' ⊢ P) →
(↯ ε ⊢ P).
Proof.
iIntros (Hε Hk Hamp) "Herr".
destruct (err_amp_power ε k) as n Hn; done|done|.
iInduction n as |m "IH" forall (ε Hε Hn Hk) "Herr".
- iDestruct (ec_contradict with "Herr") as *)
(* [local] Lemma ec_ind_simpl_external_aux (ε ε' k : R) P : 0 < ε → ε <= ε' -> 1 < k → ((↯ (k * ε) -∗ P) ∗ ↯ ε ⊢ P) → (↯ ε' ⊢ P). Proof. iIntros (Hε Hleq Hk Hamp) "Herr". destruct (err_amp_mult ε ε' k) as [n Hn]; auto. iInduction n as [|m] "IH" forall (ε ε' Hε Hleq Hn Hk Hamp) "Herr". - iDestruct (ec_contradict with "Herr") as %[]. simpl in Hn. lra. - replace (ε') with (ε + (ε' - ε)) by lra. iDestruct (ec_split with "Herr") as "[Herr1 Herr2]"; [lra | lra |]. iApply (Hamp with "[$Herr1 Herr2]"). iIntros "Herr". assert (k * ε = (k-1)*ε + ε) as ->; [lra |]. iDestruct (ec_split with "Herr") as "[Herr3 Herr4]"; [ real_solver | lra |]. iDestruct (ec_combine with "[$Herr2 $Herr3]") as "Herr". iDestruct (ec_combine with "[$Herr $Herr4]") as "Herr". iApply ("IH" $! ε with "[] [] [] [] [] Herr"); auto. + iPureIntro. replace (ε' - ε + (k-1) * ε + ε) with (ε' + (k-1) * ε) by lra. rewrite <- (Rplus_0_r ε) at 1. apply Rplus_le_compat; auto. apply Rmult_le_pos; lra. + iPureIntro. replace (ε' - ε + (k - 1) * ε + ε) with (ε' + (k - 1) * ε) by lra. replace (m * (k - 1) * ε + (ε' + (k - 1) * ε)) with ((m + 1) * (k - 1) * ε + ε') by lra. etrans; eauto. rewrite S_INR //. Qed. *)
(* Lemma ec_ind_simpl_external (ε k : R) P :
0 < ε →
1 < k →
((↯ (k * ε) -∗ P) ∗ ↯ ε ⊢ P) →
(↯ ε ⊢ P).
Proof.
iIntros (Hε HK Hamp).
eapply ec_ind_simpl_external_aux; eauto.
lra.
Qed. *)
(* [local] Lemma ec_ind_simpl_aux (ε ε' k : R) P : 0 < ε → ε <= ε' -> 1 < k → □ ((↯ (k * ε) -∗ P) ∗ ↯ ε -∗ P) ⊢ (↯ ε' -∗ P). Proof. iIntros (Hε Hleq Hk) "Hamp Herr".
destruct (err_amp_mult ε ε' k) as n Hn; auto.
iInduction n as |m "IH" forall (ε ε' Hε Hleq Hn Hk) "Hamp Herr".
- iDestruct (ec_contradict with "Herr") as *)
(* Lemma ec_ind_simpl (ε k : R) P :
0 < ε →
1 < k →
□((↯ (k * ε) -∗ P) ∗ ↯ ε -∗ P) ⊢
(↯ ε -∗ P).
Proof.
iIntros (Hε Hk) "Hamp Herr". iApply ec_ind_simpl_aux; eauto. lra. Qed. *)
(* Lemma ec_ind_incr (ε ε' k : R) P :
0 < ε →
ε < ε' →
1 < k →
□((↯ ε' -∗ P) ∗ ↯ ε -∗ P) ⊢
(↯ ε -∗ P).
Proof.
iIntros (Hε Hε' Hk) "Hamp Herr". iApply (ec_ind_simpl ε (ε'/ε) with "[Hamp]"); auto. - apply Rcomplements.Rlt_div_r; lra. - iModIntro. iIntros "(H & Herr)". iApply ("Hamp" with "[H $Herr]"). iIntros "Herr". iApply "H". rewrite /Rdiv Rmult_assoc Rinv_l; [|lra]. rewrite Rmult_1_r. iFrame. Qed. *)
(* (* TODO: can ec_ind_amp be derived from ec_ind_amp_external ? *)
Lemma ec_ind_amp (ε k : R) P :
0 < ε →
1 < k →
□ (∀ (ε' : R), ⌜0 < ε'⌝ -∗ □ (↯ (k * ε') -∗ P) -∗ ↯ ε' -∗ P) ⊢
(↯ ε -∗ P).
Proof.
iIntros (Hpos Hgt1) "Hamp Herr". destruct (err_amp_power ε k) as [n Hn]; [done|done|]. iInduction n as [|m] "IH" forall (ε Hpos Hn Hgt1) "Herr". - iDestruct (ec_contradict with "Herr") as %[]. simpl in Hn. lra. - iApply ("Hamp" with "[//] [] Herr"). iIntros "! Herr".
iApply ("IH" with " // Herr"); iPureIntro.
+ real_solver.
+ simpl in Hn. lra.
Qed. *)
Global Instance ecm_timeless r : Timeless (↯m r).
Proof. rewrite ecm_unseal /ecm_def. apply _. Qed.
Global Instance from_sep_ecm_combine r1 r2 :
FromSep (↯m (r1 + r2)) (↯m r1) (↯m r2) | 0.
Proof. rewrite /FromSep ecm_combine //. Qed.
Global Instance into_sep_ecm_add r1 r2 :
0 <= r1 → 0 <= r2 →
IntoSep (↯m (r1 + r2)) (↯m r1) (↯m r2) | 0.
Proof. rewrite /IntoSep. apply ecm_split. Qed.
Global Instance combine_sep_as_ecm_add r1 r2 :
CombineSepAs (↯m r1) (↯m r2) (↯m (r1 + r2)) | 0.
Proof. rewrite /CombineSepAs ecm_combine //. Qed.
End error_credit_theory.
Lemma ecm_alloc `{!ecmGpreS Σ} (n : nonnegreal) :
(* (n < 1)*) ⊢ |==> ∃ _ : ecmGS Σ, ecm_supply n ∗ ↯m n.
Proof.
(* iIntros (?). *)
rewrite ecm_unseal /ecm_def ecm_supply_unseal /ecm_supply_def.
iMod (own_alloc (● n ⋅ ◯ n)) as (γECM) "[H● H◯]".
- apply auth_both_valid_2.
+ compute. destruct n; simpl in *. lra.
+ apply nonnegreal_included; lra.
- pose (C := EcmGS _ _ γECM).
iModIntro. iExists C. by iFrame.
Qed.
#[global] Hint Resolve cond_nonneg : core.