Commit d870e5cf authored by Ralf Jung's avatar Ralf Jung

monpred: note that notation is somewhat broken

parent 4b43fcc2
...@@ -816,6 +816,7 @@ Implicit Types P Q : monPred. ...@@ -816,6 +816,7 @@ Implicit Types P Q : monPred.
Global Instance monPred_bupd_facts `{BUpdFacts PROP} : BUpdFacts monPredSI. Global Instance monPred_bupd_facts `{BUpdFacts PROP} : BUpdFacts monPredSI.
Proof. Proof.
split; unseal; unfold monPred_bupd_def, monPred_upclosed. split; unseal; unfold monPred_bupd_def, monPred_upclosed.
(* Note: Notation is somewhat broken here. *)
- intros n P Q HPQ. split=>/= i. by repeat f_equiv. - intros n P Q HPQ. split=>/= i. by repeat f_equiv.
- intros P. split=>/= i. apply bi.forall_intro=>?. rewrite bi.pure_impl_forall. - intros P. split=>/= i. apply bi.forall_intro=>?. rewrite bi.pure_impl_forall.
apply bi.forall_intro=><-. apply bupd_intro. apply bi.forall_intro=><-. apply bupd_intro.
...@@ -868,6 +869,7 @@ Proof. split; try apply _; by unseal. Qed. ...@@ -868,6 +869,7 @@ Proof. split; try apply _; by unseal. Qed.
Global Instance monPred_fupd_facts `{FUpdFacts PROP} : FUpdFacts monPredSI. Global Instance monPred_fupd_facts `{FUpdFacts PROP} : FUpdFacts monPredSI.
Proof. Proof.
split; first apply _; unseal; unfold monPred_fupd_def, monPred_upclosed. split; first apply _; unseal; unfold monPred_fupd_def, monPred_upclosed.
(* Note: Notation is somewhat broken here. *)
- intros E1 E2 n P Q HPQ. split=>/= i. by repeat f_equiv. - intros E1 E2 n P Q HPQ. split=>/= i. by repeat f_equiv.
- intros E1 E2 P HE12. split=>/= i. - intros E1 E2 P HE12. split=>/= i.
do 2 setoid_rewrite bi.pure_impl_forall. do 2 apply bi.forall_intro=>?. do 2 setoid_rewrite bi.pure_impl_forall. do 2 apply bi.forall_intro=>?.
......
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