尝试在异构向量上定义类似 "rect2" 的函数

Question

我有以下（希望没有争议！）异构向量的定义：

Require Vectors.Vector.
Import Vector.VectorNotations.

Section hvec.
  Variable A : Type.
  Variable B : A -> Type.

  Inductive t : forall k : nat, Vector.t A k -> Type :=
  | nil : t 0 []
  | cons :
      forall (a : A) (b : B a) (k : nat) (v : Vector.t A k), t k v -> t (S k) (a :: v).

  Local Notation "[! ]" := nil (format "[! ]").
  Local Notation "h :! t" := (cons _ h _ _ t) (at level 60, right associativity).
  Local Notation "[! x ]" := (x :! [! ]).

我想定义一个 eqb 函数（假设有一个用于组件类型的函数）。要定义一个，我想我需要像 rect2 这样的东西。从Vectors库类推，我觉得它的类型应该是这样的：

  Fixpoint rect2
             (P : forall {k : nat} {v : Vector.t A k} (hv0 hv1 : t k v), Type)
             (bas : P nil nil)
             (rect : forall {k : nat} {v : Vector.t A k} {hv0 hv1 : t k v},
                 P hv0 hv1 ->
                 forall (a : A) (b0 b1 : B a), P (b0 :! hv0) (b1 :! hv1))
             {k : nat}
    : forall (v : Vector.t A k) (hv0 hv1 : t k v), P hv0 hv1.

问题是我不知道如何让所有依赖类型正确通过。匹配 k，然后 v 然后 hv0（这对我来说似乎是显而易见的方法）似乎不起作用。问题是你走到这一步了：

refine (
    match k with
    | 0 =>
      fun v =>
        match v with
        | [] =>
          fun hv0 hv1 => _
        | _ => tt
        end
    | S k' => _
    end
).

但无法在 hv0 上合理匹配。没有 return 注释 (match hv0 with ...)，类型如下所示：

  ...
  v : Vector.t A 0
  hv0, hv1 : t 0 []
  ============================
  P 0 [] hv0 hv1

（注意义务中的 hv0，而不是 nil）。尝试编写 match hv0 as hv0' return P 0 [] hv0' hv1 with ... 之类的 return 注释没有帮助，因为现在 hv0' 的类型已经丢失了 k 为零的事实。

我假设有一个聪明的技巧/正确的顺序来写这种东西。有人可以帮忙吗？

Answer 1

您可以使用相关的相关模式匹配进行反转，如下所示：

 Fixpoint rect2
             (P : forall {k : nat} {v : Vector.t A k} (hv0 hv1 : t k v), Type)
             (bas : P nil nil)
             (rect : forall {k : nat} {v : Vector.t A k} {hv0 hv1 : t k v},
                 P hv0 hv1 ->
                 forall (a : A) (b0 b1 : B a), P (b0 :! hv0) (b1 :! hv1))
             {k : nat}
    : forall (v : Vector.t A k) (hv0 hv1 : t k v), P hv0 hv1.
 Proof.
   intro v.
   induction v using Vector.t_rect.
   - intros hv0.
     refine (
            (* match on hv0, retaining info on its indices *)
             match hv0 as z in t k l return forall (hv1 : t k l),
                 (* match on the abstracted index l : Vector.t A k *)
                 match l as l' in Vector.t _ k'
                               return forall (hv0 hv1 : t k' l'), Type
                 with
                 (* when l = [] we have our goal *)
                 | [] => P 0 []
                 (* otherwise we create a dummy goal that we can fulfill *)
                 | _ => fun _ _ => unit
                 end z hv1
             with
             | [!] => _ (* Actual goal with hv0 replaced by [!] *)
             | _ => fun _ => tt  (* Dummy goal of type unit *)
             end).

尝试一下这些类型的模式匹配可以告诉您依赖类型如何工作（或不工作），但它很快就会变得乏味。更进一步，Equations 库提供了一些实用程序来处理类型依赖，特别是帮助处理这种依赖倒置。这是使用方程式的完整解决方案：

Require Vectors.Vector.
Import Vector.VectorNotations.

From Equations Require Import Equations.

Module VectorInd.
  (* Provided by Equations *)
  Derive Signature NoConfusionHom for Vector.t.
End VectorInd.

Import VectorInd.

Section hvec.
  Variable A : Type.
  Variable B : A -> Type.

  Inductive t : forall k : nat, Vector.t A k -> Type :=
  | nil : t 0 []
  | cons :
      forall (a : A) (b : B a) (k : nat) (v : Vector.t A k), t k v -> t (S k) (a :: v).

  Local Notation "[! ]" := nil (format "[! ]").
  Local Notation "h :! t" := (cons _ h _ _ t) (at level 60, right associativity).
  Local Notation "[! x ]" := (x :! [! ]).

  (* Provided by Equations *)
  Derive Signature NoConfusionHom for t.

 Fixpoint rect2
             (P : forall {k : nat} {v : Vector.t A k} (hv0 hv1 : t k v), Type)
             (bas : P nil nil)
             (rect : forall {k : nat} {v : Vector.t A k} {hv0 hv1 : t k v},
                 P hv0 hv1 ->
                 forall (a : A) (b0 b1 : B a), P (b0 :! hv0) (b1 :! hv1))
             {k : nat}
    : forall (v : Vector.t A k) (hv0 hv1 : t k v), P hv0 hv1.
 Proof.
   intro v.
   induction v using Vector.t_rect.
   all: intros hv0 hv1; depelim hv0; depelim hv1.
   - apply bas.
   - now apply rect, IHv.
 Defined.

尝试在异构向量上定义类似 "rect2" 的函数

Trying to define a "rect2"-like function on heterogeneous vectors

coq

dependent-type