Coq

Доказательство «на бумаге» ассоциативности композиции функций:

${\displaystyle (f\circ g)\circ h}$

${\displaystyle =\lambda x.(f\circ g)(h~x)}$ ; δ-эквивалентность

${\displaystyle =\lambda x.(\lambda y.f(g~y))(h~x)}$ ; δ-эквивалентность

${\displaystyle =\lambda x.(f(g(h~x)))}$ ; β-эквивалентность

${\displaystyle f\circ (g\circ h)}$

${\displaystyle =\lambda x.f((g\circ h)~x)}$ ; δ-эквивалентность

${\displaystyle =\lambda x.f((\lambda y.g(h~y))~x)}$ ; δ-эквивалентность

${\displaystyle =\lambda x.f(g(h~x))}$ ; β-эквивалентность

По транзитивности равенства:

${\displaystyle (f\circ g)\circ h=f\circ (g\circ h)}$

Доказательство в Coq:

 Definition cf := fun t0 t1 t2 : Type
   => fun (f : t1 -> t2) (g : t0 -> t1) => fun x => f (g x).
 Implicit Arguments cf [t0 t1 t2].
 Notation "f @ g" := (cf f g) (at level 65, left associativity).
 
 Definition cf_assoc := fun (t0 t1 t2 t3 : Type)
   (f : t2 -> t3) (g : t1 -> t2) (h : t0 -> t1)
   => (refl_equal _) : (f @ g) @ h = f @ (g @ h).

cf — определение композиции функций. Notation вводит инфиксное обозначение @ для композиции функций.

cf_assoc — собственно доказательство. Coq основан на изоморфизме Карри — Ховарда, поэтому доказательство есть терм лямбда-исчисления.

fun … => … в Coq обозначает лямбда-абстракцию. Функциям даются имена f, g, h, а их областям определения и областям значений даются имена t0, t1, t2, t3.

Кроме лямбда-абстракции доказательство состоит из refl_equal — аксиомы рефлексивности равенства. Нам нужно привести левую и правую части равенства с помощью βδ-редукций к одному выражению. Coq сам выполняет βδ-редукцию, поэтому доказательство практически пустое.

Чтобы понять роль refl_equal, выполните Check (refl_equal 2). Coq покажет автоматически выведенный тип этого терма, а именно, 2 = 2. Но в доказательстве cf_assoc аргумент refl_equal заменён на подчёркивание. Coq сам может вывести этот аргумент (см. «Вывод значений аргументов из типов»). Это сокращает объём доказательства. Выполнив Print cf_assoc., можно убедиться, что Coq вывел терм (f @ g) @ h вместо подчёркивания.

Тип натуральных чисел определён в стандартной библиотеке индуктивно:

 Inductive nat : Set :=
   | O : nat
   | S : nat -> nat.

Конструкторы ${\displaystyle O}$ и ${\displaystyle S}$ суть ноль и функция, возвращающая следующее число.

Необходимо доказать, что ${\displaystyle n\cdot m=m\cdot n}$. Доказательство коммутативности в арифметике Пеано строится с помощью математической индукции по одному из множителей.

Будут использоваться обозначения, принятые в Coq, чтобы было легче сопоставить оба доказательства.

Выполним индукцию по ${\displaystyle n}$.

База индукции: доказать ${\displaystyle O\cdot m=m\cdot O}$. Высказывание ${\displaystyle O\cdot m=O}$ следует из βδι-преобразования. ${\displaystyle O=m\cdot O}$ доказывается отдельной леммой (см. Coq.Init.Peano.mult_n_O).

Шаг индукции: имея индуктивную гипотезу ${\displaystyle n\cdot m=m\cdot n}$, доказать ${\displaystyle (S~n)\cdot m=m\cdot (S~n)}$. Из βδι-преобразования следует ${\displaystyle (S~n)\cdot m=m+n\cdot m}$. Имеется лемма (см. Coq.Init.Peano.mult_n_Sm), которая утверждает ${\displaystyle m\cdot n+m=m\cdot (S~n)}$. Используем коммутативность сложения и индуктивную гипотезу.

Следующее доказательство скопировано с небольшими изменениями из стандартной библиотеки. Оно использует тактики.

Тактика автоматически генерирует доказательство (или его часть), опираясь на цель (что нужно доказать). Конечно, чтобы тактика сработала, должен существовать алгоритм поиска доказательства. В некоторых случаях тактики могут сильно уменьшить объём доказательства.

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

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

Режим редактирования доказательства (англ. proof editing mode) не запрещает строить доказательство как лямбда-терм. Тактика refine (см. «#Коммутативность умножения в кольце Гротендика») доказать цель с помощью указанного после refine лябмда-терма. refine имеет следующую дополнительную возможность: если в лямбда-терме вместо некоторых подтермов стоит подчёркивание и Coq не может вывести значение подтермов автоматически, то это подчёркивание генерирует подцель. Таким образом, refine может генерировать произвольное количество подцелей.

 Require Import Coq.Arith.Plus.
 
 Definition mult_comm : forall n m, n * m = m * n.
 Proof.
 intros. elim n.
 auto with arith.
 intros. simpl in |- *. elim mult_n_Sm. elim H. apply plus_comm.
 Qed.

intros вводит предпосылки (n и m). elim применяет математическую индукцию, после чего цель доказательства разбивается на две подцели: база и шаг индукции. auto with arith доказывает базу индукции; тактика auto ищет простым перебором подходящую теорему в базе данных теорем и подставляет её в доказательство. В данном случае она находит лемму mult_n_O. В этом можно убедиться, выполнив Show Proof. При доказательстве шага индукции применяются леммы mult_n_Sm, plus_comm, и индуктивная гипотеза H. Имя индуктивной гипотезы было сгенерировано автоматически тактикой intros, второе вхождение тактики. simpl in |- * выполняет βδι-преобразование цели. Хотя она не генерирует доказательства, но она приводит цель к такому виду, который нужен для вывода аргументов тактикой apply plus_comm.

То же доказательство можно выразить лямбда-термом.

 Definition mult_comm := fun n:nat
 => fix rec (m : nat)
 : n * m = m * n
 := match m as m return n * m = m * n with
   | O => sym_eq (mult_n_O _)
   | S pm => match rec pm in _ = dep return _ = n + dep
     with refl_equal =>
       match mult_n_Sm _ _ in _ = dep return dep = _
       with refl_equal => plus_comm _ _ end
     end
   end.

elim n соответствует fix … match … as …. Остальные elim соответствуют match … in _=dep …. В доказательстве с помощью тактик нет нужды указывать конструкторы O и S, так как они выводятся из nat.

 Definition mult_comm := fun n:nat
 => nat_ind (fun m => n * m = m * n)
   (sym_eq (mult_n_O _))
   (fun _ rec =>
     eq_ind _ (fun dep => _ = n + dep)
     (eq_ind _ (fun dep => dep = _)
       (plus_comm _ _) _ (mult_n_Sm _ _))
     _ rec).

Это более компактная, хотя менее наглядная запись. nat_ind и eq_ind называются принципами индукции и являются функциями, сгенерированными согласно структуре индуктивных типов (nat, если nat_ind, и eq, если eq_ind). Тактики вставляют в доказательство именно эти функции.

Как видно, тактики позволяют опускать множество термов, которые можно вывести автоматически.

Это пример использования специализированной тактики ring. Она выполняет преобразования формул, построенных из операций полукольца или кольца.

Кольцо Гротендика конструируется из полукольца следующим образом. int_bipart — носитель кольца — есть вторая декартова степень nat — носителя полукольца.

 Record int_bipart : Set := {pneg : nat; ppos : nat}.

Record не только конструирует декартово произведение множеств, но и генерирует левую (названа pneg) и правую (названа ppos) проекции. Значение ${\displaystyle i}$ из множества int_bipart можно понимать как решение уравнения ${\displaystyle x+(pneg~i)=(ppos~j)}$, где ${\displaystyle x}$ — неизвестная величина. Если ${\displaystyle (pneg~i)>(ppos~j)}$, то решение является отрицательным числом.

Сложение в кольце определено как покомпонентное сложение, то есть pneg левого слагаемого складывается с pneg правого слагаемого, ppos левого слагаемого складывается с ppos правого слагаемого.

 Notation "a !+ b" := (Peano.plus a b) (at level 50, left associativity).
 Definition plus a b := Build_int_bipart
   (pneg a !+ pneg b) (ppos a !+ ppos b).
 Notation "a + b" := (plus a b).

Мы обозначаем сложение в полукольце как «!+» и сложение в кольце как «+».

Умножение определяется так: в часть pneg (это первый аргумент Build_int_bipart) идут произведения разных компонент, в часть ppos (это второй аргумент Build_int_bipart) идут произведения одинаковых компонент.

 Notation "a !* b" := (Peano.mult a b) (at level 40, left associativity).
 Definition mult a b := Build_int_bipart
   (pneg a !* ppos b !+ ppos a !* pneg b)
   (pneg a !* pneg b !+ ppos a !* ppos b).
 Notation "a * b" := (mult a b) (at level 40, left associativity).

Мы обозначаем умножение в полукольце как «!*» и умножение в кольце как «*».

Сначала докажем лемму «если оба компонента int_bipart равны, то int_bipart равны».

 Definition int_bipart_eq_part
   : forall an bn, an = bn -> forall ap bp, ap = bp
   -> Build_int_bipart an ap = Build_int_bipart bn bp.
 Proof.
 refine (fun _ _ eqn _ _ eqp => _).
 refine (eq_ind _ (fun n => _ = Build_int_bipart n _) _ _ eqn).
 refine (f_equal _ eqp).
 Qed.

Теперь докажем коммутативность умножения в кольце, то есть n * m = m * n.

 Require Import ArithRing.
 
 Definition mult_comm : forall n m, n * m = m * n.
 Proof.
 refine (fun n m => int_bipart_eq_part _ _ _ _ _ _); simpl; ring.
 Qed.

Нужно доказать равенство двух int_bipart. Лемма int_bipart_eq_part разбивает нашу цель на две подцели. Первая подцель есть равенство компонент pneg, вторая подцель есть равенство компонент ppos. Увидеть эти подцели можно, если сразу после Proof. выполнить refine (fun n m => int_bipart_eq_part _ _ _ _ _ _). «;» между refine и (simpl; ring) означает, что комбинированная тактика (simpl; ring) доказывает все подцели, генерируемые тактикой refine.

Чтобы доказать «на бумаге», нужно последовательно применить свойства операций полукольца:

${\displaystyle (pneg~n)\cdot (ppos~m)+(ppos~n)\cdot (pneg~m)}$

${\displaystyle =(ppos~m)\cdot (pneg~n)+(ppos~n)\cdot (pneg~m)}$ ; коммутативность умножения

${\displaystyle =(ppos~m)\cdot (pneg~n)+(pneg~m)\cdot (ppos~n)}$ ; коммутативность умножения

${\displaystyle =(pneg~m)\cdot (ppos~n)+(ppos~m)\cdot (pneg~n)}$ ; коммутативность сложения

${\displaystyle (pneg~n)\cdot (pneg~m)+(ppos~n)\cdot (ppos~m)}$

${\displaystyle =(pneg~m)\cdot (pneg~n)+(ppos~n)\cdot (ppos~m)}$ ; коммутативность умножения

${\displaystyle =(pneg~m)\cdot (pneg~n)+(ppos~m)\cdot (ppos~n)}$ ; коммутативность умножения

Тактика ring генерирует все эти преобразования автоматически.