Есть несколько проблем с этим доказательством. Во-первых, вы неправильно поняли, что хотел Кок; фактическая цель была следующей:
((true && false) = true) -> (false = true)
Это не сопровождается рефлексивностью, поскольку вывод этой формулы, false = true, является равенством между двумя синтаксически различными выражениями.
Во-вторых, Coq не упрощает операторы -> и = так, как вы описали. Теория Кока позволяет автоматическое упрощение в нескольких выбранных выражениях, таких как те, которые определены анализом случая Например, && является синтаксическим сахаром для функции andb, которая определена в стандартной библиотеке следующим образом:
Definition andb b c :=
if b then c else false.
Когда Coq видит выражение, такое как false && true, оно расширяет его до эквивалентного if false then true else false, что, в свою очередь, упрощает ветвь else true. Вы можете проверить это, вызвав тактику simpl на проблемной ветке.
Операторы -> и =, с другой стороны, определены по-разному: первый является примитивом в логике, тогда как другой является так называемым индуктивным высказыванием. Ни один из них не может быть автоматически упрощен в Coq, потому что они выражают понятия, которые, как правило, не являются вычислимыми: например, мы можем использовать =, чтобы выразить равенство двух функций f и g, которые принимают бесконечное число натуральных чисел в качестве входных данных. Этот вопрос обсуждает эту разницу более подробно.
Если хотите, вы можете сформулировать свою теорему чисто вычислимым образом с альтернативными определениями импликации и равенства:
Definition negb b := if b then false else true.
Definition eqb b c := if b then c else negb c.
Definition implb b c := if b then c else true.
Lemma test : forall b c, (implb (eqb (andb b c) true) (eqb c true))
= true.
Proof. intros [] []; reflexivity. Qed.
Однако такое утверждение, как правило, труднее использовать в Coq.