Here we supply basic definitions, abbreviations, and lemmas about the syntax of BML.

source

inductive Lean4GlCoalgebras.Formula :

Type

Type of BML Formulas.

bottom : Formula
top : Formula
atom : ℕ → Formula
negAtom : ℕ → Formula
and : Formula → Formula → Formula
or : Formula → Formula → Formula
box : Formula → Formula
diamond : Formula → Formula

Instances For

source

@[implicit_reducible]

instance Lean4GlCoalgebras.instReprFormula :

Repr Formula

Equations

Lean4GlCoalgebras.instReprFormula = { reprPrec := Lean4GlCoalgebras.instReprFormula.repr }

source

def Lean4GlCoalgebras.instReprFormula.repr :

Formula → ℕ → Std.Format

Equations

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

Instances For

source

def Lean4GlCoalgebras.instDecidableEqFormula.decEq (x✝ x✝¹ : Formula) :

Decidable (x✝ = x✝¹)

Equations

One or more equations did not get rendered due to their size.
Lean4GlCoalgebras.instDecidableEqFormula.decEq Lean4GlCoalgebras.Formula.bottom Lean4GlCoalgebras.Formula.bottom = isTrue ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq Lean4GlCoalgebras.Formula.bottom Lean4GlCoalgebras.Formula.top = isFalse Lean4GlCoalgebras.instDecidableEqFormula.decEq._proof_1
Lean4GlCoalgebras.instDecidableEqFormula.decEq Lean4GlCoalgebras.Formula.bottom (at a) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq Lean4GlCoalgebras.Formula.bottom (na a) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq Lean4GlCoalgebras.Formula.bottom (a&a_1) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq Lean4GlCoalgebras.Formula.bottom (a v a_1) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq Lean4GlCoalgebras.Formula.bottom (□a) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq Lean4GlCoalgebras.Formula.bottom (◇a) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq Lean4GlCoalgebras.Formula.top Lean4GlCoalgebras.Formula.bottom = isFalse Lean4GlCoalgebras.instDecidableEqFormula.decEq._proof_8
Lean4GlCoalgebras.instDecidableEqFormula.decEq Lean4GlCoalgebras.Formula.top Lean4GlCoalgebras.Formula.top = isTrue ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq Lean4GlCoalgebras.Formula.top (at a) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq Lean4GlCoalgebras.Formula.top (na a) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq Lean4GlCoalgebras.Formula.top (a&a_1) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq Lean4GlCoalgebras.Formula.top (a v a_1) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq Lean4GlCoalgebras.Formula.top (□a) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq Lean4GlCoalgebras.Formula.top (◇a) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (at a) Lean4GlCoalgebras.Formula.bottom = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (at a) Lean4GlCoalgebras.Formula.top = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (at a) (at b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (at a) (na a_1) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (at a) (a_1&a_2) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (at a) (a_1 v a_2) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (at a) (□a_1) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (at a) (◇a_1) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (na a) Lean4GlCoalgebras.Formula.bottom = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (na a) Lean4GlCoalgebras.Formula.top = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (na a) (at a_1) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (na a) (na b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (na a) (a_1&a_2) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (na a) (a_1 v a_2) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (na a) (□a_1) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (na a) (◇a_1) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (a&a_1) Lean4GlCoalgebras.Formula.bottom = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (a&a_1) Lean4GlCoalgebras.Formula.top = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (a&a_1) (at a_2) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (a&a_1) (na a_2) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (a&a_1) (a_2 v a_3) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (a&a_1) (□a_2) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (a&a_1) (◇a_2) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (a v a_1) Lean4GlCoalgebras.Formula.bottom = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (a v a_1) Lean4GlCoalgebras.Formula.top = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (a v a_1) (at a_2) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (a v a_1) (na a_2) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (a v a_1) (a_2&a_3) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (a v a_1) (□a_2) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (a v a_1) (◇a_2) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (□a) Lean4GlCoalgebras.Formula.bottom = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (□a) Lean4GlCoalgebras.Formula.top = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (□a) (at a_1) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (□a) (na a_1) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (□a) (a_1&a_2) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (□a) (a_1 v a_2) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (□a) (□b) = if h : a = b then h ▸ have inst := Lean4GlCoalgebras.instDecidableEqFormula.decEq a a; isTrue ⋯ else isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (□a) (◇a_1) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (◇a) Lean4GlCoalgebras.Formula.bottom = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (◇a) Lean4GlCoalgebras.Formula.top = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (◇a) (at a_1) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (◇a) (na a_1) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (◇a) (a_1&a_2) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (◇a) (a_1 v a_2) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (◇a) (□a_1) = isFalse ⋯
Lean4GlCoalgebras.instDecidableEqFormula.decEq (◇a) (◇b) = if h : a = b then h ▸ have inst := Lean4GlCoalgebras.instDecidableEqFormula.decEq a a; isTrue ⋯ else isFalse ⋯

Instances For

source

@[implicit_reducible]

instance Lean4GlCoalgebras.instDecidableEqFormula :

DecidableEq Formula

Equations

Lean4GlCoalgebras.instDecidableEqFormula = Lean4GlCoalgebras.instDecidableEqFormula.decEq

source

@[reducible, inline]

abbrev Lean4GlCoalgebras.Sequent :

Type

A sequent is a finite set of formulas, read disjunctively.

Equations

Lean4GlCoalgebras.Sequent = Finset Lean4GlCoalgebras.Formula

Instances For

source

def Lean4GlCoalgebras.Formula.termAt_ :

Lean.ParserDescr

Auxiliary declaration used in the GL coalgebra development.

Equations

Lean4GlCoalgebras.Formula.termAt_ = Lean.ParserDescr.node `Lean4GlCoalgebras.Formula.termAt_ 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "at") (Lean.ParserDescr.cat `term 70))

Instances For

source

def Lean4GlCoalgebras.Formula.termNa_ :

Lean.ParserDescr

Auxiliary declaration used in the GL coalgebra development.

Equations

Lean4GlCoalgebras.Formula.termNa_ = Lean.ParserDescr.node `Lean4GlCoalgebras.Formula.termNa_ 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "na") (Lean.ParserDescr.cat `term 70))

Instances For

source

def Lean4GlCoalgebras.Formula.«term□_» :

Lean.ParserDescr

Auxiliary declaration used in the GL coalgebra development.

Equations

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

Instances For

source

def Lean4GlCoalgebras.Formula.«term◇_» :

Lean.ParserDescr

Auxiliary declaration used in the GL coalgebra development.

Equations

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

Instances For

source

def Lean4GlCoalgebras.Formula.«term_&_» :

Lean.TrailingParserDescr

Auxiliary declaration used in the GL coalgebra development.

Equations

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

Instances For

source

def Lean4GlCoalgebras.Formula.term_V_ :

Lean.TrailingParserDescr

Auxiliary declaration used in the GL coalgebra development.

Equations

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

Instances For

source

@[implicit_reducible]

instance Lean4GlCoalgebras.Formula.instBot :

Bot Formula

Equations

Lean4GlCoalgebras.Formula.instBot = { bot := Lean4GlCoalgebras.Formula.bottom }

source

@[implicit_reducible]

instance Lean4GlCoalgebras.Formula.instTop :

Top Formula

Equations

Lean4GlCoalgebras.Formula.instTop = { top := Lean4GlCoalgebras.Formula.top }

source

def Lean4GlCoalgebras.Formula.neg :

Formula → Formula

Negation of a BML Formula.

Equations

(~Lean4GlCoalgebras.Formula.bottom) = ⊤
(~Lean4GlCoalgebras.Formula.top) = ⊥
(~at a) = na a
(~na a) = at a
(~(a&a_1)) = (~a v ~a_1)
(~(a v a_1)) = (~a&~a_1)
(~□a) = ◇(~a)
(~◇a) = □(~a)

Instances For

source

def Lean4GlCoalgebras.Formula.«term~_» :

Lean.ParserDescr

Auxiliary declaration used in the GL coalgebra development.

Equations

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

Instances For

source

def Lean4GlCoalgebras.Formula.«term_↣_» :

Lean.TrailingParserDescr

Auxiliary declaration used in the GL coalgebra development.

Equations

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

Instances For

source

def Lean4GlCoalgebras.Formula.«term_⟷_» :

Lean.TrailingParserDescr

Auxiliary declaration used in the GL coalgebra development.

Equations

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

Instances For

source

def Lean4GlCoalgebras.Formula.«term⊡_» :

Lean.ParserDescr

Auxiliary declaration used in the GL coalgebra development.

Equations

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

Instances For

Basic operations and simp lemmas for Formulas #

source

def Lean4GlCoalgebras.Formula.isAtomic :

Formula → Bool

Returns true if the formula is a propositional atom at n.

Equations

(at a).isAtomic = true
x✝.isAtomic = false

Instances For

source

def Lean4GlCoalgebras.Formula.isNegAtomic :

Formula → Bool

Returns true if the formula is a negated atom na n.

Equations

(na a).isNegAtomic = true
x✝.isNegAtomic = false

Instances For

source

def Lean4GlCoalgebras.Formula.isDiamond :

Formula → Bool

Returns true if the formula is a diamond formula ◇ φ.

Equations

(◇a).isDiamond = true
x✝.isDiamond = false

Instances For

source

def Lean4GlCoalgebras.Formula.opUnDi (φ : Formula) :

Option Formula

Returns some φ if the formula is ◇ φ, otherwise none.

Equations

(◇a).opUnDi = some a
φ.opUnDi = none

Instances For

source

@[simp]

theorem Lean4GlCoalgebras.Formula.opUnDi_eq {φ ψ : Formula} :

φ.opUnDi = some ψ ↔ φ = ◇ψ

source

def Lean4GlCoalgebras.Formula.unDi (φ : Formula) (h : φ.isDiamond = true) :

Formula

Extracts φ from ◇ φ, given a proof that the formula is a diamond.

Equations

(◇φ_2).unDi h_2 = φ_2

Instances For

source

def Lean4GlCoalgebras.Formula.isBox :

Formula → Bool

Returns true if the formula is a box formula □ φ.

Equations

(□a).isBox = true
x✝.isBox = false

Instances For

source

theorem Lean4GlCoalgebras.Formula.neg_eq {φ ψ : Formula} :

(~φ) = (~ψ) → φ = ψ

Negation is injective.

source

@[simp]

theorem Lean4GlCoalgebras.Formula.neg_neg_eq (φ : Formula) :

(~~φ) = φ

Negation is involutive.

source

def Lean4GlCoalgebras.Formula.length :

Formula → ℕ

Length of a BML Formula.

Equations

Lean4GlCoalgebras.Formula.bottom.length = 0
Lean4GlCoalgebras.Formula.top.length = 0
(at a).length = 1
(na a).length = 1
(a&a_1).length = a.length + a_1.length + 1
(a v a_1).length = a.length + a_1.length + 1
(□a).length = a.length + 1
(◇a).length = a.length + 1

Instances For

source

def Lean4GlCoalgebras.Formula.vocab :

Formula → Finset ℕ

Vocab of a BML Formula. Expressed as underlying natural numbers.

Equations

Lean4GlCoalgebras.Formula.bottom.vocab = ∅
Lean4GlCoalgebras.Formula.top.vocab = ∅
(at a).vocab = {a}
(na a).vocab = {a}
(a&a_1).vocab = a.vocab ∪ a_1.vocab
(a v a_1).vocab = a.vocab ∪ a_1.vocab
(□a).vocab = a.vocab
(◇a).vocab = a.vocab

Instances For

source

def Lean4GlCoalgebras.Formula.atoms :

Formula → Finset ℕ

Atoms of a BML Formula. Expressed as underlying natural numbers.

Equations

Lean4GlCoalgebras.Formula.bottom.atoms = ∅
Lean4GlCoalgebras.Formula.top.atoms = ∅
(at a).atoms = {a}
(na a).atoms = ∅
(a&a_1).atoms = a.vocab ∪ a_1.vocab
(a v a_1).atoms = a.vocab ∪ a_1.vocab
(□a).atoms = a.vocab
(◇a).atoms = a.vocab

Instances For

source

def Lean4GlCoalgebras.Formula.lit :

Formula → Finset (ℕ ⊕ ℕ)

Literals of a BML Formula. Expressed as underlying natural numbers.

Equations

Lean4GlCoalgebras.Formula.bottom.lit = ∅
Lean4GlCoalgebras.Formula.top.lit = ∅
(at a).lit = {Sum.inl a}
(na a).lit = {Sum.inr a}
(a&a_1).lit = a.lit ∪ a_1.lit
(a v a_1).lit = a.lit ∪ a_1.lit
(□a).lit = a.lit
(◇a).lit = a.lit

Instances For

source

def Lean4GlCoalgebras.Formula.freshVar :

Formula → ℕ

Get a fresh variable not occuring in a BML Formula.

Equations

Lean4GlCoalgebras.Formula.top.freshVar = 0
Lean4GlCoalgebras.Formula.bottom.freshVar = 0
(at n).freshVar = n + 1
(na n).freshVar = n + 1
(φ&ψ).freshVar = max φ.freshVar ψ.freshVar
(φ v ψ).freshVar = max φ.freshVar ψ.freshVar
(□φ).freshVar = φ.freshVar
(◇φ).freshVar = φ.freshVar

Instances For

source

def Lean4GlCoalgebras.Formula.FL :

Formula → Sequent

Fischer-Ladner closure of a BML Formula.

Equations

Lean4GlCoalgebras.Formula.bottom.FL = {⊥}
Lean4GlCoalgebras.Formula.top.FL = {⊤}
(at n).FL = {at n}
(na n).FL = {na n}
(φ v ψ).FL = {φ v ψ} ∪ φ.FL ∪ ψ.FL
(φ&ψ).FL = {φ&ψ} ∪ φ.FL ∪ ψ.FL
(□φ).FL = {□φ} ∪ φ.FL
(◇φ).FL = {◇φ} ∪ φ.FL

Instances For

Lemmas about FL Closure of BML Formulas #

source

theorem Lean4GlCoalgebras.Formula.FL_refl {φ : Formula} :

φ ∈ φ.FL

Fischer-Ladner closure is reflexive.

source

theorem Lean4GlCoalgebras.Formula.FL_mon {φ ψ : Formula} (ψ_sub_φ : ψ ∈ φ.FL) :

ψ.FL ⊆ φ.FL

Fischer-Ladner closure is monotone.

Basic operations and simp lemmas for Sequents #

source

def Lean4GlCoalgebras.Sequent.length (Γ : Sequent) :

ℕ

Length of a sequent.

Equations

Γ.length = Finset.sum Γ Lean4GlCoalgebras.Formula.length

Instances For

source

def Lean4GlCoalgebras.Sequent.vocab (Γ : Sequent) :

Finset ℕ

Auxiliary declaration used in the GL coalgebra development.

Equations

Γ.vocab = Finset.biUnion Γ Lean4GlCoalgebras.Formula.vocab

Instances For

source

def Lean4GlCoalgebras.Sequent.lit (Γ : Sequent) :

Finset (ℕ ⊕ ℕ)

Auxiliary declaration used in the GL coalgebra development.

Equations

Γ.lit = Finset.biUnion Γ Lean4GlCoalgebras.Formula.lit

Instances For

source

def Lean4GlCoalgebras.Sequent.neg (Γ : Sequent) :

Finset Formula

Auxiliary declaration used in the GL coalgebra development.

Equations

Γ.neg = Finset.biUnion Γ fun (φ : Lean4GlCoalgebras.Formula) => {~φ}

Instances For

source

def Lean4GlCoalgebras.Sequent.freshVar (Γ : Finset Formula) :

ℕ

Auxiliary declaration used in the GL coalgebra development.

Equations

Lean4GlCoalgebras.Sequent.freshVar Γ = if h : Γ = ∅ then 0 else (Finset.image Lean4GlCoalgebras.Formula.freshVar Γ).max' ⋯

Instances For

source

def Lean4GlCoalgebras.Sequent.D (Γ : Sequent) :

Sequent

Auxiliary declaration used in the GL coalgebra development.

Equations

Γ.D = {x ∈ Γ | decide (x.isDiamond = true) = true} ∪ Finset.filterMap Lean4GlCoalgebras.Formula.opUnDi Γ Lean4GlCoalgebras.Sequent.D._proof_1

Instances For

source

theorem Lean4GlCoalgebras.Sequent.form_in_seq_size_le {A : Formula} {Δ : Sequent} :

A ∈ Δ → A.length ≤ Δ.length

source

def Lean4GlCoalgebras.Sequent.FL :

Sequent → Sequent

Fischer-Ladner closure of a sequent.

Equations

Δ.FL = Finset.biUnion Δ Lean4GlCoalgebras.Formula.FL

Instances For

Lemmas about FL Closure of Sequents #

source

theorem Lean4GlCoalgebras.Sequent.FL_refl {Δ : Sequent} :

Δ ⊆ Δ.FL

source

theorem Lean4GlCoalgebras.Sequent.FL_mon {Δ Γ : Sequent} (Δ_sub_Γ : Δ ⊆ Γ) :

Δ.FL ⊆ Γ.FL

source

theorem Lean4GlCoalgebras.Sequent.FL_idem {Δ : Sequent} :

Δ.FL.FL = Δ.FL

source

@[reducible, inline]

abbrev Lean4GlCoalgebras.SplitFormula :

Type

Auxiliary declaration used in the GL coalgebra development.

Equations

Lean4GlCoalgebras.SplitFormula = (Lean4GlCoalgebras.Formula ⊕ Lean4GlCoalgebras.Formula)

Instances For

source

@[reducible, inline]

abbrev Lean4GlCoalgebras.SplitSequent :

Type

Auxiliary declaration used in the GL coalgebra development.

Equations

Lean4GlCoalgebras.SplitSequent = Finset Lean4GlCoalgebras.SplitFormula

Instances For

Basic operations and simp lemmas for Split Sequents #

source

def Lean4GlCoalgebras.SplitFormula.isDiamond :

SplitFormula → Bool

Auxiliary declaration used in the GL coalgebra development.

Equations

Lean4GlCoalgebras.SplitFormula.isDiamond (Sum.inl (◇a)) = true
Lean4GlCoalgebras.SplitFormula.isDiamond (Sum.inr (◇a)) = true
x✝.isDiamond = false

Instances For

source

def Lean4GlCoalgebras.SplitFormula.opUnDi (φ : SplitFormula) :

Option SplitFormula

Auxiliary declaration used in the GL coalgebra development.

Equations

Lean4GlCoalgebras.SplitFormula.opUnDi (Sum.inl (◇a)) = some (Sum.inl a)
Lean4GlCoalgebras.SplitFormula.opUnDi (Sum.inr (◇a)) = some (Sum.inr a)
φ.opUnDi = none

Instances For

source

def Lean4GlCoalgebras.SplitFormula.length :

Formula ⊕ Formula → ℕ

Auxiliary declaration used in the GL coalgebra development.

Equations

Lean4GlCoalgebras.SplitFormula.length (Sum.inl φ) = φ.length
Lean4GlCoalgebras.SplitFormula.length (Sum.inr φ) = φ.length

Instances For

source

@[irreducible]

def Lean4GlCoalgebras.SplitFormula.FL :

SplitFormula → SplitSequent

Auxiliary declaration used in the GL coalgebra development.

Equations

Lean4GlCoalgebras.SplitFormula.FL (Sum.inl Lean4GlCoalgebras.Formula.bottom) = {Sum.inl ⊥}
Lean4GlCoalgebras.SplitFormula.FL (Sum.inr Lean4GlCoalgebras.Formula.bottom) = {Sum.inr ⊥}
Lean4GlCoalgebras.SplitFormula.FL (Sum.inl Lean4GlCoalgebras.Formula.top) = {Sum.inl ⊤}
Lean4GlCoalgebras.SplitFormula.FL (Sum.inr Lean4GlCoalgebras.Formula.top) = {Sum.inr ⊤}
Lean4GlCoalgebras.SplitFormula.FL (Sum.inl (at n)) = {Sum.inl (at n)}
Lean4GlCoalgebras.SplitFormula.FL (Sum.inr (at n)) = {Sum.inr (at n)}
Lean4GlCoalgebras.SplitFormula.FL (Sum.inl (na n)) = {Sum.inl (na n)}
Lean4GlCoalgebras.SplitFormula.FL (Sum.inr (na n)) = {Sum.inr (na n)}
Lean4GlCoalgebras.SplitFormula.FL (Sum.inl (φ v ψ)) = {Sum.inl (φ v ψ)} ∪ Lean4GlCoalgebras.SplitFormula.FL (Sum.inl φ) ∪ Lean4GlCoalgebras.SplitFormula.FL (Sum.inl ψ)
Lean4GlCoalgebras.SplitFormula.FL (Sum.inr (φ v ψ)) = {Sum.inr (φ v ψ)} ∪ Lean4GlCoalgebras.SplitFormula.FL (Sum.inr φ) ∪ Lean4GlCoalgebras.SplitFormula.FL (Sum.inr ψ)
Lean4GlCoalgebras.SplitFormula.FL (Sum.inl (φ&ψ)) = {Sum.inl (φ&ψ)} ∪ Lean4GlCoalgebras.SplitFormula.FL (Sum.inl φ) ∪ Lean4GlCoalgebras.SplitFormula.FL (Sum.inl ψ)
Lean4GlCoalgebras.SplitFormula.FL (Sum.inr (φ&ψ)) = {Sum.inr (φ&ψ)} ∪ Lean4GlCoalgebras.SplitFormula.FL (Sum.inr φ) ∪ Lean4GlCoalgebras.SplitFormula.FL (Sum.inr ψ)
Lean4GlCoalgebras.SplitFormula.FL (Sum.inl (□φ)) = {Sum.inl (□φ)} ∪ Lean4GlCoalgebras.SplitFormula.FL (Sum.inl φ)
Lean4GlCoalgebras.SplitFormula.FL (Sum.inr (□φ)) = {Sum.inr (□φ)} ∪ Lean4GlCoalgebras.SplitFormula.FL (Sum.inr φ)
Lean4GlCoalgebras.SplitFormula.FL (Sum.inl (◇φ)) = {Sum.inl (◇φ)} ∪ Lean4GlCoalgebras.SplitFormula.FL (Sum.inl φ)
Lean4GlCoalgebras.SplitFormula.FL (Sum.inr (◇φ)) = {Sum.inr (◇φ)} ∪ Lean4GlCoalgebras.SplitFormula.FL (Sum.inr φ)

Instances For

Lemmas about FL Closure of Split Formulas #

source

theorem Lean4GlCoalgebras.SplitFormula.FL_SplitFormula_left_eq_FL_Formula_map (φ : Formula) :

FL (Sum.inl φ) = Finset.map { toFun := Sum.inl, inj' := ⋯ } φ.FL

source

theorem Lean4GlCoalgebras.SplitFormula.FL_SplitFormula_right_eq_FL_Formula_map (φ : Formula) :

FL (Sum.inr φ) = Finset.map { toFun := Sum.inr, inj' := ⋯ } φ.FL

source

theorem Lean4GlCoalgebras.SplitFormula.in_FL_SplitFormula_left {φ : Formula} {ψ : SplitFormula} (ψ_sub_φ : ψ ∈ FL (Sum.inl φ)) :

Sum.isLeft ψ = true

source

theorem Lean4GlCoalgebras.SplitFormula.in_FL_SplitFormula_right {φ : Formula} {ψ : SplitFormula} (ψ_sub_φ : ψ ∈ FL (Sum.inr φ)) :

Sum.isRight ψ = true

source

theorem Lean4GlCoalgebras.SplitFormula.in_FL_of_in_FL_SplitFormula_left {φ : Formula} {ψ : SplitFormula} (ψ_sub_φ : ψ ∈ FL (Sum.inl φ)) :

Sum.elim id id ψ ∈ φ.FL

source

theorem Lean4GlCoalgebras.SplitFormula.in_FL_of_in_FL_SplitFormula_right {φ : Formula} {ψ : SplitFormula} (ψ_sub_φ : ψ ∈ FL (Sum.inr φ)) :

Sum.elim id id ψ ∈ φ.FL

source

theorem Lean4GlCoalgebras.SplitFormula.FL_refl {φ : SplitFormula} :

φ ∈ φ.FL

Fischer-Ladner Closure is reflexive.

source

theorem Lean4GlCoalgebras.SplitFormula.FL_mon {φ ψ : SplitFormula} (ψ_sub_φ : ψ ∈ φ.FL) :

ψ.FL ⊆ φ.FL

Fischer-Ladner Closure is monotone.

Lemmas about FL Closure of Split Sequents #

source

def Lean4GlCoalgebras.SplitSequent.FL :

SplitSequent → SplitSequent

Auxiliary declaration used in the GL coalgebra development.

Equations

Δ.FL = Finset.biUnion Δ Lean4GlCoalgebras.SplitFormula.FL

Instances For

source

theorem Lean4GlCoalgebras.SplitSequent.FL_refl {Δ : SplitSequent} :

Δ ⊆ Δ.FL

Fischer-Ladner Closure is reflexive.

source

theorem Lean4GlCoalgebras.SplitSequent.FL_mon {Δ Γ : SplitSequent} (Δ_sub_Γ : Δ ⊆ Γ) :

Δ.FL ⊆ Γ.FL

Fischer-Ladner Closure is monotone.

source

theorem Lean4GlCoalgebras.SplitSequent.FL_idem {Δ : SplitSequent} :

Δ.FL.FL = Δ.FL

Fischer-Ladner Closure is idempotent.

source

def Lean4GlCoalgebras.SplitSequent.D (Γ : SplitSequent) :

SplitSequent

□₄⁻¹ operator for Split Sequents.

Equations

Γ.D = {x ∈ Γ | decide (x.isDiamond = true) = true} ∪ Finset.filterMap Lean4GlCoalgebras.SplitFormula.opUnDi Γ Lean4GlCoalgebras.SplitSequent.D._proof_1

Instances For

Basic operations and simp lemmas for Split Sequents #

source

def Lean4GlCoalgebras.SplitSequent.toSequent (Δ : SplitSequent) :

Sequent

Find underlying Sequent of a Split Sequent.

Equations

Δ.toSequent = Finset.image (Sum.elim id id) Δ

Instances For

source

def Lean4GlCoalgebras.SplitSequent.length (Δ : SplitSequent) :

ℕ

Length of a Split Sequent.

Equations

Δ.length = Finset.sum Δ Lean4GlCoalgebras.SplitFormula.length

Instances For

source

@[simp]

theorem Lean4GlCoalgebras.SplitSequent.opUnDi_eqₗₗ {φ ψ : Formula} :

SplitFormula.opUnDi (Sum.inl φ) = some (Sum.inl ψ) ↔ φ = ◇ψ

source

@[simp]

theorem Lean4GlCoalgebras.SplitSequent.opUnDi_eqᵣᵣ {φ ψ : Formula} :

SplitFormula.opUnDi (Sum.inr φ) = some (Sum.inr ψ) ↔ φ = ◇ψ

source

@[simp]

theorem Lean4GlCoalgebras.SplitSequent.opUnDi_eqₗᵣ {φ ψ : Formula} :

¬SplitFormula.opUnDi (Sum.inl φ) = some (Sum.inr ψ)

source

@[simp]

theorem Lean4GlCoalgebras.SplitSequent.opUnDi_eqᵣₗ {φ ψ : Formula} :

¬SplitFormula.opUnDi (Sum.inr φ) = some (Sum.inl ψ)

source

noncomputable def Lean4GlCoalgebras.SplitSequent.filterLeft :

SplitSequent → SplitSequent

Auxiliary declaration used in the GL coalgebra development.

Equations

Lean4GlCoalgebras.SplitSequent.filterLeft = Finset.filter fun (x : Lean4GlCoalgebras.SplitFormula) => match x with | Sum.inl val => true = true | Sum.inr val => false = true

Instances For

source

noncomputable def Lean4GlCoalgebras.SplitSequent.filterRight :

SplitSequent → SplitSequent

Auxiliary declaration used in the GL coalgebra development.

Equations

Lean4GlCoalgebras.SplitSequent.filterRight = Finset.filter fun (x : Lean4GlCoalgebras.SplitFormula) => match x with | Sum.inl val => false = true | Sum.inr val => true = true

Instances For

source

def Lean4GlCoalgebras.SplitSequent.left (Γ : SplitSequent) :

Sequent

Auxiliary declaration used in the GL coalgebra development.

Equations

Γ.left = Finset.filterMap Sum.getLeft? Γ Lean4GlCoalgebras.SplitSequent.left._proof_1

Instances For

source

def Lean4GlCoalgebras.SplitSequent.right (Γ : SplitSequent) :

Sequent

Auxiliary declaration used in the GL coalgebra development.

Equations

Γ.right = Finset.filterMap Sum.getRight? Γ Lean4GlCoalgebras.SplitSequent.right._proof_1

Instances For

Properties of Substitutions #

source

def Lean4GlCoalgebras.single (n : ℕ) (ψ : Formula) :

Formula → Formula

Substiting p with ψ in φ (φ[ψ/p]).

Equations

Lean4GlCoalgebras.single n ψ Lean4GlCoalgebras.Formula.bottom = ⊥
Lean4GlCoalgebras.single n ψ Lean4GlCoalgebras.Formula.top = ⊤
Lean4GlCoalgebras.single n ψ (at a) = if (a == n) = true then ψ else at a
Lean4GlCoalgebras.single n ψ (na a) = if (a == n) = true then ~ψ else na a
Lean4GlCoalgebras.single n ψ (a&a_1) = (Lean4GlCoalgebras.single n ψ a&Lean4GlCoalgebras.single n ψ a_1)
Lean4GlCoalgebras.single n ψ (a v a_1) = (Lean4GlCoalgebras.single n ψ a v Lean4GlCoalgebras.single n ψ a_1)
Lean4GlCoalgebras.single n ψ (□a) = □Lean4GlCoalgebras.single n ψ a
Lean4GlCoalgebras.single n ψ (◇a) = ◇Lean4GlCoalgebras.single n ψ a

Instances For

source

theorem Lean4GlCoalgebras.single_neg (n : ℕ) (φ ψ : Formula) :

single n ψ (~φ) = (~single n ψ φ)

source

theorem Lean4GlCoalgebras.single_imp (n : ℕ) (C D E : Formula) :

single n C (~D v E) = (~single n C D v single n C E)

source

theorem Lean4GlCoalgebras.single_iff (n : ℕ) (C D E : Formula) :

single n C ((~D v E)&~E v D) = ((~single n C D v single n C E)&~single n C E v single n C D)

source

@[simp]

theorem Lean4GlCoalgebras.single_identity (n : ℕ) (φ : Formula) :

single n (at n) φ = φ

source

def Lean4GlCoalgebras.partial_ {c : ℕ → Prop} [DecidablePred c] (σ : Subtype c → Formula) :

Formula → Formula

Simultaneous substitution for p meeting criteria c.

Equations

Lean4GlCoalgebras.partial_ σ Lean4GlCoalgebras.Formula.bottom = ⊥
Lean4GlCoalgebras.partial_ σ Lean4GlCoalgebras.Formula.top = ⊤
Lean4GlCoalgebras.partial_ σ (at a) = if h : c a then σ ⟨a, h⟩ else at a
Lean4GlCoalgebras.partial_ σ (na a) = if h : c a then ~σ ⟨a, h⟩ else na a
Lean4GlCoalgebras.partial_ σ (a&a_1) = (Lean4GlCoalgebras.partial_ σ a&Lean4GlCoalgebras.partial_ σ a_1)
Lean4GlCoalgebras.partial_ σ (a v a_1) = (Lean4GlCoalgebras.partial_ σ a v Lean4GlCoalgebras.partial_ σ a_1)
Lean4GlCoalgebras.partial_ σ (□a) = □Lean4GlCoalgebras.partial_ σ a
Lean4GlCoalgebras.partial_ σ (◇a) = ◇Lean4GlCoalgebras.partial_ σ a

Instances For

source

@[irreducible]

def Lean4GlCoalgebras.full (σ : ℕ → Formula) (A : Formula) :

Formula

Full substitution of all p.

Equations

Lean4GlCoalgebras.full σ Lean4GlCoalgebras.Formula.bottom = ⊥
Lean4GlCoalgebras.full σ Lean4GlCoalgebras.Formula.top = ⊤
Lean4GlCoalgebras.full σ (at a) = σ a
Lean4GlCoalgebras.full σ (na a) = (~σ a)
Lean4GlCoalgebras.full σ (a&a_1) = (Lean4GlCoalgebras.full σ a&Lean4GlCoalgebras.full σ a_1)
Lean4GlCoalgebras.full σ (a v a_1) = (Lean4GlCoalgebras.full σ a v Lean4GlCoalgebras.full σ a_1)
Lean4GlCoalgebras.full σ (□a) = □Lean4GlCoalgebras.full σ a
Lean4GlCoalgebras.full σ (◇a) = ◇Lean4GlCoalgebras.full σ a

Instances For

Properties of Vocab #

source

@[simp]

theorem Lean4GlCoalgebras.in_neg_voc_iff {n : ℕ} {φ : Formula} :

n ∈ (~φ).vocab ↔ n ∈ φ.vocab

source

theorem Lean4GlCoalgebras.in_single_voc (m n : ℕ) (φ ψ : Formula) :

m ∉ φ.vocab → (m ≠ n → m ∉ ψ.vocab) → n ∉ φ.vocab → m ∉ (single n φ ψ).vocab

source

theorem Lean4GlCoalgebras.not_in_single_voc (n : ℕ) (φ ψ : Formula) :

n ∉ φ.vocab → single n ψ φ = φ

source

theorem Lean4GlCoalgebras.not_in_single_top_voc (n : ℕ) (φ : Formula) :

n ∉ (single n ⊤ φ).vocab

source

theorem Lean4GlCoalgebras.not_in_single_bot_voc (n : ℕ) (φ : Formula) :

n ∉ (single n ⊥ φ).vocab

source

theorem Lean4GlCoalgebras.in_single_voc' {m n : ℕ} {φ ψ : Formula} :

m ∈ (single n φ ψ).vocab → m ∈ φ.vocab ∧ n ∈ ψ.vocab ∨ m ∈ ψ.vocab ∧ m ≠ n

Some very specific lemmas about Finset.sum #

Ideally grind or aesop or some other tactic could sort out these simple helper lemmas, but I could not figure out how.

source

theorem Lean4GlCoalgebras.sub_add_left {n m l : ℕ} :

n + m = l → n = l - m

source

theorem Lean4GlCoalgebras.lt_and_le_imp_add_lt {a b c : ℕ} :

b ≤ a → c < b → a - b + c < a

source

theorem Lean4GlCoalgebras.Finset.sum_diff_singleton_lt {α : Type} [DecidableEq α] {A C : Finset α} {b : α} {f : α → ℕ} :

b ∈ A → C.sum f < f b → (A \ {b} ∪ C).sum f < A.sum f

Documentation

LeanPool.Lean4GlCoalgebras.Logic.Syntax

Basic operations and simp lemmas for Formulas #

Lemmas about FL Closure of BML Formulas #

Basic operations and simp lemmas for Sequents #

Lemmas about FL Closure of Sequents #

Basic operations and simp lemmas for Split Sequents #

Lemmas about FL Closure of Split Formulas #

Lemmas about FL Closure of Split Sequents #

Basic operations and simp lemmas for Split Sequents #

Properties of Substitutions #

Properties of Vocab #

Some very specific lemmas about Finset.sum #

Syntax of Basic Modal Logic #

Basic operations and simp lemmas for Formulas #

Lemmas about FL Closure of BML Formulas #

Basic operations and simp lemmas for Sequents #

Lemmas about FL Closure of Sequents #

Basic operations and simp lemmas for Split Sequents #

Lemmas about FL Closure of Split Formulas #

Lemmas about FL Closure of Split Sequents #

Basic operations and simp lemmas for Split Sequents #

Properties of Substitutions #

Properties of Vocab #

Some very specific lemmas about Finset.sum #