Подробно о Coq: зависимое сопоставление с образцом / forpes.ru

15.11.2023 06:30

andreykl 1 632 Источник

Предисловие

Сопоставление с образцом в Coq на первый взгляд выглядит не сложнее, чем в
большинстве языков программирования, т.е. довольно просто. Правда, это
впечатление остаётся только до тех пор, пока программисту не приходится
столкнуться с зависимыми типами. И тут всё становится гораздо интереснее. Тем
не менее интуицию вполне можно выработать. У автора было желание получше
разобраться с данной темой и выдалось немного свободного времени. Надеемся, что
результат окажется полезен и читателю.

Для кого эта статья

Эта статья предназначена для программистов и специалистов по формальным доказательствам, которые имеют некоторый опыт использования Coq (ориентировочно около года).

Совсем новичкам в Coq предложенные методы, конечно, тоже могут быть полезны. Однако объяснения, хоть и довольно подробны, но всё же не ориентированы на новичков, вследствие чего понимание излагаемого материала может занять несколько больше времени. Поэтому тем, кто только начинает заниматься формальной верификацией и планирует посвятить этому какую-то часть своей жизни, может быть имеет смысл добавить статью в закладки. Чтобы при встрече с описанным вопросом статья оказалась под рукой.

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

Итак, если у вас возникла потребность поглубже разобраться в данной теме, то добро пожаловать!

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

Так же, благодаря прекрасному jscoq можно использовать и онлайн версию IDE с примерами из статьи.

Терминологические замечания

Мы старались придерживаться принятой русскоязычной терминологии которую удалось найти в широко доступных общих работах по данной теме. В частности это "Практикум по математической логике. COQ. В.Н. Крупский, С.Л. Кузнецов"¹. Кроме того, мы сверялись с некоторыми публикации на habr.com, содержащими терминологию^{2 3}.

Мы предлагаем термин "разбирающий" ("сопоставляющий", "с разбором случаев" или просто "с разбором") как замену англицизму "деструктурирующий" для обозначения, например, конструкции let с разбором случаев. Иногда встречающийся термин "разрушающий" в данном случае не подходит, так как является устоявшимся термином для обозначения присваивания после которого изменяется состояние мутабельной переменной (т.е. обычного присваивания в императивных языках программирования).

На наш взгляд новые варианты хорошо согласуются с существующей терминологией: "разбор случаев" и "сопоставление с образцом". Таким образом, мы переводим "destructuring let" как "разбирающее let", "сопоставляющее let", или "let с разбором [случаев]". Соответственно, в более общем случае, "destructuring assignment" мы предлагаем переводить как "разбирающее присваивание", "сопоставляющее присваивание" или "присваивание с разбором [случаев]".

Обычно "сопоставление с образцом" применяется в отношении конструкции match (и подобных), а под "разбором случаев" может подразумеваться как конструкция match (см. например, Крупский-Кузнецов¹), так и применение тактики destruct (или подобных) в режиме построения доказательств. В большинстве случаев в данной статье мы используем словосочетания "сопоставление с образцом", "зависимое сопоставление с образцом" и "разбор случаев" как синонимы, имея ввиду конструкцию match в системе Coq. Если мы говорим о тактиках, используется "разбор случаев".

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

Структура статьи

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

Основные техники при работе с зависимым сопоставлением с образцом

Как уже было замечено, предполагается, что читатель близко знаком с системой Coq, и словосочетания "зависимые типы" и "сопоставление с образцом" по-отдельности не являются чем-то, что нужно объяснять. Предварительное знакомство с сопоставлением с образцом предполагается на уровне уверенного использования выражения match без подвыражений as, in и return.

Успешное использование зависимого сопоставления с образцом в Coq на взгляд автора основывается на следующих составляющих:

Сопоставляющее выражение let, представление о "контексте".
Связывание переменных в подвыражениях as, in и return выражения match, паттерн "конвой".

Рассмотрим каждый из этих пунктов.

Сопоставляющее выражение let и представление о контексте.

Разбирающее выражение let (далее "выражение let",
"сопоставляющее/разбирающее выражение", "let с разбором" или просто "let")
применяется для извлечения аргументов из конструктора в тех случаях, когда тип
имеет единственный конструктор экземпляра. Выражение транслируется в
последовательность выражений match на этапе синтаксического разбора. Нам
понадобится лишь одна форма выражения let с разбором случаев, а именно:

let 'pair a b := x in y

(другие варианты см. в руководстве Coq раздел match⁵).

В данном случае предполагается, что терм x имеет тип A * B, a имеет тип A, b -- B. Терм y может быть сложным, зависеть от a и b и иметь любой тип который подойдёт по контексту.

Пример. Определение функции fst с использованием let.

Inductive prod (A B : Type) : Type := pair (a : A) (b : B).

Arguments pair {A B} a b : assert.

Definition fst {A B} (p : prod A B) : A := let 'pair a _ := p in a.

Функция fst должна возвращать первый компонент пары. Подчёркивание обозначает,
что в данном случае мы просто игнорируем второй аргумент.

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

Рассмотрим пример. Пусть требуется определить выражение типа forall A (x y : A), x = y -> y = x (т.е. доказать симметричность выражения типа eq A x y).

Задача состоит в том, чтобы вернуть конструктор eq_refl типа eq A x y. Если мы попытаемся сделать это без предварительной подготовки, система не примет наше решение.

Fail Definition eq_sym_refl {A} {x y : A} (H : x = y) : y = x := eq_refl.

Ответ системы

The term "eq_refl" has type "y = y" while it is expected to have type "y = x" (cannot unify "y" and "x").

Ответ понятен. Мы не можем создать экземпляр типа eq A x y, а только экземпляр типа eq A x x. Чтобы система посчитала x и y одним и тем же термом, нужно чтобы произошла унификация термов x и y. Унифицировать термы можно следующими способами.

Во-первых, очевидно, используя eq_rect.

Definition eq_sym_eq_rect {A} {x y : A} (H : x = y) : y = x :=
  eq_rect _ (fun x' => x' = x) eq_refl _ H.

Но сам eq_rect использует конструкцию match (можно посмотреть выполнив Print eq_rect.). Перепишем наше определение с использованием match.

Definition eq_sym_match {A} {x y : A} (H : x = y) : y = x :=
  match H with
  | eq_refl => eq_refl
  end.

Такое определение система принимает. Попробуем понять как это происходит. Для этого перепишем определение eq_sym используя язык тактик.

Lemma eq_sym_destruct {A} {x y : A} (H : x = y) : y = x.
Proof.

Вот что мы видим в целях:

A : Type
x, y : A
H : x = y
============================
y = x

Для того чтобы решить цель, можно произвести разбор случаев используя, например, тактику destruct H..

Lemma eq_sym_destruct {A} {x y : A} (H : x = y) : y = x.
Proof.
  destruct H.

После этого происходит унификация термов x и y. То есть система "видит", что это один и тот же терм потому, что он встречается в конструкторе eq_refl. Унифицировав термы, система убирает у из контекста, заменяя все вхождения у на x. После этого цель решается простым применением конструктора eq_refl.

A : Type
x : A
============================
x = x

Примерно то же самое происходит когда мы сопоставляем H с eq_refl в
выражении match: текущий контекст изменяется, переменная y из него
пропадает и вместо её вхождений в цели подставляется переменная x. Система
сравнивает получившуюся цель (x = x) с типом который имеет eq_refl
и ей теперь удаётся вывести нужные параметры конструктора.

Вот как выглядит определение eq_sym с использованием сопоставляющего let:

  Definition eq_sym_let {A} {x y : A} (H : x = y) : y = x :=
    let 'eq_refl := H in eq_refl.

И ещё одно замечание по выражению let. Можно писать так

let e : y = x := let 'eq_refl := H in eq_refl in RES

где RES -- некоторое конечное выражение. Например,

  Definition eq_sym_let {A} {x y : A} (H : x = y) : y = x :=
    let e : y = x := let 'eq_refl := H in eq_refl in e.

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

Философско-лирическое отступление о том, почему для профессионального роста важно работать в сильной команде, навеянное автору статьи темой разбирающего let (для тех, кому интересно), находится в конце статьи.

Связывание переменных в подвыражениях as, in и return выражения match. Паттерн конвой.

Выражения as и in позволяют связать термы в типах сопоставляемых выражений с типом возвращаемого значения в выражении return. Рассмотрим пример, с которым мы будем работать в дальнейшем. Пример взят из замечательной книги Coq'Art: The Calculus of Inductive Constructions Ива Берто и Пьера Кастерана (Yves Bertot, Pierre Castéran), английскую версию которой можно легко купить, а французская версия свободно доступна для скачивания⁶ (Для любителей: обязательно оцените картину на официальной страничке книги!).

Задача. Предлагается определить тип данных binary_word для кодирования двоичных машинных слов. Например, binary_word 8 будет соответствовать 8-битному слову. Затем предлагается определить для этого типа две функции: binary_word_concat, которая сцепляет два двоичных слова и binary_word_or, которая действует аналогично оператору | языка си, т.е. принимает на входе два бинарных слова и возвращает слово полученное применением логического или к соответствующим битам двух исходных слов.

Определим двоичное слово следующим образом.

Inductive binary_word : nat -> Set :=
| bw1 (b : bool) : binary_word 1
| bwn {n} (b : bool) : binary_word n -> binary_word (S n).

Как видно, у нас два конструктора: базовый и рекурсивный. Базовый конструктор хранит один бит. Рекурсивный конструктор принимает слово из n битов и добавляет к нему ещё один бит.

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

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

Попробуем написать самую простую версию.

  Fail Fixpoint binary_word_or {n} (w1 w2 : binary_word n) : binary_word n :=
    match w1, w2 with
    | bw1 b1, bw1 b2 => bw1 (b1 || b2)
    | bwn b1 pw1, bwn b2 pw2 => bwn (b1 || b2) (binary_word_or pw1 pw2)
    end.

В коде мы разбираем только пары одинаковых конструкторов. Невозможность других пар следует из того факта, что оба слова имеют одинаковый тип. А для одного и того же n подходит только один конструктор: либо bw1 когда n имеет значение 1, либо bwn когда n больше единицы. Тем не менее, для системы этот факт неочевиден и мы получаем следующее сообщение об ошибке.

The command has indeed failed with message:
Non exhaustive pattern-matching: no clause found for patterns bw1 _, bwn _ _

Система сообщает о неполном сопоставлении с образцом. Чтобы избавиться от этой ошибки, можно воспользоваться одним из трёх следующих способов:

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

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

  Fail Fixpoint binary_word_or {n} (w1 w2 : binary_word n) : binary_word n :=
    match w1, w2 with
    | bw1 b1, bw1 b2 => bw1 (b1 || b2)
    | bwn b1 pw1, bwn b2 pw2 => bwn (b1 || b2) (binary_word_or pw1 pw2)
    | bw, _ => bw
    end.

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

The command has indeed failed with message:
In environment
binary_word_or : forall n : nat, binary_word n -> binary_word n -> binary_word n
n : nat
w1 : binary_word n
w2 : binary_word n
n0 : nat
b1 : bool
pw1 : binary_word n0
b := bwn b1 pw1 : binary_word (S n0)
w0 : binary_word (S n0)
n1 : nat
b2 : bool
pw2 : binary_word n1
The term "pw2" has type "binary_word n1" while it is expected to have type "binary_word n0".

Видно, что в контексте ошибки термы w1 и w2 имеют одинаковый тип. Однако термы pw1 и pw2, представляющие собой базовые слова для термов w1 и w2 соответственно, имеют типы binary_word n0 и binary_word n1. Т.е. мы видим, что типы базовых слов различаются. А тип функции binary_word предполагает, что переданные аргументы должны быть одного и того же типа. При этом для системы неочевидно из контекста, что n равно S n0. Чтобы это было очевидно для системы, термы n и S n0 должны быть конвертируемы, т.е. должна существовать цепочка редукций, которые приводят один из термов к другому (подробнее о редукции см. в руководстве Coq раздел conversion⁷). Стоит отметить, что совершенно аналогичная ситуация возникнет при написании binary_word_or в режиме построения доказательств (т.е. с помощью языка тактик). В аналогичной ситуации мы будем иметь аналогичный контекст и прежде чем применить рекурсивный вызов, нам нужно будет показать, что термы pw1 и pw2 имеют один и тот же тип.

Задачка 1! Eсли кому-то интересна задачка для самостоятельной работы, то написание binary_word_or с помощью языка тактик представляет собой хоть и не совсем относящееся к теме сопоставления с образцом, но тем не менее весьма любопытное упражнение. Решение в конце статьи.

Далее, будем использовать выражение "снаружи выражения match" для обозначения термов и контекста который мы имеем либо 1) до начала выражения match; либо 2) после окончания выражения match; либо 3) после слова match и до слова with. Будем использовать выражения "внутри выражения match" и "внутри ветки выражения match" для обозначения термов и контекста который мы имеем справа от стрелки => в выражении match. Выражение "в образце" или, иногда, "в конструкторе", применительно к выражению match обозначает, что терм встречается слева от стрелки => в выражении match.

Приведём несколько примеров использования данного соглашения. В следующем примере (см. ниже) eq_refl, n1', n2', n1' = n2' находятся снаружи, а, например, fun _ bw1 (b1 || b2) -- внутри выражения match и внутри первой ветки. Термы b1 и b2 встречаются впервые в образце выражения match.

Итак, наша новая задача -- это показать что термы pw1 и pw2 имеют один и тот же тип. Рассмотрим контекст приведённый выше внимательнее. Во-первых заметим, что кроме термов, которым мы дали имена (при сопоставлении с образцом или полученных в качестве аргументов), появились ещё термы b, w0, n0 и n1. Термы n0 и n1 -- это длины слов pw1 и pw2 соответственно. Они впервые появляются в выражении match в образце и у нас не фигурируют, поскольку мы не дали им имена при сопоставлении. Термы b' и w0 это синонимы терма w1 созданные системой во время работы.

Снаружи выражения match очевидно (и для человека и системы), что термы w1 и w2 имеют один и тот же тип. Однако в процессе iota-редукции (редукции выражения match) одна и та же переменная n получила два разных синонима, S n0 и S n1 (второго в контексте сейчас не видно).

Это случилось, в сущности, потому, что в общем случае два разных терма могут иметь два разных разбиения. Так, в нашем примере, возможен вариант | bw1 _, bwn _ _. Правда, в только что предложенном варианте разбиения невозможно (для нашего индуктивного типа), чтобы bw1 и bwn имели один и тот же тип (в частности, с одним и тем же натуральным числом n). Но для системы данный факт очевидным не является.

Синтаксические правила языка диктуют системе правила именования синонимов внутри match. Cинонимы составляются из имён данных нами (или системой) в образцах выражения match. По правилам языка при сопоставлении мы (или система) обязаны дать два разных имени в двух разных образцах для сопоставления.

В итоге, внутри выражения match мы имеем два разных синонима для одного и того же терма n который мы видим снаружи выражения. Снаружи выражения match вполне очевидно, что это синонимы одного терма и, следовательно, они равны. Но эта информация теряется в процессе сопоставления.

Чтобы получить информацию о равенстве термов внутри выражения match, нам потребуется передать её снаружи. Для этого мы воспользуемся выражениями in и return (так же попутно поименуем переменные для удобства чтения).

  Fail Fixpoint binary_word_or {n} (w1 w2 : binary_word n) : binary_word n :=
    match
      w1 in binary_word n1', w2 in binary_word n2'
      return n1' = n2' -> binary_word n1'
    with
    | bw1 b1, bw1 b2 => fun _ => bw1 (b1 || b2)
    | @bwn n1 b1 pw1, @bwn n2 b2 pw2 => fun e =>
        bwn (b1 || b2) (binary_word_or pw1 pw2)
    | bw, _ => fun _ => bw
    end eq_refl.

С помощью выражения in мы дали переменной n синоним n1' в случае когда она встречается в типе терма w1 и синоним n2' когда переменная n встречается в типе терма w2. Так же с помощью return мы изменили тип возвращаемого выражением match значения. Теперь выражение match будет возвращать функцию типа n1' = n2' -> binary_word n1'.

Этот трюк, а именно "нахождение способа закодировать свободные переменные, от которых зависит тип результата выражения match так, чтобы в подвыражении return можно было выразить связь" и называется "паттерном конвой". "В частности, мы можем расширить match так, чтобы оно возвращало функции над свободными переменными чьи типы мы хотели бы вычислить". Что мы, собственно, здесь и делаем. (Цитата взята из другой замечательной книги, а именно Certified Programming with Dependent Types от Адама Клипалы. Английскую версию книжки можно купить, а последний черновик свободно доступен для скачивания на домашней страничке книги⁸. Цитата переведена автором статьи).

Конечно же, нам нужно передать выражению match дополнительный аргумент типа n1' = n2' чтобы тип получившегося значения совпал с типом, ожидаемым функцией binary_word_or. Снаружи выражения match для системы очевидно, что термы n, n1' и n2' суть один и тот же терм, поэтому она сможет унифицировать n1' и n2' чтобы создать экземпляр eq_refl : n1' = n2'. Конечно, каждая ветка выражения match должна теперь возвращать функцию.

Рассмотрим ответ системы.

The command has indeed failed with message:
In environment
binary_word_or : forall n : nat, binary_word n -> binary_word n -> binary_word n
n : nat
w1 : binary_word n
w2 : binary_word n
n1 : nat
b1 : bool
pw1 : binary_word n1
b := bwn b1 pw1 : binary_word (S n1)
w0 : binary_word (S n1)
n2 : nat
b2 : bool
pw2 : binary_word n2
e : S n1 = S n2
The term "pw2" has type "binary_word n2" while it is expected to have type "binary_word n1".

Как видно, система представила термы n1' и n2' в виде S n1 и S n2 соответственно. И подставила эти синонимы везде где встречались термы n1' и n2' внутри рассматриваемой ветки выражения match. Затем мы связали переданный в качестве аргумента терм eq_refl с именем e, и теперь у нас в контексте есть равенство e : S n1 = S n2!

Дальше нам очень пригодится let с разбором. Первая мысль, конечно, написать примерно так

  Fail Fixpoint binary_word_or {n} (w1 w2 : binary_word n) : binary_word n :=
    match
      w1 in binary_word n1', w2 in binary_word n2'
      return n1' = n2' -> binary_word n1'
    with
    | bw1 b1, bw1 b2 => fun _ => bw1 (b1 || b2)
    | @bwn n1 b1 pw1, @bwn n2 b2 pw2 => fun e =>
       let pw2' : binary_word n1 := let 'eq_refl := e in pw2 in
       bwn (b1 || b2) (binary_word_or pw1 pw2')
    | bw, _ => fun _ => bw
    end eq_refl.

Таким образом мы хотели бы изменить тип выражения pw2 чтобы получить выражение pw2' которое подходит нам по типу, попытавшись для этого запустить унификацию путём разбора выражения e типа S n1 = S n2.

The command has indeed failed with message:
In environment
binary_word_or : forall n : nat, binary_word n -> binary_word n -> binary_word n
n : nat
w1 : binary_word n
w2 : binary_word n
n1 : nat
b1 : bool
pw1 : binary_word n1
b := bwn b1 pw1 : binary_word (S n1)
w0 : binary_word (S n1)
n2 : nat
b2 : bool
pw2 : binary_word n2
e : S n1 = S n2
The term "pw2" has type "binary_word n2" while it is expected to have type "binary_word n1".

Как и ожидалось, в данном случае это ни к чему не приводит, поскольку из факта S n1 = S n2 равенство n1 = n2 напрямую не следует. Бесплодна, конечно же, и подобная попытка в языке тактик (тактика destruct). В языке тактик для получения равенства n1 = n2 нужно воспользоваться свойством инъективности конструкторов. Мы могли бы использовать, например, injection e as e или inversion e (пример см. в решении данной задачи в режиме доказательств в конце статьи). Хотя, конечно, и в режиме написания кода мы можем использовать любые подходящие леммы и теоремы как из стандартной библиотеки, так и написанные нами (примеры будут ниже).

Тем не менее, аналогия с контекстом, или, вернее, с правилами формирования контекста из режима доказательств здесь начинает "подтекать" (ведь все аналогии рано или поздно "протекают"...).

Первая "протечка" аналогии состоит в том, что мы можем написать let e' : n1 = n2 := let 'eq_refl := e in eq_refl in .. и после этого в контексте даже появится нечто похожее на равенство e' : n1 = n2. Хотя прямо из S n1 = S n2 факт n1 = n2 и не следует.

Вторая "протечка" состоит в том, что имея нечто похожее на равенство e' : n1 = n2 мы всё-таки не сможем затем разобрать его для унификации теомов n1 и n2.

Вероятно, вторую "протечку" не совсем верно считать "протечкой", а скорее наоборот, подтверждением аналогии, т.к. факта n1 = n2 в контексте у нас всё таки нет. Тем не менее, работать с контекстом в режиме программирования немного сложнее.

  Fail Fixpoint binary_word_or {n} (w1 w2 : binary_word n) : binary_word n :=
    match
      w1 in binary_word n1', w2 in binary_word n2'
      return n1' = n2' -> binary_word n1'
    with
    | bw1 b1, bw1 b2 => fun _ => bw1 (b1 || b2)
    | @bwn n1 b1 pw1, @bwn n2 b2 pw2 => fun (e : S n1 = S n2) =>
       let e' : n1 = n2 := let 'eq_refl := e in eq_refl in
       let pw2' : binary_word n1 := let 'eq_refl := e' in pw2 in
       bwn (b1 || b2) (binary_word_or pw1 pw2')
    | bw, _ => fun _ => bw
    end eq_refl.

The command has indeed failed with message:
In environment
binary_word_or : forall n : nat, binary_word n -> binary_word n -> binary_word n
n : nat
w1 : binary_word n
w2 : binary_word n
n1 : nat
b1 : bool
pw1 : binary_word n1
b := bwn b1 pw1 : binary_word (S n1)
w0 : binary_word (S n1)
n2 : nat
b2 : bool
pw2 : binary_word n2
e : S n1 = S n2
e' := let 'eq_refl in (_ = n) := e return match n with
                                          | 0 => ?P
                                          | S n0 => n1 = n0
                                          end in eq_refl : n1 = n2
The term "pw2" has type "binary_word n2" while it is expected to have type "binary_word n1".

Часто, если в контексте уже есть то, что нам нужно в виде, например, факта H (т.е. человеку очевидно, что из факта H, находящегося в контексте, следует требуемый факт), то бывает нужно ещё немного "помассажировать" факт H, чтобы система смогла сделать необходимый вывод.

Мы пользуемся следующим набором инструментов для такого "массажа": явное типизирование, леммы eq_sym, eq_trans и похожие, а так же учитываем условное правило "переписывания слева направо".

Явное типизирование означает, что приходящим аргументам, а так же термам создаваемым с помощью выражения let явно приписывается тип. Это помогает заметно быстрее ориентироваться. Иногда такое типизирование нельзя опустить (подобный случай будет рассмотрен в следующем разделе статьи).

Использование лемм eq_sym и eq_trans обычно самоочевидно, поэтому не будем подробно останавливаться на этом пункте (пример использования eq_sym будет дан ниже в тексте статьи, пример использования eq_trans в дополнении).

Обсудим правило переписывания слева направо. Положим, у нас есть необходимость переписать какой-то терм (например, n2) в типе некоего терма (pw2 : binary_word n2) на некий другой терм (n1 в нашем случае). В таком случае равенство, которое мы переписываем, должно иметь форму похожую на нужную тактике rewrite по умолчанию (по умолчанию rewrite переписывает слева направо).

В нашем случае rewrite не смогла бы переписать уравнение e' : n1 = n2 в терме pw2 : binary_word n2 (мы немного упрощаем когда говорим о n1 = n2). Говоря конкретнее, условно rewrite e' in pw2 не сработает. Сработает (условно) rewrite <- e' in pw2, но нам нужно именно поведение rewrite по умолчанию. Подытоживая, в нашем случае нужно равенство n2 = n1 вместо n1 = n2.

  Fixpoint binary_word_or_pre {n} (w1 w2 : binary_word n) : binary_word n :=
    match
      w1 in binary_word n1', w2 in binary_word n2'
      return n1' = n2' -> binary_word n1'
    with
    | bw1 b1, bw1 b2 => fun _ => bw1 (b1 || b2)
    | @bwn n1 b1 pw1, @bwn n2 b2 pw2 => fun (e : S n1 = S n2) =>
       let e' : n2 = n1 := let 'eq_refl := e in eq_refl in
       let pw2' : binary_word n1 := let 'eq_refl := e' in pw2 in
       bwn (b1 || b2) (binary_word_or_pre pw1 pw2')
    | bw, _ => fun _ => bw
    end eq_refl.

Финальная для этой части статьи версия кода выглядит так.

  Fixpoint binary_word_or_good {n} (w1 w2 : binary_word n) : binary_word n :=
    match
      w1 in binary_word n1', w2 in binary_word n2'
      return n1' = n2' -> binary_word n1'
    with
    | bw1 b1, bw1 b2 => fun _ => bw1 (b1 || b2)
    | @bwn n1 b1 pw1, @bwn n2 b2 pw2 => fun e =>
       let pw2' : binary_word n1 := let 'eq_refl := eq_sym e in pw2 in
       bwn (b1 || b2) (binary_word_or_good pw1 pw2')
    | bw, _ => fun _ => bw
    end eq_refl.

Здесь, чтобы развернуть равенство e используется eq_sym и результат разбирается сразу, без заведения дополнительных переменных. Любопытно, что для "переписывания" не обязательно предоставлять системе равенство n2 = n1, а достаточно равенства S n2 = S n1. Здесь можно ещё раз заметить, что работа системы в режиме построения доказательств и в режиме написания кода немного различается.

Позволим себе ещё одно замечание по процессу. Конечно, после наработки интуиции код пишется довольно быстро и необходимость в дополнительных переменных пропадает практически полностью (например, в binary_word_or_pre дополнительно заведена e', в отличие от binary_word_or_good где использование дополнительных переменных уменьшено). Но, когда встречаются сложности с написанием, мы стараемся вносить в контекст всё что кажется близким к нужному результату. Обычно такой подход позволяет проще и быстрее строить решения. Это происходит за счёт того, что для достижения очередного результата можно быстро попробовать разобрать несколько разных термов по очереди, меняя для этого иногда лишь имя сопоставляемого терма в конструкции let.

О результате. Можно сказать, что на данном этапе описание самых важных техник для работы с зависимым сопоставлением с образцом, в основном, закончено.

Последняя версия выглядит, конечно, немного простовато. В том смысле, что словосочетание "зависимое сопоставление с образцом" вызывает, по крайней мере у автора, гораздо больше пиетета, чем получившийся код. И, возможно, кто-то глядя на результат скажет даже, что и не стоило писать об этом статью... НО! В таком случае автор просит вас не спешить с выводами! Хочется заверить, что если приложить ещё немного усилий, то мы вполне сможем получить что-то весьма похожее на первый пример в следующем разделе (который, согласитесь, внушает к себе уже гораздо больше уважения!).

Нет предела совершенству. Невозможный код и работа с ним

Мы уже встречались с невозможным кодом (т.е. с кодом, который никогда не выполнится), когда писали binary_word_or_good. Тогда, в невозможной ветке мы просто вернули подходящий по типу аргумент, посчитав, что если код никогда не выполнится, то и не важно, что именно оттуда возвращать. Рассмотрим ещё два подхода к работе с невозможным кодом.

Два подхода отражают тот факт, что в Coq есть два вида невозможного кода: 1) невозможный код, который система всё таки считает возможным и 2) невозможный код, который система распознаёт как невозможный.

Невозможный код, который система тем не менее считает возможным.

Пример невозможного кода с которыми мы встретились выше, когда возвращали удобное значение в ветке, которую мы считали невозможной, относится к этому случаю. Т.е. Coq считает такие участки кода на самом деле возможными и, конечно же, требует 1) их наличия 2) чтобы возвращаемое такими участками выражение правильно типизировалось.

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

Этот способ особенно подходит в том числе когда на практике бывает не так просто вернуть подходящее значение: типы могут быть довольно сложными, подходящие по типу экземпляры могут не присутствовать в текущем контексте, а конструкторы экземпляров иногда требуют множества параметров. Все эти факторы, как вместе так и по отдельности, могут заметно затруднять создание подходящего значения. А когда экземпляр всё таки написан, код зачастую получается довольно громоздким и, уж конечно, требует от автора комментария. Решение, представленное в коде ниже является самодокументируемым и лаконичным. Кроме того, оно является проверенным системой доказательством невозможности ветки, что так же может быть полезно, и на наш взгляд в общем случае выглядит предпочтительнее.

Итак, рассмотрим следующий код (взят с официальной странички книги Coq'Art.⁶, так же можно найти код на github⁹).

Module CoqArt.
	Inductive binary_word : nat -> Set :=
	| bw0 :  binary_word 0
	| bwS (p : nat)(b:bool)(w: binary_word p) : binary_word (S p).

    Lemma discriminate_O_S {p:nat}:  0 = S p -> False.
	Proof.
		intros;discriminate.
	Qed.

	Lemma  discriminate_S_O {p:nat}:  S p = 0 -> False.
	Proof.
		intros;discriminate.
	Qed.

	Fixpoint binary_word_or (n:nat)(w1:binary_word n) {struct w1}:
		binary_word n -> binary_word n :=
	match w1 in binary_word p return binary_word p -> binary_word p with
		bw0 =>
			(fun w2:binary_word 0 =>
				match w2 in binary_word p' return p'=0->binary_word p' with
					bw0 =>
						(fun h => bw0)
					| bwS q b w2' =>
						(fun h => False_rec (binary_word (S q)) (discriminate_S_O h))
	            end (refl_equal 0))
	   | bwS q b1 w1' =>
		   (fun w2:binary_word (S q) =>
			   match w2 in binary_word p' return S q=p'->binary_word p' with
				   bw0 =>
					   (fun h => False_rec (binary_word 0) (discriminate_S_O h))
				   | bwS q' b2 w2' =>
					   (fun h =>
						   bwS q'
						   (orb b1 b2)
						   (binary_word_or q'
						   (* this use of eq_rec transforms w1' into an element of (binary_word (S q'))
							   instead of (binary_word (S q)), thanks to the equality h. *)
							   (eq_rec (S q)
							   (fun v:nat => binary_word (pred v))
								   w1'
								   (S q')
								   (h:S q=S q'))
								   w2'))
	           end (refl_equal (S q)))
	end.
End CoqArt.

Здесь мы подробно остановимся лишь на важных для нас моментах, оставляя
возможность пытливому читателю разобрать оставшиеся вопросы самостоятельно.

Во-первых, обратим внимание на определение индуктивного типа. В отличие от написанного нами выше, данное определение начинается с пустого конструктора. Благодаря такому определению по форме натурального числа в типе можно точно сказать, какой конструктор был использован. Если натуральное число n в типе binary_word n имеет форму O (binary_word O), значит использовался конструктор bw0, если же n имеет форму S n' (binary_word (S n')), то был использован конструктор bwS. Отметим здесь так же удачные имена конструкторов.

Далее идут две леммы: discriminate_O_S и discriminate_S_O. Они просто принимают на вход противоречие и возвращают экземпляр типа False, который в дальнейшем будет весьма удобен для получения любого подходящего по типу значения.

Общий смысл паттерна конвой, который применили авторы в двух внутренних выражениях match тот же, что и в нашем примере: снаружи выражения match система распознаёт равенство и позволяет передать конструктор eq_refl (для параметризации конструктора аргументом здесь используется обёртка refl_equal). Но передавая снаружи равенство, в одном из случаев (для каждого внутреннего выражения match) мы получаем доказательство противоречия! Конечно же, эти ветки кода никогда не выполнятся, т.е. это невозможный код. И противоречие именно это и показывает. Используя полученное противоречие, мы, далее, легко получаем подходящее по типу значение с помощью индуктивного принципа False_rect.

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

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

Изменим нашу версию binary_word_or_good добавив в неё данное решение.

  Lemma discriminate_bwn_SO_n {n} (w : binary_word n)
    :
    match w with
    | bw1 _ => False
    | _ => True
    end
    -> 1 = n
    -> False.
  Proof.
    remember w as w2 eqn:Heq.
    destruct w as [b | b n w]; intros H **; [subst; destruct H|].
    destruct w; discriminate.
  Qed.

  Fixpoint binary_word_or {n} (w1 w2 : binary_word n) : binary_word n :=
    match
      w1 in binary_word n1', w2 in binary_word n2'
      return n2' = n1' -> binary_word n1'
    with
    | bw1 b1, bw1 b2 => fun _ => bw1 (b1 || b2)
    | @bwn n1 b1 pw1, @bwn n2 b2 pw2 => fun e =>
      bwn (b1 || b2) (binary_word_or pw1 (let 'eq_refl := e in pw2))
    | bw1 _, bwn _ _ as bw => fun e =>
      False_rect _ (discriminate_bwn_SO_n bw I (eq_sym e))
    | bwn _ _ as bw, bw1 _ => fun e =>
      False_rect _ (discriminate_bwn_SO_n bw I e)
    end eq_refl.

Здесь есть некоторые отличия от предыдущего решения (из Coq'Art), но они чисто
технические. Во-первых, немного отличается форма вспомогательной леммы: у нас
используется сравнение с единицей. Во-вторых, мы требуем определённую форму
конструктора, а именно bwn, отсекая bw1 с помощью False. В остальном
решение, которое использовано нами, совершенно аналогично приведённому в примере
выше: мы получаем доказательство противоречия внутри невозможных веток выражения
match, передавая в него снаружи доказательство равенства.

Кроме того, есть так же два отличия от нашего предыдущего решения: равенство n1' = n2' развёрнуто, так что внутрь выражения match передаётся n2' = n1', это нужно чтобы уменьшить использования eq_sym; так же мы убрали промежуточную переменную pw2'.

Задачка 2! Для желающих сделать перерыв и решить несложную задачку. Докажите и используйте в теле функции binary_word_or вместо discriminate_bwn_SO_n следующую лемму. (Решение в конце статьи).

Lemma discriminate_bwn_SO_n' {n b w'} (w : binary_word (S n)) 
  : w = bwn b n w' -> 1 = S n -> False.

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

Далее мы рассмотрим версию binary_word_or в которой система считает невозможный код невозможным. Для этого нам придётся изменить определение типа binary_word.

Невозможный код, который система признаёт невозможным.

Когда Coq распознаёт какую-то ветку кода как невозможную, то он 1) не требует её наличия и 2) позволяет вернуть в данной ветке абсолютно любое значение, не зависимо от того, подходит ли оно по типу или нет.

Первый пример невозможного кода который система считает невозможным мы возьмём из руководства Coq ⁵.

Inductive listn : nat -> Set :=
| niln : listn 0
| consn : forall n:nat, nat -> listn n -> listn (S n).

Definition tail n (v: listn (S n)) :=
  match v in listn (S m) return listn m with
  | niln => False_rect unit
  | consn n' a y => y
  end.

В данном фрагменте кода тип listn представляет собой тип списка, для каждого
экземпляра которого в типе этого экземпляра указано количество элементов,
которые экземпляр содержит. Например, если l : listn 3, то это значит, что в
l ровно три элемента.

Приведённое выше определение tail на самом деле не требует написания случая для niln. Это легко проверить просто закоментировав строчку с конструктором.

Inductive listn : nat -> Set :=
| niln : listn 0
| consn : forall n:nat, nat -> listn n -> listn (S n).

Definition tail n (v: listn (S n)) :=
  match v in listn (S m) return listn m with
  (* | niln => False_rect unit *)
  | consn n' a y => y
  end.

Система по прежнему принимает такое решение. Кроме того, у нас не получится
вернуть значение False_rect unit как подходящее по типу, если мы не
находимся в невозможной ветке. False_rect unit -- это способ самодокументации
кода в таких случаях. Оставить строчку и вернуть False_rect unit может быть
удобно, например, когда имеется множество конструкторов. В таких случая код
стараются писать однообразно, для того чтобы легче было в нём ориентироваться.
Это значит, что конструкторы при сопоставлениях с образцом будут идти в одном и
том же порядке. При чтении кода, если какой-то конструктор отсутствует на месте,
это может значить что разработчик либо перепутал порядок либо переставил
конструкторы местами намеренно, что заставит потратить дополнительное время на
выяснение ситуации.

Закоментированный конструктор с комментарием, или, ещё лучше, ветка возвращающая False_rect unit является одновременно и прекрасной документацией, и доказательством невозможности данной ветки. Хотя, конечно же, свойством быть доказательством невозможности ветки в данном случае, как уже упоминалось, обладает и любое другое неподходящее по типу значение. Однако, всё же, любое другое значение может вводить в заблуждение. False_rect unit таким недостатком не обладает.

Попробуем теперь разобраться, как системе удаётся распознать ветку с конструктором niln как невозможную. Обратим внимание на определение типа listn. Видно, что каждый из конструкторов имеет уникальную форму индекса nat: конструктор niln имеет тип listn 0, а consn имеет тип listn (S n). Именно различие форм индексов у типов разных конструкторов и позволяет системе определять, что некоторая ветка является невозможной. В определении tail указано, что индекс аргумента имеет форму S n, а так как 0 непредставим в виде S n, то при сопоставлении с конструкторами система может однозначно определить, что ветка с niln является невозможным кодом.

Вернёмся к последнему примеру binary_word_or и разберём этот вопрос немного подробнее. Так как в нашем типе binary_word форма индекса от конструктора к конструктору не отличается (для обоих конструкторов индекс в типе имеет форму S n), то различить ветки исходя из формы натурального числа в типе не удаётся:

Когда мы сопоставляем w1 с bw1, система вычисляет, что n имеет вид S O. Далее система попытается подставить вычисленное n в тип, получив w2 : binary_word (S O). Но, так как система в данный момент считает, что оба возможных конструктора терма w2 могут иметь тип binary_word (S O), то исключить ни один из двух возможных конструкторов для w2 не удаётся. ("В данный момент" здесь употреблено в том смысле, что для доказательства невозможности нужны пусть и довольно простые, но всё же нетривиальные вычисления).
Точно такая же ситуация возникает при сопоставлении w1 с конструктором bwn. После сопоставления мы имеем n вида S n', но любой возможный конструктор терма w2 может иметь тип binary_word (S n), поэтому система опять не может исключить ни один из двух возможных конструкторов для w2.

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

Задача. Написать версию binary_word_or в которой невозможные ветки кода будут распознаваться системой как невозможные.

Лучше представляя себе то, как система проводит анализ невозможности той или иной ветки кода, мы можем сделать предположение, что для нашего типа binary_word вряд ли получится построить решение, в котором система распознавала бы невозможные ветки как невозможные. (По крайней мере нам этого сделать не удалось. Если кто-то из читателей знает способ сделать это, может быть и экзотический, пожалуйста, не сочтите за труд и вышлите автору пример кода).

Определим новый тип binary_word в модуле BinaryWord2.

Module BinaryWord2.

Inductive binary_word : nat -> Set :=
| bw1 (b : bool) : binary_word 1
| bwn {n} (b : bool) : binary_word (S n) -> binary_word (S (S n)).

End BinaryWord2.

Мы видим, что в данном случае по форме натурального числа в типе можно
однозначно определить, какой именно конструктор был использован для создания
терма. Например, если w : binary_word (S O), то при создании w использовался
конструктор bw1, если же w : binary_word (S (S n)), то при создании w был
использован конструктор bwn.

Определим функцию binary_word_or внутри модуля BinaryWord2.

  Fixpoint binary_word_or {n} (w1 w2 : binary_word n) : binary_word n :=
    match w1 in binary_word n1'
          return binary_word n1' -> n1' = n1' -> binary_word n1' with
    | bw1 b1 =>
        fun '(bw1 b2) _ => bw1 (b1 || b2)
    | @bwn n1 b1 pw1 =>
        fun '(@bwn n2 b2 pw2) (e : S (S n2) = S (S n1)) =>
          bwn (b1 || b2) (binary_word_or pw1 (let 'eq_refl := e in pw2))
    end w2 eq_refl.

Как видно, лишних веток нет. Кроме того, так как теперь система может убедиться, что в каждой ветке полученной при сопоставлении w1 возможен только один конструктор для w2, то мы можем сопоставить ожидаемый конструктор с образцом непосредственно при определении анонимной функции (т.е. при определении аргументов для выражения fun). Вместо такого сопоставления можно было бы использовать обычное выражение match или его краткую форму let. Но от выражения fun отказаться в данном случае всё равно не получится, так как это выражение является частью паттерна конвой.

Паттерн конвой используется для связывания вычисленного значения n1', полученного при анализе конструктора w1, с типом переданного в анонимную аргумента w2 и с возвращаемым из выражения match значением. Так же с помощью паттерна конвой передаётся дополнительный параметр позволяющий показать соответствие типа терма pw2 значению, ожидаемому рекурсивным вызовом.

Параметр, который внешне выглядит бесполезным (n1' = n1') внутри принимает форму S (S n2) = S (S n1). Так получается потому, что терм n1' связан в выражении match сразу с двумя различными копиями терма n. Из-за того, что n1' можно связать как с S (S n1), так и с S (S n2), возникает неоднозначность, и система не связывает окончательно n ни с одним из возможных значений. Поэтому при получении аргумента в анонимной функции мы можем связать различные копии n1' с подходящими переменными так, как нам удобно. После того как связывание произошло, изменить тип темра e уже не удастся. Но мы вполне могли бы написать (e : S (S n1) = S (S n2)) вместо (e : S (S n2) = S (S n1)) и система типизировала бы терм e подобным образом без ошибок.

Задачка 3. Напишите binary_word_concat для индуктивного типа BinaryWord2.binary_word. Решение в конце статьи. Указание. Автор не использовал для решения этой задачи зависимое сопоставление с образцом.

Задачка 4. Определите binary_word_or для варианта индуктивного типа из модуля CoqArt.binary_word. Решение в конце статьи.

Решения задач, дополнение и философско-лирическое отступление

Решение задачки 1: binary_word_or, написанная с помощью языка тактик.

  Lemma binary_word_or_lemma : forall n (w1 w2 : binary_word n), binary_word n.
  Proof.
    fix F 2.
    intros n w1 w2.
    destruct w1 as [b1|n1 b1 pw1].
    { remember 1 as x eqn:Ex.
      remember w2 as w2' eqn:Ew2.
      destruct w2 as [b2|n2 b2 pw2].
      - apply (bw1 (b1 || b2)).
      - (* impossible case. we could just use `apply w2'` to solve the goal *)
        (* so, what we have below is just for fun *)
        injection Ex as Ex.
        subst n2.
        inversion pw2.
    }
    { remember (S n1) as x eqn:Ex.
      destruct w2 as [b2|n2 b2 pw2].
      - (* impossible case, so we just supply an appropriate value *)
        apply (bw1 true).
      - (* here we have 2 different types for terms pw1 and pw2 *)
        injection Ex as Ex.
        rewrite Ex in *.
        apply (bwn (b1 || b2) (F _ pw1 pw2)).
    }
  Qed.

Решение задачки 2: discriminate_bwn_SO_n' вместо discriminate_bwn_SO_n в теле функции binary_word_or.

  Lemma discriminate_bwn_SO_n' {n b pw} (w : binary_word (S n))
    : w = bwn b pw -> 1 = S n -> False.
  Proof.
    intros; destruct pw; discriminate.
  Qed.

  Fixpoint binary_word_or' {n} (w1 w2 : binary_word n) : binary_word n :=
    match
      w1 in binary_word n1', w2 in binary_word n2'
      return n2' = n1' -> binary_word n1'
    with
    | bw1 b1, bw1 b2 => fun _ => bw1 (b1 || b2)
    | bwn b1 pw1, bwn b2 pw2 => fun e =>
       bwn (b1 || b2) (binary_word_or' pw1 (let 'eq_refl := e in pw2))
    | bw1 _, bwn _ _ as bw => fun e =>
       False_rect _ (discriminate_bwn_SO_n' bw eq_refl (eq_sym e))
    | bwn _ _ as bw, bw1 _ => fun e =>
       False_rect _ (discriminate_bwn_SO_n' bw eq_refl e)
    end eq_refl.

Решение задачки 3: binary_word_concat для типа BinaryWord2.binary_word.

  Definition to_S {n} (w : binary_word n) : {n' & binary_word (S n') & S n' = n} :=
    match w with
    | bw1 b' => existT2 _ _ 0 (bw1 b') eq_refl
    | @bwn n' b' w' => existT2 _ _ (S n') (bwn b' w') eq_refl
    end.

  Fixpoint binary_word_concat {n m} (w1 : binary_word n) (w2 : binary_word m)
    : binary_word (n + m) :=
    match w1 with
    | bw1 b =>
        let t3 : {m' & binary_word (S m') & S m' = m} := to_S w2 in
        let w2' := projT2 (sigT_of_sigT2 t3) in
        let 'eq_refl := projT3 t3 in bwn b w2'
    | bwn b w => bwn b (binary_word_concat w w2)
    end.

Решение задачки 4: binary_word_or для варианта индуктивного типа из
модуля CoqArt.

  Fixpoint binary_word_or' {n} (w1 w2 : binary_word n) : binary_word n :=
    match w1 in binary_word n1' return binary_word n1' -> n1' = n1' -> binary_word n1' with
    | bw0 => fun _ _ => bw0
    | bwS p1 b1 pw1 => fun '(bwS p2 b2 pw2) (e : S p2 = S p1) =>
        bwS _ (b1 || b2) (binary_word_or' pw1 (let 'eq_refl := e in pw2))
    end w2 eq_refl.

Дополнение: пример использования eq_trans.

  Fixpoint binary_word_or1 {n} (w1 w2 : binary_word n) : binary_word n :=
    match
      w1 in binary_word n1'
      return binary_word n1' -> n1' = n -> binary_word n1'
    with
    | bw1 b1 => fun w2 e0 =>
      match w2 in binary_word n2' return n = n2' -> binary_word n2' with
      | bw1 b2 => fun _ => bw1 (b1 || b2)
      | bwn b2 pw2 as bw => fun e1 =>
        False_rect _ (discriminate_bwn_SO_n bw I (eq_trans e0 e1))
      end (let 'eq_refl := e0 in eq_refl)
    | @bwn n1 b1 pw1 as bw => fun w2 e0 =>
       match w2 in binary_word n2' return n2' = n -> binary_word n2' with
       | bw1 b1 => fun e1 =>
         False_rect _ (discriminate_bwn_SO_n bw I (eq_trans e1 (eq_sym e0)))
       | @bwn n2 b2 pw2 as bw => fun e1 =>
         let e' : S n2 = S n1 := eq_trans e1 (eq_sym e0) in
         let 'eq_refl := eq_sym e' in
         bwn (b1 || b2) (binary_word_or pw1 (let 'eq_refl := e' in pw2))
       end (let 'eq_refl := e0 in eq_refl)
    end w2 eq_refl.

Философско-лирическое отступление о том, почему для профессионального роста важно работать в сильной команде.

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

Однако, подспудно возникает вопрос -- какие преимущества даёт командная работа? Должна ли быть у программиста личная заинтересованность в командной работе или лучше писать код в одиночку?

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

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

Некоторое время назад автор имел удовольствие работать в компании Formal.Land¹⁰. Formal.Land это небольшая команда профессионалов, после работы в которой у автора остались исключительно положительные эмоции. Задача, о которой пойдёт речь, была связана с зависимым сопоставлением с образцом. Дело шло довольно медленно. И вот, после написания автором очередного, надо заметить, не слишком уклюжего конвоя, наш лидер Гийом Кларет (Guillaume Claret), талантливый организатор и блестящий специалист, написал в комментарии на код конвоя что-то вроде "так это же просто let Y := let 'eq_refl := e in X in Z". И, после такого незамысловатого комментария, работа над данной задачей пошла, без преувеличения, иногда вполовину быстрее.

Нужно отметить, что автор знал о существовании let с разбором случаев. Но уместное применение "теоретических" знаний на практике требует предварительно дополнительных усилий по выявлению определенных шаблонов и по формированию умения распознавать эти шаблоны в коде. Такие усилия обычно довольно затратны (собственно, наверное это и есть практическая часть обучения как такового в нашей профессии). Однако, для того чтобы эти усилия приложить, сначала ещё нужно понять, что их следует приложить. Что требует так же и некоторого озарения.

И вот здесь команда даёт уникальную возможность быстрого обмена такими опытом. При этом на порядок сокращается стадия выявления шаблонов и понимания того факта, что тут вообще нужно обучение. (Про плохо предсказуемое озарение и вообще говорить не приходится). "Проходящий мимо" коллега, пользуясь своим багажом знаний, просто делится с нами накопленным опытом как нельзя в более подходящий момент. Причём, момент действительно подходящий, потому, что в рабочем процессе совет даётся именно в контексте текущего решения практической задачи. И, поэтому, формирование и закрепление навыка происходит гораздо быстрее, чем при других известных автору способах обучения. Т.е., говоря проще, коллега может просто указать одной фразой на простую в применении технику, до которой без такого указания, возможно, вообще не дойдёт дело.

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

Большое спасибо за внимание всем кто читал статью! Надеемся, это было полезно!

Подробно о Coq: зависимое сопоставление с образцом +5