ATS证明：为什么需要大于或等于此静态？

Question

[我正在写a*0=0的证明，但偶然发现了一些奇怪之处。为什么第7行上的sif a >= 0需要是>=，而当它只是sif > 0时却不编译？

prfn mul_ax0_0 {a:int} () : MUL(a,0,0) =
let
    prfun auxnat {a:nat} .<a>. () : MUL(a,0,0) =
        sif a == 0 then MULbas()
        else MULind(auxnat{a-1}())
in
    sif a >= 0 then auxnat{a}() // line 7
    else MULneg(auxnat{~a}())
end

implement main0 () = ()

直觉上，a=0应该通过任何一条路径都可以很好地处理，但只有第一个路径有效。为什么？

Answer 1

MULneg声明如下：

  | {m:pos}{n:int}{p:int}
    MULneg (~(m), n, ~(p)) of MUL_prop (m, n, p)

请注意，'m'必须为正数。在您的情况下，“ m”是“〜a”。如果您使用'>'而不是'> ='，则无法推断'〜a> 0'成立当测试“ a> 0”失败时。