Trestle.Model.PropAssn

Propositional assignments #

source

def Trestle.Model.PropAssignment (ν : Type u) :

Type u

A (total) assignment of truth values to propositional variables.

Equations

Trestle.Model.PropAssignment ν = (ν → Bool)

Instances For

source

instance Trestle.Model.PropAssignment.instInhabited {ν : Type u_1} :

Inhabited (PropAssignment ν)

Equations

Trestle.Model.PropAssignment.instInhabited = inferInstanceAs (Inhabited (ν → Bool))

source

instance Trestle.Model.PropAssignment.instDecidableEqOfFintype {V : Type u_1} [DecidableEq V] [Fintype V] :

DecidableEq (PropAssignment V)

Equations

Trestle.Model.PropAssignment.instDecidableEqOfFintype = inferInstanceAs (DecidableEq (V → Bool))

source

instance Trestle.Model.PropAssignment.instFintypeOfDecidableEq {V : Type u_1} [DecidableEq V] [Fintype V] :

Fintype (PropAssignment V)

Equations

Trestle.Model.PropAssignment.instFintypeOfDecidableEq = inferInstanceAs (Fintype (V → Bool))

source

theorem Trestle.Model.PropAssignment.ext {ν : Type u_1} (v1 v2 : PropAssignment ν) (h : ∀ (x : ν), v1 x = v2 x) :

v1 = v2

source

theorem Trestle.Model.PropAssignment.ext_iff {ν : Type u_1} {v1 v2 : PropAssignment ν} :

v1 = v2 ↔ ∀ (x : ν), v1 x = v2 x

source

def Trestle.Model.PropAssignment.set {ν : Type u_1} [DecidableEq ν] (τ : PropAssignment ν) (x : ν) (v : Bool) :

PropAssignment ν

Equations

τ.set x v y = if y = x then v else τ y

Instances For

source

@[simp]

theorem Trestle.Model.PropAssignment.set_get {ν : Type u_1} [DecidableEq ν] (τ : PropAssignment ν) (x : ν) (v : Bool) :

τ.set x v x = v

source

@[simp]

theorem Trestle.Model.PropAssignment.set_get_of_ne {ν : Type u_1} [DecidableEq ν] {x y : ν} (τ : PropAssignment ν) (v : Bool) :

x ≠ y → τ.set x v y = τ y

source

@[simp]

theorem Trestle.Model.PropAssignment.set_set {ν : Type u_1} [DecidableEq ν] (τ : PropAssignment ν) (x : ν) (v v' : Bool) :

(τ.set x v).set x v' = τ.set x v'

source

@[simp]

theorem Trestle.Model.PropAssignment.set_same {ν : Type u_1} [DecidableEq ν] (τ : PropAssignment ν) (x : ν) :

τ.set x (τ x) = τ

source

theorem Trestle.Model.PropAssignment.set_comm {ν : Type u_1} [DecidableEq ν] (τ : PropAssignment ν) (x₁ : ν) (b₁ : Bool) (x₂ : ν) (b₂ : Bool) (h : x₁ ≠ x₂) :

(τ.set x₂ b₂).set x₁ b₁ = (τ.set x₁ b₁).set x₂ b₂

source

def Trestle.Model.PropAssignment.setMany {ν : Type u_1} [DecidableEq ν] (τ : PropAssignment ν) (xs : Finset ν) (τ' : PropAssignment ν) :

PropAssignment ν

Assignment which agrees with τ' on xs but τ everywhere else.

Equations

τ.setMany xs τ' v = if v ∈ xs then τ' v else τ v

Instances For

source

@[simp]

theorem Trestle.Model.PropAssignment.setMany_mem {ν : Type u_1} [DecidableEq ν] (τ : PropAssignment ν) {v : ν} (xs : Finset ν) (τ' : PropAssignment ν) (h : v ∈ xs) :

τ.setMany xs τ' v = τ' v

source

@[simp]

theorem Trestle.Model.PropAssignment.setMany_not_mem {ν : Type u_1} [DecidableEq ν] (τ : PropAssignment ν) {v : ν} (xs : Finset ν) (τ' : PropAssignment ν) (h : v ∉ xs) :

τ.setMany xs τ' v = τ v

source

@[simp]

theorem Trestle.Model.PropAssignment.setMany_same {ν : Type u_1} [DecidableEq ν] (τ : PropAssignment ν) (xs : Finset ν) :

τ.setMany xs τ = τ

source

@[simp]

theorem Trestle.Model.PropAssignment.setMany_setMany {ν : Type u_1} [DecidableEq ν] (τ : PropAssignment ν) (xs₁ : Finset ν) (τ₁ : PropAssignment ν) (xs₂ : Finset ν) (τ₂ : PropAssignment ν) :

(τ.setMany xs₁ τ₁).setMany xs₂ τ₂ = τ.setMany (xs₁ ∪ xs₂) (τ₁.setMany xs₂ τ₂)

source

theorem Trestle.Model.PropAssignment.setMany_union {ν : Type u_1} [DecidableEq ν] (τ : PropAssignment ν) (xs₁ xs₂ : Finset ν) (τ' : PropAssignment ν) :

τ.setMany (xs₁ ∪ xs₂) τ' = (τ.setMany xs₁ τ').setMany xs₂ τ'

source

@[simp]

theorem Trestle.Model.PropAssignment.setMany_singleton {ν : Type u_1} [DecidableEq ν] (τ : PropAssignment ν) (v : ν) (τ' : PropAssignment ν) :

τ.setMany {v} τ' = τ.set v (τ' v)

source

theorem Trestle.Model.PropAssignment.set_setMany_comm {ν : Type u_1} [DecidableEq ν] (τ : PropAssignment ν) (xs : Finset ν) (τ' : PropAssignment ν) (v : ν) (b : Bool) (h : v ∉ xs) :

(τ.setMany xs τ').set v b = (τ.set v b).setMany xs τ'

source

def Trestle.Model.PropAssignment.agreeOn {ν : Type u_1} (X : Set ν) (σ₁ σ₂ : PropAssignment ν) :

Prop

Equations

Trestle.Model.PropAssignment.agreeOn X σ₁ σ₂ = ∀ x ∈ X, σ₁ x = σ₂ x

Instances For

source

theorem Trestle.Model.PropAssignment.agreeOn_refl {ν : Type u_1} (X : Set ν) (σ : PropAssignment ν) :

agreeOn X σ σ

source

theorem Trestle.Model.PropAssignment.agreeOn.symm {α✝ : Type u_1} {X : Set α✝} {σ₁ σ₂ : PropAssignment α✝} :

agreeOn X σ₁ σ₂ → agreeOn X σ₂ σ₁

source

theorem Trestle.Model.PropAssignment.agreeOn.trans {α✝ : Type u_1} {X : Set α✝} {σ₁ σ₂ σ₃ : PropAssignment α✝} :

agreeOn X σ₁ σ₂ → agreeOn X σ₂ σ₃ → agreeOn X σ₁ σ₃

source

theorem Trestle.Model.PropAssignment.agreeOn.subset {α✝ : Type u_1} {X Y : Set α✝} {σ₁ σ₂ : PropAssignment α✝} :

X ⊆ Y → agreeOn Y σ₁ σ₂ → agreeOn X σ₁ σ₂

source

theorem Trestle.Model.PropAssignment.agreeOn_empty {ν : Type u_1} (σ₁ σ₂ : PropAssignment ν) :

agreeOn ∅ σ₁ σ₂

source

theorem Trestle.Model.PropAssignment.agreeOn_set_of_not_mem {ν : Type u_1} [DecidableEq ν] {x : ν} {X : Set ν} (σ : PropAssignment ν) (v : Bool) :

x ∉ X → agreeOn X (σ.set x v) σ

source

theorem Trestle.Model.PropAssignment.agreeOn_setMany {ν : Type u_1} (τ : PropAssignment ν) [DecidableEq ν] (xs : Finset ν) (τ' : PropAssignment ν) :

agreeOn (↑xs) (τ.setMany xs τ') τ'

source

theorem Trestle.Model.PropAssignment.agreeOn_setMany_of_disjoint {ν : Type u_1} (τ : PropAssignment ν) [DecidableEq ν] (xs : Set ν) (xs' : Finset ν) (τ' : PropAssignment ν) (h : Disjoint xs ↑xs') :

agreeOn xs (τ.setMany xs' τ') τ

source

theorem Trestle.Model.PropAssignment.agreeOn_setMany_compl {ν : Type u_1} (τ : PropAssignment ν) [DecidableEq ν] (xs : Finset ν) (τ' : PropAssignment ν) :

agreeOn (↑xs)ᶜ (τ.setMany xs τ') τ

source

@[reducible, inline]

abbrev Trestle.Model.PropAssignment.map {ν₂ : Type u_1} {ν₁ : Type u_2} (f : ν₂ → ν₁) (τ : PropAssignment ν₁) :

PropAssignment ν₂

Equations

Trestle.Model.PropAssignment.map f τ = τ ∘ f

Instances For

source

@[simp]

theorem Trestle.Model.PropAssignment.get_map {ν₂✝ : Type u_1} {ν✝ : Type u_2} {f : ν₂✝ → ν✝} {τ : PropAssignment ν✝} {v : ν₂✝} :

map f τ v = τ (f v)

source

@[simp]

theorem Trestle.Model.PropAssignment.map_set {ν₁ : Type u_1} {ν₂ : Type u_2} {v : ν₂} {b : Bool} [DecidableEq ν₁] [DecidableEq ν₂] (f : ν₂ → ν₁) (τ : PropAssignment ν₁) (finj : Function.Injective f) :

map f (τ.set (f v) b) = (map f τ).set v b

source

theorem Trestle.Model.PropAssignment.map_eq_map {ν : Type u_1} {ν₁ : Type u_2} {ν₂ : Type u_3} (f : ν → ν₁) (τ : PropAssignment ν₁) (f' : ν → ν₂) (τ' : PropAssignment ν₂) :

map f τ = map f' τ' ↔ ∀ (v : ν), τ (f v) = τ' (f' v)

source

def Trestle.Model.PropAssignment.pmap {ν₂ : Type u_1} {ν₁ : Type u_2} {vs : Set ν₂} [DecidablePred fun (x : ν₂) => x ∈ vs] [DecidableEq ν₂] (f : ↑vs → ν₁) (τ : PropAssignment ν₁) :

PropAssignment ν₂

Equations

Trestle.Model.PropAssignment.pmap f τ v = if h : v ∈ vs then τ (f ⟨v, h⟩) else false

Instances For

source

def Trestle.Model.PropAssignment.exists_preimage {ν₂ : Type u_1} {ν₁ : Type u_2} [DecidableEq ν₂] (f : ν₁ ↪ ν₂) (τ : PropAssignment ν₁) :

∃ (σ : PropAssignment ν₂), τ = map (⇑f) σ

Equations

⋯ = ⋯

Instances For