diff options
| -rw-r--r-- | Data/System.agda | 72 |
1 files changed, 49 insertions, 23 deletions
diff --git a/Data/System.agda b/Data/System.agda index c5bc347..fa7d8e7 100644 --- a/Data/System.agda +++ b/Data/System.agda @@ -7,27 +7,49 @@ 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 Level using (Level; _⊔_; 0ℓ; suc) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) open import Relation.Binary using (Rel; Reflexive; Transitive; Preorder; _⇒_; Setoid) open import Function.Base using (id; _∘_) +import Function.Construct.Identity as Id +open import Data.Vec.Functional.Relation.Binary.Equality.Setoid using (≋-setoid) -Input : ℕ → Set -Input = Vector Value +open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_) -Output : ℕ → Set -Output = Vector Value +open import Function.Construct.Setoid using (setoid; _∙_) +open Func + +_⇒ₛ_ : {a₁ a₂ b₁ b₂ : Level} → Setoid a₁ a₂ → Setoid b₁ b₂ → Setoid (a₁ ⊔ a₂ ⊔ b₁ ⊔ b₂) (a₁ ⊔ b₂) +_⇒ₛ_ = setoid + +infixr 0 _⇒ₛ_ + +∣_∣ : {c ℓ : Level} → Setoid c ℓ → Set c +∣_∣ = Setoid.Carrier + +Values : ℕ → Setoid 0ℓ 0ℓ +Values = ≋-setoid (≡.setoid Value) + +_≋_ : {n : ℕ} → Rel (Vector Value n) 0ℓ +_≋_ {n} = Setoid._≈_ (Values n) + +module ≋ {n : ℕ} = Setoid (Values n) 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 + S : Setoid ℓ ℓ + fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣ + fₒ : ∣ Values n ⇒ₛ S ⇒ₛ Values n ∣ + + fₛ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ S ∣ + fₛ′ = to ∘ to fₛ + + fₒ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ Values n ∣ + fₒ′ = to ∘ to fₒ + + open Setoid S public module _ {n : ℕ} where @@ -35,25 +57,29 @@ module _ {ℓ : Level} 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 + ⇒S : ∣ A.S ⇒ₛ B.S ∣ + ≗-fₛ + : (i : ∣ Values n ∣) (s : ∣ A.S ∣) + → ⇒S ⟨$⟩ (A.fₛ′ i s) B.≈ B.fₛ′ i (⇒S ⟨$⟩ s) + ≗-fₒ + : (i : ∣ Values n ∣) (s : ∣ A.S ∣) + → A.fₒ′ i s ≋ B.fₒ′ i (⇒S ⟨$⟩ s) open ≤-System ≤-refl : Reflexive ≤-System - ⇒S ≤-refl = id - ≗-fₛ ≤-refl _ _ = ≡.refl - ≗-fₒ ≤-refl _ _ _ = ≡.refl + ⇒S ≤-refl = Id.function _ + ≗-fₛ (≤-refl {x}) p e = System.refl x + ≗-fₒ (≤-refl {x}) _ _ = ≋.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) + ⇒S (≤-trans a b) = ⇒S b ∙ ⇒S a + ≗-fₛ (≤-trans {x} {y} {z} a b) i s = System.trans z (cong (⇒S b) (≗-fₛ a i s)) (≗-fₛ b i (⇒S a ⟨$⟩ s)) + ≗-fₒ (≤-trans {x} {y} {z} a b) i s = ≋.trans (≗-fₒ a i s) (≗-fₒ b i (⇒S a ⟨$⟩ s)) System-Preorder : Preorder (suc ℓ) (suc ℓ) ℓ System-Preorder = record @@ -70,5 +96,5 @@ module _ {ℓ : Level} where module _ (n : ℕ) where open PreorderProperties (System-Preorder {n}) using (InducedEquivalence) - System-Setoid : Setoid (suc ℓ) ℓ - System-Setoid = InducedEquivalence + Systemₛ : Setoid (suc ℓ) ℓ + Systemₛ = InducedEquivalence |