Proof scores

A single reduction can prove a simple equation. More complex properties are proved by combining several reductions, which is called a proof score. A basic building block of a proof score is a proof of an implication 'E1 implies E2':

• Open a module with the open command.
• Declare constants (operators with the empty arity) as arbitrary elements used in E1 and E2.
• Declare equations E1.
• Reduce equations E2.

The difference between open and select is that operators and equations can be declared when a module opened.

When all reductions of E2 return true, it is guaranteed that the above property holds. By combining basic building blocks, case splitting, introducing lemma and induction can be done. While CafeOBJ system guarantees a single equational reasoning by reduction, the user is responsible for the correctness of a proof score.

Comments are important especially for proof scores. Comments enough to understand the proof score are expected to be included in a proof score.

For example, the following text file is a proof score of the associativity of + in NAT+:

-- CLAIM: associativity over _+_
--        \forall i, j, k \in Nat: (i + j) + k = i + (j + k)
-- will be proven by induction on i.

-- PROOF:

open NAT+ + EQL .

-- declaring three arbitrary numbers i,j and k on the sort Nat:
ops i j k : -> Nat .

-- base step:
red ((0 + j) + k) = (0 + (j + k)) .
--> should be true.

-- induction hypothesis:
eq (i + j) + k = i + (j + k) .
-- inductive step:
red ((s(i) + j) + k) = (s(i) + (j + k)) .
--> should be true.

close

-- Q.E.D.

The meaning of this proof score will be explained later. Save the above text file as simple-nat-proof-assoc.mod, and read it by the in command. Then, CafeOBJ system shows its result as follows:

CafeOBJ> in simple-nat-proof-assoc.mod
processing input : /Users/seino/simple-nat-proof-assoc.mod_*
-- opening module NAT+ + EQL.. done._*
-- reduce in %NAT+ + EQL : (0 + j) + k = 0 + (j + k)
true : Bool
(0.003 sec for parse, 3 rewrites(0.002 sec), 11 matches)
--> should be true.*
-- reduce in %NAT+ + EQL : (s(i) + j) + k = s(i) + (j + k)
true : Bool
(0.004 sec for parse, 5 rewrites(0.003 sec), 26 matches)
--> should be true.
CafeOBJ> 

Since the all reductions (base step and induction step) return true, the associativity of + has been proved.

[Next] Equality predicate =

Original Copyright © Takahiro Seino, all rights reserved.