Replace subexpression in equality proof in Idris

Question

As an exercise in Idris I am trying to prove this property:

multCancel : (a:Nat) -> (b:Nat) -> (c:Nat) -> (S a) * b = (S a) * c -> b = c

I came to the conclusion, that as an itermediate step, I need to prove something like this:

lemma1 : {x:Nat} -> {y:Nat} -> {z:Nat} -> (x + x) + (x * z) = (y + y) + (y * z) -> (x * (S (S z))) = (y * (S (S z)))
lemma1 {x=x} {y=y} {z=z} prf = ?todo

Of course, I already have proven that:

plusDouble : (a:Nat) -> (a + a) = a*2
plusDouble a =
  rewrite multCommutative a 2 in
  rewrite plusZeroRightNeutral a in Refl

So I believe I basically only need to replace (x + x) by (x*2) and then invoke distributivity in order to prove lemma1 . I don't know how to do this replacement. I thought I could simply do something like

rewrite plusDouble x in ...

But that apparently won't work because the subexpression I want to replace is in prf and in in the goal.

Is there some general approach to this? Or something you would recommend in this particular case?

Answer 1

Ok, so I figured out that I do not have to always simplify the goal using rewrite rules but I can instead expand it to match the proof I get as argument.

Answer 2

The rewrite feature uses replace : (x = y) -> P x -> P y under the hood; it is figuring out what P should be (as far as I understand).

To replace x + x with x*2 you may use the equality x + x = x*2 as you have. To replace x*2 with x + x you may use the equality x*2 = x + x; that is sym prf in your case. You need two replacements to achieve both.

When the rewrite tool (or inference) cannot figure it out you can explicitly provide P, such as replace {P = \x' => x' + (x * z) = (y + y) + (y * z)} (plusDouble x) prf. This is particularly useful when you need to rewrite some sites of x + x but not all.