Bounded string constraints: finite-search specification

TheoremKeys of the association list built from an assignment#✓fully proved

The keys of the association list built from an assignment are the variables themselves.

theorem map_fst_map_pair {α : Type*} {V : Type*} {vs : List V} {σ : V → List α} :
    (vs.map fun i => (i, σ i)).map Prod.fst = vs

Used by 1

Used bySoundness and completeness of the bounded-search specification

20 fully proved

Words

DefinitionWords of a given length over a finite alphabet#✓fully proved

All words of length exactly n over a finite alphabet, each occurring once: each step extends only the words of the previous length, never the whole wordsUpTo enumeration, so no word is duplicated.

noncomputable def wordsOfLength : ℕ → List (List α)
  | 0 => [[]]
  | n + 1 =>
    (wordsOfLength n).flatMap (fun w =>
      (Finset.univ : Finset α).toList.map (fun a => w ++ [a]))

Used by 6

Used byMembership in the exact-length word enumeration · Membership in the bounded-length word enumeration · Empty word is in every bounded enumeration · Size of the exact-length word enumeration · Words of length at most \(B\) over a finite alphabet · Size of the bounded-length word enumeration

TheoremMembership in the exact-length word enumeration#✓fully proved

Membership in the exact-length enumeration is exactly the length equality.

theorem mem_wordsOfLength {w : List α} {n : ℕ} :
    w ∈ wordsOfLength (α := α) n ↔ w.length = n

Uses 1 · Used by 1

Statement usesWords of a given length over a finite alphabet

Used byMembership in the bounded-length word enumeration

TheoremSize of the exact-length word enumeration#✓fully proved

Counting the exact-length enumeration: |Σ| ^ n words.

theorem wordsOfLength_length (n : ℕ) :
    (wordsOfLength (α := α) n).length = (Fintype.card α) ^ n

Uses 1 · Used by 1

Statement usesWords of a given length over a finite alphabet

Used bySize of the bounded-length word enumeration

DefinitionNumber of words of length at most \(B\)#✓fully proved

The number of words of length at most B: ∑_{n ≤ B} |Σ| ^ n.

noncomputable def wordsUpToCount (B : ℕ) : ℕ :=
  ((List.range (B + 1)).map fun n => (Fintype.card α) ^ n).sum

Used by 2

Used bySize of the bounded assignment enumeration · Size of the bounded-length word enumeration

DefinitionWords of length at most \(B\) over a finite alphabet#✓fully proved

All words of length at most B over a finite alphabet, each occurring once: the concatenation of the exact-length layers 0, …, B.

noncomputable def wordsUpTo (B : ℕ) : List (List α) :=
  (List.range (B + 1)).flatMap (fun n => wordsOfLength (α := α) n)

Uses 1 · Used by 6

Statement usesWords of a given length over a finite alphabet

Used byEnumeration of bounded assignments as association lists · Size of the bounded assignment enumeration · Membership in the bounded assignment enumeration · Membership in the bounded-length word enumeration · Empty word is in every bounded enumeration · Size of the bounded-length word enumeration

TheoremEmpty word is in every bounded enumeration#✓fully proved

The empty word is enumerated at every bound.

theorem nil_mem_wordsUpTo (B : ℕ) : [] ∈ wordsUpTo (α := α) B

Uses 2

Statement usesWords of length at most \(B\) over a finite alphabet

Proof usesWords of a given length over a finite alphabet

TheoremMembership in the bounded-length word enumeration#✓fully proved

Membership in the enumeration is exactly the length bound.

theorem mem_wordsUpTo {w : List α} {B : ℕ} :
    w ∈ wordsUpTo (α := α) B ↔ w.length ≤ B

Uses 3 · Used by 1

Statement usesWords of length at most \(B\) over a finite alphabet

Proof usesMembership in the exact-length word enumeration · Words of a given length over a finite alphabet

Used byMembership in the bounded assignment enumeration

TheoremSum of a constant over a list#✓fully proved

Summing a constant over a list.

theorem sum_map_const {β : Type*} {l : List β} {c : ℕ} :
    (l.map (fun _ => c)).sum = l.length * c

Used by 1

Used bySize of the bounded assignment enumeration

TheoremSize of the bounded-length word enumeration#✓fully proved

Counting the enumeration: ∑_{n ≤ B} |Σ| ^ n words, the number of distinct words of length at most B.

theorem wordsUpTo_length (B : ℕ) :
    (wordsUpTo (α := α) B).length = wordsUpToCount (α := α) B

Uses 4 · Used by 1

Statement usesWords of length at most \(B\) over a finite alphabet · Number of words of length at most \(B\)

Proof usesWords of a given length over a finite alphabet · Size of the exact-length word enumeration

Used bySize of the bounded assignment enumeration

Lookup

DefinitionAssociation-list lookup defaulting to the empty word#✓fully proved

Lookup in an association list; unbound variables read as [].

def getVal : List (V × List α) → V → List α
  | [], _ => []
  | (i, w) :: l, j => if j = i then w else getVal l j

Used by 6

Used byEnumerated lists over distinct variables are recovered from lookups · Enumerated lists over distinct variables give distinct assignments · Bounded-search satisfiability specification · Soundness and completeness of the bounded-search specification · Lookup inherits the length bound on values · Lookup recovers the assignment from its association list

TheoremLookup inherits the length bound on values#✓fully proved

A lookup returns one of the values in the list, so it inherits the length bound on values.

theorem getVal_length_le {l : List (V × List α)} {i : V} {B : ℕ}
    (hvalues : ∀ w ∈ l.map Prod.snd, w.length ≤ B) (hkeys : i ∈ l.map Prod.fst) :
    (getVal l i).length ≤ B

Uses 1 · Used by 1

Statement usesAssociation-list lookup defaulting to the empty word

Used bySoundness and completeness of the bounded-search specification

TheoremLookup recovers the assignment from its association list#✓fully proved

Lookup in the association list built from an assignment returns the assignment.

theorem getVal_map {σ : V → List α} {vs : List V} {i : V} (hi : i ∈ vs) :
    getVal (vs.map fun j => (j, σ j)) i = σ i

Uses 1 · Used by 1

Statement usesAssociation-list lookup defaulting to the empty word

Used bySoundness and completeness of the bounded-search specification

Assignments

DefinitionEnumeration of bounded assignments as association lists#✓fully proved

All assignments of the variables in vs to words of length at most B, as association lists, each occurring once (as in wordsUpTo).

noncomputable def assignLists : List V → ℕ → List (List (V × List α))
  | [], _ => [[]]
  | i :: vs, B => (assignLists vs B).flatMap
      (fun l => (wordsUpTo B).map (fun w => (i, w) :: l))

Uses 1 · Used by 6

Statement usesWords of length at most \(B\) over a finite alphabet

Used byEnumerated lists over distinct variables are recovered from lookups · Enumerated lists over distinct variables give distinct assignments · Size of the bounded assignment enumeration · Bounded-search satisfiability specification · Soundness and completeness of the bounded-search specification · Membership in the bounded assignment enumeration

TheoremMembership in the bounded assignment enumeration#✓fully proved

Membership in the assignment enumeration: the keys are exactly vs and every value has length at most B.

theorem mem_assignLists {vs : List V} {l : List (V × List α)} {B : ℕ} :
    l ∈ assignLists vs B ↔
      l.map Prod.fst = vs ∧ ∀ w ∈ l.map Prod.snd, w.length ≤ B

Uses 3 · Used by 2

Statement usesEnumeration of bounded assignments as association lists

Proof usesMembership in the bounded-length word enumeration · Words of length at most \(B\) over a finite alphabet

Used byEnumerated lists over distinct variables are recovered from lookups · Soundness and completeness of the bounded-search specification

TheoremSize of the bounded assignment enumeration#✓fully proved

Counting the assignment enumeration: the total (worst-case) size of the candidate search space is (wordsUpToCount B) ^ |vs|. This counts enumerated association lists; see the cost model in the module header for when it coincides with the number of distinct assignments.

theorem assignLists_length (vs : List V) (B : ℕ) :
    (assignLists (α := α) vs B).length
      = (wordsUpToCount (α := α) B) ^ vs.length

Uses 5

Statement usesEnumeration of bounded assignments as association lists · Number of words of length at most \(B\)

Proof usesSum of a constant over a list · Words of length at most \(B\) over a finite alphabet · Size of the bounded-length word enumeration

Uniqueness

TheoremEnumerated lists over distinct variables are recovered from lookups#✓fully proved

Under vs.Nodup, an enumerated association list is recovered from its lookup function: there is no duplicate key for getVal to shadow, so the list is exactly the association list built from its own lookups.

theorem assignLists_eq_map_getVal {vs : List V} {l : List (V × List α)} {B : ℕ}
    (hl : l ∈ assignLists vs B) (hvs : vs.Nodup) :
    l = vs.map (fun i => (i, getVal l i))

Uses 3 · Used by 1

Statement usesEnumeration of bounded assignments as association lists · Association-list lookup defaulting to the empty word

Proof usesMembership in the bounded assignment enumeration

Used byEnumerated lists over distinct variables give distinct assignments

TheoremEnumerated lists over distinct variables give distinct assignments#✓fully proved

Under vs.Nodup, distinct enumerated association lists denote distinct assignments: if two enumerated lists agree as lookup functions on vs, they are the same list. Without Nodup this fails, since a duplicate key lets a later entry be shadowed by an earlier one.

theorem assignLists_getVal_injective {vs : List V} {B : ℕ} (hvs : vs.Nodup)
    {l₁ l₂ : List (V × List α)} (h₁ : l₁ ∈ assignLists vs B)
    (h₂ : l₂ ∈ assignLists vs B)
    (h : ∀ i ∈ vs, getVal l₁ i = getVal l₂ i) : l₁ = l₂

Uses 3

Statement usesEnumeration of bounded assignments as association lists · Association-list lookup defaulting to the empty word

Proof usesEnumerated lists over distinct variables are recovered from lookups

Specification

DefinitionBounded-search satisfiability specification#✓fully proved

The bounded-search specification: enumerate bounded assignments and check φ on each one. This is a classical specification, not an executable decision procedure: assignLists is noncomputable, so this Boolean cannot be evaluated by decide.

noncomputable def boundedSatSpec (vs : List V) (φ : Formula α V) (B : ℕ) : Bool :=
  (assignLists vs B).any (fun l => satB (getVal l) φ)

Uses 4 · Used by 2

Statement usesString formulas · Enumeration of bounded assignments as association lists · Association-list lookup defaulting to the empty word · Boolean checker for formula satisfaction

Used bySoundness and completeness of the bounded-search specification · SAT iff the bounded-search specification holds of the encoding

TheoremSoundness and completeness of the bounded-search specification#✓fully proved

Soundness and completeness of the bounded-search specification: it reports true exactly when φ has a solution whose values on vs have length at most B. The hypothesis is that vs covers the variables of φ.

theorem boundedSatSpec_iff (vs : List V) (φ : Formula α V) (B : ℕ)
    (hvars : ∀ i ∈ varsOfFormula φ, i ∈ vs) :
    boundedSatSpec vs φ B = true ↔
      ∃ σ : V → List α, (∀ i ∈ vs, (σ i).length ≤ B) ∧ Sat σ φ

Uses 13 · Used by 1

Statement usesString formulas · Satisfaction of a string formula · Bounded-search satisfiability specification · Variables occurring in a string formula

Proof usesEnumeration of bounded assignments as association lists · Association-list lookup defaulting to the empty word · Lookup inherits the length bound on values · Lookup recovers the assignment from its association list · Keys of the association list built from an assignment · Membership in the bounded assignment enumeration · Boolean checker for formula satisfaction · Correctness of the Boolean formula checker · Formula satisfaction depends only on its variables

Used bySAT iff the bounded-search specification holds of the encoding

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.