```{-
Computer Aided Formal Reasoning (G53CFR, G54CFR)
Thorsten Altenkirch

Lecture 9: Arithmetic and fast reverse

In this lecture we look at proving simple equalities over the
natural numbers by writing recursive programs. We will then use
those to implement fast reverse on vectors.
-}
module l09 where

{- We start using the library, but hide the definitions of + and ≤
because we are going to redefine them. -}
open import Data.Nat hiding ( _+_ ; _≤_ ) -- natural numbers
open import Data.Vec -- contains the definition of vectors
open import Relation.Binary.PropositionalEquality -- defines ≡

{- we define + by recursion over the first argument. -}
_+_ : ℕ → ℕ → ℕ
zero  + n = n
suc m + n = suc (m + n)

{- An alternative would be to define it by recursion over the 2nd -}
_+'_ : ℕ → ℕ → ℕ
m +' zero = m
m +' suc n = suc (m +' n)

{- What is the difference between + and +'?
The are extensionally equivalent, but they are intensionally
different. That is they behave different when we program (or prove)
-}

{- Let's prove some basic equations -}

{- It is obvious that zero is left neutral, indeed this
follows from the 1st line of the definition of +. Hence the prove
is also trivial. "By definition" translates to "refl".
-}
0+ : (n : ℕ) → zero + n ≡ n
0+ n = refl

{- While it is true that zero is also right neutral, it is less
obvious. It doesn't follow from the definition. Indeed, if we try

+0 : (n : ℕ) → n + zero ≡ n
+0 n    = refl

Agda complaints by saying: n + 0 != n ? This means that n + 0 isn't
definitionally equal to n. However they are propositionally equal
(≡), which we can prove using pattern matching and recursion.

-}

+0 : (n : ℕ) → n + zero ≡ n
+0 zero    = refl
+0 (suc n) = cong suc (+0 n)

{- In the suc case we use
cong f :  m ≡ n → f m ≡ f n
which we proved in the previous lecture (but called it resp).
"cong" stands for congruence. This and other gadgets to reason
about equality are defined in Relation.Binary.PropositionalEquality -}

{- What changes in the previous proofs, if we use +' instead of + ? -}

{- Let's look at the interaction of + and suc -}

{- suc in the first argument commutes with + and this follows from the
definition. -}
suc+ : (m n : ℕ) → (suc m) + n ≡ suc (m + n)
suc+ m n = refl

{- suc also commutes with + in the 2nd argument, but as before for +0
this requires a recursive proof. -}

+suc : (m n : ℕ) → m + (suc n) ≡ suc (m + n)
+suc zero n = refl
+suc (suc m) n = cong suc (+suc m n)

{- We have now all the pieces together to prove commutativity of addition.
Basically we do yet another recursion and in each case exploit the lemmas
we have proven previously.
-}

+-comm : (m n : ℕ) → m + n ≡ n + m
+-comm m zero    = +0 m
+-comm m (suc n) = trans (+suc m n) (cong suc (+-comm m n))

{- In the successor case we have to combine +suc and the recursive
proof of +-comm using transitivity (trans).
-}

{- What does this "program" actually compute? Let's evaluate
+-comm 3 7
using C-c C-n (normalize expression).
right "refl" because "3 + 7" and "7 + 3" both reduce to 10
and "refl" proves "10 ≡ 10". However, we can't replace +-comm by

+-comm m n = refl

because the typechecker wouldn't accept it.

Running +-comm doesn't tell us anything new (hence we should
never execute it) but having it is useful as the following example
shows.

Remember in l02 we tried to define ++' (actually the auxilliary
function for fast reverse).

_++'_ : {A : Set} → {m n : ℕ} → Vec A m → Vec A n → Vec A (m + n)
as ++' [] = as
as ++' (b ∷ bs) = (b ∷ as) ++' bs

but the type checker wouldn't accept it. In the []-clause it expects
a "Vec A (m + 0)" but sees "Vec A m" and similarily in the ∷-clause
it expects "Vec (m + (succ n)" but sees "Vec (suc m) + n". This
should ring a bell.

Indeed combining our lemmas above with "subst" we can coerce between
the instances of Vec with provably equal indizes. Given a family "B
: A → Set" and "a b : A" which are equal "p : a ≡ b" we can coerce

subst B p : P a → P b

See last lecture for the proof. We use this to write ++' and reverse
(rev).
-}

_++'_ : {A : Set}{m n : ℕ} → Vec A m → Vec A n → Vec A (m + n)
_++'_ {A} {m} {zero}  as  []
= subst (Vec A) (sym (+0 m)) as
_++'_ {A} {m} {suc n} as  (b ∷ bs)
= subst (Vec A) (sym (+suc m n)) (b ∷ as ++' bs)

{- Note that we had to use the prefix version of ++' to be able to
access the implicit arguments. -}

{- We can now implement rev easily, and we know from its type that it
is length preserving.  -}

rev : {A : Set}{m : ℕ} → Vec A m → Vec A m
rev as = [] ++' as

{- Hence "programs" like +0 , +succ and +-comm are useful as witnesses
at compile time to verify that we performed safe coercions. -}```