Commit d840f8cb authored by Ralf Jung's avatar Ralf Jung

add derived soundness_bupd matching soundness_later

parent c8379abc
...@@ -213,6 +213,8 @@ Lemma soundness_later P : bi_emp_valid (▷ P) → bi_emp_valid P. ...@@ -213,6 +213,8 @@ Lemma soundness_later P : bi_emp_valid (▷ P) → bi_emp_valid P.
Proof. apply soundness_later. Qed. Proof. apply soundness_later. Qed.
End restate. End restate.
(** See [derived.v] for the version for basic updates. *)
(** New unseal tactic that also unfolds the BI layer. (** New unseal tactic that also unfolds the BI layer.
This is used by [base_logic.double_negation]. This is used by [base_logic.double_negation].
TODO: Can we get rid of this? *) TODO: Can we get rid of this? *)
......
...@@ -92,6 +92,12 @@ Global Instance uPred_ownM_sep_homomorphism : ...@@ -92,6 +92,12 @@ Global Instance uPred_ownM_sep_homomorphism :
Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed. Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
(** Consistency/soundness statement *) (** Consistency/soundness statement *)
Lemma soundness_bupd_plain P `{!Plain P} : bi_emp_valid (|==> P) bi_emp_valid P.
Proof.
eapply bi_emp_valid_mono. etrans; last exact: bupd_plainly. apply bupd_mono'.
apply: plain.
Qed.
Corollary soundness φ n : (^n φ : uPred M)%I φ. Corollary soundness φ n : (^n φ : uPred M)%I φ.
Proof. Proof.
induction n as [|n IH]=> /=. induction n as [|n IH]=> /=.
......
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