A basic question about tactics

Stream: new members

[Victor Miller]

I'm going through the M40001/M40009 exercises for 2019. I'm still not completely getting the hang of how to structure some tactic proofs.

For example, I stated the following that I wanted to prove

lemma question_5_aux2 (P: ℤ → Prop) (h: ∀ n, P n ↔ P (n+1)): (∀ n, P n) ∨ (∀ n, ¬ (P n)) :=

I'd like to prove this by induction -- once I have a variable n: int I can do cases on it and then do induction positively and negatively.
But I can't figure out which tactic can introduce such a variable. I can't do left or right since there are two possibilities that are mutually exclusive.
Also, while trying to do this, I realize that I have to simplify the arithmetic, for example P(n+1+1) simplified to P(n+2), but simp doesn't seem to do this . I'm assuming that I need to do a rw, but how do I find what things are in the definition of integers that allows me to do this?

[Henning Dieterichs]

How would you do a pen&paper proof for this statement?

[Kevin Buzzard]

This is a tricky question for a Lean beginner! Rather than doing cases on the integer I'd recommend the more principled induction procedure int.induction_on. n+1+1 and n+2 are equal by definition, so change can be used to change between two forms, and you might not need to use it at all.

[Patrick Massot]

This is not what he is missing. He is blocked by the or. Victor, you need to start with by_cases h : P 0.

[Victor Miller]

@Patrick: Thanks. I didn't know about by_cases.

[Henning Dieterichs]

I think any pen&paper proof for this would also start with a case distinction on P(0), wouldn't it?

[Patrick Massot]

You could think such things should be automatic but there is all this crazyness about constructive mathematics. Some people would say you statement is unprovable. :shrug:

[Kevin Buzzard]

Oh come on, the pen and paper proof is "it's obvious" ;-)

[Patrick Massot]

Victor, you may be interested in doing the tutorial project. It covers by_cases (and many more basic stuff, although there is no induction there).

[Henning Dieterichs]

@Victor Miller I can highly recommend bookmarking this cheatsheet of common lean tactics: https://leanprover-community.github.io//img/lean-tactics.pdf - it helped me a lot

[Kevin Buzzard]

import tactic

lemma question_5_aux2 (P: ℤ → Prop) (h: ∀ n, P n ↔ P (n+1)) :
  (∀ n, P n) ∨ (∀ n, ¬ (P n)) :=
begin
  by_cases h0 : P 0,
  { left,
    intro n,
    apply int.induction_on n h0,
    { intro i, convert (h i).1, refl },
    { intro i, convert (h (-(i : ℤ) - 1)).2, simp, }
  },
  { right,
    intro n,
    apply int.induction_on n,
    { exact h0 },
    { intro i, apply mt, convert (h i).2, refl },
    { intro i, apply mt, convert (h (-(i : ℤ) - 1)).1, simp },
  },

end

[Mario Carneiro]

I would go through a lemma that says \forall n, P n <-> P 0

[Victor Miller]

@Mario, I had that as another lemma. Great minds think alike :-).

[Mario Carneiro]

or \forall n (m:nat), P n <-> P (n+m)

[Mario Carneiro]

that approach doesn't even need int.induction_on

[Victor Miller]

@Kevin Buzzard int.induction_on is something I didn't know about. Thanks