Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] forall n m (H1 H2:le n m), H1=H2.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] forall n m (H1 H2:le n m), H1=H2.


chronological Thread 
  • From: Frederic Blanqui <frederic.blanqui AT inria.fr>
  • To: roconnor AT theorem.ca
  • Cc: Coq Club <coq-club AT pauillac.inria.fr>, sebastien.hinderer AT loria.fr
  • Subject: Re: [Coq-Club] forall n m (H1 H2:le n m), H1=H2.
  • Date: Fri, 19 Sep 2008 08:17:18 +0200
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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

--------------------------------------------------------
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







Archive powered by MhonArc 2.6.16.

Top of Page