Explicit least witnesses to existentials on positive natural numbers

Implemented via calling out to Nat.find.

instance PNat.decidablePredExistsNat {p : ℕ+ → Prop} [DecidablePred p] : DecidablePred fun (n' : ℕ) => ∃ (n : ℕ+) (_ : n' = ↑n), p n

Equations

• PNat.decidablePredExistsNat n' = decidable_of_iff' (∃ (h : 0 < n'), p ⟨n', h⟩) ⋯

def PNat.findX {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) : { n : ℕ+ // p n ∧ ∀ m < n, ¬p m }

The PNat version of Nat.findX

Equations

• PNat.findX h = let_fun this := ⋯; let_fun n := Nat.findX this; ⟨⟨↑n, ⋯⟩, ⋯⟩

def PNat.find {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) : ℕ+

If p is a (decidable) predicate on ℕ+ and hp : ∃ (n : ℕ+), p n is a proof that there exists some positive natural number satisfying p, then PNat.find hp is the smallest positive natural number satisfying p. Note that PNat.find is protected, meaning that you can't just write find, even if the PNat namespace is open.

The API for PNat.find is:

• PNat.find_spec is the proof that PNat.find hp satisfies p.
• PNat.find_min is the proof that if m < PNat.find hp then m does not satisfy p.
• PNat.find_min' is the proof that if m does satisfy p then PNat.find hp ≤ m.

Equations

• PNat.find h = ↑(PNat.findX h)

theorem PNat.find_spec {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) : p (PNat.find h)

theorem PNat.find_min {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) {m : ℕ+} : m < PNat.find h → ¬p m

theorem PNat.find_min' {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) {m : ℕ+} (hm : p m) : PNat.find h ≤ m

theorem PNat.find_eq_iff {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) {m : ℕ+} : PNat.find h = m ↔ p m ∧ ∀ n < m, ¬p n

@[simp]

theorem PNat.find_lt_iff {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) (n : ℕ+) : PNat.find h < n ↔ ∃ m < n, p m

@[simp]

theorem PNat.find_le_iff {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) (n : ℕ+) : PNat.find h ≤ n ↔ ∃ m ≤ n, p m

@[simp]

theorem PNat.le_find_iff {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) (n : ℕ+) : n ≤ PNat.find h ↔ ∀ m < n, ¬p m

@[simp]

theorem PNat.lt_find_iff {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) (n : ℕ+) : n < PNat.find h ↔ ∀ m ≤ n, ¬p m

@[simp]

theorem PNat.find_eq_one {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) : PNat.find h = 1 ↔ p 1

theorem PNat.one_le_find {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) : 1 < PNat.find h ↔ ¬p 1

theorem PNat.find_mono {p : ℕ+ → Prop} {q : ℕ+ → Prop} [DecidablePred p] [DecidablePred q] (h : ∀ (n : ℕ+), q n → p n) {hp : ∃ (n : ℕ+), p n} {hq : ∃ (n : ℕ+), q n} : PNat.find hp ≤ PNat.find hq

theorem PNat.find_le {p : ℕ+ → Prop} [DecidablePred p] {n : ℕ+} {h : ∃ (n : ℕ+), p n} (hn : p n) : PNat.find h ≤ n

theorem PNat.find_comp_succ {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) (h₂ : ∃ (n : ℕ+), p (n + 1)) (h1 : ¬p 1) : PNat.find h = PNat.find h₂ + 1