Zulip Chat Archive

Stream: new members

Topic: bit0? how do I get succ(succ(0)) from 2?


view this post on Zulip eax (Feb 28 2021 at 08:13):

I'm trying to prove ⊢ a ^ 2 = a ^ 2 + 0 ^ 2 (actually, part of (a + b) ^ (2 : mynat) = a ^ (2 : mynat) + b ^ (2 : mynat) + 2 * a * b := but ignore that for the moment) and think I need the fact that 2 = succ(succ(0)) but can't seem to get lean to output this. if I try one_eq_succ_zero I get a bit0 which I'm not sure how to deal with yet.

view this post on Zulip eax (Feb 28 2021 at 08:14):

if I could get this, then I should be able to use pow_succ and then mul_zero and then refl

view this post on Zulip Eric Wieser (Feb 28 2021 at 08:26):

It's true by rfl

view this post on Zulip eax (Feb 28 2021 at 16:58):

thanks! Same idea as my previous tread then. is there a more direct way of getting there fwiw?

view this post on Zulip eax (Feb 28 2021 at 17:18):

or alternatively, is there a way to enable tracing in the NNG? it would nice to see what lean is actually doing

view this post on Zulip Kevin Buzzard (Feb 28 2021 at 17:40):

Download the repo from GitHub and play with it in VS Code maybe. It's filed under ImperialCollegeLondon IIRC.

view this post on Zulip Lars Ericson (Feb 28 2021 at 19:22):

@eax there is a little more detail on bit1 in this thread: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/if.20a.20.3C.20b.20then.20a.5E3.20.3C.20b.5E3/near/224516939


Last updated: May 11 2021 at 00:31 UTC