[ add ] syntax for antisym equality reasoning in Relation.Binary.Reasoning.PartialOrder #3047

[jamesmckinna]

Tackles the PartialOrder/antisym question in #3047 , with specimen usage illustrated in Algebra.Properties.KleeneAlgebra (which prompted the question in the first place).

The nice thing is that it was a (very) easy add-on, once I'd figured out what the parser was doing/failing to do. But maybe too easy, see the second point below.

TODO: currently

• the new syntax is the one that @JacquesCarette hates, so I'm open to some sort of debate around this, and offer a suggestion below
• the deployment isn't (yet) quite right, because its use in anger probably will entail nested reasoning, which for readability reasons, we tend to avoid, see the use of lemma in KleeneAlgebra for examples.

[jamesmckinna]

So... I suppose something like

Suggested change

	syntax antisym-syntax x≤y y≤x = x≤y ⟨⟩ y≤x
	syntax antisym-syntax x≤y y≤x = x≤y ≤≥ y≤x

might achieve greater consensus?

[JacquesCarette]

I now doubly don't like it. Seeing it in use, it seems to disappear and become just another argument to everything that is already there. I'm worried that ≤≥ may also not act very well as a visually distinctive divider.

Looking through the available symbols: ⋛ ? ⨇ ? ⋈ ? ▦ ? ✹ ?

[jamesmckinna]

I now doubly don't like it. Seeing it in use, it seems to disappear and become just another argument to everything that is already there. I'm worried that ≤≥ may also not act very well as a visually distinctive divider.

Looking through the available symbols: ⋛ ? ⨇ ? ⋈ ? ▦ ? ✹ ?

Well, this is strictly 'new' functionality that occurred to me in the course of the #3031 refactoring, so should be consider super low-priority until we've cleared everything else off the v3.0 docket.

But I am grateful for the prompt to think again about symbols, and the observation that if punctuation is too silent/invisible/... then it's perhaps not earning its place properly.

[gallais]

I am going to be annoying but I don't like this syntax (anything pushing
auxiliary equational proofs to where clauses is pointing to limitations in
our eDSL).

I could not find a good syntax for it, but I was wondering whether something
roller-coastery would work: we have some equality proof steps then we start
going up-up-up the hill all the way to the peak, then come crashing down back
to where we started and that lets us take new equality steps.

Something like this:

k ≈⟨ proof of k ≈ l ⟩
l ≈⟨ proof of l ≈ m ⟩
m up⟨ proof of m ≤ n ⟩ -- we're starting to go up
n ≤⟨ proof of n ≤ p ⟩
p ≤⟨ proof of p ≤ q ⟩
q down⟨ proof of r ≤ q ⟩ -- q is our peak altitude
r ≥⟨ proof of s ≤ r ⟩
s ≥⟨ proof of s ≤ m ⟩
m done⟨⟩ -- we've made it back, we know start ≈ peak i.e. m ≈ q!
q ∎

-- Overall, we get `k ≈ q`

[jamesmckinna]

I'm delighted that this has sparked so much debate/thinking about the issue, esp. wrt the ergonomics. As I've said above, there's no rush, and I hope that if/when we merge this in some form or other, we'll have achieved a good consensus.

So for now: thanks for all the additional commentary/input!