Skip to content
Snippets Groups Projects
Commit 25131c02 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Better instance for `IntoWand` of `∀ _ : φ, P`. Fixes #799.

parent c4aeb8dd
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris/proofmode/class_instances.v
+ 6
− 4
View file @ 25131c02
...@@ -497,11 +497,13 @@ Proof. ...@@ -497,11 +497,13 @@ Proof.
-impl_wand_intuitionistically -pure_impl_forall -impl_wand_intuitionistically -pure_impl_forall
bi.persistently_elim //. bi.persistently_elim //.
Qed. Qed.
Global Instance into_wand_forall_prop_false p (φ : Prop) P : Global Instance into_wand_forall_prop_false p (φ : Prop) Pφ P :
Absorbing P → IntoWand p false (∀ _ : φ, P) ⌜ φ ⌝ P. MakeAffinely ⌜ φ ⌝ Pφ →
IntoWand p false (∀ _ : φ, P) Pφ P.
Proof. Proof.
intros ?. rewrite /MakeAffinely /IntoWand=> <-.
rewrite /IntoWand (intuitionistically_if_elim p) /= pure_wand_forall //. rewrite (intuitionistically_if_elim p) /=.
by rewrite -pure_impl_forall -persistent_impl_wand_affinely.
Qed. Qed.
Global Instance into_wand_forall {A} p q (Φ : A → PROP) P Q x : Global Instance into_wand_forall {A} p q (Φ : A → PROP) P Q x :
......
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