feat(Studies): translate BSL into modal information logic

Linglib/Core/Data/Set/Sups.lean

@@ -7,19 +7,22 @@ module
 
 public import Mathlib.Data.Set.Sups
 public import Mathlib.Order.CompleteLattice.Basic
+public import Mathlib.Order.UpperLower.Closure
 public import Mathlib.Order.UpperLower.CompleteLattice
 public import Mathlib.Order.SupClosed
 public import Mathlib.Order.Interval.Set.OrdConnected
+public import Linglib.Core.Order.DistribSemilattice
 
 /-!
 # Suprema of pointwise sups
 
 Mirror of `Mathlib/Data/Set/Sups.lean`. Pointwise sups preserve sup-closure and the bottom element
-in any semilattice, and downward closure and order-convexity (the latter given sup-closure) in a
-distributive lattice, where `c ≤ a ⊔ b` splits as `c = (c ⊓ a) ⊔ (c ⊓ b)`. In a complete lattice,
-the supremum of `s ⊻ t` is the join of the suprema of two nonempty sets. The indexed form of
-`s ⊻ t` is `Set.iSups s`, the set of suprema of choices of an element from each member of a family
-`s`. [UPSTREAM]
+in any semilattice, and their sups with `univ` are the upper closure. They preserve downward
+closure and, given sup-closure, order-convexity in a distributive semilattice, and preserving
+downward closure characterizes distributivity. They respect any relation along which splits
+transport both ways. In a complete lattice, the supremum of `s ⊻ t` is the join of the suprema of
+two nonempty sets. The indexed form of `s ⊻ t` is `Set.iSups s`, the set of suprema of choices of
+an element from each member of a family `s`. [UPSTREAM]
 -/
 
 @[expose] public section
@@ -43,30 +46,64 @@ theorem SupClosed.sups (hs : SupClosed s) (ht : SupClosed t) : SupClosed (s ⊻
 theorem Set.bot_mem_sups [OrderBot α] (hs : ⊥ ∈ s) (ht : ⊥ ∈ t) : ⊥ ∈ s ⊻ t :=
   Set.mem_sups.mpr ⟨⊥, hs, ⊥, ht, bot_sup_eq ⊥⟩
 
+/-- The pointwise sups of a set with everything are its upper closure. -/
+theorem Set.sups_univ (s : Set α) : s ⊻ Set.univ = upperClosure s :=
+  Set.ext fun x ↦ ⟨fun hx ↦ let ⟨a, ha, _, _, h⟩ := Set.mem_sups.1 hx
+    mem_upperClosure.2 ⟨a, ha, h ▸ le_sup_left⟩,
+    fun hx ↦ let ⟨a, ha, hax⟩ := mem_upperClosure.1 hx
+      Set.mem_sups.2 ⟨a, ha, x, trivial, sup_eq_right.2 hax⟩⟩
+
+/-- Pointwise sups respect a relation between semilattices along which splits transport both ways:
+if `r` relates `a` to `c`, a split of `a` gives a split of `c` into related parts and conversely,
+then membership in `s₁ ⊻ s₂` and in `t₁ ⊻ t₂` agree on `r` when membership in each pair does. -/
+theorem Set.mem_sups_congr {β : Type*} [SemilatticeSup β] {r : α → β → Prop}
+    (hl : ∀ {a₁ a₂ c}, r (a₁ ⊔ a₂) c → ∃ c₁ c₂, c₁ ⊔ c₂ = c ∧ r a₁ c₁ ∧ r a₂ c₂)
+    (hr : ∀ {a c₁ c₂}, r a (c₁ ⊔ c₂) → ∃ a₁ a₂, a₁ ⊔ a₂ = a ∧ r a₁ c₁ ∧ r a₂ c₂)
+    {s₁ s₂ : Set α} {t₁ t₂ : Set β} (h₁ : ∀ ⦃a c⦄, r a c → (a ∈ s₁ ↔ c ∈ t₁))
+    (h₂ : ∀ ⦃a c⦄, r a c → (a ∈ s₂ ↔ c ∈ t₂)) {a : α} {c : β} (h : r a c) :
+    a ∈ s₁ ⊻ s₂ ↔ c ∈ t₁ ⊻ t₂ := by
+  simp only [Set.mem_sups]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨a₁, ha₁, a₂, ha₂, rfl⟩
+    obtain ⟨c₁, c₂, rfl, hr₁, hr₂⟩ := hl h
+    exact ⟨c₁, (h₁ hr₁).1 ha₁, c₂, (h₂ hr₂).1 ha₂, rfl⟩
+  · rintro ⟨c₁, hc₁, c₂, hc₂, rfl⟩
+    obtain ⟨a₁, a₂, rfl, hr₁, hr₂⟩ := hr h
+    exact ⟨a₁, (h₁ hr₁).2 hc₁, a₂, (h₂ hr₂).2 hc₂, rfl⟩
+
 end SemilatticeSup
 
-section DistribLattice
+section IsDistribSemilatticeSup
 
-variable [DistribLattice α] {s t : Set α}
+variable [SemilatticeSup α] {s t : Set α}
 
-theorem IsLowerSet.sups (hs : IsLowerSet s) (ht : IsLowerSet t) : IsLowerSet (s ⊻ t) := by
+theorem IsLowerSet.sups [IsDistribSemilatticeSup α] (hs : IsLowerSet s) (ht : IsLowerSet t) :
+    IsLowerSet (s ⊻ t) := by
   intro x c hc hx
   obtain ⟨a, ha, b, hb, rfl⟩ := Set.mem_sups.mp hx
-  exact Set.mem_sups.mpr ⟨c ⊓ a, hs inf_le_right ha, c ⊓ b, ht inf_le_right hb,
-    by rw [← inf_sup_left, inf_eq_left.mpr hc]⟩
+  obtain ⟨a', ha', b', hb', rfl⟩ := exists_sup_eq_of_le_sup hc
+  exact Set.sup_mem_sups (hs ha' ha) (ht hb' hb)
 
-theorem Set.OrdConnected.sups (hs : s.OrdConnected) (ht : t.OrdConnected) (hs' : SupClosed s)
-    (ht' : SupClosed t) : (s ⊻ t).OrdConnected := by
+theorem Set.OrdConnected.sups [IsDistribSemilatticeSup α] (hs : s.OrdConnected)
+    (ht : t.OrdConnected) (hs' : SupClosed s) (ht' : SupClosed t) : (s ⊻ t).OrdConnected := by
   rw [Set.ordConnected_iff]
   intro y hy z hz hle x ⟨hx₁, hx₂⟩
   obtain ⟨a, ha, b, hb, rfl⟩ := Set.mem_sups.mp hy
   obtain ⟨c, hc, d, hd, rfl⟩ := Set.mem_sups.mp hz
-  refine Set.mem_sups.mpr ⟨(a ⊔ c) ⊓ x, hs.out ha (hs' ha hc)
-      ⟨le_inf le_sup_left (le_sup_left.trans hx₁), inf_le_left⟩, (b ⊔ d) ⊓ x,
-      ht.out hb (ht' hb hd) ⟨le_inf le_sup_left (le_sup_right.trans hx₁), inf_le_left⟩, ?_⟩
-  rw [← inf_sup_right, sup_sup_sup_comm, sup_eq_right.mpr hle, inf_eq_right.mpr hx₂]
-
-end DistribLattice
+  obtain ⟨e, he, f, hf, rfl⟩ := exists_sup_eq_of_le_sup
+    (hx₂.trans_eq (sup_sup_sup_comm a b c d ▸ sup_eq_right.2 hle).symm)
+  refine Set.mem_sups.mpr ⟨a ⊔ e, hs.out ha (hs' ha hc) ⟨le_sup_left, sup_le le_sup_left he⟩,
+    b ⊔ f, ht.out hb (ht' hb hd) ⟨le_sup_left, sup_le le_sup_left hf⟩, ?_⟩
+  rw [sup_sup_sup_comm, sup_eq_right.2 hx₁]
+
+/-- A semilattice is distributive exactly when pointwise sups of lower sets are lower sets. -/
+theorem isDistribSemilatticeSup_iff_isLowerSet_sups : IsDistribSemilatticeSup α ↔
+    ∀ s t : Set α, IsLowerSet s → IsLowerSet t → IsLowerSet (s ⊻ t) := by
+  refine ⟨fun _ _ _ hs ht ↦ hs.sups ht, fun h ↦ ⟨fun {a b c} hle ↦ ?_⟩⟩
+  exact Set.mem_sups.1 <| h _ _ (isLowerSet_Iic b) (isLowerSet_Iic c) hle
+    (Set.sup_mem_sups Set.self_mem_Iic Set.self_mem_Iic)
+
+end IsDistribSemilatticeSup
 
 end Closure
 

Linglib/Core/Order/DistribSemilattice.lean

@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2026 Robert Hawkins. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robert Hawkins
+-/
+module
+
+public import Mathlib.Order.Directed
+public import Mathlib.Order.SupClosed
+
+/-!
+# Distributive join-semilattices
+
+[UPSTREAM] candidate for a new `Mathlib/Order/DistribSemilattice.lean`.
+
+A join-semilattice is *distributive* when every element below a join `b ⊔ c` is the join of an
+element below `b` and an element below `c`. Every distributive lattice is distributive in this
+sense, and a lattice that is distributive in this sense obeys the distributive law
+([`inf_sup_le`](##IsDistribSemilatticeSup.inf_sup_le)), so the notion extends distributivity to
+semilattices that lack meets. Any two elements of a distributive semilattice have a lower bound,
+and the largest lower set inside a sup-closed set is again sup-closed.
+
+## Main definitions
+
+* `IsDistribSemilatticeSup α`: `α` is a distributive join-semilattice.
+-/
+
+@[expose] public section
+
+variable {α : Type*}
+
+/-- A join-semilattice is distributive when every element below `b ⊔ c` is the join of an element
+below `b` and an element below `c`. -/
+class IsDistribSemilatticeSup (α : Type*) [SemilatticeSup α] : Prop where
+  /-- An element below a join splits along the join. -/
+  exists_sup_eq_of_le_sup {a b c : α} (h : a ≤ b ⊔ c) : ∃ b' ≤ b, ∃ c' ≤ c, b' ⊔ c' = a
+
+export IsDistribSemilatticeSup (exists_sup_eq_of_le_sup)
+
+instance (priority := 100) DistribLattice.toIsDistribSemilatticeSup [DistribLattice α] :
+    IsDistribSemilatticeSup α where
+  exists_sup_eq_of_le_sup {a b c} h :=
+    ⟨a ⊓ b, inf_le_right, a ⊓ c, inf_le_right, by rw [← inf_sup_left, inf_eq_left.2 h]⟩
+
+/-- The distributive law, in a lattice distributive as a semilattice. -/
+theorem IsDistribSemilatticeSup.inf_sup_le [Lattice α] [IsDistribSemilatticeSup α] (a b c : α) :
+    a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c := by
+  obtain ⟨b', hb, c', hc, h⟩ := exists_sup_eq_of_le_sup (inf_le_right : a ⊓ (b ⊔ c) ≤ b ⊔ c)
+  have ha : b' ⊔ c' ≤ a := h.le.trans inf_le_left
+  rw [← h]
+  exact sup_le_sup (le_inf (le_sup_left.trans ha) hb) (le_inf (le_sup_right.trans ha) hc)
+
+variable [SemilatticeSup α] [IsDistribSemilatticeSup α]
+
+instance (priority := 50) IsDistribSemilatticeSup.toIsCodirectedOrder : IsCodirectedOrder α where
+  directed a b :=
+    let ⟨_, _, c, hc, h⟩ := exists_sup_eq_of_le_sup (le_sup_left : a ≤ a ⊔ b)
+    ⟨c, h ▸ le_sup_right, hc⟩
+
+/-- The largest lower set inside a sup-closed set is sup-closed. -/
+theorem SupClosed.setOf_forall_le {s : Set α} (hs : SupClosed s) :
+    SupClosed {x | ∀ y ≤ x, y ∈ s} := fun _ ha _ hb _ hc ↦
+  let ⟨a', ha', b', hb', h⟩ := exists_sup_eq_of_le_sup hc
+  h ▸ hs (ha a' ha') (hb b' hb')

Linglib/Logic/Team/Bisimulation.lean

@@ -174,16 +174,13 @@ theorem _root_.Set.LiftRel.exists_finset_union_eq {s t u : Finset α} {s' : Fins
     (fun h ↦ Finset.mem_filter.2 ⟨hb, a, h, hab⟩) fun h ↦ Finset.mem_filter.2 ⟨hb, a, h, hab⟩
 
 theorem Invariant.tensor (h₁ : Invariant r P P') (h₂ : Invariant r Q Q') :
-    Invariant r (tensor P Q) (tensor P' Q') := by
-  intro s s' hs
-  constructor
-  · rintro ⟨t, ht, u, hu, rfl⟩
-    obtain ⟨t', u', hsplit, htt', huu'⟩ := hs.exists_finset_union_eq rfl
-    exact ⟨t', (h₁ htt').1 ht, u', (h₂ huu').1 hu, hsplit⟩
-  · rintro ⟨t', ht', u', hu', rfl⟩
-    obtain ⟨t, u, hsplit, htt', huu'⟩ := (Set.liftRel_swap.2 hs).exists_finset_union_eq rfl
-    rw [Set.liftRel_swap] at htt' huu'
-    exact ⟨t, (h₁ htt').2 ht', u, (h₂ huu').2 hu', hsplit⟩
+    Invariant r (tensor P Q) (tensor P' Q') := fun _ _ hs ↦
+  Set.mem_sups_congr (r := fun (s : Finset α) (s' : Finset β) ↦ Set.LiftRel r ↑s ↑s')
+    (fun h ↦ h.exists_finset_union_eq rfl)
+    (fun h ↦
+      let ⟨t, u, hsplit, htt', huu'⟩ := (Set.liftRel_swap.2 h).exists_finset_union_eq rfl
+      ⟨t, u, hsplit, Set.liftRel_swap.1 htt', Set.liftRel_swap.1 huu'⟩)
+    h₁ h₂ hs
 
 /-! ### Image modalities of dependence and inclusion logic -/
 

Linglib/Logic/Team/Closure.lean

@@ -46,11 +46,6 @@ infrastructure to consumers of `IsFlat`.
 * [anttila-2021] Anttila, The Logic of Free Choice: Axiomatizations of State-based Modal Logics
 * [anttila-2025] Anttila, Not Nothing: Nonemptiness in Team Semantics
 * [vaananen-2007] Väänänen, Dependence Logic: A New Approach to Independence Friendly Logic
-
-## TODO
-
-* Generalise `IsFlat` to atomistic lattices (`[SemilatticeSup L]
-  [OrderBot L] [IsAtomistic L]`) once a non-`Finset` consumer surfaces.
 -/
 
 @[expose] public section

Linglib/Logic/Truthmaker/Basic.lean

@@ -39,6 +39,8 @@ pooled inexact verifiers of `s` and `t`.
   when conjoining `t` leaves it unchanged.
 * `Truthmaker.isClosed_regularClosure_iff`: the regular propositions are those closed under
   nonempty fusions and convex.
+* `Truthmaker.isClosed_regularClosure_iff_of_finite`: in a finite lattice, the regular propositions
+  are the convex sup-closed sets.
 * `Truthmaker.isConjunctivePart_regularClosure_iff`: regular closure does not change containment.
 * `Truthmaker.regularClosure_eq_iff`: a regular proposition is determined by its inexact verifiers
   and its subject-matter.
@@ -266,6 +268,13 @@ theorem ordConnected_of_isClosed_regularClosure (hs : regularClosure.IsClosed s)
     s.OrdConnected :=
   (isClosed_regularClosure_iff.1 hs).2
 
+/-- In a finite lattice, the regular propositions are the convex sup-closed sets. -/
+theorem isClosed_regularClosure_iff_of_finite [Finite S] :
+    regularClosure.IsClosed s ↔ SupClosed s ∧ s.OrdConnected :=
+  ⟨fun h ↦ ⟨supClosed_of_isClosed_regularClosure h, ordConnected_of_isClosed_regularClosure h⟩,
+    fun ⟨hc, ho⟩ ↦ isClosed_regularClosure_iff.2
+      ⟨fun _ hts ht ↦ hc.sSup_mem_of_nonempty (Set.toFinite _) ht hts, ho⟩⟩
+
 /-- Regular closure preserves containment. -/
 theorem IsConjunctivePart.regularClosure (h : IsConjunctivePart t s) :
     IsConjunctivePart (regularClosure t) (regularClosure s) := by