 # Dependent association list parametrised over equality predicate?

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!

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