StateMachine → KripkeStructure via ToKripke #
StateMachine S D inv に対する ToKripke instance を提供する。
これにより Always sm P 等の呼び出しが型クラス resolution 経由で透過的に解決される。
Coe からの移行理由 #
Coe (StateMachine S D inv) (KripkeStructure S D) instance は、inv が α 側のみに
現れるため Lean 4.30 の strict semi-out-params チェックに引っかかる (β = KripkeStructure S D
から inv が flow できない)。
ToKripke 型クラスは State / Data のみ outParam とし、α = StateMachine S D inv
全体に対する instance matching を行うため、inv も含めて自然に解決される。
B-8 での拡張 #
KripkeStructure が inv / step / reachable_inv / step_preserves_reachable を
持つようになったため、StateMachine.toKripke もこれらを埋める必要がある:
inv= StateMachine の型引数inv : S → D → Propをそのまま代入 (defeq 成立)reachable_inv= 既存のReachable.inv_holdsの薄いラッパーstep= transition を存在量化した 1 ステップ関係step_preserves_reachable=Reachable.stepコンストラクタを呼ぶだけ
abbrev のまま維持することで (sm.toKripke).inv = inv /
(sm.toKripke).reachable s d = Reachable sm s d の defeq が保たれる。
StateMachine を KripkeStructure として見る。
abbrev なので reducible で、以下の defeq 関係が成立する:
(sm.toKripke).inv=inv(型引数そのもの)(sm.toKripke).reachable s d=Reachable sm s d(sm.toKripke).step s d s' d'= 遷移の存在量化
step の定義 #
step s d s' d' は「ある遷移 t ∈ sm.transitions が存在して、
t.source = s かつ t.guard d が成立し、t.target = s' かつ
t.effect d = d' となる」ことを表す。
step_preserves_reachable の証明 #
step の存在量化を展開すると、対応する t と各等式が手に入るので、
Reachable.step コンストラクタをそのまま適用できる。
Equations
- One or more equations did not get rendered due to their size.
Instances For
StateMachine に対する ToKripke instance。
これにより Always sm P で sm : StateMachine S D inv が渡されると、
ToKripke (StateMachine S D inv) S D が resolve され、
State = S, Data = D が outParam で決定される。
Equations
- VerifiedMBSE.Behavior.instToKripkeStateMachine = { toKripke := fun (sm : VerifiedMBSE.Behavior.StateMachine S D inv) => sm.toKripke }
sm.WellFormed から sm.toKripke.NonEmpty を導く。
ドット記法用のエイリアス: hwf.nonEmpty.