The Coq mailing list

[Gregory Malecha <gmalecha AT cs.harvard.edu>]

Hello --

I've been thinking a bit about the membership type and trying to prove that the function that erases it to a nat is injective. Formally, here is the statement.

Context {T : Type}.

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

Section to_nat.

  Variable a : T.

  Fixpoint to_nat {ls} (m : member a ls) : nat :=

    match m with

      | MZ _ => 0

      | MN _ _ m => S (to_nat m)

    end.

End to_nat.

Lemma to_nat_eq_member_eq

: forall x ls (a b : member x ls),

    to_nat a = to_nat b ->

    a = b.

Proof. ???

My question is, is there any way to prove [to_nat_eq_member_eq] without using K? I've hacked around with it enough that I think the answer might be no, but I am not certain how I might justify that to myself.

Any suggestions would be greatly appreciated.

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/