The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

Here is a principled feature going some small way in this direction
that was implemented in LEGO over a decade ago.

Consider an inductive definition; just for example take:

  Inductive np : nat -> Prop :=
    c1 : forall (n:nat) (pr1:np O), np n.

Notice I've explicitly named the premise pr1.  Now consider a proof by
induction

  Lemma test: forall (n:nat), np n -> np O.
    induction 1.

The Coq goal state now looks like:

  n : nat
  H : np 0
  IHnp : np 0
  ============================
   np 0

My suggestion is that Coq should use the user-given name of the
premise (in this case "pr1") for the assumption arising from that
premise (instead of "H").  Also Coq should use a name generated from
the premise name for the IH arising from that premise, e.g. IH_pr1
instead of IHnp.

Best,
Randy
--
AUGER Cedric writes:
 > Hi all,
 >  when we do "dirty" developpements in Coq,
 >  we use tactics like "intros.", "inversion H7.", "destruct x."
 >  without giving names.
 > 
 >  Coq generates names automatically, using a counter, and
 >  checking non collision; so that if you change the order of tactics,
 >  change your inductive types, give name to some hypothesis,
 >  clear of some hypothesis, ...,
 >  all the proof script will be broken due to shifting the names
 >  (H3 becomes H0, H4 becomes H1, ...).
 > 
 >  As these tactics exist, we want the user to be able to do
 >  "dirty" proofs, to help him, couldn't the name generation use
 >  a hash of the type of the hypothesis, so that messing with
 >  the previous operations won't "shift" the name of hypothesis
 >  (as far as two hypothesis don't have same type)?
 > 
 >  Of course, such a feature may (slightly) slow the generation of
 >  hypothesis, and imply a command like "Set NameGeneration Hash.",
 >  to keep backward compatibility, when this command doesn't appear.
 > 
 > I am not sure my message is clear and such a feature hasn't already
 > been discussed; if so, let it me know.
 > 

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.