Zulip Chat Archive

Stream: new members

Topic: A basic question about tactics


view this post on Zulip 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?

view this post on Zulip Henning Dieterichs (Dec 30 2020 at 22:37):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Victor Miller (Dec 30 2020 at 22:40):

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

view this post on Zulip 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?

view this post on Zulip 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:

view this post on Zulip Kevin Buzzard (Dec 30 2020 at 22:41):

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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 30 2020 at 22:47):

view this post on Zulip Mario Carneiro (Dec 30 2020 at 22:55):

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

view this post on Zulip Victor Miller (Dec 30 2020 at 22:56):

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

view this post on Zulip Mario Carneiro (Dec 30 2020 at 22:56):

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

view this post on Zulip Mario Carneiro (Dec 30 2020 at 22:57):

that approach doesn't even need int.induction_on

view this post on Zulip 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