Introduction to Programming in ATS:
PrevChapter 11. Theorem-Proving in ATS/LFNext

Example: Establishing 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: 

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: 

primplement
lemma_existence
  {n}((*void*)) = let
//
prfun
lemma{n:nat} .<n>.
(
  // argless
) : [t:tree] (isBraun (t), SZ (t, n)) =
  sif n==0
    then (isBraunE (), SZE ())
    else let
      stadef nl = n / 2
      stadef nr = n - 1 - nl
      val (pfl1, pfl2) = lemma{nl}((*void*))
      and (pfr1, pfr2) = lemma{nr}((*void*))
    in
      (isBraunB (pfl1, pfr1, pfl2, pfr2), SZB (pfl2, pfr2))
    end // end of [else]
  // end of [sif]
//
in
  lemma{n}((*void*))
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: 

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: 

primplement
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 SZE () = pf3 and SZE () = pf4
        prval isBraunE () = pf1 and isBraunE () = pf2
      in
        EQE ()
      end // end of [then]
      else 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 // end of [else]
    // 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: 

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: 

primplement
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 pattern 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.

PrevHomeNext
Algebraic DatasortsUpProgrammer-Centric Theorem-Proving