Commit 3f468582 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso Committed by Robbert

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.
parent a979391c
......@@ -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.
......
......@@ -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 :
......
......@@ -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
......
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