主页 / coding / 问题 / 77738685
Accepted
Andreas Florath
Asked: 2023-12-31 17:07:56 +0800 CST

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

  • 772

我想在 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
coq

2 个回答

  1. Best Answer

    考虑以下定义qn（为了方便起见，我重命名了一些内容）：

    (* Define [qn] with conditions for [q] and [n]. *)
Record qn := mkQn
{
  qn_q : nat ;
  qn_n : nat ;
  qn_q_ge_2 : qn_q >= 2 ;
  qn_n_ge_1 : qn_n >= 1 ;
}.

    前提是 Coq 中的所有函数都必须是总计的，我们实际上可以证明根据您的问题不存在“快捷构造qn函数”，即不存在（总计）函数，给定任意 q和n，返回qn这样的它的qn_q=q和qn_n= n：

    (* The type of "short-cutting [qn] constructors". *)
Definition MkQnSc := forall q n : nat,
  { i : qn | i.(qn_q) = q /\ i.(qn_n) = n }.

(* [MkQnSc] is empty! *)
Lemma no_MkQnSc : MkQnSc -> False.
Proof.
  unfold MkQnSc.
  intros F.
  destruct (F 0 0) as [[q n Hq Hn] [Eq _]].
  simpl in Eq.
  rewrite Eq in Hq.
  inversion Hq.
Qed.

    顺便说一句，“快捷构造qn函数”的一种可能方法（根据您的问题）是作为option qn返回类型，尽管这当然只是移动球门柱，因为那时需要对返回的option/进行模式匹配证明我们有一个Somevs None。

    也就是说，减轻每次在构造函数中必须提供证明项的不便的一种方法（@Villetaneuse 在对他的答案的评论中也提到过）是使用带有战术的符号，它确实可以用于构造项，虽然不能用于模式匹配（我不知道其他显着差异，至少在这种情况下）：

    From Coq Require Import Lia.

Notation mkQnSc q n :=
  (mkQn q n ltac:(lia) ltac:(lia))
  (only parsing).

Example ex_qn_2_1 : qn := mkQnSc 2 1.  (* OK *)

Fail Definition is_qn_2_1 (i : qn) : Prop :=
  match i with
  | mkQnSc 2 1 => True
  | _          => False
  end.  (* ERROR: Quotations not supported in patterns *)

Definition is_qn_2_1 (i : qn) : Prop :=
  match i with
  | mkQn 2 1 _ _ => True
  | _            => False
  end.  (* OK *)
    • 1

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

    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).
    • 0

相关问题