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.

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

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

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

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.