coq - 在 Coq 中展开证明项

我想知道是否有一种方法可以在当前上下文之外的某个级别(或仅到原语)获得证明项(是否通过 Print 序列化)。例如，执行以下

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 递归查询每个标识符。或者通过程序提取的不那么幼稚(并且由于表示证明项的语言发生变化而不太理想)的解决方案。

最佳答案

我不确定是否有直接的方法可以做到这一点，但实现起来并不难，在这个级别上，不透明度只是一个标志，可以绕过。

但是，我想知道您想实现什么目标？

请注意，以这种方式获得的大多数证明项都将是难以管理的，特别是展开将很快导致比指数规模膨胀更糟糕的情况。

关于coq - 在 Coq 中展开证明项，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/40477368/