blob: 84d8e03f68887cf08dde2fbbc1a80f76e42b1501 (
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
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
|
module Data.List.Relation.Binary.Prefix where
open import Data.Empty using (⊥-elim)
open import Data.List.Base using (List; []; _∷_; _++_; length; inits; map)
open import Data.List.Properties using (length-++)
open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_; setoid)
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
open import Data.Nat using (_≤_; z≤n; s≤s; _+_) renaming (_<_ to _<ⁿ_)
open import Data.Nat.Properties using (<⇒≱; m<m+n; module ≤-Reasoning)
open import Data.Product using (_,_; uncurry)
open import Function.Equivalence using (_⇔_; equivalence)
open import Level using (Level; _⊔_)
open import Relation.Binary
open import Relation.Nullary using (Dec; yes; no; ¬_)
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Unary using (Pred)
private
variable
a ℓ : Level
module _
{A : Set a} (P : Set) (_≈_ : Rel A ℓ)
where
data Prefix : Rel (List A) ℓ where
base : P → Prefix [] []
halt : ∀ {y ys} → Prefix [] (y ∷ ys)
next : ∀ {x xs y ys}
(x≈y : x ≈ y) (xs<ys : Prefix xs ys) → Prefix (x ∷ xs) (y ∷ ys)
module _
{A : Set a} {P : Set} {_≈_ : Rel A ℓ}
where
private
_≋_ = Pointwise _≈_
_<_ = Prefix P _≈_
initsPrefixes : P → Reflexive _≈_ → ∀ xs → All (_< xs) (inits xs)
initsPrefixes p refl [] = base p ∷ []
initsPrefixes p refl (x ∷ xs) = halt ∷ map′ (x ∷_ ) (next refl) (initsPrefixes p refl xs)
where
map′ : ∀ {a b p q} {A : Set a} {B : Set b} {P : Pred A p} {Q : Pred B q} →
(f : A → B) → (∀ {x} → P x → Q (f x)) → ∀ {xs} → All P xs → All Q (map f xs)
map′ f pres [] = []
map′ f pres (px ∷ pxs) = pres px ∷ map′ f pres pxs
module _
(equivalence : IsEquivalence _≈_)
where
open IsEquivalence equivalence
open import Data.List.Membership.Setoid (setoid (record { isEquivalence = equivalence })) using (_∈_)
open import Data.List.Relation.Unary.Any using (Any; here; there)
prefix∈inits : ∀ {xs ys} → xs < ys → xs ∈ inits ys
prefix∈inits (base x) = here []
prefix∈inits halt = here []
prefix∈inits (next x≈y xs<ys) = there (map′ (_∷_ _) (x≈y ∷_) (prefix∈inits xs<ys))
where
map′ : ∀ {a b p q} {A : Set a} {B : Set b} {P : Pred A p} {Q : Pred B q} →
(f : A → B) → (∀ {x} → P x → Q (f x)) → ∀ {xs} → Any P xs → Any Q (map f xs)
map′ f pres (here px) = here (pres px)
map′ f pres (there pxs) = there (map′ f pres pxs)
reflexive : P → Reflexive _≈_ → Reflexive _<_
reflexive p refl {[]} = base p
reflexive p refl {x ∷ xs} = next refl (reflexive p refl)
irreflexive : ¬ P → Irreflexive _≋_ _<_
irreflexive ¬p [] (base p) = ¬p p
irreflexive ¬p (_ ∷ xs≋ys) (next _ xs<ys) = irreflexive ¬p xs≋ys xs<ys
transitive : Transitive _≈_ → Transitive _<_
transitive trans (base _) ys<zs = ys<zs
transitive trans halt (next _ _) = halt
transitive trans (next x≈y xs<ys) (next y≈z ys<zs) =
next (trans x≈y y≈z) (transitive trans xs<ys ys<zs)
antisymmetric : Symmetric _≈_ → Antisymmetric _≋_ _<_
antisymmetric sym (base _) (base _) = []
antisymmetric sym (next x≈y xs<ys) (next y≈x ys<xs) =
x≈y ∷ antisymmetric sym xs<ys ys<xs
decidable : Dec P → Decidable _≈_ → Decidable _<_
decidable P? _≈?_ [] [] = Dec.map′ base (λ { (base p) → p }) P?
decidable P? _≈?_ [] (x ∷ ys) = yes halt
decidable P? _≈?_ (x ∷ xs) [] = no λ ()
decidable P? _≈?_ (x ∷ xs) (y ∷ ys) =
Dec.map′ (uncurry next)
(λ { (next x≈y xs<ys) → x≈y , xs<ys })
((x ≈? y) ×-dec (decidable P? _≈?_ xs ys))
length≤ : ∀ {xs} {ys} → xs < ys → length xs ≤ length ys
length≤ (base x) = z≤n
length≤ halt = z≤n
length≤ (next x≈y xs<ys) = s≤s (length≤ xs<ys)
length< : ∀ {xs} {ys} → ¬ P → xs < ys → length xs <ⁿ length ys
length< ¬p (base p) = ⊥-elim (¬p p)
length< ¬p halt = s≤s z≤n
length< ¬p (next x≈y xs<ys) = s≤s (length< ¬p xs<ys)
minimum : P → Minimum _<_ []
minimum p [] = base p
minimum p (x ∷ xs) = halt
¬maximum : A → ∀ xs → ¬ Maximum _<_ xs
¬maximum a xs max =
<⇒≱
(begin-strict
length xs <⟨ m<m+n (length xs) (s≤s z≤n) ⟩
length xs + length (a ∷ []) ≡˘⟨ length-++ xs ⟩
length (xs ++ a ∷ []) ∎)
(length≤ (max (xs ++ a ∷ [])))
where open ≤-Reasoning
|
