mathport improvements for `data.num.add`

Stream: lean4

[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

[Notification Bot]

This topic was moved to #mathlib4 > mathport improvements for data.num.add by Mario Carneiro.