# Natural Number Example of Substitution - Replace and Rewrite

### Rewrite

Lets start by trying to prove commutativity of Nat addition: a + b = b + a.

We have already seen this proof derived here. On that page the proof was derived in a 'Type Driven Development' sort of way (filling in holes and so on). Here we are taking a complimentary, more theoretical approach in order to get an intuitive understanding of constructs and functions such as 'rewrite'.

Here is the proof from Prelude.Nat although I've changed its name so that I can avoid conflicts when experimenting with it.
 ```total plusCommutes : (left : Nat) -> (right : Nat) -> left + right = right + left plusCommutes Z right = rewrite plusZeroRightNeutral right in Refl plusCommutes (S left) right = let inductiveHypothesis = plusCommutes left right in rewrite inductiveHypothesis in rewrite plusSuccRightSucc right left in Refl```

For now we want to concentrate on the first case where the left parameter is Z.

 ```plusCommutes Z right = rewrite plusZeroRightNeutral right in Refl ```

This calls plusZeroRightNeutral from Prelude.Nat which is rewritten to produce our proof:

So how does this work? How does this apply the proof of plusCommutative in this proof?

 (plusZeroRightNeutral right) returns this: Refl:(right + Z = right) but this is the goal we want to get to: Refl: Z + right = right + Z

So we are rewriting something of type right + Z = right to get to the goal Z + right = right + Z. However the code does not tell us how it is doing this. When we look at the difference between the goal and what we have we can see that we need to apply Z + right = right to transform a proof of one equation into another.

We can make this more explicit (and therefore more understamdable to someone reading the code) by using the ==> construct like this.

 ```plusCommutes Z right = rewrite plusZeroRightNeutral right ==> (Z + right = right) in Refl```

But rewrite is syntactic suger, how is it actually implemented? ### Another Example

As a simple example to explore the proof capabilities in Idris lets look at proving that adding zero does not alter a number.

As we have already seen, plus pattern matches on its first operand so:

 'plus Z x' normalises to 'x' so proof is trivial: ```test1 : x=plus Z x test1 = Refl``` However 'plus x Z ' does not normalise to 'x' so we try using just Refl we get the following error: Type mismatch between plus x 0 and x ```test2 : x=plus x Z test2 = Refl fails```

We therefore need to give the compiler some help to prove this second case.

Perhaps the simplest way to think about what what we are trying to do here is to keep moving 'S' outside of the plus until we end up with (plus Z Z) which normalises to Z. So we need to recursively call a function like this until all terms apart from Z are moved out of the plus:
 ```moveSOutside : (x : Nat) -> S (plus x Z) = (plus (S x) Z) moveSOutside x = Refl```

### Generalising to other Nat Number Proofs

In order to prove something for all natural numbers, that is involving a variable like x:Nat, we need to use proof by induction. That is, we need to prove that,

• Its true for x=Z
• If its true for x then its also true for S x

In our case these translate as:

• plus Z Z = Z
• if plus x Z = x then plus (S x) Z = (S x)

The first one is trivial, the second one needs a proof like this:

inductiveStep: (x : Nat) -> x = (plus x Z) -> S x = plus (S x) Z)

#### inductiveStep

So our proof by induction would be of this form using recursion:
 ```total plusZeroRight : (x : Nat) -> (plus x Z) = x plusZeroRight Z = Refl plusZeroRight (S n) = inductiveStep (plusZeroRight n)```

All we have to do is implement inductiveStep.

In order to prove (x : Nat) -> x = (plus x Z) -> S x = plus (S x) Z) there are some proofs that are available to us:

We can increment both sides of an equation and it will still remain true.

This is just a version of 'cong' which is specific to Nat.

 ```incBothSides : x = y -> S x = S y incBothSides Refl = Refl```
We can move 'S' outside the plus.
 ```moveSOutside : (x : Nat) -> S (plus x Z) = (plus (S x) Z) moveSOutside x = Refl```

As shown, Idris can do these without any help. So we only need to combine tem to get what we want:

So here is a full proof:
 ```total plusZeroRight : (x : Nat) -> (plus x Z) = x plusZeroRight Z = Refl plusZeroRight (S n) = inductiveStep n (plusZeroRight n) where incBothSides : x = y -> S x = S y incBothSides Refl = Refl inductiveStep: (x : Nat) -> (plus x Z) = x -> plus (S x) Z = S x inductiveStep x p = incBothSides p```

The 'moveSOutside' has not been called explicitly because Idris can just apply that rule.

in fact we don't need to state these steps in the proof explicitly, Idris can infer them. All we need to do is call the built-in function 'cong' .
 ```total plusZeroRightNeutralC : (x : Nat) -> (plus x Z) = x plusZeroRightNeutralC Z = Refl plusZeroRightNeutralC (S n) = cong {f = S} (plusZeroRightNeutralC n) ```

### Using 'rewrite'

We have seen that the easiest way to prove this example is to use the built-in 'cong' function. However in more complicated examples this will not be the case. So, I think its worth seeing how to prove it using 'rewrite', this may help us with more complicated examples.

'cong' works by doing the same thing to both of an equation, however we may want to subtitute an individual variable in which case we need to use 'replace' or 'rewrite' .

So lets try using rewrite to prove this example.

Here is a proof using rewrite.

Similar to a proof in libs/prelude/Prelude/Nat.idr

 ```total plusZeroRightNeutral : (x : Nat) -> (plus x Z) = x plusZeroRightNeutral Z = Refl plusZeroRightNeutral (S n) = rewrite plusZeroRightNeutral n in Refl ```

The problem is that the above proof does not give the reader of the code many clues about how it actually works.

I think it is rewriting the first 'n' in 'S n = S n' to 'plus n Z'

So we could make this a bit more explicit like this:
 ```total plusZeroRightNeutralRW : (x : Nat) -> (plus x Z) = x plusZeroRightNeutralRW Z = Refl plusZeroRightNeutralRW (S n) = rewrite plusZeroRightNeutralRW n in (the (S n = S n) Refl) ```
I have tried to represnt this as a diagram here: #### Using Match Syntax

There is a nicer syntax for explicitly giving the type of Refl shown above (more about match syntax on this page)

Example using match syntax:
 ```total plusZeroRightNeutralRW2 : (x : Nat) -> (plus x Z) = x plusZeroRightNeutralRW2 Z = Refl plusZeroRightNeutralRW2 (S n) = rewrite plusZeroRightNeutralRW2 n ==> (S n = S n) in Refl```

The above syntax can be extended further, using <==, like this:

Z + n = n + Z could easily be proved from what we have already proved: Z + n = n and n + Z = n

but instead this proof uses match syntax

 ```zCommutes : (n : Nat) -> (Z + n = n + Z) (Z + n = n + Z) <== zCommutes = rewrite ((n + Z = n) <== plusZeroRightNeutral) ==> (Z + n = n) in Refl```

For other examples of match syntax see:

```prop : (x : Nat) -> Type
prop x = (plus x Z) = x

moveSOutside1 : (x : Nat) -> S (plus x Z) = (plus (S x) Z)
moveSOutside1 x = Refl

moveSOutside2 : (x : Nat) -> (plus (S x) Z) = S (plus x Z)
moveSOutside2 x = Refl

incBothSides : x = y -> S x = S y
incBothSides Refl = Refl

incx : (x : Nat) -> x = (plus x Z) -> S x = S (plus x Z)
incx x p = rewrite p in Refl  -- rewrites x to plus x 0 in S x = S (plus x Z)

incxr : (x : Nat) -> (plus x Z) = x -> S (plus x Z) = S x
incxr x p = rewrite p in Refl  -- rewrites plus x 0 to x in S x = S (plus x Z)

-- following fails with Type mismatch between plus x 0 and x
--incxb : (x : Nat) -> x = (plus x Z) -> S x = S (plus x Z)
--incxb x p = Refl

incx2 : (x : Nat) -> x = (plus x Z) -> S x = plus (S x) Z
incx2 x p = rewrite p in (the (S (plus x 0) = S (plus x 0)) Refl)
-- rewrites plus x 0 to x in (S (plus x 0) = S (plus x 0))

incx2r : (x : Nat) -> (plus x Z) = x -> plus (S x) Z = S x
incx2r x p = rewrite p in (the (S x = S x) Refl)
-- rewrites x to plus x 0 in (S x = S x)

-- following fails with Type mismatch between plus x 0 and x
--incx2b : (x : Nat) -> x = (plus x Z) -> S x = plus (S x) Z
--incx2b x p = Refl

-- rewrite__impl : (P : a -> Type) -> x = y -> P y -> P x
doNothing : (x : Nat) -> (plus x Z) = x -> (plus x Z) = x
doNothing x pr = rewrite__impl prop (the (x = x) Refl) pr

--doNothing2 : (x : Nat) -> (plus x Z) = x -> S (plus x Z) = S x
--doNothing2 x pr = rewrite__impl prop (the (x = x) Refl) pr

-- prove if x = (plus x Z) then S x = (plus (S x) Z)
-- we might be able to prove this by first proving:
-- if x = (plus x Z) then S x = S (plus x Z)

----------------------------------------------------------
--replace
-- Replace is defined like this:
--    ||| Perform substitution in a term according to some equality.
--    replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
--    replace Refl prf = prf
-- What I am trying to do here is to take the following proof which uses
-- rewrite and use replace instead:
total plusZeroRightNeutralRW : (x : Nat) -> (plus x Z) = x
plusZeroRightNeutralRW Z     = Refl
plusZeroRightNeutralRW (S n) =
rewrite plusZeroRightNeutralRW n in (the (S n = S n) Refl)
-- rewrites (plus n Z) to n in (S n = S n)
--
-- instead of (S n = S n) I tried (S (plus n Z)) = S n) and ((plus (S n) Z) = S n)
-- and (S n = (S (plus n Z))) and (S n = (plus (S n) Z))
-- but they did not work. I got Type mismatch between n and plus n 0
--
-- Looking at this function it is not self explanatory, its not clear:
-- * What is the type of Refl ?
-- * What is the property P ?
--
-- So how do we change it to use replace? First try to use
-- rewrite__impl : (P : a -> Type) -> x = y -> P y -> P x
--
--total plusZeroRightNeutralRI : (x : Nat) -> (plus x Z) = x
--plusZeroRightNeutralRI Z     = Refl
--plusZeroRightNeutralRI (S n) =
--     rewrite__impl prop (the (S n = S n) Refl) (plusZeroRightNeutralRI n)
--
--total plusZeroRightNeutralRI : (x : Nat) -> (plus x Z) = x
--plusZeroRightNeutralRI Z     = Refl
--plusZeroRightNeutralRI (S n) =
--     rewrite__impl prop (the (S n = S n) Refl) (plusZeroRightNeutralRI n)
--
--total plusZeroRightNeutralRI : (x : Nat) -> (plus x Z) = x
--plusZeroRightNeutralRI Z     = Refl
--plusZeroRightNeutralRI (S n) =
--     rewrite__impl prop ?t1 ?t2
--
--*proof> :t t1
--  n : Nat
--  y : Nat
--------------------------------------
--t1 : S n = y
--*proof> :t t2
--  n : Nat
--  y : Nat
--------------------------------------
--t2 : plus y 0 = y
--
-- this requires the second parameter to be S n = n
-- but rewrite__impl prop (the (S n = n) Refl) (plusZeroRightNeutralRI n)
-- means unifying n and S n would lead to infinite value
--
--total plusZeroRightNeutralRI : (x : Nat) -> (plus x Z) = x
--plusZeroRightNeutralRI Z     = Refl
--plusZeroRightNeutralRI (S n) =
--  let y = S n in
--     rewrite__impl prop (the (y = S n) Refl) (plusZeroRightNeutralRI n)
--
-- So how do we change it to use replace?
--
--total plusZeroRightNeutralRep : (x : Nat) -> (plus x Z) = x
--plusZeroRightNeutralRep Z     = Refl
--plusZeroRightNeutralRep (S n) =
--      replace {P = prop} (plusZeroRightNeutralRep n) (the (S n = S n) Refl)

--     |
-- 134 |       replace {P = prop} (the (x = (S n)) Refl) plusZeroRightNeutralRep n
--     |       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- When checking right hand side of plusZeroRightNeutralRep with expected type
--         plus (S n) 0 = S n
-- When checking an application of function replace:
--         Type mismatch between
--                 S n = S n
--         and
--                 x = S n
```