Commit 777cf634 authored by Robbert's avatar Robbert

Merge branch 'proofmode_notation_fix' into 'master'

Make proofnode notation more robust in the context of import order

See merge request FP/iris-coq!75
parents bd807e25 8574d1ea
......@@ -8,7 +8,7 @@ Module Import uPred.
End uPred.
(* Hint DB for the logic *)
Hint Resolve pure_intro.
Hint Resolve pure_intro : I.
Hint Resolve or_elim or_intro_l' or_intro_r' : I.
Hint Resolve and_intro and_elim_l' and_elim_r' : I.
Hint Resolve persistently_mono : I.
......
......@@ -330,7 +330,7 @@ Section gmap.
intros. apply (anti_symm _).
{ apply forall_intro=> k; apply forall_intro=> x.
apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
induction m as [|i x m ? IH] using map_ind; [rewrite ?big_sepM_empty; auto|].
induction m as [|i x m ? IH] using map_ind; auto using big_sepM_empty'.
rewrite big_sepM_insert // -and_sep_l. apply and_intro.
- rewrite (forall_elim i) (forall_elim x) lookup_insert.
by rewrite pure_True // True_impl.
......@@ -488,8 +488,7 @@ Section gset.
intros. apply (anti_symm _).
{ apply forall_intro=> x.
apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
induction X as [|x X ? IH] using collection_ind_L.
{ rewrite big_sepS_empty; auto. }
induction X as [|x X ? IH] using collection_ind_L; auto using big_sepS_empty'.
rewrite big_sepS_insert // -and_sep_l. apply and_intro.
- by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
- rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
......@@ -619,5 +618,3 @@ Section gmultiset.
Proof. rewrite /big_opMS. apply _. Qed.
End gmultiset.
End big_op.
Hint Resolve big_sepL_nil' big_sepM_empty' big_sepS_empty' big_sepMS_empty' | 0.
......@@ -224,7 +224,7 @@ Section proofmode_classes.
Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
End proofmode_classes.
Hint Extern 2 (coq_tactics.of_envs _ |={_}=> _) => iModIntro.
Hint Extern 2 (coq_tactics.envs_entails _ (|={_}=> _)) => iModIntro.
(** Fancy updates that take a step. *)
......
......@@ -9,20 +9,25 @@ Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ :
PureExec φ e1 e2
φ
IntoLaterNEnvs 1 Δ Δ'
(Δ' WP fill K e2 @ E {{ Φ }})
(Δ WP fill K e1 @ E {{ Φ }}).
envs_entails Δ' (WP fill K e2 @ E {{ Φ }})
envs_entails Δ (WP fill K e1 @ E {{ Φ }}).
Proof.
intros ??? HΔ'. rewrite into_laterN_env_sound /=.
rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=.
rewrite -lifting.wp_bind HΔ' -wp_pure_step_later //.
by rewrite -ectx_lifting.wp_ectx_bind_inv.
Qed.
Ltac wp_value_head := etrans; [|eapply wp_value; apply _]; simpl.
Lemma tac_wp_value `{heapG Σ} Δ E Φ e v :
IntoVal e v
envs_entails Δ (Φ v) envs_entails Δ (WP e @ E {{ Φ }}).
Proof. rewrite /envs_entails=> ? ->. by apply wp_value. Qed.
Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
Tactic Notation "wp_pure" open_constr(efoc) :=
iStartProof;
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
| |- envs_entails _ (wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
unify e' efoc;
eapply (tac_wp_pure K);
[simpl; apply _ (* PureExec *)
......@@ -47,16 +52,21 @@ Tactic Notation "wp_proj" := wp_pure (Fst _) || wp_pure (Snd _).
Tactic Notation "wp_case" := wp_pure (Case _ _ _).
Tactic Notation "wp_match" := wp_case; wp_let.
Lemma tac_wp_bind `{heapG Σ} K Δ E Φ e :
envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I
envs_entails Δ (WP fill K e @ E {{ Φ }}).
Proof. rewrite /envs_entails=> ->. by apply wp_bind. Qed.
Ltac wp_bind_core K :=
lazymatch eval hnf in K with
| [] => idtac
| _ => etrans; [|fast_by apply (wp_bind K)]; simpl
| _ => apply (tac_wp_bind K); simpl
end.
Tactic Notation "wp_bind" open_constr(efoc) :=
iStartProof;
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
| |- envs_entails _ (wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
match e' with
| efoc => unify e' efoc; wp_bind_core K
end) || fail "wp_bind: cannot find" efoc "in" e
......@@ -75,10 +85,11 @@ Lemma tac_wp_alloc Δ Δ' E j K e v Φ :
IntoLaterNEnvs 1 Δ Δ'
( l, Δ'',
envs_app false (Esnoc Enil j (l v)) Δ' = Some Δ''
(Δ'' WP fill K (Lit (LitLoc l)) @ E {{ Φ }}))
Δ WP fill K (Alloc e) @ E {{ Φ }}.
envs_entails Δ'' (WP fill K (Lit (LitLoc l)) @ E {{ Φ }}))
envs_entails Δ (WP fill K (Alloc e) @ E {{ Φ }}).
Proof.
intros ?? HΔ. rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
rewrite /envs_entails=> ?? HΔ.
rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
by rewrite right_id HΔ'.
......@@ -87,10 +98,11 @@ Qed.
Lemma tac_wp_load Δ Δ' E i K l q v Φ :
IntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I
(Δ' WP fill K (of_val v) @ E {{ Φ }})
Δ WP fill K (Load (Lit (LitLoc l))) @ E {{ Φ }}.
envs_entails Δ' (WP fill K (of_val v) @ E {{ Φ }})
envs_entails Δ (WP fill K (Load (Lit (LitLoc l))) @ E {{ Φ }}).
Proof.
intros. rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
rewrite /envs_entails=> ???.
rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
by apply later_mono, sep_mono_r, wand_mono.
Qed.
......@@ -100,10 +112,11 @@ Lemma tac_wp_store Δ Δ' Δ'' E i K l v e v' Φ :
IntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v')) Δ' = Some Δ''
(Δ'' WP fill K (Lit LitUnit) @ E {{ Φ }})
Δ WP fill K (Store (Lit (LitLoc l)) e) @ E {{ Φ }}.
envs_entails Δ'' (WP fill K (Lit LitUnit) @ E {{ Φ }})
envs_entails Δ (WP fill K (Store (Lit (LitLoc l)) e) @ E {{ Φ }}).
Proof.
intros. rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
rewrite /envs_entails=> ?????.
rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
......@@ -112,10 +125,11 @@ Lemma tac_wp_cas_fail Δ Δ' E i K l q v e1 v1 e2 Φ :
IntoVal e1 v1 AsVal e2
IntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I v v1
(Δ' WP fill K (Lit (LitBool false)) @ E {{ Φ }})
Δ WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}.
envs_entails Δ' (WP fill K (Lit (LitBool false)) @ E {{ Φ }})
envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}).
Proof.
intros. rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail.
rewrite /envs_entails=> ??????.
rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail.
rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
by apply later_mono, sep_mono_r, wand_mono.
Qed.
......@@ -125,10 +139,11 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' E i K l v e1 v1 e2 v2 Φ :
IntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I v = v1
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ''
(Δ'' WP fill K (Lit (LitBool true)) @ E {{ Φ }})
Δ WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}.
envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ E {{ Φ }})
envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}).
Proof.
intros; subst. rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
rewrite /envs_entails=> ???????; subst.
rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
......@@ -137,7 +152,7 @@ End heap.
Tactic Notation "wp_apply" open_constr(lem) :=
iPoseProofCore lem as false true (fun H =>
lazymatch goal with
| |- _ wp ?E ?e ?Q =>
| |- envs_entails _ (wp ?E ?e ?Q) =>
reshape_expr e ltac:(fun K e' =>
wp_bind_core K; iApplyHyp H; try iNext; simpl) ||
lazymatch iTypeOf H with
......@@ -149,7 +164,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
iStartProof;
lazymatch goal with
| |- _ wp ?E ?e ?Q =>
| |- envs_entails _ (wp ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' =>
eapply (tac_wp_alloc _ _ _ H K); [apply _|..])
......@@ -168,7 +183,7 @@ Tactic Notation "wp_alloc" ident(l) :=
Tactic Notation "wp_load" :=
iStartProof;
lazymatch goal with
| |- _ wp ?E ?e ?Q =>
| |- envs_entails _ (wp ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ K))
|fail 1 "wp_load: cannot find 'Load' in" e];
......@@ -182,7 +197,7 @@ Tactic Notation "wp_load" :=
Tactic Notation "wp_store" :=
iStartProof;
lazymatch goal with
| |- _ wp ?E ?e ?Q =>
| |- envs_entails _ (wp ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' =>
eapply (tac_wp_store _ _ _ _ _ K); [apply _|..])
......@@ -198,7 +213,7 @@ Tactic Notation "wp_store" :=
Tactic Notation "wp_cas_fail" :=
iStartProof;
lazymatch goal with
| |- _ wp ?E ?e ?Q =>
| |- envs_entails _ (wp ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' =>
eapply (tac_wp_cas_fail _ _ _ _ K); [apply _|apply _|..])
......@@ -214,7 +229,7 @@ Tactic Notation "wp_cas_fail" :=
Tactic Notation "wp_cas_suc" :=
iStartProof;
lazymatch goal with
| |- _ wp ?E ?e ?Q =>
| |- envs_entails _ (wp ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' =>
eapply (tac_wp_cas_suc _ _ _ _ _ K); [apply _|apply _|..])
......
This diff is collapsed.
......@@ -11,18 +11,19 @@ Notation "" := Enil (only printing) : proof_scope.
Notation "Γ H : P" := (Esnoc Γ H P)
(at level 1, P at level 200,
left associativity, format "Γ H : P '//'", only printing) : proof_scope.
Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
(of_envs (Envs Γ Δ) Q%I)
(envs_entails (Envs Γ Δ) Q%I)
(at level 1, Q at level 200, left associativity,
format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q '//'", only printing) :
C_scope.
Notation "Δ '--------------------------------------' ∗ Q" :=
(of_envs (Envs Enil Δ) Q%I)
(envs_entails (Envs Enil Δ) Q%I)
(at level 1, Q at level 200, left associativity,
format "Δ '--------------------------------------' ∗ '//' Q '//'", only printing) : C_scope.
Notation "Γ '--------------------------------------' □ Q" :=
(of_envs (Envs Γ Enil) Q%I)
(envs_entails (Envs Γ Enil) Q%I)
(at level 1, Q at level 200, left associativity,
format "Γ '--------------------------------------' □ '//' Q '//'", only printing) : C_scope.
Notation "'--------------------------------------' ∗ Q" := (of_envs (Envs Enil Enil) Q%I)
Notation "'--------------------------------------' ∗ Q" := (envs_entails (Envs Enil Enil) Q%I)
(at level 1, Q at level 200, format "'--------------------------------------' ∗ '//' Q '//'", only printing) : C_scope.
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Import base intro_patterns spec_patterns sel_patterns.
From iris.base_logic Require Export base_logic.
From iris.base_logic Require Export base_logic big_op.
From iris.proofmode Require Export classes notation.
From iris.proofmode Require Import class_instances.
From stdpp Require Import stringmap hlist.
......@@ -22,7 +22,7 @@ Ltac env_reflexivity := env_cbv; exact eq_refl.
(* Tactic Notation tactics cannot return terms *)
Ltac iFresh' H :=
lazymatch goal with
|- of_envs ?Δ _ =>
|- envs_entails ?Δ _ =>
(* [vm_compute fails] if any of the hypotheses in [Δ] contain evars, so
first use [cbv] to compute the domain of [Δ] *)
let Hs := eval cbv in (envs_dom Δ) in
......@@ -34,14 +34,14 @@ Ltac iFresh := iFresh' "~".
Ltac iMissingHyps Hs :=
let Δ :=
lazymatch goal with
| |- of_envs ?Δ _ => Δ
| |- envs_entails ?Δ _ => Δ
| |- context[ envs_split _ _ ?Δ ] => Δ
end in
let Hhyps := eval env_cbv in (envs_dom Δ) in
eval vm_compute in (list_difference Hs Hhyps).
Ltac iTypeOf H :=
let Δ := match goal with |- of_envs ?Δ _ => Δ end in
let Δ := match goal with |- envs_entails ?Δ _ => Δ end in
eval env_cbv in (envs_lookup H Δ).
Tactic Notation "iMatchHyp" tactic1(tac) :=
......@@ -64,7 +64,7 @@ Proof. split. apply uPred.equiv_iff. apply uPred.iff_equiv. Qed.
(** * Start a proof *)
Ltac iStartProof :=
lazymatch goal with
| |- of_envs _ _ => idtac
| |- envs_entails _ _ => idtac
| |- ?P =>
apply (proj2 (_ : AsValid P _)), tac_adequate
|| fail "iStartProof: not a uPred"
......@@ -100,7 +100,7 @@ Ltac iElaborateSelPat pat :=
end
end in
lazymatch goal with
| |- of_envs ?Δ _ =>
| |- envs_entails ?Δ _ =>
let pat := sel_pat.parse pat in go pat Δ (@nil esel_pat)
end.
......@@ -152,7 +152,7 @@ Tactic Notation "iAssumption" :=
|find p Γ Q]
end in
match goal with
| |- of_envs (Envs ?Γp ?Γs) ?Q =>
| |- envs_entails (Envs ?Γp ?Γs) ?Q =>
first [find true Γp Q | find false Γs Q
|fail "iAssumption:" Q "not found"]
end.
......@@ -189,7 +189,7 @@ Tactic Notation "iPureIntro" :=
Local Ltac iFrameFinish :=
lazy iota beta;
try match goal with
| |- _ True => exact (uPred.pure_intro _ _ I)
| |- envs_entails _ True => exact (uPred.pure_intro _ _ I)
end.
Local Ltac iFramePure t :=
......@@ -213,7 +213,7 @@ Local Ltac iFrameAnyPersistent :=
let rec go Hs :=
match Hs with [] => idtac | ?H :: ?Hs => repeat iFrameHyp H; go Hs end in
match goal with
| |- of_envs ?Δ _ =>
| |- envs_entails ?Δ _ =>
let Hs := eval cbv in (env_dom (env_persistent Δ)) in go Hs
end.
......@@ -221,7 +221,7 @@ Local Ltac iFrameAnySpatial :=
let rec go Hs :=
match Hs with [] => idtac | ?H :: ?Hs => try iFrameHyp H; go Hs end in
match goal with
| |- of_envs ?Δ _ =>
| |- envs_entails ?Δ _ =>
let Hs := eval cbv in (env_dom (env_spatial Δ)) in go Hs
end.
......@@ -284,7 +284,7 @@ Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
try iStartProof;
lazymatch goal with
| |- _ _ =>
| |- envs_entails _ _ =>
eapply tac_forall_intro;
[apply _ ||
let P := match goal with |- FromForall ?P _ => P end in
......@@ -342,14 +342,14 @@ Local Tactic Notation "iIntroForall" :=
lazymatch goal with
| |- _, ?P => fail
| |- _, _ => intro
| |- _ ( x : _, _) => let x' := fresh x in iIntro (x')
| |- envs_entails _ ( x : _, _) => let x' := fresh x in iIntro (x')
end.
Local Tactic Notation "iIntro" :=
try iStartProof;
lazymatch goal with
| |- _ ?P => intro
| |- _ (_ - _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
| |- _ (_ _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
| |- envs_entails _ (_ - _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
| |- envs_entails _ (_ _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
end.
(** * Specialize *)
......@@ -692,13 +692,10 @@ Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
(** * Conjunction and separating conjunction *)
Tactic Notation "iSplit" :=
iStartProof;
lazymatch goal with
| |- _ _ =>
eapply tac_and_split;
[apply _ ||
let P := match goal with |- FromAnd _ ?P _ _ => P end in
fail "iSplit:" P "not a conjunction"| |]
end.
eapply tac_and_split;
[apply _ ||
let P := match goal with |- FromAnd _ ?P _ _ => P end in
fail "iSplit:" P "not a conjunction"| |].
Tactic Notation "iSplitL" constr(Hs) :=
iStartProof;
......@@ -809,7 +806,7 @@ Tactic Notation "iAlways":=
(** * Later *)
Tactic Notation "iNext" open_constr(n) :=
iStartProof;
let P := match goal with |- _ ?P => P end in
let P := match goal with |- envs_entails _ ?P => P end in
try lazymatch n with 0 => fail 1 "iNext: cannot strip 0 laters" end;
eapply (tac_next _ _ n);
[apply _ || fail "iNext:" P "does not contain" n "laters"
......@@ -1357,7 +1354,7 @@ result in the following actions:
Tactic Notation "iInductionCore" constr(x) "as" simple_intropattern(pat) constr(IH) :=
let rec fix_ihs :=
lazymatch goal with
| H : context [coq_tactics.of_envs _ _] |- _ =>
| H : context [envs_entails _ _] |- _ =>
eapply (tac_revert_ih _ _ _ H _);
[reflexivity
|| fail "iInduction: spatial context not empty, this should not happen"|];
......@@ -1377,8 +1374,8 @@ Ltac iHypsContaining x :=
| _ => go Γ x Hs
end
end in
let Γp := lazymatch goal with |- of_envs (Envs ?Γp _) _ => Γp end in
let Γs := lazymatch goal with |- of_envs (Envs _ ?Γs) _ => Γs end in
let Γp := lazymatch goal with |- envs_entails (Envs ?Γp _) _ => Γp end in
let Γs := lazymatch goal with |- envs_entails (Envs _ ?Γs) _ => Γs end in
let Hs := go Γp x (@nil string) in go Γs x Hs.
Tactic Notation "iInductionRevert" constr(x) constr(Hs) "with" tactic(tac) :=
......@@ -1703,24 +1700,33 @@ 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).
Hint Extern 0 (_ _) => iStartProof.
(* Make sure that by and done solve trivial things in proof mode *)
Hint Extern 0 (of_envs _ _) => by iPureIntro.
Hint Extern 0 (of_envs _ _) => iAssumption.
Hint Resolve uPred.internal_eq_refl'. (* Maybe make an [iReflexivity] tactic *)
(* For iIntros we do not check whether we are in proof mode because we actually
want it to enter proof mode when we are not already in it. *)
Hint Extern 0 (_ _) => progress iIntros.
Hint Extern 1 (of_envs _ _ _) => iSplit.
Hint Extern 1 (of_envs _ _ _) => iSplit.
Hint Extern 1 (of_envs _ _) => iNext.
Hint Extern 1 (of_envs _ _) => iAlways.
Hint Extern 1 (of_envs _ _) => iAlways.
Hint Extern 1 (of_envs _ _, _) => iExists _.
Hint Extern 1 (of_envs _ |==> _) => iModIntro.
Hint Extern 1 (of_envs _ _) => iModIntro.
Hint Extern 1 (of_envs _ _ _) => iLeft.
Hint Extern 1 (of_envs _ _ _) => iRight.
Hint Extern 2 (of_envs _ _ _) => progress iFrame : iFrame.
Hint Extern 0 (envs_entails _ _) => iPureIntro; try done.
Hint Extern 0 (envs_entails _ _) => iAssumption.
(* TODO: look for a more principled way of adding trivial hints like those
below; see the discussion in !75 for further details. *)
Hint Extern 0 (envs_entails _ (_ _)) => apply uPred.internal_eq_refl'.
Hint Extern 0 (envs_entails _ (big_opL _ _ _)) => apply big_sepL_nil'.
Hint Extern 0 (envs_entails _ (big_opM _ _ _)) => apply big_sepM_empty'.
Hint Extern 0 (envs_entails _ (big_opS _ _ _)) => apply big_sepS_empty'.
Hint Extern 0 (envs_entails _ (big_opMS _ _ _)) => apply big_sepMS_empty'.
Hint Extern 0 (envs_entails _ ( _, _)) => iIntros.
Hint Extern 0 (envs_entails _ (_ _)) => iIntros.
Hint Extern 0 (envs_entails _ (_ - _)) => iIntros.
Hint Extern 1 (envs_entails _ (_ _)) => iSplit.
Hint Extern 1 (envs_entails _ (_ _)) => iSplit.
Hint Extern 1 (envs_entails _ ( _)) => iNext.
Hint Extern 1 (envs_entails _ ( _)) => iAlways.
Hint Extern 1 (envs_entails _ ( _)) => iAlways.
Hint Extern 1 (envs_entails _ ( _, _)) => iExists _.
Hint Extern 1 (envs_entails _ (|==> _)) => iModIntro.
Hint Extern 1 (envs_entails _ ( _)) => iModIntro.
Hint Extern 1 (envs_entails _ (_ _)) => iLeft.
Hint Extern 1 (envs_entails _ (_ _)) => iRight.
Hint Extern 2 (envs_entails _ (_ _)) => progress iFrame : iFrame.
......@@ -144,7 +144,7 @@ Qed.
Lemma test_eauto_iFramE P Q R `{!Persistent R} :
P - Q - R - R Q P R False.
Proof. eauto with iFrame. Qed.
Proof. eauto 10 with iFrame. Qed.
Lemma test_iCombine_persistent P Q R `{!Persistent R} :
P - Q - R - R Q P R False.
......
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