Prove the associativity of
NAT+, that is, prove
(i + j) + k = i + (j + k) for each
k, with the induction on
First, Module expression
NAT+ + EQL is opened by the
open NAT+ + EQL .
Next, declare Constants
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.
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.