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.modprocessing 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.

Original Copyright © Takahiro Seino, all rights reserved.