Reference · Finite types, distributions and Markov chains

rainbow.math.finite.index

Finite types, distributions and Markov chainssrc/rainbow/math/finite/index.clj6 definitions, 13 theorems

Axiom-free bounded indices as a structural finite family. `finite/Index 0` is a recursive-only empty data type (it has no base constructor) and `finite/Index (n+1)` is `Option (finite/Index n)`. Thus the last index is `none` and weakening an earlier index is `some`. Unlike a proof-carrying subtype of Nat, this representation needs no proof-irrelevance axiom for equality and is suitable for executable finite tables. This first layer supplies the family, its constructors, and the complete successor case split. Enumeration and certified equality build on that structural split. Native, kernel-checked, and axiom-free on D63.

finite/Index :
  (x₁ : ℕ)
  → Type

finite/index-last :
  (upper : ℕ)
  → finite/Index (data/succ upper)

finite/index-weaken :
  (upper : ℕ) (source : finite/Index upper)
  → finite/Index (data/succ upper)

finite/index-enumeration :
  (upper : ℕ)
  → List (finite/Index upper)

finite/index-decide-equality :
  (upper : ℕ) (x₁ x₂ : finite/Index upper)
  → data/Bool

finite/index-finset :
  (upper : ℕ)
  → Finset (finite/Index upper)

finite/index-weaken-injective :
  (upper : ℕ) (left right : finite/Index upper)
  (same : finite/index-weaken upper left = finite/index-weaken upper right)
  → left = right

finite/index-decide-equality-reflexive-true :
  (upper : ℕ) (value : finite/Index upper)
  → finite/index-decide-equality upper value value = data/true

finite/index-equality-implies-decide-equality-true :
  (upper : ℕ) (left right : finite/Index upper)
  (same : left = right)
  → finite/index-decide-equality upper left right = data/true

finite/index-decide-equality-true-sound :
  (upper : ℕ) (left right : finite/Index upper)
  (accepted : finite/index-decide-equality upper left right = data/true)
  → left = right

finite/index-last-different-from-weaken :
  (upper : ℕ) (source : finite/Index upper)
  (h₁ : finite/index-last upper = finite/index-weaken upper source)
  → proposition/falsity

finite/index-weaken-membership-reflects :
  (upper : ℕ) (items : List (finite/Index upper)) (selected : finite/Index upper)
  (mapped-member : list/membership (finite/Index (data/succ upper)) (map) (finite/index-weaken upper selected))
  → list/membership (finite/Index upper) items selected
  where map := list/map (finite/Index upper) (finite/Index (data/succ upper)) (fun source => finite/index-weaken upper source) items

finite/index-last-not-member-map-weaken :
  (upper : ℕ) (items : List (finite/Index upper))
  (x₁ : list/membership (finite/Index (data/succ upper)) (map) (finite/index-last upper))
  → proposition/falsity
  where map := list/map (finite/Index upper) (finite/Index (data/succ upper)) (fun source => finite/index-weaken upper source) items

finite/index-map-weaken-no-duplicates :
  (upper : ℕ) (items : List (finite/Index upper))
  (distinct : list/no-duplicates (finite/Index upper) items)
  → list/no-duplicates (finite/Index (data/succ upper)) (map)
  where map := list/map (finite/Index upper) (finite/Index (data/succ upper)) (fun source => finite/index-weaken upper source) items

finite/index-enumeration-no-duplicates :
  (upper : ℕ)
  → list/no-duplicates (finite/Index upper) (finite/index-enumeration upper)

finite/index-successor-cases :
  (upper : ℕ) (source : finite/Index (data/succ upper))
  → proposition/disjunction (source = finite/index-last upper) (existence)
  where existence := proposition/existence (finite/Index upper) (fun prior => source = finite/index-weaken upper prior)

finite/index-enumeration-covers :
  (upper : ℕ) (source : finite/Index upper)
  → list/membership (finite/Index upper) (finite/index-enumeration upper) source

finite/certified-index-equality :
  (upper : ℕ)
  → finite/certified-equality-decision (finite/Index upper) (fun left => fun right => finite/index-decide-equality upper left right)

finite/index-exhaustive-carrier :
  (upper : ℕ)
  → finite/certified-exhaustive-carrier (finite/Index upper) (finite/index-finset upper) (fun left => fun right => finite/index-decide-equality upper left right)