`+`

Prove the commutativity of `+`

, that is, prove `i + j = j + i`

for each `i`

and `j`

with the induction on `i`

.

The following is a proof score of the base step:

open NAT+ + EQL . -- arbitarily choosen two naturals: ops i j : -> Nat . -- base step: red 0 + j = j + 0 . --> should be true. close

Unfortunately, this proof score does not return `true`

as follows:

-- reduce in %NAT+ + EQL : 0 + j = j + 0 j = j + 0 : Bool (0.002 sec for parse, 1 rewrites(0.001 sec), 6 matches) --> should be true. CafeOBJ>

When an unexpected output returned, check the output carefully. If the output is considered to be true, try to prove the output next. So, prove the following lemma next:

- Lemma 1.
`i + 0 = i`

for each`i`

.

The following is a proof score for Lemma 1:

-- LEMMA1: \forall i \in Nat: i + 0 = i . -- PROOF: open NAT+ + EQL . ops i : -> Nat . -- base step: red 0 + 0 = 0 . --> should be true. -- induction hypothesis: eq i + 0 = i . -- inductive step: red s(i) + 0 = s(i) . --> should be true. close -- Q.E.D.

CafeOBJ system returns `true`

for all reductions (base step and induction step) as follows:

-- opening module NAT+ + EQL.. done. -- reduce in %NAT+ + EQL : 0 + 0 = 0 true : Bool (0.001 sec for parse, 2 rewrites(0.000 sec), 2 matches) --> should be true.* -- reduce in %NAT+ + EQL : s(i) + 0 = s(i) true : Bool (0.001 sec for parse, 3 rewrites(0.001 sec), 5 matches) --> should be true.

After finishing the proof of a lemma, the lemma can be added to the proof score of `i + j = j + i`

as follows:

open NAT+ + EQL . -- arbitarily choosen two naturals: ops i j : -> Nat . -- base step: eq N:Nat + 0 = N . -- use LEMMA1. red 0 + j = j + 0 . --> should be true. close

Then, CafeOBJ system returns `true`

as follows:

-- opening module NAT+ + EQL.. done._* -- reduce in %NAT+ + EQL : 0 + j = j + 0 true : Bool (0.001 sec for parse, 3 rewrites(0.000 sec), 4 matches) --> should be true.

Now, the base step has been proved. The induction step also needs another lemma. Proving the induction step by finding and proving a lemma is left as a reader's exercise.

Original Copyright © Takahiro Seino, all rights reserved.