Challenge: member_heq_eq

Working on a polymorphic version of MirrorCore I have been working a lot with heterogeneous lists and proof-relevant membership. The later is the source of this challenge problem.

A shell of the code is available as a gist, and my solution is available as well.

The Function

Suppose that I want to implement the following version of hetergeneous decideable equality on them:

Section del_val.
  Context {T : Type}.
  Variable ku : T.

  Fixpoint del_member (ls : list T) (m : member ku ls) : list T :=
    match m with
    | MZ l => l
    | MN ku' m => ku' :: del_member m
    end.
End del_val.

Definition member_heq
: forall (T : Type) (l r : T) (ls : list T) (m : member l ls),
  member r ls -> member r (del_member m) + (l = r)

Essntially del_member computes the list that is the result of removing the position marked by m. You can see how this might be useful in the context of manipulating syntax because when you replace a unification variable (notated by m) with an expression, you will get an expression that has all the same unification variables but without any occurances of m.

Given that, what member_heq is doing is comparing two members and returning the translation of the second into the del_membered list in the case that they are not the same, or proving that the two types are the same. Parametricity will guarantee that if we return an inr pf for any pf, that the two memberes must be equal; however, we’ll prove that as the second (more challenging) part of the challenge.

First part of the challenge is to implement member_heq without using any axioms or additional assumptions. If you are going to try to do it with tactics, note that tactics such as dependent induction and dependent destruct can silently introduce axioms, so you should check the proof at the end with Print Assumptions member_heq.. Don’t forget to finish your definition with Defined or you won’t be able to prove anything about the function!

The verification

The second step, which is significantly more challenging, is to prove that if member_heq a b returns inr pf then a = b. Of course, you won’t simply be able to simply write a = b since the two terms have different types, but the pf proof shows that these two types are provably equal.

Here’s the statement of the second part of the challenge.

Lemma member_heq_eq : forall {l l' ls} (m1 : member l ls) (m2 : member l' ls) pf,
  member_heq m1 m2 = inr pf ->
  match pf in _ = X return member X ls with
  | eq_refl => m1
  end = m2.

As before, no axioms. The proof needs to reduce completely, i.e.

member_heq_eq MZ MZ eq_refl eq_refl = eq_refl

and

member_heq_eq (MN MZ) (MN MZ) eq_refl eq_refl = eq_refl

Finished?

If you’ve found a solution that you’d like to share, leave a link in the comments.