Commit 4516513e authored by Simon Friis Vindum's avatar Simon Friis Vindum
Browse files

Separate module for number RAs, box max_nat, absorb for min_nat

parent a241bf9d
......@@ -14,6 +14,7 @@ theories/algebra/cmra.v
theories/algebra/big_op.v
theories/algebra/cmra_big_op.v
theories/algebra/sts.v
theories/algebra/numbers.v
theories/algebra/auth.v
theories/algebra/gmap.v
theories/algebra/ofe.v
......
......@@ -1054,137 +1054,6 @@ Section empty.
Proof. by constructor. Qed.
End empty.
(** ** Natural numbers *)
Section nat.
Instance nat_valid : Valid nat := λ x, True.
Instance nat_validN : ValidN nat := λ n x, True.
Instance nat_pcore : PCore nat := λ x, Some 0.
Instance nat_op : Op nat := plus.
Definition nat_op_plus x y : x y = x + y := eq_refl.
Lemma nat_included (x y : nat) : x y x y.
Proof. by rewrite nat_le_sum. Qed.
Lemma nat_ra_mixin : RAMixin nat.
Proof.
apply ra_total_mixin; try by eauto.
- solve_proper.
- intros x y z. apply Nat.add_assoc.
- intros x y. apply Nat.add_comm.
- by exists 0.
Qed.
Canonical Structure natR : cmraT := discreteR nat nat_ra_mixin.
Global Instance nat_cmra_discrete : CmraDiscrete natR.
Proof. apply discrete_cmra_discrete. Qed.
Instance nat_unit : Unit nat := 0.
Lemma nat_ucmra_mixin : UcmraMixin nat.
Proof. split; apply _ || done. Qed.
Canonical Structure natUR : ucmraT := UcmraT nat nat_ucmra_mixin.
Global Instance nat_cancelable (x : nat) : Cancelable x.
Proof. by intros ???? ?%Nat.add_cancel_l. Qed.
End nat.
(** ** Natural numbers with [max] as the operation. *)
Definition mnat := nat.
Section mnat.
Instance mnat_unit : Unit mnat := 0.
Instance mnat_valid : Valid mnat := λ x, True.
Instance mnat_validN : ValidN mnat := λ n x, True.
Instance mnat_pcore : PCore mnat := Some.
Instance mnat_op : Op mnat := Nat.max.
Definition mnat_op_max x y : x y = x `max` y := eq_refl.
Lemma mnat_included (x y : mnat) : x y x y.
Proof.
split.
- intros [z ->]; unfold op, mnat_op; lia.
- exists y. by symmetry; apply Nat.max_r.
Qed.
Lemma mnat_ra_mixin : RAMixin mnat.
Proof.
apply ra_total_mixin; apply _ || eauto.
- intros x y z. apply Nat.max_assoc.
- intros x y. apply Nat.max_comm.
- intros x. apply Max.max_idempotent.
Qed.
Canonical Structure mnatR : cmraT := discreteR mnat mnat_ra_mixin.
Global Instance mnat_cmra_discrete : CmraDiscrete mnatR.
Proof. apply discrete_cmra_discrete. Qed.
Lemma mnat_ucmra_mixin : UcmraMixin mnat.
Proof. split; apply _ || done. Qed.
Canonical Structure mnatUR : ucmraT := UcmraT mnat mnat_ucmra_mixin.
Global Instance mnat_core_id (x : mnat) : CoreId x.
Proof. by constructor. Qed.
End mnat.
(** ** Natural numbers with [min] as the operation. *)
Record min_nat := MinNat { min_nat_car :> nat }.
Canonical Structure min_natO := leibnizO min_nat.
Section min_nat.
Instance min_nat_valid : Valid min_nat := λ x, True.
Instance min_nat_validN : ValidN min_nat := λ n x, True.
Instance min_nat_pcore : PCore min_nat := Some.
Instance min_nat_op : Op min_nat := λ n m, MinNat (n `min` m).
Definition min_nat_op_min x y : MinNat x MinNat y = MinNat (x `min` y) := eq_refl.
Lemma min_nat_included (x y : min_nat) : x y (min_nat_car x) (min_nat_car y).
Proof.
split.
- intros [z ->]. simpl. lia.
- exists y. rewrite /op /min_nat_op. rewrite Nat.min_r; last lia. by destruct y.
Qed.
Lemma min_nat_ra_mixin : RAMixin min_nat.
Proof.
apply ra_total_mixin; apply _ || eauto.
- intros [x] [y] [z]. repeat rewrite min_nat_op_min. by rewrite Nat.min_assoc.
- intros [x] [y]. by rewrite min_nat_op_min Nat.min_comm.
- intros [x]. by rewrite min_nat_op_min Min.min_idempotent.
Qed.
Canonical Structure min_natR : cmraT := discreteR min_nat min_nat_ra_mixin.
Global Instance min_nat_cmra_discrete : CmraDiscrete min_natR.
Proof. apply discrete_cmra_discrete. Qed.
Global Instance min_nat_core_id (x : min_nat) : CoreId x.
Proof. by constructor. Qed.
End min_nat.
(** ** Positive integers. *)
Section positive.
Instance pos_valid : Valid positive := λ x, True.
Instance pos_validN : ValidN positive := λ n x, True.
Instance pos_pcore : PCore positive := λ x, None.
Instance pos_op : Op positive := Pos.add.
Definition pos_op_plus x y : x y = (x + y)%positive := eq_refl.
Lemma pos_included (x y : positive) : x y (x < y)%positive.
Proof. by rewrite Plt_sum. Qed.
Lemma pos_ra_mixin : RAMixin positive.
Proof.
split; try by eauto.
- by intros ??? ->.
- intros ???. apply Pos.add_assoc.
- intros ??. apply Pos.add_comm.
Qed.
Canonical Structure positiveR : cmraT := discreteR positive pos_ra_mixin.
Global Instance pos_cmra_discrete : CmraDiscrete positiveR.
Proof. apply discrete_cmra_discrete. Qed.
Global Instance pos_cancelable (x : positive) : Cancelable x.
Proof. intros n y z ??. by eapply Pos.add_reg_l, leibniz_equiv. Qed.
Global Instance pos_id_free (x : positive) : IdFree x.
Proof.
intros y ??. apply (Pos.add_no_neutral x y). rewrite Pos.add_comm.
by apply leibniz_equiv.
Qed.
End positive.
(** ** Product *)
Section prod.
Context {A B : cmraT}.
......
From iris.algebra Require Export cmra.
From iris.algebra Require Export cmra numbers.
Set Default Proof Using "Type".
(** * Local updates *)
......@@ -198,9 +198,11 @@ Proof.
compute -[minus plus]; lia.
Qed.
Lemma mnat_local_update (x y x' : mnatUR) :
x x' (x,y) ~l~> (x',x').
Lemma max_nat_local_update (x y x' : max_natUR) :
max_nat_car x max_nat_car x' (x,y) ~l~> (x',x').
Proof.
intros ??; apply local_update_unital_discrete=> z _.
compute -[max]; lia.
move: x y x' => [x] [y] [y'] /= ??.
apply local_update_unital_discrete=> [[z]] _.
rewrite 2!max_nat_op_max. inversion 1.
split; first done. apply f_equal. lia.
Qed.
From iris.algebra Require Export cmra.
(** ** Natural numbers *)
Section nat.
Instance nat_valid : Valid nat := λ x, True.
Instance nat_validN : ValidN nat := λ n x, True.
Instance nat_pcore : PCore nat := λ x, Some 0.
Instance nat_op : Op nat := plus.
Definition nat_op_plus x y : x y = x + y := eq_refl.
Lemma nat_included (x y : nat) : x y x y.
Proof. by rewrite nat_le_sum. Qed.
Lemma nat_ra_mixin : RAMixin nat.
Proof.
apply ra_total_mixin; try by eauto.
- solve_proper.
- intros x y z. apply Nat.add_assoc.
- intros x y. apply Nat.add_comm.
- by exists 0.
Qed.
Canonical Structure natR : cmraT := discreteR nat nat_ra_mixin.
Global Instance nat_cmra_discrete : CmraDiscrete natR.
Proof. apply discrete_cmra_discrete. Qed.
Instance nat_unit : Unit nat := 0.
Lemma nat_ucmra_mixin : UcmraMixin nat.
Proof. split; apply _ || done. Qed.
Canonical Structure natUR : ucmraT := UcmraT nat nat_ucmra_mixin.
Global Instance nat_cancelable (x : nat) : Cancelable x.
Proof. by intros ???? ?%Nat.add_cancel_l. Qed.
End nat.
(** ** Natural numbers with [max] as the operation. *)
Record max_nat := MaxNat { max_nat_car : nat }.
Canonical Structure max_natO := leibnizO max_nat.
Section max_nat.
Instance max_nat_unit : Unit max_nat := MaxNat 0.
Instance max_nat_valid : Valid max_nat := λ x, True.
Instance max_nat_validN : ValidN max_nat := λ n x, True.
Instance max_nat_pcore : PCore max_nat := Some.
Instance max_nat_op : Op max_nat := λ n m, MaxNat (max_nat_car n `max` max_nat_car m).
Definition max_nat_op_max x y : MaxNat x MaxNat y = MaxNat (x `max` y) := eq_refl.
Lemma max_nat_included x y : x y max_nat_car x max_nat_car y.
Proof.
split.
- intros [z ->]. simpl. lia.
- exists y. rewrite /op /max_nat_op. rewrite Nat.max_r; last lia. by destruct y.
Qed.
Lemma max_nat_ra_mixin : RAMixin max_nat.
Proof.
apply ra_total_mixin; apply _ || eauto.
- intros [x] [y] [z]. repeat rewrite max_nat_op_max. by rewrite Nat.max_assoc.
- intros [x] [y]. by rewrite max_nat_op_max Nat.max_comm.
- intros [x]. by rewrite max_nat_op_max Max.max_idempotent.
Qed.
Canonical Structure max_natR : cmraT := discreteR max_nat max_nat_ra_mixin.
Global Instance max_nat_cmra_discrete : CmraDiscrete max_natR.
Proof. apply discrete_cmra_discrete. Qed.
Lemma max_nat_ucmra_mixin : UcmraMixin max_nat.
Proof. split; try apply _ || done. intros [x]. done. Qed.
Canonical Structure max_natUR : ucmraT := UcmraT max_nat max_nat_ucmra_mixin.
Global Instance max_nat_core_id (x : max_nat) : CoreId x.
Proof. by constructor. Qed.
End max_nat.
(** ** Natural numbers with [min] as the operation. *)
Record min_nat := MinNat { min_nat_car : nat }.
Canonical Structure min_natO := leibnizO min_nat.
Section min_nat.
Instance min_nat_valid : Valid min_nat := λ x, True.
Instance min_nat_validN : ValidN min_nat := λ n x, True.
Instance min_nat_pcore : PCore min_nat := Some.
Instance min_nat_op : Op min_nat := λ n m, MinNat (min_nat_car n `min` min_nat_car m).
Definition min_nat_op_min x y : MinNat x MinNat y = MinNat (x `min` y) := eq_refl.
Lemma min_nat_included (x y : min_nat) : x y min_nat_car y min_nat_car x.
Proof.
split.
- intros [z ->]. simpl. lia.
- exists y. rewrite /op /min_nat_op. rewrite Nat.min_r; last lia. by destruct y.
Qed.
Lemma min_nat_ra_mixin : RAMixin min_nat.
Proof.
apply ra_total_mixin; apply _ || eauto.
- intros [x] [y] [z]. repeat rewrite min_nat_op_min. by rewrite Nat.min_assoc.
- intros [x] [y]. by rewrite min_nat_op_min Nat.min_comm.
- intros [x]. by rewrite min_nat_op_min Min.min_idempotent.
Qed.
Canonical Structure min_natR : cmraT := discreteR min_nat min_nat_ra_mixin.
Global Instance min_nat_cmra_discrete : CmraDiscrete min_natR.
Proof. apply discrete_cmra_discrete. Qed.
Global Instance min_nat_core_id (x : min_nat) : CoreId x.
Proof. by constructor. Qed.
Global Instance : LeftAbsorb (=) (MinNat 0) ().
Proof. done. Qed.
Global Instance : RightAbsorb (=) (MinNat 0) ().
Proof. intros [x]. by rewrite min_nat_op_min Min.min_0_r. Qed.
End min_nat.
(** ** Positive integers. *)
Section positive.
Instance pos_valid : Valid positive := λ x, True.
Instance pos_validN : ValidN positive := λ n x, True.
Instance pos_pcore : PCore positive := λ x, None.
Instance pos_op : Op positive := Pos.add.
Definition pos_op_plus x y : x y = (x + y)%positive := eq_refl.
Lemma pos_included (x y : positive) : x y (x < y)%positive.
Proof. by rewrite Plt_sum. Qed.
Lemma pos_ra_mixin : RAMixin positive.
Proof.
split; try by eauto.
- by intros ??? ->.
- intros ???. apply Pos.add_assoc.
- intros ??. apply Pos.add_comm.
Qed.
Canonical Structure positiveR : cmraT := discreteR positive pos_ra_mixin.
Global Instance pos_cmra_discrete : CmraDiscrete positiveR.
Proof. apply discrete_cmra_discrete. Qed.
Global Instance pos_cancelable (x : positive) : Cancelable x.
Proof. intros n y z ??. by eapply Pos.add_reg_l, leibniz_equiv. Qed.
Global Instance pos_id_free (x : positive) : IdFree x.
Proof.
intros y ??. apply (Pos.add_no_neutral x y). rewrite Pos.add_comm.
by apply leibniz_equiv.
Qed.
End positive.
From iris.algebra Require Export cmra.
From iris.algebra Require Export cmra numbers.
From iris.proofmode Require Export classes.
(* There are various versions of [IsOp] with different modes:
......
......@@ -13,8 +13,8 @@ Definition incr : val := rec: "incr" "l" :=
Definition read : val := λ: "l", !"l".
(** Monotone counter *)
Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR mnatUR) }.
Definition mcounterΣ : gFunctors := #[GFunctor (authR mnatUR)].
Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR max_natUR) }.
Definition mcounterΣ : gFunctors := #[GFunctor (authR max_natUR)].
Instance subG_mcounterΣ {Σ} : subG mcounterΣ Σ mcounterG Σ.
Proof. solve_inG. Qed.
......@@ -23,10 +23,10 @@ Section mono_proof.
Context `{!heapG Σ, !mcounterG Σ} (N : namespace).
Definition mcounter_inv (γ : gname) (l : loc) : iProp Σ :=
n, own γ ( (n : mnat)) l #n.
n, own γ ( (MaxNat n)) l #n.
Definition mcounter (l : loc) (n : nat) : iProp Σ :=
γ, inv N (mcounter_inv γ l) own γ ( (n : mnat)).
γ, inv N (mcounter_inv γ l) own γ ( (MaxNat n)).
(** The main proofs. *)
Global Instance mcounter_persistent l n : Persistent (mcounter l n).
......@@ -36,7 +36,7 @@ Section mono_proof.
{{{ True }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
Proof.
iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
iMod (own_alloc ( (O:mnat) (O:mnat))) as (γ) "[Hγ Hγ']";
iMod (own_alloc ( (MaxNat O) (MaxNat O))) as (γ) "[Hγ Hγ']";
first by apply auth_both_valid.
iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
{ iNext. iExists 0. by iFrame. }
......@@ -54,15 +54,15 @@ Section mono_proof.
iInv N as (c') ">[Hγ Hl]".
destruct (decide (c' = c)) as [->|].
- iDestruct (own_valid_2 with "Hγ Hγf")
as %[?%mnat_included _]%auth_both_valid.
as %[?%max_nat_included _]%auth_both_valid.
iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply auth_update, (mnat_local_update _ _ (S c)); auto. }
{ apply auth_update, (max_nat_local_update _ _ (MaxNat (S c))). simpl. auto. }
wp_cmpxchg_suc. iModIntro. iSplitL "Hl Hγ".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
wp_pures. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
iApply (own_mono with "Hγf").
(* FIXME: FIXME(Coq #6294): needs new unification *)
apply: auth_frag_mono. by apply mnat_included, le_n_S.
apply: auth_frag_mono. by apply max_nat_included, le_n_S.
- wp_cmpxchg_fail; first (by intros [= ?%Nat2Z.inj]). iModIntro.
iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
wp_pures. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
......@@ -76,9 +76,9 @@ Section mono_proof.
rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]".
wp_load.
iDestruct (own_valid_2 with "Hγ Hγf")
as %[?%mnat_included _]%auth_both_valid.
as %[?%max_nat_included _]%auth_both_valid.
iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply auth_update, (mnat_local_update _ _ c); auto. }
{ apply auth_update, (max_nat_local_update _ _ (MaxNat c)); auto. }
iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
iApply ("HΦ" with "[-]"). rewrite /mcounter; eauto 10.
Qed.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment