# New Examples in ATS/Anairiats

In this page, we primarily present some newly constructed examples in ATS that are relatively short but interesting.

```(*
**
** A proof sketch for the representation
** of Pythagorean triangluar integer triples
**
** Suppose that a and b are positive integers
** satisfying gcd (a, b) = 1.
**
** If a*a + b*b = c*c for some integer c, then
**
** 1. either a or b is even
** 2. if a is even, then there exist integers
**    p, q such that:
**
**    a = 2*p*q
**    b = p*p - q*q
**    c = p*p + q*q
**
*)

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

(*
** Author: Hongwei Xi (hwxi AT cs DOT bu DOT edu)
** Time: February 7, 2010
*)

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

(*
**
** HX-2010-02-08:
**
** What is written as follows is not really a proof in any rigourous
** sense. However, it is close to a style we as human being do mathematics.
** I envision a system (ATS/LF) where refinement can be done gradually to
** remove the number of __assert functions used in such a proof. Who will
** take the grand challenge :)
**
*)

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

absprop MOD (n:int, p:int, r:int) // n mod p = r

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

extern prfun lemma1 {n:nat} {n2:int}
(pf1: MOD (n, 2, 0), pf2: MUL (n, n, n2)): MOD (n2, 4, 0)
// end of [lemma1]

extern prfun lemma2 {n:nat} {n2:int}
(pf1: MOD (n, 2, 1), pf2: MUL (n, n, n2)): MOD (n2, 4, 1)
// end of [lemma2]

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

dataprop por (A: prop, B: prop) = inl (A, B) of A | inr (A, B) of B

extern prfun lemma3 {a,b,c:nat} {a2,b2:int}
(pfa: MUL (a, a, a2), pfb: MUL (b, b, b2), pfc: MUL (c, c, a2+b2))
: por (MOD (a, 2, 0), MOD (b, 2, 0))

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

extern prfun lemma5 {P,Q:pos} {n:nat}
(pf: GCD (P, Q, 1), pf: MUL (P, Q, n*n))
: [p,q:nat] (MUL (p, p, P), MUL (p, q, n), MUL (q, q, Q))
// end of [lemma5]

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

extern prfun PyTri {a,b,c:pos} {a2,b2:int} (
pfa_mod: MOD (a, 2, 0)
, pfab_gcd: GCD (a, b, 1)
, pfa: MUL (a, a, a2)
, pfb: MUL (b, b, b2)
, pfc: MUL (c, c, a2+b2)
) : [p,q:nat]
[p2,pq,q2:int | a == 2*pq; b == p2-q2; c == p2+q2]
(MUL (p, p, p2), MUL (p, q, pq), MUL (q, q, q2))
// end of [PyTri]

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

implement PyTri {a,b,c} {a2,b2}
(pfa_mod, pfab_gcd, pfa, pfb, pfc) = let
prval [ha:int] () = __assert (pfa_mod) where {
extern prfun __assert (pf: MOD (a, 2, 0)): [ha:int | 2*ha==a] void
}
prval [hb:int] () = __assert (pfb_mod) where {
extern prfun __assert (pf: MOD (b, 2, 1)): [hb:int | 2*hb+1==b] void
prval pfb_mod = __assert (pfa_mod, pfab_gcd) where {
extern prfun __assert (pf1: MOD (a, 2, 0), pf2: GCD (a, b, 1)): MOD (b, 2, 1)
} // end of [prval]
} // end of [prval]
prval [hc:int] () = __assert () where {
extern prfun __assert (): [hc:int | 2*hc+1==c] void
} // end of [prval]
prval () = __assert () where {
extern prfun __assert (): [a < c; b < c] void
}
//
prval [ha2:int] _pf = mul_istot {ha,ha} ()
prval () = mul_elim (_pf)
prval () = __assert () where {
extern prfun __assert (): [4*ha2 == a2] void
}
//
prval [_a2:int] _pf = mul_istot {c+b,c-b} ()
prval () = mul_elim (_pf)
prval () = __assert () where {
extern prfun __assert (): [_a2 == a2] void // (c+b)*(c-b) = c*c - b*b
} // end of [prval]
stadef P = hc+hb+1 and Q = hc-hb
prval [PQ:int] pfPQ_mul = mul_istot {P,Q} ()
prval () = mul_elim (_pf)
prval () = __assert () where {
extern prfun __assert (): [4*PQ == a2] void
}
prval pfPQ_gcd = __assert () where {
extern prfun __assert (): GCD (P, Q, 1)
}
prval [p,q:int] (pfpp, pfpq, pfqq) = lemma5 {P,Q} {ha} (pfPQ_gcd, pfPQ_mul)
// prval () = verify_constraint {false} () // check for sanity
in
(pfpp, pfpq, pfqq)
end // end of [PyTri]

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

(* end of [PyTri.dats] *)
```

```(*
**
** A proof of the equivalence of two definitions
** of the Ackermann function
**
** Author: Hongwei Xi (hwxi AT cs DOT bu DOT edu)
** Time: December 2, 2009
**
*)

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

(*

The following two functions are proven to be the same
(in the set-theoretic sense):

fun ack
(m:int, n:int): int =
case+ m of
| 0 => n+1
| _ => begin case+ n of
| 0 => ack (m-1, 1) | _ => ack (m-1, ack (m, n-1))
end // end of [_]
// end of [ack1]

fun ackf (m: int): int -<cloref1> int = let
fun helper
(f: int -<cloref1> int): int -<cloref1> int =
lam n => if n = 0 then f (1) else f (helper f (n-1))
// end of [helper]
in
case+ m of
| 0 => lam n => n+1 | _ => helper (ackf (m-1))
end // end of [ackf]

*)

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

dataprop ACK (int, int, int) =
| {n:nat} ACK1 (0, n, n+1) of ()
| {m:nat} {r:int} ACK2 (m+1, 0, r) of ACK (m, 1, r)
| {m,n:nat} {r1,r2:int}
ACK3 (m+1, n+1, r2) of (ACK (m+1, n, r1), ACK (m, r1, r2))
// end of [ACK]

prfun ACK_nat_nat_nat {m,n:nat}
{r:int} .<m,n>. (pf: ACK (m, n, r)): [r >= 0] void =
case+ pf of
| ACK1 () => ()
| ACK2 pf1 => ACK_nat_nat_nat (pf1)
| ACK3 (pf1, pf2) => let
prval () = ACK_nat_nat_nat pf1
prval () = ACK_nat_nat_nat pf2
in
// nothing
end // end of [ACK3]
// end of [ACK_nat_nat_nat]

prfun ACK_isfun {m,n:nat} {r1,r2:int} .<m,n>.
(pf1: ACK (m, n, r1), pf2: ACK (m, n, r2)): [r1==r2] void =
case+ (pf1, pf2) of
| (ACK1 (), ACK1 ()) => ()
| (ACK2 (pf11), ACK2 (pf12)) => ACK_isfun (pf11, pf12)
| (ACK3 (pf11, pf12), ACK3 (pf21, pf22)) => let
prval () = ACK_nat_nat_nat (pf11)
prval () = ACK_isfun (pf11, pf21) in ACK_isfun (pf12, pf22)
end // end of [ACK3, ACK3]
// end of [ACK_isfun]

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

sortdef int2rel = (int, int) -> prop

dataprop SUCC (int, int) = {n:nat} SUCC1 (n, n+1) of ()

dataprop HELPER (rel:int2rel, int, int) =
| {r:int} HELPER1 (rel, 0, r) of rel (1, r)
| {n:nat} {r1,r2:int}
HELPER2 (rel, n+1, r2) of (HELPER (rel, n, r1), rel (r1, r2))
// end of [HELPER]

dataprop ACKF (int, int2rel) =
| ACKF1 (0, SUCC) of ()
| {m:nat} {rel:int2rel}
ACKF2 (m+1, lam (r1:int, r2:int) => HELPER (rel, r1, r2)) of ACKF (m, rel)
// end of [ACKF]

prfun ACKF_istot
{m:nat} .<m>. (): [rel:int2rel] ACKF (m, rel) =
sif m > 0 then ACKF2 (ACKF_istot {m-1} ()) else ACKF1 ()
// end of [ACKF_istot]

propdef int2rel_istot
(rel: int2rel) = {n:nat} () -<prf> [r:nat] rel (n, r)
// end of [int2rel_istot]

prfn HELPER_istot
{rel:int2rel} (fpf: int2rel_istot rel)
: int2rel_istot (lam (r1:int,r2:int) => HELPER (rel, r1, r2)) = let
prfun fpf_res {n:nat} .<n>. (): [r:nat] HELPER (rel, n, r) =
sif n > 0 then let
prval [r1:int] pf1 = fpf_res {n-1} ()
in
HELPER2 (pf1, fpf {r1} ())
end else // n = 0
HELPER1 (fpf {1} ())
// end of [sif]
// end of [pf_res]
in
fpf_res
end // end of [HELPER_istot]

prfun ACKF_rel_istot
{m:nat} {rel:int2rel} .<m>.
(pf: ACKF (m, rel)): int2rel_istot (rel) =
sif m > 0 then let
prval ACKF2 pf1 = pf
prval fpf1 = ACKF_rel_istot {m-1} (pf1)
in
HELPER_istot (fpf1)
end else let // m = 0
prval ACKF1 () = pf // rel = SUCC
in
lam {n:nat} () =<prf> SUCC1 {n} ()
end // end of [sif]
// end of [ACKF_rel_istot]

(*
** this lemma means that applying ackf (m) to n gives
** ack (m, n)
*)
prfun ackf_ack_lemma
{m,n:nat} {rel:int2rel} {r:int} .<m,n+1>.
(pf1: ACKF (m, rel), pf2: rel (n, r)): ACK (m, n, r) =
case pf1 of
| ACKF1 () => let
prval SUCC1 () = pf2 in ACK1 {n} ()
end // end of [ACKF1]
| ACKF2 pf11 => ackf_ack_lemma2 (pf11, pf2)
// end of [ackf_ack_lemma]

(*
** this lemma means that applying ackf (m) n times to 1
** gives ack (m+1, n)
*)
and ackf_ack_lemma2
{m,n:nat} {rel:int2rel} {r:int} .<m+1,n>.
(pf1: ACKF (m, rel), pf2: HELPER (rel, n, r)): ACK (m+1, n, r) =
sif n > 0 then let
prval HELPER2 (pf21, pf22) = pf2
prval pf_ack = ackf_ack_lemma2 (pf1, pf21) // ACK (m+1, n-1)
prval () = ACK_nat_nat_nat (pf_ack)
in
ACK3 (pf_ack, ackf_ack_lemma (pf1, pf22))
end else let // n == 0
prval HELPER1 (pf21) = pf2
in
ACK2 (ackf_ack_lemma (pf1, pf21))
end // end of [sif]
// end of [ackf_ack_lemma2]

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

prfun ack_ackf_lemma
{m,n:nat} {r:int} .<>. (pf: ACK (m, n, r))
: [rel:int2rel] (ACKF (m, rel), rel (n, r)) = let
prval pf_ackf = ACKF_istot {m} ()
prval fpf_rel = ACKF_rel_istot (pf_ackf)
prval pf_rel = fpf_rel {n} ()
prval pf_alt = ackf_ack_lemma (pf_ackf, pf_rel)
prval () = ACK_isfun (pf, pf_alt)
in
(pf_ackf, pf_rel)
end // end of [ack_ackf_lemma]

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

(*
**
** By [ackf_ack_lemma] and [ack_ackf_lemma], it is clearly
** one can go from ACKF to ACK and vice versa.
**
*)

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

(* end of [Ackermann.dats] *)
```

```(*
**
** [infprime] proves that for any given natural number [n], there exists a
** prime number [p] that is greater than [n]
**
** Author: Hongwei Xi (hwxi AT cs DOT bu DOT edu)
** Time: October 7, 2009
**
*)

propdef PRIME (p:int) = // if p >= 2
{x,y:nat | x <= y} MUL (x, y, p) -<> [x==1] void
// end of [propdef]

(*

extern prval prime2: PRIME (2)
extern prval prime3: PRIME (3)
extern prval prime5: PRIME (5)
extern prval prime7: PRIME (7)

*)

extern // this one is not proven
prfun lemma10 {n:nat | n >= 2} (): [p,q:int | p >= 2] (PRIME p, MUL (p, q, n))

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

dataprop FACT (int, int) =
| FACTbas (0, 1)
| {n:nat} {r,r1:int} FACTind (n+1, r) of (FACT (n, r1), MUL (n+1, r1, r))
// end of [FACT]

prfun fact_istot
{n:nat} .<n>. (): [r:nat] FACT (n, r) =
sif n == 0 then FACTbas ()
else let
prval pf_fac = fact_istot {n-1} ()
prval pf_mul = mul_istot (); prval () = mul_nat_nat_nat (pf_mul)
in
FACTind (pf_fac, pf_mul)
end // end of [sif]
// end of [fact_istot]

prfun fact_isfun {n:nat} {r1,r2:int} .<n>.
(pf1: FACT (n, r1), pf2: FACT (n, r2)): [r1==r2] void =
case+ (pf1, pf2) of
| (FACTbas (), FACTbas ()) => ()
| (FACTind (pf11, pf12), FACTind (pf21, pf22)) => let
prval () = fact_isfun (pf11, pf21); prval () = mul_isfun (pf12, pf22)
in
// nothing
end // end of [FACTind, FACTind]
// end of [fact_isfun]

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

prfun lemma20 {n,r:int}
{i:pos | i <= n} .<n>.
(pf_fac: FACT (n, r)): [k:nat] MUL (k, i, r) = let
prval FACTind (pf1_fac, pf2_mul) = pf_fac // r = n*r1
in
sif i < n then let
prval [k1:int] pf3_res = lemma20 {..} {i} (pf1_fac) // pf3_res: k1 * i = r1
prval [k:int] pf4_mul = mul_istot {n,k1} () // k = n*k1
prval () = mul_nat_nat_nat (pf4_mul)
prval pf5_res = mul_istot {k,i} ()
prval () = mul_nat_nat_nat (pf5_res)
prval () = mul_associate (pf4_mul, pf3_res, pf5_res, pf2_mul)
in
pf5_res
end else let
prval pf1_fac_another = fact_istot {n-1} ()
prval () = fact_isfun (pf1_fac, pf1_fac_another)
in
mul_commute (pf2_mul)
end // end of [sif]
end (* end of [lemma20] *)

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

extern
prfun infprime {n:int | n >= 1} (): [p:int | p > n] PRIME p

implement infprime {n} () = let
prval [r:int] pf_fac = fact_istot {n} ()
prval () = lemma (pf_fac) where {
prfun lemma {n,r:int | n >= 1} .<n>. (pf_fac: FACT (n, r)): [r >= n] void =
sif n >= 2 then let
prval FACTind (pf1_fac, pf2_mul) = pf_fac
prval () = lemma (pf1_fac)
prval pf2_mul = mul_commute (pf2_mul)
prval MULind (pf3_mul) = pf2_mul
prval () = mul_nat_nat_nat (pf3_mul)
in
// nothing
end else let
prval FACTind (pf1_fac, pf1_mul) = pf_fac
prval FACTbas () = pf1_fac
prval () = mul_elim {1,1} (pf1_mul)
in
// nothing
end // end of [sif]
// end of [lemma]
}
prval [p,q:int]
(pf_prime, pf1_mul) = lemma10 {r+1} () // pf1_mul: p * q = r+1
prval () = (sif p <= n then let
prval [k:int] pf2_mul = lemma20 {n,r} {p} (pf_fac) // pf2_mul: k * p = r
prval pf2_mul = mul_negate (pf2_mul) // pf2_mul: ~k * p = ~r
prval pf2_mul = mul_commute (pf2_mul) // pf2_mul: p * ~k = ~r
prval pf3_mul = mul_distribute (pf1_mul, pf2_mul) // pf3_mul: p * (q-k) = 1
prval pf3_mul = mul_commute (pf3_mul) // pf3_mul : (q-k) * p = 1
in
sif q > k then let
prval MULind pf4_mul = pf3_mul
prval () = mul_nat_nat_nat (pf4_mul)
in
// nothing
end else sif q < k then let
prval pf3_mul = mul_negate (pf3_mul) // pf3_mul: (k-q) * p = 1
prval MULind pf4_mul = pf3_mul
prval () = mul_nat_nat_nat (pf4_mul)
in
// nothing
end else let // q = k
prval MULbas () = pf3_mul in ()
end // end of [sif]
end else begin
// nothing
end) : [p > n] void // end of [prval]
in
#[p | pf_prime]
end // end of [infprime]

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

(* end of [infprime.dats] *)
```

```(*
**
** A proof of the pigeonhole principle in ATS
**
**
** Author: Hongwei Xi (hwxi AT cs DOT bu DOT edu)
** Time: September 28, 2009
**
*)

(*

What is encoded and proven in ATS is the following formulation of
pigeonhole principle:

Let P be a relation on pairs of integers and m and n be two naturnal
numbers satisfying m > n and n >= 1. If there exists a natural number
j < n for each given naturnal number i < m such that P (i, j) holds,
then there exists i1, i2 and j satisfying 0 <= i1 < i2 < m and j < n
such that both P (i1, j) and P (i2, j) hold.

*)

sortdef int2rel = (int, int) -> prop // for binary relations on integers

prfun pigeonhole
{P: int2rel} {m,n:nat | m > n; n >= 1} .<m>. (
fpf: {i:nat | i < m} () -> [j:nat | j < n] P (i, j)
) : [i1,i2,j:nat | i1 < i2; i2 < m] (P (i1, j), P (i2, j)) = sif n >= 2 then let
val [x:int] pf0 = fpf {m-1} ()
dataprop P1 (i:int, int) =
| P1r1 (i, 0) of P (i, x)
| {x>0} P1r2 (i, x-1) of P (i, 0)
| {j:int | j > 0; j <> x} P1r3 (i, j-1) of P (i, j)
prfn fpf1 {i:nat | i < m-1} (): [j:nat | j < n-1] P1 (i, j) = let
val [j:int] pf = fpf {i} ()
in
sif j == 0 then
(sif x == 0 then P1r1 (pf) else P1r2 (pf))
else
(sif j == x then P1r1 (pf) else P1r3 (pf))
// end of [sif]
end // end of [fpf1]
val [i1,i2,j:int] (pf1, pf2) = pigeonhole {P1} {m-1,n-1} (fpf1)
in
case+ pf1 of
| P1r1 (pf1) => (pf1, pf0)
| P1r2 (pf1) => begin case+ pf2 of
| P1r1 pf2 => (pf2, pf0) | P1r2 pf2 => (pf1, pf2)
end // end of [P1r2]
| P1r3 (pf1) => begin case+ pf2 of
| P1r1 pf2 => (pf2, pf0) | P1r3 pf2 => (pf1, pf2)
end // end of [P1r3]
end else begin // n = 1
(fpf {0} (), fpf {1} ())
end // end of [pigenhole]

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

(* end of [pigeonhole.dats] *)
```