Reference · Natural numbers

rainbow.math.nat.extremal-index

Natural numberssrc/rainbow/math/nat/extremal_index.clj0 definitions, 3 theorems

LEAST AND GREATEST WITNESSES of a decidable predicate on 0..k, constructively (for the Floyd-Warshall invariant: the first and last intermediate visit of the new pivot). nat/bounded-search-decidable : (forall s, Q s \/ not Q s) -> (exists s <= k, Q s) \/ (forall s <= k, not Q s) nat/least-witness : decidable Q -> (exists s <= k, Q s) -> exists s, s <= k /\ Q s /\ forall s' < s, not Q s' nat/greatest-witness : decidable Q -> (exists s <= k, Q s) -> exists s, s <= k /\ Q s /\ forall s', s < s' -> s' <= k -> not Q s' All three are by induction on k.

Depends onmath.nat.pigeonhole

nat/bounded-search-decidable :
  (Q : ℕ → Prop)
  (hd : ∀ (s : ℕ), proposition/disjunction (Q s) (Q s → proposition/falsity)) (k : ℕ)
  → proposition/disjunction (existence) (∀ (s : ℕ), ∀ (hs : s ≤ k), Q s → proposition/falsity)
  where existence := proposition/existence ℕ (fun s => proposition/conjunction (s ≤ k) (Q s))

nat/least-witness :
  (Q : ℕ → Prop)
  (hd : ∀ (s : ℕ), proposition/disjunction (Q s) (Q s → proposition/falsity)) (k : ℕ)
  (x₁ : proposition/existence ℕ (fun s => proposition/conjunction (s ≤ k) (Q s)))
  → proposition/existence ℕ (fun s => proposition/conjunction (s ≤ k) (proposition/conjunction (Q s) (∀ (s2 : ℕ), ∀ (hs2 : nat/strict-below s2 s), Q s2 → proposition/falsity)))

nat/greatest-witness :
  (Q : ℕ → Prop)
  (hd : ∀ (s : ℕ), proposition/disjunction (Q s) (Q s → proposition/falsity)) (k : ℕ)
  (x₁ : proposition/existence ℕ (fun s => proposition/conjunction (s ≤ k) (Q s)))
  → proposition/existence ℕ (fun s => proposition/conjunction (s ≤ k) (proposition/conjunction (Q s) (∀ (s2 : ℕ), ∀ (hs2 : nat/strict-below s s2), ∀ (hk2 : s2 ≤ k), Q s2 → proposition/falsity)))