From 021bd4dc6b0d2c00f0f4e38ec3b52e63851c021a Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 24 Jan 2023 18:45:12 +0000 Subject: [PATCH 1/3] self-inverse operation on `Algebra`s and their properties --- CHANGELOG.md | 16 ++++++++++++ src/Algebra/Consequences/Base.agda | 22 +++++++++++----- src/Algebra/Consequences/Setoid.agda | 39 ++++++++++++++++++++++++++++ src/Algebra/Definitions.agda | 3 +++ 4 files changed, 74 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index e56fc6dcd8..ac09dedbb3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1565,8 +1565,22 @@ Other minor changes ``` and their corresponding algebraic subbundles. +* Added new proofs to `Algebra.Consequences.Base`: + ```agda + reflexive+selfinverse⇒involutive : Reflexive _≈_ → + SelfInverse _≈_ f → + Involutive _≈_ f + ``` + * Added new proofs to `Algebra.Consequences.Setoid`: ```agda + involutive⇒surjective : Involutive f → Surjective f + selfinverse⇒congruent : SelfInverse f → Congruent f + selfinverse⇒inverseᵇ : SelfInverse f → Inverseᵇ f f + selfinverse⇒surjective : SelfInverse f → Surjective f + selfinverse⇒injective : SelfInverse f → Injective f + selfinverse⇒bijective : SelfInverse f → Bijective f + comm+idˡ⇒id : Commutative _•_ → LeftIdentity e _•_ → Identity e _•_ comm+idʳ⇒id : Commutative _•_ → RightIdentity e _•_ → Identity e _•_ comm+zeˡ⇒ze : Commutative _•_ → LeftZero e _•_ → Zero e _•_ @@ -1622,6 +1636,8 @@ Other minor changes * Added new definition to `Algebra.Definitions`: ```agda + SelfInverse : Op₁ A → Set _ + LeftDividesˡ : Op₂ A → Op₂ A → Set _ LeftDividesʳ : Op₂ A → Op₂ A → Set _ RightDividesˡ : Op₂ A → Op₂ A → Set _ diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda index 914aaf2cec..200c6db782 100644 --- a/src/Algebra/Consequences/Base.agda +++ b/src/Algebra/Consequences/Base.agda @@ -2,7 +2,7 @@ -- The Agda standard library -- -- Lemmas relating algebraic definitions (such as associativity and --- commutativity) that don't the equality relation to be a setoid. +-- commutativity) that don't require the equality relation to be a setoid. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} @@ -14,9 +14,19 @@ open import Algebra.Core open import Algebra.Definitions open import Data.Sum.Base open import Relation.Binary.Core +open import Relation.Binary.Definitions using (Reflexive) + +module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where + + sel⇒idem : Selective _≈_ _•_ → Idempotent _≈_ _•_ + sel⇒idem sel x with sel x x + ... | inj₁ x•x≈x = x•x≈x + ... | inj₂ x•x≈x = x•x≈x + +module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where + + reflexive+selfinverse⇒involutive : Reflexive _≈_ → + SelfInverse _≈_ f → + Involutive _≈_ f + reflexive+selfinverse⇒involutive refl inv _ = inv refl -sel⇒idem : ∀ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) → - Selective _≈_ _•_ → Idempotent _≈_ _•_ -sel⇒idem _ sel x with sel x x -... | inj₁ x•x≈x = x•x≈x -... | inj₂ x•x≈x = x•x≈x diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda index 11723af49d..2d8857537e 100644 --- a/src/Algebra/Consequences/Setoid.agda +++ b/src/Algebra/Consequences/Setoid.agda @@ -17,6 +17,7 @@ open import Algebra.Definitions _≈_ open import Data.Sum.Base using (inj₁; inj₂) open import Data.Product using (_,_) open import Function.Base using (_$_) +import Function.Definitions as FunDefs import Relation.Binary.Consequences as Bin open import Relation.Binary.Reasoning.Setoid S open import Relation.Unary using (Pred) @@ -28,6 +29,44 @@ open import Relation.Unary using (Pred) open import Algebra.Consequences.Base public +------------------------------------------------------------------------ +-- Involutive/SelfInverse functions + +module _ {f : Op₁ A} (inv : Involutive f) where + + open FunDefs _≈_ _≈_ + + involutive⇒surjective : Surjective f + involutive⇒surjective y = f y , inv y + +module _ {f : Op₁ A} (self : SelfInverse f) where + + inv : Involutive f + inv = reflexive+selfinverse⇒involutive _≈_ refl self + + open FunDefs _≈_ _≈_ + + selfinverse⇒congruent : Congruent f + selfinverse⇒congruent {x} {y} x≈y = sym (self (begin + f (f x) ≈⟨ inv x ⟩ + x ≈⟨ x≈y ⟩ + y ∎)) + + selfinverse⇒inverseᵇ : Inverseᵇ f f + selfinverse⇒inverseᵇ = inv , inv + + selfinverse⇒surjective : Surjective f + selfinverse⇒surjective = involutive⇒surjective inv + + selfinverse⇒injective : Injective f + selfinverse⇒injective {x} {y} x≈y = begin + x ≈˘⟨ self x≈y ⟩ + f (f y) ≈⟨ inv y ⟩ + y ∎ + + selfinverse⇒bijective : Bijective f + selfinverse⇒bijective = selfinverse⇒injective , selfinverse⇒surjective + ------------------------------------------------------------------------ -- Magma-like structures diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda index c2a51fed69..b75b474ce6 100644 --- a/src/Algebra/Definitions.agda +++ b/src/Algebra/Definitions.agda @@ -126,6 +126,9 @@ _∙_ Absorbs _∘_ = ∀ x y → (x ∙ (x ∘ y)) ≈ x Absorptive : Op₂ A → Op₂ A → Set _ Absorptive ∙ ∘ = (∙ Absorbs ∘) × (∘ Absorbs ∙) +SelfInverse : Op₁ A → Set _ +SelfInverse f = ∀ {x y} → f x ≈ y → f y ≈ x + Involutive : Op₁ A → Set _ Involutive f = ∀ x → f (f x) ≈ x From ec59192ba708df365fa9dc68f28945a551e0f7d9 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 24 Jan 2023 19:50:44 +0000 Subject: [PATCH 2/3] TODOs, plus renaming; `CHANGELOG` --- CHANGELOG.md | 1 + src/Algebra/Consequences/Setoid.agda | 8 +++++-- src/Data/Parity/Properties.agda | 34 +++++++++++++++------------- src/Data/Sign/Properties.agda | 22 ++++++++++++++---- 4 files changed, 43 insertions(+), 22 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index ac09dedbb3..5d61141570 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1575,6 +1575,7 @@ Other minor changes * Added new proofs to `Algebra.Consequences.Setoid`: ```agda involutive⇒surjective : Involutive f → Surjective f + selfinverse⇒involutive : SelfInverse f → Involutive f selfinverse⇒congruent : SelfInverse f → Congruent f selfinverse⇒inverseᵇ : SelfInverse f → Inverseᵇ f f selfinverse⇒surjective : SelfInverse f → Surjective f diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda index 2d8857537e..219ac31b14 100644 --- a/src/Algebra/Consequences/Setoid.agda +++ b/src/Algebra/Consequences/Setoid.agda @@ -41,8 +41,12 @@ module _ {f : Op₁ A} (inv : Involutive f) where module _ {f : Op₁ A} (self : SelfInverse f) where - inv : Involutive f - inv = reflexive+selfinverse⇒involutive _≈_ refl self + selfinverse⇒involutive : Involutive f + selfinverse⇒involutive = reflexive+selfinverse⇒involutive _≈_ refl self + + private + + inv = selfinverse⇒involutive open FunDefs _≈_ _≈_ diff --git a/src/Data/Parity/Properties.agda b/src/Data/Parity/Properties.agda index fc5eeb9815..f93776916a 100644 --- a/src/Data/Parity/Properties.agda +++ b/src/Data/Parity/Properties.agda @@ -25,8 +25,8 @@ open import Relation.Nullary using (yes; no) open import Algebra.Structures {A = Parity} _≡_ open import Algebra.Definitions {A = Parity} _≡_ - -open import Algebra.Consequences.Propositional using (comm+distrˡ⇒distrʳ) +open import Algebra.Consequences.Propositional + using (selfinverse⇒involutive; selfinverse⇒injective; comm+distrˡ⇒distrʳ) open import Algebra.Morphism.Structures ------------------------------------------------------------------------ @@ -52,22 +52,24 @@ _≟_ : DecidableEquality Parity ------------------------------------------------------------------------ -- _⁻¹ -p≢p⁻¹ : ∀ p → p ≢ p ⁻¹ -p≢p⁻¹ 1ℙ () -p≢p⁻¹ 0ℙ () +-- Algebraic properties of _⁻¹ + +⁻¹-self-inverse : SelfInverse _⁻¹ +⁻¹-self-inverse { 1ℙ } { 0ℙ } refl = refl +⁻¹-self-inverse { 0ℙ } { 1ℙ } refl = refl -⁻¹-inverts : ∀ {p q} → p ⁻¹ ≡ q → q ⁻¹ ≡ p -⁻¹-inverts { 1ℙ } { 0ℙ } refl = refl -⁻¹-inverts { 0ℙ } { 1ℙ } refl = refl +⁻¹-involutive : Involutive _⁻¹ +⁻¹-involutive = selfinverse⇒involutive ⁻¹-self-inverse -⁻¹-involutive : ∀ p → (p ⁻¹) ⁻¹ ≡ p -⁻¹-involutive p = ⁻¹-inverts refl +⁻¹-injective : Injective _≡_ _≡_ _⁻¹ +⁻¹-injective = selfinverse⇒injective ⁻¹-self-inverse -⁻¹-injective : ∀ {p q} → p ⁻¹ ≡ q ⁻¹ → p ≡ q -⁻¹-injective {p} {q} eq = begin - p ≡⟨ sym (⁻¹-inverts eq) ⟩ - (q ⁻¹) ⁻¹ ≡⟨ ⁻¹-involutive q ⟩ - q ∎ where open ≡-Reasoning +------------------------------------------------------------------------ +-- other properties of _⁻¹ + +p≢p⁻¹ : ∀ p → p ≢ p ⁻¹ +p≢p⁻¹ 1ℙ () +p≢p⁻¹ 0ℙ () ------------------------------------------------------------------------ -- ⁻¹ and _+_ @@ -480,7 +482,7 @@ toSign-isGroupIsomorphism = record suc-homo-⁻¹ : ∀ n → (parity (suc n)) ⁻¹ ≡ parity n suc-homo-⁻¹ zero = refl -suc-homo-⁻¹ (suc n) = ⁻¹-inverts (suc-homo-⁻¹ n) +suc-homo-⁻¹ (suc n) = ⁻¹-self-inverse (suc-homo-⁻¹ n) -- parity is a _+_ homomorphism diff --git a/src/Data/Sign/Properties.agda b/src/Data/Sign/Properties.agda index e9c278e676..004682fa6d 100644 --- a/src/Data/Sign/Properties.agda +++ b/src/Data/Sign/Properties.agda @@ -21,6 +21,8 @@ open import Relation.Nullary.Decidable using (yes; no) open import Algebra.Structures {A = Sign} _≡_ open import Algebra.Definitions {A = Sign} _≡_ +open import Algebra.Consequences.Propositional + using (selfinverse⇒involutive; selfinverse⇒injective) ------------------------------------------------------------------------ -- Equality @@ -45,14 +47,26 @@ _≟_ : DecidableEquality Sign ------------------------------------------------------------------------ -- opposite +-- Algebraic properties of opposite + +opposite-self-inverse : SelfInverse opposite +opposite-self-inverse { - } { + } refl = refl +opposite-self-inverse { + } { - } refl = refl + +opposite-involutive : Involutive opposite +opposite-involutive = selfinverse⇒involutive opposite-self-inverse + +opposite-injective : Injective _≡_ _≡_ opposite +opposite-injective = selfinverse⇒injective opposite-self-inverse + + +------------------------------------------------------------------------ +-- other properties of opposite + s≢opposite[s] : ∀ s → s ≢ opposite s s≢opposite[s] - () s≢opposite[s] + () -opposite-injective : ∀ {s t} → opposite s ≡ opposite t → s ≡ t -opposite-injective { - } { - } refl = refl -opposite-injective { + } { + } refl = refl - ------------------------------------------------------------------------ -- _*_ From 78ae1bd823764302e1d99ba2165fc56f5ca185f7 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 3 Feb 2023 11:20:17 +0000 Subject: [PATCH 3/3] renaming as per Matthew's review --- CHANGELOG.md | 14 +++++++------- src/Algebra/Consequences/Base.agda | 4 ++-- src/Algebra/Consequences/Setoid.agda | 26 +++++++++++++------------- src/Data/Parity/Properties.agda | 14 +++++++------- src/Data/Sign/Properties.agda | 12 ++++++------ 5 files changed, 35 insertions(+), 35 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5d61141570..0d4dec5315 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1567,7 +1567,7 @@ Other minor changes * Added new proofs to `Algebra.Consequences.Base`: ```agda - reflexive+selfinverse⇒involutive : Reflexive _≈_ → + reflexive+selfInverse⇒involutive : Reflexive _≈_ → SelfInverse _≈_ f → Involutive _≈_ f ``` @@ -1575,12 +1575,12 @@ Other minor changes * Added new proofs to `Algebra.Consequences.Setoid`: ```agda involutive⇒surjective : Involutive f → Surjective f - selfinverse⇒involutive : SelfInverse f → Involutive f - selfinverse⇒congruent : SelfInverse f → Congruent f - selfinverse⇒inverseᵇ : SelfInverse f → Inverseᵇ f f - selfinverse⇒surjective : SelfInverse f → Surjective f - selfinverse⇒injective : SelfInverse f → Injective f - selfinverse⇒bijective : SelfInverse f → Bijective f + selfInverse⇒involutive : SelfInverse f → Involutive f + selfInverse⇒congruent : SelfInverse f → Congruent f + selfInverse⇒inverseᵇ : SelfInverse f → Inverseᵇ f f + selfInverse⇒surjective : SelfInverse f → Surjective f + selfInverse⇒injective : SelfInverse f → Injective f + selfInverse⇒bijective : SelfInverse f → Bijective f comm+idˡ⇒id : Commutative _•_ → LeftIdentity e _•_ → Identity e _•_ comm+idʳ⇒id : Commutative _•_ → RightIdentity e _•_ → Identity e _•_ diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda index 200c6db782..440546820b 100644 --- a/src/Algebra/Consequences/Base.agda +++ b/src/Algebra/Consequences/Base.agda @@ -25,8 +25,8 @@ module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where - reflexive+selfinverse⇒involutive : Reflexive _≈_ → + reflexive+selfInverse⇒involutive : Reflexive _≈_ → SelfInverse _≈_ f → Involutive _≈_ f - reflexive+selfinverse⇒involutive refl inv _ = inv refl + reflexive+selfInverse⇒involutive refl inv _ = inv refl diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda index 219ac31b14..37618ff7f7 100644 --- a/src/Algebra/Consequences/Setoid.agda +++ b/src/Algebra/Consequences/Setoid.agda @@ -41,35 +41,35 @@ module _ {f : Op₁ A} (inv : Involutive f) where module _ {f : Op₁ A} (self : SelfInverse f) where - selfinverse⇒involutive : Involutive f - selfinverse⇒involutive = reflexive+selfinverse⇒involutive _≈_ refl self + selfInverse⇒involutive : Involutive f + selfInverse⇒involutive = reflexive+selfInverse⇒involutive _≈_ refl self private - inv = selfinverse⇒involutive + inv = selfInverse⇒involutive open FunDefs _≈_ _≈_ - selfinverse⇒congruent : Congruent f - selfinverse⇒congruent {x} {y} x≈y = sym (self (begin + selfInverse⇒congruent : Congruent f + selfInverse⇒congruent {x} {y} x≈y = sym (self (begin f (f x) ≈⟨ inv x ⟩ x ≈⟨ x≈y ⟩ y ∎)) - selfinverse⇒inverseᵇ : Inverseᵇ f f - selfinverse⇒inverseᵇ = inv , inv + selfInverse⇒inverseᵇ : Inverseᵇ f f + selfInverse⇒inverseᵇ = inv , inv - selfinverse⇒surjective : Surjective f - selfinverse⇒surjective = involutive⇒surjective inv + selfInverse⇒surjective : Surjective f + selfInverse⇒surjective = involutive⇒surjective inv - selfinverse⇒injective : Injective f - selfinverse⇒injective {x} {y} x≈y = begin + selfInverse⇒injective : Injective f + selfInverse⇒injective {x} {y} x≈y = begin x ≈˘⟨ self x≈y ⟩ f (f y) ≈⟨ inv y ⟩ y ∎ - selfinverse⇒bijective : Bijective f - selfinverse⇒bijective = selfinverse⇒injective , selfinverse⇒surjective + selfInverse⇒bijective : Bijective f + selfInverse⇒bijective = selfInverse⇒injective , selfInverse⇒surjective ------------------------------------------------------------------------ -- Magma-like structures diff --git a/src/Data/Parity/Properties.agda b/src/Data/Parity/Properties.agda index f93776916a..74be6c44f5 100644 --- a/src/Data/Parity/Properties.agda +++ b/src/Data/Parity/Properties.agda @@ -26,7 +26,7 @@ open import Relation.Nullary using (yes; no) open import Algebra.Structures {A = Parity} _≡_ open import Algebra.Definitions {A = Parity} _≡_ open import Algebra.Consequences.Propositional - using (selfinverse⇒involutive; selfinverse⇒injective; comm+distrˡ⇒distrʳ) + using (selfInverse⇒involutive; selfInverse⇒injective; comm+distrˡ⇒distrʳ) open import Algebra.Morphism.Structures ------------------------------------------------------------------------ @@ -54,15 +54,15 @@ _≟_ : DecidableEquality Parity -- Algebraic properties of _⁻¹ -⁻¹-self-inverse : SelfInverse _⁻¹ -⁻¹-self-inverse { 1ℙ } { 0ℙ } refl = refl -⁻¹-self-inverse { 0ℙ } { 1ℙ } refl = refl +⁻¹-selfInverse : SelfInverse _⁻¹ +⁻¹-selfInverse { 1ℙ } { 0ℙ } refl = refl +⁻¹-selfInverse { 0ℙ } { 1ℙ } refl = refl ⁻¹-involutive : Involutive _⁻¹ -⁻¹-involutive = selfinverse⇒involutive ⁻¹-self-inverse +⁻¹-involutive = selfInverse⇒involutive ⁻¹-selfInverse ⁻¹-injective : Injective _≡_ _≡_ _⁻¹ -⁻¹-injective = selfinverse⇒injective ⁻¹-self-inverse +⁻¹-injective = selfInverse⇒injective ⁻¹-selfInverse ------------------------------------------------------------------------ -- other properties of _⁻¹ @@ -482,7 +482,7 @@ toSign-isGroupIsomorphism = record suc-homo-⁻¹ : ∀ n → (parity (suc n)) ⁻¹ ≡ parity n suc-homo-⁻¹ zero = refl -suc-homo-⁻¹ (suc n) = ⁻¹-self-inverse (suc-homo-⁻¹ n) +suc-homo-⁻¹ (suc n) = ⁻¹-selfInverse (suc-homo-⁻¹ n) -- parity is a _+_ homomorphism diff --git a/src/Data/Sign/Properties.agda b/src/Data/Sign/Properties.agda index 004682fa6d..24a4d15832 100644 --- a/src/Data/Sign/Properties.agda +++ b/src/Data/Sign/Properties.agda @@ -22,7 +22,7 @@ open import Relation.Nullary.Decidable using (yes; no) open import Algebra.Structures {A = Sign} _≡_ open import Algebra.Definitions {A = Sign} _≡_ open import Algebra.Consequences.Propositional - using (selfinverse⇒involutive; selfinverse⇒injective) + using (selfInverse⇒involutive; selfInverse⇒injective) ------------------------------------------------------------------------ -- Equality @@ -49,15 +49,15 @@ _≟_ : DecidableEquality Sign -- Algebraic properties of opposite -opposite-self-inverse : SelfInverse opposite -opposite-self-inverse { - } { + } refl = refl -opposite-self-inverse { + } { - } refl = refl +opposite-selfInverse : SelfInverse opposite +opposite-selfInverse { - } { + } refl = refl +opposite-selfInverse { + } { - } refl = refl opposite-involutive : Involutive opposite -opposite-involutive = selfinverse⇒involutive opposite-self-inverse +opposite-involutive = selfInverse⇒involutive opposite-selfInverse opposite-injective : Injective _≡_ _≡_ opposite -opposite-injective = selfinverse⇒injective opposite-self-inverse +opposite-injective = selfInverse⇒injective opposite-selfInverse ------------------------------------------------------------------------