The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi all,

Is there some way to use some, but not all features of Program? The
opening of goals for "_" is sometimes really useful, while I find the
automatic introduction of eq_rect fairly disturbing -- not to mention
that it makes debugging pretty much impossible, since Coq will just
accept completely broken definitions and then expect you to show
impossible equivalences.

For example, consider this definition:

==============
Require Import Program.

Inductive tt : nat -> Type :=
| TT (n CTX : nat) : tt (CTX + n).

Program Definition t n : tt 5 := match n with
                               | O => TT 6 1
                               | S n => TT 0 5
                               end.
Next Obligation.
(* Goal: 7 = 5. This is not going to work out... *)
===============

What happens here is that Program inserts an eq_rect in the first arm of
the match, and then has me prove the necessary inequality. I'd much
rather explicitly call a cast function when coercions over equalities
are necessary. With eq_rect being inserted, there may be coercions in
places where you don't expect them (if Program solves that obligation
automatically), so I find myself manually checking "Print my_def" for
unexpected occurrences of eq_rect (and I found some!). Furthermore, in
case of a typo one does not get an error message (stating the expected
and actual type), but an impossible to prove and also often impossible
to parse goal. For some definitions the best I can do is watch the
number of obligations that are created; if it's 4, then I have a type
error somewhere (where? no idea), if it's 2, the definition is all
right. That is a pretty horrible way to write complex definitions.

It would be nice if there was a way to gradually use some of the
features of Program, without being forced to use others. Is that possible?

Kind regards,
Ralf