Logical Equivalence in HML

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

def Cslib.Logic.HML.Proposition.Equiv {State : Type u} {Label : Type v} (a b : Proposition Label) : Prop

Logical equivalence for HML propositions.

Equations

• a.Equiv b = ∀ (lts : Cslib.LTS State Label), a.denotation lts = b.denotation lts

theorem Cslib.Logic.HML.Proposition.equiv_def {State : Type u} {Label : Type v} (a b : Proposition Label) : a.Equiv b ↔ ∀ (lts : LTS State Label), a.denotation lts = b.denotation lts

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
• orL {Label : Type u} (c : Context Label) (φ : Proposition Label) : Context Label
• orR {Label : Type u} (φ : Proposition Label) (c : Context Label) : Context Label
• diamond {Label : Type u} (μ : Label) (c : Context Label) : Context Label
• box {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.orL φ').fill φ = (c_2.fill φ).or φ'
• (Cslib.Logic.HML.Proposition.Context.orR φ' c_2).fill φ = φ'.or (c_2.fill φ)
• (Cslib.Logic.HML.Proposition.Context.diamond μ c_2).fill φ = Cslib.Logic.HML.Proposition.diamond μ (c_2.fill φ)
• (Cslib.Logic.HML.Proposition.Context.box μ c_2).fill φ = Cslib.Logic.HML.Proposition.box μ (c_2.fill φ)

@[implicit_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 }

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

instance Cslib.Logic.HML.instCongruencePropositionEquiv {State : Type u} {Label : Type v} : Congruence (Proposition Label) Proposition.Equiv

structure Cslib.Logic.HML.Satisfies.Judgement (State : Type u) (Label : Type v) : Type (max u v)

Bundled version of a judgement for Satisfy.

• lts : LTS State Label

  The state transition system to consider.

• state : State

  The state to check the proposition against.

• φ : Proposition Label

  The proposition to check.

def Cslib.Logic.HML.Satisfies.Bundled {State : Type u_1} {Label : Type u_2} (j : Judgement State Label) : Prop

Satisfies variant using bundled judgements.

Equations

• Cslib.Logic.HML.Satisfies.Bundled j = Cslib.Logic.HML.Satisfies j.lts j.state j.φ

theorem Cslib.Logic.HML.Satisfies.bundled_char {State✝ : Type u_1} {Label✝ : Type u_2} {j : Judgement State✝ Label✝} : Bundled j ↔ Satisfies j.lts j.state j.φ

structure Cslib.Logic.HML.Satisfies.Context (State : Type u) (Label : Type v) : Type (max u v)

Judgemental contexts.

• lts : LTS State Label

  The state transition system to consider.

• state : State

  The state to check propositions against.

def Cslib.Logic.HML.Satisfies.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, φ := φ }

@[implicit_reducible]

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

Equations

• Cslib.Logic.HML.judgementalContext = { Context := Cslib.Logic.HML.Satisfies.Context State Label, fill := Cslib.Logic.HML.Satisfies.Context.fill }

@[implicit_reducible]

instance Cslib.Logic.HML.instLogicalEquivalencePropositionJudgementBundled {Label : Type u_1} {State : Type u_2} : LogicalEquivalence (Proposition Label) (Satisfies.Judgement State Label) Satisfies.Bundled

Equations

• Cslib.Logic.HML.instLogicalEquivalencePropositionJudgementBundled = { eqv := Cslib.Logic.HML.Proposition.Equiv, congruence := ⋯, eqv_fill_valid := ⋯ }