Equality predicate =

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+ + EQL
NAT+ + 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> close
CafeOBJ> 

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> close
CafeOBJ> 

[Next] Associativity of +

Original Copyright © Takahiro Seino, all rights reserved.