coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] forall n m (H1 H2:le n m), H1=H2., roconnor
- Re: [Coq-Club] forall n m (H1 H2:le n m), H1=H2., Frederic Blanqui
- Re: [Coq-Club] forall n m (H1 H2:le n m), H1=H2.,
Pierre Casteran
- Re: [Coq-Club] forall n m (H1 H2:le n m), H1=H2., frederic . blanqui
- Re: [Coq-Club] forall n m (H1 H2:le n m), H1=H2., Sébastien Hinderer
- Re: [Coq-Club] forall n m (H1 H2:le n m), H1=H2., Hugo Herbelin
- Re: [Coq-Club] forall n m (H1 H2:le n m), H1=H2.,
Pierre Casteran
- Re: [Coq-Club] forall n m (H1 H2:le n m), H1=H2., Frederic Blanqui
Archive powered by MhonArc 2.6.16.