Zulip Chat Archive

Stream: new members

Topic: complete_lattice.Inf and nat.find


Patrick Johnson (Dec 09 2021 at 11:31):

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 (Dec 09 2021 at 11:34):

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 (Dec 09 2021 at 11:38):

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

Patrick Johnson (Dec 09 2021 at 11:38):

h₄ after replace h₄ := h₄ n

Andrew Yang (Dec 09 2021 at 11:41):

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 (Dec 09 2021 at 11:42):

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 (Dec 09 2021 at 11:43):

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

Ruben Van de Velde (Dec 09 2021 at 11:43):

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 (Dec 09 2021 at 11:55):

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


Last updated: Dec 20 2023 at 11:08 UTC