coq - 如何定义一个自动展开的定义

Question

我有时想为现有函数定义一些快捷方式，如下例所示:

Parameter T : Set.
Parameter zero one: T.
Parameter f : T -> T -> option T.
Hypothesis f_unit : forall t, f zero t = None.

Definition g (t : T) := f t one.

然而，这个定义似乎很抽象，因为我不能使用关于 f 的定理。在 g 的实例上没有首先展开:

Goal (g zero = None).
  unfold g.
  rewrite f_unit.
  reflexivity.
Qed.

有没有办法将定义标记为自动展开？

Answer 1

有几种方法可以完成您的要求，以下是对我所知道的方法的解释:

使用缩写。报价 the reference manual :

An abbreviation is a name, possibly applied to arguments, that denotes a (presumably) more complex expression.

[...]

Abbreviations are bound to an absolute name as an ordinary definition is, and they can be referred by qualified names too.

Abbreviations are syntactic in the sense that they are bound to expressions which are not typed at the time of the definition of the abbreviation but at the time it is used.

在你的情况下，这将是

Notation g t := (f t one).

这很像 Daniel Schepler 对 Notation 的建议。 , 除了它不保留 g作为全局关键字。

使用 setoid_rewrite . Coq's setoid_rewrite战术类似于rewrite ，除了它寻找模δ(展开)的出现，可以在活页夹下重写，以及其他一些小东西。

对于您的示例，这是:

Require Import Coq.Setoids.Setoid.
Goal (g zero = None).
Proof.
  setoid_rewrite f_unit.
  reflexivity.
Qed.

在某些情况下，您可以使用 Set Keyed Unification和 Declare Equivalent Keys ，虽然这在你的情况下不起作用(我已经打开了一个问题 on GitHub here 。这告诉 rewrite 将一个头部常量“展开”到另一个，尽管它显然不足以处理你的案例。有一些文档 on the relevant commit message 和一个 open issue to add proper documentation .

这是一个有用的示例:

Parameter T : Set.
Parameter zero one: T.
Parameter f : T -> T -> option T.
Hypothesis f_unit : forall t, f zero t = None.

Definition g := f zero zero.

Set Keyed Unification.
Goal (g = None).
Proof.
  Fail rewrite f_unit.
  Declare Equivalent Keys g f.
  rewrite f_unit.
  reflexivity.
Qed.