basic logic

Stream: general

[Kevin Buzzard]

lemma finite_or_infinite_peaks (a : ℕ → ℝ) :
(∃ N, ∀ i, is_peak a i → i ≤ N) ∨ (∀ N, ∃ i, is_peak a i ∧ i > N) := sorry

(is_peak a i is just some random predicate). This is true by pure logic. Is there a tactic which does this for me? I tried cc and finish and now I'm out of ideas.

[Johan Commelin]

tauto?

[Kevin Buzzard]

I'm happy to be classical if this is an issue

[Johan Commelin]

Didn't try it though...

[Kevin Buzzard]

tauto doesn't work for me. I hope I've not made a typo :-) I didn't try to prove it :-)

[Kevin Buzzard]

OK, no typo :-)

lemma finite_or_infinite_peaks (a : ℕ → ℝ) :
(∃ N, ∀ i, is_peak a i → i ≤ N) ∨ (∀ N, ∃ i, is_peak a i ∧ i > N) :=
begin
  cases classical.em (∃ N, ∀ i, is_peak a i → i ≤ N),
    left, assumption,
  right,
  intro N,
  replace h := forall_not_of_not_exists h,
  replace h := h N,
  dsimp at h,
  rw not_forall at h,
  cases h with x hx,
  use x,
  rw not_imp at hx,
  convert hx,
  simp,
end

Help!

[Kevin Buzzard]

Just to be clear, the question is how to pwn it, not how to prove it.

[Patrick Massot]

Did you try something like

lemma finite_or_infinite_peaks (a : ℕ → ℝ) :
(∃ N, ∀ i, is_peak a i → i ≤ N) ∨ (∀ N, ∃ i, is_peak a i ∧ i > N) :=
begin
  by_cases H : (∃ N, ∀ i, is_peak a i → i ≤ N),
  { left, assumption },
  { right,
    simpa [not_exists, not_forall, not_le, exists_prop] using H }
end

[Patrick Massot]

I agree there should be a tactic for this. I started to work on it, but have too many things going on...

[Patrick Massot]

Better:

lemma finite_or_infinite_peaks (a : ℕ → ℝ) :
(∃ N, ∀ i, is_peak a i → i ≤ N) ∨ (∀ N, ∃ i, is_peak a i ∧ i > N) :=
begin
  rw or_iff_not_imp_left,
  intro H,
  simpa [not_exists, not_forall, not_le, exists_prop] using H
end

[Patrick Massot]

I realized while teaching that students don't like left vs right when proving disjunctions, what they feel to be natural is exactly this "or_iff_not_imp_left" style of proof

[Patrick Massot]

I mean normal students, not constructive Kenny

[Mario Carneiro]

open classical
local attribute [instance] prop_decidable
variables (R : Type) (is_peak : (ℕ → R) → ℕ → Prop)
lemma finite_or_infinite_peaks (a : ℕ → R) :
  (∃ N, ∀ i, is_peak a i → i ≤ N) ∨ (∀ N, ∃ i, is_peak a i ∧ i > N) :=
by simpa [not_forall] using em (∃ N, ∀ i, is_peak a i → i ≤ N)

[Mario Carneiro]

I would usually use by_cases ∃ N, ∀ i, is_peak a i → i ≤ N and simplify the hypothesis in the second branch

[Patrick Massot]

I should have written my solution works with simpa only

[Patrick Massot]

I still don't know why not_exists is a simp lemma while not_forall isn't

[Mario Carneiro]

I was just asking myself the same question

[Patrick Massot]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/not_forall

[Mario Carneiro]

those decidability assumptions are really awkward tho

[Kenny Lau]

because one is constructive and the other isn't?

[Mario Carneiro]

they are both constructive kenny

[Kenny Lau]

you know what I mean