mathport improvements for `data.num.add`

Stream: mathlib4

[michal wallace (tangentstorm)]

I'm working on improving the mathport translation of data.num.add

What should I do about this output?

protected def add : PosNum → PosNum → PosNum
  | 1, b => succ b
  | a, 1 => succ a
  | bit0 a, bit0 b => bit0 (add a b)
  | bit1 a, bit1 b => bit0 (succ (add a b))
  | bit0 a, bit1 b => bit1 (add a b)
  | bit1 a, bit0 b => bit1 (add a b)

instance : Add PosNum :=
  ⟨PosNum.add⟩

It gives unknown identifier 'add' errors in each of the recursive calls.

Other than capitalization, the definition was the same in lean3 and working fine. I'm not clear what has changed. Has the behavior of protected changed so that the shorter name is no longer accessible even within the recursive function? Or was lean3 somehow able to see the has_add instance on the following lines (that is now being translated to Add)?

Or... is this just a bug in lean4?

Unless it's a bug, I think the most general fix here is to have mathport always add the type prefix to the current definition's name (replacing each recursive add with PosNum.add in this case)...

[michal wallace (tangentstorm)]

the behavior for mul is also interesting:
old:

protected def mul (a : pos_num) : pos_num → pos_num
  | 1        := a
  | (bit0 b) := bit0 (mul b)
  | (bit1 b) := bit0 (mul b) + a

the generated code is wrong on two counts:

protected def mul (a : PosNum) : PosNum → PosNum
  | 1 => a
  | bit0 b => bit0 (mul b)
  | bit1 b => bit0 (mul b) + a

first, it doesn't know the name mul, but second, if i change it to PosNum.mul, it fails because it's missing an a argument.

[michal wallace (tangentstorm)]

Okay, well... Here's the step-by-step changelog for the cleanup I was able to do manually:
https://github.com/tangentstorm/tangentlabs/commits/master/lean4/Bin/Lean4DataNumBasic.lean

[michal wallace (tangentstorm)]

there are still several remaining bugs that i don't know how to address yet:

• implement dsimp'
• castPosNum :: bit0 needs to be on the α type, and I don't think bit0 is part of lean4?
• in general, the generic coercion stuff seems to need a revamp ( CoeTₓ )
• lack of coercion is breaking the repr implementation
• Nat.binaryRec seems to be a standard function in lean3 that no longer exists. (Is that on purpose? I think I could have actually used it earlier.)
• re-enable has_reflect (probably will need to implement the deriving code in lean4 to make that happen)

[michal wallace (tangentstorm)]

If anyone can either:

• a) look over my changelog and see if I screwed anything up, or
• b) help me out with these last few issues,
  ... I'd really appreciate it.

Meanwhile, I'll move on to studying the mathport code and see if I can have it handle the changes I was doing by hand.

[Kyle Miller]

I'm not sure what the plan is, but docs#nat.binary_rec is in Lean 3 core rather than mathlib and could be ported too, though perhaps for computational reasons you'd want to make the z : C 0 argument be z : Unit -> C 0

[Mario Carneiro]

There are mathlib4 files that correspond to lean 3 core files in Mathlib.Init.*

[Mario Carneiro]

so Nat.binaryRec would go in one of those

[Mario Carneiro]

if it's not in lean 4 core, then it's probably not needed anymore so if mathlib needs it it should be redefined in mathlib4

[Mario Carneiro]

We probably want to migrate away from bit0 and bit1 eventually, but for the port I think we should just add it to Mathlib.Init.*

[Mario Carneiro]

As for referencing protected definitions, that is one of many small elaboration differences that is likely to cause problems in the port, and we don't have any uniform solution there. I'm not sure how feasible it is to backport the change - I don't think lean 3 can handle local variables that are not atomic

[Mario Carneiro]

If it's a common enough pattern, I think we could detect it in synport

[Notification Bot]

This topic was moved here from #lean4 > mathport improvements for data.num.add by Mario Carneiro.

[michal wallace (tangentstorm)]

I added a github repo to start collecting notes/work on this.
https://github.com/tangentstorm/Lean4-DataNumBasic/
I've got next week off for moving house, but i hope to have some free time to work on this as well. (In any case, I expect this to be my main project for most of next month.)