'Proving an addition function is associative using Coq
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
Solution 1:[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.
Solution 2:[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.
Sources
This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.
Source: Stack Overflow
| Solution | Source |
|---|---|
| Solution 1 | kyo dralliam |
| Solution 2 | larsr |