Strange behaviour of nested induction?

Stream: lean4

[Siddhartha Gadgil]

I must be missing something simple, but I have been staring at this for a while and cannot spot it. In the code below, there is a have in part of a proof which seems to have the wrong induction hypothesis (hb below), hence the proof does not finish. When I extract that as a theorem, everything is fine.

open Nat
theorem add_comm₃ : ∀ (a b : Nat), a + b = b + a :=
  by
  intro a b
  induction a
  case zero =>
    try (simp only)
    rw [(Nat.add_zero b)]
    try (simp only)
    have rw_lemma : zero + b = b := by
      induction b
      case zero =>
        rw [(Nat.add_zero zero)]
      case succ aa ha =>
        try (simp only)
        rw [(add_succ zero aa)]
        rw [(ha)]
    rw [(rw_lemma)]
  case succ aa ha =>
    try (simp only)
    have rw_lemma : succ aa + b = succ (aa + b) := by
      induction b
      case zero =>
        rw [(Nat.add_zero (succ aa))]
      case succ bb hb =>
        rw [(add_succ (succ aa) bb)]
        rw [(add_succ aa bb)]
        rw [(hb)]
    rw [(rw_lemma)]
    try (simp only)
    rw [(add_succ b aa)]
    rw [(ha)]


theorem rw_lemma : succ aa + b = succ (aa + b) := by
      induction b
      case zero =>
        rw [(Nat.add_zero (succ aa))]
      case succ bb hb =>
        rw [(add_succ (succ aa) bb)]
        rw [(add_succ aa bb)]
        rw [(hb)]

Any help is appreciated.

[Ruben Van de Velde]

Might be an issue with the case tactic and duplicated labels?

[Ruben Van de Velde]

(Why do you wrap all your rewrite lemmas in parentheses?)

[Kyle Miller]

Have the first step of have rw_lemma be clear ha. That keeps it from being used as an induction hypothesis.

[Siddhartha Gadgil]

So should it be considered a bug? (The rewrites are in parenthesis as this is the result of code generation, and somehow (tactic|rw [($t)]) for a term t` but not without the parenthesis.

[Kyle Miller]

No, it's not a bug

[Siddhartha Gadgil]

Kyle Miller said:

No, it's not a bug

What is the principle based on which hb has different type in the two cases?

[Kyle Miller]

(Watch out that simp [foo] and simp [(foo)] can be different, since the first adds foo as a simp lemma, and the second elaborates foo, abstracts the result, and adds that as a simp lemma.)

[Kyle Miller]

The principle is that when you do induction an a variable, then every hypothesis in the local context that depends on that variable is now something that has to be inductively proved to be true.

[Siddhartha Gadgil]

How do I avoid the parenthesis: (tactic| rw [$t]) does not accept a term $t`

[Kyle Miller]

Clearing it says "I will not depend on this, so do not require me to prove it along with the induction."

[Kyle Miller]

Maybe rw [$t:term]?

[Kyle Miller]

Here's a hint regarding clearing: try doing revert b and see what the goal looks like. That's the form of the induction hypothesis.

[Siddhartha Gadgil]

Kyle Miller said:

Maybe rw [$t:term]?

Thanks. That works. I thought I had tried that.

[Siddhartha Gadgil]

The clear works fine. As I am doing code generation I will have to keep track of the context which I will.

[Kyle Miller]

The reason I thought to suggest $t:term is that when more complicated expressions are supported in a particular location, then specifying what kind of expression it's supposed to be can help it parse.

[Siddhartha Gadgil]

I have experienced this and done the same many times. Somehow thought I had tried it here and it failed. But it does work.

[Kyle Miller]

The clear works fine.

Sure, but it seemed like you were asking why it was necessary, and I think seeing what revert b does is useful. (The induction tactic itself reverts the induction target.)

[Kyle Miller]

It's basically revert b; refine Nat.rec ?zero ?zucc followed by some appropriate intros per case. (The generalizing clause adds more things to be reverted.)

[Siddhartha Gadgil]

Indeed revert b with and without the clear makes things vivid. I see that b a priori is a function of the context, hence the induction behave differently.