From d5d02af503ed73343a0b954df016cf6e414801c3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Fri, 8 Nov 2019 16:41:51 +0100
Subject: [PATCH] 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.

tests/proofmode.ref  10 +
theories/base_logic/lib/boxes.v  8 +
theories/base_logic/lib/saved_prop.v  5 +
theories/bi/lib/fixpoint.v  2 +
theories/proofmode/coq_tactics.v  19 ++++
theories/proofmode/ltac_tactics.v  94 ++++++++++++
6 files changed, 69 insertions(+), 69 deletions()
diff git a/tests/proofmode.ref b/tests/proofmode.ref
index 51b84fa2..6cbde74a 100644
 a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ 578,13 +578,13 @@ Tactic failure: iStartProof: not a BI assertion.
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (tactic3)",
"iPoseProofCoreLem (constr) as (tactic3)" and
"", last call failed.
Tactic failure: iPoseProof: not a BI assertion.
+"iPoseProofCoreLem (open_constr) as (tactic3)" and
+"iIntoEmpValid", last call failed.
+Tactic failure: iPoseProof: (0 = 0) not a BI assertion.
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"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 H => iDestructHyp H as pat), "iDestructHyp (constr) as (constr)",
@@ 604,7 +604,7 @@ Tactic failure: iPoseProof: "Hx" not found.
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"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 ]), "spec_tac" (bound to
fun Htmp =>
diff git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 3e76db38..5a17f50c 100644
 a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ 271,7 +271,7 @@ Proof.
iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
{ by eapply lookup_insert_None. }
{ 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).
 iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done.
iMod (slice_insert_empty with "Hbox") as (γ1 ?) "[#Hslice1 Hbox]".
@@ 279,7 +279,7 @@ Proof.
iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
{ by eapply lookup_insert_None. }
{ 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).
Qed.
@@ 296,14 +296,14 @@ Proof.
iMod (slice_insert_full _ _ _ _ (Q1 ∗ Q2)%I with "[$HQ1 $HQ2] Hbox")
as (γ ?) "[#Hslice Hbox]"; first done.
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.
 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.
{ by simplify_map_eq. }
iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
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.
Qed.
End box.
diff git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 7f096f39..8e1a9e59 100644
 a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ 95,7 +95,8 @@ Proof. iApply saved_anything_alloc. Qed.
Lemma saved_prop_agree `{!savedPropG Σ} γ P Q :
saved_prop_own γ P ∗ saved_prop_own γ Q ∗ ▷ (P ≡ Q).
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.
(* Saved predicates. *)
@@ 129,6 +130,6 @@ Lemma saved_pred_agree `{!savedPredG Σ A} γ Φ Ψ x :
saved_pred_own γ Φ ∗ saved_pred_own γ Ψ ∗ ▷ (Φ x ≡ Ψ x).
Proof.
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 "?".
Qed.
diff git a/theories/bi/lib/fixpoint.v b/theories/bi/lib/fixpoint.v
index 1423040d..df9083d3 100644
 a/theories/bi/lib/fixpoint.v
+++ b/theories/bi/lib/fixpoint.v
@@ 108,7 +108,7 @@ Section greatest.
F (bi_greatest_fixpoint F) x ⊢ bi_greatest_fixpoint F x.
Proof.
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.
Qed.
diff git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 72164546..62c14026 100644
 a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ 452,8 +452,19 @@ Proof.
by rewrite (entails_wand P) // intuitionistically_emp emp_wand.
Qed.
Lemma tac_pose_proof Δ j P Q :
 P →
+Definition IntoEmpValid (φ : Type) (P : PROP) := φ → bi_emp_valid 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
 None => False
 Some Δ' => envs_entails Δ' Q
@@ 461,8 +472,8 @@ Lemma tac_pose_proof Δ j P Q :
envs_entails Δ Q.
Proof.
destruct (envs_app _ _ _) as [Δ'] eqn:?; last done.
 rewrite envs_entails_eq => HP ?. rewrite envs_app_singleton_sound //=.
 by rewrite HP /= intuitionistically_emp emp_wand.
+ rewrite envs_entails_eq => ? HP <. rewrite envs_app_singleton_sound //=.
+ by rewrite HP //= intuitionistically_emp emp_wand.
Qed.
Lemma tac_pose_proof_hyp Δ i j Q :
diff git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index fbde9ca8..915b812d 100644
 a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ 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).
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 nondependent 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) :=
let Δ := iGetCtx in
 eapply tac_pose_proof_hyp with H Hnew;
+ notypeclasses refine (tac_pose_proof_hyp _ H Hnew _ _);
pm_reduce;
lazymatch goal with
  False =>
@@ 787,10 +738,47 @@ Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
 _ => idtac
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 nondependent 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
 eapply tac_pose_proof with Hnew _; (* (j:=H) *)
 [iIntoEmpValid lem
+ notypeclasses refine (tac_pose_proof _ Hnew _ _ _ lem _ _);
+ [iIntoEmpValid
pm_reduce;
lazymatch goal with
  False =>

2.24.1