Coq如何漂亮地打印使用策略構造的術語？

Question

我是Coq的新手，正在做一些練習，以便更熟悉它。

我的理解是，在證明勒柯克命題「真」是寫下來加利納一個類型，然後顯示出它的使用戰術方面確定性的方式結合在一起居住。

我不知道是否有一種方式來獲得實際刑期的一個漂亮的印刷表示，所有的戰術中刪除。

在下面，plus_comm (x y : N) : plus x y = plus y x類型的匿名術語最終產生的例子。我想。如果我想看看，我應該怎麼做？從某種意義上說，我很好奇什麼策略「脫鉤」。

這裏是有問題的代碼，在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是不類型的一部分。你得到了一個名爲類型forall x y : N, plus x y = plus y x.您可以使用下面的命令

檢查它的 plus_comm長期

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策略。