2
$\begingroup$

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.
$\endgroup$

3 Answers 3

5
$\begingroup$

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. *)
$\endgroup$
7
  • $\begingroup$ @Naïm Favier I don't think you can avoid the use of UIP here, but I would be delighted if you have an idea of how this proof can go around it. Also, I don't see how opacity got in your way, everything here is just fine? $\endgroup$ Commented Jul 5 at 10:44
  • 1
    $\begingroup$ No, I changed my mind after thinking it through; you do need UIP. The opacity problems I had were in proving that Vladimir's le_n' was equal to le_n, without using the general fact. $\endgroup$ Commented Jul 5 at 10:46
  • 1
    $\begingroup$ We're clear on the fac tthat UIP for nat is provable, yes? This isn't some extra assumption we're talking about. $\endgroup$ Commented Jul 5 at 12:02
  • 2
    $\begingroup$ @NaïmFavier: I think a better way of stating what you're saying is: "This wouldn't hold if nat were replaced with some type in which non-trivial loops exist." (Saying "if nat had non-trivial loops" is like saying "if 6 were an odd number".) $\endgroup$ Commented Jul 5 at 13:49
  • 2
    $\begingroup$ In fact proving that it implies UIP is rather straightforward since a <= b /\ b <= a gives you a Hedberg function. $\endgroup$ Commented Jul 5 at 18:56
1
$\begingroup$

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.
$\endgroup$
-2
$\begingroup$

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.
$\endgroup$
10
  • 1
    $\begingroup$ Th should be provable without assuming proof irrelevance. $\endgroup$ Commented Jul 5 at 9:01
  • $\begingroup$ Another proof might look like this: Lemma le_n' n : n <= n. Proof. induction n; [reflexivity | apply le_n_S, IHn]. Qed. There is no proof of Theorem Th' n : le_n' n = le_n n.. $\endgroup$ Commented Jul 5 at 9:40
  • $\begingroup$ Those are clearly equal by induction on n. In general, you should be able to use the full induction principle for <= to show that every proof of n <= n is equal to le_n n. (I realise the burden of proof is on me; currently trying to remember enough about Coq syntax to formalise this.) $\endgroup$ Commented Jul 5 at 9:46
  • 2
    $\begingroup$ It is definitely provable, see lemma le_unique in the standard library. Whether we can make a reasonably readable proof of this fact is another question. $\endgroup$ Commented Jul 5 at 10:09
  • 1
    $\begingroup$ @JoJoModding thank you, it seems like what I need. The proof uses UIP on nat (the result is similat to UIP so it is expected) $\endgroup$ Commented Jul 5 at 11:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.