From a27982f7e0862abe491e2cd5522144adf2736ac6 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Fri, 8 Dec 2017 17:32:01 +0100 Subject: [PATCH] move comment up --- theories/base_logic/upred.v | 68 ++++++++++++++++++------------------- 1 file changed, 34 insertions(+), 34 deletions(-) diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v index d51b589e..6a7aa906 100644 --- a/theories/base_logic/upred.v +++ b/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'. -- GitLab