inductive Hex.PermGroup.Search.Decision {n : Nat} {G : Group n} {test : Perm n → Bool} (C : Pruner G test) (t : Node G) : Type

A node either supplies a satisfying completion or a checked account of why every completion fails. There is no exhausted-search constructor.

• found {n : Nat} {G : Group n} {test : Perm n → Bool} {C : Pruner G test} {t : Node G} (p : Element G) (inside : t.Contains p.val) (satisfies : test p.val = true) : Decision C t
• absent {n : Nat} {G : Group n} {test : Perm n → Bool} {C : Pruner G test} {t : Node G} (certificate : Certificate C.Reason) (checked : checkFailure C t certificate = true) : Decision C t

inductive Hex.PermGroup.Search.First.Children {n : Nat} {G : Group n} {test : Perm n → Bool} (C : Pruner G test) {m : Nat} (nodes : Fin m → Node G) (k : Nat) (hk : k ≤ m) : Type

The first k children either yielded a witness, or all have failure certificates. A witness prevents visiting any later children.

• found {n : Nat} {G : Group n} {test : Perm n → Bool} {C : Pruner G test} {m : Nat} {nodes : Fin m → Node G} {k : Nat} {hk : k ≤ m} (i : Fin k) (p : Element G) (inside : (nodes ⟨↑i, ⋯⟩).Contains p.val) (satisfies : test p.val = true) : Children C nodes k hk
• absent {n : Nat} {G : Group n} {test : Perm n → Bool} {C : Pruner G test} {m : Nat} {nodes : Fin m → Node G} {k : Nat} {hk : k ≤ m} (certificates : Vector (Certificate C.Reason) k) (checked : ∀ (i : Fin k), checkFailure C (nodes ⟨↑i, ⋯⟩) certificates[↑i] = true) : Children C nodes k hk

def Hex.PermGroup.Search.First.collect {n : Nat} {G : Group n} {test : Perm n → Bool} (C : Pruner G test) {m : Nat} (nodes : Fin m → Node G) (visit : (i : Fin m) → Decision C (nodes i)) (k : Nat) (hk : k ≤ m) : Children C nodes k hk

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.Search.First.collect C nodes visit 0 hk_2 = Hex.PermGroup.Search.First.Children.absent #v[] ⋯

@[irreducible]

def Hex.PermGroup.Search.First.visit {n : Nat} {G : Group n} {test : Perm n → Bool} (C : Pruner G test) (t : Node G) : Decision C t

Follow the checked chain and refine assigned images before expanding a node. A successful leaf ends the search immediately.

Equations

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

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

The original-generator program and defining equation are independently checkable data for a positive transporter answer.

• value : Perm n
• word : Program
• checked : checkWitness G test self.value self.word = true

def Hex.PermGroup.Search.Witness.element {n : Nat} {G : Group n} {test : Perm n → Bool} (w : Witness G test) : Element G

Equations

• w.element = ⟨w.value, ⋯⟩

theorem Hex.PermGroup.Search.Witness.satisfies {n : Nat} {G : Group n} {test : Perm n → Bool} (w : Witness G test) : test w.value = true

def Hex.PermGroup.Search.Witness.ofElement {n : Nat} {G : Group n} {test : Perm n → Bool} (p : Element G) (hp : test p.val = true) : Witness G test

Equations

• Hex.PermGroup.Search.Witness.ofElement p hp = { value := p.val, word := (G.word? p.val).get ⋯, checked := ⋯ }

inductive Hex.PermGroup.Search.Answer {n : Nat} {G : Group n} {test : Perm n → Bool} (C : Pruner G test) : Type

• found {n : Nat} {G : Group n} {test : Perm n → Bool} {C : Pruner G test} (witness : Witness G test) : Answer C
• absent {n : Nat} {G : Group n} {test : Perm n → Bool} {C : Pruner G test} (certificate : Certificate C.Reason) (checked : checkFailure C (Node.root G) certificate = true) : Answer C

def Hex.PermGroup.Search.Answer.element? {n : Nat} {G : Group n} {test : Perm n → Bool} (C : Pruner G test) : Answer C → Option (Element G)

Equations

• Hex.PermGroup.Search.Answer.element? C (Hex.PermGroup.Search.Answer.found w) = some w.element
• Hex.PermGroup.Search.Answer.element? C (Hex.PermGroup.Search.Answer.absent certificate checked) = none

theorem Hex.PermGroup.Search.Answer.some_spec {n : Nat} {G : Group n} {test : Perm n → Bool} (C : Pruner G test) (a : Answer C) (p : Element G) (h : element? C a = some p) : test p.val = true

theorem Hex.PermGroup.Search.Answer.none_spec {n : Nat} {G : Group n} {test : Perm n → Bool} (C : Pruner G test) (a : Answer C) : element? C a = none ↔ ¬∃ (p : Element G), test p.val = true

def Hex.PermGroup.Search.first {n : Nat} {G : Group n} {test : Perm n → Bool} (C : Pruner G test) : Answer C

Exact existence search carries either a checked positive word or a complete negative certificate.

Equations

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