# Stuck on destructing

**URL:** <https://discourse.rocq-prover.org/t/stuck-on-destructing/1883>\
**Category:** Using Rocq\
**Created:** [January 17, 2023, 9:52pm UTC](https://discourse.rocq-prover.org/t/stuck-on-destructing/1883 "2023-01-17T21:52:12Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![jeanas](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jeanas/32/762_2.png) [@jeanas](https://discourse.rocq-prover.org/u/jeanas)\
**Post date:** [January 17, 2023, 9:52pm UTC](https://discourse.rocq-prover.org/t/stuck-on-destructing/1883/1 "2023-01-17T21:52:12Z")

</div>

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 🙂

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.

```auto
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:

```auto
  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.

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [January 17, 2023, 10:12pm UTC](https://discourse.rocq-prover.org/t/stuck-on-destructing/1883/2 "2023-01-17T22:12:03Z")

</div>

`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:

```coq
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.

```

---

<div class="post-metadata">

**Author:** ![jeanas](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jeanas/32/762_2.png) [@jeanas](https://discourse.rocq-prover.org/u/jeanas)\
**Post date:** [January 17, 2023, 10:58pm UTC](https://discourse.rocq-prover.org/t/stuck-on-destructing/1883/3 "2023-01-17T22:58:33Z")

</div>

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