Typy indukcyjne o jednakowym indeksowaniu implikują równe wskaźniki


9

Miejmy fooindeksowany typ indukcyjny x : X.

Parameter X : Type.

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

Jestem ciekawa, jeśli to foo x = foo ysugeruje x = y. Nie mam pomysłów, jak to udowodnić.

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

Jeśli nie można tego udowodnić, dlaczego?

Odpowiedzi:


8

Nie można tego udowodnić. Rozważmy następujący szczególny przypadek twierdzenia, gdy ustawiamy X := bool:

foo true = foo false -> true = false

Biorąc to pod uwagę truei falsesą różne, gdyby twierdzenie to było możliwe do udowodnienia, powinno być możliwe wykazanie tego foo truei foo falsesą różne. Problem polega na tym, że te dwa typy są izomorficzne :

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.

W teorii Coqa nie można pokazać, że dwa typy izomorficzne są różne bez przyjęcia dodatkowych aksjomatów. Właśnie dlatego rozszerzenie teorii Coqa, takiej jak teoria typu homotopii, jest rozsądne. W HoTT można wykazać, że typy izomorficzne są równe, a gdyby można było udowodnić swoje twierdzenie, HoTT byłby niespójny.


Boli mnie głowa, ale chyba to rozumiem. Czy miałbyś odniesienie do stwierdzenia „W teorii Coqa nie można wykazać, że dwa typy izomorficzne są różne bez przyjęcia dodatkowych aksjomatów”. ?
tom

I czy można to pokazać (x <> y) -> (foo x <> foo y)? Jestem naprawdę zdezorientowany na tym świecie bez zasady wykluczonego środka.
tom

Najlepszą znaną mi referencją (choć może nie najbardziej dostępną) jest praca Hofmanna i Streichera „The Groupoid Interpretation of Theory Theory”. Jak to ujął Hofmann ( ncatlab.org/homotopytypetheory/files/HofmannDMV.pdf ), możemy mieć rozszerzenie dźwięku teorii typów Martina-Löfa, w której typy izomorficzne są równe. Ten wynik dotyczy również teorii Coqa.
Arthur Azevedo De Amorim,

I nie, nie można pokazać tego, co jest przeciwne. Kontrprzykład, który podałem z prawdą i fałszem, również przeczyłby temu stwierdzeniu.
Arthur Azevedo De Amorim,
Korzystając z naszej strony potwierdzasz, że przeczytałeś(-aś) i rozumiesz nasze zasady używania plików cookie i zasady ochrony prywatności.
Licensed under cc by-sa 3.0 with attribution required.