The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Taral wrote:
> On Wed, Mar 25, 2009 at 7:55 AM, Matthieu Sozeau 
> <Matthieu.Sozeau AT lri.fr>
>  wrote:
>   
> > P.S.: and there's a workaround too:
> >     
>
> Neat workaround.
>
> I tried to solve this for fun, and was forced at once point to use
> proof irrelevance. Ew. Anyone know a way that doesn't use that?
>   

You can assume the weaker axiom from the [Eqdep] module, and that 
implies proof irrelevance for [lt], which is all that we need here.  An 
old coq-club post gives the proof of this implication.

Here's a Program-free implementation, for the heck of it:


Axiom lt_irrel : forall n m (pf1 pf2 : n < m), pf1 = pf2.

Notation "'No'" := (right _ _).
Notation "'Yes'" := (left _ _).

Notation "'Red' e" := (if e then Yes else No) (at level 60).
Notation "'RedE' e" := (if e then value _ else error) (at level 60).

Parameter max : nat.
Parameter P : {n | n < max} -> Prop.
Parameter dec : forall x, {P x} + {~P x}.

Definition P' n := exists pf, P (exist _ n pf).
Definition dec' (x : nat) : {P' x} + {~P' x}.
 Hint Extern 1 False => match goal with
                          | [ pf1 : ?N < ?M, pf2 : ?N < ?M |- _ ] =>
                            rewrite (lt_irrel N M pf1 pf2) in *
                        end.

 intro; refine (match le_lt_dec max x with
                  | left _ => No
                  | right Hlt => Red (dec (exist (fun n => n < max) _ Hlt))
                end); unfold P', not; firstorder.
Qed.

Definition total' : forall max', max' <= max -> Exc (forall x, x < max' 
-> P' x).
 Hint Extern 1 (_ < _) => omega.

 Hint Extern 1 (P' _) => elimtype False; omega.
 Hint Extern 1 (P' ?X) => match goal with
                            | [ H : X < S ?N |- _ ] =>
                              destruct (eq_nat_dec X N); subst
                          end.

 refine (fix F (max' : nat) : max' <= max -> Exc (forall x, x < max' -> 
P' x) :=
   match max' return max' <= max -> Exc (forall x, x < max' -> P' x) with
     | O => fun _ => value _
     | S max' => fun _ =>
       if dec' max'
         then RedE (F max' _)
         else error
   end); intuition.
Qed.

Definition total : Exc (forall x, P x).
 refine (RedE (total' max _)); intuition;
   match goal with
     | [ x : {n | n < max}, H : forall x, x < max -> _ |- _ ] =>
       let n := fresh "n" with pf := fresh "pf"
         with pf' := fresh "pf'" in
           destruct x as [n pf]; destruct (H n pf) as [pf'];
             rewrite (lt_irrel _ _ pf pf'); assumption
   end.
Qed.