On the previous page we discussed type theoretical encodings for mathematical structures that are suitable for proofs. Here we go on to discuss how to use them to do proofs.
To prove associatively, we take P m to be the property:
(m + n) + p == m + (n + p)
Here n and p are arbitrary natural numbers, so if we can show the equation holds for all m it will also hold for all n and p. The appropriate instances of the inference rules are:
We want to prove:
m + n == n + m
Does it help to deconstruct one of the operands as before?
0 + n == n + 0
(1 + m) + n == n + (1 + m)
See pages here which show this used in the Idris language.