From 2167866c53aa7f9cbb52e776bfb64f53acf3fa2c Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Sat, 2 Apr 2022 11:41:51 +0100
Subject: Add more properties for ordered structures.

---
 src/Helium/Semantics/Axiomatic.agda         | 11 +++--------
 src/Helium/Semantics/Axiomatic/Term.agda    |  4 ++--
 src/Helium/Semantics/Denotational/Core.agda |  6 +++---
 3 files changed, 8 insertions(+), 13 deletions(-)

(limited to 'src/Helium/Semantics')

diff --git a/src/Helium/Semantics/Axiomatic.agda b/src/Helium/Semantics/Axiomatic.agda
index dfac609..2fa3db1 100644
--- a/src/Helium/Semantics/Axiomatic.agda
+++ b/src/Helium/Semantics/Axiomatic.agda
@@ -15,11 +15,10 @@ module Helium.Semantics.Axiomatic
 
 open import Helium.Data.Pseudocode.Algebra.Properties pseudocode
 
-open import Agda.Builtin.FromNat
 open import Data.Nat using (ℕ)
-import Data.Nat.Literals as ℕₗ
 import Data.Unit
 open import Data.Vec using (Vec)
+open import Function using (_∘_)
 open import Helium.Data.Pseudocode.Core
 import Helium.Semantics.Axiomatic.Core rawPseudocode as Core
 import Helium.Semantics.Axiomatic.Assertion rawPseudocode as Assertion
@@ -36,12 +35,8 @@ open Term.Term public
 open Term public
   using (Term)
 
-instance
-  numberℕ : Number ℕ
-  numberℕ = ℕₗ.number
-
-2≉0 : 2 ℝ.≉ 0
-2≉0 = ℝ.>⇒≉ (ℝ.n≉0⇒0<+n 2)
+2≉0 : 2 ℝ.× 1ℝ ℝ.≉ 0ℝ
+2≉0 = ℝ.<⇒≉ (ℝ.n≢0∧x>0⇒n×x>0 2 (ℝ.≤∧≉⇒< ℝ.0≤1 (ℝ.1≉0 ∘ ℝ.Eq.sym))) ∘ ℝ.Eq.sym
 
 HoareTriple : ∀ {o} {Σ : Vec Type o} {n} {Γ : Vec Type n} {m} {Δ : Vec Type m} → Assertion Σ Γ Δ → Code.Statement Σ Γ → Assertion Σ Γ Δ → Set _
 HoareTriple = Triple.HoareTriple 2≉0
diff --git a/src/Helium/Semantics/Axiomatic/Term.agda b/src/Helium/Semantics/Axiomatic/Term.agda
index eaefb89..c9ddd02 100644
--- a/src/Helium/Semantics/Axiomatic/Term.agda
+++ b/src/Helium/Semantics/Axiomatic/Term.agda
@@ -32,7 +32,7 @@ import Helium.Data.Pseudocode.Manipulate as M
 open import Helium.Semantics.Axiomatic.Core rawPseudocode
 open import Level using (_⊔_; lift; lower)
 open import Relation.Binary.PropositionalEquality hiding ([_]) renaming (subst to ≡-subst)
-open import Relation.Nullary using (does; yes; no)
+open import Relation.Nullary using (¬_; does; yes; no)
 open import Relation.Nullary.Decidable.Core using (True; toWitness)
 open import Relation.Nullary.Negation using (contradiction)
 
@@ -216,7 +216,7 @@ cast τ eq = func₁ (cast′ τ eq)
 [ real ][ t ^ n ] = func₁ (lift ∘ (ℝ′._^′ n) ∘ lower) t
 
 2≉0 : Set _
-2≉0 = 2 ℝ′.×′ 1ℝ ℝ.≉ 0ℝ
+2≉0 = ¬ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ
 
 [_][_>>_] : 2≉0 → Term Σ Γ Δ int → ℕ → Term Σ Γ Δ int
 [ 2≉0 ][ t >> n ] = func₁ (lift ∘ ⌊_⌋ ∘ (ℝ._* 2≉0 ℝ.⁻¹ ℝ′.^′ n) ∘ _/1 ∘ lower) t
diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda
index 090e0ba..07c71bd 100644
--- a/src/Helium/Semantics/Denotational/Core.agda
+++ b/src/Helium/Semantics/Denotational/Core.agda
@@ -33,7 +33,7 @@ import Induction as I
 import Induction.WellFounded as Wf
 open import Level using (Level; _⊔_; 0ℓ)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning)
-open import Relation.Nullary using (does)
+open import Relation.Nullary using (does) renaming (¬_ to ¬′_)
 open import Relation.Nullary.Decidable.Core using (True; False; toWitness; fromWitness)
 
 ⟦_⟧ₗ : Type → Level
@@ -196,12 +196,12 @@ pow : ∀ {t} → IsNumeric t → ⟦ t ⟧ₜ → ℕ → ⟦ t ⟧ₜ
 pow int  x n = x ℤ′.^′ n
 pow real x n = x ℝ′.^′ n
 
-shiftr : 2 ℝ′.×′ 1ℝ ℝ.≉ 0ℝ → ⟦ int ⟧ₜ → ℕ → ⟦ int ⟧ₜ
+shiftr : ¬′ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ → ⟦ int ⟧ₜ → ℕ → ⟦ int ⟧ₜ
 shiftr 2≉0 x n = ⌊ x /1 ℝ.* 2≉0 ℝ.⁻¹ ℝ′.^′ n ⌋
 
 module Expression
   {o} {Σ : Vec Type o}
-  (2≉0 : 2 ℝ′.×′ 1ℝ ℝ.≉ 0ℝ)
+  (2≉0 : ¬′ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ)
   where
 
   open Code Σ
-- 
cgit v1.2.3