Commit 694425f0 authored by Joseph Tassarotti's avatar Joseph Tassarotti Committed by Robbert Krebbers

Support selecting invariants by hypothesis name.

parent a7b8df6f
......@@ -170,11 +170,11 @@ Rewriting / simplification
Iris
----
- `iInv (N with "selpat") as (x1 ... xn) "ipat" "Hclose"` : open the invariant
`N`. The selection pattern `selpat` is used for any auxiliary assertions
needed to open the invariant (e.g. for cancelable or non-atomic
invariants). The update for closing the invariant is put in a hypothesis named
`Hclose`.
- `iInv S with "selpat" as (x1 ... xn) "ipat" "Hclose"` : where `S` is either
a namespace N or an identifier "H". Open the invariant indicated by S. The
selection pattern `selpat` is used for any auxiliary assertions needed to
open the invariant (e.g. for cancelable or non-atomic invariants). The update
for closing the invariant is put in a hypothesis named `Hclose`.
Miscellaneous
-------------
......
......@@ -94,7 +94,7 @@ Section proofs.
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) N (cinv N γ P) (cinv_own γ p) P' Q Q'.
ElimInv (N E) (cinv N γ P) (cinv_own γ p) P' Q Q'.
Proof.
rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&Hown&H2)".
iApply Helim; auto. iFrame "H2".
......
......@@ -98,7 +98,7 @@ 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) N (inv N P) True P' Q Q'.
ElimInv (N E) (inv N P) True P' Q Q'.
Proof.
rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&_&H2)".
iApply Helim; auto; iFrame.
......
......@@ -115,7 +115,7 @@ Section proofs.
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) N (na_inv p N P) (na_own p F) P' Q Q'.
ElimInv (N E N F) (na_inv p N P) (na_own p F) P' Q Q'.
Proof.
rewrite /ElimInv /ElimModal. iIntros (Helim (?&?)) "(#H1&Hown&H2)".
iApply Helim; auto. iFrame "H2".
......
......@@ -487,11 +487,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) (N : namespace) (Pinv Pin Pout Q Q' : PROP) :=
Class ElimInv {PROP : bi} (φ : Prop) (Pinv Pin Pout Q Q' : PROP) :=
elim_inv : φ Pinv Pin (Pout - Q') Q.
Arguments ElimInv {_} _ _ _ _%I _%I _%I _%I : simpl never.
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
......
......@@ -1171,9 +1171,9 @@ Proof.
Qed.
(** * Invariants *)
Lemma tac_inv_elim Δ Δ' i j φ N p P Pin Pout Q Q' :
Lemma tac_inv_elim Δ Δ' i j φ p P Pin Pout Q Q' :
envs_lookup_delete false i Δ = Some (p, P, Δ')
ElimInv φ N P Pin Pout Q Q'
ElimInv φ P Pin Pout Q Q'
φ
( R, Δ'',
envs_app false (Esnoc Enil j (Pin - (Pout - Q') - R)%I) Δ' = Some Δ''
......
......@@ -1865,7 +1865,7 @@ Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
Tactic Notation "iMod" open_constr(lem) "as" "%" simple_intropattern(pat) :=
iDestructCore lem as false (fun H => iModCore H; iPure H as pat).
(** * Assert *)
(** * Invariant *)
(* Finds a hypothesis in the context that is an invariant with
namespace [N]. To do so, we check whether for each hypothesis
......@@ -1874,7 +1874,8 @@ Tactic Notation "iAssumptionInv" constr(N) :=
let rec find Γ i P :=
lazymatch Γ with
| Esnoc ?Γ ?j ?P' =>
first [assert (IntoInv P' N) by apply _; unify P P'; unify i j|find Γ i P]
first [(let H := constr:(_: IntoInv P' N) in
unify P P'; unify i j)|find Γ i P]
end in
match goal with
| |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs) = Some (_, ?P, _) =>
......@@ -1883,14 +1884,31 @@ Tactic Notation "iAssumptionInv" constr(N) :=
is_evar i; first [find Γp i P | find Γs i P]; env_reflexivity
end.
Tactic Notation "iInvCore" constr(N) "with" constr(pats) "as" tactic(tac) constr(Hclose) :=
(* The argument [select] is the namespace [N] or hypothesis name ["H"] of the
invariant. *)
Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" tactic(tac) constr(Hclose) :=
iStartProof;
let pats := spec_pat.parse pats in
lazymatch pats with
| [_] => idtac
| _ => fail "iInv: exactly one specialization pattern should be given"
end;
let H := iFresh in
eapply tac_inv_elim with _ _ H _ N _ _ _ _ _;
[iAssumptionInv N || fail "iInv: invariant" N "not found"
|apply _ ||
let I := match goal with |- ElimInv _ ?N ?I _ _ _ _ => I end in
fail "iInv: cannot eliminate invariant " I " with namespace " N
lazymatch type of select with
| string =>
eapply tac_inv_elim with _ select H _ _ _ _ _ _;
first by (iAssumptionCore || fail "iInv: invariant" select "not found")
| ident =>
eapply tac_inv_elim with _ select H _ _ _ _ _ _;
first by (iAssumptionCore || fail "iInv: invariant" select "not found")
| namespace =>
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
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 (
......@@ -1900,7 +1918,7 @@ Tactic Notation "iInvCore" constr(N) "with" constr(pats) "as" tactic(tac) constr
let patintro := constr:(IList [[IIdent H; patclose]]) in
iDestructHyp H as patintro;
tac H
)].
)].
Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
iInvCore N with "[$]" as ltac:(tac) Hclose.
......
......@@ -144,4 +144,47 @@ Section iris_tests.
iInv N as "HP" "Hclose".
iMod ("Hclose" with "[$HP]"). auto.
Qed.
(* test selection by hypothesis name instead of namespace *)
Lemma test_iInv_9 t N1 N2 N3 E1 E2 P:
N3 E1
inv N1 P na_inv t N3 (bi_persistently P) inv N2 P na_own t E1 na_own t E2
={}= na_own t E1 na_own t E2 P.
Proof.
iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
iInv "HInv" with "Hown1" as "(#HP&Hown1)" "Hclose".
iMod ("Hclose" with "[$HP $Hown1]").
iModIntro. iFrame. by iNext.
Qed.
(* test selection by hypothesis name instead of namespace *)
Lemma test_iInv_10 t N1 N2 N3 E1 E2 P:
N3 E1
inv N1 P na_inv t N3 (bi_persistently P) inv N2 P na_own t E1 na_own t E2
={}= na_own t E1 na_own t E2 P.
Proof.
iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
iInv "HInv" as "(#HP&Hown1)" "Hclose".
iMod ("Hclose" with "[$HP $Hown1]").
iModIntro. iFrame. by iNext.
Qed.
(* test selection by ident name *)
Lemma test_iInv_11 N P: inv N (bi_persistently P) ={}= P.
Proof.
let H := iFresh in
(iIntros H; iInv H as "#H2" "Hclose").
iMod ("Hclose" with "H2").
iModIntro. by iNext.
Qed.
(* error messages *)
Lemma test_iInv_12 N P: inv N (bi_persistently P) ={}= True.
Proof.
iIntros "H".
Fail iInv 34 as "#H2" "Hclose".
Fail iInv nroot as "#H2" "Hclose".
Fail iInv "H2" as "#H2" "Hclose".
done.
Qed.
End iris_tests.
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