forked from agda/agda-stdlib
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathProperties.agda
168 lines (134 loc) · 7.19 KB
/
Properties.agda
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
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the heterogeneous infix relation
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.List.Relation.Binary.Infix.Heterogeneous.Properties where
open import Level
open import Data.Bool.Base using (true; false)
open import Data.Empty using (⊥-elim)
open import Data.List.Base as List using (List; []; _∷_; length; map; filter; replicate)
open import Data.Nat.Base using (zero; suc; _≤_)
import Data.Nat.Properties as ℕₚ
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
open import Function.Base using (case_of_; _$′_)
open import Relation.Nullary.Decidable using (yes; no; does; map′; _⊎-dec_)
open import Relation.Nullary.Negation using (¬_; contradiction)
open import Relation.Unary as U using (Pred)
open import Relation.Binary.Core using (REL; _⇒_)
open import Relation.Binary.Definitions using (Decidable; Trans; Antisym)
open import Relation.Binary.PropositionalEquality.Core using (_≢_; refl; cong)
open import Data.List.Relation.Binary.Pointwise.Base as Pointwise using (Pointwise)
open import Data.List.Relation.Binary.Infix.Heterogeneous
open import Data.List.Relation.Binary.Prefix.Heterogeneous
as Prefix using (Prefix; []; _∷_)
import Data.List.Relation.Binary.Prefix.Heterogeneous.Properties as Prefixₚ
open import Data.List.Relation.Binary.Suffix.Heterogeneous
as Suffix using (Suffix; here; there)
private
variable
a b r s : Level
A : Set a
B : Set b
R : REL A B r
S : REL A B s
------------------------------------------------------------------------
-- Conversion functions
fromPointwise : ∀ {as bs} → Pointwise R as bs → Infix R as bs
fromPointwise pw = here (Prefixₚ.fromPointwise pw)
fromSuffix : ∀ {as bs} → Suffix R as bs → Infix R as bs
fromSuffix (here pw) = fromPointwise pw
fromSuffix (there p) = there (fromSuffix p)
module _ {c t} {C : Set c} {T : REL A C t} where
fromPrefixSuffix : Trans R S T → Trans (Prefix R) (Suffix S) (Infix T)
fromPrefixSuffix tr p (here q) = here (Prefixₚ.trans tr p (Prefixₚ.fromPointwise q))
fromPrefixSuffix tr p (there q) = there (fromPrefixSuffix tr p q)
fromSuffixPrefix : Trans R S T → Trans (Suffix R) (Prefix S) (Infix T)
fromSuffixPrefix tr (here p) q = here (Prefixₚ.trans tr (Prefixₚ.fromPointwise p) q)
fromSuffixPrefix tr (there p) (_ ∷ q) = there (fromSuffixPrefix tr p q)
∷⁻ : ∀ {as b bs} → Infix R as (b ∷ bs) → Prefix R as (b ∷ bs) ⊎ Infix R as bs
∷⁻ (here pref) = inj₁ pref
∷⁻ (there inf) = inj₂ inf
------------------------------------------------------------------------
-- length
length-mono : ∀ {as bs} → Infix R as bs → length as ≤ length bs
length-mono (here pref) = Prefixₚ.length-mono pref
length-mono (there p) = ℕₚ.m≤n⇒m≤1+n (length-mono p)
------------------------------------------------------------------------
-- As an order
module _ {c t} {C : Set c} {T : REL A C t} where
Prefix-Infix-trans : Trans R S T → Trans (Prefix R) (Infix S) (Infix T)
Prefix-Infix-trans tr p (here q) = here (Prefixₚ.trans tr p q)
Prefix-Infix-trans tr p (there q) = there (Prefix-Infix-trans tr p q)
Infix-Prefix-trans : Trans R S T → Trans (Infix R) (Prefix S) (Infix T)
Infix-Prefix-trans tr (here p) q = here (Prefixₚ.trans tr p q)
Infix-Prefix-trans tr (there p) (_ ∷ q) = there (Infix-Prefix-trans tr p q)
Suffix-Infix-trans : Trans R S T → Trans (Suffix R) (Infix S) (Infix T)
Suffix-Infix-trans tr p (here q) = fromSuffixPrefix tr p q
Suffix-Infix-trans tr p (there q) = there (Suffix-Infix-trans tr p q)
Infix-Suffix-trans : Trans R S T → Trans (Infix R) (Suffix S) (Infix T)
Infix-Suffix-trans tr p (here q) = Infix-Prefix-trans tr p (Prefixₚ.fromPointwise q)
Infix-Suffix-trans tr p (there q) = there (Infix-Suffix-trans tr p q)
trans : Trans R S T → Trans (Infix R) (Infix S) (Infix T)
trans tr p (here q) = Infix-Prefix-trans tr p q
trans tr p (there q) = there (trans tr p q)
antisym : Antisym R S T → Antisym (Infix R) (Infix S) (Pointwise T)
antisym asym (here p) (here q) = Prefixₚ.antisym asym p q
antisym asym {i = a ∷ as} {j = bs} p@(here _) (there q)
= ⊥-elim $′ ℕₚ.<-irrefl refl $′ begin-strict
length as <⟨ length-mono p ⟩
length bs ≤⟨ length-mono q ⟩
length as ∎ where open ℕₚ.≤-Reasoning
antisym asym {i = as} {j = b ∷ bs} (there p) q@(here _)
= ⊥-elim $′ ℕₚ.<-irrefl refl $′ begin-strict
length bs <⟨ length-mono q ⟩
length as ≤⟨ length-mono p ⟩
length bs ∎ where open ℕₚ.≤-Reasoning
antisym asym {i = a ∷ as} {j = b ∷ bs} (there p) (there q)
= ⊥-elim $′ ℕₚ.<-irrefl refl $′ begin-strict
length as <⟨ length-mono p ⟩
length bs <⟨ length-mono q ⟩
length as ∎ where open ℕₚ.≤-Reasoning
------------------------------------------------------------------------
-- map
module _ {c d r} {C : Set c} {D : Set d} {R : REL C D r} where
map⁺ : ∀ {as bs} (f : A → C) (g : B → D) →
Infix (λ a b → R (f a) (g b)) as bs →
Infix R (List.map f as) (List.map g bs)
map⁺ f g (here p) = here (Prefixₚ.map⁺ f g p)
map⁺ f g (there p) = there (map⁺ f g p)
map⁻ : ∀ {as bs} (f : A → C) (g : B → D) →
Infix R (List.map f as) (List.map g bs) →
Infix (λ a b → R (f a) (g b)) as bs
map⁻ {bs = []} f g (here p) = here (Prefixₚ.map⁻ f g p)
map⁻ {bs = b ∷ bs} f g (here p) = here (Prefixₚ.map⁻ f g p)
map⁻ {bs = b ∷ bs} f g (there p) = there (map⁻ f g p)
------------------------------------------------------------------------
-- filter
module _ {p q} {P : Pred A p} {Q : Pred B q} (P? : U.Decidable P) (Q? : U.Decidable Q)
(P⇒Q : ∀ {a b} → P a → Q b) (Q⇒P : ∀ {a b} → Q b → P a)
where
filter⁺ : ∀ {as bs} → Infix R as bs → Infix R (filter P? as) (filter Q? bs)
filter⁺ (here p) = here (Prefixₚ.filter⁺ P? Q? (λ _ → P⇒Q) (λ _ → Q⇒P) p)
filter⁺ {bs = b ∷ bs} (there p) with does (Q? b)
... | true = there (filter⁺ p)
... | false = filter⁺ p
------------------------------------------------------------------------
-- replicate
replicate⁺ : ∀ {m n a b} → m ≤ n → R a b →
Infix R (replicate m a) (replicate n b)
replicate⁺ m≤n r = here (Prefixₚ.replicate⁺ m≤n r)
replicate⁻ : ∀ {m n a b} → m ≢ 0 →
Infix R (replicate m a) (replicate n b) → R a b
replicate⁻ {m = m} {n = zero} m≢0 (here p) = Prefixₚ.replicate⁻ m≢0 p
replicate⁻ {m = m} {n = suc n} m≢0 (here p) = Prefixₚ.replicate⁻ m≢0 p
replicate⁻ {m = m} {n = suc n} m≢0 (there p) = replicate⁻ m≢0 p
------------------------------------------------------------------------
-- decidability
infix? : Decidable R → Decidable (Infix R)
infix? R? [] [] = yes (here [])
infix? R? (a ∷ as) [] = no (λ where (here ()))
infix? R? as bbs@(_ ∷ bs) =
map′ [ here , there ]′ ∷⁻
(Prefixₚ.prefix? R? as bbs ⊎-dec infix? R? as bs)