Stuck on destructing

Using Coq
1

Hi,

I am working on the following proof that ∀ n, ⟦0, n⟧ is finite (for “finite” defined as "no injection from ℕ to this type”). Please note that there could be more elegant definitions, stdlib use, etc. but my goal is more to increase my understanding of Coq than to do this fast :slight_smile:

I have omitted parts of the proof that are not relevant here, using admit.

While I can see other ways, I went for an inductive proof.

Require Import PeanoNat.
Require Import ProofIrrelevance.

Definition iv (n : nat) : Type := {a : nat | a <= n}.

Definition injective {X Y : Type} (f : X -> Y) : Prop := forall x x' : X, f x = f x' -> x = x'.

Definition finite (X : Type) : Prop := ~(exists f : nat -> X, injective f).

Lemma iv_finite (n : nat) : finite (iv n).
Proof.
  induction n as [|n Hn].
  * admit.
  * intro. destruct H as [f Hf]. apply Hn. clear Hn.
    assert (exists N, forall m, N <= m -> proj1_sig (f m) <> S n) by admit.
    destruct H as [N HN].
    unshelve eexists (fun (p : nat) => _ : iv n). {
      set (i := p+N).
      assert (H : N <= i) by apply Nat.le_add_l.
      apply HN in H.
      destruct (f i) as [fi Hfi].
      exists fi. now apply le_S_n, Nat.le_neq.
    }
    intros x x' H. inversion H. clear H.

At this point, the proof state looks like this:

  n : nat
  f : nat -> iv (S n)
  Hf : injective f
  N : nat
  HN : forall m : nat, N <= m -> proj1_sig (f m) <> S n
  x, x' : nat
  H1 : (let (x, p) as s return (proj1_sig s <> S n -> iv n) := f (x + N) in
        fun H : x <> S n =>
        exist (fun a : nat => a <= n) x
          (le_S_n x n (match Nat.le_neq x (S n) with
                       | conj _ x1 => x1
                       end (conj p H)))) (HN (x + N) (Nat.le_add_l N x)) =
       (let (x, p) as s return (proj1_sig s <> S n -> iv n) := f (x' + N) in
        fun H : x <> S n =>
        exist (fun a : nat => a <= n) x
          (le_S_n x n (match Nat.le_neq x (S n) with
                       | conj _ x1 => x1
                       end (conj p H)))) (HN (x' + N) (Nat.le_add_l N x'))
  ============================
  x = x'

I want to prove f (x + N) = f (x' + N), which implies x = x' by Hf (f injective). If you squint at this big equality H1, you can see that it says essentially this, plus equality of some proofs. In each of the members, f (x + N) (resp. f (x' + N) is destructed with let as (x, p), and the term built up is exist ... x .... I just want to set the third element of the exist (the proof of existence) and keep the equality of the second element (the witness). However, I was not able to do that. I tried variants of destruct (f (x + N)), which fails while abstracting because the term f (x + N) occurs in the types in the proof I want to discard. Also, I don’t fully understand why this term (let (x, p) as s return ... in fun H => ...) (...) is not reduced by compute into (let (x, p) as s return ... in let H := ... in ...) or something similar.

2

let (x, p) := bla in foo is just syntax sugar for match bla with C x p => foo end (with the constructor name C left unsaid and obtained from the type of bla).

I don’t quite know how to make this proof work as-is but if you change it do exists (proj1_sig (f i)) instead of destruct (f i). exists fi. it’s pretty easy:

Require Import PeanoNat Lia Arith.

Definition iv (n : nat) : Type := {a : nat | a <= n}.

Definition injective {X Y : Type} (f : X -> Y) : Prop := forall x x' : X, f x = f x' -> x = x'.

Definition finite (X : Type) : Prop := ~(exists f : nat -> X, injective f).

Lemma iv_finite (n : nat) : finite (iv n).
Proof.
  induction n as [|n Hn].
  - admit.
  - intro. destruct H as [f Hf]. apply Hn. clear Hn.
    assert (exists N, forall m, N <= m -> proj1_sig (f m) <> S n) by admit.
    destruct H as [N HN].
    unshelve eexists (fun (p : nat) => _ : iv n). {
      set (i := p+N).
      assert (H : N <= i) by apply Nat.le_add_l.
      apply HN in H.
      exists (proj1_sig (f i)).
      apply le_S_n, Nat.le_neq.
      intuition.
      apply proj2_sig.
    }
    intros x x' H. inversion H. clear H.
    apply eq_sig_hprop_iff in H1.
    + apply Hf in H1.
      lia.
    + intros;apply le_unique.
3

Thanks a lot! I guess it was a bad idea to mix proj1_sig and destructuring in the same proof.