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 4 _≡_

yields

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

_≡_ is an equivalence and a congruence

_≡_ 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   -- after pattern matching on 'refl', 'a' and 'b' coincides

Exercise


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

Prove that every function is compatible with the equivalence relation (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.
This is safe because all functions terminate.

Example:

1 + 1 ≡ 2 ⇓ 2 ≡ 2.

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

Example


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

Counterexample

Suppose that n : ℕ is a parameter.

refl : n + 0 ≡ 0 + n   -- type error!

This doesn't 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 + 0 ≡ n
+-right-identity zero    = refl
+-right-identity (suc n) = cong suc (+-right-identity n)

So n + 0 ≡ n is not trivial,
but for any n we can construct the proof of it.

This is a bit funny though:

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

So the code of +-right-identity is kind of dead code (doesn't do anything meaningful at run time).
We'll discuss this later.

Exercises

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 commutativity you need a helper function first:


m+1+n≡1+m+n : ∀ m n → m + suc n ≡ suc (m + n)

Exercise: List ⊤ ~ ℕ

Let


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

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

Let's prove that fromList and toList are inverses of each other and that they preserve the operations _++_ and _+_!


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 2 _≡⟨_⟩_

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

infix  2 _∎

Usage example:


+-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'd like to prove that (ℕ, _*_) is a commutative monoid.

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
  ∎

Define the following functions:


*-assoc        : ∀ a b c → a * (b * c) ≡ (a * b) * c


*-left-identity  : ∀ a → 1 * a ≡ a


*-right-identity : ∀ a → a * 1 ≡ a

Commutativity:


-- helper functions:
n*0≡0 : ∀ n → n * 0 ≡ 0


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


*-comm : ∀ m n → m * n ≡ n * m

Semiring solver


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