Ordinary word equations

DefinitionSubstitution of words for variables in a word#✓fully proved

Substitute words for variables in a word over constants and variables.

def evalWord (σ : V → List α) (w : List (α ⊕ V)) : List α :=
  w.flatMap (Sum.elim (fun a => [a]) σ)

Used by 13

Used byFixed-length bit-blasting is equisatisfiable · Decidability of Boolean-word pattern matching · Target length bounds the pattern-matching search · Word evaluation depends only on occurring variables · Normalization does not change the evaluated word · Word embedding preserves substitution semantics · Executable satisfaction test for ground word equations · Ground test agrees with satisfaction under any substitution · Occurring variable's image is no longer than the evaluated word · Normalized images are bounded by the evaluation length · Bounding variable images by the target loses no pattern matches · Formula embedding of word equations preserves satisfaction · Solution of a word equation

DefinitionEmbedding of ordinary words into string terms#✓fully proved

Embed an ordinary word in the larger string-constraint term language.

def wordTerm : List (α ⊕ V) → Term α V
  | [] => .const []
  | Sum.inl a :: w => .append (.const [a]) (wordTerm w)
  | Sum.inr i :: w => .append (.var i) (wordTerm w)

Uses 1 · Used by 3

Statement usesString term over variables

Used byWord embedding preserves substitution semantics · Formula embedding of word equations preserves satisfaction · Word equation as a string-constraint formula

TheoremWord embedding preserves substitution semantics#✓fully proved

The embedding preserves substitution semantics.

@[simp] theorem eval_wordTerm (σ : V → List α) (w : List (α ⊕ V)) :
    eval σ (wordTerm w) = evalWord σ w

Uses 3 · Used by 1

Statement usesEvaluation of a string term under an assignment · Substitution of words for variables in a word · Embedding of ordinary words into string terms

Used byFormula embedding of word equations preserves satisfaction

StructureOrdinary word equation#✓fully proved

An ordinary word equation, with no morphisms or language-membership atoms.

structure WordEq (α V : Type*) where
  lhs : List (α ⊕ V)
  rhs : List (α ⊕ V)

Used by 21

Used byCNF encoding of a word-equation system at fixed lengths · Exact clause count of the CNF encoding · CNF encoding uses clauses of width at most two · Bounded word-equation solver via DPLL · SAT backend agrees with the bounded formula semantics · Soundness and completeness of the bounded word-equation solver · Fixed-length bit-blasting is equisatisfiable · Decision procedure for bounded Boolean word equations · Fixed-length word-equation solver via DPLL · Correctness of the fixed-length SAT-backed solver · Pattern-matching decision against a concrete target · Target length bounds the pattern-matching search · Satisfiability as acceptance by some bounded SAT search · Executable satisfaction test for ground word equations · Ground test agrees with satisfaction under any substitution · Ground test decides solvability of ground word equations · Formula embedding of word equations preserves satisfaction · Satisfiability of a single word equation at a finite length bound · Solution of a word equation · Word equation as a string-constraint formula · Solvability of word equation systems at a finite length bound

DefinitionSolution of a word equation#✓fully proved

A substitution solves a word equation when the substituted sides agree.

def WordEq.Satisfies (σ : V → List α) (e : WordEq α V) : Prop :=
  evalWord σ e.lhs = evalWord σ e.rhs

Uses 2 · Used by 12

Statement usesOrdinary word equation · Substitution of words for variables in a word

Used bySAT backend agrees with the bounded formula semantics · Soundness and completeness of the bounded word-equation solver · Fixed-length bit-blasting is equisatisfiable · Decision procedure for bounded Boolean word equations · Correctness of the fixed-length SAT-backed solver · Target length bounds the pattern-matching search · Satisfiability as acceptance by some bounded SAT search · Ground test agrees with satisfaction under any substitution · Ground test decides solvability of ground word equations · Formula embedding of word equations preserves satisfaction · Satisfiability of a single word equation at a finite length bound · Solvability of word equation systems at a finite length bound

DefinitionWord equation as a string-constraint formula#✓fully proved

View an ordinary word equation as a string-constraint formula.

def WordEq.toFormula (e : WordEq α V) : Formula α V :=
  .atom (.eq (wordTerm e.lhs) (wordTerm e.rhs))

Uses 5 · Used by 2

Statement usesString constraint atom · String formulas · String term over variables · Ordinary word equation · Embedding of ordinary words into string terms

Used bySAT backend agrees with the bounded formula semantics · Formula embedding of word equations preserves satisfaction

TheoremFormula embedding of word equations preserves satisfaction#✓fully proved

The formula embedding preserves satisfaction.

@[simp] theorem WordEq.sat_toFormula (σ : V → List α) (e : WordEq α V) :
    Sat σ e.toFormula ↔ e.Satisfies σ

Uses 12 · Used by 1

Statement usesSatisfaction of a string formula · Ordinary word equation · Solution of a word equation · Word equation as a string-constraint formula

Proof usesString constraint atom · String formulas · Satisfaction of a string atom · String term over variables · Evaluation of a string term under an assignment · Substitution of words for variables in a word · Word embedding preserves substitution semantics · Embedding of ordinary words into string terms

Used bySAT backend agrees with the bounded formula semantics

TheoremWord evaluation depends only on occurring variables#✓fully proved

Evaluation depends only on variables that occur in the word.

theorem evalWord_eq_of_agree_on_vars {σ τ : V → List α} {w : List (α ⊕ V)}
    (h : ∀ i, Sum.inr i ∈ w → σ i = τ i) : evalWord σ w = evalWord τ w

Uses 1 · Used by 1

Statement usesSubstitution of words for variables in a word

Used byNormalization does not change the evaluated word

TheoremOccurring variable's image is no longer than the evaluated word#✓fully proved

Each occurring variable contributes a contiguous block, so its length cannot exceed the length of the evaluated word, even when substitutions may be empty.

theorem length_le_evalWord_of_mem (σ : V → List α) {w : List (α ⊕ V)} {i : V}
    (hi : Sum.inr i ∈ w) : (σ i).length ≤ (evalWord σ w).length

Uses 1 · Used by 1

Statement usesSubstitution of words for variables in a word

Used byNormalized images are bounded by the evaluation length

DefinitionWord substitution normalized by emptying unused images#✓fully proved

Retain the images of occurring variables and replace every unused image by []. Only equality of variables, not equality of alphabet symbols, is needed.

def normalizeWordSubst [DecidableEq V] (σ : V → List α) (w : List (α ⊕ V)) :
    V → List α :=
  fun i => if i ∈ w.filterMap (Sum.elim (fun _ => none) some) then σ i else []

Used by 5

Used byNormalization does not change the evaluated word · Normalized images are bounded by the evaluation length · Normalization keeps images of occurring variables · Normalization empties images of absent variables · Bounding variable images by the target loses no pattern matches

TheoremNormalization keeps images of occurring variables#✓fully proved

Normalization preserves the image of every occurring variable.

theorem normalizeWordSubst_of_mem [DecidableEq V] (σ : V → List α)
    {w : List (α ⊕ V)} {i : V} (hi : Sum.inr i ∈ w) :
    normalizeWordSubst σ w i = σ i

Uses 1 · Used by 1

Statement usesWord substitution normalized by emptying unused images

Used byNormalization does not change the evaluated word

TheoremNormalization empties images of absent variables#✓fully proved

Every variable absent from the word has empty normalized image.

theorem normalizeWordSubst_of_not_mem [DecidableEq V] (σ : V → List α)
    {w : List (α ⊕ V)} {i : V} (hi : Sum.inr i ∉ w) :
    normalizeWordSubst σ w i = []

Uses 1

Statement usesWord substitution normalized by emptying unused images

TheoremNormalization does not change the evaluated word#✓fully proved

Removing unused images does not change the evaluated word.

@[simp] theorem evalWord_normalizeWordSubst [DecidableEq V] (σ : V → List α)
    (w : List (α ⊕ V)) : evalWord (normalizeWordSubst σ w) w = evalWord σ w

Uses 4 · Used by 1

Statement usesSubstitution of words for variables in a word · Word substitution normalized by emptying unused images

Proof usesWord evaluation depends only on occurring variables · Normalization keeps images of occurring variables

Used byBounding variable images by the target loses no pattern matches

TheoremNormalized images are bounded by the evaluation length#✓fully proved

After normalization, every variable image, including unused ones, is bounded by the length of the original evaluation.

theorem length_normalizeWordSubst_le [DecidableEq V] (σ : V → List α)
    (w : List (α ⊕ V)) (i : V) :
    (normalizeWordSubst σ w i).length ≤ (evalWord σ w).length

Uses 3 · Used by 1

Statement usesSubstitution of words for variables in a word · Word substitution normalized by emptying unused images

Proof usesOccurring variable's image is no longer than the evaluated word

Used byBounding variable images by the target loses no pattern matches

TheoremBounding variable images by the target loses no pattern matches#✓fully proved

Matching a pattern against a fixed target loses no solutions by bounding ALL variable images by the target length. Unused variables are normalized to []; an arbitrary unnormalized solution need not obey this bound.

theorem patternMatch_iff_bounded {n : ℕ} (w : List (α ⊕ Fin n)) (target : List α) :
    (∃ σ : Fin n → List α, evalWord σ w = target) ↔
      ∃ σ : Fin n → List α, (∀ i, (σ i).length ≤ target.length) ∧
        evalWord σ w = target

Uses 4 · Used by 1

Statement usesSubstitution of words for variables in a word

Proof usesNormalization does not change the evaluated word · Normalized images are bounded by the evaluation length · Word substitution normalized by emptying unused images

Used byTarget length bounds the pattern-matching search

DefinitionExecutable satisfaction test for ground word equations#✓fully proved

Executable satisfaction test for a ground equation. Since the variable type is Empty, no substitution search is required.

def WordEq.groundSatB [DecidableEq α] (e : WordEq α Empty) : Bool :=
  decide (evalWord Empty.elim e.lhs = evalWord Empty.elim e.rhs)

Uses 2 · Used by 2

Statement usesOrdinary word equation · Substitution of words for variables in a word

Used byGround test agrees with satisfaction under any substitution · Ground test decides solvability of ground word equations

TheoremGround test agrees with satisfaction under any substitution#✓fully proved

The ground test agrees with satisfaction under any substitution.

theorem WordEq.groundSatB_eq_true_iff [DecidableEq α] (e : WordEq α Empty)
    (σ : Empty → List α) : e.groundSatB = true ↔ e.Satisfies σ

Uses 4 · Used by 1

Statement usesOrdinary word equation · Solution of a word equation · Executable satisfaction test for ground word equations

Proof usesSubstitution of words for variables in a word

Used byGround test decides solvability of ground word equations

TheoremGround test decides solvability of ground word equations#✓fully proved

The executable ground test decides existence of a solution, not just satisfaction of one guessed substitution.

theorem WordEq.groundSatB_iff [DecidableEq α] (e : WordEq α Empty) :
    e.groundSatB = true ↔ ∃ σ : Empty → List α, e.Satisfies σ

Uses 4

Statement usesOrdinary word equation · Solution of a word equation · Executable satisfaction test for ground word equations

Proof usesGround test agrees with satisfaction under any substitution

TheoremSolvability of word equation systems at a finite length bound#✓fully proved

A system over finitely many variables has a solution iff one substitution solves every equation at some finite global length bound. The witness bound is obtained from the solution; this supplies no terminating general UNSAT test.

theorem wordSystem_satisfiable_iff_exists_bound {n : ℕ} (es : List (WordEq α (Fin n))) :
    (∃ σ : Fin n → List α, ∀ e ∈ es, e.Satisfies σ) ↔
      ∃ B : ℕ, ∃ σ : Fin n → List α, (∀ i, (σ i).length ≤ B) ∧
        ∀ e ∈ es, e.Satisfies σ

Uses 2 · Used by 2

Statement usesOrdinary word equation · Solution of a word equation

Used bySatisfiability as acceptance by some bounded SAT search · Satisfiability of a single word equation at a finite length bound

TheoremSatisfiability of a single word equation at a finite length bound#✓fully proved

An equation over Fin n is satisfiable iff it is satisfiable at some finite global length bound. There is no equation-computable bound claimed.

theorem WordEq.satisfiable_iff_exists_bound {n : ℕ} (e : WordEq α (Fin n)) :
    (∃ σ : Fin n → List α, e.Satisfies σ) ↔
      ∃ B : ℕ, ∃ σ : Fin n → List α, (∀ i, (σ i).length ≤ B) ∧ e.Satisfies σ

Uses 3

Statement usesOrdinary word equation · Solution of a word equation

Proof usesSolvability of word equation systems at a finite length bound

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.