Search code examples
dependent-typeidristheorem-proving

Replace subexpression in equality proof in Idris

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?

Solution

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