Contents Previous Next


module Types.equational2 where

open import Agda.Primitive using (Level; __; lsuc; lzero)
open import Types.equality
open import Types.product using (Σ; _,_)

We now define a more complex version where there is symmetry in equivalence preservation, unlike the previous naive version where it is only covariant, capturing the commutativity of the equivalence relation.

Equational Reasoning over equivalence relations

module ★-reasoning
  {a ℓ}
  {A : Set a}
  (__ : Rel A ℓ)
  (reflexive : Reflexive __)
  (trans : Transitive __)
  where

  infix  4 _IsRelatedTo_
  infix  3 _
  infixr 2 _∼⟨__ _≡⟨__ _≡˘⟨__ _≡⟨⟩_
  infix  1 begin_

We start with a vague notion of being related to:

  data _IsRelatedTo_ (x y : A) : Set (a ⊔ ℓ) where
    relTo : (x∼y : x ∼ y)  x IsRelatedTo y

we concretize the fact of being related to into a begin statement, this forms the basis or starting point of any reasoning sequence.

  begin_ :  {x y}  x IsRelatedTo y  x ∼ y
  begin relTo x∼y = x∼y

chaining transitivity:

  _∼⟨__ :  x {y z}  x ∼ y  y IsRelatedTo z  x IsRelatedTo z
  _ ∼⟨ x∼y ⟩ relTo y∼z = relTo (trans x∼y y∼z)

covariant equivalence preservation:

  _≡⟨__ :  x {y z}  x ≡ y  y IsRelatedTo z  x IsRelatedTo z
  _ ≡⟨ refl ⟩ x∼z = x∼z

contravariant equivalence preservation:

  _≡˘⟨__ :  x {y z}  y ≡ x  y IsRelatedTo z  x IsRelatedTo z
  _ ≡˘⟨ refl ⟩ x∼z = x∼z

preservation of reflexivity:

  _≡⟨⟩_ :  x {y}  x IsRelatedTo y  x IsRelatedTo y
  _ ≡⟨⟩ x∼y = _ ≡⟨ refl ⟩ x∼y

and we end chains of reasoning with a QED:

  _:  x  x IsRelatedTo x
  __ = relTo reflexive

Some Proofs using equational reasoning

A lot of assymetric laws can be derived with one half of the symmetry and mixing it with commutativity. E.g. left inverse coiuld be derived using right inverse and commutativity, similarly, right inverse can be derived using left inverse and commutativity.

open import Types.operations

module withCommutativity {a ℓ}
  {A : Set a}
  {__ : Rel A ℓ}
  {__ : (__) A}
  {_⁻¹ : (__) A}
  (reflexive : Reflexive __)
  (trans : Transitive __)
  (comm : Commutative __ __)
  (ϵ : A)
  where

    open ★-reasoning __ reflexive trans public
    comm+invˡ⇒invʳ :
        LeftInverse __ ϵ _⁻¹ __
       RightInverse __ ϵ _⁻¹ __
    comm+invˡ⇒invʳ invˡ x = begin
      x • (x ⁻¹) ∼⟨ comm x (x ⁻¹)
      (x ⁻¹) • x ∼⟨ invˡ x ⟩
      ϵ          ∎
    comm+invʳ⇒invˡ : RightInverse __ ϵ _⁻¹ __  LeftInverse __ ϵ _⁻¹ __
    comm+invʳ⇒invˡ invʳ x = begin
      (x ⁻¹) • x ∼⟨ comm (x ⁻¹) x ⟩
      x • (x ⁻¹) ∼⟨ invʳ x ⟩
      ϵ          ∎
module withCongruence {a ℓ}
  {A : Set a}
  (__ : Rel A ℓ)
  (__ : (__) A)
  (_⁻¹ : (__) A)
  (reflexive : Reflexive __)
  (trans : Transitive __)
  (sym : Symmetric __)
  (cong : Congruent₂ __ __)
  (ϵ : A)
  where

    open ★-reasoning __ reflexive trans public
    assoc+id+invʳ⇒invˡ-unique :
        Associative __ __
       Identity __ ϵ __
       RightInverse __ ϵ _⁻¹ __
        x y
       (x • y) ∼ ϵ
       x ∼ (y ⁻¹)
    assoc+id+invʳ⇒invˡ-unique assoc (idˡ , idʳ) invʳ x y eq = begin
      x                ∼⟨ sym (idʳ x)
      x • ϵ            ∼⟨ cong reflexive (sym (invʳ y))
      x • (y • (y ⁻¹)) ∼⟨ sym (assoc x y (y ⁻¹))
      (x • y)(y ⁻¹) ∼⟨ cong eq reflexive ⟩
      ϵ • (y ⁻¹)       ∼⟨ idˡ (y ⁻¹)
      y ⁻¹             ∎
    assoc+id+invˡ⇒invʳ-unique :
        Associative __ __
       Identity __ ϵ __
       LeftInverse __ ϵ _⁻¹ __
        x y
       (x • y) ∼ ϵ
       y ∼ (x ⁻¹)
    assoc+id+invˡ⇒invʳ-unique assoc (idˡ , idʳ) invˡ x y eq = begin
      y                ∼⟨ sym (idˡ y)
      ϵ • y            ∼⟨ cong (sym (invˡ x)) reflexive ⟩
      ((x ⁻¹) • x) • y ∼⟨ assoc (x ⁻¹) x y ⟩
      (x ⁻¹)(x • y) ∼⟨ cong reflexive eq ⟩
      (x ⁻¹) • ϵ       ∼⟨ idʳ (x ⁻¹)
      x ⁻¹             ∎

Introduction