1
------------------------------------------------------------------------
2
-- Lexicographic products of binary relations
3
------------------------------------------------------------------------
5
-- The definition of lexicographic product used here is suitable if
6
-- the left-hand relation is a (non-strict) partial order.
8
module Relation.Binary.Product.NonStrictLex where
10
open import Data.Product
13
open import Relation.Binary
14
open import Relation.Binary.Consequences
15
import Relation.Binary.NonStrictToStrict as Conv
16
open import Relation.Binary.Product.Pointwise as Pointwise
18
import Relation.Binary.Product.StrictLex as Strict
21
module Dummy {a₁ a₂ : Set} where
23
×-Lex : (≈₁ ≤₁ : Rel a₁ zero) → (≤₂ : Rel a₂ zero) →
25
×-Lex ≈₁ ≤₁ ≤₂ = Strict.×-Lex ≈₁ (Conv._<_ ≈₁ ≤₁) ≤₂
27
-- Some properties which are preserved by ×-Lex (under certain
30
×-reflexive : ∀ ≈₁ ≤₁ {≈₂} ≤₂ →
31
≈₂ ⇒ ≤₂ → (≈₁ ×-Rel ≈₂) ⇒ (×-Lex ≈₁ ≤₁ ≤₂)
32
×-reflexive ≈₁ ≤₁ ≤₂ refl₂ {x} {y} =
33
Strict.×-reflexive ≈₁ (Conv._<_ ≈₁ ≤₁) ≤₂ refl₂ {x} {y}
35
×-transitive : ∀ {≈₁ ≤₁} → IsPartialOrder ≈₁ ≤₁ →
36
∀ {≤₂} → Transitive ≤₂ →
37
Transitive (×-Lex ≈₁ ≤₁ ≤₂)
38
×-transitive {≈₁ = ≈₁} {≤₁ = ≤₁} po₁ {≤₂ = ≤₂} trans₂
42
isEquivalence (Conv.<-resp-≈ _ _ isEquivalence ≤-resp-≈)
44
{≤₂ = ≤₂} trans₂ {x} {y} {z}
45
where open IsPartialOrder po₁
47
×-antisymmetric : ∀ {≈₁ ≤₁} → IsPartialOrder ≈₁ ≤₁ →
48
∀ {≈₂ ≤₂} → Antisymmetric ≈₂ ≤₂ →
49
Antisymmetric (≈₁ ×-Rel ≈₂) (×-Lex ≈₁ ≤₁ ≤₂)
50
×-antisymmetric {≈₁ = ≈₁} {≤₁ = ≤₁} po₁ {≤₂ = ≤₂} antisym₂
52
Strict.×-antisymmetric {<₁ = Conv._<_ ≈₁ ≤₁} ≈-sym₁ irrefl₁ asym₁
53
{≤₂ = ≤₂} antisym₂ {x} {y}
55
open IsPartialOrder po₁
56
open Eq renaming (refl to ≈-refl₁; sym to ≈-sym₁)
58
irrefl₁ : Irreflexive ≈₁ (Conv._<_ ≈₁ ≤₁)
59
irrefl₁ = Conv.irrefl ≈₁ ≤₁
61
asym₁ : Asymmetric (Conv._<_ ≈₁ ≤₁)
62
asym₁ = trans∧irr⟶asym {≈ = ≈₁}
63
≈-refl₁ (Conv.trans _ _ po₁) irrefl₁
65
×-≈-respects₂ : ∀ {≈₁ ≤₁} → IsEquivalence ≈₁ → ≤₁ Respects₂ ≈₁ →
66
∀ {≈₂ ≤₂} → ≤₂ Respects₂ ≈₂ →
67
(×-Lex ≈₁ ≤₁ ≤₂) Respects₂ (≈₁ ×-Rel ≈₂)
68
×-≈-respects₂ eq₁ resp₁ resp₂ =
69
Strict.×-≈-respects₂ eq₁ (Conv.<-resp-≈ _ _ eq₁ resp₁) resp₂
71
×-decidable : ∀ {≈₁ ≤₁} → Decidable ≈₁ → Decidable ≤₁ →
72
∀ {≤₂} → Decidable ≤₂ →
73
Decidable (×-Lex ≈₁ ≤₁ ≤₂)
74
×-decidable dec-≈₁ dec-≤₁ dec-≤₂ =
75
Strict.×-decidable dec-≈₁ (Conv.decidable _ _ dec-≈₁ dec-≤₁)
78
×-total : ∀ {≈₁ ≤₁} → Symmetric ≈₁ → Decidable ≈₁ →
79
Antisymmetric ≈₁ ≤₁ → Total ≤₁ →
81
Total (×-Lex ≈₁ ≤₁ ≤₂)
82
×-total {≈₁ = ≈₁} {≤₁ = ≤₁} sym₁ dec₁ antisym₁ total₁
83
{≤₂ = ≤₂} total₂ = total
85
tri₁ : Trichotomous ≈₁ (Conv._<_ ≈₁ ≤₁)
86
tri₁ = Conv.trichotomous _ _ sym₁ dec₁ antisym₁ total₁
88
total : Total (×-Lex ≈₁ ≤₁ ≤₂)
89
total x y with tri₁ (proj₁ x) (proj₁ y)
90
... | tri< x₁<y₁ x₁≉y₁ x₁≯y₁ = inj₁ (inj₁ x₁<y₁)
91
... | tri> x₁≮y₁ x₁≉y₁ x₁>y₁ = inj₂ (inj₁ x₁>y₁)
92
... | tri≈ x₁≮y₁ x₁≈y₁ x₁≯y₁ with total₂ (proj₂ x) (proj₂ y)
93
... | inj₁ x₂≤y₂ = inj₁ (inj₂ (x₁≈y₁ , x₂≤y₂))
94
... | inj₂ x₂≥y₂ = inj₂ (inj₂ (sym₁ x₁≈y₁ , x₂≥y₂))
96
-- Some collections of properties which are preserved by ×-Lex
97
-- (under certain assumptions).
99
_×-isPartialOrder_ : ∀ {≈₁ ≤₁} → IsPartialOrder ≈₁ ≤₁ →
100
∀ {≈₂ ≤₂} → IsPartialOrder ≈₂ ≤₂ →
101
IsPartialOrder (≈₁ ×-Rel ≈₂) (×-Lex ≈₁ ≤₁ ≤₂)
102
_×-isPartialOrder_ {≈₁ = ≈₁} {≤₁ = ≤₁} po₁ {≤₂ = ≤₂} po₂ = record
103
{ isPreorder = record
104
{ isEquivalence = Pointwise._×-isEquivalence_
107
; reflexive = λ {x y} →
108
×-reflexive ≈₁ ≤₁ ≤₂ (reflexive po₂) {x} {y}
109
; trans = λ {x y z} →
110
×-transitive po₁ {≤₂ = ≤₂} (trans po₂)
112
; ∼-resp-≈ = ×-≈-respects₂ (isEquivalence po₁)
116
; antisym = λ {x y} →
117
×-antisymmetric {≤₁ = ≤₁} po₁
118
{≤₂ = ≤₂} (antisym po₂) {x} {y}
120
where open IsPartialOrder
122
×-isTotalOrder : ∀ {≈₁ ≤₁} → Decidable ≈₁ → IsTotalOrder ≈₁ ≤₁ →
123
∀ {≈₂ ≤₂} → IsTotalOrder ≈₂ ≤₂ →
124
IsTotalOrder (≈₁ ×-Rel ≈₂) (×-Lex ≈₁ ≤₁ ≤₂)
125
×-isTotalOrder {≤₁ = ≤₁} ≈₁-dec to₁ {≤₂ = ≤₂} to₂ = record
126
{ isPartialOrder = isPartialOrder to₁ ×-isPartialOrder
128
; total = ×-total {≤₁ = ≤₁} (Eq.sym to₁) ≈₁-dec
129
(antisym to₁) (total to₁)
130
{≤₂ = ≤₂} (total to₂)
132
where open IsTotalOrder
134
_×-isDecTotalOrder_ : ∀ {≈₁ ≤₁} → IsDecTotalOrder ≈₁ ≤₁ →
135
∀ {≈₂ ≤₂} → IsDecTotalOrder ≈₂ ≤₂ →
136
IsDecTotalOrder (≈₁ ×-Rel ≈₂) (×-Lex ≈₁ ≤₁ ≤₂)
137
_×-isDecTotalOrder_ {≤₁ = ≤₁} to₁ {≤₂ = ≤₂} to₂ = record
138
{ isTotalOrder = ×-isTotalOrder (_≟_ to₁)
141
; _≟_ = Pointwise._×-decidable_ (_≟_ to₁) (_≟_ to₂)
142
; _≤?_ = ×-decidable (_≟_ to₁) (_≤?_ to₁) (_≤?_ to₂)
144
where open IsDecTotalOrder
148
-- "Packages" (e.g. posets) can also be combined.
150
_×-poset_ : Poset _ _ _ → Poset _ _ _ → Poset _ _ _
151
p₁ ×-poset p₂ = record
152
{ isPartialOrder = isPartialOrder p₁ ×-isPartialOrder
157
DecTotalOrder _ _ _ → TotalOrder _ _ _ → TotalOrder _ _ _
158
t₁ ×-totalOrder t₂ = record
159
{ isTotalOrder = ×-isTotalOrder T₁._≟_ T₁.isTotalOrder T₂.isTotalOrder
162
module T₁ = DecTotalOrder t₁
163
module T₂ = TotalOrder t₂
166
DecTotalOrder _ _ _ → DecTotalOrder _ _ _ → DecTotalOrder _ _ _
167
t₁ ×-decTotalOrder t₂ = record
168
{ isDecTotalOrder = isDecTotalOrder t₁ ×-isDecTotalOrder
170
} where open DecTotalOrder
added
removed
src/Relation/Binary/Product/NonStrictLex.agda
