Proving an addition function is associative using Coq

Question

I am trying to prove that a predefined addition function is associative, but I am stuck at the step where the goal reads

plus (S x') (plus y z) = plus (plus (S x') y) z

but the only hypothesis I have is :

IHx' : forall y z : nat,
plus x' (plus y z) = plus (plus x' y) z

Answer 1

You should use the definition of your function plus at this point, for instance using a function to evaluate your goal such as cbn (simpl or lazy may also work). Then you obtain a goal where your induction hypothesis apply so you can finish with congruence.

By the way, the base case when x = 0 can be solved simply by computation so reflexivity suffices.

Answer 2

You have proved that plus 0 x = x, but you can also (easily) prove that plus (S x) y = S (plus x y). If you do that, you can rewrite your goal into S (plus x' (plus y z)) = S (plus (plus x' y) z) and then you can rewrite with your induction hypothesis.