diff options
Diffstat (limited to 'src/Problem10.agda')
| -rw-r--r-- | src/Problem10.agda | 89 |
1 files changed, 89 insertions, 0 deletions
diff --git a/src/Problem10.agda b/src/Problem10.agda new file mode 100644 index 0000000..0e465d6 --- /dev/null +++ b/src/Problem10.agda @@ -0,0 +1,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 ᵒ ∎ |