Commit 8574d1ea authored by Robbert Krebbers's avatar Robbert Krebbers

Hide the proof mode entailment behind a definition.

This solves issue #100: the proof mode notation is sometimes not printed. As
Ralf discovered, the problem is that there are two overlapping notations:

```coq
Notation "P ⊢ Q" := (uPred_entails P Q).
```

And the "proof mode" notation:

```
Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
  (of_envs (Envs Γ Δ) ⊢ Q%I).
```

These two notations overlap, so, when having a "proof mode" goal of the shape
`of_envs (Envs Γ Δ) ⊢ Q%I`, how do we know which notation is Coq going to pick
for pretty printing this goal? As we have seen, this choice depends on the
import order (since both notations appear in different files), and as such, Coq
sometimes (unintendedly) uses the first notation instead of the latter.

The idea of this commit is to wrap `of_envs (Envs Γ Δ) ⊢ Q%I` into a definition
so that there is no ambiguity for the pretty printer anymore.
parent bd807e25
......@@ -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