Mercurial > hg > Papers > 2021 > soto-prosym

comparison Paper/src/agda/_Fresh.agda.replaced @ 5:339fb67b4375

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
INIT rbt.agda
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Sun, 07 Nov 2021 00:51:16 +0900
parents 9176dff8f38a
children
comparison
equal deleted inserted replaced
4:72667e8198e2 5:339fb67b4375
1 ------------------------------------------------------------------------ 1 ------------------------------------------------------------------------
2 -- The Agda standard library 2 -- The Agda standard library
3 -- 3 --
4 -- Fresh lists, a proof relevant variant of Catarina Coquand's contexts in 4 -- Fresh lists, a proof relevant variant of Catarina Coquand!$\prime$!s contexts in
5 -- "A Formalised Proof of the Soundness and Completeness of a Simply Typed 5 -- "A Formalised Proof of the Soundness and Completeness of a Simply Typed
6 -- Lambda-Calculus with Explicit Substitutions" 6 -- Lambda-Calculus with Explicit Substitutions"
7 ------------------------------------------------------------------------ 7 ------------------------------------------------------------------------
8 8
9 -- See README.Data.List.Fresh and README.Data.Trie.NonDependent for 9 -- See README.Data.List.Fresh and README.Data.Trie.NonDependent for
10 -- examples of how to use fresh lists. 10 -- examples of how to use fresh lists.
11 11
12 {-@$\#$@ OPTIONS --without-K --safe @$\#$@-} 12 {-!$\#$! OPTIONS --without-K --safe !$\#$!-}
13 13
14 module Data.List.Fresh where 14 module Data.List.Fresh where
15 15
16 open import Level using (Level; _@$\sqcup$@_) 16 open import Level using (Level; _!$\sqcup$!_)
17 open import Data.Bool.Base using (true; false) 17 open import Data.Bool.Base using (true; false)
18 open import Data.Unit.Polymorphic.Base using (@$\top$@) 18 open import Data.Unit.Polymorphic.Base using (!$\top$!)
19 open import Data.Product using (∃; _@$\times$@_; _,_; -,_; proj@$\_{1}$@; proj@$\_{2}$@) 19 open import Data.Product using (∃; _!$\times$!_; _,_; -,_; proj!$\_{1}$!; proj!$\_{2}$!)
20 open import Data.List.Relation.Unary.All using (All; []; _@$\text{::}$@_) 20 open import Data.List.Relation.Unary.All using (All; []; _!$\text{::}$!_)
21 open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _@$\text{::}$@_) 21 open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _!$\text{::}$!_)
22 open import Data.Maybe.Base as Maybe using (Maybe; just; nothing) 22 open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
23 open import Data.Nat.Base using (@$\mathbb{N}$@; zero; suc) 23 open import Data.Nat.Base using (!$\mathbb{N}$!; zero; suc)
24 open import Function using (_∘′_; flip; id; _on_) 24 open import Function using (_∘′_; flip; id; _on_)
25 open import Relation.Nullary using (does) 25 open import Relation.Nullary using (does)
26 open import Relation.Unary as U using (Pred) 26 open import Relation.Unary as U using (Pred)
27 open import Relation.Binary as B using (Rel) 27 open import Relation.Binary as B using (Rel)
28 open import Relation.Nary 28 open import Relation.Nary
39 -- If we pick an R such that (R a b) means that a is different from b 39 -- If we pick an R such that (R a b) means that a is different from b
40 -- then we have a list of distinct values. 40 -- then we have a list of distinct values.
41 41
42 module _ {a} (A : Set a) (R : Rel A r) where 42 module _ {a} (A : Set a) (R : Rel A r) where
43 43
44 data List@$\#$@ : Set (a @$\sqcup$@ r) 44 data List!$\#$! : Set (a !$\sqcup$! r)
45 fresh : (a : A) (as : List@$\#$@) @$\rightarrow$@ Set r 45 fresh : (a : A) (as : List!$\#$!) !$\rightarrow$! Set r
46 46
47 data List@$\#$@ where 47 data List!$\#$! where
48 [] : List@$\#$@ 48 [] : List!$\#$!
49 cons : (a : A) (as : List@$\#$@) @$\rightarrow$@ fresh a as @$\rightarrow$@ List@$\#$@ 49 cons : (a : A) (as : List!$\#$!) !$\rightarrow$! fresh a as !$\rightarrow$! List!$\#$!
50 50
51 -- Whenever R can be reconstructed by η-expansion (e.g. because it is 51 -- Whenever R can be reconstructed by η-expansion (e.g. because it is
52 -- the erasure ⌊_⌋ of a decidable predicate, cf. Relation.Nary) or we 52 -- the erasure ⌊_⌋ of a decidable predicate, cf. Relation.Nary) or we
53 -- do not care about the proof, it is convenient to get back list syntax. 53 -- do not care about the proof, it is convenient to get back list syntax.
54 54
55 -- We use a different symbol to avoid conflict when importing both Data.List 55 -- We use a different symbol to avoid conflict when importing both Data.List
56 -- and Data.List.Fresh. 56 -- and Data.List.Fresh.
57 infixr 5 _@$\text{::}$@@$\#$@_ 57 infixr 5 _!$\text{::}$!!$\#$!_
58 pattern _@$\text{::}$@@$\#$@_ x xs = cons x xs _ 58 pattern _!$\text{::}$!!$\#$!_ x xs = cons x xs _
59 59
60 fresh a [] = @$\top$@ 60 fresh a [] = !$\top$!
61 fresh a (x @$\text{::}$@@$\#$@ xs) = R a x @$\times$@ fresh a xs 61 fresh a (x !$\text{::}$!!$\#$! xs) = R a x !$\times$! fresh a xs
62 62
63 -- Convenient notation for freshness making A and R implicit parameters 63 -- Convenient notation for freshness making A and R implicit parameters
64 infix 5 _@$\#$@_ 64 infix 5 _!$\#$!_
65 _@$\#$@_ : {R : Rel A r} (a : A) (as : List@$\#$@ A R) @$\rightarrow$@ Set r 65 _!$\#$!_ : {R : Rel A r} (a : A) (as : List!$\#$! A R) !$\rightarrow$! Set r
66 _@$\#$@_ = fresh _ _ 66 _!$\#$!_ = fresh _ _
67 67
68 ------------------------------------------------------------------------ 68 ------------------------------------------------------------------------
69 -- Operations for modifying fresh lists 69 -- Operations for modifying fresh lists
70 70
71 module _ {R : Rel A r} {S : Rel B s} (f : A @$\rightarrow$@ B) (R@$\Rightarrow$@S : @$\forall$@[ R @$\Rightarrow$@ (S on f) ]) where 71 module _ {R : Rel A r} {S : Rel B s} (f : A !$\rightarrow$! B) (R!$\Rightarrow$!S : !$\forall$![ R !$\Rightarrow$! (S on f) ]) where
72 72
73 map : List@$\#$@ A R @$\rightarrow$@ List@$\#$@ B S 73 map : List!$\#$! A R !$\rightarrow$! List!$\#$! B S
74 map-@$\#$@ : @$\forall$@ {a} as @$\rightarrow$@ a @$\#$@ as @$\rightarrow$@ f a @$\#$@ map as 74 map-!$\#$! : !$\forall$! {a} as !$\rightarrow$! a !$\#$! as !$\rightarrow$! f a !$\#$! map as
75 75
76 map [] = [] 76 map [] = []
77 map (cons a as ps) = cons (f a) (map as) (map-@$\#$@ as ps) 77 map (cons a as ps) = cons (f a) (map as) (map-!$\#$! as ps)
78 78
79 map-@$\#$@ [] _ = _ 79 map-!$\#$! [] _ = _
80 map-@$\#$@ (a @$\text{::}$@@$\#$@ as) (p , ps) = R@$\Rightarrow$@S p , map-@$\#$@ as ps 80 map-!$\#$! (a !$\text{::}$!!$\#$! as) (p , ps) = R!$\Rightarrow$!S p , map-!$\#$! as ps
81 81
82 module _ {R : Rel B r} (f : A @$\rightarrow$@ B) where 82 module _ {R : Rel B r} (f : A !$\rightarrow$! B) where
83 83
84 map@$\_{1}$@ : List@$\#$@ A (R on f) @$\rightarrow$@ List@$\#$@ B R 84 map!$\_{1}$! : List!$\#$! A (R on f) !$\rightarrow$! List!$\#$! B R
85 map@$\_{1}$@ = map f id 85 map!$\_{1}$! = map f id
86 86
87 module _ {R : Rel A r} {S : Rel A s} (R@$\Rightarrow$@S : @$\forall$@[ R @$\Rightarrow$@ S ]) where 87 module _ {R : Rel A r} {S : Rel A s} (R!$\Rightarrow$!S : !$\forall$![ R !$\Rightarrow$! S ]) where
88 88
89 map@$\_{2}$@ : List@$\#$@ A R @$\rightarrow$@ List@$\#$@ A S 89 map!$\_{2}$! : List!$\#$! A R !$\rightarrow$! List!$\#$! A S
90 map@$\_{2}$@ = map id R@$\Rightarrow$@S 90 map!$\_{2}$! = map id R!$\Rightarrow$!S
91 91
92 ------------------------------------------------------------------------ 92 ------------------------------------------------------------------------
93 -- Views 93 -- Views
94 94
95 data Empty {A : Set a} {R : Rel A r} : List@$\#$@ A R @$\rightarrow$@ Set (a @$\sqcup$@ r) where 95 data Empty {A : Set a} {R : Rel A r} : List!$\#$! A R !$\rightarrow$! Set (a !$\sqcup$! r) where
96 [] : Empty [] 96 [] : Empty []
97 97
98 data NonEmpty {A : Set a} {R : Rel A r} : List@$\#$@ A R @$\rightarrow$@ Set (a @$\sqcup$@ r) where 98 data NonEmpty {A : Set a} {R : Rel A r} : List!$\#$! A R !$\rightarrow$! Set (a !$\sqcup$! r) where
99 cons : @$\forall$@ x xs pr @$\rightarrow$@ NonEmpty (cons x xs pr) 99 cons : !$\forall$! x xs pr !$\rightarrow$! NonEmpty (cons x xs pr)
100 100
101 ------------------------------------------------------------------------ 101 ------------------------------------------------------------------------
102 -- Operations for reducing fresh lists 102 -- Operations for reducing fresh lists
103 103
104 length : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ @$\mathbb{N}$@ 104 length : {R : Rel A r} !$\rightarrow$! List!$\#$! A R !$\rightarrow$! !$\mathbb{N}$!
105 length [] = 0 105 length [] = 0
106 length (_ @$\text{::}$@@$\#$@ xs) = suc (length xs) 106 length (_ !$\text{::}$!!$\#$! xs) = suc (length xs)
107 107
108 ------------------------------------------------------------------------ 108 ------------------------------------------------------------------------
109 -- Operations for constructing fresh lists 109 -- Operations for constructing fresh lists
110 110
111 pattern [_] a = a @$\text{::}$@@$\#$@ [] 111 pattern [_] a = a !$\text{::}$!!$\#$! []
112 112
113 fromMaybe : {R : Rel A r} @$\rightarrow$@ Maybe A @$\rightarrow$@ List@$\#$@ A R 113 fromMaybe : {R : Rel A r} !$\rightarrow$! Maybe A !$\rightarrow$! List!$\#$! A R
114 fromMaybe nothing = [] 114 fromMaybe nothing = []
115 fromMaybe (just a) = [ a ] 115 fromMaybe (just a) = [ a ]
116 116
117 module _ {R : Rel A r} (R-refl : B.Reflexive R) where 117 module _ {R : Rel A r} (R-refl : B.Reflexive R) where
118 118
119 replicate : @$\mathbb{N}$@ @$\rightarrow$@ A @$\rightarrow$@ List@$\#$@ A R 119 replicate : !$\mathbb{N}$! !$\rightarrow$! A !$\rightarrow$! List!$\#$! A R
120 replicate-@$\#$@ : (n : @$\mathbb{N}$@) (a : A) @$\rightarrow$@ a @$\#$@ replicate n a 120 replicate-!$\#$! : (n : !$\mathbb{N}$!) (a : A) !$\rightarrow$! a !$\#$! replicate n a
121 121
122 replicate zero a = [] 122 replicate zero a = []
123 replicate (suc n) a = cons a (replicate n a) (replicate-@$\#$@ n a) 123 replicate (suc n) a = cons a (replicate n a) (replicate-!$\#$! n a)
124 124
125 replicate-@$\#$@ zero a = _ 125 replicate-!$\#$! zero a = _
126 replicate-@$\#$@ (suc n) a = R-refl , replicate-@$\#$@ n a 126 replicate-!$\#$! (suc n) a = R-refl , replicate-!$\#$! n a
127 127
128 ------------------------------------------------------------------------ 128 ------------------------------------------------------------------------
129 -- Operations for deconstructing fresh lists 129 -- Operations for deconstructing fresh lists
130 130
131 uncons : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ Maybe (A @$\times$@ List@$\#$@ A R) 131 uncons : {R : Rel A r} !$\rightarrow$! List!$\#$! A R !$\rightarrow$! Maybe (A !$\times$! List!$\#$! A R)
132 uncons [] = nothing 132 uncons [] = nothing
133 uncons (a @$\text{::}$@@$\#$@ as) = just (a , as) 133 uncons (a !$\text{::}$!!$\#$! as) = just (a , as)
134 134
135 head : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ Maybe A 135 head : {R : Rel A r} !$\rightarrow$! List!$\#$! A R !$\rightarrow$! Maybe A
136 head = Maybe.map proj@$\_{1}$@ ∘′ uncons 136 head = Maybe.map proj!$\_{1}$! ∘′ uncons
137 137
138 tail : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ Maybe (List@$\#$@ A R) 138 tail : {R : Rel A r} !$\rightarrow$! List!$\#$! A R !$\rightarrow$! Maybe (List!$\#$! A R)
139 tail = Maybe.map proj@$\_{2}$@ ∘′ uncons 139 tail = Maybe.map proj!$\_{2}$! ∘′ uncons
140 140
141 take : {R : Rel A r} @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ List@$\#$@ A R 141 take : {R : Rel A r} !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! List!$\#$! A R !$\rightarrow$! List!$\#$! A R
142 take-@$\#$@ : {R : Rel A r} @$\rightarrow$@ @$\forall$@ n a (as : List@$\#$@ A R) @$\rightarrow$@ a @$\#$@ as @$\rightarrow$@ a @$\#$@ take n as 142 take-!$\#$! : {R : Rel A r} !$\rightarrow$! !$\forall$! n a (as : List!$\#$! A R) !$\rightarrow$! a !$\#$! as !$\rightarrow$! a !$\#$! take n as
143 143
144 take zero xs = [] 144 take zero xs = []
145 take (suc n) [] = [] 145 take (suc n) [] = []
146 take (suc n) (cons a as ps) = cons a (take n as) (take-@$\#$@ n a as ps) 146 take (suc n) (cons a as ps) = cons a (take n as) (take-!$\#$! n a as ps)
147 147
148 take-@$\#$@ zero a xs _ = _ 148 take-!$\#$! zero a xs _ = _
149 take-@$\#$@ (suc n) a [] ps = _ 149 take-!$\#$! (suc n) a [] ps = _
150 take-@$\#$@ (suc n) a (x @$\text{::}$@@$\#$@ xs) (p , ps) = p , take-@$\#$@ n a xs ps 150 take-!$\#$! (suc n) a (x !$\text{::}$!!$\#$! xs) (p , ps) = p , take-!$\#$! n a xs ps
151 151
152 drop : {R : Rel A r} @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ List@$\#$@ A R 152 drop : {R : Rel A r} !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! List!$\#$! A R !$\rightarrow$! List!$\#$! A R
153 drop zero as = as 153 drop zero as = as
154 drop (suc n) [] = [] 154 drop (suc n) [] = []
155 drop (suc n) (a @$\text{::}$@@$\#$@ as) = drop n as 155 drop (suc n) (a !$\text{::}$!!$\#$! as) = drop n as
156 156
157 module _ {P : Pred A p} (P? : U.Decidable P) where 157 module _ {P : Pred A p} (P? : U.Decidable P) where
158 158
159 takeWhile : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ List@$\#$@ A R 159 takeWhile : {R : Rel A r} !$\rightarrow$! List!$\#$! A R !$\rightarrow$! List!$\#$! A R
160 takeWhile-@$\#$@ : @$\forall$@ {R : Rel A r} a (as : List@$\#$@ A R) @$\rightarrow$@ a @$\#$@ as @$\rightarrow$@ a @$\#$@ takeWhile as 160 takeWhile-!$\#$! : !$\forall$! {R : Rel A r} a (as : List!$\#$! A R) !$\rightarrow$! a !$\#$! as !$\rightarrow$! a !$\#$! takeWhile as
161 161
162 takeWhile [] = [] 162 takeWhile [] = []
163 takeWhile (cons a as ps) with does (P? a) 163 takeWhile (cons a as ps) with does (P? a)
164 ... | true = cons a (takeWhile as) (takeWhile-@$\#$@ a as ps) 164 ... | true = cons a (takeWhile as) (takeWhile-!$\#$! a as ps)
165 ... | false = [] 165 ... | false = []
166 166
167 takeWhile-@$\#$@ a [] _ = _ 167 takeWhile-!$\#$! a [] _ = _
168 takeWhile-@$\#$@ a (x @$\text{::}$@@$\#$@ xs) (p , ps) with does (P? x) 168 takeWhile-!$\#$! a (x !$\text{::}$!!$\#$! xs) (p , ps) with does (P? x)
169 ... | true = p , takeWhile-@$\#$@ a xs ps 169 ... | true = p , takeWhile-!$\#$! a xs ps
170 ... | false = _ 170 ... | false = _
171 171
172 dropWhile : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ List@$\#$@ A R 172 dropWhile : {R : Rel A r} !$\rightarrow$! List!$\#$! A R !$\rightarrow$! List!$\#$! A R
173 dropWhile [] = [] 173 dropWhile [] = []
174 dropWhile aas@(a @$\text{::}$@@$\#$@ as) with does (P? a) 174 dropWhile aas@(a !$\text{::}$!!$\#$! as) with does (P? a)
175 ... | true = dropWhile as 175 ... | true = dropWhile as
176 ... | false = aas 176 ... | false = aas
177 177
178 filter : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ List@$\#$@ A R 178 filter : {R : Rel A r} !$\rightarrow$! List!$\#$! A R !$\rightarrow$! List!$\#$! A R
179 filter-@$\#$@ : @$\forall$@ {R : Rel A r} a (as : List@$\#$@ A R) @$\rightarrow$@ a @$\#$@ as @$\rightarrow$@ a @$\#$@ filter as 179 filter-!$\#$! : !$\forall$! {R : Rel A r} a (as : List!$\#$! A R) !$\rightarrow$! a !$\#$! as !$\rightarrow$! a !$\#$! filter as
180 180
181 filter [] = [] 181 filter [] = []
182 filter (cons a as ps) with does (P? a) 182 filter (cons a as ps) with does (P? a)
183 ... | true = cons a (filter as) (filter-@$\#$@ a as ps) 183 ... | true = cons a (filter as) (filter-!$\#$! a as ps)
184 ... | false = filter as 184 ... | false = filter as
185 185
186 filter-@$\#$@ a [] _ = _ 186 filter-!$\#$! a [] _ = _
187 filter-@$\#$@ a (x @$\text{::}$@@$\#$@ xs) (p , ps) with does (P? x) 187 filter-!$\#$! a (x !$\text{::}$!!$\#$! xs) (p , ps) with does (P? x)
188 ... | true = p , filter-@$\#$@ a xs ps 188 ... | true = p , filter-!$\#$! a xs ps
189 ... | false = filter-@$\#$@ a xs ps 189 ... | false = filter-!$\#$! a xs ps
190 190
191 ------------------------------------------------------------------------ 191 ------------------------------------------------------------------------
192 -- Relationship to List and AllPairs 192 -- Relationship to List and AllPairs
193 193
194 toList : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ ∃ (AllPairs R) 194 toList : {R : Rel A r} !$\rightarrow$! List!$\#$! A R !$\rightarrow$! ∃ (AllPairs R)
195 toAll : @$\forall$@ {R : Rel A r} {a} as @$\rightarrow$@ fresh A R a as @$\rightarrow$@ All (R a) (proj@$\_{1}$@ (toList as)) 195 toAll : !$\forall$! {R : Rel A r} {a} as !$\rightarrow$! fresh A R a as !$\rightarrow$! All (R a) (proj!$\_{1}$! (toList as))
196 196
197 toList [] = -, [] 197 toList [] = -, []
198 toList (cons x xs ps) = -, toAll xs ps @$\text{::}$@ proj@$\_{2}$@ (toList xs) 198 toList (cons x xs ps) = -, toAll xs ps !$\text{::}$! proj!$\_{2}$! (toList xs)
199 199
200 toAll [] ps = [] 200 toAll [] ps = []
201 toAll (a @$\text{::}$@@$\#$@ as) (p , ps) = p @$\text{::}$@ toAll as ps 201 toAll (a !$\text{::}$!!$\#$! as) (p , ps) = p !$\text{::}$! toAll as ps
202 202
203 fromList : @$\forall$@ {R : Rel A r} {xs} @$\rightarrow$@ AllPairs R xs @$\rightarrow$@ List@$\#$@ A R 203 fromList : !$\forall$! {R : Rel A r} {xs} !$\rightarrow$! AllPairs R xs !$\rightarrow$! List!$\#$! A R
204 fromList-@$\#$@ : @$\forall$@ {R : Rel A r} {x xs} (ps : AllPairs R xs) @$\rightarrow$@ 204 fromList-!$\#$! : !$\forall$! {R : Rel A r} {x xs} (ps : AllPairs R xs) !$\rightarrow$!
205 All (R x) xs @$\rightarrow$@ x @$\#$@ fromList ps 205 All (R x) xs !$\rightarrow$! x !$\#$! fromList ps
206 206
207 fromList [] = [] 207 fromList [] = []
208 fromList (r @$\text{::}$@ rs) = cons _ (fromList rs) (fromList-@$\#$@ rs r) 208 fromList (r !$\text{::}$! rs) = cons _ (fromList rs) (fromList-!$\#$! rs r)
209 209
210 fromList-@$\#$@ [] _ = _ 210 fromList-!$\#$! [] _ = _
211 fromList-@$\#$@ (p @$\text{::}$@ ps) (r @$\text{::}$@ rs) = r , fromList-@$\#$@ ps rs 211 fromList-!$\#$! (p !$\text{::}$! ps) (r !$\text{::}$! rs) = r , fromList-!$\#$! ps rs