move comment up

theories/base_logic/upred.v

@@ -6,6 +6,40 @@ Set Default Proof Using "Type".
     base_logic.base_logic; that will also give you all the primitive
     and many derived laws for the logic. *)
 
+(* A good way of understanding this definition of the uPred OFE is to
+   consider the OFE uPred0 of monotonous SProp predicates. That is,
+   uPred0 is the OFE of non-expansive functions from M to SProp that
+   are monotonous with respect to CMRA inclusion. This notion of
+   monotonicity has to be stated in the SProp logic. Together with the
+   usual closedness property of SProp, this gives exactly uPred_mono.
+
+   Then, we quotient uPred0 *in the sProp logic* with respect to
+   equivalence on valid elements of M. That is, we quotient with
+   respect to the following *sProp* equivalence relation:
+     P1 ≡ P2 := ∀ x, ✓ x → (P1(x) ↔ P2(x))       (1)
+   When seen from the ambiant logic, obtaining this quotient requires
+   definig both a custom Equiv and Dist.
+
+
+   It is worth noting that this equivalence relation admits canonical
+   representatives. More precisely, one can show that every
+   equivalence class contains exactly one element P0 such that:
+     ∀ x, (✓ x → P(x)) → P(x)                   (2)
+   (Again, this assertion has to be understood in sProp). Starting
+   from an element P of a given class, one can build this canonical
+   representative by chosing:
+     P0(x) := ✓ x → P(x)                        (3)
+
+   Hence, as an alternative definition of uPred, we could use the set
+   of canonical representatives (i.e., the subtype of monotonous
+   sProp predicates that verify (2)). This alternative definition would
+   save us from using a quotient. However, the definitions of the various
+   connectives would get more complicated, because we have to make sure
+   they all verify (2), which sometimes requires some adjustments. We
+   would moreover need to prove one more property for every logical
+   connective.
+ *)
+
 Record uPred (M : ucmraT) : Type := IProp {
   uPred_holds :> nat → M → Prop;
 
@@ -23,40 +57,6 @@ Arguments uPred_holds {_} _%I _ _.
 Section cofe.
   Context {M : ucmraT}.
 
-  (* A good way of understanding this definition of the uPred OFE is to
-     consider the OFE uPred0 of monotonous SProp predicates. That is,
-     uPred0 is the OFE of non-expansive functions from M to SProp that
-     are monotonous with respect to CMRA inclusion. This notion of
-     monotonicity has to be stated in the SProp logic. Together with the
-     usual closedness property of SProp, this gives exactly uPred_mono.
-
-     Then, we quotient uPred0 *in the sProp logic* with respect to
-     equivalence on valid elements of M. That is, we quotient with
-     respect to the following *sProp* equivalence relation:
-        P1 ≡ P2 := ∀ x, ✓ x → (P1(x) ↔ P2(x))       (1)
-     When seen from the ambiant logic, obtaining this quotient requires
-     definig both a custom Equiv and Dist.
-
-
-     It is worth noting that this equivalence relation admits canonical
-     representatives. More precisely, one can show that every
-     equivalence class contains exactly one element P0 such that:
-        ∀ x, (✓ x → P(x)) → P(x)                   (2)
-     (Again, this assertion has to be understood in sProp). Starting
-     from an element P of a given class, one can build this canonical
-     representative by chosing:
-        P0(x) := ✓ x → P(x)                        (3)
-
-     Hence, as an alternative definition of uPred, we could use the set
-     of canonical representatives (i.e., the subtype of monotonous
-     sProp predicates that verify (2)). This alternative definition would
-     save us from using a quotient. However, the definitions of the various
-     connectives would get more complicated, because we have to make sure
-     they all verify (2), which sometimes requires some adjustments. We
-     would moreover need to prove one more property for every logical
-     connective.
-   *)
-
   Inductive uPred_equiv' (P Q : uPred M) : Prop :=
     { uPred_in_equiv : ∀ n x, ✓{n} x → P n x ↔ Q n x }.
   Instance uPred_equiv : Equiv (uPred M) := uPred_equiv'.