blob: c0723b3f4923152527ec136462cee9d35e90a2d7 (
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
|
------------------------------------------------------------------------
-- Agda Helium
--
-- Algebraic properties of ordered groups
------------------------------------------------------------------------
{-# OPTIONS --safe --without-K #-}
open import Helium.Algebra.Ordered.StrictTotal.Bundles
module Helium.Algebra.Ordered.StrictTotal.Properties.Group
{ℓ₁ ℓ₂ ℓ₃}
(group : Group ℓ₁ ℓ₂ ℓ₃)
where
open Group group
open import Data.Sum using (inj₂; [_,_]′; fromInj₁)
open import Function using (_∘_; flip)
open import Relation.Binary using (tri<; tri≈; tri>)
open import Relation.Binary.Reasoning.StrictPartialOrder strictPartialOrder
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (contradiction)
open import Algebra.Properties.Group Unordered.group public
open import Algebra.Properties.Monoid.Mult.TCOptimised Unordered.monoid public
<⇒≱ : ∀ {x y} → x < y → ¬ x ≥ y
<⇒≱ {x} {y} x<y x≥y with compare x y
... | tri< _ x≉y x≱y = [ x≱y , x≉y ∘ Eq.sym ]′ x≥y
... | tri≈ x≮y _ _ = x≮y x<y
... | tri> x≮y _ _ = x≮y x<y
≤⇒≯ : ∀ {x y} → x ≤ y → ¬ x > y
≤⇒≯ = flip <⇒≱
>⇒≉ : ∀ {x y} → x > y → x ≉ y
>⇒≉ x>y = <⇒≱ x>y ∘ inj₂
≈⇒≯ : ∀ {x y} → x ≈ y → ¬ x > y
≈⇒≯ = flip >⇒≉
<⇒≉ : ∀ {x y} → x < y → x ≉ y
<⇒≉ x<y = >⇒≉ x<y ∘ Eq.sym
≈⇒≮ : ∀ {x y} → x ≈ y → ¬ x < y
≈⇒≮ = flip <⇒≉
≤∧≉⇒< : ∀ {x y} → x ≤ y → x ≉ y → x < y
≤∧≉⇒< x≤y x≉y = fromInj₁ (λ x≈y → contradiction x≈y x≉y) x≤y
≥∧≉⇒> : ∀ {x y} → x ≥ y → x ≉ y → x > y
≥∧≉⇒> x≥y x≉y = ≤∧≉⇒< x≥y (x≉y ∘ Eq.sym)
x<y⇒ε<yx⁻¹ : ∀ {x y} → x < y → ε < y ∙ x ⁻¹
x<y⇒ε<yx⁻¹ {x} {y} x<y = begin-strict
ε ≈˘⟨ inverseʳ x ⟩
x ∙ x ⁻¹ <⟨ ∙-invariantʳ (x ⁻¹) x<y ⟩
y ∙ x ⁻¹ ∎
|
