Commit 10a93b0b authored by Robbert Krebbers's avatar Robbert Krebbers

Improve True stripping of iPoseProof.

It is no longer triggered when posing [P ⊢ Q] with [P] an evar. This, for
example, makes sure that iApply pvs_intro works, which failed before.
parent d3622918
Pipeline #567 passed with stage
......@@ -560,12 +560,23 @@ Proof.
by rewrite right_id {1}(persistentP P) always_and_sep_l wand_elim_r.
Qed.
Lemma tac_pose_proof Δ Δ' j P Q :
True P envs_app true (Esnoc Enil j P) Δ = Some Δ'
(** Whenever posing [lem : True ⊢ Q] as [H} we want it to appear as [H : Q] and
not as [H : True -★ Q]. The class [ToPosedProof] is used to strip off the
[True]. Note that [to_posed_proof_True] is declared using a [Hint Extern] to
make sure it is not used while posing [lem : ?P ⊢ Q] with [?P] an evar. *)
Class ToPosedProof (P1 P2 R : uPred M) := to_pose_proof : P1 P2 True R.
Arguments to_pose_proof : clear implicits.
Instance to_posed_proof_True P : ToPosedProof True P P.
Proof. by rewrite /ToPosedProof. Qed.
Global Instance to_posed_proof_wand P Q : ToPosedProof P Q (P - Q).
Proof. rewrite /ToPosedProof. apply entails_wand. Qed.
Lemma tac_pose_proof Δ Δ' j P1 P2 R Q :
P1 P2 ToPosedProof P1 P2 R envs_app true (Esnoc Enil j R) Δ = Some Δ'
Δ' Q Δ Q.
Proof.
intros HP ? <-. rewrite envs_app_sound //; simpl.
by rewrite -HP left_id always_const wand_True.
intros HP ?? <-. rewrite envs_app_sound //; simpl.
by rewrite right_id -(to_pose_proof P1 P2 R) // always_const wand_True.
Qed.
Lemma tac_apply Δ Δ' i p R P1 P2 :
......@@ -867,6 +878,8 @@ Proof.
Qed.
End tactics.
Hint Extern 0 (ToPosedProof True _ _) =>
class_apply @to_posed_proof_True : typeclass_instances.
(** Make sure we can frame in the presence of evars without making Coq loop due
to it applying these rules too eager.
......
......@@ -282,11 +282,11 @@ Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
(** * Pose proof *)
Tactic Notation "iPoseProof" open_constr(lem) "as" constr(H) :=
eapply tac_pose_proof with _ H _; (* (j:=H) *)
eapply tac_pose_proof with _ H _ _ _; (* (j:=H) *)
[first
[eapply lem
|apply uPred.entails_impl; eapply lem
|apply uPred.equiv_iff; eapply lem]
|apply _
|env_cbv; reflexivity || fail "iPoseProof:" H "not fresh"|].
Tactic Notation "iPoseProof" open_constr(lem) constr(Hs) "as" constr(H) :=
......
......@@ -45,7 +45,7 @@ Section LiftingTests.
iIntros {Hn} "HΦ". iLöb {n1 Hn} as "IH".
wp_rec. wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
- iApply "IH" "% HΦ". omega.
- iPvsIntro. by assert (n1 = n2 - 1) as -> by omega.
- iApply pvs_intro. by assert (n1 = n2 - 1) as -> by omega.
Qed.
Lemma Pred_spec n E Φ : Φ #(n - 1) WP Pred #n @ E {{ Φ }}.
......
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