module Functions.Equality_Proofs where

Import list

open import Data.Nat using (ℕ; zero; suc; _≤_; z≤n; s≤s)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _≤_; z≤n; s≤s)
open import Data.List using (List; []; _∷_; _++_)
open import Data.Unit using (⊤; tt)
open import Data.Product using (_×_; _,_)
open import Function using (_$_)         --

Propositional equality: _≡_

Recall the definition of propositional equality:

data _≡_ {A : Set} (x : A) : A → Set  where
  refl : x ≡ x

infix  _≡_

that yields the following statements:

refl {ℕ} {0} : 0 ≡ 0
refl {ℕ} {1} : 1 ≡ 1
refl {ℕ} {2} : 2 ≡ 2
...
refl {Bool} {true} : true ≡ true
...
refl {Bool} {not b} : not b ≡ not b   -- if 'b : Bool' is a parameter
...

_≡_ as an equivalence and a congruence

Note that _≡_ is an equivalence relation:

refl'  : ∀ {A} (a : A) → a ≡ a
refl' a = refl

sym   : ∀ {A} {a b : A} → a ≡ b → b ≡ a
sym refl = refl

In the definition of sym, we can prove the symmetry with pattern matching on refl, in which case a and b coincides.

Exercises

1. Prove that ≡ is a transitive relation:

   trans : ∀ {A} {a b c : A} → a ≡ b → b ≡ c → a ≡ c

2. Prove that every function is compatible with the equivalence relation, which is called congruency:

   cong : ∀ {A B} {m n : A} → (f : A → B) → m ≡ n → f m ≡ f n

Automatic reduction of types

Agda reduces types automatically during type checking. That is safe because all functions terminate (that is, they are all total functions). For example:

1 + 1 ≡ 2 ⇓ 2 ≡ 2.

Note the consequences:

refl : 1 + 1 ≡ 2
...
refl : 0 + n ≡ n    -- if 'n : ℕ' is a parameter
...

Definitional and propositional equality

x and y are definitionally equal iff refl : x ≡ y.

"Definitional equality is trivial equality."

As an example, consider the following:

1+1≡2 :  +  ≡ 
1+1≡2 = refl

While as a counterexample, consider this. Suppose that n : ℕ is a parameter.

refl : n + 0 ≡ 0 + n

Here, we will get a type error, that is it will not typecheck because n + 0 ≡ 0 + n ⇓ n + 0 ≡ n and n + 0 is not the same as n.

Proof of a + 0 ≡ a

+-right-identity : ∀ n → n +  ≡ n
+-right-identity zero    = refl
+-right-identity (suc n) = cong suc (+-right-identity n)

Thus n + 0 ≡ n is not trivial to prove, but for any n, we can construct the proof for it. While that is a bit funny though:

+-right-identity 0   ⇓  refl
+-right-identity 1   ⇓  refl
+-right-identity 2   ⇓  refl
...

That is, the code of +-right-identity is kind of dead code (which does not do anything meaningful at run time). We will come back to this later.

Exercises

Finish the ingredients of the proof that (ℕ, _+_) is a commutative monoid!

+-left-identity  : ∀ a →  + a ≡ a
+-assoc          : ∀ a b c → a + (b + c) ≡ (a + b) + c -- hint: use cong

For proving the commutativity, you will need a helper function first:

m+1+n≡1+m+n : ∀ m n → m + suc n ≡ suc (m + n)
+-comm      : ∀ a b → a + b ≡ b + a

Exercise: List ⊤ ~ ℕ

Consider the following function definitions:

fromList : List ⊤ → ℕ
fromList []       = zero
fromList (x ∷ xs) = suc (fromList xs)

toList : ℕ → List ⊤
toList zero    = []
toList (suc n) = tt ∷ toList n

Let us prove that fromList and toList are inverses of each other and that they preserve the _++_ and _+_ operations.

from-to : ∀ a → fromList (toList a) ≡ a
to-from : ∀ a → toList (fromList a) ≡ a

fromPreserves++ : ∀ (a b : List ⊤) → fromList (a ++ b) ≡ fromList a + fromList b
toPreserves+    : ∀ (a b : ℕ) → toList (a + b) ≡ toList a ++ toList b

Equational reasoning

Equational reasoning is not a new language construct.

_≡⟨_⟩_ : ∀ {A : Set} (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
x ≡⟨ refl ⟩ refl = refl

infixr  _≡⟨_⟩_

_∎ : ∀ {A : Set} (x : A) → x ≡ x
x ∎ = refl

infix   _∎

This could be then used in the following way:

+-comm' : (n m : ℕ) → n + m ≡ m + n
+-comm' zero    n = sym (+-right-identity n)
+-comm' (suc m) n =
      suc m + n
    ≡⟨ refl ⟩
      suc (m + n)
    ≡⟨ cong suc (+-comm' m n) ⟩
      suc (n + m)
    ≡⟨ sym (m+1+n≡1+m+n n m) ⟩
      n + suc m
    ∎

Properties of _*_

We would like to prove that (ℕ, _*_) is a commutative monoid. In order to do so, first we will need distributivity:

distribʳ-*-+ : ∀ a b c → (a + b) * c ≡ a * c + b * c
distribʳ-*-+ zero    b c = refl
distribʳ-*-+ (suc a) b c =
    c + (a + b) * c
  ≡⟨ cong (λ x → c + x) (distribʳ-*-+ a b c) ⟩
    c + (a * c + b * c)
  ≡⟨ +-assoc c (a * c) (b * c) ⟩
    c + a * c + b * c
  ∎

We can also see that the proof involves using the so-called λ-functions. Such functions are basically functions without names, and can be used at places where we would have defined a function for a single use only.

Their syntax is as follows:

λ x → E(x)

where x is a variable bound by λ as a quantifier, and E(x) is the scope of this variable. It corresponds to such a function, with the name, f missing:

f x = E(x)

Define the following functions (or, rather, prove the following series of lemmata):

*-assoc          : ∀ a b c → a * (b * c) ≡ (a * b) * c
*-left-identity  : ∀ a →  * a ≡ a
*-right-identity : ∀ a → a *  ≡ a
*-identity       : ∀ a →  * a ≡ a × a *  ≡ a

Proving commutativity:

n*0≡0  : ∀ n → n *  ≡ 
*-suc  : ∀ n m → n + n * m ≡ n * suc m
*-comm : ∀ m n → m * n ≡ n * m

Semiring solver

As another approach to proving certain properties about operations, one may consider using the SemiringSolver module. This exports the solve function that could be fed with the abstract representation of the theorem to be proven, and then it tries to find (construct) a proof for that.

Note that it has to be imported together with the Data.Nat.Properties module.

module trySemiringSolver where

open import Data.Nat
open import Data.Nat.Properties
open SemiringSolver
open import Relation.Binary.PropositionalEquality renaming (_≡_ to _≡-official_)

f : ∀ a b c → a + b * c +  ≡-official  + c * b + a
f = solve  (λ a b c → a :+ b :* c :+ con  := con  :+ c :* b :+ a) refl