The Coq mailing list

[Matthew Brecknell <coq-club AT brecknell.org>]

Jeff Terrell wrote:
> Is it possible to configure Coq so that the assumptions underlying all
> goals are displayed at each step? For example, the assumptions
> underlying subgoal 2 do appear later, but only when subgoal 2 becomes
> the current goal.

I'm not aware of such a feature, but that may just be because I haven't
looked for it in the manual. :-)

> T < exists nil.
> 
> Interestingly, any list of packages would work, not only nil. Given
> that the specification defines a transformation between lists of
> processes and lists of packages, one would intuitively expect an empty
> list of processes to be mapped to an empty list of packages. However,
> there's nothing in the specification to enforce this, which suggests
> that the specification lacks precision. I presume the alternative
> method of proof (using the map function) accounts for this.

For this subgoal, all you care about is getting hold of the false
hypothesis (In p nil), since that allows you to solve the subgoal
without further ado. Thus, any list which eliminates the existential
quantifier is fine: "nil" is just the easiest list to exhibit.

This theorem does not serve well as a specification, and the proof using
"map" does nothing to change this. For example, this obfuscated proof
also works:

Proof.
  Hint Resolve in_map in_or_app.
  intro l; exists (map p2p l ++ map p2p l);
  intro p; exists (p2p p); auto.
Qed.

> Is it possible to specify the name 'a' above (which appears to have
> come from the induction step at the beginning of the proof) and the
> name 'x' below (which is a witness of the existential quantification
> above)?

Adam has already answered this, but he didn't mention that his
book-in-progress also describes a general approach to writing robust
proofs using Ltac pattern matching:

http://adam.chlipala.net/cpdt/

Well worth a read. The exercises are challenging, but rewarding.
(Thanks, Adam!)

> Could you explain the difference between simpl and (a possible
> alternative) unfold In in this context. Both appear to do a similar
> sort of thing (although one is more concise than the other), and both
> work.

There are numerous ways to ask Coq to perform various kinds of
reductions. See also the manual entries for "cbv" and "lazy". Often it
is not really necessary to use these, since many tactics will perform
reductions automatically, and this proof is no exception. However, I
frequently use "simpl" during exploratory work, since it often helps to
clarify a goal. I just forgot to remove it (and the unfold) from the
proof before I posted.

Regards,
Matthew