Coq中高效构造记录：能否直接嵌入证明？

你好！看了你的需求，确实在Coq里构造带约束的记录时，手动传那些eq_refl true的证明项有点繁琐——你想让make_qn能直接像make_qn 2 1这样调用，不用额外写证明参数对吧？我给你整理了几种实用的简化方案，让构造过程更顺畅。

先回顾下你当前的实现，方便对比：

Require Import Arith.

(* 定义带约束的qn记录 *)
Record qn := {
  q : nat;
  q_ge_2 : leb 2 q = true; (* 确保q ≥ 2 *)
  n : nat;
  n_ge_1 : leb 1 n = true  (* 确保n ≥ 1 *)
}.

(* 构造函数需要手动传入证明项 *)
Definition make_qn (q n: nat) (Hq : leb 2 q = true) (Hn : leb 1 n = true) : qn :=
{| q := q; q_ge_2 := Hq; n := n; n_ge_1 := Hn |}.

(* 示例需要手动传证明 *)
Example qn_example1 : qn := make_qn 2 1 (eq_refl true) (eq_refl true).
Example qn_example2 : qn := make_qn 3 5 (eq_refl true) (eq_refl true).
Example qn_example3 : qn := make_qn 4 2 (eq_refl true) (eq_refl true).

方案1：用隐式参数让Coq自动填充证明 #

你可以把构造函数里的证明参数设为隐式参数，让Coq自动尝试寻找对应的证明项。修改后的make_qn可以直接省略证明参数调用：

Require Import Arith.

Record qn := {
  q : nat;
  q_ge_2 : leb 2 q = true;
  n : nat;
  n_ge_1 : leb 1 n = true
}.

(* 将Hq和Hn设为隐式参数，用{}包裹 *)
Definition make_qn (q n: nat) {Hq : leb 2 q = true} {Hn : leb 1 n = true} : qn :=
{| q := q; q_ge_2 := Hq; n := n; n_ge_1 := Hn |}.

(* 告诉Coq自动尝试用reflexivity证明这些布尔等式 *)
Arguments make_qn q n {Hq Hn} : simpl never.

(* 现在就能直接这样调用了！ *)
Example qn_simple1 : qn := make_qn 2 1.
Example qn_simple2 : qn := make_qn 3 5.
Example qn_simple3 : qn := make_qn 4 2.

这里的核心是{Hq Hn}语法把证明参数标记为隐式，Coq会自动检查是否能通过简单策略（比如reflexivity）证明这些布尔等式，完全不需要你手动写eq_refl true。

方案2：改用Prop类型约束（更符合Coq逻辑风格） #

你提到过尝试用Prop代替bool，这其实是Coq里更常用的做法——Prop是Coq的逻辑命题类型，配合lia这类算术证明策略，能处理更复杂的约束场景。重新定义记录后，构造过程会更直观：

Require Import Arith Lia.

(* 改用直观的Prop约束：直接写q ≥ 2、n ≥ 1 *)
Record qn := {
  q : nat;
  q_ge_2 : 2 <= q;
  n : nat;
  n_ge_1 : 1 <= n
}.

(* 用Program Definition让Coq自动生成证明义务，再用lia自动解决 *)
Program Definition make_qn (q n: nat) (Hq : 2 <= q) (Hn : 1 <= n) : qn :=
{| q := q; q_ge_2 := Hq; n := n; n_ge_1 := Hn |}.
Next Obligation. lia. Qed.

(* 同样设为隐式参数，调用时无需传证明 *)
Arguments make_qn q n {Hq Hn} : simpl never.

(* 直接构造实例，甚至支持表达式形式的参数 *)
Example qn_simple1 : qn := make_qn 2 1.
Example qn_simple2 : qn := make_qn 3 5.
Example qn_simple3 : qn := make_qn (1+3) (2*1).

这种方式的优势是约束可读性更强，而且lia能处理各种算术表达式的证明，哪怕q或n是计算出来的值，Coq也能自动验证约束。

方案3：用自定义Ltac战术快速构造 #

如果需要在证明脚本里快速生成实例，还可以写一个自定义的Ltac战术，直接跳过证明项的手动处理：

Require Import Arith.

Record qn := {
  q : nat;
  q_ge_2 : leb 2 q = true;
  n : nat;
  n_ge_1 : leb 1 n = true
}.

(* 自定义战术，自动填充证明项 *)
Ltac make_qn_tac q_val n_val :=
  refine ({| q := q_val; q_ge_2 := _; n := n_val; n_ge_1 := _ |});
  reflexivity.

(* 在证明中使用战术构造实例 *)
Example qn_simple1 : qn.
Proof. make_qn_tac 2 1. Qed.

Example qn_simple2 : qn.
Proof. make_qn_tac 3 5. Qed.

这个战术会自动生成记录的框架，并用reflexivity填充所有布尔约束的证明项，适合在交互式证明里快速构造实例。

总结 #

如果想保留你原来的布尔约束风格，方案1最直接；如果希望更贴合Coq的逻辑推理习惯，方案2的Prop约束+lia更灵活，能应对复杂场景；方案3则适合在证明脚本里快速生成实例。

备注：内容来源于stack exchange，提问作者Andreas Florath