From 1df177bdec7f94e4616ae0d9f8fe6ca20f7ee0b6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 8 Dec 2017 17:57:56 +0100
Subject: [PATCH] uPred: show that the definition in the appendix is equivalent
 to the one in Coq

---
 theories/base_logic/upred.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 6a7aa906b..8a9f675fc 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -107,6 +107,23 @@ Proof.
   intros [Hne] ???. eapply Hne; try done. eauto using uPred_mono, cmra_validN_le.
 Qed.
 
+(* Equivalence to the definition of uPred in the appendix. *)
+Lemma uPred_alt {M : ucmraT} (P: nat → M → Prop) :
+  (∀ n1 n2 x1 x2, P n1 x1 → x1 ≼{n1} x2 → n2 ≤ n1 → P n2 x2) ↔
+  ( (∀ x n1 n2, n2 ≤ n1 → P n1 x → P n2 x) (* Pointwise down-closed *)
+  ∧ (∀ n x1 x2, x1 ≡{n}≡ x2 → ∀ m, m ≤ n → P m x1 ↔ P m x2) (* Non-expansive *)
+  ∧ (∀ n x1 x2, x1 ≼{n} x2 → ∀ m, m ≤ n → P m x1 → P m x2) (* Monotonicity *)
+  ).
+Proof.
+  (* Provide this lemma to eauto. *)
+  assert (∀ n1 n2 (x1 x2 : M), n2 ≤ n1 → x1 ≡{n1}≡ x2 → x1 ≼{n2} x2).
+  { intros ????? H. eapply cmra_includedN_le; last done. by rewrite H. }
+  (* Now go ahead. *)
+  split.
+  - intros Hupred. repeat split; eauto using cmra_includedN_le.
+  - intros (Hdown & _ & Hmono) **. eapply Hmono; [done..|]. eapply Hdown; done.
+Qed.
+
 (** functor *)
 Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
   `{!CmraMorphism f} (P : uPred M1) :
-- 
GitLab