The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sun, 07 Apr 2013 12:17:53 +0200,
Robbert Krebbers 
<mailinglists AT robbertkrebbers.nl>
 a écrit :

> On 04/07/2013 06:56 AM, Chris Dams wrote:
> > This kind of proof is in
> > generally possible for the cases you describe but it is kind of
> > tedious. There may be a more efficient way.
> 
> For such proofs, I use dependent equality (eq_dec) to simulate
> dependent pattern matching. In case equality of the indexes is
> decidable, eq_dec coincides with Leibniz equality for equal indexes.
> 
> This way you can do the proof in a more structured and less tedious
> way. It extends straightforwardly to most other inductive types.
> 
> Require Import Eqdep Eqdep_dec Omega Utf8.
> 
> Lemma nat_le_pi: ∀ (x y : nat) (p q : x < y), p = q.
> Proof.
>    assert (∀ x y (p : x ≤ y) y' (q : x ≤ y'),
>      y = y' → eq_dep nat (le x) y p y' q) as aux.
>    { fix 3. intros x ? [|y p] ? [|y' q].
>      * easy.
>      * clear nat_le_pi. omega.
>      * clear nat_le_pi. omega.
>      * injection 1. intros Hy. now case (nat_le_pi x y p y' q Hy). }
>    intros x y p q. now apply (eq_dep_eq_dec eq_nat_dec), aux.
> Qed.

That is cheating, you are using an axiom ^^

Print eq_dep_eq_dec.
Print eq_rect_eq__eq_dep_eq.
Print eq_rect_eq.
Print Eq_rect_eq.eq_rect_eq.