## Stream: new members

### Topic: A basic question about tactics

#### Victor Miller (Dec 30 2020 at 22:33):

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 (Dec 30 2020 at 22:37):

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

#### Kevin Buzzard (Dec 30 2020 at 22:38):

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 (Dec 30 2020 at 22:39):

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 (Dec 30 2020 at 22:40):

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

#### Henning Dieterichs (Dec 30 2020 at 22:41):

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

#### Patrick Massot (Dec 30 2020 at 22:41):

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 (Dec 30 2020 at 22:41):

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

#### Patrick Massot (Dec 30 2020 at 22:43):

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 (Dec 30 2020 at 22:43):

@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

#### Mario Carneiro (Dec 30 2020 at 22:55):

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

#### Victor Miller (Dec 30 2020 at 22:56):

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

#### Mario Carneiro (Dec 30 2020 at 22:56):

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

#### Mario Carneiro (Dec 30 2020 at 22:57):

that approach doesn't even need int.induction_on

#### Victor Miller (Dec 30 2020 at 23:00):

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

Last updated: May 11 2021 at 13:22 UTC