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))

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))

Basic modalities

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))

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.HasDynamicBox (α : Type u_1) (β : 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.

class Cslib.Logic.HasDynamicDiamond (α : Type u_1) (β : 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.

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))