blob: e2ac073621c0c6cddd02c3a9b4acea43b371831f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
|
{-# 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 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 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 _⇒ₛ_
∣_∣ : {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 : 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
|
