if-statement - ATS 证明 : Why does this static if need greater than or equal to?

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' 失败时。