Substitution - Replace and Rewrite

When doing proofs about equations we sometimes need to replace a variable, that occurs in an equation, with some expression. For example, if we are working with natural numbers we may want to replace a vaiable 'k' with say '(S m)' everywhere it occurs in an equation.

The replace and rewrite functions allow us to substitute identical terms in an equation. For instance if:

'x=x+0' and 'y=x'

then

'y=y+0'

However Idris does not solve symultanous equations (a variable name inside some equation is not linked to the same name in other equations), instead Idris uses the indiscernability of identicals principle.

Indiscernability of Identicals

For any x and y, if x is identical to y, then x and y have all the same properties.

for allxfor ally [ x = y ->for allP ( P x ↔ P y)]

Here these properties are usually equations.

From Wikipedia:

Indiscernability of identicals doesn't entail reflexivity of = but both properties together entail symmetry and transitivity. Therefore, indiscernability of identicals and reflexivity is sometimes used as a (second-order) axiomatization for the equality relation.

Properties

equations

In set theory a property can be given by a function from Set to Bool. For instace: the property of being an even number can be represented like this: property in set theory
Since we are using constructive logic we represent properties as a function into a type (in this case an equation). type property

So, in Idris, this is not intended for a property like this:

which can't be proved for all values of n (that is, it generates a type that can't be constructed, using Refl, for all values of n).

 
p1: Nat -> Type
p1 n = (n=2)

Whereas a property like this:

can be proved for all values of n

 
p2: Nat -> Type
p2 n = (n=n+0)
So 'p1' can be contructed at 2 but when we try to construct at 3 we get an error as expected:
*proof> the (p1 2) Refl
Refl : 2 = 2
*proof> the (p1 3) Refl
(input):1:1-15:When checking argument value to function Prelude.Basics.the:
        Type mismatch between
                x = x (Type of Refl)
        and
                p1 3 (Expected type)
        
        Specifically:
                Type mismatch between
                        1
                and
                        0
As expected we can construct 'p2' at any value. However this needs to be proved and, for this we need Replace or Rewrite.
*proof> the (p2 2) Refl
Refl : 2 = 2
*proof> the (p2 3) Refl
Refl : 3 = 3
*proof> 

Variables

We can represent variables in an equation by using dependent types, like this:

plusZeroRightNeutral: (x:Nat) -> (x = plus x Z) 

So this generates a family of types:

To prove it we must be able to construct for every value of x (it must be total).

An Example

The simplest example I can find is a proof that x=x+0 for all x.

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

Using cong

It is possible to prove this by using cong

total plusZeroRightNeutralC : (x : Nat) -> (plus x Z) = x
plusZeroRightNeutralC Z     = Refl
plusZeroRightNeutralC (S n) = cong  {f = S} (plusZeroRightNeutralC n)

So (plusZeroRightNeutralC n) has type (plus x Z) = x that can be interpeted as,

(plusZeroRightNeutralC n) is a proof (that is a constructor) of (plus x Z) = x

'cong' is applied to this which says if we have a proof of (plus x Z) = x then we get a proof of S (plus x Z) = S x

So,

but x = S n so,

????

So 'cong' works for this case since we only need to apply the same function to both sides of the equation. In more complicated cases we may need to substitute variables so its worth using this example with replace/rewrite to gain understanding before we go on to more complex examples.

Replace

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

total plusZeroRightNeutralRep : (x : Nat) -> (plus x Z) = x
plusZeroRightNeutralRep Z     = Refl
plusZeroRightNeutralRep {x} (S n) =
      replace {P = prop} (the (x = (S n)) Refl) plusZeroRightNeutralRep n
For the second case we need to proove that: if it is true for (S x) then its also true for 'x'. plusZeroRightNeutralRep

The following are extracts from a reply to a question I had on the Idris group, I need to think about these issues before I write it up:

Your goal for this whole expression on the RHS is to show that S (plus n 0) = S n

(Given that that looks like the type signature of plusZeroRightNeutral itself, only with S applied to both sides, at this point I use cong : (a = b) -> f a = f b.
Which says, "given an equality, make a new equality by applying the same function to both sides".

So you could write this line as plusZeroRightNeutral (S n) = cong $ plusZeroRightNeutral n,
or cong {f = S} $ plusZeroRightNeutral n if you prefer, to make it explicit what cong is applying to both sides of the equality.)

We can get both sides of this to be equal by rewriting the "plus n 0" part - we have an equality that fits that in scope: plusZeroRightNeutral : (x : Nat) -> (plus x Z) = x
So "plusZeroRightNeutral n" will be of type "plus n Z = n", meaning anywhere we see "plus n 0" we can have it replace that with n. And then S n = S n is just Refl (reflexive equality - a thing equals itself).

OK, I was trying to get from a proof of (plus n 0) = n to a proof of (plus (S n) 0) = S n because that seemed to be whats required for induction.
can Idris do the S (plus n 0) to (plus (S n) 0) stage itself?


Incidentally, you don't have to assign that to a variable e.g. "inductiveHypothesis" if you don't want - you could just apply it directly with: plusZeroRightNeutral (S n) = rewrite plusZeroRightNeutral n in Refl
Maybe it's just a style thing - could be a remnant from before we had the "rewrite" syntax, and proofs were often done in the interactive "tactics" mode (since deprecated): http://docs.idris-lang.org/en/latest/reference/tactics.html
They would get things set up to being at:

plusZeroRightNeutral (S n) =
    let inductiveHypothesis = plusZeroRightNeutral n in ?foo
and then call ":prove foo" at the repl.
After running the "intros" tactic, it gave you:

----------              Assumptions:              ----------
 k : Nat
 inductiveHypothesis : plus k 0 = k
----------                 Goal:                  ----------
{hole_2} : S (plus k 0) = S k

At which point you would apply the "rewrite" tactic with your inductive hypothesis.

Hardly seems necessary to me, though. Go with whatever makes the most sense to you.

Yes, I was wondering why that was, I assumed it was giving 'rewrite' (or the human reader) some clue about what the property was.

==> and <== were introduced in a blog post by Edwin Brady which I can't find at the moment - maybe we could find where that went later.
They're kind of mentioned here: http://docs.idris-lang.org/en/latest/reference/misc.html#match-application, which is a version of this test (only with older syntax which no longer works, which you see commented out in this test):
https://github.com/idris-lang/Idris-dev/blob/master/test/proof001/test029.idr

From what I recall, and looking at that, I thought it was a way of supplying a goal type or target to your rewrite, to better tell Idris how to apply the rewrite and to get better error messages if it didn't work, and as documentation for yourself.
Similar to how you might use the preorder reasoning syntax to document the type after each step being applied when doing a proof:
http://docs.idris-lang.org/en/latest/reference/misc.html#preorder-reasoning

I got your example to typecheck with "rewrite inductiveHypothesis ==> (S k = S k) in Refl", but I'm not really clear what's going on or how exactly that's helping - that S k = S k is already the type of Relf (which you're rewriting).
I also see that in use in libs/base/Data/Vect.idr.

but I would like to try to understand rewrite without the syntactic sugar so that I can go on to more complicated examples with some intuition.

Some nores from this thread:

Generally proof equations are written as complexity-reducing devices, with the more complex part on the left and the less complex on the right. For example, the monoid neutral law looks like n + 0 = n, because n is simpler than n + 0. But with factors, the reduction in complexity is to say that a larger number can be written as the product of smaller numbers, so I think n = p * q is appropriate.

I try to use rewrite rather than replace whenever I can, but it's not always possible. There is the huge difference between them, however.

replace makes a substitution in a proof you already have to create another proof. rewrite makes a substitution in the goal (which is a proof you do not have yet) instead.

In practice it means that with rewrite you work kind of backwards, rewriting your goal until it matches something you already have, while replace has a more direct approach. Also with rewrite you can only use equality (=) proofs (the same with replace of course), which means that you you need use a custom proof-altering function like cong or something in the middle of replacements, you actually can no longer use rewrite from that point on.

For some reason I don't feel I am going to understand 'rewrite' fully unless I can do it using 'replace'.

This is my attempt but it fails (Unifying n and S n would lead to infinite value):

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

total plusZeroRightNeutralRep : (x : Nat) -> (plus x Z) = x
plusZeroRightNeutralRep Z     = Refl
plusZeroRightNeutralRep (S n) =
    let m = (S n) in
      replace {P = prop} (the (m = (S n)) Refl) plusZeroRightNeutralRep n

Replace

Parity may have some interesting examples.

This implements the indiscernability of identicals principle, if two terms are equal then they have the same properties. In other words, if ``x=y``, then we can substitute ``y`` for ``x`` in any expression. In our proofs we can express this as:

    if x=y
    then P x = P y

where ``P`` is a pure function representing the property. In the examples below ``P`` is an expression in some variable with a type like this: ``P: n -> Type``.

So if ``n`` is a natural number variable then ``P`` could be something like ``2*n + 3``.

To use this in our proofs there is the following function in the prelude:

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

Removing the implicits, if we supply an equality ``x=y`` and a proof of a property of ``x`` (i.e. ``P x``) then we get a proof of a property of ``y`` (i.e. ``P y``)

    > :t replace
    replace : (x = y) -> P x -> P y
So we can call replace like this:
testReplace2: (x=y) -> (x=plus x Z) -> (y=plus y Z)
testReplace2 a b = replace a b

This replaces (x=plus x Z) with (y=plus y Z). To do this replace infers the property: P x is (x=plus x Z).

This example does not really do anything, it just changes the name of the variable (α-conversion in lambda calculus).

A more useful example would be something like this:
testReplace3: ((S x)=y) -> ((S x)=plus (S x) Z) -> (y=plus y Z)
testReplace3 a b = replace a b
but this produces this error:
    |
103 | testReplace3 a b = replace a b
    |                    ~~~~~~~~~~~
When checking right hand side of testReplace3 
with expected type
        y = plus y 0

When checking an application of function replace:
        Type mismatch between
                S x = plus (S x) 0 (Type of b)
        and
                P (S x) (Expected type)
        
        Specifically:
                Type mismatch between
                        S x = S (plus x 0)
                and
                        P (S x)

Holes: Main.testReplace3
      
It doesn't seem to be able to infer P in this case so we need to help it by suppling the property like this:
p2: Nat -> Type
p2 x = (x=plus x Z)

testReplace3: ((S x)=y) -> ((S x)=plus (S x) Z) -> (y=plus y Z)
testReplace3 a b = replace {P = p2} a b

So can we prove (x=plus x Z) for all values of x?

Since we can't have an infinite number of cases like this:

we need to do it recursivly.

plusZeroRightNeutral3 : (y : Nat) -> y = (plus y Z)
plusZeroRightNeutral3 Z = Refl
plusZeroRightNeutral3 (S Z) = the (1 = (plus 1 Z)) Refl
plusZeroRightNeutral3 (S (S Z)) = the (2 = (plus 2 Z)) Refl
plusZeroRightNeutral3 (S (S (S Z))) = the (3 = (plus 3 Z)) Refl

Or change it so left and right depend on the same natural number.

plusZeroRightNeutral4 : (y : Nat) -> y = (plus y Z)
plusZeroRightNeutral4 Z = Refl
plusZeroRightNeutral4 (S Z) = the (p2 1) Refl
plusZeroRightNeutral4 (S (S Z)) = the (p2 2) Refl
plusZeroRightNeutral4 (S (S (S Z))) = the (p2 3) Refl

We need a case that says that if 'plusZeroRightNeutral3 x' constructs Refl then 'plusZeroRightNeutral3 (S x)' will constructs Refl.

If we replace the literal natural numbers with 'n' like this:

plusZeroRightNeutral5 : (y : Nat) -> y = (plus y Z)
plusZeroRightNeutral5 Z = Refl
plusZeroRightNeutral5 (S n) = the (p2 (S n)) Refl

then we get this error

    |
119 | plusZeroRightNeutral5 (S n) = the (p2 (S n)) Refl
    |                               ~~~~~~~~~~~~~~~~~~~
When checking right hand side of plusZeroRightNeutral5 with expected type
        S n = plus (S n) 0

When checking argument value to function Prelude.Basics.the:
        Type mismatch between
                S (plus n 0) = S (plus n 0) (Type of Refl)
        and
                p2 (S n) (Expected type)
        
        Specifically:
                Type mismatch between
                        plus n 0
                and
                        n

Holes: Main.plusZeroRightNeutral5

Another Example

Example from: Idris-dev/samples/tutorial/Theorems.idr and test/tutorial004/tutorial004.idr

total disjoint : (n : Nat) -> Z = S n -> Void
disjoint n p = replace {P = disjointTy} p ()
  where
    disjointTy : Nat -> Type
    disjointTy Z = ()
    disjointTy (S k) = Void

This takes the equation 'Z = S n'

and subsitites to 'Void = ()' which does not have a constructor so is Void.


Rewrite

https://medium.com/@prozacchiwawa/beginner-notes-on-proofs-in-idris-f7322cbe2086

rewrite t in Refl
takes Refl : left = right object and expr : t.
Searches left in t.
Replaces all occurrences of left with right in t

 

Like replace, rewrite can apply substitutions but is built into the Idris syntax and not purely a library function. In addition to the special syntax there are differences from replace.

Here is the rewrite syntax (from Idris-dev/src/Idris/Parser/Expr.hs):
@
RewriteTerm ::=
  'rewrite' Expr ('==>' Expr)? 'in' Expr
  ;
@

there is an optional '==>' term

So when the compiler encounters 'rewrite' it infers the property 'P' and then uses rewrite__impl from libs/prelude/Builtins.idr
||| Perform substitution in a term according to some equality.
|||
||| Like `replace`, but with an explicit predicate, and applying the rewrite
||| in the other direction, which puts it in a form usable by the `rewrite`
||| tactic and term.
rewrite__impl : (P : a -> Type) -> x = y -> P y -> P x
rewrite__impl p Refl prf = prf

      

Rewrite can be dificult to use and debug. This is because the intemediate values of types are not always given in the source code and since we are relying on the automatic pattern matching and normalisation that the compiler does. So there may not be many clues to the reader of the source code. When debuging we tend to get error messages like:

Which don't give many clues about what is going on.

There is ==> and <==, to add extra type annotations to rewrite: http://docs.idris-lang.org/en/latest/reference/misc.html#match-application but these are not fully documented and are seldom used.

Here is an example:
rewrite ((m + Z = m) <== plusZeroRightNeutral) ==>
        (Z + m = m) in Refl

This is linked as a syntax example from release notes (http://www.idris-lang.org/idris-0-9-9-released/), but has bitrotted. A up-to-date example version of this can be found in the tests: https://github.com/idris-lang/Idris-dev/blob/master/test/proof001/test029.idr

plus_comm : (n : Nat) -> (m : Nat) -> (n + m = m + n)

-- Base case
(O + m = m + O) <== plus_comm = 
    rewrite ((m + O = m)
       <== plusZeroRightNeutral) ==> 
            (O + m = m) in refl

-- Step case
(S k + m = m + S k) <== plus_comm =
    rewrite ((k + m = m + k)
        <== plus_comm) in
    rewrite ((S (m + k) = m + S k)
        <== plusSuccRightSucc) in
          refl

If both sides of the equation don't normalise to the same value/type then we may be able to use rewrite so they do:

plus_commutes_Z : m = plus m 0
plus_commutes_Z {m = Z} = Refl
plus_commutes_Z {m = (S k)} = let rec = plus_commutes_Z {m=k} in
                                  rewrite rec in Refl
For instance, in this example:

What is the type of this last Refl?

I would be expecting something like m=(S n) so it would rewrite
(plus (S n) 0 = (S n)) as (plus m 0 = m) but how do you introduce a new variable and prove that it is equal to something?

If I put a hole like this:

rewrite inductiveHypothesis in ?myrefl

I get:

Holes: Main.myrefl 
 
*> :type myrefl
  n : Nat
  inductiveHypothesis : plus n 0 = n
  _rewrite_rule : plus n 0 = n
--------------------------------------
myrefl : S n = S n

So how does that work? 'm' and 'plus m 0' dont normalise to the same value so how can Refl construct the type 'm = plus m 0' ?

If we have   X:x=z
then   rewrite X in Y

will do a substitution to replace all occurences of x with y in Y.

replace : (x = y) -> P x -> P y

Given a proof that x = y, and a property P which holds for x, we can get a proof of the same property for y, because we know x and y must be the same. In practice, this function can be a little tricky to use because in general the implicit argument P can be hard to infer by unification, so Idris provides a high level syntax which calculates the property and applies replace:

I am trying to find a simple example to experiment with rewrite:

It does not seem to make sence using rewrite with literal values:
testRewriteNull: Z=Z
testRewriteNull = rewrite (the (Z=Z) Refl) in Refl
because any rewrite is trivial:
    |
135 | testRewriteNull = rewrite (the (Z=Z) Refl) in Refl
    |                   ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking right hand side of testRewriteNull with
                 expected type
        0 = 0

rewriting 0 to 0 did not change type 0 = 0
So, to demonstrate rewrite, we need to find an example with variables:
testRewriteNull: (a:Nat) -> a=a
testRewriteNull a = rewrite (the (a=a) Refl) in Refl
even so we still need more structure for a meaningful example:
    |
135 | testRewriteNull a = rewrite (the (a=a) Refl) in Refl
    |                     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking right hand side of testRewriteNull with
         expected type
        a = a

rewriting a to a did not change type a = a
Proving x = x + Z is the simplest meaningfull example I can think of: rewrite

 

 

rewrite prf in expr

If we have prf : x = y, and the required type for expr is some property of x, the rewrite ... in syntax will search for x in the required type of expr and replace it with y

for example

rewrite x=y in x=x+0

gives y=y+0

so rewrite (S n)=n in 5=5+0

gives 4=4+0

total plusZeroRightNeutral2 : (x : Nat) -> (plus x Z) = x
plusZeroRightNeutral2 Z     = Refl
plusZeroRightNeutral2 (S n) =
    let inductiveHypothesis = plusZeroRightNeutral2 n in
      rewrite inductiveHypothesis in Refl





 
-- without 'let'
total plusZeroRightNeutral21 : (x : Nat) -> (plus x Z) = x
plusZeroRightNeutral21 Z     = Refl
plusZeroRightNeutral21 (S n) =
      rewrite (plusZeroRightNeutral21 n) in Refl
 
prop : (x : Nat) -> Type
prop x = (plus x Z) = x

propS : (x : Nat) -> Type
propS x = (plus (S x) Z) = (S x)

propRev : (x : Nat) -> Type
propRev x = x = (plus x Z)

rewrite__impl requires an explicit property

This gives an error:

plusZeroRightNeutral21x : (x : Nat) -> (plus x Z) = x
plusZeroRightNeutral21x Z     = Refl
plusZeroRightNeutral21x (S n) =
  rewrite__impl prop (plusZeroRightNeutral21x n) Refl

When checking right hand side of
    plusZeroRightNeutral21x with expected type
        plus (S n) 0 = S n

When checking an application of function rewrite__impl:
        Type mismatch between
                n = n (Type of Refl)
        and
                prop n (Expected type)
        
        Specifically:
                Type mismatch between
                        n
                and
                        plus n 0

Holes: Main.plusZeroRightNeutral21x

try changing (plus x Z) = x to x = (plus x Z) which now gives this error:

 

plusZeroRightNeutral21xr : (x : Nat) -> x = (plus x Z)
plusZeroRightNeutral21xr Z     = Refl
plusZeroRightNeutral21xr (S n) =
  let inductiveHypothesis = plusZeroRightNeutral21xr n in
    rewrite__impl propRev inductiveHypothesis Refl

    |
127 |     rewrite__impl propRev inductiveHypothesis Refl
    |                           ~~~~~~~~~~~~~~~~~~~
When checking right hand side of
   plusZeroRightNeutral21xr with expected type
        S n = plus (S n) 0

When checking an application of function rewrite__impl:
        Unifying n and S n would lead to infinite value

Holes: Main.plusZeroRightNeutral21xr

Try defining simpler examples:

x
-- rewrite__impl requires an explicit property
testRewritex3: (y=x) -> (prop x) -> (prop y)
testRewritex3 a b = rewrite__impl prop a b

testRewritex: {x,y:Nat} -> (y=x) -> (prop x) -> (prop y)
testRewritex a b = rewrite a in b

see this thread

One of the difficulties of writing programs with dependent types is that when you write a function
implementation, you have to prove that the type of the returned value is the same as that in the
definition.

Replace and rewrite do that but the syntax used in them can hinder the readability of the code,
making very simple proofs very difficult for no reason.

There is a nice syntax for rewrite that is like this:

rewrite ((m + Z = m) <== plusZeroRightNeutral) ==>
        (Z + m = m) in Refl

as can be seen in misc.rst
but it is not adequately documented.

This syntax is nice because when someone reviews the proof, they can see the changed type
 as is common in mathematical proofs.

A secondary issue regarding the readability of the code when using rewrite and the "match" 
application syntax can be found in #3425.

The difference from ``replace`` above is nicer syntax and the property ``p1`` is explicitly supplied and it goes in the opposite direction (input and output reversed).

Example: again we supply ``p1`` which is a proof that ``x=2`` and the equality ``x=y`` then we get a proof that ``y=2``.

    p1: Nat -> Type
    p1 x = (x=2)
    
    testRewrite2: (x=y) -> (p1 y) -> (p1 x)
    testRewrite2 a b = rewrite a in b

We can think of rewrite doing this:

That is, we are doing a substitution.

testRewrite: (x=y) -> (p1 y) -> (p1 x)
testRewrite a b = rewrite__impl p1 a b

Issues

From Wikipedia:

In mathematics, a change of variables is a basic technique used to simplify problems in which the original variables are replaced with functions of other variables. The intent is that when expressed in new variables, the problem may become simpler, or equivalent to a better understood problem.

In Idris we need to be able to prove that equations represent the same type, for instance, if a function requires a term of the type: 'x=x+0' can we pass it a term of the type: 'x=x+0' or pehaps '2=2+0'?

Note on terminology: strictly there is a distiction between the term 'substitution' and 'change of variables'. In a system of equations we can only change variable if it is not used in the other equations. For instance:

The equation 'x=x+0' expresses the same identity as 'y=y+0'. The name of the variable does not matter (a bit like alpha equivalence in lambda calculus where the choice of a bound variable name does not matter provided it is not bound to an outer term).

Substitution as Pullback

Can we express substitution in category theory terms? See discussion on page here.

  Substitution of a term into a predicate is pullback, but substitution of a term into a term is composition.
Type theory version Substitution of a term into a dependant type is pullback, but substitution of a term into a term is composition.

There is a discussion of this topic on this site.

So why the difference? I think in the predicate case we are going backwards.

Typically a predicate could be an equation which may be true or false depending on the values of its variables.

Or a function from a variable to bool (or some truth object).

diagram

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.