How to prove all proofs of le equal?

Question

I'm basically trying to prove

Theorem le_unique {x y : nat} (p q : x <= y) : p = q.

without assuming any axioms (e.g. proof irrelevance). In particular, I've tried to get through le_unique by induction and inversion, but it never seems to get far

Theorem le_unique (x y : nat) (p q : x <= y) : p = q.
Proof.
  revert p q.
  induction x as [ | x rec_x]. (* induction on y similarly fruitless; induction on p, q fails *)
  - destruct p as [ | y p].
    + inversion q as [ | ]. (* destruct q fails and inversion q makes no progress *)
      admit.
    + admit.
  - admit.
Admitted.

Answer 1

In the standard library, this lemma can be found as Peano_dec.le_unique in the module Coq.Arith.Peano_dec.

As for a relatively simple direct proof, I like to go by induction on p itself. After proving by hand a few induction principles that Coq doesn't automatically generate, and remembering that proofs of equality on nat are unique, the proof is a relatively straightforward induction on p followed by cases on q, giving four cases two of which are absurd.

Below is a complete Coq file proving le_unique.

Import EqNotations.
Require Eqdep_dec PeanoNat.

Lemma nat_uip {x y : nat} (p q : x = y) : p = q.
apply Eqdep_dec.UIP_dec.
exact PeanoNat.Nat.eq_dec.
Qed.

(* Generalize le_ind to prove things about the proof *)
Lemma le_ind_dependent :
  forall (n : nat) (P : forall m : nat, n <= m -> Prop),
  P n (le_n n) ->
  (forall (m : nat) (p : n <= m), P m p -> P (S m) (le_S n m p)) ->
  forall (m : nat) (p : n <= m), P m p.
exact (fun n P Hn HS => fix ind m p : P m p := match p with
  | le_n _ => Hn | le_S _ m p => HS m p (ind m p) end).
Qed.

(*
Here we give an proof-by-cases principle for <= which keeps both the left
and right hand sides fixed.
*)
Lemma le_case_remember (x y : nat) (P : x <= y -> Prop)
  (IHn : forall (e : y = x), P (rew <- e in le_n x))
  (IHS : forall y' (q' : x <= y') (e : y = S y'), P (rew <- e in le_S x y' q'))
  : forall (p : x <= y), P p.
exact (fun p => match p with le_n _ => IHn | le_S _ y' q' => IHS y' q' end eq_refl).
Qed.

Theorem le_unique {x y : nat} (p q : x <= y) : p = q.
revert q.
induction p as [|y p IHp] using le_ind_dependent;
intro q;
case q as [e|x' q' e] using le_case_remember.

- rewrite (nat_uip e eq_refl).
  reflexivity.

- (* x = S x' but x <= x', so S x' <= x', which is a contradiction *)
  exfalso.
  rewrite e in q'.
  exact (PeanoNat.Nat.nle_succ_diag_l _ q').

- (* S y' = x but x <= y', so S y' <= y', which is a contradiction *)
  exfalso; clear IHp.
  rewrite <- e in p.
  exact (PeanoNat.Nat.nle_succ_diag_l _ p).

- injection e as e'.
  (* We now get rid of e as equal to (f_equal S e'), and then destruct e'
     now that it is an equation between variables. *)
  assert (f_equal S e' = e).
  + apply nat_uip.
  + destruct H.
    destruct e'.
    change (le_S x y p = le_S x y q').
    f_equal.
    apply IHp.

Qed.