When I destruct record, can I make a hypothesis name without 0?

Question

I made such record.

Record dlos := mkdlos { 
  X : Type; 
  Xlt : relation X;
  Xeq : relation X; 
  eq : equivalence Xeq;
  st : strict_order Xlt;
  to : total_order Xlt Xeq;
  den : dense Xlt;
}.

For example, if I wrote such code,

Example exists_0 (S : dlos) : 
True. 
Proof. 
destruct S. 

then I saw this window.

1 goal
X0 : Type
Xlt0, Xeq0 : relation X0
eq0 : equivalence Xeq0
st0 : strict_order Xlt0
to0 : total_order Xlt0 Xeq0
den0 : dense Xlt0
______________________________________(1/1)
True

I want to erase all of 0 by default.

Is there a way to do this?

Answer 1

The following will give you explicit names:

Record dlos := mkdlos { 
  X : Type; 
  x: X;
}.

Example exists_0 (S : dlos) : 
True. 
Proof. 
destruct S as [X x]. 

or if you are going to be destructing the record a lot of times, you can define a new tactic:

Ltac destruct_dlos S := destruct S as [X x] || destruct S.

Example exists_0 (S : dlos) (R : dlos): 
True. 
Proof. 
destruct_dlos S.
destruct_dlos R.

Note that the above definition will switch to a regular destruct where Coq chooses the names if the explicit destruct fails.

Generally speaking, the as ... part of a tactic lets you provide explicit names, with as [a b c...] naming products (pairs, records) and as [a|b|...] naming sums (inductive data).

Answer 2

It may be worth having a look at Pierre Courtieu's LibHyps library, which allows you to control the new hypotheses generated by a tactic.

https://github.com/Matafou/LibHyps