Чудеса пруфчекинга.
May. 6th, 2022 11:28 am![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
66georgeОпределяю некоторый тип A : Set
С разрешимым равенством eq : forall ( x y : A), {x=y} + {~x=y}
Определяю функцию примерно такую
f x y := if (eq x y) then 0 else 1
Пытаюсь доказать f x x = 0 простым вычислением.
Фиг. Оказывается, тут надо делать разбор случаев по eq x x, которое типа {x=x} + {~x=x}
Если оно типа {x=x} (доказывает x=x), то всё хорошо. А если вдруг типа {~x=x} (доказывает ~x=x), то мы получили противоречие и из него выводим что угодно!
С разрешимым равенством eq : forall ( x y : A), {x=y} + {~x=y}
Определяю функцию примерно такую
f x y := if (eq x y) then 0 else 1
Пытаюсь доказать f x x = 0 простым вычислением.
Фиг. Оказывается, тут надо делать разбор случаев по eq x x, которое типа {x=x} + {~x=x}
Если оно типа {x=x} (доказывает x=x), то всё хорошо. А если вдруг типа {~x=x} (доказывает ~x=x), то мы получили противоречие и из него выводим что угодно!
