The closed straight-line fragment is decidable

StructureClosed straight-line system#✓fully proved

A closed straight-line system: one defining term per variable, plus a query formula. The definition at position k is the definition of variable k. There are no free input variables: every variable the system talks about must be defined by the system itself.

structure SLSys (α : Type*) where
  /-- The defining terms, in variable order. -/
  defs : List (Term α ℕ)
  /-- The query formula. -/
  query : Formula α ℕ

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

CSLibExt/AutomatedReasoning/StringConstraints/Syntax.lean:74

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

CSLibExt/AutomatedReasoning/StringConstraints/Syntax.lean:150

Uses 2 · Used by 9

Statement usesString formulas · String term over variables

Used byAcyclic 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 · Candidate assignment of a straight-line system · Candidate assignment satisfies every definition · Folded assignment values of a straight-line system · Folded values have one entry per definition

DefinitionAcyclic closed straight-line system#✓fully proved

A closed straight-line system is acyclic when every defining term mentions only earlier variables, and the query mentions only defined variables. Hence every variable occurring anywhere in the system is defined, and unfolding the definitions terminates at ground terms: there is no free input variable.

def Acyclic (S : SLSys α) : Prop :=
  (∀ k (h : k < S.defs.length), ∀ j ∈ varsOf (S.defs[k]'h), j < k) ∧
    ∀ j ∈ varsOfFormula S.query, j < S.defs.length

structure SLSys (α : Type*) where
  /-- The defining terms, in variable order. -/
  defs : List (Term α ℕ)
  /-- The query formula. -/
  query : Formula α ℕ

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:74

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

CSLibExt/AutomatedReasoning/StringConstraints/Syntax.lean:100

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 => []

CSLibExt/AutomatedReasoning/StringConstraints/Syntax.lean:168

Uses 5 · Used by 4

Statement usesString formulas · Closed straight-line system · String term over variables · Variables occurring in a string term · Variables occurring in a string formula

Used bySatisfiability 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 · Candidate assignment satisfies every definition

DefinitionSatisfaction of a closed straight-line system#✓fully proved

Satisfaction of a closed straight-line system: the assignment obeys every definition and satisfies the query.

def SLSat (S : SLSys α) (σ : ℕ → List α) : Prop :=
  (∀ k (h : k < S.defs.length), σ k = eval σ (S.defs[k]'h)) ∧ Sat σ S.query

structure SLSys (α : Type*) where
  /-- The defining terms, in variable order. -/
  defs : List (Term α ℕ)
  /-- The query formula. -/
  query : Formula α ℕ

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:74

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

CSLibExt/AutomatedReasoning/StringConstraints/Syntax.lean:81

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

CSLibExt/AutomatedReasoning/StringConstraints/Syntax.lean:183

Uses 5 · Used by 3

Statement usesString formulas · Closed straight-line system · Satisfaction of a string formula · String term over variables · Evaluation of a string term under an assignment

Used bySatisfiability 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

DefinitionOne fold step of straight-line evaluation#✓fully proved

One fold step: evaluate the next defining term under the values computed so far and append the result.

def slStep (acc : List (List α)) (t : Term α ℕ) : List (List α) :=
  acc ++ [eval (fun j => acc.getD j []) t]

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

CSLibExt/AutomatedReasoning/StringConstraints/Syntax.lean:74

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

CSLibExt/AutomatedReasoning/StringConstraints/Syntax.lean:81

Uses 2 · Used by 7

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

Used byDefining 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 · Candidate assignment satisfies every definition · Folded assignment values of a straight-line system · Folded values have one entry per definition

DefinitionFolded assignment values of a straight-line system#✓fully proved

The folded assignment values, in variable order.

def values (S : SLSys α) : List (List α) :=
  S.defs.foldl slStep []

structure SLSys (α : Type*) where
  /-- The defining terms, in variable order. -/
  defs : List (Term α ℕ)
  /-- The query formula. -/
  query : Formula α ℕ

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:74

def slStep (acc : List (List α)) (t : Term α ℕ) : List (List α) :=
  acc ++ [eval (fun j => acc.getD j []) t]

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:96

Uses 3 · Used by 2

Statement usesClosed straight-line system · String term over variables · One fold step of straight-line evaluation

Used byCandidate assignment of a straight-line system · Folded values have one entry per definition

DefinitionCandidate assignment of a straight-line system#✓fully proved

The candidate assignment of a straight-line system.

def sol (S : SLSys α) : ℕ → List α :=
  fun i => (values S).getD i []

structure SLSys (α : Type*) where
  /-- The defining terms, in variable order. -/
  defs : List (Term α ℕ)
  /-- The query formula. -/
  query : Formula α ℕ

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:74

def values (S : SLSys α) : List (List α) :=
  S.defs.foldl slStep []

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:100

Uses 2 · Used by 4

Statement usesClosed straight-line system · Folded assignment values of a straight-line system

Used bySatisfiability 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 · Candidate assignment satisfies every definition

TheoremIn-bounds lookup with default equals indexed access#✓fully proved

Lookup with a proof of the bound is the getElem value.

theorem getD_eq_of_lt {l : List (List α)} {n : ℕ} (h : n < l.length) :
    l.getD n [] = l[n]'h

Used by 3

Used byDefining equation for the folded values · Lookup in an appended list below the prefix length · Lookup in a taken prefix agrees with the whole list

TheoremStraight-line fold preserves its initial segment#✓fully proved

The fold preserves its initial segment.

theorem foldl_take (defs : List (Term α ℕ)) (acc : List (List α)) :
    (defs.foldl slStep acc).take acc.length = acc

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

CSLibExt/AutomatedReasoning/StringConstraints/Syntax.lean:74

def slStep (acc : List (List α)) (t : Term α ℕ) : List (List α) :=
  acc ++ [eval (fun j => acc.getD j []) t]

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:96

Uses 3 · Used by 1

Statement usesString term over variables · One fold step of straight-line evaluation

Proof usesEvaluation of a string term under an assignment

Used byDefining equation for the folded values

TheoremStraight-line fold appends one value per definition#✓fully proved

The fold appends exactly one value per definition.

theorem foldl_length (defs : List (Term α ℕ)) (acc : List (List α)) :
    (defs.foldl slStep acc).length = acc.length + defs.length

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

CSLibExt/AutomatedReasoning/StringConstraints/Syntax.lean:74

def slStep (acc : List (List α)) (t : Term α ℕ) : List (List α) :=
  acc ++ [eval (fun j => acc.getD j []) t]

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:96

Uses 3 · Used by 2

Statement usesString term over variables · One fold step of straight-line evaluation

Proof usesEvaluation of a string term under an assignment

Used byDefining equation for the folded values · Folded values have one entry per definition

TheoremFolded values have one entry per definition#✓fully proved

Length of the folded values: one per definition.

theorem values_length (S : SLSys α) :
    (values S).length = S.defs.length

structure SLSys (α : Type*) where
  /-- The defining terms, in variable order. -/
  defs : List (Term α ℕ)
  /-- The query formula. -/
  query : Formula α ℕ

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:74

def values (S : SLSys α) : List (List α) :=
  S.defs.foldl slStep []

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:100

Uses 5

Statement usesClosed straight-line system · String term over variables · Folded assignment values of a straight-line system

Proof usesStraight-line fold appends one value per definition · One fold step of straight-line evaluation

TheoremLookup in a taken prefix agrees with the whole list#✓fully proved

Lookup in a taken prefix agrees with lookup in the whole list.

theorem getD_take_of_lt {l : List (List α)} {n m : ℕ} (h : n < m) (hl : n < l.length) :
    (l.take m).getD n [] = l.getD n []

Uses 1 · Used by 1

Proof usesIn-bounds lookup with default equals indexed access

Used byDefining equation for the folded values

TheoremLookup in an appended list below the prefix length#✓fully proved

Lookup in an appended list agrees with lookup below the prefix length.

theorem getD_append_of_lt {acc : List (List α)} {x : List α} {j : ℕ}
    (hj : j < acc.length) :
    (acc ++ [x]).getD j [] = acc.getD j []

Uses 1 · Used by 2

Proof usesIn-bounds lookup with default equals indexed access

Used byDefining equation for the folded values · Lookup in a folded list below the starting length

TheoremLookup in a folded list below the starting length#✓fully proved

Lookup in a folded list agrees with lookup in the starting list below its length.

theorem getD_foldl_of_lt (defs : List (Term α ℕ)) (acc : List (List α)) {j : ℕ}
    (hj : j < acc.length) :
    (defs.foldl slStep acc).getD j [] = acc.getD j []

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

CSLibExt/AutomatedReasoning/StringConstraints/Syntax.lean:74

def slStep (acc : List (List α)) (t : Term α ℕ) : List (List α) :=
  acc ++ [eval (fun j => acc.getD j []) t]

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:96

Uses 4 · Used by 1

Statement usesString term over variables · One fold step of straight-line evaluation

Proof usesEvaluation of a string term under an assignment · Lookup in an appended list below the prefix length

Used byDefining equation for the folded values

TheoremDefining equation for the folded values#✓fully proved

The defining equation for the folded values: the value at position acc.length + k is the k-th defining term evaluated under the folded values. The variable condition says the term only looks at positions below acc.length + k.

theorem foldl_getD (defs : List (Term α ℕ)) (acc : List (List α)) (k : ℕ)
    (hk : k < defs.length)
    (hvars : ∀ j ∈ varsOf (defs[k]'hk), j < acc.length + k) :
    (defs.foldl slStep acc).getD (acc.length + k) []
      = eval (fun j => (defs.foldl slStep acc).getD j []) (defs[k]'hk)

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

CSLibExt/AutomatedReasoning/StringConstraints/Syntax.lean:74

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

CSLibExt/AutomatedReasoning/StringConstraints/Syntax.lean:100

def slStep (acc : List (List α)) (t : Term α ℕ) : List (List α) :=
  acc ++ [eval (fun j => acc.getD j []) t]

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:96

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

CSLibExt/AutomatedReasoning/StringConstraints/Syntax.lean:81

Uses 11 · Used by 1

Statement usesString term over variables · Evaluation of a string term under an assignment · One fold step of straight-line evaluation · Variables occurring in a string term

Proof usesString term evaluation depends only on its variables · Straight-line fold appends one value per definition · Straight-line fold preserves its initial segment · Lookup in an appended list below the prefix length · In-bounds lookup with default equals indexed access · Lookup in a folded list below the starting length · Lookup in a taken prefix agrees with the whole list

Used byCandidate assignment satisfies every definition

TheoremCandidate assignment satisfies every definition#✓fully proved

The candidate assignment satisfies every definition.

theorem sol_satisfies_defs (S : SLSys α) (hacy : Acyclic S) (k : ℕ)
    (hk : k < S.defs.length) :
    sol S k = eval (sol S) (S.defs[k]'hk)

structure SLSys (α : Type*) where
  /-- The defining terms, in variable order. -/
  defs : List (Term α ℕ)
  /-- The query formula. -/
  query : Formula α ℕ

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:74

def Acyclic (S : SLSys α) : Prop :=
  (∀ k (h : k < S.defs.length), ∀ j ∈ varsOf (S.defs[k]'h), j < k) ∧
    ∀ j ∈ varsOfFormula S.query, j < S.defs.length

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:85

def sol (S : SLSys α) : ℕ → List α :=
  fun i => (values S).getD i []

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:104

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

CSLibExt/AutomatedReasoning/StringConstraints/Syntax.lean:81

Uses 10 · Used by 2

Statement usesAcyclic closed straight-line system · Closed straight-line system · String term over variables · Evaluation of a string term under an assignment · Candidate assignment of a straight-line system

Proof usesString formulas · Defining equation for the folded values · One fold step of straight-line evaluation · Variables occurring in a string term · Variables occurring in a string formula

Used bySatisfying assignments agree with the candidate on defined variables · Straight-line satisfiability iff the query holds on the candidate

TheoremSatisfying assignments agree with the candidate on defined variables#✓fully proved

Any satisfying assignment agrees with the candidate on defined variables.

theorem eq_sol_of_sat {S : SLSys α} {σ : ℕ → List α} (hacy : Acyclic S)
    (hSat : SLSat S σ) (k : ℕ) (hk : k < S.defs.length) :
    σ k = sol S k

structure SLSys (α : Type*) where
  /-- The defining terms, in variable order. -/
  defs : List (Term α ℕ)
  /-- The query formula. -/
  query : Formula α ℕ

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:74

def Acyclic (S : SLSys α) : Prop :=
  (∀ k (h : k < S.defs.length), ∀ j ∈ varsOf (S.defs[k]'h), j < k) ∧
    ∀ j ∈ varsOfFormula S.query, j < S.defs.length

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:85

def SLSat (S : SLSys α) (σ : ℕ → List α) : Prop :=
  (∀ k (h : k < S.defs.length), σ k = eval σ (S.defs[k]'h)) ∧ Sat σ S.query

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:91

def sol (S : SLSys α) : ℕ → List α :=
  fun i => (values S).getD i []

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:104

Uses 12 · Used by 1

Statement usesAcyclic closed straight-line system · Satisfaction of a closed straight-line system · Closed straight-line system · String term over variables · Candidate assignment of a straight-line system

Proof usesString formulas · Satisfaction of a string formula · Evaluation of a string term under an assignment · String term evaluation depends only on its variables · Candidate assignment satisfies every definition · Variables occurring in a string term · Variables occurring in a string formula

Used byStraight-line satisfiability iff the query holds on the candidate

TheoremStraight-line satisfiability iff the query holds on the candidate#✓fully proved

Satisfiability of a closed straight-line system is equivalent to the query holding on the candidate assignment.

theorem exists_sat_iff_sat_sol (S : SLSys α) (hacy : Acyclic S) :
    (∃ σ, SLSat S σ) ↔ Sat (sol S) S.query

structure SLSys (α : Type*) where
  /-- The defining terms, in variable order. -/
  defs : List (Term α ℕ)
  /-- The query formula. -/
  query : Formula α ℕ

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:74

def Acyclic (S : SLSys α) : Prop :=
  (∀ k (h : k < S.defs.length), ∀ j ∈ varsOf (S.defs[k]'h), j < k) ∧
    ∀ j ∈ varsOfFormula S.query, j < S.defs.length

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:85

def SLSat (S : SLSys α) (σ : ℕ → List α) : Prop :=
  (∀ k (h : k < S.defs.length), σ k = eval σ (S.defs[k]'h)) ∧ Sat σ S.query

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:91

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

CSLibExt/AutomatedReasoning/StringConstraints/Syntax.lean:183

def sol (S : SLSys α) : ℕ → List α :=
  fun i => (values S).getD i []

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:104

Uses 13 · Used by 1

Statement usesAcyclic closed straight-line system · String formulas · Satisfaction of a closed straight-line system · Closed straight-line system · Satisfaction of a string formula · Candidate assignment of a straight-line system

Proof usesString term over variables · Satisfying assignments agree with the candidate on defined variables · Evaluation of a string term under an assignment · Formula satisfaction depends only on its variables · Candidate assignment satisfies every definition · Variables occurring in a string term · Variables occurring in a string formula

Used bySatisfiability of a closed acyclic straight-line system is decidable

DefinitionSatisfiability of a closed acyclic straight-line system is decidable#✓fully proved

The decision procedure checks the query on the unique ground assignment; it does not search over free inputs, because the closed fragment has none.

def decidableExistsSatOfAcyclic (S : SLSys α) (hacy : Acyclic S) [DecidableEq α] :
    Decidable (∃ σ, SLSat S σ) := by
  haveI : Decidable (Sat (sol S) S.query) := by
    exact decidable_of_decidable_of_iff satB_iff
  exact decidable_of_decidable_of_iff (exists_sat_iff_sat_sol S hacy).symm

structure SLSys (α : Type*) where
  /-- The defining terms, in variable order. -/
  defs : List (Term α ℕ)
  /-- The query formula. -/
  query : Formula α ℕ

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:74

def Acyclic (S : SLSys α) : Prop :=
  (∀ k (h : k < S.defs.length), ∀ j ∈ varsOf (S.defs[k]'h), j < k) ∧
    ∀ j ∈ varsOfFormula S.query, j < S.defs.length

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:85

def SLSat (S : SLSys α) (σ : ℕ → List α) : Prop :=
  (∀ k (h : k < S.defs.length), σ k = eval σ (S.defs[k]'h)) ∧ Sat σ S.query

CSLibExt/AutomatedReasoning/StringConstraints/StraightLine.lean:91

Uses 9

Statement usesAcyclic closed straight-line system · String formulas · Satisfaction of a closed straight-line system · Closed straight-line system · Satisfaction of a string formula · Straight-line satisfiability iff the query holds on the candidate · Boolean checker for formula satisfaction · Correctness of the Boolean formula checker · Candidate assignment of a straight-line system

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.