Entpacken eines Beweisbegriffs in Coq

Question

Ich frage mich, ob es eine Möglichkeit gibt, den Beweis Begriff (serialisiert über Print oder nicht) auf einer Ebene über den aktuellen Kontext (oder nur auf Primitiven) zu erhalten. Zum Beispiel Ausführen der folgenden

From mathcomp Require Import odd_order.PFsection14. 
Print Feit_Thompson. 

Ergebnisse in

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)) 

aber ich mag die Kennungen (Theoreme und Definitionen) im Beweis Begriff wie no_minSimple_odd_group ihren Beweis verwendete Begriffe entfalten. Ich vermute, dass die Undurchsichtigkeit von Theoremen und Lemmas ein Hindernis für diesen Zweck darstellen könnte.

Die naive Lösung, die ich mir vorstellen kann, ist die rekursive Abfrage jeder Kennung über Print. Oder eine weniger naive (und weniger ideal wegen der Änderung der Sprache, die den Beweis Begriff darstellt) Lösung, über Programm-Extraktion.

Answer 1

Ich bin mir nicht sicher, ob es einen direkten Weg gibt, aber es wäre nicht zu schwer zu implementieren, auf dieser Ebene ist die Deckkraft nur ein Flag und kann umgangen werden.

Allerdings frage ich mich, was Sie erreichen möchten?

Beachten Sie, dass die meisten Beweisbeweise, die auf diese Weise erhalten werden, nur schwer zu handhaben sind, besonders das Entfalten führt schnell zu einem schlechteren Exponentialgrößenauftrieb.