ATSLIB/prelude/arith_prf

This package contains some common proof functions for handling arithmetics.


  • MUL
  • mul_make
  • mul_elim
  • mul_istot
  • mul_isfun
  • mul_isfun2
  • mul_add_const
  • mul_expand_linear
  • mul_expand2_linear
  • mul_gte_gte_gte
  • mul_lte_gte_lte
  • mul_gte_lte_lte
  • mul_lte_lte_gte
  • mul_nat_nat_nat
  • mul_pos_pos_pos
  • mul_negate
  • mul_negate2
  • mul_commute
  • mul_is_commutative
  • mul_distribute
  • mul_distribute2
  • mul_is_associative
  • DIVMOD
  • div_istot
  • divmod_istot
  • divmod_isfun
  • divmod_elim
  • EXP2
  • lemma_exp2_param
  • exp2_istot
  • exp2_isfun
  • exp2_ispos
  • exp2_is_mono
  • exp2_muladd
  • EXP
  • lemma_exp_param
  • exp_istot
  • exp_isfun
  • exp_elim_0
  • exp_elim_1
  • exp_elim_2
  • exp_elim_b_0
  • exp_elim_b_1
  • exp_elim_b_2
  • exp_muladd
  • exp_expmul

  • MUL

    Synopsis

    The dataprop MUL is declared as follows:

    dataprop
    MUL (int, int, int) =
      | {n:int}
        MULbas (0, n, 0)
      | {m:nat}{n:int}{p:int}
        MULind (m+1, n, p+n) of MUL (m, n, p)
      | {m:pos}{n:int}{p:int}
        MULneg (~m, n, ~p) of MUL (m, n, p)
    // end of [MUL]
    

    Description

    Given integers m, n and p, the type (or more precisely, prop) MUL(m, n, p) captures the relation m*n=p.

    mul_make

    Synopsis

    praxi mul_make : {m,n:int} () -<prf> MUL (m, n, m*n)

    Description

    This proof function applies to static integers m and n to generate a proof of the type MUL(m, n, m*n).

    mul_elim

    Synopsis

    praxi mul_elim : {m,n:int} {p:int} MUL (m, n, p) -<prf> [p == m*n] void

    Description

    This proof function relates the relation MUL to the pre-defined static multiplication function on integers.

    mul_istot

    Synopsis

    prfun mul_istot {m,n:int} ():<prf> [p:int] MUL (m, n, p)

    Description

    This proof function applies to static integers m and n to generate a proof of the type MUL(m, n, p) for some integer p. In other words, the function proves that MUL is total on its first two arguments. The following code gives a direct implementation of mul_istot:
    primplmnt
    mul_istot
      {m,n} () = let
    //
    prfun lemma
      {m:nat;n:int} .<m>. (): [p:int] MUL (m, n, p) =
      sif m > 0 then MULind (lemma {m-1,n} ()) else MULbas ()
    //
    in
      sif m >= 0 then lemma {m,n} () else MULneg (lemma {~m,n} ())
    end // end of [mul_istot]
    
    Note that mul_make entirely supersedes mul_istot.

    mul_isfun

    Synopsis

    prfun mul_isfun {m,n:int} {p1,p2:int}
      (pf1: MUL (m, n, p1), pf2: MUL (m, n, p2)):<prf> [p1==p2] void

    Description

    This proof function proves that the relation MUL is functional on its first two arguments. The following code gives a direct implementation of mul_isfun:
    primplmnt
    mul_isfun
      {m,n} (pf1, pf2) = let
    //
    prfun lemma
      {m:nat;n:int}
      {p1,p2:int} .<m>. (
      pf1: MUL (m, n, p1), pf2: MUL (m, n, p2)
    ) : [p1==p2] void =
      case+ (pf1, pf2) of
      | (MULind (pf1), MULind (pf2)) => lemma (pf1, pf2)
      | (MULbas (), MULbas ()) => ()
    //
    in
      sif m >= 0 then
        lemma (pf1, pf2)
      else let
        prval MULneg (pf1) = pf1 and MULneg (pf2) = pf2
      in
        lemma (pf1, pf2)
      end (* end of [sif] *)
    end // end of [mul_isfun]
    

    mul_isfun2

    Synopsis

    prfun mul_isfun2 {m,n:int} {p1,p2:int}
      (pf1: MUL (m, n, p1), pf2: MUL (m, n, p2)):<prf> EQINT (p1, p2)

    Description

    This proof function is a variation of mul_isfun.

    mul_add_const

    Synopsis

    praxi mul_add_const {i:int}
      {m,n:int} {p:int} (pf: MUL (m, n, p)):<prf> MUL (m+i, n, p+i*n)

    Description

    This proof function essentially captures the identity: (m+i)*n=m*n+i*n. It is kept mostly for the sake of backward compatibility as the constraint-solver for ATS2 (Postiats) is able to verify such an identity automatically. For instance, this ability is made of use in typechecking the following implementation of mul_add_const:
    primplmnt
    mul_add_const
      {i}{m,n}{p} (pf) = let
      prval () = mul_elim (pf) in mul_make {m+i,n} ()
    end // end of [mul_add_const]
    

    mul_expand_linear

    Synopsis

    praxi mul_expand_linear // a,b,c,d: constants!
      {a,b:int}
      {c,d:int}
      {x,y:int}
      {xy:int} (
      pf: MUL (x, y, xy)
    ) :<prf> MUL (a*x+b, c*y+d, a*c*xy+a*d*x+b*c*y+b*d)

    Description

    This proof function essentially captures the following identity:

    (a*x+b)*(c*y+d) = a*c*xy+a*d*x+b*c*y+b*d

    It is kept mostly for the sake of backward compatibility.

    mul_expand2_linear

    Synopsis

    praxi mul_expand2_linear // a1,b1,c1,a2,b2,c2: constants!
      {a1,a2,b:int}
      {c1,c2,d:int}
      {x1,x2:int}
      {y1,y2:int}
      {x1y1,x1y2,x2y1,x2y2:int} (
      pf11: MUL (x1, y1, x1y1), pf12: MUL (x1, y2, x1y2)
    , pf21: MUL (x2, y1, x2y1), pf22: MUL (x2, y2, x2y2)
    ) :<prf> MUL (
      a1*x1+a2*x2+b
    , c1*y1+c2*y2+d
    , a1*c1*x1y1 + a1*c2*x1y2 +
      a2*c1*x2y1 + a2*c2*x2y2 +
      a1*d*x1 + a2*d*x2 +
      b*c1*y1 + b*c2*y2 +
      b*d
    ) // end of [mul_expand2_linear]

    Description

    This proof function essentially captures the following identity:

    (a1*x1+a2*x2+b)*(c1*y1+c2*y2+d) = a1*c1*x1*y1 + a1*c2*x1*y2 + a2*c1*x2*y1 + a2*c2*x2*y2 + a1*d*x1 + a2*d*x2 + b*c1*y1 + b*c2*y2 + b*d

    It is kept mostly for the sake of backward compatibility.

    mul_gte_gte_gte

    Synopsis

    prfun mul_gte_gte_gte
      : {m,n:int | m >= 0; n >= 0} () -<prf> [m*n >= 0] void

    Description

    This proof function proves m >= 0 and n >= 0 implying m*n >= 0 for any integers m and n.

    mul_lte_gte_lte

    Synopsis

    prfun mul_lte_gte_lte
      : {m,n:int | m <= 0; n >= 0} () -<prf> [m*n <= 0] void

    Description

    This proof function proves m <= 0 and n >= 0 implying m*n <= 0 for any integers m and n.

    mul_gte_lte_lte

    Synopsis

    prfun mul_gte_lte_lte
      : {m,n:int | m >= 0; n <= 0} () -<prf> [m*n <= 0] void

    Description

    This proof function proves m >= 0 and n <= 0 implying m*n <= 0 for any integers m and n.

    mul_lte_lte_gte

    Synopsis

    prfun mul_lte_lte_gte
      : {m,n:int | m <= 0; n <= 0} () -<prf> [m*n >= 0] void

    Description

    This proof function proves m <= 0 and n <= 0 implying m*n >= 0 for any integers m and n.

    mul_nat_nat_nat

    Synopsis

    prfun mul_nat_nat_nat :
      {m,n:nat} {p:int} MUL (m, n, p) -<prf> [p >= 0] void

    Description

    This proof function establishes p >= 0 if given a proof of the type MUL(m, n, p) for some natural numbers m and n. A straigtforward implementation of mul_nat_nat_nat is given as follows:
    primplmnt
    mul_nat_nat_nat (pf) = let
    //
    prfun lemma
      {m,n:nat}{p:int} .<m>.
      (pf: MUL (m, n, p)): [p >= 0] void =
      case+ pf of
      | MULind (pf1) => lemma (pf1) | MULbas () => ()
    // end of [lemma]
    in
      lemma (pf)
    end // end of [mul_nat_nat_nat]
    

    mul_pos_pos_pos

    Synopsis

    prfun mul_pos_pos_pos :
      {m,n:pos} {p:int} MUL (m, n, p) -<prf> [p >= m+n-1] void

    Description

    This proof function establishes p >= m+n-1 if given a proof of the type MUL(m, n, p) for some postive intgers m and n. A direct implementation of mul_pos_pos_pos based on mul_nat_nat_nat is given as follows:
    primplmnt
    mul_pos_pos_pos {m,n} (pf) = let
      prval MULind (pf1) = pf // pf1: MUL(m-1, n, ...)
      prval pf2 = mul_commute (pf1) // pf2: MUL (n, m-1, ...)
      prval MULind (pf3) = pf2 // pf3: MUL(m-1, n-1, ...)
    in
      mul_nat_nat_nat (pf3)
    end // end of [mul_pos_pos_pos]
    

    mul_negate

    Synopsis

    prfun mul_negate
      {m,n:int} {p:int} (pf: MUL (m, n, p)):<prf> MUL (~m, n, ~p)

    Description

    This proof function essentially proves (~m)*n=~(m*n) for any given integers m and n, where ~ is the symbol for integer negation in ATS. Note that mul_negate is kept mostly for the sake of backward compatibility as the constraint-solver for ATS2 (Postiats) can readily infer the identity (~m)*n=~(m*n). However, typechecking the following implementation of mul_negate involves solving only linear integer constraints:
    primplmnt
    mul_negate
      {m,n} (pf) = (
      sif m > 0 then let
        prval pf1 = mul_make {~m,n} ()
        prval MULneg (pf2) = pf1
        prval () = mul_isfun (pf, pf2)
      in
        pf1
      end else sif m < 0 then let
        prval MULneg (pf1) = pf in pf1
      end else let
        prval MULbas () = pf in MULbas ()
      end // end of [sif]
    ) // end of [mul_negate]
    

    mul_negate2

    Synopsis

    prfun mul_negate2
      {m,n:int} {p:int} (pf: MUL (m, n, p)):<prf> MUL (m, ~n, ~p)

    Description

    This proof function essentially proves m*(~n)=~(m*n) for any given integers m and n, where ~ is the symbol for integer negation in ATS. Note that mul_negate2 is kept mostly for the sake of backward compatibility as the constraint-solver for ATS2 (Postiats) can readily infer the identity m*(~n)=~(m*n). However, typechecking the following implementation of mul_negate2 involves solving only linear integer constraints:
    primplmnt
    mul_negate2
      {m,n}{p} (pf) = let
    //
    prfun lemma
      {m:nat;n:int}
      {p:int} .<m>. (
      pf: MUL (m, n, p)
    ) : MUL (m, ~n, ~p) =
      case+ pf of
      | MULind
          (pf) => MULind (lemma (pf))
      | MULbas () => MULbas ()
    // end of [mul_m_neg_n_neg_mn]
    //
    in // in of [local]
    //
    sif m >= 0 then
       lemma (pf)
    else let
      prval MULneg pf = pf in MULneg (lemma (pf))
    end // end of [sif]
    //
    end // end of [mul_negate2]
    

    mul_commute

    Synopsis

    prfun mul_commute
      {m,n:int} {p:int} (pf: MUL (m, n, p)):<prf> MUL (n, m, p)

    Description

    This proof function essentially proves m*n=n*m for any given integers m and n. It is kept mostly for the sake of backward compatibility as the constraint-solver of ATS2 (Postiats) is able to infer the identity m*n=n*m automatically. However, typechecking the following implementation of mul_commute involves solving only linear integer constraints:
    local
    //
    prfun mul_m_n1_mnm
      {m,n:int}{p:int}
      .<max(2*m, 2*(~m)+1)>.
      (pf: MUL (m, n, p)): MUL (m, n+1, p+m) =
      case+ pf of
      | MULbas () => MULbas ()
      | MULind pf => MULind (mul_m_n1_mnm pf)
      | MULneg pf => MULneg (mul_m_n1_mnm pf)
    // end of [mul_m_n1_mnm]
    //
    in // in of [local]
    //
    primplmnt
    mul_commute
      {m,n}{p} (pf) = let
    //
    prfun aux
      {m:nat;n:int}
      {p:int} .<m>. (
      pf: MUL (m, n, p)
    ) : MUL (n, m, p) =
      case+ pf of
      | MULbas () => let
          prval pf =
            mul_istot {n,0} ()
          prval () = mul_elim pf
        in
          pf
        end // end of [MULbas]
      | MULind pf => mul_m_n1_mnm (aux pf)
    // end of [aux]
    //
    in
      sif m >= 0 then aux pf else begin
        let prval MULneg (pf) = pf in mul_negate2 (aux pf) end
      end // end of [sif]
    end // end of [mul_commute]
    //
    end // end of [local]
    

    mul_is_commutative

    Synopsis

    prfun mul_is_commutative
      {m,n:int} {p,q:int} (pf1: MUL (m, n, p), pf2: MUL (n, m, q)): [p==q] void

    Description

    This proof function is just a slight variation of mul_commute:
    primplmnt
    mul_is_commutative (pf1, pf2) = mul_isfun (mul_commute (pf1), pf2)
    

    mul_distribute

    Synopsis

    prfun mul_distribute
      {m:int} {n1,n2:int} {p1,p2:int}
      (pf1: MUL (m, n1, p1), pf2: MUL (m, n2, p2)):<prf> MUL (m, n1+n2, p1+p2)

    Description

    This proof function essentially proves the identity m*(n1+n2)=m*n1+m*n2 for any given integers m, n1 and n2. It is kept mostly for the sake of backward compatibility as the constraint-solver of ATS2 (Postiats) is able to infer the identity m*(n1+n2)=m*n1+m*n2 automatically. However, typechecking the following implementation of mul_distribute involves solving only linear integer constraints:
    primplmnt
    mul_distribute
      {m}{n1,n2}{p1,p2} (pf1, pf2) = let
    //
    prfun lemma
      {m:nat}
      {n1,n2:int}
      {p1,p2:int} .<m>. (
      pf1: MUL (m, n1, p1), pf2: MUL (m, n2, p2)
    ) : MUL (m, n1+n2, p1+p2) =
      case+ (pf1, pf2) of
      | (MULbas (), MULbas ()) => MULbas ()
      | (MULind pf1, MULind pf2) => MULind (lemma (pf1, pf2))
    // end of [lemma]
    //
    in // in of [let]
    //
    sif m >= 0 then
      lemma (pf1, pf2)
    else let
      prval MULneg pf1 = pf1 and MULneg pf2 = pf2
    in
      MULneg (lemma (pf1, pf2))
    end // end of [sif]
    //
    end // end of [mul_distribute]
    

    mul_distribute2

    Synopsis

    prfun mul_distribute2
      {m1,m2:int} {n:int} {p1,p2:int}
      (pf1: MUL (m1, n, p1), pf2: MUL (m2, n, p2)):<prf> MUL (m1+m2, n, p1+p2)

    Description

    This proof function essentially proves the identity (m1+m2)*n=m1*n+m2*n for any given integers m1, m2 and n. It is kept mostly for the sake of backward compatibility as the constraint-solver of ATS2 (Postiats) is able to infer the identity (m1+m2)*n=m1*n+m2*n automatically. The following implementation of mul_distribute2 is based on mul_commute and mul_distribute:
    primplmnt
    mul_distribute2 (pf1, pf2) =
      mul_commute (mul_distribute (mul_commute (pf1), mul_commute (pf2)))
    // end of [mul_distribute2]
    

    mul_is_associative

    Synopsis

    prfun
    mul_is_associative
      {x,y,z:int}
      {xy,yz:int}
      {xy_z,x_yz:int} (
      pf1: MUL (x, y, xy), pf2: MUL (y, z, yz)
    , pf3: MUL (xy, z, xy_z), pf4: MUL (x, yz, x_yz)
    ) :<prf> [xy_z==x_yz] void

    Description

    This proof function essentially proves (x*y)*z=x*(y*z) for any given integers x, y and z. It is kept mostly for the sake of backward compatibility as the constraint-solver of ATS2 (Postiats) is able to infer the identity (x*y)*z=x*(y*z) automatically.

    DIVMOD

    Synopsis

    absprop
    DIVMOD (
      x:int, y: int, q: int, r: int // x = q * y + r
    ) // end of [DIVMOD]

    Description

    Given integers x, y, q, r, the prop DIVMOD(x, y, q, r) captures that x=q*y+r holds and r is natural number less than y.

    div_istot

    Synopsis

    praxi
    div_istot
      {x,y:int | x >= 0; y > 0} (): DIV (x, y, x/y)

    divmod_istot

    Synopsis

    praxi
    divmod_istot
      {x,y:int |
       x >= 0; y > 0}
      ((*void*)): [q,r:nat | r < y] DIVMOD (x, y, q, r)

    divmod_isfun

    Synopsis

    praxi
    divmod_isfun
      {x,y:int | x >= 0; y > 0}
      {q1,q2:int} {r1,r2:int} (
      pf1: DIVMOD (x, y, q1, r1)
    , pf2: DIVMOD (x, y, q2, r2)
    ) : [q1==q2;r1==r2] void // end of [divmod_isfun]

    divmod_elim

    Synopsis

    praxi
    divmod_elim
      {x,y:int | x >= 0; y > 0}
      {q,r:int}
    (
      pf: DIVMOD (x, y, q, r)
    ) : [qy:nat | 0 <= r; r < y; x==qy+r] MUL (q, y, qy)

    EXP2

    Synopsis

    The dataprop EXP2 is declared as follows:

    dataprop EXP2 (int, int) =
      | {n:nat}{p:nat} EXP2ind (n+1, 2*p) of EXP2 (n, p)
      | EXP2bas (0, 1)
    // end of [EXP2]
    

    Description

    Given integers n and p, the prop EXP2(n, p) captures the relation that 2^n=p holds and n is a natural number.

    lemma_exp2_param

    Synopsis

    prfun lemma_exp2_param :
      {n:int}{p:int} EXP2 (n, p) -<prf> [n>=0;p>=1] void

    exp2_istot

    Synopsis

    prfun exp2_istot {n:nat} (): [p:nat] EXP2 (n, p)

    exp2_isfun

    Synopsis

    prfun exp2_isfun {n:nat} {p1,p2:int}
      (pf1: EXP2 (n, p1), pf2: EXP2 (n, p2)): [p1==p2] void

    exp2_ispos

    Synopsis

    prfun exp2_ispos
      {n:nat} {p:int} (pf: EXP2 (n, p)): [p >= 1] void

    exp2_is_mono

    Synopsis

    prfun exp2_is_mono
      {n1,n2:nat | n1 <= n2} {p1,p2:int}
      (pf1: EXP2 (n1, p1), pf2: EXP2 (n2, p2)): [p1 <= p2] void

    exp2_muladd

    Synopsis

    prfun exp2_muladd
      {n1,n2:nat | n1 <= n2} {p1,p2:int} {p:int} (
      pf1: EXP2 (n1, p1), pf2: EXP2 (n2, p2), pf3: MUL (p1, p2, p)
    ) : EXP2 (n1+n2, p) // end of [exp2_muladd]

    EXP

    Synopsis

    absprop EXP (int(*base*), int(*power*), int(*res*))

    Description

    Given integers b, n and p, the prop EXP(b, n, p) captures the relation that b^n=p holds and n is a natural number, where b^n refers to the exponential function for base b and exponent n.

    lemma_exp_param

    Synopsis

    praxi lemma_exp_param
      {b:int}{n:int}{p:int} (pf: EXP (b, n, p)): [n >= 0] void

    exp_istot

    Synopsis

    praxi exp_istot {b:int}{n:nat} (): [p:nat] EXP (b, n, p)

    exp_isfun

    Synopsis

    praxi exp_isfun {b:int}{n:int}{p1,p2:int}
      (pf1: EXP (b, n, p1), pf2: EXP (b, n, p2)): [p1==p2] void

    exp_elim_0

    Synopsis

    praxi exp_elim_0 {n:pos}{p:int} (pf: EXP (0, n, p)): [p==0] void

    exp_elim_1

    Synopsis

    praxi exp_elim_1 {n:int}{p:int} (pf: EXP (1, n, p)): [p==1] void

    exp_elim_2

    Synopsis

    praxi exp_elim_2 {n:int}{p:int} (pf: EXP (2, n, p)): EXP2 (n, p)

    exp_elim_b_0

    Synopsis

    praxi exp_elim_b_0 {b:int}{p:int} (pf: EXP (b, 0, p)): [p==1] void

    exp_elim_b_1

    Synopsis

    praxi exp_elim_b_1 {b:int}{p:int} (pf: EXP (b, 1, p)): [p==b] void

    exp_elim_b_2

    Synopsis

    praxi exp_elim_b_2 {b:int}{p:int} (pf: EXP (b, 2, p)): MUL (b, b, p)

    exp_muladd

    Synopsis

    praxi exp_muladd
      {b:int}{n1,n2:int}{p1,p2:int}{p:int} (
      pf1: EXP (b, n1, p1), pf2: EXP (b, n2, p2)
    ) : EXP (b, n1+n2, p1*p2) // end of [exp_muladd]

    Description

    This proof function proves b^(n1+n2)=(b^n1)*(b^n2) for integer b and natural numbers n1, n2.

    exp_expmul

    Synopsis

    praxi exp_expmul
      {b:int}{n1,n2:int}{bn1:int}{bn1n2:int} (
      pf1: EXP (b, n1, bn1), pf2: EXP (bn1, n2, bn1n2)
    ) : EXP (b, n1*n2, bn1n2) // end of [exp_muladd]

    Description

    This proof function proves (b^n1)^n2=b^(n1*n2) for integer b and natural numbers n1, n2.
    This page is created with ATS by Hongwei Xi and also maintained by Hongwei Xi. SourceForge.net Logo