ATS - 约束 C3NSTRprop(C3TKmain(); S2Eeqeq(S2Eintinf(0); S2Evar(abc(4303)))) 指的是什么？

Question

我有以下 ATS 代码:

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 () = ()

代码的动机是使用依赖类型系统完成一个简单的练习:证明整数乘法是关联的。证明的思想是将 3 个整数变量 a、b、c 分解为它们符号的可能情况，然后将问题简化为证明自然数乘法的结合性，我们可以在其中使用归纳法。

从数学上讲，这个策略应该是合理的(尽管分解案例并制作一个巨大的决策树是乏味的)。问题是，当我尝试使用命令 patscc assoc.dats 编译上述文件时，我收到以下错误消息:

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)

坦率地说，我不知道如何解释此错误消息。什么是约束 C3NSTRprop(C3TKmain(); S2Eeqeq(S2Eintinf(0); S2Evar(abc(4303))))？

Answer 1

当前代码存在不少问题。例如，以下案例不起作用:

   case+ pf1 of
        | MULbas()     => MULbas()

因为abc==0还没有被证明。这可以很容易地修复如下:

   case+ pf1 of
        | MULbas()     => let prval MULbas() = pf3 in MULbas() end       

我不建议继续使用当前的验证代码。

一般来说，如果你想从第一性原理证明涉及MUL的定理，那么你几乎总是需要以下两个证明函数:

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

顺便说一句，mul_assoc 的以下实现通过了类型检查:

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] *)