Lucy

Stream: new members

[Lucy]

Hi, I'm Lucy, I'm getting into Lean in preparation for it being the PPCG SE's language of the month for October. I was particularly interested in Lean because I have some experience with Agda, and experience in formal logic more generally (though I'm a little rusty). I was working through the natural number game and was messing around trying to prove commutativity of addition without the lemmas proved earlier in addition world. When attempting to construct a proof, I attempted to perform induction inside the induction step of another induction, the induction step turned out to be this (hd is the hypothesis from the outer induction, id is the hypothesis from the inner induction):

h i : mynat,
id : i + h = h + i → succ (h + i) = succ h + i,
hd : succ i + h = h + succ i
⊢ succ (h + succ i) = succ h + succ i

I was confused as to why id required i + h = h + i as a prior, which seems like it would make id, and therefore the second use of induction, useless to me in proving the goal. I was wondering if anyone could clarify why nested induction behaves like this, and how to mitigate it.

[Scott Morrison]

I'm not sure exactly what your goal or proof-so-far is (can you post a #mwe?) but often the advice in this situation is that when you do the first induction you need with write something like induction x generalizing y (where y is the thing you're planning on doing the second induction on).

[Chris B]

@Lucy

The induction tactic isn't inferring the motive you want (In lean 3, it's the thing labelled C in the recursor). It's inferring it as:

(λ (b : ℕ), x + b = b + x → x.succ + b = b + x.succ)

when you probably want it to be:

(λ b, x.succ + b = b + x.succ)

You can control the motive yourself by using rec/rec_on manually instead of using the induction tactic, but I think this isn't recommended in the general case:

example (a b : nat ) : a + b = b + a :=
begin
  induction a with x,
  case zero : { simp },
  case succ : {
    refine @nat.rec_on (λ b, x.succ + b = b + x.succ) b _ _,
    { simp, },
    { simp [nat.add_succ, nat.succ_add], }
  }
end

[Chris B]

Or maybe you want a different motive, what was your strategy for proving it by using induction twice without other lemmas?

[Scott Morrison]

I think I agree with Chris's suggestion that it's not such a great idea to avoid using all other lemmas and to do a double induction, but it does work:

inductive mynat
| zero
| succ : mynat → mynat

open mynat

def add : mynat → mynat → mynat
| x zero := x
| x (succ y) := succ (add x y)

example (a b : mynat) : add a b = add b a :=
begin
  induction a with a ih generalizing b,
  { induction b with b ih',
    { refl, },
    { dsimp [add], rw [ih'], refl, } },
  { induction b with b ih',
    { dsimp [add], rw [←ih], refl, },
    { dsimp [add], rw [ih'], dsimp [add], rw [←ih, ←ih], refl, }, }
end