Commit 45cd995f authored by Ralf Jung's avatar Ralf Jung

Deprecate dec_agree

Thanks to Robbert for fixing gen_heap
parent 4800d9e2
......@@ -48,7 +48,6 @@ algebra/base.v
algebra/dra.v
algebra/cofe_solver.v
algebra/agree.v
algebra/dec_agree.v
algebra/excl.v
algebra/iprod.v
algebra/frac.v
......
From iris.algebra Require Export cmra.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ _ !_ /.
Local Arguments pcore _ _ !_ /.
(* This is isomorphic to option, but has a very different RA structure. *)
Inductive dec_agree (A : Type) : Type :=
| DecAgree : A dec_agree A
| DecAgreeBot : dec_agree A.
Arguments DecAgree {_} _.
Arguments DecAgreeBot {_}.
Instance maybe_DecAgree {A} : Maybe (@DecAgree A) := λ x,
match x with DecAgree a => Some a | _ => None end.
Section dec_agree.
Context `{EqDecision A}.
Implicit Types a b : A.
Implicit Types x y : dec_agree A.
Instance dec_agree_valid : Valid (dec_agree A) := λ x,
if x is DecAgree _ then True else False.
Canonical Structure dec_agreeC : ofeT := leibnizC (dec_agree A).
Instance dec_agree_op : Op (dec_agree A) := λ x y,
match x, y with
| DecAgree a, DecAgree b => if decide (a = b) then DecAgree a else DecAgreeBot
| _, _ => DecAgreeBot
end.
Instance dec_agree_pcore : PCore (dec_agree A) := Some.
Definition dec_agree_ra_mixin : RAMixin (dec_agree A).
Proof.
apply ra_total_mixin; apply _ || eauto.
- intros [?|] [?|] [?|]; by repeat (simplify_eq/= || case_match).
- intros [?|] [?|]; by repeat (simplify_eq/= || case_match).
- intros [?|]; by repeat (simplify_eq/= || case_match).
- by intros [?|] [?|] ?.
Qed.
Canonical Structure dec_agreeR : cmraT :=
discreteR (dec_agree A) dec_agree_ra_mixin.
Global Instance dec_agree_total : CMRATotal dec_agreeR.
Proof. intros x. by exists x. Qed.
(* Some properties of this CMRA *)
Global Instance dec_agree_persistent (x : dec_agreeR) : Persistent x.
Proof. by constructor. Qed.
Lemma dec_agree_ne a b : a b DecAgree a DecAgree b = DecAgreeBot.
Proof. intros. by rewrite /= decide_False. Qed.
Lemma dec_agree_idemp (x : dec_agree A) : x x = x.
Proof. destruct x; by rewrite /= ?decide_True. Qed.
Lemma dec_agree_op_inv (x1 x2 : dec_agree A) : (x1 x2) x1 = x2.
Proof. destruct x1, x2; by repeat (simplify_eq/= || case_match). Qed.
Lemma DecAgree_included a b : DecAgree a DecAgree b a = b.
Proof.
split. intros [[c|] [=]%leibniz_equiv]. by simplify_option_eq. by intros ->.
Qed.
End dec_agree.
Arguments dec_agreeC : clear implicits.
Arguments dec_agreeR _ {_}.
From iris.algebra Require Import ofe.
From iris.algebra Require Import ofe cmra.
(* Old notation for backwards compatibility. *)
(* Deprecated 2016-11-22. Use ofeT instead. *)
Notation cofeT := ofeT (only parsing).
(* Deprecated 2016-12-09. Use agree instead. *)
(* The module is called dec_agree_deprecated because if it was just dec_agree,
it would still be imported by "From iris Import dec_agree", and people would
not notice they use sth. deprecated. *)
Module dec_agree_deprecated.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ _ !_ /.
Local Arguments pcore _ _ !_ /.
(* This is isomorphic to option, but has a very different RA structure. *)
Inductive dec_agree (A : Type) : Type :=
| DecAgree : A dec_agree A
| DecAgreeBot : dec_agree A.
Arguments DecAgree {_} _.
Arguments DecAgreeBot {_}.
Instance maybe_DecAgree {A} : Maybe (@DecAgree A) := λ x,
match x with DecAgree a => Some a | _ => None end.
Section dec_agree.
Context `{EqDecision A}.
Implicit Types a b : A.
Implicit Types x y : dec_agree A.
Instance dec_agree_valid : Valid (dec_agree A) := λ x,
if x is DecAgree _ then True else False.
Canonical Structure dec_agreeC : ofeT := leibnizC (dec_agree A).
Instance dec_agree_op : Op (dec_agree A) := λ x y,
match x, y with
| DecAgree a, DecAgree b => if decide (a = b) then DecAgree a else DecAgreeBot
| _, _ => DecAgreeBot
end.
Instance dec_agree_pcore : PCore (dec_agree A) := Some.
Definition dec_agree_ra_mixin : RAMixin (dec_agree A).
Proof.
apply ra_total_mixin; apply _ || eauto.
- intros [?|] [?|] [?|]; by repeat (simplify_eq/= || case_match).
- intros [?|] [?|]; by repeat (simplify_eq/= || case_match).
- intros [?|]; by repeat (simplify_eq/= || case_match).
- by intros [?|] [?|] ?.
Qed.
Canonical Structure dec_agreeR : cmraT :=
discreteR (dec_agree A) dec_agree_ra_mixin.
Global Instance dec_agree_total : CMRATotal dec_agreeR.
Proof. intros x. by exists x. Qed.
(* Some properties of this CMRA *)
Global Instance dec_agree_persistent (x : dec_agreeR) : Persistent x.
Proof. by constructor. Qed.
Lemma dec_agree_ne a b : a b DecAgree a DecAgree b = DecAgreeBot.
Proof. intros. by rewrite /= decide_False. Qed.
Lemma dec_agree_idemp (x : dec_agree A) : x x = x.
Proof. destruct x; by rewrite /= ?decide_True. Qed.
Lemma dec_agree_op_inv (x1 x2 : dec_agree A) : (x1 x2) x1 = x2.
Proof. destruct x1, x2; by repeat (simplify_eq/= || case_match). Qed.
Lemma DecAgree_included a b : DecAgree a DecAgree b a = b.
Proof.
split. intros [[c|] [=]%leibniz_equiv]. by simplify_option_eq. by intros ->.
Qed.
End dec_agree.
Arguments dec_agreeC : clear implicits.
Arguments dec_agreeR _ {_}.
End dec_agree_deprecated.
......@@ -21,6 +21,6 @@ Proof.
iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh".
{ apply: auth_auth_valid. exact: to_gen_heap_valid. }
iModIntro. iExists (λ σ, own γ ( to_gen_heap σ)); iFrame.
set (Hheap := GenHeapG loc val Σ _ _ _ _ γ).
set (Hheap := GenHeapG loc val Σ _ _ _ γ).
iApply (Hwp (HeapG _ _ _)).
Qed.
From iris.algebra Require Import auth gmap frac dec_agree.
From iris.algebra Require Import auth gmap frac agree.
From iris.base_logic.lib Require Export own.
From iris.base_logic.lib Require Import fractional.
From iris.proofmode Require Import tactics.
Import uPred.
Definition gen_heapUR (L V : Type) `{Countable L, EqDecision V} : ucmraT :=
gmapUR L (prodR fracR (dec_agreeR V)).
Definition to_gen_heap `{Countable L, EqDecision V} : gmap L V gen_heapUR L V :=
fmap (λ v, (1%Qp, DecAgree v)).
Definition gen_heapUR (L V : Type) `{Countable L} : ucmraT :=
gmapUR L (prodR fracR (agreeR (leibnizC V))).
Definition to_gen_heap {L V} `{Countable L} : gmap L V gen_heapUR L V :=
fmap (λ v, (1%Qp, to_agree (v : leibnizC V))).
(** The CMRA we need. *)
Class gen_heapG (L V : Type) (Σ : gFunctors)
`{Countable L, EqDecision V} := GenHeapG {
Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
gen_heap_inG :> inG Σ (authR (gen_heapUR L V));
gen_heap_name : gname
}.
Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L, EqDecision V} :=
Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} :=
{ gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V)) }.
Definition gen_heapΣ (L V : Type) `{Countable L, EqDecision V} : gFunctors :=
Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors :=
#[GFunctor (constRF (authR (gen_heapUR L V)))].
Instance subG_gen_heapPreG {Σ} `{Countable L, EqDecision V} :
Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
subG (gen_heapΣ L V) Σ gen_heapPreG L V Σ.
Proof. intros ?%subG_inG; split; apply _. Qed.
......@@ -33,7 +32,7 @@ Section definitions.
own gen_heap_name ( to_gen_heap σ).
Definition mapsto_def (l : L) (q : Qp) (v: V) : iProp Σ :=
own gen_heap_name ( {[ l := (q, DecAgree v) ]}).
own gen_heap_name ( {[ l := (q, to_agree (v : leibnizC V)) ]}).
Definition mapsto_aux : { x | x = @mapsto_def }. by eexists. Qed.
Definition mapsto := proj1_sig mapsto_aux.
Definition mapsto_eq : @mapsto = @mapsto_def := proj2_sig mapsto_aux.
......@@ -60,14 +59,14 @@ Section gen_heap.
Lemma lookup_to_gen_heap_None σ l : σ !! l = None to_gen_heap σ !! l = None.
Proof. by rewrite /to_gen_heap lookup_fmap=> ->. Qed.
Lemma gen_heap_singleton_included σ l q v :
{[l := (q, DecAgree v)]} to_gen_heap σ σ !! l = Some v.
{[l := (q, to_agree v)]} to_gen_heap σ σ !! l = Some v.
Proof.
rewrite singleton_included=> -[[q' av] [/leibniz_equiv_iff Hl Hqv]].
move: Hl. rewrite /to_gen_heap lookup_fmap fmap_Some=> -[v' [Hl [??]]]; subst.
by move: Hqv=> /Some_pair_included_total_2 [_ /DecAgree_included ->].
rewrite singleton_included=> -[[q' av] []].
rewrite /to_gen_heap lookup_fmap fmap_Some_equiv => -[v' [Hl [/= -> ->]]].
move=> /Some_pair_included_total_2 [_] /to_agree_included /leibniz_equiv_iff -> //.
Qed.
Lemma to_gen_heap_insert l v σ :
to_gen_heap (<[l:=v]> σ) = <[l:=(1%Qp, DecAgree v)]> (to_gen_heap σ).
to_gen_heap (<[l:=v]> σ) = <[l:=(1%Qp, to_agree (v:leibnizC V))]> (to_gen_heap σ).
Proof. by rewrite /to_gen_heap fmap_insert. Qed.
(** General properties of mapsto *)
......@@ -76,7 +75,7 @@ Section gen_heap.
Global Instance mapsto_fractional l v : Fractional (λ q, l {q} v)%I.
Proof.
intros p q. by rewrite mapsto_eq -own_op -auth_frag_op
op_singleton pair_op dec_agree_idemp.
op_singleton pair_op agree_idemp.
Qed.
Global Instance mapsto_as_fractional l q v :
AsFractional (l {q} v) (λ q, l {q} v)%I q.
......@@ -86,7 +85,7 @@ Section gen_heap.
Proof.
rewrite mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
f_equiv=> /auth_own_valid /=. rewrite op_singleton singleton_valid pair_op.
by move=> [_ /= /dec_agree_op_inv [?]].
by intros [_ ?%agree_op_inv%(inj to_agree)%leibniz_equiv].
Qed.
Global Instance heap_ex_mapsto_fractional l : Fractional (λ q, l {q} -)%I.
......@@ -105,8 +104,7 @@ Section gen_heap.
rewrite mapsto_eq /mapsto_def own_valid !discrete_valid.
by apply pure_mono=> /auth_own_valid /singleton_valid [??].
Qed.
Lemma mapsto_valid_2 l q1 q2 v1 v2 :
l {q1} v1 l {q2} v2 (q1 + q2)%Qp.
Lemma mapsto_valid_2 l q1 q2 v1 v2 : l {q1} v1 l {q2} v2 (q1 + q2)%Qp.
Proof.
iIntros "[H1 H2]". iDestruct (mapsto_agree with "[$H1 $H2]") as %->.
iApply (mapsto_valid l _ v2). by iFrame.
......@@ -118,7 +116,7 @@ Section gen_heap.
iIntros (?) "Hσ". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
iMod (own_update with "Hσ") as "[Hσ Hl]".
{ eapply auth_update_alloc,
(alloc_singleton_local_update _ _ (1%Qp, DecAgree v))=> //.
(alloc_singleton_local_update _ _ (1%Qp, to_agree (v:leibnizC _)))=> //.
by apply lookup_to_gen_heap_None. }
iModIntro. rewrite to_gen_heap_insert. iFrame.
Qed.
......@@ -138,7 +136,7 @@ Section gen_heap.
as %[Hl%gen_heap_singleton_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
{ eapply auth_update, singleton_local_update,
(exclusive_local_update _ (1%Qp, DecAgree v2))=> //.
(exclusive_local_update _ (1%Qp, to_agree (v2:leibnizC _)))=> //.
by rewrite /to_gen_heap lookup_fmap Hl. }
iModIntro. rewrite to_gen_heap_insert. iFrame.
Qed.
......
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang.
From iris.algebra Require Import excl dec_agree csum.
From iris.algebra Require Import excl agree csum.
From iris.heap_lang Require Import assert proofmode notation.
From iris.proofmode Require Import tactics.
......@@ -19,9 +19,9 @@ Definition one_shot_example : val := λ: <>,
end
end)).
Definition one_shotR := csumR (exclR unitC) (dec_agreeR Z).
Definition one_shotR := csumR (exclR unitC) (agreeR ZC).
Definition Pending : one_shotR := (Cinl (Excl ()) : one_shotR).
Definition Shot (n : Z) : one_shotR := (Cinr (DecAgree n) : one_shotR).
Definition Shot (n : Z) : one_shotR := (Cinr (to_agree n) : one_shotR).
Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
Definition one_shotΣ : gFunctors := #[GFunctor (constRF one_shotR)].
......@@ -76,8 +76,8 @@ Proof.
{ iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as %?. }
wp_load.
iCombine "Hγ" "Hγ'" as "Hγ".
iDestruct (own_valid with "Hγ") as %[=->]%dec_agree_op_inv.
iMod ("Hclose" with "[Hl]") as "_".
iDestruct (own_valid with "Hγ") as %?%agree_op_inv%to_agree_inj.
fold_leibniz. subst. iMod ("Hclose" with "[Hl]") as "_".
{ iNext; iRight; by eauto. }
iModIntro. wp_match. iApply wp_assert. wp_op=>?; simplify_eq/=; eauto.
Qed.
......
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