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