Coq: Eine Anwendung testen

Question

Dies ist ein bisschen theoretische Frage. Wir können fx definieren, aber scheinbar nicht fx':

Function fx {A} (x:A) (f:A->Type) (g:Type->f x): f x := g (f x). 
Definition fx' {A} (x:A) (f:A->Type): f x. 

In gewisser Weise macht den Sinn, da man nicht von den f beweisen kann und x dass f wurde (oder wird), die auf x. Aber wir können f-x gelten etwas vom Typ zu bekommen Type:

assert (h := f x). 

Dies scheint rätselhaft: ein f-x anwenden können aber noch kann kein Zeugnis erhalten y: f x, dass er so getan hat.

Die einzige Erklärung, die ich mir vorstellen kann, ist: als eine Art, f x ist eine Anwendung, als ein Begriff, es ist nur ein Typ. Wir können keine frühere Anwendung von einem Typ ableiten; In ähnlicher Weise können wir aus einer Funktion und ihrem möglichen Argument nicht auf eine zukünftige Anwendung schließen. Was das Anwenden betrifft, ist es keine Stufe in einem Beweis, so dass wir kein Zeugnis davon haben können. Aber ich rate nur. Die Frage:

Ist es möglich, fx' zu definieren? Wenn ja, wie; wenn nein, warum (bitte eine theoretische Erklärung geben)

Answer 1

Erstens eine direkte Antwort auf Ihre Frage: keine, ist es nicht möglich fx' zu definieren. Entsprechend Ihrem Snippet sollte, fx' haben Typ

forall (A : Type) (x : A) (f : A -> Type), f x. 

Es ist nicht schwer zu sehen, dass die Existenz von fx' einen Widerspruch impliziert, wie das folgende Skript zeigt.

Section Contra. 

Variable fx' : forall (A : Type) (x : A) (f : A -> Type), f x. 

Lemma contra : False. 
Proof. 
    exact (fx' unit tt (fun x => False)). 
Qed. 

End Contra. 

Was ist hier passiert? Der Typ fx' besagt, dass wir für jede Familie von Typen f, die durch einen Typ A indiziert sind, ein Element f x erzeugen können, wobei x beliebig ist. Insbesondere können wir f zu einer konstanten Familie von Typen (fun x => False) nehmen, in welchem ​​Fall f x das Gleiche ist wie False. (Beachten Sie, dass False, abgesehen davon, daß ein Mitglied der Prop, ist auch ein Mitglied der Type.)

, nun Ihre Frage gegeben, ich glaube, Sie sind leicht durch die Bedeutung von Typen und Sätze in Coq verwirrt. Sie sagte:

Dies scheint rätselhaft: ein f-x anwenden können aber nach wie vor keinen Zeuge erhalten y: f x, dass er so getan hat.

Die Tatsache, dass wir anwenden können, bedeutet f-x einfach, dass der Ausdruck f x einen gültigen Typen hat, die in diesem Fall Type ist. Mit anderen Worten, Coq zeigt das f x : Type.Aber mit einem Typ ist eine andere Sache als bewohnt: wenn f und x sind beliebig, ist es nicht möglich, einen Begriff y so zu bauen, dass y : f x. Insbesondere haben wir False : Type, aber es gibt keine Möglichkeit, einen Begriff mit p : False zu bauen, weil das bedeuten würde, dass die Logik von Coq inkonsistent ist.