The Coq mailing list

[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