Formulas

This file provides typeclasses for formulas and different operations these formulas can support. Note that this file does not implement any of these operations, but it formalizes what these operations should do. More specifically the file contains

• some functions for working with Validator.VarSet',
• definitions and methods for models, partial models, literals, clauses, cubes, CNF-formulas and DNF-formulas, and
• type classes for formulas and various operations on formulas.

VarSet'

def Validator.VarSet'.empty {n : ℕ} : VarSet' n

Equations

• Validator.VarSet'.empty = ⟨[], ⋯⟩

def Validator.VarSet'.union {n : ℕ} (V V' : VarSet' n) : VarSet' n

Equations

• V.union V' = ⟨(↑V).mergeDedup ↑V', ⋯⟩

@[simp]

theorem Validator.VarSet'.mem_union {n : ℕ} {V V' : VarSet' n} {i : Fin n} : i ∈ ↑(V.union V') ↔ i ∈ ↑V ∨ i ∈ ↑V'

def Validator.VarSet'.insert {n : ℕ} (V : VarSet' n) (v : Fin n) : VarSet' n

Equations

• V.insert v = ⟨(↑V).insertDedup v, ⋯⟩

@[simp]

theorem Validator.VarSet'.mem_insert {n : ℕ} {V : VarSet' n} {v i : Fin n} : i ∈ ↑(V.insert v) ↔ i ∈ ↑V ∨ i = v

def Validator.VarSet'.diff {n : ℕ} (V V' : VarSet' n) : VarSet' n

Equations

• V.diff V' = ⟨(↑V).diff' ↑V', ⋯⟩

@[simp]

theorem Validator.VarSet'.mem_diff {n : ℕ} {V V' : VarSet' n} {i : Fin n} : i ∈ ↑(V.diff V') ↔ i ∈ ↑V ∧ i ∉ ↑V'

Model and PartialModel

@[reducible, inline]

abbrev Validator.Formula.Model (n : ℕ) : Type

Model is usually in the in the context of a formula, where it represents a model of this formula, i.e. an assignment of variables making the formula true. It is used to show the correctness of operations.

Equations

• Validator.Formula.Model n = (Fin n → Prop)

@[reducible, inline]

abbrev Validator.Formula.Models (n : ℕ) : Type

A set of models.

Equations

• Validator.Formula.Models n = Set (Validator.Formula.Model n)

@[reducible, inline]

abbrev Validator.Formula.PartialModel {n : ℕ} (V : VarSet' n) : Type

Partial models are partial assignments. In contrast to Model, these are used at runtime.

Equations

• Validator.Formula.PartialModel V = BitVec (↑V).length

def Validator.Formula.PartialModel.models {n : ℕ} {V : VarSet' n} (M : PartialModel V) : Models n

All models corresponding to to partial model M.

Equations

• M.models = {M' : Validator.Formula.Model n | ∀ (i : Fin (↑V).length), M' ⟨↑(↑V)[i], ⋯⟩ ↔ M[i] = true}

Literal

def Validator.Formula.Literal (n : ℕ) : Type

A Literal is a variable i (represented by (i, true)) or its negation (represented by (i, false)).

Equations

• Validator.Formula.Literal n = (Fin n × Bool)

instance Validator.Formula.instDecidableEqLiteral (n : ℕ) : DecidableEq (Literal n)

Equations

• Validator.Formula.instDecidableEqLiteral n a b = instDecidableEqProd a b

instance Validator.Formula.instReprLiteral (n : ℕ) : Repr (Literal n)

Equations

• Validator.Formula.instReprLiteral n = instReprProdOfReprTuple

def Validator.Formula.Literal.models {n : ℕ} : Literal n → Models n

Equations

• Validator.Formula.Literal.models (i, true) = {M : Validator.Formula.Model n | M i}
• Validator.Formula.Literal.models (i, false) = {M : Validator.Formula.Model n | ¬M i}

theorem Validator.Formula.Literal.mem_models {n : ℕ} (l : Literal n) (M : Model n) : M ∈ l.models ↔ (M l.1 ↔ l.2 = true)

def Validator.Formula.Literal.negate {n : ℕ} : Literal n → Literal n

Equations

• Validator.Formula.Literal.negate (i, true) = (i, false)
• Validator.Formula.Literal.negate (i, false) = (i, true)

@[simp]

theorem Validator.Formula.Literal.models_negate {n : ℕ} (l : Literal n) : l.negate.models = l.modelsᶜ

theorem Validator.Formula.Literal.eq_or_eq_negate_iff_var_eq {n : ℕ} {l l' : Literal n} : l.1 = l'.1 ↔ l = l' ∨ l = l'.negate

Clause

@[reducible, inline]

abbrev Validator.Formula.Clause (n : ℕ) : Type

A clause is a disjuction of literals.

Equations

• Validator.Formula.Clause n = List (Validator.Formula.Literal n)

def Validator.Formula.Clause.models {n : ℕ} (γ : Clause n) : Models n

Equations

• γ.models = {M : Validator.Formula.Model n | ∃ l ∈ γ, M ∈ l.models}

@[simp]

theorem Validator.Formula.Clause.mem_models {n : ℕ} (γ : Clause n) (M : Model n) : M ∈ γ.models ↔ ∃ l ∈ γ, M ∈ l.models

@[simp]

theorem Validator.Formula.Clause.models_append {n : ℕ} (γ1 γ2 : Clause n) : (γ1 ++ γ2).models = γ1.models ∪ γ2.models

Cube

@[reducible, inline]

abbrev Validator.Formula.Cube (n : ℕ) : Type

A cube is a conjunction of literals.

Equations

• Validator.Formula.Cube n = List (Validator.Formula.Literal n)

def Validator.Formula.Cube.models {n : ℕ} (δ : Cube n) : Models n

Equations

• δ.models = {M : Validator.Formula.Model n | ∀ l ∈ δ, M ∈ l.models}

@[simp]

theorem Validator.Formula.Cube.mem_models {n : ℕ} (δ : Cube n) (M : Model n) : M ∈ δ.models ↔ ∀ l ∈ δ, M ∈ l.models

@[simp]

theorem Validator.Formula.Cube.models_append {n : ℕ} (δ1 δ2 : Cube n) : (δ1 ++ δ2).models = δ1.models ∩ δ2.models

@[simp]

theorem Validator.Formula.Cube.models_cons {n : ℕ} {l : Literal n} (δ : Cube n) : models (l :: δ) = l.models ∩ δ.models

def Validator.Formula.Cube.vars {n : ℕ} (δ : Cube n) : VarSet n

Equations

• δ.vars = {i : Fin n | ∃ l ∈ δ, l.1 = i}

@[simp]

theorem Validator.Formula.Cube.vars_cons {n : ℕ} (δ : Cube n) {l : Literal n} : vars (l :: δ) = {l.1} ∪ δ.vars

def Validator.Formula.Cube.consistent {n : ℕ} (δ : Cube n) : Bool

Equations

• δ.consistent = List.all δ fun (l : Validator.Formula.Literal n) => decide (l.negate ∉ δ)

theorem Validator.Formula.Cube.consistent_iff {n : ℕ} {δ : Cube n} : δ.consistent = true ↔ δ.models ≠ ∅

def Validator.Formula.Clause.neg {n : ℕ} (γ : Clause n) : Cube n

The negation of a clause

Equations

• γ.neg = List.map Validator.Formula.Literal.negate γ

theorem Validator.Formula.Clause.models_neg {n : ℕ} {γ : Clause n} : γ.neg.models = γ.modelsᶜ

def Validator.Formula.Cube.neg {n : ℕ} (δ : Cube n) : Clause n

The negation of a cube

Equations

• δ.neg = List.map Validator.Formula.Literal.negate δ

theorem Validator.Formula.Cube.models_neg {n : ℕ} {δ : Cube n} : δ.neg.models = δ.modelsᶜ

CNF

@[reducible, inline]

abbrev Validator.Formula.CNF (n : ℕ) : Type

A CNF-formula is a conjunction of clauses.

Equations

• Validator.Formula.CNF n = List (Validator.Formula.Clause n)

def Validator.Formula.CNF.models {n : ℕ} (φ : CNF n) : Models n

Equations

• φ.models = {M : Validator.Formula.Model n | ∀ γ ∈ φ, ∃ l ∈ γ, M ∈ l.models}

@[simp]

theorem Validator.Formula.CNF.mem_models {n : ℕ} (φ : CNF n) {M : Model n} : M ∈ φ.models ↔ ∀ γ ∈ φ, ∃ l ∈ γ, M ∈ l.models

theorem Validator.Formula.CNF.models_mem_empty {n : ℕ} (φ : CNF n) (h : [] ∈ φ) : φ.models = ∅

def Validator.Formula.CNF.vars {n : ℕ} (φ : CNF n) : VarSet n

Equations

• φ.vars = {i : Fin n | ∃ γ ∈ φ, ∃ l ∈ γ, l.1 = i}

@[simp]

theorem Validator.Formula.CNF.mem_vars {n : ℕ} (φ : CNF n) {i : Fin n} : i ∈ φ.vars ↔ ∃ γ ∈ φ, ∃ v ∈ γ, v.1 = i

@[simp]

theorem Validator.Formula.CNF.forall_iff_subset_models {n : ℕ} {φ : CNF n} {Ms : Models n} : (∀ γ ∈ φ, Ms ⊆ γ.models) ↔ Ms ⊆ φ.models

theorem Validator.Formula.CNF.models_equiv_right {n : ℕ} {φ : CNF n} {M M' : Model n} : (∀ i ∈ φ.vars, M i = M' i) → M ∈ φ.models → M' ∈ φ.models

DNF

@[reducible, inline]

abbrev Validator.Formula.DNF (n : ℕ) : Type

A DNF-formula is a conjunction of cubes.

Equations

• Validator.Formula.DNF n = List (Validator.Formula.Cube n)

def Validator.Formula.DNF.models {n : ℕ} (φ : DNF n) : Models n

Equations

• φ.models = {M : Validator.Formula.Model n | ∃ δ ∈ φ, ∀ l ∈ δ, M ∈ l.models}

@[simp]

theorem Validator.Formula.DNF.mem_models {n : ℕ} (φ : DNF n) {M : Model n} : M ∈ φ.models ↔ ∃ δ ∈ φ, ∀ l ∈ δ, M ∈ l.models

@[simp]

theorem Validator.Formula.DNF.exists_iff_models_subset {n : ℕ} {φ : DNF n} {Ms : Models n} : (∀ δ ∈ φ, δ.models ⊆ Ms) ↔ φ.models ⊆ Ms

Formula

class Validator.Formula (n : ℕ) (R : Type) : Type

Type class for formulas with variables Fin n. The variables are ordered by ordering <.

• vars (φ : R) : VarSet' n

  The variables associated with the formula φ. Note that not all of these variables need to 'appear' in φ.

• models (φ : R) : Models n

  The models of the formula φ

• models_equiv_right (φ : R) (M M' : Model n) : (∀ i ∈ ↑(vars φ), M i = M' i) → M ∈ models φ → M' ∈ models φ

  If two assignments coincide on the variables of φ, then the second is a model of φ if the first one is a model of φ.

theorem Validator.Formula.models_equiv {n : ℕ} {R : Type} [h : Formula n R] {φ : R} {M M' : Model n} (h1 : ∀ i ∈ ↑(vars φ), M i = M' i) : M ∈ models φ ↔ M' ∈ models φ

If two assignments M and M' coincide on the variables of φ, then M is a model of φ iff M' is a model of φ.

Operations on Formulas

class Validator.Formula.Top (n : ℕ) (R : Type) [F : Formula n R] : Type

• top : R
• top_correct : models (top n) = Set.univ

class Validator.Formula.Bot (n : ℕ) (R : Type) [F : Formula n R] : Type

• bot : R
• bot_correct : models (bot n) = ∅ ∧ vars (bot n) = VarSet'.empty

class Validator.Formula.Consistency (n : ℕ) (R : Type) [F : Formula n R] : Type

• consistent (φ : R) : Bool
• consistent_correct (φ : R) : consistent n φ = true ↔ Set.Nonempty (models φ)

class Validator.Formula.ClausalEntailment (n : ℕ) (R : Type) [F : Formula n R] : Type

• entails (φ : R) (γ : Clause n) : Bool
• entails_correct (φ : R) (γ : Clause n) : entails φ γ = true ↔ models φ ⊆ γ.models

class Validator.Formula.Implicant (n : ℕ) (R : Type) [F : Formula n R] : Type

• entails (δ : Cube n) (φ : R) : Bool
• entails_correct (δ : Cube n) (φ : R) : entails δ φ = true ↔ δ.models ⊆ models φ

class Validator.Formula.SententialEntailment (n : ℕ) (R : Type) [F : Formula n R] : Type

• entails (φ ψ : R) : Bool
• entails_correct (φ ψ : R) : entails n φ ψ = true ↔ models φ ⊆ models ψ

class Validator.Formula.BoundedConjuction (n : ℕ) (R : Type) [F : Formula n R] : Type

• and : R → R → R
• and_correct (φ ψ : R) : models (and n φ ψ) = models φ ∩ models ψ

def Validator.Formula.BoundedConjuction.andList {n : ℕ} {R : Type} [Formula n R] [Top n R] [h : BoundedConjuction n R] : List R → R

The time complexity of andList is generally bad, therefore it should only be used if the number of conjuncts is bounded.

Equations

• Validator.Formula.BoundedConjuction.andList [] = Validator.Formula.Top.top n
• Validator.Formula.BoundedConjuction.andList [φ] = φ
• Validator.Formula.BoundedConjuction.andList (φ :: ψ :: tail) = Validator.Formula.BoundedConjuction.and n φ (Validator.Formula.BoundedConjuction.andList (ψ :: tail))

theorem Validator.Formula.BoundedConjuction.andList_correct {n : ℕ} {R : Type} [F : Formula n R] [Top n R] [h : BoundedConjuction n R] {l : List R} : models (andList l) = {M : Model n | ∀ φ ∈ l, M ∈ models φ}

class Validator.Formula.BoundedDisjunction (n : ℕ) (R : Type) [F : Formula n R] : Type

• or : R → R → R
• or_correct (φ ψ : R) : models (or n φ ψ) = models φ ∪ models ψ

def Validator.Formula.BoundedDisjunction.orList {n : ℕ} {R : Type} [Formula n R] [Bot n R] [h : BoundedDisjunction n R] : List R → R

The timecomplexity of andList is generally bad, therefore it should only be used if the number of conjuncts is bounded.

Equations

• Validator.Formula.BoundedDisjunction.orList [] = Validator.Formula.Bot.bot n
• Validator.Formula.BoundedDisjunction.orList [φ] = φ
• Validator.Formula.BoundedDisjunction.orList (φ :: ψ :: tail) = Validator.Formula.BoundedDisjunction.or n φ (Validator.Formula.BoundedDisjunction.orList (ψ :: tail))

theorem Validator.Formula.BoundedDisjunction.orList_correct {n : ℕ} {R : Type} [F : Formula n R] [Bot n R] [h : BoundedDisjunction n R] {l : List R} : models (orList l) = {M : Model n | ∃ φ ∈ l, M ∈ models φ}

class Validator.Formula.OfPartialModel (n : ℕ) (R : Type) [F : Formula n R] : Type

• ofPartialModel (V : VarSet' n) : PartialModel V → R
• ofPartialModel_correct {V : VarSet' n} {M : PartialModel V} : models (ofPartialModel V M) = M.models ∧ vars (ofPartialModel V M) = V

structure Validator.Formula.Renaming {n : ℕ} (dom : VarSet' n) : Type

• rename : Fin n → Fin n
• mono : StrictMonoOn self.rename ↑(↑dom).toFinset
• prop (i : Fin n) : i ∉ (↑dom).toFinset → self.rename i = i

def Validator.Formula.Model.rename {n : ℕ} {V : VarSet' n} (r : Renaming V) (M : Model n) : Model n

Equations

• Validator.Formula.Model.rename r M i = M (r.rename i)

def Validator.Formula.Literal.rename {n : ℕ} {V : VarSet' n} (r : Renaming V) (l : Literal n) : Literal n

Equations

• Validator.Formula.Literal.rename r l = (r.rename l.1, l.2)

def Validator.Formula.Clause.rename {n : ℕ} {V : VarSet' n} (r : Renaming V) (γ : Clause n) : Clause n

Equations

• Validator.Formula.Clause.rename r γ = List.map (Validator.Formula.Literal.rename r) γ

def Validator.Formula.Cube.rename {n : ℕ} {V : VarSet' n} (r : Renaming V) (δ : Cube n) : Cube n

Equations

• Validator.Formula.Cube.rename r δ = List.map (Validator.Formula.Literal.rename r) δ

def Validator.Formula.CNF.rename {n : ℕ} {V : VarSet' n} (r : Renaming V) (φ : CNF n) : CNF n

Equations

• Validator.Formula.CNF.rename r φ = List.map (Validator.Formula.Clause.rename r) φ

def Validator.Formula.VarSet'.rename {n : ℕ} {V : VarSet' n} (r : Renaming V) (V' : VarSet' n) : VarSet' n

Equations

• Validator.Formula.VarSet'.rename r V' = (V'.diff V).union ⟨List.map r.rename ↑V, ⋯⟩

theorem Validator.Formula.VarSet'.mem_rename {n : ℕ} {V : VarSet' n} {r : Renaming V} {V' : VarSet' n} {i : Fin n} : i ∈ ↑(rename r V') ↔ i ∈ ↑V' ∧ i ∉ ↑V ∨ ∃ j ∈ ↑V, i = r.rename j

class Validator.Formula.Rename (n : ℕ) (R : Type) [F : Formula n R] : Type

Renaming consistent with order

• rename (φ : R) {V : VarSet' n} (f : Renaming V) : R
• rename_correct (φ : R) (V : VarSet' n) (f : Renaming V) : (∀ (i : Fin n), i ∈ ↑(vars (rename φ f)) ↔ i ∈ f.rename '' ↑(↑(vars φ)).toFinset) ∧ models (rename φ f) = {M : Model n | ∃ M' ∈ models φ, ∀ i ∈ (↑(vars φ)).attach, M (f.rename ↑i) ↔ M' ↑i}

theorem Validator.Formula.Rename.mem_rename_models {n : ℕ} {R : Type} [F : Formula n R] [Rename n R] {φ : R} {V : VarSet' n} {r : Renaming V} {M : Model n} : M ∈ models (rename φ r) ↔ Model.rename r M ∈ models φ

class Validator.Formula.RenamingOld (n : ℕ) (R : Type) [F : Formula n R] : Type

Renaming consistent with order

• rename (φ : R) (vars' : VarSet' n) : (↑vars').length = (↑(vars φ)).length → R
• rename_correct {φ : R} {vars' : VarSet' n} {h : (↑vars').length = (↑(vars φ)).length} : vars (rename φ vars' h) = vars' ∧ models (rename φ vars' h) = {M : Model n | ∃ M' ∈ models φ, ∀ (i : Fin (↑vars').length), M (↑vars')[i] ↔ M' (↑(vars φ))[i]}

def Validator.Formula.RenamingOld.renameModel {n : ℕ} (V V' : VarSet' n) (h : (↑V').length = (↑V).length) (M : Model n) : Model n

Equations

• Validator.Formula.RenamingOld.renameModel V V' h M i = match List.finIdxOf? i ↑V with | none => M i | some j => M (↑V')[j]

theorem Validator.Formula.RenamingOld.mem_rename_models {n : ℕ} {R : Type} [F : Formula n R] [RenamingOld n R] {φ : R} {vars' : VarSet' n} {h : (↑vars').length = (↑(vars φ)).length} {M : Model n} : M ∈ models (rename φ vars' h) ↔ renameModel (vars φ) vars' ⋯ M ∈ models φ

def Validator.Formula.RenamingOld.renameLiteral {n : ℕ} (V V' : VarSet' n) (h : (↑V').length = (↑V).length) (l : Literal n) : Literal n

Equations

• Validator.Formula.RenamingOld.renameLiteral V V' h l = match List.finIdxOf? l.1 ↑V with | none => l | some j => ((↑V')[j], l.2)

class Validator.Formula.ToCNF (n : ℕ) (R : Type) [F : Formula n R] : Type

• toCNF : R → CNF n
• toCNF_correct (φ : R) : (toCNF φ).models = models φ

def Validator.Formula.ToCNF.disjunctionToCNF {n : ℕ} {R : Type} [Formula n R] [ToCNF n R] (l : List R) : CNF n

Equations

• Validator.Formula.ToCNF.disjunctionToCNF l = (List.map Validator.Formula.ToCNF.toCNF l).multiply

theorem Validator.Formula.ToCNF.disjunctionToCNF_correct {n : ℕ} {R : Type} [F : Formula n R] [h : ToCNF n R] {φs : List R} : (disjunctionToCNF φs).models = {M : Model n | ∃ φ ∈ φs, M ∈ models φ}

def Validator.Formula.ToCNF.negToDNF {n : ℕ} {R : Type} [Formula n R] [h : ToCNF n R] (φ : R) : DNF n

Transform ¬x to a DNF formula by translating x to a CNF-formula and applying De Morgans laws.

Equations

• Validator.Formula.ToCNF.negToDNF φ = List.map (List.map Validator.Formula.Literal.negate) (Validator.Formula.ToCNF.toCNF φ)

theorem Validator.Formula.ToCNF.negToDNF_correct {n : ℕ} {R : Type} [F : Formula n R] [h : ToCNF n R] {φ : R} : (negToDNF φ).models = (models φ)ᶜ

class Validator.Formula.ToDNF (n : ℕ) (R : Type) [F : Formula n R] : Type

• toDNF : R → DNF n
• toDNF_correct {φ : R} : (toDNF φ).models = models φ

def Validator.Formula.ToDNF.conjunctionToDNF {n : ℕ} {R : Type} [Formula n R] [ToDNF n R] (l : List R) : DNF n

Equations

• Validator.Formula.ToDNF.conjunctionToDNF l = (List.map Validator.Formula.ToDNF.toDNF l).multiply

theorem Validator.Formula.ToDNF.conjunctionToDnF_correct {n : ℕ} {R : Type} [F : Formula n R] [h : ToDNF n R] {φs : List R} : (conjunctionToDNF φs).models = {M : Model n | ∀ φ ∈ φs, M ∈ models φ}

def Validator.Formula.ToDNF.negToCNF {n : ℕ} {R : Type} [Formula n R] [h : ToDNF n R] (φ : R) : CNF n

Transform ¬x to a CNF formula by translating x to a DNF-formula and applying De Morgans laws.

Equations

• Validator.Formula.ToDNF.negToCNF φ = List.map (List.map Validator.Formula.Literal.negate) (Validator.Formula.ToDNF.toDNF φ)

theorem Validator.Formula.ToDNF.negToCNF_correct {n : ℕ} {R : Type} [F : Formula n R] [h : ToDNF n R] {φ : R} : (negToCNF φ).models = (models φ)ᶜ