Documentation

Validator.StateSetFormalism.Mods

structure Validator.MODS (n : ℕ) :

vars : VarSet' n
mods : List (Formula.PartialModel self.vars)

Instances For

instance Validator.instDecidableEqMODS {n✝ : ℕ} :

DecidableEq (MODS n✝)

Equations

Validator.instDecidableEqMODS = Validator.instDecidableEqMODS.decEq

def Validator.instDecidableEqMODS.decEq {n✝ : ℕ} (x✝ x✝¹ : MODS n✝) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

instance Validator.instReprMODS {n✝ : ℕ} :

Repr (MODS n✝)

Equations

Validator.instReprMODS = { reprPrec := Validator.instReprMODS.repr }

def Validator.instReprMODS.repr {n✝ : ℕ} :

MODS n✝ → ℕ → Std.Format

Equations

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

Instances For

theorem Validator.Formula.PartialModel.models_nonempty {n : ℕ} {V : VarSet' n} (M : PartialModel V) :

Nonempty ↑M.models

theorem Validator.Formula.PartialModel.disjoint {n : ℕ} {V : VarSet' n} {M1 M2 : PartialModel V} {M : Model n} :

M ∈ M1.models → M ∈ M2.models → M1 = M2

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

Literal n → Bool

Equations

M.contains_literal (var, b) = (List.finRange (↑V).length).any fun (i : Fin (↑V).length) => decide ((↑V)[i] = var) && decide (M[i] = b)

Instances For

theorem Validator.Formula.PartialModel.contains_literal_iff {n : ℕ} {V : VarSet' n} (M : PartialModel V) (l : Literal n) :

M.contains_literal l = true ↔ ∃ (i : Fin (↑V).length), (↑V)[i] = l.1 ∧ M[i] = l.2

theorem Validator.Formula.PartialModel.mem_models_to_mem_literal_models {n : ℕ} {V : VarSet' n} {M : PartialModel V} {l : Literal n} {M' : Model n} :

M.contains_literal l = true → M' ∈ M.models → M' ∈ l.models

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

Equations

γ.isTrivial = (Validator.Formula.Clause.isTrivial_aux✝ (Vector.replicate n (false , false )) γ).contains (true , true )

Instances For

theorem Validator.Formula.Clause.isTrivial_iff {n : ℕ} {γ : Clause n} :

γ.isTrivial = true ↔ ∃ (x : Fin n), (x, true ) ∈ γ ∧ (x, false ) ∈ γ

def Validator.MODS.models {n : ℕ} (φ : MODS n) :

Formula.Models n

Equations

φ.models = {M : Validator.Formula.Model n | ∃ M' ∈ φ.mods, M ∈ M'.models}

Instances For

@[simp]

theorem Validator.MODS.mem_models {n : ℕ} {φ : MODS n} {M : Formula.Model n} :

M ∈ φ.models ↔ ∃ M' ∈ φ.mods, M ∈ M'.models

instance Validator.MODS.instFormula {n : ℕ} :

Formula n (MODS n)

Equations

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

instance Validator.MODS.instTop {n : ℕ} :

Formula.Top n (MODS n)

Equations

Validator.MODS.instTop = { top := sorry, top_correct := ⋯ }

instance Validator.MODS.instBot {n : ℕ} :

Formula.Bot n (MODS n)

Equations

Validator.MODS.instBot = { bot := sorry, bot_correct := ⋯ }

instance Validator.MODS.instClausalEntailment {n : ℕ} :

Formula.ClausalEntailment n (MODS n)

Equations

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

instance Validator.MODS.instImplicant {n : ℕ} :

Formula.Implicant n (MODS n)

Equations

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

instance Validator.MODS.instBoundedConjuction {n : ℕ} :

Formula.BoundedConjuction n (MODS n)

Equations

Validator.MODS.instBoundedConjuction = { and := fun (φ ψ : Validator.MODS n) => sorry, and_correct := ⋯ }

instance Validator.MODS.instSententialEntailment {n : ℕ} :

Formula.SententialEntailment n (MODS n)

Equations

Validator.MODS.instSententialEntailment = { entails := fun (φ ψ : Validator.MODS n) => sorry, entails_correct := ⋯ }

instance Validator.MODS.instOfPartialModel {n : ℕ} :

Formula.OfPartialModel n (MODS n)

Equations

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

instance Validator.MODS.instRename {n : ℕ} :

Formula.Rename n (MODS n)

Equations

Validator.MODS.instRename = { rename := sorry, rename_correct := ⋯ }

instance Validator.MODS.instToCNF {n : ℕ} :

Formula.ToCNF n (MODS n)

Equations

Validator.MODS.instToCNF = { toCNF := sorry, toCNF_correct := ⋯ }

instance Validator.MODS.instToDNF {n : ℕ} :

Formula.ToDNF n (MODS n)

Equations

Validator.MODS.instToDNF = { toDNF := sorry, toDNF_correct := ⋯ }