`+`

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

Original Copyright © Takahiro Seino, all rights reserved.