The Coq mailing list

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

Thanks, all. This is helpful.

On Wed, Aug 6, 2014 at 4:01 PM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

On 06/08/2014 21:07, Jason Gross wrote:
> 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.)

Indeed:

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.

Definition project {x y} (p : member x (cons y nil)) : x = y.
Proof.
refine (
match p in member _ l return
  match l with
  | nil => True
  | cons x l => (l = nil) -> _
  end
with
| MZ _ _ => fun _ => eq_refl
| MN _ _ _ m => fun e => False_rect _ _
end eq_refl
).
rewrite e in *; inversion m.
Defined.

Definition inject {x y} (p : x = y) : member x (cons y nil).
Proof.
destruct p; constructor.
Defined.

Lemma retract : forall x y (p : x = y), project (inject p) = p.
Proof.
intros x y p; unfold project, inject.
destruct p.
reflexivity.
Qed.

Definition member_eq x ls (a b : member x ls) :=
    to_nat x a = to_nat x b -> a = b.

Lemma to_nat_eq_member_eq : forall x, (forall ls a b, member_eq x ls a b) ->
  (forall (p : x = x), p = eq_refl).
Proof.
intros x Hx p; unfold member_eq in *.
rewrite <- (retract _ _ p), <- (retract _ _ eq_refl).
f_equal.
apply Hx.
destruct p.
reflexivity.
Qed.

PMP

--

gregory malecha

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