structure Hex.PermGroup.Search.Predicate (n : Nat) : Type

An executable subgroup predicate. Closure is proved for the actual test used at leaves and on the result group's generators.

• test : Perm n → Bool
• id : self.test (Perm.id n) = true
• comp (p q : Perm n) : self.test p = true → self.test q = true → self.test (p.comp q) = true
• inv (p : Perm n) : self.test p = true → self.test p.inv = true

theorem Hex.PermGroup.Search.Predicate.generated {n : Nat} (P : Predicate n) {S : Array (Perm n)} (h : ∀ (i : Fin S.size), P.test S[↑i] = true) {p : Perm n} (hp : Generated S p) : P.test p = true

def Hex.PermGroup.Search.Predicate.subgroup {n : Nat} (H : Group n) : Predicate n

Membership in a second checked group is a subgroup predicate even when neither group is contained in the other.

Equations

• Hex.PermGroup.Search.Predicate.subgroup H = { test := H.contains, id := ⋯, comp := ⋯, inv := ⋯ }

structure Hex.PermGroup.Search.Pruner {n : Nat} (G : Group n) (test : Perm n → Bool) : Type 1

A refinement provides a replayable reason for excluding a whole prefix coset. Its checker must prove impossibility for every completion of that node.

• Reason : Type
• reject : Node G → self.Reason → Bool
• sound (t : Node G) (r : self.Reason) : self.reject t r = true → ∀ (p : Perm n), t.Contains p → test p = false
• trials : Node G → Trials self.Reason

def Hex.PermGroup.Search.Pruner.find {n : Nat} {G : Group n} {test : Perm n → Bool} (C : Pruner G test) (t : Node G) : Option C.Reason

Equations

• C.find t = (C.trials t).find (C.reject t)

theorem Hex.PermGroup.Search.Pruner.checked {n : Nat} {G : Group n} {test : Perm n → Bool} (C : Pruner G test) (t : Node G) (r : C.Reason) (h : C.find t = some r) : C.reject t r = true

theorem Hex.PermGroup.Search.Pruner.find_none {n : Nat} {G : Group n} {test : Perm n → Bool} (C : Pruner G test) (t : Node G) : C.find t = none ↔ ∀ (i : Fin (C.trials t).size), C.reject t ((C.trials t).get i) = false

def Hex.PermGroup.Search.Pruner.findBudgeted {n : Nat} {G : Group n} {test : Perm n → Bool} (C : Pruner G test) (t : Node G) (capacity : Nat) : (C.trials t).Run (C.reject t) 0 capacity

Bounded refinement counts individual rejection tests and distinguishes an unfinished scan from a completed scan that found no rejecting reason.

Equations

• C.findBudgeted t capacity = (C.trials t).scan (C.reject t) 0 capacity

@[reducible, inline]

abbrev Hex.PermGroup.Search.Constraint {n : Nat} (G : Group n) (P : Predicate n) : Type 1

Subgroup search specializes the same pruning interface used by transporter search to a predicate closed under the group operations.

Equations

• Hex.PermGroup.Search.Constraint G P = Hex.PermGroup.Search.Pruner G P.test

def Hex.PermGroup.Search.Constraint.none {n : Nat} (G : Group n) (P : Predicate n) : Constraint G P

The absence of additional refinement still leaves exact leaf checking and the subgroup-containment pruning rule available.

Equations

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

def Hex.PermGroup.Search.Constraint.ofTest {n : Nat} {G : Group n} {P : Predicate n} (reject : Node G → Bool) (sound : ∀ (t : Node G), reject t = true → ∀ (p : Perm n), t.Contains p → P.test p = false) : Constraint G P

A deterministic impossibility test whose complete input is already in the node needs no additional witness data.

Equations

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

def Hex.PermGroup.Search.Constraint.combine {n : Nat} {G : Group n} {P : Predicate n} (C D : Constraint G P) : Constraint G P

Try the first refinement, then the second, preserving which rejection checker must be replayed.

Equations

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

def Hex.PermGroup.Search.Node.covered {n : Nat} {G : Group n} (t : Node G) (K : Group n) : Bool

A whole prefix coset is contained in a checked group when its prefix and all suffix generators belong to that group.

Equations

• t.covered K = (K.contains t.rep.val && decide (∀ (i : Fin t.suffix.generators.size), K.contains t.suffix.generators[↑i] = true))

theorem Hex.PermGroup.Search.Node.covered_sound {n : Nat} {G : Group n} (t : Node G) (K : Group n) (h : t.covered K = true) {p : Perm n} (hp : t.Contains p) : Generated K.generators p

theorem Hex.PermGroup.Search.Node.covered_mono {n : Nat} {G : Group n} (t : Node G) {K L : Group n} (hkl : K.IsSubgroup L) (h : t.covered K = true) : t.covered L = true