The Coq mailing list

[S�bastien Hinderer <Sebastien.Hinderer AT loria.fr>]

Hi,

Well I think this proof was provided to me by Boris Yakobowski, in copy.
Sébastien.

Frederic Blanqui (2008/09/19 08:17 +0200):
>Â 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.
>>
>>
>>
>> --------------------------------------------------------
>> Bug reports: http://logical.futurs.inria.fr/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
>
>