Applying rules in Agda

Question

I am new to Agda, and I think I still have a problem to think in that paradigm. Here is my question.. I have a type monoid and a type Group implemented as follows:

record Monoid : Set₁ where 
   constructor monoid
   field Carrier : Set
         _⊙_     : Carrier → Carrier → Carrier
         e       : Carrier
         leftId  : ∀ {x : Carrier} → (e ⊙ x) ≡ x 
         rightId : ∀ {x : Carrier} → (x ⊙ e) ≡ x
         assoc   : ∀ {x y z : Carrier} → (x ⊙ (y ⊙ z)) ≡ ((x ⊙ y) ⊙ z)

record Group : Set₁ where 
    constructor group 
    field m        : Monoid 
          inv      : Carrier → Carrier 
          inverse1 : {x y : Carrier} → x ⊙ (inv x) ≡ e
          inverse2 : {x y : Carrier} → (inv x) ⊙ x ≡ e

Now, I want to proof the following lemma :

 lemma1 : (x y : Carrier) → (inv x) ⊙ (x ⊙ y) ≡ y 
 lemma1 x y = ?

If I do it on paper, I will apply associativity then left identity.. but I do not know how to tell agda to apply these rules.. I have the problem of translating my thoughts to the Agda paradigm..

Any help is highly appreciated..

Answer 1

When you do the proof on the paper, applying associativity and then left identity uses ony key property of the identity relation - transitivity. That is, when you have a proof of p : x ≡ y and q : y ≡ z you can combine them into a single proof of trans p q : x ≡ z. The trans function is already part of the standard library (Relation.Binary.PropositionalEquality module), but its implementation is fairly simple anyways:

trans : {A : Set} {i j k : A} → i ≡ j → j ≡ k → i ≡ k
trans refl eq = eq

I'm using a bit different presentation of monoids and groups, but you can easily adapt the proof to your scenario.

open import Function
open import Relation.Binary.PropositionalEquality

Op₁ : Set → Set
Op₁ A = A → A

Op₂ : Set → Set
Op₂ A = A → A → A

record IsMonoid {A : Set}
       (_∙_ : Op₂ A) (ε : A) : Set where
  field
    right-id : ∀ x → x ∙ ε ≡ x
    left-id  : ∀ x → ε ∙ x ≡ x
    assoc    : ∀ x y z → x ∙ (y ∙ z) ≡ (x ∙ y) ∙ z

record IsGroup {A : Set}
       (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set where
  field
    monoid    : IsMonoid _∙_ ε
    right-inv : ∀ x → x ∙ x ⁻¹ ≡ ε
    left-inv  : ∀ x → x ⁻¹ ∙ x ≡ ε

  open IsMonoid monoid public

(To keep things simple, indented code is written as part of the IsGroup record). We'd like to prove that:

  lemma : ∀ x y → x ⁻¹ ∙ (x ∙ y) ≡ y
  lemma x y = ?

The first step is to use associativity, that is assoc (x ⁻¹) x y, this leaves us with a goal (x ⁻¹ ∙ x) ∙ y ≡ y - once we prove that, we can merge these two parts together using trans:

  lemma x y =
    trans (assoc (x ⁻¹) x y) ?

Now, we need to apply the right inverse property, but the types don't seem to fit. We have left-inv x : x ⁻¹ ∙ x ≡ ε and we need to somehow deal with the extra y. This is when another property of the identity comes into play.

Ordinary functions preserve identity; if we have a function f and a proof p : x ≡ y we can apply f to both x and y and the proof should be still valid, that is cong f p : f x ≡ f y. Again, implementation is already in the standard library, but here it is anyways:

cong : {A : Set} {B : Set}
       (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

What function should we apply? Good candidate seems to be λ z → z ∙ y, which adds the missing y part. So, we have:

cong (λ z → z ∙ y) (left-inv x) : (x ⁻¹ ∙ x) ∙ y ≡ ε ∙ y

Again, we just need to prove that ε ∙ y ≡ y and we can then piece those together using trans. But this last property is easy, it's just left-id y. Putting it all together, we get:

  lemma : ∀ x y → x ⁻¹ ∙ (x ∙ y) ≡ y
  lemma x y =
    trans (assoc (x ⁻¹) x y) $
    trans (cong (λ z → z ∙ y) (left-inv x)) $
          (left-id y)

---

Standard library also gives us some nice syntactic sugar for this:

  open ≡-Reasoning

  lemma′ : ∀ x y → x ⁻¹ ∙ (x ∙ y) ≡ y
  lemma′ x y = begin
     x ⁻¹ ∙ (x ∙ y)  ≡⟨ assoc (x ⁻¹) x y ⟩
    (x ⁻¹ ∙ x) ∙ y   ≡⟨ cong (λ z → z ∙ y) (left-inv x) ⟩
     ε ∙ y           ≡⟨ left-id y ⟩
     y               ∎

Behind the scenes, ≡⟨ ⟩ uses precisely trans to merge those proofs. The types are optional (the proofs themselves carry enough information about them), but they are here for readability.

---

To get your original Group record, we can do something like:

record Group : Set₁ where
  field
    Carrier : Set
    _∙_     : Op₂ Carrier
    ε       :     Carrier
    _⁻¹     : Op₁ Carrier

    isGroup : IsGroup _∙_ ε _⁻¹

  open IsGroup isGroup public