The Coq mailing list

[Stefan Berghofer <berghofe AT in.tum.de>]

Xavier Leroy wrote:
> > PS for Benjamin P: now you understand why there are very few POPLmark
> > solutions that address part B of the challenge :-)
>
> I meant solutions written in Coq, of course.  Could it be the case
> that other provers are less challenged than Coq by mutual inductive
> definitions and by T / list T inductive definitions?

Dear all,

my solution to the POPLmark challenge in Isabelle/HOL, which is contained
in the Archive of Formal Proofs [1], addresses part B of the challenge as
well. For the datatype of F_<: types with records (see section 3 of the
proof document available from [1])

  datatype type =
      TVar nat
    | Top
    | Fun type type
    | TyAll type type
    | RcdT (name * type) list

Isabelle's datatype package generates the induction rule

  [| !!n. P1 (TVar n);
     P1 Top;
     !!T U. [| P1 T; P1 U |] ==> P1 (Fun T U);
     !!T U. [| P1 T; P1 U |] ==> P1 (TyAll T U);
     !!Ts. P2 Ts ==> P1 (RcdT Ts);
     P2 [];
     !!f fs. [| P3 f; P2 fs |] ==> P2 (f # fs);
     !!l T. P1 T ==> P3 (l, T) |]
  ==> P1 T & P2 Ts & P3 f

This looks similar to the induction rule one would get when defining a
mutually recursive datatype as described in Robert Dockins' email,
with the difference that the P2 predicate in the above rule really
works on the original list datatype, and not on some isomorphic copy
of the list datatype (see [2], section 3.4.2). Internally, the datatype
package performs the same construction as in the case of a mutually
recursive type, but then proves that the unfolded lists, which are
only used internally, are isomorphic to the original lists (see [3],
section 5.4). Functions defined by primitive recursion on the datatype
type have to be given as a set of mutually recursive equations as well.
For example, the substitution function on types is specified by

  substTT (RcdT fs) k S = RcdT (substrTT fs k S)
  ...
  substrTT [] k S = []
  substrTT (f # fs) k S = substfTT f k S # substrTT fs k S
  substfTT (l, T) k S = (l, substTT T k S)

where

  substTT :: type => nat => type => type
  substrTT :: (name * type) list => nat => type => (name * type) list
  substfTT :: (name * type) => nat => type => (name * type)

Although the approach of unfolding a datatype with nested recursion to
a datatype with mutual recursion considerably simplifies the implementation
of the datatype package, it seems that it does not scale very well, in 
particular
when defining datatypes containing many recursions through other datatypes.
I already thought of modifying Isabelle's datatype package to produce 
induction
rules using generic "all" functions (as described in Benjamin Werner's email),
and recursion equations using generic "map" functions, but it was unclear
to me how many of our users would appreciate such a change.


[1] Stefan Berghofer. POPLmark Challenge Via de Bruijn Indices. Archive of
    Formal Proofs, 
http://afp.sourceforge.net/devel-entries/POPLmark-deBruijn.shtml

[2] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL -
    A Proof Assistant for Higher-Order Logic. LNCS 2283, Springer-Verlag 2002,
    http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf

[3] Stefan Berghofer and Markus Wenzel. Inductive datatypes in HOL - lessons
    learned in Formal-Logic Engineering. TPHOLs'99, LNCS 1690. 
Springer-Verlag 1999,
    http://www.in.tum.de/~berghofe/papers/TPHOLs99.pdf


Greetings,
Stefan

--
Dr. Stefan Berghofer               E-Mail: 
berghofe AT in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe