Zulip Chat Archive

Stream: Is there code for X?

Topic: nat.find_ge_of_not?


view this post on Zulip Ryan Lahfa (Feb 01 2021 at 14:45):

I'm looking for something like this:

import data.real.basic
import data.nat.choose.basic

lemma nat.const_le_find_of_not (p:   Prop) [decidable_pred p] (c: ) (H:  n, p n):
  ( (n: ), n  c  ¬ p n)  c  nat.find H := sorry

theorem mwe (exists_nat_unbdd:  z : , abs (z: ) > 1):
  2  nat.find exists_nat_unbdd := sorry

It appears to me it does not exist in mathlib, should this exist? In this case, I believe I could finish the main theorem by some decidability tactic, am I wrong?

view this post on Zulip Floris van Doorn (Feb 01 2021 at 18:16):

The first inequality is an easy consequence of docs#nat.find_spec (by contradiction).
You can even make one of the \le into <. Is it worth adding? Not sure.

view this post on Zulip Floris van Doorn (Feb 01 2021 at 18:45):

I think the first lemma (and variants) is useful when formulated as iff:

@[simp] lemma find_lt_iff (h :  n : , p n) (n : ) : nat.find h < n   m < n, p m :=
λ h2, nat.find h, h2, nat.find_spec h⟩, λ m, hmn, hm⟩, (nat.find_min' h hm).trans_lt hmn

@[simp] lemma find_le_iff (h :  n : , p n) (n : ) : nat.find h  n   m  n, p m :=
by simp only [exists_prop,  lt_succ_iff, find_lt_iff]

@[simp] lemma le_find_iff (h :  (n : ), p n) (n : ) : n  nat.find h   m < n, ¬ p m :=
by simp_rw [ not_lt, not_iff_comm, not_forall, not_not, find_lt_iff]

@[simp] lemma lt_find_iff (h :  n : , p n) (n : ) : n < nat.find h   m  n, ¬ p m :=
by simp only [ succ_le_iff, le_find_iff, succ_le_succ_iff]

See #6002

view this post on Zulip Ryan Lahfa (Feb 03 2021 at 00:03):

Really, thanks a lot!

view this post on Zulip Ryan Lahfa (Feb 03 2021 at 00:04):

Indeed, I had the feeling they were not that far from find_spec or find_min, but it's really cool they are in mathlib now :)


Last updated: May 17 2021 at 15:13 UTC