Zulip Chat Archive

Stream: new members

Topic: NNG and change of induction basis


Kwame Porter Robinson (Feb 07 2022 at 19:58):

I'm working on a natural numbers game level (World 9, Level 4), solved it, and am now exploring other proofs to that level. I know Lean has le_induction that starts from a different base case (e.g. n=1) but in NNG we have induction. Is there a way to change the basis of induction?

I attempted to do this with,

have a := 1 <= a, -- "error: failed to synthesize type class instance for for a b c : mynat,"
induction a with k h1,

In Lean 4
theorem mul_left_cancel2 (a b c : nat) (ha : a ≠ 0) : a * b = a * c → b = c := begin have a : 1 <= a,
gives

2 goals
abc: 
ha: a  0
 1  a

abc: 
ha: a  0
a: 1  a
 a * b = a * c  b = c

and I can continue to solve the level with a different proof.

Kyle Miller (Feb 07 2022 at 20:00):

One way is to do cases a first, and for the second goal you do induction a like usual.


Last updated: Dec 20 2023 at 11:08 UTC