Another simple theorem

Using Coq
1 
Require Import List.
Theorem aux n L (H: forall x, x < n -> In x L) (H0: length L = n): NoDup L.

It feels harder than the previous one (How to approach this (seemingly) simple theorem?). Or maybe I lack creativity/cleverness to imagine correct intermediate lemmas.

Can someone give hints? I tried doing induction on n, but I’m missing something.

2

Hi,

  1. Prove using H that [0; ...; n-1] is included in L.
  2. Deduce by H0 that in fact [0; ...; n-1] = L.
  3. Conclude by NoDup [0; ...; n-1].

Cheers,
Nicolás

3

Deduce by H0 that in fact [0; ...; n-1] = L .

Is it “Permutation (seq 0 n) L”? Thank you for the help.

4

Yes, absolutely! Look at NoDup_Permutation_bis from the standard library.

Cheers,
Nicolás

1 Like
5

By the way, there is apparently a problem with this statement in the standard library: no need for the NoDup l' hypothesis (Issue #12119).

1 Like