Refactoring nat.cast to nat.bin_cast

Stream: general

[Yakov Pechersky]

On a side note, I've been trying a branch to refactor the default cast to nat to be nat.bin_cast. It hasn't been going well. There's a lot of abuse of numeral notation, like this: docs#pgame.short_nat, docs#pgame.short_bit0, docs#pgame.short_bit1. The data-relation pgame.relabelling has an "add_monoid"al aspect to it, but trying to show that via a sigma type hasn't worked out. And the proofs juggling around pgame.relabelling have been difficult, because I couldn't get calc to work with it.

[Yakov Pechersky]

Mario Carneiro said:

In the PR you linked though, you are parsing decimal strings, so the obvious approach would be to look for 0-9 and evaluate 10*n+a for each digit

That's exactly what src#parser.nat does

[Mario Carneiro]

(moved from #general > semantics of description logics: binary representation of...)

[Mario Carneiro]

What if you generalized parser.nat to any type with + and *, instead of parsing to nat and then casting to A?

[Yakov Pechersky]

Sure, but that was a change in core, as opposed to adding a variant in mathlib

[Mario Carneiro]

I'm not sure it's a good idea to change nat.cast to nat.bin_cast since this impacts all other users

[Mario Carneiro]

You can just copy/paste the definition

[Yakov Pechersky]

Agreed, I was just testing if it worked. In general, I wasn't sure if there were any types with has_zero has_one and has_add that were not add_monoid. But the pgame related things are.

[Mario Carneiro]

Yeah, that's what surreal is about, it's the quotient of pgame by associativity among other things

[Mario Carneiro]

not sure how that affects your refactor though

[Yakov Pechersky]

All sorts of lemmas like src#pgame.short_nat break, because they use the equation compiler to break into the 0 and succ case instead of what now has to be 0, 1, bit0, bit1 and require more passing of assumptions about 0 + 0 ~ 0 and x + y + z ~ x + (y + z), etc.

[Mario Carneiro]

That theorem would have to be proven by binary recursion if you want to prove the analogous result for nat.bin_cast

[Mario Carneiro]

you don't need associativity to prove it

[Yakov Pechersky]

(deleted)

[Yakov Pechersky]

I had issues using nat.binary_rec for this

[Mario Carneiro]

Well this is part of why I said it might not be a good idea, nat.bin_cast is defined by binary recursion so you need a good story for doing proofs by binary recursion if you want to replace it