feat: product of FLTS (#218)

This PR introduces the product of two FLTS and refactors DA.prod to use
that definition and its theorems (currently only one).

Author: fmontesi

Cslib.lean

@@ -33,11 +33,12 @@ import Cslib.Foundations.Data.OmegaSequence.Init
 import Cslib.Foundations.Data.OmegaSequence.Temporal
 import Cslib.Foundations.Data.Relation
 import Cslib.Foundations.Lint.Basic
+import Cslib.Foundations.Semantics.FLTS.Basic
+import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
+import Cslib.Foundations.Semantics.FLTS.LTSToFLTS
+import Cslib.Foundations.Semantics.FLTS.Prod
 import Cslib.Foundations.Semantics.LTS.Basic
 import Cslib.Foundations.Semantics.LTS.Bisimulation
-import Cslib.Foundations.Semantics.LTS.FLTS
-import Cslib.Foundations.Semantics.LTS.FLTSToLTS
-import Cslib.Foundations.Semantics.LTS.LTSToFLTS
 import Cslib.Foundations.Semantics.LTS.Simulation
 import Cslib.Foundations.Semantics.LTS.TraceEq
 import Cslib.Foundations.Semantics.ReductionSystem.Basic

Cslib/Computability/Automata/DA/Basic.lean

@@ -7,7 +7,7 @@ Authors: Fabrizio Montesi, Ching-Tsun Chou
 import Cslib.Computability.Automata.Acceptors.Acceptor
 import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
 import Cslib.Foundations.Data.OmegaSequence.InfOcc
-import Cslib.Foundations.Semantics.LTS.FLTS
+import Cslib.Foundations.Semantics.FLTS.Basic
 
 /-! # Deterministic Automata
 

Cslib/Computability/Automata/DA/Prod.lean

@@ -5,6 +5,7 @@ Authors: Ching-Tsun Chou
 -/
 
 import Cslib.Computability.Automata.DA.Basic
+import Cslib.Foundations.Semantics.FLTS.Prod
 
 /-! # Product of deterministic automata. -/
 
@@ -17,20 +18,19 @@ variable {State1 State2 Symbol : Type*}
 
 namespace DA
 
-/-- The product of two deterministic automata.
-TODO: This operation could be generalised to FLTS and lifted here. -/
+/-- The product of two deterministic automata. -/
 @[scoped grind =]
 def prod (da1 : DA State1 Symbol) (da2 : DA State2 Symbol) : DA (State1 × State2) Symbol where
+  toFLTS := da1.toFLTS.prod da2.toFLTS
   start := (da1.start, da2.start)
-  tr := fun (s1, s2) x ↦ (da1.tr s1 x, da2.tr s2 x)
 
 /-- A state is reachable by the product automaton iff its components are reachable by
-the respective component automata. -/
+the respective automaton components. -/
 @[simp, scoped grind =]
 theorem prod_mtr_eq (da1 : DA State1 Symbol) (da2 : DA State2 Symbol)
     (s : State1 × State2) (xs : List Symbol) :
-    (da1.prod da2).mtr s xs = (da1.mtr s.fst xs, da2.mtr s.snd xs) := by
-  induction xs generalizing s <;> grind
+    (da1.prod da2).mtr s xs = (da1.mtr s.fst xs, da2.mtr s.snd xs) :=
+  FLTS.prod_mtr_eq da1.toFLTS da2.toFLTS s xs
 
 end DA
 

Cslib/Computability/Automata/DA/ToNA.lean

@@ -6,7 +6,7 @@ Authors: Fabrizio Montesi
 
 import Cslib.Computability.Automata.DA.Basic
 import Cslib.Computability.Automata.NA.Basic
-import Cslib.Foundations.Semantics.LTS.FLTSToLTS
+import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
 
 /-! # Translation of Deterministic Automata into Nonodeterministic Automata.
 

Cslib/Computability/Automata/NA/ToDA.lean

@@ -6,7 +6,7 @@ Authors: Fabrizio Montesi
 
 import Cslib.Computability.Automata.DA.Basic
 import Cslib.Computability.Automata.NA.Basic
-import Cslib.Foundations.Semantics.LTS.LTSToFLTS
+import Cslib.Foundations.Semantics.FLTS.LTSToFLTS
 
 /-! # Translation of Nondeterministic Automata for finite strings into Deterministic Automata
 

Cslib/Foundations/Semantics/LTS/FLTS.lean …ib/Foundations/Semantics/FLTS/Basic.leanCslib/Foundations/Semantics/LTS/FLTS.lean renamed to Cslib/Foundations/Semantics/FLTS/Basic.lean Cslib/Foundations/Semantics/LTS/FLTS.lean renamed to Cslib/Foundations/Semantics/FLTS/Basic.lean

@@ -5,7 +5,7 @@ Authors: Fabrizio Montesi
 -/
 
 import Cslib.Foundations.Semantics.LTS.Basic
-import Cslib.Foundations.Semantics.LTS.FLTS
+import Cslib.Foundations.Semantics.FLTS.Basic
 
 variable {State Label : Type*}
 

…Foundations/Semantics/LTS/FLTSToLTS.lean …oundations/Semantics/FLTS/FLTSToLTS.leanCslib/Foundations/Semantics/LTS/FLTSToLTS.lean renamed to Cslib/Foundations/Semantics/FLTS/FLTSToLTS.lean Cslib/Foundations/Semantics/LTS/FLTSToLTS.lean renamed to Cslib/Foundations/Semantics/FLTS/FLTSToLTS.lean

@@ -5,7 +5,7 @@ Authors: Fabrizio Montesi
 -/
 
 import Cslib.Foundations.Semantics.LTS.Basic
-import Cslib.Foundations.Semantics.LTS.FLTS
+import Cslib.Foundations.Semantics.FLTS.Basic
 
 variable {State Label : Type*}
 

…Foundations/Semantics/LTS/LTSToFLTS.lean …oundations/Semantics/FLTS/LTSToFLTS.leanCslib/Foundations/Semantics/LTS/LTSToFLTS.lean renamed to Cslib/Foundations/Semantics/FLTS/LTSToFLTS.lean Cslib/Foundations/Semantics/LTS/LTSToFLTS.lean renamed to Cslib/Foundations/Semantics/FLTS/LTSToFLTS.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ching-Tsun Chou, Fabrizio Montesi
+-/
+
+import Cslib.Foundations.Semantics.FLTS.Basic
+
+/-! # Product of functional labelled transition systems -/
+
+namespace Cslib.FLTS
+
+variable {State Label : Type*}
+
+/-- The product of two FLTS with the same label type. -/
+@[scoped grind =]
+def prod (flts1 : FLTS State1 Label) (flts2 : FLTS State2 Label) :
+    FLTS (State1 × State2) Label where
+  tr := fun (s1, s2) μ ↦ (flts1.tr s1 μ, flts2.tr s2 μ)
+
+/-- A state is reachable by the product FLTS iff its components are reachable by
+the respective FLTS components. -/
+@[simp, scoped grind =]
+theorem prod_mtr_eq (flts1 : FLTS State1 Label) (flts2 : FLTS State2 Label)
+    (s : State1 × State2) (μs : List Label) :
+    (flts1.prod flts2).mtr s μs = (flts1.mtr s.fst μs, flts2.mtr s.snd μs) := by
+  induction μs generalizing s <;> grind
+
+end Cslib.FLTS