The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I think your lemma implies UIP on T.  If you strip off the MN constructor, and instantiate ls to nil, then you've defined the equality type on T.  So you should be able to show that [member a (b::nil)] and [a = b] are equivalent types.  (Note that there is only one proof of [nil = nil], regardless of what type your list has; this is because you can always decide whether or not [ls = nil] for any [ls], and the "decidable equality -> UIP" implication works even when you fix the parameter to eq; I've gotten some development of this merged into the stdlib in trunk.)

Going the other way, if T is an hset, then so is list T, and your type should be an hprop.  So I suspect that your lemma is equivalent to UIP on T, but I don't have a formal proof.

-Jason

On Wed, Aug 6, 2014 at 7:54 PM, Gregory Malecha <gmalecha AT cs.harvard.edu> wrote:

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/