Linglib.Theories.Semantics.Dynamic.PLA.Basic

source

@[reducible, inline]

abbrev Semantics.Dynamic.PLA.VarIdx :

Type

Variable index: identifies a variable x_i

Equations

Semantics.Dynamic.PLA.VarIdx = ℕ

Instances For

source

@[reducible, inline]

abbrev Semantics.Dynamic.PLA.PronIdx :

Type

Pronoun index: identifies a pronoun p_i

Equations

Semantics.Dynamic.PLA.PronIdx = ℕ

Instances For

source

inductive Semantics.Dynamic.PLA.Term :

Type

Term: either a variable or a pronoun

var : VarIdx → Term
pron : PronIdx → Term

Instances For

source

@[implicit_reducible]

instance Semantics.Dynamic.PLA.instDecidableEqTerm :

DecidableEq Term

Equations

Semantics.Dynamic.PLA.instDecidableEqTerm = Semantics.Dynamic.PLA.instDecidableEqTerm.decEq

source

def Semantics.Dynamic.PLA.instDecidableEqTerm.decEq (x✝ x✝¹ : Term) :

Decidable (x✝ = x✝¹)

Equations

Semantics.Dynamic.PLA.instDecidableEqTerm.decEq (Semantics.Dynamic.PLA.Term.var a) (Semantics.Dynamic.PLA.Term.var b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Semantics.Dynamic.PLA.instDecidableEqTerm.decEq (Semantics.Dynamic.PLA.Term.var a) (Semantics.Dynamic.PLA.Term.pron a_1) = isFalse ⋯
Semantics.Dynamic.PLA.instDecidableEqTerm.decEq (Semantics.Dynamic.PLA.Term.pron a) (Semantics.Dynamic.PLA.Term.var a_1) = isFalse ⋯
Semantics.Dynamic.PLA.instDecidableEqTerm.decEq (Semantics.Dynamic.PLA.Term.pron a) (Semantics.Dynamic.PLA.Term.pron b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

source

def Semantics.Dynamic.PLA.instReprTerm.repr :

Term → ℕ → Std.Format

Equations

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

Instances For

source

@[implicit_reducible]

instance Semantics.Dynamic.PLA.instReprTerm :

Repr Term

Equations

Semantics.Dynamic.PLA.instReprTerm = { reprPrec := Semantics.Dynamic.PLA.instReprTerm.repr }

source

@[implicit_reducible]

instance Semantics.Dynamic.PLA.instHashableTerm :

Hashable Term

Equations

Semantics.Dynamic.PLA.instHashableTerm = { hash := Semantics.Dynamic.PLA.instHashableTerm.hash }

source

def Semantics.Dynamic.PLA.instHashableTerm.hash :

Term → UInt64

Equations

Semantics.Dynamic.PLA.instHashableTerm.hash (Semantics.Dynamic.PLA.Term.var a) = mixHash 0 (hash a)
Semantics.Dynamic.PLA.instHashableTerm.hash (Semantics.Dynamic.PLA.Term.pron a) = mixHash 1 (hash a)

Instances For

source

def Semantics.Dynamic.PLA.Term.pronouns :

Term → Finset PronIdx

Pronouns in a term (singleton or empty)

Equations

(Semantics.Dynamic.PLA.Term.var a).pronouns = ∅
(Semantics.Dynamic.PLA.Term.pron a).pronouns = {a}

Instances For

source

def Semantics.Dynamic.PLA.Term.vars :

Term → Finset VarIdx

Variables in a term

Equations

(Semantics.Dynamic.PLA.Term.var a).vars = {a}
(Semantics.Dynamic.PLA.Term.pron a).vars = ∅

Instances For

source

def Semantics.Dynamic.PLA.Term.isPron :

Term → Prop

Is this a pronoun?

Equations

(Semantics.Dynamic.PLA.Term.var a).isPron = False
(Semantics.Dynamic.PLA.Term.pron a).isPron = True

Instances For

source

@[implicit_reducible]

instance Semantics.Dynamic.PLA.Term.instDecidablePredIsPron :

DecidablePred isPron

Equations

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

source

theorem Semantics.Dynamic.PLA.Term.pronouns_var (i : VarIdx) :

(var i).pronouns = ∅

source

theorem Semantics.Dynamic.PLA.Term.pronouns_pron (i : PronIdx) :

(pron i).pronouns = {i}

source

def Semantics.Dynamic.PLA.termsPronouns (ts : List Term) :

Finset PronIdx

Pronouns in a list of terms via Finset.biUnion.

Equations

Semantics.Dynamic.PLA.termsPronouns ts = ts.toFinset.biUnion Semantics.Dynamic.PLA.Term.pronouns

Instances For

source

theorem Semantics.Dynamic.PLA.mem_termsPronouns (ts : List Term) (i : PronIdx) :

i ∈ termsPronouns ts ↔ ∃ t ∈ ts, i ∈ t.pronouns

source

theorem Semantics.Dynamic.PLA.termsPronouns_nil :

termsPronouns [] = ∅

source

inductive Semantics.Dynamic.PLA.Formula :

Type

PLA Formula

atom : String → List Term → Formula
neg : Formula → Formula
conj : Formula → Formula → Formula
exists_ : VarIdx → Formula → Formula

Instances For

source

@[implicit_reducible]

instance Semantics.Dynamic.PLA.instReprFormula :

Repr Formula

Equations

Semantics.Dynamic.PLA.instReprFormula = { reprPrec := Semantics.Dynamic.PLA.instReprFormula.repr }

source

def Semantics.Dynamic.PLA.instReprFormula.repr :

Formula → ℕ → Std.Format

Equations

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

Instances For

source

def Semantics.Dynamic.PLA.Formula.«term_⋀_» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

def Semantics.Dynamic.PLA.Formula.«term∼_» :

Lean.ParserDescr

Equations

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

Instances For

source

def Semantics.Dynamic.PLA.Formula.disj (φ ψ : Formula) :

Formula

Equations

(φ ⋁ ψ) = (∼(∼φ ⋀ ∼ψ))

Instances For

source

def Semantics.Dynamic.PLA.Formula.«term_⋁_» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

def Semantics.Dynamic.PLA.Formula.impl (φ ψ : Formula) :

Formula

Equations

(φ ⟶ ψ) = (∼(φ ⋀ ∼ψ))

Instances For

source

def Semantics.Dynamic.PLA.Formula.«term_⟶_» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

def Semantics.Dynamic.PLA.Formula.forall_ (i : VarIdx) (φ : Formula) :

Formula

Equations

Semantics.Dynamic.PLA.Formula.forall_ i φ = (∼Semantics.Dynamic.PLA.Formula.exists_ i (∼φ))

Instances For

source

def Semantics.Dynamic.PLA.Formula.domain :

Formula → Finset VarIdx

Domain: existentially bound variables

Equations

(Semantics.Dynamic.PLA.Formula.atom a a_1).domain = ∅
(∼a).domain = a.domain
(a ⋀ a_1).domain = a.domain ∪ a_1.domain
(Semantics.Dynamic.PLA.Formula.exists_ a a_1).domain = insert a a_1.domain

Instances For

source

def Semantics.Dynamic.PLA.Formula.range :

Formula → Finset PronIdx

Range: pronouns in formula (using biUnion for atoms)

Equations

(Semantics.Dynamic.PLA.Formula.atom a a_1).range = Semantics.Dynamic.PLA.termsPronouns a_1
(∼a).range = a.range
(a ⋀ a_1).range = a.range ∪ a_1.range
(Semantics.Dynamic.PLA.Formula.exists_ a a_1).range = a_1.range

Instances For

source

def Semantics.Dynamic.PLA.Formula.freeVars :

Formula → Finset VarIdx

Free variables in formula

Equations

(Semantics.Dynamic.PLA.Formula.atom a a_1).freeVars = a_1.toFinset.biUnion Semantics.Dynamic.PLA.Term.vars
(∼a).freeVars = a.freeVars
(a ⋀ a_1).freeVars = a.freeVars ∪ a_1.freeVars
(Semantics.Dynamic.PLA.Formula.exists_ a a_1).freeVars = a_1.freeVars.erase a

Instances For

source

theorem Semantics.Dynamic.PLA.Formula.range_atom (name : String) (ts : List Term) :

(atom name ts).range = termsPronouns ts

source

theorem Semantics.Dynamic.PLA.Formula.range_neg (φ : Formula) :

(∼φ).range = φ.range

source

theorem Semantics.Dynamic.PLA.Formula.range_conj (φ ψ : Formula) :

(φ ⋀ ψ).range = φ.range ∪ ψ.range

source

theorem Semantics.Dynamic.PLA.Formula.range_exists (i : VarIdx) (φ : Formula) :

(exists_ i φ).range = φ.range

source

theorem Semantics.Dynamic.PLA.Formula.pron_in_atom_range (name : String) (ts : List Term) (t : Term) (i : PronIdx) (ht : t ∈ ts) (hi : i ∈ t.pronouns) :

i ∈ (atom name ts).range

If a pronoun appears in a term in the formula's argument list, it's in the range

source

theorem Semantics.Dynamic.PLA.Formula.range_conj_left (φ ψ : Formula) :

φ.range ⊆ (φ ⋀ ψ).range

Range is monotonic over conjunction

source

theorem Semantics.Dynamic.PLA.Formula.range_conj_right (φ ψ : Formula) :

ψ.range ⊆ (φ ⋀ ψ).range

source

@[reducible, inline]

abbrev Semantics.Dynamic.PLA.Resolution :

Type

Resolution: maps pronouns to variables

Equations

Semantics.Dynamic.PLA.Resolution = (Semantics.Dynamic.PLA.PronIdx → Semantics.Dynamic.PLA.VarIdx)

Instances For

source

def Semantics.Dynamic.PLA.Term.resolve (ρ : Resolution) :

Term → Term

Apply resolution to a term

Equations

Instances For

source

def Semantics.Dynamic.PLA.Formula.resolve (ρ : Resolution) :

Formula → Formula

Apply resolution to a formula

Equations

Semantics.Dynamic.PLA.Formula.resolve ρ (Semantics.Dynamic.PLA.Formula.atom a a_1) = Semantics.Dynamic.PLA.Formula.atom a (List.map (Semantics.Dynamic.PLA.Term.resolve ρ) a_1)
Semantics.Dynamic.PLA.Formula.resolve ρ (∼a) = (∼Semantics.Dynamic.PLA.Formula.resolve ρ a)
Semantics.Dynamic.PLA.Formula.resolve ρ (a ⋀ a_1) = (Semantics.Dynamic.PLA.Formula.resolve ρ a ⋀ Semantics.Dynamic.PLA.Formula.resolve ρ a_1)
Semantics.Dynamic.PLA.Formula.resolve ρ (Semantics.Dynamic.PLA.Formula.exists_ a a_1) = Semantics.Dynamic.PLA.Formula.exists_ a (Semantics.Dynamic.PLA.Formula.resolve ρ a_1)

Instances For

source

theorem Semantics.Dynamic.PLA.Formula.resolve_preserves_domain (φ : Formula) (ρ : Resolution) :

(resolve ρ φ).domain = φ.domain

Observation 2 (@cite{dekker-2012} §2.1): Resolution preserves domain.

n(φ^ρ) = n(φ): resolving pronouns doesn't affect which variables are bound.

source

theorem Semantics.Dynamic.PLA.Term.resolve_no_pronouns (t : Term) (ρ : Resolution) :

(resolve ρ t).pronouns = ∅

Resolution removes all pronouns from a term

source

theorem Semantics.Dynamic.PLA.Formula.resolve_no_pronouns (φ : Formula) (ρ : Resolution) :

(resolve ρ φ).range = ∅

Observation 3 (@cite{dekker-2012} §2.1): Resolution eliminates all pronouns.

r(φ^ρ) = ∅: after resolution, the formula contains no pronouns.