Zulip Chat Archive

Stream: new members

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


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

view this post on Zulip Kenny Lau (Sep 06 2020 at 18:24):

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

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

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

view this post on Zulip toc (Sep 06 2020 at 18:36):

Ah, thank you!

view this post on Zulip Chris Wong (Sep 07 2020 at 00:18):

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

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

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

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

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 21:42):

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

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

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

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

view this post on Zulip Kyle Miller (Sep 29 2020 at 07:47):

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

view this post on Zulip Kevin Buzzard (Sep 29 2020 at 08:08):

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

view this post on Zulip Kevin Buzzard (Sep 29 2020 at 08:09):

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

view this post on Zulip Kevin Buzzard (Sep 29 2020 at 08:09):

It's best to never mention them.


Last updated: May 14 2021 at 03:27 UTC