mathport: cases_on => casesOn

Stream: mathlib4

[Michal Wallace (tangentstorm)]

So, as far as I can tell, when you define a new inductive type T with n constructors, lean3 creates a function called T.cases_on with n arguments, and lean4 creates a function called T.casesOn with n+1 arguments: the addition is an extra initial argument that looks like {motive : T → Sort u} ...

Suppose I want to tell mathport about this change. I suspect this is going to wind up as a new trTactic somewhere under Mathport/Syntax/Translate/Tactic, but I don't yet have a clear idea where to start..

I believe the rule to add is: every time I see a function called T.cases_on where T is inductive, I need to add an extra argument that looks like: ( motive =: fun _ => T ).

I do not yet have enough knowledge to guess where that rule should go or what it should look like. Can someone point me in the right direction?

[Reid Barton]

Lean 3's cases_on also has a motive argument, it's called C. for example

bool.cases_on : Π {C : bool → Sort u_1} (n : bool), C ff → C tt → C n

[Reid Barton]

versus

@Bool.casesOn : {motive : Bool → Sort u_1} → (t : Bool) → motive false → motive true → motive t

[Michal Wallace (tangentstorm)]

Well that's interesting. I'm looking at lean3 code in mathlib that doesn't use that parameter, but lean4 seems to require it. Ex: https://github.com/leanprover-community/mathlib/blob/master/src/data/num/basic.lean#L350

protected def bit1 : znum → znum
  | 0       := 1
  | (pos n) := pos (pos_num.bit1 n)
  | (neg n) := neg (num.cases_on (pred' n) 1 pos_num.bit1)

[Michal Wallace (tangentstorm)]

Is there some way to provide a default motive, maybe, and that's what's missing from lean4?

[Reid Barton]

I think I heard that Lean 4 doesn't have the elab_as_eliminator elaboration strategy so you will usually need to provide the motive explicitly, yeah.

[Leonardo de Moura]

You can write num.cases_on (pred' n) 1 pos_num.bit1 in Lean 4 as

match pred' n with
| num.zero => 1
| num.pos n => pos_num.bit1 n

You can also use match pred' n with | .zero => 1 | .pos n => n.bit1

[Michal Wallace (tangentstorm)]

NIce. So we can either generate the motive or use match... But the question is how and where to add one of those rules to mathport. :D

[Leonardo de Moura]

You can try to use the Lean pretty-printer option set_option pp.analyze true. It generates the motives for us. This option was originally developed for Mathport.

[Michal Wallace (tangentstorm)]

@Mario Carneiro can you help me understand how to make a change like this in synport?

[Michal Wallace (tangentstorm)]

@Leonardo de Moura where are you suggesting to put this? i tried in the individual source file, but that didn't have an effect.
Is the pretty printer involved in generating the json ASTs, and there's some place I could inject this at a global level?

[Michal Wallace (tangentstorm)]

I think my problem is that I don't yet have a high level picture of how mathport works. There doesn't seem to be any technical / architectural documentation, so right now I'm just reading code and trying to understand how anything fits together.

[Leonardo de Moura]

@Mario Carneiro @Gabriel Ebner Are you using set_option pp.analyze true in Mathport? I recall that @Daniel Selsam implemented this option for Mathport, and it was enabled by default in Lean 4 for a while.

[Michal Wallace (tangentstorm)]

Wait, you're saying enable that in the lean4 pretty printer? I understand the lean 4 pretty printer is used to format the lean4 syntax once you have it, but a pretty printer shouldn't be generating new information that stock lean 4 can't infer by itself.

It makes sense to have something in lean3 output formerly implicit information that now needs to be explicit... But if lean4 can fill in the information itself, it should just do so, and we wouldn't have to change the generated code at all.

[Michal Wallace (tangentstorm)]

I think mathport does not yet allow modifying function applications at all. As far as I can tell, if it did do that, it would be in this function, in Mathport\Syntax\Translate\Basic.lean:

partial def trAppArgs [Inhabited α] : (e : Spanned Expr) → (m : Spanned Expr → M α) → M (α × Array Syntax)
  | { kind := Expr.app f x, .. }, m => do let (f, args) ← trAppArgs f m; pure (f, args.push (← trExpr x))
  | e, m => return (← m e, #[])

[Leonardo de Moura]

The Lean pretty-printer module also includes a delaborator which converts Expr (kernel terms) back into Syntax.

[Michal Wallace (tangentstorm)]

My guess is this is the first time anyone's looked at translating individual function calls, because the current code is focused on translating functions that mathlib authors have written, whereas this is getting at fundamental changes between the auto-generated code in lean3 vs lean4.

[Leonardo de Moura]

BTW, the Expr in the example above is not the Lean 4 Expr, but an Expr defined in Mathport. The set_option pp.analyze true will not help here because the function is not using Lean 4 Expr.

[Michal Wallace (tangentstorm)]

@Leonardo de Moura ohhh... so you mean have lean3 pretty-print the mathlib code "in place" before we do the lean3 -> ast.json step?

[Michal Wallace (tangentstorm)]

hrm. so pp.analyze appears to be a valid option in lean4, but not in lean 3.44.1, which is what is generating the .ast.json files:

 lean --make --ast src/data/num/basic.lean
D:\ver\Lean4-DataNumBasic\mathport\sources\mathlib\src\data\num\basic.lean:6:11:
error: unknown option 'pp.analyze', type 'help options.' for list of available options

D:\ver\Lean4-DataNumBasic\mathport\sources\mathlib\src\data\num\basic.lean: parsing at line 62

[Michal Wallace (tangentstorm)]

but there is this: pp.implicit (Bool) (pretty printer) display implicit parameters (default: false)

[Michal Wallace (tangentstorm)]

i added set_option pp.implicit true but it didn't make any difference to the generated code (other than adding that line, as far as i can tell...) i don't think lean --ast is affected by the options set in the file itself... but i do think getting lean3 to include the extra information in the --ast dump would be a good fix.

[Gabriel Ebner]

Are you using set_option pp.analyze true in Mathport?

@Leonardo de Moura No, not at all. We don't use the delaborator for anything (as far as I can tell) since we start from the Lean 3 AST.

[Gabriel Ebner]

Michal Wallace (tangentstorm) said:

I believe the rule to add is: every time I see a function called T.cases_on where T is inductive, I need to add an extra argument that looks like: ( motive =: fun _ => T ).

A slightly easier fix is to add (motive := _ => _) to the output. This doesn't require the pretty-printer at all. We could add this fairly easy in the trExpr' function (if the function is an identifier ending in casesOn, add a (motive := _ => _) argument).

[Gabriel Ebner]

I think my problem is that I don't yet have a high level picture of how mathport works. There doesn't seem to be any technical / architectural documentation, so right now I'm just reading code and trying to understand how anything fits together.

Please ask if you're missing something. Documentation hasn't been a big priority.

I think you've already got a lot of the big picture. For synport, we use AST files generated by Lean 3. These AST files contain a serialized representation of a Lean 3 abstract syntax tree, plus some extra information. Essentially we take the Lean 3 abstract syntax tree, convert it to a Lean 3 Syntax object and print that. There are some tweaks we apply during this conversions, and some tweaks we apply to the final Syntax (mathport_rules).

One of the extra informations recorded in the AST file is name resolution: for example that pos resolves to num.pos. We use this information to determine how a name should be translated (i.e., whether it should become pos or Pos).

[Gabriel Ebner]

IIRC the AST files also contain the elaborated expression for every AST node. But I don't think we use this for anything yet.

[Michal Wallace (tangentstorm)]

@Gabriel Ebner thanks! ... i will give this a shot next time i have time to work on this (may not be until next week).

Where is that pos / Pos decision happening? (Because num.pos becomes Pos sometimes and not others, and num.neg becomes neg)

[Michal Wallace (tangentstorm)]

I have a whole list of little changes like this that I think I can make once I get my head around how to actually write the transformations.

[Gabriel Ebner]

Feel free to add these as bugs to the mathport repo. (some are already bugs, please check first)

[Gabriel Ebner]

Where is that pos / Pos decision happening?

That happens during an earlier phase: the binport. In binport we translate the serialized Lean 3 environment (stored in tlean files). During this translation we decide how definitions should be renamed. The synport then checks: how is the name resolved in Lean 3 -> how was it translated in binport.