Des types inductifs indexés égaux impliquent des indices égaux

9

Ayons un type inductif fooindexé par x : X.

Parameter X : Type.

Inductive foo : X -> Type :=
| constr : forall (x : X), foo x.

Je suis curieux, si cela foo x = foo yimplique x = y. Je n'ai plus d'idées pour prouver cela.

Lemma type_equality_implies_index_equality : forall (x y : X), foo x = foo y -> x = y.

Si cela ne peut pas être prouvé, pourquoi?

coq à M
la source

Réponses:

8

Cela ne peut pas être prouvé. Considérons le cas spécial suivant du théorème, lorsque nous posons X := bool:

foo true = foo false -> true = false

Étant donné que trueet falsesont différents, si le théorème était prouvable, il devrait être possible de le montrer foo trueet foo falsesont différents. Le problème est que ces deux types sont isomorphes :

Inductive foo : bool -> Type :=
| constr : forall (x : bool), foo x.

(* An isomorphism between foo true and foo false *)
Definition foo_t_f (x : foo true) : foo false := constr false.
Definition foo_f_t (x : foo false) : foo true := constr true.

(* Proofs that the functions are inverses of each other *)
Lemma foo_t_fK x : foo_f_t (foo_t_f x) = x.
Proof. unfold foo_f_t, foo_t_f. now destruct x. Qed.

Lemma foo_f_tK x : foo_t_f (foo_f_t x) = x.
Proof. unfold foo_f_t, foo_t_f. now destruct x. Qed.

Dans la théorie de Coq, il n'est pas possible de montrer que deux types isomorphes sont différents sans supposer des axiomes supplémentaires. C'est pourquoi une extension de la théorie de Coq telle que la théorie du type d'homotopie est valable. Dans HoTT, on peut montrer que les types isomorphes sont égaux, et s'il était possible de prouver votre théorème, HoTT serait incohérent.

Arthur Azevedo De Amorim
la source
Ma tête me fait mal, mais je pense que je comprends. Auriez-vous une référence pour l'énoncé "Dans la théorie de Coq, il n'est pas possible de montrer que deux types isomorphes sont différents sans supposer des axiomes supplémentaires." ?
Tom
Et est-il possible de montrer (x <> y) -> (foo x <> foo y)? Je suis vraiment confus dans ce monde sans principe de milieu exclu.
Tom
La meilleure référence que je connaisse (mais peut-être pas la plus accessible) est l'article de Hofmann et Streicher "L'interprétation Groupoïde de la théorie des types". Comme le dit Hofmann ( ncatlab.org/homotopytypetheory/files/HofmannDMV.pdf ), nous pouvons avoir une extension solide de la théorie des types de Martin-Löf où les types isomorphes sont égaux. Ce résultat s'applique également à la théorie de Coq.
Arthur Azevedo De Amorim
Et non, il n'est pas possible de montrer le contrapositif. Le contre-exemple que j'ai donné avec vrai et faux contredirait également cette affirmation.
Arthur Azevedo De Amorim