(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2010-2015 Hongwei Xi, ATS Trustful Software, Inc.
** All rights reserved
**
** ATS is free software;  you can  redistribute it and/or modify it under
** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
** Free Software Foundation; either version 3, or (at  your  option)  any
** later version.
**
** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
** for more details.
**
** You  should  have  received  a  copy of the GNU General Public License
** along  with  ATS;  see the  file COPYING.  If not, please write to the
** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
** 02110-1301, USA.
*)

(* ****** ****** *)

(*
** Source:
** $PATSHOME/prelude/SATS/CODEGEN/arith_prf.atxt
** Time of generation: Thu Jan 11 11:00:02 2018
*)

(* ****** ****** *)

(* Author: Hongwei Xi *)
(* Authoremail: hwxi AT cs DOT bu DOT edu *)
(* Start time: September, 2011 *)

(* ****** ****** *)

#if(0)
//
// It is available in [basic_dyn.sats]
//
dataprop
MUL_prop
(
  int, int, int
) = // MUL_prop
  | {n:int}
    MULbas (0, n, 0)
  | {m:nat}{n:int}{p:int}
    MULind (m+1, n, p+n) of MUL_prop (m, n, p)
  | {m:pos}{n:int}{p:int}
    MULneg (~(m), n, ~(p)) of MUL_prop (m, n, p)
//
propdef MUL = MUL_prop
//
#endif

(* ****** ****** *)

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)
//
prfun
mul_isfun
{m,n:int}{p1,p2:int}
(
  MUL(m, n, p1), MUL(m, n, p2)
) :<prf> [p1==p2] void // endfun
prfun
mul_isfun2{m,n:int}{p1,p2:int}
  (MUL(m, n, p1), MUL(m, n, p2)):<prf> EQINT(p1, p2)
//
(* ****** ****** *)
//
// HX: (m+i)*n = m*n+i*n
//
praxi
mul_add_const
  {i:int}{m,n:int}{p:int}
  (pf: MUL (m, n, p)):<prf> MUL(m+i, n, p+i*n)
// end of [mul_add_const]
//
(* ****** ****** *)
//
// HX: (ax+b)*(cy+d) = ac*xy + ad*x + bc*y + bd
//
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)
// end of [mul_expand_linear]

(* ****** ****** *)
//
// HX: (a1x1+a2x2+b)*(c1y1+c2y2+d) = ...
//
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] *)

(* ****** ****** *)
//
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
prfun
mul_pos_pos_pos :
  {m,n:pos} {p:int} MUL(m, n, p) -<prf> [p >= m+n-1] void
//
(* ****** ****** *)
//
prfun mul_negate
  {m,n:int}{p:int}(pf: MUL(m, n, p)):<prf> MUL(~m, n, ~p)
prfun mul_negate2
  {m,n:int}{p:int}(pf: MUL(m, n, p)):<prf> MUL(m, ~n, ~p)
//
(* ****** ****** *)
//
// HX: m*n = n*m
//
prfun mul_commute
  {m,n:int}{p:int}(pf: MUL(m, n, p)):<prf> MUL(n, m, p)
prfun mul_is_commutative
  {m,n:int}{p,q:int}(pf1: MUL(m, n, p), pf2: MUL(n, m, q)): [p==q] void
//
(* ****** ****** *)
//
// HX: m*(n1+n2) = m*n1+m*n2
//
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)
//
// HX: (m1+m2)*n = m1*n + m2*n
//
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)
//
(* ****** ****** *)

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

(* ****** ****** *)
//
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)

praxi
divmod_mul_elim
  {x,y:int | x >= 0; y > 0}
  {q,r:int}
  (pf: DIVMOD (x, y, q, r))
: [0 <= q; 0 <= r; r < y; q==ndiv_int_int(x, y); x==q*y+r] void
// end of [divmod_mul_elim]

(* ****** ****** *)
//
dataprop
EXP2 (int, int) =
  | EXP2bas (0, 1)
  | {n:nat}{p:nat}
    EXP2ind (n+1, 2*p) of EXP2 (n, p)
// end of [EXP2]
//
prfun lemma_exp2_param :
  {n:int}{p:int} EXP2 (n, p) -<prf> [n>=0;p>=1] void
// end of [lemma_exp2_param]
//
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
// end of [exp2_isfun]
//
// HX: proven in [arith_prf.dats]
//
prfun exp2_ispos
  {n:nat} {p:int} (pf: EXP2 (n, p)): [p >= 1] void
// end of [exp2_ispos]
//
// HX: proven in [arith_prf.dats]
//
prfun exp2_is_mono
  {n1,n2:nat | n1 <= n2} {p1,p2:int}
  (pf1: EXP2 (n1, p1), pf2: EXP2 (n2, p2)): [p1 <= p2] void
// end of [exp2_is_mono]
//
// HX: proven in [arith_prf.dats]
//
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
// end of [lemma_exp_param]

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
// end of [exp_isfun]

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]

(* ****** ****** *)

(* end of [arith_prf.sats] *)