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/Algebra/Construct/Pointwise.agda | 68 ---- src/Helium/Algebra/Decidable/Bundles.agda | 108 ++++++ .../Algebra/Decidable/Construct/Pointwise.agda | 93 +++++ src/Helium/Algebra/Decidable/Structures.agda | 87 +++++ src/Helium/Algebra/Morphism/Structures.agda | 42 +++ .../Algebra/Ordered/StrictTotal/Bundles.agda | 182 +++++++++- .../Algebra/Ordered/StrictTotal/Structures.agda | 160 +++++++-- src/Helium/Data/Pseudocode.agda | 398 ++++++++++++++++----- src/Helium/Semantics/Denotational.agda | 26 +- 9 files changed, 961 insertions(+), 203 deletions(-) delete mode 100644 src/Helium/Algebra/Construct/Pointwise.agda create mode 100644 src/Helium/Algebra/Decidable/Bundles.agda create mode 100644 src/Helium/Algebra/Decidable/Construct/Pointwise.agda create mode 100644 src/Helium/Algebra/Decidable/Structures.agda create mode 100644 src/Helium/Algebra/Morphism/Structures.agda (limited to 'src') diff --git a/src/Helium/Algebra/Construct/Pointwise.agda b/src/Helium/Algebra/Construct/Pointwise.agda deleted file mode 100644 index d3aa560..0000000 --- a/src/Helium/Algebra/Construct/Pointwise.agda +++ /dev/null @@ -1,68 +0,0 @@ ------------------------------------------------------------------------- --- Agda Helium --- --- Construct algebras of vectors in a pointwise manner ------------------------------------------------------------------------- - -{-# OPTIONS --safe --without-K #-} - -module Helium.Algebra.Construct.Pointwise where - -open import Algebra -open import Relation.Binary.Core using (Rel) -open import Data.Nat using (ℕ) -open import Data.Product using (_,_) -open import Data.Vec.Functional using (replicate; map; zipWith) -open import Data.Vec.Functional.Relation.Binary.Pointwise using (Pointwise) -import Data.Vec.Functional.Relation.Binary.Pointwise.Properties as Pwₚ -open import Function using (_$_) -open import Relation.Binary.Bundles using (Setoid) - -module _ {a ℓ} {A : Set a} {_≈_ : Rel A ℓ} where - private - _≋_ = Pointwise _≈_ - - module _ {∨ ∧ : Op₂ A} where - isLattice : IsLattice _≈_ ∨ ∧ → ∀ n → IsLattice (_≋_ {n}) (zipWith ∨) (zipWith ∧) - isLattice L n = record - { isEquivalence = Pwₚ.isEquivalence isEquivalence n - ; ∨-comm = λ x y i → ∨-comm (x i) (y i) - ; ∨-assoc = λ x y z i → ∨-assoc (x i) (y i) (z i) - ; ∨-cong = λ x≈y u≈v i → ∨-cong (x≈y i) (u≈v i) - ; ∧-comm = λ x y i → ∧-comm (x i) (y i) - ; ∧-assoc = λ x y z i → ∧-assoc (x i) (y i) (z i) - ; ∧-cong = λ x≈y u≈v i → ∧-cong (x≈y i) (u≈v i) - ; absorptive = (λ x y i → ∨-absorbs-∧ (x i) (y i)) - , (λ x y i → ∧-absorbs-∨ (x i) (y i)) - } - where open IsLattice L - - isDistributiveLattice : IsDistributiveLattice _≈_ ∨ ∧ → ∀ n → IsDistributiveLattice (_≋_ {n}) (zipWith ∨) (zipWith ∧) - isDistributiveLattice L n = record - { isLattice = isLattice L.isLattice n - ; ∨-distribʳ-∧ = λ x y z i → L.∨-distribʳ-∧ (x i) (y i) (z i) - } - where module L = IsDistributiveLattice L - - module _ {∨ ∧ : Op₂ A} {¬ : Op₁ A} {⊤ ⊥ : A} where - isBooleanAlgebra : IsBooleanAlgebra _≈_ ∨ ∧ ¬ ⊤ ⊥ → ∀ n → IsBooleanAlgebra (_≋_ {n}) (zipWith ∨) (zipWith ∧) (map ¬) (replicate ⊤) (replicate ⊥) - isBooleanAlgebra B n = record - { isDistributiveLattice = isDistributiveLattice B.isDistributiveLattice n - ; ∨-complementʳ = λ x i → B.∨-complementʳ (x i) - ; ∧-complementʳ = λ x i → B.∧-complementʳ (x i) - ; ¬-cong = λ x≈y i → B.¬-cong (x≈y i) - } - where module B = IsBooleanAlgebra B - -lattice : ∀ {a ℓ} → Lattice a ℓ → ℕ → Lattice a ℓ -lattice L n = record { isLattice = isLattice (Lattice.isLattice L) n } - -distributiveLattice : ∀ {a ℓ} → DistributiveLattice a ℓ → ℕ → DistributiveLattice a ℓ -distributiveLattice L n = record - { isDistributiveLattice = - isDistributiveLattice (DistributiveLattice.isDistributiveLattice L) n - } - -booleanAlgebra : ∀ {a ℓ} → BooleanAlgebra a ℓ → ℕ → BooleanAlgebra a ℓ -booleanAlgebra B n = record - { isBooleanAlgebra = isBooleanAlgebra (BooleanAlgebra.isBooleanAlgebra B) n } diff --git a/src/Helium/Algebra/Decidable/Bundles.agda b/src/Helium/Algebra/Decidable/Bundles.agda new file mode 100644 index 0000000..e446706 --- /dev/null +++ b/src/Helium/Algebra/Decidable/Bundles.agda @@ -0,0 +1,108 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Definitions of decidable algebraic structures like monoids and rings +-- (packed in records together with sets, operations, etc.) +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Helium.Algebra.Decidable.Bundles where + +open import Algebra.Bundles using (RawLattice) +open import Algebra.Core +open import Helium.Algebra.Decidable.Structures +open import Level using (suc; _⊔_) +open import Relation.Binary.Bundles using (DecSetoid) +open import Relation.Binary.Core using (Rel) + +record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where + infixr 7 _∧_ + infixr 6 _∨_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∨_ : Op₂ Carrier + _∧_ : Op₂ Carrier + isLattice : IsLattice _≈_ _∨_ _∧_ + + open IsLattice isLattice public + + rawLattice : RawLattice c ℓ + rawLattice = record + { _≈_ = _≈_ + ; _∧_ = _∧_ + ; _∨_ = _∨_ + } + + open RawLattice rawLattice public + using (∨-rawMagma; ∧-rawMagma) + + decSetoid : DecSetoid _ _ + decSetoid = record { isDecEquivalence = isDecEquivalence } + + open DecSetoid decSetoid public + using (_≉_; setoid) + +record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where + infixr 7 _∧_ + infixr 6 _∨_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∨_ : Op₂ Carrier + _∧_ : Op₂ Carrier + isDistributiveLattice : IsDistributiveLattice _≈_ _∨_ _∧_ + + open IsDistributiveLattice isDistributiveLattice public + + lattice : Lattice _ _ + lattice = record { isLattice = isLattice } + + open Lattice lattice public + using (_≉_; setoid; decSetoid; ∨-rawMagma; ∧-rawMagma; rawLattice) + +record RawBooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where + infix 8 ¬_ + infixr 7 _∧_ + infixr 6 _∨_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∧_ : Op₂ Carrier + _∨_ : Op₂ Carrier + ¬_ : Op₁ Carrier + ⊤ : Carrier + ⊥ : Carrier + + rawLattice : RawLattice c ℓ + rawLattice = record { _≈_ = _≈_; _∨_ = _∨_; _∧_ = _∧_ } + + open RawLattice rawLattice public + using (_≉_; ∨-rawMagma; ∧-rawMagma) + +record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where + infix 8 ¬_ + infixr 7 _∧_ + infixr 6 _∨_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∨_ : Op₂ Carrier + _∧_ : Op₂ Carrier + ¬_ : Op₁ Carrier + ⊤ : Carrier + ⊥ : Carrier + isBooleanAlgebra : IsBooleanAlgebra _≈_ _∨_ _∧_ ¬_ ⊤ ⊥ + + open IsBooleanAlgebra isBooleanAlgebra public + + distributiveLattice : DistributiveLattice _ _ + distributiveLattice = record { isDistributiveLattice = isDistributiveLattice } + + open DistributiveLattice distributiveLattice public + using (_≉_; setoid; decSetoid; ∨-rawMagma; ∧-rawMagma; rawLattice; lattice) diff --git a/src/Helium/Algebra/Decidable/Construct/Pointwise.agda b/src/Helium/Algebra/Decidable/Construct/Pointwise.agda new file mode 100644 index 0000000..9f067ba --- /dev/null +++ b/src/Helium/Algebra/Decidable/Construct/Pointwise.agda @@ -0,0 +1,93 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Construct algebras of vectors in a pointwise manner +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +module Helium.Algebra.Decidable.Construct.Pointwise where + +open import Algebra.Bundles using (RawLattice) +open import Algebra.Core +open import Data.Nat using (ℕ) +open import Data.Product using (_,_) +open import Data.Vec.Functional using (replicate; map; zipWith) +open import Data.Vec.Functional.Relation.Binary.Pointwise using (Pointwise) +import Data.Vec.Functional.Relation.Binary.Pointwise.Properties as Pwₚ +open import Function using (_$_) +open import Helium.Algebra.Decidable.Bundles +open import Helium.Algebra.Decidable.Structures +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Core using (Rel) + +module _ {a ℓ} {A : Set a} {_≈_ : Rel A ℓ} where + private + _≋_ = Pointwise _≈_ + + module _ {∨ ∧ : Op₂ A} where + isLattice : IsLattice _≈_ ∨ ∧ → ∀ n → IsLattice (_≋_ {n}) (zipWith ∨) (zipWith ∧) + isLattice L n = record + { isDecEquivalence = Pwₚ.isDecEquivalence isDecEquivalence n + ; ∨-comm = λ x y i → ∨-comm (x i) (y i) + ; ∨-assoc = λ x y z i → ∨-assoc (x i) (y i) (z i) + ; ∨-cong = λ x≈y u≈v i → ∨-cong (x≈y i) (u≈v i) + ; ∧-comm = λ x y i → ∧-comm (x i) (y i) + ; ∧-assoc = λ x y z i → ∧-assoc (x i) (y i) (z i) + ; ∧-cong = λ x≈y u≈v i → ∧-cong (x≈y i) (u≈v i) + ; absorptive = (λ x y i → ∨-absorbs-∧ (x i) (y i)) + , (λ x y i → ∧-absorbs-∨ (x i) (y i)) + } + where open IsLattice L + + isDistributiveLattice : IsDistributiveLattice _≈_ ∨ ∧ → ∀ n → IsDistributiveLattice (_≋_ {n}) (zipWith ∨) (zipWith ∧) + isDistributiveLattice L n = record + { isLattice = isLattice L.isLattice n + ; ∨-distrib-∧ = (λ x y z i → L.∨-distribˡ-∧ (x i) (y i) (z i)) + , (λ x y z i → L.∨-distribʳ-∧ (x i) (y i) (z i)) + } + where module L = IsDistributiveLattice L + + module _ {∨ ∧ : Op₂ A} {¬ : Op₁ A} {⊤ ⊥ : A} where + isBooleanAlgebra : IsBooleanAlgebra _≈_ ∨ ∧ ¬ ⊤ ⊥ → ∀ n → IsBooleanAlgebra (_≋_ {n}) (zipWith ∨) (zipWith ∧) (map ¬) (replicate ⊤) (replicate ⊥) + isBooleanAlgebra B n = record + { isDistributiveLattice = isDistributiveLattice B.isDistributiveLattice n + ; ∨-complement = (λ x i → B.∨-complementˡ (x i)) + , (λ x i → B.∨-complementʳ (x i)) + ; ∧-complement = (λ x i → B.∧-complementˡ (x i)) + , (λ x i → B.∧-complementʳ (x i)) + ; ¬-cong = λ x≈y i → B.¬-cong (x≈y i) + } + where module B = IsBooleanAlgebra B + +rawLattice : ∀ {a ℓ} → RawLattice a ℓ → ℕ → RawLattice a ℓ +rawLattice L n = record + { _≈_ = Pointwise _≈_ {n} + ; _∧_ = zipWith _∧_ + ; _∨_ = zipWith _∨_ + } + where open RawLattice L + +lattice : ∀ {a ℓ} → Lattice a ℓ → ℕ → Lattice a ℓ +lattice L n = record { isLattice = isLattice (Lattice.isLattice L) n } + +distributiveLattice : ∀ {a ℓ} → DistributiveLattice a ℓ → ℕ → DistributiveLattice a ℓ +distributiveLattice L n = record + { isDistributiveLattice = + isDistributiveLattice (DistributiveLattice.isDistributiveLattice L) n + } + +rawBooleanAlgebra : ∀ {a ℓ} → RawBooleanAlgebra a ℓ → ℕ → RawBooleanAlgebra a ℓ +rawBooleanAlgebra B n = record + { _≈_ = Pointwise _≈_ {n} + ; _∧_ = zipWith _∧_ + ; _∨_ = zipWith _∨_ + ; ¬_ = map ¬_ + ; ⊤ = replicate ⊤ + ; ⊥ = replicate ⊥ + } + where open RawBooleanAlgebra B + +booleanAlgebra : ∀ {a ℓ} → BooleanAlgebra a ℓ → ℕ → BooleanAlgebra a ℓ +booleanAlgebra B n = record + { isBooleanAlgebra = isBooleanAlgebra (BooleanAlgebra.isBooleanAlgebra B) n } diff --git a/src/Helium/Algebra/Decidable/Structures.agda b/src/Helium/Algebra/Decidable/Structures.agda new file mode 100644 index 0000000..4380cc5 --- /dev/null +++ b/src/Helium/Algebra/Decidable/Structures.agda @@ -0,0 +1,87 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Some decidable algebraic structures (not packed up with sets, +-- operations, etc.) +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Relation.Binary.Core using (Rel) + +module Helium.Algebra.Decidable.Structures + {a ℓ} {A : Set a} -- The underlying set + (_≈_ : Rel A ℓ) -- The underlying equality relation + where + +open import Algebra.Core +open import Algebra.Definitions (_≈_) +open import Data.Product using (proj₁; proj₂) +open import Level using (_⊔_) +open import Relation.Binary.Structures using (IsDecEquivalence) + +record IsLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where + field + isDecEquivalence : IsDecEquivalence _≈_ + ∨-comm : Commutative ∨ + ∨-assoc : Associative ∨ + ∨-cong : Congruent₂ ∨ + ∧-comm : Commutative ∧ + ∧-assoc : Associative ∧ + ∧-cong : Congruent₂ ∧ + absorptive : Absorptive ∨ ∧ + + open IsDecEquivalence isDecEquivalence public + + ∨-absorbs-∧ : ∨ Absorbs ∧ + ∨-absorbs-∧ = proj₁ absorptive + + ∧-absorbs-∨ : ∧ Absorbs ∨ + ∧-absorbs-∨ = proj₂ absorptive + + ∧-congˡ : LeftCongruent ∧ + ∧-congˡ y≈z = ∧-cong refl y≈z + + ∧-congʳ : RightCongruent ∧ + ∧-congʳ y≈z = ∧-cong y≈z refl + + ∨-congˡ : LeftCongruent ∨ + ∨-congˡ y≈z = ∨-cong refl y≈z + + ∨-congʳ : RightCongruent ∨ + ∨-congʳ y≈z = ∨-cong y≈z refl + +record IsDistributiveLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where + field + isLattice : IsLattice ∨ ∧ + ∨-distrib-∧ : ∨ DistributesOver ∧ + + open IsLattice isLattice public + + ∨-distribˡ-∧ : ∨ DistributesOverˡ ∧ + ∨-distribˡ-∧ = proj₁ ∨-distrib-∧ + + ∨-distribʳ-∧ : ∨ DistributesOverʳ ∧ + ∨-distribʳ-∧ = proj₂ ∨-distrib-∧ + +record IsBooleanAlgebra + (∨ ∧ : Op₂ A) (¬ : Op₁ A) (⊤ ⊥ : A) : Set (a ⊔ ℓ) where + field + isDistributiveLattice : IsDistributiveLattice ∨ ∧ + ∨-complement : Inverse ⊤ ¬ ∨ + ∧-complement : Inverse ⊥ ¬ ∧ + ¬-cong : Congruent₁ ¬ + + open IsDistributiveLattice isDistributiveLattice public + + ∨-complementˡ : LeftInverse ⊤ ¬ ∨ + ∨-complementˡ = proj₁ ∨-complement + + ∨-complementʳ : RightInverse ⊤ ¬ ∨ + ∨-complementʳ = proj₂ ∨-complement + + ∧-complementˡ : LeftInverse ⊥ ¬ ∧ + ∧-complementˡ = proj₁ ∧-complement + + ∧-complementʳ : RightInverse ⊥ ¬ ∧ + ∧-complementʳ = proj₂ ∧-complement diff --git a/src/Helium/Algebra/Morphism/Structures.agda b/src/Helium/Algebra/Morphism/Structures.agda new file mode 100644 index 0000000..bf219ef --- /dev/null +++ b/src/Helium/Algebra/Morphism/Structures.agda @@ -0,0 +1,42 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Redefine Ring monomorphisms to resolve problems with overloading. +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +module Helium.Algebra.Morphism.Structures where + +open import Algebra.Bundles using (RawRing) +open import Algebra.Morphism.Structures + hiding (IsRingHomomorphism; module RingMorphisms) +open import Level using (Level; _⊔_) + +private + variable + a b ℓ₁ ℓ₂ : Level + +module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where + module R₁ = RawRing R₁ renaming (Carrier to A) + module R₂ = RawRing R₂ renaming (Carrier to B) + open R₁ using (A) + open R₂ using (B) + + private + module +′ = GroupMorphisms R₁.+-rawGroup R₂.+-rawGroup + module *′ = MonoidMorphisms R₁.*-rawMonoid R₂.*-rawMonoid + + record IsRingHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + field + +-isGroupHomomorphism : +′.IsGroupHomomorphism ⟦_⟧ + *-isMonoidHomomorphism : *′.IsMonoidHomomorphism ⟦_⟧ + + open +′.IsGroupHomomorphism +-isGroupHomomorphism public + renaming (homo to +-homo; ε-homo to 0#-homo; ⁻¹-homo to -‿homo) + + open *′.IsMonoidHomomorphism *-isMonoidHomomorphism public + hiding (⟦⟧-cong) + renaming (homo to *-homo; ε-homo to 1#-homo) + +open RingMorphisms public diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda index 6904bfb..a9430e9 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda @@ -10,13 +10,12 @@ module Helium.Algebra.Ordered.StrictTotal.Bundles where -import Algebra.Bundles as Unordered +import Algebra.Bundles as NoOrder open import Algebra.Core open import Data.Sum using (_⊎_) open import Function using (flip) open import Helium.Algebra.Core -open import Helium.Algebra.Bundles using - (RawAlmostGroup; AlmostGroup; AlmostAbelianGroup) +import Helium.Algebra.Bundles as NoOrder′ open import Helium.Algebra.Ordered.StrictTotal.Structures open import Level using (suc; _⊔_) open import Relation.Binary @@ -44,6 +43,10 @@ record RawMagma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where _≥_ : Rel Carrier _ _≥_ = flip _≤_ + module Unordered where + rawMagma : NoOrder.RawMagma c ℓ₁ + rawMagma = record { _≈_ = _≈_ ; _∙_ = _∙_ } + record Magma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infixl 7 _∙_ infix 4 _≈_ _<_ @@ -55,6 +58,7 @@ record Magma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where isMagma : IsMagma _≈_ _<_ _∙_ open IsMagma isMagma public + hiding (module Unordered) rawMagma : RawMagma _ _ _ rawMagma = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_ } @@ -62,6 +66,15 @@ record Magma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where open RawMagma rawMagma public using (_≉_; _≤_; _>_; _≥_) + module Unordered where + magma : NoOrder.Magma c ℓ₁ + magma = record { isMagma = IsMagma.Unordered.isMagma isMagma } + + open NoOrder.Magma magma public + using (rawMagma) + + open IsMagma.Unordered isMagma public + record Semigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infixl 7 _∙_ infix 4 _≈_ _<_ @@ -73,6 +86,7 @@ record Semigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where isSemigroup : IsSemigroup _≈_ _<_ _∙_ open IsSemigroup isSemigroup public + hiding (module Unordered) magma : Magma c ℓ₁ ℓ₂ magma = record { isMagma = isMagma } @@ -80,6 +94,16 @@ record Semigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where open Magma magma public using (_≉_; _≤_; _>_; _≥_; rawMagma) + module Unordered where + semigroup : NoOrder.Semigroup c ℓ₁ + semigroup = + record { isSemigroup = IsSemigroup.Unordered.isSemigroup isSemigroup } + + open NoOrder.Semigroup semigroup public + using (rawMagma; magma) + + open IsSemigroup.Unordered isSemigroup public + record RawMonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infixl 7 _∙_ infix 4 _≈_ _<_ @@ -96,6 +120,13 @@ record RawMonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where open RawMagma rawMagma public using (_≉_; _≤_; _>_; _≥_) + module Unordered where + rawMonoid : NoOrder.RawMonoid c ℓ₁ + rawMonoid = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε } + + open NoOrder.RawMonoid rawMonoid public + using (rawMagma) + record Monoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infixl 7 _∙_ infix 4 _≈_ _<_ @@ -108,6 +139,7 @@ record Monoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where isMonoid : IsMonoid _≈_ _<_ _∙_ ε open IsMonoid isMonoid public + hiding (module Unordered) semigroup : Semigroup _ _ _ semigroup = record { isSemigroup = isSemigroup } @@ -118,6 +150,15 @@ record Monoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where rawMonoid : RawMonoid _ _ _ rawMonoid = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_; ε = ε} + module Unordered where + monoid : NoOrder.Monoid c ℓ₁ + monoid = record { isMonoid = IsMonoid.Unordered.isMonoid isMonoid } + + open NoOrder.Monoid monoid public + using (rawMagma; rawMonoid; magma; semigroup) + + open IsMonoid.Unordered isMonoid public + record RawGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 8 _⁻¹ infixl 7 _∙_ @@ -136,6 +177,12 @@ record RawGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where open RawMonoid rawMonoid public using (_≉_; _≤_; _>_; _≥_; rawMagma) + module Unordered where + rawGroup : NoOrder.RawGroup c ℓ₁ + rawGroup = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε; _⁻¹ = _⁻¹ } + + open NoOrder.RawGroup rawGroup public + using (rawMagma; rawMonoid) record Group c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 8 _⁻¹ @@ -151,6 +198,7 @@ record Group c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where isGroup : IsGroup _≈_ _<_ _∙_ ε _⁻¹ open IsGroup isGroup public + hiding (module Unordered) rawGroup : RawGroup _ _ _ rawGroup = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_; ε = ε; _⁻¹ = _⁻¹} @@ -161,6 +209,15 @@ record Group c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where open Monoid monoid public using (_≉_; _≤_; _>_; _≥_; rawMagma; magma; semigroup; rawMonoid) + module Unordered where + group : NoOrder.Group c ℓ₁ + group = record { isGroup = IsGroup.Unordered.isGroup isGroup } + + open NoOrder.Group group public + using (rawMagma; rawMonoid; rawGroup; magma; semigroup; monoid) + + open IsGroup.Unordered isGroup public + record AbelianGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 8 _⁻¹ infixl 7 _∙_ @@ -175,6 +232,7 @@ record AbelianGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where isAbelianGroup : IsAbelianGroup _≈_ _<_ _∙_ ε _⁻¹ open IsAbelianGroup isAbelianGroup public + hiding (module Unordered) group : Group _ _ _ group = record { isGroup = isGroup } @@ -186,6 +244,16 @@ record AbelianGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where ; rawMagma; rawMonoid; rawGroup ) + module Unordered where + abelianGroup : NoOrder.AbelianGroup c ℓ₁ + abelianGroup = + record { isAbelianGroup = IsAbelianGroup.Unordered.isAbelianGroup isAbelianGroup } + + open NoOrder.AbelianGroup abelianGroup public + using (rawMagma; rawMonoid; rawGroup; magma; semigroup; monoid; group) + + open IsAbelianGroup.Unordered isAbelianGroup public + record RawRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 8 -_ infixl 7 _*_ @@ -211,13 +279,21 @@ record RawRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where ; rawMonoid to +-rawMonoid ) - *-rawMonoid : Unordered.RawMonoid c ℓ₁ + *-rawMonoid : NoOrder.RawMonoid c ℓ₁ *-rawMonoid = record { _≈_ = _≈_; _∙_ = _*_; ε = 1# } - open Unordered.RawMonoid *-rawMonoid public + open NoOrder.RawMonoid *-rawMonoid public using () renaming ( rawMagma to *-rawMagma ) + module Unordered where + rawRing : NoOrder.RawRing c ℓ₁ + rawRing = + record { _≈_ = _≈_ ; _+_ = _+_ ; _*_ = _*_ ; -_ = -_ ; 0# = 0# ; 1# = 1# } + + open NoOrder.RawRing rawRing public + using (+-rawMagma; +-rawMonoid; +-rawGroup; rawSemiring) + record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 8 -_ infixl 7 _*_ @@ -235,6 +311,7 @@ record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where isRing : IsRing _≈_ _<_ _+_ _*_ -_ 0# 1# open IsRing isRing public + hiding (module Unordered) rawRing : RawRing c ℓ₁ ℓ₂ rawRing = record @@ -262,10 +339,10 @@ record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where ; group to +-group ) - *-monoid : Unordered.Monoid _ _ + *-monoid : NoOrder.Monoid _ _ *-monoid = record { isMonoid = *-isMonoid } - open Unordered.Monoid *-monoid public + open NoOrder.Monoid *-monoid public using () renaming ( rawMagma to *-rawMagma @@ -274,6 +351,19 @@ record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where ; semigroup to *-semigroup ) + module Unordered where + ring : NoOrder.Ring c ℓ₁ + ring = record { isRing = IsRing.Unordered.isRing isRing } + + open NoOrder.Ring ring public + using + ( +-rawMagma; +-rawMonoid + ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup + ; rawRing; semiring + ) + + open IsRing.Unordered isRing public + record CommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 8 -_ infixl 7 _*_ @@ -291,6 +381,7 @@ record CommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) whe isCommutativeRing : IsCommutativeRing _≈_ _<_ _+_ _*_ -_ 0# 1# open IsCommutativeRing isCommutativeRing public + hiding (module Unordered) ring : Ring _ _ _ ring = record { isRing = isRing } @@ -298,12 +389,30 @@ record CommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) whe open Ring ring public using ( _≉_; _≤_; _>_; _≥_ + ; rawRing ; +-rawMagma; +-rawMonoid; +-rawGroup ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup ; *-rawMagma; *-rawMonoid ; *-magma; *-semigroup; *-monoid ) + module Unordered where + commutativeRing : NoOrder.CommutativeRing c ℓ₁ + commutativeRing = + record { isCommutativeRing = IsCommutativeRing.Unordered.isCommutativeRing isCommutativeRing } + + open NoOrder.CommutativeRing commutativeRing public + using + ( +-rawMagma; +-rawMonoid + ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup + ; rawRing; semiring; ring + ) + + open NoOrder.Semiring semiring public + using (rawSemiring) + + open IsCommutativeRing.Unordered isCommutativeRing public + record RawField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 9 _⁻¹ infix 8 -_ @@ -343,7 +452,7 @@ record RawField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where ; *-rawMagma; *-rawMonoid ) - *-rawAlmostGroup : RawAlmostGroup c ℓ₁ + *-rawAlmostGroup : NoOrder′.RawAlmostGroup c ℓ₁ *-rawAlmostGroup = record { _≈_ = _≈_ ; _∙_ = _*_ @@ -352,6 +461,21 @@ record RawField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where ; _⁻¹ = _⁻¹ } + module Unordered where + rawField : NoOrder′.RawField c ℓ₁ + rawField = record + { _≈_ = _≈_ + ; _+_ = _+_ + ; _*_ = _*_ + ; -_ = -_ + ; 0# = 0# + ; 1# = 1# + ; _⁻¹ = _⁻¹ + } + + open NoOrder′.RawField rawField public + using (+-rawMagma; +-rawMonoid; +-rawGroup; rawSemiring; rawRing) + record DivisionRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 9 _⁻¹ infix 8 -_ @@ -371,6 +495,7 @@ record DivisionRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where isDivisionRing : IsDivisionRing _≈_ _<_ _+_ _*_ -_ 0# 1# _⁻¹ open IsDivisionRing isDivisionRing public + hiding (module Unordered) rawField : RawField c ℓ₁ ℓ₂ rawField = record @@ -397,13 +522,28 @@ record DivisionRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where ; *-magma; *-semigroup; *-monoid ) - *-almostGroup : AlmostGroup _ _ + *-almostGroup : NoOrder′.AlmostGroup _ _ *-almostGroup = record { isAlmostGroup = *-isAlmostGroup } - open AlmostGroup *-almostGroup public + open NoOrder′.AlmostGroup *-almostGroup public using () renaming (rawAlmostGroup to *-rawAlmostGroup) + module Unordered where + divisionRing : NoOrder′.DivisionRing c ℓ₁ + divisionRing = + record { isDivisionRing = IsDivisionRing.Unordered.isDivisionRing isDivisionRing } + + open NoOrder′.DivisionRing divisionRing public + using + ( +-rawMagma; +-rawMonoid + ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup + ; rawSemiring; rawRing + ; semiring; ring + ) + + open IsDivisionRing.Unordered isDivisionRing public + record Field c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 9 _⁻¹ infix 8 -_ @@ -423,15 +563,35 @@ record Field c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where isField : IsField _≈_ _<_ _+_ _*_ -_ 0# 1# _⁻¹ open IsField isField public + hiding (module Unordered) divisionRing : DivisionRing c ℓ₁ ℓ₂ divisionRing = record { isDivisionRing = isDivisionRing } - open DivisionRing divisionRing + open DivisionRing divisionRing public using ( _≉_; _≤_; _>_; _≥_ + ; rawRing; rawField; ring ; +-rawMagma; +-rawMonoid; +-rawGroup ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup ; *-rawMagma; *-rawMonoid; *-rawAlmostGroup ; *-magma; *-semigroup; *-monoid; *-almostGroup ) + + commutativeRing : CommutativeRing c ℓ₁ ℓ₂ + commutativeRing = record { isCommutativeRing = isCommutativeRing } + + module Unordered where + field′ : NoOrder′.Field c ℓ₁ + field′ = + record { isField = IsField.Unordered.isField isField } + + open NoOrder′.Field field′ public + using + ( +-rawMagma; +-rawMonoid + ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup + ; rawSemiring; rawRing + ; semiring; ring; divisionRing + ) + + open IsField.Unordered isField public diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda b/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda index 9dc0043..6f6b38d 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda @@ -18,11 +18,11 @@ module Helium.Algebra.Ordered.StrictTotal.Structures import Algebra.Consequences.Setoid as Consequences open import Algebra.Core open import Algebra.Definitions _≈_ -import Algebra.Structures _≈_ as Unordered +import Algebra.Structures _≈_ as NoOrder open import Data.Product using (_,_; proj₁; proj₂) open import Helium.Algebra.Core open import Helium.Algebra.Definitions _≈_ -open import Helium.Algebra.Structures _≈_ using (IsAlmostGroup) +import Helium.Algebra.Structures _≈_ as NoOrder′ open import Helium.Algebra.Ordered.Definitions _<_ open import Level using (_⊔_) @@ -52,26 +52,55 @@ record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where ∙-invariantʳ : RightInvariant ∙ ∙-invariantʳ = proj₂ ∙-invariant + module Unordered where + isMagma : NoOrder.IsMagma ∙ + isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ∙-cong } + record IsSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isMagma : IsMagma ∙ assoc : Associative ∙ open IsMagma isMagma public + hiding (module Unordered) + + module Unordered where + isSemigroup : NoOrder.IsSemigroup ∙ + isSemigroup = record + { isMagma = IsMagma.Unordered.isMagma isMagma + ; assoc = assoc + } + + open NoOrder.IsSemigroup isSemigroup public + using (isMagma) -record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where +record IsMonoid (_∙_ : Op₂ A) (ε : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field - isSemigroup : IsSemigroup ∙ - identity : Identity ε ∙ + isSemigroup : IsSemigroup _∙_ + identity : Identity ε _∙_ open IsSemigroup isSemigroup public + hiding (module Unordered) - identityˡ : LeftIdentity ε ∙ + identityˡ : LeftIdentity ε _∙_ identityˡ = proj₁ identity - identityʳ : RightIdentity ε ∙ + identityʳ : RightIdentity ε _∙_ identityʳ = proj₂ identity + identity² : (ε ∙ ε) ≈ ε + identity² = identityˡ ε + + module Unordered where + isMonoid : NoOrder.IsMonoid _∙_ ε + isMonoid = record + { isSemigroup = IsSemigroup.Unordered.isSemigroup isSemigroup + ; identity = identity + } + + open NoOrder.IsMonoid isMonoid public + using (isMagma; isSemigroup) + record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isMonoid : IsMonoid _∙_ ε @@ -79,6 +108,7 @@ record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁ ⁻¹-cong : Congruent₁ _⁻¹ open IsMonoid isMonoid public + hiding (module Unordered) infixl 6 _-_ _-_ : Op₂ A @@ -98,6 +128,17 @@ record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁ uniqueʳ-⁻¹ = Consequences.assoc+id+invˡ⇒invʳ-unique strictTotalOrder.Eq.setoid ∙-cong assoc identity inverseˡ + module Unordered where + isGroup : NoOrder.IsGroup _∙_ ε _⁻¹ + isGroup = record + { isMonoid = IsMonoid.Unordered.isMonoid isMonoid + ; inverse = inverse + ; ⁻¹-cong = ⁻¹-cong + } + + open NoOrder.IsGroup isGroup public + using (isMagma; isSemigroup; isMonoid) + record IsAbelianGroup (∙ : Op₂ A) (ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field @@ -105,14 +146,25 @@ record IsAbelianGroup (∙ : Op₂ A) comm : Commutative ∙ open IsGroup isGroup public + hiding (module Unordered) + + module Unordered where + isAbelianGroup : NoOrder.IsAbelianGroup ∙ ε ⁻¹ + isAbelianGroup = record + { isGroup = IsGroup.Unordered.isGroup isGroup + ; comm = comm + } -record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + open NoOrder.IsAbelianGroup isAbelianGroup public + using (isMagma; isSemigroup; isMonoid; isGroup) + +record IsRing (+ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field - +-isAbelianGroup : IsAbelianGroup + 0# -_ - *-isMonoid : Unordered.IsMonoid * 1# - distrib : * DistributesOver + - zero : Zero 0# * - preservesPositive : PreservesPositive 0# * + +-isAbelianGroup : IsAbelianGroup + 0# -_ + *-isMonoid : NoOrder.IsMonoid _*_ 1# + distrib : _*_ DistributesOver + + zero : Zero 0# _*_ + 0>_ @@ -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<> toℕ esize) + ⦇ (λ x y → (2ℤ ℤ.* sint x ℤ.* sint y ℤ.+ rval) >> toℕ esize) (! elem (toℕ esize) (&cast (sym e*e≡32) (var (# 2))) (!# 0)) ([ (λ src₂ → ! slice (&R ⦇ src₂ ⦈) ⦇ (esize , zero , refl) ⦈) , (λ src₂ → ! elem (toℕ esize) (&cast (sym e*e≡32) (&Q ⦇ src₂ ⦈ (!# 4))) (!# 0)) -- cgit v1.2.3