Bisimulation for modal team logics

[AAY24] [Ant25] [Vaa08]

Bisimulation is the canonical equivalence relation on Kripke models that abstracts away from the choice of world-carrier and identifies models no modal formula can distinguish. This file provides the carrier-level bisimulation substrate shared by every team-semantic modal logic in Core/Logic/Modal/: bounded-depth world bisimulation (Definition 3.1 of [AAY24]), state bisimulation lifted to teams (Definition 3.6), and the structural lemmas (Lemma 3.7) that each logic's invariance theorem (BSML Theorem 3.8, the MDL analogue, …) consumes.

Nothing here mentions a Formula type or an eval relation — everything is stated over the bare KripkeModel carrier (access + val). Each logic states its own bisim_invariant_eval against its own evaluation, recursing through these carrier lemmas at the modal step. This file is the genus-level home the per-logic invariance proofs were extracted to once a second consumer (MDL) landed; see Core/Logic/Modal/README.md.

Main declarations

• WorldBisim k M w M' w' — bounded k-bisimulation between pointed worlds.
• StateBisim k M s M' s' — state bisimulation lifting it to teams.
• WorldBisim.refl / .symm / .mono_succ / .mono_le and the StateBisim analogues — the equivalence-relation and depth-monotonicity properties.
• WorldBisim.val_eq, WorldBisim.accessStateBisim — valuation and accessibility-image transfer.
• StateBisim.eq_empty_iff, StateBisim.nonempty_iff — emptiness transfer.
• StateBisim.accessImage — Lemma 3.7(i): per-world accessibility-image bisim.
• StateBisim.splitPreserve — Lemma 3.7(ii): team-split preservation.
• StateBisim.exists_image_subset — sub-team transport (BSML's per-world ◇).
• StateBisim.biUnionAccess — union-of-images preservation (MDL's anti-◇).
• StateBisim.possWitness — single-witness team transport (MDL's ◇-support).

Implementation notes

WorldBisim recurses on k: base case is atom invariance, inductive case adds back/forth on accessibility. The split- and witness-transport lemmas (splitPreserve, exists_image_subset, possWitness) construct the other-side team by Finset.filter over the bisim's existential witnesses, using Classical.choice only inside pure-Prop existentials.

World bisimulation

def Core.Logic.Modal.WorldBisim {W : Type u_1} {W' : Type u_2} [DecidableEq W] [Fintype W] [DecidableEq W'] [Fintype W'] {Atom : Type u_3} : ℕ → KripkeModel W Atom → W → KripkeModel W' Atom → W' → Prop

Bounded-depth bisimulation between pointed worlds across two KripkeModels (Definition 3.1 of [AAY24]). At depth 0, requires only that atoms match. At depth k+1, additionally requires the standard back/forth conditions on accessibility relating depth-k bisimilar successors.

Equations

• One or more equations did not get rendered due to their size.
• Core.Logic.Modal.WorldBisim 0 x✝³ x✝² x✝¹ x✝ = ∀ (p : Atom), x✝³.val p x✝² = x✝¹.val p x✝

theorem Core.Logic.Modal.WorldBisim.refl {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_3} (k : ℕ) (M : KripkeModel W Atom) (w : W) : WorldBisim k M w M w

World bisimulation is reflexive at every depth.

theorem Core.Logic.Modal.WorldBisim.symm {W : Type u_1} {W' : Type u_2} [DecidableEq W] [Fintype W] [DecidableEq W'] [Fintype W'] {Atom : Type u_3} {k : ℕ} {M : KripkeModel W Atom} {w : W} {M' : KripkeModel W' Atom} {w' : W'} : WorldBisim k M w M' w' → WorldBisim k M' w' M w

World bisimulation is symmetric (swap models).

theorem Core.Logic.Modal.WorldBisim.mono_succ {W : Type u_1} {W' : Type u_2} [DecidableEq W] [Fintype W] [DecidableEq W'] [Fintype W'] {Atom : Type u_3} {k : ℕ} {M : KripkeModel W Atom} {w : W} {M' : KripkeModel W' Atom} {w' : W'} : WorldBisim (k + 1) M w M' w' → WorldBisim k M w M' w'

Bisimilarity at depth k+1 implies bisimilarity at depth k: higher depths are stricter.

theorem Core.Logic.Modal.WorldBisim.mono_le {W : Type u_1} {W' : Type u_2} [DecidableEq W] [Fintype W] [DecidableEq W'] [Fintype W'] {Atom : Type u_3} {m n : ℕ} (hmn : m ≤ n) {M : KripkeModel W Atom} {w : W} {M' : KripkeModel W' Atom} {w' : W'} : WorldBisim n M w M' w' → WorldBisim m M w M' w'

Bisimilarity is monotone in depth: m ≤ n → WorldBisim n → WorldBisim m.

State bisimulation

def Core.Logic.Modal.StateBisim {W : Type u_1} {W' : Type u_2} [DecidableEq W] [Fintype W] [DecidableEq W'] [Fintype W'] {Atom : Type u_3} (k : ℕ) (M : KripkeModel W Atom) (s : Finset W) (M' : KripkeModel W' Atom) (s' : Finset W') : Prop

State bisimulation (Definition 3.6 of [AAY24]): every world in s is k-bisimilar to some world in s', and every world in s' is k-bisimilar to some world in s. Lifts world bisimulation from points to teams.

Equations

• Core.Logic.Modal.StateBisim k M s M' s' = ((∀ w ∈ s, ∃ w' ∈ s', Core.Logic.Modal.WorldBisim k M w M' w') ∧ ∀ w' ∈ s', ∃ w ∈ s, Core.Logic.Modal.WorldBisim k M w M' w')

theorem Core.Logic.Modal.StateBisim.refl {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_3} (k : ℕ) (M : KripkeModel W Atom) (s : Finset W) : StateBisim k M s M s

theorem Core.Logic.Modal.StateBisim.symm {W : Type u_1} {W' : Type u_2} [DecidableEq W] [Fintype W] [DecidableEq W'] [Fintype W'] {Atom : Type u_3} {k : ℕ} {M : KripkeModel W Atom} {s : Finset W} {M' : KripkeModel W' Atom} {s' : Finset W'} : StateBisim k M s M' s' → StateBisim k M' s' M s

theorem Core.Logic.Modal.StateBisim.mono_succ {W : Type u_1} {W' : Type u_2} [DecidableEq W] [Fintype W] [DecidableEq W'] [Fintype W'] {Atom : Type u_3} {k : ℕ} {M : KripkeModel W Atom} {s : Finset W} {M' : KripkeModel W' Atom} {s' : Finset W'} : StateBisim (k + 1) M s M' s' → StateBisim k M s M' s'

theorem Core.Logic.Modal.StateBisim.mono_le {W : Type u_1} {W' : Type u_2} [DecidableEq W] [Fintype W] [DecidableEq W'] [Fintype W'] {Atom : Type u_3} {m n : ℕ} (hmn : m ≤ n) {M : KripkeModel W Atom} {s : Finset W} {M' : KripkeModel W' Atom} {s' : Finset W'} : StateBisim n M s M' s' → StateBisim m M s M' s'

Helpers for the invariance theorems

theorem Core.Logic.Modal.WorldBisim.val_eq {W : Type u_1} {W' : Type u_2} [DecidableEq W] [Fintype W] [DecidableEq W'] [Fintype W'] {Atom : Type u_3} {k : ℕ} {M : KripkeModel W Atom} {w : W} {M' : KripkeModel W' Atom} {w' : W'} (h : WorldBisim k M w M' w') (p : Atom) : M.val p w = M'.val p w'

World bisimilarity at any depth preserves atom valuations.

theorem Core.Logic.Modal.WorldBisim.accessStateBisim {W : Type u_1} {W' : Type u_2} [DecidableEq W] [Fintype W] [DecidableEq W'] [Fintype W'] {Atom : Type u_3} {k : ℕ} {M : KripkeModel W Atom} {w : W} {M' : KripkeModel W' Atom} {w' : W'} (h : WorldBisim (k + 1) M w M' w') : StateBisim k M (M.access w) M' (M'.access w')

World bisim at depth k+1 yields state bisim of the accessibility images at depth k.

theorem Core.Logic.Modal.StateBisim.eq_empty_iff {W : Type u_1} {W' : Type u_2} [DecidableEq W] [Fintype W] [DecidableEq W'] [Fintype W'] {Atom : Type u_3} {k : ℕ} {M : KripkeModel W Atom} {s : Finset W} {M' : KripkeModel W' Atom} {s' : Finset W'} (h : StateBisim k M s M' s') : s = ∅ ↔ s' = ∅

State bisim preserves emptiness: s = ∅ ↔ s' = ∅. The back/forth conditions force any worlds on one side to have partners on the other, so emptiness is mutually determined.

theorem Core.Logic.Modal.StateBisim.nonempty_iff {W : Type u_1} {W' : Type u_2} [DecidableEq W] [Fintype W] [DecidableEq W'] [Fintype W'] {Atom : Type u_3} {k : ℕ} {M : KripkeModel W Atom} {s : Finset W} {M' : KripkeModel W' Atom} {s' : Finset W'} (h : StateBisim k M s M' s') : s.Nonempty ↔ s'.Nonempty

State bisim preserves nonemptiness.

theorem Core.Logic.Modal.StateBisim.exists_image_subset {W : Type u_1} {W' : Type u_2} [DecidableEq W] [Fintype W] [DecidableEq W'] [Fintype W'] {Atom : Type u_3} {k : ℕ} {M : KripkeModel W Atom} {s t : Finset W} {M' : KripkeModel W' Atom} {s' : Finset W'} (h : StateBisim k M s M' s') (hsub : t ⊆ s) : ∃ t' ⊆ s', (t.Nonempty → t'.Nonempty) ∧ StateBisim k M t M' t'

Given s ⇌_k s' and a sub-team t ⊆ s, there exists a corresponding sub-team t' ⊆ s' such that t ⇌_k t'. Non-emptiness transfers. Used by the per-world poss-support case of BSML's invariance proof.

Lemma 3.7: state bisimulation preserves modal step and team splits

theorem Core.Logic.Modal.StateBisim.accessImage {W : Type u_1} {W' : Type u_2} [DecidableEq W] [Fintype W] [DecidableEq W'] [Fintype W'] {Atom : Type u_3} {k : ℕ} {M : KripkeModel W Atom} {s : Finset W} {M' : KripkeModel W' Atom} {s' : Finset W'} {w : W} (h : StateBisim (k + 1) M s M' s') (hw : w ∈ s) : ∃ w' ∈ s', StateBisim k M (M.access w) M' (M'.access w')

Lemma 3.7(i) of [AAY24]: at depth k+1, state bisim provides for each w ∈ s a witness w' ∈ s' such that the accessibility images R[w] and R'[w'] are state-bisimilar at depth k.

theorem Core.Logic.Modal.StateBisim.splitPreserve {W : Type u_1} {W' : Type u_2} [DecidableEq W] [Fintype W] [DecidableEq W'] [Fintype W'] {Atom : Type u_3} {k : ℕ} {M : KripkeModel W Atom} {s t u : Finset W} {M' : KripkeModel W' Atom} {s' : Finset W'} (h : StateBisim k M s M' s') (hsplit : Team.splitsAs s t u) (htsub : t ⊆ s) (husub : u ⊆ s) : ∃ (t' : Finset W') (u' : Finset W'), Team.splitsAs s' t' u' ∧ StateBisim k M t M' t' ∧ StateBisim k M u M' u'

Lemma 3.7(ii) of [AAY24]: state bisim preserves binary team splits. Given s = t ∪ u and s ⇌_k s', there exist t', u' ⊆ s' with s' = t' ∪ u', t ⇌_k t', and u ⇌_k u'.

Constructed via classical choice over the bisim's existential witnesses: t' collects all of s''s witnesses for t, and u' likewise for u.

Single-relation modal step (Väänänen-style ◇)

The MDL modality uses the union of accessibility images (anti-support) and a single witness team (support), rather than BSML's per-world sub-witness. These two lemmas are the Lemma 3.7 analogues for that modality.

theorem Core.Logic.Modal.StateBisim.biUnionAccess {W : Type u_1} {W' : Type u_2} [DecidableEq W] [Fintype W] [DecidableEq W'] [Fintype W'] {Atom : Type u_3} {k : ℕ} {M : KripkeModel W Atom} {s : Finset W} {M' : KripkeModel W' Atom} {s' : Finset W'} (h : StateBisim (k + 1) M s M' s') : StateBisim k M (s.biUnion M.access) M' (s'.biUnion M'.access)

State bisim at depth k+1 preserves the union of accessibility images at depth k: s.biUnion R ⇌_k s'.biUnion R'. The MDL anti-◇ clause ([Vaa08] (T9)) evaluates the inner formula on this union.

theorem Core.Logic.Modal.StateBisim.possWitness {W : Type u_1} {W' : Type u_2} [DecidableEq W] [Fintype W] [DecidableEq W'] [Fintype W'] {Atom : Type u_3} {k : ℕ} {M : KripkeModel W Atom} {s : Finset W} {M' : KripkeModel W' Atom} {s' : Finset W'} (h : StateBisim (k + 1) M s M' s') {Y : Finset W} (hYsub : Y ⊆ s.biUnion M.access) (hwit : ∀ w ∈ s, ∃ y ∈ Y, y ∈ M.access w) : ∃ Y' ⊆ s'.biUnion M'.access, (∀ w' ∈ s', ∃ y' ∈ Y', y' ∈ M'.access w') ∧ StateBisim k M Y M' Y'

Single-witness team transport. Given s ⇌_{k+1} s' and a witness team Y ⊆ s.biUnion R that every world in s reaches (∀ w ∈ s, ∃ y ∈ Y ∩ R[w]), there is a corresponding Y' ⊆ s'.biUnion R' that every world in s' reaches, with Y ⇌_k Y'. This is the Lemma 3.7 analogue for the MDL ◇-support clause ([Vaa08] (T8)). The Y ⊆ s.biUnion R hypothesis is supplied by the caller via downward closure (shrinking a raw witness to its reachable part).