blob: 7696f98d944cbb35663123ef4b96440268ba1af0 (
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
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
|
------------------------------------------------------------------------
-- Agda Helium
--
-- Relations between algebraic properties of ordered structures
------------------------------------------------------------------------
{-# OPTIONS --safe --without-K #-}
open import Relation.Binary
module Helium.Algebra.Ordered.StrictTotal.Consequences
{a ℓ₁ ℓ₂}
(strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
where
open StrictTotalOrder strictTotalOrder
renaming
( Carrier to A
; trans to <-trans
; irrefl to <-irrefl
; asym to <-asym
)
open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder
open import Relation.Binary.Reasoning.StrictPartialOrder strictPartialOrder
open import Algebra.Core
open import Algebra.Definitions
open import Data.Product using (_,_)
open import Data.Sum using (inj₁; inj₂)
open import Function using (_∘_)
open import Function.Definitions
open import Helium.Algebra.Ordered.Definitions
open import Relation.Nullary using (¬_)
----
-- Consequences for a single unary operation
module _ {f : Op₁ A} where
cong₁+mono₁-<⇒mono₁-≤ : Congruent₁ _≈_ f → Congruent₁ _<_ f → Congruent₁ _≤_ f
cong₁+mono₁-<⇒mono₁-≤ cong mono (inj₁ x<y) = inj₁ (mono x<y)
cong₁+mono₁-<⇒mono₁-≤ cong mono (inj₂ x≈y) = inj₂ (cong x≈y)
cong₁+anti-mono₁-<⇒anti-mono₁-≤ : Congruent₁ _≈_ f → f Preserves _<_ ⟶ _>_ → f Preserves _≤_ ⟶ _≥_
cong₁+anti-mono₁-<⇒anti-mono₁-≤ cong anti-mono (inj₁ x<y) = inj₁ (anti-mono x<y)
cong₁+anti-mono₁-<⇒anti-mono₁-≤ cong anti-mono (inj₂ x≈y) = inj₂ (cong (Eq.sym x≈y))
mono₁-<⇒cancel₁-≤ : Congruent₁ _<_ f → Injective _≤_ _≤_ f
mono₁-<⇒cancel₁-≤ mono fx≤fy = ≮⇒≥ (≤⇒≯ fx≤fy ∘ mono)
mono₁-≤⇒cancel₁-< : Congruent₁ _≤_ f → Injective _<_ _<_ f
mono₁-≤⇒cancel₁-< mono fx<fy = ≰⇒> (<⇒≱ fx<fy ∘ mono)
cancel₁-<⇒mono₁-≤ : Injective _<_ _<_ f → Congruent₁ _≤_ f
cancel₁-<⇒mono₁-≤ cancel x≤y = ≮⇒≥ (≤⇒≯ x≤y ∘ cancel)
cancel₁-≤⇒mono₁-< : Injective _≤_ _≤_ f → Congruent₁ _<_ f
cancel₁-≤⇒mono₁-< cancel x<y = ≰⇒> (<⇒≱ x<y ∘ cancel)
anti-mono₁-<⇒anti-cancel₁-≤ : f Preserves _<_ ⟶ _>_ → Injective _≤_ _≥_ f
anti-mono₁-<⇒anti-cancel₁-≤ anti-mono fx≥fy = ≮⇒≥ (≤⇒≯ fx≥fy ∘ anti-mono)
anti-mono₁-≤⇒anti-cancel₁-< : f Preserves _≤_ ⟶ _≥_ → Injective _<_ _>_ f
anti-mono₁-≤⇒anti-cancel₁-< anti-mono fx>fy = ≰⇒> (<⇒≱ fx>fy ∘ anti-mono)
mono₁-<⇒cancel₁ : Congruent₁ _<_ f → Injective _≈_ _≈_ f
mono₁-<⇒cancel₁ mono fx≈fy = ≮∧≯⇒≈ (<-irrefl fx≈fy ∘ mono) (<-irrefl (Eq.sym fx≈fy) ∘ mono)
anti-mono₁-<⇒cancel₁ : f Preserves _<_ ⟶ _>_ → Injective _≈_ _≈_ f
anti-mono₁-<⇒cancel₁ anti-mono fx≈fy = ≮∧≯⇒≈
(<-irrefl (Eq.sym fx≈fy) ∘ anti-mono)
(<-irrefl fx≈fy ∘ anti-mono)
----
-- Consequences for a single binary operation
module _ {_∙_ : Op₂ A} where
invariant⇒mono-< : Invariant _<_ _∙_ → Congruent₂ _<_ _∙_
invariant⇒mono-< (invˡ , invʳ) {x} {y} {u} {v} x<y u<v = begin-strict
x ∙ u <⟨ invˡ x u<v ⟩
x ∙ v <⟨ invʳ v x<y ⟩
y ∙ v ∎
invariantˡ⇒monoˡ-< : LeftInvariant _<_ _∙_ → LeftCongruent _<_ _∙_
invariantˡ⇒monoˡ-< invˡ u<v = invˡ _ u<v
invariantʳ⇒monoʳ-< : RightInvariant _<_ _∙_ → RightCongruent _<_ _∙_
invariantʳ⇒monoʳ-< invʳ x<y = invʳ _ x<y
cong+invariant⇒mono-≤ : Congruent₂ _≈_ _∙_ → Invariant _<_ _∙_ → Congruent₂ _≤_ _∙_
cong+invariant⇒mono-≤ cong inv@(invˡ , invʳ) (inj₁ x<y) (inj₁ u<v) = inj₁ (invariant⇒mono-< inv x<y u<v)
cong+invariant⇒mono-≤ cong inv@(invˡ , invʳ) (inj₁ x<y) (inj₂ u≈v) = inj₁ (<-respʳ-≈ (cong Eq.refl u≈v) (invʳ _ x<y))
cong+invariant⇒mono-≤ cong inv@(invˡ , invʳ) (inj₂ x≈y) (inj₁ u<v) = inj₁ (<-respʳ-≈ (cong x≈y Eq.refl) (invˡ _ u<v))
cong+invariant⇒mono-≤ cong inv@(invˡ , invʳ) (inj₂ x≈y) (inj₂ u≤v) = inj₂ (cong x≈y u≤v)
congˡ+monoˡ-<⇒monoˡ-≤ : LeftCongruent _≈_ _∙_ → LeftCongruent _<_ _∙_ → LeftCongruent _≤_ _∙_
congˡ+monoˡ-<⇒monoˡ-≤ congˡ monoˡ = cong₁+mono₁-<⇒mono₁-≤ congˡ monoˡ
congʳ+monoʳ-<⇒monoʳ-≤ : RightCongruent _≈_ _∙_ → RightCongruent _<_ _∙_ → RightCongruent _≤_ _∙_
congʳ+monoʳ-<⇒monoʳ-≤ congʳ monoʳ = cong₁+mono₁-<⇒mono₁-≤ congʳ monoʳ
monoˡ-<⇒cancelˡ-≤ : LeftCongruent _<_ _∙_ → LeftCancellative _≤_ _∙_
monoˡ-<⇒cancelˡ-≤ monoˡ _ = mono₁-<⇒cancel₁-≤ monoˡ
monoʳ-<⇒cancelʳ-≤ : RightCongruent _<_ _∙_ → RightCancellative _≤_ _∙_
monoʳ-<⇒cancelʳ-≤ monoʳ _ _ = mono₁-<⇒cancel₁-≤ monoʳ
monoˡ-≤⇒cancelˡ-< : LeftCongruent _≤_ _∙_ → LeftCancellative _<_ _∙_
monoˡ-≤⇒cancelˡ-< monoˡ _ = mono₁-≤⇒cancel₁-< monoˡ
monoʳ-≤⇒cancelʳ-< : RightCongruent _≤_ _∙_ → RightCancellative _<_ _∙_
monoʳ-≤⇒cancelʳ-< monoʳ _ _ = mono₁-≤⇒cancel₁-< monoʳ
cancelˡ-<⇒monoˡ-≤ : LeftCancellative _<_ _∙_ → LeftCongruent _≤_ _∙_
cancelˡ-<⇒monoˡ-≤ cancelˡ = cancel₁-<⇒mono₁-≤ (cancelˡ _)
cancelʳ-<⇒monoʳ-≤ : RightCancellative _<_ _∙_ → RightCongruent _≤_ _∙_
cancelʳ-<⇒monoʳ-≤ cancelʳ = cancel₁-<⇒mono₁-≤ (cancelʳ _ _)
cancelˡ-≤⇒monoˡ-< : LeftCancellative _≤_ _∙_ → LeftCongruent _<_ _∙_
cancelˡ-≤⇒monoˡ-< cancelˡ = cancel₁-≤⇒mono₁-< (cancelˡ _)
cancelʳ-≤⇒monoʳ-< : RightCancellative _≤_ _∙_ → RightCongruent _<_ _∙_
cancelʳ-≤⇒monoʳ-< cancelʳ = cancel₁-≤⇒mono₁-< (cancelʳ _ _)
monoˡ-<⇒cancelˡ : LeftCongruent _<_ _∙_ → LeftCancellative _≈_ _∙_
monoˡ-<⇒cancelˡ monoˡ _ = mono₁-<⇒cancel₁ monoˡ
monoʳ-<⇒cancelʳ : RightCongruent _<_ _∙_ → RightCancellative _≈_ _∙_
monoʳ-<⇒cancelʳ monoʳ _ _ = mono₁-<⇒cancel₁ monoʳ
¬comm-< : A → ¬ Commutative _<_ _∙_
¬comm-< a comm = <-irrefl Eq.refl (comm a a )
-- cong+mono-<⇒mono-≤ : Congruent₂ _≈_ _∙_ → Congruent₂ _<_ _∙_ → Congruent₂ _≤_ _∙_
-- cong+mono-<⇒mono-≤ cong mono (inj₁ x<y) (inj₁ u<v) = inj₁ (mono x<y u<v)
-- cong+mono-<⇒mono-≤ cong mono (inj₁ x<y) (inj₂ u≈v) = inj₁ {!!}
-- cong+mono-<⇒mono-≤ cong mono (inj₂ x≈y) (inj₁ u<v) = inj₁ {!!}
-- cong+mono-<⇒mono-≤ cong mono (inj₂ x≈y) (inj₂ u≈v) = inj₂ (cong x≈y u≈v)
|
