Coq: Prouver une application

Question

C'est une question un peu théorique. Nous pouvons définir fx mais apparemment pas 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. 

D'une certaine manière, cela a du sens, comme on ne peut pas prouver de la f et x que f a été (ou sera) appliquée à x. Mais nous pouvons appliquer f-x pour obtenir quelque chose du type Type:

assert (h := f x). 

Cela semble déroutante: on peut appliquer f-x mais encore ne peut pas obtenir un témoin y: f x qu'il a fait.

La seule explication que je peux penser est la suivante: en tant que type, f x est une application, en tant que terme, c'est juste un type. Nous ne pouvons pas déduire une application passée d'un type; De même, nous ne pouvons pas déduire une application future d'une fonction et son argument potentiel. Quant à l'application de soi, ce n'est pas une étape dans une preuve, nous ne pouvons donc pas en avoir le témoignage. Mais je devine juste. La question:

Est-il possible de définir fx'? Si oui, comment? si non, pourquoi (s'il vous plaît donner une explication théorique)

Answer 1

D'abord, une réponse directe à votre question: pas, il est impossible de définir fx'. Selon votre extrait, fx' devrait avoir le type

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

Il est pas difficile de voir que l'existence de fx' implique une contradiction, comme le script suivant.

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. 

Que s'est-il passé ici? Le type de fx' indique que pour toute famille de types f indexée par un type A, nous pouvons produire un élément de f x, où x est arbitraire. En particulier, nous pouvons prendre f pour être une famille constante de types (fun x => False), auquel cas f x est la même chose que False. (Notez que False, en plus d'être membre de Prop, est également membre du Type.)

Maintenant, compte tenu de votre question, je pense que vous êtes un peu confus par la signification des types et des propositions en Coq. Vous avez dit:

Cela semble déroutante: on peut appliquer f-x mais ne peut toujours pas obtenir un témoin y: f x qu'il a fait.

Le fait que nous pouvons appliquer f-x signifie simplement que l'expression f x a un type valide, ce qui, dans ce cas, est Type. En d'autres termes, Coq montre que f x : Type.Mais avoir un type est une chose différente d'être habité: lorsque f et sont arbitraires, il n'est pas possible de construire un terme y tel que y : f x. En particulier, nous avons False : Type, mais il est impossible de construire un terme p avec p : False, car cela signifierait que la logique de Coq est incohérente.