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:
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.
(x <> y) -> (foo x <> foo y)? Jestem naprawdę zdezorientowany na tym świecie bez zasady wykluczonego środka.