Zulip Chat Archive

Stream: new members

Topic: (∀ (n : ℤ), P n) ∨ ∀ (n : ℤ), ¬P n

toc (Sep 06 2020 at 18:23):

I have a goal (from one of the icl exercises) that looks like:

( (n : ), P n)   (n : ), ¬P n

how do I... even start? None of the split/cases/assume/&c seems to break it down at all.

Kenny Lau (Sep 06 2020 at 18:24):

what if P 0 is true but P 1 is false?

toc (Sep 06 2020 at 18:25):

The whole exercise has also

P:   Prop
h8:  (n : ), P n  P (n + 8)
h3:  (n : ), P n  P (n - 3)

so I will be proving that that is not possible.

Jason KY. (Sep 06 2020 at 18:32):

I would think you can start with something like

import tactic

example (P:   Prop)
  (h8:  (n : ), P n  P (n + 8))
  (h3:  (n : ), P n  P (n - 3)) : ( (n : ), P n)   (n : ), ¬P n :=
  by_cases (P 0),
  left, sorry,
  right, sorry,

toc (Sep 06 2020 at 18:36):

Ah, thank you!

Chris Wong (Sep 07 2020 at 00:18):

Yep, that goal looks like classical reasoning so by_cases is a good suggestion

Kevin Buzzard (Sep 07 2020 at 06:09):

Ha ha yes sorry, I do not make it at all clear in the questions that classical reasoning is allowed because my audience knows no other reasoning

toc (Sep 08 2020 at 21:39):

@Kevin Buzzard It's you! Thank you for all the learning materials! If that's the case are there lecture (videos? notes?) I could be following along for these exercises?

Kevin Buzzard (Sep 08 2020 at 21:41):

No, I never made any instructions for them, I just told my students to come to the Xena meetings on Thursdays and ask questions

Kevin Buzzard (Sep 08 2020 at 21:42):

You might want to read Mathematics in Lean instead, that has more explanations!

Bryan Gin-ge Chen (Sep 08 2020 at 21:42):

There's a list of Lean-related tutorials and other learning material here: https://leanprover-community.github.io/learn.html

blackxv (Sep 29 2020 at 07:45):

h8: ∀ (n : ℤ), P n → P (n + 8)
h3: ∀ (n : ℤ), P n → P (n - 3)
n: ℕ
hn: P (int.of_nat n)
⊢ P (int.of_nat n.succ)

Now, if I
apply h3 (n+4:ℤ),
get the error

invalid apply tactic, failed to unify
P (int.of_nat n.succ)
P (↑n + 4 - 3)


Kyle Miller (Sep 29 2020 at 07:46):

If you do convert instead of apply, then you'll get a new goal which is just the arithmetic you have to show.

Kyle Miller (Sep 29 2020 at 07:47):

(Or is it convert_to? I always forget which is which...)

Kevin Buzzard (Sep 29 2020 at 08:08):

You can use the better induction principle int.induction_on instead of casing on the int

Kevin Buzzard (Sep 29 2020 at 08:09):

One problem you have right now is that subtraction on naturals stinks

Kevin Buzzard (Sep 29 2020 at 08:09):

It's best to never mention them.

Last updated: Dec 20 2023 at 11:08 UTC