Commit 357f1cc2 authored by Ralf Jung's avatar Ralf Jung

allow specializing a wand with a Coq-level proof of the premise

parent b41623db
......@@ -111,6 +111,10 @@ Lemma test_iSpecialize_auto_frame P Q R :
(P - True - True - Q - R) - P - Q - R.
Proof. iIntros "H ? HQ". by iApply ("H" with "[$]"). Qed.
Lemma test_iSpecialize_Coq_entailment P Q R :
P (P - Q) Q.
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.
Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} :
P - Q R - emp.
Proof. iIntros "HP #HQ HR". iEmpIntro. Qed.
......@@ -806,6 +806,8 @@ Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.
Global Instance into_forall_embed `{BiEmbed PROP PROP'} {A} P (Φ : A PROP) :
IntoForall P Φ IntoForall P (λ a, ⎡Φ a%I).
Proof. by rewrite /IntoForall -embed_forall => <-. Qed.
Global Instance into_forall_wand P Q : IntoForall (P - Q) (λ _ : bi_emp_valid P, Q).
Proof. rewrite /IntoForall. apply forall_intro=><-. rewrite emp_wand //. Qed.
(* FromForall *)
Global Instance from_forall_forall {A} (Φ : A PROP) :
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