member_heq_eq

member_heq_eq.v

(* Answer to the challenge member_heq_eq of Gregory Malecha
   (https://gmalecha.github.io/reflections/2017/challenge-member_heq_eq)

   This answer is partly inspired from his own answer
   (https://gist.github.com/gmalecha/75c1577c2bed86e6d126859193909715)
*)

Require Import List. Import ListNotations.

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

  Inductive member (a : T) : list T -> Type :=
  | MZ : forall ls, member a (a :: ls)
  | MN : forall l ls, member a ls -> member a (l :: ls).

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

  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}.

  Definition member_heq {l r : T} {ls : list T} (m : member l ls)
  : member r ls -> member r (del_member m) + (l = r).
  Proof.
  induction m; intros; simpl.
  - refine (match X in member _ (a::b) return member r b + (a=r)
            with | MZ _ => _ | MN _ _ => _ end).
    right; reflexivity.
    left; assumption.
  - revert IHm.
    refine (match X
            in member _ (a::b)
            return (member r b -> member r (del_member m) + (l=r)) ->
                    member r (a::del_member m) + (l=r)
            with
            | MZ _ => _
            | MN _ _ => _ end);
      intros.
    + left; left.
    + apply X0 in m0.
      destruct m0.
      left; right; assumption.
      right; assumption.
  Defined.

  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.
    (* The induction is made on [m1] and not [m2] so that [pf]
       can be generalized correctly. *)
    intros l l' ls m1 m2. revert l m1. induction m2; intros.
    - revert pf H.
      refine (match m1 as m0 in member _ (a::b)
              return (forall pf : l = a,
                      member_heq m0 (MZ b) = inr pf ->
                      match pf in (_ = X) return (member X (a::b)) with
                      | eq_refl => m0
                      end = MZ b)
              with
              | MZ _ => _
              | MN _ _ => _
              end).
      + intros. simpl in H.
        refine (match H in (_ = inr pf) with
                | eq_refl => _
                end). reflexivity.
      + intros. simpl in H. discriminate.
    - revert l' pf m2 H IHm2.
      refine (match m1 as m0 in member _ (a::b)
              return (forall l' (pf : l0=l') (m2:member l' b),
                      member_heq m0 (MN a m2) = inr pf ->
                      (forall (l1 : T) (m3 : member l1 b) (pf0 : l1 = l'),
                      member_heq m3 m2 = inr pf0 ->
                      match pf0 in (_ = X) return (member X b) with
                      | eq_refl => m3
                      end = m2) ->
                      match pf in (_ = X) return (member X (a :: b)) with
                      | eq_refl => m0
                      end = MN a m2)
              with | MZ _ => _
                   | MN _ _ => _
                   end); intros.
      + simpl in H. discriminate H.
      + simpl in H. specialize (H0 _ m pf). destruct (member_heq m m2).
        * discriminate.
        * destruct pf. rewrite H0. reflexivity.
          refine (match H in (_ = inr e) with | eq_refl => _ end). reflexivity.
Defined.

End member_heq.

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.