Commit e9abd1bf authored by Robbert Krebbers's avatar Robbert Krebbers

Make closing update explicit in `ElimInv.

parent be7ca8aa
......@@ -92,12 +92,13 @@ Section proofs.
Qed.
Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N.
Global Instance elim_inv_cinv p γ E N P P' Q Q' :
ElimModal True (|={E,E∖↑N}=> ( P cinv_own γ p) ( P ={E∖↑N,E}= True))%I P' Q Q'
ElimInv (N E) (cinv N γ P) (cinv_own γ p) P' Q Q'.
Global Instance elim_inv_cinv p γ E N P Q Q' :
( R, ElimModal True (|={E,E∖↑N}=> R) R Q Q')
ElimInv (N E) (cinv N γ P) (cinv_own γ p)
( P cinv_own γ p) ( P ={E∖↑N,E}= True) Q Q'.
Proof.
rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&Hown&H2)".
iApply Helim; auto. iFrame "H2".
iApply (Helim with "[- $H2]"); first done.
iMod (cinv_open E N γ p P with "[#] [Hown]") as "(HP&Hown&Hclose)"; auto.
by iFrame.
Qed.
......
......@@ -96,12 +96,12 @@ Qed.
Global Instance into_inv_inv N P : IntoInv (inv N P) N.
Global Instance elim_inv_inv E N P P' Q Q' :
ElimModal True (|={E,E∖↑N}=> P ( P ={E∖↑N,E}= True))%I P' Q Q'
ElimInv (N E) (inv N P) True P' Q Q'.
Global Instance elim_inv_inv E N P Q Q' :
( R, ElimModal True (|={E,E∖↑N}=> R) R Q Q')
ElimInv (N E) (inv N P) True ( P) ( P ={E∖↑N,E}= True) Q Q'.
Proof.
rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&_&H2)".
iApply Helim; auto; iFrame.
iApply (Helim with "[$H2]"); first done.
iMod (inv_open _ N with "[#]") as "(HP&Hclose)"; auto with iFrame.
Qed.
......
......@@ -112,13 +112,13 @@ Section proofs.
Qed.
Global Instance into_inv_na p N P : IntoInv (na_inv p N P) N.
Global Instance elim_inv_na p F E N P P' Q Q':
ElimModal True (|={E}=> ( P na_own p (F∖↑N)) ( P na_own p (F∖↑N) ={E}= na_own p F))%I
P' Q Q'
ElimInv (N E N F) (na_inv p N P) (na_own p F) P' Q Q'.
Global Instance elim_inv_na p F E N P Q Q':
( R, ElimModal True (|={E}=> R)%I R Q Q')
ElimInv (N E N F) (na_inv p N P) (na_own p F)
( P na_own p (F∖↑N)) ( P na_own p (F∖↑N) ={E}= na_own p F) Q Q'.
Proof.
rewrite /ElimInv /ElimModal. iIntros (Helim (?&?)) "(#H1&Hown&H2)".
iApply Helim; auto. iFrame "H2".
iApply (Helim with "[- $H2]"); first done.
iMod (na_inv_open p E F N P with "[#] [Hown]") as "(HP&Hown&Hclose)"; auto.
by iFrame.
Qed.
......
......@@ -479,6 +479,7 @@ Hint Mode IntoInv + ! - : typeclass_instances.
- [Pinv] is an invariant assertion
- [Pin] is an additional assertion needed for opening an invariant
- [Pout] is the assertion obtained by opening the invariant
- [Pclose] is the assertion which contains an update modality to close the invariant
- [Q] is a goal on which iInv may be invoked
- [Q'] is the transformed goal that must be proved after opening the invariant.
......@@ -487,11 +488,11 @@ Hint Mode IntoInv + ! - : typeclass_instances.
is not a clearly associated instance of ElimModal of the right form
(e.g. to handle Iris 2.0 usage of iInv).
*)
Class ElimInv {PROP : bi} (φ : Prop) (Pinv Pin Pout Q Q' : PROP) :=
elim_inv : φ Pinv Pin (Pout - Q') Q.
Class ElimInv {PROP : bi} (φ : Prop) (Pinv Pin Pout Pclose Q Q' : PROP) :=
elim_inv : φ Pinv Pin (Pout Pclose - Q') Q.
Arguments ElimInv {_} _ _ _%I _%I _%I _%I : simpl never.
Arguments elim_inv {_} _ _ _%I _%I _%I _%I _%I _%I.
Hint Mode ElimInv + - ! - - - - : typeclass_instances.
Hint Mode ElimInv + - ! - - - ! - : typeclass_instances.
(* We make sure that tactics that perform actions on *specific* hypotheses or
parts of the goal look through the [tc_opaque] connective, which is used to make
......@@ -540,5 +541,6 @@ Instance elim_modal_tc_opaque {PROP : bi} φ (P P' Q Q' : PROP) :
ElimModal φ P P' Q Q' ElimModal φ (tc_opaque P) P' Q Q' := id.
Instance into_inv_tc_opaque {PROP : bi} (P : PROP) N :
IntoInv P N IntoInv (tc_opaque P) N := id.
Instance elim_inv_tc_opaque {PROP : bi} φ (Pinv Pin Pout Q Q' : PROP) :
ElimInv φ Pinv Pin Pout Q Q' ElimInv φ (tc_opaque Pinv) Pin Pout Q Q' := id.
Instance elim_inv_tc_opaque {PROP : bi} φ (Pinv Pin Pout Pclose Q Q' : PROP) :
ElimInv φ Pinv Pin Pout Pclose Q Q'
ElimInv φ (tc_opaque Pinv) Pin Pout Pclose Q Q' := id.
......@@ -1171,19 +1171,19 @@ Proof.
Qed.
(** * Invariants *)
Lemma tac_inv_elim Δ Δ' i j φ p P Pin Pout Q Q' :
Lemma tac_inv_elim Δ Δ' i j φ p P Pin Pout Pclose Q Q' :
envs_lookup_delete false i Δ = Some (p, P, Δ')
ElimInv φ P Pin Pout Q Q'
ElimInv φ P Pin Pout Pclose Q Q'
φ
( R, Δ'',
envs_app false (Esnoc Enil j (Pin - (Pout - Q') - R)%I) Δ' = Some Δ''
envs_app false (Esnoc Enil j (Pin - (Pout - Pclose - Q') - R)%I) Δ' = Some Δ''
envs_entails Δ'' R)
envs_entails Δ Q.
Proof.
rewrite envs_entails_eq=> /envs_lookup_delete_Some [? ->] ?? /(_ Q) [Δ'' [? <-]].
rewrite (envs_lookup_sound' _ false) // envs_app_singleton_sound //; simpl.
apply wand_elim_r', wand_mono; last done.
apply wand_intro_r, wand_intro_r. rewrite affinely_persistently_if_elim -assoc. auto.
apply wand_elim_r', wand_mono; last done. apply wand_intro_r, wand_intro_r.
rewrite affinely_persistently_if_elim -assoc wand_curry. auto.
Qed.
End bi_tactics.
......
......@@ -1893,27 +1893,25 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" tactic(tac) c
let H := iFresh in
lazymatch type of select with
| string =>
eapply tac_inv_elim with _ select H _ _ _ _ _ _;
eapply tac_inv_elim with _ select H _ _ _ _ _ _ _;
first by (iAssumptionCore || fail "iInv: invariant" select "not found")
| ident =>
eapply tac_inv_elim with _ select H _ _ _ _ _ _;
eapply tac_inv_elim with _ select H _ _ _ _ _ _ _;
first by (iAssumptionCore || fail "iInv: invariant" select "not found")
| namespace =>
eapply tac_inv_elim with _ _ H _ _ _ _ _ _;
eapply tac_inv_elim with _ _ H _ _ _ _ _ _ _;
first by (iAssumptionInv select || fail "iInv: invariant" select "not found")
| _ => fail "iInv: selector" select "is not of the right type "
end;
[apply _ ||
let I := match goal with |- ElimInv _ ?I _ _ _ _ => I end in
let I := match goal with |- ElimInv _ ?I _ _ _ _ _ => I end in
fail "iInv: cannot eliminate invariant " I
|try (split_and?; solve [ fast_done | solve_ndisj ])
|let R := fresh in intros R; eexists; split; [env_reflexivity|];
iSpecializePat H pats; last (
iApplyHyp H; clear R;
iIntros H; (* H was spatial, so it's gone due to the apply and we can reuse the name *)
let patclose := intro_pat.parse_one Hclose in
let patintro := constr:(IList [[IIdent H; patclose]]) in
iDestructHyp H as patintro;
iIntros Hclose;
tac H
)].
......
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