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

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?

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

• I know your suggested way. By the way, I might use this 'dlos' a hundreds of times, and every time I write 'as...' seems not so good. (Moreover, since the number of my components of dlos is many, if I write 'as ... ' then it possesses many spaces. ) Thus I share my question. Aug 10, 2022 at 2:39
• You can define a new tactic to prevent retyping out the syntax: Ltac destruct_dlos S := destruct S as [X x]. Aug 10, 2022 at 2:52

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