blob: 484143c4c970a35de4627dd24b5533b2d57254ee (
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
|
------------------------------------------------------------------------
-- Agda Helium
--
-- Algebraic properties of ordered rings
------------------------------------------------------------------------
{-# OPTIONS --safe --without-K #-}
open import Helium.Algebra.Ordered.StrictTotal.Bundles
module Helium.Algebra.Ordered.StrictTotal.Properties.Ring
{ℓ₁ ℓ₂ ℓ₃}
(ring : Ring ℓ₁ ℓ₂ ℓ₃)
where
open Ring ring
open import Agda.Builtin.FromNat
open import Agda.Builtin.FromNeg
open import Data.Nat using (suc; NonZero)
open import Data.Sum using (inj₁; inj₂)
open import Data.Unit.Polymorphic using (⊤)
open import Relation.Binary using (tri<; tri≈; tri>)
open import Relation.Binary.Reasoning.StrictPartialOrder strictPartialOrder
open import Algebra.Properties.Ring Unordered.ring public
renaming (-0#≈0# to -0≈0)
open import Algebra.Properties.Semiring.Mult.TCOptimised Unordered.semiring public
open import Algebra.Properties.Semiring.Exp.TCOptimised Unordered.semiring public
open import Helium.Algebra.Ordered.StrictTotal.Properties.AbelianGroup +-abelianGroup public
using (<⇒≱; ≤⇒≯; >⇒≉; ≈⇒≯; <⇒≉; ≈⇒≮; ≤∧≉⇒<; ≥∧≉⇒>)
renaming
( x<y⇒ε<yx⁻¹ to x<y⇒0<y-x
; ⁻¹-anti-mono to -‿anti-mono
)
instance
⊤′ : ∀ {ℓ} → ⊤ {ℓ = ℓ}
⊤′ = _
number : Number Carrier
number = record
{ Constraint = λ _ → ⊤
; fromNat = _× 1#
}
negative : Negative Carrier
negative = record
{ Constraint = λ _ → ⊤
; fromNeg = λ x → - (x × 1#)
}
0≤1 : 0 ≤ 1
0≤1 with compare 0 1
... | tri< 0<1 _ _ = inj₁ 0<1
... | tri≈ _ 0≈1 _ = inj₂ 0≈1
... | tri> _ _ 0>1 = inj₁ (begin-strict
0 <⟨ 0<a+0<b⇒0<ab 0<-1 0<-1 ⟩
-1 * -1 ≈˘⟨ -‿distribˡ-* 1 -1 ⟩
- (1 * -1) ≈⟨ -‿cong (*-identityˡ -1) ⟩
- -1 ≈⟨ -‿involutive 1 ⟩
1 ∎)
where
0<-1 = begin-strict
0 ≈˘⟨ -0≈0 ⟩
- 0 <⟨ -‿anti-mono 0>1 ⟩
-1 ∎
1≉0+n≉0⇒0<+n : 1 ≉ 0 → ∀ n → {{NonZero n}} → 0 < fromNat n
1≉0+n≉0⇒0<+n 1≉0 (suc 0) = ≥∧≉⇒> 0≤1 1≉0
1≉0+n≉0⇒0<+n 1≉0 (suc (suc n)) = begin-strict
0 ≈˘⟨ +-identity² ⟩
0 + 0 <⟨ +-invariantˡ 0 (≥∧≉⇒> 0≤1 1≉0) ⟩
0 + 1 <⟨ +-invariantʳ 1 (1≉0+n≉0⇒0<+n 1≉0 (suc n)) ⟩
fromNat (suc n) + 1 ∎
1≉0+n≉0⇒-n<0 : 1 ≉ 0 → ∀ n → {{NonZero n}} → fromNeg n < 0
1≉0+n≉0⇒-n<0 1≉0 n = begin-strict
- fromNat n <⟨ -‿anti-mono (1≉0+n≉0⇒0<+n 1≉0 n) ⟩
- 0 ≈⟨ -0≈0 ⟩
0 ∎
|
