Create a gist now

Instantly share code, notes, and snippets.

Solution to member_heq_eq
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment