尝试在异构向量上定义类似"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函数(假设有一个组件类型)。为了定义1，我想我需要像rect2这样的东西。从vector库类推，我认为它的类型应该是这样的:

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上合理匹配。如果没有返回注释(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 ...这样的返回注释没有帮助，因为现在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).

使用这些类型的模式匹配可以让您了解依赖类型如何工作(或不工作)，但很快就会变得乏味。更进一步，方程组库提供了一些实用程序来处理类型依赖关系，特别是帮助处理这种依赖反转。下面是使用方程式的完整解决方案:

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.