Ergonomic way to define elements of dependent records in proof mode?

Question

I tend to have trouble defining elements of dependent records when I would like to define their fields in proof mode.

Consider the following simple minimal example:

Record foo : Type := {
  num : nat;
  num_refl : num = num
  }.

Goal foo.
Proof.
  econstructor.
  (* goal is now ?num = ?num *)
Abort.

I would like to be able to instantiate ?num in proof mode since ?num stands in for expressions that generally will be difficult to write out by hand. Ideally, I would like to be able to do something like the following:

Goal foo.
Proof.
  better_econstructor.
  (* generates two goals, nat and ?num = ?num *)
  - exact 2.
  - (* goal is now 2 = 2 *) reflexivity.
Defined.

Are there any approaches that mimic this style? Right now, I define the non-dependent stuff elsewhere and then do the proofs using refine, i.e. something like

Definition two : nat := 2.

Goal foo.
Proof.
  refine {|
    num := two;
    num_refl := _
    |}.
  reflexivity.
Defined.

This works but is a bit tedious when it involves copying and pasting a lot of types.

Answer 1

You can use the unshelve tac tactical. It applies tac and transforms every existential variable it creates into a goal.

Goal foo.
Proof.
  unshelve econstructor.