Introduction to Programming in ATS:
<<< PreviousTheorem-Proving in ATS/LFNext >>>

Datasorts

A datasort is rather similar to a dataype. However, the former is declared in the statics of ATS while the latter in the dynamics of ATS. To see a typical need for datasorts, let us try to encode a theorem in ATS stating that s is strictly less than 2h if s and h are the size and height, respectively, of a given binary tree. To represent binary trees in the statics, we first declare a datasort as follows: 

datasort tree = E of () | B of (tree, tree)

The name of the declared datasort is tree and there are two constructor associated with it: E and B, where E forms the empty tree and B forms a tree by joining two given trees. For instance, B(E(), E()) is a static term of the sort tree that represents a singleton tree, that is, a tree consisting of exactly one node. Please note that the trees formed by E and B are really just tree skeletons carrying no data.

We now declare two dataprops as follows for capturing the notion of size and height of trees: 

dataprop SZ (tree, int) =
  | SZE (E (), 0) of ()
  | {tl,tr:tree} {sl,sr:nat}
    SZB (B (tl, tr), 1+sl+sr) of (SZ (tl, sl), SZ (tr, sr))
// end of [SZ]

dataprop HT (tree, int) =
  | HTE (E (), 0) of ()
  | {tl,tr:tree} {hl,hr:nat}
    HTB (B (tl, tr), 1+max(hl,hr)) of (HT (tl, hl), HT (tr, hr))
// end of [HT]

Given a tree t and an integer s, SZ(t, s) encodes the relation that the size of t equals s. Similiarly, given a tree t and an integer h, HZ(t, h) encodes the relation that the height of t equals h.

As the power function (of base 2) is not available in the statics of ATS, we declare a dataprop as follows to capture it: 

dataprop POW2 (int, int) =
  | POW2bas (0, 1)
  | {n:nat} {p:int} POW2ind (n+1, p+p) of POW2 (n, p)
// end of [POW2]

Given two integers h and p, POW2 (h, p) encodes the relation that 2h equals p.

It should be clear by now that the following proof function interface encodes the theorem stating that s is strictly less than 2h if s and h are the size and height of a given binary tree: 

extern
prfun lemma_tree_size_height
  {t:tree} {s,h:nat} {p:int} (
  pf1: SZ (t, s), pf2: HT (t, h), pf3: POW2 (h, p)
) : [s < p] void // end of [prfun]

Let us now construct an implementation of this proof function as follows.

We first establish some elementary properties on the power function (of base 2): 

prfun pow2_istot
  {h:nat} .<h>. (): [p:int] POW2 (h, p) =
  sif h > 0 then POW2ind (pow2_istot {h-1} ()) else POW2bas ()
// end of [pow2_istot]

prfun pow2_pos
  {h:nat} {p:int} .<h>.
  (pf: POW2 (h, p)): [p > 0] void =
  case+ pf of
  | POW2ind (pf1) => pow2_pos (pf1) | POW2bas () => ()
// end of [pow2_pos]

prfun pow2_inc
  {h1,h2:nat | h1 <= h2} {p1,p2:int} .<h2>.
  (pf1: POW2 (h1, p1), pf2: POW2 (h2, p2)): [p1 <= p2] void =
  case+ pf1 of
  | POW2ind (pf11) => let
      prval POW2ind (pf21) = pf2 in pow2_inc (pf11, pf21)
    end
  | POW2bas () => pow2_pos (pf2)
// end of [pow2_inc]

Clearly, pow2_istot shows that the relation encoded by the dataprop POW2 is a total relation; pow2_pos proves that the power of each natural number is positive; pow2_inc establishes that the power function is increasing.

The function lemma_tree_size_height can be implemented as follows: 

implement
lemma_tree_size_height
  (pf1, pf2, pf3) = let
//
prfun lemma
  {t:tree} {s,h:nat} {p:int} .<t>. (
  pf1: SZ (t, s), pf2: HT (t, h), pf3: POW2 (h, p)
) : [p > s] void =
  scase t of
  | B (tl, tr) => let
      prval SZB (pf1l, pf1r) = pf1
      prval HTB {tl,tr} {hl,hr} (pf2l, pf2r) = pf2
      prval POW2ind (pf31) = pf3
      prval pf3l = pow2_istot {hl} ()
      prval pf3r = pow2_istot {hr} ()
      prval () = lemma (pf1l, pf2l, pf3l)
      prval () = lemma (pf1r, pf2r, pf3r)
      prval () = pow2_inc (pf3l, pf31)
      prval () = pow2_inc (pf3r, pf31)
    in
      // nothing
    end // end of [B]
  | E () => let
      prval SZE () = pf1
      prval HTE () = pf2
      prval POW2bas () = pf3
   in
     // nothing
   end // end of [E]
//
in
  lemma (pf1, pf2, pf3)
end // end of [lemma_tree_size_height]

The inner function lemma, which is given a termination metric consisting of a static term of the sort tree, corresponds to a proof based on structural induction (where the involved structure is the binary tree t). Given two terms t1 and t2 of the sort tree, t1 is (strictly) less than t2 if t1 is a (proper) substructure of t2. Evidently, this is a well-founded ordering. The keyword scase is used to form a dynamic expression that does case-analysis on a static term (built by constructors associated with some declared datasort). So the relation between sif and scase is essentially parallel to that between if and case. Please find the entirety of the above code on-line.

<<< PreviousHomeNext >>>
Example: Proving Distributivity of MultiplicationUpExample: Proving Properties on Braun Trees