This package contains some common proof functions for handling arithmetics.
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]
praxi
mul_make : {m,n:int} () -<prf> MUL (m, n, m*n)
praxi
mul_elim : {m,n:int} {p:int} MUL (m, n, p) -<prf> [p == m*n] void
prfun
mul_istot{m,n:int}():<prf> [p:int] MUL(m, n, p)
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.
prfun mul_isfun {m,n:int}{p1,p2:int} ( MUL(m, n, p1), MUL(m, n, p2) ) :<prf> [p1==p2] void // endfun
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]
prfun
mul_isfun2{m,n:int}{p1,p2:int}
(MUL(m, n, p1), MUL(m, n, p2)):<prf> EQINT(p1, p2)
praxi
mul_add_const
{i:int}{m,n:int}{p:int}
(pf: MUL (m, n, p)):<prf> MUL(m+i, n, p+i*n)
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]
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)
(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.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} ( MUL(x1, y1, x1y1), MUL(x1, y2, x1y2) , MUL(x2, y1, x2y1), MUL(x2, y2, x2y2) ) :<prf> MUL_prop ( 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] *)
(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.
prfun
mul_gte_gte_gte
: {m,n:int | m >= 0; n >= 0} () -<prf> [m*n >= 0] void
prfun
mul_lte_gte_lte
: {m,n:int | m <= 0; n >= 0} () -<prf> [m*n <= 0] void
prfun
mul_gte_lte_lte
: {m,n:int | m >= 0; n <= 0} () -<prf> [m*n <= 0] void
prfun
mul_lte_lte_gte
: {m,n:int | m <= 0; n <= 0} () -<prf> [m*n >= 0] void
prfun
mul_nat_nat_nat :
{m,n:nat} {p:int} MUL (m, n, p) -<prf> [p >= 0] void
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]
prfun
mul_pos_pos_pos :
{m,n:pos} {p:int} MUL (m, n, p) -<prf> [p >= m+n-1] void
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]
prfun mul_negate
{m,n:int} {p:int} (pf: MUL (m, n, p)):<prf> MUL (~m, n, ~p)
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]
prfun mul_negate2
{m,n:int} {p:int} (pf: MUL (m, n, p)):<prf> MUL (m, ~n, ~p)
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]
prfun mul_commute
{m,n:int} {p:int} (pf: MUL (m, n, p)):<prf> MUL (n, m, p)
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]
prfun mul_is_commutative
{m,n:int} {p,q:int} (pf1: MUL (m, n, p), pf2: MUL (n, m, q)): [p==q] void
primplmnt
mul_is_commutative (pf1, pf2) = mul_isfun (mul_commute (pf1), pf2)
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)
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]
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)
primplmnt mul_distribute2 (pf1, pf2) = mul_commute (mul_distribute (mul_commute (pf1), mul_commute (pf2))) // end of [mul_distribute2]
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
Synopsis for [DIVMOD] is unavailable.
praxi
div_istot
{x,y:int | x >= 0; y > 0} (): DIV(x, y, x/y)
praxi
divmod_istot
{ x,y:int
| x >= 0; y > 0
} ((*void*)): [q,r:nat | r < y] DIVMOD(x, y, q, r)
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]
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)
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]
prfun lemma_exp2_param :
{n:int}{p:int} EXP2 (n, p) -<prf> [n>=0;p>=1] void
prfun exp2_istot {n:nat} (): [p:nat] EXP2 (n, p)
prfun exp2_isfun {n:nat} {p1,p2:int}
(pf1: EXP2 (n, p1), pf2: EXP2 (n, p2)): [p1==p2] void
prfun exp2_ispos
{n:nat} {p:int} (pf: EXP2 (n, p)): [p >= 1] void
prfun exp2_is_mono
{n1,n2:nat | n1 <= n2} {p1,p2:int}
(pf1: EXP2 (n1, p1), pf2: EXP2 (n2, p2)): [p1 <= p2] void
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]
absprop EXP (int(*base*), int(*power*), int(*res*))
praxi lemma_exp_param
{b:int}{n:int}{p:int} (pf: EXP (b, n, p)): [n >= 0] void
praxi exp_istot {b:int}{n:nat} (): [p:nat] EXP (b, n, p)
praxi exp_isfun {b:int}{n:int}{p1,p2:int}
(pf1: EXP (b, n, p1), pf2: EXP (b, n, p2)): [p1==p2] void
praxi exp_elim_0 {n:pos}{p:int} (pf: EXP (0, n, p)): [p==0] void
praxi exp_elim_1 {n:int}{p:int} (pf: EXP (1, n, p)): [p==1] void
praxi exp_elim_2 {n:int}{p:int} (pf: EXP (2, n, p)): EXP2 (n, p)
praxi exp_elim_b_0 {b:int}{p:int} (pf: EXP (b, 0, p)): [p==1] void
praxi exp_elim_b_1 {b:int}{p:int} (pf: EXP (b, 1, p)): [p==b] void
praxi exp_elim_b_2 {b:int}{p:int} (pf: EXP (b, 2, p)): MUL (b, b, p)
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]
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]
This page is created with ATS by Hongwei Xi and also maintained by Hongwei Xi. |