Uniqueness of proofs for inductively defined predicates

Question

In Init/Peano.v the less-than-or-equal predicate is defined as follows:

Inductive le (n:nat) : nat -> Prop :=
  | le_n : n <= n
  | le_S : forall m:nat, n <= m -> n <= S m

where "n <= m" := (le n m) : nat_scope.

Can I prove the following theorem?

Theorem Th n (p : n <= n) : p = le_n n.

Answer 1

Here is a short proof:

Require Import Arith Lia.
Import EqNotations.

(* A generalised lemma, which generalises over the index using a
proof of equality to make case distinction well-defined. *)
Lemma le_n_eq_gen n m (e : m = n) (h : n <= m) : rew e in h = le_n n :> (n <= n).
Proof.
  destruct h.
  - (* to get rid of the n = n proof, we need UIP to replace it by reflexivity.
    I don't think this step can be avoided (but note that the UIP we use is a 
    proven theorem from the standard library, not an axiom/assumption. *)
    rewrite (UIP_nat _ _ e eq_refl).
    reflexivity.
  - (* the other case is impossible by arithmetic reasoning, lia can take care of that. *)
    lia.
Qed.

(* now the corollary is trivial *)
Corollary le_n_eq n (h : n <= n) : h = le_n n.
Proof.
  apply (le_n_eq_gen eq_refl).
Qed.

Here we did not need any induction on the equality proof, only destruct. Had we needed it, the standard induction for le derived by Coq would not have been sufficient, because it is non-dependent, and so we cannot use it to prove properties of a proof witness. To derive the dependent induction principle, one can use:

Scheme Induction for le Sort Prop.
About le_ind_dep. (* the induction principle we really want to use. *)

Answer 2

Here is a proof that is somehow self-explaining. Jean François Monin and I reworked it about two years ago. Below is an Ltac style proof script. The keywork is of course dependent pattern matching for small inversion.

Notice that the proof is not only for a ≤ a but for a ≤ b.

Require Import Arith Utf8.  (* for Nat.lt_irrefl *)

Local Definition lt_irrefl {a b} : S a = b → b ≤ a → False :=
  λ e, match e with eq_refl => Nat.lt_irrefl _ end.

Section eq_nat_pirr.

  (** We need proof irrelevance for "@eq nat" 
      Below is a direct proof by induction on "a"
      that does not use Hedberg theorem, theorem
      which generalizes the irrelevance result to all
      equality predicates which are (weakly) decidable. *)

  Fact eq_0_inv {a} (e : 0 = a) :
    match a return _ = a → Prop with
    | 0   => λ f, eq_refl = f
    | S _ => λ _, False
    end e.
  Proof. now destruct e. Qed.

  Definition eq_0_pirr (e : 0 = 0) : eq_refl = e.
  Proof. exact (eq_0_inv e). Qed.

  Print eq_S.

  Fact eq_S_inv {a b} (e : S a = b) :
    match b return _ = b → Prop with
    | 0   => λ _, False
    | S b => λ e, ∃f, f_equal S f = e
    end e.
  Proof. destruct e; now exists eq_refl. Qed.

  Definition eq_S_pirr {a b} (e : S a = S b) : ∃f : a = b, f_equal S f = e.
  Proof. exact (eq_S_inv e). Qed.

  Theorem eq_nat_pirr {a : nat} : ∀e : a = a, eq_refl = e.
  Proof.
    induction a as [ | a IHa ].
    + apply eq_0_pirr.
    + intros e.
      destruct (eq_S_pirr e) as (f & <-).
      now destruct (IHa f).
  Qed.

End eq_nat_pirr.

Section le_pirr.

  Arguments le_n {_}.
  Arguments le_S {_ _}.

  Print le.

  (** We implement a simulateous induction principle
      on two proofs of "l₁ l₂ : a ≤ b", which proceeds
      by induction on l₁ and then dependent inversion 
      on l₂. 

      The used inversion lemmas are "le_eq_pirr"
      and "le_S_pirr" below but proving them requires
      some generalization. *)

  Definition le_eq_inv {a b} (l : a ≤ b) : ∀e : b = a, le_n = eq_rect _ (le a) l _ e.
  Proof.
    destruct l; intros e.
    + now destruct (eq_nat_pirr e).
    + destruct (lt_irrefl e l).
  Qed.

  Definition le_eq_pirr {a} (l : a ≤ a) : le_n = l.
  Proof. apply le_eq_inv with (e := eq_refl). Qed.

  Definition le_S_inv {a b} (l : a ≤ b) :
     match b return _ ≤ b → Prop with
     | 0   => λ _, True
     | S b => λ l, S b = a ∨ ∃l', le_S l' = l
     end l.
  Proof. 
    destruct l.
    + destruct a; auto.
    + eauto.
  Qed.

  Definition le_S_pirr {a b} (lS : a ≤ S b) : a ≤ b → ∃l, le_S l = lS.
  Proof. 
    destruct (le_S_inv lS) as [ e | ]; intros l.
    + destruct (lt_irrefl e l).
    + assumption.
  Qed.

  Section le_le_indd.

    Variables (a : nat) 
              (P : ∀b, a ≤ b → a ≤ b → Prop)
              (P_n : P a le_n le_n)
              (P_S : ∀ {b} {l₁ l₂ : a ≤ b}, P _ l₁ l₂ → P _ (le_S l₁) (le_S l₂)).

    Fixpoint le_le_indd {b} (l₁ : a ≤ b) {struct l₁} : ∀l₂, P _ l₁ l₂.
    Proof.
      destruct l₁ as [ | b l₁ ]; intros l₂.
      + now destruct (le_eq_pirr l₂).
      + destruct (le_S_pirr l₂ l₁) as [ l <- ].
        now apply P_S.
    Qed.

  End le_le_indd.

  Theorem le_pirr a : ∀b (l₁ l₂ : a ≤ b), l₁ = l₂.
  Proof. now apply le_le_indd; intros; subst. Qed.

End le_pirr.

Answer 3

The principle of proof irrelevance cannot be proved in Coq, but we can introduce axiom proof_irrelevance from https://coq.inria.fr/library/Coq.Logic.ProofIrrelevance.html:

From Coq Require Import
     Arith.PeanoNat
     Logic.ProofIrrelevance.

Import Nat.

Theorem Th n (p : n <= n) : p = le_n n.
Proof.
  apply proof_irrelevance.
Qed.