`=`

The built-in equality predicate `_=_`

takes terms of the same sort and returns `true`

when they are reduced into a same term.

The equality predicate `_=_`

is defined in the built-in module `EQL`

as follows:

sys:mod! EQL { imports { protecting (TRUTH) } signature { pred _ = _ : _ Cosmos _ _ Cosmos _ { comm prec: 51 } } axioms { eq CUX = CUX = true . } }

(*) The equality predicate `_=_`

and the keyword `_=_`

in the equation declaration are confusing. When using the equality predicate in an equation, it is recommended to put a term in brackets like `eq p(N:Nat, M:Nat) = (N = M) .`

The following is an example of equational reasoning with the equality predicate `_=_`

:

CafeOBJ>select NAT+ + EQLNAT+ + EQL>red s(s(0)) + 0 = s(0) + s(0) .-- reduce in NAT+ + EQL : s(s(0)) + 0 = s(0) + s(0) true : Bool (0.004 sec for parse, 6 rewrites(0.002 sec), 9 matches) NAT+ + EQL>

The expression `NAT+ + EQL`

is a module expression which stands for the sum of `NAT+`

and `EQL`

. In the first line, `NAT+ + EQL`

is selected, and elements of both modules can be used hereafter. In the next line, try to reduce the equation of `s(s(0)) + 0`

and `s(0) + s(0)`

. Here, the symbol `_=_`

is the equality predicate. In the fourth line, CafeOBJ system returns `true`

, which means that the input terms are equivalent.

The equality predicate `_=_`

(or reduction) does not give a complete equational reasoning. Only the output `true`

is trustworthy. From syntactical and/or semantical reasons, it may fail to prove an equation even if it is true.

The following is an example of equational reasoning with `_=_`

which fails to prove the equation `n + m = m + n`

for arbitrary elements `n, m`

, that is, the commutativity of `+`

:

CafeOBJ>open NAT+ + EQL .-- opening module NAT+ + EQL.. done. %NAT+ + EQL>ops n m : -> Nat . -- arbitrarily choosen two naturals n and m%NAT+ + EQL>red n + m = m + n . -- try to verify + is commutative_* -- reduce in %NAT+ + EQL : n + m = m + n n + m = m + n : Bool (0.003 sec for parse, 0 rewrites(0.010 sec), 9 matches) %NAT+ + EQL>closeCafeOBJ>

The output term is not `true`

, though the commutativity of `+`

holds for `NAT+`

.

CafeOBJ>open NAT+ + EQL .-- opening module NAT+ + EQL.. done. %NAT+ + EQL>ops n m : -> Nat .%NAT+ + EQL>op _+_ : Nat Nat -> Nat { comm } .%NAT+ + EQL>red n + m = m + n .-- reduce in %NAT+ + EQL : n + m = m + n true : Bool (0.002 sec for parse, 1 rewrites(0.003 sec), 9 matches) %NAT+ + EQL>closeCafeOBJ>

Original Copyright © Takahiro Seino, all rights reserved.