Mathport `$` -> `<|`

Stream: mathlib4

[Maxwell Thum]

Mathport seems to be replacing quotient.induction_on s $ (for instance) with (Quotient.induction_on s), when it should be Quotient.inductionOn s <|.

[Siddhartha Gadgil]

Indeed in one file I had to change a bunch of parenthesis for quotients manually.

[Reid Barton]

In general if there are weird errors around induction principle applications and there are weird parentheses, try deleting the parentheses

[Mario Carneiro]

By the way, the reason this causes an error in lean 4 even though you would think that (f x) y and f x y are the same, is because lean (both 3 and 4) treats applications in "groups", so that for example if you had foo : \forall {a b} (c d), .. then both x and y are affected in the application @foo x y in the sense that x goes in for a and y for b, while if you put parentheses in the middle as in (@foo x) y then x goes in for a and it is treated as having no more arguments (so _ goes in for b), and then y goes in for c. This behavior is useful, since it means you can control when things are made explicit or not using variations like foo a b, (foo a) b, (@foo a) b, @(foo a) b and @(foo a b), all of which do slightly different things.

In this case, we are using the @[elab_as_elim] method, which requires that the eliminator be fully applied, so if you put parentheses in the middle then it will appear unapplied and cause an error.

[Ruben Van de Velde]

It feels kinda weird that mathport outputs those extra parentheses

[Mario Carneiro]

It's a bug (and a relatively recent one too I think). MWE:

import Lean
open Lean
#eval show MetaM _ from do
  let stx ← `(a b)
  let stx ← `($stx fun _ => c)
  let stx ← PrettyPrinter.parenthesizeTerm stx
  PrettyPrinter.formatTerm stx
-- (a.1 b.1) fun _ => c.1

[Mario Carneiro]

I think the issue is that in Syntax, the node for "application" is n-ary, i.e. $f $args*, which means that there is a difference between app (app f [x]) [y] and app f [x, y]. In fact, the parenthesizer might be inserting parentheses on purpose to distinguish between these, since as I mentioned they can cause lean to behave differently

[Mario Carneiro]

Interestingly, using $ directly does not result in an extra application (which makes sense, otherwise lots of user code would be broken):

import Lean
open Lean Elab
#eval show TermElabM _ from do
  let stx ← `(a b)
  let stx ← `($stx $ fun _ => c)
  let stx ← Elab.liftMacroM <| expandMacros stx
  let stx ← PrettyPrinter.parenthesizeTerm stx
  PrettyPrinter.formatTerm stx
-- a.1 b.1 fun _ => c.1

[Mario Carneiro]

It seems the reason is that there is an extra case to handle this in the macro expansion for $:

syntax:min term atomic(" $" ws) term:min : term

macro_rules
  | `($f $args* $ $a) => `($f $args* $a)
  | `($f $ $a) => `($f $a)

[Mario Carneiro]

so I guess it is mathport's fault after all, for not including this case

[Mario Carneiro]

fixed in 2bfc0cb