Coq 如何漂亮地打印使用策略构造的术语？

Question

我是 Coq 的新手，正在做一些练习以更加熟悉它。

我的理解是，在 Coq 中证明一个命题 "really" 就是在 Gallina 中写下一个类型，然后使用策略以确定性的方式将术语组合在一起来证明它存在。

我想知道是否有一种方法可以获得实际术语的漂亮印刷表示，并删除所有策略。

在下面的示例中，最终生成了一个 plus_comm (x y : N) : plus x y = plus y x 类型的匿名术语……我认为。想看怎么办？从某种意义上说，我很好奇"desugar"的战术是什么。

这是有问题的代码，基本上是从 YouTube 上的教程中逐字提取的 https://www.youtube.com/watch?v=OaIn7g8BAIc。

Inductive N : Type :=
| O : N
| S : N -> N
.

Fixpoint plus (x y : N) : N :=
match x with
| O => y
| S x' => S (plus x' y)
end.

Lemma plus_0 (x : N) : plus x O = x.

Proof.
  induction x.
  - simpl. reflexivity.
  - simpl. rewrite IHx. reflexivity.
Qed.

Lemma plus_S (x y : N) : plus x (S y) = S(plus x y).

Proof.
  induction x.
  - simpl. reflexivity.
  - simpl. rewrite IHx. reflexivity.
Qed.


Lemma plus_comm (x y : N) : plus x y = plus y x.

Proof.
  induction x.
  - simpl. rewrite plus_0. reflexivity.
  - simpl. rewrite IHx. rewrite plus_S. reflexivity.
Qed.

Answer 1

首先，plus_comm是不是类型的一部分。你得到一个术语 named plus_comm 类型 forall x y : N, plus x y = plus y x. 你可以使用以下命令检查它

Check plus_comm.

因此，另一种定义 plus_comm 引理的方法是

Lemma plus_comm : forall x y : N, plus x y = plus y x.

附带说明：在这种情况下，您需要在 Proof. 部分之后添加 intros x y.（或只是 intros.）。

策略（以及将它们粘合在一起的方法）是一种称为 Ltac 的元语言，因为它们用于生成另一种语言的术语，称为 Gallina，它是 Coq 的规范语言。

例如forall x y : N, plus x y = plus y x是Gallina语句的一个实例，也是plus函数的主体。要获取附加到 plus_comm 的术语，请使用 Print 命令：

Print plus_comm.

plus_comm = 
fun x y : N =>
N_ind (fun x0 : N => plus x0 y = plus y x0)
  (eq_ind_r (fun n : N => y = n) eq_refl (plus_0 y))
  (fun (x0 : N) (IHx : plus x0 y = plus y x0) =>
   eq_ind_r (fun n : N => S n = plus y (S x0))
     (eq_ind_r (fun n : N => S (plus y x0) = n) eq_refl (plus_S y x0))
     IHx) x
     : forall x y : N, plus x y = plus y x

这本书读起来并不容易，但只要有一些经验，你就能理解它。

顺便说一下，这里是我们如何在不使用策略的情况下证明引理的：

Definition plus_comm : forall x y : N, plus x y = plus y x :=
  fix IH (x y : N) :=
    match x return plus x y = plus y x with
    | O => eq_sym (plus_0 y)
    | S x => eq_ind _ (fun p => S p = plus y (S x)) (eq_sym (plus_S y x)) _ (eq_sym (IH x y))
    end.

说明几点：fix是定义递归函数的手段，eq_sym是用来把x = y变成y = x，eq_ind对应于rewrite策略。

Coq 如何漂亮地打印使用策略构造的术语？

Coq how to pretty-print a term constructed using tactics?

coq