The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

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/