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

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 :=
begin
by_cases (P 0),
left, sorry,
right, sorry,
end


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)
with
P (↑n + 4 - 3)

:broken_heart:

#### 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: May 14 2021 at 03:27 UTC