blob: c5bc347dc9581feee8f893166e97ea0625ccb4f1 (
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
|
{-# 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
|
