Sind Pfeile in Coq Aliase von universellen Quantifizierungen?

Question

Ich lese chapter 4 of the reference manual of Coq. Gemäß den in der Referenz beschriebenen Schreibregeln lautet die Art des Ausdrucks fun x: nat => xforall x: nat, nat.

Assume that E is [nat: Set]. 

       ...         ... 
------------------------------ Prod-Set ------------------- Var 
E[] ⊢ forall x: nat, nat : Set   E[x: nat] ⊢ x : nat 
------------------------------------------------------------ Lam 
     E[] ⊢ fun x: nat => x : forall x: nat, nat 

Allerdings, wenn ich Check dieser Begriff von Coq, es nat -> nat eingegeben wird.

Welcome to Coq 8.5pl2 (July 2016) 

Coq < Check fun x: nat => x. 
fun x : nat => x 
    : nat -> nat 

Sind diese beiden Typen die gleichen? Wenn ja, haben Pfeile verborgene Namen gebundener Variablen?

Answer 1

Der tatsächliche Typ von fun x: nat => x ist nat -> nat, weil ihre Art nicht abhängig ist. Der Pfeil ist Syntaxzucker für forall _:nat, nat: der Typ des Körpers hängt nicht von dem Wert x ab, nur der Körper selbst verwendet x. Ein Beispiel für die Typabhängigkeit wäre vector.

vector A n ist der Typ der Liste der Länge n mit Elementen des Typs A. Lassen Sie uns die concat Funktion betrachten, die zwei Vektoren verketten:

concat : forall n m: nat, vector n A -> vector m A -> vector (n + m) A 

als Eingabe zwei ganzen Zahlen nimmt, n und m, zwei Vektoren der jeweiligen Größe n und m und sie verketten. Diesmal hängt der Typconcat von dem Wert n und m ab, also müssen Sie sie benennen und die forall anstelle der -> verwenden. Wenn Sie versuchen, nat -> nat -> vector n A -> ... zu schreiben, wird die Variable n nicht korrekt begrenzt.

Answer 2

Wie andere gesagt haben, Pfeil ist in der Tat eine Notation finden Sie unter: https://github.com/coq/coq/blob/trunk/theories/Init/Logic.v#L13

Diese Datei wird vom Prelude geladen wird, können Sie es mit mit -noinit vermeiden können.