coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Is this provable without K?
- Date: Wed, 6 Aug 2014 22:31:20 +0200
For completeness (member x [y] and x=y are indeed isomorphic types):
Lemma inject_project : forall x y (p:member x (cons y nil)), inject (project p) = p.
Proof.
intros x y p.
refine match p in member _ l
return match l return member x l -> Prop with cons z nil => fun p => inject (project p) = p | _ => fun _ => True end p
with
| MZ _ _ => _
| MN _ _ _ m => _
end; swap 1 2.
all:destruct l; [|easy].
{ inversion m. }
reflexivity.
Qed.
Lemma inject_project : forall x y (p:member x (cons y nil)), inject (project p) = p.
Proof.
intros x y p.
refine match p in member _ l
return match l return member x l -> Prop with cons z nil => fun p => inject (project p) = p | _ => fun _ => True end p
with
| MZ _ _ => _
| MN _ _ _ m => _
end; swap 1 2.
all:destruct l; [|easy].
{ inversion m. }
reflexivity.
Qed.
On 6 August 2014 22:01, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:
On 06/08/2014 21:07, Jason Gross wrote:Indeed:
> 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.)
| MZ _ _ => 0
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
| 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
- [Coq-Club] Is this provable without K?, Gregory Malecha, 08/06/2014
- Re: [Coq-Club] Is this provable without K?, Jason Gross, 08/06/2014
- Re: [Coq-Club] Is this provable without K?, Pierre-Marie Pédrot, 08/06/2014
- Re: [Coq-Club] Is this provable without K?, Gregory Malecha, 08/06/2014
- Re: [Coq-Club] Is this provable without K?, Arnaud Spiwack, 08/06/2014
- Re: [Coq-Club] Is this provable without K?, Arnaud Spiwack, 08/06/2014
- Re: [Coq-Club] Is this provable without K?, Pierre-Marie Pédrot, 08/06/2014
- Re: [Coq-Club] Is this provable without K?, Robbert Krebbers, 08/06/2014
- Re: [Coq-Club] Is this provable without K?, Jason Gross, 08/06/2014
- Re: [Coq-Club] Is this provable without K?, Jason Gross, 08/06/2014
- Re: [Coq-Club] Is this provable without K?, Jason Gross, 08/06/2014
- Re: [Coq-Club] Is this provable without K?, Jason Gross, 08/06/2014
Archive powered by MHonArc 2.6.18.