[ add ] Relation.Binary.Properties.PartialSetoid
#2678
Conversation
|
@JacquesCarette any suggestions regarding the names? |
|
I'm actually fine with the names as they are. |
| p-refl : x ≈ y → x ≈ x × y ≈ y | ||
| p-refl p = p-reflˡ p , p-reflʳ p | ||
|
|
||
| p-reflexiveˡ : x ≈ y → x ≡ z → x ≈ z |
There was a problem hiding this comment.
This is Trans _≈_ _≡_ _≈_ (and similarly below), suggesting that reflexive may not be quite the right name? Similarly is this not just a variant of subst?
There was a problem hiding this comment.
Hmmm... I see what you mean... Will ponder this for a bit!
There was a problem hiding this comment.
So... my reasoning (with a bit of post hoc rationalisation...) was as follows:
reflexiveproofs are of the formx ≡ z → x ≈ z- these ones are 'partial', because preconditioned on having a proof of
x ≈ yto licence them - the left/right designators then pick out which of
xoryis being matched on
Possibly a bit convoluted, so I'm open to 'better' names!
There was a problem hiding this comment.
This is not Trans _≈_ _≡_ _≈_ because the second x would be a y in that case.
This is an extremely weird property which basically says: if x is related to something (anything) and we have evidence of that, and x and z are identical, then we can get evidence that x and z are related.
I'm at a loss for what to name it.
There was a problem hiding this comment.
I don't know about 'weird'... these properties are characteristic of being a PER rather than a full IsEquivalence!? Namely that the relation is reflexive only on its domain of definition, rather than on the whole type...
There was a problem hiding this comment.
As to names: I could call it (something like) conditional-reflexive, but then we would lose that the ≡.refl instantiation of such a lemma should be partial-refl... so those lemmas would also need to be renamed. And then... names are getting too long?
There was a problem hiding this comment.
Weird likely because I generically find PERs weird.
However, your comment hits the real issue on the head: only on its domain of definition. We really ought to define an 'is defined' construction (a la Trans and Symmetric, etc) and use it here. Then I would have understood that you were asking for some indirect evidence of being defined. Then we'll be in a decent position to think about names.
At least now I understand this combinator's meaning (when x is defined, then equality that involve it is reflexive), and that is no longer weird at all.
There was a problem hiding this comment.
Not sure I see clearly what the IsDefined construction would look like, and whether it would be 'free-standing', or tied to being in a PER?
Cf. Scott's "Identity and Existence in Intuitionistic Logic" (LNM 753) which explores variations on the theme of E t vs. t = t as expressions of 't is defined'/'t exists', but does seem tied to _=_ being an 'equality' (Leibniz-like) relation...?
| -- Proofs for partial equivalence relations | ||
|
|
||
| trans-reflˡ : LeftTrans _≡_ _≈_ | ||
| trans-reflˡ ≡.refl p = p |
There was a problem hiding this comment.
Do we actually need to match on the proof here? Is this not just a variant of subst?
There was a problem hiding this comment.
Oh... yes, probably! er, no, actually, as the arguments are in the wrong order, and introducing a flip/≡.sym seemed like an indirection too far!?
|
|
This adds the properties of PERs discussed in #2677 .
Issues:
p-prefix to signify 'partial'Properties(as here)Consequences(contra: dependency onPropositionalEquality)Relation.Binary.Structures.IsPartialEquivalence(contra: everyIsEquivalencegets bloated by the addition)Downstream:
Relation.Binary.Properties.Setoidto inherit from this?