Coq 中的高效记录构建：直接证明包含可能吗？

Question

我想在 Coq 中定义一个小记录，其中还包括某些条件。此外，我想要一个定义来以简单的方式创建记录。这是我的方法：

Require Import Arith.

(* Define the qn record with conditions for q and n *)
Record qn := {
    q : nat;
    q_ge_2 : leb 2 q = true; (* Ensuring q is greater or equal than 2 *)
    n : nat;
    n_ge_1 : leb 1 n = true  (* Ensuring n is greater or equal than 1 *)
  }.

(* A support function to create instances of qn more conveniently *)
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 |}.

(* Examples of qn *)
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).

我已经尝试了一些不同的方法 - 也定义了 qn 记录，例如使用 Prop 而不是 bool。

有没有办法简化

make_qn

定义以直接包含证明？例如。像这样使用它

Example qn_simple1 : qn := make_qn 2 1

Answer 1

这是我尝试简化您的代码。

1. 我使用

   Prop

   代替

   bool

   ，因为

   lia

   更喜欢

   Prop

   ，但

   bool

   也可以与其他工具一起保留以证明不等式（甚至简单的计算）。
2. 我没有在记录外部定义

   make_qn

   ，而是为记录构造函数指定一个名称。
3. 我在示例中使用

   ltac:(tactic)

   构造证明项。

它可能并不完美（例如，该记录的平等性必须使用某种形式的无关性证明）。

我认为没有一个神奇的解决方案可以在不给出证明条件的情况下构建元素。

Require Import Arith.

(* Define the qn record with conditions for q and n *)
(* I have changed bool with Prop. *)
Record qn := MakeQn {
    q : nat;
    q_ge_2 : q >= 2; (* Ensuring q is greater or equal than 2 *)
    n : nat;
    n_ge_1 : n >= 1  (* Ensuring n is greater or equal than 1 *)
  }.

Require Import Lia.
(* Examples of qn *)
Example qn_example1 : qn := MakeQn 2 ltac:(lia) 1 ltac:(lia).
Example qn_example2 : qn := MakeQn 3 ltac:(lia) 5 ltac:(lia).
Example qn_example3 : qn := MakeQn 4 ltac:(lia) 2 ltac:(lia).