Почему Кок не принимает эту лемму в качестве подсказки?Лемма не может использоваться в качестве подсказки
Lemma contr : forall p1 : Prop, False -> p1.
Proof. tauto. Qed.
Hint Resolve contr : Hints.
Или другие Леммы, которые заканчиваются с Prop переменной?
Глядя на документацию для Hint Resolve (http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#@command232):
term cannot be used as a hint
The type of term contains products over variables which do not appear in the conclusion. A typical example is a transitivity axiom. In that case the apply tactic fails, and thus is useless.
Однако, это не кажется (мне), чтобы быть в данном случае, как только продукт через p1 который появляется в заключении ,
Проблема здесь в том, что ваш вывод абсолютно не имеет формы. auto, похоже, работает, сопоставляя форму вашей цели с формой возвращаемого типа базы данных подсказок. Здесь это может быть расстроено тем фактом, что ваша цель - это просто количественная переменная. Я не уверен, что это разумная вещь для поездки, но этот конкретный случай может быть единственным случаем, когда у вас может быть такой бесформенный тип возврата (с тем же случаем для Set и Type), так что это не большая сделка ,
Таким образом, вы, вероятно, не нужно это как намек? ... просто использовать тактику, такие как tauto, intuition или выполнять какие-либо устранение/уничтожение/инверсии на значение типа False в среде ... не очень удовлетворительно, но eh: \