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] *)

This page is maintained by Hongwei Xi. As always, your comments are welcome.