Coq學習筆記11：策略和證明自動化

目錄：類型論驛站寫作計劃

上一篇：Coq學習筆記10：歸納數據結構-2

下一篇：Coq學習筆記12：歸納謂詞

這份筆記對應的是 CoqArt法文版 的第八章。

I. 歸納類型的策略（les tactiques des types inductifs）

已經學過的策略回顧：

• ：進行分類處理
• ：進行轉換
• ：進行歸納推理
• ：核實構造子構造的項是不同的，以及是單射的

分類討論和遞歸策略：

• ：通常等同於
• ：和 的關係類似 與 的關係。

轉換策略：

• ： 只能歸約；而 可以做任何轉換，但需要用戶提供新的聲明
• ：惰性求值，可以規定所需的轉換
• ：參數歸約先於函數，與 相反
• ：歸約 形式的表達式
• ：歸約常量和函數的定義，可以攜帶參數，參數是需要歸約的對象
• ：歸約分類和遞歸函數
• ：歸約 形式的表達式

自動化策略：

• ：使用初始環境提供的
• ：使用
• ，為 提供提示，使用時應將 做為 的參數
• ：語法和 一致，但搜尋範圍更廣

數值策略：

• ：適用於環
• ：適用於線性等式和不等式
• ：適用於除環/域
• ：和 功能相似，但適用於實數

命題邏輯決策過程：

• ：直覺主義命題邏輯自動化判定
• ：作用等同於 再加上一個 無法取代的策略

II. 策略定義語言 （le langage de définition de tactiques）

參數的聯繫：

Ltac autoClear h := try (clear h; auto with arith; fail).

以策略為參數：

Ltac autoAfter tac := try (tac; auto with arith; fail).

遞歸策略：

Ltac le_S_star := apply le_n || (apply le_S; le_S_star).

分類構造：

Ltac check_not_divides := match goal with | [ |- (~divides ?X1 ?X2) ] ) cut (X1 <= X2);[ idtac | le_S_star ]; intros Hle; rewrite (le_plus_minus _ _ Hle); apply not_divides_plus; simpl; clear Hle; check_not_divides | [ |- _ ] ) apply not_divides_lt; unfold lt; le_S_starend.

使用假設名稱：

Ltac contrapose H := match goal with | [id:(~_) |- (~_) ] ) intro H; apply id end.

和歸約的互動：

Ltac simpl_on e := let v := eval simpl in e in match goal with | [ |- context [e] ] ) replace e with v; [idtac | auto] end.

目錄：類型論驛站寫作計劃

上一篇：Coq學習筆記10：歸納數據結構-2

下一篇：Coq學習筆記12：歸納謂詞

推薦閱讀：