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?

commute Z

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.

diagram showing how to move S out of plus
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,

In our case these translate as:

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)

Books & Papers about Agda

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: diagram of the substitution

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

metadata block
see also:
Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

flag flag flag flag flag flag Type-Driven Development with Idris

 

Commercial Software Shop

Where I can, I have put links to Amazon for commercial software, not directly related to the software project, but related to the subject being discussed, click on the appropriate country flag to get more details of the software or to buy it from them.

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.