Commutativity of +

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.

[Next] Troubleshooting

Original Copyright © Takahiro Seino, all rights reserved.