Commit 6c1297e7 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add instances for Löb and contractiveness of later for monPred.

parent cfac1295
......@@ -424,6 +424,13 @@ Proof. unseal. split. solve_proper. Qed.
Global Instance monPred_in_flip_mono : Proper (() ==> flip ()) (@monPred_in I PROP).
Proof. solve_proper. Qed.
Global Instance monPred_later_contractive :
Contractive (bi_later (PROP:=PROP)) Contractive (bi_later (PROP:=monPredI)).
Proof. unseal=> ? n P Q HPQ. split=> i /=. f_contractive. apply HPQ. Qed.
Global Instance monPred_bi_löb : BiLöb PROP BiLöb monPredI.
Proof.
split=> i. unseal. by rewrite (bi.forall_elim i) bi.pure_True // left_id löb.
Qed.
Global Instance monPred_bi_positive : BiPositive PROP BiPositive monPredI.
Proof. split => ?. unseal. apply bi_positive. Qed.
Global Instance monPred_bi_affine : BiAffine PROP BiAffine monPredI.
......
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