# Zulip Chat Archive

## 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

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

#### 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