Associativity of +

Prove the associativity of + in NAT+, that is, prove (i + j) + k = i + (j + k) for each i, j and k, with the induction on i.

First, Module expression NAT+ + EQL is opened by the open command.

open NAT+ + EQL .

Next, declare Constants i, j and k of Sort Nat as arbitrary natural numbers:

-- declaring three arbitrary numbers i,j and k on the sort Nat:
ops i j k : -> Nat .

Prove the base step, that is, prove the equation for i = 0:

-- base step:
red (0 + j) + k = 0 + (j + k) .
--> should be true.

Prove the induction step: prove (s(i) + j) + k = s(i) + (j + k) under the induction hypothesis (i + j) + k = i + (j + k). The induction hypothesis is declared as an equation in a proof score.

-- induction hypothesis:
eq (i + j) + k = i + (j + k) .
-- inductive step:
red (s(i) + j) + k = s(i) + (j + k) .
--> should be true.

Finally, close the opened module by the close command. The constants and equations are released.

close

All operators and equations declared after opening a module are active until closing the module. So, it should be careful declaring several operators and equations in a proof score. For example, consider the following wrong proof score for proving some property by the case splitting: a natural number n is odd or not:

...
-- case: n is an arbitrary odd number.
eq odd(n) = true .
...
-- case: n is an arbitrary even number.
eq odd(n) = false .
...

Since inconsistent equations are declared in a single open-close unit, this proof score is inconsistent (true = false can be deduced!). To avoid such troubles, do not forget closing a module when each basic building block finished.

open NAT-EVENODD .
...
-- case: n is an arbitrary odd number.
eq odd(n) = true .
...
close

open NAT-EVENODD .
...
-- case: n is an arbitrary even number.
eq odd(n) = false .
...
close

[Next] Commutativity of +

Original Copyright © Takahiro Seino, all rights reserved.