From 6c1297e7eacbae8acee37f08d3c22faddaaa3e67 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 21 Apr 2020 20:14:39 +0200 Subject: [PATCH] =?UTF-8?q?Add=20instances=20for=20L=C3=B6b=20and=20contra?= =?UTF-8?q?ctiveness=20of=20later=20for=20monPred.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- theories/bi/monpred.v | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v index a969068bc..30252b28e 100644 --- a/theories/bi/monpred.v +++ b/theories/bi/monpred.v @@ -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. -- GitLab