Logical operators

This module contains typeclasses and associated notation for common logical operators: propositional connectives (like ∧ and →), modalities (like ◇, plain and indexed), linear connectives (like ⊗), etc.

Propositional connectives

class Cslib.Logic.HasAnd (α : Type u_1) : Type u_1

The type α has an and connective (∧).

• and (a b : α) : α

  a ∧ b is the conjunction of a and b.

def Cslib.Logic.«term_∧_» : Lean.TrailingParserDescr

a ∧ b is the conjunction of a and b.

Equations

• Cslib.Logic.«term_∧_» = Lean.ParserDescr.trailingNode `Cslib.Logic.«term_∧_» 36 37 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∧ ") (Lean.ParserDescr.cat `term 36))

class Cslib.Logic.HasOr (α : Type u_1) : Type u_1

The type α has an or connective (∨).

• or (a b : α) : α

  a ∨ b is the disjunction of a and b.

def Cslib.Logic.«term_∨_» : Lean.TrailingParserDescr

a ∨ b is the disjunction of a and b.

Equations

• Cslib.Logic.«term_∨_» = Lean.ParserDescr.trailingNode `Cslib.Logic.«term_∨_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∨ ") (Lean.ParserDescr.cat `term 30))

def Cslib.Logic.finiteAnd {α : Type u_1} [HasAnd α] [Top α] (as : List α) : α

Finite conjunction, with empty conjunction equal to truth.

Equations

• Cslib.Logic.finiteAnd as = List.foldr (fun (x1 x2 : α) => Cslib.Logic.HasAnd.and x1 x2) ⊤ as

def Cslib.Logic.«term⋀_» : Lean.ParserDescr

Finite conjunction, with empty conjunction equal to truth.

Equations

• Cslib.Logic.«term⋀_» = Lean.ParserDescr.node `Cslib.Logic.«term⋀_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋀") (Lean.ParserDescr.cat `term 1024))

@[simp]

theorem Cslib.Logic.finiteAnd_nil {α : Type u_1} [HasAnd α] [Top α] : finiteAnd [] = ⊤

@[simp]

theorem Cslib.Logic.finiteAnd_cons {α : Type u_1} [HasAnd α] [Top α] (a : α) (as : List α) : finiteAnd (a :: as) = HasAnd.and a (finiteAnd as)

def Cslib.Logic.finiteOr {α : Type u_1} [HasOr α] [Bot α] (as : List α) : α

Finite disjunction, with empty disjunction equal to falsehood.

Equations

• Cslib.Logic.finiteOr as = List.foldr (fun (x1 x2 : α) => Cslib.Logic.HasOr.or x1 x2) ⊥ as

def Cslib.Logic.«term⋁_» : Lean.ParserDescr

Finite disjunction, with empty disjunction equal to falsehood.

Equations

• Cslib.Logic.«term⋁_» = Lean.ParserDescr.node `Cslib.Logic.«term⋁_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋁") (Lean.ParserDescr.cat `term 1024))

@[simp]

theorem Cslib.Logic.finiteOr_nil {α : Type u_1} [HasOr α] [Bot α] : finiteOr [] = ⊥

@[simp]

theorem Cslib.Logic.finiteOr_cons {α : Type u_1} [HasOr α] [Bot α] (a : α) (as : List α) : finiteOr (a :: as) = HasOr.or a (finiteOr as)

class Cslib.Logic.HasImp (α : Type u_1) : Type u_1

The type α has an implication connective (→).

• imp (a b : α) : α

  a → b denotes a implies b.

def Cslib.Logic.«term_→_» : Lean.TrailingParserDescr

a → b denotes a implies b.

Equations

• Cslib.Logic.«term_→_» = Lean.ParserDescr.trailingNode `Cslib.Logic.«term_→_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " → ") (Lean.ParserDescr.cat `term 25))

class Cslib.Logic.HasIff (α : Type u_1) : Type u_1

The type α has a bi-implication connective (↔).

• iff (a b : α) : α

  a ↔ b denotes a implies b and vice-versa.

def Cslib.Logic.«term_↔_» : Lean.TrailingParserDescr

a ↔ b denotes a implies b and vice-versa.

Equations

• Cslib.Logic.«term_↔_» = Lean.ParserDescr.trailingNode `Cslib.Logic.«term_↔_» 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↔ ") (Lean.ParserDescr.cat `term 20))

class Cslib.Logic.HasNot (α : Type u_1) : Type u_1

The type α has a negation connective (¬).

• not (a : α) : α

  ¬a is the negation of a.

def Cslib.Logic.«term¬_» : Lean.ParserDescr

¬a is the negation of a.

Equations

• Cslib.Logic.«term¬_» = Lean.ParserDescr.node `Cslib.Logic.«term¬_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "¬") (Lean.ParserDescr.cat `term 40))

General modalities from modal similarity types (polynomial functors)

class Cslib.Logic.HasTriangle (α : Type u_1) (τ : outParam PFunctor.{u_3, u_2}) : Type (max (max u_1 u_2) u_3)

The type α has a family of triangle operators (Δ).

• triangle (op : τ.A) (arg : τ.B op → α) : α

  Δ[op](φ₁, ..., φₙ) means that φ₁, ..., φₙ are valid at some respective related states.

def Cslib.Logic.«termΔ[_]_» : Lean.ParserDescr

Δ[op](φ₁, ..., φₙ) means that φ₁, ..., φₙ are valid at some respective related states.

Equations

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

class Cslib.Logic.HasNabla (α : Type u_1) (τ : outParam PFunctor.{u_3, u_2}) : Type (max (max u_1 u_2) u_3)

The type α has a family of nabla operators (∇).

• nabla (op : τ.A) (arg : τ.B op → α) : α

  ∇[op](φ₁, ..., φₙ) means that φ₁, ..., φₙ are valid at all respective related states.

def Cslib.Logic.«term∇[_]_» : Lean.ParserDescr

∇[op](φ₁, ..., φₙ) means that φ₁, ..., φₙ are valid at all respective related states.

Equations

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

Dynamic modalities

Here we need to use the prefix d to distinguish our notation from the normal [·] and ⟨·⟩. A refactoring that makes this unnecessary would be welcome.

class Cslib.Logic.HasDynamicDiamond (α : Type u_1) (β : outParam (Type u_2)) : Type (max u_1 u_2)

The type α has a dynamic diamond modality with action type β (d⟨a⟩φ).

• dynDiamond (a : β) (b : α) : α

  b is possibly valid after a.

def Cslib.Logic.«termD⟨_⟩_» : Lean.ParserDescr

b is possibly valid after a.

Equations

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

class Cslib.Logic.HasDynamicBox (α : Type u_1) (β : outParam (Type u_2)) : Type (max u_1 u_2)

The type α has a dynamic box modality with action type β (d[a]φ).

• dynBox (a : β) (b : α) : α

  b is necessarily valid after a.

def Cslib.Logic.«termD[_]_» : Lean.ParserDescr

b is necessarily valid after a.

Equations

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

@[instance_reducible]

instance Cslib.Logic.instHasDynamicDiamondAOfHasTriangle {α : Type u_1} {τ : PFunctor.{u_2, u_3}} [HasTriangle α τ] : HasDynamicDiamond α τ.A

A family of triangle operators over induces dynamic diamond modalities by applying each operator to the constant argument family.

Equations

• Cslib.Logic.instHasDynamicDiamondAOfHasTriangle = { dynDiamond := fun (op : τ.A) (φ : α) => Cslib.Logic.HasTriangle.triangle op (PFunctor.const op φ) }

@[simp]

theorem Cslib.Logic.dynDiamond_eq_triangle {α : Type u_1} {τ : PFunctor.{u_2, u_3}} [HasTriangle α τ] (op : τ.A) (φ : α) : HasDynamicDiamond.dynDiamond op φ = HasTriangle.triangle op (PFunctor.const op φ)

@[instance_reducible]

instance Cslib.Logic.instHasDynamicBoxAOfHasNabla {α : Type u_1} {τ : PFunctor.{u_2, u_3}} [HasNabla α τ] : HasDynamicBox α τ.A

A family of nabla operators induces dynamic box modalities by applying each operator to the constant argument family.

Equations

• Cslib.Logic.instHasDynamicBoxAOfHasNabla = { dynBox := fun (op : τ.A) (φ : α) => Cslib.Logic.HasNabla.nabla op (PFunctor.const op φ) }

@[simp]

theorem Cslib.Logic.dynBox_eq_nabla {α : Type u_1} {τ : PFunctor.{u_2, u_3}} [HasNabla α τ] (op : τ.A) (φ : α) : HasDynamicBox.dynBox op φ = HasNabla.nabla op (PFunctor.const op φ)

Basic modalities (Unimodal logic operators)

class Cslib.Logic.HasBox (α : Type u_1) : Type u_1

The type α has a box modality (□).

• box (a : α) : α

  a is valid in all immediately reachable states.

def Cslib.Logic.«term□_» : Lean.ParserDescr

a is valid in all immediately reachable states.

Equations

• Cslib.Logic.«term□_» = Lean.ParserDescr.node `Cslib.Logic.«term□_» 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "□") (Lean.ParserDescr.cat `term 40))

class Cslib.Logic.HasDiamond (α : Type u_1) : Type u_1

The type α has a diamond modality (◇).

• diamond (a : α) : α

  a is valid in a reachable state.

def Cslib.Logic.«term◇_» : Lean.ParserDescr

a is valid in a reachable state.

Equations

• Cslib.Logic.«term◇_» = Lean.ParserDescr.node `Cslib.Logic.«term◇_» 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "◇") (Lean.ParserDescr.cat `term 40))

@[instance_reducible]

instance Cslib.Logic.instHasDiamondOfUniqueOfHasDynamicDiamond {β : Type u_1} {α : Type u_2} [Unique β] [HasDynamicDiamond α β] : HasDiamond α

A dynamic diamond modality with a unique action induces a basic diamond modality.

Equations

• Cslib.Logic.instHasDiamondOfUniqueOfHasDynamicDiamond = { diamond := fun (φ : α) => Cslib.Logic.HasDynamicDiamond.dynDiamond default φ }

@[simp]

theorem Cslib.Logic.diamond_eq_dynDiamond {β : Type u_1} {α : Type u_2} [Unique β] [HasDynamicDiamond α β] {φ : α} : HasDiamond.diamond φ = HasDynamicDiamond.dynDiamond default φ

@[instance_reducible]

instance Cslib.Logic.instHasBoxOfUniqueOfHasDynamicBox {β : Type u_1} {α : Type u_2} [Unique β] [HasDynamicBox α β] : HasBox α

A dynamic box modality with a unique action induces a basic box modality.

Equations

• Cslib.Logic.instHasBoxOfUniqueOfHasDynamicBox = { box := fun (φ : α) => Cslib.Logic.HasDynamicBox.dynBox default φ }

@[simp]

theorem Cslib.Logic.box_eq_dynBox {β : Type u_1} {α : Type u_2} [Unique β] [HasDynamicBox α β] {φ : α} : HasBox.box φ = HasDynamicBox.dynBox default φ

Linear connectives

class Cslib.Logic.HasTensor (α : Type u_1) : Type u_1

The type α has a tensor connective (⊗).

• tensor (a b : α) : α

  a ⊗ b is the multiplicative conjunction of a and b.

def Cslib.Logic.«term_⊗_» : Lean.TrailingParserDescr

a ⊗ b is the multiplicative conjunction of a and b.

Equations

• Cslib.Logic.«term_⊗_» = Lean.ParserDescr.trailingNode `Cslib.Logic.«term_⊗_» 35 36 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ ") (Lean.ParserDescr.cat `term 35))