Commit b2711d60 authored by Ralf Jung's avatar Ralf Jung

Add support for ElimInv to introduce a binder from the accessor

If the accessor introduces a binder, the first Coq-level intro pattern of `iInv`
is used for that binder unless the type of the binder is unit, in which case
`iInv` removes it completely.  Binders on the closing view shift are not (yet)
supported as they are harder to smoothly eliminate in the unit case.
parent b71c6f44
......@@ -92,7 +92,7 @@ Section proofs.
Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N.
Global Instance elim_inv_cinv E N γ P p :
Global Instance into_acc_cinv E N γ P p :
IntoAcc (X:=unit) (cinv N γ P)
(N E) (cinv_own γ p) E (E∖↑N)
(λ _, P cinv_own γ p)%I (λ _, P)%I (λ _, None)%I.
......
......@@ -109,7 +109,7 @@ Qed.
Global Instance into_inv_inv N P : IntoInv (inv N P) N.
Global Instance elim_inv_inv E N P :
Global Instance into_acc_inv E N P :
IntoAcc (X:=unit) (inv N P)
(N E) True E (E∖↑N) (λ _, P)%I (λ _, P)%I (λ _, None)%I.
Proof.
......
......@@ -113,7 +113,7 @@ Section proofs.
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 :
Global Instance into_acc_na p F E N P :
IntoAcc (X:=unit) (na_inv p N P)
(N E N F) (na_own p F) E E
(λ _, P na_own p (F∖↑N))%I (λ _, P na_own p (F∖↑N))%I
......
......@@ -569,28 +569,31 @@ Qed.
the first binder. *)
(* ElimInv *)
Global Instance elim_inv_acc_without_close `{BiFUpd PROP} φ Pinv Pin
E1 E2 α β γ Q (Q' : () PROP) :
IntoAcc (X:=unit) Pinv φ Pin E1 E2 α β γ
AccElim (X:=unit) E1 E2 α β γ Q Q'
ElimInv φ Pinv Pin (α ()) None Q (Q' ()).
Global Instance elim_inv_acc_without_close `{BiFUpd PROP} {X : Type}
φ Pinv Pin
E1 E2 α β γ Q (Q' : X PROP) :
IntoAcc (X:=X) Pinv φ Pin E1 E2 α β γ
AccElim (X:=X) E1 E2 α β γ Q Q'
ElimInv φ Pinv Pin α None Q Q'.
Proof.
rewrite /AccElim /IntoAcc /ElimInv.
iIntros (Hacc Helim Hφ) "(Hinv & Hin & Hcont)".
iApply (Helim with "[Hcont]").
- rewrite right_id. iIntros ([]). done.
- iIntros (x) "Hα". iApply "Hcont". iSplitL; done.
- iApply (Hacc with "Hinv Hin"). done.
Qed.
Global Instance elim_inv_acc_with_close `{BiFUpd PROP} φ Pinv Pin
Global Instance elim_inv_acc_with_close `{BiFUpd PROP} {X : Type}
φ Pinv Pin
E1 E2 α β γ Q Q' :
IntoAcc (X:=unit) Pinv φ Pin E1 E2 α β γ
IntoAcc Pinv φ Pin E1 E2 α β γ
( R, ElimModal True false false (|={E1,E2}=> R) R Q Q')
ElimInv φ Pinv Pin (α ()) (Some (β () ={E2,E1}= default emp (γ ()) id))%I Q Q'.
ElimInv (X:=X) φ Pinv Pin α (Some (λ x, β x ={E2,E1}= default emp (γ x) id))%I
Q (λ _, Q').
Proof.
rewrite /AccElim /IntoAcc /ElimInv.
iIntros (Hacc Helim Hφ) "(Hinv & Hin & Hcont)".
iMod (Hacc with "Hinv Hin") as ([]) "[Hα Hclose]"; first done.
iMod (Hacc with "Hinv Hin") as (x) "[Hα Hclose]"; first done.
iApply "Hcont". simpl. iSplitL "Hα"; done.
Qed.
......
......@@ -573,14 +573,15 @@ Hint Mode IntoAcc + - ! - - - - - - - - : typeclass_instances.
TODO: Add support for a binder (like accessors have it).
This is defined on sbi instead of bi as typeclass search otherwise
fails (e.g. in the iInv as used in cancelable_invariants.v)
fails (e.g. in the iInv as used in cancelable_invariants.v).
*)
Class ElimInv {PROP : sbi} (φ : Prop)
(Pinv Pin : PROP) (Pout : PROP) (Pclose : option PROP) (Q Q' : PROP) :=
elim_inv : φ Pinv Pin (Pout default emp Pclose id - Q') Q.
Arguments ElimInv {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
Arguments elim_inv {_} _ _%I _%I _%I _%I _%I _%I {_}.
Hint Mode ElimInv + - ! - - ! ! - : typeclass_instances.
Class ElimInv {PROP : sbi} {X : Type} (φ : Prop)
(Pinv Pin : PROP) (Pout : X PROP) (Pclose : option (X PROP))
(Q : PROP) (Q' : X PROP) :=
elim_inv : φ Pinv Pin ( x, Pout x (default (λ _, emp) Pclose id) x - Q' x) Q.
Arguments ElimInv {_} {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
Arguments elim_inv {_} {_} _ _%I _%I _%I _%I _%I _%I {_}.
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
......@@ -628,6 +629,6 @@ Instance elim_modal_tc_opaque {PROP : bi} φ p p' (P P' Q Q' : PROP) :
ElimModal φ p p' P P' Q Q' ElimModal φ p p' (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 : sbi} φ Pinv Pin Pout Pclose Q Q' :
ElimInv (PROP:=PROP) φ Pinv Pin Pout Pclose Q Q'
Instance elim_inv_tc_opaque {PROP : sbi} {X} φ Pinv Pin Pout Pclose Q Q' :
ElimInv (PROP:=PROP) (X:=X) φ Pinv Pin Pout Pclose Q Q'
ElimInv φ (tc_opaque Pinv) Pin Pout Pclose Q Q' := id.
......@@ -1325,19 +1325,24 @@ Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.
(** * Invariants *)
Lemma tac_inv_elim Δ Δ' i j φ p Pinv Pin Pout (Pclose : option PROP) Q Q' :
Lemma tac_inv_elim {X : Type} Δ Δ' i j φ p Pinv Pin Pout (Pclose : option (X PROP))
Q (Q' : X PROP) :
envs_lookup_delete false i Δ = Some (p, Pinv, Δ')
ElimInv φ Pinv Pin Pout Pclose Q Q'
φ
( R, Δ'',
envs_app false (Esnoc Enil j (Pin - (Pout - maybe_wand Pclose Q') - R)%I) Δ' = Some Δ''
envs_app false (Esnoc Enil j
(Pin - ( x, Pout x - default (Q' x) Pclose (λ Pclose, Pclose x - Q' x)) - R)%I) Δ'
= Some Δ''
envs_entails Δ'' R)
envs_entails Δ Q.
Proof.
rewrite envs_entails_eq=> /envs_lookup_delete_Some [? ->] ?? /(_ Q) [Δ'' [? <-]].
rewrite envs_entails_eq=> /envs_lookup_delete_Some [? ->] Hinv ? /(_ 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 intuitionistically_if_elim maybe_wand_sound -assoc wand_curry. auto.
rewrite intuitionistically_if_elim -assoc. destruct Pclose; simpl in *.
- setoid_rewrite wand_curry. auto.
- setoid_rewrite <-(right_id emp%I _ (Pout _)). auto.
Qed.
(** * Rewriting *)
......
......@@ -1887,7 +1887,7 @@ Tactic Notation "iAssumptionInv" constr(N) :=
(* 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) open_constr(Hclose) :=
Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(Hclose) "in" tactic(tac) :=
iStartProof;
let pats := spec_pat.parse pats in
lazymatch pats with
......@@ -1896,7 +1896,7 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" tactic(tac) o
end;
let H := iFresh in
let Pclose_pat :=
match Hclose with
lazymatch Hclose with
| Some _ => open_constr:(Some _)
| None => open_constr:(None)
end in
......@@ -1917,97 +1917,161 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" tactic(tac) o
fail "iInv: cannot eliminate invariant " I
|try (split_and?; solve [ fast_done | solve_ndisj ])
|let R := fresh in intros R; eexists; split; [env_reflexivity|];
(* Now we are left proving [envs_entails Δ'' R]. *)
iSpecializePat H pats; last (
iApplyHyp H; clear R; env_cbv;
(* Now the goal is [∀ x, Pout x -∗ maybe_wand (Pclose x) (Q' x)] *)
let x := fresh in
iIntros (x);
iIntro H; (* H was spatial, so it's gone due to the apply and we can reuse the name *)
match Hclose with
lazymatch Hclose with
| Some ?Hcl => iIntros Hcl
| None => idtac
end;
tac H
tac x H
)].
(* Without closing view shift *)
Tactic Notation "iInvCore" constr(N) "with" constr(pats) "as" tactic(tac) :=
iInvCore N with pats as ltac:(tac) (@None string).
Tactic Notation "iInvCore" constr(N) "with" constr(pats) "in" tactic(tac) :=
iInvCore N with pats as (@None string) in ltac:(tac).
(* Without pattern *)
Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
iInvCore N with "[$]" as ltac:(tac) Hclose.
Tactic Notation "iInvCore" constr(N) "as" constr(Hclose) "in" tactic(tac) :=
iInvCore N with "[$]" as Hclose in ltac:(tac).
(* Without both *)
Tactic Notation "iInvCore" constr(N) "as" tactic(tac) :=
iInvCore N with "[$]" as ltac:(tac) (@None string).
Tactic Notation "iInvCore" constr(N) "in" tactic(tac) :=
iInvCore N with "[$]" as (@None string) in ltac:(tac).
(* With everything *)
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" constr(pat) constr(Hclose) :=
iInvCore N with Hs as (fun H => iDestructHyp H as pat) (Some Hclose).
iInvCore N with Hs as (Some Hclose) in (fun x H => iDestructHyp H as pat).
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1) ")"
constr(pat) constr(Hclose) :=
iInvCore N with Hs as (fun H => iDestructHyp H as (x1) pat) (Some Hclose).
iInvCore N with Hs as (Some Hclose) in (fun x H => iDestructHyp H as (x1) pat).
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) ")" constr(pat) constr(Hclose) :=
iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2) pat) (Some Hclose).
iInvCore N with Hs as (Some Hclose) in (fun x H => iDestructHyp H as (x1 x2) pat).
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) ")"
constr(pat) constr(Hclose) :=
iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3) pat) (Some Hclose).
iInvCore N with Hs as (Some Hclose) in (fun x H => iDestructHyp H as (x1 x2 x3) pat).
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
constr(pat) constr(Hclose) :=
iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat) (Some Hclose).
iInvCore N with Hs as (Some Hclose) in (fun x H => iDestructHyp H as (x1 x2 x3 x4) pat).
(* Without closing view shift *)
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" constr(pat) :=
iInvCore N with Hs as (fun H => iDestructHyp H as pat).
iInvCore N with Hs in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as pat
| _ => fail "Missing intro pattern for accessor variable"
end).
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1) ")"
constr(pat) :=
iInvCore N with Hs as (fun H => iDestructHyp H as (x1) pat).
iInvCore N with Hs in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1) pat
| _ => revert x; intros x1; iDestructHyp H as pat
end).
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) ")" constr(pat) :=
iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2) pat).
iInvCore N with Hs in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2) pat
end).
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) ")"
constr(pat) :=
iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3) pat).
iInvCore N with Hs in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3) pat
end).
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
constr(pat) :=
iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat).
iInvCore N with Hs in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4) pat
end).
(* Without pattern *)
Tactic Notation "iInv" constr(N) "as" constr(pat) constr(Hclose) :=
iInvCore N as (fun H => iDestructHyp H as pat) (Some Hclose).
iInvCore N as (Some Hclose) in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as pat
| _ => fail "Missing intro pattern for accessor variable"
end).
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1) ")"
constr(pat) constr(Hclose) :=
iInvCore N as (fun H => iDestructHyp H as (x1) pat) (Some Hclose).
iInvCore N as (Some Hclose) in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1) pat
| _ => revert x; intros x1; iDestructHyp H as pat
end).
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) ")" constr(pat) constr(Hclose) :=
iInvCore N as (fun H => iDestructHyp H as (x1 x2) pat) (Some Hclose).
iInvCore N as (Some Hclose) in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2) pat
end).
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) ")"
constr(pat) constr(Hclose) :=
iInvCore N as (fun H => iDestructHyp H as (x1 x2 x3) pat) (Some Hclose).
iInvCore N as (Some Hclose) in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3) pat
end).
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
constr(pat) constr(Hclose) :=
iInvCore N as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat) (Some Hclose).
iInvCore N as (Some Hclose) in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4) pat
end).
(* Without both *)
Tactic Notation "iInv" constr(N) "as" constr(pat) :=
iInvCore N as (fun H => iDestructHyp H as pat).
iInvCore N in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as pat
| _ => fail "Missing intro pattern for accessor variable"
end).
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1) ")"
constr(pat) :=
iInvCore N as (fun H => iDestructHyp H as (x1) pat).
iInvCore N in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1) pat
| _ => revert x; intros x1; iDestructHyp H as pat
end).
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) ")" constr(pat) :=
iInvCore N as (fun H => iDestructHyp H as (x1 x2) pat).
iInvCore N in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2) pat
end).
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) ")"
constr(pat) :=
iInvCore N as (fun H => iDestructHyp H as (x1 x2 x3) pat).
iInvCore N in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3) pat
end).
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
constr(pat) :=
iInvCore N as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat).
iInvCore N in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4) pat
end).
(** Miscellaneous *)
Tactic Notation "iAccu" :=
......
......@@ -486,21 +486,28 @@ Global Instance add_modal_at_fupd_goal `{BiFUpd PROP} E1 E2 𝓟 𝓟' Q i :
AddModal 𝓟 𝓟' (|={E1,E2}=> Q i) AddModal 𝓟 𝓟' ((|={E1,E2}=> Q) i).
Proof. by rewrite /AddModal !monPred_at_fupd. Qed.
Global Instance elim_inv_embed_with_close φ 𝓟inv 𝓟in 𝓟out 𝓟close Pin Pout Pclose Q Q' :
( i, ElimInv φ 𝓟inv 𝓟in 𝓟out (Some 𝓟close) (Q i) (Q' i))
MakeEmbed 𝓟in Pin MakeEmbed 𝓟out Pout MakeEmbed 𝓟close Pclose
ElimInv φ ⎡𝓟inv Pin Pout (Some Pclose) Q Q'.
Proof.
rewrite /MakeEmbed /ElimInv=>H <- <- <- ?. iStartProof PROP.
iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros "?". by iApply "HQ'".
Qed.
Global Instance elim_inv_embed_without_close φ 𝓟inv 𝓟in 𝓟out Pin Pout Q Q' :
( i, ElimInv φ 𝓟inv 𝓟in 𝓟out None (Q i) (Q' i))
MakeEmbed 𝓟in Pin MakeEmbed 𝓟out Pout
ElimInv φ ⎡𝓟inv Pin Pout None Q Q'.
Proof.
rewrite /MakeEmbed /ElimInv=>H <- <- ?. iStartProof PROP.
iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros "?". by iApply "HQ'".
Global Instance elim_inv_embed_with_close {X : Type} φ
𝓟inv 𝓟in (𝓟out 𝓟close : X PROP)
Pin (Pout Pclose : X monPred)
Q (Q' : X monPred) :
( i, ElimInv φ 𝓟inv 𝓟in 𝓟out (Some 𝓟close) (Q i) (λ x, Q' x i))
MakeEmbed 𝓟in Pin ( x, MakeEmbed (𝓟out x) (Pout x))
( x, MakeEmbed (𝓟close x) (Pclose x))
ElimInv (X:=X) φ ⎡𝓟inv Pin Pout (Some Pclose) Q Q'.
Proof.
rewrite /MakeEmbed /ElimInv=>H <- Hout Hclose ?. iStartProof PROP.
setoid_rewrite <-Hout. setoid_rewrite <-Hclose.
iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros (x) "?". by iApply "HQ'".
Qed.
Global Instance elim_inv_embed_without_close {X : Type}
φ 𝓟inv 𝓟in (𝓟out : X PROP) Pin (Pout : X monPred) Q (Q' : X monPred) :
( i, ElimInv φ 𝓟inv 𝓟in 𝓟out None (Q i) (λ x, Q' x i))
MakeEmbed 𝓟in Pin ( x, MakeEmbed (𝓟out x) (Pout x))
ElimInv (X:=X) φ ⎡𝓟inv Pin Pout None Q Q'.
Proof.
rewrite /MakeEmbed /ElimInv=>H <-Hout ?. iStartProof PROP.
setoid_rewrite <-Hout.
iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros (x) "?". by iApply "HQ'".
Qed.
End sbi.
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