The Coq mailing list

[Jean-Francois Monin <Jean-Francois.Monin AT imag.fr>]

Dear all,

An alternative approach is to use a built-in proof-irrelevant
equivalent (old-fashioned ?) definition of le :

Fixpoint LE (n m : nat) {struct n} : Prop :=
  match n, m with
  | O, _ => True
  | S n, O => False
  | S n, S m => LE n m
  end.

(* simplistic but enough at the beginning *)
Ltac induc_LE n :=
  induction n as [| n induc_n]; 
     [ simpl |
       intro m; destruct m; simpl; [intro pF; case pF | idtac]].

Lemma LE_proof_irr : forall n m (p q: LE n m), p = q.
Proof.
intros n. induc_LE n.
  intros _ () (); reflexivity.
  apply induc_n. 
Qed.

Then you have: 

Lemma LE_le : forall n m, LE n m -> n <= m.
Lemma le_LE : forall n m, n <= m -> LE n m.

(Easy and very short proofs).

Of course it does NOT yield a proof of le_unique, so you have
to really use LE, e.g. in {x | LE x n}.

I happen use it currently, and I am happy so far.

  JF

On Fri, Sep 19, 2008 at 08:17:18AM +0200, Frederic Blanqui wrote:
>Â roconnor AT theorem.ca
>  a écrit :
> 
> >I completed a proof of the theorem that le is proof irrelevent, but it
> >was more difficult than I thought it would be.  Does anyone know of a
> >simpler (axiom-free) proof?
> 
> Dear Russel, here is a proof due to Sebastien Hinderer in 2005  
> available in CoLoR (file Util/Nat/NatUtil.v):
> 
> Scheme le_ind_dep := Induction for le Sort Prop.
> 
> Lemma le_unique : forall n m (h1 h2 : le n m), h1 = h2.
> 
> Proof.
> intro n.
> assert (forall m : nat, forall h1 : le n m, forall p : nat, forall h2  
> : le n p,
>   m=p -> eq_dep nat (le n) m h1 p h2).
>  intros m h1; elim h1 using le_ind_dep.
>   intros p h2; case h2; intros.
>    auto.
>    subst n. absurd (S m0 <= m0); auto with arith.
>  intros m0 l Hrec p h2.
>   case h2; intros.
>    subst n; absurd (S m0 <= m0); auto with arith.
>    assert (m0=m1); auto ; subst m0.
>    replace l0 with l; auto.
>    apply (@eq_dep_eq _ eq_nat_dec (le n) m1); auto.
>  intros; apply (@eq_dep_eq _ eq_nat_dec (le n) m); auto.
> Qed.
> 
> >(* My proof *)
> >Require Import Eqdep_dec.
> >Require Import Omega.
> >
> >Lemma le_irrelevent : forall n m (H1 H2:le n m), H1=H2.
> >Proof.
> >assert (forall n (H1: le n n), H1 = le_n n).
> > intros n H1.
> > change H1 with (eq_rec n (fun a => a <= n) H1 _ (refl_equal n)).
> > generalize (refl_equal n).
> > revert H1.
> > generalize n at 1 3 7.
> > dependent inversion H1.
> >  apply K_dec_set.
> >   decide equality.
> >  reflexivity.
> > intros; elimtype False; omega.
> >induction m.
> > dependent inversion H1.
> > symmetry.
> > apply H.
> >dependent inversion H1.
> > symmetry.
> > apply H.
> >intros H3.
> >change H3 with (eq_rec (S m) (le n) (eq_rec n (fun n => n <= S m) H3 _
> >(refl_equal n)) _ (refl_equal (S m))).
> >generalize (refl_equal n) (refl_equal (S m)).
> >revert H3.
> >generalize n at 1 2 7.
> >generalize (S m) at 1 2 5 6.
> >dependent inversion H3.
> > intros; elimtype False; omega.
> >intros e e0.
> >assert (e':=e).
> >assert (e0':=e0).
> >revert e e0 l0.
> >rewrite e', (eq_add_S _ _ e0').
> >intros e.
> >elim e using K_dec_set.
> > decide equality.
> >intros e0.
> >elim e0 using K_dec_set.
> > decide equality.
> >simpl.
> >intros l0.
> >rewrite (IHm l l0).
> >reflexivity.
> >Qed.
> >
> >
> >-- 
> >Russell O'Connor                                      <http://r6.ca/>
> >``All talk about `theft,''' the general counsel of the American 
> >Graphophone
> >Company wrote, ``is the merest claptrap, for there exists no property in
> >ideas musical, literary or artistic, except as defined by statute.''

-- 
Jean-Francois Monin           Univ. Joseph Fourier, GRENOBLE
VERIMAG - Centre Equation     http://www-verimag.imag.fr/~monin/
2 avenue de Vignate           tel (+33 | 0) 4 56 52 04 39
F-38610 GIERES                fax (+33 | 0) 4 56 52 04 46