diff options
Diffstat (limited to 'Data')
| -rw-r--r-- | Data/Circuit/Merge.agda | 112 | ||||
| -rw-r--r-- | Data/Circuit/Value.agda | 29 | ||||
| -rw-r--r-- | Data/System.agda | 179 | ||||
| -rw-r--r-- | Data/System/Values.agda | 96 | ||||
| -rw-r--r-- | Data/Vector.agda | 50 |
5 files changed, 376 insertions, 90 deletions
diff --git a/Data/Circuit/Merge.agda b/Data/Circuit/Merge.agda index 82c0d92..9cf180a 100644 --- a/Data/Circuit/Merge.agda +++ b/Data/Circuit/Merge.agda @@ -3,11 +3,12 @@ module Data.Circuit.Merge where open import Data.Nat.Base using (ℕ) -open import Data.Fin.Base using (Fin; pinch; punchIn; punchOut) +open import Data.Fin.Base using (Fin; pinch; punchIn; punchOut; splitAt) open import Data.Fin.Properties using (punchInᵢ≢i; punchIn-punchOut) open import Data.Bool.Properties using (if-eta) open import Data.Bool using (Bool; if_then_else_) open import Data.Circuit.Value using (Value; join; join-comm; join-assoc) +open import Data.Sum.Properties using ([,]-cong; [,-]-cong; [-,]-cong; [,]-∘; [,]-map) open import Data.Subset.Functional using ( Subset @@ -18,6 +19,7 @@ open import Data.Subset.Functional ; foldl-fusion ) open import Data.Vector as V using (Vector; head; tail; removeAt) +open import Data.Vec.Functional using (_++_) open import Data.Fin.Permutation using ( Permutation @@ -31,14 +33,16 @@ open import Data.Fin.Permutation ) open import Data.Product using (Σ-syntax; _,_) open import Data.Fin.Preimage using (preimage; preimage-cong₁; preimage-cong₂) -open import Function.Base using (∣_⟩-_; _∘_) -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_) +open import Function.Base using (∣_⟩-_; _∘_; case_of_; _$_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≢_; _≗_; module ≡-Reasoning) open Value using (U) open ℕ open Fin open Bool +open ≡-Reasoning + _when_ : Value → Bool → Value x when b = if b then x else U @@ -90,8 +94,6 @@ merge-with-U {suc A} e S = begin merge-with e (tail (λ _ → U)) (tail S) ≡⟨⟩ merge-with e (λ _ → U) (tail S) ≡⟨ merge-with-U e (tail S) ⟩ e ∎ - where - open ≡.≡-Reasoning merge : {A : ℕ} → Vector Value A → Subset A → Value merge v = merge-with U v @@ -146,8 +148,6 @@ merge-removeAt {A} zero v S = begin merge-with U v S ≡⟨ merge-suc v S ⟩ merge-with (head v when head S) (tail v) (tail S) ≡⟨ join-merge (head v when head S) (tail v) (tail S) ⟨ join (head v when head S) (merge-with U (tail v) (tail S)) ∎ - where - open ≡.≡-Reasoning merge-removeAt {suc A} (suc k) v S = begin merge-with U v S ≡⟨ merge-suc v S ⟩ merge-with v0? (tail v) (tail S) ≡⟨ join-merge _ (tail v) (tail S) ⟨ @@ -166,7 +166,6 @@ merge-removeAt {suc A} (suc k) v S = begin v- = removeAt v (suc k) S- : Subset (suc A) S- = removeAt S (suc k) - open ≡.≡-Reasoning import Function.Structures as FunctionStructures open module FStruct {A B : Set} = FunctionStructures {_} {_} {_} {_} {A} _≡_ {B} _≡_ using (IsInverse) @@ -211,7 +210,6 @@ merge-preimage-ρ {suc A} {suc B} ρ v S = begin S- = tail S vρˡ0? : Value vρˡ0? = head (v ∘ ρˡ) when head S - open ≡.≡-Reasoning ≡vρˡ0? : head (v ∘ ρˡ) when S (ρʳ (head ρˡ)) ≡ head (v ∘ ρˡ) when head S ≡vρˡ0? = ≡.cong ((head (v ∘ ρˡ) when_) ∘ S) (inverseʳ ρ) v∘ρˡ- : v- ∘ ρˡ- ≗ tail (v ∘ ρˡ) @@ -252,8 +250,6 @@ mutual U ≡⟨ merge-with-U U S ⟨ merge (λ _ → U) S ≡⟨ merge-cong₁ (λ x → ≡.sym (merge-[] v (⁅ x ⁆ ∘ f))) S ⟩ merge (push v f) S ∎ - where - open ≡.≡-Reasoning merge-preimage {suc A} {zero} f v S with () ← f zero merge-preimage {suc A} {suc B} f v S with insert-f0-0 f ... | ρ , ρf0≡0 = begin @@ -266,7 +262,6 @@ mutual merge (merge v ∘ preimage (ρˡ ∘ ρʳ ∘ f) ∘ ⁅_⁆) S ≡⟨ merge-cong₁ (merge-cong₂ v ∘ preimage-cong₁ (λ y → inverseˡ ρ {f y}) ∘ ⁅_⁆) S ⟩ merge (merge v ∘ preimage f ∘ ⁅_⁆) S ∎ where - open ≡.≡-Reasoning ρʳ ρˡ : Fin (ℕ.suc B) → Fin (ℕ.suc B) ρʳ = ρ ⟨$⟩ʳ_ ρˡ = ρ ⟨$⟩ˡ_ @@ -319,7 +314,6 @@ mutual v0? = v0 when f⁻¹[S]0 v0?+[f[v-]0?] = (if S0 then join v0? f[v-]0 else v0?) f[v]0? = f[v]0 when S0 - open ≡.≡-Reasoning ≡f[v]0 : v0?+[f[v-]0?] ≡ f[v]0? ≡f[v]0 rewrite f0≡0 with S0 ... | true = begin @@ -339,3 +333,95 @@ mutual where v0?′ : Value v0?′ = v0 when head (preimage f ⁅ suc x ⁆) + +merge-++ + : {n m : ℕ} + (xs : Vector Value n) + (ys : Vector Value m) + (S₁ : Subset n) + (S₂ : Subset m) + → merge (xs ++ ys) (S₁ ++ S₂) + ≡ join (merge xs S₁) (merge ys S₂) +merge-++ {zero} {m} xs ys S₁ S₂ = begin + merge (xs ++ ys) (S₁ ++ S₂) ≡⟨ merge-cong₂ (xs ++ ys) (λ _ → ≡.refl) ⟩ + merge (xs ++ ys) S₂ ≡⟨ merge-cong₁ (λ _ → ≡.refl) S₂ ⟩ + merge ys S₂ ≡⟨ ≡.cong (λ h → join h (merge ys S₂)) (merge-[] xs S₁) ⟨ + join (merge xs S₁) (merge ys S₂) ∎ +merge-++ {suc n} {m} xs ys S₁ S₂ = begin + merge (xs ++ ys) (S₁ ++ S₂) ≡⟨ merge-suc (xs ++ ys) (S₁ ++ S₂) ⟩ + merge-with (head xs when head S₁) (tail (xs ++ ys)) (tail (S₁ ++ S₂)) ≡⟨ join-merge (head xs when head S₁) (tail (xs ++ ys)) (tail (S₁ ++ S₂)) ⟨ + join (head xs when head S₁) (merge (tail (xs ++ ys)) (tail (S₁ ++ S₂))) + ≡⟨ ≡.cong (join (head xs when head S₁)) (merge-cong₁ ([,]-map ∘ splitAt n) (tail (S₁ ++ S₂))) ⟩ + join (head xs when head S₁) (merge (tail xs ++ ys) (tail (S₁ ++ S₂))) + ≡⟨ ≡.cong (join (head xs when head S₁)) (merge-cong₂ (tail xs ++ ys) ([,]-map ∘ splitAt n)) ⟩ + join (head xs when head S₁) (merge (tail xs ++ ys) (tail S₁ ++ S₂)) ≡⟨ ≡.cong (join (head xs when head S₁)) (merge-++ (tail xs) ys (tail S₁) S₂) ⟩ + join (head xs when head S₁) (join (merge (tail xs) (tail S₁)) (merge ys S₂)) ≡⟨ join-assoc (head xs when head S₁) (merge (tail xs) (tail S₁)) _ ⟨ + join (join (head xs when head S₁) (merge (tail xs) (tail S₁))) (merge ys S₂) + ≡⟨ ≡.cong (λ h → join h (merge ys S₂)) (join-merge (head xs when head S₁) (tail xs) (tail S₁)) ⟩ + join (merge-with (head xs when head S₁) (tail xs) (tail S₁)) (merge ys S₂) ≡⟨ ≡.cong (λ h → join h (merge ys S₂)) (merge-suc xs S₁) ⟨ + join (merge xs S₁) (merge ys S₂) ∎ + +open import Function using (Equivalence) +open Equivalence +open import Data.Nat using (_+_) +open import Data.Fin using (_↑ˡ_; _↑ʳ_; _≟_) +open import Data.Fin.Properties using (↑ˡ-injective; ↑ʳ-injective; splitAt⁻¹-↑ˡ; splitAt-↑ˡ; splitAt⁻¹-↑ʳ; splitAt-↑ʳ) +open import Relation.Nullary.Decidable using (does; does-⇔; dec-false) + +open Fin +⁅⁆-≟ : {n : ℕ} (x y : Fin n) → ⁅ x ⁆ y ≡ does (x ≟ y) +⁅⁆-≟ zero zero = ≡.refl +⁅⁆-≟ zero (suc y) = ≡.refl +⁅⁆-≟ (suc x) zero = ≡.refl +⁅⁆-≟ (suc x) (suc y) = ⁅⁆-≟ x y + +open import Data.Sum using ([_,_]′; inj₁; inj₂) +⁅⁆-++ + : {n′ m′ : ℕ} + (i : Fin (n′ + m′)) + → [ (λ x → ⁅ x ⁆ ++ ⊥) , (λ x → ⊥ ++ ⁅ x ⁆) ]′ (splitAt n′ i) ≗ ⁅ i ⁆ +⁅⁆-++ {n′} {m′} i x with splitAt n′ i in eq₁ +... | inj₁ i′ with splitAt n′ x in eq₂ +... | inj₁ x′ = begin + ⁅ i′ ⁆ x′ ≡⟨ ⁅⁆-≟ i′ x′ ⟩ + does (i′ ≟ x′) ≡⟨ does-⇔ ⇔ (i′ ≟ x′) (i′ ↑ˡ m′ ≟ x′ ↑ˡ m′) ⟩ + does (i′ ↑ˡ m′ ≟ x′ ↑ˡ m′) ≡⟨ ⁅⁆-≟ (i′ ↑ˡ m′) (x′ ↑ˡ m′) ⟨ + ⁅ i′ ↑ˡ m′ ⁆ (x′ ↑ˡ m′) ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ˡ eq₁) (splitAt⁻¹-↑ˡ eq₂) ⟩ + ⁅ i ⁆ x ∎ + where + ⇔ : Equivalence (≡.setoid (i′ ≡ x′)) (≡.setoid (i′ ↑ˡ m′ ≡ x′ ↑ˡ m′)) + ⇔ .to = ≡.cong (_↑ˡ m′) + ⇔ .from = ↑ˡ-injective m′ i′ x′ + ⇔ .to-cong ≡.refl = ≡.refl + ⇔ .from-cong ≡.refl = ≡.refl +... | inj₂ x′ = begin + false ≡⟨ dec-false (i′ ↑ˡ m′ ≟ n′ ↑ʳ x′) ↑ˡ≢↑ʳ ⟨ + does (i′ ↑ˡ m′ ≟ n′ ↑ʳ x′) ≡⟨ ⁅⁆-≟ (i′ ↑ˡ m′) (n′ ↑ʳ x′) ⟨ + ⁅ i′ ↑ˡ m′ ⁆ (n′ ↑ʳ x′) ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ˡ eq₁) (splitAt⁻¹-↑ʳ eq₂) ⟩ + ⁅ i ⁆ x ∎ + where + ↑ˡ≢↑ʳ : i′ ↑ˡ m′ ≢ n′ ↑ʳ x′ + ↑ˡ≢↑ʳ ≡ = case ≡.trans (≡.sym (splitAt-↑ˡ n′ i′ m′)) (≡.trans (≡.cong (splitAt n′) ≡) (splitAt-↑ʳ n′ m′ x′)) of λ { () } +⁅⁆-++ {n′} i x | inj₂ i′ with splitAt n′ x in eq₂ +⁅⁆-++ {n′} {m′} i x | inj₂ i′ | inj₁ x′ = begin + [ ⊥ , ⁅ i′ ⁆ ]′ (splitAt n′ x) ≡⟨ ≡.cong ([ ⊥ , ⁅ i′ ⁆ ]′) eq₂ ⟩ + false ≡⟨ dec-false (n′ ↑ʳ i′ ≟ x′ ↑ˡ m′) ↑ʳ≢↑ˡ ⟨ + does (n′ ↑ʳ i′ ≟ x′ ↑ˡ m′) ≡⟨ ⁅⁆-≟ (n′ ↑ʳ i′) (x′ ↑ˡ m′) ⟨ + ⁅ n′ ↑ʳ i′ ⁆ (x′ ↑ˡ m′) ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ʳ eq₁) (splitAt⁻¹-↑ˡ eq₂) ⟩ + ⁅ i ⁆ x ∎ + where + ↑ʳ≢↑ˡ : n′ ↑ʳ i′ ≢ x′ ↑ˡ m′ + ↑ʳ≢↑ˡ ≡ = case ≡.trans (≡.sym (splitAt-↑ʳ n′ m′ i′)) (≡.trans (≡.cong (splitAt n′) ≡) (splitAt-↑ˡ n′ x′ m′)) of λ { () } +⁅⁆-++ {n′} i x | inj₂ i′ | inj₂ x′ = begin + [ ⊥ , ⁅ i′ ⁆ ]′ (splitAt n′ x) ≡⟨ ≡.cong [ ⊥ , ⁅ i′ ⁆ ]′ eq₂ ⟩ + ⁅ i′ ⁆ x′ ≡⟨ ⁅⁆-≟ i′ x′ ⟩ + does (i′ ≟ x′) ≡⟨ does-⇔ ⇔ (i′ ≟ x′) (n′ ↑ʳ i′ ≟ n′ ↑ʳ x′) ⟩ + does (n′ ↑ʳ i′ ≟ n′ ↑ʳ x′) ≡⟨ ⁅⁆-≟ (n′ ↑ʳ i′) (n′ ↑ʳ x′) ⟨ + ⁅ n′ ↑ʳ i′ ⁆ (n′ ↑ʳ x′) ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ʳ eq₁) (splitAt⁻¹-↑ʳ eq₂) ⟩ + ⁅ i ⁆ x ∎ + where + ⇔ : Equivalence (≡.setoid (i′ ≡ x′)) (≡.setoid (n′ ↑ʳ i′ ≡ n′ ↑ʳ x′)) + ⇔ .to = ≡.cong (n′ ↑ʳ_) + ⇔ .from = ↑ʳ-injective n′ i′ x′ + ⇔ .to-cong ≡.refl = ≡.refl + ⇔ .from-cong ≡.refl = ≡.refl diff --git a/Data/Circuit/Value.agda b/Data/Circuit/Value.agda index 512a622..b135c35 100644 --- a/Data/Circuit/Value.agda +++ b/Data/Circuit/Value.agda @@ -2,12 +2,22 @@ module Data.Circuit.Value where -open import Relation.Binary.Lattice.Bundles using (BoundedJoinSemilattice) +import Relation.Binary.Lattice.Properties.BoundedJoinSemilattice as LatticeProp + +open import Algebra.Bundles using (CommutativeMonoid) +open import Algebra.Structures using (IsCommutativeMonoid; IsMonoid; IsSemigroup; IsMagma) open import Data.Product.Base using (_×_; _,_) open import Data.String.Base using (String) open import Level using (0ℓ) +open import Relation.Binary.Lattice.Bundles using (BoundedJoinSemilattice) open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) +open CommutativeMonoid +open IsCommutativeMonoid +open IsMagma +open IsMonoid +open IsSemigroup + data Value : Set where U T F X : Value @@ -129,8 +139,8 @@ join-assoc X X T = ≡.refl join-assoc X X F = ≡.refl join-assoc X X X = ≡.refl -ValueLattice : BoundedJoinSemilattice 0ℓ 0ℓ 0ℓ -ValueLattice = record +Lattice : BoundedJoinSemilattice 0ℓ 0ℓ 0ℓ +Lattice = record { Carrier = Value ; _≈_ = _≡_ ; _≤_ = ≤-Value @@ -155,3 +165,16 @@ ValueLattice = record X → U≤X } } + +module Lattice = BoundedJoinSemilattice Lattice + +Monoid : CommutativeMonoid 0ℓ 0ℓ +Monoid .Carrier = Lattice.Carrier +Monoid ._≈_ = Lattice._≈_ +Monoid ._∙_ = Lattice._∨_ +Monoid .ε = Lattice.⊥ +Monoid .isCommutativeMonoid .isMonoid .isSemigroup .isMagma .isEquivalence = ≡.isEquivalence +Monoid .isCommutativeMonoid .isMonoid .isSemigroup .isMagma .∙-cong = ≡.cong₂ join +Monoid .isCommutativeMonoid .isMonoid .isSemigroup .assoc = join-assoc +Monoid .isCommutativeMonoid .isMonoid .identity = LatticeProp.identity Lattice +Monoid .isCommutativeMonoid .comm = join-comm diff --git a/Data/System.agda b/Data/System.agda index cecdfcd..5d5e484 100644 --- a/Data/System.agda +++ b/Data/System.agda @@ -1,85 +1,144 @@ {-# OPTIONS --without-K --safe #-} open import Level using (Level; 0ℓ; suc) + module Data.System {ℓ : Level} where -import Function.Construct.Identity as Id import Relation.Binary.Properties.Preorder as PreorderProperties +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning -open import Data.Circuit.Value using (Value) -open import Data.Nat.Base using (ℕ) +open import Categories.Category using (Category) +open import Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to ⊤ₛ) +open import Data.Circuit.Value using (Monoid) +open import Data.Nat using (ℕ) open import Data.Setoid using (_⇒ₛ_; ∣_∣) -open import Data.System.Values Value using (Values; _≋_; module ≋) +open import Data.System.Values Monoid using (Values; _≋_; module ≋; <ε>) +open import Function using (Func; _⟨$⟩_; flip) +open import Function.Construct.Constant using () renaming (function to Const) +open import Function.Construct.Identity using () renaming (function to Id) +open import Function.Construct.Setoid using (_∙_) open import Level using (Level; 0ℓ; suc) +open import Relation.Binary as Rel using (Reflexive; Transitive; Preorder; Setoid; Rel) open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) -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 Func -record System (n : ℕ) : Set₁ where - - field - S : Setoid 0ℓ 0ℓ - 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 -module _ {n : ℕ} where + record System : Set₁ 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) + S : Setoid 0ℓ 0ℓ + fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣ + fₒ : ∣ S ⇒ₛ Values n ∣ - open ≤-System + fₛ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ S ∣ + fₛ′ i = to (to fₛ i) - ≤-refl : Reflexive ≤-System - ⇒S ≤-refl = Id.function _ - ≗-fₛ (≤-refl {x}) _ _ = System.refl x - ≗-fₒ (≤-refl {x}) _ = ≋.refl + fₒ′ : ∣ S ∣ → ∣ Values n ∣ + fₒ′ = to fₒ - ≡⇒≤ : _≡_ ⇒ ≤-System - ≡⇒≤ ≡.refl = ≤-refl + module S = Setoid S 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 0ℓ) (suc 0ℓ) ℓ - System-Preorder = record - { Carrier = System n - ; _≈_ = _≡_ - ; _≲_ = ≤-System - ; isPreorder = record - { isEquivalence = ≡.isEquivalence - ; reflexive = ≡⇒≤ - ; trans = ≤-trans - } - } + discrete : System + discrete .S = ⊤ₛ + discrete .fₛ = Const (Values n) (⊤ₛ ⇒ₛ ⊤ₛ) (Id ⊤ₛ) + discrete .fₒ = Const ⊤ₛ (Values n) <ε> -module _ (n : ℕ) where +module _ {n : ℕ} where - open PreorderProperties (System-Preorder {n}) using (InducedEquivalence) + record _≤_ (a b : System n) : Set ℓ where - Systemₛ : Setoid (suc 0ℓ) ℓ - Systemₛ = InducedEquivalence + private + module A = System a + module B = System b + + open B using (S) + + field + ⇒S : ∣ A.S ⇒ₛ B.S ∣ + ≗-fₛ : (i : ∣ Values n ∣) (s : ∣ A.S ∣) → ⇒S ⟨$⟩ (A.fₛ′ i s) S.≈ B.fₛ′ i (⇒S ⟨$⟩ s) + ≗-fₒ : (s : ∣ A.S ∣) → A.fₒ′ s ≋ B.fₒ′ (⇒S ⟨$⟩ s) + + infix 4 _≤_ + +open System + +private + + module _ {n : ℕ} where + + open _≤_ + + ≤-refl : Reflexive (_≤_ {n}) + ⇒S ≤-refl = Id _ + ≗-fₛ (≤-refl {x}) _ _ = S.refl x + ≗-fₒ ≤-refl _ = ≋.refl + + ≡⇒≤ : _≡_ Rel.⇒ _≤_ + ≡⇒≤ ≡.refl = ≤-refl + + ≤-trans : Transitive _≤_ + ⇒S (≤-trans a b) = ⇒S b ∙ ⇒S a + ≗-fₛ (≤-trans {x} {y} {z} a b) i s = let open ≈-Reasoning (S z) in begin + ⇒S b ⟨$⟩ (⇒S a ⟨$⟩ (fₛ′ x i s)) ≈⟨ cong (⇒S b) (≗-fₛ a i s) ⟩ + ⇒S b ⟨$⟩ (fₛ′ y i (⇒S a ⟨$⟩ s)) ≈⟨ ≗-fₛ b i (⇒S a ⟨$⟩ s) ⟩ + fₛ′ z i (⇒S b ⟨$⟩ (⇒S a ⟨$⟩ s)) ∎ + ≗-fₒ (≤-trans {x} {y} {z} a b) s = let open ≈-Reasoning (Values n) in begin + fₒ′ x s ≈⟨ ≗-fₒ a s ⟩ + fₒ′ y (⇒S a ⟨$⟩ s) ≈⟨ ≗-fₒ b (⇒S a ⟨$⟩ s) ⟩ + fₒ′ z (⇒S b ⟨$⟩ (⇒S a ⟨$⟩ s)) ∎ + + variable + A B C : System n + + _≈_ : Rel (A ≤ B) 0ℓ + _≈_ {A} {B} ≤₁ ≤₂ = ⇒S ≤₁ A⇒B.≈ ⇒S ≤₂ + where + module A⇒B = Setoid (S A ⇒ₛ S B) + + open Rel.IsEquivalence + + ≈-isEquiv : Rel.IsEquivalence (_≈_ {A} {B}) + ≈-isEquiv {B = B} .refl = S.refl B + ≈-isEquiv {B = B} .sym a = S.sym B a + ≈-isEquiv {B = B} .trans a b = S.trans B a b + + ≤-resp-≈ : {f h : B ≤ C} {g i : A ≤ B} → f ≈ h → g ≈ i → ≤-trans g f ≈ ≤-trans i h + ≤-resp-≈ {_} {C} {_} {f} {h} {g} {i} f≈h g≈i {x} = begin + ⇒S f ⟨$⟩ (⇒S g ⟨$⟩ x) ≈⟨ f≈h ⟩ + ⇒S h ⟨$⟩ (⇒S g ⟨$⟩ x) ≈⟨ cong (⇒S h) g≈i ⟩ + ⇒S h ⟨$⟩ (⇒S i ⟨$⟩ x) ∎ + where + open ≈-Reasoning (System.S C) + +System-≤ : ℕ → Preorder (suc 0ℓ) (suc 0ℓ) ℓ +System-≤ n = record + { _≲_ = _≤_ {n} + ; isPreorder = record + { isEquivalence = ≡.isEquivalence + ; reflexive = ≡⇒≤ + ; trans = ≤-trans + } + } + +Systemₛ : ℕ → Setoid (suc 0ℓ) ℓ +Systemₛ n = PreorderProperties.InducedEquivalence (System-≤ n) + +Systems : ℕ → Category (suc 0ℓ) ℓ 0ℓ +Systems n = record + { Obj = System n + ; _⇒_ = _≤_ + ; _≈_ = _≈_ + ; id = ≤-refl + ; _∘_ = flip ≤-trans + ; assoc = λ {D = D} → S.refl D + ; sym-assoc = λ {D = D} → S.refl D + ; identityˡ = λ {B = B} → S.refl B + ; identityʳ = λ {B = B} → S.refl B + ; identity² = λ {A = A} → S.refl A + ; equiv = ≈-isEquiv + ; ∘-resp-≈ = λ {f = f} {h} {g} {i} → ≤-resp-≈ {f = f} {h} {g} {i} + } diff --git a/Data/System/Values.agda b/Data/System/Values.agda index bf8fa38..737e34e 100644 --- a/Data/System/Values.agda +++ b/Data/System/Values.agda @@ -1,21 +1,95 @@ {-# OPTIONS --without-K --safe #-} -module Data.System.Values (A : Set) where +open import Algebra.Bundles using (CommutativeMonoid) +open import Level using (0ℓ) + +module Data.System.Values (A : CommutativeMonoid 0ℓ 0ℓ) where + +import Algebra.Properties.CommutativeMonoid.Sum as Sum +import Data.Vec.Functional.Properties as VecProps +import Relation.Binary.PropositionalEquality as ≡ -open import Data.Nat.Base using (ℕ) -open import Data.Vec.Functional using (Vector) +open import Data.Fin using (_↑ˡ_; _↑ʳ_; zero; suc) +open import Data.Nat using (ℕ; _+_; suc) +open import Data.Product using (_,_) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Setoid using (∣_∣) +open import Data.Vec.Functional as Vec using (Vector; zipWith; replicate) +open import Data.Vec.Functional.Relation.Binary.Equality.Setoid using (≋-setoid) +open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_) open import Level using (0ℓ) open import Relation.Binary using (Rel; Setoid) -open import Data.Vec.Functional.Relation.Binary.Equality.Setoid using (≋-setoid) -import Relation.Binary.PropositionalEquality as ≡ +open CommutativeMonoid A renaming (Carrier to Value) +open Func +open Sum A using (sum) + +opaque + + Values : ℕ → Setoid 0ℓ 0ℓ + Values = ≋-setoid (≡.setoid Value) + +module _ {n : ℕ} where + + opaque + + unfolding Values + + merge : ∣ Values n ∣ → Value + merge = sum + + _⊕_ : ∣ Values n ∣ → ∣ Values n ∣ → ∣ Values n ∣ + xs ⊕ ys = zipWith _∙_ xs ys + + <ε> : ∣ Values n ∣ + <ε> = replicate n ε + + head : ∣ Values (suc n) ∣ → Value + head xs = xs zero + + tail : ∣ Values (suc n) ∣ → ∣ Values n ∣ + tail xs = xs ∘ suc + + module ≋ = Setoid (Values n) + + _≋_ : Rel ∣ Values n ∣ 0ℓ + _≋_ = ≋._≈_ + + infix 4 _≋_ + +opaque + + unfolding Values + + [] : ∣ Values 0 ∣ + [] = Vec.[] + + []-unique : (xs ys : ∣ Values 0 ∣) → xs ≋ ys + []-unique xs ys () + +module _ {n m : ℕ} where + + opaque + + unfolding Values + + _++_ : ∣ Values n ∣ → ∣ Values m ∣ → ∣ Values (n + m) ∣ + _++_ = Vec._++_ -Values : ℕ → Setoid 0ℓ 0ℓ -Values = ≋-setoid (≡.setoid A) + infixr 5 _++_ -_≋_ : {n : ℕ} → Rel (Vector A n) 0ℓ -_≋_ {n} = Setoid._≈_ (Values n) + ++-cong + : (xs xs′ : ∣ Values n ∣) + {ys ys′ : ∣ Values m ∣} + → xs ≋ xs′ + → ys ≋ ys′ + → xs ++ ys ≋ xs′ ++ ys′ + ++-cong xs xs′ = VecProps.++-cong xs xs′ -infix 4 _≋_ + splitₛ : Values (n + m) ⟶ₛ Values n ×ₛ Values m + to splitₛ v = v ∘ (_↑ˡ m) , v ∘ (n ↑ʳ_) + cong splitₛ v₁≋v₂ = v₁≋v₂ ∘ (_↑ˡ m) , v₁≋v₂ ∘ (n ↑ʳ_) -module ≋ {n : ℕ} = Setoid (Values n) + ++ₛ : Values n ×ₛ Values m ⟶ₛ Values (n + m) + to ++ₛ (xs , ys) = xs ++ ys + cong ++ₛ (≗xs , ≗ys) = ++-cong _ _ ≗xs ≗ys diff --git a/Data/Vector.agda b/Data/Vector.agda index 052f624..874f0b2 100644 --- a/Data/Vector.agda +++ b/Data/Vector.agda @@ -3,10 +3,10 @@ module Data.Vector where open import Data.Nat.Base using (ℕ) -open import Data.Vec.Functional using (Vector; head; tail; []; removeAt; map) public -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_) +open import Data.Vec.Functional using (Vector; head; tail; []; removeAt; map; _++_) public +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_; module ≡-Reasoning) open import Function.Base using (∣_⟩-_; _∘_) -open import Data.Fin.Base using (Fin; toℕ) +open import Data.Fin.Base using (Fin; toℕ; _↑ˡ_; _↑ʳ_) open ℕ open Fin @@ -80,3 +80,47 @@ foldl-[] {e : B 0} → foldl B f e [] ≡ e foldl-[] _ _ = ≡.refl + +open import Data.Sum using ([_,_]′) +open import Data.Sum.Properties using ([,-]-cong; [-,]-cong; [,]-∘) +open import Data.Fin.Properties using (splitAt-↑ˡ; splitAt-↑ʳ) +open import Data.Fin using (splitAt) +open import Data.Nat using (_+_) +++-↑ˡ + : {n m : ℕ} + {A : Set} + (X : Vector A n) + (Y : Vector A m) + → (X ++ Y) ∘ (_↑ˡ m) ≗ X +++-↑ˡ {n} {m} X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ˡ n i m) + +++-↑ʳ + : {n m : ℕ} + {A : Set} + (X : Vector A n) + (Y : Vector A m) + → (X ++ Y) ∘ (n ↑ʳ_) ≗ Y +++-↑ʳ {n} {m} X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ʳ n m i) + ++-assocʳ : {m n o : ℕ} → Fin (m + (n + o)) → Fin (m + n + o) ++-assocʳ {m} {n} {o} = [ (λ x → x ↑ˡ n ↑ˡ o) , [ (λ x → (m ↑ʳ x) ↑ˡ o) , m + n ↑ʳ_ ]′ ∘ splitAt n ]′ ∘ splitAt m + +open ≡-Reasoning +++-assoc + : {m n o : ℕ} + {A : Set} + (X : Vector A m) + (Y : Vector A n) + (Z : Vector A o) + → ((X ++ Y) ++ Z) ∘ +-assocʳ {m} ≗ X ++ (Y ++ Z) +++-assoc {m} {n} {o} X Y Z i = begin + ((X ++ Y) ++ Z) (+-assocʳ {m} i) ≡⟨⟩ + ((X ++ Y) ++ Z) ([ (λ x → x ↑ˡ n ↑ˡ o) , _ ]′ (splitAt m i)) ≡⟨ [,]-∘ ((X ++ Y) ++ Z) (splitAt m i) ⟩ + [ ((X ++ Y) ++ Z) ∘ (λ x → x ↑ˡ n ↑ˡ o) , _ ]′ (splitAt m i) ≡⟨ [-,]-cong (++-↑ˡ (X ++ Y) Z ∘ (_↑ˡ n)) (splitAt m i) ⟩ + [ (X ++ Y) ∘ (_↑ˡ n) , _ ]′ (splitAt m i) ≡⟨ [-,]-cong (++-↑ˡ X Y) (splitAt m i) ⟩ + [ X , ((X ++ Y) ++ Z) ∘ [ _ , _ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([,]-∘ ((X ++ Y) ++ Z) ∘ splitAt n) (splitAt m i) ⟩ + [ X , [ (_ ++ Z) ∘ (_↑ˡ o) ∘ (m ↑ʳ_) , _ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([-,]-cong (++-↑ˡ (X ++ Y) Z ∘ (m ↑ʳ_)) ∘ splitAt n) (splitAt m i) ⟩ + [ X , [ (X ++ Y) ∘ (m ↑ʳ_) , _ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([-,]-cong (++-↑ʳ X Y) ∘ splitAt n) (splitAt m i) ⟩ + [ X , [ Y , ((X ++ Y) ++ Z) ∘ (m + n ↑ʳ_) ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([,-]-cong (++-↑ʳ (X ++ Y) Z) ∘ splitAt n) (splitAt m i) ⟩ + [ X , [ Y , Z ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨⟩ + (X ++ (Y ++ Z)) i ∎ |