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

• 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.

Model

@[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)

Literal

@[unbox]

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

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

• var : Fin n
• isPos : Bool

def Validator.Formula.instDecidableEqLiteral.decEq {n✝ : ℕ} (x✝ x✝¹ : Literal n✝) : Decidable (x✝ = x✝¹)

Equations

• Validator.Formula.instDecidableEqLiteral.decEq { var := a, isPos := a_1 } { var := b, isPos := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

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

Equations

• Validator.Formula.instDecidableEqLiteral = Validator.Formula.instDecidableEqLiteral.decEq

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

Equations

• { var := i, isPos := true }.models = {M : Validator.Formula.Model n | M i}
• { var := i, isPos := false }.models = {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.var ↔ l.isPos = true)

def Validator.Formula.Literal.negate {n : ℕ} (l : Literal n) : Literal n

Equations

• l.negate = { var := l.var, isPos := !l.isPos }

@[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.var = l'.var ↔ 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_nil {n : ℕ} : models [] = ∅

@[simp]

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

def Validator.Formula.Clause.vars {n : ℕ} (γ : Clause n) : STRIPS.VarSet n

Equations

• γ.vars = STRIPS.VarSet.ofList (List.map Validator.Formula.Literal.var γ)

@[simp]

theorem Validator.Formula.Clause.mem_vars {n : ℕ} (γ : Clause n) {i : Fin n} : i ∈ γ.vars ↔ ∃ l ∈ γ, l.var = i

@[simp]

theorem Validator.Formula.Clause.vars_cons {n : ℕ} (γ : Clause n) {l : Literal n} : vars (l :: γ) = STRIPS.VarSet.insert l.var γ.vars

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_nil {n : ℕ} : models [] = Set.univ

@[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) : STRIPS.VarSet n

Equations

• δ.vars = STRIPS.VarSet.ofList (List.map Validator.Formula.Literal.var δ)

@[simp]

theorem Validator.Formula.Cube.mem_vars {n : ℕ} (δ : Cube n) (i : Fin n) : i ∈ δ.vars ↔ ∃ l ∈ δ, i = l.var

@[simp]

theorem Validator.Formula.Cube.vars_cons {n : ℕ} (δ : Cube n) {l : Literal n} : vars (l :: δ) = STRIPS.VarSet.insert l.var δ.vars

theorem Validator.Formula.Cube.vars_append {n : ℕ} (δ δ' : Cube n) : (δ ++ δ').vars = δ.vars ∪ δ'.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 | ∀ γ ∈ φ, M ∈ γ.models}

@[simp]

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

@[simp]

theorem Validator.Formula.CNF.models_nil {n : ℕ} : models [] = Set.univ

@[simp]

theorem Validator.Formula.CNF.models_cons {n : ℕ} (φ : CNF n) {γ : Clause n} : models (γ :: φ) = γ.models ∩ φ.models

@[simp]

theorem Validator.Formula.CNF.models_append {n : ℕ} (φ ψ : CNF n) : (φ ++ ψ).models = φ.models ∩ ψ.models

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

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

Equations

• φ.vars = List.foldr (fun (γ : Validator.Formula.Clause n) (V : STRIPS.VarSet n) => V ∪ γ.vars) ∅ φ

@[simp]

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

@[simp]

theorem Validator.Formula.CNF.vars_cons {n : ℕ} {γ : Clause n} {φ : CNF n} : vars (γ :: φ) = γ.vars ∪ φ.vars

@[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 | ∃ δ ∈ φ, M ∈ δ.models}

@[simp]

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

@[simp]

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

PartialModel

structure Validator.Formula.PartialModel (n : ℕ) : Type

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

• pos : STRIPS.VarSet n
• neg : STRIPS.VarSet n
• disjoint : self.pos ∩ self.neg = ∅

@[implicit_reducible]

instance Validator.Formula.instDecidableEqPartialModel {n✝ : ℕ} : DecidableEq (PartialModel n✝)

Equations

• Validator.Formula.instDecidableEqPartialModel = Validator.Formula.instDecidableEqPartialModel.decEq

def Validator.Formula.instDecidableEqPartialModel.decEq {n✝ : ℕ} (x✝ x✝¹ : PartialModel n✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Validator.Formula.PartialModel.instMembershipLiteral {n : ℕ} : Membership (Literal n) (PartialModel n)

Equations

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

@[simp]

theorem Validator.Formula.PartialModel.mem_def {n : ℕ} (M : PartialModel n) (x✝ : Literal n) : (x✝ ∈ M) = match x✝ with | { var := i, isPos := true } => i ∈ M.pos | { var := i, isPos := false } => i ∈ M.neg

theorem Validator.Formula.PartialModel.mem_iff {n : ℕ} (M : PartialModel n) (l : Literal n) : l ∈ M ↔ l.var ∈ M.pos ∧ l.isPos = true ∨ l.var ∈ M.neg ∧ ¬l.isPos = true

@[implicit_reducible]

instance Validator.Formula.PartialModel.instDecidableMemLiteral {n : ℕ} {l : Literal n} {M : PartialModel n} : Decidable (l ∈ M)

Equations

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

def Validator.Formula.PartialModel.vars {n : ℕ} (M : PartialModel n) : STRIPS.VarSet n

Equations

• M.vars = M.pos ∪ M.neg

theorem Validator.Formula.PartialModel.vars_eq {n : ℕ} (M : PartialModel n) : M.vars = M.pos ∪ M.neg

theorem Validator.Formula.PartialModel.mem_vars {n : ℕ} {i : Fin n} {M : PartialModel n} : i ∈ M.vars ↔ ∃ l ∈ M, l.var = i

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

All models corresponding to to partial model M.

Equations

• M.models = {M' : Validator.Formula.Model n | (∀ i ∈ M.pos, M' i) ∧ ∀ i ∈ M.neg, ¬M' i}

theorem Validator.Formula.PartialModel.mem_models' {n : ℕ} (M : PartialModel n) {M' : Model n} : M' ∈ M.models ↔ (∀ i ∈ M.pos, M' i) ∧ ∀ i ∈ M.neg, ¬M' i

theorem Validator.Formula.PartialModel.mem_models {n : ℕ} {M : PartialModel n} {M' : Model n} : M' ∈ M.models ↔ ∀ l ∈ M, M' ∈ l.models

theorem Validator.Formula.PartialModel.models_nonempty {n : ℕ} (M : PartialModel n) : Set.Nonempty M.models

theorem Validator.Formula.PartialModel.subset_models_of_mem {n : ℕ} {M : PartialModel n} {l : Literal n} : l ∈ M → M.models ⊆ l.models

def Validator.Formula.PartialModel.empty {n : ℕ} : PartialModel n

Equations

• Validator.Formula.PartialModel.empty = { pos := ∅, neg := ∅, disjoint := ⋯ }

@[simp]

theorem Validator.Formula.PartialModel.vars_empty {n : ℕ} : empty.vars = ∅

@[simp]

theorem Validator.Formula.PartialModel.models_empty {n : ℕ} : empty.models = Set.univ

def Validator.Formula.PartialModel.insert {n : ℕ} (M : PartialModel n) : Literal n → Option (PartialModel n)

Returns none if the negation of the literal already occurs in M

Equations

• M.insert { var := i, isPos := true } = if h : i ∈ M.neg then none else some { pos := STRIPS.VarSet.insert i M.pos, neg := M.neg, disjoint := ⋯ }
• M.insert { var := i, isPos := false } = if h : i ∈ M.pos then none else some { pos := M.pos, neg := STRIPS.VarSet.insert i M.neg, disjoint := ⋯ }

@[simp]

theorem Validator.Formula.PartialModel.insert_eq_none_iff {n : ℕ} {M : PartialModel n} {l : Literal n} : M.insert l = none ↔ l.negate ∈ M

@[simp]

theorem Validator.Formula.PartialModel.insert_eq_some_iff {n : ℕ} {M M' : PartialModel n} {l : Literal n} : M.insert l = some M' ↔ l.negate ∉ M ∧ ∀ (l' : Literal n), l' ∈ M' ↔ l' ∈ M ∨ l' = l

theorem Validator.Formula.PartialModel.vars_insert {n : ℕ} {M M' : PartialModel n} {l : Literal n} (h : M.insert l = some M') : M'.vars = STRIPS.VarSet.insert l.var M.vars

theorem Validator.Formula.PartialModel.models_insert {n : ℕ} {M M' : PartialModel n} {l : Literal n} : M.insert l = some M' → M'.models = M.models ∩ l.models

def Validator.Formula.PartialModel.foldl {α : Sort u_1} {n : ℕ} (f : α → Literal n → α) (init : α) (M : PartialModel n) : α

Equations

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

theorem Validator.Formula.PartialModel.foldl_cons {α : Type u_1} {n : ℕ} {M : PartialModel n} {f : Literal n → α} {a : α} : a ∈ foldl (fun (a : List α) (l : Literal n) => f l :: a) [] M ↔ ∃ l ∈ M, a = f l

def Validator.Formula.PartialModel.toCNF {n : ℕ} (M : PartialModel n) : CNF n

Equations

• M.toCNF = Validator.Formula.PartialModel.foldl (fun (φ : Validator.Formula.CNF n) (l : Validator.Formula.Literal n) => [l] :: φ) [] M

theorem Validator.Formula.PartialModel.mem_toCNF {n : ℕ} {M : PartialModel n} {γ : Clause n} : γ ∈ M.toCNF ↔ ∃ l ∈ M, γ = [l]

theorem Validator.Formula.PartialModel.models_toCNF {n : ℕ} {M : PartialModel n} : M.toCNF.models = M.models

def Validator.Formula.PartialModel.toCube {n : ℕ} (M : PartialModel n) : Cube n

Equations

• M.toCube = Validator.Formula.PartialModel.foldl (fun (δ : Validator.Formula.Cube n) (l : Validator.Formula.Literal n) => l :: δ) [] M

@[simp]

theorem Validator.Formula.PartialModel.vars_toCube {n : ℕ} {M : PartialModel n} : M.toCube.vars = M.vars

@[simp]

theorem Validator.Formula.PartialModel.models_toCube {n : ℕ} {M : PartialModel n} : M.toCube.models = M.models

def Validator.Formula.Cube.toPartialModel {n : ℕ} (δ : Cube n) : Option (PartialModel n)

Translate δ to a partial model. Returns none if δ is inconsistent.

Equations

• δ.toPartialModel = List.foldlM Validator.Formula.PartialModel.insert Validator.Formula.PartialModel.empty δ

@[simp]

theorem Validator.Formula.Cube.toPartialModel_eq_none_iff {n : ℕ} {δ : Cube n} : δ.toPartialModel = none ↔ δ.models = ∅

@[simp]

theorem Validator.Formula.Cube.models_toPartialModel {n : ℕ} {δ : Cube n} {M : PartialModel n} : δ.toPartialModel = some M → M.models = δ.models

Formula

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

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

• vars (φ : R) : STRIPS.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
• models_top : models (top n) = Set.univ

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

• bot : R
• vars_bot : vars (bot n) = ∅
• models_bot : models (bot n) = ∅

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

• consistent (φ : R) : Bool
• consistent_iff (φ : 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_iff (φ : 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_iff (δ : Cube n) (φ : R) : entails δ φ = true ↔ δ.models ⊆ models φ

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

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

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

• and : R → R → R
• models_and (φ ψ : 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.models_andList {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
• models_or (φ ψ : 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.models_orList {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 : PartialModel n → R
• vars_ofPartialModel (M : PartialModel n) : vars (ofPartialModel M) = M.vars
• models_ofPartialModel (M : PartialModel n) : models (ofPartialModel M) = M.models

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

• rename : Fin n → Fin n
• mono : StrictMonoOn self.rename ↑dom

theorem Validator.Formula.Renaming.ne {n : ℕ} {dom : STRIPS.VarSet n} {r : Renaming dom} (i : Fin n) : i ∈ dom → ∀ j ∈ dom, i ≠ j → r.rename i ≠ r.rename j

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

Equations

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

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

Equations

• Validator.Formula.Literal.rename r l = { var := r.rename l.var, isPos := l.isPos }

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

Equations

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

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

Equations

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

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

Equations

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

@[simp]

theorem Validator.Formula.CNF.mem_vars_rename {n : ℕ} {dom : STRIPS.VarSet n} {r : Renaming dom} {φ : CNF n} {i : Fin n} : i ∈ (rename r φ).vars ↔ ∃ j ∈ φ.vars, i = r.rename j

@[simp]

theorem Validator.Formula.CNF.models_rename {n : ℕ} {dom : STRIPS.VarSet n} {r : Renaming dom} {φ : CNF n} : (rename r φ).models = Model.rename r ⁻¹' φ.models

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

Equations

• Validator.Formula.VarSet.rename r V = V.map r.rename

@[simp]

theorem Validator.Formula.VarSet.mem_rename {n : ℕ} {dom : STRIPS.VarSet n} {r : Renaming dom} {V : STRIPS.VarSet n} {i : Fin n} : i ∈ rename r V ↔ ∃ j ∈ V, i = r.rename j

def Validator.Formula.PartialModel.rename {n : ℕ} {dom : STRIPS.VarSet n} (r : Renaming dom) (M : PartialModel n) (h1 : M.vars ⊆ dom) : PartialModel n

Equations

• Validator.Formula.PartialModel.rename r M h1 = { pos := Validator.Formula.VarSet.rename r M.pos, neg := Validator.Formula.VarSet.rename r M.neg, disjoint := ⋯ }

@[simp]

theorem Validator.Formula.PartialModel.mem_vars_rename {n : ℕ} {dom : STRIPS.VarSet n} {r : Renaming dom} {M : PartialModel n} {h1 : M.vars ⊆ dom} {i : Fin n} : i ∈ (rename r M h1).vars ↔ ∃ j ∈ M.vars, i = r.rename j

@[simp]

theorem Validator.Formula.PartialModel.models_rename {n : ℕ} {dom : STRIPS.VarSet n} {r : Renaming dom} {M : PartialModel n} {h1 : M.vars ⊆ dom} : (rename r M h1).models = Model.rename r ⁻¹' M.models

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

Renaming consistent with order

• rename (φ : R) {V : STRIPS.VarSet n} (f : Renaming V) (h1 : vars φ ⊆ V) : R
• vars_rename (φ : R) (V : STRIPS.VarSet n) (r : Renaming V) (h : vars φ ⊆ V) (i : Fin n) : i ∈ vars (rename φ r h) ↔ i ∈ r.rename '' ↑(vars φ)
• models_rename (φ : R) (V : STRIPS.VarSet n) (r : Renaming V) (h : vars φ ⊆ V) : models (rename φ r h) = Model.rename r ⁻¹' models φ

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

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

• toCNF : R → CNF n
• models_toCNF (φ : 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.models_disjunctionToCNF {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 Validator.Formula.Clause.neg (Validator.Formula.ToCNF.toCNF φ)

theorem Validator.Formula.ToCNF.models_negToDNF {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
• models_toDNF (φ : 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.models_conjunctionToDnF {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 Validator.Formula.Cube.neg (Validator.Formula.ToDNF.toDNF φ)

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