Add some properties of algebraic pseudocode types.

1 files changed, 65 insertions, 0 deletions

diff --git a/src/Helium/Data/Pseudocode/Algebra/Properties.agda b/src/Helium/Data/Pseudocode/Algebra/Properties.agda
new file mode 100644
index 0000000..3ea96be
--- /dev/null
+++ b/src/Helium/Data/Pseudocode/Algebra/Properties.agda
@@ -0,0 +1,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