Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
Shell of the proof of 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}.
Definition member_heq (l r : T) (ls : list T) (m : member l ls)
: member r ls -> member r (del_member m) + (l = r).
Admitted.
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.
Admitted.
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