Commit b8c2bcf3 authored by Ike Mulder's avatar Ike Mulder
Browse files

Small improvements in reloc, add some comments.

parent c84cba84
Pipeline #66064 passed with stage
in 15 minutes and 20 seconds
......@@ -377,7 +377,6 @@ Section reloc_executor.
- rewrite /template_M_inv bi_tforall_forall; simpl.
iIntros (a) "HP".
iPoseProof (Hjk j K with "[$Hs $Hj] HP") as "HQ".
rewrite !bi_texist_exist.
iMod "HQ" as (b) "[_ [Hj HQ]]".
iExists b.
by iFrame.
......
......@@ -69,7 +69,7 @@ Section proof.
<<
(CG_locked_push st' v') : ().
Proof.
iStepsS.
iStepsS.
iLöb as "IH".
rel_rec_l.
iStepsS.
......@@ -160,12 +160,10 @@ Section proof.
iStepsS.
iLöb as "IH". rel_rec_l.
iStepsS.
destruct x4 as [|h1 ls1]; iRevert "H3 H7"; iStepS.
- iStepS.
iStepR; iStepsS. iRestore.
destruct x4 as [|h1 ls1]; iReIntro "H7".
- iStepR; iStepsS. iRestore.
iStepsS.
- iStepS.
iRestore.
- iRestore.
iStepsS.
Qed.
......
......@@ -113,7 +113,9 @@ Section aupd_autom.
(* we can access the contents of an atomic update as follows: *)
Global Instance atomic_update_access p {TA TB : tele} Eo Ei E (α : TA PROP) (β Φ : TA TB PROP) beq :
(* TODO: at some point we may wish toget rid of this inhabited constraint, but I do not see a nice way of doing that *)
(* TODO: at some point we may wish toget rid of this inhabited constraint, but I do not see a nice way of doing that.
It can probably be done by introducing an extra copy of tele that we force to be lower in the universe hierarchy,
then having a way to lift it back to the regular telescopes. *)
(inh : Inhabited TB),
SimplTeleEq TB beq (* like invariants, AtomIntoWand causes problems because the E cannot be found *)
IntoWand2 p (atomic_update Eo Ei α β Φ) Eo E (|={E, Ei}=> .. x, α x ( (b : bool), .. (y : TB),
......
......@@ -15,10 +15,10 @@ Section intuitionistically.
Global Instance intuitionistically_re_intro : ModReIntro (bi_intuitionistically (PROP := PROP))
(λ p P R R', TCAnd (TCAnd (TCEq p false) $ TCOr (BiAffine PROP) (Affine P)) (TCEq R R'))%I.
(λ p P R R', TCAnd (TCAnd (TCEq p false) $ Affine P) (TCEq R R'))%I.
Proof.
move => p P Q R [[ -> [H|H]] ->] /=;
iIntros "#HQ _ !>";
move => p P Q R [[ -> H] ->] /=.
iIntros "#HQ _ !>".
by iApply "HQ".
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