diff options
Diffstat (limited to 'src/Helium/Data/Pseudocode.agda')
| -rw-r--r-- | src/Helium/Data/Pseudocode.agda | 398 |
1 files changed, 312 insertions, 86 deletions
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<<n≉0 : ∀ n → False (float (1ℤ << n) ≟ʳ 0ℝ)) + (1<<n≉0 : ∀ n → False ((1ℤ << n) /1 ≟ʳ 0ℝ)) where infixl 5 _>>_ @@ -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 + ; _≟ᶻ_ = ℤ._≟_ + ; _<ᶻ?_ = ℤ._<?_ + ; _≟ʳ_ = ℝ._≟_ + ; _<ʳ?_ = ℝ._<?_ + ; _≟ᵇ₁_ = 𝔹._≟_ + ; _/1 = _/1 + ; ⌊_⌋ = ⌊_⌋ + } + + open RawPseudocode rawPseudocode public + using + ( 2ℤ; cast; getᵇ; setᵇ; sliceᵇ; updateᵇ; hasBit + ; _div_; _mod_; _<<_; uint; sint + ) + + private + -- FIXME: move almost all of these proofs into a separate module + a<b⇒ca<cb : ∀ {a b c} → 0ℤ ℤ.< c → a ℤ.< b → c ℤ.* a ℤ.< c ℤ.* b + a<b⇒ca<cb {a} {b} {c} 0<c a<b = begin-strict + c ℤ.* a ≈˘⟨ ℤ.+-identityʳ _ ⟩ + c ℤ.* a ℤ.+ 0ℤ <⟨ ℤ.+-invariantˡ _ $ ℤ.0<a+0<b⇒0<ab 0<c 0<b-a ⟩ + c ℤ.* a ℤ.+ c ℤ.* (b ℤ.- a) ≈˘⟨ ℤ.distribˡ c a (b ℤ.- a) ⟩ + c ℤ.* (a ℤ.+ (b ℤ.- a)) ≈⟨ ℤ.*-congˡ $ ℤ.+-congˡ $ ℤ.+-comm b (ℤ.- a) ⟩ + c ℤ.* (a ℤ.+ (ℤ.- a ℤ.+ b)) ≈˘⟨ ℤ.*-congˡ $ ℤ.+-assoc a (ℤ.- a) b ⟩ + c ℤ.* ((a ℤ.+ ℤ.- a) ℤ.+ b) ≈⟨ ℤ.*-congˡ $ ℤ.+-congʳ $ ℤ.-‿inverseʳ a ⟩ + c ℤ.* (0ℤ ℤ.+ b) ≈⟨ (ℤ.*-congˡ $ ℤ.+-identityˡ b) ⟩ + c ℤ.* b ∎ + where + open ℤ-Reasoning + + 0<b-a : 0ℤ ℤ.< b ℤ.- a + 0<b-a = begin-strict + 0ℤ ≈˘⟨ ℤ.-‿inverseʳ a ⟩ + a ℤ.- a <⟨ ℤ.+-invariantʳ (ℤ.- a) a<b ⟩ + b ℤ.- a ∎ + + -‿idem : ∀ x → ℤ.- (ℤ.- x) ℤ.≈ x + -‿idem x = begin-equality + ℤ.- (ℤ.- x) ≈˘⟨ ℤ.+-identityˡ _ ⟩ + 0ℤ ℤ.- ℤ.- x ≈˘⟨ ℤ.+-congʳ $ ℤ.-‿inverseʳ x ⟩ + x ℤ.- x ℤ.- ℤ.- x ≈⟨ ℤ.+-assoc x (ℤ.- x) _ ⟩ + x ℤ.+ (ℤ.- x ℤ.- ℤ.- x) ≈⟨ ℤ.+-congˡ $ ℤ.-‿inverseʳ (ℤ.- x) ⟩ + x ℤ.+ 0ℤ ≈⟨ ℤ.+-identityʳ x ⟩ + x ∎ + where open ℤ-Reasoning + + -a*b≈-ab : ∀ a b → ℤ.- a ℤ.* b ℤ.≈ ℤ.- (a ℤ.* b) + -a*b≈-ab a b = begin-equality + ℤ.- a ℤ.* b ≈˘⟨ ℤ.+-identityʳ _ ⟩ + ℤ.- a ℤ.* b ℤ.+ 0ℤ ≈˘⟨ ℤ.+-congˡ $ ℤ.-‿inverseʳ _ ⟩ + ℤ.- a ℤ.* b ℤ.+ (a ℤ.* b ℤ.- a ℤ.* b) ≈˘⟨ ℤ.+-assoc _ _ _ ⟩ + ℤ.- a ℤ.* b ℤ.+ a ℤ.* b ℤ.- a ℤ.* b ≈˘⟨ ℤ.+-congʳ $ ℤ.distribʳ b _ a ⟩ + (ℤ.- a ℤ.+ a) ℤ.* b ℤ.- a ℤ.* b ≈⟨ ℤ.+-congʳ $ ℤ.*-congʳ $ ℤ.-‿inverseˡ a ⟩ + 0ℤ ℤ.* b ℤ.- a ℤ.* b ≈⟨ ℤ.+-congʳ $ ℤ.zeroˡ b ⟩ + 0ℤ ℤ.- a ℤ.* b ≈⟨ ℤ.+-identityˡ _ ⟩ + ℤ.- (a ℤ.* b) ∎ + where open ℤ-Reasoning + + a*-b≈-ab : ∀ a b → a ℤ.* ℤ.- b ℤ.≈ ℤ.- (a ℤ.* b) + a*-b≈-ab a b = begin-equality + a ℤ.* ℤ.- b ≈⟨ ℤ.*-comm a (ℤ.- b) ⟩ + ℤ.- b ℤ.* a ≈⟨ -a*b≈-ab b a ⟩ + ℤ.- (b ℤ.* a) ≈⟨ ℤ.-‿cong $ ℤ.*-comm b a ⟩ + ℤ.- (a ℤ.* b) ∎ + where open ℤ-Reasoning + + 0<a⇒0>-a : ∀ {a} → 0ℤ ℤ.< a → 0ℤ ℤ.> ℤ.- a + 0<a⇒0>-a {a} 0<a = begin-strict + ℤ.- a ≈˘⟨ ℤ.+-identityˡ _ ⟩ + 0ℤ ℤ.- a <⟨ ℤ.+-invariantʳ _ 0<a ⟩ + a ℤ.- a ≈⟨ ℤ.-‿inverseʳ a ⟩ + 0ℤ ∎ + where open ℤ-Reasoning + + 0>a⇒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 : ∀ {a} → 0ℤ ℤ.> ℤ.- a → 0ℤ ℤ.< a + 0>-a⇒0<a {a} 0>-a = begin-strict + 0ℤ ≈˘⟨ ℤ.-‿inverseʳ a ⟩ + a ℤ.- a <⟨ ℤ.+-invariantˡ a 0>-a ⟩ + a ℤ.+ 0ℤ ≈⟨ ℤ.+-identityʳ a ⟩ + a ∎ + where open ℤ-Reasoning + + 0>a+0<b⇒0>ab : ∀ {a b} → 0ℤ ℤ.> a → 0ℤ ℤ.< b → 0ℤ ℤ.> a ℤ.* b + 0>a+0<b⇒0>ab {a} {b} 0>a 0<b = 0<-a⇒0>a $ begin-strict + 0ℤ <⟨ ℤ.0<a+0<b⇒0<ab (0>a⇒0<-a 0>a) 0<b ⟩ + ℤ.- a ℤ.* b ≈⟨ -a*b≈-ab a b ⟩ + ℤ.- (a ℤ.* b) ∎ + where open ℤ-Reasoning + + 0<a+0>b⇒0>ab : ∀ {a b} → 0ℤ ℤ.< a → 0ℤ ℤ.> b → 0ℤ ℤ.> a ℤ.* b + 0<a+0>b⇒0>ab {a} {b} 0<a 0>b = 0<-a⇒0>a $ begin-strict + 0ℤ <⟨ ℤ.0<a+0<b⇒0<ab 0<a (0>a⇒0<-a 0>b) ⟩ + a ℤ.* ℤ.- b ≈⟨ a*-b≈-ab a b ⟩ + ℤ.- (a ℤ.* b) ∎ + where open ℤ-Reasoning + + 0>a+0>b⇒0<ab : ∀ {a b} → 0ℤ ℤ.> a → 0ℤ ℤ.> b → 0ℤ ℤ.< a ℤ.* b + 0>a+0>b⇒0<ab {a} {b} 0>a 0>b = begin-strict + 0ℤ <⟨ ℤ.0<a+0<b⇒0<ab (0>a⇒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<ab a<0 b<0 + ... | tri< a<0 _ _ | tri≈ _ b≈0 _ = b≉0 b≈0 + ... | tri< a<0 _ _ | tri> _ _ b>0 = ℤ.irrefl ab≈0 $ 0>a+0<b⇒0>ab a<0 b>0 + ... | tri≈ _ a≈0 _ | _ = a≉0 a≈0 + ... | tri> _ _ a>0 | tri< b<0 _ _ = ℤ.irrefl ab≈0 $ 0<a+0>b⇒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) $ ℤ.0<a+0<b⇒0<ab a>0 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<<n≈a<<1+n : ∀ a n → 2ℤ ℤ.* (a << n) ℤ.≈ a << suc n + 2a<<n≈a<<1+n a zero = ℤ.*-congˡ $ ℤ.*-identityˡ a + 2a<<n≈a<<1+n a (suc n) = begin-equality + 2ℤ ℤ.* (a << suc n) ≈˘⟨ ℤ.*-assoc 2ℤ _ a ⟩ + (2ℤ ℤ.* _) ℤ.* a ≈⟨ ℤ.*-congʳ $ ℤ.*-comm 2ℤ _ ⟩ + a << suc (suc n) ∎ + where open ℤ-Reasoning + + 0<1 : 0ℤ ℤ.< 1ℤ + 0<1 with ℤ.compare 0ℤ 1ℤ + ... | tri< 0<1 _ _ = 0<1 + ... | tri≈ _ 0≈1 _ = ⊥-elim (1≉0 (ℤ.Eq.sym 0≈1)) + ... | tri> _ _ 0>1 = begin-strict + 0ℤ ≈˘⟨ ℤ.zeroʳ (ℤ.- 1ℤ) ⟩ + ℤ.- 1ℤ ℤ.* 0ℤ <⟨ a<b⇒ca<cb (0>a⇒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<<n≉0 : ∀ n → 1ℤ << n ℤ.≉ 0ℤ + 1<<n≉0 zero eq = 1≉0 1≈0 + where + open ℤ-Reasoning + 1≈0 = begin-equality + 1ℤ ≈˘⟨ ℤ.*-identity² ⟩ + 1ℤ ℤ.* 1ℤ ≈⟨ eq ⟩ + 0ℤ ∎ + 1<<n≉0 (suc zero) eq = ℤ.irrefl 0≈2 0<2 + where + open ℤ-Reasoning + 0≈2 = begin-equality + 0ℤ ≈˘⟨ eq ⟩ + 2ℤ ℤ.* 1ℤ ≈⟨ ℤ.*-identityʳ 2ℤ ⟩ + 2ℤ ∎ + 1<<n≉0 (suc (suc n)) eq = + [ (λ 2≈0 → ℤ.irrefl (ℤ.Eq.sym 2≈0) 0<2) , 1<<n≉0 (suc n) ]′ + $ ab≈0⇒a≈0⊎b≈0 $ ℤ.Eq.trans (2a<<n≈a<<1+n 1ℤ (suc n)) eq + + 1<<n≉0ℝ : ∀ n → (1ℤ << n) /1 ℝ.≉ 0ℝ + 1<<n≉0ℝ n eq = 1<<n≉0 n $ (begin-equality + 1ℤ << n ≈˘⟨ ⌊⌋∘/1≗id (1ℤ << n) ⟩ + ⌊ (1ℤ << n) /1 ⌋ ≈⟨ ⌊⌋.cong $ eq ⟩ + ⌊ 0ℝ ⌋ ≈⟨ ⌊⌋.0#-homo ⟩ + 0ℤ ∎) + where open ℤ-Reasoning + + open RawPseudocode rawPseudocode using (module ShiftNotZero) + + open ShiftNotZero (λ n → fromWitnessFalse (1<<n≉0ℝ n)) public |