Commit d5d02af5 authored by Robbert Krebbers's avatar Robbert Krebbers

Use `notypeclasses refine` in `iPoseProof` helpers.

Also, rewrite `iIntoEmpValid`. Now, instead of using Ltac to traverse
the type of the term and generate goals for the premises, we repeatedly
apply a series of lemmas. This has the advantage that it works up to
convertability, and we no longer need the `eval ...` hacks.
parent d9662274
...@@ -578,13 +578,13 @@ Tactic failure: iStartProof: not a BI assertion. ...@@ -578,13 +578,13 @@ Tactic failure: iStartProof: not a BI assertion.
The command has indeed failed with message: The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)", In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (tactic3)", "iPoseProofCore (open_constr) as (constr) (tactic3)",
"iPoseProofCoreLem (constr) as (tactic3)" and "iPoseProofCoreLem (open_constr) as (tactic3)" and
"<iris.proofmode.ltac_tactics.iIntoEmpValid>", last call failed. "iIntoEmpValid", last call failed.
Tactic failure: iPoseProof: not a BI assertion. Tactic failure: iPoseProof: (0 = 0) not a BI assertion.
The command has indeed failed with message: The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)", In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (tactic3)", "iPoseProofCore (open_constr) as (constr) (tactic3)",
"iPoseProofCoreLem (constr) as (tactic3)", "tac" (bound to "iPoseProofCoreLem (open_constr) as (tactic3)", "tac" (bound to
fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
fun H => iDestructHyp H as pat), "iDestructHyp (constr) as (constr)", fun H => iDestructHyp H as pat), "iDestructHyp (constr) as (constr)",
...@@ -604,7 +604,7 @@ Tactic failure: iPoseProof: "Hx" not found. ...@@ -604,7 +604,7 @@ Tactic failure: iPoseProof: "Hx" not found.
The command has indeed failed with message: The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)", In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (tactic3)", "iPoseProofCore (open_constr) as (constr) (tactic3)",
"iPoseProofCoreLem (constr) as (tactic3)", "tac" (bound to "iPoseProofCoreLem (open_constr) as (tactic3)", "tac" (bound to
fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "spec_tac" (bound to fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "spec_tac" (bound to
fun Htmp => fun Htmp =>
......
...@@ -271,7 +271,7 @@ Proof. ...@@ -271,7 +271,7 @@ Proof.
iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro. iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
{ by eapply lookup_insert_None. } { by eapply lookup_insert_None. }
{ by apply (lookup_insert_None (delete γ f) γ1 γ2 true). } { by apply (lookup_insert_None (delete γ f) γ1 γ2 true). }
iNext. iApply (internal_eq_rewrite_contractive _ _ (λ P, _) with "[Heq] Hbox"). iNext. iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq] Hbox").
iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2). iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
- iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done. - iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done.
iMod (slice_insert_empty with "Hbox") as (γ1 ?) "[#Hslice1 Hbox]". iMod (slice_insert_empty with "Hbox") as (γ1 ?) "[#Hslice1 Hbox]".
...@@ -279,7 +279,7 @@ Proof. ...@@ -279,7 +279,7 @@ Proof.
iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro. iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
{ by eapply lookup_insert_None. } { by eapply lookup_insert_None. }
{ by apply (lookup_insert_None (delete γ f) γ1 γ2 false). } { by apply (lookup_insert_None (delete γ f) γ1 γ2 false). }
iNext. iApply (internal_eq_rewrite_contractive _ _ (λ P, _) with "[Heq] Hbox"). iNext. iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq] Hbox").
iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2). iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
Qed. Qed.
...@@ -296,14 +296,14 @@ Proof. ...@@ -296,14 +296,14 @@ Proof.
iMod (slice_insert_full _ _ _ _ (Q1 Q2)%I with "[$HQ1 $HQ2] Hbox") iMod (slice_insert_full _ _ _ _ (Q1 Q2)%I with "[$HQ1 $HQ2] Hbox")
as (γ ?) "[#Hslice Hbox]"; first done. as (γ ?) "[#Hslice Hbox]"; first done.
iExists γ. iIntros "{$% $#} !>". iNext. iExists γ. iIntros "{$% $#} !>". iNext.
iApply (internal_eq_rewrite_contractive _ _ (λ P, _) with "[Heq1 Heq2] Hbox"). iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq1 Heq2] Hbox").
iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc. iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
- iMod (slice_delete_empty with "Hslice1 Hbox") as (P1) "(Heq1 & Hbox)"; try done. - iMod (slice_delete_empty with "Hslice1 Hbox") as (P1) "(Heq1 & Hbox)"; try done.
iMod (slice_delete_empty with "Hslice2 Hbox") as (P2) "(Heq2 & Hbox)"; first done. iMod (slice_delete_empty with "Hslice2 Hbox") as (P2) "(Heq2 & Hbox)"; first done.
{ by simplify_map_eq. } { by simplify_map_eq. }
iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]". iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
iExists γ. iIntros "{$% $#} !>". iNext. iExists γ. iIntros "{$% $#} !>". iNext.
iApply (internal_eq_rewrite_contractive _ _ (λ P, _) with "[Heq1 Heq2] Hbox"). iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq1 Heq2] Hbox").
iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc. iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
Qed. Qed.
End box. End box.
......
...@@ -95,7 +95,8 @@ Proof. iApply saved_anything_alloc. Qed. ...@@ -95,7 +95,8 @@ Proof. iApply saved_anything_alloc. Qed.
Lemma saved_prop_agree `{!savedPropG Σ} γ P Q : Lemma saved_prop_agree `{!savedPropG Σ} γ P Q :
saved_prop_own γ P - saved_prop_own γ Q - (P Q). saved_prop_own γ P - saved_prop_own γ Q - (P Q).
Proof. Proof.
iIntros "HP HQ". iApply later_equivI. iApply (saved_anything_agree with "HP HQ"). iIntros "HP HQ". iApply later_equivI.
iApply (saved_anything_agree (F := ) with "HP HQ").
Qed. Qed.
(* Saved predicates. *) (* Saved predicates. *)
...@@ -129,6 +130,6 @@ Lemma saved_pred_agree `{!savedPredG Σ A} γ Φ Ψ x : ...@@ -129,6 +130,6 @@ Lemma saved_pred_agree `{!savedPredG Σ A} γ Φ Ψ x :
saved_pred_own γ Φ - saved_pred_own γ Ψ - (Φ x Ψ x). saved_pred_own γ Φ - saved_pred_own γ Ψ - (Φ x Ψ x).
Proof. Proof.
unfold saved_pred_own. iIntros "#HΦ #HΨ /=". iApply later_equivI. unfold saved_pred_own. iIntros "#HΦ #HΨ /=". iApply later_equivI.
iDestruct (saved_anything_agree with "HΦ HΨ") as "Heq". iDestruct (saved_anything_agree (F := A -d> ) with "HΦ HΨ") as "Heq".
by iDestruct (discrete_fun_equivI with "Heq") as "?". by iDestruct (discrete_fun_equivI with "Heq") as "?".
Qed. Qed.
...@@ -108,7 +108,7 @@ Section greatest. ...@@ -108,7 +108,7 @@ Section greatest.
F (bi_greatest_fixpoint F) x bi_greatest_fixpoint F x. F (bi_greatest_fixpoint F) x bi_greatest_fixpoint F x.
Proof. Proof.
iIntros "HF". iExists (OfeMor (F (bi_greatest_fixpoint F))). iIntros "HF". iExists (OfeMor (F (bi_greatest_fixpoint F))).
iSplit; last done. iIntros "!#" (y) "Hy". iApply (bi_mono_pred with "[#] Hy"). iSplit; last done. iIntros "!#" (y) "Hy /=". iApply (bi_mono_pred with "[#] Hy").
iIntros "!#" (z) "?". by iApply greatest_fixpoint_unfold_1. iIntros "!#" (z) "?". by iApply greatest_fixpoint_unfold_1.
Qed. Qed.
......
...@@ -452,8 +452,19 @@ Proof. ...@@ -452,8 +452,19 @@ Proof.
by rewrite -(entails_wand P) // intuitionistically_emp emp_wand. by rewrite -(entails_wand P) // intuitionistically_emp emp_wand.
Qed. Qed.
Lemma tac_pose_proof Δ j P Q : Definition IntoEmpValid (φ : Type) (P : PROP) := φ bi_emp_valid P.
P Lemma into_emp_valid_here φ P : AsEmpValid φ P IntoEmpValid φ P.
Proof. by intros [??]. Qed.
Lemma into_emp_valid_impl (φ ψ : Type) P :
φ IntoEmpValid ψ P IntoEmpValid (φ ψ) P.
Proof. rewrite /IntoEmpValid; auto. Qed.
Lemma into_emp_valid_forall {A} (φ : A Type) P x :
IntoEmpValid (φ x) P IntoEmpValid ( x : A, φ x) P.
Proof. rewrite /IntoEmpValid; auto. Qed.
Lemma tac_pose_proof Δ j (φ : Prop) P Q :
φ
IntoEmpValid φ P
match envs_app true (Esnoc Enil j P) Δ with match envs_app true (Esnoc Enil j P) Δ with
| None => False | None => False
| Some Δ' => envs_entails Δ' Q | Some Δ' => envs_entails Δ' Q
...@@ -461,8 +472,8 @@ Lemma tac_pose_proof Δ j P Q : ...@@ -461,8 +472,8 @@ Lemma tac_pose_proof Δ j P Q :
envs_entails Δ Q. envs_entails Δ Q.
Proof. Proof.
destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done. destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
rewrite envs_entails_eq => HP ?. rewrite envs_app_singleton_sound //=. rewrite envs_entails_eq => ? HP <-. rewrite envs_app_singleton_sound //=.
by rewrite -HP /= intuitionistically_emp emp_wand. by rewrite -HP //= intuitionistically_emp emp_wand.
Qed. Qed.
Lemma tac_pose_proof_hyp Δ i j Q : Lemma tac_pose_proof_hyp Δ i j Q :
......
...@@ -720,58 +720,9 @@ Notation "( H $! x1 .. xn 'with' pat )" := ...@@ -720,58 +720,9 @@ Notation "( H $! x1 .. xn 'with' pat )" :=
(ITrm H (hcons x1 .. (hcons xn hnil) ..) pat) (at level 0, x1, xn at level 9). (ITrm H (hcons x1 .. (hcons xn hnil) ..) pat) (at level 0, x1, xn at level 9).
Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0). Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0).
(* The tactic [iIntoEmpValid] tactic solves a goal [bi_emp_valid ?Q]. The
argument [t] must be a Coq term whose type is of the following shape:
[∀ (x_1 : A_1) .. (x_n : A_n), φ]
for which we have an instance [AsEmpValid φ ?Q].
Examples of such [φ]s are
- [bi_emp_valid P], in which case [Q] is unified with [P].
- [P1 ⊢ P2], in which case [Q] is unified with [P1 -∗ P2].
- [P1 ⊣⊢ P2], in which case [Q] is unified with [P1 ↔ P2].
The tactic instantiates each dependent argument [x_i : A_i] with an evar and
generates a goal [A_i] for each non-dependent argument [x_i : A_i].
For example, if the initial goal is [bi_emp_valid ?Q] and [t] has type
[∀ x, P x → R x], then it generates an evar [?x] for [x], a subgoal [P ?x],
and unifies [?Q] with [R x]. *)
Local Ltac iIntoEmpValid t :=
let go_specialize t tT :=
lazymatch tT with (* We do not use hnf of tT, because, if
entailment is not opaque, then it would
unfold it. *)
| ?P ?Q => let H := fresh in assert P as H; [|iIntoEmpValid uconstr:(t H); clear H]
| _ : ?T, _ =>
(* Put [T] inside an [id] to avoid TC inference from being invoked. *)
(* This is a workarround for Coq bug #6583. *)
let e := fresh in evar (e:id T);
let e' := eval unfold e in e in clear e; iIntoEmpValid (t e')
end
in
(* We try two reduction tactics for the type of t before trying to
specialize it. We first try the head normal form in order to
unfold all the definition that could hide an entailment. Then,
we try the much weaker [eval cbv zeta], because entailment is
not necessarilly opaque, and could be unfolded by [hnf].
However, for calling type class search, we only use [cbv zeta]
in order to make sure we do not unfold [bi_emp_valid]. *)
let tT := type of t in
first
[ let tT' := eval hnf in tT in go_specialize t tT'
| let tT' := eval cbv zeta in tT in go_specialize t tT'
| let tT' := eval cbv zeta in tT in
notypeclasses refine (as_emp_valid_1 tT _ _);
[iSolveTC || fail 1 "iPoseProof: not a BI assertion"
|exact t]].
Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) := Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
let Δ := iGetCtx in let Δ := iGetCtx in
eapply tac_pose_proof_hyp with H Hnew; notypeclasses refine (tac_pose_proof_hyp _ H Hnew _ _);
pm_reduce; pm_reduce;
lazymatch goal with lazymatch goal with
| |- False => | |- False =>
...@@ -787,10 +738,47 @@ Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) := ...@@ -787,10 +738,47 @@ Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
| _ => idtac | _ => idtac
end. end.
Tactic Notation "iPoseProofCoreLem" constr(lem) "as" tactic3(tac) := (* The tactic [iIntoEmpValid] tactic "imports a Coq lemma into the proofmode",
i.e. it solves a goal [IntoEmpValid ψ ?Q]. The argument [ψ] must be of the
following shape:
[∀ (x_1 : A_1) .. (x_n : A_n), φ]
for which we have an instance [AsEmpValid φ ?Q].
Examples of such [φ]s are
- [bi_emp_valid P], in which case [?Q] is unified with [P].
- [P1 ⊢ P2], in which case [?Q] is unified with [P1 -∗ P2].
- [P1 ⊣⊢ P2], in which case [?Q] is unified with [P1 ↔ P2].
The tactic instantiates each dependent argument [x_i : A_i] with an evar, and
generates a goal [A_i] for each non-dependent argument [x_i : A_i].
For example, if goal is [bi_emp_valid (∀ x, P x → R1 x ⊢ R2 x) ?Q], then the
[iIntoEmpValid] tactic generates an evar [?x], a subgoal [P ?x], and unifies
[?Q] with [R1 ?x -∗ R2 ?x]. *)
Ltac iIntoEmpValid_go := first
[(* Case [φ → ψ] *)
notypeclasses refine (into_emp_valid_impl _ _ _ _ _);
[(*goal for [φ] *)|iIntoEmpValid_go]
|(* Case [∀ x : A, φ] *)
notypeclasses refine (into_emp_valid_forall _ _ _ _); iIntoEmpValid_go
|(* Case [P ⊢ Q], [P ⊣⊢ Q], [bi_emp_valid P] *)
notypeclasses refine (into_emp_valid_here _ _ _)].
Ltac iIntoEmpValid :=
(* Factor out the base case of the loop to avoid needless backtracking *)
iIntoEmpValid_go;
[.. (* goals for premises *)
|iSolveTC ||
let φ := lazymatch goal with |- AsEmpValid ?φ _ => φ end in
fail "iPoseProof:" φ "not a BI assertion"].
Tactic Notation "iPoseProofCoreLem" open_constr(lem) "as" tactic3(tac) :=
let Hnew := iFresh in let Hnew := iFresh in
eapply tac_pose_proof with Hnew _; (* (j:=H) *) notypeclasses refine (tac_pose_proof _ Hnew _ _ _ lem _ _);
[iIntoEmpValid lem [iIntoEmpValid
|pm_reduce; |pm_reduce;
lazymatch goal with lazymatch goal with
| |- False => | |- 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