Maths - Proof of Equality

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:

(zero + n) + p == zero + (n + p)
(m + n) + p == m + (n + p)
(suc m + n) + p == suc m + (n + p)

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)

 
 
 

Next

See pages here which show this used in the Idris language.

 


metadata block
see also:
Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

 

Commercial Software Shop

Where I can, I have put links to Amazon for commercial software, not directly related to the software project, but related to the subject being discussed, click on the appropriate country flag to get more details of the software or to buy it from them.

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2022 Martin John Baker - All rights reserved - privacy policy.