Читаю Coq'Art. Доказал только что очередной (достаточно очевидный) факт, и внезапно захотелось поделиться и успехом (это было не очень просто), и мыслями на тему. А за одно решил обновить бложек - кучу лет сюда не заходил, а тут такой лонгрид получился.
Решал задание 6.47: написать функцию, которая строит бинарное дерево заполненное попарно различными натуральными числами. В этом задании используется тип не просто бинарного дерева, а бинарного дерева строго определённой высоты, т.е. высота - это параметр типа, и все листья лежат строго на одной глубине:
Inductive htree (X : Type) : nat -> Type := hleaf : X -> htree X 0 | hnode : forall h : nat, X -> htree X h -> htree X h -> htree X (S h).
Моё решение - нумерация "ахнентафелем". Это способ индексации, используемый для хранения бинарной кучи в массиве, что то же самое, что индексация по порядку обхода в ширину, но об этом ниже.
Fixpoint pn_tree_aux (h n : nat) {struct h} : htree nat h := match h with | O => hleaf n | S h' => hnode h' n (pn_tree_aux h' (2*n + 1)) (pn_tree_aux h' (2*n + 2)) end. Definition pn_tree (h : nat) : htree nat h := pn_tree_aux h 0.
А авторское - нумерация по обходу в глубину.
Fixpoint make_htree_aux (h: nat) (start : Z) : Z * htree Z h := match h with | 0 => ((1+ start)%Z, hleaf start) | S h' => let p := make_htree_aux h' (1+start)%Z in let q := make_htree_aux h' (fst p) in (fst q, hnode start (snd p) (snd q)) end. Definition make_htree (n:nat) : htree Z n := snd (make_htree_aux n 0%Z).
Я стараюсь про такие задания кроме самого решения ещё доказывать, что оно возвращает то, что нужно. В данном случае я решил доказать сначала, что все значения в получившихся деревьях попарно различны, а потом более сильное, что если разложить эти деревья одним из обходов в список, то получится интервал натуральных чисел от 0 до (2^(h+1) - 2). Факты, казалось бы, тривиальные, а попробуй докажи. Особенно много сложностей возникло с моим решением.
Первая часть ещё куда ни шло, но в моём варианте много проблем доставили операции со степенями и вычитанием, т.к. автоматические тактики вроде lia/nia, позволяющие не преобразовывать простенькую арифметику руками с помощью примитивных теорем, не справляются с выражениями, в которых результат как-то зависит от этих самых степеней или вычитания. Например для подобных неравенств мне пришлось отдельную теорему завести и доказать её по индукции:
2 <= 2 ^ h * (2 * n + 1 + 2)
А вот такое требует минут 5-10 размышлений и пяти довольно длинных строчек на доказательство:
S (2^(S h) - 1 + (2^(S h) - 1)) = 2 * (2^h + (2^h + 0)) - 1
Подбешивает, кстати, что тактика simpl разворачивает умножение на константу слева. Т.е. если написано 2*n, то после simpl будет n + (n + 0). Не знаю, как это запретить. Поэтому сделал теорему, которая переписывает выражение обратно. Но её приходится регулярно вызывать, чтобы можно было прочитать, что там теперь в goal.
А с доказательством, что уплощение построенного дерева образует интервал натуральных чисел проблемы начались уже с того, что для htree (дерева фиксированной высоты) нельзя просто так взять и написать обход в ширину, как для обычного. Пример для обычного дерева с Rosetta Code:
Fixpoint levelorder_forest (fuel: nat) (f: list tree) : list nat := match fuel with | O => nil | S fuel' => let g := (fun t r => let '(x, f) := r in (value t :: x, children t ++ f)) in let '(p, f) := fold_right g (nil, nil) f in p ++ levelorder_forest fuel' f end. Definition levelorder (t: tree) : list nat := levelorder_forest (height t) (t :: nil).
Моя попытка повторить (все использованные тут определения можно найти тут же):
Definition flat_htree_bfs_aux1 {X : Type} (h : nat) (t : htree X (S h)) (acc : list (htree X h)) := (htree_t1 t) :: (htree_t2 t) :: acc. Fixpoint flat_htree_bfs_aux {X : Type} {h : nat} (q : list (htree X h)) {struct h} : list X := match h with | O => map htree_x q | S h' => let q' := fold_right (flat_htree_bfs_aux1 h') [] q in (* <--- error *) let cur_layer := map htree_x q in let next_layers := (flat_htree_bfs_aux q') in cur_layer ++ next_layers end. Definition flat_htree_bfs {X : Type} {h : nat} (t : htree X h) : list X := @flat_htree_bfs_aux X h [t].
Выдаёт ошибку "The term "q" has type "list (htree X h)" while it is expected to have type "list (htree X (S h'))" (cannot unify "h" and "S h'").". Т.е. coq не понимает, что S h' = h, хотя казалось бы должен - мы же тут как раз деструктурируем h на S h'.
Как оказалось это известная проблема, которая даже описана в книгах, а у воркэраунда даже есть собственное название "convoy pattern". Этот паттерн предполагает замену типа всего match-выражения на эквивалентное, но возвращающее функцию, которая в свою очередь принимает как аргумент проблемное значение (в моём случае q), и возвращает то что нужно. Т.е. нужно переписать так:
Fixpoint flat_htree_bfs_aux {X : Type} {h : nat} (q : list (htree X h)) {struct h} : list X := match h return list (htree X h) -> list X with | O => fun Q => map htree_x Q | S h' => fun Q => let q' := fold_right (flat_htree_bfs_aux1 h') [] Q in let cur_layer := map htree_x Q in let next_layers := (flat_htree_bfs_aux q') in cur_layer ++ next_layers end q.
Почему без этого не работает, а с этим работает, я пока не очень понял, но надеюсь ещё пойму.
А дальше, конечно же возникла целая пачка сложностей в работе со столь громоздким определением обхода (и снова со степенями и минусами). Особенно всё усложняло то, что simpl часто разворачивал цели в слишком большую портянку, а попытка запретить ему некоторые преобразования, связанные с паттернматчингом по (S h') (высота дерева + 1. естественным образом постоянно возникает при доказательствах по индукции) выносом его в контекст (remember (S h') as h eqn:eq_h) часто приводили к ошибкам из-за того, что где-то в этом же выражении есть дерево высоты h, и получается выражение вроде такого (упрощённо) htree X h1 = htree X (S h), которое coq опять не может типизировать.
Эти проблемы я порешал тем, что максимально повыносил все преобразования, которые мне были нужны в отдельные теоремы. Но это породило другую сложность: в этой пачке теорем уже сложно ориентироваться, а выражения в целях всё равно стремятся становиться огромными.
Поэтому в который раз, убедился, что из-за обилия в формальном доказательстве технических деталей тенденции к росту длин имён сущностей и тупо объёма кода, по которому не всегда просто навигироваться, любой нетривиальный факт надо сначала доказать более неформально на листочке, а уже потом переписывать формально. На фотке мои заметки к доказательству, что мой вариант разворачивается BFS'ом в интервал. Без плана в виде этих закорючек за деревьями леса уже было совсем не видно и я напрочь перестал понимать, что доказываю в данный момент, и что с этим надо делать.
