Agda-stdlib: Fix the syntax for symmetric equality reasoning combinator

[ajrouvoet]

Quoting @MatthewDaggitt

I too would like to do something about the ˘ syntax, even though I introduced it
I really hate it: it's difficult to type, it ruins the alignment of proofs and doesn't clearly convey symmetry to me.

Here are a few proposals to get the discussion going:

1. _↑≡⟨_⟩_ and _↓≡⟨_⟩_, stolen from the categories library (at least they used to be there when I used it way back). The arrow indicates the direction in which we are applying the equality.
2. _↑⟨_⟩_ and _↓⟨_⟩_ as shorter alternatives.

[JacquesCarette]

I like the shorter alternatives. If we have to put in the relation wrt which we're working, I'm wondering about putting it in the other order, i.e. _≡↑⟨_⟩_.

I think having these as aliases (or the current ones as aliases) could be an interesting experiment. Let a couple of versions go by, and see what people tend to use the most, then deprecate the other.

[dylanede]

+1 for putting the direction indicator after the relation symbol.

Regarding the direction indicator, would horizontal arrows (of some style) make more sense or be more likely to be confused with the many other uses of horizontal arrows?

[ajrouvoet]

Equality reasoning proves are usually code-set vertically. :man_shrugging:

[MatthewDaggitt]

I like the idea of vertical arrows. My only comment is that I also like having the angle brackets aligned on the page, which is one of things that I find very distressing about the current sym notation. This proposal would partially fix it as the sym and non-sym-ed versions would now align, but it still wouldn't align with other operators, e.g. inequalities:

begin
  (m / n) * n          ≤⟨ ... ⟩
  (m / n) * n + m % n  ≡↑⟨ ... ⟩
  m % n + (m / n) * n  ≡↓⟨ ... ⟩
  m                    ∎

Would people hate it if we moved the arrows inside the brackets? i.e. _≡⟨↓_⟩_ and _≡⟨↑_⟩_

begin
  (m / n) * n          ≤⟨ ... ⟩
  (m / n) * n + m % n  ≡⟨↑ ... ⟩
  m % n + (m / n) * n  ≡⟨↓ ... ⟩
  m                    ∎

[WolframKahl]

Yes. :wink:

If you want them inside, you can also define ↓_ = ≡-sym with appropriate low precedence.

Having the arrows after the closing hint bracket looks more acceptable to me:

  (m / n) * n          ≤⟨ ... ⟩
  (m / n) * n + m % n  ≡⟨ ... ⟩↑
  m % n + (m / n) * n  ≡⟨ ... ⟩↓
  m                    ∎

Or, even better: :wink:

  (m / n) * n          ≤⟨ ... ⟩
  (m / n) * n + m % n  ≡⟨ ... ⟩
  m % n + (m / n) * n  ≡⟨ ... ⟩˘
  m                    ∎

[JacquesCarette]

I also would dislike the arrows inside the brackets. Having them after is better than inside [though not necessarily the best choice].

[gallais]

A trailing character at the far right of the line is easy to miss. We dismissed
this possibility last time around for this reason.

What about a modified ≡? I see ⩧ ("identical with dot above") exists.

Or if we want to merge the idea of an arrow and an equality sign, we have the
pair ≙ and ≚ that could play this role and still be only 1 character. I am not
too happy about the fact that they are not derived from ≡ though. :disappointed:

Note that ⩪ exists! I could not find ≈ with a dot but for some reason
there's ⩯ and even weirder stuff such as ⥵ ⭊. WTF unicode?!
We do have ⩭ but that's not the blessed setoid symbol. :/

[ajrouvoet]

I am not too happy about the fact that they are not derived from ≡ though

Yeah I think using different symbols to denote the same equality is more confusing than necessary.

It looks like we're mixing pragmatics and aesthetics. The pragmatics seem to be:

• The syntax needs to support alignment of the brackets.
• It needs to be easy to spot, so not to confuse people.

Additionally it would be nice if it is notation that is portable to other reasoning combinators?

[ajrouvoet]

Oh, that is embarrassing, there is standard notation for this!

_≡⟨╯°□°╯︵┻━┻_⟩_