-
Notifications
You must be signed in to change notification settings - Fork 247
/
Copy pathCore.agda
155 lines (123 loc) · 8.23 KB
/
Core.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
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lexicographic ordering of same-length vectors
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Vec.Relation.Binary.Lex.Core {a} {A : Set a} where
open import Data.Empty
open import Data.Nat.Base using (ℕ; suc)
import Data.Nat.Properties as ℕ
open import Data.Product.Base using (_×_; _,_; proj₁; proj₂; uncurry)
open import Data.Vec.Base using (Vec; []; _∷_)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise; []; _∷_)
open import Function.Base using (flip)
open import Function.Bundles using (_⇔_; mk⇔)
open import Level using (Level; _⊔_)
open import Relation.Binary.Core using (Rel; REL)
open import Relation.Binary.Definitions
using (Transitive; Symmetric; Asymmetric; Antisymmetric; Irreflexive; Trans; _Respects₂_; _Respectsˡ_; _Respectsʳ_; Decidable; Irrelevant)
open import Relation.Binary.Structures using (IsPartialEquivalence)
open import Relation.Binary.PropositionalEquality.Core as ≡
using (_≡_; refl; cong)
import Relation.Nullary as Nullary
open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×-dec_; _⊎-dec_)
open import Relation.Nullary.Negation
private
variable
ℓ₁ ℓ₂ : Level
------------------------------------------------------------------------
-- Definition
-- The lexicographic ordering itself can be either strict or non-strict,
-- depending on whether type P is inhabited.
data Lex {A : Set a} (P : Set) (_≈_ : Rel A ℓ₁) (_≺_ : Rel A ℓ₂)
: ∀ {m n} → REL (Vec A m) (Vec A n) (a ⊔ ℓ₁ ⊔ ℓ₂) where
base : (p : P) → Lex P _≈_ _≺_ [] []
this : ∀ {x y m n} {xs : Vec A m} {ys : Vec A n}
(x≺y : x ≺ y) (m≡n : m ≡ n) → Lex P _≈_ _≺_ (x ∷ xs) (y ∷ ys)
next : ∀ {x y m n} {xs : Vec A m} {ys : Vec A n}
(x≈y : x ≈ y) (xs<ys : Lex P _≈_ _≺_ xs ys) → Lex P _≈_ _≺_ (x ∷ xs) (y ∷ ys)
------------------------------------------------------------------------
-- Operations
map-P : ∀ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} {P₁ P₂ : Set} → (P₁ → P₂) →
∀ {m n} {xs : Vec A m} {ys : Vec A n} →
Lex P₁ _≈_ _≺_ xs ys → Lex P₂ _≈_ _≺_ xs ys
map-P f (base p) = base (f p)
map-P f (this x≺y m≡n) = this x≺y m≡n
map-P f (next x≈y xs<ys) = next x≈y (map-P f xs<ys)
------------------------------------------------------------------------
-- Properties
module _ {P : Set} {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
length-equal : ∀ {m n} {xs : Vec A m} {ys : Vec A n} →
Lex P _≈_ _≺_ xs ys → m ≡ n
length-equal (base _) = refl
length-equal (this x≺y m≡n) = cong suc m≡n
length-equal (next x≈y xs<ys) = cong suc (length-equal xs<ys)
module _ {P : Set} {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
private
_≋_ = Pointwise _≈_
_<ₗₑₓ_ = Lex P _≈_ _≺_
≰-this : ∀ {x y m n} {xs : Vec A m} {ys : Vec A n} →
¬ (x ≈ y) → ¬ (x ≺ y) → ¬ (x ∷ xs) <ₗₑₓ (y ∷ ys)
≰-this x≉y x≮y (this x≺y m≡n) = contradiction x≺y x≮y
≰-this x≉y x≮y (next x≈y xs<ys) = contradiction x≈y x≉y
≰-next : ∀ {x y m n} {xs : Vec A m} {ys : Vec A n} →
¬ (x ≺ y) → ¬ (xs <ₗₑₓ ys) → ¬ (x ∷ xs) <ₗₑₓ (y ∷ ys)
≰-next x≮y xs≮ys (this x≺y m≡n) = contradiction x≺y x≮y
≰-next x≮y xs≮ys (next x≈y xs<ys) = contradiction xs<ys xs≮ys
P⇔[]<[] : P ⇔ [] <ₗₑₓ []
P⇔[]<[] = mk⇔ base (λ { (base p) → p })
toSum : ∀ {x y n} {xs ys : Vec A n} → (x ∷ xs) <ₗₑₓ (y ∷ ys) → (x ≺ y ⊎ (x ≈ y × xs <ₗₑₓ ys))
toSum (this x≺y m≡n) = inj₁ x≺y
toSum (next x≈y xs<ys) = inj₂ (x≈y , xs<ys)
∷<∷-⇔ : ∀ {x y n} {xs ys : Vec A n} → (x ≺ y ⊎ (x ≈ y × xs <ₗₑₓ ys)) ⇔ (x ∷ xs) <ₗₑₓ (y ∷ ys)
∷<∷-⇔ = mk⇔ [ flip this refl , uncurry next ] toSum
module _ (≈-equiv : IsPartialEquivalence _≈_)
((≺-respˡ-≈ , ≺-respʳ-≈) : _≺_ Respects₂ _≈_)
(≺-trans : Transitive _≺_)
(open IsPartialEquivalence ≈-equiv)
where
transitive′ : ∀ {m n o P₂} → Trans (Lex P _≈_ _≺_ {m} {n}) (Lex P₂ _≈_ _≺_ {n} {o}) (Lex (P × P₂) _≈_ _≺_)
transitive′ (base p₁) (base p₂) = base (p₁ , p₂)
transitive′ (this x≺y m≡n) (this y≺z n≡o) = this (≺-trans x≺y y≺z) (≡.trans m≡n n≡o)
transitive′ (this x≺y m≡n) (next y≈z ys<zs) = this (≺-respʳ-≈ y≈z x≺y) (≡.trans m≡n (length-equal ys<zs))
transitive′ (next x≈y xs<ys) (this y≺z n≡o) = this (≺-respˡ-≈ (sym x≈y) y≺z) (≡.trans (length-equal xs<ys) n≡o)
transitive′ (next x≈y xs<ys) (next y≈z ys<zs) = next (trans x≈y y≈z) (transitive′ xs<ys ys<zs)
transitive : ∀ {m n o} → Trans (_<ₗₑₓ_ {m} {n}) (_<ₗₑₓ_ {n} {o}) _<ₗₑₓ_
transitive xs<ys ys<zs = map-P proj₁ (transitive′ xs<ys ys<zs)
module _ (≈-sym : Symmetric _≈_) (≺-irrefl : Irreflexive _≈_ _≺_) (≺-asym : Asymmetric _≺_) where
antisym : ∀ {n} → Antisymmetric (_≋_ {n}) (_<ₗₑₓ_)
antisym (base _) (base _) = []
antisym (this x≺y m≡n) (this y≺x n≡m) = ⊥-elim (≺-asym x≺y y≺x)
antisym (this x≺y m≡n) (next y≈x ys<xs) = ⊥-elim (≺-irrefl (≈-sym y≈x) x≺y)
antisym (next x≈y xs<ys) (this y≺x m≡n) = ⊥-elim (≺-irrefl (≈-sym x≈y) y≺x)
antisym (next x≈y xs<ys) (next y≈x ys<xs) = x≈y ∷ (antisym xs<ys ys<xs)
module _ (≈-equiv : IsPartialEquivalence _≈_) (open IsPartialEquivalence ≈-equiv) where
respectsˡ : _≺_ Respectsˡ _≈_ → ∀ {m n} → (_<ₗₑₓ_ {m} {n}) Respectsˡ _≋_
respectsˡ resp [] (base p) = base p
respectsˡ resp (x≈y ∷ xs≋ys) (this x≺z m≡n) = this (resp x≈y x≺z) m≡n
respectsˡ resp (x≈y ∷ xs≋ys) (next x≈z xs<zs) = next (trans (sym x≈y) x≈z) (respectsˡ resp xs≋ys xs<zs)
respectsʳ : _≺_ Respectsʳ _≈_ → ∀ {m n} → (_<ₗₑₓ_ {m} {n}) Respectsʳ _≋_
respectsʳ resp [] (base p) = base p
respectsʳ resp (x≈y ∷ xs≋ys) (this x≺z m≡n) = this (resp x≈y x≺z) m≡n
respectsʳ resp (x≈y ∷ xs≋ys) (next x≈z xs<zs) = next (trans x≈z x≈y) (respectsʳ resp xs≋ys xs<zs)
respects₂ : _≺_ Respects₂ _≈_ → ∀ {n} → (_<ₗₑₓ_ {n} {n}) Respects₂ _≋_
respects₂ (≺-resp-≈ˡ , ≺-resp-≈ʳ) = respectsˡ ≺-resp-≈ˡ , respectsʳ ≺-resp-≈ʳ
module _ (P? : Dec P) (_≈?_ : Decidable _≈_) (_≺?_ : Decidable _≺_) where
decidable : ∀ {m n} → Decidable (_<ₗₑₓ_ {m} {n})
decidable {m} {n} xs ys with m ℕ.≟ n
decidable {_} {_} [] [] | yes refl = Dec.map P⇔[]<[] P?
decidable {_} {_} (x ∷ xs) (y ∷ ys) | yes refl = Dec.map ∷<∷-⇔ ((x ≺? y) ⊎-dec (x ≈? y) ×-dec (decidable xs ys))
decidable {_} {_} _ _ | no m≢n = no (λ xs<ys → contradiction (length-equal xs<ys) m≢n)
module _ (P-irrel : Nullary.Irrelevant P)
(≈-irrel : Irrelevant _≈_)
(≺-irrel : Irrelevant _≺_)
(≺-irrefl : Irreflexive _≈_ _≺_)
where
irrelevant : ∀ {m n} → Irrelevant (_<ₗₑₓ_ {m} {n})
irrelevant (base p₁) (base p₂) rewrite P-irrel p₁ p₂ = refl
irrelevant (this x≺y₁ m≡n₁) (this x≺y₂ m≡n₂) rewrite ≺-irrel x≺y₁ x≺y₂ | ℕ.≡-irrelevant m≡n₁ m≡n₂ = refl
irrelevant (this x≺y m≡n) (next x≈y xs<ys₂) = contradiction x≺y (≺-irrefl x≈y)
irrelevant (next x≈y xs<ys₁) (this x≺y m≡n) = contradiction x≺y (≺-irrefl x≈y)
irrelevant (next x≈y₁ xs<ys₁) (next x≈y₂ xs<ys₂) rewrite ≈-irrel x≈y₁ x≈y₂ | irrelevant xs<ys₁ xs<ys₂ = refl