Доказательство упрощением
Итак, в предыдущих частях мы определили новые типы данных и функции над ними. Настало время обратиться к вопросу о том, как сформулировать и доказать их свойства и поведение. В некотором смысле мы уже начали делать это – в первой части мы написали своего рода юнит-тест, используя ключевое слово 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.
Ссылки на предыдущие части:
Автор: ymn
