blob: 0e465d680f85dca1ef93539b6adf7aef0a829396 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
|
module Problem10 where
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
infixl 15 _⋆_
postulate
C : Set
_⋆_ : C → C → C
_ᵒ : C → C
assoc : ∀ a b c → (a ⋆ b) ⋆ c ≡ a ⋆ (b ⋆ c)
ᵒ-prop : ∀ a → a ⋆ a ᵒ ⋆ a ≡ a
_ᶜ : C → C
x ᶜ = x ᵒ ⋆ x ⋆ x ᵒ
prop₁ : ∀ a → a ⋆ a ᶜ ⋆ a ≡ a
prop₁ a = begin
a ⋆ (a ᵒ ⋆ a ⋆ a ᵒ) ⋆ a ≡˘⟨ cong (_⋆ a) (assoc a (a ᵒ ⋆ a) (a ᵒ)) ⟩
a ⋆ (a ᵒ ⋆ a) ⋆ a ᵒ ⋆ a ≡˘⟨ cong (λ - → - ⋆ a ᵒ ⋆ a) (assoc a (a ᵒ) a) ⟩
a ⋆ a ᵒ ⋆ a ⋆ a ᵒ ⋆ a ≡⟨ cong (λ - → - ⋆ a ᵒ ⋆ a) (ᵒ-prop a) ⟩
a ⋆ a ᵒ ⋆ a ≡⟨ ᵒ-prop a ⟩
a ∎
prop₂ : ∀ a → a ᶜ ⋆ a ⋆ a ᶜ ≡ a ᶜ
prop₂ a = begin
a ᵒ ⋆ a ⋆ a ᵒ ⋆ a ⋆ (a ᵒ ⋆ a ⋆ a ᵒ) ≡˘⟨ assoc (a ᵒ ⋆ a ⋆ a ᵒ ⋆ a) (a ᵒ ⋆ a) (a ᵒ) ⟩
a ᵒ ⋆ a ⋆ a ᵒ ⋆ a ⋆ (a ᵒ ⋆ a) ⋆ a ᵒ ≡˘⟨ cong (_⋆ a ᵒ) (assoc (a ᵒ ⋆ a ⋆ a ᵒ ⋆ a) (a ᵒ) a) ⟩
a ᵒ ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ ≡⟨ cong (λ - → - ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ) (assoc (a ᵒ) a (a ᵒ)) ⟩
a ᵒ ⋆ (a ⋆ a ᵒ) ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ ≡⟨ cong (λ - → - ⋆ a ᵒ ⋆ a ⋆ a ᵒ) (assoc (a ᵒ) (a ⋆ a ᵒ) a) ⟩
a ᵒ ⋆ (a ⋆ a ᵒ ⋆ a) ⋆ a ᵒ ⋆ a ⋆ a ᵒ ≡⟨ cong (λ - → a ᵒ ⋆ - ⋆ a ᵒ ⋆ a ⋆ a ᵒ) (ᵒ-prop a) ⟩
a ᵒ ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ ≡⟨ cong (λ - → - ⋆ a ⋆ a ᵒ) (assoc (a ᵒ) a (a ᵒ)) ⟩
a ᵒ ⋆ (a ⋆ a ᵒ) ⋆ a ⋆ a ᵒ ≡⟨ cong (_⋆ (a ᵒ)) (assoc (a ᵒ) (a ⋆ a ᵒ) a) ⟩
a ᵒ ⋆ (a ⋆ a ᵒ ⋆ a) ⋆ a ᵒ ≡⟨ cong (λ - → a ᵒ ⋆ - ⋆ a ᵒ) (ᵒ-prop a) ⟩
a ᵒ ⋆ a ⋆ a ᵒ ∎
postulate
commute : ∀ a b → a ⋆ a ≡ a → b ⋆ b ≡ b → a ⋆ b ≡ b ⋆ a
uniqueness : ∀ a z → a ⋆ z ⋆ a ≡ a
→ z ⋆ a ⋆ z ≡ z
→ z ≡ a ᶜ
uniqueness a z aza≡a zaz≡z = begin
z ≡˘⟨ zaz≡z ⟩
z ⋆ a ⋆ z ≡˘⟨ cong (λ - → z ⋆ - ⋆ z) (ᵒ-prop a) ⟩
z ⋆ (a ⋆ a ᵒ ⋆ a) ⋆ z ≡˘⟨ cong (_⋆ z) (assoc z (a ⋆ a ᵒ) a) ⟩
z ⋆ (a ⋆ a ᵒ) ⋆ a ⋆ z ≡⟨ assoc (z ⋆ (a ⋆ a ᵒ)) a z ⟩
z ⋆ (a ⋆ a ᵒ) ⋆ (a ⋆ z) ≡⟨ assoc z (a ⋆ a ᵒ) (a ⋆ z) ⟩
z ⋆ ((a ⋆ a ᵒ) ⋆ (a ⋆ z)) ≡⟨ cong (z ⋆_) (commute (a ⋆ a ᵒ) (a ⋆ z) aaᵒaaᵒ≡aaᵒ azaz≡az) ⟩
z ⋆ ((a ⋆ z) ⋆ (a ⋆ a ᵒ)) ≡˘⟨ assoc z (a ⋆ z) (a ⋆ a ᵒ) ⟩
z ⋆ (a ⋆ z) ⋆ (a ⋆ a ᵒ) ≡˘⟨ cong (_⋆ (a ⋆ a ᵒ)) (assoc z a z) ⟩
z ⋆ a ⋆ z ⋆ (a ⋆ a ᵒ) ≡⟨ cong (_⋆ (a ⋆ a ᵒ)) zaz≡z ⟩
z ⋆ (a ⋆ a ᵒ) ≡˘⟨ assoc z a (a ᵒ) ⟩
z ⋆ a ⋆ a ᵒ ≡˘⟨ cong (λ - → z ⋆ - ⋆ (a ᵒ)) (ᵒ-prop a) ⟩
z ⋆ (a ⋆ a ᵒ ⋆ a) ⋆ a ᵒ ≡˘⟨ cong (_⋆ a ᵒ) (assoc z (a ⋆ a ᵒ) a) ⟩
z ⋆ (a ⋆ a ᵒ) ⋆ a ⋆ a ᵒ ≡˘⟨ cong (λ - → - ⋆ a ⋆ a ᵒ) (assoc z a (a ᵒ)) ⟩
z ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ ≡⟨ cong (_⋆ a ᵒ) (assoc (z ⋆ a) (a ᵒ) a) ⟩
z ⋆ a ⋆ (a ᵒ ⋆ a) ⋆ a ᵒ ≡⟨ cong (_⋆ a ᵒ) (commute (z ⋆ a) (a ᵒ ⋆ a) zaza≡za aᵒaaᵒa≡aᵒa) ⟩
a ᵒ ⋆ a ⋆ (z ⋆ a) ⋆ a ᵒ ≡˘⟨ cong (_⋆ a ᵒ) (assoc (a ᵒ ⋆ a) z a) ⟩
a ᵒ ⋆ a ⋆ z ⋆ a ⋆ a ᵒ ≡⟨ cong (λ - → - ⋆ a ⋆ a ᵒ) (assoc (a ᵒ) a z) ⟩
a ᵒ ⋆ (a ⋆ z) ⋆ a ⋆ a ᵒ ≡⟨ cong (_⋆ a ᵒ) (assoc (a ᵒ) (a ⋆ z) a) ⟩
a ᵒ ⋆ (a ⋆ z ⋆ a) ⋆ a ᵒ ≡⟨ cong (λ - → a ᵒ ⋆ - ⋆ a ᵒ) aza≡a ⟩
a ᵒ ⋆ a ⋆ a ᵒ ∎
where
zaza≡za : z ⋆ a ⋆ (z ⋆ a) ≡ z ⋆ a
zaza≡za = begin
z ⋆ a ⋆ (z ⋆ a) ≡˘⟨ assoc (z ⋆ a) z a ⟩
z ⋆ a ⋆ z ⋆ a ≡⟨ cong (_⋆ a) zaz≡z ⟩
z ⋆ a ∎
azaz≡az : a ⋆ z ⋆ (a ⋆ z) ≡ a ⋆ z
azaz≡az = begin
a ⋆ z ⋆ (a ⋆ z) ≡˘⟨ assoc (a ⋆ z) a z ⟩
a ⋆ z ⋆ a ⋆ z ≡⟨ cong (_⋆ z) aza≡a ⟩
a ⋆ z ∎
aᵒaaᵒa≡aᵒa : a ᵒ ⋆ a ⋆ (a ᵒ ⋆ a) ≡ a ᵒ ⋆ a
aᵒaaᵒa≡aᵒa = begin
a ᵒ ⋆ a ⋆ (a ᵒ ⋆ a) ≡⟨ assoc (a ᵒ) a (a ᵒ ⋆ a) ⟩
a ᵒ ⋆ (a ⋆ (a ᵒ ⋆ a)) ≡˘⟨ cong (a ᵒ ⋆_) (assoc a (a ᵒ) a) ⟩
a ᵒ ⋆ (a ⋆ a ᵒ ⋆ a) ≡⟨ cong (a ᵒ ⋆_) (ᵒ-prop a) ⟩
a ᵒ ⋆ a ∎
aaᵒaaᵒ≡aaᵒ : a ⋆ a ᵒ ⋆ (a ⋆ a ᵒ) ≡ a ⋆ a ᵒ
aaᵒaaᵒ≡aaᵒ = begin
a ⋆ a ᵒ ⋆ (a ⋆ a ᵒ) ≡˘⟨ assoc (a ⋆ a ᵒ) a (a ᵒ) ⟩
a ⋆ a ᵒ ⋆ a ⋆ a ᵒ ≡⟨ cong (_⋆ a ᵒ) (ᵒ-prop a) ⟩
a ⋆ a ᵒ ∎
|
