Подстановки функций и типов или представления в Coq

Question

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

Heap : Set -> Set

и изоморфизм

f : forall A, Heap A -> List A.

Кроме того, у меня есть функции H_app и H_nth, такие, что

H_app (f a) (f b) = f (a ++ b)

а также

H_nth (f a) = nth a

С одной стороны, я должен был бы заменить каждую рекурсию списка специализированной функцией, которая имитирует рекурсию списка. С другой стороны, заранее я бы хотел заменить ++ а также nth от H_app а также H_nthТаким образом, извлеченные алгоритмы будут быстрее. Проблема в том, что я использую такую ​​тактику, как simpl а также compute в некоторых местах, что, вероятно, не удастся, если я просто заменю все в коде доказательства Было бы хорошо иметь возможность "перегружать" функции впоследствии.

Возможно ли что-то подобное?

Изменить: чтобы уточнить, похожая проблема возникает с числами: у меня есть несколько старых доказательств, которые используют nat, но цифры становятся слишком большими. С помощью BinNat было бы лучше, но можно ли использовать BinNat вместо nat также в старых доказательствах без особых изменений? (И особенно, заменить неэффективные использования + более эффективным определением для BinNat?)

Answer 1

Просто для ясности, я так понимаю, Heap должен выглядеть так:

Inductive Heap A : Type :=
| Node : Heap A -> A -> Heap A -> Heap A
| Leaf : Heap A.

с f определяется как

Fixpoint f A (h : Heap A) : list A :=
  match h with
  | Node h1 a h2 => f h1 ++ a :: f h2
  | Leaf => []
  end.

Если это так, то f не определяет изоморфизм между Heap A а также list A для всех A, Вместо этого мы можем найти функцию g : forall A, list A -> Heap A такой, что

forall A (l : list A), f (g l) = l

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

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

Это немного абстрактно, поэтому давайте попробуем сделать это более конкретным. Предположим, что у вас есть функция над списками (скажем, foo) который использует только ++ а также nth, Чтобы иметь возможность заменить foo эквивалентной версией на Heap используя параметричность, нам нужно сделать foo Определение полиморфное, абстрагируясь над функциями над списками:

Definition foo (T : Set -> Set)
               (app : forall A, T A -> T A -> T A)
               (nth : forall A, T A -> nat -> option A)
               A (l : T A) : T A :=
  (* ... *)

Сначала вы должны доказать свойства foo, создав его в списках:

Definition list_foo := foo list @app @nth.

Lemma list_foo_lemma : (* Some statement *).

Теперь, потому что мы сейчас H_app а также H_nth совместимы с их списками аналогов, и потому foo полиморфна, теория параметричности говорит, что мы можем доказать

Definition H_foo := foo Heap @H_app @H_nth.

Lemma foo_param : forall A (h : Heap A),
                    f (H_foo h) = list_foo (f h).

с этой леммой в руках, должно быть возможно транспортировать свойства list_foo к аналогичным свойствам H_foo, Например, в качестве тривиального примера мы можем показать, что H_app является ассоциативным, вплоть до преобразования в список:

forall A (h1 h2 h3 : Heap A),
  list_foo (H_app h1 (H_app h2 h3)) =
  list_foo (H_app (H_app h1 h2) h3).

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

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

1. Есть плагин параметрическости для Coq (CoqParam), который должен помочь автоматически получить шаблонные доказательства. Однако я никогда не использовал его, поэтому не могу сказать, насколько просто им пользоваться.

2. Библиотека эффективной алгебры Coq (или, если коротко, CoqEAL) использует параметричность для доказательства эффективности эффективных алгоритмов, в то же время рассуждая о более удобных. В частности, они определяют уточнения, которые позволяют переключаться между nat а также BinNat, как вы предложили. Внутренне они используют инфраструктуру, основанную на логическом выводе класса типов, которую вы можете адаптировать к исходному примеру, но я слышал, что в настоящее время они переносят свою реализацию на использование CoqParam.