blob: eb46e276a61a3ab2db663a385fb8ddd0781fb3b3 (
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
138
139
140
|
------------------------------------------------------------------------
-- Agda Helium
--
-- Algebraic properties of ordered fields
------------------------------------------------------------------------
{-# OPTIONS --without-K --safe #-}
open import Helium.Algebra.Ordered.StrictTotal.Bundles
module Helium.Algebra.Ordered.StrictTotal.Properties.Field
{ℓ₁ ℓ₂ ℓ₃}
(field′ : Field ℓ₁ ℓ₂ ℓ₃)
where
open Field field′
renaming
( trans to <-trans
; irrefl to <-irrefl
; asym to <-asym
; 0<a+0<b⇒0<ab to x>0∧y>0⇒x*y>0
)
open import Function using (_∘_)
open import Relation.Binary.Reasoning.StrictPartialOrder strictPartialOrder
open import Algebra.Properties.Ring Unordered.ring public
renaming (-0#≈0# to -0≈0)
open import Helium.Algebra.Properties.AlmostGroup *-almostGroup public
renaming
( x≉0⇒∙-cancelˡ to x≉0⇒*-cancelˡ
; x≉0⇒∙-cancelʳ to x≉0⇒*-cancelʳ
; ⁻¹-anti-homo-∙ to ⁻¹-anti-homo-*
; identityˡ-unique to *-identityˡ-unique
; identityʳ-unique to *-identityʳ-unique
; inverseˡ-unique to *-inverseˡ-unique
; inverseʳ-unique to *-inverseʳ-unique
)
open import Algebra.Properties.Semiring.Mult.TCOptimised Unordered.semiring public
open import Algebra.Properties.CommutativeSemiring.Exp.TCOptimised Unordered.commutativeSemiring public
open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder public
open import Helium.Algebra.Ordered.StrictTotal.Properties.DivisionRing divisionRing public
using
( +-mono-<; +-monoˡ-<; +-monoʳ-<
; +-mono-≤; +-monoˡ-≤; +-monoʳ-≤
; +-cancel-<; +-cancelˡ-<; +-cancelʳ-<
; +-cancel-≤; +-cancelˡ-≤; +-cancelʳ-≤
; x≥0∧y>0⇒x+y>0 ; x>0∧y≥0⇒x+y>0
; x≤0∧y<0⇒x+y<0 ; x<0∧y≤0⇒x+y<0
; x≥0∧y≥0⇒x+y≥0 ; x≤0∧y≤0⇒x+y≤0
; x≤0∧x+y>0⇒y>0 ; x≤0∧y+x>0⇒y>0 ; x<0∧x+y≥0⇒y>0 ; x<0∧y+x≥0⇒y>0
; x≥0∧x+y<0⇒y<0 ; x≥0∧y+x<0⇒y<0 ; x>0∧x+y≤0⇒y<0 ; x>0∧y+x≤0⇒y<0
; x≤0∧x+y≥0⇒y≥0 ; x≤0∧y+x≥0⇒y≥0
; x≥0∧x+y≤0⇒y≤0 ; x≥0∧y+x≤0⇒y≤0
; ×-zeroˡ; ×-zeroʳ
; ×-identityˡ
; n≢0⇒×-monoˡ-< ; x>0⇒×-monoʳ-< ; x<0⇒×-anti-monoʳ-<
; ×-monoˡ-≤; x≥0⇒×-monoʳ-≤; x≤0⇒×-anti-monoʳ-≤
; ×-cancelˡ-<; x≥0⇒×-cancelʳ-<; x≤0⇒×-anti-cancelʳ-<
; n≢0⇒×-cancelˡ-≤ ; x>0⇒×-cancelʳ-≤ ; x<0⇒×-anti-cancelʳ-≤
; n≢0∧x>0⇒n×x>0; n≢0∧x<0⇒n×x<0
; x≥0⇒n×x≥0; x≤0⇒n×x≤0
; n×x>0⇒x>0; n×x<0⇒x<0
; n≢0∧n×x≥0⇒x≥0; n≢0∧n×x≤0⇒x≤0
; -‿anti-mono-<; -‿anti-mono-≤
; -‿anti-cancel-<; -‿anti-cancel-≤
; x≈0⇒-x≈0 ; x<0⇒-x>0; x>0⇒-x<0; x≤0⇒-x≥0; x≥0⇒-x≤0
; -x≈0⇒x≈0 ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0
; x<y⇒0<y-x; 0<y-x⇒x<y
; x≤y⇒0≤y-x; 0≤y-x⇒x≤y
; x<y+z⇒x-z<y
; 0≤1; 1≈0⇒x≈y; x≉y⇒0<1; x<y⇒0<1
; x>0⇒*-monoˡ-<; x>0⇒*-monoʳ-<; x<0⇒*-anti-monoˡ-<; x<0⇒*-anti-monoʳ-<
; x≥0⇒*-monoˡ-≤; x≥0⇒*-monoʳ-≤; x≤0⇒*-anti-monoˡ-≤; x≤0⇒*-anti-monoʳ-≤
; x≥0⇒*-cancelˡ-<; x≥0⇒*-cancelʳ-<; x≤0⇒*-anti-cancelˡ-<; x≤0⇒*-anti-cancelʳ-<
; x>0⇒*-cancelˡ-≤; x>0⇒*-cancelʳ-≤; x<0⇒*-anti-cancelˡ-≤; x<0⇒*-anti-cancelʳ-≤
; x≈0⇒x*y≈0; x≈0⇒y*x≈0
; -x*-y≈x*y
; x>0∧y<0⇒x*y<0; x<0∧y>0⇒x*y<0; x<0∧y<0⇒x*y>0
; x≥0∧y≥0⇒x*y≥0; x≥0∧y≤0⇒x*y≤0; x≤0∧y≥0⇒x*y≤0; x≤0∧y≤0⇒x*y≥0
; x>1∧y≥1⇒x*y>1; x≥1∧y>1⇒x*y>1; 0≤x<1∧y≤1⇒x*y<1; x≤1∧0≤y<1⇒x*y<1
; x≥1∧y≥1⇒x*y≥1; 0≤x≤1∧y≤1⇒x*y≤1; x≤1∧0≤y≤1⇒x*y≤1
; x*x≥0; x*y≈0⇒x≈0⊎y≈0
; ^-zeroˡ; ^-zeroʳ
; ^-identityʳ
; n≢0⇒0^n≈0
; x>1⇒^-monoˡ-<; 0<x<1⇒^-anti-monoˡ-<
; x≥1⇒^-monoˡ-≤; 0≤x≤1⇒^-anti-monoˡ-≤
; x>0⇒x^n>0
; x≥0⇒x^n≥0
; x^n≈0⇒x≈0
; x>1∧n≢0⇒x^n>1; 0≤x<1∧n≢0⇒x^n<1
; x≥1⇒x^n≥1; 0≤x≤1⇒x^n≤1
; x>0⇒x⁻¹>0 ; x<0⇒x⁻¹<0
; x⁻¹>0⇒x>0 ; x⁻¹<0⇒x<0
; x>1⇒x⁻¹<1; 0<x<1⇒x⁻¹>1
; x⁻¹>1⇒x<1; 0<x⁻¹<1⇒x>1
; -‿⁻¹-comm
; x≉0⇒x⁻¹≉0
; y>0∧x<y⇒x*y⁻¹<1; y>0∧x≤y⇒x*y⁻¹≤1
)
--------------------------------------------------------------------------------
---- Properties of _⁻¹ and _^_
⁻¹-^-comm : ∀ {x} (x≉0 : x ≉ 0#) k → x≉0 ⁻¹ ^ k ≈ (x≉0 ∘ x^n≈0⇒x≈0 x k) ⁻¹
⁻¹-^-comm {x} x≉0 k = *-inverseˡ-unique (x≉0 ∘ x^n≈0⇒x≈0 x k) (begin-equality
x≉0 ⁻¹ ^ k * x ^ k ≈˘⟨ ^-distrib-* _ x k ⟩
(x≉0 ⁻¹ * x) ^ k ≈⟨ ^-congˡ k (⁻¹-inverseˡ x≉0) ⟩
1# ^ k ≈⟨ ^-zeroˡ k ⟩
1# ∎)
|
