Add preliminary setoid of discrete dynamical systemsmain

1 files changed, 74 insertions, 0 deletions

diff --git a/Data/System.agda b/Data/System.agda
new file mode 100644
index 0000000..c5bc347
--- /dev/null
+++ b/Data/System.agda
@@ -0,0 +1,74 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.System where
+
+import Relation.Binary.Properties.Preorder as PreorderProperties
+
+open import Data.Circuit.Value using (Value)
+open import Data.Nat.Base using (ℕ)
+open import Data.Vec.Functional using (Vector)
+open import Data.Fin.Base using (Fin)
+open import Level using (Level; suc; 0ℓ)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
+open import Relation.Binary using (Rel; Reflexive; Transitive; Preorder; _⇒_; Setoid)
+open import Function.Base using (id; _∘_)
+
+Input : ℕ → Set
+Input = Vector Value
+
+Output : ℕ → Set
+Output = Vector Value
+
+module _ {ℓ : Level} where
+
+  record System (n : ℕ) : Set (suc ℓ) where
+    field
+      S : Set ℓ
+      fₛ : Input n → S → S
+      fₒ : Input n → S → Output n
+      fₛ-cong : {i j : Input n} → i ≗ j → fₛ i ≗ fₛ j
+      fₒ-cong : {i j : Input n} → i ≗ j → (s : S) → fₒ i s ≗ fₒ j s
+
+  module _ {n : ℕ} where
+
+    record ≤-System (a b : System n) : Set ℓ where
+      module A = System a
+      module B = System b
+      field
+        ⇒S : A.S → B.S
+        ≗-fₛ : (i : Input n) (s : A.S) → ⇒S (A.fₛ i s) ≡ B.fₛ i (⇒S s)
+        ≗-fₒ : (i : Input n) (s : A.S) (k : Fin n) → A.fₒ i s k ≡ B.fₒ i (⇒S s) k
+
+    open ≤-System
+
+    ≤-refl : Reflexive ≤-System
+    ⇒S ≤-refl = id
+    ≗-fₛ ≤-refl _ _ = ≡.refl
+    ≗-fₒ ≤-refl _ _ _ = ≡.refl
+
+    ≡⇒≤ : _≡_ ⇒ ≤-System
+    ≡⇒≤ ≡.refl = ≤-refl
+
+    open System
+    ≤-trans : Transitive ≤-System
+    ⇒S (≤-trans a b) = ⇒S b ∘ ⇒S a
+    ≗-fₛ (≤-trans a b) i s = ≡.trans (≡.cong (⇒S b) (≗-fₛ a i s)) (≗-fₛ b i (⇒S a s))
+    ≗-fₒ (≤-trans a b) i s k = ≡.trans (≗-fₒ a i s k) (≗-fₒ b i (⇒S a s) k)
+
+    System-Preorder : Preorder (suc ℓ) (suc ℓ) ℓ
+    System-Preorder = record
+        { Carrier = System n
+        ; _≈_ = _≡_
+        ; _≲_ = ≤-System
+        ; isPreorder = record
+            { isEquivalence = ≡.isEquivalence
+            ; reflexive = ≡⇒≤
+            ; trans = ≤-trans
+            }
+        }
+
+  module _ (n : ℕ) where
+
+    open PreorderProperties (System-Preorder {n}) using (InducedEquivalence)
+    System-Setoid : Setoid (suc ℓ) ℓ
+    System-Setoid = InducedEquivalence