if-statementtheorem-provingats

ATS Proof: Why does this static if need greater than or equal to?

I was writing a proof of a*0=0 and I stumbled on some strangeness. Why does the sif a >= 0 on line 7 need to be a >=, and does not compile when its just 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 () = ()

Intuitively, the a=0 should be handled fine by either path, yet only the first path works. Why?

Solution

  • MULneg is declared as follows:

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

    Note that 'm' is required to be positive. In your case, 'm' is '~a'. If you use '>' instead of '>=', then it cannot be inferred that '~a > 0' holds when the test 'a > 0' fails.