COQ: верификация функций, содержащих fold_left

Данная статья является адаптированной русскоязычной версией моей статьи: Handling fold_left in proofs.

Функция fold_left , сворачивающая список, довольно популярна во многих (функциональных и не очень) языках программирования. Она есть и в Haskell, и в OCaml и в Rust. Используется чаще, чем fold_right, вероятно потому, что с ее помощью проще писать эффективный код.

fold_left и fold_right из библиотеки OCaml library: List.

val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a  fold_left f init [b1; ...; bn] is f (... (f (f init b1) b2) ...) bn.  val fold_right : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b  fold_right f [a1; ...; an] init is f a1 (f a2 (... (f an init) ...)).  Not tail-recursive.

Но с точки зрения формальной верификации, доказывать утверждения для fold_right проще, чем для fold_left. Почему? Причина кроется во внутренней организации этих функций. В формальной верификации часто используется математическая индукция как инструмент для доказательства утверждений о таких структурах данных как списки. Как известно, fold_left, свернет список слева. То есть на первом шаге она добавит первый элемент списка к аккумулятору, и для следующего шага итерации аккумулятор будет изменен. А это означает, что индукционную гипотезу использовать уже нельзя. С другой стороны, функция fold_right не изменит аккумулятор до самого конца своей работы, а значит индукционную гипотезу можно применить в доказательстве.

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

Переписать fold_left на fold_right: тактика rewrite

Чтобы применить rewrite, прежде всего нужно удостовериться, что функция внутри fold_left симметрична.

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

Если в нашем случае это так, мы столкнулись с самым простым случаем, потому, что можем применить теорему fold_symmetric из стандартной библиотеки Coq Lists library.

  Theorem fold_symmetric :     forall (A : Type) (f : A -> A -> A),     (forall x y z : A, f x (f y z) = f (f x y) z) ->     forall (a0 : A), (forall y : A, f a0 y = f y a0) ->     forall (l : list A), fold_left f l a0 = fold_right f a0 l.

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

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

1. Написать функцию симуляцию, которая делает то же, что исходная верифицируемая функция, но с использованием fold_right

2. Доказать равенство двух функций: исходной функции (использующей в своем теле fold_left) и ее симуляции (написанной нами, и использующей в своем теле fold_right) для всех возможных входящих значений.

3. В теле доказательства переписать исходную функцию ее симуляцией (тактика rewrite).

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

Обобщение (Generalization)

Причина, по которой мы не можем использовать индукционную гипотезу с fold_left — это аккумулятор, который изменяется на каждом шаге редукции. Обобщение параметров — это очень мощный инструмент: в доказательствах мы часто используем тактику generalize dependent parameter_name. Давайте посмотрим как можно сделать обобщение для функций, содержащих в себе fold_left.

План работы:

1. Создать обобщенную версию нашей функции (мы обобщаем аккумулятор)

2. Доказать, что эта симуляция равна исходной функции

3. С помощью тактики rewrite переписать функции (fold_left на fold_right) и применить математическую индукцию

4. Возможно в процессе работы нам понадобятся некоторые вспомогательные функции (сформулируем их и докажем)

Рассмотрим детальный (дистиллированный) пример с подробными комментариями

(* Создаем два простых индуктивных типа. *) Inductive good : Set := wealth | health | glory .  Inductive bad : Set := poverty | disease | oblivion.  (* Создаем парочку функций-преобразователей *) (* Простое преобразование *) Definition fate (a : good) : bad :=   match a with   | wealth => poverty   | health => disease   | glory => oblivion   end.             Definition destiny (b : bad) : good :=   match b with   | poverty => wealth   | disease => health   | oblivion => glory   end.       (* Преобразование с аккумулятором. Эта функция будет использована внутри [fold_left].    Она получает элемент и аккумулятор-список, преобразует элемент и добавляет его в аккумулятор-список. *) Definition fate_acc (ls : list bad) (a : good) : list bad :=   match a with   | wealth => poverty :: ls   | health => disease :: ls   | glory => oblivion :: ls   end.             Definition destiny_acc (ls : list good) (a : bad) : list good :=   match a with   | poverty => wealth :: ls   | disease => health :: ls   | oblivion => glory :: ls   end.                (* Для этих определений (содержащих [fold_left]) мы будем доказывать некоторые утверждения. *) Definition good_to_bad (ls : list good) : list bad :=   fold_left fate_acc [] ls.  Definition bad_to_good (ls : list bad) : list good :=   fold_left destiny_acc [] ls.  (* С этими списками мы будем работать. *) Definition bad_list : list bad := [oblivion; disease; oblivion; oblivion]. Definition good_list : list good := [wealth; health; health; glory].  (* Проверим наши определения: *) Compute good_to_bad good_list. Compute bad_to_good bad_list.  (* Эти два утверждения равны. *) Compute (bad_to_good bad_list). Compute rev (Lists.List.map destiny bad_list).  (* Попробуем это доказать. *) Lemma transformation : forall (ls : list bad),     bad_to_good ls = Lists.List.rev (Lists.List.map destiny ls). Proof. intros.        induction ls.        simpl. reflexivity.        simpl.        unfold bad_to_good in *.        simpl. destruct a.        Abort.  (*  На этом шаге у нас есть индукционная гипотеза:     IHls : fold_left destiny_acc [] ls = Lists.List.rev (Lists.List.map destiny ls)     А также цель: fold_left destiny_acc [wealth] ls =     (Lists.List.rev (Lists.List.map destiny ls) ++ [destiny poverty])%list  Мы можем видеть, что сразу после первой итерации мы уже не можем переписать  индукционную гипотезу, потому, что аккумулятор изменился. Предпримем следующие шаги:          1. Создадим версию нашей функции, но с обобщенным аккумулятором     2. Докажем, что эта симуляция равна исходной функции     3. Перепишем функции внутри нашей леммы и пойдем по индукции     4. Определим и докажем некоторые вспомогательные леммы. *)  Definition bad_to_good_generalized   (ls : list bad) (acc : list good) : list good :=   fold_left destiny_acc acc ls.  (* Прежде чем сформулировать лемму, осуществляем проверку. *) Compute bad_to_good bad_list.  Compute bad_to_good_generalized bad_list [].  Lemma bad_to_good_eq : forall ls, bad_to_good ls = bad_to_good_generalized ls []. Proof.   reflexivity. Qed.   (* Нам понадобится аккумулятор. *) Definition accum : list good := [wealth; glory].  (* Прежде, чем сформулировать лемму, делаем проверку. *)  Compute bad_to_good_generalized bad_list accum.  (*  = [glory; glory; health; glory; wealth; glory]      : list good *)  Compute (bad_to_good_generalized bad_list [] ++ accum)%list.   (*  = [glory; glory; health; glory; wealth; glory]      : list good *)  (* Формулируем вспомогательную лемму - она понадобится нам в основном     доказательстве. *) Lemma bad_to_good_generalized_acc : forall ls acc,     bad_to_good_generalized ls acc =       (bad_to_good_generalized ls [] ++ acc)%list. Proof.   intros.   (* Мы собираемся делать индукцию по ls.      Чтобы наша индукционная гипотеза применялась к любому аккумулятору —       мы его обобщаем с помощью тактики generalize *)   generalize dependent acc.   induction ls; intros.   (* базовый случай *)   { simpl.  sfirstorder. }   (* индуктивный случай *)   { destruct a eqn:A.     (* a = poverty *)     { unfold bad_to_good_generalized. simpl.       replace (fold_left destiny_acc (wealth :: acc) ls) with         (bad_to_good_generalized ls (wealth :: acc )) by sfirstorder.       rewrite IHls.       replace (fold_left destiny_acc [wealth] ls) with         (bad_to_good_generalized ls [wealth]) by sfirstorder.       replace (bad_to_good_generalized ls [wealth]) with         ((bad_to_good_generalized ls [] ++ [wealth])%list) by sfirstorder.       rewrite <- List.app_assoc. sfirstorder. }     (* Используя этот же самый блок кода мы доказываем остальные случаи для типа `bad` *)     ...   (* Основная лемма, пытаемся доказать исходное утверждение, используя метод обобщения [generalization]. *) Lemma transformation_attempt2 : forall (ls : list bad),     bad_to_good ls = Lists.List.rev (Lists.List.map destiny ls). Proof.   intros.   rewrite bad_to_good_eq.  (* теперь мы работаем с обобщенной версией *)   induction ls. reflexivity.   simpl.   (* делаем один шаг редукции *)   destruct a; simpl; unfold bad_to_good_generalized; simpl.   replace (fold_left destiny_acc [wealth] ls) with     (bad_to_good_generalized ls [wealth]) by sfirstorder.   (* здесь мы используем нашу вспомогательную лемму *)   rewrite bad_to_good_generalized_acc.   (* теперь мы можем, наконец, переписать нашу индуктивную гипотезу *)   rewrite IHls; reflexivity. (* voila! *)   (* Сделаем то же самое для еще двух конструкторов типа[good].      Мы могли бы упаковать это в группу тактик, но мы не делаем этого      с тем, чтобы наше доказательство было демонстративным. *)   (* То же для `health` *)   replace (fold_left destiny_acc [health] ls) with     (bad_to_good_generalized ls [health]) by sfirstorder.   rewrite bad_to_good_generalized_acc.   rewrite IHls; reflexivity.   (* То же для `glory` *)   replace (fold_left destiny_acc [glory] ls) with     (bad_to_good_generalized ls [glory]) by sfirstorder.   rewrite bad_to_good_generalized_acc.   rewrite IHls; reflexivity. Qed.

Да, доказывать утверждения, содержащие fold_left — задача не всегда простая, например, для этой статьи я пыталась доказать, что функции good_to_bad и bad_to_good являются инверсиями:

Lemma round_and_round (ls : list bad) : good_to_bad (bad_to_good ls) = ls.

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

Одно о доказательстве утверждений использующих fold_left можно сказать наверняка: это всегда очень увлекательно, потому, что каждая такая лемма — это маленький интеллектуальный вызов.