ProductKripke: Heterogeneous Product of Kripke Structures

Interleaving product ProductKripke x y of two Kripke structures for arbitrary [ToKripke α S₁ D₁] and [ToKripke β S₂ D₂]. This module is independent of StateMachine and develops the pure Kripke-level theory only.

Heterogeneous composition

ProductKripke accepts any two types carrying a ToKripke instance, so the following all use the same API:

• ProductKripke sm₁ sm₂ : Type — two StateMachines
• ProductKripke (pk : ProductKripke sm₁ sm₂) sm₃ : Type — a 3-way nested composition
• ProductKripke ct₁ ct₂ — two continuous-time systems (once ContinuousSystem instances exist)

The specialization ProductStateMachine sm₁ sm₂ for two StateMachine operands is retained as an abbrev in Behavior/Product.lean and simply elaborates to ProductKripke sm₁ sm₂.

Design

ProductKripke x y is an empty structure

The type itself acts as a marker encoding the agreement "take the product of x and y". Values carry no information and are built with ⟨⟩. The structure is kept (rather than using Unit) as an extension point for future metadata such as synchronization tables or labels.

ProductKripkeReachable is interleaving

Each step advances exactly one side — either x or y — while the other side remains unchanged. Synchronous (both-sides-at-once) steps are not modeled.

Invariant preservation

ProductKripkeReachable itself carries no invariant-preservation obligation. The safety result inv_holds is established in two stages:

1. fst_reachable / snd_reachable project the product reachability onto component-level reachability.
2. Each component's reachable_inv field (an axiom of the KripkeStructure record) combines with those projections to derive inv_holds on the product.

This keeps the KripkeStructure definition light: the step relation carries no built-in invariant obligation, and type-level contracts such as Transition.preserves are confined to the component layer.

structure VerifiedMBSE.Behavior.ProductKripke {α β S₁ D₁ S₂ D₂ : Type} [ToKripke α S₁ D₁] [ToKripke β S₂ D₂] (x : α) (y : β) : Type

Marker type for the product of x : α and y : β, given [ToKripke α S₁ D₁] and [ToKripke β S₂ D₂].

An empty structure: values are built with ⟨⟩. The type itself encodes the agreement "consider the product of x and y"; the Kripke semantics are supplied by ProductKripkeReachable and ProductKripke.toKripke.

The explicit mk :: declaration ensures the Lean parser reads the following declaration correctly even though the structure has no fields.

inductive VerifiedMBSE.Behavior.ProductKripkeReachable {α β S₁ D₁ S₂ D₂ : Type} [ToKripke α S₁ D₁] [ToKripke β S₂ D₂] (x : α) (y : β) : S₁ × S₂ → D₁ × D₂ → Prop

Reachability relation for the product Kripke structure, defined as the interleaving product.

• init: starts from any pair of component-level reachable points (s₁, d₁) / (s₂, d₂). Because arbitrary reachable points are admitted, subsequent lifting lemmas (fromLeft, fromRight) do not require induction.
• stepLeft / stepRight: advances (toKripke x).step or (toKripke y).step by one step while the other side remains unchanged.

• init {α β S₁ D₁ S₂ D₂ : Type} [ToKripke α S₁ D₁] [ToKripke β S₂ D₂] {x : α} {y : β} {s₁ : S₁} {s₂ : S₂} {d₁ : D₁} {d₂ : D₂} : (ToKripke.toKripke x).reachable s₁ d₁ → (ToKripke.toKripke y).reachable s₂ d₂ → ProductKripkeReachable x y (s₁, s₂) (d₁, d₂)

  Initial case: start from reachable points of both Kripke structures.

• stepLeft {α β S₁ D₁ S₂ D₂ : Type} [ToKripke α S₁ D₁] [ToKripke β S₂ D₂] {x : α} {y : β} {s₁ : S₁} {s₂ : S₂} {d₁ : D₁} {d₂ : D₂} {s₁' : S₁} {d₁' : D₁} : ProductKripkeReachable x y (s₁, s₂) (d₁, d₂) → (ToKripke.toKripke x).step s₁ d₁ s₁' d₁' → ProductKripkeReachable x y (s₁', s₂) (d₁', d₂)

  Left step: x advances by one step, y remains unchanged.

• stepRight {α β S₁ D₁ S₂ D₂ : Type} [ToKripke α S₁ D₁] [ToKripke β S₂ D₂] {x : α} {y : β} {s₁ : S₁} {s₂ : S₂} {d₁ : D₁} {d₂ : D₂} {s₂' : S₂} {d₂' : D₂} : ProductKripkeReachable x y (s₁, s₂) (d₁, d₂) → (ToKripke.toKripke y).step s₂ d₂ s₂' d₂' → ProductKripkeReachable x y (s₁, s₂') (d₁, d₂')

  Right step: y advances by one step, x remains unchanged.

theorem VerifiedMBSE.Behavior.ProductKripkeReachable.fst_reachable {α β S₁ D₁ S₂ D₂ : Type} [ToKripke α S₁ D₁] [ToKripke β S₂ D₂] {x : α} {y : β} {p : S₁ × S₂} {d : D₁ × D₂} (h : ProductKripkeReachable x y p d) : (ToKripke.toKripke x).reachable p.fst d.fst

Projection: product reachability implies left-component reachability.

The stepLeft case uses the component's step_preserves_reachable axiom; the stepRight case leaves the left component unchanged and returns the induction hypothesis directly.

theorem VerifiedMBSE.Behavior.ProductKripkeReachable.snd_reachable {α β S₁ D₁ S₂ D₂ : Type} [ToKripke α S₁ D₁] [ToKripke β S₂ D₂] {x : α} {y : β} {p : S₁ × S₂} {d : D₁ × D₂} (h : ProductKripkeReachable x y p d) : (ToKripke.toKripke y).reachable p.snd d.snd

Projection: product reachability implies right-component reachability.

theorem VerifiedMBSE.Behavior.ProductKripkeReachable.inv_holds {α β S₁ D₁ S₂ D₂ : Type} [ToKripke α S₁ D₁] [ToKripke β S₂ D₂] {x : α} {y : β} {p : S₁ × S₂} {d : D₁ × D₂} (h : ProductKripkeReachable x y p d) : (ToKripke.toKripke x).inv p.fst d.fst ∧ (ToKripke.toKripke y).inv p.snd d.snd

Product-level safety: a product-reachable state satisfies the invariant of both components.

Extracts component reachability via fst_reachable / snd_reachable and applies each component's reachable_inv axiom. No induction on ProductKripkeReachable itself is required.

theorem VerifiedMBSE.Behavior.ProductKripkeReachable.step_preserves_reachable {α β S₁ D₁ S₂ D₂ : Type} [ToKripke α S₁ D₁] [ToKripke β S₂ D₂] {x : α} {y : β} (p : S₁ × S₂) (d : D₁ × D₂) (p' : S₁ × S₂) (d' : D₁ × D₂) : ProductKripkeReachable x y p d → (ToKripke.toKripke x).step p.fst d.fst p'.fst d'.fst ∧ p.snd = p'.snd ∧ d.snd = d'.snd ∨ (ToKripke.toKripke y).step p.snd d.snd p'.snd d'.snd ∧ p.fst = p'.fst ∧ d.fst = d'.fst → ProductKripkeReachable x y p' d'

The product step preserves reachability.

Supplied to the step_preserves_reachable field of ProductKripke.toKripke. Decomposes the interleaving disjunction and applies stepLeft / stepRight in the respective branches.

theorem VerifiedMBSE.Behavior.ProductKripkeReachable.fromLeft {α β S₁ D₁ S₂ D₂ : Type} [ToKripke α S₁ D₁] [ToKripke β S₂ D₂] {x : α} {y : β} {s₁ : S₁} {d₁ : D₁} (hr₁ : (ToKripke.toKripke x).reachable s₁ d₁) (hne₂ : (ToKripke.toKripke y).NonEmpty) : ∃ (s₂ : S₂), ∃ (d₂ : D₂), ProductKripkeReachable x y (s₁, s₂) (d₁, d₂)

Lifting: construct product reachability from a left-component reachable point together with a NonEmpty witness on the right.

Because ProductKripkeReachable.init accepts arbitrary reachable points on both sides, the init constructor discharges this lemma directly — no induction required.

theorem VerifiedMBSE.Behavior.ProductKripkeReachable.fromRight {α β S₁ D₁ S₂ D₂ : Type} [ToKripke α S₁ D₁] [ToKripke β S₂ D₂] {x : α} {y : β} {s₂ : S₂} {d₂ : D₂} (hr₂ : (ToKripke.toKripke y).reachable s₂ d₂) (hne₁ : (ToKripke.toKripke x).NonEmpty) : ∃ (s₁ : S₁), ∃ (d₁ : D₁), ProductKripkeReachable x y (s₁, s₂) (d₁, d₂)

Lifting: construct product reachability from a right-component reachable point together with a NonEmpty witness on the left.

@[reducible, inline]

abbrev VerifiedMBSE.Behavior.ProductKripke.toKripke {α β S₁ D₁ S₂ D₂ : Type} [ToKripke α S₁ D₁] [ToKripke β S₂ D₂] {x : α} {y : β} : ProductKripke x y → KripkeStructure (S₁ × S₂) (D₁ × D₂)

View ProductKripke x y as a KripkeStructure (S₁ × S₂) (D₁ × D₂).

Defined as abbrev so elaboration is reducible and the following definitional equalities hold:

• (pk.toKripke).inv p d = (toKripke x).inv p.1 d.1 ∧ (toKripke y).inv p.2 d.2
• (pk.toKripke).reachable p d = ProductKripkeReachable x y p d
• (pk.toKripke).step = the interleaving disjunction

reachable_inv / step_preserves_reachable

Supplied by the lemmas from §4 and §5 (ProductKripkeReachable.inv_holds and ProductKripkeReachable.step_preserves_reachable).

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance VerifiedMBSE.Behavior.instToKripkeProductKripke {α β S₁ D₁ S₂ D₂ : Type} [ToKripke α S₁ D₁] [ToKripke β S₂ D₂] {x : α} {y : β} : ToKripke (ProductKripke x y) (S₁ × S₂) (D₁ × D₂)

ToKripke instance for ProductKripke x y.

Makes Always pk P, Eventually pk P, and Leads pk P Q available for products with the same API used for StateMachine and ProductStateMachine. Nested compositions of three or more operands (e.g. ProductKripke (pk : ProductKripke ...) sm₃) work because instance resolution recurses through this declaration.

Equations

• VerifiedMBSE.Behavior.instToKripkeProductKripke = { toKripke := fun (pk : VerifiedMBSE.Behavior.ProductKripke x y) => pk.toKripke }

theorem VerifiedMBSE.Behavior.ProductKripke.nonEmpty {α β S₁ D₁ S₂ D₂ : Type} [ToKripke α S₁ D₁] [ToKripke β S₂ D₂] {x : α} {y : β} (pk : ProductKripke x y) (hne₁ : (ToKripke.toKripke x).NonEmpty) (hne₂ : (ToKripke.toKripke y).NonEmpty) : pk.toKripke.NonEmpty

NonEmpty on both sides implies NonEmpty on the product.

The init constructor assembles a product-reachable state from the two component reachable points, so the proof is immediate and requires no induction.