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. 🤷‍♂️

[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. 😉

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:

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

Or, even better: 😉

begin
  (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. 😞

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!

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

[jamesmckinna]

A (perhaps mischievous) thought:

• left-to-right rewriting by an equation _≡⟩_⟩_
• right-to-left rewriting _≡⟨_⟩_

The tragedy is that it clashes with our existing conventions (sigh ;-)), but it has always seemed to me a cognitive overload to insist that \langle,\rangle function merely as parentheses, on top of which we then (discuss how best to) attempt to overlay an additional directional indicator: they're directional already!

The tragedy is compounded by the choices for _≤⟨_⟩_ etc., ... so my suggestion would be to (go against the tide ;-)) and invert the order direction of the above suggestions, and simply write _≡⟩_⟩_ for uses of sym... the point being to have it stick out, yet not violate the otherwise ambient typograhical/layout conventions.

[jamesmckinna]

On second thoughts, it seems that I prefer to reverse the 'bracket orientation':

• _≡⟩_⟩_ for LHS to RHS appeal to an equation
• _≡⟨_⟨_ for the sym direction...

I'll fix this up when I'm not writing on my phone...
DONE. I was nearly there above, but now I think I'm happy. But we still won't make that change, alas... :-(

[MatthewDaggitt]

On second thoughts, it seems that I prefer to reverse the 'bracket orientation':

_≡⟩_⟩_ for LHS to RHS appeal to an equation
_≡⟨_⟨_ for the sym direction...

I really like this suggestion 👍 The only one I've seen I'd be happy implementing! And it would be backwards compatible as we could leave the old names in place.