Проблема в реализации зависимого типизированного поиска в Coq с использованием уравнений

Question

Я пытаюсь использовать пакет Equations для определения функции над векторами в Coq. Минимальный код, который показывает проблему, которую я опишу, доступен по следующему адресу: gist .

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

  Inductive vec (A : Type) : nat -> Type :=
  | VNil  : vec A 0
  | VCons : forall n, A -> vec A n -> vec A (S n).

Используя предыдущий тип, я определил следующую (также стандартную) операцию поиска (используя уравнения):

   Equations vlookup {A}{n}(i : fin n) (v : vec A n) : A :=
      vlookup  FZero (VCons x _) := x ;
      vlookup  (FSucc ix) (VCons _ xs) := vlookup ix xs.

Теперь проблема начинается. Я хочу определить тип "доказательства", что некоторые свойство выполняется для всех элементов вектора. Следующий индуктивный тип выполняет эту работу:

   Inductive vforall {A : Type}(P : A -> Type) : forall n, vec A n -> Type :=
   | VFNil  : vforall P _ VNil
   | VFCons : forall n x xs,
         P x -> vforall P n xs -> vforall P (S n) (VCons x xs).

Наконец, функция, которую я хочу определить:

Equations vforall_lookup
            {n}
            {A : Type}
            {P : A -> Type}
            {xs : vec A n}
            (idx : fin n) :
            vforall P xs -> P (vlookup idx xs) :=
    vforall_lookup FZero (VFCons _ _ pf _) := pf ;
    vforall_lookup (FSucc ix) (VFCons _ _ _ ps) := vforall_lookup ix ps.

По-моему, это определение имеет смысл, и оно должно проверять тип. Но уравнения показали следующее предупреждение и оставили мне обязательство по доказательству, в котором я понятия не имел, как его закончить.

Сообщение, представленное после определения предыдущей функции:

  Warning:
  In environment
  eos : end_of_section
  fix_0 : forall (n : nat) (A : Type) (P : A -> Type) (xs : vec A n) 
                 (idx : fin n) (v : vforall P xs),
                  vforall_lookup_ind n A P xs idx v (vforall_lookup idx v)
  A : Type
  P : A -> Type
  n0 : nat
  x : A
  xs0 : vec A n0
  idx : fin n0
  p : P x
  v : vforall P xs0
  Unable to unify "VFCons P n0 x xs0 p v" with "v".

Обязательство осталось

  Obligation 1 of vforall_lookup_ind_fun:
  (forall (n : nat) (A : Type) (P : A -> Type) (xs : vec A n) 
      (idx : fin n) (v : vforall P xs),
  vforall_lookup_ind n A P xs idx v (vforall_lookup idx v)).

Позже, просмотрев аналогичное определение в стандартной библиотеке Agda, я понял, что в предыдущем определении функции отсутствует регистр для пустого вектора:

  lookup : ∀ {a p} {A : Set a} {P : A → Set p} {k} {xs : Vec A k} →
          (i : Fin k) → All P xs → P (Vec.lookup i xs)
  lookup ()      []
  lookup zero    (px ∷ pxs) = px
  lookup (suc i) (px ∷ pxs) = lookup i pxs

Мой вопрос: как я могу указать, что в случае пустого вектора правая часть должна быть пустой, то есть противоречие? Руководство по уравнениям показывает пример равенства, но я мог бы адаптировать его к этому случаю. Есть идеи, что я делаю не так?

Answer 1

Мне кажется, я наконец понял, что происходит в этом примере, внимательно изучив сгенерированное обязательство.

Определение правильное, и оно принято (вы можете использовать vforall_lookup без решения обязательства). Что не может быть сгенерировано, так это принцип индукции, связанный с функцией.

Точнее, Equations генерирует правильный принцип индукции в три этапа (это подробно описано в справочном руководстве ) в разделе «Принцип исключения»:

• генерирует график функции (в моей версии Уравнений она называется vforall_lookup_graph, в предыдущих версиях она называлась vforall_lookup_ind). Я не уверен, что полностью понимаю, что это такое. Интуитивно, это отражает структуру тела функции. В любом случае, это ключевой компонент для генерации принципа индукции.

• доказывает, что функция учитывает этот граф (в лемме под названием vforall_lookup_graph_correct или vforall_lookup_ind_fun);

• объединяет последние два результата для генерации принципа индукции, связанного с функцией (эта лемма называется vforall_lookup_elim во всех версиях).

В вашем случае график был сгенерирован правильно, но Уравнения не смогли автоматически доказать, что функция уважает свой график (шаг 2), поэтому он оставлен вам.

Давайте попробуем!

Next Obligation.
  induction v.
  - inversion idx.
  - dependent elimination idx.
    (* a powerful destruct provided by Equations
       that correctly working with dependent types
    *)
    + constructor.
    + constructor.

Coq отклоняет последний вызов constructor с ошибкой

Unable to unify "VFCons P n1 x xs p v" with "v".

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

Мы должны доказать

vforall_lookup_graph (S n1) A P (VCons x xs) (FSucc f) (VFCons P n1 x xs p v) (vforall_lookup (FSucc f) (VFCons P n1 x xs p v))

в то время как тип vforall_lookup_graph_equation_2, второй конструктор vforall_lookup_graph_equation равен

forall (n : nat) (A : Type) (P : A -> Type) (x : A) (xs0 : vec A n) (f : fin n) (p : P x) (v : vforall P xs0),
  vforall_lookup_graph n A P xs0 f v (vforall_lookup f v) -> vforall_lookup_graph (S n) A P (VCons x xs0) (FSucc f) (VFCons P n x xs0 p v) (vforall_lookup f v)

Разница заключается в звонках на vforall_lookup. В первом случае имеем

vforall_lookup (FSucc f) (VFCons P n1 x xs p v)

и во втором случае

vforall_lookup f v

Но они идентичны по определению vforall_lookup! Но по умолчанию объединение не признает это. Нам нужно немного помочь. Мы можем либо дать значение некоторого аргумента, например

apply (vforall_lookup_graph_equation_2 n0).

или мы можем использовать exact или refine, которые объединяются более агрессивно, чем apply, поскольку им дан весь термин, а не только его голова

refine (vforall_lookup_graph_equation_2 _ _ _ _ _ _ _ _ _).

Мы можем легко сделать вывод из предположения об индукции. Это дает следующее доказательство

Next Obligation.
  induction v.
  - inversion idx.
  - dependent elimination idx.
    + constructor.
    + (* IHv is the induction hypothesis *)
      exact (vforall_lookup_graph_equation_2 _ _ _ _ _ _ _ _ (IHv _)).
Defined.

---

Так как мне нравится делать доказательства с зависимыми типами вручную, я не могу не дать доказательство, которое не использует dependent elimination.

Next Obligation.
  induction v.
  - inversion idx.
  - revert dependent xs.
    refine (
      match idx as id in fin k return
        match k return fin k -> Type with
        | 0 => fun _ => IDProp
        | S n => fun _ => _
        end id
      with
      | FZero => _
      | FSucc f => _
      end); intros.
    + constructor.
    + exact (vforall_lookup_graph_equation_2 _ _ _ _ _ _ _ _ (IHv _)).
Defined.