Данная статья является адаптированной русскоязычной версией моей статьи: 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
.
Механизм решения может быть описан следующей последовательностью шагов:
Написать функцию симуляцию, которая делает то же, что исходная верифицируемая функция, но с использованием
fold_right
Доказать равенство двух функций: исходной функции (использующей в своем теле
fold_left
) и ее симуляции (написанной нами, и использующей в своем телеfold_right
) для всех возможных входящих значений.В теле доказательства переписать исходную функцию ее симуляцией (тактика
rewrite
).Доказать утверждение, используя математическую индукцию, а как мы уже отмечали в начале статьи, с
fold_right
математическая индукция работает без проблем.
Обобщение (Generalization)
Причина, по которой мы не можем использовать индукционную гипотезу с fold_left — это аккумулятор, который изменяется на каждом шаге редукции. Обобщение параметров — это очень мощный инструмент: в доказательствах мы часто используем тактику generalize dependent parameter_name
. Давайте посмотрим как можно сделать обобщение для функций, содержащих в себе fold_left.
План работы:
Создать обобщенную версию нашей функции (мы обобщаем аккумулятор)
Доказать, что эта симуляция равна исходной функции
С помощью тактики
rewrite
переписать функции и применить математическую индукциюВозможно в процессе работы нам понадобятся некоторые вспомогательные функции (сформулируем их и докажем)
Рассмотрим детальный (дистиллированный) пример с подробными комментариями
(* Создаем два простых индуктивных типа. *)
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
можно сказать наверняка: это всегда очень увлекательно, потому, что каждая такая лемма — это маленький интеллектуальный вызов.
Комментарии (7)
shuhray
20.07.2023 14:37Написал сложное доказательство, в котором естественно возникают зависимые типы (некоторый тип данных естественным образом делится на "слои", индексированные натуральными числами). Итого, есть типы B и A n, где n:nat. Хочу доказать, что B есть сумма всех A n. Строю функции
foo (n:nat) (a: A n) : B
rang (b:B) : nat
bar (b:B) : A (rang b)
Доказываю
forall (b:B), foo (rang b) (bar b) = b
forall (n:nat) (a: A n), rang (foo n a) = n
Но когда выписываю теорему
forall (n:nat) (a: A n), bar (foo n a) = a
получаю
"The term
bar (foo n a)
has typeA (rang (foo n a))
while it is expected to have typeA n
".Спрашиваю на форуме, отвечают -- надо присобачить тип равенства. Прикидываю, как его присобачить, понимаю, что доказательство (и без того сложное) станет сложнее в два раза, бросаю Coq нафиг. Хотя, сделан Coq хорошо, это я такой хитроумный.
GospodinKolhoznik
20.07.2023 14:37+1Она есть и в Haskell, и в OCaml и в Rust. Используется чаще, чем
fold_right
, вероятно потому, что с ее помощью проще писать эффективный код.Мне казалось, что foldr используют чаще, чем foldl, потому что она работает быстрее и меньше жрет памяти. Ну по крайней мере так в Haskell, потому что там эти функции ленивые и foldl порождает много отложенных вычислений. Про другие языки не скажу.
AnthonyMikh
20.07.2023 14:37Если операция свёртки энергичная (как в набившем оскомину примере суммы списка через свёртку), то левая свёртка эффективнее, потому что не плодит thunk-и.
NooneAtAll3
Я с функциональщиной не особо знаком, поэтому извините за возможно тупой вопрос, но
Зачем ограничиваться симметричными функциями а не влепить
f(a,b) = g(b,a)
и разворот списка?AxeFizik
В функциональных языках принято считать, что списки приходящие как аргументы функции могут быть бесконечные. Поэтому не получится развернуть бесконечный список.
Natasha_Klaus Автор
Вы правы, в статье подразумевается конечный список. В Коке для работы с бесконечными списками используется ко-индукция (это есть в книге Adam Chlipala: CPDT там работают несколько другие правила).
NooneAtAll3
> > списки могут быть бесконечные
> Вы правы, в статье подразумевается конечный список.
вы либо «но» пропустили, либо он не прав…