在Coq证明模式下便捷定义依赖记录元素的方法？

以下几种方法可以实现你想要的分步处理效果，无需预先在外部定义非依赖字段：

方法1：带通配符的refine拆分目标 #

直接通过refine为非依赖字段保留通配符，Coq会自动生成对应目标：

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

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

第一个目标为nat，填入2后，第二个目标自动更新为2 = 2，完全匹配你期望的分步逻辑。

方法2：econstructor配合instantiate #

先用econstructor生成依赖目标，再手动实例化占位符：

Goal foo.
Proof.
  econstructor.
  instantiate (1 := 2). (* 将第一个占位符?num替换为2 *)
  reflexivity.
Defined.

instantiate (n := term)用于替换第n个存在变量，替换后目标会自动变为2 = 2。

方法3：自定义tactic（进阶） #

如果需要频繁使用这类逻辑，可以自定义类似better_econstructor的tactic：

Ltac better_econstructor :=
  match goal with
  | [ |- foo ] => refine (Build_foo _ _)
  end.

(* 使用示例 *)
Goal foo.
Proof.
  better_econstructor.
  - exact 2.
  - reflexivity.
Defined.

这里Build_foo是Coq为foo记录自动生成的构造函数，自定义tactic后可以直接调用分步处理。

你之前的方法虽可行，但处理大量字段时会冗余，上述方法均能在证明模式内直接完成字段实例化与依赖证明，避免额外的外部定义。

内容的提问来源于stack exchange，提问作者user4614475