# 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_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
• 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_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.

### 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
{i}{m,n}{p} (pf) = let
prval () = mul_elim (pf) in mul_make {m+i,n} ()
```

## 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```

### 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)`

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