The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi,

There is an axiom-free version of this lemma in the Coq FAQ (question
138). Somehow, this is for fun, as eq_dep_eq itself is a very weak
axiom that can be realized in a slight extension of the Calculus of
Inductive Constructions (using dependent pattern-matching à la Agda).

Hugo Herbelin

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