From 0495154ccb210fcf3fbc024ad20d18a9327eb393 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Tue, 4 Apr 2017 16:55:08 +0200
Subject: [PATCH] Upred : explain why things are how they are.

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

diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 52ac2d274..eec44f42d 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -8,7 +8,26 @@ Set Default Proof Using "Type".
 
 Record uPred (M : ucmraT) : Type := IProp {
   uPred_holds :> nat → M → Prop;
+
+  (* [uPred_mono] is used to prove non-expansiveness (guaranteed by
+     [uPred_ne]). Therefore, it is important that we do not restrict
+     it to only valid elements. *)
   uPred_mono n x1 x2 : uPred_holds n x1 → x1 ≼{n} x2 → uPred_holds n x2;
+
+  (* We have to restrict this to hold only for valid elements,
+     otherwise this condition is no longer limit preserving, and uPred
+     does no longer form a COFE (i.e., [uPred_compl] breaks). This is
+     because the distance and equivalence on this cofe ignores the
+     truth valid on invalid elements. This, in turns, is required by
+     the fact that entailment has to ignore invalid elements, which is
+     itself essential for proving [ownM_valid].
+
+     We could, actually, make the following condition true even for
+     invalid elements: we have proved that uPred is isomorphic to a
+     sub-COFE of the COFE of predicates that are monotonous both with
+     respect to the step index and with respect to x. However, that
+     would essentially require changing (by making more complicated)
+     the model of many connectives of the logic, which we don't want. *)
   uPred_closed n1 n2 x : uPred_holds n1 x → n2 ≤ n1 → ✓{n2} x → uPred_holds n2 x
 }.
 Arguments uPred_holds {_} _ _ _ : simpl never.
-- 
GitLab