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

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

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

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 переписать функции и применить математическую индукцию

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 можно сказать наверняка: это всегда очень увлекательно, потому, что каждая такая лемма — это маленький интеллектуальный вызов.