Feature request: don't convert a forall to an implicitation if it has an explicit variable name

[cpitclaudel]

I commonly run into the following two related issues:

1. If a quantified variable doesn't appear in the goal, its name is lost:

   Inductive Strs := Const (s: string) | Sub (s: Strs) (start len: nat) | Concat (s1 s2: Strs).
   
   Goal forall s: Strs, True.
     Fail destruct s. (* This should succeed, and the goal should be `forall s, True`, not `Strs -> True`. *)
     destruct 1.

2. When printing an inductive, the name of its arguments are often lost:

   Print Strs.
   

   Inductive Strs : Set :=
       Const : string -> Strs
     | Sub : Strs -> nat -> nat -> Strs
     | Concat : Strs -> Strs -> Strs

Would it be possible to preserve explicitly named binders? I imagine this might break things, so it would have to be under a flag? Fixing the output of Print, on the other hand, should be safe?

Coq Version

8.13

[ppedrot]

The name is technically still there in the AST, it's just ignored by notation printing. Meanwhile, destruct is explicitly designed to ignore the internal name and rely on the user-facing display, similarly to what #13837 tries to solve.

[Alizter]

Is this really something well-defined? To me, destruct s for forall s, P s would be a bit silly since the goal is alpha equivalent to any other renaming of s. In this case destruct 1 is the more sensible syntax no?

For the second, even if you have printing of low level contents, it appears that the names have been lost (replaced with _). I guess this is something that needs to be addressed.

[ppedrot]

destruct 1 does not mean the same thing, it's quite precisely the opposite. If you pass an integer to destruct it will use the first non-dependent premise. So in particular, it would not be printed as a forall.

it appears that the names have been lost

It's quite easy to fix, but then you'd have nasty interactions with tactics relying on user-facing printing.

[cpitclaudel]

Is this really something well-defined?

I think so?

To me, destruct s for forall s, P s would be a bit silly since the goal is alpha equivalent to any other renaming of s.

destruct 1 doesn't work on forall s, P s, nor should it, AFAIK:

Axiom P: nat -> Prop.
Goal forall s, P s.
  destruct 1.
  (* Error: No 1st non dependent hypothesis in current goal even after head-reduction. *)

Am I misunderstanding you?

[Alizter]

I misunderstood the meaning of destruct 1 as pointed out by ppedrot above. My first point is that s doesn't really exist as a variable in the environment so it seemed a bit dubious for a tactic to mention it.

[cpitclaudel]

It's quite easy to fix, but then you'd have nasty interactions with tactics relying on user-facing printing.

Things like intros *, or is it something more pervasive? (I was guessing it would affect handwritten scripts but not so much automated ones.)