Is there a better way to solve this excercise?

Stream: new members

[Spearman]

https://lean-lang.org/functional_programming_in_lean/tactics-induction-proofs.html#exercises

• Prove plusR_succ_left using the induction ... with tactic.

After a few weekends of not getting anywhere with trying to solve this exercise, I asked chatgpt for suggestions and the thing I was missing was the intro tactic, which I don't see mentioned in the text. I ended up with this solution:

theorem plusR_succ_left (n : Nat) :
  (k : Nat) -> Nat.plusR (n + 1) k = Nat.plusR n k + 1 := by
  induction n with
    | zero => simp <;> intro k <;> induction k with
      | zero => rfl
      | succ nn aa => rw [Nat.plusR] <;> simp <;> exact aa
    | succ m _a => intro k <;> induction k with
      | zero => rfl
      | succ nn aa => rw [Nat.plusR] <;> simp <;> exact aa

I imagine that there's a more succinct proof although I think this one is pretty readable, I'm not sure about the un-used assumption I ended up with (_a).

In general how do you go about finding the tactic that you need, it seems especially hard given that they don't have types, or at least I can't figure out how to view the types.

[Eric Wieser]

I'm not sure about the un-used assumption I ended up with (_a).

If you find yourself with the induction hypothesis unused, you can replace induction with cases

[Eric Wieser]

And if you find yourself with a cases tactic where both branches are the same, then you can often eliminate the cases altogether.

[Eric Wieser]

I think this exercise is trying to teach you how to translate the proof you already wrote (without tactics) in https://lean-lang.org/functional_programming_in_lean/dependent-types/pitfalls.html?highlight=plusR_succ_left#propositional-equality

[Spearman]

Eric Wieser said:

And if you find yourself with a cases tactic where both branches are the same, then you can often eliminate the cases altogether.

I did find that I had an un-needed simp in the first base case, without which both cases have the same tactics used. The next exercise is:

• Rewrite the proof of plus$_succ_left to use <;> in a single line.

So I ended up with this:

theorem plusR_succ_left' (n : Nat) :
  (k : Nat) -> Nat.plusR (n + 1) k = Nat.plusR n k + 1 := by
  induction n <;> intro k <;> induction k with | zero => rfl | succ nn aa => rw [Nat.plusR] <;> simp <;> exact aa

[Eric Wieser]

I'm pretty sure you can drop the induction n entirely