tutch Bug in primitive recursion

Question

I'd like to prove a simple proposition:

  !m:nat. !n:nat. m < s(n) => (m = n | m < n)

i.e. if m < n + 1, then either m = n or m < n. This is a proposed proof term:

term lemmaCompleteInduction :
  !m:nat. !n:nat. m < s(n) => (m = n | m < n)
=
  fn m =>
    rec m of
      g 0 =>
        (fn n => fn u =>
          rec n of
            h 0 => inl eq0
          | h (s(n')) => inr less0
          end
        )
    | g (s(m')) =>
        (fn n => fn u =>
          rec n of
            k 0 => lessE0 (lessES u)          % type mismatch here
          | k (s(n')) =>
            case g m' n' (lessES u) of
              inl p => inl (eqS p)
            | inr p => inr (lessS p)
            end
          end
        )
    end ;

[gs100.sp.cs.cmu.edu:50 ] tutch ass8.tut
TUTCH 0.52 beta, $Date: 2002/10/24 19:25:49 $
[Opening file ass8.tut]
...
Checking term lemmaCompleteInduction: !m:nat. !n:nat. m < s n => m = n | m < n
ass8.tut:84.28-84.36 Error:
Type mismatch: lessES u proves m' < n, but a proof of a less-than relation between natural numbers is required in this place

So, the situtation is as follows:

 1) m = m' + 1              (second branch of 'rec m of ...')
 2) u : m < s n
 3) n = 0                   (first branch of 'rec n of ...')
 4) lessES u : m' < n       (this is what the Tutch message says.)

Since lessES u proves m' < n and we have n = 0, it looks like

  lessE0 (lessES u)

should typecheck.

Answer

Here is a minor variant of your proof that works:

term lemmaCompleteInduction :
  !m:nat. !n:nat. m < s(n) => (m = n | m < n)
=
  fn m =>
    rec m of
      g 0 =>
        (fn n =>
          rec n of
            h 0 => fn u => inl eq0
          | h (s(n')) => fn u => inr less0
          end
        )
    | g (s(m')) =>
        (fn n =>
          rec n of
            k 0 => fn u => lessE0 (lessES u)
          | k (s(n')) => fn u =>
            case g m' n' (lessES u) of
              inl p => inl (eqS p)
            | inr p => inr (lessS p)
            end
          end
        )
    end ;

All I have changed is: I have moved the abstraction "fn u =>" into the inner primitive recursion. Now, "rec" is done only over variables immediately after their abstraction. This means that the type of "u" does not have to be updated after "n" is instantiated to "0" or "s(n')". This update of the value of "n" seems to be missing or buggy in tutch.

Last modified: Mon Mar 14 15:31:44 CET 2005