diff options
Diffstat (limited to 'src/Helium/Data/Pseudocode')
| -rw-r--r-- | src/Helium/Data/Pseudocode/Algebra/Properties.agda | 13 |
1 files changed, 2 insertions, 11 deletions
diff --git a/src/Helium/Data/Pseudocode/Algebra/Properties.agda b/src/Helium/Data/Pseudocode/Algebra/Properties.agda index 3c22216..1c52cda 100644 --- a/src/Helium/Data/Pseudocode/Algebra/Properties.agda +++ b/src/Helium/Data/Pseudocode/Algebra/Properties.agda @@ -22,6 +22,7 @@ open import Data.Sum using (_⊎_; inj₁; inj₂; map) import Data.Unit open import Function using (_∘_) import Helium.Algebra.Ordered.StrictTotal.Properties.CommutativeRing as CommRingₚ +import Helium.Algebra.Ordered.StrictTotal.Properties.Field as Fieldₚ open import Level using (_⊔_) open import Relation.Binary.Core using (_Preserves_⟶_) open import Relation.Binary.Definitions using (tri<; tri≈; tri>) @@ -77,7 +78,7 @@ module ℝ where ) module Reasoning = pseudocode.ℝ-Reasoning - open CommRingₚ commutativeRing public + open Fieldₚ realField public hiding () 1≉0 : 1ℝ ≉ 0ℝ @@ -92,16 +93,6 @@ module ℝ where open ℤ.Reasoning open pseudocode using (module /1; module ⌊⌋) - x>0⇒x⁻¹>0 : ∀ {x} → (x≉0 : x ≉ 0ℝ) → x > 0ℝ → x≉0 ⁻¹ > 0ℝ - x>0⇒x⁻¹>0 {x} x≉0 x>0 = ≰⇒> (λ x⁻¹≤0 → <⇒≱ x>0 (begin - x ≈˘⟨ *-identityˡ x ⟩ - 1ℝ * x ≈˘⟨ *-congʳ (⁻¹-inverseˡ x≉0) ⟩ - x≉0 ⁻¹ * x * x ≤⟨ x≥0⇒*-monoʳ-≤ (<⇒≤ x>0) (x≤0⇒*-anti-monoˡ-≤ x⁻¹≤0 (<⇒≤ x>0)) ⟩ - x≉0 ⁻¹ * 0ℝ * x ≈⟨ *-congʳ (zeroʳ (x≉0 ⁻¹)) ⟩ - 0ℝ * x ≈⟨ zeroˡ x ⟩ - 0ℝ ∎)) - where open Reasoning - record IsMonotoneContinuous (f : ℝ → ℝ) : Set (r₁ ⊔ r₂ ⊔ r₃) where field cong : f Preserves _≈_ ⟶ _≈_ |