blob: 3ea96be495bc9e3c852f9c4ee84dfc114ff1b8c6 (
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
|
------------------------------------------------------------------------
-- Agda Helium
--
-- Algebraic properties of types used by the Armv8-M pseudocode.
------------------------------------------------------------------------
{-# OPTIONS --safe --without-K #-}
open import Helium.Data.Pseudocode.Algebra
module Helium.Data.Pseudocode.Algebra.Properties
{b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
(pseudocode : Pseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃)
where
open import Agda.Builtin.FromNat
open import Agda.Builtin.FromNeg
import Helium.Algebra.Ordered.StrictTotal.Properties.CommutativeRing as CommRingₚ
open import Data.Nat using (NonZero)
private
module pseudocode = Pseudocode pseudocode
open pseudocode public
hiding
(1≉0; module ℤ; module ℤ′; module ℝ; module ℝ′; module ℤ-Reasoning; module ℝ-Reasoning)
module ℤ where
open pseudocode.ℤ public hiding (ℤ; 0ℤ; 1ℤ)
module Reasoning = pseudocode.ℤ-Reasoning
open CommRingₚ integerRing public
hiding (1≉0+n≉0⇒0<+n; 1≉0+n≉0⇒-n<0)
1≉0 : 1 ≉ 0
1≉0 = pseudocode.1≉0
n≉0⇒0<+n : ∀ n → {{NonZero n}} → 0 < fromNat n
n≉0⇒0<+n = CommRingₚ.1≉0+n≉0⇒0<+n integerRing 1≉0
n≉0⇒-n<0 : ∀ n → {{NonZero n}} → fromNeg n < 0
n≉0⇒-n<0 = CommRingₚ.1≉0+n≉0⇒-n<0 integerRing 1≉0
module ℝ where
open pseudocode.ℝ public hiding (ℝ; 0ℝ; 1ℝ)
module Reasoning = pseudocode.ℝ-Reasoning
open CommRingₚ commutativeRing public
hiding ()
1≉0 : 1 ≉ 0
1≉0 1≈0 = ℤ.1≉0 (begin-equality
1 ≈˘⟨ ⌊⌋∘/1≗id 1 ⟩
⌊ 1 /1 ⌋ ≈⟨ ⌊⌋.cong /1.1#-homo ⟩
⌊ 1 ⌋ ≈⟨ ⌊⌋.cong 1≈0 ⟩
⌊ 0 ⌋ ≈˘⟨ ⌊⌋.cong /1.0#-homo ⟩
⌊ 0 /1 ⌋ ≈⟨ ⌊⌋∘/1≗id 0 ⟩
0 ∎)
where open ℤ.Reasoning
n≉0⇒0<+n : ∀ n → {{NonZero n}} → 0 < fromNat n
n≉0⇒0<+n = CommRingₚ.1≉0+n≉0⇒0<+n commutativeRing 1≉0
n≉0⇒-n<0 : ∀ n → {{NonZero n}} → fromNeg n < 0
n≉0⇒-n<0 = CommRingₚ.1≉0+n≉0⇒-n<0 commutativeRing 1≉0
|
