CODEWITHSUNDEEP
agda
Yasmine Shaorda
Yasmine Shaorda

Reputation: 383

Applying rules in Agda

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..

Upvotes: 3

Views: 330

Answers (1)

Vitus
Vitus

Reputation: 11922

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

Upvotes: 4

Related Questions