Skip to content

Commit 92b278b

Browse files
committed
One line proof
1 parent b219694 commit 92b278b

File tree

1 file changed

+10
-34
lines changed

1 file changed

+10
-34
lines changed

src/Algebra/Properties/Monoid/Reasoning.agda

Lines changed: 10 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -13,20 +13,17 @@ open import Algebra.Structures using (IsMagma)
1313
module Algebra.Properties.Monoid.Reasoning {o ℓ} (M : Monoid o ℓ) where
1414

1515
open Monoid M
16-
using (Carrier; _∙_; _≈_; setoid; isMagma; semigroup; ε; sym; identityˡ; identityʳ
17-
; ∙-cong; refl; assoc; ∙-congˡ; ∙-congʳ)
16+
using (Carrier; _∙_; _≈_; setoid; isMagma; semigroup; ε; sym; identityˡ
17+
; identityʳ ; ∙-cong; refl; assoc; ∙-congˡ; ∙-congʳ; trans)
1818
open import Relation.Binary.Reasoning.Setoid setoid
1919
open import Algebra.Properties.Semigroup.Reasoning semigroup public
2020

2121
module Identity {a : Carrier } where
2222
id-unique : ( b b ∙ a ≈ b) a ≈ ε
23-
id-unique b∙a≈b = trans (sym (identityˡ a) ) (b∙a≈b ε)
23+
id-unique b∙a≈b = trans (sym (identityˡ a)) (b∙a≈b ε)
2424

2525
id-comm : a ∙ ε ≈ ε ∙ a
26-
id-comm = begin
27-
a ∙ ε ≈⟨ identityʳ a ⟩
28-
a ≈⟨ sym (identityˡ a)⟩
29-
ε ∙ a ∎
26+
id-comm = trans (identityʳ a) (sym (identityˡ a))
3027

3128
id-comm-sym : ε ∙ a ≈ a ∙ ε
3229
id-comm-sym = sym id-comm
@@ -35,16 +32,10 @@ open Identity public
3532

3633
module IntroElim {a b : Carrier} (a≈ε : a ≈ ε) where
3734
elimʳ : b ∙ a ≈ b
38-
elimʳ = begin
39-
b ∙ a ≈⟨ ∙-congˡ a≈ε ⟩
40-
b ∙ ε ≈⟨ identityʳ b ⟩
41-
b ∎
35+
elimʳ = trans (∙-congˡ a≈ε) (identityʳ b)
4236

4337
elimˡ : a ∙ b ≈ b
44-
elimˡ = begin
45-
a ∙ b ≈⟨ ∙-congʳ a≈ε ⟩
46-
ε ∙ b ≈⟨ identityˡ b ⟩
47-
b ∎
38+
elimˡ = trans (∙-congʳ a≈ε) (identityˡ b)
4839

4940
introʳ : a ≈ ε b ≈ b ∙ a
5041
introʳ a≈ε = sym elimʳ
@@ -53,29 +44,17 @@ module IntroElim {a b : Carrier} (a≈ε : a ≈ ε) where
5344
introˡ a≈ε = sym elimˡ
5445

5546
introcenter : c b ∙ c ≈ b ∙ (a ∙ c)
56-
introcenter c = begin
57-
b ∙ c ≈⟨ ∙-congˡ (identityˡ c) ⟨
58-
b ∙ (ε ∙ c) ≈⟨ ∙-congˡ (∙-congʳ a≈ε) ⟨
59-
b ∙ (a ∙ c) ∎
47+
introcenter c = trans (∙-congˡ (sym (identityˡ c))) (∙-congˡ (∙-congʳ (sym a≈ε)))
6048

6149
open IntroElim public
6250

6351
module Cancellers {a b c : Carrier} (inv : a ∙ c ≈ ε) where
6452

6553
cancelʳ : (b ∙ a) ∙ c ≈ b
66-
cancelʳ = begin
67-
(b ∙ a) ∙ c ≈⟨ assoc b a c ⟩
68-
b ∙ (a ∙ c) ≈⟨ ∙-congˡ inv ⟩
69-
b ∙ ε ≈⟨ identityʳ b ⟩
70-
b ∎
71-
54+
cancelʳ = trans (assoc b a c) (trans (∙-congˡ inv) (identityʳ b))
7255

7356
cancelˡ : a ∙ (c ∙ b) ≈ b
74-
cancelˡ = begin
75-
a ∙ (c ∙ b) ≈⟨ assoc a c b ⟨
76-
(a ∙ c) ∙ b ≈⟨ ∙-congʳ inv ⟩
77-
ε ∙ b ≈⟨ identityˡ b ⟩
78-
b ∎
57+
cancelˡ = trans (sym (assoc a c b)) (trans (∙-congʳ inv) (identityˡ b))
7958

8059
insertˡ : b ≈ a ∙ (c ∙ b)
8160
insertˡ = sym cancelˡ
@@ -84,10 +63,7 @@ module Cancellers {a b c : Carrier} (inv : a ∙ c ≈ ε) where
8463
insertʳ = sym cancelʳ
8564

8665
cancelInner : {g} (b ∙ a) ∙ (c ∙ g) ≈ b ∙ g
87-
cancelInner {g = g} = begin
88-
(b ∙ a) ∙ (c ∙ g) ≈⟨ assoc (b ∙ a) c g ⟨
89-
((b ∙ a) ∙ c) ∙ g ≈⟨ ∙-congʳ cancelʳ ⟩
90-
b ∙ g ∎
66+
cancelInner {g = g} = trans (sym (assoc (b ∙ a) c g)) (∙-congʳ cancelʳ)
9167

9268
insertInner : {g} b ∙ g ≈ (b ∙ a) ∙ (c ∙ g)
9369
insertInner = sym cancelInner

0 commit comments

Comments
 (0)