The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

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.