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: Dec 20 2023 at 11:08 UTC