coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: robert dockins <robdockins AT fastmail.fm>
- To: Coq Club <coq-club AT pauillac.inria.fr>
- Subject: [Coq-Club] decidable eq on a well-specified type
- Date: Fri, 22 Apr 2005 09:38:27 -0400
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
I'm playing around with well-specified types and tried to prove something like the following :
Parameter limit:nat.
Definition nat_subset := { n:nat | n < limit }.
Lemma eq_nat_subset_dec : forall x y:nat_subset, {x=y}+{x<>y}.
I've had great difficulties, however. The problem comes down to showing that two proofs of (x<limit) are equivalent. From the definition of 'le' it seems pretty clear that this is the case. However I run into problems with second-order unification and the restrictions between the Prop and Set universes with all the techniques I have tried. Is it possible to prove a goal like this one without resorting to classic (and hence proof irrelevance)?
- [Coq-Club] decidable eq on a well-specified type, robert dockins
- Re: [Coq-Club] decidable eq on a well-specified type,
Haixing Hu
- Re: [Coq-Club] decidable eq on a well-specified type, Benjamin Werner
- Message not available
- Re: [Coq-Club] decidable eq on a well-specified type, robert dockins
- Re: [Coq-Club] decidable eq on a well-specified type,
robert dockins
- Re: [Coq-Club] decidable eq on a well-specified type, Pierre Letouzey
- Re: [Coq-Club] decidable eq on a well-specified type,
Haixing Hu
Archive powered by MhonArc 2.6.16.