1

我有一个异构列表，如 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.

并尝试在Ensembles 列表和元素列表之间定义“逐点成员资格”谓词：

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 模式的信息，但不确定如何在这种情况下应用它。

4

1 回答 1

2

这是 CPDT 的convoy 模式的一个经典应用：当你需要在模式匹配后争论两个索引相等时，你需要改变匹配，使其返回一个函数。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。）

于 2020-07-01T14:25:42.497 回答