使用 'same_relation'（以及可能的其他库定义）是否会受到惩罚？

Question

给定任何编程语言，只要存在标准库函数，我们最有可能使用它而不是编写自己的代码。有人会认为这一建议同样适用于 Coq。但是，我最近强迫自己使用Relation模块的same_relation谓词，我有一种被淘汰的感觉。所以我必须遗漏一些东西，因此我的问题。为了说明我的意思，让我们考虑可能的关系：

Require Import Relations.      (* same_relation *)
Require Import Setoids.Setoid. (* seems to be needed for rewrite *)

Inductive rel1 {A:Type} : A -> A -> Prop :=
  | rel1_refl : forall x:A, rel1 x x.   (* for example *)

Inductive rel2 {A:Type} : A -> A -> Prop :=
  | rel2_refl : forall x:A, rel2 x x.   (* for example *)

这些关系的具体细节在这里并不重要，只要rel1和rel2等价即可。现在，如果我想忽略 Coq 库，我可以简单地声明：

Lemma L1: forall (A:Type)(x y:A), rel1 x y <-> rel2 x y.
Proof.
  (* some proof *)
Qed.

如果我想听从直觉并使用 Coq 库：

Lemma L2: forall (A:Type), same_relation A rel1 rel2.
Proof.
  (* some proof *)
Qed.

在最简单的情况下，证明引理 L1 或引理 L2 似乎同样有益：

Lemma application1: forall (A:Type) (x y:A), 
  rel1 x y -> rel2 x y (* for example *)
Proof.
  intros A x y H. apply L1 (* or L2 *) . exact H.
Qed.

无论我决定使用 apply L1 还是 apply L2 都没有区别...

然而在实践中，我们可能会面临更复杂的目标：

Lemma application2: forall (A:Type) (x y:A) (p:Prop),
  p /\ rel1 x y -> p /\ rel2 x y.
Proof.
  intros A x y p H. rewrite <- L1. exact H.
Qed.

我的观点是，用 rewrite <- L2 替换 rewrite <- L1 会失败。前面的示例也是如此，但至少我能够使用 apply 而不是 rewrite。在这种情况下我不能使用 apply （除非我经历了拆分目标的麻烦）。所以好像我已经失去了使用rewrite的便利，如果我只有引理L2.

在等价（不仅仅是等价）的结果上使用 rewrite 非常方便。似乎将等价包装到谓词 same_relation 中会带走这种便利。我跟随自己的直觉并强迫自己使用 same_relation 是否正确？更一般地说，如果在标准 Coq 库中定义了一个构造，我应该使用它，而不是定义我自己的版本，这是真的吗？

Answer 1

你提两个问题，我尽量分开回答：

关于您的重写问题，这个问题很自然，因为 same_relation 的定义是双重包含。我同意也许使用 iff 的定义会更方便。这实际上取决于您的目标类型。您的问题的可能解决方案是定义一个视图：

Lemma L1 {A:Type} {x y:A} : rel1 x y <-> rel2 x y.
Proof.
Admitted.

Lemma L2 {A:Type} : same_relation A rel1 rel2.
Proof.
Admitted.

Lemma U {T} {R1 R2 : relation T} :
  same_relation _ R1 R2 -> forall x y, R1 x y <-> R2 x y.
Proof. now destruct 1; intros x y; split; auto. Qed.

Lemma application2 {A:Type} {x y:A} {p:Prop} :
   p /\ rel1 x y -> p /\ rel2 x y.
Proof. now rewrite (U L2). Qed.

另请注意，使用 <-> 关系重写并不是真正基于相等性，而是基于 "setoid rewriting"。事实上，以下内容在 Coq A <-> B -> A = B.

关于你的第二个问题，是否使用Coq标准库是一个很主观的话题。我个人很少使用它，我更喜欢另一个名为 math-comp 的库，但是 YMMV。关于关系，mathcomp 主要专门用于布尔关系 rel x y = x -> y -> bool，因此，等价简单地定义为相等，通常，给定 r1 r2 你会写 r1 =2 r2.

恕我直言，这样的选择在很大程度上取决于您的应用领域。

[编辑]：请注意关系库的日期为：

Naive set theory in Coq. Coq V6.1. This work was started in July 1993 by F. Prost.

所以确实，它可能不是构建 Coq 开发的最佳现代基础。

使用 'same_relation'（以及可能的其他库定义）是否会受到惩罚？

Is one being penalized by using 'same_relation' (and possibly other library definitions)?

coq