Coq: Zeige alle Begriffe in einem Typ oder Typen in einem Universum in der Umgebung

Question

Gibt es eine Möglichkeit, alle Begriffe in einem Typ oder alle Typen in einem Universum in der Umgebung anzuzeigen?

Print Set. (*Syntax error: 'Firstorder' 'Solver' expected after 'Print' (in [vernac:command]).*) 

Answer 1

Nein, es gibt keine solche Funktionalität in Coq. Print wird nur den Körper des gegebenen Begriffs angezeigt werden, zum Beispiel:

Print plus. 
plus = 
fix plus (n m : nat) {struct n} : nat := 
    match n with 
    | 0 => m 
    | S p => S (plus p m) 
    end 
    : nat -> nat -> nat 

Argument scopes are [nat_scope nat_scope] 

Answer 2

Die folgende benutzerdefinierte Taktik genau dies tun kann, wenn sie von Umgebung, die Sie den Beweis Umwelt bedeuten.

Ltac printInType t := 
    match goal with 
    | [ H : t |- _ ] => 
     idtac H; fail 
    | _ => idtac 
    end 
. 

Theorem test : forall n m, n + m = m + n. 
Proof. 
    intros. 
    printInType nat. 
    (* prints in the Message window: 
    m 
    n 
    *) 
    printInType Set. 
    (* prints nothing 
    because nat for instance is not explicitely in the proof environment *) 

Was es tut genau das ist es durch den Beweis Umwelt geht und findet eine Hypothese oder eine Variable, die das Argument Typ t hat. idtac H druckt es, dann scheitert der Zweig wegen der fail Taktik. Jetzt versucht Coq wieder den gleichen Zweig auf einer anderen Hypothese/Variable, folglich werden alle solche Hypothesen/Variablen am Ende gedruckt. Jetzt ist der zweite Zweig | _ => idtac nur um sicherzustellen, dass die Taktik schließlich erfolgreich ist. Wenn dieser Zweig nicht vorhanden wäre, würde die Taktik mit einem Fehler fehlschlagen und beim Drucken des Fehlers würde Coq die zuvor gedruckten Informationen löschen.

Answer 3

Sie können die Suche nach einer Annäherung dazu verwenden. Sie tun können:

Search $Type. 

und bekommen Ergebnisse mit Typ $Type. Zum Beispiel

Search nat -(forall _, _). 

zeigt alle Bedingungen des Typs nat.

Search Set -(forall _, _). 

Zeigt alle nicht funktionalen Terme des Typs Set an. SearchPattern sollte ähnliche Funktionalität bieten, aber ich bin mir nicht sicher. Ssreflect Suche kann das und mehr tun.