From ec372859de15d780ae5e3244813a7b006518fcab Mon Sep 17 00:00:00 2001 From: pmbittner Date: Thu, 13 Jun 2024 20:23:56 +0200 Subject: [PATCH] fix: Haskell.Law.Num to re-export all instances Haskell.Law.Num should publicly import all available instances as well as the LawfulNum class. To avoid cyclic dependencies, the functions for concluding number laws were move to Haskell.Law.Num.Def. --- lib/Haskell/Law/Num.agda | 101 +--------------------------------- lib/Haskell/Law/Num/Def.agda | 93 +++++++++++++++++++++++++++++++ lib/Haskell/Law/Num/Int.agda | 2 +- lib/Haskell/Law/Num/Word.agda | 4 +- 4 files changed, 100 insertions(+), 100 deletions(-) diff --git a/lib/Haskell/Law/Num.agda b/lib/Haskell/Law/Num.agda index beb0b191..80dd27e3 100644 --- a/lib/Haskell/Law/Num.agda +++ b/lib/Haskell/Law/Num.agda @@ -1,102 +1,7 @@ module Haskell.Law.Num where open import Haskell.Law.Num.Def public -open import Haskell.Law.Num.Nat public +open import Haskell.Law.Num.Int public open import Haskell.Law.Num.Integer public - -open import Haskell.Prim -open import Haskell.Prim.Num -open import Haskell.Prim.Function - -open import Haskell.Law.Equality -open import Haskell.Law.Function - -{-| -A number homomorphism establishes a homomorphism from one Num type a to another one b. -In particular, zero and one are mapped to zero and one in the other Num type, -and addition, multiplication, and negation are homorphic. --} -record NumHomomorphism (a b : Set) ⦃ iNuma : Num a ⦄ ⦃ iNumb : Num b ⦄ (φ : a → b) : Set where - 0ᵃ = Num.fromInteger iNuma (pos 0) - 0ᵇ = Num.fromInteger iNumb (pos 0) - 1ᵃ = Num.fromInteger iNuma (pos 1) - 1ᵇ = Num.fromInteger iNumb (pos 1) - - field - +-hom : Homomorphism₂ _+_ _+_ φ - *-hom : Homomorphism₂ _*_ _*_ φ - ⦃ minus-ok ⦄ : ∀ {x y : a} → ⦃ MinusOK x y ⦄ → MinusOK (φ x) (φ y) - ⦃ negate-ok ⦄ : ∀ {x : a} → ⦃ NegateOK x ⦄ → NegateOK (φ x) - ⦃ fromInteger-ok ⦄ : ∀ {i : Integer} → ⦃ Num.FromIntegerOK iNuma i ⦄ → Num.FromIntegerOK iNumb i - 0-hom : ⦃ @0 _ : Num.FromIntegerOK iNuma (pos 0) ⦄ → φ 0ᵃ ≡ 0ᵇ - 1-hom : ⦃ @0 _ : Num.FromIntegerOK iNuma (pos 1) ⦄ → φ 1ᵃ ≡ 1ᵇ - negate-hom : ∀ (x : a) → ⦃ @0 _ : Num.NegateOK iNuma x ⦄ → φ (negate x) ≡ negate (φ x) --Homomorphism₁ inlined for type instances - -{-| -A number embedding is an invertible number homomorphism. --} -record NumEmbedding (a b : Set) ⦃ iNuma : Num a ⦄ ⦃ iNumb : Num b ⦄ (φ : a → b) (φ⁻¹ : b → a) : Set where - field - hom : NumHomomorphism a b φ - embed : φ⁻¹ ∘ φ ≗ id - - open NumHomomorphism hom - - +-Embedding₂ : Embedding₂ _+_ _+_ φ φ⁻¹ - Embedding₂.hom +-Embedding₂ = +-hom - Embedding₂.embed +-Embedding₂ = embed - - *-Embedding₂ : Embedding₂ _*_ _*_ φ φ⁻¹ - Embedding₂.hom *-Embedding₂ = *-hom - Embedding₂.embed *-Embedding₂ = embed - - +-MonoidEmbedding₂ : ⦃ @0 _ : Num.FromIntegerOK iNuma (pos 0) ⦄ → MonoidEmbedding₂ _+_ _+_ φ φ⁻¹ 0ᵃ 0ᵇ - MonoidEmbedding₂.embedding +-MonoidEmbedding₂ = +-Embedding₂ - MonoidEmbedding₂.0-hom +-MonoidEmbedding₂ = 0-hom - - *-MonoidEmbedding₂ : ⦃ @0 _ : Num.FromIntegerOK iNuma (pos 1) ⦄ → MonoidEmbedding₂ _*_ _*_ φ φ⁻¹ 1ᵃ 1ᵇ - MonoidEmbedding₂.embedding *-MonoidEmbedding₂ = *-Embedding₂ - MonoidEmbedding₂.0-hom *-MonoidEmbedding₂ = 1-hom - -{-| -Given an embedding from one number type a onto another one b, -we can conclude that b satisfies the laws of Num if a satisfies the -laws of Num. --} -map-IsLawfulNum : ∀ {a b : Set} ⦃ iNuma : Num a ⦄ ⦃ iNumb : Num b ⦄ - → (a2b : a → b) (b2a : b → a) - → NumEmbedding a b a2b b2a - → IsLawfulNum b - ----------------------- - → IsLawfulNum a -map-IsLawfulNum {a} {b} {{numa}} {{numb}} f g proj lawb = - record - { +-assoc = map-assoc _+ᵃ_ _+ᵇ_ f g +-Embedding₂ (+-assoc lawb) - ; +-comm = map-comm _+ᵃ_ _+ᵇ_ f g +-Embedding₂ (+-comm lawb) - ; +-idˡ = λ x → map-idˡ _+ᵃ_ _+ᵇ_ f g 0ᵃ 0ᵇ +-MonoidEmbedding₂ (λ y → +-idˡ lawb y) x - ; +-idʳ = λ x → map-idʳ _+ᵃ_ _+ᵇ_ f g 0ᵃ 0ᵇ +-MonoidEmbedding₂ (λ y → +-idʳ lawb y) x - ; neg-inv = map-neg-inv - ; *-assoc = map-assoc _*ᵃ_ _*ᵇ_ f g *-Embedding₂ (*-assoc lawb) - ; *-idˡ = λ x → map-idˡ _*ᵃ_ _*ᵇ_ f g 1ᵃ 1ᵇ *-MonoidEmbedding₂ (λ y → *-idˡ lawb y) x - ; *-idʳ = λ x → map-idʳ _*ᵃ_ _*ᵇ_ f g 1ᵃ 1ᵇ *-MonoidEmbedding₂ (λ y → *-idʳ lawb y) x - ; distributeˡ = map-distributeˡ _+ᵃ_ _+ᵇ_ _*ᵃ_ _*ᵇ_ f g embed +-hom *-hom (distributeˡ lawb) - ; distributeʳ = map-distributeʳ _+ᵃ_ _+ᵇ_ _*ᵃ_ _*ᵇ_ f g embed +-hom *-hom (distributeʳ lawb) - } - where - open NumEmbedding proj - open NumHomomorphism hom - open IsLawfulNum lawb - open Num numa renaming (_+_ to _+ᵃ_; _*_ to _*ᵃ_; negate to negateᵃ) - open Num numb renaming (_+_ to _+ᵇ_; _*_ to _*ᵇ_; negate to negateᵇ) - - map-neg-inv : ∀ (x : a) ⦃ @0 _ : Num.FromIntegerOK numa (pos 0) ⦄ ⦃ @0 _ : Num.NegateOK numa x ⦄ - → x +ᵃ negateᵃ x ≡ 0ᵃ - map-neg-inv x = - x +ᵃ negateᵃ x ≡˘⟨ embed (x +ᵃ negateᵃ x) ⟩ - g (f (x +ᵃ negateᵃ x)) ≡⟨ cong g (+-hom x (negateᵃ x)) ⟩ - g (f x +ᵇ f (negateᵃ x)) ≡⟨ cong g (cong (f x +ᵇ_) (negate-hom x)) ⟩ - g (f x +ᵇ negateᵇ (f x)) ≡⟨ cong g (neg-inv lawb (f x)) ⟩ - g 0ᵇ ≡˘⟨ cong g 0-hom ⟩ - g (f 0ᵃ) ≡⟨ embed 0ᵃ ⟩ - 0ᵃ ∎ - +open import Haskell.Law.Num.Nat public +open import Haskell.Law.Num.Word public diff --git a/lib/Haskell/Law/Num/Def.agda b/lib/Haskell/Law/Num/Def.agda index 16365819..7753542f 100644 --- a/lib/Haskell/Law/Num/Def.agda +++ b/lib/Haskell/Law/Num/Def.agda @@ -31,3 +31,96 @@ record IsLawfulNum (a : Set) ⦃ iNum : Num a ⦄ : Set₁ where -- We are currently missing the following because toInteger is missing in our Prelude. -- "if the type also implements Integral, then fromInteger is a left inverse for toInteger, i.e. fromInteger (toInteger i) == i" open IsLawfulNum ⦃ ... ⦄ public + +open import Haskell.Prim.Function +open import Haskell.Law.Equality +open import Haskell.Law.Function + +{-| +A number homomorphism establishes a homomorphism from one Num type a to another one b. +In particular, zero and one are mapped to zero and one in the other Num type, +and addition, multiplication, and negation are homorphic. +-} +record NumHomomorphism (a b : Set) ⦃ iNuma : Num a ⦄ ⦃ iNumb : Num b ⦄ (φ : a → b) : Set where + 0ᵃ = Num.fromInteger iNuma (pos 0) + 0ᵇ = Num.fromInteger iNumb (pos 0) + 1ᵃ = Num.fromInteger iNuma (pos 1) + 1ᵇ = Num.fromInteger iNumb (pos 1) + + field + +-hom : Homomorphism₂ _+_ _+_ φ + *-hom : Homomorphism₂ _*_ _*_ φ + ⦃ minus-ok ⦄ : ∀ {x y : a} → ⦃ MinusOK x y ⦄ → MinusOK (φ x) (φ y) + ⦃ negate-ok ⦄ : ∀ {x : a} → ⦃ NegateOK x ⦄ → NegateOK (φ x) + ⦃ fromInteger-ok ⦄ : ∀ {i : Integer} → ⦃ Num.FromIntegerOK iNuma i ⦄ → Num.FromIntegerOK iNumb i + 0-hom : ⦃ @0 _ : Num.FromIntegerOK iNuma (pos 0) ⦄ → φ 0ᵃ ≡ 0ᵇ + 1-hom : ⦃ @0 _ : Num.FromIntegerOK iNuma (pos 1) ⦄ → φ 1ᵃ ≡ 1ᵇ + negate-hom : ∀ (x : a) → ⦃ @0 _ : Num.NegateOK iNuma x ⦄ → φ (negate x) ≡ negate (φ x) --Homomorphism₁ inlined for type instances + +{-| +A number embedding is an invertible number homomorphism. +-} +record NumEmbedding (a b : Set) ⦃ iNuma : Num a ⦄ ⦃ iNumb : Num b ⦄ (φ : a → b) (φ⁻¹ : b → a) : Set where + field + hom : NumHomomorphism a b φ + embed : φ⁻¹ ∘ φ ≗ id + + open NumHomomorphism hom + + +-Embedding₂ : Embedding₂ _+_ _+_ φ φ⁻¹ + Embedding₂.hom +-Embedding₂ = +-hom + Embedding₂.embed +-Embedding₂ = embed + + *-Embedding₂ : Embedding₂ _*_ _*_ φ φ⁻¹ + Embedding₂.hom *-Embedding₂ = *-hom + Embedding₂.embed *-Embedding₂ = embed + + +-MonoidEmbedding₂ : ⦃ @0 _ : Num.FromIntegerOK iNuma (pos 0) ⦄ → MonoidEmbedding₂ _+_ _+_ φ φ⁻¹ 0ᵃ 0ᵇ + MonoidEmbedding₂.embedding +-MonoidEmbedding₂ = +-Embedding₂ + MonoidEmbedding₂.0-hom +-MonoidEmbedding₂ = 0-hom + + *-MonoidEmbedding₂ : ⦃ @0 _ : Num.FromIntegerOK iNuma (pos 1) ⦄ → MonoidEmbedding₂ _*_ _*_ φ φ⁻¹ 1ᵃ 1ᵇ + MonoidEmbedding₂.embedding *-MonoidEmbedding₂ = *-Embedding₂ + MonoidEmbedding₂.0-hom *-MonoidEmbedding₂ = 1-hom + +{-| +Given an embedding from one number type a onto another one b, +we can conclude that b satisfies the laws of Num if a satisfies the +laws of Num. +-} +map-IsLawfulNum : ∀ {a b : Set} ⦃ iNuma : Num a ⦄ ⦃ iNumb : Num b ⦄ + → (a2b : a → b) (b2a : b → a) + → NumEmbedding a b a2b b2a + → IsLawfulNum b + ----------------------- + → IsLawfulNum a +map-IsLawfulNum {a} {b} {{numa}} {{numb}} f g proj lawb = + record + { +-assoc = map-assoc _+ᵃ_ _+ᵇ_ f g +-Embedding₂ (+-assoc lawb) + ; +-comm = map-comm _+ᵃ_ _+ᵇ_ f g +-Embedding₂ (+-comm lawb) + ; +-idˡ = λ x → map-idˡ _+ᵃ_ _+ᵇ_ f g 0ᵃ 0ᵇ +-MonoidEmbedding₂ (λ y → +-idˡ lawb y) x + ; +-idʳ = λ x → map-idʳ _+ᵃ_ _+ᵇ_ f g 0ᵃ 0ᵇ +-MonoidEmbedding₂ (λ y → +-idʳ lawb y) x + ; neg-inv = map-neg-inv + ; *-assoc = map-assoc _*ᵃ_ _*ᵇ_ f g *-Embedding₂ (*-assoc lawb) + ; *-idˡ = λ x → map-idˡ _*ᵃ_ _*ᵇ_ f g 1ᵃ 1ᵇ *-MonoidEmbedding₂ (λ y → *-idˡ lawb y) x + ; *-idʳ = λ x → map-idʳ _*ᵃ_ _*ᵇ_ f g 1ᵃ 1ᵇ *-MonoidEmbedding₂ (λ y → *-idʳ lawb y) x + ; distributeˡ = map-distributeˡ _+ᵃ_ _+ᵇ_ _*ᵃ_ _*ᵇ_ f g embed +-hom *-hom (distributeˡ lawb) + ; distributeʳ = map-distributeʳ _+ᵃ_ _+ᵇ_ _*ᵃ_ _*ᵇ_ f g embed +-hom *-hom (distributeʳ lawb) + } + where + open NumEmbedding proj + open NumHomomorphism hom + open IsLawfulNum lawb + open Num numa renaming (_+_ to _+ᵃ_; _*_ to _*ᵃ_; negate to negateᵃ) + open Num numb renaming (_+_ to _+ᵇ_; _*_ to _*ᵇ_; negate to negateᵇ) + + map-neg-inv : ∀ (x : a) ⦃ @0 _ : Num.FromIntegerOK numa (pos 0) ⦄ ⦃ @0 _ : Num.NegateOK numa x ⦄ + → x +ᵃ negateᵃ x ≡ 0ᵃ + map-neg-inv x = + x +ᵃ negateᵃ x ≡˘⟨ embed (x +ᵃ negateᵃ x) ⟩ + g (f (x +ᵃ negateᵃ x)) ≡⟨ cong g (+-hom x (negateᵃ x)) ⟩ + g (f x +ᵇ f (negateᵃ x)) ≡⟨ cong g (cong (f x +ᵇ_) (negate-hom x)) ⟩ + g (f x +ᵇ negateᵇ (f x)) ≡⟨ cong g (neg-inv lawb (f x)) ⟩ + g 0ᵇ ≡˘⟨ cong g 0-hom ⟩ + g (f 0ᵃ) ≡⟨ embed 0ᵃ ⟩ + 0ᵃ ∎ diff --git a/lib/Haskell/Law/Num/Int.agda b/lib/Haskell/Law/Num/Int.agda index 91f617f0..bea98da1 100644 --- a/lib/Haskell/Law/Num/Int.agda +++ b/lib/Haskell/Law/Num/Int.agda @@ -5,7 +5,7 @@ open import Haskell.Prim.Num open import Haskell.Prim.Int open import Haskell.Prim.Word -open import Haskell.Law.Num +open import Haskell.Law.Num.Def open import Haskell.Law.Num.Word instance diff --git a/lib/Haskell/Law/Num/Word.agda b/lib/Haskell/Law/Num/Word.agda index 7e95de01..9af4e289 100644 --- a/lib/Haskell/Law/Num/Word.agda +++ b/lib/Haskell/Law/Num/Word.agda @@ -7,11 +7,13 @@ open import Haskell.Prim.Num open import Haskell.Prim.Word open Haskell.Prim.Word.WordInternal -open import Haskell.Law.Num open import Haskell.Law.Equality open import Haskell.Law.Function open import Haskell.Law.Nat +open import Haskell.Law.Num.Def +open import Haskell.Law.Num.Nat + open Num iNumNat renaming (_+_ to _+ⁿ_; _*_ to _*ⁿ_) open Num iNumWord renaming (_+_ to _+ʷ_; _*_ to _*ʷ_)