The Coq mailing list

[roconnor AT theorem.ca]

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?

(* 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.''