在 Coq 中展开嵌套定义

Question

我正在使用 Coq 中的 math-类库。这个库巧妙地使用类型类来重载符号，就像这样。

(* From math-classes *)
Class Equiv A := equiv : relation A.
Infix "=" := equiv : type_scope.

(* My code *)
Definition MyDataType : Type := ...
Definition MyEquality (x y : MyDataType) : Prop := ...
Instance MyEq_equiv : Equiv MyDataType := MyEquality.

我可以为许多不同的数据类型定义这样的实例，x = y 可以理解为我注册的x和y类型的相等性，感谢实例解析机制

然而，在证明中处理这些等式有点烦人，因为我必须 unfold 许多连续的定义：

Lemma MyEquality_refl : forall x : MyDataType, x = x.
Proof.
   intro.
   unfold equiv, MyEq_equiv, MyEquality.
   ...
Qed.

有没有更有效的方法unfold？

Answer 1

(1) 您可以使用自定义策略：

(* unfolds only in the goal *)
Ltac unfold_equiv := unfold equiv, MyEq_equiv, MyEquality.

(* unfolds in the goal and in the context *)
Ltac unfold_equiv_everywhere := unfold equiv, MyEq_equiv, MyEquality in *.

Lemma MyEquality_refl : forall x : MyDataType, x = x.
Proof.
   intro.
   unfold_equiv.    (* or `unfold_equiv_everywhere.` *)
   ...
Qed.

(2) 您可以使用提示数据库。只需将 Hint Unfold 的定义添加到数据库中即可。

Hint Unfold equiv MyEq_equiv MyEquality.

(* a couple more convenient pseudonyms *)
Ltac unfold_selected := repeat autounfold with *.
Ltac unfold_selected_everywhere := repeat autounfold with * in *.

Lemma MyEquality_refl : forall x : MyDataType, x = x.
Proof.
   intro.
   unfold_selected. (* or just literally `repeat autounfold with *.` *)
   ...
Qed.

在 Coq 中展开嵌套定义

Unfolding nested definitions in Coq

typeclass

coq