Функция доказательства для элементарного утверждения о умножении - PullRequest
Новая
       26

Функция доказательства для элементарного утверждения о умножении

0 голосов
/ 16 декабря 2018

Если у нас есть три целых числа a> 0, b, ab> = 0, таких что a * b = ab, то b> = 0, а если ab = 0, то b = 0, если ab> 0, то ab> 0.

Каков хороший способ реализовать это утверждение в качестве функции доказательства в ATS?

Полагаю, функция доказательства должна выглядеть примерно так: 

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

1 Ответ

0 голосов
/ 17 декабря 2018

Мне удалось написать правильную функцию доказательства.Но мое решение довольно длинное: 

  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
...