structure Hex.PermGroup.Search.Trials (α : Type) : Type

A finite sequence of refinement reasons, constructed by index. Even a quadratic family can be searched under a small budget without allocating it.

• size : Nat
• get : Fin self.size → α

def Hex.PermGroup.Search.Trials.empty {α : Type} : Trials α

Equations

• Hex.PermGroup.Search.Trials.empty = { size := 0, get := Fin.elim0 }

def Hex.PermGroup.Search.Trials.singleton {α : Type} (x : α) : Trials α

Equations

• Hex.PermGroup.Search.Trials.singleton x = { size := 1, get := fun (x_1 : Fin 1) => x }

def Hex.PermGroup.Search.Trials.range (n : Nat) : Trials (Fin n)

Equations

• Hex.PermGroup.Search.Trials.range n = { size := n, get := id }

def Hex.PermGroup.Search.Trials.map {α β : Type} (f : α → β) (t : Trials α) : Trials β

Equations

• Hex.PermGroup.Search.Trials.map f t = { size := t.size, get := fun (i : Fin t.size) => f (t.get i) }

def Hex.PermGroup.Search.Trials.append {α : Type} (s t : Trials α) : Trials α

Equations

• s.append t = { size := s.size + t.size, get := fun (i : Fin (s.size + t.size)) => if h : ↑i < s.size then s.get ⟨↑i, h⟩ else t.get ⟨↑i - s.size, ⋯⟩ }

def Hex.PermGroup.Search.Trials.product {α β : Type} (s : Trials α) (t : Trials β) : Trials (α × β)

Row-major candidate order, without constructing a list of pairs.

Equations

• s.product t = { size := s.size * t.size, get := fun (i : Fin (s.size * t.size)) => have ht := ⋯; (s.get ⟨↑i / t.size, ⋯⟩, t.get ⟨↑i % t.size, ⋯⟩) }

inductive Hex.PermGroup.Search.Trials.Result {α : Type} (t : Trials α) (test : α → Bool) (start : Nat) : Type

A scan either finds the first successful test, checks every remaining test, or stops with no completeness claim.

• found {α : Type} {t : Trials α} {test : α → Bool} {start : Nat} (i : Fin t.size) (after : start ≤ ↑i) (valid : test (t.get i) = true) (earlier : ∀ (j : Fin t.size), start ≤ ↑j → ↑j < ↑i → test (t.get j) = false) : t.Result test start
• clear {α : Type} {t : Trials α} {test : α → Bool} {start : Nat} (checked : ∀ (i : Fin t.size), start ≤ ↑i → test (t.get i) = false) : t.Result test start
• incomplete {α : Type} {t : Trials α} {test : α → Bool} {start : Nat} : t.Result test start

structure Hex.PermGroup.Search.Trials.Run {α : Type} (t : Trials α) (test : α → Bool) (start capacity : Nat) : Type

used counts calls of the refinement test. An incomplete scan has spent its entire allowance and still has an unvisited candidate.

• result : t.Result test start
• used : Nat
• bounded : self.used ≤ capacity
• depleted : self.result = Result.incomplete → self.used = capacity
• unfinished : self.result = Result.incomplete → start + self.used < t.size

def Hex.PermGroup.Search.Trials.advance {α : Type} {t : Trials α} {test : α → Bool} {start capacity : Nat} (hs : start < t.size) (h : test (t.get ⟨start, hs⟩) = false) (r : t.Run test (start + 1) capacity) : t.Run test start (capacity + 1)

Equations

• One or more equations did not get rendered due to their size.

def Hex.PermGroup.Search.Trials.scan {α : Type} (t : Trials α) (test : α → Bool) (start capacity : Nat) : t.Run test start capacity

Stop before the next test if the allowance is exhausted. Reaching the end of an empty candidate suffix needs no allowance and proves completeness.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.PermGroup.Search.Trials.scan_complete {α : Type} (t : Trials α) (test : α → Bool) : (t.scan test 0 t.size).result ≠ Result.incomplete

def Hex.PermGroup.Search.Trials.find {α : Type} (t : Trials α) (test : α → Bool) : Option α

Unbounded refinement discovery uses precisely the same scan as its budgeted counterpart, with enough allowance for every candidate.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.PermGroup.Search.Trials.find_checked {α : Type} (t : Trials α) (test : α → Bool) (x : α) (h : t.find test = some x) : test x = true

theorem Hex.PermGroup.Search.Trials.find_none {α : Type} (t : Trials α) (test : α → Bool) : t.find test = none ↔ ∀ (i : Fin t.size), test (t.get i) = false