Если у меня есть такая общая установка, как следующая, как я могу доказать, что утверждаю (f a)?
A : Type
f : A -> Prop
a : A
...
============================
f a
В частности, почему я не могу использовать любую из этих тактик и что означают ошибки?
specialize (f a).
Error: Cannot change f, it is used in conclusion.
apply (f a).
Unable to unify "Prop" with "f a".
Вы не можете специализироваться f, потому что это используется в заключении, то есть в цели. specalize (f a) заменяет вашу гипотезу f ее прикладной версией. Если мы забудем о цели, то потом вы получите f : Prop. Однако, поскольку f появляется в цели, вам не разрешается изменять его значение.
Также f a является предложением, а не доказательством самого f a! Тот факт, что он назван f, не означает, что это не предикат.
f a- это утверждение, которое необходимо доказать. Это не доказательство самого себя! Например. приговор Сегодня пошел банановый дождь. - грамматически правильное предложение, но на самом деле оно неверно. - person HTNW schedule 02.05.2020