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

Stream: new members

[toc]

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]

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

[toc]

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.]

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

[toc]

Ah, thank you!

[Chris Wong]

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

[Kevin Buzzard]

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]

@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]

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]

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

[Bryan Gin-ge Chen]

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

[blackxv]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

It's best to never mention them.