diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v index eec44f42d1184a029f0f7ac427ddabe77e43f49f..5beea6517bd6cecaecad9dd9344df48b22a295c8 100644 --- a/theories/base_logic/upred.v +++ b/theories/base_logic/upred.v @@ -18,16 +18,17 @@ Record uPred (M : ucmraT) : Type := IProp { 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 + truth value on invalid elements. This, in turn, 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. *) + We could, actually, remove this restriction and make this + condition apply even to 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 it 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.