Мягкое введение в Coq: используем тактики

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

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

This entry passed through the Full-Text RSS service — if this is your content and you're reading it on someone else's site, please read the FAQ at fivefilters.org/content-only/faq.php#publishers. Five Filters recommends: 'You Say What You Like, Because They Like What You Say' - http://www.medialens.org/index.php/alerts/alert-archive/alerts-2013/731-you-say-what-you-like-because-they-like-what-you-say.html