------------------------------------------------------------------------
-- The Agda standard library
--
-- Some properties about parities
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Parity.Properties where
open import Algebra.Bundles
open import Data.Nat.Base as ℕ using (zero; suc; parity)
open import Data.Parity.Base as ℙ using (Parity; 0ℙ; 1ℙ; _⁻¹; toSign; fromSign)
open import Data.Product.Base using (_,_)
open import Data.Sign.Base as 𝕊
using (Sign; +; -; _*_; opposite; *-rawMagma; *-1-rawMonoid; *-1-rawGroup)
open import Function.Base using (_$_; id)
open import Function.Definitions
using (Injective; Surjective; Inverseʳ; Inverseˡ)
open import Function.Consequences.Propositional
using (inverseʳ⇒injective; inverseˡ⇒surjective)
open import Level using (0ℓ)
open import Relation.Binary
using (Decidable; DecidableEquality; Setoid; DecSetoid; IsDecEquivalence)
open import Relation.Binary.PropositionalEquality.Core
using (_≡_; _≢_; refl; sym; cong; cong₂)
open import Relation.Binary.PropositionalEquality.Properties
using (module ≡-Reasoning; setoid; isEquivalence; decSetoid; isDecEquivalence)
open import Relation.Nullary.Decidable.Core using (yes; no)
open import Relation.Nullary.Negation.Core using (contradiction)
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ʳ)
open import Algebra.Morphism.Structures
------------------------------------------------------------------------
-- Equality
infix 4 _≟_
_≟_ : DecidableEquality Parity
1ℙ ≟ 1ℙ = yes refl
1ℙ ≟ 0ℙ = no λ()
0ℙ ≟ 1ℙ = no λ()
0ℙ ≟ 0ℙ = yes refl
≡-setoid : Setoid 0ℓ 0ℓ
≡-setoid = setoid Parity
≡-decSetoid : DecSetoid 0ℓ 0ℓ
≡-decSetoid = decSetoid _≟_
≡-isDecEquivalence : IsDecEquivalence _≡_
≡-isDecEquivalence = isDecEquivalence _≟_
------------------------------------------------------------------------
-- _⁻¹
-- Algebraic properties of _⁻¹
⁻¹-selfInverse : SelfInverse _⁻¹
⁻¹-selfInverse { 1ℙ } { 0ℙ } refl = refl
⁻¹-selfInverse { 0ℙ } { 1ℙ } refl = refl
⁻¹-involutive : Involutive _⁻¹
⁻¹-involutive = selfInverse⇒involutive ⁻¹-selfInverse
⁻¹-injective : Injective _≡_ _≡_ _⁻¹
⁻¹-injective = selfInverse⇒injective ⁻¹-selfInverse
------------------------------------------------------------------------
-- other properties of _⁻¹
p≢p⁻¹ : ∀ p → p ≢ p ⁻¹
p≢p⁻¹ 1ℙ ()
p≢p⁻¹ 0ℙ ()
------------------------------------------------------------------------
-- ⁻¹ and _+_
p+p⁻¹≡1ℙ : ∀ p → p ℙ.+ p ⁻¹ ≡ 1ℙ
p+p⁻¹≡1ℙ 0ℙ = refl
p+p⁻¹≡1ℙ 1ℙ = refl
p⁻¹+p≡1ℙ : ∀ p → p ⁻¹ ℙ.+ p ≡ 1ℙ
p⁻¹+p≡1ℙ 0ℙ = refl
p⁻¹+p≡1ℙ 1ℙ = refl
------------------------------------------------------------------------
-- ⁻¹ and _*_
p*p⁻¹≡0ℙ : ∀ p → p ℙ.* p ⁻¹ ≡ 0ℙ
p*p⁻¹≡0ℙ 0ℙ = refl
p*p⁻¹≡0ℙ 1ℙ = refl
p⁻¹*p≡0ℙ : ∀ p → p ⁻¹ ℙ.* p ≡ 0ℙ
p⁻¹*p≡0ℙ 0ℙ = refl
p⁻¹*p≡0ℙ 1ℙ = refl
------------------------------------------------------------------------
-- _+_
-- Algebraic properties of _+_
p+p≡0ℙ : ∀ p → p ℙ.+ p ≡ 0ℙ
p+p≡0ℙ 0ℙ = refl
p+p≡0ℙ 1ℙ = refl
+-identityˡ : LeftIdentity 0ℙ ℙ._+_
+-identityˡ _ = refl
+-identityʳ : RightIdentity 0ℙ ℙ._+_
+-identityʳ 1ℙ = refl
+-identityʳ 0ℙ = refl
+-identity : Identity 0ℙ ℙ._+_
+-identity = +-identityˡ , +-identityʳ
+-comm : Commutative ℙ._+_
+-comm 0ℙ 0ℙ = refl
+-comm 0ℙ 1ℙ = refl
+-comm 1ℙ 0ℙ = refl
+-comm 1ℙ 1ℙ = refl
+-assoc : Associative ℙ._+_
+-assoc 0ℙ 0ℙ _ = refl
+-assoc 0ℙ 1ℙ _ = refl
+-assoc 1ℙ 0ℙ _ = refl
+-assoc 1ℙ 1ℙ 0ℙ = refl
+-assoc 1ℙ 1ℙ 1ℙ = refl
+-cancelʳ-≡ : RightCancellative ℙ._+_
+-cancelʳ-≡ _ 1ℙ 1ℙ _ = refl
+-cancelʳ-≡ _ 1ℙ 0ℙ eq = contradiction (sym eq) (p≢p⁻¹ _)
+-cancelʳ-≡ _ 0ℙ 1ℙ eq = contradiction eq (p≢p⁻¹ _)
+-cancelʳ-≡ _ 0ℙ 0ℙ _ = refl
+-cancelˡ-≡ : LeftCancellative ℙ._+_
+-cancelˡ-≡ 1ℙ _ _ eq = ⁻¹-injective eq
+-cancelˡ-≡ 0ℙ _ _ eq = eq
+-cancel-≡ : Cancellative ℙ._+_
+-cancel-≡ = +-cancelˡ-≡ , +-cancelʳ-≡
+-inverse : Inverse 0ℙ id ℙ._+_
+-inverse = p+p≡0ℙ , p+p≡0ℙ
------------------------------------------------------------------------
-- Bundles
+-isMagma : IsMagma ℙ._+_
+-isMagma = record
{ isEquivalence = isEquivalence
; ∙-cong = cong₂ ℙ._+_
}
+-magma : Magma 0ℓ 0ℓ
+-magma = record
{ isMagma = +-isMagma
}
+-isSemigroup : IsSemigroup ℙ._+_
+-isSemigroup = record
{ isMagma = +-isMagma
; assoc = +-assoc
}
+-semigroup : Semigroup 0ℓ 0ℓ
+-semigroup = record
{ isSemigroup = +-isSemigroup
}
+-isCommutativeSemigroup : IsCommutativeSemigroup ℙ._+_
+-isCommutativeSemigroup = record
{ isSemigroup = +-isSemigroup
; comm = +-comm
}
+-commutativeSemigroup : CommutativeSemigroup 0ℓ 0ℓ
+-commutativeSemigroup = record
{ isCommutativeSemigroup = +-isCommutativeSemigroup
}
+-0-isMonoid : IsMonoid ℙ._+_ 0ℙ
+-0-isMonoid = record
{ isSemigroup = +-isSemigroup
; identity = +-identity
}
+-0-monoid : Monoid 0ℓ 0ℓ
+-0-monoid = record
{ isMonoid = +-0-isMonoid
}
+-0-isCommutativeMonoid : IsCommutativeMonoid ℙ._+_ 0ℙ
+-0-isCommutativeMonoid = record
{ isMonoid = +-0-isMonoid
; comm = +-comm
}
+-0-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
+-0-commutativeMonoid = record
{ isCommutativeMonoid = +-0-isCommutativeMonoid
}
+-0-isGroup : IsGroup ℙ._+_ 0ℙ id
+-0-isGroup = record
{ isMonoid = +-0-isMonoid
; inverse = +-inverse
; ⁻¹-cong = id
}
+-0-group : Group 0ℓ 0ℓ
+-0-group = record
{ isGroup = +-0-isGroup
}
+-0-isAbelianGroup : IsAbelianGroup ℙ._+_ 0ℙ id
+-0-isAbelianGroup = record
{ isGroup = +-0-isGroup
; comm = +-comm
}
+-0-abelianGroup : AbelianGroup 0ℓ 0ℓ
+-0-abelianGroup = record
{ isAbelianGroup = +-0-isAbelianGroup
}
------------------------------------------------------------------------
-- _*_
-- Algebraic properties of _*_
*-idem : Idempotent ℙ._*_
*-idem 0ℙ = refl
*-idem 1ℙ = refl
*-comm : Commutative ℙ._*_
*-comm 0ℙ 0ℙ = refl
*-comm 0ℙ 1ℙ = refl
*-comm 1ℙ 0ℙ = refl
*-comm 1ℙ 1ℙ = refl
*-assoc : Associative ℙ._*_
*-assoc 0ℙ 0ℙ _ = refl
*-assoc 0ℙ 1ℙ _ = refl
*-assoc 1ℙ 0ℙ _ = refl
*-assoc 1ℙ 1ℙ 0ℙ = refl
*-assoc 1ℙ 1ℙ 1ℙ = refl
*-distribˡ-+ : ℙ._*_ DistributesOverˡ ℙ._+_
*-distribˡ-+ 0ℙ q r = refl
*-distribˡ-+ 1ℙ 0ℙ 0ℙ = refl
*-distribˡ-+ 1ℙ 0ℙ 1ℙ = refl
*-distribˡ-+ 1ℙ 1ℙ 0ℙ = refl
*-distribˡ-+ 1ℙ 1ℙ 1ℙ = refl
*-distribʳ-+ : ℙ._*_ DistributesOverʳ ℙ._+_
*-distribʳ-+ = comm∧distrˡ⇒distrʳ *-comm *-distribˡ-+
*-distrib-+ : ℙ._*_ DistributesOver ℙ._+_
*-distrib-+ = *-distribˡ-+ , *-distribʳ-+
*-zeroˡ : LeftZero 0ℙ ℙ._*_
*-zeroˡ p = refl
*-zeroʳ : RightZero 0ℙ ℙ._*_
*-zeroʳ p = *-comm p 0ℙ
*-zero : Zero 0ℙ ℙ._*_
*-zero = *-zeroˡ , *-zeroʳ
*-identityˡ : LeftIdentity 1ℙ ℙ._*_
*-identityˡ _ = refl
*-identityʳ : RightIdentity 1ℙ ℙ._*_
*-identityʳ 1ℙ = refl
*-identityʳ 0ℙ = refl
*-identity : Identity 1ℙ ℙ._*_
*-identity = *-identityˡ , *-identityʳ
------------------------------------------------------------------------
-- Structures and Bundles
*-isMagma : IsMagma ℙ._*_
*-isMagma = record
{ isEquivalence = isEquivalence
; ∙-cong = cong₂ ℙ._*_
}
*-magma : Magma 0ℓ 0ℓ
*-magma = record
{ isMagma = *-isMagma
}
*-isSemigroup : IsSemigroup ℙ._*_
*-isSemigroup = record
{ isMagma = *-isMagma
; assoc = *-assoc
}
*-semigroup : Semigroup 0ℓ 0ℓ
*-semigroup = record
{ isSemigroup = *-isSemigroup
}
*-isCommutativeSemigroup : IsCommutativeSemigroup ℙ._*_
*-isCommutativeSemigroup = record
{ isSemigroup = *-isSemigroup
; comm = *-comm
}
*-commutativeSemigroup : CommutativeSemigroup 0ℓ 0ℓ
*-commutativeSemigroup = record
{ isCommutativeSemigroup = *-isCommutativeSemigroup
}
*-1-isMonoid : IsMonoid ℙ._*_ 1ℙ
*-1-isMonoid = record
{ isSemigroup = *-isSemigroup
; identity = *-identity
}
*-1-monoid : Monoid 0ℓ 0ℓ
*-1-monoid = record
{ isMonoid = *-1-isMonoid
}
*-1-isCommutativeMonoid : IsCommutativeMonoid ℙ._*_ 1ℙ
*-1-isCommutativeMonoid = record
{ isMonoid = *-1-isMonoid
; comm = *-comm
}
*-1-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
*-1-commutativeMonoid = record
{ isCommutativeMonoid = *-1-isCommutativeMonoid
}
+-*-isSemiring : IsSemiring ℙ._+_ ℙ._*_ 0ℙ 1ℙ
+-*-isSemiring = record
{ isSemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = +-0-isCommutativeMonoid
; *-cong = cong₂ ℙ._*_
; *-assoc = *-assoc
; *-identity = *-identity
; distrib = *-distrib-+
}
; zero = *-zero
}
+-*-semiring : Semiring 0ℓ 0ℓ
+-*-semiring = record
{ isSemiring = +-*-isSemiring
}
+-*-isCommutativeSemiring : IsCommutativeSemiring ℙ._+_ ℙ._*_ 0ℙ 1ℙ
+-*-isCommutativeSemiring = record
{ isSemiring = +-*-isSemiring
; *-comm = *-comm
}
+-*-commutativeSemiring : CommutativeSemiring 0ℓ 0ℓ
+-*-commutativeSemiring = record
{ isCommutativeSemiring = +-*-isCommutativeSemiring
}
+-*-isRing : IsRing ℙ._+_ ℙ._*_ id 0ℙ 1ℙ
+-*-isRing = record
{ +-isAbelianGroup = +-0-isAbelianGroup
; *-cong = cong₂ ℙ._*_
; *-assoc = *-assoc
; *-identity = *-identity
; distrib = *-distrib-+
}
+-*-ring : Ring 0ℓ 0ℓ
+-*-ring = record
{ isRing = +-*-isRing
}
+-*-isCommutativeRing : IsCommutativeRing ℙ._+_ ℙ._*_ id 0ℙ 1ℙ
+-*-isCommutativeRing = record
{ isRing = +-*-isRing
; *-comm = *-comm
}
+-*-commutativeRing : CommutativeRing 0ℓ 0ℓ
+-*-commutativeRing = record
{ isCommutativeRing = +-*-isCommutativeRing
}
------------------------------------------------------------------------
-- relating Parity and Sign
+-homo-* : ∀ p q → toSign (p ℙ.+ q) ≡ (toSign p) 𝕊.* (toSign q)
+-homo-* 0ℙ 0ℙ = refl
+-homo-* 0ℙ 1ℙ = refl
+-homo-* 1ℙ 0ℙ = refl
+-homo-* 1ℙ 1ℙ = refl
⁻¹-homo-opposite : ∀ p → toSign (p ⁻¹) ≡ 𝕊.opposite (toSign p)
⁻¹-homo-opposite 0ℙ = refl
⁻¹-homo-opposite 1ℙ = refl
toSign-inverseʳ : Inverseʳ _≡_ _≡_ toSign fromSign
toSign-inverseʳ {0ℙ} refl = refl
toSign-inverseʳ {1ℙ} refl = refl
toSign-inverseˡ : Inverseˡ _≡_ _≡_ toSign fromSign
toSign-inverseˡ { 𝕊.+ } refl = refl
toSign-inverseˡ { 𝕊.- } refl = refl
toSign-injective : Injective _≡_ _≡_ toSign
toSign-injective = inverseʳ⇒injective toSign toSign-inverseʳ
toSign-surjective : Surjective _≡_ _≡_ toSign
toSign-surjective = inverseˡ⇒surjective toSign-inverseˡ
toSign-isMagmaHomomorphism : IsMagmaHomomorphism ℙ.+-rawMagma 𝕊.*-rawMagma toSign
toSign-isMagmaHomomorphism = record
{ isRelHomomorphism = record
{ cong = cong toSign }
; homo = +-homo-*
}
toSign-isMagmaMonomorphism : IsMagmaMonomorphism ℙ.+-rawMagma 𝕊.*-rawMagma toSign
toSign-isMagmaMonomorphism = record
{ isMagmaHomomorphism = toSign-isMagmaHomomorphism
; injective = toSign-injective
}
toSign-isMagmaIsomorphism : IsMagmaIsomorphism ℙ.+-rawMagma 𝕊.*-rawMagma toSign
toSign-isMagmaIsomorphism = record
{ isMagmaMonomorphism = toSign-isMagmaMonomorphism
; surjective = toSign-surjective
}
toSign-isMonoidHomomorphism : IsMonoidHomomorphism ℙ.+-0-rawMonoid 𝕊.*-1-rawMonoid toSign
toSign-isMonoidHomomorphism = record
{ isMagmaHomomorphism = toSign-isMagmaHomomorphism
; ε-homo = refl
}
toSign-isMonoidMonomorphism : IsMonoidMonomorphism ℙ.+-0-rawMonoid 𝕊.*-1-rawMonoid toSign
toSign-isMonoidMonomorphism = record
{ isMonoidHomomorphism = toSign-isMonoidHomomorphism
; injective = toSign-injective
}
toSign-isMonoidIsomorphism : IsMonoidIsomorphism ℙ.+-0-rawMonoid 𝕊.*-1-rawMonoid toSign
toSign-isMonoidIsomorphism = record
{ isMonoidMonomorphism = toSign-isMonoidMonomorphism
; surjective = toSign-surjective
}
toSign-isGroupHomomorphism : IsGroupHomomorphism ℙ.+-0-rawGroup 𝕊.*-1-rawGroup toSign
toSign-isGroupHomomorphism = record
{ isMonoidHomomorphism = toSign-isMonoidHomomorphism
; ⁻¹-homo = ⁻¹-homo-opposite
}
toSign-isGroupMonomorphism : IsGroupMonomorphism ℙ.+-0-rawGroup 𝕊.*-1-rawGroup toSign
toSign-isGroupMonomorphism = record
{ isGroupHomomorphism = toSign-isGroupHomomorphism
; injective = toSign-injective
}
toSign-isGroupIsomorphism : IsGroupIsomorphism ℙ.+-0-rawGroup 𝕊.*-1-rawGroup toSign
toSign-isGroupIsomorphism = record
{ isGroupMonomorphism = toSign-isGroupMonomorphism
; surjective = toSign-surjective
}
------------------------------------------------------------------------
-- Relating Nat and Parity
-- successor and (_⁻¹)
suc-homo-⁻¹ : ∀ n → (parity (suc n)) ⁻¹ ≡ parity n
suc-homo-⁻¹ zero = refl
suc-homo-⁻¹ (suc n) = ⁻¹-selfInverse (suc-homo-⁻¹ n)
-- parity is a _+_ homomorphism
+-homo-+ : ∀ m n → parity (m ℕ.+ n) ≡ parity m ℙ.+ parity n
+-homo-+ zero n = refl
+-homo-+ (suc m) n = begin
parity (suc m ℕ.+ n) ≡⟨ suc-+-homo-⁻¹ m n ⟩
(parity m) ⁻¹ ℙ.+ parity n ≡⟨ cong (ℙ._+ parity n) (suc-homo-⁻¹ (suc m)) ⟩
parity (suc m) ℙ.+ parity n ∎
where
open ≡-Reasoning
suc-+-homo-⁻¹ : ∀ m n → parity (suc m ℕ.+ n) ≡ (parity m) ⁻¹ ℙ.+ parity n
suc-+-homo-⁻¹ zero n = sym (suc-homo-⁻¹ (suc n))
suc-+-homo-⁻¹ (suc m) n = begin
parity (suc (suc m) ℕ.+ n) ≡⟨⟩
parity (m ℕ.+ n) ≡⟨ +-homo-+ m n ⟩
parity m ℙ.+ parity n ≡⟨ cong (ℙ._+ parity n) (sym (suc-homo-⁻¹ m)) ⟩
(parity (suc m)) ⁻¹ ℙ.+ parity n ∎
-- parity is a _*_ homomorphism
*-homo-* : ∀ m n → parity (m ℕ.* n) ≡ parity m ℙ.* parity n
*-homo-* zero n = refl
*-homo-* (suc m) n = begin
parity (suc m ℕ.* n) ≡⟨⟩
parity (n ℕ.+ m ℕ.* n) ≡⟨ +-homo-+ n (m ℕ.* n) ⟩
q ℙ.+ parity (m ℕ.* n) ≡⟨ cong (q ℙ.+_) (*-homo-* m n) ⟩
q ℙ.+ (p ℙ.* q) ≡⟨ lemma p q ⟩
(p ⁻¹) ℙ.* q ≡⟨⟩
(parity m) ⁻¹ ℙ.* q ≡⟨ cong (ℙ._* q) (suc-homo-⁻¹ (suc m)) ⟩
parity (suc m) ℙ.* q ≡⟨⟩
parity (suc m) ℙ.* parity n ∎
where
open ≡-Reasoning
p = parity m
q = parity n
-- this lemma simplifies things a lot
lemma : ∀ p q → q ℙ.+ (p ℙ.* q) ≡ (p ⁻¹) ℙ.* q
lemma 0ℙ 0ℙ = refl
lemma 0ℙ 1ℙ = refl
lemma 1ℙ 0ℙ = refl
lemma 1ℙ 1ℙ = refl
------------------------------------------------------------------------
-- parity is a Semiring homomorphism from Nat to Parity
parity-isMagmaHomomorphism : IsMagmaHomomorphism ℕ.+-rawMagma ℙ.+-rawMagma parity
parity-isMagmaHomomorphism = record
{ isRelHomomorphism = record
{ cong = cong parity }
; homo = +-homo-+
}
parity-isMonoidHomomorphism : IsMonoidHomomorphism ℕ.+-0-rawMonoid ℙ.+-0-rawMonoid parity
parity-isMonoidHomomorphism = record
{ isMagmaHomomorphism = parity-isMagmaHomomorphism
; ε-homo = refl
}
parity-isNearSemiringHomomorphism : IsNearSemiringHomomorphism ℕ.+-*-rawNearSemiring ℙ.+-*-rawNearSemiring parity
parity-isNearSemiringHomomorphism = record
{ +-isMonoidHomomorphism = parity-isMonoidHomomorphism
; *-homo = *-homo-*
}
parity-isSemiringHomomorphism : IsSemiringHomomorphism ℕ.+-*-rawSemiring ℙ.+-*-rawSemiring parity
parity-isSemiringHomomorphism = record
{ isNearSemiringHomomorphism = parity-isNearSemiringHomomorphism
; 1#-homo = refl
}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4