Доказательство упрощением

Итак, в предыдущих частях мы определили новые типы данных и функции над ними. Настало время обратиться к вопросу о том, как сформулировать и доказать их свойства и поведение. В некотором смысле мы уже начали делать это – в первой части мы написали своего рода юнит-тест, используя ключевое слово Example, который содержал некоторые утверждения о поведении некоторой функции, применяемой к определенному набору аргументов. Используя определение функции, Coq упрощает выражение и проверяет на равенство его левую и правую часть.

Подобного рода доказательства могут быть использованы для довольно широкого круга задач. Покажем, что 0 является нейтральным элементом для операции сложения слева:

 Theorem plus_O_n : forall n : nat, 0 + n = n. Proof.   simpl. reflexivity. Qed. 

Команда reflexivity неявно упрощает обе стороны выражения перед сравнением.

Ключевые слова simpl и reflexivity являются примерами тактик. Главная цель тактики – подсказать Coq каким образом следует проверить корректность нужных утверждений. Существует довольно узкий круг задач, корректность которых может быть доказана автоматически. Докажем, что 2 + 2 = 4:

 Coq < Lemma using_auto: 2 + 2 = 4. 1 subgoal      ============================    2 + 2 = 4  using_auto < Proof. auto. Qed.  Proof completed.  auto.  using_auto is defined 

В подавляющем большинстве случаев необходимо использовать тактики.

Тактика intros

Помимо юнит-тестов, которые применяют функции к набору аргументов, мы будем заинтересованы в доказательстве свойств программ, формулировка которых содержит математические кванторы (например, «для всех натуральных чисел n») и гипотезы (например, «пусть a = b»). Тактика intros позволяет перенести кванторы и гипотезы из утверждения в контекст текущих рассуждений. Докажем, что результатом умножения слева любого натурального числа на нуль является нуль:

 Theorem mult_zero: forall n : nat, 0 * n = 0. Proof. intros n. reflexivity. Qed. 

Доказательство перезаписью

Рассмотрим более интересный пример:

 Theorem plus_id_example : forall n m : nat, n = m -> n + m = m + n. 

Вместо того, чтобы формулировать и доказывать универсальное утверждение относительно любых n и m, эта теорема гласит о более узких свойствах, которые имеют место при n = m. Поскольку n и m – произвольные числа, мы не можем использовать упрощение для доказательства. Вместо этого, мы докажем, что заменяя m на n в условии (в предположении n = m), мы получим верное тождество. Тактика, которая указывает Coq совершить такую замену, называется rewrite:

 Proof.  intros n m.  intros H.  rewrite -> H.  reflexivity. Qed. 

Для того, чтобы лучше понять что же здесь произошло, я настоятельно рекомендую запустить этот пример в CoqIDE и последовательно пройти по этому доказательству.

Итак, формулируем теорему и начинаем доказательство:

Следующим шагом переносим выражения из-под кванторов всеобщности и гипотезу в текущий контекст доказательства (в правой верхней части CoqIDE наблюдаем как изменяется текущий контекст доказательства):

Осуществляем перезапись текущей цели доказательства:

Заканчиваем доказательство с помощью упрощения:

Заключение

В следующей части мы познакомимся с более продвинутыми тактиками и начнем работать со структурами данных в Coq. Еще раз обращаю внимание читателя на важность самостоятельного запуска примеров в CoqIDE.

Ссылки на предыдущие части:

1. Начало.
2. Индуктивные определения.