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

Example: Proving Properties on Braun Trees

As stated previously in this book, a binary tree is a Braun tree if it is empty or if its left and right subtrees are Braun trees and the size of the left one minus the size of the right one is either 0 or 1. Formally, we can declare the following dataprop isBraun to capture the notion of Braun trees: 

dataprop isBraun (tree) =
  | isBraunE (E) of ()
  | {tl,tr:tree}
    {sl,sr:nat | sr <= sl; sl <= sr + 1}
    isBraunB (
      B(tl, tr)) of (isBraun tl, isBraun tr, SZ (tl, sl), SZ (tr, sr)
    ) // end of [isBraunB]
// end of [isBraun]

We first prove that there exists a Braun tree of any given size. This property can be encoded as follows in ATS: 

extern
prfun lemma_existence {n:nat} (): [t:tree] (isBraun (t), SZ (t, n))

Literally, the type assigned to lemma_existence means that there exists a tree t for any given natural number n such that t is a Braun tree and the size of t is n. The following code gives an implementation of lemma_existence: 

implement
lemma_existence {n} () = let
  prfun lemma {n:nat} .<n>.
    (): [t:tree] (isBraun (t), SZ (t, n)) =
    sif n > 0 then let
      stadef nl = n / 2 // size for the left subtree
      stadef nr = n - 1 - nl // size for the right subtree
      val (pfl1, pfl2) = lemma {nl} ()
      and (pfr1, pfr2) = lemma {nr} ()
    in
      (isBraunB (pfl1, pfr1, pfl2, pfr2), SZB (pfl2, pfr2))
    end else
      (isBraunE (), SZE ())
    // end of [sif]
in
  lemma {n} ()
end // end of [lemma_existence]

Note that stadef is a keyword in ATS for introducting a static binding between a name and a static term (of any sort). If one prefers, this keyword can be chosen to replace the keyword typedef (for introducing a name and a static term of the sort t@ype).

Next we show that two Braun trees of the same size are identical. This property can be encoded as follows: 

extern
prfun lemma_unicity {n:nat} {t1,t2:tree} (
  pf1: isBraun t1, pf2: isBraun t2, pf3: SZ (t1, n), pf4: SZ (t2, n)
) : EQ (t1, t2) // end of [lemma_unicity]

where EQ is a prop-constructor introduced by the following dataprop declaration: 

dataprop EQ (tree, tree) =
  | EQE (E, E) of ()
  | {t1l,t1r:tree} {t2l,t2r:tree}
    EQB (B (t1l, t1r), B (t2l, t2r)) of (EQ (t1l, t2l), EQ (t1r, t2r))
// end of [EQ]

Clearly, EQ is the inductively defined equality on trees. An implementation of the proof function lemma_unicity is presented as follows: 

implement
lemma_unicity (pf1, pf2, pf3, pf4) = let
  prfun lemma {n:nat} {t1,t2:tree} .<n>. (
    pf1: isBraun t1, pf2: isBraun t2, pf3: SZ (t1, n), pf4: SZ (t2, n)
  ) : EQ (t1, t2) =
    sif n > 0 then let
      prval SZB (pf3l, pf3r) = pf3
      prval SZB (pf4l, pf4r) = pf4
      prval isBraunB (pf1l, pf1r, pf1lsz, pf1rsz) = pf1
      prval isBraunB (pf2l, pf2r, pf2lsz, pf2rsz) = pf2
      prval () = SZ_istot (pf1lsz, pf3l) and () = SZ_istot (pf1rsz, pf3r)
      prval () = SZ_istot (pf2lsz, pf4l) and () = SZ_istot (pf2rsz, pf4r)
      prval pfeql = lemma (pf1l, pf2l, pf3l, pf4l)
      prval pfeqr = lemma (pf1r, pf2r, pf3r, pf4r)
    in
      EQB (pfeql, pfeqr)
    end else let
      prval SZE () = pf3 and SZE () = pf4
      prval isBraunE () = pf1 and isBraunE () = pf2
    in
      EQE ()
    end // end of [sif]
in
  lemma (pf1, pf2, pf3, pf4)
end // end of [lemma_unicity]

Note that the proof function SZ_istot in this implementation of lemma_unicity is given the following interface: 

extern
prfun SZ_istot {t:tree} {n1,n2:int}
  (pf1: SZ (t, n1), pf2: SZ (t, n2)): [n1==n2] void

which simply states that SZ is a functional relation with respect to its first parameter, that is, there is at most one n for every given t such that t and n are related according to SZ. Clearly, the mathematical proof corresponding to this implementation is of induction on the size n of the two given trees t1 and t2. In the base case where n is 0, t1 and t2 are equal as they both are the empty tree. In the inductive case where n > 0, it is proven that n1l and n2l are of the same value where n1l and n2l are the sizes of the left subtrees of t1 and t2, respecitvely; similarly, it is also proven that n1r and n2r are of the same value where n1r and n2r are the sizes of the right subtrees of t1 and t2, respectively; by induction hypothesis on n1l, the left substrees of t1 and t2 are the same; by induction hypothesis on n1r, the right substrees of t1 and t2 are the same; by the definition of tree equality (encoded by EQ), t1 and t2 are the same.

As a comparison, the following code gives another implementation of lemma_unicity that is of a different (and rather unusual) style: 

implement
lemma_unicity (pf1, pf2, pf3, pf4) = let
  prfun lemma {n:nat} {t1,t2:tree} .<t1>. (
    pf1: isBraun t1, pf2: isBraun t2, pf3: SZ (t1, n), pf4: SZ (t2, n)
  ) : EQ (t1, t2) =
    case+ (pf1, pf2) of
    | (isBraunE (), isBraunE ()) => EQE ()
    | (isBraunB (pf11, pf12, pf13, pf14),
       isBraunB (pf21, pf22, pf23, pf24)) => let
//
        prval SZB (pf31, pf32) = pf3
        prval SZB (pf41, pf42) = pf4
//
        prval () = SZ_istot (pf13, pf31)
        prval () = SZ_istot (pf23, pf41)
//
        prval () = SZ_istot (pf14, pf32)
        prval () = SZ_istot (pf24, pf42)
//
        prval pfeq1 = lemma (pf11, pf21, pf31, pf41)
        prval pfeq2 = lemma (pf12, pf22, pf32, pf42)
      in
        EQB (pfeq1, pfeq2)
      end
    | (isBraunE _, isBraunB _) =/=> let
        prval SZE _ = pf3 and SZB _ = pf4 in (*none*)
      end
    | (isBraunB _, isBraunE _) =/=> let
        prval SZB _ = pf3 and SZE _ = pf4 in (*none*)
      end
in
  lemma (pf1, pf2, pf3, pf4)
end // end of [lemma_unicity]

This implementation corresponds to a proof by induction on the structure of the given tree t1. Note that the use of the special symbol =/=>, which is a keyword in ATS, is to indicate to the typechecker of ATS that the involved clause of patter matching is unreachable: It is the responsibility of the programmer to establish the falsehood on the right-hand side of the clause. Please find the entirety of the above code on-line.

<<< PreviousHomeNext >>>
DatasortsUpProgramming with Theorem-Proving