# Stuck on destructing

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.

``````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].
* 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.

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

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