Commit b50a4f9f authored by Robbert Krebbers's avatar Robbert Krebbers

Soundness lemma for internal equality of `uPred`.

parent b958d569
......@@ -209,6 +209,9 @@ Proof. exact: uPred_primitive.discrete_fun_validI. Qed.
Lemma pure_soundness φ : bi_emp_valid (PROP:=uPredI M) φ φ.
Proof. apply pure_soundness. Qed.
Lemma internal_eq_soundness {A : ofeT} (x y : A) : (True x y) x y.
Proof. apply internal_eq_soundness. Qed.
Lemma later_soundness P : bi_emp_valid ( P) bi_emp_valid P.
Proof. apply later_soundness. Qed.
(** See [derived.v] for a similar soundness result for basic updates. *)
......
......@@ -803,6 +803,12 @@ Proof. by unseal. Qed.
Lemma pure_soundness φ : (True φ ) φ.
Proof. unseal=> -[H]. by apply (H 0 ε); eauto using ucmra_unit_validN. Qed.
Lemma internal_eq_soundness {A : ofeT} (x y : A) : (True x y) x y.
Proof.
unseal=> -[H]. apply equiv_dist=> n.
by apply (H n ε); eauto using ucmra_unit_validN.
Qed.
Lemma later_soundness P : (True P) (True P).
Proof.
unseal=> -[HP]; split=> n x Hx _.
......
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