-- The reduced labelling of a point of the cube: the first coordinate whose
-- label is one, or the dimension when every label is zero
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.FixedPoint.KuhnLabel
import KuhnThrough

-- The indices where a labelling stops: the dimension itself and every
-- coordinate whose label is not zero.
def labelStops (n lab x : Set) : Set := { k ∈ succ(n) | k = n ∨ lab(x)(k) ≠ 0 }

def reduced (n lab x : Set) : Set := leastNatural(labelStops(n, lab, x))

theorem labelStops.nonempty (n : Nat) (lab x : Set)
  shows Nonempty(labelStops(n, lab, x))
proof
  witness n
  apply labelStops.membership.backward
  constructor
  . exact bootstrap.succ.self at n
  . left
    rfl

theorem labelStops.naturals (n : Nat) (lab x : Set)
  shows labelStops(n, lab, x) ⊆ ℕ
proof
  intros k hk
  have parts := labelStops.membership.forward with hk
  have kNat := natural.member at succ(n) with parts.left
  exact nat.omega.forward with kNat

theorem reduced.stops (n : Nat) (lab x : Set)
  shows reduced(n, lab, x) ∈ labelStops(n, lab, x)
proof
  have inhabited := labelStops.nonempty at n, lab, x
  have naturals := labelStops.naturals at n, lab, x
  have same : reduced(n, lab, x) = leastNatural(labelStops(n, lab, x))
    unfold reduced
    rfl
  rw same
  exact leastNatural.member with inhabited, naturals

theorem reduced.bound (n : Nat) (lab x : Set)
  shows reduced(n, lab, x) ∈ succ(n)
proof
  have stops := reduced.stops at n, lab, x
  have parts := labelStops.membership.forward with stops
  exact parts.left

theorem reduced.natural (n : Nat) (lab x : Set)
  shows Nat(reduced(n, lab, x))
proof
  have bound := reduced.bound at n, lab, x
  exact natural.member at succ(n) with bound

theorem reduced.stop (n : Nat) (lab x : Set)
  shows reduced(n, lab, x) = n ∨ lab(x)(reduced(n, lab, x)) ≠ 0
proof
  have stops := reduced.stops at n, lab, x
  have parts := labelStops.membership.forward with stops
  exact parts.right

theorem reduced.least (n : Nat) (lab x k : Set)
  requires hk : k ∈ labelStops(n, lab, x)
  shows reduced(n, lab, x) ≤ k
proof
  have inhabited := labelStops.nonempty at n, lab, x
  have naturals := labelStops.naturals at n, lab, x
  have parts := labelStops.membership.forward with hk
  have kNat := natural.member at succ(n) with parts.left
  have same : reduced(n, lab, x) = leastNatural(labelStops(n, lab, x))
    unfold reduced
    rfl
  rw same
  exact leastNatural.least with inhabited, naturals, hk

-- Below the reduced label every label is zero.
theorem reduced.below (n : Nat) (lab x i : Set)
  requires hi : i ∈ reduced(n, lab, x)
  shows lab(x)(i) = 0
proof
  have reducedNat := reduced.natural at n, lab, x
  have iNat := natural.member at reduced(n, lab, x) with hi
  have iLess := Less.of_membership with hi
  have bound := reduced.bound at n, lab, x
  have reducedLess := Less.of_membership with bound
  by_contra nonzero
  have less : i < succ(n) by arith
  have iIn := membership.of_Less with less
  have stop : i ∈ labelStops(n, lab, x)
    apply labelStops.membership.backward
    constructor
    . exact iIn
    . right
      exact nonzero
  have least := reduced.least with stop
  arith

theorem reduced.unique (n : Nat) (lab x r : Set)
  requires hr : r ∈ succ(n)
  requires zeros : ∀ i ∈ r, lab(x)(i) = 0
  requires stop : r = n ∨ lab(x)(r) ≠ 0
  shows reduced(n, lab, x) = r
proof
  have rNat := natural.member at succ(n) with hr
  have rLess := Less.of_membership with hr
  have inStops : r ∈ labelStops(n, lab, x) := labelStops.membership.backward with ⟨hr, stop⟩
  have least := reduced.least with inStops
  by_contra different
  have strict : reduced(n, lab, x) < r
    by_contra notLess
    have reverse := LessEqual.of_not_Less with notLess
    apply different
    exact LessEqual.antisymmetric with least, reverse
  have inside := membership.of_Less with strict
  have zero := zeros with inside
  have reducedStop := reduced.stop at n, lab, x
  cases reducedStop with top | nonzero
  . rw top at strict
    arith
  . exact nonzero with zero

theorem reduced.ne_of_zero (n : Nat) (lab x j : Set)
  requires hj : j ∈ n
  requires zero : lab(x)(j) = 0
  shows reduced(n, lab, x) ≠ j
proof
  intro equal
  have stop := reduced.stop at n, lab, x
  rw equal at stop
  cases stop with top | nonzero
  . rw top at hj
    exact membership.irreflexive with hj
  . exact nonzero with zero

theorem reduced.le_of_nonzero (n : Nat) (lab x j : Set)
  requires hj : j ∈ n
  requires nonzero : lab(x)(j) ≠ 0
  shows reduced(n, lab, x) ≤ j
proof
  have inStops : j ∈ labelStops(n, lab, x)
    apply labelStops.membership.backward
    constructor
    . exact membership.into_successor with hj
    . right
      exact nonzero
  exact reduced.least with inStops

-- The reduced labelling as a function on a set of points.
defgraph reducedMap (n lab S : Set) (x ∈ S) : succ(n) := reduced(n, lab, x)
requires nNat : Nat(n)
proof
  exact reduced.bound

def labelImage (n lab S : Set) : Set := functionImage(reducedMap(n, lab, S), S, succ(n))

theorem labelImage.membership (n : Nat) (k lab S : Set)
  shows k ∈ labelImage(n, lab, S) ↔ k ∈ succ(n) ∧ ∃ x ∈ S, k = reduced(n, lab, x)
proof
  have same : labelImage(n, lab, S) = functionImage(reducedMap(n, lab, S), S, succ(n))
    unfold labelImage
    rfl
  rw same
  constructor
  . intro hk
    obtain ⟨inSucc, x, hx, shape⟩ := functionImage.membership.forward with hk
    have value := reducedMap.value at n, lab, S, x with *
    constructor
    . exact inSucc
    . witness x
      constructor
      . exact hx
      . rw [shape, value]
        rfl
  . intro hk
    obtain ⟨inSucc, x, hx, shape⟩ := hk
    have value := reducedMap.value at n, lab, S, x with *
    apply functionImage.membership.backward
    constructor
    . exact inSucc
    . witness x
      constructor
      . exact hx
      . rw [shape, value]
        rfl

-- The simplices all of whose vertices carry different reduced labels.
def completeSimplices (p n lab : Set) : Set :=
  { s ∈ kuhnSimplices(p, n) | labelImage(n, lab, s) = succ(n) }