Развертывание доказательства в Coq

Question

Интересно, есть ли способ получить доказательство (сериализован через 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. Или менее наивный (и менее идеальный из-за изменения языка, представляющего собой доказательство), путем извлечения программы.

Answer 1

Я не уверен, что есть прямой способ сделать это, но реализовать его было бы непросто, на непрозрачности этого уровня просто флаг и его можно обойти.

Однако, интересно, чего вы хотите достичь?

Обратите внимание, что большинство доказанных условий, полученных таким образом, будут просто неуправляемыми, особенно разворачивание быстро приведет к ухудшению экспоненциального размера.