From 3f4685826e401d318cf044a0013610489d1f870b Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 22 Nov 2019 18:23:59 +0100
Subject: [PATCH] Fix iPoseProof on recursive lemmas (fix #274)

When proving `foo` through a fixpoint, Coq's guardedness checker needs to see to
which arguments `foo` is applied. Opaque lemmas applied to `foo` itself prevent
that, so make them transparent.
* Make `IntoEmpValid` lemmas transparent.
* Expose application of `IntoEmpValid` instance to its argument.
* Add comment to `tac_pose_proof`

This MR brings back the type of `tac_pose_proof` to the one it had before !329.
Hence, this seems worth a comment.
---
 tests/proofmode.v                 |  7 +++++++
 theories/proofmode/coq_tactics.v  | 26 +++++++++++++++++---------
 theories/proofmode/ltac_tactics.v |  2 +-
 3 files changed, 25 insertions(+), 10 deletions(-)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index fe6b8969a..1100315a6 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -12,6 +12,13 @@ Proof. eauto 6. Qed.
 Lemma test_eauto_isplit_biwand P : (P ∗-∗ P)%I.
 Proof. eauto. Qed.
 
+Fixpoint test_fixpoint (n : nat) {struct n} : True → emp ⊢@{PROP} ⌜ (n + 0)%nat = n ⌝%I.
+Proof.
+  case: n => [|n] /=; first (iIntros (_) "_ !%"; reflexivity).
+  iIntros (_) "_".
+  by iDestruct (test_fixpoint with "[//]") as %->.
+Qed.
+
 Check "demo_0".
 Lemma demo_0 P Q : □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P).
 Proof.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 62c140260..3018f180b 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -453,18 +453,26 @@ Proof.
 Qed.
 
 Definition IntoEmpValid (φ : Type) (P : PROP) := φ → bi_emp_valid P.
+(** These lemmas are [Defined] because the guardedness checker must see
+through them. See https://gitlab.mpi-sws.org/iris/iris/issues/274. For the
+same reason, their bodies use as little automation as possible. *)
 Lemma into_emp_valid_here φ P : AsEmpValid φ P → IntoEmpValid φ P.
-Proof. by intros [??]. Qed.
+Proof. by intros [??]. Defined.
 Lemma into_emp_valid_impl (φ ψ : Type) P :
   φ → IntoEmpValid ψ P → IntoEmpValid (φ → ψ) P.
-Proof. rewrite /IntoEmpValid; auto. Qed.
+Proof. rewrite /IntoEmpValid => Hφ Hi1 Hi2. apply Hi1, Hi2, Hφ. Defined.
 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 →
+Proof. rewrite /IntoEmpValid => Hi1 Hi2. apply Hi1, Hi2. Defined.
+Lemma into_emp_valid_proj φ P : IntoEmpValid φ P → φ → bi_emp_valid P.
+Proof. intros HP. apply HP. Defined.
+
+(** When called by the proof mode, the proof of [P] is produced by calling
+[into_emp_valid_proj]. That call must be transparent to the guardedness
+checker, per https://gitlab.mpi-sws.org/iris/iris/issues/274; hence, it must
+be done _outside_ [tac_pose_proof], so the latter can remain opaque. *)
+Lemma tac_pose_proof Δ j P Q :
+  P →
   match envs_app true (Esnoc Enil j P) Δ with
   | None => False
   | Some Δ' => envs_entails Δ' Q
@@ -472,8 +480,8 @@ Lemma tac_pose_proof Δ j (φ : Prop) 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 915b812d0..786f912f5 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -777,7 +777,7 @@ Ltac iIntoEmpValid :=
 
 Tactic Notation "iPoseProofCoreLem" open_constr(lem) "as" tactic3(tac) :=
   let Hnew := iFresh in
-  notypeclasses refine (tac_pose_proof _ Hnew _ _ _ lem _ _);
+  notypeclasses refine (tac_pose_proof _ Hnew _ _ (into_emp_valid_proj _ _ _ lem) _);
     [iIntoEmpValid
     |pm_reduce;
      lazymatch goal with
-- 
GitLab