Commit ee701141 authored by Ralf Jung's avatar Ralf Jung

bump Iris; fix for notation changes

parent 91237cf7
Pipeline #17386 passed with stage
in 15 minutes and 21 seconds
...@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"] ...@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ]
depends: [ depends: [
"coq-iris" { (= "dev.2019-06-11.5.e65b06a7") | (= "dev") } "coq-iris" { (= "dev.2019-06-11.8.a51fa3cf") | (= "dev") }
] ]
...@@ -34,7 +34,7 @@ Definition fcinv_own_eq `{ironInvG Σ} : fcinv_own = _ := fcinv_own_aux.(seal_eq ...@@ -34,7 +34,7 @@ Definition fcinv_own_eq `{ironInvG Σ} : fcinv_own = _ := fcinv_own_aux.(seal_eq
Definition fcinv_cancel_own_def `{ironInvG Σ} (γ : fcinv_name) (p : frac) : ironProp Σ := Definition fcinv_cancel_own_def `{ironInvG Σ} (γ : fcinv_name) (p : frac) : ironProp Σ :=
FracPred (λ π, if π is Some π FracPred (λ π, if π is Some π
then own (fcinv_frac_name γ) (!{p} (π:ufrac)) else False)%I. then own (fcinv_frac_name γ) (F{p} (π:ufrac)) else False)%I.
Definition fcinv_cancel_own_aux `{ironInvG Σ} : seal fcinv_cancel_own_def. by eexists. Qed. Definition fcinv_cancel_own_aux `{ironInvG Σ} : seal fcinv_cancel_own_def. by eexists. Qed.
Definition fcinv_cancel_own `{ironInvG Σ} := fcinv_cancel_own_aux.(unseal). Definition fcinv_cancel_own `{ironInvG Σ} := fcinv_cancel_own_aux.(unseal).
Definition fcinv_cancel_own_eq `{ironInvG Σ} : fcinv_cancel_own = _ := Definition fcinv_cancel_own_eq `{ironInvG Σ} : fcinv_cancel_own = _ :=
...@@ -43,7 +43,7 @@ Definition fcinv_cancel_own_eq `{ironInvG Σ} : fcinv_cancel_own = _ := ...@@ -43,7 +43,7 @@ Definition fcinv_cancel_own_eq `{ironInvG Σ} : fcinv_cancel_own = _ :=
Definition fcinv_def `{ironInvG Σ, invG Σ} (N : namespace) (γ : fcinv_name) Definition fcinv_def `{ironInvG Σ, invG Σ} (N : namespace) (γ : fcinv_name)
(P : ironProp Σ) : ironProp Σ := (P : ironProp Σ) : ironProp Σ :=
(<affine> cinv N (fcinv_cinv_name γ) ( π1 π2, (<affine> cinv N (fcinv_cinv_name γ) ( π1 π2,
own (fcinv_frac_name γ) (! (π1 ? π2 : ufrac)) perm π1 P π2) )%I. own (fcinv_frac_name γ) (F (π1 ? π2 : ufrac)) perm π1 P π2) )%I.
Definition fcinv_aux `{ironInvG Σ, invG Σ} : seal fcinv_def. by eexists. Qed. Definition fcinv_aux `{ironInvG Σ, invG Σ} : seal fcinv_def. by eexists. Qed.
Definition fcinv `{ironInvG Σ, invG Σ} := fcinv_aux.(unseal). Definition fcinv `{ironInvG Σ, invG Σ} := fcinv_aux.(unseal).
Definition fcinv_eq `{ironInvG Σ, invG Σ} : fcinv = _ := fcinv_aux.(seal_eq). Definition fcinv_eq `{ironInvG Σ, invG Σ} : fcinv = _ := fcinv_aux.(seal_eq).
...@@ -122,7 +122,7 @@ Proof. ...@@ -122,7 +122,7 @@ Proof.
iStartProof (iProp _); iIntros (π1) "Hp". iStartProof (iProp _); iIntros (π1) "Hp".
iMod (cinv_alloc_strong (λ _, True) _ N) as (γinv ?) "[Hγinv Halloc]". iMod (cinv_alloc_strong (λ _, True) _ N) as (γinv ?) "[Hγinv Halloc]".
{ apply pred_infinite_True. } { apply pred_infinite_True. }
iMod (own_alloc (! (1%Qp : ufrac) ! (1%Qp : ufrac))) iMod (own_alloc (F (1%Qp : ufrac) F (1%Qp : ufrac)))
as (γf) "[Hγauth Hγ]"; first by apply auth_both_valid. as (γf) "[Hγauth Hγ]"; first by apply auth_both_valid.
set (γ := FcInvName γinv γf). set (γ := FcInvName γinv γf).
iModIntro. iExists π1, ε. iSplit; [done|iFrame "Hp"]. iModIntro. iExists π1, ε. iSplit; [done|iFrame "Hp"].
...@@ -132,7 +132,7 @@ Proof. ...@@ -132,7 +132,7 @@ Proof.
iMod (own_update_2 with "Hγauth Hγ") as "[Hγauth Hγ]". iMod (own_update_2 with "Hγauth Hγ") as "[Hγauth Hγ]".
{ by apply frac_auth_update, { by apply frac_auth_update,
(replace_local_update _ ((π3 / 2)%Qp ? π2 : ufrac)). } (replace_local_update _ ((π3 / 2)%Qp ? π2 : ufrac)). }
iMod ("Halloc" $! ( π1 π2, own (fcinv_frac_name γ) (! (π1 ? π2 : ufrac)) iMod ("Halloc" $! ( π1 π2, own (fcinv_frac_name γ) (F (π1 ? π2 : ufrac))
perm π1 P π2)%I with "[Hγauth Hp HP]"); first by eauto with iFrame. perm π1 P π2)%I with "[Hγauth Hp HP]"); first by eauto with iFrame.
iModIntro; iSplit; [by rewrite -!cmra_opM_opM_assoc_L /= frac_op' Qp_div_2|]. iModIntro; iSplit; [by rewrite -!cmra_opM_opM_assoc_L /= frac_op' Qp_div_2|].
iExists (Some (π3 / 2)%Qp π2), ε; iSplit; first by rewrite right_id_L. iExists (Some (π3 / 2)%Qp π2), ε; iSplit; first by rewrite right_id_L.
......
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