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:

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

Or, even better: :wink:

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. :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!

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

[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 :+1: 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.

[JacquesCarette]

I could definitely warm up to this too.

[Taneb]

I'd want to check how it interacts with emacs' parenthesis-matching tools; I think ⟨ and ⟩ count as parentheses for that, and this suggestion would interact badly there.

[gallais]

Looking at Orestis' talk this morning, I realise we could do the following:

begin
  (m / n) * n          ≤⟨ ... ⟩
  (m / n) * n + m % n  ≡⟨ ... ⟫
  m % n + (m / n) * n  ≡⟪ ... ⟩
  m                    ∎

[jamesmckinna]

Given @Taneb's objections to my 'non-well-bracketed' proposals, this seems like a palatable alternative!

UPDATED: I suppose that @MatthewDaggitt 's support for my suggestion, and his comment about backwards compatibility, means that @Taneb wouldn't be committed, except by (eventual? immediate?) weight of convention, to adopt the new syntax (or will emacs simply plague your workflow with spurious non-matching parenthesis warnings?). I appreciate @gallais 's attempt to find a middle ground, but I wonder if there really isn't going to be one around which we can all agree/make common cause? In any case, I guess any eventual solution falls under 'beyond v2.0' ...?

UPDATED: For v2.0? Or for later?

[MatthewDaggitt]

The problem is that @gallais suggestion would also interact badly with a parens matching algorithm. To be honest I'm not very convinced that the parens matching problem is really a huge issue. It must be configurable for which unicode symbols it counts as parantheses. There are so many of them that could definition be used for other purposes apart from parens.

My vote would be to implement @jamesmckinna 's suggestion v2.0. The only change I'd suggest is that we have:

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

so that only the right most paren would indicate direction. This would have two minor advantages. Firstly, we'd only change the sym operator and not the main operator. Secondly, the main operator would still interact nicely with parens matching, so if people wanted to prioritise matching parens they could always just apply sym manually!

[WolframKahl]

If vertical alignment is the problem, then you can always get that for example by inserting a "visible space":

_≡␣⟨_⟩_
_≡˘⟨_⟩_

I prefer this since I like to think of the angle brackets as "hint brackets" delimiting the justification for the relationship via _≡_ respectively _≡˘_ between the expression on the previous line and the one on the next, assuming long vertical layout:

   E₁
 ≡␣⟨ H₁ ⟩
   E₂
 ≡˘⟨ H₂ ⟩
   E₃

Since not all uses of calculational presentation will involve symmetric relations, I think that just keeping the whole relation in front of the hint brackets is more consistent.

(Many informal users of calculational presentation, as well as CalcCheck, allow an arbitrary number of spaces between the relation and the hint opening bracket; this can also be used to achieve vertical alignment:

   E₁
 ≡   ⟨ H₁ ⟩
   E₂
 ≡˘  ⟨ H₂ ⟩
   E₃

)

[MatthewDaggitt]

Thanks for the interesting suggestion and context @WolframKahl!

If vertical alignment is the problem, then you can always get that for example by inserting a "visible space":

Unfortunately, vertical alignment is just one of the issues. The other two issues included at the top of this issue are "difficulty to type" and "convey the notion of symmetry/direction". We're also looking ideally for something that doesn't involve us renaming the existing standard operator.

Since not all uses of calculational presentation will involve symmetric relations, I think that just keeping the whole relation in front of the hint brackets is more consistent.

I agree, which is why I think we shouldn't change the forward direction combinator so that we don't have any effects on non-symmetric theories.

[MatthewDaggitt]

To be honest the more I think about it, the more I'm on board with _≡⟨_⟨_. It:

• conveys direction
• preserves vertical alignment
• doesn't require renaming the forward direction
• is easy to type

I think we're going to be hard pressed to beat that!

[jamesmckinna]

Regarding parenthesis matching (of which, in emacs, I am entirely ignorant), note that, thanks to whitespace discipline in agda, the L/R parenthesis pairs (under my 2.0 proposal) are, in lexical terms:

• for forward reasoning, ≡⟩ and ⟩
• for backwards, ≡⟨ and ⟨

and those pairs are unambiguous for the lexer, by contrast with forward reasoning in terms of ≡⟨ and ⟩...