Commit 2418fccd authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ralf/frac_auth' into 'master'

change frac_auth notation

See merge request iris/iris!259
parents 265c2a13 94cfebc2
Pipeline #17370 passed with stage
in 14 minutes and 16 seconds
......@@ -143,6 +143,7 @@ Changes in Coq:
* Add the camera `ufrac` for unbounded fractions (i.e. without fractions that
can be `> 1`) and the camera `ufrac_auth` for a variant of the authoritative
fractional camera (`frac_auth`) with unbounded fractions.
* Changed `frac_auth` notation from `●!`/`◯!` to `●F`/`◯F`.
## Iris 3.1.0 (released 2017-12-19)
......
......@@ -24,9 +24,9 @@ Typeclasses Opaque frac_auth_auth frac_auth_frag.
Instance: Params (@frac_auth_auth) 1 := {}.
Instance: Params (@frac_auth_frag) 2 := {}.
Notation "●! a" := (frac_auth_auth a) (at level 10).
Notation "◯!{ q } a" := (frac_auth_frag q a) (at level 10, format "◯!{ q } a").
Notation "◯! a" := (frac_auth_frag 1 a) (at level 10).
Notation "●F a" := (frac_auth_auth a) (at level 10).
Notation "◯F{ q } a" := (frac_auth_frag q a) (at level 10, format "◯F{ q } a").
Notation "◯F a" := (frac_auth_frag 1 a) (at level 10).
Section frac_auth.
Context {A : cmraT}.
......@@ -41,79 +41,79 @@ Section frac_auth.
Global Instance frac_auth_frag_proper q : Proper (() ==> ()) (@frac_auth_frag A q).
Proof. solve_proper. Qed.
Global Instance frac_auth_auth_discrete a : Discrete a Discrete (! a).
Global Instance frac_auth_auth_discrete a : Discrete a Discrete (F a).
Proof. intros; apply auth_auth_discrete; [apply Some_discrete|]; apply _. Qed.
Global Instance frac_auth_frag_discrete q a : Discrete a Discrete (!{q} a).
Global Instance frac_auth_frag_discrete q a : Discrete a Discrete (F{q} a).
Proof. intros; apply auth_frag_discrete, Some_discrete; apply _. Qed.
Lemma frac_auth_validN n a : {n} a {n} (! a ! a).
Lemma frac_auth_validN n a : {n} a {n} (F a F a).
Proof. by rewrite auth_both_validN. Qed.
Lemma frac_auth_valid a : a (! a ! a).
Lemma frac_auth_valid a : a (F a F a).
Proof. intros. by apply auth_both_valid_2. Qed.
Lemma frac_auth_agreeN n a b : {n} (! a ! b) a {n} b.
Lemma frac_auth_agreeN n a b : {n} (F a F b) a {n} b.
Proof.
rewrite auth_both_validN /= => -[Hincl Hvalid].
by move: Hincl=> /Some_includedN_exclusive /(_ Hvalid ) [??].
Qed.
Lemma frac_auth_agree a b : (! a ! b) a b.
Lemma frac_auth_agree a b : (F a F b) a b.
Proof.
intros. apply equiv_dist=> n. by apply frac_auth_agreeN, cmra_valid_validN.
Qed.
Lemma frac_auth_agreeL `{!LeibnizEquiv A} a b : (! a ! b) a = b.
Lemma frac_auth_agreeL `{!LeibnizEquiv A} a b : (F a F b) a = b.
Proof. intros. by apply leibniz_equiv, frac_auth_agree. Qed.
Lemma frac_auth_includedN n q a b : {n} (! a !{q} b) Some b {n} Some a.
Lemma frac_auth_includedN n q a b : {n} (F a F{q} b) Some b {n} Some a.
Proof. by rewrite auth_both_validN /= => -[/Some_pair_includedN [_ ?] _]. Qed.
Lemma frac_auth_included `{CmraDiscrete A} q a b :
(! a !{q} b) Some b Some a.
(F a F{q} b) Some b Some a.
Proof. by rewrite auth_both_valid /= => -[/Some_pair_included [_ ?] _]. Qed.
Lemma frac_auth_includedN_total `{CmraTotal A} n q a b :
{n} (! a !{q} b) b {n} a.
{n} (F a F{q} b) b {n} a.
Proof. intros. by eapply Some_includedN_total, frac_auth_includedN. Qed.
Lemma frac_auth_included_total `{CmraDiscrete A, CmraTotal A} q a b :
(! a !{q} b) b a.
(F a F{q} b) b a.
Proof. intros. by eapply Some_included_total, frac_auth_included. Qed.
Lemma frac_auth_auth_validN n a : {n} (! a) {n} a.
Lemma frac_auth_auth_validN n a : {n} (F a) {n} a.
Proof.
rewrite auth_auth_frac_validN Some_validN. split.
by intros [?[]]. intros. by split.
Qed.
Lemma frac_auth_auth_valid a : (! a) a.
Lemma frac_auth_auth_valid a : (F a) a.
Proof. rewrite !cmra_valid_validN. by setoid_rewrite frac_auth_auth_validN. Qed.
Lemma frac_auth_frag_validN n q a : {n} (!{q} a) {n} q {n} a.
Lemma frac_auth_frag_validN n q a : {n} (F{q} a) {n} q {n} a.
Proof. done. Qed.
Lemma frac_auth_frag_valid q a : (!{q} a) q a.
Lemma frac_auth_frag_valid q a : (F{q} a) q a.
Proof. done. Qed.
Lemma frac_auth_frag_op q1 q2 a1 a2 : !{q1+q2} (a1 a2) !{q1} a1 !{q2} a2.
Lemma frac_auth_frag_op q1 q2 a1 a2 : F{q1+q2} (a1 a2) F{q1} a1 F{q2} a2.
Proof. done. Qed.
Lemma frac_auth_frag_validN_op_1_l n q a b : {n} (!{1} a !{q} b) False.
Lemma frac_auth_frag_validN_op_1_l n q a b : {n} (F{1} a F{q} b) False.
Proof. rewrite -frac_auth_frag_op frac_auth_frag_validN=> -[/exclusiveN_l []]. Qed.
Lemma frac_auth_frag_valid_op_1_l q a b : (!{1} a !{q} b) False.
Lemma frac_auth_frag_valid_op_1_l q a b : (F{1} a F{q} b) False.
Proof. rewrite -frac_auth_frag_op frac_auth_frag_valid=> -[/exclusive_l []]. Qed.
Global Instance is_op_frac_auth (q q1 q2 : frac) (a a1 a2 : A) :
IsOp q q1 q2 IsOp a a1 a2 IsOp' (!{q} a) (!{q1} a1) (!{q2} a2).
IsOp q q1 q2 IsOp a a1 a2 IsOp' (F{q} a) (F{q1} a1) (F{q2} a2).
Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.
Global Instance is_op_frac_auth_core_id (q q1 q2 : frac) (a : A) :
CoreId a IsOp q q1 q2 IsOp' (!{q} a) (!{q1} a) (!{q2} a).
CoreId a IsOp q q1 q2 IsOp' (F{q} a) (F{q1} a) (F{q2} a).
Proof.
rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
by rewrite -frac_auth_frag_op -core_id_dup.
Qed.
Lemma frac_auth_update q a b a' b' :
(a,b) ~l~> (a',b') ! a !{q} b ~~> ! a' !{q} b'.
(a,b) ~l~> (a',b') F a F{q} b ~~> F a' F{q} b'.
Proof.
intros. by apply auth_update, option_local_update, prod_local_update_2.
Qed.
Lemma frac_auth_update_1 a b a' : a' ! a ! b ~~> ! a' ! a'.
Lemma frac_auth_update_1 a b a' : a' F a F b ~~> F a' F a'.
Proof.
intros. by apply auth_update, option_local_update, exclusive_local_update.
Qed.
......
......@@ -97,13 +97,13 @@ Section contrib_spec.
Context `{!heapG Σ, !ccounterG Σ} (N : namespace).
Definition ccounter_inv (γ : gname) (l : loc) : iProp Σ :=
( n, own γ (! n) l #n)%I.
( n, own γ (F n) l #n)%I.
Definition ccounter_ctx (γ : gname) (l : loc) : iProp Σ :=
inv N (ccounter_inv γ l).
Definition ccounter (γ : gname) (q : frac) (n : nat) : iProp Σ :=
own γ (!{q} n).
own γ (F{q} n).
(** The main proofs. *)
Lemma ccounter_op γ q1 q2 n1 n2 :
......@@ -115,7 +115,7 @@ Section contrib_spec.
{{{ γ l, RET #l; ccounter_ctx γ l ccounter γ 1 0 }}}.
Proof.
iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
iMod (own_alloc (! O%nat ! 0%nat)) as (γ) "[Hγ Hγ']";
iMod (own_alloc (F O%nat F 0%nat)) as (γ) "[Hγ Hγ']";
first by apply auth_both_valid.
iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
{ iNext. iExists 0%nat. by iFrame. }
......
Markdown is supported
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