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 of equational reasoning on top of an equivalence relation _~_ rather than on equality.

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_

This seemingly unnecessary type is used to make it possible to infer arguments even if the underlying equality evaluates.

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

Use this to indicate beginning of reasoning:

  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 asymmetric laws can be derived with one half of the symmetry and mixing it with commutativity. E.g. left inverse could 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

Commutativity and left inverse yields right inverse

    comm+invˡ⇒invʳ :
        LeftInverse __ ϵ _⁻¹ __
       RightInverse __ ϵ _⁻¹ __
    comm+invˡ⇒invʳ invˡ x = begin
      x • (x ⁻¹) ∼⟨ comm x (x ⁻¹)
      (x ⁻¹) • x ∼⟨ invˡ x ⟩
      ϵ          ∎

Commutativity and right inverse yields left inverse

    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

Uniqueness of left inverse

Given an operation is associative, has an identity, every given right inverse has a unique left inverse.

    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 ⁻¹             ∎

Uniqueness of right inverse

Given an operation is associative, has an identity, every given left inverse has a unique right inverse.

    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 ⁻¹             ∎

Relations other than equality

Equational reasoning can also be done on other relations except equality and equivalence ones. For example, here we derive the framework for the order operator _<=_:

open import Types.proofsAsData using (_<=_; ltz; lt)
open import Lang.dataStructures
open import Types.relations hiding (Rel)

≤-trans : Transitive {A =} _<=_
≤-trans ltz j≤k = ltz
≤-trans (lt x) (lt y) = lt (≤-trans x y)

module ≤-Reasoning where
  infix  3 _
  infixr 2 _≤⧏⧐_ _≤⧏__
  infix  1 begin_

  begin_ :  {x y :}  x <= y  x <= y
  begin_ x≤y = x≤y

  -- Apply reflexivity, arguments required within the ⧏⧐
  _≤⧏⧐_ :  (x {y} :)  x <= y  x <= y
  _ ≤⧏⧐ x≤y = x≤y

  -- Transitivity with arguments applied within the ⧏⧐
  _≤⧏__ :  (x {y z} :)  x <= y  y <= z  x <= z
  _ ≤⧏ x≤y ⧐ y≤z = ≤-trans x≤y y≤z

  _:  (x :)  x <= x
  _■ zero = ltz
  _(succ x) = lt (_■ x)

Equational reasoning for any operator

As we see the pattern above, given the proof for transitivity of an operator, we can generate the constructs for doing equational with the operator.

module λ-Reasoning {a ℓ}
  {A : Set a}
  {__ : Rel A ℓ}
  {⌬-trans : Transitive __}
  {⌬-refl : Reflexive __}
  where

  infix  3 _
  infixr 2 _⌬◀▶_ _⌬◀__
  infix  1 begin_

  begin_ :  {x y : A}  x ⌬ y  x ⌬ y
  begin_ x⌬y = x⌬y

  -- Apply reflexivity, arguments required within the ◀▶
  _⌬◀▶_ :  (x {y} : A)  x ⌬ y  x ⌬ y
  _ ⌬◀▶ x⌬y = x⌬y

  -- Transitivity with arguments applied within the ◀▶
  _⌬◀__ :  (x {y z} : A)  x ⌬ y  y ⌬ z  x ⌬ z
  _ ⌬◀ x⌬y ▶ y⌬z = ⌬-trans x⌬y y⌬z

  _:  (x : A)  x ⌬ x
  __ = ⌬-refl

Introduction