# Injectivity, Surjectivity and Smallness on lists of natural numbers imply each other

Require Import Coq.Lists.List.


I have the following properties defined on a list of natural numbers:

Definition small (l : list nat) : Prop :=
forall n, In n l -> n < length l.

Definition surj (l : list nat) : Prop :=
forall n, n < length l -> In n l.

Definition inj (l : list nat)  : Prop :=
NoDup l.


The predicate NoDup is defined here

Two alternative characterizations of NoDup are as follows:

Theorem NoDup_count_occ' l:
NoDup l <-> (forall x:A, In x l -> count_occ decA l x = 1).

Lemma NoDup_nth_error l :
NoDup l <->
(forall i j, i<length l -> nth_error l i = nth_error l j -> i = j).


These are also proven in Coq.Lists.List.

How can I prove that any two of these entail the third?

Lemma small_surj_impl_inj : forall l, small l -> surj l -> inj l.
Admitted.

Lemma surj_inj_impl_small : forall l, surj l -> inj l -> small l.
Admitted.

Lemma small_inj_impl_surj : forall l, small l -> inj l -> surj l.
Admitted.


Is it possible to have a proof that recycles things from the Standard Library, without having to prove things from scratch?

• Do you have proofs on paper? They're a bit tricky, I think. Aug 17, 2023 at 20:28