From 9690a7ee5600a9ca1c381650da63cfe766a112b1 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Wed, 4 Jul 2018 00:37:50 +0200 Subject: [PATCH] Move laterN_iter to derived_laws_sbi, because it's more generic. --- theories/base_logic/derived.v | 4 ---- theories/bi/derived_laws_sbi.v | 3 +++ 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v index 004892b1c..d3ff12d81 100644 --- a/theories/base_logic/derived.v +++ b/theories/base_logic/derived.v @@ -91,10 +91,6 @@ Global Instance uPred_ownM_sep_homomorphism : MonoidHomomorphism op uPred_sep (≡) (@uPred_ownM M). Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed. -(** Iterated later *) -Lemma laterN_iter n P : (▷^n P)%I = Nat.iter n sbi_later P. -Proof. induction n; f_equal/=; auto. Qed. - (** Consistency/soundness statement *) Lemma soundness φ n : (▷^n ⌜ φ ⌠: uPred M)%I → φ. Proof. rewrite laterN_iter. apply soundness_iter. Qed. diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v index 842fcdaa1..e1e93317e 100644 --- a/theories/bi/derived_laws_sbi.v +++ b/theories/bi/derived_laws_sbi.v @@ -247,6 +247,9 @@ Proof. induction n1; f_equiv/=; auto. Qed. Lemma laterN_le n1 n2 P : n1 ≤ n2 → ▷^n1 P ⊢ ▷^n2 P. Proof. induction 1; simpl; by rewrite -?later_intro. Qed. +Lemma laterN_iter n P : (▷^n P)%I = Nat.iter n sbi_later P. +Proof. induction n; f_equal/=; auto. Qed. + Lemma laterN_mono n P Q : (P ⊢ Q) → ▷^n P ⊢ ▷^n Q. Proof. induction n; simpl; auto. Qed. Global Instance laterN_mono' n : Proper ((⊢) ==> (⊢)) (@sbi_laterN PROP n). -- GitLab