Proof function for an elementary statement about multiplication

Question

If we have three integers a>0, b, ab>=0 such that a*b=ab, then b>=0 and if ab=0 then b=0, if ab>0 then ab>0.

What is the good way to implement this statement as a proof function in ATS?

I guess the proof function must be something like this:

prfn lemma_mul_gez
    {a:  pos}
    {b:  int}
    {ab: nat}
    ( pf: MUL(a,b,ab) )
    : [b >= 0; (ab == 0 && b == 0) || (ab > 0 && b > 0)] void
  = (* ... implementation here ... *)

Answer 1

I was able to write a correct proof function. But my solution is quite long:

  prfun lemma_nat_mul_1_is_nat
    {x: nat}
    {y: int}
    .<x>.
    ( pf_x1: MUL(x,1,y) )
    : [y == x] void
  = sif x <= 0 
      then let
          prval pf_01_0 = MULbas{1}()
          prval _       = mul_isfun(pf_01_0, pf_x1)
        in () end
      else let
          prval pf_xm1  = mul_istot{x-1,1}()
          prval _       = lemma_nat_mul_1_is_nat{x-1}(pf_xm1)
          prval pf2_x1  = mul_add_const{1}{x-1,1}(pf_xm1)
          prval _       = mul_isfun(pf_x1, pf2_x1)
        in () end


  prfn lemma_x_mul_1_is_x
    {x: int}
    {y: int}
    ( pf_x1: MUL(x,1,y) )
    : [y == x] void
  = sif x < 0 
      then let
          prval pf_neg = mul_istot{~x,1}()
          prval _      = lemma_nat_mul_1_is_nat{~x}(pf_neg)
          prval pf2_x1 = mul_negate{~x,1}(pf_neg)
          prval _      = mul_isfun(pf_x1, pf2_x1)
        in () end
      else lemma_nat_mul_1_is_nat{x}{y}(pf_x1)


  prfn lemma_mul_gez
    {a:  pos}
    {b:  int}
    {ab: nat}
    ( pf: MUL(a,b,ab) )
    : [b >= 0; (ab == 0 && b == 0) || (ab > 0 && b > 0)] void
  = let
    prfun loop
      {a:  pos}
      {b:  int}
      {ab: int}
      {i:  pos | i <= a}
      {ib: int | (ib < 0 && b < 0) || (ib == 0 && b == 0) || (ib > 0 && b > 0) }
      .<a-i>.
      ( pfi: MUL(i,b,ib)
      , pf : MUL(a,b,ab) )
      : [(ab < 0 && b < 0) || (ab == 0 && b == 0) || (ab > 0 && b > 0)] void
    = sif i >= a (* i == a *)
      then mul_isfun(pf,pfi)
      else let
          prval pfi_inc = mul_add_const{1}(pfi)
        in loop(pfi_inc, pf) end

    prval pf1 = mul_istot{1,b}()
    prval _   = lemma_x_mul_1_is_x(mul_commute(pf1))
  in loop(pf1, pf) end