~ubuntu-branches/ubuntu/lucid/agda-stdlib/lucid

« back to all changes in this revision

Viewing changes to src/Algebra/Props/AbelianGroup.agda

• browse files at revision 1
• compare with another revision
• download diff
• download tarball
• view history from revision 1

Show diffs side-by-side

added

removed

src/Algebra/Props/AbelianGroup.agda

 

1

------------------------------------------------------------------------

 

2

-- Some derivable properties

 

3

------------------------------------------------------------------------

 

4

 

 

5

open import Algebra

 

6

 

 

7

module Algebra.Props.AbelianGroup (g : AbelianGroup) where

 

8

 

 

9

open AbelianGroup g

 

10

import Relation.Binary.EqReasoning as EqR; open EqR setoid

 

11

open import Data.Function

 

12

open import Data.Product

 

13

 

 

14

private

 

15

  lemma : ∀ x y → x ∙ y ∙ x ⁻¹ ≈ y

 

16

  lemma x y = begin

 

17

    x ∙ y ∙ x ⁻¹    ≈⟨ comm _ _ ⟨ ∙-cong ⟩ refl ⟩

 

18

    y ∙ x ∙ x ⁻¹    ≈⟨ assoc _ _ _ ⟩

 

19

    y ∙ (x ∙ x ⁻¹)  ≈⟨ refl ⟨ ∙-cong ⟩ proj₂ inverse _ ⟩

 

20

    y ∙ ε           ≈⟨ proj₂ identity _ ⟩

 

21

    y               ∎

 

22

 

 

23

-‿∙-comm : ∀ x y → x ⁻¹ ∙ y ⁻¹ ≈ (x ∙ y) ⁻¹

 

24

-‿∙-comm x y = begin

 

25

  x ⁻¹ ∙ y ⁻¹                         ≈⟨ comm _ _ ⟩

 

26

  y ⁻¹ ∙ x ⁻¹                         ≈⟨ sym $ lem ⟨ ∙-cong ⟩ refl ⟩

 

27

  x ∙ (y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹) ∙ x ⁻¹  ≈⟨ lemma _ _ ⟩

 

28

  y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹               ≈⟨ lemma _ _ ⟩

 

29

  (x ∙ y) ⁻¹                          ∎

 

30

  where

 

31

  lem = begin

 

32

    x ∙ (y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹)  ≈⟨ sym $ assoc _ _ _ ⟩

 

33

    x ∙ (y ∙ (x ∙ y) ⁻¹) ∙ y ⁻¹  ≈⟨ sym $ assoc _ _ _ ⟨ ∙-cong ⟩ refl ⟩

 

34

    x ∙ y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹    ≈⟨ proj₂ inverse _ ⟨ ∙-cong ⟩ refl ⟩

 

35

    ε ∙ y ⁻¹                     ≈⟨ proj₁ identity _ ⟩

 

36

    y ⁻¹                         ∎

• Older »

Loggerhead is a web-based interface for Breezy
Version: 2.0.1