Commit bf5df6e8 authored by Ralf Jung's avatar Ralf Jung

fix iSpecialize on pure assertions

parent 56c7bb4c
Pipeline #9555 passed with stage
in 26 minutes and 32 seconds
......@@ -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_pure (φ : Prop) Q R:
φ (⌜φ⌝ - Q) Q.
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.
Lemma test_iSpecialize_Coq_entailment P Q R :
P (P - Q) Q.
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.
......
......@@ -806,8 +806,13 @@ 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).
(* These instances must be used only after [into_forall_wand_pure] in
[class_instances_sbi] failed. *)
Global Instance into_forall_wand P Q : IntoForall (P - Q) (λ _ : bi_emp_valid P, Q) | 10.
Proof. rewrite /IntoForall. apply forall_intro=><-. rewrite emp_wand //. Qed.
Global Instance into_forall_impl `{!BiAffine PROP} P Q :
IntoForall (P Q) (λ _ : bi_emp_valid P, Q) | 10.
Proof. rewrite /IntoForall. apply forall_intro=><-. rewrite -True_emp True_impl //. 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