使用方程式在 Coq 中实现依赖类型查找的问题

Question

我正在尝试使用 Equations package to define a function over vectors in Coq. The minimum code that shows the problem that I will describe is available at the following gist。

我的想法是编写一个函数，该函数在 "proof" 上进行查找，某种类型适用于向量的所有元素，具有标准定义：

  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.

现在，麻烦开始了。我想定义一些 "proofs" 的类型属性适用于向量中的所有元素。以下归纳类型完成这项工作：

   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.

至少对我来说，这个定义是有意义的，应该进行类型检查。但是，Equations 显示了以下警告，给我留下了证明义务，我不知道如何完成它。

前面函数定义后呈现的信息是：

  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标准库中类似的定义，才发现之前的函数定义少了一个空向量的case：

  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 在 "Elimination principle":

部分分三步生成正确的归纳原理（这在 reference manual 中有详细说明）

它生成函数的图形（在我的 Equations 版本中它被称为 vforall_lookup_graph，在以前的版本中它被称为 vforall_lookup_ind）。我不确定我是否完全理解它是什么。直观上，它反映了函数体的结构。不管怎么说，它都是产生归纳原理的关键部件。
它证明函数遵守这个图（在一个称为 vforall_lookup_graph_correct 或 vforall_lookup_ind_fun 的引理中）；
结合最后两个结果生成与函数相关的归纳原理（该引理在所有版本中都称为vforall_lookup_elim）。

在您的情况下，图形已正确生成，但 Equations 无法自动证明该函数符合其图形（第 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.

使用方程式在 Coq 中实现依赖类型查找的问题

Trouble in implementing dependently typed lookup in Coq using Equations

coq

dependent-type