complete_lattice.Inf and nat.find

Stream: new members

[Patrick Johnson]

What is the recommended way to prove this sorry? It seems trivial: since there is at least one number that satisfies the argument of nat.find, it means that if nat.find returns 0, then the argument must hold for 0, but h₁ asserts that it doesn't hold; contradiction. But I'm failing to see how nat.find lemmas can easily prove this.

example
  (f : ℕ → Prop)
  (h₁ : f 0)
  (h₂ : ∃ (n : ℕ), ¬f n)
  (h₃ : Inf {b | ¬f b} = 0)
  : false :=
begin
  unfold Inf at h₃,
  obtain ⟨n, h₂⟩ := h₂,
  split_ifs at h₃ with h₄,
  { cases n,
    { exact h₂ h₁ },
    { sorry }},
  { push_neg at h₄,
    replace h₄ := h₄ n,
    exact h₄ h₂ },
end

The proof already looks excessively long for such a trivial statement. Is there a better way to deal with Inf?

[Patrick Johnson]

By the way, is there a short way to rewrite n ∉ {b : ℕ | ¬f b} to ¬¬f n. They are definitionally equal, but the first one looks ugly.

[Eric Wieser]

Which hypothesis contains n ∉ {b : ℕ | ¬f b}?

[Patrick Johnson]

h₄ after replace h₄ := h₄ n

[Andrew Yang]

You could use Inf_mem to obtain a one line proof

example
  (f : ℕ → Prop)
  (h₁ : f 0)
  (h₂ : ∃ (n : ℕ), ¬f n)
  (h₃ : Inf {b | ¬f b} = 0)
  : false := (h₃ ▸ Inf_mem h₂) h₁

[Eric Rodriguez]

if you want to do it "directly", your first case in the split_ifs can be replaced with

{ letI := classical.prop_decidable,
    have := nat.find_spec h₄,
    dsimp at this,
    rw h₃ at this,
    contradiction },

but Inf_mem is a better approach

[Eric Wieser]

docs#nat.Inf_eq_zero also looked promising, but isn't as fast

[Ruben Van de Velde]

Patrick Johnson said:

it means that if nat.find returns 0, then the argument must hold for 0

nat.find_eq_zero should do this, but I got stuck in decidability hell

[Eric Rodriguez]

Ruben Van de Velde said:

Patrick Johnson said:

it means that if nat.find returns 0, then the argument must hold for 0

nat.find_eq_zero should do this, but I got stuck in decidability hell

Inf uses classical.prop_decidable