如何定义自动可展开的定义

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

有几种方法可以完成你的要求,这里是我所知道的解释:

1. 使用缩写.引用参考手册:

   的缩写是一个名称,可能施加到参数,即表示一个(可能)更复杂的表达式.

   [...]

   缩写与普通定义绑定为绝对名称,并且它们也可以由限定名称引用.

   缩写在语法上是句法的,它们与缩写定义时但不是在使用时键入的表达式绑定在一起.

在你的情况下,这将是

Notation g t := (f t one).

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

2. 使用setoid_rewrite.Coq的setoid_rewrite策略类似于rewrite,除了它寻找模数δ(展开)的事件,可以在粘合剂下重写,以及一些其他小事.

对于您的示例,这是:

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

3. 在某些情况下,你可以使用Set Keyed Unification和Declare Equivalent Keys,虽然这在你的情况下不起作用(我在GitHub上打开了一个问题.这告诉rewrite"展开"一个头部常数到另一个,虽然它显然不够好到处理您的案例.有关相关提交消息的文档,以及添加适当文档的未解决问题.

这是一个有用的例子:

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.