如何向 Coq 传达某些类型是相等的？

Question

我有一个 CPDT 中描述的异构列表：

Section hlist.
  Variable A : Type.
  Variable B : A -> Type.
  Inductive hlist : list A -> Type :=
  | HNil : hlist nil
  | HCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls)
  .
End hlist.

并且正在尝试在 Ensemble 列表和元素列表之间定义 'pointwise membership' 谓词：

Definition hlist_in_ensemble_hlist {A : Type}{B : A -> Type}(types : list A)
           (sets : hlist A (fun a => Ensemble (B a)) types) (elems : hlist A B types) : Prop :=
  match sets with
  | HNil _ _ => True
  | HCons _ _ a1 a1s b1 b1s =>
    match elems with
    | HNil _ _ => False
    | HCons _ _ a2 a2s b2 b2s =>
      Ensembles.In (B a1) b1 b2 (* /\ recursion (TODO) *)
    end
  end.

然而，Coq 抱怨 Ensembles.In (B a1) b1 b2 部分：

The term "b2" has type "B a2" while it is expected to have type "B a1"

直觉上，a1 和 a2 是相同的，因为它们是同一个 types 列表的头部。我如何将其传达给 Coq？我尝试将 elems 与 cons x xs 匹配并将违规行更改为 Ensembles.In (B x) b1 b2，但这会导致类似的错误。我还阅读了 Convoy 模式，但不确定如何在这种情况下应用它。

Answer 1

这是CPDT的convoy pattern的经典应用：当你需要争论两个索引在模式匹配后是否相等时，你需要改变匹配使得它returns一个函数。在这种情况下，我发现在 hlist 索引上执行递归更容易：

Require Import Coq.Lists.List.
Import ListNotations.

Section hlist.
  Variable A : Type.
  Variable B : A -> Type.
  Inductive hlist : list A -> Type :=
  | HNil : hlist nil
  | HCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls)
  .
  Definition head x xs (l : hlist (x :: xs)) : B x :=
    match l with
    | HCons _ _ b _ => b
    end.

  Definition tail x xs (l : hlist (x :: xs)) : hlist xs :=
    match l with
    | HCons _ _ _ l => l
    end.
End hlist.

Fixpoint hlist_in_ensemble_hlist {A : Type}{B : A -> Type}(types : list A)
           : hlist A (fun a => B a -> Prop) types -> hlist A B types -> Prop :=
  match types with
  | [] => fun _ _ => True
  | x :: xs => fun sets elems =>
    head _ _ _ _ sets (head _ _ _ _ elems) /\
    hlist_in_ensemble_hlist _ (tail _ _ _ _ sets) (tail _ _ _ _ elems)
  end.

（注意我已经内联了 Ensemble 的定义。）

如何向 Coq 传达某些类型是相等的？

How to communicate to Coq that certain types are equal?

coq

dependent-type

convoy-pattern