Logical Equivalence in HML

This module defines logical equivalence for HML propositions and instantiates LogicalEquivalence.

Theory of logical equivalence

def Cslib.Logic.HML.Proposition.Equiv {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) (φ₁ φ₂ : Proposition Label) : Prop

The HML propositions φ₁ and φ₂ are logically equivalent under the LTS lts.

Equations

• Cslib.Logic.HML.Proposition.Equiv lts φ₁ φ₂ = ∀ (s : State), ⇓{ lts := lts, state := s, φ := Cslib.Logic.HasIff.iff φ₁ φ₂ }

@[instance_reducible]

instance Cslib.Logic.HML.instCongruencePropositionEquiv {State✝ : Type u_1} {Label✝ : Type u_2} {lts : LTS State✝ Label✝} : Congruence (Proposition.Equiv lts)

Equations

• Cslib.Logic.HML.instCongruencePropositionEquiv = { }

theorem Cslib.Logic.HML.Proposition.equiv_def {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) (φ₁ φ₂ : Proposition Label) : Equiv lts φ₁ φ₂ ↔ Congruence.r (Equiv lts) φ₁ φ₂

theorem Cslib.Logic.HML.Proposition.equiv_forall_der {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) (φ₁ φ₂ : Proposition Label) (h : Congruence.r (Equiv lts) φ₁ φ₂) (s : State) : ⇓{ lts := lts, state := s, φ := HasIff.iff φ₁ φ₂ }

theorem Cslib.Logic.HML.Proposition.forall_der_equiv {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) (φ₁ φ₂ : Proposition Label) (h : ∀ (s : State), ⇓{ lts := lts, state := s, φ := HasIff.iff φ₁ φ₂ }) : Congruence.r (Equiv lts) φ₁ φ₂

theorem Cslib.Logic.HML.Proposition.equiv_iff {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {φ₁ φ₂ : Proposition Label} (h : Congruence.r (Equiv lts) φ₁ φ₂) (s : State) : ⇓{ lts := lts, state := s, φ := φ₁ } ↔ ⇓{ lts := lts, state := s, φ := φ₂ }

inductive Cslib.Logic.HML.Proposition.Context (Label : Type u) : Type u

Propositional contexts.

• hole {Label : Type u} : Context Label
• andL {Label : Type u} (c : Context Label) (φ : Proposition Label) : Context Label
• andR {Label : Type u} (φ : Proposition Label) (c : Context Label) : Context Label
• not {Label : Type u} (c : Context Label) : Context Label
• diamond {Label : Type u} (μ : Label) (c : Context Label) : Context Label

def Cslib.Logic.HML.Proposition.Context.fill {Label : Type u_1} (c : Context Label) (φ : Proposition Label) : Proposition Label

Replaces a hole in a propositional context with a proposition.

Equations

• Cslib.Logic.HML.Proposition.Context.hole.fill φ = φ
• (c_2.andL φ').fill φ = (c_2.fill φ).and φ'
• (Cslib.Logic.HML.Proposition.Context.andR φ' c_2).fill φ = φ'.and (c_2.fill φ)
• c_2.not.fill φ = (c_2.fill φ).not
• (Cslib.Logic.HML.Proposition.Context.diamond μ c_2).fill φ = Cslib.Logic.HML.Proposition.diamond μ (c_2.fill φ)

@[instance_reducible]

instance Cslib.Logic.HML.instHasContextProposition {Label : Type u_1} : HasContext (Proposition Label)

Equations

• Cslib.Logic.HML.instHasContextProposition = { Context := Cslib.Logic.HML.Proposition.Context Label, fill := Cslib.Logic.HML.Proposition.Context.fill }

theorem Cslib.Logic.HML.Proposition.Context.fill_def {Atom : Type u_1} {φ : Proposition Atom} {c : HasContext.Context (Proposition Atom)} : fill c φ = c<[φ]

instance Cslib.Logic.HML.instIsEquivPropositionEquiv {Label : Type u_1} {State✝ : Type u_2} {lts : LTS State✝ Label} : IsEquiv (Proposition Label) (Proposition.Equiv lts)

Logical equivalence is an equivalence relation.

instance Cslib.Logic.HML.instLawfulCongruencePropositionEquiv {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) : LawfulCongruence (Proposition.Equiv lts)

Logical equivalence is a lawful congruence.

structure Cslib.Logic.HML.Judgement.Context (State : Type u_1) (Label : Type u_2) : Type (max u_1 u_2)

Judgemental contexts.

• lts : LTS State Label

  The labelled transition system to consider.

• state : State

  The state to check propositions against.

def Cslib.Logic.HML.Judgement.Context.fill {State : Type u_1} {Label : Type u_2} (c : Context State Label) (φ : Proposition Label) : Judgement State Label

Fills a judgemental context with a proposition.

Equations

• c.fill φ = { lts := c.lts, state := c.state, φ := φ }

@[instance_reducible]

instance Cslib.Logic.HML.instHasHContextJudgementProposition {State : Type u_1} {Label : Type u_2} : HasHContext (Judgement State Label) (Proposition Label)

Equations

• Cslib.Logic.HML.instHasHContextJudgementProposition = { Context := Cslib.Logic.HML.Judgement.Context State Label, fill := Cslib.Logic.HML.Judgement.Context.fill }

theorem Cslib.Logic.HML.Judgement.Context.fill_def {World : Type u_1} {Atom : Type u_2} {c : Context World Atom} {φ : Proposition Atom} : { lts := c.lts, state := c.state, φ := φ } = c<[φ]

def Cslib.Logic.HML.Proposition.UEquiv {Label : Type v} (φ₁ φ₂ : Proposition Label) : Prop

Universal logical equivalence: logical equivalence under all LTSs.

Equations

• φ₁.UEquiv φ₂ = ∀ ⦃State : Type ?u.2⦄ (lts : Cslib.LTS State Label), Cslib.Congruence.r (Cslib.Logic.HML.Proposition.Equiv lts) φ₁ φ₂

@[instance_reducible]

instance Cslib.Logic.HML.instDefaultCongruencePropositionUEquiv {Label : Type u_1} : DefaultCongruence (Proposition Label) Proposition.UEquiv

Equations

• Cslib.Logic.HML.instDefaultCongruencePropositionUEquiv = { }

theorem Cslib.Logic.HML.Proposition.uEquiv_def {Label✝ : Type v} {φ₁ φ₂ : Proposition Label✝} : φ₁.UEquiv φ₂ ↔ Congruence.r UEquiv φ₁ φ₂

theorem Cslib.Logic.HML.Proposition.uEquiv_iff_forall_equiv {Label : Type v} (φ₁ φ₂ : Proposition Label) : Congruence.r UEquiv φ₁ φ₂ ↔ ∀ {State : Type u} (lts : LTS State Label), Congruence.r (Equiv lts) φ₁ φ₂

instance Cslib.Logic.HML.instIsEquivPropositionUEquiv {Label : Type u_1} : IsEquiv (Proposition Label) Proposition.UEquiv

Universal logical equivalence is an equivalence relation.

instance Cslib.Logic.HML.instLawfulCongruencePropositionUEquiv {Label : Type u_1} : LawfulCongruence Proposition.UEquiv

Universal logical equivalence is a lawful congruence.

@[instance_reducible]

instance Cslib.Logic.HML.instLogicalEquivalencePropositionJudgementDefaultUEquiv {State : Type u_1} {Label : Type u_2} : LogicalEquivalence InferenceSystem.Default Proposition.UEquiv

Equations

• Cslib.Logic.HML.instLogicalEquivalencePropositionJudgementDefaultUEquiv = { toLawfulCongruence := ⋯, eqvFillValid := ⋯ }

Database of logical equivalences

theorem Cslib.Logic.HML.Proposition.false_and_false_eqv_false {Label : Type u_1} : DefaultCongruence.r (HasAnd.and ⊥ ⊥) ⊥

theorem Cslib.Logic.HML.Proposition.dual {Label : Type u_1} (μ : Label) (φ : Proposition Label) : DefaultCongruence.r (HasDynamicDiamond.dynDiamond μ φ) (HasNot.not (HasDynamicBox.dynBox μ (HasNot.not φ)))

The dual axiom (reformulated for HML from modal logic).