Система автоматизированного построения доказательств Coq

Учебник

Версия 7.3 ¹

Gйrard Huet, Gilles Kahn and Christine Paulin-Mohring
LogiCal Project

V7.3,
╘INRIA 1999-2002

Введение

Coq - это система автоматизированного построения доказательств для Logical Framework, известной, как исчисление индуктивных конструкций (the Calculus of Inductive Constructions). Она позволяет интерактивно строить формальные доказательства, а также манипулировать функциональными программами в соответствии с их спецификациями. Система Coq реализована на различных, в основном Unix, платформах. Для нее разработано несколько типов интерфейсов пользователя. Этот документ не претендует на исчерпывающий обзор всех возможностей Coq. Он содержит вводный курс по базовому языку спецификаций, называемому Gallina, на котором может быть разработана формальная аксиоматизация, и по основным proof tools.

Далее мы будем полагать, что читатель инсталлировав Coq на своем рабочем месте, вызывает Coq из стандартного окна терминала, не используя специализированных интерфейсов, таких как Emacs или Centaur. Инструкции по установке и более полную документацию можно найти в стандартном дистрибутиве Coq, который доступен на анонимном FTP сайта ftp.inria.fr в директории INRIA/coq/V7.3.

Во всех примерах ниже, вводимые пользователем комманды будут предварятся приглашением системы Coq < . Все комманды оканчиваются точкой. Следующие строки - это, обычно, ответ Coq в том виде, в котором он появляется на экране пользователя. Последовательность таких примеров, если иное не оговорено, образует возможную сессию Coq. Данная версия учебника была подготовлена на персональном компьютере под управлением Linux. После стандартного вызова Coq появляется сообщение похожее на это:

unix:~> coqtop
Welcome to Coq 7.3 (May 2002)

Coq <

Первая строка содержит точную версию Coq . Обязательно вставте эту строку в сообщения об аномалиях, отправляя их на нашу горячую линию coq@pauillac.inria.fr.

Глава 1: Basic Predicate Calculus (Основы исчисления предикатов)

1.1 Обзор языка спецификаций Gallina

Формальная спецификация (formal development) в Gallina состоит из последовательности объявлений (declarations) и определений (definitions). Вы можете также вводить комманды. Они не являются частью формальной спецификации, а выполняют информационные запросы или сервисные функции. Например, комманда

Coq < Quit.

завершает текущую сессию.

1.1.1 Объявления (Declarations)

Объявление ставит в соответствие некоторому имени (name) спецификацию (specification). Имя приблизительно соответствует понятию "идентификатор" в языках программирования, то есть начинающейся с буквы строке из букв, цифр и некторорых символов ASCII, таких как подчеркивание (_) и кавычка ('). Заглавные и строчные буквы различаются. Так символы A и a различны. Некоторые строки зарезервированы под ключевые слова Coq и не могут быть использованы как идентификаторы.

Спецификация - это формальное выражение, которое классифицирует описываемое понятие. Существует три основных вида спецификаций: логические высказывания, математические коллекции и абстрактные типы. Они классифицируются тремя базовыми сортами системы, называемыми соответственно Prop, Set и Type, являющимися в свою очередь базовыми абстрактными типами.

Каждому допустимому выражению e языка Gallina сопоставляется спецификация, называемая типом выражения t(E). Эта спецификация также является допустимым языком выражением. Запись e:t(E) означает решение, что e имеет тип E. С помощью команды Check вы можете запросить тип допустимого языком выражения:

Coq < Check O.
O
: nat

Таким образом, мы знаем, что идентификатор O (не путайте имя 'O' с цифрой '0', цифра не может быть идентификатором!) известен в текущем контексте и его тип - спецификация nat. Эта спецификация, в свою очередь, классифицируется, как математическая коллекция. Что мы и можем легко проверить:

Coq < Check nat.
nat
: Set

Спецификация Set - это абстрактный тип, один из базовых сортов языка Gallina. nat и O - это аксиоматизированные понятия, которые определены в арифметическом модуле, автоматически загружающемся при запуске системы Coq.

Сначала, введем имя секции. Секции нужны для того, чтобы структурировать modelisation (моделирование), ограничив область видимости параметров, гипотез и определений. Использование секций также дает удобную возможность заменить некоторую часть потсроенной формальной спецификации.

Coq < Section Declaration.

Теперь мы можем ввести в систему объявление, соответствующее неформальному математическому высказыванию: "пусть n - натуральное число".

Coq < Variable n:nat.
n is assumed

Если мы хотим ввести более точное утверждение, такое как "пусть n положительное натуральное число", мы должны добавить другое объявление, которое явно введет гипотезу Pos_n, специфицированную соответствующим логическим высказыванием:

Coq < Hypothesis Pos_n : (gt n O).
Pos_n is assumed

Мы можем проверить, что отношение gt известно в текущем контексте и имеет нужный нам тип:

Coq < Check gt.
gt
: nat->nat->Prop

Мы видим, что gt - функция, получающая два аргумента и возвращающая логическое высказывание. Данная запись аналогична той, которая используется в функциональных языках программирования: мы можем сформировать функциональный тип nat->Prop с помощью стрелки - конструктора функций - из типа nat (специфицированного) и типа логических высказывавний Prop (абстрактного):

Coq < Check nat->Prop.
nat->Prop
: Type

Далее мы можем еще раз добавить nat, чтобы получить тип nat->nat->Prop - тип бинарных отношений над натуральными числами. nat->nat->Prop - это сокращение для nat->(nat->Prop).

Функциональные понятия применяются обычным образом. Выражение f типа A->B можно применить к выражению e типа A, сформировав выражение (f e) типа B. Отсюда мы получаем, что выражение (gt n) имеет тип nat->Prop, а выражение (gt n O), которое является сокращением для выражения ((gt n) O), является логическим высказыванием.

Coq < Check (gt n O).
(gt n O)
: Prop

1.1.2 Определения

Первоначально, COQ содержит несколько арифметических определений: nat определено как математическая коллекция (тип Set), константы O, S, plus определены, как объекты с типами nat, nat->nat и nat->nat->nat соответсвенно. Мы можем ввести новое определение, которое свяжет имя со значением известного типа. Например, ввести константу one, как следующую за нулем:

Coq < Definition one := (S O).
one is defined

Мы можем дополнительно указать требуемый тип:

Coq < Definition two : nat := (S one).
two is defined

Coq позволяет использовать несколько разных способов записи:

Coq < Definition three := (S two) : nat.
three is defined

Вот способ определить удваивающую функцию от аргумента m типа nat находящую результат, как (plus m m):

Coq < Definition double := [m:nat](plus m m).
double is defined

Квадратные скобки понимаются следующим образом: если в некотором контексте выражение e имеет тип B, то мы можем, добавив объявление x с типом A, получить выражение [x:A]e с типом A->B. В выражении [x:A]e x - связанная переменная. Мы могли бы с таким же успехом определить double, как [n:nat](plus n n).

Связанные (локальные) переменные и свободные (глобальные) переменные могут использоваться одновременно. Например, мы можем определить функцию, которая прибавляет константу n к своему аргументу:

Coq < Definition add_n := [m:nat](plus m n).
add_n is defined

Тем не менее, отметим, что здесь мы не можем заменить формальный аргумент m на n не затронув свободное вхождение n, что привело бы к изменению значения определяемого понятия.

Операции связывания хорошо известны, например, в логике, где они назваются кванторами. Таким обазом, мы можем universally quantify высказывание, например m>0, получая universal высказывание " m╥ m>0. Действительно, этот оператор доступен в Coq и имеет следующий синтаксис: (m:nat)(gt m O). Аналогично, в случае the functional abstraction binding мы обязаны явно объявить тип quantified (квантифицируемой) переменной. We check:

Coq < Check (m:nat)(gt m O).
(m:nat)(gt m O)
: Prop

Мы можем удалить созданную формальную спецификацию, удалив содержание текущей секции:

Coq < Reset Declaration.

1.2 Введение в мезанизм вывода: Minimal Logic

Далее, мы будем рассматривать различные высказывания построенные из атомарных выссказываний A, B, C. Для простоты обявим эти атомы глобальными переменны типа Prop. Объявить несколько имен с одной и той же спецификацией можно одной командой:

Coq < Section Minimal_Logic.

Coq < Variables A,B,C:Prop.
A is assumed
B is assumed
C is assumed

Мы будем рассматривать простую импликацию, как например A╝ B, читая ``из A следует B''. Заметим, что символ стрелки перегружен. Ранее он использовался, как конструктор функционального типа, теперь же, как пропозициональная связка:

Coq < Check A->B.
A->B
: Prop

Давайте начнем простое доказательство. Мы хотим доказать легкую тавтологию ((A╝ (B╝ C))╝ (A╝ B)╝ (A╝ C). Мы запускаем механизм доказательства командой Goal, за которой следует предположение, которое мы хотим проверить:

Coq < Goal (A->(B->C))->(A->B)->(A->C).
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   (A->B->C)->(A->B)->A->C

Система отображает текущую цель под двойной линией и локальные гипотезы (пока их нет) над линией. Мы назаваем комбинацию локальных гипотез и цели суждением (judgment). Новая подсказка Unnamed_thm < указывает на то, что мы сейчас на самом нижнем уровне системы в режиме доказательства. В этом режиме доступны новые комманды, такие как тактики (tactics), которые являются примитивами построения доказательства. Тактика действует на текущую цель, пытаясь построить доказательство соответствующего суждения, возможно на основе некоторых гипотетических суждений, которые затем добавляются к текущему списку предполагаемых суждений. Например, тактика Intro применима к любому суждению, цель которого - импликация. Она перемещает посылку импликации в список локальных гипотез:

Coq < Intro H.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A->B->C
  ============================
   (A->B)->A->C

Можно получить результат нескольких применений тактики Intro за один шаг:

Coq < Intros H' HA.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A->B->C
  H' : A->B
  HA : A
  ============================
   C

Мы видим, что текущая цель C может быть получена из гипотезы H, если установить истинность A и B. Этот способ аргументации реализует тактика Apply:

Coq < Apply H.
2 subgoals

  A : Prop
  B : Prop
  C : Prop
  H : A->B->C
  H' : A->B
  HA : A
  ============================
   A
subgoal 2 is:
B

Сейчас мы в ситуации, когда нам необходимо доказать два суждения. Первое из них отображается полностью. Для второго система выводит только соответствующую подцель, но не отображает список его локальных гипотез. Заметим, что тактика Apply сохранила локальные гипотезы исходного суждения, и они все еще доступны в суждении, сгенерированном ею.

Чтобы доказать текущую цель, мы просто должны отметить, что она в точности доступна нам, как гипотеза HA:

Coq < Exact HA.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A->B->C
  H' : A->B
  HA : A
  ============================
   B

Теперь применим H' :

Coq < Apply H'.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A->B->C
  H' : A->B
  HA : A
  ============================
   A

Мы можем закончить доказательство, опять использовав Exact HA. Но мы можем и не вспоминать про имя HA, а просто указать, что текущая цель следует, из локальных предположений:

Coq < Assumption.
Subtree proved!

Доказательство закончено. Мы может отвергнуть его, используя команду Abort, которая без дальнейших хлопот вернет нас на верхний уровень) Coq, или сохранить его как лемму в текущем контексте, под именем trivial_lemma:

Coq < Save trivial_lemma.
Intro H.
Intros H' HA.
Apply H.
Exact HA.
Apply H'.
Assumption.
trivial_lemma is defined

В качестве коментария система выводит доказательство, как последовательность примененных тактик.

Давайте повторим это доказательство, немного изменив его. Во-первых, мы можем назвать начальную цель леммой:

Coq < Lemma distr_impl : (A->(B->C))->(A->B)->(A->C).
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   (A->B->C)->(A->B)->A->C

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

Coq < Intros.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A->B->C
  H0 : A->B
  H1 : A
  ============================
   C

Тактика Intros дает тот же результат, что и многократное применение тактики Intro.

Затем, мы можем объединять несколько тактик вместе последовательно или параллельно, получая комбинации тактик (tacticals). Основные конструкции таковы:

T₁ ; T₂ применить тактику T₁ к текущей цели, затем тактику T₂ ко всем подцелям, созданным тактикой T₁.
T; [T₁ | T₂ | ... | T_n] применить тактику T к текущей цели, затем тактику T₁ к первой созданной подцели, ..., тактику T_n к n-ой подцели.

Теперь мы можем завершить доказательство distr_impl с помощью одной составной тактики:

Coq < Apply H; [Assumption | Apply H0; Assumption].
Subtree proved!

Давайте теперь сохраним лемму distr_impl:

Coq < Save.
Intros.
Apply H; [ Assumption | Apply H0; Assumption ].
distr_impl is defined

Здесь комманда Save не требует аргументов, так как мы уже присвоили имя distr_impl вначале; тем не менее можно изменить его, указав как аргумент комманды Save другое.

Такая простая комбинация тактик Intro, Apply и Assumption может быть найдена автоматически, применением тактики Auto:

Coq < Lemma distr_imp : (A->(B->C))->(A->B)->(A->C).
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   (A->B->C)->(A->B)->A->C

Coq < Auto.
Subtree proved!

В этот раз мы не будем сохранять доказательство. Мы просто отвергнем его коммандой Abort:

Coq < Abort.
Current goal aborted

В любой момент по ходу доказательства можно выйти из него и вернуться на верхний уровень Coq, использовав команду Abort. Также можно использовать команду Restart, чтобы начать доказательство текущей леммы с самого начала, команду Undo, чтобы вернуться на один шаг назад, или комманду Undo n, чтобы вернуться на n шагов.

В завершении, посмотрим на полезную команду Inspect n., которая проверяет глобальное окружение Coq, отображая n понятий, определенных последними:

Coq < Inspect 3.
distr_impl : (A->B->C)->(A->B)->A->C

Объявления (и глобальные параметры, и аксиомы) отображаются предваренными ***; у определений и лемм отображаются только спецификации, а их значения (доказательства) опускаются.

1.3 Исчисление высказываний

1.3.1 Коньюнкция

Мы видели, как можно доказывать утверждения, содержащие импликацию, комбинируя тактики Intro и Apply. В большинстве случаев для построения доказательств в Coq используется естественный вывод (Natural Deduction). При этом правила построения доказательств разделяются на правила введения логических связок (introduction rules) и на правила снятия логических связок (elimination rules). Давайте проиллюстрируем это на примере пропозициональных связок /\ и \/.

Coq < Lemma and_commutative : A /\ B -> B /\ A.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   A/\B->B/\A

Coq < Intro.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A/\B
  ============================
   B/\A

Разделим коньюктивную гипотезу H на компоненты, применив тактику Elim:

Coq < Elim H.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A/\B
  ============================
   A->B->B/\A

Теперь применим тактику введения коньюнкции - Split, которая разделит коньюктивную цель на две подцели:

Coq < Split.
2 subgoals

  A : Prop
  B : Prop
  C : Prop
  H : A/\B
  H0 : A
  H1 : B
  ============================
   B
subgoal 2 is:
A

Дальнейшее тривиально. Есть и другой способ ввести полное доказательство:

Coq < Restart.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   A/\B->B/\A

Coq < Intro H; Elim H; Auto.
Subtree proved!

Coq < Save.
Intro H; Elim H; Auto.
and_commutative is defined

Тактика Auto достигает цели в данной ситуации, так как ей известен оператор введения коньюнкции - conj:

Coq < Check conj.
conj
: (A,B:Prop)A->B->A/\B

В действительности, тактика Split - это всего лишь сокращение для Apply conj.

Как мы только что видели, тактика Auto не ограничевается применением лишь локальных гипотез; она также пытается применять леммы из указанного ей списка. Добавляя леммы в этот сисок коммандой Hints Resolve, можно пошагово наращивать мощность тактики Auto.

1.3.2 Дизьюнкция

Давайте аналогичным образом рассмотрим дизьюнкцию:

Coq < Lemma or_commutative : A \/ B -> B \/ A.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   A\/B->B\/A

Coq < Intro H; Elim H.
2 subgoals

  A : Prop
  B : Prop
  C : Prop
  H : A\/B
  ============================
   A->B\/A
subgoal 2 is:
B->B\/A

Разберем доказательство первой подцели пордробно. Для того, чтобы доказать импликацию, предполагаем посылку A, используя тактику Intro:

Coq < Intro HA.
2 subgoals

  A : Prop
  B : Prop
  C : Prop
  H : A\/B
  HA : A
  ============================
   B\/A
subgoal 2 is:
B->B\/A

Гипотеза H нам больше не нужна, и мы можем удалить ее тактикой Clear; в нашем случае это не так важно, но в больших доказательствах бывает полезным убрать все ненужные гипотезы, которые засоряют ваш экран:

Coq < Clear H.
2 subgoals

  A : Prop
  B : Prop
  C : Prop
  HA : A
  ============================
   B\/A
subgoal 2 is:
B->B\/A

Существует два правила введения дизьюнкции. Мы можем получить P\/Q как из P, так и из Q. Эти правила реализуются двумя proof constructors: or_introl и or_intror. Они могут быть применены к текущей цели тактиками Left и Right соответственно. Например:

Coq < Right.
2 subgoals

  A : Prop
  B : Prop
  C : Prop
  HA : A
  ============================
   A
subgoal 2 is:
B->B\/A

Coq < Trivial.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A\/B
  ============================
   B->B\/A

Тактика Trivial работает также, как и Auto и использует тот же список лемм, но пытается применить только те тактики, которые могут достичь цели за один шаг.

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

Coq < Auto.
Subtree proved!

Тем не менее, тактика Auto не докажет всю лемму, так как она не пытается выполнять шаги, снимающие логические связки. Неспособность тактики Auto автоматически доказывать столь простые тавтологии немного разочаровывает, но это сделано для того, чтобы ее применение было эффективным в любых ситуациях.

1.3.3 Tauto

В Coq существует полная тактика для пропозициональных тавтологий - тактика Tauto.

Coq < Restart.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   A\/B->B\/A

Coq < Tauto.
Subtree proved!

Coq < Save.
Tauto.
or_commutative is defined

С помощью стандартной комманды, печатающей значение любого понятия, определенного в текущем контексте, можно проверить фактическое дерево вывода, построенное тактикой Tauto:

Coq < Print or_commutative.
or_commutative =
[H:(A\/B)]
(or_ind A B B\/A [H0:A](or_intror B A H0) [H0:B](or_introl B A H0) H)
: A\/B->B\/A

Не так-то просто понять правила записи доказательства без некоторых объяснений. The square brackets, such as [H:A\/B], correspond to Intro H, whereas a subterm such as (or_intror B A H0) corresponds to the sequence Apply or_intror; Exact H0. The extra arguments B and A correspond to instantiations to the generic combinator or_intror, which are effected automatically by the tactic Apply when pattern-matching a goal. The specialist will of course recognize our proof term as a l-term, used as notation for the natural deduction proof term through the Curry-Howard isomorphism. The naive user of Coq may safely ignore these formal details.

Давайте испытаем тактику Tauto на более сложном примере:

Coq < Lemma distr_and : A->(B/\C) -> (A->B /\ A->C).
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   A->B/\C->A->B/\A->C

Coq < Tauto.
Subtree proved!

Coq < Save.
Tauto.
distr_and is defined

1.3.4 Классическая логика

Вот пример, на котором тактика Tauto не срабатывает:

Coq < Lemma Peirce : ((A->B)->A)->A.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   ((A->B)->A)->A

Coq < Try Tauto.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   ((A->B)->A)->A

В общем случае, Tauto всегда возвращвет ответ. При использовании же тактики Try ничего не меняется, если тактика указанная как аргумент не срабатывает.

Если вы хорошо знакомы с классической логикой, то такой результат может оказаться для вас неожиданным. Peirce's lemma истина в булевой логике, так как она истина при любых истинностных значениях A и B. В Coq с помощью тактики Tauto можно доказать двойное отрицание Peirce's law:

Coq < Abort.
Current goal aborted

Coq < Lemma NNPeirce : ~~(((A->B)->A)->A).
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   ~~(((A->B)->A)->A)

Coq < Tauto.
Subtree proved!

Coq < Save.
Tauto.
NNPeirce is defined

В классической логике двойное отрицание высказывания эквивалентно ему самому, но в конструктивной логике Coq это не так. Если вы хотите использовать классическую логику, вы должны явно импортировать модуль Classical, в котором объявлен закон исключенного третьего и классические тавтологии, такие как de Morgan's laws. Для импорта модулей из библиотеки в Coq используется комманда Require:

Coq < Require Classical.

Coq < Check NNPP.
NNPP
: (p:Prop)~~p->p

Теперь можно легко доказать (хотя предположительно и не самым прямым путем) любой классический закон, такой как Peirce's закон :

Coq < Lemma Peirce : ((A->B)->A)->A.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   ((A->B)->A)->A

Coq < Apply NNPP; Tauto.
Subtree proved!

Coq < Save.
Apply NNPP; Tauto.
Peirce is defined

Вот еще один пример из логики выссказываний в форме Шотландской задачки. В частном клубе действуют следующие правила:

Все не шотландцы носят красные носки.
Все члены клуба или носят кильт, или не носят красные носки.
Женатые члены клуба не приходят (go out) по воскресеньям.
Члены клуба приходят по воскресеньям если и только если они шотландцы.
Каждый член клуба, носящий кильт - шотландец и женат.
Каждый шотландец носит кильт.

Теперь покажем, что правила так строги, что никто не может быть принят в клуб.

Coq < Section club.

Coq < Variable Scottish, RedSocks, WearKilt, Married, GoOutSunday : Prop.
Scottish is assumed
RedSocks is assumed
WearKilt is assumed
Married is assumed
GoOutSunday is assumed

Coq < Hypothesis rule1 : ~Scottish -> RedSocks.
rule1 is assumed

Coq < Hypothesis rule2 : WearKilt \/ ~RedSocks.
rule2 is assumed

Coq < Hypothesis rule3 : Married -> ~GoOutSunday.
rule3 is assumed

Coq < Hypothesis rule4 : GoOutSunday <-> Scottish.
rule4 is assumed

Coq < Hypothesis rule5 : WearKilt -> (Scottish /\ Married).
rule5 is assumed

Coq < Hypothesis rule6 : Scottish -> WearKilt.
rule6 is assumed

Coq < Lemma NoMember : False.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  Scottish : Prop
  RedSocks : Prop
  WearKilt : Prop
  Married : Prop
  GoOutSunday : Prop
  rule1 : ~Scottish->RedSocks
  rule2 : WearKilt\/~RedSocks
  rule3 : Married->~GoOutSunday
  rule4 : GoOutSunday<->Scottish
  rule5 : WearKilt->Scottish/\Married
  rule6 : Scottish->WearKilt
  ============================
   False

Coq < Tauto.
Subtree proved!

Coq < Save.
Tauto.
NoMember is defined

At that point NoMember is a proof of the absurdity depending on hypotheses. Мы можем закрыть секцию. В этом случае переменные и гипотезы станут недоступны, а тип NoMember будет обобщен.

Coq < End club.
NoMember is discharged.

Coq < Check NoMember.
NoMember
     : (Scottish,RedSocks,WearKilt,Married,GoOutSunday:Prop)
        (~Scottish->RedSocks)
        ->WearKilt\/~RedSocks
        ->(Married->~GoOutSunday)
        ->(GoOutSunday<->Scottish)
        ->(WearKilt->Scottish/\Married)
        ->(Scottish->WearKilt)
        ->False

1.4 Исчисление предикатов

Давайте перейдем к логике предикатов и, в первую очередь, к иссчислению предикатов первого порядка. Суть исчисления предикатов в том, чтобы попробовать доказать теоремы в наиболее абстрактном виде, не используя определений математических понятий, а манипулируя непроинтерпретированными функциональными и предикатными символами.

1.4.1 Sections and signatures

Обычно, работа идет в некоторой domain of discourse (дискурсе, понимании, предметной области) над рядом символов переменных и функций. В Coq используется язык с большим разнообразием типов, так что мы можем смешивать несколько domains of discourse в нашем многосортном языке. Сейчас мы сделаем несколько упражнений. В domain of discourse D аксиоматизированно как Set, и мы используем два предикатных символа P и R над D с арностью соответственно 1 и 2. Эти абстрактные сущности могут быть введены в контекст, как глобальные переменные, но нужно соблюдать аккуратность и не засорять нашу глобальную среду такими описаниями. Например, мы уже засорили нашу сессию Coq, объявив переменные n, Pos_n, A, B и C. Чтобы вернуться к исходному состоянию нашей сессии, можно использовать комманду Reset. Она вернет нас точно к тому состоянию, которое предшествовало данному глобальному понятию, как мы и делали ранее, чтобы удалить секцию. Другой способ вернуться к исходному состоянию - использовать:

Coq < Reset Initial.

Сейчас мы объявим новую Section, которая позволит нам определять понятия локально внутри удачно ограниченной области. Начнем мы с определений domain of discourse D и бинарного отношения R над D:

Coq < Section Predicate_calculus.

Coq < Variable D:Set.
D is assumed

Coq < Variable R: D -> D -> Prop.
R is assumed

Продемонстрируем простой пример вывода в исчислении предикатов. Предположим, что отношение R симметрично и транзитивно. Докажем, что R рефлексивно в любой точке x, которая имеет предшествующую по отношению R. Так как мы решили сделать предположения о R локальными гипотезами теоремы, а не глобальными аксиомами теории, то мы откроем для этого новую секцию.

Coq < Section R_sym_trans.

Coq < Hypothesis R_symmetric : (x,y:D) (R x y) -> (R y x).
R_symmetric is assumed

Coq < Hypothesis R_transitive : (x,y,z:D) (R x y) -> (R y z) -> (R x z).
R_transitive is assumed

Заметим, что конструкция (x:D) соответствует квантору всеобщности " x : D.

1.4.2 Квантор существования

Теперь займемся леммой и перейдем в режим доказательства.

Coq < Lemma refl_if : (x:D)(EX y | (R x y)) -> (R x x).
1 subgoal

  D : Set
  R : D->D->Prop
  R_symmetric : (x,y:D)(R x y)->(R y x)
  R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x z)
  ============================
   (x:D)(EX y:D | (R x y))->(R x x)

Заметим, что локальные гипотезы открытой в данный момент секции перечислены как локальные гипотезы текущей цели. Это сделано так, потому что эти гипотезы будут выгружены, как мы и увидим, когда мы закроем соответствующую секцию.

Отметим функциональный синтаксис квантора существования. Он строится на основе оператора ex, который получает в качестве аргумента предикат:

Coq < Check ex.
ex
: (A:Set)(A->Prop)->Prop

Нотация (EX x | (P x)) является сокращением (ex D [x:D](P x)). Квантор существования обрабатывается в Coq аналогичным способом, что и связки /\ и \/: он вводится proof combinator'ом ex_intro, который вызывается специальной тактикой Exists, и его снятие дает свидетельства a:D для P и h:(P a), которое подтверждает истинность P в точке a. Позвольте нам показать как это работает на нашем примере:

Coq < Intros x x_Rlinked.
1 subgoal

  D : Set
  R : D->D->Prop
  R_symmetric : (x,y:D)(R x y)->(R y x)
  R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x z)
  x : D
  x_Rlinked : (EX y:D | (R x y))
  ============================
   (R x x)

Отметим, что Intro обрабатывает квантор всеобщности таким же образом, как и посылку импликации. Связанные переменные переименовываются тогда, когда это необходимо; например, если бы мы начали с Intro y, мы бы получили такую цель:

Coq < Intro y.
1 subgoal

  D : Set
  R : D->D->Prop
  R_symmetric : (x,y:D)(R x y)->(R y x)
  R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x z)
  y : D
  ============================
   (EX y0:D | (R y y0))->(R y y)

Давайте теперь используем гипотезу x_Rlinked, чтобы получить y, следующий за x по отношению R. Для этого нужно сделать два шага: первый - Elim, второй - Intros

Coq < Elim x_Rlinked.
1 subgoal

  D : Set
  R : D->D->Prop
  R_symmetric : (x,y:D)(R x y)->(R y x)
  R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x z)
  x : D
  x_Rlinked : (EX y:D | (R x y))
  ============================
   (x0:D)(R x x0)->(R x x)

Coq < Intros y Rxy.
1 subgoal

  D : Set
  R : D->D->Prop
  R_symmetric : (x,y:D)(R x y)->(R y x)
  R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x z)
  x : D
  x_Rlinked : (EX y:D | (R x y))
  y : D
  Rxy : (R x y)
  ============================
   (R x x)

Теперь мы хотим использовать R_transitive. Тактике Apply будет известно, что переменным x и z гипотезы надо сопоставить переменную x нашего доказательства, но нужно подсказать, что сопоставить переменной y, которая присутствует в гипотезе R_transitive, но в ее посылке, а не в заключении. Мы даем Apply соответствующую подсказку, используя with:

Coq < Apply R_transitive with y.
2 subgoals

  D : Set
  R : D->D->Prop
  R_symmetric : (x,y:D)(R x y)->(R y x)
  R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x z)
  x : D
  x_Rlinked : (EX y:D | (R x y))
  y : D
  Rxy : (R x y)
  ============================
   (R x y)
subgoal 2 is:
(R y x)

Далее, завершаем доказательство по уже известной схеме:

Coq < Assumption.
1 subgoal

  D : Set
  R : D->D->Prop
  R_symmetric : (x,y:D)(R x y)->(R y x)
  R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x z)
  x : D
  x_Rlinked : (EX y:D | (R x y))
  y : D
  Rxy : (R x y)
  ============================
   (R y x)

Coq < Apply R_symmetric; Assumption.
Subtree proved!

Coq < Save.

Давайте теперь закроем текущую секцию.

Coq < End R_sym_trans.
refl_if is discharged.

Here Coq's printout is a warning that all local hypotheses have been discharged in the statement of refl_if, which now becomes a general theorem in the first-order language declared in section Predicate_calculus. In this particular example, the use of section R_sym_trans has not been really significant, since we could have instead stated theorem refl_if in its general form, and done basically the same proof, obtaining R_symmetric and R_transitive as local hypotheses by initial Intros rather than as global hypotheses in the context. But if we had pursued the theory by proving more theorems about relation R, we would have obtained all general statements at the closing of the section, with minimal dependencies on the hypotheses of symmetry and transitivity.

1.4.3 Парадоксы классического исчисления предикатов

Чтобы проиллистрировать это свойство, расширим наш язык, продолжив секцию Predicate_calculus объявлением унарного предиката P и константы d:

Coq < Variable P:D->Prop.
P is assumed

Coq < Variable d:D.
d is assumed

Попытаемся доказать хорошо известный факт логики первого порядка: "a universal predicate is non-empty" или, другими словами, существование следует из всеобщности.

Coq < Lemma weird : ((x:D)(P x)) -> (EX a | (P a)).
1 subgoal

  D : Set
  R : D->D->Prop
  P : D->Prop
  d : D
  ============================
   ((x:D)(P x))->(EX a:D | (P a))

Coq < Intro UnivP.
1 subgoal

  D : Set
  R : D->D->Prop
  P : D->Prop
  d : D
  UnivP : (x:D)(P x)
  ============================
   (EX a:D | (P a))

Вначале обратим внимание на пару скобок вокруг (x:D)(P x) в формулировке леммы weird. Если бы мы опустили их, парсер Coq проинтерпретировал бы это высказывание, как тривиально истинный факт, since we would postulate an x verifying (P x). В данном случае ситуация, конечно, более сложная. Если у нас есть конкретный элемент множества D, то мы можем применить к нему UnivP, получив требуемое. В противном случае мы в тупике. Конечно, такой елемент d существует, но это только потому, что мы ввели его в нашу сигнатуру явно. Эта ситуация демонстрирует различие между стандартным исчислением предикатов и Coq. В стандартной логике первого порядка всегда есть лемма, эквивалентная weird. Она является правилом логического вывода для кванторов, the semantic justification being that the interpretation domain is assumed to be non-empty. Так как в Coq не предполагается, что все типы не пусты, то лемма weird выполняется только в тех сигнатурах, где можно явно получить элемент из области определения предиката.

Давайте завершим доказательство, продемонстрировав использование тактики Exists:

Coq < Exists d; Trivial.
Subtree proved!

Coq < Save.
Intro UnivP.
Split with d; Trivial.
weird is defined

Еще один пример, когда правила классического исчисления предикатов приводят в замешательство - это Smullyan's drinkers' paradox: "В любом не пустом баре есть такой человек, что если она пьет, то все пьют". Мы моделируем бар множеством D, пьющих предикатом P. Нам потребуется классическая логика. Вместо того, чтобы загружать модуль Classical, как мы делали раньше, мы просто изложим закон исключенного третьего, как локальную схему гипотез:

Coq < Hypothesis EM : (A:Prop) A \/ ~A.
EM is assumed

Coq < Lemma drinker : (EX x | (P x) -> (x:D)(P x)).
1 subgoal

  D : Set
  R : D->D->Prop
  P : D->Prop
  d : D
  EM : (A:Prop)A\/~A
  ============================
   (EX x:D | (P x)->(x0:D)(P x0))

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

Coq < Elim (EM  (EX x | ~(P x))).
2 subgoals

  D : Set
  R : D->D->Prop
  P : D->Prop
  d : D
  EM : (A:Prop)A\/~A
  ============================
   (EX x:D | ~(P x))->(EX x:D | (P x)->(x0:D)(P x0))
subgoal 2 is:
~(EX x:D | ~(P x))->(EX x:D | (P x)->(x0:D)(P x0))

Вначале мы займемся первым случаем. Пусть непьющий - Том:

Coq < Intro Non_drinker; Elim Non_drinker; Intros Tom Tom_does_not_drink.
2 subgoals

  D : Set
  R : D->D->Prop
  P : D->Prop
  d : D
  EM : (A:Prop)A\/~A
  Non_drinker : (EX x:D | ~(P x))
  Tom : D
  Tom_does_not_drink : ~(P Tom)
  ============================
   (EX x:D | (P x)->(x0:D)(P x0))
subgoal 2 is:
~(EX x:D | ~(P x))->(EX x:D | (P x)->(x0:D)(P x0))

Мы докажем этот случай с помощью Тома, так как то, что он пьет приводит нас к противоречию:

Coq < Exists Tom; Intro Tom_drinks.
2 subgoals

  D : Set
  R : D->D->Prop
  P : D->Prop
  d : D
  EM : (A:Prop)A\/~A
  Non_drinker : (EX x:D | ~(P x))
  Tom : D
  Tom_does_not_drink : ~(P Tom)
  Tom_drinks : (P Tom)
  ============================
   (x:D)(P x)
subgoal 2 is:
~(EX x:D | ~(P x))->(EX x:D | (P x)->(x0:D)(P x0))

Существует несколько способов устранить противоречивый случай. Например, мы можем использовать тактику Absurd:

Coq < Absurd (P Tom); Trivial.
1 subgoal

  D : Set
  R : D->D->Prop
  P : D->Prop
  d : D
  EM : (A:Prop)A\/~A
  ============================
   ~(EX x:D | ~(P x))->(EX x:D | (P x)->(x0:D)(P x0))

Теперь разберем второй случай, в котором все пьют, как и некто, представленный у нас елементом d:

Coq < Intro No_nondrinker; Exists d; Intro d_drinks.
1 subgoal

  D : Set
  R : D->D->Prop
  P : D->Prop
  d : D
  EM : (A:Prop)A\/~A
  No_nondrinker : ~(EX x:D | ~(P x))
  d_drinks : (P d)
  ============================
   (x:D)(P x)

Возьмем любого человека в баре (назовем его Dick) и разберем два случая: пьет он или нет:

Coq < Intro Dick; Elim (EM (P Dick)); Trivial.
1 subgoal

  D : Set
  R : D->D->Prop
  P : D->Prop
  d : D
  EM : (A:Prop)A\/~A
  No_nondrinker : ~(EX x:D | ~(P x))
  d_drinks : (P d)
  Dick : D
  ============================
   ~(P Dick)->(P Dick)

Один случай тривиален. В торой также, как и раньше, сведем к противоречию:

Coq < Intro Dick_does_not_drink; Absurd (EX x | ~(P x)); Trivial.
1 subgoal

  D : Set
  R : D->D->Prop
  P : D->Prop
  d : D
  EM : (A:Prop)A\/~A
  No_nondrinker : ~(EX x:D | ~(P x))
  d_drinks : (P d)
  Dick : D
  Dick_does_not_drink : ~(P Dick)
  ============================
   (EX x:D | ~(P x))

Coq < Exists Dick; Trivial.
Subtree proved!

Coq < Save.
Elim (EM (EX x:? | ~(P x))).
Intro Non_drinker; Elim Non_drinker; Intros Tom Tom_does_not_drink.
Split with Tom; Intro Tom_drinks.
Absurd (P Tom); Trivial.
Intro No_nondrinker; Split with d; Intro d_drinks.
Intro Dick; Elim (EM (P Dick)); Trivial.
Intro Dick_does_not_drink; Absurd (EX x:? | ~(P x)); Trivial.
Split with Dick; Trivial.
drinker is defined

Теперь закроем основную секцию:

Coq < End Predicate_calculus.
refl_if is discharged.
weird is discharged.
drinker is discharged.

Remark how the three theorems are completely generic in the most general fashion; the domain D is discharged in all of them, R is discharged in refl_if only, P is discharged only in weird and drinker, along with the hypothesis that D is inhabited. Finally, the excluded middle hypothesis is discharged only in drinker.

Note that the name d has vanished as well from the statements of weird and drinker, since Coq's pretty-printer replaces systematically a quantification such as (d:D)E, where d does not occur in E, by the functional notation D->E. Similarly the name EM does not appear in drinker.

Actually, universal quantification, implication, as well as function formation, are all special cases of one general construct of type theory called dependent product. This is the mathematical construction corresponding to an indexed family of functions. A function fО P x:D╥ Cx maps an element x of its domain D to its (indexed) codomain Cx. Thus a proof of " x:D╥ Px is a function mapping an element x of D to a proof of proposition Px.

1.4.4 Гибкое использование локальных гипотез

Очень часто по-ходу доказательства мы хотим извлечь локальную гипотезу и сделать ее опять явной посылкой цели, например, чтобы получить более обобщенную гипотезу индукции. В таких случаях нам потребуется тактика Generalize:

Coq < Section Predicate_Calculus.

Coq < Variable P,Q:nat->Prop. Variable R: nat->nat->Prop.
P is assumed
Q is assumed
R is assumed

Coq < Lemma PQR : (x,y:nat)((R x x)->(P x)->(Q x))->(P x)->(R x y)->(Q x).
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  ============================
   (x,y:nat)((R x x)->(P x)->(Q x))->(P x)->(R x y)->(Q x)

Coq < Intros.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  x : nat
  y : nat
  H : (R x x)->(P x)->(Q x)
  H0 : (P x)
  H1 : (R x y)
  ============================
   (Q x)

Coq < Generalize H0.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  x : nat
  y : nat
  H : (R x x)->(P x)->(Q x)
  H0 : (P x)
  H1 : (R x y)
  ============================
   (P x)->(Q x)

Иногда бывает удобно использовать при доказательстве лемму. Хотя у нас и нет прямой возможности ссослаться на такой ранее доказанный факт, но мы можем использовать тактику Cut, которая позволит применить лемму, отложив ее доказательство на потом в виде еще одной подцели:

Coq < Cut (R x x); Trivial.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  x : nat
  y : nat
  H : (R x x)->(P x)->(Q x)
  H0 : (P x)
  H1 : (R x y)
  ============================
   (R x x)

1.4.5 Равенство

Основное используемое вCoq равенство - это равенство Лейбница (Leibniz), записываемое в инфиксной форме в виде x=y, где x и y - это два выражения, типы которых принадлежат одному множеству. Заменить x на y в любом терме можно, используя ряд тактик, например Rewrite или Replace.

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

Coq < Variable f:nat->nat.
Warning: Variable f is not visible from current goals
f is assumed

Coq < Hypothesis foo : (f O)=O.
Warning: Variable foo is not visible from current goals
foo is assumed

Докажем следующее условное равенство:

Coq < Lemma L1 : (k:nat)k=O->(f k)=k.

Как обычно, первым делом предполагаем посылки тактикой Intro:

Coq < Intros k E.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f O)=O
  k : nat
  E : k=O
  ============================
   (f k)=k

Применим равенство E слева направо:

Coq < Rewrite E.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f O)=O
  k : nat
  E : k=O
  ============================
   (f O)=O

В результате оба вхождения k были заменены на O.

Теперь применим foo, чтобы завершить доказательство:

Coq < Apply foo.
Subtree proved!

Coq < Save.
Intros k E.
Rewrite E.
Apply foo.
L1 is defined

Чтобы применить равенство справа налево, нужно импользовать Rewrite <- E, чтобы слева направо - Rewrite E или Rewrite -> E. Теперь проиллюстрируем использование тактики Replace.

Coq < Hypothesis f10 : (f (S O))=(f O).
Warning: Variable f10 is not visible from current goals
f10 is assumed

Coq < Lemma L2 : (f (f (S O)))=O.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f O)=O
  f10 : (f (S O))=(f O)
  ============================
   (f (f (S O)))=O

Coq < Replace (f (S O)) with O.
2 subgoals

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f O)=O
  f10 : (f (S O))=(f O)
  ============================
   (f O)=O
subgoal 2 is:
O=(f (S O))

Применение тактики Replace позволило нам существенно упростить нашу основную цель, но оно также поставило перед нами вторую подзадачу. Первая цель достигается применением леммы foo; вторая - использованием транзитивности а затем симметричности равенства, например, с помощью тактик Transitivity и Symmetry:

Coq < Apply foo.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f O)=O
  f10 : (f (S O))=(f O)
  ============================
   O=(f (S O))

Coq < Transitivity (f O); Symmetry; Trivial.
Subtree proved!

Если равенство t=u, сгенерированное Replace u with t имеется в списке гипотез (возможно с точностью до симметрии), то оно будет автоматически доказано и соответствующая цель не появиться. Например:

Coq < Restart.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f O)=O
  f10 : (f (S O))=(f O)
  ============================
   (f (f (S O)))=O

Coq < Replace (f O) with O.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f O)=O
  f10 : (f (S O))=(f O)
  ============================
   (f (f (S O)))=O

Coq < Rewrite f10; Rewrite foo; Trivial.
Subtree proved!

Coq < Save.
Replace (f O) with O.
Rewrite f10; Rewrite foo; Trivial.
L2 is defined

1.4.6 Исчисление предикатов over Type

Мы только что продемонстрировали основы логического вывода первого порядка в универсе математических множеств (Set). Аналогичный логический вывод доступен и на уровне абстрактных типов (Type). Для этого потребуется загрузить библиотеку Logic_Type.

Coq < Require Logic_Type.

Теперь доступны новые proof combinators, например, квантор существования exT над типами - (EXT x | (P x)). Соответствующее правило введения, как и раньше, может быть применено тактикой Exists.

Coq < Check exT_intro.
exT_intro
: (A:Type; P:(A->Prop); x:A)(P x)->(ExT P)

Аналогично, равенство над типами доступно в форме M==N, и тактики равенства работают с == так же, как и с =.

1.5 Использование определений

The development of mathematics does not simply proceed by logical argumentation from first principles: definitions are used in an essential way. A formal development proceeds by a dual process of abstraction, where one proves abstract statements in predicate calculus, and use of definitions, which in the contrary one instantiates general statements with particular notions in order to use the structure of mathematical values for the proof of more specialised properties.

1.5.1 Unfolding definitions

Предположим, что мы хотим описать (to develop) теорию множеств, представленных характеристическими предикатами над некторым универсом U. Например:

Coq < Variable U:Type.
Warning: Variable U is not visible from current goals
U is assumed

Coq < Definition set := U->Prop.
set is defined

Coq < Definition element := [x:U][S:set](S x).
element is defined

Coq < Definition subset := [A,B:set](x:U)(element x A)->(element x B).
subset is defined

Теперь, предположим, что мы загрузили модуль, описывающий общие свойства отношений над некоторым абстрактным типом T, например, транзитивность:

Coq < Definition transitive := [T:Type][R:T->T->Prop]
Coq < (x,y,z:T)(R x y)->(R y z)->(R x z).
transitive is defined

Предположим, мы хотим доказать, что subset - транзитивное отношение.

Coq < Lemma subset_transitive : (transitive set subset).
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f O)=O
  f10 : (f (S O))=(f O)
  U : Type
  ============================
   (transitive set subset)

Чтобы добится какого-нибудь результата, нам нужно использовать определение transitive. Для этого может быть использована тактика Unfold, которая заменяет все вхождения понятия в текущей цели на его определение.

Coq < Unfold transitive.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f O)=O
  f10 : (f (S O))=(f O)
  U : Type
  ============================
   (x,y,z:set)(subset x y)->(subset y z)->(subset x z)

Теперь мы должны раскрыть (unfold) subset:

Coq < Unfold subset.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f O)=O
  f10 : (f (S O))=(f O)
  U : Type
  ============================
   (x,y,z:set)
    ((x0:U)(element x0 x)->(element x0 y))
    ->((x:U)(element x y)->(element x z))
    ->(x0:U)(element x0 x)->(element x0 z)

Раскрывать element не стоит, так как простое доказательство может быть найдено тактикой Auto над абстрактным предикатом element:

Coq < Auto.
Subtree proved!

В Coq предусмотренно множество вариаций тактики Unfold. Например, мы можем избирательно раскрыть нужное вхождение понятия:

Coq < Undo 2.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f O)=O
  f10 : (f (S O))=(f O)
  U : Type
  ============================
   (x,y,z:set)(subset x y)->(subset y z)->(subset x z)

Coq < Unfold 2 subset.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f O)=O
  f10 : (f (S O))=(f O)
  U : Type
  ============================
   (x,y,z:set)
    (subset x y)->((x:U)(element x y)->(element x z))->(subset x z)

Также можно раскрыть определение в нужной локальной гипотезе, используя нотацию in:

Coq < Intros.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f O)=O
  f10 : (f (S O))=(f O)
  U : Type
  x : set
  y : set
  z : set
  H : (subset x y)
  H0 : (x:U)(element x y)->(element x z)
  ============================
   (subset x z)

Coq < Unfold subset in H.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f O)=O
  f10 : (f (S O))=(f O)
  U : Type
  x : set
  y : set
  z : set
  H : (x0:U)(element x0 x)->(element x0 y)
  H0 : (x:U)(element x y)->(element x z)
  ============================
   (subset x z)

Наконец, тактика Red раскрывает только первое (? head occurrence) вхождение понятия в текущей цели:

Coq < Red.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f O)=O
  f10 : (f (S O))=(f O)
  U : Type
  x : set
  y : set
  z : set
  H : (x0:U)(element x0 x)->(element x0 y)
  H0 : (x:U)(element x y)->(element x z)
  ============================
   (x0:U)(element x0 x)->(element x0 z)

Coq < Auto. Save.
Subtree proved!
Unfold transitive.
Unfold 2 subset.
Intros.
Unfold subset in H.
Red.
Auto.
subset_transitive is defined

1.5.2 Principle of proof irrelevance

Even though in principle the proof term associated with a verified lemma corresponds to a defined value of the corresponding specification, such definitions cannot be unfolded in Coq: a lemma is considered an opaque definition. This conforms to the mathematical tradition of proof irrelevance: the proof of a logical proposition does not matter, and the mathematical justification of a logical development relies only on provability of the lemmas used in the formal proof.

Conversely, ordinary mathematical definitions can be unfolded at will, they are transparent. It is possible to enforce the reverse convention by declaring a definition as opaque or a lemma as transparent.

Глава 2: Индукция

2.1 Типы данных, как индуктивно определенные математические коллекции

Все понятия, которые мы рассматривали ранее относились к традиционной математической логике. Объекты описывались с помощью абстрактных отношений, которые использовались в доказательствах более или менее конструктивно; теперь мы переходим в область инудктивных типов, которые специфицируют существование конкретных математических конструкций.

2.1.1 Booleans

Дававйте начнем с коллекции booleans в том виде, в каком она специфицирована в модуле Prelude Coq:

Coq < Inductive bool : Set := true : bool | false : bool.
bool is defined
bool_rect is defined
bool_ind is defined
bool_rec is defined

Такое объявление определяет одновременно несколько объектов. Во-первых, объявляется новое множество с именем bool. Далее, объявляются конструкторы этого множества, именуемые true и false. Они аналогичны правилам ввода для нового множества bool. И наконец, объявляются специфичные для bool правила снятия, позволяющие проводить доказательства разбором случаев по элементам множества bool. Это три новых proof combinators в глобальном контексте: bool_ind, использующийся для разбора случаев; bool_rec - програмная конструкция if-then-else; bool_rect - аналогичный combinator, действующий на уровне типов (at the level of types).

Coq < Check bool_ind.
bool_ind
     : (P:(bool->Prop))(P true)->(P false)->(b:bool)(P b)

Coq < Check bool_rec.
bool_rec
     : (P:(bool->Set))(P true)->(P false)->(b:bool)(P b)

Coq < Check bool_rect.
bool_rect
     : (P:(bool->Type))(P true)->(P false)->(b:bool)(P b)

Давайте для примера докажем, что каждый Boolean - это true или false.

Coq < Lemma duality : (b:bool)(b=true \/ b=false).
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f O)=O
  f10 : (f (S O))=(f O)
  U : Type
  ============================
   (b:bool)b=true\/b=false

Coq < Intro b.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f O)=O
  f10 : (f (S O))=(f O)
  U : Type
  b : bool
  ============================
   b=true\/b=false

Используем факт, что b - элемент множества bool, вызвав тактику Elim, которая в данном случае обратится к combinator bool_ind, чтобы разделить доказательство соответственно на два случая:

Coq < Elim b.
2 subgoals

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f O)=O
  f10 : (f (S O))=(f O)
  U : Type
  b : bool
  ============================
   true=true\/true=false
subgoal 2 is:
false=true\/false=false

Оба случая доказываются тривиально:

Coq < Left; Trivial.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f O)=O
  f10 : (f (S O))=(f O)
  U : Type
  b : bool
  ============================
   false=true\/false=false

Coq < Right; Trivial.
Subtree proved!

На самом деле, полное доказательство может быть получено с помощью тактики Induction, которая комбинирует Intro и Elim, и хорошей старой тактики Auto:

Coq < Restart.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f O)=O
  f10 : (f (S O))=(f O)
  U : Type
  ============================
   (b:bool)b=true\/b=false

Coq < Induction b; Auto.
Subtree proved!

Coq < Save.
Induction b; Auto.
duality is defined

2.1.2 Натуральные числа

Натуральные числа определены в модуле Prelude с помощью конструкторов S и O аналогично Booleans:

Coq < Inductive nat : Set := O : nat | S : nat->nat.
nat is defined
nat_rect is defined
nat_ind is defined
nat_rec is defined

Сгенерированные автоматически правила снятия - это принцип инукции Peano и оператор рекурсии:

Coq < Check nat_ind.
nat_ind
: (P:(nat->Prop))(P O)->((n:nat)(P n)->(P (S n)))->(n:nat)(P n)

Coq < Check nat_rec.
nat_rec
: (P:(nat->Set))(P O)->((n:nat)(P n)->(P (S n)))->(n:nat)(P n)

Начнем с того, что покажем, как запрограммировать стандартный оператор примитивной рекурсии prim_rec с помощью более общего оператора nat_rec:

Coq < Definition prim_rec := (nat_rec [i:nat]nat).
prim_rec is defined

Вместо того, чтобы вычислять по натуральному числу i элемент индексированного множества (P i), prim_rec вычисляет тем же образом элемент множества nat. Давайте проверим тип prim_rec:

Coq < Check prim_rec.
prim_rec
     : ([_:nat]nat O)
       ->((n:nat)([_:nat]nat n)->([_:nat]nat (S n)))
       ->(n:nat)([_:nat]nat n)

Oops! Вместо ожидавшегося типа nat->(nat->nat->nat)->nat->nat мы получили более сложное выражение. На самом деле тип prim_rec эквивалентен по правилу b ожидавшемуся типу; это можно проверить в Coq с помощью комманды Eval Cbv Beta, которая b-редуцирует выражение до его нормальной формы:

Coq < Eval Cbv Beta in
Coq <      ([_:nat]nat O)
Coq <         ->((y:nat)([_:nat]nat y)->([_:nat]nat (S y)))
Coq <            ->(n:nat)([_:nat]nat n).
     = nat->(nat->nat->nat)->nat->nat
     : Set

Давайте посмотрим, как с помощью примитивной рекурсии запрограммировать сложение:

Coq < Definition addition := [n,m:nat](prim_rec m [p:nat][rec:nat](S rec) n).
addition is defined

Мы определили, что (addition n m) проводит вычисление разбором случаев по n в соответствии с конструктором натуральных чисел; если n=O, берется m; если n=(S p), берется (S rec), где rec - результат рекурсивного вычисления (addition p m). Давайте проверим это, попробовав вычислить, например, 2+3:

Coq < Eval Compute in (addition (S (S O)) (S (S (S O)))).
= (S (S (S (S (S O)))))
: ([_:nat]nat (S (S O)))

Мы не обязаны делать все явно. Coq предоставляет специальный синтаксис Fixpoint/Cases для обобщенной примитивной рекурсии, и мы можем таким образом определить сложение непосредственно:

Coq < Fixpoint plus [n:nat] : nat -> nat :=
Coq <    [m:nat]Cases n of
Coq <              O    => m
Coq <           | (S p) => (S (plus p m))
Coq <           end.
plus is recursively defined

For the rest of the session, давайте отчистим все что мы сделали, начиная с типов bool и nat, чтобы использовать первоначальные определения из модуля Prelude Coq, и чтобы не получать лишних сообщений об ошибках из-за того, что мы переопределили понятия. Таким образом, с помощью комманды Reset мы вернемся к состоянию, которое было до нашего определения bool:

Coq < Reset bool.

2.1.3 Простые доказательства индукцией

Давайте посмотрим, как вести доказательства by structural induction. Мы начнем с простого свойства толькочто определенной нами функции plus. Давайте докажем, что n=n+0.

Coq < Lemma plus_n_O : (n:nat)n=(plus n O).
1 subgoal

  ============================
   (n:nat)n=(plus n O)

Coq < Intro n; Elim n.
2 subgoals

  n : nat
  ============================
   O=(plus O O)
subgoal 2 is:
(n0:nat)n0=(plus n0 O)->(S n0)=(plus (S n0) O)

Мы видим, что Elim n, чтобы получить предикат над nat (i.e. n) - нашу исходную цель, обратился к соответствующему принципу индукции nat_ind, которая, как мы видели, является в точности схемой индукции Peano. В результате сопоставления с образцом, предикату P было приписано значение [n:nat]n=(plus n O), и мы получили в качестве подцелей соответствующие экземпляры базы индукции (P O) и шага индукции (y:nat)(P y)->(P (S y)). В обоих случаях у нас есть вхождения функции plus, в которых второй аргумент начинается с конструктора. Таким образом, они поддаются упрощению с помощью примитивной рекурсии, применимой в Coq тактикой Simpl:

Coq < Simpl.
2 subgoals

  n : nat
  ============================
   O=O
subgoal 2 is:
(n0:nat)n0=(plus n0 O)->(S n0)=(plus (S n0) O)

Coq < Auto.
1 subgoal

  n : nat
  ============================
   (n0:nat)n0=(plus n0 O)->(S n0)=(plus (S n0) O)

Выполним те же действия и для шага индукции:

Coq < Simpl; Auto.
Subtree proved!

Coq < Save.
Intro n; Elim n.
Simpl.
Auto.
Simpl; Auto.
plus_n_O is defined

Тактика Autoприменима здесь, так как использует в качестве подсказки лемму eq_S, которая утверждает, что функция S сохраняет равенство:

Coq < Check eq_S.
eq_S
: (x,y:nat)x=y->(S x)=(S y)

Давайте посмотрим, как сделать нашу лемму plus_n_O подсказкой для Auto:

Coq < Hints Resolve plus_n_O.

Теперь перейд╦м к аналогичному свойству конструктора S:

Coq < Lemma plus_n_S : (n,m:nat)(S (plus n m))=(plus n (S m)).
1 subgoal

  ============================
   (n,m:nat)(S (plus n m))=(plus n (S m))

Сделаем вс╦ быстрее, помня что тактика Induction применяет последовательно Intros и Elim. Комбинация Simpl и Auto благодаря tactic composition будет использована в обоих случаях, и мы докажем эту лемму в одну строчку:

Coq < Induction n; Simpl; Auto.
Subtree proved!

Coq < Save.
Induction n; Simpl; Auto.
plus_n_S is defined

Coq < Hints Resolve plus_n_S.

Взавершение упражнения, докажем коммуникативность функции plus:

Coq < Lemma plus_com : (n,m:nat)(plus n m)=(plus m n).
1 subgoal

  ============================
   (n,m:nat)(plus n m)=(plus m n)

Нам необходимо сделать выбор, вести ли индукцию по n или по m, ситуация будет симметрична. Например:

Coq < Induction m; Simpl; Auto.
1 subgoal

  n : nat
  m : nat
  ============================
   (n0:nat)(plus n n0)=(plus n0 n)->(plus n (S n0))=(S (plus n0 n))

Благодаря нашей подсказке plus_n_O, база индукции была доказана автоматически, но шаг индукции требует провести подстановку, а их тактика Auto не использует:

Coq < Intros m' E; Rewrite <- E; Auto.
Subtree proved!

Coq < Save.
Induction m; Simpl; Auto.
Intros m' E; Rewrite <- E; Auto.
plus_com is defined

2.1.4 Discriminate

С помощью примитивной рекурсии мы можем определять новые высказывания. Давайте, например, определим предикат, который различает конструкторы O и S: он возвращает False, когда его аргумент равен O, и True, когда его аргумент представлен в форме (S n):

Coq < Definition Is_S
Coq < := [n:nat]Cases n of O => False | (S p) => True end.
Is_S is defined

Теперь мы можем использовать вычислительную мощность Is_S для доказательства тривиального факта, что (Is_S (S n)):

Coq < Lemma S_Is_S : (n:nat)(Is_S (S n)).
1 subgoal

  ============================
   (n:nat)(Is_S (S n))

Coq < Simpl; Trivial.
Subtree proved!

Coq < Save.
Simpl; Trivial.
S_Is_S is defined

Но мы можем также использовать этот предикат, чтобы преобразовывать цель в форме False в форму (Is_S O). Рассмотрим особенно важное применение этого свойства; докажем, что O и S конструируют различные значения, - одну из аксиом Peano:

Coq < Lemma no_confusion : (n:nat)~(O=(S n)).
1 subgoal

  ============================
   (n:nat)~O=(S n)

Во-первых, заменим отрицание его определением, упростив цель тактикой Red; далее, получим противоречие, применив Intros:

Coq < Red; Intros n H.
1 subgoal

  n : nat
  H : O=(S n)
  ============================
   False

Теперь используем нашу хитрость:

Coq < Change (Is_S O).
1 subgoal

  n : nat
  H : O=(S n)
  ============================
   (Is_S O)

Наконец, применим равенство и, упростив полученное выражение, получим True:

Coq < Rewrite H; Trivial.
1 subgoal

  n : nat
  H : O=(S n)
  ============================
   (Is_S (S n))

Coq < Simpl; Trivial.
Subtree proved!

Чтобы пользователю не приходилось явно вводить различающие предикаты, предусмотрена специальная тактика Discriminate, позволяющая получать подобные доказательства автоматически:

Coq < Restart.
1 subgoal

  ============================
   (n:nat)~O=(S n)

Coq < Intro n; Discriminate.
Subtree proved!

Coq < Save.
Intro n; Discriminate.
no_confusion is defined

2.2 Логическое программирование

Тем же способом, каким мы выше определяли стандартные типы данных, мы можем определить и inductive families, и, например, индуктивные предикаты. Вот определение предиката ё над типом nat, в том виде, в котором оно дано в модуле Prelude в Coq:

Coq < Inductive le [n:nat] : nat -> Prop
Coq < := le_n : (le n n)
Coq < | le_S : (m:nat)(le n m)->(le n (S m)).

Это определение вводит новый предикат le:nat->nat->Prop и два конструктора le_n и le_S - определяющие le утверждения. В результате мы получаем не только "аксиомы" le_n и le_S, но и обратное свойство, что высказывание (le n m) верно в том и только в том случае, если оно может быть получено как следствие этих определяющих утверждений; другими словами, le - это минимальный предикат, удовлетворяющий утверждениям le_n и le_S. This is insured, as in the case of inductive data types, by an elimination principle, which here amounts to an induction principle le_ind, stating this minimality property:

Coq < Check le.
le
     : nat->nat->Prop

Coq < Check le_ind.
le_ind
     : (n:nat; P:(nat->Prop))
        (P n)
        ->((m:nat)(le n m)->(P m)->(P (S m)))
        ->(n0:nat)(le n n0)->(P n0)

Давайте посмотрим, как с помощью этого принципа проводить доказательства. Сначала покажем, что nё m Ю n+1ё m+1:

Coq < Lemma le_n_S : (n,m:nat)(le n m)->(le (S n) (S m)).
1 subgoal

  ============================
   (n,m:nat)(le n m)->(le (S n) (S m))

Coq < Intros n m n_le_m.
1 subgoal

  n : nat
  m : nat
  n_le_m : (le n m)
  ============================
   (le (S n) (S m))

Coq < Elim n_le_m.
2 subgoals

  n : nat
  m : nat
  n_le_m : (le n m)
  ============================
   (le (S n) (S n))
subgoal 2 is:
(m0:nat)(le n m0)->(le (S n) (S m0))->(le (S n) (S (S m0)))

То, что произошло, аналогично поведению Elim на натуральных числах: тактика Elim обратилась к подходящему принципу индукции, в данном случае le_ind, сгенерировавшему две подцели, которые могут быть теперь легко доказаны с помощью определяющих le утверждений.

Coq < Apply le_n; Trivial.
1 subgoal

  n : nat
  m : nat
  n_le_m : (le n m)
  ============================
   (m0:nat)(le n m0)->(le (S n) (S m0))->(le (S n) (S (S m0)))

Coq < Intros; Apply le_S; Trivial.
Subtree proved!

Хорошая идея - сделать определяющие утверждения подсказками, чтобы доказательство можно было бы получить простой комбинацией Induction и Auto.

Coq < Restart.
1 subgoal

  ============================
   (n,m:nat)(le n m)->(le (S n) (S m))

Coq < Hints Resolve le_n le_S.

Тем не менее, у нас есть небольшая проблема. Мы хотим сказать: "проведи индукцию по гипотезе (le n m)", но у нас нет для не╦ явного имени. Тогда мы скажем: "проведи индукцию по первой безымянной гипотезе".

Coq < Induction 1; Auto.
Subtree proved!

Coq < Save.
Induction 1; Auto.
le_n_S is defined

Рассмотрим более сложную задачу. Докажем, что nё 0 Ю n=0. Это должно легко следовать из того факта, что в денном случае применимо только первое из определяющих le утверждений.

Coq < Lemma tricky : (n:nat)(le n O)->n=O.
1 subgoal

  ============================
   (n:nat)(le n O)->n=O

Тем не менее, попытка применить здесь что-нибудь вроде Induction 1 ни к чему не привед╦т (попробуйте и посмотрите что получится). Индукция по n также не поможет. Нам нужно проанализировать определение le, сопоставив гипотезу (le n O) с определяющими утверждениями, чтобы обнаружить, что применимо только le_n, из чего и следует результат. Такой анализ может быть проведен тактикой "inversion" - Inversion_clear:

Coq < Intros n H; Inversion_clear H.
1 subgoal

  n : nat
  ============================
   O=O

Coq < Trivial.
Subtree proved!

Coq < Save.
Intros n H; Inversion_clear H.
Trivial.
tricky is defined

Chapter 3: Модули

3.1 Открытие библиотечных модулей

Когда вы запускаете Coq, не указывая дополнительных требований в коммандной строке, вы получаете минимальную систему, в которой загружены лишь несколько библиотек. Как мы видели, standard prelude module предоставляет стандартные логические связки и a few арифметических понятий. Если вы хотите загрузить и открыть другие модули из библиотеки, вы должны использовать комманду Require также, как мы делали это раньше для классической логики. Например, если вам нужно больше арифметических конструкций, вы должны запросить:

Coq < Require Arith.

Такая команда ищет (скомпилированный) файл модуля Arith.vo в библиотеках, зарегистрированных в Coq. Библиотеки наследуют структуру файловой системы операционной системы и регестрируются командой Add LoadPath. Физические директории отображаются в логические директории. Стандартные библиотеки Coq зарегестрированы под именем Coq. Модули имеют абсолютные уникальные имена, обозначающие их место в библиотеках Coq. Абсолютное имя - это последовательность идентификаторов, разделенных точками. Так Coq.Arith.Arith - это полное имя модуля Arith, и, так как он находится в eponym поддиректории Arith стандартной библиотеки, он также может быть запрошен командой

Coq < Require Coq.Arith.Arith.

Это может помочь избежать неоднозначности, если где-нибудь в другой ветке библиотек, известных Coq, другой модуль также будет называться Arith. Отметим, что по умолчанию при регистрации библиотек все их содержимое и все содержимое их подкаталогов рекурсивно видно и доступно по коротким (относительным) именам, таким как Arith. Также отметим, что модули и определения не зарегистрированные в библиотеках явно складываются в библиотеку по умолчанию, имеющую имя Scratch.

Скомпилированные файлы загружаются быстро, так как соответствующая development не подвергается проверке типов повторно.

Предупреждение: Coq пока не работает с параметрическими модулями.

3.2 Создание ваших собственных модулей

Вы можете создаь свой модуль, записав команды Coq в файл, скажем, my_module.v. Такой модуль может быть легко загружен в текущем контексте командой Load my_module. Также он может быть скомпилирован командой Compile Module my_module непосредственно в Coq toplevel или в "пакетном" режиме командой coqc. В результате компиляции модуля my_module.v будет создан файл my_module.vo, который может быть перезагружен командой Require my_module.

Если запрашиваемый модуль зависит от других модулей, то они будут запрошены автоматически, но их содержимое не будет доступно. Если вы хотите, чтобы при запросе модуля N используемый им модуль M автоматически становился доступным, вы должны использовать в модуле N команду Require Export M.

3.3 Управление контекстом

Часто бывает трудно запомнить имена всех лемм и определений, доступных в текущем контексте, особенно, если были загружены большие библиотеки. Есть удобная команда Search, которая ищет все известные относительно данного предиката факты. Например, если вас интересуют все леммы об отношении "меньше или равно", просто спросите:

Coq < Search le.
Top.le_n_S: (n,m:nat)(le n m)->(le (S n) (S m))
le_n: (n:nat)(le n n)
le_S: (n,m:nat)(le n m)->(le n (S m))

Новое и еще более удобное средство поиска - это команда SearchPattern. Она позволяет искать теоремы, заключения которых соответствуют заданному образцу, в котором символ ? может быть использован вместо произвольного терма.

Coq < SearchPattern (plus ? ?)=?.
le_plus_minus_r: (n,m:nat)(Peano.le n m)->(plus n (minus m n))=m
mult_acc_aux: (n,s,m:nat)(plus s (mult n m))=(mult_acc s m n)
plus_sym: (n,m:nat)(plus n m)=(plus m n)
plus_Snm_nSm: (n,m:nat)(plus (S n) m)=(plus n (S m))
plus_assoc_l: (n,m,p:nat)(plus n (plus m p))=(plus (plus n m) p)
plus_permute: (n,m,p:nat)(plus n (plus m p))=(plus m (plus n p))
plus_assoc_r: (n,m,p:nat)(plus (plus n m) p)=(plus n (plus m p))
plus_permute_2_in_4:
(a,b,c,d:nat)
(plus (plus a b) (plus c d))=(plus (plus a c) (plus b d))
plus_tail_plus: (n,m:nat)(plus n m)=(tail_plus n m)
plus_O_n: (n:nat)(plus (0) n)=n
plus_Sn_m: (n,m:nat)(plus (S n) m)=(S (plus n m))
mult_n_Sm: (n,m:nat)(plus (mult n m) n)=(mult n (S m))
plus_com: (n,m:nat)(plus n m)=(plus m n)

3.4 Now you are on your own

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

1: This research was partly supported by ESPRIT Basic Research Action ``Types''

This document was translated from L^AT_EX by H^EV^EA.