如何使Coq形式化可重用？

Question

我正在研究算法的Coq形式化。但是這種算法的組件（一些函數和引理）可以在不同類型上「重載」（按Haskell的意義）。

我的意圖是避免代碼重複。我知道Coq有模塊（如ML）和類型類（如Haskell）。什麼是實現引理和函數定義的可重用性的最佳方式，它可以在不同類型上進行參數化？

Answer 1

避免使用Coq模塊執行除命名空間或定義不透明之外的任何操作。依賴記錄（類型類背後的基本特徵）優於編寫參數定義的模塊，因爲它們是可以通過適用於Coq中其他對象的相同規則操縱的第一類對象。也就是說，當將Coq代碼提取到OCaml中時，Coq模塊被提取到OCaml模塊中，而依賴記錄依靠巧妙的記錄正常工作。因此，如果你關心解壓縮到OCaml中，並且關心與提取的代碼的接口，模塊可能是更好的選擇。

類型類是一種構建在依賴記錄之上的功能，通過添加自動實例推斷來使它們更易於使用。不幸的是，Coq中的類型實例推理並不是非常強大，需要你調整你的實例或者手動提供它們以便在實踐中使用它們 - 無論如何，它們肯定比Haskell的同類產品更難使用 - 並且也會延緩編譯時間。 MathClasses庫在很大程度上依賴於類型類來定義數學結構，並且它似乎對它們很好。

還有一個叫做規範結構的特徵，它也是基於依賴記錄，完成或多或少與類型類相同，但是有一個稍微不同的編程模型和推理引擎。在某些情況下，他們的工作比打字班要好，但在其他人中更難使用。例如，Ssreflect庫廣泛使用它們。

有一個關於使用模塊或記錄here的小討論。