Adds unary disjoint relation

[bsaul]

This PR adds the relation between two predicates expressing disjointness.

I am not at all wedded to the _#_ notation.

See the discussion on the Agda Zulip for more background.

[bsaul]

Before I fix the build errors (due to overloaded # symbol), I'll wait till we've settled on notation.

[jamesmckinna]

(in lieu of my (now deleted) comment, I took the liberty of adding the link myself to your OP... hope that's OK)

[bsaul]

(I took the liberty of adding the link myself to your OP... hope that's OK)

Of course, thanks!

[jamesmckinna]

cf. #2594 ... Can you also add some properties of these relations? Or other extensions, eg.:

• prove Symmetric _⊥_, Symmetric _≬_
• lift _⊥_ to Relation.Binary.Definitions (and even: Relation.Nullary?), and redefine Irreflexive using it?
• redefine relational composition using _≬_? (there may be dependency issues in trying to do this; partly because of the Nullary/Unary/Binary distinction, and partly because neither of Unary nor Nullary split off distinct Definitions modules...)
• ...

All of these strictly go outside the scope of what you have so far, but might also give life to the new definitions.

You also alluded to how they are part of your basic toolkit when developing in Agda, so what's a specimen client application/deployment context which might also be generally useful as an addition to the library?

[bsaul]

Can you also add some properties of these relations?

Yes, will do. Those are good suggestions.

[bsaul]

You also alluded to how they are part of your basic toolkit when developing in Agda, so what's a specimen client application/deployment context which might also be generally useful as an addition to the library?

I'm working on formalizing parts probability/statistics/causal inference wherein disjoint "events" or sets are sometimes a precondition in a theorem, e.g. Pearl's definition of d-separation.

[jamesmckinna]

You also alluded to how they are part of your basic toolkit when developing in Agda, so what's a specimen client application/deployment context which might also be generally useful as an addition to the library?

I'm working on formalizing parts probability/statistics/causal inference wherein disjoint "events" or sets are sometimes a precondition in a theorem, e.g. Pearl's definition of d-separation.

Nice! But not sure quite how in scope (yet) that might be for stdlib. Still the two concepts introduced are familiar to me from constructive approaches to (the foundations of) probability, cf. eg. Jan van Plato's book from some years ago now...

[bsaul]

Nice! But not sure quite how in scope (yet) that might be for stdlib.

I wouldn't expect most of what I'm noodling on to be in scope for stdlib -- I'm just trying to upstream things that might be.

[bsaul]

cf. eg. Jan van Plato's book from some years ago now...

Thanks for the reference -- looks quite interesting.

[bsaul]

• prove Symmetric _⊥_, Symmetric _≬_

Done in f77d38b

[bsaul]

• lift _⊥_ to Relation.Binary.Definitions? and redefine Irreflexive using it?

Trying to import Relation.Unary into Relation.Binary.Defintions introduces a cyclic dependency, so I suspect there would be a bit of refactoring to make this happen.

[WolframKahl]

On Tue, Feb 25, 2025 at 05:20:24PM -0800, Jacques Carette wrote:

that would be nice (fat perp)

Fat perp is apparently not on offer by Unicode, but see:

https://www.fileformat.info/info/unicode/char/search.htm?q=perp&han=Y

https://www.fileformat.info/info/unicode/char/search.htm?q=tack&han=Y

[jamesmckinna]

In favour of \perp:

• easy to type
• mildly distinct visually from \bot
• definitely distinct visually/lexically from _#_

In favour of _#_

• semantically it is an apartness
• ... what else?

Regarding @WolframKahl 's links to Unicode, I wonder if perhaps we should make every module preamble comment include the new (infix/mixfix) symbols introduced with their character encodings (emacs and Unicode?), as 'self-documentation', rather than trying to build a big lookup table in style-guide?

[JacquesCarette]

I wonder if perhaps we should make every module preamble comment include the new (infix/mixfix) symbols introduced with their character encodings (emacs and Unicode?), as 'self-documentation', rather than trying to build a big lookup table in style-guide?

That seems like a good idea.

[bsaul]

I wonder if perhaps we should make every module preamble comment include the new (infix/mixfix) symbols introduced with their character encodings (emacs and Unicode?), as 'self-documentation', rather than trying to build a big lookup table in style-guide?

That seems like a good idea.

Agreed.

[WolframKahl]

On Wed, Feb 26, 2025 at 03:58:22AM -0800, jamesmckinna wrote:

In favour of \perp:

• [...]
• mildly distinct visually from \bot

With my current fonts, I can see that when they are side-by-side, but I wouldn't be able to distinguish individual occurrences. I'd therefore argue against using both symbols in Agda.

[jamesmckinna]

On Wed, Feb 26, 2025 at 03:58:22AM -0800, jamesmckinna wrote: In favour of \perp: * [...] * mildly distinct visually from \bot With my current fonts, I can see that when they are side-by-side, but I wouldn't be able to distinguish individual occurrences. I'd therefore argue against using both symbols in Agda.

Hmm... that's a shame, I think. I'd maybe try to influence things further by adding

• \perp as a definition is lifting/proxying for the underlying appeal to \bot, so 'it makes sense' (?) to use cognate symbols
• plus any additional cognitive reinforcement arising from documenting the symbology sur place

But I'd better stop beating this particular donkey now.

[MatthewDaggitt]

I have no strong opinions on the choice of symbol. We use quite a lot of close cognates in the library already, but I can understand the urge not to add more.

[jamesmckinna]

@bsaul I've made a couple of suggestions, and additions, happy to commit those if you don't have time, along with fixing up the merge conflicts.

[bsaul]

@bsaul I've made a couple of suggestions, and additions, happy to commit those if you don't have time, along with fixing up the merge conflicts.

@jamesmckinna looks good to me. I can make the changes later today. But if you have time sooner, please feel free to make the commits and fix up.

[jamesmckinna]

Merge conflicts resolved; additions improve level polymorphism, but also (hopefully) avoid potential unsolved metas when applying the *-sym proofs, but given my involvement, a second review/fresh pair of eyes would be helpful before merging.

[gallais]

I've opened https://github.com/agda/agda/pull/7791/files to add the relevant unicode symbols

[JacquesCarette]

So maybe we should hold off on this, so that the new symbol(s) can be used?

[jamesmckinna]

Very happy/happier still with fat perp over perp... however we end up supporting it?

[jamesmckinna]

I've opened https://github.com/agda/agda/pull/7791/files to add the relevant unicode symbols

Oh I see, \bbot is 'short' like \bot, rather than 'tall' like \perp. Hmmm...

[jamesmckinna]

Once we can and do agree on the symbol, suggest updating the declaration of the symbol in the spirit of #2690 ...

[jamesmckinna]

Can we (@JacquesCarette @gallais) agree this for v2.3?