The Coq mailing list

[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)?

The answer is yes.  The proof required a stronger induction principle 
and inversion lemma than the usual ones and some fancy dancing to avoid 
second-order unification.  The main interesting point of the development 
is the lemma:

Lemma le_eq : forall (x y:nat) (p1 p2: x <= y), p1 = p2.


Development attached for the curious.

Robert Dockins
Require Import Le.
Require Import Eqdep.
Require Import Peano_dec.

Section nat_subset.

Variable limit:nat.
Definition nat_subset := { n:nat | n < limit }.

Scheme le_rec := Induction for le Sort Prop.

Lemma le_inversion :
  forall (x y:nat) (P:le x y),
    (exists H:x=y, P = (eq_rect x (le x) (le_n x) y H)) \/
    (exists y':nat, exists R:(S y') = y, exists H:(le x y'), 
        P = (eq_rect (S y') (le x) (le_S x y' H) y R)).

intros x y P.
elim P using le_rec.
left.
exists (refl_equal x).
simpl; trivial.
intros m H H1.
right.
elim H1; clear H1.
intros H1; elim H1; clear H1.
intros H1 H2.
exists m.
exists (refl_equal (S m)).
exists H.
apply eq_rect_eq.

intros H0.
elim H0; clear H0.
intros x0 H1.
elim H1; clear H1.
intros H1 H2.
elim H2; clear H2.
intros H2 H3.
exists m.
exists (refl_equal (S m)).
simpl.
exists H.
trivial.
Qed.


Lemma le_eq : forall (x y:nat) (p1 p2: x <= y), p1 = p2.

intros x y p1.
elim p1 using le_rec.
intros p2.
elim le_inversion with x x p2.
intros H; elim H.
intros x0 H0.
rewrite H0.
apply eq_rect_eq.
intro H; elim H; clear H.
intros x0 H; elim H; clear H.
intros x1 H; elim H; clear H.
intros x2 H; elim H; clear H.
rewrite <- x1 in x2.
absurd (S x0 <= x0); auto with arith.
intros.

elim le_inversion with x (S m) p2.
intros H0; elim H0; clear H0.
intros x0 H0.
absurd (S m <= m); auto with arith.
clear H H0.
rewrite x0 in l.
assumption.

intro H0; elim H0; clear H0.
intros x0 H0; elim H0; clear H0.
intros x1 H0; elim H0; clear H0.
intros x2 H0.
injection x1.
intros.
cut (eq_rect (S x0) (le x) (le_S x x0 x2) (S m) x1 =
     eq_rect (S m) (le x) (le_S x m l) (S m) (refl_equal (S m))).
intros H2.
rewrite H2 in H0.
rewrite H0.
apply eq_rect_eq.
clear H0.
generalize x1 x2.
rewrite H1.
intros x3 x4.
cut (x4 = l).
intros H0.
rewrite H0.
cut (x3 = (refl_equal (S m))).
intros H2.
rewrite H2.
simpl.
trivial.
apply UIP.
symmetry.
apply H.
Qed.

Theorem nat_subset_eq_dec : forall x y:nat_subset, {x=y}+{x<>y}.
unfold nat_subset.
intros x y.
case x.
case y.
clear x y.
intros x p y q.
case (eq_nat_dec x y).
intro H.
left.
generalize p q; clear p q.
rewrite H.
intros p q.
cut (p = q).
intro H0.
rewrite H0.
trivial.
unfold lt in p, q.
elim le_eq with (S y) limit p q.
trivial.

intros H.
right.
red; intros.
injection H0.
intro H1.
absurd (x=y).
exact H.
symmetry.
exact H1.
Qed.

End nat_subset.