Commit 19e25cbd authored by Robbert Krebbers's avatar Robbert Krebbers

WIP on faster iDestruct.

parent 92e0e7e0
......@@ -9,8 +9,8 @@
x : A
============================
"HP" : P
"HΨ" : Ψ x
"HR" : R
"HΨ" : Ψ x
--------------------------------------∗
Ψ x ∗ P
......
......@@ -555,10 +555,9 @@ In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]),
"tac" (bound to fun H => iDestructHyp H as pat),
"iDestructHyp (constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
"<iris.proofmode.ltac_tactics.iDestructHypGo>" and
"iRename (constr) into (constr)", last call failed.
Tactic failure: iRename: "H" not fresh.
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>" and
"iFastDestructHyp (constr) as (constr)", last call failed.
Tactic failure: iDestruct: given names not fresh.
"iPoseProof_not_found_fail"
: string
The command has indeed failed with message:
......@@ -602,8 +601,9 @@ In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)",
"tac" (bound to fun H => iDestructHyp H as pat),
"iDestructHyp (constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>" and
"<iris.proofmode.ltac_tactics.iDestructHypGo>", last call failed.
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
"iFastDestructHyp (constr) as (constr)" and
"<iris.proofmode.ltac_tactics.iFastDestructHypGo>", last call failed.
Tactic failure: iDestruct: (IList [[IClear (sel_patterns.SelIdent "HP")]])
invalid.
"iOrDestruct_fail"
......
......@@ -261,7 +261,7 @@ Proof. iIntros "H". iNext. done. Qed.
Lemma test_iFrame_persistent (P Q : PROP) :
P - Q - <pers> (P P) (P Q Q).
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
Proof. iIntros "#HP". iFrame "HP". by iIntros "$". Qed.
Lemma test_iSplit_persistently P Q : P - <pers> (P P).
Proof. iIntros "#?". by iSplit. Qed.
......@@ -321,7 +321,7 @@ Qed.
Lemma test_iIntros_let P :
Q, let R := emp%I in P - R - Q - P Q.
Proof. iIntros (Q R) "$ _ $". Qed.
Proof. by iIntros (Q R) "$ _ $". Qed.
Lemma test_iNext_iRewrite P Q : <affine> (Q P) - <affine> Q - <affine> P.
Proof.
......@@ -565,18 +565,18 @@ Proof. iIntros "HP" (Q) "_ #HPQ". by iApply "HPQ". Qed.
Lemma test_and_sep (P Q R : PROP) : P (Q R) (P Q) R.
Proof.
iIntros "H". repeat iSplit.
- iDestruct "H" as "[$ _]".
- iDestruct "H" as "[_ [$ _]]".
- iDestruct "H" as "[_ [_ #$]]".
- by iDestruct "H" as "[$ _]".
- by iDestruct "H" as "[_ [$ _]]".
- by iDestruct "H" as "[_ [_ #$]]".
Qed.
Lemma test_and_sep_2 (P Q R : PROP) `{!Persistent R, !Affine R} :
P (Q R) (P Q) R.
Proof.
iIntros "H". repeat iSplit.
- iDestruct "H" as "[$ _]".
- iDestruct "H" as "[_ [$ _]]".
- iDestruct "H" as "[_ [_ #$]]".
- by iDestruct "H" as "[$ _]".
- by iDestruct "H" as "[_ [$ _]]".
- by iDestruct "H" as "[_ [_ #$]]".
Qed.
Check "test_and_sep_affine_bi".
......
......@@ -60,8 +60,8 @@
_ : cinv N γ (<pers> P)
"HP" : ▷ <pers> P
--------------------------------------□
"Hown" : cinv_own γ p
"Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
"Hown" : cinv_own γ p
--------------------------------------∗
|={⊤ ∖ ↑N,⊤}=> cinv_own γ p ∗ ▷ P
......@@ -102,8 +102,8 @@
"HP" : ▷ <pers> P
--------------------------------------□
"Hown1" : na_own t E1
"Hown2" : na_own t (E2 ∖ ↑N)
"Hclose" : ▷ <pers> P ∗ na_own t (E2 ∖ ↑N) ={⊤}=∗ na_own t E2
"Hown2" : na_own t (E2 ∖ ↑N)
--------------------------------------∗
|={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P
......@@ -155,8 +155,8 @@ Tactic failure: iInv: invariant "H2" not found.
𝓟 : iProp Σ
H : ↑N ⊆ E
============================
"HP" : ⎡ ▷ 𝓟 ⎤
"Hclose" : ⎡ ▷ 𝓟 ={E ∖ ↑N,E}=∗ emp ⎤
"HP" : ⎡ ▷ 𝓟 ⎤
--------------------------------------∗
|={E ∖ ↑N,E}=> emp
......@@ -40,13 +40,13 @@ Section base_logic_tests.
Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.
Lemma test_iStartProof_1 P : P - P.
Proof. iStartProof. iStartProof. iIntros "$". Qed.
Proof. iStartProof. iStartProof. by iIntros "$". Qed.
Lemma test_iStartProof_2 P : P - P.
Proof. iStartProof (uPred _). iStartProof (uPredI _). iIntros "$". Qed.
Proof. iStartProof (uPred _). iStartProof (uPredI _). by iIntros "$". Qed.
Lemma test_iStartProof_3 P : P - P.
Proof. iStartProof (uPredI _). iStartProof (uPredSI _). iIntros "$". Qed.
Proof. iStartProof (uPredI _). iStartProof (uPredSI _). by iIntros "$". Qed.
Lemma test_iStartProof_4 P : P - P.
Proof. iStartProof (uPredSI _). iStartProof (uPred _). iIntros "$". Qed.
Proof. iStartProof (uPredSI _). iStartProof (uPred _). by iIntros "$". Qed.
End base_logic_tests.
Section iris_tests.
......
......@@ -11,20 +11,20 @@ Section tests.
Implicit Types i j : I.
Lemma test0 P : P - P.
Proof. iIntros "$". Qed.
Proof. by iIntros "$". Qed.
Lemma test_iStartProof_1 P : P - P.
Proof. iStartProof. iStartProof. iIntros "$". Qed.
Proof. iStartProof. iStartProof. by iIntros "$". Qed.
Lemma test_iStartProof_2 P : P - P.
Proof. iStartProof monPred. iStartProof monPredI. iIntros "$". Qed.
Proof. iStartProof monPred. iStartProof monPredI. by iIntros "$". Qed.
Lemma test_iStartProof_3 P : P - P.
Proof. iStartProof monPredI. iStartProof monPredSI. iIntros "$". Qed.
Proof. iStartProof monPredI. iStartProof monPredSI. by iIntros "$". Qed.
Lemma test_iStartProof_4 P : P - P.
Proof. iStartProof monPredSI. iStartProof monPred. iIntros "$". Qed.
Proof. iStartProof monPredSI. iStartProof monPred. by iIntros "$". Qed.
Lemma test_iStartProof_5 P : P - P.
Proof. iStartProof PROP. iIntros (i) "$". Qed.
Proof. iStartProof PROP. by iIntros (i) "$". Qed.
Lemma test_iStartProof_6 P : P P.
Proof. iStartProof PROP. iIntros (i). iSplit; iIntros "$". Qed.
Proof. iStartProof PROP. iIntros (i). iSplit; by iIntros "$". Qed.
Lemma test_iStartProof_7 P : ((P P)%I : monPredI).
Proof. iStartProof PROP. done. Qed.
......@@ -58,11 +58,11 @@ Section tests.
Lemma test_iStartProof_forall_1 (Φ : nat monPredI) : n, Φ n - Φ n.
Proof.
iStartProof PROP. iIntros (n i) "$".
iStartProof PROP. by iIntros (n i) "$".
Qed.
Lemma test_iStartProof_forall_2 (Φ : nat monPredI) : n, Φ n - Φ n.
Proof.
iStartProof. iIntros (n) "$".
iStartProof. by iIntros (n) "$".
Qed.
Lemma test_embed_wand (P Q : PROP) : (P - Q) - P - Q : monPred.
......@@ -160,7 +160,7 @@ Section tests.
Lemma test_iFrame_embed (P : PROP) i :
P - (embed (B:=monPredI) P) i.
Proof. iIntros "$". Qed.
Proof. by iIntros "$". Qed.
(* Make sure search doesn't diverge on an evar *)
Lemma test_iFrame_monPred_at_evar (P : monPred) i j :
......
......@@ -48,7 +48,7 @@ Section proofs.
iIntros "#HPQ". rewrite /na_inv. iDestruct 1 as (i ?) "#Hinv".
iExists i. iSplit; first done. iApply (inv_iff with "[] Hinv").
iNext; iAlways.
iSplit; iIntros "[[? Ho]|$]"; iLeft; iFrame "Ho"; by iApply "HPQ".
iSplit; iIntros "[[? Ho]|$] //"; iLeft; iFrame "Ho"; by iApply "HPQ".
Qed.
Lemma na_alloc : (|==> p, na_own p )%I.
......
......@@ -66,7 +66,7 @@ Proof.
iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]".
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- iModIntro. iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
wp_apply ("IH" with "Hγ [HΦ]"). auto.
wp_apply ("IH" with "[HΦ] Hγ"). auto.
- iDestruct "Hinv" as (v' ->) "[HΨ|Hγ']".
+ iModIntro. iSplitL "Hl Hγ"; [iNext; iExists _; iFrame; eauto|].
wp_pures. by iApply "HΦ".
......
......@@ -715,6 +715,170 @@ Proof.
- setoid_rewrite <-(right_id emp%I _ (Pout _)). auto.
Qed.
(** * Delayed tactics *)
Local Notation of_env_temps tmps :=
([ list] tmp tmps, of_env_temp tmp)%I.
Local Notation of_env_actions acts :=
([ list] act acts, of_env_action act)%I.
Lemma envs_entails_delayed_unfold Δ acts tmps Q :
envs_entails_delayed Δ acts tmps Q
(of_env_temps tmps of_env_actions acts of_envs Δ Q).
Proof.
rewrite /envs_entails_delayed envs_entails_eq. split.
- intros ->. by rewrite assoc (comm _ (of_env_temps _)) wand_elim_r.
- intros <-. apply wand_intro_l. by rewrite -(comm _ (of_env_temps _)) assoc.
Qed.
Lemma tac_delay_destruct Δ Q i :
match envs_lookup_delete true i Δ with
| Some (p,P,Δ') => envs_entails_delayed Δ' [] [ETemp p P] Q
| None => False
end
envs_entails Δ Q.
Proof.
destruct (envs_lookup_delete true i Δ) as [[[p P] Δ']|] eqn:?; last done.
rewrite envs_entails_delayed_unfold envs_entails_eq /= => <-.
rewrite envs_lookup_delete_sound //. by rewrite right_id left_id comm.
Qed.
Lemma tac_force Δ acts Q :
match envs_actions_app acts Δ with
| Some Δ' => envs_entails Δ' Q
| None => False
end
envs_entails_delayed Δ acts [] Q.
Proof.
destruct (envs_actions_app acts Δ) as [Δ'|] eqn:?; last done.
rewrite envs_entails_delayed_unfold envs_entails_eq /= => <-.
by rewrite left_id comm envs_actions_app_sound.
Qed.
Lemma tac_delayed_rename Δ acts tmps (p : bool) mi P Q :
envs_entails_delayed Δ (EAction p mi P :: acts) tmps Q
envs_entails_delayed Δ acts (ETemp p P :: tmps) Q.
Proof. rewrite !envs_entails_delayed_unfold /= => <-. solve_sep_entails. Qed.
Lemma tac_delayed_falso Δ acts tmps p P Q :
FromAssumption p P False
envs_entails_delayed Δ acts (ETemp p P :: tmps) Q.
Proof.
rewrite !envs_entails_delayed_unfold /= => ->.
rewrite !left_absorb. apply False_elim.
Qed.
Lemma tac_delayed_clear Δ acts tmps (p : bool) P Q :
(if p then TCTrue else TCOr (Affine P) (Absorbing Q))
envs_entails_delayed Δ acts tmps Q
envs_entails_delayed Δ acts (ETemp p P :: tmps) Q.
Proof.
rewrite !envs_entails_delayed_unfold /= => HPQ HQ.
rewrite -!assoc HQ. destruct p; simpl; by rewrite sep_elim_r.
Qed.
Lemma tac_delayed_pure Δ acts tmps (p : bool) P Q φ :
IntoPure P φ
(if p then TCTrue else TCOr (Affine P) (Absorbing Q))
(φ envs_entails_delayed Δ acts tmps Q)
envs_entails_delayed Δ acts (ETemp p P :: tmps) Q.
Proof.
rewrite !envs_entails_delayed_unfold /= => ? HPQ HQ. rewrite -!assoc.
destruct p; simpl.
{ rewrite (into_pure P) intuitionistically_affinely -persistent_and_affinely_sep_l.
auto using pure_elim_l. }
destruct HPQ.
- rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
auto using pure_elim_l.
- rewrite (into_pure P) (persistent_absorbingly_affinely_2 _ )%I.
rewrite !absorbingly_sep_l -(absorbing_absorbingly Q); f_equiv.
rewrite -persistent_and_affinely_sep_l. auto using pure_elim_l.
Qed.
Lemma tac_delayed_and Δ acts tmps (p : bool) P P1 P2 Q :
(if p then IntoAnd true P P1 P2 else IntoSep P P1 P2)
envs_entails_delayed Δ acts (ETemp p P1 :: ETemp p P2 :: tmps) Q
envs_entails_delayed Δ acts (ETemp p P :: tmps) Q.
Proof.
rewrite !envs_entails_delayed_unfold /= -!assoc=> HP <-. destruct p.
- rewrite (into_and true P) /= .
by rewrite intuitionistically_and persistent_and_sep_1 -!assoc.
- by rewrite (into_sep P) /= -!assoc.
Qed.
Lemma tac_delayed_and_l Δ acts tmps (p : bool) P P1 P2 Q :
(if p then IntoAnd p P P1 P2 else
TCOr (IntoAnd p P P1 P2)
(TCAnd (IntoSep P P1 P2) (TCOr (Affine P2) (Absorbing Q))))
envs_entails_delayed Δ acts (ETemp p P1 :: tmps) Q
envs_entails_delayed Δ acts (ETemp p P :: tmps) Q.
Proof.
rewrite !envs_entails_delayed_unfold /= -!assoc=> HP HQ. destruct p.
{ by rewrite (into_and true P) /= and_elim_l. }
destruct HP as [?|[? HP2Q]].
{ by rewrite (into_and false P) /= and_elim_l. }
rewrite (into_sep P) /=. destruct HP2Q.
- by rewrite (sep_elim_l P1 P2).
- by rewrite (comm _ P1) -!assoc HQ sep_elim_r.
Qed.
Lemma tac_delayed_and_r Δ acts tmps (p : bool) P P1 P2 Q :
(if p then IntoAnd p P P1 P2 else
TCOr (IntoAnd p P P1 P2)
(TCAnd (IntoSep P P1 P2) (TCOr (Affine P1) (Absorbing Q))))
envs_entails_delayed Δ acts (ETemp p P2 :: tmps) Q
envs_entails_delayed Δ acts (ETemp p P :: tmps) Q.
Proof.
rewrite !envs_entails_delayed_unfold /= -!assoc=> HP HQ. destruct p.
{ by rewrite (into_and true P) /= and_elim_r. }
destruct HP as [?|[? HP2Q]].
{ by rewrite (into_and false P) /= and_elim_r. }
rewrite (into_sep P) /=. destruct HP2Q.
- by rewrite (sep_elim_r P1 P2).
- by rewrite -!assoc HQ sep_elim_r.
Qed.
Lemma tac_delayed_or Δ acts tmps (p : bool) P P1 P2 Q :
IntoOr P P1 P2
envs_entails_delayed Δ acts (ETemp p P1 :: tmps) Q
envs_entails_delayed Δ acts (ETemp p P2 :: tmps) Q
envs_entails_delayed Δ acts (ETemp p P :: tmps) Q.
Proof.
rewrite !envs_entails_delayed_unfold /= -!assoc=> HP HQ1 HQ2.
rewrite (into_or P) intuitionistically_if_or sep_or_r. by apply or_elim.
Qed.
Lemma tac_delayed_intuitionistic Δ acts tmps (p : bool) P P' Q :
IntoPersistent p P P'
(if p then TCTrue else TCOr (Affine P) (Absorbing Q))
envs_entails_delayed Δ acts (ETemp true P' :: tmps) Q
envs_entails_delayed Δ acts (ETemp p P :: tmps) Q.
Proof.
rewrite /IntoPersistent !envs_entails_delayed_unfold /= -!assoc=> HP HPQ HQ.
destruct p; simpl in *.
{ by rewrite /bi_intuitionistically HP. }
destruct HPQ.
- by rewrite -(affine_affinely P) HP.
- rewrite HP -absorbingly_intuitionistically_into_persistently.
by rewrite absorbingly_sep_l HQ.
Qed.
Lemma tac_delayed_modal Δ acts tmps p p' P P' Q Q' φ :
ElimModal φ p p' P P' Q Q'
φ
envs_entails_delayed Δ acts (ETemp p' P' :: tmps) Q'
envs_entails_delayed Δ acts (ETemp p P :: tmps) Q.
Proof.
rewrite /ElimModal !envs_entails_delayed_unfold /= -!assoc => HP Hφ HQ'.
rewrite -HP //. apply sep_mono; first done. by apply wand_intro_l.
Qed.
Lemma tac_delayed_frame Δ acts tmps p P Q Q' :
Frame p P Q Q'
envs_entails_delayed Δ (if p then EAction p None P :: acts else acts) tmps Q'
envs_entails_delayed Δ acts (ETemp p P :: tmps) Q.
Proof.
rewrite /Frame !envs_entails_delayed_unfold /= -!assoc=> <- <-.
destruct p; simpl; last done.
rewrite {1}(intuitionistically_sep_dup P). solve_sep_entails.
Qed.
End bi_tactics.
(** The following _private_ classes are used internally by [tac_modal_intro] /
......
......@@ -373,6 +373,44 @@ Definition env_to_prop {PROP : bi} (Γ : env PROP) : PROP :=
in
match Γ with Enil => emp%I | Esnoc Γ _ P => aux Γ P end.
Inductive env_temp (PROP : bi) :=
| ETemp (p : bool) (P : PROP).
Arguments ETemp {_} _ _.
Inductive env_action (PROP : bi) :=
| EAction (p : bool) (i : option ident) (P : PROP).
Arguments EAction {_} _ _ _.
Definition of_env_temp {PROP} (act : env_temp PROP) : PROP :=
match act with ETemp p P => ?p P end%I.
Definition of_env_action {PROP} (act : env_action PROP) : PROP :=
match act with EAction p _ P => ?p P end%I.
Definition envs_entails_delayed {PROP : bi} (Δ : envs PROP)
(acts : list (env_action PROP)) (tmps : list (env_temp PROP)) (Q : PROP) :=
envs_entails Δ (([ list] act acts, of_env_action act)
([ list] tmp tmps, of_env_temp tmp) - Q).
Fixpoint envs_actions_flatten {PROP} (acts : list (env_action PROP))
(c : positive) (Γp Γs : env PROP) : (positive * env PROP * env PROP) :=
match acts with
| [] => (c,Γp,Γs)
| EAction q None P :: acts =>
if q
then envs_actions_flatten acts (Pos_succ c) (Esnoc Γp (IAnon c) P) Γs
else envs_actions_flatten acts (Pos_succ c) Γp (Esnoc Γs (IAnon c) P)
| EAction q (Some j) P :: acts =>
if q
then envs_actions_flatten acts c (Esnoc Γp j P) Γs
else envs_actions_flatten acts c Γp (Esnoc Γs j P)
end.
Definition envs_actions_app {PROP}
(acts : list (env_action PROP)) (Δ : envs PROP) : option (envs PROP) :=
let '(c,Γp,Γs) := envs_actions_flatten (pm_reverse acts) (env_counter Δ) Enil Enil in
Δ envs_app true Γp Δ;
Δ envs_app false Γs Δ;
Some (envs_set_counter c Δ).
Section envs.
Context {PROP : bi}.
Implicit Types Γ Γp Γs : env PROP.
......@@ -777,4 +815,43 @@ Proof.
- by rewrite right_id.
- rewrite /= IH (comm _ Q _) assoc. done.
Qed.
Lemma envs_replace_action_filter_sound acts c Γp Γs c' Γp' Γs' :
envs_actions_flatten acts c Γp Γs = (c',Γp',Γs')
([ list] act acts, of_env_action act) [] Γp [] Γs
[] Γp' [] Γs'.
Proof.
revert c Γp Γs.
induction acts as [|[q [j|] P] acts IH]=> c Γp Γs ?; simplify_eq/=.
- by rewrite left_id.
- destruct q; simplify_eq/=.
+ rewrite -IH //; simpl.
rewrite intuitionistically_and and_sep_intuitionistically. solve_sep_entails.
+ rewrite -IH //; simpl. solve_sep_entails.
- destruct q; simplify_eq/=.
+ rewrite -IH //; simpl.
rewrite intuitionistically_and and_sep_intuitionistically. solve_sep_entails.
+ rewrite -IH //; simpl. solve_sep_entails.
Qed.
Lemma envs_replace_action_filter_sound_nil acts c c' Γp' Γs' :
envs_actions_flatten acts c Enil Enil = (c',Γp',Γs')
([ list] act acts, of_env_action act) [] Γp' [] Γs'.
Proof.
intros. rewrite -envs_replace_action_filter_sound //; simpl.
by rewrite intuitionistically_True_emp !right_id.
Qed.
Lemma envs_actions_app_sound Δ Δ' acts :
envs_actions_app acts Δ = Some Δ'
of_envs Δ ([ list] act acts, of_env_action act) of_envs Δ'.
Proof.
rewrite /envs_actions_app=> Hacts.
destruct (envs_actions_flatten _ _ _ _) as [[c Γp] Γs] eqn:?.
destruct (envs_app true _ _) as [Δ1|] eqn:?; simplify_eq/=.
destruct (envs_app false _ _) as [Δ2|] eqn:?; simplify_eq/=.
rewrite envs_app_sound // envs_app_sound // envs_set_counter_sound; simpl.
rewrite -(reverse_Permutation acts) envs_replace_action_filter_sound_nil //.
by rewrite wand_curry wand_elim_l.
Qed.
End envs.
......@@ -1288,29 +1288,128 @@ Tactic Notation "iModCore" constr(H) :=
|pm_reduce; pm_prettify(* subgoal *)].
(** * Basic destruct tactic *)
Local Ltac iDestructHypGo Hz pat :=
Local Ltac iFastDestructHypGo pat :=
lazymatch pat with
| IFresh =>
lazymatch Hz with
| IAnon _ => idtac
| INamed ?Hz => let Hz' := iFresh in iRename Hz into Hz'
end
| IDrop => iClearHyp Hz
| IFrame => iFrameHyp Hz
| IIdent ?y => iRename Hz into y
| IList [[]] => iExFalso; iExact Hz
| IList [[?pat1; IDrop]] => iAndDestructChoice Hz as Left Hz; iDestructHypGo Hz pat1
| IList [[IDrop; ?pat2]] => iAndDestructChoice Hz as Right Hz; iDestructHypGo Hz pat2
eapply (tac_delayed_rename _ _ _ _ None)
| IIdent ?y =>
eapply (tac_delayed_rename _ _ _ _ (Some y))
| IDrop =>
eapply tac_delayed_clear;
[pm_reduce; iSolveTC ||
let P := match goal with |- TCOr (Affine ?P) _ => P end in
fail "iDestruct: cannot clear" P "; not affine and the goal not absorbing"
|]
| IFrame =>
eapply tac_delayed_frame;
[iSolveTC ||
let R := match goal with |- Frame _ ?R _ _ => R end in
fail "iDestruct: cannot frame" R
|]
| IList [[]] =>
eapply tac_delayed_falso;
[iSolveTC ||
let P := match goal with |- FromAssumption _ ?P _ => P end in
fail "iDestruct:" P " is not False"]
| IList [[?pat; IDrop]] =>
eapply tac_delayed_and_l;
[pm_reduce; iSolveTC ||
let P := match goal with |- context [ IntoAnd _ ?P _ _ ] => P end in
fail "iDestruct: cannot destruct" P
|iFastDestructHypGo pat]
| IList [[IDrop; ?pat]] =>
eapply tac_delayed_and_r;
[pm_reduce; iSolveTC ||
let P := match goal with |- context [ IntoAnd _ ?P _ _ ] => P end in
fail "iDestruct: cannot destruct" P
|iFastDestructHypGo pat]
| IList [[?pat1; ?pat2]] =>
let Hy := iFresh in iAndDestruct Hz as Hz Hy; iDestructHypGo Hz pat1; iDestructHypGo Hy pat2
| IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [iDestructHypGo Hz pat1|iDestructHypGo Hz pat2]
| IPureElim => iPure Hz as ?
| IRewrite Right => iPure Hz as ->
| IRewrite Left => iPure Hz as <-
| IAlwaysElim ?pat => iIntuitionistic Hz; iDestructHypGo Hz pat
| IModalElim ?pat => iModCore Hz; iDestructHypGo Hz pat
eapply tac_delayed_and;
[pm_reduce; iSolveTC ||
let P :=
lazymatch goal with
| |- IntoSep ?P _ _ => P
| |- IntoAnd _ ?P _ _ => P
end in
fail "iDestruct: cannot destruct" P
|iFastDestructHypGo pat1; iFastDestructHypGo pat2]
| IList [[?pat1];[?pat2]] =>
eapply tac_delayed_or;
[pm_reduce; iSolveTC ||
let P := match goal with |- context [ IntoOr ?P _ _ ] => P end in
fail "iDestruct: cannot turn " P "into a disjunction"
|iFastDestructHypGo pat1
|iFastDestructHypGo pat2]
| IPureElim =>
eapply tac_delayed_pure;
[iSolveTC ||
let P := match goal with |- IntoPure ?P _ => P end in
fail "iDestruct:" P "not pure"
|pm_reduce; iSolveTC ||
let P := match goal with |- TCOr (Affine ?P) _ => P end in
fail "iDestruct:" P "not affine and the goal not absorbing"
|intros ?]
| IRewrite Right =>
(* Get rid of the duplication *)
eapply tac_delayed_pure;
[iSolveTC ||
let P := match goal with |- IntoPure ?P _ => P end in
fail "iDestruct:" P "not pure"
|pm_reduce; iSolveTC ||
let P := match goal with |- TCOr (Affine ?P) _ => P end in
fail "iDestruct:" P "not affine and the goal not absorbing"
|intros ->]
| IRewrite Left =>
(* Get rid of the duplication *)
eapply tac_delayed_pure;
[iSolveTC ||
let P := match goal with |- IntoPure ?P _ => P end in
fail "iDestruct:" P "not pure"
|pm_reduce; iSolveTC ||
let P := match goal with |- TCOr (Affine ?P) _ => P end in
fail "iDestruct:" P "not affine and the goal not absorbing"
|intros <-]
| IAlwaysElim ?pat =>
eapply tac_delayed_intuitionistic;
[iSolveTC ||
let P := match goal with |- IntoPersistent _ ?P _ => P end in
fail "iDestruct:" P "not persistent"
|pm_reduce; iSolveTC ||
let P := match goal with |- TCOr (Affine ?P) _ => P end in
fail "iDestruct:" P "not affine and the goal not absorbing"
|iFastDestructHypGo pat]
| IModalElim ?pat =>
eapply tac_delayed_modal;
[iSolveTC ||
let P := match goal with |- ElimModal _ _ _ ?P _ _ _ => P end in
let Q := match goal with |- ElimModal _ _ _ _ _ ?Q _ => Q end in
fail "iMod: cannot eliminate modality" P "in" Q
|iSolveSideCondition
|iFastDestructHypGo pat]
| _ => fail "iDestruct:" pat "invalid"
end.
Tactic Notation "iFastDestructHyp" constr(H) "as" constr(pat) :=
let pat := intro_pat.parse_one pat in
iStartProof;
notypeclasses refine (tac_delay_destruct _ _ H _);
pm_reduce;
lazymatch goal with
| |- False => fail "iDestruct:" H "not found"
| |- envs_entails_delayed ?Δ ?acts ?tmps ?Q =>
let HΔ := fresh "Δ" in
pose (HΔ := Δ);
convert_concl_no_check (envs_entails_delayed HΔ acts tmps Q);
iFastDestructHypGo pat;
notypeclasses refine (tac_force _ _ _ _);
unfold HΔ; clear HΔ;
pm_reduce;
lazymatch goal with
| |- False => fail "iDestruct: given names not fresh"
| |- _ => idtac
end
end.
Local Ltac iDestructHypFindPat Hgo pat found pats :=
lazymatch pats with
| [] =>
......@@ -1323,7 +1422,7 @@ Local Ltac iDestructHypFindPat Hgo pat found pats :=
| IClearFrame ?H :: ?pats => iFrame H; iDestructHypFindPat Hgo pat found pats
| ?pat :: ?pats =>
lazymatch found with
| false => iDestructHypGo Hgo pat; iDestructHypFindPat Hgo pat true pats
| false => iFastDestructHyp Hgo as pat; iDestructHypFindPat Hgo pat true pats
| true => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
end
end.
......
......@@ -192,7 +192,7 @@ Global Instance as_emp_valid_monPred_at_equiv φ P Q (Φ Ψ : I → PROP) :
Proof.
rewrite /AsEmpValid0 /AsEmpValid /MakeMonPredAt. intros -> EQ1 EQ2.
setoid_rewrite <-EQ1. setoid_rewrite <-EQ2. split.
- move=>/bi.wand_iff_equiv HP. setoid_rewrite HP. iIntros. iSplit; iIntros "$".
- move=>/bi.wand_iff_equiv HP. setoid_rewrite HP. iIntros. iSplit; by iIntros "$".
- move=>HP. apply bi.equiv_wand_iff. split=>i. by iSplit; iIntros; iApply HP.
Qed.
......