Instantly share code, notes, and snippets.

# gmalecha/member_heq_eq.v Last active Feb 22, 2017

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