The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Mon, 25 Oct 2010 16:53:36 +0100,
Randy Pollack 
<rpollack AT inf.ed.ac.uk>
 a écrit :

> 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.

In fact, I believed it was already the case,
but it is only the case for inversion

Lemma test: forall (n:nat), np n -> np O.
intros.
inversion_clear H.

1 subgoal
n : nat
pr1 : np 0
______________________________________(1/1)
np 0


But that won't solve the problem, as lot of inductives are
not tagged, and tagging them can make them less readable.

For instance, the "inhabited" type it was question recently is:
"Inductive inhabited (A: Type) : Prop :=
inhabitant : A -> inhabited A.".

I am not sure that having

Inductive inhabited (A: Type) : Prop :=
inhabitant : forall (inhabitant : A), inhabited A.

would be more clear.

(Ok, you can use "Record inhabited (A: Type) : Prop :=
                  {inhabitant: A}."
which has IMO better syntax, but when multiple
constructors occur, you cannot do that)

Patching that should not be too hard, since "inversion" does what you
say.

What you suggest would certainly be more readable;
I think it should be used before trying to hash values, even if in
some cases (2 inductives sharing the same parameter name) it will
have collisions (but in practice, that won't be a real problem).

> 
> 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.
>  > 
>