module Functions.Equality_Proofs where

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 (_$_) --

`_≡_`

Recall the definition of propositional equality:

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

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 congruenceNote 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.

Prove that

`≡`

is a transitive relation:`trans : ∀ {A} {a b c : A} → a ≡ b → b ≡ c → a ≡ c`

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`

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

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

.

`a + 0 ≡ a`

+-right-identity : ∀ n → n + 0 ≡ 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.

Finish the ingredients of the proof that (`ℕ`

, `_+_`

) is a commutative monoid!

+-left-identity : ∀ a → 0 + 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

`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 is *not* a new language construct.

_≡⟨_⟩_ : ∀ {A : Set} (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z x ≡⟨ refl ⟩ refl = refl infixr 2 _≡⟨_⟩_ _∎ : ∀ {A : Set} (x : A) → x ≡ x x ∎ = refl infix 3 _∎

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 ∎

`_*_`

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 → 1 * a ≡ a *-right-identity : ∀ a → a * 1 ≡ a *-identity : ∀ a → 1 * a ≡ a × a * 1 ≡ a

Proving commutativity:

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

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 + 1 ≡-official 1 + c * b + a f = solve 3 (λ a b c → a :+ b :* c :+ con 1 := con 1 :+ c :* b :+ a) refl