diff options
Diffstat (limited to 'Data/System.agda')
| -rw-r--r-- | Data/System.agda | 148 |
1 files changed, 67 insertions, 81 deletions
diff --git a/Data/System.agda b/Data/System.agda index e2ac073..0361369 100644 --- a/Data/System.agda +++ b/Data/System.agda @@ -1,100 +1,86 @@ {-# OPTIONS --without-K --safe #-} -module Data.System where +open import Level using (Level) +module Data.System {ℓ : Level} where + +import Function.Construct.Identity as Id 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.Setoid using (_⇒ₛ_; ∣_∣) +open import Data.System.Values Value using (Values; _≋_; module ≋) 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) +open import Relation.Binary using (Reflexive; Transitive; Preorder; _⇒_; Setoid) +open import Function.Base using (_∘_) +open import Function.Bundles using (Func; _⟨$⟩_) +open import Function.Construct.Setoid using (_∙_) -open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_) - -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 _⇒ₛ_ +record System (n : ℕ) : Set (suc ℓ) where -∣_∣ : {c ℓ : Level} → Setoid c ℓ → Set c -∣_∣ = Setoid.Carrier + field + S : Setoid ℓ ℓ + fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣ + fₒ : ∣ S ⇒ₛ Values n ∣ -Values : ℕ → Setoid 0ℓ 0ℓ -Values = ≋-setoid (≡.setoid Value) + fₛ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ S ∣ + fₛ′ = to ∘ to fₛ -_≋_ : {n : ℕ} → Rel (Vector Value n) 0ℓ -_≋_ {n} = Setoid._≈_ (Values n) + fₒ′ : ∣ S ∣ → ∣ Values n ∣ + fₒ′ = to fₒ -module ≋ {n : ℕ} = Setoid (Values n) + open Setoid S public -module _ {ℓ : Level} where +module _ {n : ℕ} where - record System (n : ℕ) : Set (suc ℓ) where + record ≤-System (a b : System n) : Set ℓ where + module A = System a + module B = System b field - S : Setoid ℓ ℓ - fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣ - fₒ : ∣ S ⇒ₛ Values n ∣ - - fₛ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ S ∣ - fₛ′ = to ∘ to fₛ - - fₒ′ : ∣ S ∣ → ∣ Values n ∣ - fₒ′ = to fₒ - - open Setoid S public - - 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 : ∣ Values n ∣) (s : ∣ A.S ∣) - → ⇒S ⟨$⟩ (A.fₛ′ i s) B.≈ B.fₛ′ i (⇒S ⟨$⟩ s) - ≗-fₒ - : (s : ∣ A.S ∣) - → A.fₒ′ s ≋ B.fₒ′ (⇒S ⟨$⟩ s) - - open ≤-System - - ≤-refl : Reflexive ≤-System - ⇒S ≤-refl = Id.function _ - ≗-fₛ (≤-refl {x}) _ _ = 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 {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 a b) s = ≋.trans (≗-fₒ a s) (≗-fₒ b (⇒S a ⟨$⟩ s)) - - 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 (suc ℓ) ℓ - Systemₛ = InducedEquivalence + ⇒S : ∣ A.S ⇒ₛ B.S ∣ + ≗-fₛ + : (i : ∣ Values n ∣) (s : ∣ A.S ∣) + → ⇒S ⟨$⟩ (A.fₛ′ i s) B.≈ B.fₛ′ i (⇒S ⟨$⟩ s) + ≗-fₒ + : (s : ∣ A.S ∣) + → A.fₒ′ s ≋ B.fₒ′ (⇒S ⟨$⟩ s) + + open ≤-System + + ≤-refl : Reflexive ≤-System + ⇒S ≤-refl = Id.function _ + ≗-fₛ (≤-refl {x}) _ _ = 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 {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 a b) s = ≋.trans (≗-fₒ a s) (≗-fₒ b (⇒S a ⟨$⟩ s)) + + 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 (suc ℓ) ℓ + Systemₛ = InducedEquivalence |