2
$\begingroup$

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?

$\endgroup$

2 Answers 2

2
$\begingroup$

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

$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$ Aug 10 at 2:39
  • 1
    $\begingroup$ You can define a new tactic to prevent retyping out the syntax: Ltac destruct_dlos S := destruct S as [X x]. $\endgroup$ Aug 10 at 2:52
0
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.