Reference · Natural numbers

rainbow.math.nat.pigeonhole

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

THE PIGEONHOLE PRINCIPLE ON NAT, constructively. n + 1 values below n repeat one: nat/pigeonhole : forall n f, (forall t <= n, f t < n) -> exists a b, a < b /\ b <= n /\ f a = f b with its supports: nat/trichotomy : a < b \/ a = b \/ b < a nat/bounded-search : (exists t <= n, f t = c) \/ (forall t <= n, f t = c -> False) Pigeonhole is by induction on n. Let c = f(n+1). If some t <= n has f t = c, the pair is (t, n+1). Otherwise squeeze the top value into c: g t = if f t < n then f t else c. Then every g t < n: when f t is not below n it is n, and c is not n because otherwise f t = n = c. The induction hypothesis gives a < b <= n with g a = g b. In each of the four cases of the two decisions, f a = f b follows directly or the mixed case would make f a or f b equal to c. Consumer: the Bellman-Ford cycle-removal lemma (a walk of >= n arcs over n nodes repeats a node).

Depends onmath.nat.divmodmath.rational.signed.decide-completeness

nat/trichotomy :
  (a b : ℕ)
  → proposition/disjunction (nat/strict-below a b) (disjunction)
  where disjunction := proposition/disjunction (a = b) (nat/strict-below b a)

nat/bounded-search :
  (f : ℕ → ℕ) (c n : ℕ)
  → proposition/disjunction (existence) (∀ (t : ℕ), ∀ (ht : t ≤ n), f t = c → proposition/falsity)
  where existence := proposition/existence ℕ (fun t => proposition/conjunction (t ≤ n) (f t = c))

nat/pigeonhole :
  (n : ℕ) (f : ℕ → ℕ) (hf : ∀ (t : ℕ), ∀ (ht : t ≤ n), nat/strict-below (f t) n)
  → proposition/existence ℕ (fun a => proposition/existence ℕ (fun b => proposition/conjunction (nat/strict-below a b) (proposition/conjunction (b ≤ n) (f a = f b))))