The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Why do you think you can't do it if you have UIP for [T], but not decidable equality?

On Wed, Aug 6, 2014 at 8:15 PM, Robbert Krebbers <mailinglists AT robbertkrebbers.nl> wrote:

If T has decidable equality, then yes, otherwise, I suppose not.

My rather ugly proof of the "yes" part:

Require Import Eqdep_dec EqdepFacts List.
Lemma to_nat_eq_member_eq (dec : forall x y : T, {x = y} + {x <> y}) :

  forall x ls (a b : member x ls),
  to_nat a = to_nat b -> a = b.
Proof.

  intros x ls a b Hab.
  apply eq_dep_eq_dec; [intros; now apply list_eq_dec|].
  revert b Hab. induction a as [ls|l ls a]; simpl.
  { cut (forall ls' (b : member x ls'), ls' = x :: ls -> 0 = to_nat b ->
      eq_dep (list T) (member x) (x :: ls) (MZ x ls) ls' b); auto.
    intros ? [?|???]; injection 1; intros; subst; try discriminate. constructor. }
  cut (forall ls' (b : member x ls'), ls' = l :: ls -> S (to_nat a) = to_nat b ->
    eq_dep (list T) (member x) (l :: ls) (MN x l ls a) ls' b); auto.
  intros ? [?|???]; injection 1; [discriminate|injection 3; intros; subst].
  cut (MN x l ls a = MN x l ls m); [now intros ->|].
  f_equal. apply eq_dep_eq_dec; [intros; now apply list_eq_dec|auto].
Qed.
Print Assumptions to_nat_eq_member_eq.

On 08/06/2014 08:54 PM, Gregory Malecha 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/