# 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.