locus: Blueprint

7.4. Congruence🔗

In this section \sim is the library's bisimilarity, whose labels are contexts and which is a congruence under the hypotheses stated at Theorem 4.2.2 (for bigraphs, Theorem 4.2.3), while \sim_t is the strong bisimilarity over rule tags of the closed-system sections above (written \sim there) and \sim_r is the same with every tag forgotten; no theorem relates \sim_t or the weak \approx over tags to the library's \sim. Agents are ground agents a, b : \varepsilon \to I of hard bigraphs, and composition is partial, so a statement about a context C is about a C composable with both agents.

Definition7.4.1
uses 0
Used by 5
Reverse dependency previews
Preview
Theorem 7.4.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsbridgednot audited

A formula of the tracked logic is closed when it has no free first-order and no free fixpoint variable. For tracked rule lists \mathcal{R}_1, \mathcal{R}_2, write (\mathcal{R}_1, a) \equiv (\mathcal{R}_2, b) when the two systems satisfy the same closed formulas at the empty valuation, a \equiv_{\mathcal{R}} b for the case \mathcal{R}_1 = \mathcal{R}_2 = \mathcal{R}, and (\mathcal{R}_1, a) \equiv^{\forall} (\mathcal{R}_2, b) when they satisfy the same formulas, closed or not, at every valuation (free fixpoint variables read as false). For a family of labelled reaction relations a \xrightarrow{t} a' on the agents of a wide reactive system, \sim_\ell is the largest bisimulation; the contextual closure of a relation Q is a \mathrel{Q^c} b \iff \forall C, x, y.\; C \circ a = x \wedge C \circ b = y \Rightarrow x \mathrel{Q} y; saturated bisimilarity \sim_{\mathrm{sat}} is the largest relation R such that a \mathrel{R} b, C \circ a = x, C \circ b = y and x \xrightarrow{t} x' give a y' with y \xrightarrow{t} y' and x' \mathrel{R} y', and symmetrically (after Bonchi, König and Montanari, Saturated semantics for reactive systems, 2006); and Q is a congruence when a \mathrel{Q} b, C \circ a = x, C \circ b = y imply x \mathrel{Q} y. The labels are the rule tags for \sim_t, and a single label, the reaction relation, for \sim_r.

Class: PForm.Closed not audited; LEq, LEq2, Congr.PEquiv, Congr.LBisim, Congr.CtxCl, Congr.SatBisim, Congr.IsCongr BRIDGED.

Lean code for Definition7.4.1●8 definitions
  • defdefined in Logic/CongruenceChar.lean
    complete
    def Closed {α Ctrl : Type} (φ : PForm α Ctrl) : Prop
    def Closed {α Ctrl : Type}
  (φ : PForm α Ctrl) : Prop
    **A closed formula**: no free first-order variable (`PForm.fvIn`, the
library's free variables) and no free fixpoint variable.
  • defdefined in Logic/CongruenceChar.lean
    complete
    def LEq {α : Type} [DecidableEq α] {Ctrl : Type} [DecidableEq Ctrl]
  {J : Face} (S : Bigraph.Sig Ctrl) (trs : List (TrRule α Ctrl))
  (a b : BigH S Face.origin J) : Prop
    def LEq {α : Type} [DecidableEq α]
  {Ctrl : Type} [DecidableEq Ctrl]
  {J : Face} (S : Bigraph.Sig Ctrl)
  (trs : List (TrRule α Ctrl))
  (a b : BigH S Face.origin J) : Prop
    **Logical equivalence** `(ℛ, a) ≡ (ℛ, b)`: the same closed formulas
hold (at the empty valuation `PVal.empty`; a closed formula has no free fixpoint
variable for the environment to interpret).
  • defdefined in Logic/TagGaps.lean
    complete
    def LEq2 {α : Type} [DecidableEq α] {Ctrl : Type} [DecidableEq Ctrl]
  {J : Face} (S : Bigraph.Sig Ctrl) (trs₁ trs₂ : List (TrRule α Ctrl))
  (a b : BigH S Face.origin J) : Prop
    def LEq2 {α : Type} [DecidableEq α]
  {Ctrl : Type} [DecidableEq Ctrl]
  {J : Face} (S : Bigraph.Sig Ctrl)
  (trs₁ trs₂ : List (TrRule α Ctrl))
  (a b : BigH S Face.origin J) : Prop
    **Logical equivalence of two tracked systems over one signature**, as
displayed in `docs/logic-congruence.md` § 1:

  (ℛ₁, a) ≡ (ℛ₂, b)  :⟺  ∀ closed φ. (ℛ₁, a ⊨ φ ⟺ ℛ₂, b ⊨ φ)

with `⊨` the tracked logic's `PSat` at the empty valuation
`PVal.empty`, free fixpoint variables read as false, and "closed"
`PForm.Closed`. `a` and `b` are ground agents of one face. `LEq` is the
case `ℛ₁ = ℛ₂`; `Congr.PEquiv` quantifies over all formulas and all
valuations and implies it.
  • defdefined in Logic/Congruence.lean
    complete
    def PEquiv {α : Type} [DecidableEq α] {Ctrl : Type} [DecidableEq Ctrl]
  (S : Bigraph.Sig Ctrl) (trs₁ trs₂ : List (TrRule α Ctrl)) {J : Face}
  (a b : BigH S Face.origin J) : Prop
    def PEquiv {α : Type} [DecidableEq α]
  {Ctrl : Type} [DecidableEq Ctrl]
  (S : Bigraph.Sig Ctrl)
  (trs₁ trs₂ : List (TrRule α Ctrl))
  {J : Face}
  (a b : BigH S Face.origin J) : Prop
    **Logical equivalence of two systems** for the tracked logic:
`(ℛ₁, a) ≡ (ℛ₂, b)`, every formula at every valuation (free fixpoint
variables read as false).
  • defdefined in Logic/Congruence.lean
    complete
    def LBisim.{u, v} (W : WRS) {Λ : Type} (Rc : Congr.LRel W Λ) {I : W.Obj}
  (a b : W.Hom W.origin I) : Prop
    def LBisim.{u, v} (W : WRS) {Λ : Type}
  (Rc : Congr.LRel W Λ) {I : W.Obj}
  (a b : W.Hom W.origin I) : Prop
    **Bisimilarity** for the labelled reactions (`∼_t` for tags, `∼_r` for one label).
  • defdefined in Logic/Congruence.lean
    complete
    def CtxCl.{u, v} (W : WRS) (Q : W.ARel) : W.ARel
    def CtxCl.{u, v} (W : WRS) (Q : W.ARel) :
  W.ARel
    **The contextual closure** `Qᶜ`: `a Qᶜ b` iff `C ∘ a Q C ∘ b` for every
context `C` composable with both.
  • defdefined in Logic/Congruence.lean
    complete
    def SatBisim.{u, v} (W : WRS) {Λ : Type} (Rc : Congr.LRel W Λ) {I : W.Obj}
  (a b : W.Hom W.origin I) : Prop
    def SatBisim.{u, v} (W : WRS) {Λ : Type}
  (Rc : Congr.LRel W Λ) {I : W.Obj}
  (a b : W.Hom W.origin I) : Prop
    **Saturated bisimilarity** `∼_sat`.
  • defdefined in Logic/Congruence.lean
    complete
    def IsCongr.{u, v} (W : WRS) (Q : W.ARel) : Prop
    def IsCongr.{u, v} (W : WRS) (Q : W.ARel) :
  Prop
    **A congruence**: a relation on agents preserved by every context
composable with both sides.
Theorem7.4.2
Statement uses 2
Statement dependency previews
Preview
Definition 7.4.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

Within one tracked rule list, the tracked logic sees a ground agent exactly up to support equivalence, whatever the rules:

a \equiv_{\mathcal{R}} b \;\iff\; a \bumpeq b .

The same holds with all formulas at the empty valuation in place of the closed ones.

Lean code for Theorem7.4.2●3 theorems
  • theoremdefined in Logic/CongruenceChar.lean
    complete
    theorem c1 {α : Type} [DecidableEq α] {Ctrl : Type} [DecidableEq Ctrl]
  {S : Bigraph.Sig Ctrl} {J : Face} (trs : List (TrRule α Ctrl))
  (a b : BigH S Face.origin J) : a ≡ₚ[trs] b ↔ SEq S a b
    theorem c1 {α : Type} [DecidableEq α]
  {Ctrl : Type} [DecidableEq Ctrl]
  {S : Bigraph.Sig Ctrl} {J : Face}
  (trs : List (TrRule α Ctrl))
  (a b : BigH S Face.origin J) :
  a ≡ₚ[trs] b ↔ SEq S a b
    **C1**: for one rule set, logical equivalence is support equivalence.

(∀ φ closed. (ℛ, a) ⊨ φ ↔ (ℛ, b) ⊨ φ)  ↔  a ≏ b
  • theoremdefined in Logic/TagGaps.lean
    complete
    theorem c1_lEq2 {α : Type} [DecidableEq α] {Ctrl : Type} [DecidableEq Ctrl]
  {S : Bigraph.Sig Ctrl} {J : Face} (trs : List (TrRule α Ctrl))
  (a b : BigH S Face.origin J) : LEq2 S trs trs a b ↔ SEq S a b
    theorem c1_lEq2 {α : Type} [DecidableEq α]
  {Ctrl : Type} [DecidableEq Ctrl]
  {S : Bigraph.Sig Ctrl} {J : Face}
  (trs : List (TrRule α Ctrl))
  (a b : BigH S Face.origin J) :
  LEq2 S trs trs a b ↔ SEq S a b
    **P8 (ii), C1 restated**: for one rule set, `LEq2` is support
equivalence.

  (∀ φ closed. (ℛ, a) ⊨ φ ↔ (ℛ, b) ⊨ φ)  ↔  a ≏ b
  • theoremdefined in Logic/CongruenceChar.lean
    complete
    theorem c1_all {α : Type} [DecidableEq α] {Ctrl : Type} [DecidableEq Ctrl]
  {S : Bigraph.Sig Ctrl} {J : Face} (trs : List (TrRule α Ctrl))
  (a b : BigH S Face.origin J) : LEqAll S trs a b ↔ SEq S a b
    theorem c1_all {α : Type} [DecidableEq α]
  {Ctrl : Type} [DecidableEq Ctrl]
  {S : Bigraph.Sig Ctrl} {J : Face}
  (trs : List (TrRule α Ctrl))
  (a b : BigH S Face.origin J) :
  LEqAll S trs a b ↔ SEq S a b
    C1 for all formulas at the empty valuation: the same relation.
Theorem7.4.3
uses 1used by 0✓L∃∀N

Within one rule list, logical equivalence for the tracked logic is a congruence for composition: for every context C : I \to K,

a \equiv_{\mathcal{R}} b, \quad C \circ a = x, \quad C \circ b = y \;\Longrightarrow\; x \equiv_{\mathcal{R}} y .

Lean code for Theorem7.4.3●1 theorem
  • theoremdefined in Logic/CongruenceChar.lean
    complete
    theorem lEq_comp {α : Type} [DecidableEq α] {Ctrl : Type} [DecidableEq Ctrl]
  {S : Bigraph.Sig Ctrl} {J : Face} (trs : List (TrRule α Ctrl))
  {K : Face} {a b : BigH S Face.origin J} {C : BigH S J K}
  {ca cb : BigH S Face.origin K} (h : a ≡ₚ[trs] b) (ha : C ◦ a ≃ ca)
  (hb : C ◦ b ≃ cb) : ca ≡ₚ[trs] cb
    theorem lEq_comp {α : Type} [DecidableEq α]
  {Ctrl : Type} [DecidableEq Ctrl]
  {S : Bigraph.Sig Ctrl} {J : Face}
  (trs : List (TrRule α Ctrl)) {K : Face}
  {a b : BigH S Face.origin J}
  {C : BigH S J K}
  {ca cb : BigH S Face.origin K}
  (h : a ≡ₚ[trs] b) (ha : C ◦ a ≃ ca)
  (hb : C ◦ b ≃ cb) : ca ≡ₚ[trs] cb
    **Logical equivalence is a congruence for composition**: `a ≡ b` gives
`C ∘ a ≡ C ∘ b` for every context `C : J → K`.
Theorem7.4.4
Statement uses 2
Statement dependency previews
Preview
Definition 7.4.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

Across two rule lists, logical equivalence for the tracked logic is not preserved by contexts. REFUTED, over the signature with atomic controls K, K', L, M, Z of arity 0 and for \mathcal{R}_1 = \{K \to L : t\}, \mathcal{R}_2 = \emptyset, is the statement that for all a, b, C, x, y,

(\mathcal{R}_1, a) \equiv (\mathcal{R}_2, b), \quad C \circ a = x, \quad C \circ b = y \;\Longrightarrow\; (\mathcal{R}_1, x) \equiv (\mathcal{R}_2, y) ,

and likewise with \equiv^{\forall} throughout. The countermodel is the unit \mathrm{id}_\varepsilon : \varepsilon \to \varepsilon on both sides, composed with the ground agent K: the closed formula \Diamond_t \top holds of K under \mathcal{R}_1 only. In general (\mathcal{R}_1, a) \equiv^{\forall} (\mathcal{R}_2, b) implies (\mathcal{R}_1, a) \equiv (\mathcal{R}_2, b).

Rests on NEW: Congr.C2.R₁, Congr.C2.R₂; not audited: Congr.Ctl, Congr.sig.

Lean code for Theorem7.4.4●3 theorems
  • theoremdefined in Logic/Congruence.lean
    complete
    theorem c2 :
  ¬∀ {I J : Face} (a b : BigH Congr.sig Face.origin I)
      (C : BigH Congr.sig I J) (x y : BigH Congr.sig Face.origin J),
      Congr.PEquiv Congr.sig Congr.C2.R₁ Congr.C2.R₂ a b →
        C ◦ a ≃ x →
          C ◦ b ≃ y → Congr.PEquiv Congr.sig Congr.C2.R₁ Congr.C2.R₂ x y
    theorem c2 :
  ¬∀ {I J : Face}
      (a b : BigH Congr.sig Face.origin I)
      (C : BigH Congr.sig I J)
      (x y :
        BigH Congr.sig Face.origin J),
      Congr.PEquiv Congr.sig Congr.C2.R₁
          Congr.C2.R₂ a b →
        C ◦ a ≃ x →
          C ◦ b ≃ y →
            Congr.PEquiv Congr.sig
              Congr.C2.R₁ Congr.C2.R₂ x y
    **C2. Across rule sets, logical equivalence for the tracked logic is not
a congruence**: `(ℛ₁, id_ε) ≡ (ℛ₂, id_ε)`, but in the context `K ∥ –`
the two systems are separated by `⟨t⟩tt`. REFUTED (kernel-checked).
  • theoremdefined in Logic/TagGaps.lean
    complete
    theorem c2_lEq2 :
  ¬∀ {I J : Face} (a b : BigH Congr.sig Face.origin I)
      (C : BigH Congr.sig I J) (x y : BigH Congr.sig Face.origin J),
      LEq2 Congr.sig Congr.C2.R₁ Congr.C2.R₂ a b →
        C ◦ a ≃ x →
          C ◦ b ≃ y → LEq2 Congr.sig Congr.C2.R₁ Congr.C2.R₂ x y
    theorem c2_lEq2 :
  ¬∀ {I J : Face}
      (a b : BigH Congr.sig Face.origin I)
      (C : BigH Congr.sig I J)
      (x y :
        BigH Congr.sig Face.origin J),
      LEq2 Congr.sig Congr.C2.R₁
          Congr.C2.R₂ a b →
        C ◦ a ≃ x →
          C ◦ b ≃ y →
            LEq2 Congr.sig Congr.C2.R₁
              Congr.C2.R₂ x y
    **P8 (iii), C2 restated for `LEq2`. Across two rule sets, the logical
equivalence of § 1 is not preserved by contexts**:
`(ℛ₁, id_ε) ≡ (ℛ₂, id_ε)`, but in the context `K ∥ –` the closed formula
`⟨t⟩tt` separates the two systems. REFUTED (kernel-checked).
  • theoremdefined in Logic/TagGaps.lean
    complete
    theorem lEq2_of_pEquiv {α : Type} [DecidableEq α] {Ctrl : Type}
  [DecidableEq Ctrl] {S : Bigraph.Sig Ctrl} {J : Face}
  {trs₁ trs₂ : List (TrRule α Ctrl)} {a b : BigH S Face.origin J}
  (h : Congr.PEquiv S trs₁ trs₂ a b) : LEq2 S trs₁ trs₂ a b
    theorem lEq2_of_pEquiv {α : Type} [DecidableEq α]
  {Ctrl : Type} [DecidableEq Ctrl]
  {S : Bigraph.Sig Ctrl} {J : Face}
  {trs₁ trs₂ : List (TrRule α Ctrl)}
  {a b : BigH S Face.origin J}
  (h : Congr.PEquiv S trs₁ trs₂ a b) :
  LEq2 S trs₁ trs₂ a b
    **P8 (iv)**: equivalence for all formulas at all valuations
(`Congr.PEquiv`) implies `LEq2`.
Theorem7.4.5
Statement uses 2
Statement dependency previews
Preview
Definition 7.2.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

Bisimilarity over rule tags, and reaction bisimilarity, are not congruences. REFUTED, over the same signature and for the rules K \to Z : t, K' \to Z : t, L \mid K \to M : u, M \to Z : t, is

a \sim_t b, \quad C \circ a = x, \quad C \circ b = y \;\Longrightarrow\; x \sim_t y ,

and likewise with \sim_r for the same rules with their tags forgotten. The countermodel is K \sim_t K' in the context L \mid \square: only L \mid K has a reaction tagged u, and only L \mid K has two successive reactions.

Rests on NEW: Congr.C3.trs; not audited: Congr.C3.Wr, Congr.Ctl, Congr.sig, Congr.tW.

Lean code for Theorem7.4.5●2 theorems
  • theoremdefined in Logic/Congruence.lean
    complete
    theorem c3_tagged :
  ¬Congr.IsCongr (Congr.tW Congr.sig) fun {I} =>
      Congr.LBisim (Congr.tW Congr.sig)
        (Congr.tRc Congr.sig Congr.C3.trs)
    theorem c3_tagged :
  ¬Congr.IsCongr (Congr.tW Congr.sig)
      fun {I} =>
      Congr.LBisim (Congr.tW Congr.sig)
        (Congr.tRc Congr.sig Congr.C3.trs)
    **C3, tagged. `∼_t` is not a congruence**: `K ∼_t K′`, but not in the
context `L ∥ –`. REFUTED (kernel-checked).
  • theoremdefined in Logic/Congruence.lean
    complete
    theorem c3_reaction :
  ¬Congr.IsCongr Congr.C3.Wr fun {I} =>
      Congr.LBisim Congr.C3.Wr (Congr.rct Congr.C3.Wr)
    theorem c3_reaction :
  ¬Congr.IsCongr Congr.C3.Wr fun {I} =>
      Congr.LBisim Congr.C3.Wr
        (Congr.rct Congr.C3.Wr)
    **C3, untagged. `∼_r` is not a congruence**: `K ∼_r K′`, but not in the
context `L ∥ –`. REFUTED (kernel-checked).
Theorem7.4.6
Statement uses 2
Statement dependency previews
Preview
Definition 7.4.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

For a BRS over hard bigraphs with any set of parametric rules, the equivalences form a chain:

a \bumpeq b \;\Longrightarrow\; a \sim b \;\Longrightarrow\; a \sim_{\mathrm{sat}} b \;\Longrightarrow\; a \mathrel{(\sim_r)^c} b \;\Longrightarrow\; a \sim_r b .

The last implication is strict for the rules of the previous theorem. For a list of tagged rules, likewise, a \bumpeq b \Rightarrow a \sim_{t,\mathrm{sat}} b \Rightarrow a \mathrel{(\sim_t)^c} b \Rightarrow a \sim_t b. Whether \sim_{\mathrm{sat}} implies \sim, and whether (\sim_r)^c implies \sim_{\mathrm{sat}}, for linear rules, is OPEN.

Rests on NEW: BigraphSim.BD.outFace, BigraphSim.Item, BigraphSim.Par, Congr.C3.trs, TRules; not audited: Congr.C3.Wr, Congr.Ctl, Congr.J1, Congr.sig, Congr.tW.

Lean code for Theorem7.4.6●3 theorems
  • theoremdefined in Logic/Congruence.lean
    complete
    theorem c4 {Ctrl : Type} {S : Bigraph.Sig Ctrl} (rules : PRule S → Prop)
  {I : Face} (a b : BigH S Face.origin I) :
  (a ≏ b → a ∼ b) ∧
    (a ∼ b → Congr.SatBisim (BRS rules) (Congr.rct (BRS rules)) a b) ∧
      (Congr.SatBisim (BRS rules) (Congr.rct (BRS rules)) a b →
          Congr.CtxCl (BRS rules)
            (fun {I} =>
              Congr.LBisim (BRS rules) (Congr.rct (BRS rules)))
            a b) ∧
        (Congr.CtxCl (BRS rules)
            (fun {I} =>
              Congr.LBisim (BRS rules) (Congr.rct (BRS rules)))
            a b →
          Congr.LBisim (BRS rules) (Congr.rct (BRS rules)) a b)
    theorem c4 {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  (rules : PRule S → Prop) {I : Face}
  (a b : BigH S Face.origin I) :
  (a ≏ b → a ∼ b) ∧
    (a ∼ b →
        Congr.SatBisim (BRS rules)
          (Congr.rct (BRS rules)) a b) ∧
      (Congr.SatBisim (BRS rules)
            (Congr.rct (BRS rules)) a b →
          Congr.CtxCl (BRS rules)
            (fun {I} =>
              Congr.LBisim (BRS rules)
                (Congr.rct (BRS rules)))
            a b) ∧
        (Congr.CtxCl (BRS rules)
            (fun {I} =>
              Congr.LBisim (BRS rules)
                (Congr.rct (BRS rules)))
            a b →
          Congr.LBisim (BRS rules)
            (Congr.rct (BRS rules)) a b)
    **C4, the chain** `≏ ⊆ ∼ ⊆ ∼_sat ⊆ (∼_r)ᶜ ⊆ ∼_r` for a BRS over ´BIG_h
(any rule set; no linearity is used). PROVED.
  • theoremdefined in Logic/Congruence.lean
    complete
    theorem c4_tagged {α : Type} [DecidableEq α] {Ctrl : Type} [DecidableEq Ctrl]
  {S : Bigraph.Sig Ctrl} {trs : TRules α Ctrl} {J : Face}
  (a b : BigH S Face.origin J) :
  (SEq S a b → Congr.SatBisim (Congr.tW S) (Congr.tRc S trs) a b) ∧
    (Congr.SatBisim (Congr.tW S) (Congr.tRc S trs) a b →
        Congr.CtxCl (Congr.tW S)
          (fun {I} => Congr.LBisim (Congr.tW S) (Congr.tRc S trs)) a
          b) ∧
      (Congr.CtxCl (Congr.tW S)
          (fun {I} => Congr.LBisim (Congr.tW S) (Congr.tRc S trs)) a b →
        a ∼[trs | trs] b)
    theorem c4_tagged {α : Type} [DecidableEq α]
  {Ctrl : Type} [DecidableEq Ctrl]
  {S : Bigraph.Sig Ctrl}
  {trs : TRules α Ctrl} {J : Face}
  (a b : BigH S Face.origin J) :
  (SEq S a b →
      Congr.SatBisim (Congr.tW S)
        (Congr.tRc S trs) a b) ∧
    (Congr.SatBisim (Congr.tW S)
          (Congr.tRc S trs) a b →
        Congr.CtxCl (Congr.tW S)
          (fun {I} =>
            Congr.LBisim (Congr.tW S)
              (Congr.tRc S trs))
          a b) ∧
      (Congr.CtxCl (Congr.tW S)
          (fun {I} =>
            Congr.LBisim (Congr.tW S)
              (Congr.tRc S trs))
          a b →
        a ∼[trs | trs] b)
    **C4 for tags**: `≏ ⊆ ∼_t,sat ⊆ (∼_t)ᶜ ⊆ ∼_t`.
  • theoremdefined in Logic/Congruence.lean
    complete
    theorem ctxCl_strict :
  ∃ a b,
    Congr.LBisim Congr.C3.Wr (Congr.rct Congr.C3.Wr) a b ∧
      ¬Congr.CtxCl Congr.C3.Wr
          (fun {I} => Congr.LBisim Congr.C3.Wr (Congr.rct Congr.C3.Wr))
          a b
    theorem ctxCl_strict :
  ∃ a b,
    Congr.LBisim Congr.C3.Wr
        (Congr.rct Congr.C3.Wr) a b ∧
      ¬Congr.CtxCl Congr.C3.Wr
          (fun {I} =>
            Congr.LBisim Congr.C3.Wr
              (Congr.rct Congr.C3.Wr))
          a b
    **`(∼_r)ᶜ ⊊ ∼_r`**: the last inclusion of the chain C4 is strict.
Theorem7.4.7
Statement uses 2
Statement dependency previews
Preview
Definition 7.1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

Modalities indexed by contexts characterise the two congruences of the chain. CLASSICAL. Add to the Hennessy–Milner logic over labels (\varphi ::= \top \mid \neg\varphi \mid \varphi \wedge \varphi \mid \langle t \rangle \varphi) a modality C \triangleright \varphi, satisfied by a when (\pi \bullet C) \circ a = x and x \models \varphi for some support translation \pi; let \equiv_{\mathrm{top}} be logical equivalence for formulas C \triangleright \varphi with \varphi free of the new modality, and \equiv_{\triangleright} for all formulas. If the labelled reactions respect support equivalence and are image-finite up to it, then

a \equiv_{\mathrm{top}} b \;\iff\; a \mathrel{(\sim_\ell)^c} b, \qquad a \equiv_{\triangleright} b \;\iff\; a \sim_{\mathrm{sat}} b .

Both hypotheses hold for the tagged reactions of any list of tagged rules.

Rests on UNBRIDGED: Congr.AEquiv, Congr.SEquiv; NEW: Congr.ImgFin, TRules; not audited: Congr.Resp, Congr.tW.

Lean code for Theorem7.4.7●4 theorems
  • theoremdefined in Logic/Congruence.lean
    complete
    theorem c5a.{u, v} {W : WRS} {Λ : Type} {Rc : Congr.LRel W Λ}
  (hresp : Congr.Resp W Rc) (hfin : Congr.ImgFin W Rc) {I : W.Obj}
  {a b : W.Hom W.origin I} :
  Congr.AEquiv W Rc a b ↔
    Congr.CtxCl W (fun {I} => Congr.LBisim W Rc) a b
    theorem c5a.{u, v} {W : WRS} {Λ : Type}
  {Rc : Congr.LRel W Λ}
  (hresp : Congr.Resp W Rc)
  (hfin : Congr.ImgFin W Rc) {I : W.Obj}
  {a b : W.Hom W.origin I} :
  Congr.AEquiv W Rc a b ↔
    Congr.CtxCl W
      (fun {I} => Congr.LBisim W Rc) a b
    **C5a.** Label-HML with top-level context adjuncts characterises the
contextual closure `(∼_ℓ)ᶜ`, for image-finite labelled reactions
respecting `≏`. CLASSICAL (through `lbisim_of_hequiv`); the direction
`(∼_ℓ)ᶜ ⊆ ≡` is constructive (`asat_of_ctxCl`).
  • theoremdefined in Logic/Congruence.lean
    complete
    theorem c5b.{u, v} {W : WRS} {Λ : Type} {Rc : Congr.LRel W Λ}
  (hresp : Congr.Resp W Rc) (hfin : Congr.ImgFin W Rc) {I : W.Obj}
  {a b : W.Hom W.origin I} :
  Congr.SEquiv W Rc a b ↔ Congr.SatBisim W Rc a b
    theorem c5b.{u, v} {W : WRS} {Λ : Type}
  {Rc : Congr.LRel W Λ}
  (hresp : Congr.Resp W Rc)
  (hfin : Congr.ImgFin W Rc) {I : W.Obj}
  {a b : W.Hom W.origin I} :
  Congr.SEquiv W Rc a b ↔
    Congr.SatBisim W Rc a b
    **C5b.** Label-HML with context adjuncts anywhere characterises
saturated bisimilarity `∼_sat`, for image-finite labelled reactions
respecting `≏`. CLASSICAL (the direction `≡ ⊆ ∼_sat`); the direction
`∼_sat ⊆ ≡` is constructive (`ssat_of_satBisim`).
  • theoremdefined in Logic/Congruence.lean
    complete
    theorem c5a_tagged {α : Type} [DecidableEq α] {Ctrl : Type} [DecidableEq Ctrl]
  {S : Bigraph.Sig Ctrl} {trs : TRules α Ctrl} {J : Face}
  (a b : BigH S Face.origin J) :
  Congr.AEquiv (Congr.tW S) (Congr.tRc S trs) a b ↔
    Congr.CtxCl (Congr.tW S)
      (fun {I} => Congr.LBisim (Congr.tW S) (Congr.tRc S trs)) a b
    theorem c5a_tagged {α : Type} [DecidableEq α]
  {Ctrl : Type} [DecidableEq Ctrl]
  {S : Bigraph.Sig Ctrl}
  {trs : TRules α Ctrl} {J : Face}
  (a b : BigH S Face.origin J) :
  Congr.AEquiv (Congr.tW S)
      (Congr.tRc S trs) a b ↔
    Congr.CtxCl (Congr.tW S)
      (fun {I} =>
        Congr.LBisim (Congr.tW S)
          (Congr.tRc S trs))
      a b
    **C5a for tags**: tag-HML with top-level context adjuncts characterises
`(∼_t)ᶜ`. CLASSICAL.
  • theoremdefined in Logic/Congruence.lean
    complete
    theorem c5b_tagged {α : Type} [DecidableEq α] {Ctrl : Type} [DecidableEq Ctrl]
  {S : Bigraph.Sig Ctrl} {trs : TRules α Ctrl} {J : Face}
  (a b : BigH S Face.origin J) :
  Congr.SEquiv (Congr.tW S) (Congr.tRc S trs) a b ↔
    Congr.SatBisim (Congr.tW S) (Congr.tRc S trs) a b
    theorem c5b_tagged {α : Type} [DecidableEq α]
  {Ctrl : Type} [DecidableEq Ctrl]
  {S : Bigraph.Sig Ctrl}
  {trs : TRules α Ctrl} {J : Face}
  (a b : BigH S Face.origin J) :
  Congr.SEquiv (Congr.tW S)
      (Congr.tRc S trs) a b ↔
    Congr.SatBisim (Congr.tW S)
      (Congr.tRc S trs) a b
    **C5b for tags**: tag-HML with context adjuncts anywhere characterises
tagged saturated bisimilarity. CLASSICAL.
Theorem7.4.8
uses 1used by 0✓L∃∀N

The tags partition the library's reaction relation and add or remove nothing. For a list \mathcal{R} of tagged rules, with \mathcal{R}^{-} the list of its rules with the tags dropped (only the rules that pass the rule check take part, on both sides),

(\exists t.\;\; a \xrightarrow{t} a') \;\iff\; a \longrightarrow_{\mathcal{R}^{-}} a' .

The same holds for tracked rules, with some tag and some tracking map on the left.

Rests on NEW: TReact, TRules, TrRule.rules.

Lean code for Theorem7.4.8●2 theorems
  • theoremdefined in Logic/TagGaps.lean
    complete
    theorem exists_tReact_iff {α : Type} [DecidableEq α] {Ctrl : Type}
  [DecidableEq Ctrl] {S : Bigraph.Sig Ctrl} {trs : TRules α Ctrl}
  {J : Face} {a a' : BigH S Face.origin J} :
  (∃ t, TReact S trs t a a') ↔ a ⟶[brsOf S (List.map Prod.snd trs)] a'
    theorem exists_tReact_iff {α : Type}
  [DecidableEq α] {Ctrl : Type}
  [DecidableEq Ctrl]
  {S : Bigraph.Sig Ctrl}
  {trs : TRules α Ctrl} {J : Face}
  {a a' : BigH S Face.origin J} :
  (∃ t, TReact S trs t a a') ↔
    a ⟶[brsOf S (List.map Prod.snd trs)]
      a'
    **P2, tagged rules**: a reaction by the rules of some tag is exactly a
reaction of the BRS of the whole rule list, tags forgotten.
  • theoremdefined in Logic/TagGaps.lean
    complete
    theorem exists_trReact_iff {α : Type} [DecidableEq α] {Ctrl : Type}
  [DecidableEq Ctrl] {S : Bigraph.Sig Ctrl} {trs : List (TrRule α Ctrl)}
  {J : Face} {a a' : BigH S Face.origin J} :
  (∃ t f, TrReact S trs t a a' f) ↔ a ⟶[brsOf S (TrRule.rules trs)] a'
    theorem exists_trReact_iff {α : Type}
  [DecidableEq α] {Ctrl : Type}
  [DecidableEq Ctrl]
  {S : Bigraph.Sig Ctrl}
  {trs : List (TrRule α Ctrl)} {J : Face}
  {a a' : BigH S Face.origin J} :
  (∃ t f, TrReact S trs t a a' f) ↔
    a ⟶[brsOf S (TrRule.rules trs)] a'
    **P2, tracked rules**: a tracked reaction with some tag and some
tracking map is exactly a reaction of the BRS of the whole rule list.