Documentation

CslibFrontier.Logics.Propositional.CSP.AffineTemplate

Instantiating fixed affine templates #

A relation's affine normal form uses its finite coordinate type. Relabeling coordinates by their natural values gives fixed local templates, instantiated by scope lookup and concatenation. Repeated scope variables need no injectivity assumption: their occurrences cancel in the existing Boolean ring. Empty systems, inconsistent constant equations and nullary relations are included.

This is the fixed-template substitution step in [Che06], Theorem 4.3 and the following Gaussian-elimination argument (arXiv v1, printed pp. 15–16). The normal forms are fixed with the language; no efficient transformation of an input truth table is claimed.

Main definitions #

Main results #

source
def Cslib.Logic.PL.AffineEquation.relabel {V : Type u_2} {W : Type u_3} (f : V → W) (e : AffineEquation V) :
AffineEquation W

Rename the variables of an affine equation, retaining all occurrences.

Instances For
    source
    @[simp]
    theorem Cslib.Logic.PL.AffineEquation.holds_relabel {V : Type u_2} {W : Type u_3} (f : V → W) (e : AffineEquation V) (a : W → Bool) :
    (relabel f e).Holds a ↔ e.Holds (a ∘ f)

    Substitution composes assignments; the variable map need not be injective.

    source
    def Cslib.Logic.PL.AffineSystem.relabel {V : Type u_2} {W : Type u_3} (f : V → W) (F : AffineSystem V) :
    AffineSystem W

    Rename every equation of an affine system.

    Instances For
      source
      @[simp]
      theorem Cslib.Logic.PL.AffineSystem.holds_relabel {V : Type u_2} {W : Type u_3} (f : V → W) (F : AffineSystem V) (a : W → Bool) :
      (relabel f F).Holds a ↔ F.Holds (a ∘ f)

      System substitution preserves satisfaction under composed assignments, including repeated images of distinct variables.

      source
      def Cslib.Logic.PL.CSP.AffineTemplates {Rel : Type u_1} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (template : Rel → AffineSystem ℕ) :
      Prop

      Correct natural-position templates, evaluated at the declared finite tuple.

      Instances For
        source
        theorem Cslib.Logic.PL.CSP.affineTemplates_relabel_fin {Rel : Type u_1} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {φ : (R : Rel) → AffineSystem (Fin (arity R))} (h : ∀ (R : Rel) (a : Fin (arity R) → Bool), a ∈ booleanRelation arity sem R ↔ (φ R).Holds a) :
        AffineTemplates arity sem fun (R : Rel) => AffineSystem.relabel Fin.val (φ R)

        Finite-coordinate definitions yield correct natural-position templates.

        source
        def Cslib.Logic.PL.Constraint.instantiateAffine {Rel : Type u_1} {V : Type u_2} (fallback : V) (template : Rel → AffineSystem ℕ) (c : Constraint Rel V) :
        AffineSystem V

        Instantiate a local system using scope lookup. The fallback is irrelevant on correctly sized scopes for correct templates.

        Instances For
          source
          theorem Cslib.Logic.PL.Constraint.holds_instantiateAffine {Rel : Type u_1} {V : Type u_2} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {template : Rel → AffineSystem ℕ} (h : CSP.AffineTemplates arity sem template) (fallback : V) {c : Constraint Rel V} (hc : c.2.length = arity c.1) (σ : V → Bool) :
          (instantiateAffine fallback template c).Holds σ ↔ eval sem σ c = true

          Correctness of an instantiated constraint under every assignment.

          source
          def Cslib.Logic.PL.CSP.instantiateAffine {Rel : Type u_1} {V : Type u_2} (fallback : V) (template : Rel → AffineSystem ℕ) (F : CSP Rel V) :
          AffineSystem V

          Instantiate each constraint and concatenate the resulting systems.

          Instances For
            source
            theorem Cslib.Logic.PL.CSP.holds_instantiateAffine {Rel : Type u_1} {V : Type u_2} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {template : Rel → AffineSystem ℕ} (h : AffineTemplates arity sem template) (fallback : V) {F : CSP Rel V} (hF : WellFormed arity F) (σ : V → Bool) :
            (instantiateAffine fallback template F).Holds σ ↔ eval sem σ F = true

            Instantiation preserves satisfaction on every assignment of a well-formed instance.

            source
            theorem Cslib.Logic.PL.CSP.satisfiable_instantiateAffine {Rel : Type u_1} {V : Type u_2} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {template : Rel → AffineSystem ℕ} (h : AffineTemplates arity sem template) (fallback : V) {F : CSP Rel V} (hF : WellFormed arity F) :
            (∃ (σ : V → Bool), (instantiateAffine fallback template F).Holds σ) ↔ Satisfiable sem F

            No auxiliary variables are needed to preserve satisfiability.