String constraints: syntax and semantics

InductiveString term over variables#✓fully proved

A string term over variables V: a constant word, a variable, the concatenation of two terms, or a letter-to-word morphism applied to a term.

inductive Term (α : Type*) (V : Type*) where
  | const : List α → Term α V
  | var : V → Term α V
  | append : Term α V → Term α V → Term α V
  | hom : (α → List α) → Term α V → Term α V

Used by 30

Used byFormula embedding of word equations preserves satisfaction · Word equation as a string-constraint formula · Embedding of ordinary words into string terms · PCP encoding as a one-variable string constraint · PCP is characterized by string-constraint satisfiability: · Membership atom of the PCP encoding checks index words · Correctness of the SAT-to-string-constraints translation · Encoding of CNF formulas as string constraints · String constraint atom · Evaluation of a string term under an assignment · String term evaluation depends only on its variables · Satisfaction of a string atom · Boolean checker for atom satisfaction · Correctness of the Boolean atom checker · Atom satisfaction depends only on its variables · Variables occurring in a string term · Variables occurring in a string atom · Acyclic closed straight-line system · Satisfying assignments agree with the candidate on defined variables · Straight-line satisfiability iff the query holds on the candidate · Defining equation for the folded values · Straight-line fold appends one value per definition · Straight-line fold preserves its initial segment · Lookup in a folded list below the starting length · One fold step of straight-line evaluation · Satisfaction of a closed straight-line system · Closed straight-line system · Candidate assignment satisfies every definition · Folded assignment values of a straight-line system · Folded values have one entry per definition

DefinitionEvaluation of a string term under an assignment#✓fully proved

Evaluation of a term under an assignment.

def eval (σ : V → List α) : Term α V → List α
  | .const w => w
  | .var i => σ i
  | .append t₁ t₂ => eval σ t₁ ++ eval σ t₂
  | .hom f t => (eval σ t).flatMap f

Uses 1 · Used by 18

Statement usesString term over variables

Used byWord embedding preserves substitution semantics · Formula embedding of word equations preserves satisfaction · PCP is characterized by string-constraint satisfiability: · Correctness of the SAT-to-string-constraints translation · String term evaluation depends only on its variables · Satisfaction of a string atom · Boolean checker for atom satisfaction · Correctness of the Boolean atom checker · Atom satisfaction depends only on its variables · Satisfying assignments agree with the candidate on defined variables · Straight-line satisfiability iff the query holds on the candidate · Defining equation for the folded values · Straight-line fold appends one value per definition · Straight-line fold preserves its initial segment · Lookup in a folded list below the starting length · One fold step of straight-line evaluation · Satisfaction of a closed straight-line system · Candidate assignment satisfies every definition

DefinitionVariables occurring in a string term#✓fully proved

The variables occurring in a term, as a list (duplicates allowed).

def varsOf : Term α V → List V
  | .const _ => []
  | .var i => [i]
  | .append t₁ t₂ => varsOf t₁ ++ varsOf t₂
  | .hom _ t => varsOf t

Uses 1 · Used by 8

Statement usesString term over variables

Used byString term evaluation depends only on its variables · Atom satisfaction depends only on its variables · Variables occurring in a string atom · Acyclic closed straight-line system · Satisfying assignments agree with the candidate on defined variables · Straight-line satisfiability iff the query holds on the candidate · Defining equation for the folded values · Candidate assignment satisfies every definition

TheoremString term evaluation depends only on its variables#✓fully proved

Evaluation depends only on the values of the variables in the term.

theorem eval_eq_of_agree_on_vars {σ τ : V → List α} {t : Term α V}
    (h : ∀ i ∈ varsOf t, σ i = τ i) : eval σ t = eval τ t

Uses 3 · Used by 3

Statement usesString term over variables · Evaluation of a string term under an assignment · Variables occurring in a string term

Used byAtom satisfaction depends only on its variables · Satisfying assignments agree with the candidate on defined variables · Defining equation for the folded values

InductiveString constraint atom#✓fully proved

A string atom: a word equation, a regular-membership test, or a length bound. Regular languages are represented by the existing Cslib.Language.EncodedRegex.

inductive Atom (α : Type*) (V : Type*) where
  | eq : Term α V → Term α V → Atom α V
  | mem : Term α V → EncodedRegex α → Atom α V
  | lenLe : Term α V → ℕ → Atom α V
  | lenGe : Term α V → ℕ → Atom α V

Uses 2 · Used by 18

Statement usesString term over variables · Encoded regular expressions

Used byFormula embedding of word equations preserves satisfaction · Word equation as a string-constraint formula · PCP encoding as a one-variable string constraint · PCP is characterized by string-constraint satisfiability: · Membership atom of the PCP encoding checks index words · Correctness of the SAT-to-string-constraints translation · Encoding of CNF formulas as string constraints · String formulas · Satisfaction of a string formula · Satisfaction of a string atom · Boolean checker for atom satisfaction · Correctness of the Boolean atom checker · Atom satisfaction depends only on its variables · Boolean checker for formula satisfaction · Correctness of the Boolean formula checker · Formula satisfaction depends only on its variables · Variables occurring in a string atom · Variables occurring in a string formula

DefinitionVariables occurring in a string atom#✓fully proved

The variables occurring in an atom.

def varsOfAtom : Atom α V → List V
  | .eq t₁ t₂ => varsOf t₁ ++ varsOf t₂
  | .mem t _ => varsOf t
  | .lenLe t _ => varsOf t
  | .lenGe t _ => varsOf t

Uses 4 · Used by 2

Statement usesString constraint atom · String term over variables · Variables occurring in a string term · Encoded regular expressions

Used byAtom satisfaction depends only on its variables · Variables occurring in a string formula

InductiveString formulas#✓fully proved

Positive Boolean combinations of atoms (conjunction, disjunction, true, false; no negation), as in the positive fragment of SMT-LIB assertions.

inductive Formula (α : Type*) (V : Type*) where
  | atom : Atom α V → Formula α V
  | and : Formula α V → Formula α V → Formula α V
  | or : Formula α V → Formula α V → Formula α V
  | true : Formula α V
  | false : Formula α V

Uses 1 · Used by 25

Statement usesString constraint atom

Used bySAT backend agrees with the bounded formula semantics · Bounded-search satisfiability specification · Soundness and completeness of the bounded-search specification · Formula embedding of word equations preserves satisfaction · Word equation as a string-constraint formula · PCP encoding as a one-variable string constraint · PCP is characterized by string-constraint satisfiability: · Correctness of the SAT-to-string-constraints translation · Encoding of CNF formulas as string constraints · Conjunction of a list of string formulas · Disjunction of a list of string formulas · Satisfaction of a string formula · Satisfaction of a conjunction chain · Boolean checker for formula satisfaction · Correctness of the Boolean formula checker · Formula satisfaction depends only on its variables · Satisfaction of a disjunction chain · Variables occurring in a string formula · Acyclic closed straight-line system · Satisfiability of a closed acyclic straight-line system is decidable · Satisfying assignments agree with the candidate on defined variables · Straight-line satisfiability iff the query holds on the candidate · Satisfaction of a closed straight-line system · Closed straight-line system · Candidate assignment satisfies every definition

DefinitionConjunction of a list of string formulas#✓fully proved

Conjunction of a list of formulas.

def andChain : List (Formula α V) → Formula α V
  | [] => .true
  | f :: fs => .and f (andChain fs)

Uses 1 · Used by 4

Statement usesString formulas

Used bySAT backend agrees with the bounded formula semantics · Correctness of the SAT-to-string-constraints translation · Encoding of CNF formulas as string constraints · Satisfaction of a conjunction chain

DefinitionDisjunction of a list of string formulas#✓fully proved

Disjunction of a list of formulas.

def orChain : List (Formula α V) → Formula α V
  | [] => .false
  | f :: fs => .or f (orChain fs)

Uses 1 · Used by 3

Statement usesString formulas

Used byCorrectness of the SAT-to-string-constraints translation · Encoding of CNF formulas as string constraints · Satisfaction of a disjunction chain

DefinitionVariables occurring in a string formula#✓fully proved

The variables occurring in a formula.

def varsOfFormula : Formula α V → List V
  | .atom a => varsOfAtom a
  | .and f g => varsOfFormula f ++ varsOfFormula g
  | .or f g => varsOfFormula f ++ varsOfFormula g
  | .true => []
  | .false => []

Uses 3 · Used by 7

Statement usesString constraint atom · String formulas · Variables occurring in a string atom

Used bySoundness and completeness of the bounded-search specification · SAT iff the bounded-search specification holds of the encoding · Formula satisfaction depends only on its variables · Acyclic closed straight-line system · Satisfying assignments agree with the candidate on defined variables · Straight-line satisfiability iff the query holds on the candidate · Candidate assignment satisfies every definition

DefinitionSatisfaction of a string atom#✓fully proved

Satisfaction of an atom under an assignment.

def SatAtom (σ : V → List α) : Atom α V → Prop
  | .eq t₁ t₂ => eval σ t₁ = eval σ t₂
  | .mem t e => eval σ t ∈ e.toRegex.matches'
  | .lenLe t k => (eval σ t).length ≤ k
  | .lenGe t k => k ≤ (eval σ t).length

Uses 5 · Used by 7

Statement usesString constraint atom · String term over variables · Evaluation of a string term under an assignment · Encoded regular expressions · The regular expression denoted by an encoding

Used byFormula embedding of word equations preserves satisfaction · PCP is characterized by string-constraint satisfiability: · Membership atom of the PCP encoding checks index words · Satisfaction of a string formula · Correctness of the Boolean atom checker · Atom satisfaction depends only on its variables · Correctness of the Boolean formula checker

DefinitionSatisfaction of a string formula#✓fully proved

Satisfaction of a formula under an assignment.

def Sat (σ : V → List α) : Formula α V → Prop
  | .atom a => SatAtom σ a
  | .and f g => Sat σ f ∧ Sat σ g
  | .or f g => Sat σ f ∨ Sat σ g
  | .true => True
  | .false => False

Uses 3 · Used by 14

Statement usesString constraint atom · String formulas · Satisfaction of a string atom

Used bySAT backend agrees with the bounded formula semantics · Soundness and completeness of the bounded-search specification · Formula embedding of word equations preserves satisfaction · PCP is characterized by string-constraint satisfiability: · SAT iff the bounded-search specification holds of the encoding · Correctness of the SAT-to-string-constraints translation · Satisfaction of a conjunction chain · Correctness of the Boolean formula checker · Formula satisfaction depends only on its variables · Satisfaction of a disjunction chain · Satisfiability of a closed acyclic straight-line system is decidable · Satisfying assignments agree with the candidate on defined variables · Straight-line satisfiability iff the query holds on the candidate · Satisfaction of a closed straight-line system

TheoremSatisfaction of a conjunction chain#✓fully proved

Satisfaction of a conjunction chain: every member is satisfied.

theorem sat_andChain {σ : V → List α} {fs : List (Formula α V)} :
    Sat σ (andChain fs) ↔ ∀ f ∈ fs, Sat σ f

Uses 3 · Used by 2

Statement usesString formulas · Satisfaction of a string formula · Conjunction of a list of string formulas

Used bySAT backend agrees with the bounded formula semantics · Correctness of the SAT-to-string-constraints translation

TheoremSatisfaction of a disjunction chain#✓fully proved

Satisfaction of a disjunction chain: one member is satisfied.

theorem sat_orChain {σ : V → List α} {fs : List (Formula α V)} :
    Sat σ (orChain fs) ↔ ∃ f ∈ fs, Sat σ f

Uses 3 · Used by 1

Statement usesString formulas · Satisfaction of a string formula · Disjunction of a list of string formulas

Used byCorrectness of the SAT-to-string-constraints translation

TheoremAtom satisfaction depends only on its variables#✓fully proved

Satisfaction of an atom depends only on the values of its variables.

theorem satAtom_congr {σ τ : V → List α} {a : Atom α V}
    (h : ∀ i ∈ varsOfAtom a, σ i = τ i) : SatAtom σ a ↔ SatAtom τ a

Uses 9 · Used by 1

Statement usesString constraint atom · Satisfaction of a string atom · Variables occurring in a string atom

Proof usesString term over variables · Evaluation of a string term under an assignment · String term evaluation depends only on its variables · Variables occurring in a string term · Encoded regular expressions · The regular expression denoted by an encoding

Used byFormula satisfaction depends only on its variables

TheoremFormula satisfaction depends only on its variables#✓fully proved

Satisfaction depends only on the values of the variables in the formula.

theorem sat_congr {σ τ : V → List α} {φ : Formula α V}
    (h : ∀ i ∈ varsOfFormula φ, σ i = τ i) : Sat σ φ ↔ Sat τ φ

Uses 5 · Used by 3

Statement usesString formulas · Satisfaction of a string formula · Variables occurring in a string formula

Proof usesString constraint atom · Atom satisfaction depends only on its variables

Used bySoundness and completeness of the bounded-search specification · SAT iff the bounded-search specification holds of the encoding · Straight-line satisfiability iff the query holds on the candidate

DefinitionBoolean checker for atom satisfaction#✓fully proved

Boolean checker for atom satisfaction. Regular membership uses EncodedRegex.memB.

def satAtomB (σ : V → List α) : Atom α V → Bool
  | .eq t₁ t₂ => decide (eval σ t₁ = eval σ t₂)
  | .mem t e => e.memB (eval σ t)
  | .lenLe t k => decide ((eval σ t).length ≤ k)
  | .lenGe t k => decide (k ≤ (eval σ t).length)

Uses 5 · Used by 3

Statement usesString constraint atom · String term over variables · Evaluation of a string term under an assignment · Encoded regular expressions · Membership test for regular expressions

Used byCorrectness of the Boolean atom checker · Boolean checker for formula satisfaction · Correctness of the Boolean formula checker

TheoremCorrectness of the Boolean atom checker#✓fully proved

The Boolean checker is correct.

theorem satAtomB_iff {σ : V → List α} {a : Atom α V} :
    satAtomB σ a = true ↔ SatAtom σ a

Uses 13 · Used by 1

Statement usesString constraint atom · Satisfaction of a string atom · Boolean checker for atom satisfaction

Proof usesString term over variables · Evaluation of a string term under an assignment · Language of an encoded grammar · The membership test for context-free grammars · Correctness of the membership test · Encoded regular expressions · The grammar generates the language of the expression · Membership test for regular expressions · The grammar of an encoded regular expression · The regular expression denoted by an encoding

Used byCorrectness of the Boolean formula checker

DefinitionBoolean checker for formula satisfaction#✓fully proved

Boolean checker for formula satisfaction.

def satB (σ : V → List α) : Formula α V → Bool
  | .atom a => satAtomB σ a
  | .and f g => satB σ f && satB σ g
  | .or f g => satB σ f || satB σ g
  | .true => true
  | .false => false

Uses 3 · Used by 4

Statement usesString constraint atom · String formulas · Boolean checker for atom satisfaction

Used byBounded-search satisfiability specification · Soundness and completeness of the bounded-search specification · Correctness of the Boolean formula checker · Satisfiability of a closed acyclic straight-line system is decidable

TheoremCorrectness of the Boolean formula checker#✓fully proved

The Boolean checker is correct.

theorem satB_iff {σ : V → List α} {φ : Formula α V} :
    satB σ φ = true ↔ Sat σ φ

Uses 7 · Used by 2

Statement usesString formulas · Satisfaction of a string formula · Boolean checker for formula satisfaction

Proof usesString constraint atom · Satisfaction of a string atom · Boolean checker for atom satisfaction · Correctness of the Boolean atom checker

Used bySoundness and completeness of the bounded-search specification · Satisfiability of a closed acyclic straight-line system is decidable

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.