@[reducible, inline]

abbrev Validator.Formula.Clause.IsHorn {n : ℕ} (γ : Clause n) : Prop

Equations

• γ.IsHorn = (List.countP Prod.snd γ ≤ 1)

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

Equations

• Validator.Formula.Cube.ofPartialModel M = (↑V).mapFinIdx fun (i : ℕ) (var : Fin n) (h : i < (↑V).length) => (var, M[i])

@[simp]

theorem Validator.Formula.Cube.models_ofPartialModel {n : ℕ} {V : VarSet' n} {M : PartialModel V} : (ofPartialModel M).models = M.models

def Validator.Formula.CNF.propagate_literal {n : ℕ} (φ : CNF n) (l : Literal n) : CNF n

Equations

• φ.propagate_literal l = List.map (List.filter fun (x : Validator.Formula.Literal n) => decide (x ≠ l.negate)) (List.filter (fun (γ : Validator.Formula.Clause n) => !List.contains γ l) φ)

theorem Validator.Formula.CNF.length_propagate_literal {n : ℕ} {φ : CNF n} {l : Literal n} : List.length (φ.propagate_literal l) ≤ List.length φ

theorem Validator.Formula.CNF.IsHorn_propagate_literal {n : ℕ} {φ : CNF n} {l : Literal n} : (∀ γ ∈ φ, γ.IsHorn) → ∀ γ ∈ φ.propagate_literal l, γ.IsHorn

theorem Validator.Formula.CNF.vars_propagate_literal {n : ℕ} {φ : CNF n} {l : Literal n} : (φ.propagate_literal l).vars ⊆ φ.vars \ {l.1}

@[simp]

theorem Validator.Formula.CNF.mem_propagate_literal {n : ℕ} {φ : CNF n} {l : Literal n} {γ : Clause n} : γ ∈ φ.propagate_literal l ↔ ∃ γ' ∈ φ, l ∉ γ' ∧ γ = List.filter (fun (x : Literal n) => decide (x ≠ l.negate)) γ'

theorem Validator.Formula.CNF.mem_models_propagate_literal {n : ℕ} {φ : CNF n} {l : Literal n} (M : Model n) : M ∈ l.models → (M ∈ (φ.propagate_literal l).models ↔ M ∈ φ.models)

structure Validator.Horn (n : ℕ) : Type

• vars : VarSet' n
• empty : Bool
• unit_literals : Formula.Cube n
• clauses : Formula.CNF n
• horn_prop (γ : Formula.Clause n) : γ ∈ self.clauses → γ.IsHorn
• clauses_prop (γ : Formula.Clause n) : γ ∈ self.clauses → 2 ≤ List.length γ
• subset_vars (i : Fin n) : i ∈ self.unit_literals.vars ∪ self.clauses.vars → i ∈ ↑self.vars
• vars_prop : self.unit_literals.vars ∩ self.clauses.vars = ∅

def Validator.instDecidableEqHorn.decEq {n✝ : ℕ} (x✝ x✝¹ : Horn n✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

instance Validator.instDecidableEqHorn {n✝ : ℕ} : DecidableEq (Horn n✝)

Equations

• Validator.instDecidableEqHorn = Validator.instDecidableEqHorn.decEq

def Validator.instReprHorn.repr {n✝ : ℕ} : Horn n✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Validator.instReprHorn {n✝ : ℕ} : Repr (Horn n✝)

Equations

• Validator.instReprHorn = { reprPrec := Validator.instReprHorn.repr }

def Validator.Horn.toCNF {n : ℕ} (φ : Horn n) : Formula.CNF n

Equations

• φ.toCNF = if φ.empty = true then [[]] else List.map (fun (l : Validator.Formula.Literal n) => [l]) φ.unit_literals ++ φ.clauses

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

Equations

• φ.models = φ.toCNF.models

theorem Validator.Horn.models_eq {n : ℕ} {φ : Horn n} : φ.models = if φ.empty = true then ∅ else φ.unit_literals.models ∩ φ.clauses.models

instance Validator.Horn.instFormula {n : ℕ} : Formula n (Horn n)

Equations

• Validator.Horn.instFormula = { vars := fun (φ : Validator.Horn n) => φ.vars, models := Validator.Horn.models, models_equiv_right := ⋯ }

@[irreducible]

def Validator.Horn.unit_propagate {n : ℕ} (φ : Horn n) (δ : Formula.Cube n) : Horn n

Equations

• One or more equations did not get rendered due to their size.
• φ.unit_propagate [] = φ

theorem Validator.Horn.models_unit_propagate {n : ℕ} {φ : Horn n} {δ : Formula.Cube n} : (φ.unit_propagate δ).models = φ.models ∩ δ.models

instance Validator.Horn.instTop {n : ℕ} : Formula.Top n (Horn n)

Equations

• One or more equations did not get rendered due to their size.

instance Validator.Horn.instBot {n : ℕ} : Formula.Bot n (Horn n)

Equations

• One or more equations did not get rendered due to their size.

instance Validator.Horn.instConsistency {n : ℕ} : Formula.Consistency n (Horn n)

Equations

• Validator.Horn.instConsistency = { consistent := fun (φ : Validator.Horn n) => decide (¬φ.empty = true ∧ φ.unit_literals.consistent = true), consistent_correct := ⋯ }

instance Validator.Horn.instClausalEntailment {n : ℕ} : Formula.ClausalEntailment n (Horn n)

Equations

• One or more equations did not get rendered due to their size.

instance Validator.Horn.instImplicant {n : ℕ} : Formula.Implicant n (Horn n)

Equations

• Validator.Horn.instImplicant = { entails := fun (δ : Validator.Formula.Cube n) (φ : Validator.Horn n) => sorry, entails_correct := ⋯ }

instance Validator.Horn.instSententialEntailment {n : ℕ} : Formula.SententialEntailment n (Horn n)

Equations

• One or more equations did not get rendered due to their size.

instance Validator.Horn.instBoundedConjuction {n : ℕ} : Formula.BoundedConjuction n (Horn n)

Equations

• One or more equations did not get rendered due to their size.

instance Validator.Horn.instOfPartialModel {n : ℕ} : Formula.OfPartialModel n (Horn n)

Equations

• One or more equations did not get rendered due to their size.

instance Validator.Horn.instRename {n : ℕ} : Formula.Rename n (Horn n)

Equations

• One or more equations did not get rendered due to their size.

instance Validator.Horn.instToCNF {n : ℕ} : Formula.ToCNF n (Horn n)

Equations

• Validator.Horn.instToCNF = { toCNF := Validator.Horn.toCNF, toCNF_correct := ⋯ }