Commit 9690a7ee authored by Robbert Krebbers's avatar Robbert Krebbers

Move laterN_iter to derived_laws_sbi, because it's more generic.

parent 7ee24879
......@@ -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.
......
......@@ -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).
......
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