Dependent association list parametrised over equality predicate?

Using Coq
1

Hello,

I am trying to represent associative lists “list (key * value)” where the type of “value” may depend on “key” and define a predicate that asserts that a given pair (key, value) belongs to the association list. My first idea was to define

Inductive Assoc {A : Type} {B : A -> Type} (a : A) (u : B a) : list (sigT B) -> Prop :=
| Ass_hd: forall xs,
    Assoc a u (existT _ a u :: xs)
| Ass_tl: forall x xs,
    Assoc a u xs ->
    Assoc a u (x :: xs).

The problem is that I need to use this when A has a specific notion of equality (eg A = Q). Hence, I want the above definition of Assoc extended so that the following property holds:

Parameter eq : A -> A -> Prop.
forall a b u xs, eq a b -> (Assoc a u xs <-> Assoc b u xs).

This looks like it would require considering compatibilities between eq and B (eg eq x y -> B x = B y), and it looks quite complicated in general. Is there a better way? How can I make this work?

Thanks!

2

I can’t see a way around having a dependently-typed equivalence on B without more details about your application, but it might be useful to decompose definitions in more reusable pieces.

Assoc is basically In:

Assoc a u xs = In (existT _ a u) xs

If you have an equivalence on A and B (the latter depending on the former), you can pack them into an equivalence on sigT B.

Parameter eq_sigT : sigT B -> sigT B -> Prop.

Then a version of In invariant under equivalence could be obtained as:

Definition In' x xs := exists x', eq_sigT x x' /\ In x' xs.
1 Like