From 91bc16d54ec0a6e5d904673951fe091a9973d9b4 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Tue, 18 Jan 2022 22:01:46 +0000 Subject: Define the semantics of pseudocode data types. --- src/Helium/Data/Pseudocode.agda | 398 +++++++++++++++++++++++++++++++--------- 1 file changed, 312 insertions(+), 86 deletions(-) (limited to 'src/Helium/Data') diff --git a/src/Helium/Data/Pseudocode.agda b/src/Helium/Data/Pseudocode.agda index 146dbf9..d75ddba 100644 --- a/src/Helium/Data/Pseudocode.agda +++ b/src/Helium/Data/Pseudocode.agda @@ -8,112 +8,80 @@ module Helium.Data.Pseudocode where -open import Algebra.Bundles using (RawRing) open import Algebra.Core import Algebra.Definitions.RawSemiring as RS open import Data.Bool.Base using (Bool; if_then_else_) +open import Data.Empty using (⊥-elim) open import Data.Fin.Base as Fin hiding (cast) import Data.Fin.Properties as Fₚ import Data.Fin.Induction as Induction open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′) open import Data.Vec.Functional open import Data.Vec.Functional.Relation.Binary.Pointwise using (Pointwise) import Data.Vec.Functional.Relation.Binary.Pointwise.Properties as Pwₚ open import Function using (_$_; _∘′_; id) -open import Helium.Algebra.Bundles using (RawField; RawBooleanAlgebra) +open import Helium.Algebra.Ordered.StrictTotal.Bundles +open import Helium.Algebra.Decidable.Bundles + using (BooleanAlgebra; RawBooleanAlgebra) +import Helium.Algebra.Decidable.Construct.Pointwise as Pw +open import Helium.Algebra.Morphism.Structures open import Level using (_⊔_) renaming (suc to ℓsuc) open import Relation.Binary.Core using (Rel) -open import Relation.Binary.Definitions using (Decidable) +open import Relation.Binary.Definitions open import Relation.Binary.PropositionalEquality as P using (_≡_) -open import Relation.Nullary using (does) -open import Relation.Nullary.Decidable.Core using (False; toWitnessFalse) +import Relation.Binary.Reasoning.StrictPartialOrder as Reasoning +open import Relation.Binary.Structures using (IsStrictTotalOrder) +open import Relation.Nullary using (does; yes; no) +open import Relation.Nullary.Decidable.Core + using (False; toWitnessFalse; fromWitnessFalse) record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁ ⊔ b₂ ⊔ i₁ ⊔ i₂ ⊔ i₃ ⊔ r₁ ⊔ r₂ ⊔ r₃)) where - infix 6 _-ᶻ_ - infix 4 _≟ᵇ_ _≟ᶻ_ _<ᶻ_ _<ᶻ?_ _≟ʳ_ _<ʳ_ _<ʳ?_ - field bitRawBooleanAlgebra : RawBooleanAlgebra b₁ b₂ - integerRawRing : RawRing i₁ i₂ - realRawField : RawField r₁ r₂ - - open RawBooleanAlgebra bitRawBooleanAlgebra public - using () - renaming (Carrier to Bit; _≈_ to _≈ᵇ₁_; _≉_ to _≉ᵇ₁_; ⊤ to 1𝔹; ⊥ to 0𝔹) - - module bitsRawBooleanAlgebra {n} = RawBooleanAlgebra record - { _≈_ = Pointwise (RawBooleanAlgebra._≈_ bitRawBooleanAlgebra) {n} - ; _∨_ = zipWith (RawBooleanAlgebra._∨_ bitRawBooleanAlgebra) - ; _∧_ = zipWith (RawBooleanAlgebra._∧_ bitRawBooleanAlgebra) - ; ¬_ = map (RawBooleanAlgebra.¬_ bitRawBooleanAlgebra) - ; ⊤ = replicate (RawBooleanAlgebra.⊤ bitRawBooleanAlgebra) - ; ⊥ = replicate (RawBooleanAlgebra.⊥ bitRawBooleanAlgebra) - } - - open bitsRawBooleanAlgebra public - hiding (Carrier) - renaming (_≈_ to _≈ᵇ_; _≉_ to _≉ᵇ_; ⊤ to ones; ⊥ to zeros) - - Bits = λ n → bitsRawBooleanAlgebra.Carrier {n} - - open RawRing integerRawRing public - renaming - ( Carrier to ℤ; _≈_ to _≈ᶻ_; _≉_ to _≉ᶻ_ - ; _+_ to _+ᶻ_; _*_ to _*ᶻ_; -_ to -ᶻ_; 0# to 0ℤ; 1# to 1ℤ - ; rawSemiring to integerRawSemiring - ; +-rawMagma to +ᶻ-rawMagma; +-rawMonoid to +ᶻ-rawMonoid - ; *-rawMagma to *ᶻ-rawMagma; *-rawMonoid to *ᶻ-rawMonoid - ; +-rawGroup to +ᶻ-rawGroup - ) - - _-ᶻ_ : Op₂ ℤ - x -ᶻ y = x +ᶻ -ᶻ y - - open RS integerRawSemiring public using () - renaming - ( _×_ to _×ᶻ_; _×′_ to _×′ᶻ_; sum to sumᶻ - ; _^_ to _^ᶻ_; _^′_ to _^′ᶻ_; product to productᶻ - ) - - open RawField realRawField public - renaming - ( Carrier to ℝ; _≈_ to _≈ʳ_; _≉_ to _≉ʳ_ - ; _+_ to _+ʳ_; _*_ to _*ʳ_; -_ to -ʳ_; 0# to 0ℝ; 1# to 1ℝ; _-_ to _-ʳ_ - ; rawSemiring to realRawSemiring; rawRing to realRawRing - ; +-rawMagma to +ʳ-rawMagma; +-rawMonoid to +ʳ-rawMonoid - ; *-rawMagma to *ʳ-rawMagma; *-rawMonoid to *ʳ-rawMonoid - ; +-rawGroup to +ʳ-rawGroup; *-rawAlmostGroup to *ʳ-rawAlmostGroup - ) - - open RS realRawSemiring public using () - renaming - ( _×_ to _×ʳ_; _×′_ to _×′ʳ_; sum to sumʳ - ; _^_ to _^ʳ_; _^′_ to _^′ʳ_; product to productʳ - ) - + integerRawRing : RawRing i₁ i₂ i₃ + realRawField : RawField r₁ r₂ r₃ + + bitsRawBooleanAlgebra : ℕ → RawBooleanAlgebra b₁ b₂ + bitsRawBooleanAlgebra = Pw.rawBooleanAlgebra bitRawBooleanAlgebra + + module 𝔹 = RawBooleanAlgebra bitRawBooleanAlgebra + renaming (Carrier to Bit; ⊤ to 1𝔹; ⊥ to 0𝔹) + module Bits {n} = RawBooleanAlgebra (bitsRawBooleanAlgebra n) + renaming (⊤ to ones; ⊥ to zeros) + module ℤ = RawRing integerRawRing renaming (Carrier to ℤ; 1# to 1ℤ; 0# to 0ℤ) + module ℝ = RawField realRawField renaming (Carrier to ℝ; 1# to 1ℝ; 0# to 0ℝ) + module ℤ′ = RS ℤ.Unordered.rawSemiring + module ℝ′ = RS ℝ.Unordered.rawSemiring + + Bits : ℕ → Set b₁ + Bits n = Bits.Carrier {n} + + open 𝔹 public using (Bit; 1𝔹; 0𝔹) + open Bits public using (ones; zeros) + open ℤ public using (ℤ; 1ℤ; 0ℤ) + open ℝ public using (ℝ; 1ℝ; 0ℝ) + + infix 4 _≟ᶻ_ _<ᶻ?_ _≟ʳ_ _<ʳ?_ _≟ᵇ₁_ _≟ᵇ_ field - _≟ᶻ_ : Decidable _≈ᶻ_ - _<ᶻ_ : Rel ℤ i₃ - _<ᶻ?_ : Decidable _<ᶻ_ - - _≟ʳ_ : Decidable _≈ʳ_ - _<ʳ_ : Rel ℝ r₃ - _<ʳ?_ : Decidable _<ʳ_ + _≟ᶻ_ : Decidable ℤ._≈_ + _<ᶻ?_ : Decidable ℤ._<_ + _≟ʳ_ : Decidable ℝ._≈_ + _<ʳ?_ : Decidable ℝ._<_ + _≟ᵇ₁_ : Decidable 𝔹._≈_ - _≟ᵇ₁_ : Decidable _≈ᵇ₁_ - - _≟ᵇ_ : ∀ {n} → Decidable (_≈ᵇ_ {n}) + _≟ᵇ_ : ∀ {n} → Decidable (Bits._≈_ {n}) _≟ᵇ_ = Pwₚ.decidable _≟ᵇ₁_ field - float : ℤ → ℝ - round : ℝ → ℤ + _/1 : ℤ → ℝ + ⌊_⌋ : ℝ → ℤ cast : ∀ {m n} → .(eq : m ≡ n) → Bits m → Bits n cast eq x i = x $ Fin.cast (P.sym eq) i 2ℤ : ℤ - 2ℤ = 2 ×′ᶻ 1ℤ + 2ℤ = 2 ℤ′.×′ 1ℤ getᵇ : ∀ {n} → Fin n → Bits n → Bit getᵇ i x = x (opposite i) @@ -148,18 +116,18 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁ infixl 7 _div_ _mod_ - _div_ : ∀ (x y : ℤ) → {y≉0 : False (float y ≟ʳ 0ℝ)} → ℤ - (x div y) {y≉0} = round (float x *ʳ toWitnessFalse y≉0 ⁻¹) + _div_ : ∀ (x y : ℤ) → {y≉0 : False (y /1 ≟ʳ 0ℝ)} → ℤ + (x div y) {y≉0} = ⌊ x /1 ℝ.* toWitnessFalse y≉0 ℝ.⁻¹ ⌋ - _mod_ : ∀ (x y : ℤ) → {y≉0 : False (float y ≟ʳ 0ℝ)} → ℤ - (x mod y) {y≉0} = x -ᶻ y *ᶻ (x div y) {y≉0} + _mod_ : ∀ (x y : ℤ) → {y≉0 : False (y /1 ≟ʳ 0ℝ)} → ℤ + (x mod y) {y≉0} = x ℤ.+ ℤ.- y ℤ.* (x div y) {y≉0} infixl 5 _<<_ _<<_ : ℤ → ℕ → ℤ - x << n = x *ᶻ 2ℤ ^′ᶻ n + x << n = 2ℤ ℤ′.^′ n ℤ.* x module ShiftNotZero - (1<>_ @@ -179,8 +147,266 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁ sliceᶻ (suc n) (suc i) x = sliceᶻ n i (x >> 1) uint : ∀ {n} → Bits n → ℤ - uint x = sumᶻ λ i → if hasBit i x then 1ℤ << toℕ i else 0ℤ + uint x = ℤ′.sum λ i → if hasBit i x then 1ℤ << toℕ i else 0ℤ sint : ∀ {n} → Bits n → ℤ sint {zero} x = 0ℤ - sint {suc n} x = uint x -ᶻ (if hasBit (fromℕ n) x then 1ℤ << suc n else 0ℤ) + sint {suc n} x = uint x ℤ.+ ℤ.- (if hasBit (fromℕ n) x then 1ℤ << suc n else 0ℤ) + +record Pseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : + Set (ℓsuc (b₁ ⊔ b₂ ⊔ i₁ ⊔ i₂ ⊔ i₃ ⊔ r₁ ⊔ r₂ ⊔ r₃)) where + field + bitBooleanAlgebra : BooleanAlgebra b₁ b₂ + integerRing : CommutativeRing i₁ i₂ i₃ + realField : Field r₁ r₂ r₃ + + bitsBooleanAlgebra : ℕ → BooleanAlgebra b₁ b₂ + bitsBooleanAlgebra = Pw.booleanAlgebra bitBooleanAlgebra + + module 𝔹 = BooleanAlgebra bitBooleanAlgebra + renaming (Carrier to Bit; ⊤ to 1𝔹; ⊥ to 0𝔹) + module Bits {n} = BooleanAlgebra (bitsBooleanAlgebra n) + renaming (⊤ to ones; ⊥ to zeros) + module ℤ = CommutativeRing integerRing + renaming (Carrier to ℤ; 1# to 1ℤ; 0# to 0ℤ) + module ℝ = Field realField + renaming (Carrier to ℝ; 1# to 1ℝ; 0# to 0ℝ) + + Bits : ℕ → Set b₁ + Bits n = Bits.Carrier {n} + + open 𝔹 public using (Bit; 1𝔹; 0𝔹) + open Bits public using (ones; zeros) + open ℤ public using (ℤ; 1ℤ; 0ℤ) + open ℝ public using (ℝ; 1ℝ; 0ℝ) + + module ℤ-Reasoning = Reasoning ℤ.strictPartialOrder + module ℝ-Reasoning = Reasoning ℝ.strictPartialOrder + + field + integerDiscrete : ∀ x y → y ℤ.≤ x ⊎ x ℤ.+ 1ℤ ℤ.≤ y + 1≉0 : 1ℤ ℤ.≉ 0ℤ + + _/1 : ℤ → ℝ + ⌊_⌋ : ℝ → ℤ + /1-isHomo : IsRingHomomorphism ℤ.Unordered.rawRing ℝ.Unordered.rawRing _/1 + ⌊⌋-isHomo : IsRingHomomorphism ℝ.Unordered.rawRing ℤ.Unordered.rawRing ⌊_⌋ + /1-mono : ∀ x y → x ℤ.< y → x /1 ℝ.< y /1 + ⌊⌋-floor : ∀ x y → x ℤ.≤ ⌊ y ⌋ → ⌊ y ⌋ ℤ.< x ℤ.+ 1ℤ + ⌊⌋∘/1≗id : ∀ x → ⌊ x /1 ⌋ ℤ.≈ x + + module /1 = IsRingHomomorphism /1-isHomo renaming (⟦⟧-cong to cong) + module ⌊⌋ = IsRingHomomorphism ⌊⌋-isHomo renaming (⟦⟧-cong to cong) + + bitRawBooleanAlgebra : RawBooleanAlgebra b₁ b₂ + bitRawBooleanAlgebra = record + { _≈_ = _≈_ + ; _∨_ = _∨_ + ; _∧_ = _∧_ + ; ¬_ = ¬_ + ; ⊤ = ⊤ + ; ⊥ = ⊥ + } + where open BooleanAlgebra bitBooleanAlgebra + + rawPseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ + rawPseudocode = record + { bitRawBooleanAlgebra = bitRawBooleanAlgebra + ; integerRawRing = ℤ.rawRing + ; realRawField = ℝ.rawField + ; _≟ᶻ_ = ℤ._≟_ + ; _<ᶻ?_ = ℤ._-a : ∀ {a} → 0ℤ ℤ.< a → 0ℤ ℤ.> ℤ.- a + 0-a {a} 0a⇒0<-a : ∀ {a} → 0ℤ ℤ.> a → 0ℤ ℤ.< ℤ.- a + 0>a⇒0<-a {a} 0>a = begin-strict + 0ℤ ≈˘⟨ ℤ.-‿inverseʳ a ⟩ + a ℤ.- a <⟨ ℤ.+-invariantʳ _ 0>a ⟩ + 0ℤ ℤ.- a ≈⟨ ℤ.+-identityˡ _ ⟩ + ℤ.- a ∎ + where open ℤ-Reasoning + + 0<-a⇒0>a : ∀ {a} → 0ℤ ℤ.< ℤ.- a → 0ℤ ℤ.> a + 0<-a⇒0>a {a} 0<-a = begin-strict + a ≈˘⟨ ℤ.+-identityʳ a ⟩ + a ℤ.+ 0ℤ <⟨ ℤ.+-invariantˡ a 0<-a ⟩ + a ℤ.- a ≈⟨ ℤ.-‿inverseʳ a ⟩ + 0ℤ ∎ + where open ℤ-Reasoning + + 0>-a⇒0 ℤ.- a → 0ℤ ℤ.< a + 0>-a⇒0-a = begin-strict + 0ℤ ≈˘⟨ ℤ.-‿inverseʳ a ⟩ + a ℤ.- a <⟨ ℤ.+-invariantˡ a 0>-a ⟩ + a ℤ.+ 0ℤ ≈⟨ ℤ.+-identityʳ a ⟩ + a ∎ + where open ℤ-Reasoning + + 0>a+0ab : ∀ {a b} → 0ℤ ℤ.> a → 0ℤ ℤ.< b → 0ℤ ℤ.> a ℤ.* b + 0>a+0ab {a} {b} 0>a 0a $ begin-strict + 0ℤ <⟨ ℤ.0a⇒0<-a 0>a) 0b⇒0>ab : ∀ {a b} → 0ℤ ℤ.< a → 0ℤ ℤ.> b → 0ℤ ℤ.> a ℤ.* b + 0b⇒0>ab {a} {b} 0b = 0<-a⇒0>a $ begin-strict + 0ℤ <⟨ ℤ.0a⇒0<-a 0>b) ⟩ + a ℤ.* ℤ.- b ≈⟨ a*-b≈-ab a b ⟩ + ℤ.- (a ℤ.* b) ∎ + where open ℤ-Reasoning + + 0>a+0>b⇒0 a → 0ℤ ℤ.> b → 0ℤ ℤ.< a ℤ.* b + 0>a+0>b⇒0a 0>b = begin-strict + 0ℤ <⟨ ℤ.0a⇒0<-a 0>a) (0>a⇒0<-a 0>b) ⟩ + ℤ.- a ℤ.* ℤ.- b ≈⟨ -a*b≈-ab a (ℤ.- b) ⟩ + ℤ.- (a ℤ.* ℤ.- b) ≈⟨ ℤ.-‿cong $ a*-b≈-ab a b ⟩ + ℤ.- (ℤ.- (a ℤ.* b)) ≈⟨ -‿idem (a ℤ.* b) ⟩ + a ℤ.* b ∎ + where open ℤ-Reasoning + + a≉0+b≉0⇒ab≉0 : ∀ {a b} → a ℤ.≉ 0ℤ → b ℤ.≉ 0ℤ → a ℤ.* b ℤ.≉ 0ℤ + a≉0+b≉0⇒ab≉0 {a} {b} a≉0 b≉0 ab≈0 with ℤ.compare a 0ℤ | ℤ.compare b 0ℤ + ... | tri< a<0 _ _ | tri< b<0 _ _ = ℤ.irrefl (ℤ.Eq.sym ab≈0) $ 0>a+0>b⇒0 _ _ b>0 = ℤ.irrefl ab≈0 $ 0>a+0ab a<0 b>0 + ... | tri≈ _ a≈0 _ | _ = a≉0 a≈0 + ... | tri> _ _ a>0 | tri< b<0 _ _ = ℤ.irrefl ab≈0 $ 0b⇒0>ab a>0 b<0 + ... | tri> _ _ a>0 | tri≈ _ b≈0 _ = b≉0 b≈0 + ... | tri> _ _ a>0 | tri> _ _ b>0 = ℤ.irrefl (ℤ.Eq.sym ab≈0) $ ℤ.00 b>0 + + ab≈0⇒a≈0⊎b≈0 : ∀ {a b} → a ℤ.* b ℤ.≈ 0ℤ → a ℤ.≈ 0ℤ ⊎ b ℤ.≈ 0ℤ + ab≈0⇒a≈0⊎b≈0 {a} {b} ab≈0 with a ℤ.≟ 0ℤ | b ℤ.≟ 0ℤ + ... | yes a≈0 | _ = inj₁ a≈0 + ... | no a≉0 | yes b≈0 = inj₂ b≈0 + ... | no a≉0 | no b≉0 = ⊥-elim (a≉0+b≉0⇒ab≉0 a≉0 b≉0 ab≈0) + + 2a< _ _ 0>1 = begin-strict + 0ℤ ≈˘⟨ ℤ.zeroʳ (ℤ.- 1ℤ) ⟩ + ℤ.- 1ℤ ℤ.* 0ℤ <⟨ aa⇒0<-a 0>1) (0>a⇒0<-a 0>1) ⟩ + ℤ.- 1ℤ ℤ.* ℤ.- 1ℤ ≈⟨ -a*b≈-ab 1ℤ (ℤ.- 1ℤ) ⟩ + ℤ.- (1ℤ ℤ.* ℤ.- 1ℤ) ≈⟨ ℤ.-‿cong $ ℤ.*-identityˡ (ℤ.- 1ℤ) ⟩ + ℤ.- (ℤ.- 1ℤ) ≈⟨ -‿idem 1ℤ ⟩ + 1ℤ ∎ + where open ℤ-Reasoning + + 0<2 : 0ℤ ℤ.< 2ℤ + 0<2 = begin-strict + 0ℤ ≈˘⟨ ℤ.+-identity² ⟩ + 0ℤ ℤ.+ 0ℤ <⟨ ℤ.+-invariantˡ 0ℤ 0<1 ⟩ + 0ℤ ℤ.+ 1ℤ <⟨ ℤ.+-invariantʳ 1ℤ 0<1 ⟩ + 2ℤ ∎ + where open ℤ-Reasoning + + 1<