The Coq mailing list

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

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 !