The Coq mailing list

[Adam Megacz <megacz AT cs.berkeley.edu>]

Changes early on in a proof script may alter the number of subgoals
generated by a lemma/theorem/definition.  If the number of subgoals is
increased and no additional commands are added to deal with the new
subgoal, the terminating [Defined] or [Qed] will fail, alerting the
user -- assuming that [Program] is not in use.

I've noticed that there isn't a similar mechanism with [Program].  For
example:

   (* code up here *)

   Program Instance foo : bar.
      Next Obligation.
        tactic.
        Defined.
      Next Obligation.
        tactic.
        Defined.

   Lemma trivial : True.
      auto.
      Defined.

   (* rest of my script *)

Now, suppose a change occurs in "(* code up here *)" which causes
[Instance foo] to generate three unsolved obligations rather than two.
Unfortuantely, there is no "terminator" on the [Program Instance], so
Coq will proceed along, even processing [Lemma trivial] correctly.  No
problems will crop up until something tries to use [foo] (which hasn't
been fully defined) or until some command which is not valid inside an
instance declaration is attempted.  However, by the time this happens
it's not always easy to trace the problem back to [foo].

I've taken to inserting

   Check (@foo).

after all of my [Program Instance] declarations to guard against this --
if an extra obligation is generated the [Check] will fail.

I just thought I'd mention this.  It's probably too late to change the
syntax of [Program] to include a terminator of some sort, but others
might find the [Check] trick useful as a defensive measure.

  - a