The Coq mailing list

[Haixing Hu <Haixing.Hu AT imag.fr>]

Yes, you are right. I also found that this lemma was independed in the CIC,
unless the equality was decidable. Thank you very much for help.



Quoting Benjamin Werner 
<benjamin.werner AT polytechnique.fr>:

> Hi,
> 
> This is not exactly a simplification. Indeed your lemma cannot be 
> proved without axiom in the current version of Coq's type theory. On 
> the other hand, the corresponding propositions over natural numbers (or 
> any type upon which equality is decidable) are provable without further 
> assumptions.
> 
> There was a discussion of the case of the predicate < (or <= ) not long 
> ago.
> 
> 
> Cheers,
> 
> 
> Benjamin
> 
> 
> 
> Le 27 avr. 05, à 16:07, Haixing Hu a écrit :
> 
> > This is an interesting problem. There is another simplified version: 
> > how to
> > prove the floowing lemma?
> >
> > Lemma single_eq_proof : forall (A : Type) (x : A) (p1 p2 : x = x), p1 
> > = p2.
> >
> >
> >
> > Quoting robert dockins 
>Â >Â <robdockins AT fastmail.fm>:
> >
> >> 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)?
> >>
> >> --------------------------------------------------------
> >> Bug reports: http://coq.inria.fr/bin/coq-bugs
> >> Archives: http://pauillac.inria.fr/pipermail/coq-club
> >>           http://pauillac.inria.fr/bin/wilma/coq-club
> >> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> >>
> >>
> >>
> >
> >
> >
> >
> > -------------------------------------------------
> > envoyé via Webmail/IMAG !
> >
> > --------------------------------------------------------
> > Bug reports: http://coq.inria.fr/bin/coq-bugs
> > Archives: http://pauillac.inria.fr/pipermail/coq-club
> >           http://pauillac.inria.fr/bin/wilma/coq-club
> > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> >
> 
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> 
> 
> 




-------------------------------------------------
envoyé via Webmail/IMAG !