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.
Associatively Property
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:
|
|
commutativity
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)
Fibrations and Proof
As an example lets invent an algebra and try to prove, in this algebra, that x=x+0.
In this algebra there are 3 elements 0, 1 and 2. Then there is one operation +.
 |
So given that 0=0+0 , 1=1+0 and 2=2+0 then we want to prove that x=x+0. That is, given some property that is true for every element we want to prove that it is true for the set as a whole. |
More information on these pages:
- Fibrations
- Proof of Equality
- Writing code for implementing algebras on this page
Next
See pages here which show this used in the Idris language.