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```

Original Copyright © Takahiro Seino, all rights reserved.