Stream: general

Topic: Refactoring nat.cast to nat.bin_cast

Yakov Pechersky (Feb 10 2021 at 17:35):

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 (Feb 10 2021 at 17:36):

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 (Feb 10 2021 at 17:58):

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

Yakov Pechersky (Feb 10 2021 at 17:59):

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

Mario Carneiro (Feb 10 2021 at 17:59):

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 (Feb 10 2021 at 18:00):

You can just copy/paste the definition

Yakov Pechersky (Feb 10 2021 at 18:00):

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 (Feb 10 2021 at 18:03):

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

Mario Carneiro (Feb 10 2021 at 18:04):

not sure how that affects your refactor though

Yakov Pechersky (Feb 10 2021 at 18:05):

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 (Feb 10 2021 at 18:06):

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

Mario Carneiro (Feb 10 2021 at 18:07):

you don't need associativity to prove it

(deleted)

Yakov Pechersky (Feb 10 2021 at 18:07):

I had issues using nat.binary_rec for this

Mario Carneiro (Feb 10 2021 at 18:08):

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

Last updated: May 11 2021 at 22:14 UTC