I have the following ATS code:
extern prfun mul_nx0_0 {n:int} (): MUL(n, 0, 0)
extern prfun mul_nx1_n {n:int} (): MUL(n, 1, n)
extern prfun mul_neg_1 {m,n,p:int} (MUL(m, n, p)): MUL(~m, n, ~p)
extern prfun mul_neg_2 {m,n,p:int} (MUL(m, n, p)): MUL(m, ~n, ~p)
extern prfun mul_assoc {a,b,c,ab,bc,abc:int}
( MUL(a, b, ab)
, MUL(b, c, bc)
, MUL(ab, c, abc)
): MUL(a, bc, abc)
primplmnt mul_assoc {a,b,c,ab,bc,abc:int} (pf1, pf2, pf3) =
let
prfun mul_assoc1 {a,b,c,ab,bc,abc:nat} .<a>.
(pf1: MUL(a, b, ab), pf2: MUL(b, c, bc), pf3: MUL(ab, c, abc)) : MUL(a, bc, abc) =
case+ pf1 of
| MULbas() => MULbas()
| MULind(pf1') =>
case+ pf2 of
| MULbas() => mul_nx0_0 {a} ()
| MULind(pf2') =>
case+ pf3 of
| MULbas() =>
sif a == 0
then MULbas()
else mul_nx0_0 {a} ()
| MULind(pf3') => MULind(mul_assoc1(pf1', pf2', pf3'))
in
sif a < 0
then let
prval _pf1 = mul_neg_1(pf1)
prval _pf3 = mul_neg_1(pf3)
in
sif b < 0
then let
prval __pf1 = mul_neg_2(_pf1)
prval _pf2 = mul_neg_1(pf2)
prval __pf3 = mul_neg_1(_pf3)
in
sif c < 0
then let
prval __pf2 = mul_neg_2(_pf2)
prval ___pf3 = mul_neg_2(__pf3)
in
MULneg(mul_assoc1(__pf1, __pf2, ___pf3))
end
else MULneg(mul_neg_2(mul_assoc1(__pf1, _pf2, __pf3)))
end
else MULneg(mul_assoc1(_pf1, pf2, _pf3))
end
else sif b < 0
then sif c < 0
then let
prval _pf1 = mul_neg_2(pf1)
prval _pf2 = mul_neg_1(mul_neg_2(pf2))
prval _pf3 = mul_neg_1(mul_neg_2(pf3))
in
mul_assoc1(_pf1, _pf2, _pf3)
end
else let
prval _pf1 = mul_neg_2(pf1)
prval _pf2 = mul_neg_2(pf2)
prval _pf3 = mul_neg_2(pf3)
in
MULneg(mul_assoc1(_pf1, _pf2, _pf3))
end
else sif c < 0
then let
prval _pf2 = mul_neg_1(pf2)
prval _pf3 = mul_neg_1(pf3)
in
MULneg(mul_assoc1(pf1, _pf2, _pf3))
end
else mul_assoc1(pf1, pf2, pf3)
end
implement main0 () = ()
The motivation of the code is to complete a simple exercise using the dependent type system: to prove that multiplication of integers is associative. The idea of the proof is to break the 3 integer variables, a,b,c, into the possible cases for their signs, and then reduce the problem to proving associativity for multiplication of natural numbers, where we can use induction.
Mathematically, this strategy ought to be sound (although breaking down the cases and making a huge decision tree was tedious). The problem is, when I try to compile the above file using the command patscc assoc.dats, I get the following error message:
assoc.dats: 591(line=20, offs=27) -- 599(line=20, offs=35): error(3): unsolved constraint: C3NSTRprop(C3TKmain(); S2Eeqeq(S2Eintinf(0); S2Evar(abc(4303))))
typechecking has failed: there are some unsolved constraints: please inspect the above reported error message(s) for information.
exit(ATS): uncaught exception: _2tmp_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
Frankly, I have no idea how to interpret this error message. What is the constraint C3NSTRprop(C3TKmain(); S2Eeqeq(S2Eintinf(0); S2Evar(abc(4303))))?
There are quite a few issues with the current code. For instance, the following case does not work:
case+ pf1 of
| MULbas() => MULbas()
because abc==0 has not be proven yet. This can be readily fixed as follows:
case+ pf1 of
| MULbas() => let prval MULbas() = pf3 in MULbas() end
I would not suggest to continue with the current proof code.
In general, if you want to prove theorems involving MUL from the first principle, then you almost always need the following two proof functions:
extern
prfun
mul_is_tot
{a,b:int}() : [c:int] MUL(a, b, c)
extern
prfun
mul_is_fun
{a,b,c1,c2:int}
( pf1: MUL(a, b, c1)
, pf2: MUL(a, b, c2)): [c1==c2] void
By the way, the following implementation of mul_assoc passes type-checking:
extern
prfun
mul_is_tot
{a,b:int}() : [c:int] MUL(a, b, c)
extern
prfun
mul_is_fun
{a,b,c1,c2:int}
( pf1: MUL(a, b, c1)
, pf2: MUL(a, b, c2)): [c1==c2] void
extern
prfun
mul_distrib
{a,b,c,ac,bc:int}
( MUL(a, c, ac)
, MUL(b, c, bc)): MUL(a+b, c, ac+bc)
extern
prfun
mul_assoc
{a,b,c,ab,bc,abc:int}
( pf1: MUL(a, b, ab),
pf2: MUL(b, c, bc),
pf3: MUL(ab, c, abc)): MUL(a, bc, abc)
extern
prfun
mul_neg_1
{m,n,p:int}(MUL(m, n, p)): MUL(~m, n, ~p)
primplmnt
mul_assoc
{a,b,c
,ab,bc,abc:int}
(pf1, pf2, pf3) =
(
sif
(a >= 0)
then
mul_assoc1(pf1, pf2, pf3)
else
mul_neg_1(mul_assoc1(mul_neg_1(pf1), pf2, mul_neg_1(pf3)))
) where
{
prfun
mul_assoc1
{a:nat
;b,c,ab,bc,abc:int} .<a>.
( pf1: MUL(a, b, ab),
pf2: MUL(b, c, bc),
pf3: MUL(ab, c, abc)): MUL(a, bc, abc) =
(
case+ pf1 of
| MULbas() =>
let
prval MULbas() = pf3 in MULbas()
end
| MULind(pf1') => // a = a'+1 // ab = a'b + b
let
prval pf3' = mul_is_tot() // (a'*b)*c
prval res' = mul_assoc1(pf1', pf2, pf3') // (a'*b)*c = a'*(b*c)
prval ( ) = mul_is_fun(pf3, mul_distrib(pf3', pf2))
in
MULind(res')
end
)
} (* end of [mul_assoc] *)