Consider the following example:

```
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Module EQ.
Record class (T: Type) := Class {cmp: T -> T -> bool}.
Structure type := Pack{obj: Type; class_of: class obj}.
Definition op (e: type): obj e -> obj e -> bool :=
let 'Pack (Class the_cmp) := e in the_cmp.
Arguments op {e} x y : simpl never.
Arguments Class {T} cmp.
Module theory.
Notation "x == y" := (op x y) (at level 70).
End theory.
End EQ.
Import EQ.theory.
Fixpoint nat_eq x y :=
match x, y with
| O, O => true
| S x', S y' => nat_eq x' y'
| _, _ => false
end.
Canonical Structure nat_eq_ty : EQ.type.
Proof.
(*econstructor works*)
```

I want a way nicer than `econstructor`

and `apply .. with`

that kind of unfolds `EQ.type`

Imagine I have like 20~30 lemmas to prove how can I do it nicely with tactics language.

what I want to do is to solve all the goals one by one instead of having to do a very long `apply ... with ...`

please explain more what's wrong with econstructor

nothing is wrong with `econstructor`

by I have intuition that `econstructor`

is mostly for testing/prototyping and it is not final solutions. but I can be wrong.

The question is not CS specific, please retitle

I am not sure I am following what you are trying to say

I'm not sure you want to define CSes using tactics (beyond prototyping); math-comp's pattern never does it. In qed proofs, econstructor or eapply are options, but ssreflect tactics like apply: or apply/ work better with CSes (they use a different unification algorithm)

What I typically do when I want to define a record which has 20..30 lemmas is to create a module where each lemma is in and then just fill in the names in the record definition.

Apparently I couldn't do it with econstructor either,

at `Qed`

coq complained about something broken,

@Michael Soegtrop

I see, I thought it might be a bit more intuitive that to prove the record instead but I might have to do it the way you described.

`econstructor`

might shelve some goals (= keeping them aside in the hope that they are automatically solved by unification when closing another goal). A pattern that I sometimes use is the combination `unshelve econstructor`

to obtain all the created goals and not leave any on the shelf.

You can also bypass `econstructor`

entirely and apply the constructor of your choice, in your case `Eq.Pack`

(yes it does depends on knowing the record you want to build, but that sounds reasonable when you want to inhabit that record type).

unshelve econstructor, almost works!

```
Canonical Structure foo : EQ.type.
Proof.
unshelve econstructor.
- apply nat.
- constructor.
apply nat_eq.
Qed.
```

gives the following error:

```
Could not declare a canonical structure foo.
Could not find its value in the global environment.
No more subgoals.
```

But I figured that I can just put everything in the record `class`

and that will be the thing that is populated

I think Qed is not correct here, you'd need Defined: Qed means Coq can't even find or run your nat_eq function

I wonder if that explains those errors

yeah it makes perfect sence, I forgot that this case Qed is not good, I thought maybe there is a deep hidden reason.

Last updated: Sep 23 2023 at 14:01 UTC