Commit b8172744 authored by Hai Dang's avatar Hai Dang

Update Iris with fractional auth

parent d586b5fc
......@@ -212,7 +212,7 @@ Section logatom_hocap.
iIntros (???) "Hf1 Hf2". iDestruct (own_valid_2 with "Hf1 Hf2") as %[].
Qed.
Next Obligation.
iIntros (???) "Ha1 Ha2". iDestruct (own_valid_2 with "Ha1 Ha2") as %[].
iIntros (???) "Ha1 Ha2". by iDestruct (own_valid_2 with "Ha1 Ha2") as %[].
Qed.
Next Obligation.
iIntros (???) "Hf Ha". iDestruct (own_valid_2 with "Ha Hf") as
......
......@@ -2,7 +2,7 @@
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.algebra Require Import auth frac gmap agree.
From iris.algebra Require Import excl auth frac gmap agree.
From iris.bi Require Import fractional.
From iris.base_logic Require Import auth.
......
From iris.program_logic Require Import lifting.
From iris.algebra Require Import auth frac agree gmap list.
From iris.algebra Require Import excl auth frac agree gmap list.
From iris_examples.logrel.F_mu_ref Require Export rules.
From iris.proofmode Require Import tactics.
Import uPred.
......
From iris_examples.logrel.F_mu_ref Require Export context_refinement.
From iris.algebra Require Import auth frac agree.
From iris.algebra Require Import excl auth frac agree.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy.
From iris_examples.logrel.F_mu_ref Require Import soundness.
......
From iris.program_logic Require Export language ectx_language ectxi_language.
From iris.program_logic Require Import lifting.
From iris.algebra Require Import auth frac agree gmap list.
From iris.algebra Require Import excl auth frac agree gmap list.
From iris_examples.logrel.F_mu_ref_conc Require Export rules.
From iris.proofmode Require Import tactics.
Import uPred.
......
......@@ -31,7 +31,9 @@ Section symbol_ghosts.
Proof. apply _. Qed.
Lemma counter_exclusive γ n1 n2 : counter γ n1 - counter γ n2 - False.
Proof. apply bi.wand_intro_r. by rewrite -own_op own_valid auth_validI. Qed.
Proof.
apply bi.wand_intro_r. rewrite -own_op own_valid /=. by iDestruct 1 as %[].
Qed.
Global Instance symbol_persistent γ n : Persistent (symbol γ n).
Proof. apply _. Qed.
......
......@@ -279,7 +279,7 @@ Section graph.
Lemma auth_own_graph_valid q G : own graph_name ( Some (q, G)) G.
Proof.
iIntros "H". unfold own_graph.
by iDestruct (own_valid with "H") as %[_ [_ ?]].
by iDestruct (own_valid with "H") as %[_ [_ [_ [_ ?]]]].
Qed.
Lemma whole_frac (G G' : Gmon):
......@@ -287,7 +287,7 @@ Section graph.
Proof.
iIntros "[H1 H2]". rewrite /own_graph.
iCombine "H1" "H2" as "H".
iDestruct (own_valid with "H") as %[H1 H2]; cbn in *.
iDestruct (own_valid with "H") as %[_ [_ [H1 H2]]]; cbn in *.
iPureIntro.
specialize (H1 O).
apply cmra_discrete_included_iff in H1.
......@@ -345,7 +345,7 @@ Section graph.
G = {[x := Excl w]} (delete x G).
Proof.
rewrite /own_graph -?own_op. iIntros "H".
iDestruct (@own_valid with "H") as %[H1 H2]; simpl in *.
iDestruct (@own_valid with "H") as %[_ [_ [H1 H2]]]; simpl in *.
iPureIntro.
specialize (H1 O).
apply cmra_discrete_included_iff in H1.
......@@ -399,7 +399,7 @@ Section graph.
Proof.
iIntros "H". unfold is_marked. rewrite -own_op.
iDestruct (own_valid with "H") as %Hvl.
iPureIntro. destruct Hvl as [Hvl _]. destruct (Hvl O) as [z Hvl'].
iPureIntro. destruct Hvl as [_ [_ [Hvl _]]]. simpl in Hvl. destruct (Hvl O) as [z Hvl'].
rewrite Hvl' /= !gset_op_union !elem_of_union elem_of_singleton; tauto.
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