Contents Previous Next

Equational Reasoning

module Types.equational where

open import Agda.Primitive using (Level; _⊔_; lsuc; lzero)
open import Types.equality renaming (cong-≡ to cong)
open import Types.product using (Σ; _,_; _×_)

Though we looked at the type theory way of constructively proving propositions, there is another way which we tend to be more familiar with: the way we solve equations on paper.

For example, consider the problem of proving a well known identity for natural numbers from linear algebra:

∀ a, b ∈ ℕ: (a+b)² ≡ a² + 2 * a * b + b²

(a + b) × (a + b)
    Applying distributivity of + and × (a + b) * c ≡ (a × c) + (b × c)
 = a × (a + b) + b × (a + b)
    Applying distributivity again, this time from the left-hand side
 = a × a + a × b + b × a + b²
    Applying
        1. The fact that a × a ≡ a²
        2. Commutativity of multiplication: a × b ≡ b × a
        3. Reflexivity of ≡ for a × b and b × a to add to 2 times
= a² + 2 * a * b + b²
Q.E.D.

Each step of such a solution essentially follows through the rule of transitivity of equality. Hence setp₂ = step₁ + actions₁ and so on. We can write an apparatus to let us do exactly that in Agda. That apparatus is “equational reasoning”. Here, we define the framework on top of equivalence relations:

module ≡-Reasoning {a} {A : Set a} where
  open ≡-properties {A = A}
  open IsEquivalence isEquivalence public

  infix  3 _∎
  infixr 2 _≡⟨⟩_ _≡⟨_⟩_
  infix  1 begin_

  -- This is just syntactical sugar to define the start of the proof
  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

  -- The QED or "hence, proved" marker to end the proof.
  _∎ : ∀ (x : A) → x ≡ x
  _∎ _ = rfl

In order to define \((a+b) × (a-b) ≡ a² - b²\) in Agda, we have to define some properties of +, - and *:

Since we are proving this literally from scratch, we have to prove quite a few basic constructions:

module Properties {a} {A : Set a} where
  open ≡-Reasoning

We start with the type of natural numbers:

  data ℕ : Set where
    zero : ℕ
    succ : ℕ → ℕ

We then proceed to define the required operations on natural numbers:

  infixl 6 _+_ _−_
  infixl 7 _*_

  _+_ : ℕ → ℕ →  ℕ
  m + zero   = m
  m + succ n = succ (m + n)

  _−_ : ℕ → ℕ → ℕ
  zero  − m     = zero
  succ n − zero  = succ n
  succ n − succ m = n − m

  _*_ : ℕ → ℕ → ℕ
  zero * x     = zero
  (succ x) * y = y + (x * y)

  _² : ℕ → ℕ
  x ² = x * x

We now prove properties of addition, upto commutativity:

  one = succ zero
  two = succ (succ zero)

  +-succ-l : ∀ x y → x + (succ y) ≡ succ (x + y)
  +-succ-l zero    n = refl
  +-succ-l (succ m) n = refl

  +-succ-r : ∀ x y → (succ x) + y ≡ succ (x + y)
  +-succ-r n zero = refl
  +-succ-r m (succ n) = cong succ (+-succ-r m n)

  +-unsucc-l : ∀ x y → succ (x + y) ≡ x + (succ y)
  +-unsucc-l n zero     = refl
  +-unsucc-l n (succ m) = refl

  +-unsucc-r : ∀ x y → succ (x + y) ≡ (succ x) + y
  +-unsucc-r m zero = refl
  +-unsucc-r m (succ n) = cong succ (+-unsucc-r m n)

  +-assoc-l : ∀ x y z → ((x + y) + z) ≡ (x + (y + z))
  +-assoc-l l m zero = refl
  +-assoc-l l m (succ n) = cong succ (+-assoc-l l m n)

  +-assoc-r : ∀ x y z → (x + (y + z)) ≡ ((x + y) + z)
  +-assoc-r l m zero = refl
  +-assoc-r l m (succ n) = cong succ (+-assoc-r l m n)

  +-identity-l : ∀ x → x + zero ≡ x
  +-identity-l _ = refl

  +-identity-r : ∀ x → zero + x ≡ x
  +-identity-r zero    = refl
  +-identity-r (succ n) = cong succ (+-identity-r n)

  +-identity : ∀ x → (x + zero ≡ x) × (zero + x ≡ x)
  +-identity n = (+-identity-l n) , (+-identity-r n)

  -- we finally use equational reasoning to prove this bit
  +-comm : ∀ x y → (x + y) ≡ (y + x)
  +-comm zero n = +-identity-r n
  +-comm (succ m) n = begin
    (succ m) + n   ≡⟨ +-succ-r m n ⟩
    succ (m + n) ≡⟨ cong succ (+-comm m n) ⟩
    succ (n + m) ≡⟨ refl ⟩
    n + succ m   ∎

As we saw, we had to prove quite a few propositions in their right and left handed versions. These will come in handy later, in fact some of them have been written while trying to prove later propositions. This highlights a central way of solving mathematics - proofs are broken up into pieces and each piece is solved separately. Mostly such smaller proofs tend to be inductively proved and used to prove more complex proofs using equational reasoning.

We now proceed to prove some propositions for multiplication:

  *-succ-l : ∀ x y → succ x * y ≡ y + (x * y)
  *-succ-l m zero = refl
  *-succ-l m (succ n) = refl

  *-succ-r : ∀ x y → x * succ y ≡ x + (x * y)
  *-succ-r zero m = refl
  *-succ-r (succ m) n = begin
    succ m * succ n             ≡⟨⟩
    succ n + m * succ n         ≡⟨ cong (_+_ (succ n)) (*-succ-r m n) ⟩
    succ n + (m + m * n)        ≡⟨ +-succ-r n (m + (m * n)) ⟩
    succ (n + (m + m * n))      ≡⟨⟩
    succ (n + (m + (m * n)))    ≡⟨ cong succ (+-assoc-r n m (m * n)) ⟩
    succ (n + m + m * n)        ≡⟨ cong (λ x → succ (x + m * n)) (+-comm n m) ⟩
    succ ((m + n) + m * n)      ≡⟨ cong succ (+-assoc-l m n (m * n)) ⟩
    succ (m + (n + m * n))      ≡⟨ +-unsucc-r m (n + m * n) ⟩
    (succ m) + (n + m * n)      ≡⟨⟩
    succ m + succ m * n         ∎

  *-zero-r : ∀ x → x * zero ≡ zero
  *-zero-r zero = refl
  *-zero-r (succ n) = begin
    (succ n) * zero       ≡⟨⟩
    zero + n * zero       ≡⟨ +-identity-r (n * zero) ⟩
    n * zero              ≡⟨ *-zero-r n ⟩
    zero                  ∎

  *-zero-l : ∀ x → zero * x ≡ zero
  *-zero-l zero = refl
  *-zero-l (succ n) = refl

  *-identity-l : ∀ x → one * x ≡ x
  *-identity-l zero = refl
  *-identity-l (succ n) = refl

  *-comm : ∀ x y → x * y ≡ y * x
  *-comm m zero = *-zero-r m
  *-comm m (succ n) = begin
    m * (succ n)        ≡⟨ *-succ-r m n ⟩
    m + m * n           ≡⟨ cong (m +_) (*-comm m n) ⟩
    m + n * m           ≡⟨ sym (*-succ-l n m) ⟩
    (succ n) * m        ∎

  *-identity-r : ∀ x → x * one ≡ x
  *-identity-r zero = refl
  *-identity-r (succ n) = begin
    (succ n) * one          ≡⟨⟩
    one + n * one           ≡⟨ cong (_+_ one) (*-identity-r n) ⟩
    (succ zero) + n         ≡⟨ +-succ-r zero n ⟩
    succ (zero + n)         ≡⟨ cong (λ x → succ x) (+-comm zero n) ⟩
    succ (n + zero)         ≡⟨⟩
    succ n                  ∎

  *-succ-r-r : ∀ x y → x * succ y ≡ (x * y) + x
  *-succ-r-r zero m = refl
  *-succ-r-r (succ m) n = begin
    succ m * succ n             ≡⟨ *-succ-r (succ m) n ⟩
    succ m + succ m * n         ≡⟨ +-comm (succ m) (succ m * n) ⟩
    succ m * n + succ m         ∎

Here we see a noteworthy pattern,

To prove for example a + (b * c) + d ≡ a + (c * b) + d, we have to apply commutativity only to (b * c) only while keeping the rest as it is. This is often achieved by using congruence over lambda pattern matching expressions in agda like cong (λ x a + x + d) (*-comm b c). Or in other words,

a + (b * c) + d     ≡⟨ cong (λ x a + x + d) (*-comm b c) ⟩
a + (c * b) + d     ∎

Note that the above proofs might not be the best way to prove these propositions.

We now prove the distributive property of * over +:

  +-distrib-*-r : ∀ x y z → x * (y + z) ≡ (x * y) + (x * z)
  +-distrib-*-r l m zero = begin
    l * (m + zero)            ≡⟨⟩
    l * m                     ≡⟨⟩
    (l * m) + zero            ≡⟨ cong ((l * m) +_) (sym (*-zero-r l)) ⟩
    (l * m) + (l * zero)      ∎
  --------------------------------------------------------
  +-distrib-*-r l m (succ n) = begin
    l * (m + (succ n))        ≡⟨⟩
    l * succ (m + n)          ≡⟨ *-succ-r l (m + n) ⟩
    l + l * (m + n)           ≡⟨ +-comm l (l * (m + n)) ⟩
    l * (m + n) + l           ≡⟨ cong (λ z → z + l) (+-distrib-*-r l m n) ⟩
    ((l * m) + (l * n)) + l   ≡⟨ +-assoc-l (l * m) (l * n) l ⟩
    (l * m) + ((l * n) + l)   ≡⟨ cong ((l * m) +_) (sym (*-succ-r-r l n)) ⟩
    (l * m) + l * (succ n)    ∎

  +-distrib-*-l : ∀ x y z → (x + y) * z ≡ (x * z) + (y * z)
  +-distrib-*-l zero m n = begin
    (zero + m) * n            ≡⟨ *-comm (zero + m) n ⟩
    n * (zero + m)            ≡⟨ +-distrib-*-r n zero m ⟩
    (n * zero) + (n * m)      ≡⟨ cong (λ x → x + (n * m)) (*-comm n zero) ⟩
    (zero * n) + (n * m)      ≡⟨ cong (λ x → (zero * n) + x) (*-comm n m) ⟩
    (zero * n) + (m * n)      ∎
  --------------------------------------------------------
  +-distrib-*-l (succ l) m n = begin
    ((succ l) + m) * n        ≡⟨ cong (λ x → x * n) (+-succ-r l m) ⟩
    succ (l + m) * n          ≡⟨⟩
    n + ((l + m) * n)         ≡⟨ cong (_+_ n) (+-distrib-*-l l m n) ⟩
    n + (l * n + m * n)       ≡⟨ +-assoc-r n (l * n) (m * n) ⟩
    (n + l * n) + (m * n)     ≡⟨⟩
    (succ l) * n + m * n      ∎

And now, finally the proof of our original proposition:

  proof : ∀ x y → (x + y) ² ≡ (x ² + two * (x * y) + y ²)
  --------------------------------------------------------
  proof zero n = begin
    (zero + n) * (zero + n)
        ≡⟨ cong (λ x → (zero + n) * x) (+-identity-r n) ⟩
    (zero + n) * n
        ≡⟨ cong (λ x → x * n) (+-identity-r n) ⟩
    n * n
        ≡⟨⟩
    n ²
        ≡⟨⟩
    n ² + zero
        ≡⟨ cong ((n ²) +_) (sym (*-zero-r zero)) ⟩
    n ² + (zero * zero)
        ≡⟨⟩
    n ² + zero ²
        ≡⟨ +-comm (n ²) (zero ²) ⟩
    (zero ² + n ²)
        ≡⟨⟩
    (zero ² + n ²) + zero
        ≡⟨ cong ((zero ² + n ²) +_) (sym (*-zero-r (two))) ⟩
    (zero ² + n ²) + (two * zero)
        ≡⟨⟩
    (zero ² + n ²) + (two * zero * n)
        ≡⟨ +-assoc-l (zero ²) (n ²) (two * zero * n) ⟩
    zero ² + (n ² + (two * zero * n))
        ≡⟨ cong (λ x → zero ² + x) (+-comm (n ²) (two * zero * n)) ⟩
    zero ² + ((two * zero * n) + n ²)
        ≡⟨ +-assoc-r (zero ²) (two * zero * n) (n ²) ⟩
    zero ² + two * zero * n + n ²
        ∎
  --------------------------------------------------------
  proof (succ m) n = begin
    ((succ m) + n) * ((succ m) + n)
        ≡⟨ +-distrib-*-l (succ m) n (succ m + n) ⟩
    (succ m) * (succ m + n) + n * (succ m + n)
        ≡⟨ cong (λ x → x + n * (succ m + n)) (+-distrib-*-r (succ m) (succ m) n) ⟩
    (succ m) * (succ m) + (succ m) * n + n * (succ m + n)
        ≡⟨ cong (λ x → (succ m) * (succ m) + (succ m) * n + x) (+-distrib-*-r n (succ m) n) ⟩
    (succ m) * (succ m) + (succ m) * n + (n * (succ m) + n * n)
        ≡⟨ +-assoc-r ((succ m) * (succ m) + (succ m) * n) (n * (succ m)) (n * n)  ⟩
    (succ m) * (succ m) + (succ m) * n + n * (succ m) + n * n
        ≡⟨ cong (λ x → (succ m) * (succ m) + (succ m) * n + x + n * n) (*-comm n (succ m)) ⟩
    (succ m) * (succ m) + (succ m) * n + (succ m) * n + n * n
        ≡⟨⟩
    (succ m) ² + (succ m) * n + (succ m) * n + n * n
        ≡⟨⟩
    ((succ m) ² + (succ m) * n) + (succ m) * n + n ²
        ≡⟨ cong (_+ n ²) (+-assoc-l ((succ m) ²) ((succ m) * n) ((succ m) * n)) ⟩
    (succ m) ² + (succ m * n + succ m * n) + n ²
        ≡⟨ cong (λ x → (succ m) ² + x + n ²) (sym (*-identity-r ((succ m) * n + (succ m) * n))) ⟩
    (succ m) ² + ( (succ m * n) + (succ m * n) ) * one + n ²
        ≡⟨ refl ⟩
    (succ m) ² + ((succ m * n) + (succ m * n)) * one + n ²
        ≡⟨ cong (λ x → (succ m) ² + x + n ²) (+-distrib-*-l (succ m * n) (succ m * n) one) ⟩
    (succ m) ² + ((succ m * n) * one + (succ m * n) * one) + n ²
        ≡⟨ cong (λ x → (succ m) ² + x + n ²) (sym (+-distrib-*-r (succ m * n) one one)) ⟩
    (succ m) ² + ((succ m * n) * (one + one)) + n ²
        ≡⟨⟩
    (succ m) ² + ((succ m * n) * two) + n ²
        ≡⟨ cong (λ x → (succ m) ² + x + n ²) (*-comm (succ m * n) two) ⟩
    (succ m) ² + two * ((succ m) * n) + n ²
        ∎

Equational Reasoning 2