Solution to member_heq_eq

member_heq_eq.v

Require Import Coq.Lists.List.
Require Import ExtLib.Data.HList.
Require Import ExtLib.Data.Member.

Set Implicit Arguments.
Set Strict Implicit.

Arguments MZ {_ _ _}.
Arguments MN {_ _ _ _} _.

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.

Section member_heq.
  Context {T : Type}.

  Fixpoint member_heq (l r : T) (ls : list T) (m : member l ls)
  : member r ls -> member r (del_member m) + (l = r) :=
    match m as m in member _ ls
          return member r ls -> member r (del_member m) + (l = r)
    with
    | @MZ _ _ ls => fun b : member r (l :: ls) =>
                     match b in member _ (z :: ls)
                           return l = z -> member r (del_member (@MZ _ _ ls)) + (l = r)
                     with
                     | MZ => @inr _ _
                     | MN m' => fun pf => inl m'
                     end eq_refl
    | @MN _ _ l' ls' mx => fun b : member r (l' :: ls') =>
                            match b in member _ (z :: ls)
                                  return (member _ ls -> member _ (del_member mx) + (_ = r)) ->
                                         member r (del_member (@MN _ _ _ _ mx)) + (_ = r)
                            with
                            | MZ => fun _ => inl MZ
                            | MN m' => fun f => match f m' with
                                            | inl m => inl (MN m)
                                            | inr pf => inr pf
                                            end
                            end (fun x => @member_heq _ _ _ mx x)
    end.

  (* This function sets up a `match` on a value of type
   * `member t (t' :: ts)` that extracts a maximal amount of
   * information from the unification.
   *)
  Definition member_match {t t' : T} {ts}
             (P : forall t t' ts, member t (t' :: ts) -> Type)
             (Hz : P t' t' ts (MZ))
             (Hn : forall m : member t ts, P t t' ts (MN m))
  : forall m, P t t' ts m :=
    fun m =>
      match m in member _ (x :: y)
            return P x x y (@MZ _ x y) -> (forall m0 : member t y, P t x y (MN _)) -> P t x y m
      with
      | MZ => fun X _ => X
      | MN m => fun _ X => X m
      end Hz Hn.

  Definition inj_inr {T U a b} (pf : @inr T U a = inr b)
  : a = b :=
    match pf in _ = X return match X with
                             | inl _ => True
                             | inr X => a = X
                             end
    with
    | eq_refl => eq_refl
    end.

  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.
  Proof.
    induction m1.
    { refine (@member_match _ _ _ (fun l' a ls m2 => forall (pf : a = l'),
                                       member_heq (@MZ _ a ls) m2 = inr pf ->
                                       match pf in (_ = X) return (member X (a :: ls)) with
                                       | eq_refl => MZ
                                       end = m2) _ _).
      { simpl. intros.
        refine
          match H in _ = X
                return match X with
                       | inl _ => True
                       | inr X => match X in (_ = X)
                                       return (member _ (l :: ls)) with
                                 | eq_refl => MZ
                                 end = MZ
                       end
          with
          | eq_refl => eq_refl
          end. }
      { simpl. inversion 1. } }
    { intro.
      revert IHm1. revert m1. revert m2.
      refine (@member_match _ _ _ (fun l' l0 ls m2 => forall m1 : member l ls,
                                       (forall (m3 : member l' ls) (pf : l = l'),
                                           member_heq m1 m3 = inr pf ->
                                           match pf in (_ = X) return (member X ls) with
                                           | eq_refl => m1
                                           end = m3) ->
                                       forall pf : l = l',
                                         member_heq (MN m1) m2 = inr pf ->
                                         match pf in (_ = X) return (member X (l0 :: ls)) with
                                         | eq_refl => MN m1
                                         end = m2) _ _).
      { inversion 2. }
      { intros.
        specialize (H m pf). simpl in *.
        destruct (member_heq m1 m).
        { inversion H0. }
        { specialize (H (f_equal _ (inj_inr H0))).
          subst. reflexivity. } } }
  Defined.

End member_heq.

Arguments member_heq_eq [_ _ _ _] _ _ _ _ : clear implicits.

Eval compute in member_heq_eq (@MZ _ 1 nil) MZ eq_refl eq_refl.

Eval compute in member_heq_eq (@MN _ 2 1 (2 :: 3 :: nil) MZ) (MN MZ) eq_refl eq_refl.