blob: 43f001c7d3ef0058d9f96ab8915dcea9ec373256 (
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
119
120
121
122
|
------------------------------------------------------------------------
-- Agda Helium
--
-- Relational properties of strict total orders
------------------------------------------------------------------------
{-# OPTIONS --safe --without-K #-}
open import Relation.Binary
module Helium.Relation.Binary.Properties.StrictTotalOrder
{a ℓ₁ ℓ₂} (STO : StrictTotalOrder a ℓ₁ ℓ₂)
where
open import Data.Sum using (inj₁; inj₂)
open import Function using (flip)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (contradiction)
open StrictTotalOrder STO
renaming
( trans to <-trans
; irrefl to <-irrefl
; asym to <-asym
)
import Relation.Binary.Construct.StrictToNonStrict _≈_ _<_ as ToNonStrict
infix 4 _≉_ _≮_ _≤_ _≰_ _>_ _≥_
_≉_ : Rel Carrier ℓ₁
x ≉ y = ¬ x ≈ y
_≮_ : Rel Carrier ℓ₂
x ≮ y = ¬ x < y
_≤_ : Rel Carrier _
_≤_ = ToNonStrict._≤_
_≰_ : Rel Carrier _
x ≰ y = ¬ x ≤ y
_>_ : Rel Carrier ℓ₂
_>_ = flip _<_
_≥_ : Rel Carrier _
_≥_ = flip _≤_
<-≤-trans : Trans _<_ _≤_ _<_
<-≤-trans = ToNonStrict.<-≤-trans <-trans <-respʳ-≈
≤-<-trans : Trans _≤_ _<_ _<_
≤-<-trans = ToNonStrict.≤-<-trans Eq.sym <-trans <-respˡ-≈
≤-respˡ-≈ : _≤_ Respectsˡ _≈_
≤-respˡ-≈ = ToNonStrict.≤-respˡ-≈ Eq.sym Eq.trans <-respˡ-≈
≤-respʳ-≈ : _≤_ Respectsʳ _≈_
≤-respʳ-≈ = ToNonStrict.≤-respʳ-≈ Eq.trans <-respʳ-≈
≤-resp-≈ : _≤_ Respects₂ _≈_
≤-resp-≈ = ToNonStrict.≤-resp-≈ Eq.isEquivalence <-resp-≈
≤-reflexive : _≈_ ⇒ _≤_
≤-reflexive = ToNonStrict.reflexive
≤-refl : Reflexive _≤_
≤-refl = ≤-reflexive Eq.refl
≤-trans : Transitive _≤_
≤-trans = ToNonStrict.trans Eq.isEquivalence <-resp-≈ <-trans
≤-antisym : Antisymmetric _≈_ _≤_
≤-antisym = ToNonStrict.antisym Eq.isEquivalence <-trans <-irrefl
≤-total : Total _≤_
≤-total = ToNonStrict.total compare
<⇒≤ : _<_ ⇒ _≤_
<⇒≤ = ToNonStrict.<⇒≤
<⇒≉ : Irreflexive _<_ _≈_
<⇒≉ = flip <-irrefl
≤∧≉⇒< : ∀ {x y} → x ≤ y → x ≉ y → x < y
≤∧≉⇒< (inj₁ x<y) x≉y = x<y
≤∧≉⇒< (inj₂ x≈y) x≉y = contradiction x≈y x≉y
≤∧≮⇒≈ : ∀ {x y} → x ≤ y → x ≮ y → x ≈ y
≤∧≮⇒≈ (inj₁ x<y) x≮y = contradiction x<y x≮y
≤∧≮⇒≈ (inj₂ x≈y) x≮y = x≈y
<⇒≱ : Irreflexive _<_ _≥_
<⇒≱ x<y (inj₁ x>y) = <-asym x<y x>y
<⇒≱ x<y (inj₂ y≈x) = <-irrefl (Eq.sym y≈x) x<y
≰⇒> : _≰_ ⇒ _>_
≰⇒> {x} {y} x≰y with compare x y
... | tri< x<y _ _ = contradiction (<⇒≤ x<y) x≰y
... | tri≈ _ x≈y _ = contradiction (≤-reflexive x≈y) x≰y
... | tri> _ _ x>y = x>y
≤⇒≯ : Irreflexive _≤_ _>_
≤⇒≯ = flip <⇒≱
≮⇒≥ : _≮_ ⇒ _≥_
≮⇒≥ {x} {y} x≮y with compare x y
... | tri< x<y _ _ = contradiction x<y x≮y
... | tri≈ _ x≈y _ = ≤-reflexive (Eq.sym x≈y)
... | tri> _ _ x>y = <⇒≤ x>y
≮∧≯⇒≈ : ∀ {x y} → x ≮ y → y ≮ x → x ≈ y
≮∧≯⇒≈ {x} {y} x≮y x≯y with compare x y
... | tri< x<y _ _ = contradiction x<y x≮y
... | tri≈ _ x≈y _ = x≈y
... | tri> _ _ x>y = contradiction x>y x≯y
|
