Это не может быть доказано. Рассмотрим следующий частный случай теоремы, когда мы устанавливаем X := bool
:
foo true = foo false -> true = false
Учитывая, что true
и false
отличаются, если теорема доказуема, должно быть возможно показать, что foo true
и foo false
отличаются. Проблема в том, что эти два типа изоморфны :
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.
В теории Кока невозможно показать, что два изоморфных типа различны без допущения дополнительных аксиом. Вот почему такое расширение теории Кока, как теория гомотопического типа, является обоснованным. В HoTT можно показать, что изоморфные типы равны, и если бы можно было доказать вашу теорему, HoTT был бы несовместимым.
Артур Азеведо Де Аморим
источник
(x <> y) -> (foo x <> foo y)
? Я действительно запутался в этом мире без принципа исключенного среднего.