← Back

Modules

Leios

  • Abstract
  • Base
  • Blocks
  • Config
  • Defaults
  • FFD
  • Foreign.BaseTypes
  • Foreign.HsTypes
  • Foreign.Types
  • Foreign.Util
  • KeyRegistration
  • Network
  • Prelude
  • Protocol
  • Short
  • Short.Decidable
  • Short.Trace.Verifier
  • Short.Trace.Verifier.Test
  • Simplified
  • Simplified.Deterministic
  • SpecStructure
  • Traces
  • Voting
  • VRF

Network

  • BasicBroadcast
  • Leios
1234567891011121314151617181920212223242526272829303132333435363738394041
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
open import Algebra
 
module Algebra.Properties.AbelianGroup
{a ℓ} (G : AbelianGroup a ℓ) where
 
open AbelianGroup G
open import Function.Base using (_$_)
open import Relation.Binary.Reasoning.Setoid setoid
 
------------------------------------------------------------------------
-- Publicly re-export group properties
 
open import Algebra.Properties.Group group public
 
------------------------------------------------------------------------
-- Properties of abelian groups
 
⁻¹-anti-homo‿- : ∀ x y → (x - y) ⁻¹ ≈ y - x
⁻¹-anti-homo‿- = ⁻¹-anti-homo-//
 
xyx⁻¹≈y : ∀ x y → x ∙ y ∙ x ⁻¹ ≈ y
xyx⁻¹≈y x y = begin
x ∙ y ∙ x ⁻¹ ≈⟨ ∙-congʳ $ comm _ _ ⟩
y ∙ x ∙ x ⁻¹ ≈⟨ assoc _ _ _ ⟩
y ∙ (x ∙ x ⁻¹) ≈⟨ ∙-congˡ $ inverseʳ _ ⟩
y ∙ ε ≈⟨ identityʳ _ ⟩
y ∎
 
⁻¹-∙-comm : ∀ x y → x ⁻¹ ∙ y ⁻¹ ≈ (x ∙ y) ⁻¹
⁻¹-∙-comm x y = begin
x ⁻¹ ∙ y ⁻¹ ≈⟨ ⁻¹-anti-homo-∙ y x ⟨
(y ∙ x) ⁻¹ ≈⟨ ⁻¹-cong $ comm y x ⟩
(x ∙ y) ⁻¹ ∎