在Coq中展開證明術語

我不知道是否有辦法在超出當前上下文的某個級別（或者僅僅是基元）上獲取證明術語（通過Print序列化）。例如，執行下面的在Coq中展開證明術語

From mathcomp Require Import odd_order.PFsection14. 
Print Feit_Thompson.

導致

Feit_Thompson = 
fun (gT : fingroup.FinGroup.type) 
    (G : fingroup.group_of (gT:=gT) 
     (ssreflect.Phant 
      (fingroup.FinGroup.arg_sort 
       (fingroup.FinGroup.base gT)))) => 
BGsection7.minSimpleOdd_ind no_minSimple_odd_group (gT:=gT) 
    (G:=G) 
    : forall (gT : fingroup.FinGroup.type) 
     (G : fingroup.group_of (gT:=gT) 
       (ssreflect.Phant 
        (fingroup.FinGroup.arg_sort 
         (fingroup.FinGroup.base gT)))), 
     is_true 
     (ssrnat.odd 
      (fintype.CardDef.card 
       (T:=fingroup.FinGroup.arg_finType 
        (fingroup.FinGroup.base gT)) 
       (ssrbool.mem 
        (finset.SetDef.pred_of_set 
        (fingroup.gval G))))) -> 
     is_true (nilpotent.solvable (fingroup.gval G))

但我想展開標識符在證明中使用的術語如no_minSimple_odd_group其證明術語（定理和定義）。我懷疑定理和引理的不透明性可能會造成這個目的的障礙。

我想到的天真的解決方案是通過Print遞歸查詢每個標識符。或者由於程序提取而導致不那麼天真（由於表示證明術語的語言改變而不太理想）解決方案。

來源

2016-11-08 Falcon

'打印所有相關性Feit_Thompson.'是否有幫助？ –

對於遞歸打印（我的天真解決方案）肯定有幫助，但我不認爲這本身會顯示證明術語（lambda術語）。 – Falcon

你可能會發現[this]（https://sympa.inria.fr/sympa/arc/coq-club/2016-11/msg00062.html）coq-club的線程有用。他們提到[template-coq]（https://github.com/gmalecha/template-coq）插件。 –

我不確定是否有直接的方式做到這一點，但實現起來並不難，在此級別上，不透明度只是一個標誌，可以繞過。

但是，我想知道你想達到什麼目的？

請注意，以這種方式獲得的大多數證明術語將會難以管理，特別是展開會很快導致比指數大小的爆炸更糟。

來源

2016-11-08 13:47:04 ejgallego

是的，它們可能非常大，取決於展開停止的常量集合，但是我希望能夠在給定不同基元集（常量）的情況下檢查相同的證明術語。 – Falcon

快速瀏覽之後，我幾乎可以肯定，如果您需要此功能，您將不得不編寫一個擴展「Eval red」策略的插件來展現更多內容。 – ejgallego

感謝您的指針。我很好奇以編程方式與Coq進行交互（作爲OCaml庫？）。你能建議一些參考嗎？ – Falcon

在Coq中展開證明術語

回答

相關問題