1
------------------------------------------------------------------------
2
-- Lexicographic ordering of lists
3
------------------------------------------------------------------------
5
-- The definition of lexicographic ordering used here is suitable if
6
-- the argument order is a strict partial order. The lexicographic
7
-- ordering itself can be either strict or non-strict, depending on
8
-- the value of a parameter.
10
module Relation.Binary.List.StrictLex where
12
open import Data.Empty
13
open import Data.Unit using (⊤; tt)
14
open import Data.Function
15
open import Data.Product
19
open import Relation.Nullary
20
open import Relation.Binary
21
open import Relation.Binary.Consequences
22
open import Relation.Binary.List.Pointwise as Pointwise
23
using ([]; _∷_; head; tail)
26
module Dummy {A : Set} where
28
data Lex (P : Set) (≈ < : Rel A zero) : Rel (List A) zero where
29
base : P → Lex P ≈ < [] []
30
halt : ∀ {y ys} → Lex P ≈ < [] (y ∷ ys)
31
this : ∀ {x xs y ys} (x<y : < x y) → Lex P ≈ < (x ∷ xs) (y ∷ ys)
32
next : ∀ {x xs y ys} (x≈y : ≈ x y)
33
(xs⊴ys : Lex P ≈ < xs ys) → Lex P ≈ < (x ∷ xs) (y ∷ ys)
35
-- Strict lexicographic ordering.
37
Lex-< : (≈ < : Rel A zero) → Rel (List A) zero
40
¬[]<[] : ∀ {≈ <} → ¬ Lex-< ≈ < [] []
43
-- Non-strict lexicographic ordering.
45
Lex-≤ : (≈ < : Rel A zero) → Rel (List A) zero
50
¬≤-this : ∀ {P ≈ < x y xs ys} → ¬ ≈ x y → ¬ < x y →
51
¬ Lex P ≈ < (x ∷ xs) (y ∷ ys)
52
¬≤-this ¬x≈y ¬x<y (this x<y) = ¬x<y x<y
53
¬≤-this ¬x≈y ¬x<y (next x≈y xs⊴ys) = ¬x≈y x≈y
55
¬≤-next : ∀ {P ≈ < x y xs ys} → ¬ < x y → ¬ Lex P ≈ < xs ys →
56
¬ Lex P ≈ < (x ∷ xs) (y ∷ ys)
57
¬≤-next ¬x<y ¬xs⊴ys (this x<y) = ¬x<y x<y
58
¬≤-next ¬x<y ¬xs⊴ys (next x≈y xs⊴ys) = ¬xs⊴ys xs⊴ys
60
----------------------------------------------------------------------
63
≤-reflexive : ∀ ≈ < → Pointwise.Rel ≈ ⇒ Lex-≤ ≈ <
64
≤-reflexive ≈ < [] = base tt
65
≤-reflexive ≈ < (x≈y ∷ xs≈ys) = next x≈y (≤-reflexive ≈ < xs≈ys)
67
<-irreflexive : ∀ {≈ <} → Irreflexive ≈ < →
68
Irreflexive (Pointwise.Rel ≈) (Lex-< ≈ <)
69
<-irreflexive irr [] (base ())
70
<-irreflexive irr (x≈y ∷ xs≈ys) (this x<y) = irr x≈y x<y
71
<-irreflexive irr (x≈y ∷ xs≈ys) (next x≊y xs⊴ys) =
72
<-irreflexive irr xs≈ys xs⊴ys
74
transitive : ∀ {P ≈ <} →
75
IsEquivalence ≈ → < Respects₂ ≈ → Transitive < →
76
Transitive (Lex P ≈ <)
77
transitive {P} {≈} {<} eq resp tr = trans
79
trans : Transitive (Lex P ≈ <)
80
trans (base p) (base _) = base p
81
trans (base y) halt = halt
82
trans halt (this y<z) = halt
83
trans halt (next y≈z ys⊴zs) = halt
84
trans (this x<y) (this y<z) = this (tr x<y y<z)
85
trans (this x<y) (next y≈z ys⊴zs) = this (proj₁ resp y≈z x<y)
86
trans (next x≈y xs⊴ys) (this y<z) =
87
this (proj₂ resp (IsEquivalence.sym eq x≈y) y<z)
88
trans (next x≈y xs⊴ys) (next y≈z ys⊴zs) =
89
next (IsEquivalence.trans eq x≈y y≈z) (trans xs⊴ys ys⊴zs)
91
antisymmetric : ∀ {P ≈ <} →
92
Symmetric ≈ → Irreflexive ≈ < → Asymmetric < →
93
Antisymmetric (Pointwise.Rel ≈) (Lex P ≈ <)
94
antisymmetric {P} {≈} {<} sym ir asym = as
96
as : Antisymmetric (Pointwise.Rel ≈) (Lex P ≈ <)
97
as (base _) (base _) = []
99
as (this x<y) (this y<x) = ⊥-elim (asym x<y y<x)
100
as (this x<y) (next y≈x ys⊴xs) = ⊥-elim (ir (sym y≈x) x<y)
101
as (next x≈y xs⊴ys) (this y<x) = ⊥-elim (ir (sym x≈y) y<x)
102
as (next x≈y xs⊴ys) (next y≈x ys⊴xs) = x≈y ∷ as xs⊴ys ys⊴xs
104
<-asymmetric : ∀ {≈ <} →
105
Symmetric ≈ → < Respects₂ ≈ → Asymmetric < →
106
Asymmetric (Lex-< ≈ <)
107
<-asymmetric {≈} {<} sym resp as = asym
109
irrefl : Irreflexive ≈ <
110
irrefl = asym⟶irr resp sym as
112
asym : Asymmetric (Lex-< ≈ <)
113
asym (base bot) _ = bot
115
asym (this x<y) (this y<x) = as x<y y<x
116
asym (this x<y) (next y≈x ys⊴xs) = irrefl (sym y≈x) x<y
117
asym (next x≈y xs⊴ys) (this y<x) = irrefl (sym x≈y) y<x
118
asym (next x≈y xs⊴ys) (next y≈x ys⊴xs) = asym xs⊴ys ys⊴xs
120
respects₂ : ∀ {P ≈ <} →
121
IsEquivalence ≈ → < Respects₂ ≈ →
122
Lex P ≈ < Respects₂ Pointwise.Rel ≈
123
respects₂ {P} {≈} {<} eq resp =
124
(λ {xs} {ys} {zs} → resp¹ {xs} {ys} {zs}) ,
125
(λ {xs} {ys} {zs} → resp² {xs} {ys} {zs})
127
resp¹ : ∀ {xs} → Lex P ≈ < xs Respects Pointwise.Rel ≈
128
resp¹ [] xs⊴[] = xs⊴[]
129
resp¹ (x≈y ∷ xs≈ys) halt = halt
130
resp¹ (x≈y ∷ xs≈ys) (this z<x) = this (proj₁ resp x≈y z<x)
131
resp¹ (x≈y ∷ xs≈ys) (next z≈x zs⊴xs) =
132
next (Eq.trans z≈x x≈y) (resp¹ xs≈ys zs⊴xs)
133
where module Eq = IsEquivalence eq
135
resp² : ∀ {ys} → flip (Lex P ≈ <) ys Respects Pointwise.Rel ≈
136
resp² [] []⊴ys = []⊴ys
137
resp² (x≈z ∷ xs≈zs) (this x<y) = this (proj₂ resp x≈z x<y)
138
resp² (x≈z ∷ xs≈zs) (next x≈y xs⊴ys) =
139
next (Eq.trans (Eq.sym x≈z) x≈y) (resp² xs≈zs xs⊴ys)
140
where module Eq = IsEquivalence eq
142
decidable : ∀ {P ≈ <} →
143
Dec P → Decidable ≈ → Decidable < →
144
Decidable (Lex P ≈ <)
145
decidable {P} {≈} {<} dec-P dec-≈ dec-< = dec
147
dec : Decidable (Lex P ≈ <)
149
... | yes p = yes (base p)
150
... | no ¬p = no helper
152
helper : ¬ Lex P ≈ < [] []
153
helper (base p) = ¬p p
154
dec [] (y ∷ ys) = yes halt
155
dec (x ∷ xs) [] = no (λ ())
156
dec (x ∷ xs) (y ∷ ys) with dec-< x y
157
... | yes x<y = yes (this x<y)
158
... | no ¬x<y with dec-≈ x y
159
... | no ¬x≈y = no (¬≤-this ¬x≈y ¬x<y)
160
... | yes x≈y with dec xs ys
161
... | yes xs⊴ys = yes (next x≈y xs⊴ys)
162
... | no ¬xs⊴ys = no (¬≤-next ¬x<y ¬xs⊴ys)
164
<-decidable : ∀ {≈ <} →
165
Decidable ≈ → Decidable < → Decidable (Lex-< ≈ <)
166
<-decidable = decidable (no id)
168
≤-decidable : ∀ {≈ <} →
169
Decidable ≈ → Decidable < → Decidable (Lex-≤ ≈ <)
170
≤-decidable = decidable (yes tt)
172
-- Note that trichotomy is an unnecessarily strong precondition for
173
-- the following lemma.
176
Symmetric ≈ → Trichotomous ≈ < → Total (Lex-≤ ≈ <)
177
≤-total {≈} {<} sym tri = total
179
total : Total (Lex-≤ ≈ <)
180
total [] [] = inj₁ (base tt)
181
total [] (x ∷ xs) = inj₁ halt
182
total (x ∷ xs) [] = inj₂ halt
183
total (x ∷ xs) (y ∷ ys) with tri x y
184
... | tri< x<y _ _ = inj₁ (this x<y)
185
... | tri> _ _ y<x = inj₂ (this y<x)
186
... | tri≈ _ x≈y _ with total xs ys
187
... | inj₁ xs≲ys = inj₁ (next x≈y xs≲ys)
188
... | inj₂ ys≲xs = inj₂ (next (sym x≈y) ys≲xs)
190
<-compare : ∀ {≈ <} →
191
Symmetric ≈ → Trichotomous ≈ < →
192
Trichotomous (Pointwise.Rel ≈) (Lex-< ≈ <)
193
<-compare {≈} {<} sym tri = cmp
195
cmp : Trichotomous (Pointwise.Rel ≈) (Lex-< ≈ <)
196
cmp [] [] = tri≈ ¬[]<[] [] ¬[]<[]
197
cmp [] (y ∷ ys) = tri< halt (λ ()) (λ ())
198
cmp (x ∷ xs) [] = tri> (λ ()) (λ ()) halt
199
cmp (x ∷ xs) (y ∷ ys) with tri x y
200
... | tri< x<y ¬x≈y ¬y<x =
201
tri< (this x<y) (¬x≈y ∘ head) (¬≤-this (¬x≈y ∘ sym) ¬y<x)
202
... | tri> ¬x<y ¬x≈y y<x =
203
tri> (¬≤-this ¬x≈y ¬x<y) (¬x≈y ∘ head) (this y<x)
204
... | tri≈ ¬x<y x≈y ¬y<x with cmp xs ys
205
... | tri< xs<ys ¬xs≈ys ¬ys<xs =
206
tri< (next x≈y xs<ys) (¬xs≈ys ∘ tail) (¬≤-next ¬y<x ¬ys<xs)
207
... | tri≈ ¬xs<ys xs≈ys ¬ys<xs =
208
tri≈ (¬≤-next ¬x<y ¬xs<ys) (x≈y ∷ xs≈ys) (¬≤-next ¬y<x ¬ys<xs)
209
... | tri> ¬xs<ys ¬xs≈ys ys<xs =
210
tri> (¬≤-next ¬x<y ¬xs<ys) (¬xs≈ys ∘ tail) (next (sym x≈y) ys<xs)
212
-- Some collections of properties which are preserved by Lex-≤ or
215
≤-isPreorder : ∀ {≈ <} →
216
IsEquivalence ≈ → Transitive < → < Respects₂ ≈ →
217
IsPreorder (Pointwise.Rel ≈) (Lex-≤ ≈ <)
218
≤-isPreorder {≈} {<} eq tr resp = record
219
{ isEquivalence = Pointwise.isEquivalence eq
220
; reflexive = ≤-reflexive ≈ <
221
; trans = transitive eq resp tr
222
; ∼-resp-≈ = respects₂ eq resp
225
≤-isPartialOrder : ∀ {≈ <} →
226
IsStrictPartialOrder ≈ < →
227
IsPartialOrder (Pointwise.Rel ≈) (Lex-≤ ≈ <)
228
≤-isPartialOrder {≈} {<} spo = record
229
{ isPreorder = ≤-isPreorder isEquivalence trans <-resp-≈
230
; antisym = antisymmetric Eq.sym irrefl
231
(trans∧irr⟶asym {≈ = ≈} {<} Eq.refl trans irrefl)
232
} where open IsStrictPartialOrder spo
234
≤-isTotalOrder : ∀ {≈ <} →
235
IsStrictTotalOrder ≈ < →
236
IsTotalOrder (Pointwise.Rel ≈) (Lex-≤ ≈ <)
237
≤-isTotalOrder sto = record
239
≤-isPartialOrder (record
240
{ isEquivalence = isEquivalence
241
; irrefl = tri⟶irr <-resp-≈ Eq.sym compare
243
; <-resp-≈ = <-resp-≈
245
; total = ≤-total Eq.sym compare
246
} where open IsStrictTotalOrder sto
248
≤-isDecTotalOrder : ∀ {≈ <} →
249
IsStrictTotalOrder ≈ < →
250
IsDecTotalOrder (Pointwise.Rel ≈) (Lex-≤ ≈ <)
251
≤-isDecTotalOrder sto = record
252
{ isTotalOrder = ≤-isTotalOrder sto
253
; _≟_ = Pointwise.decidable _≟_
254
; _≤?_ = ≤-decidable _≟_ (tri⟶dec< compare)
255
} where open IsStrictTotalOrder sto
257
<-isStrictPartialOrder
258
: ∀ {≈ <} → IsStrictPartialOrder ≈ < →
259
IsStrictPartialOrder (Pointwise.Rel ≈) (Lex-< ≈ <)
260
<-isStrictPartialOrder spo = record
261
{ isEquivalence = Pointwise.isEquivalence isEquivalence
262
; irrefl = <-irreflexive irrefl
263
; trans = transitive isEquivalence <-resp-≈ trans
264
; <-resp-≈ = respects₂ isEquivalence <-resp-≈
265
} where open IsStrictPartialOrder spo
268
: ∀ {≈ <} → IsStrictTotalOrder ≈ < →
269
IsStrictTotalOrder (Pointwise.Rel ≈) (Lex-< ≈ <)
270
<-isStrictTotalOrder sto = record
271
{ isEquivalence = Pointwise.isEquivalence isEquivalence
272
; trans = transitive isEquivalence <-resp-≈ trans
273
; compare = <-compare Eq.sym compare
274
; <-resp-≈ = respects₂ isEquivalence <-resp-≈
275
} where open IsStrictTotalOrder sto
279
-- "Packages" (e.g. preorders) can also be handled.
281
≤-preorder : Preorder _ _ _ → Preorder _ _ _
282
≤-preorder pre = record
283
{ isPreorder = ≤-isPreorder isEquivalence trans ∼-resp-≈
284
} where open Preorder pre
286
≤-partialOrder : StrictPartialOrder _ _ _ → Poset _ _ _
287
≤-partialOrder spo = record
288
{ isPartialOrder = ≤-isPartialOrder isStrictPartialOrder
289
} where open StrictPartialOrder spo
291
≤-decTotalOrder : StrictTotalOrder _ _ _ → DecTotalOrder _ _ _
292
≤-decTotalOrder sto = record
293
{ isDecTotalOrder = ≤-isDecTotalOrder isStrictTotalOrder
294
} where open StrictTotalOrder sto
296
<-strictPartialOrder :
297
StrictPartialOrder _ _ _ → StrictPartialOrder _ _ _
298
<-strictPartialOrder spo = record
299
{ isStrictPartialOrder = <-isStrictPartialOrder isStrictPartialOrder
300
} where open StrictPartialOrder spo
302
<-strictTotalOrder : StrictTotalOrder _ _ _ → StrictTotalOrder _ _ _
303
<-strictTotalOrder sto = record
304
{ isStrictTotalOrder = <-isStrictTotalOrder isStrictTotalOrder
305
} where open StrictTotalOrder sto
added
removed
src/Relation/Binary/List/StrictLex.agda
