Commit 6028d0b2 authored by Joseph Tassarotti's avatar Joseph Tassarotti
Browse files

Opening rule for invariants with a credit inside

parent faac50f2
......@@ -4,7 +4,7 @@ the Iris lifting lemmas. *)
From iris.algebra Require Import lib.frac_auth numbers auth.
From iris.proofmode Require Import tactics.
From iris.bi.lib Require Import fractional.
From iris.base_logic.lib Require Export gen_heap proph_map gen_inv_heap.
From iris.base_logic.lib Require Export gen_heap proph_map gen_inv_heap invariants.
From iris.program_logic Require Export weakestpre total_weakestpre.
From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
From iris.heap_lang Require Export class_instances.
......@@ -221,6 +221,22 @@ Proof.
iIntros (?) "H". iApply "H". iFrame.
Qed.
Lemma wp_later_cred_inv N E e `{Atomic _ StronglyAtomic e} Φ P :
N E
language.to_val e = None
inv N (cred_frag 1 P) -
(P - WP e @ E N {{ v, P Φ v }}) -
WP e @ E {{ Φ }}.
Proof.
iIntros (? Hnval) "Hcred Hwp".
iInv "Hcred" as "(>H&HP)".
iApply (wp_later_cred_use with "[$]"); auto.
iNext. iSpecialize ("Hwp" with "[$]").
iApply (wp_mono with "Hwp").
rewrite ?wp_unfold /wp_pre.
iIntros (?) "(HP&HΦ) Hcred". iFrame. eauto.
Qed.
(** Recursive functions: we do not use this lemmas as it is easier to use Löb
induction directly, but this demonstrates that we can state the expected
reasoning principle for recursive functions, without any visible . *)
......
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