How to communicate to Coq that certain types are equal?

Question

I have a heterogenous list as described in 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.

and am trying to define a 'pointwise membership' predicate between a list of Ensembles and a list of elements:

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.

However, Coq complains about the Ensembles.In (B a1) b1 b2 part:

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

Intuitively, a1 and a2 are the same, since they are the heads of the same types list. How do I communicate that to Coq? I tried matching elems with cons x xs and changing the offending line to Ensembles.In (B x) b1 b2, but that results in a similar error. I also read about the Convoy pattern, but am not sure how to apply it in this context.

Answer 1

This is a classic application of the convoy pattern of CPDT: when you need to argue that two indices are equal after pattern matching, you need to change the match so that it returns a function. In this case, I find it easier to perform the recursion on the hlist indices:

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.

(Note that I have inlined the definition of Ensemble.)