Substitution

This file defines operations on [PropForm] and [PropFun] for substituting the variables in a formula with other variables, or in general with other formulas.

The main definitions are:

• [PropForm.subst], [PropFun.subst]
• [PropForm.substOne], [PropFun.substOne]
• [PropForm.map], [PropFun.map]
• [PropForm.pmap], [PropFun.pmap]

subst

def Trestle.Model.PropAssignment.subst {ν : Type u_1} {ν' : Type u_2} (f : ν → PropFun ν') (τ : PropAssignment ν') : PropAssignment ν

Equations

• Trestle.Model.PropAssignment.subst f τ v = decide (τ ⊨ f v)

PropForm

@[reducible]

def Trestle.Model.PropForm.subst {ν₁ : Type u_1} {ν₂ : Type u_2} (p : PropForm ν₁) (f : ν₁ → PropForm ν₂) : PropForm ν₂

Equations

• (Trestle.Model.PropForm.var l).subst f = f l
• Trestle.Model.PropForm.tr.subst f = Trestle.Model.PropForm.tr
• Trestle.Model.PropForm.fls.subst f = Trestle.Model.PropForm.fls
• φ.neg.subst f = (φ.subst f).neg
• (φ₁.conj φ₂).subst f = (φ₁.subst f).conj (φ₂.subst f)
• (φ₁.disj φ₂).subst f = (φ₁.subst f).disj (φ₂.subst f)
• (φ₁.impl φ₂).subst f = (φ₁.subst f).impl (φ₂.subst f)
• (φ₁.biImpl φ₂).subst f = (φ₁.subst f).biImpl (φ₂.subst f)

theorem Trestle.Model.PropForm.subst_assoc {ν₁ : Type u_3} {ν₂ : Type u_2} {ν₃ : Type u_1} (f₁ : ν₁ → PropForm ν₂) (f₂ : ν₂ → PropForm ν₃) (φ : PropForm ν₁) : (φ.subst f₁).subst f₂ = φ.subst fun (v : ν₁) => (f₁ v).subst f₂

@[simp]

theorem Trestle.Model.PropForm.vars_subst {ν₁ : Type u_1} {ν₂ : Type u_2} (f : ν₁ → PropForm ν₂) (φ : PropForm ν₁) [DecidableEq ν₁] [DecidableEq ν₂] : (φ.subst f).vars = φ.vars.biUnion fun (v1 : ν₁) => (f v1).vars

@[simp]

theorem Trestle.Model.PropForm.satisfies_subst {ν₁ : Type u_1} {ν₂ : Type u_2} {φ : PropForm ν₁} {f : ν₁ → PropForm ν₂} {τ : PropAssignment ν₂} : τ ⊨ φ.subst f ↔ PropAssignment.subst (fun (x : ν₁) => ⟦f x⟧) τ ⊨ φ

theorem Trestle.Model.PropForm.subst_congr {ν₁ : Type u_1} {ν₂ : Type u_2} {φ₁ φ₂ : PropForm ν₁} (hφ : ⟦φ₁⟧ = ⟦φ₂⟧) (σ : ν₁ → PropForm ν₂) : ⟦φ₁.subst σ⟧ = ⟦φ₂.subst σ⟧

substOne

def Trestle.Model.PropForm.substOne {ν : Type u_1} [DecidableEq ν] (φ : PropForm ν) (v : ν) (ψ : PropForm ν) : PropForm ν

Equations

• φ.substOne v ψ = φ.subst fun (v' : ν) => if v' = v then ψ else Trestle.Model.PropForm.var v'

theorem Trestle.Model.PropForm.satisfies_substOne {ν : Type u_1} [DecidableEq ν] (ψ : PropForm ν) {φ : PropForm ν} {v : ν} {τ : PropAssignment ν} : τ ⊨ φ.substOne v ψ ↔ τ.set v (decide (τ ⊨ ψ)) ⊨ φ

theorem Trestle.Model.PropForm.substOne_congr {ν : Type u_1} [DecidableEq ν] {φ₁ φ₂ ψ₁ ψ₂ : PropForm ν} (v : ν) (hφ : ⟦φ₁⟧ = ⟦φ₂⟧) (hψ : ⟦ψ₁⟧ = ⟦ψ₂⟧) : ⟦φ₁.substOne v ψ₁⟧ = ⟦φ₂.substOne v ψ₂⟧

theorem Trestle.Model.PropForm.vars_substOne {ν : Type u_1} [DecidableEq ν] (φ : PropForm ν) (v : ν) (ψ : PropForm ν) : (φ.substOne v ψ).vars ⊆ φ.vars \ {v} ∪ ψ.vars

PropFun

def Trestle.Model.PropFun.substL {ν₁ : Type u_1} {ν₂ : Type u_2} (φ : PropFun ν₁) (f : ν₁ → PropForm ν₂) : PropFun ν₂

Equations

• φ.substL f = Quotient.lift (fun (x : Trestle.Model.PropForm ν₁) => ⟦x.subst f⟧) ⋯ φ

@[simp]

theorem Trestle.Model.PropFun.substL_distrib {ν₁ : Type u_2} {ν₂ : Type u_1} (f : ν₁ → PropForm ν₂) (v : ν₁) : (var v).substL f = ⟦f v⟧

@[simp]

theorem Trestle.Model.PropFun.substL_bot {ν₁ : Type u_2} {ν₂ : Type u_1} (f : ν₁ → PropForm ν₂) : ⊥.substL f = ⊥

@[simp]

theorem Trestle.Model.PropFun.substL_top {ν₁ : Type u_2} {ν₂ : Type u_1} (f : ν₁ → PropForm ν₂) : ⊤.substL f = ⊤

@[simp]

theorem Trestle.Model.PropFun.substL_disj {ν₁ : Type u_2} {ν₂ : Type u_1} (f : ν₁ → PropForm ν₂) (φ₁ φ₂ : PropFun ν₁) : (φ₁ ⊔ φ₂).substL f = φ₁.substL f ⊔ φ₂.substL f

@[simp]

theorem Trestle.Model.PropFun.substL_conj {ν₁ : Type u_2} {ν₂ : Type u_1} (f : ν₁ → PropForm ν₂) (φ₁ φ₂ : PropFun ν₁) : (φ₁ ⊓ φ₂).substL f = φ₁.substL f ⊓ φ₂.substL f

@[simp]

theorem Trestle.Model.PropFun.substL_neg {ν₁ : Type u_1} {ν₂ : Type u_2} (f : ν₁ → PropForm ν₂) {φ : PropFun ν₁} : φ.neg.substL f = (φ.substL f).neg

@[simp]

theorem Trestle.Model.PropFun.substL_compl {ν₁ : Type u_1} {ν₂ : Type u_2} (f : ν₁ → PropForm ν₂) {φ : PropFun ν₁} : φᶜ.substL f = (φ.substL f)ᶜ

@[simp]

theorem Trestle.Model.PropFun.satisfies_substL {ν₁ : Type u_1} {ν₂ : Type u_2} {φ : PropFun ν₁} {f : ν₁ → PropForm ν₂} {τ : PropAssignment ν₂} : τ ⊨ φ.substL f ↔ PropAssignment.subst (fun (x : ν₁) => ⟦f x⟧) τ ⊨ φ

noncomputable def Trestle.Model.PropFun.subst {ν₁ : Type u_1} {ν₂ : Type u_2} (φ : PropFun ν₁) (f : ν₁ → PropFun ν₂) : PropFun ν₂

Equations

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

@[simp]

theorem Trestle.Model.PropFun.satisfies_subst {ν₁ : Type u_1} {ν₂ : Type u_2} {φ : PropFun ν₁} {f : ν₁ → PropFun ν₂} {τ : PropAssignment ν₂} : τ ⊨ φ.subst f ↔ PropAssignment.subst f τ ⊨ φ

@[simp]

theorem Trestle.Model.PropFun.subst_distrib {ν₁ : Type u_2} {ν₂ : Type u_1} (f : ν₁ → PropFun ν₂) (v : ν₁) : subst ⟦PropForm.var v⟧ f = f v

@[simp]

theorem Trestle.Model.PropFun.subst_bot {ν₁ : Type u_2} {ν₂ : Type u_1} (f : ν₁ → PropFun ν₂) : ⊥.subst f = ⊥

@[simp]

theorem Trestle.Model.PropFun.subst_top {ν₁ : Type u_2} {ν₂ : Type u_1} (f : ν₁ → PropFun ν₂) : ⊤.subst f = ⊤

@[simp]

theorem Trestle.Model.PropFun.subst_disj {ν₁ : Type u_2} {ν₂ : Type u_1} (φ₁ φ₂ : PropFun ν₁) (f : ν₁ → PropFun ν₂) : (φ₁ ⊔ φ₂).subst f = φ₁.subst f ⊔ φ₂.subst f

@[simp]

theorem Trestle.Model.PropFun.subst_conj {ν₁ : Type u_2} {ν₂ : Type u_1} (φ₁ φ₂ : PropFun ν₁) (f : ν₁ → PropFun ν₂) : (φ₁ ⊓ φ₂).subst f = φ₁.subst f ⊓ φ₂.subst f

@[simp]

theorem Trestle.Model.PropFun.subst_neg {ν₁ : Type u_2} {ν₂ : Type u_1} (φ : PropFun ν₁) (f : ν₁ → PropFun ν₂) : φ.neg.subst f = (φ.subst f).neg

@[simp]

theorem Trestle.Model.PropFun.subst_compl {ν₁ : Type u_2} {ν₂ : Type u_1} (φ : PropFun ν₁) (f : ν₁ → PropFun ν₂) : φᶜ.subst f = (φ.subst f)ᶜ

theorem Trestle.Model.PropFun.semVars_subst {ν₁ : Type u_1} {ν₂ : Type u_2} [DecidableEq ν₁] [DecidableEq ν₂] {φ : PropFun ν₁} {f : ν₁ → PropFun ν₂} : (φ.subst f).semVars ⊆ φ.semVars.biUnion fun (v1 : ν₁) => (f v1).semVars

def Trestle.Model.PropFun.substOne {ν : Type u_1} [DecidableEq ν] (ψ : PropFun ν) (v : ν) (φ : PropFun ν) : PropFun ν

Equations

• ψ.substOne v φ = Quotient.lift (fun (ψ : Trestle.Model.PropForm ν) => Quotient.lift (fun (φ : Trestle.Model.PropForm ν) => ⟦ψ.substOne v φ⟧) ⋯ φ) ⋯ ψ

@[simp]

theorem Trestle.Model.PropFun.satisfies_substOne {ν : Type u_1} [DecidableEq ν] {φ ψ : PropFun ν} {v : ν} {τ : PropAssignment ν} : τ ⊨ ψ.substOne v φ ↔ τ.set v (decide (τ ⊨ φ)) ⊨ ψ

map

def Trestle.Model.PropForm.map {ν₁ : Type u_1} {ν₂ : Type u_2} (f : ν₁ → ν₂) : PropForm ν₁ → PropForm ν₂

Equations

• Trestle.Model.PropForm.map f (Trestle.Model.PropForm.var l) = Trestle.Model.PropForm.var (f l)
• Trestle.Model.PropForm.map f Trestle.Model.PropForm.tr = Trestle.Model.PropForm.tr
• Trestle.Model.PropForm.map f Trestle.Model.PropForm.fls = Trestle.Model.PropForm.fls
• Trestle.Model.PropForm.map f φ.neg = (Trestle.Model.PropForm.map f φ).neg
• Trestle.Model.PropForm.map f (φ₁.conj φ₂) = (Trestle.Model.PropForm.map f φ₁).conj (Trestle.Model.PropForm.map f φ₂)
• Trestle.Model.PropForm.map f (φ₁.disj φ₂) = (Trestle.Model.PropForm.map f φ₁).disj (Trestle.Model.PropForm.map f φ₂)
• Trestle.Model.PropForm.map f (φ₁.impl φ₂) = (Trestle.Model.PropForm.map f φ₁).impl (Trestle.Model.PropForm.map f φ₂)
• Trestle.Model.PropForm.map f (φ₁.biImpl φ₂) = (Trestle.Model.PropForm.map f φ₁).biImpl (Trestle.Model.PropForm.map f φ₂)

@[simp]

theorem Trestle.Model.PropForm.vars_map {ν₁ : Type u_1} {ν₂ : Type u_2} (f : ν₁ → ν₂) (φ : PropForm ν₁) [DecidableEq ν₁] [DecidableEq ν₂] : (map f φ).vars = Finset.image f φ.vars

theorem Trestle.Model.PropForm.satisfies_map {ν₁ : Type u_1} {ν₂ : Type u_2} {φ : PropForm ν₁} {f : ν₁ → ν₂} {τ : PropAssignment ν₂} : τ ⊨ map f φ ↔ PropAssignment.map f τ ⊨ φ

@[simp]

theorem Trestle.Model.PropForm.semVars_map {ν₁ : Type u_1} {ν₂ : Type u_2} [DecidableEq ν₁] [DecidableEq ν₂] [Fintype ν₁] {f : ν₁ → ν₂} (hf : Function.Injective f) (φ : PropForm ν₁) : PropFun.semVars ⟦map f φ⟧ = Finset.map { toFun := f, inj' := hf } (PropFun.semVars ⟦φ⟧)

def Trestle.Model.PropFun.map {ν₁ : Type u_1} {ν₂ : Type u_2} (f : ν₁ → ν₂) (φ : PropFun ν₁) : PropFun ν₂

Equations

• Trestle.Model.PropFun.map f φ = Quotient.lift (fun (x : Trestle.Model.PropForm ν₁) => ⟦Trestle.Model.PropForm.map f x⟧) ⋯ φ

@[simp]

theorem Trestle.Model.PropFun.satisfies_map {ν₁ : Type u_1} {ν₂ : Type u_2} {φ : PropFun ν₁} {f : ν₁ → ν₂} {τ : PropAssignment ν₂} : τ ⊨ map f φ ↔ PropAssignment.map f τ ⊨ φ

theorem Trestle.Model.PropFun.semVars_map {ν₁ : Type u_1} {ν₂ : Type u_2} [DecidableEq ν₁] [DecidableEq ν₂] [Fintype ν₁] (f : ν₁ → ν₂) (φ : PropFun ν₁) (hf : Function.Injective f) : (map f φ).semVars = Finset.map { toFun := f, inj' := hf } φ.semVars

@[simp]

theorem Trestle.Model.PropFun.map_var {ν₁ : Type u_2} {ν₂ : Type u_1} (f : ν₁ → ν₂) (v : ν₁) : map f (var v) = var (f v)

@[simp]

theorem Trestle.Model.PropFun.map_tr {ν₁ : Type u_2} {ν₂ : Type u_1} (f : ν₁ → ν₂) : map f ⊤ = ⊤

@[simp]

theorem Trestle.Model.PropFun.map_fls {ν₁ : Type u_2} {ν₂ : Type u_1} (f : ν₁ → ν₂) : map f ⊥ = ⊥

@[simp]

theorem Trestle.Model.PropFun.map_neg {ν₁ : Type u_2} {ν₂ : Type u_1} (f : ν₁ → ν₂) (φ : PropFun ν₁) : map f φᶜ = (map f φ)ᶜ

@[simp]

theorem Trestle.Model.PropFun.map_conj {ν₁ : Type u_2} {ν₂ : Type u_1} (f : ν₁ → ν₂) (φ₁ φ₂ : PropFun ν₁) : map f (φ₁ ⊓ φ₂) = map f φ₁ ⊓ map f φ₂

@[simp]

theorem Trestle.Model.PropFun.map_disj {ν₁ : Type u_2} {ν₂ : Type u_1} (f : ν₁ → ν₂) (φ₁ φ₂ : PropFun ν₁) : map f (φ₁ ⊔ φ₂) = map f φ₁ ⊔ map f φ₂

@[simp]

theorem Trestle.Model.PropFun.map_impl {ν₁ : Type u_2} {ν₂ : Type u_1} (f : ν₁ → ν₂) (φ₁ φ₂ : PropFun ν₁) : map f (φ₁ ⇨ φ₂) = map f φ₁ ⇨ map f φ₂

@[simp]

theorem Trestle.Model.PropFun.map_biImpl {ν₁ : Type u_2} {ν₂ : Type u_1} (f : ν₁ → ν₂) (φ₁ φ₂ : PropFun ν₁) : map f ((fun (φ₁ φ₂ : PropFun ν₁) => (φ₁ ⇨ φ₂) ⊓ (φ₂ ⇨ φ₁)) φ₁ φ₂) = (fun (φ₁ φ₂ : PropFun ν₂) => (φ₁ ⇨ φ₂) ⊓ (φ₂ ⇨ φ₁)) (map f φ₁) (map f φ₂)