# How to approach this (seemingly) simple theorem?

I have this theorem I can’t prove.

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


I’m searching for ideas (intermediate lemmas etc.) that would allow me to prove it. I will try to prove them (lemmas) by myself, as much as possible.

Hello,

1. Prove that L is included in [0; ...; n-1] (only using the -> of H).
2. Then using H0 you prove that length L <= length [0; ...; n-1] = n.
3. Repeat the argument with L and [0;...; n-1] switching places (using the <- of H) to conclude that n = length [0; ...; n-1] <= length L.

Points 2 and 3 are basically NoDup_incl_length and NoDup_length_incl in the standard library.

Best wishes,
Nicolás

2 Likes

The solution by @nojb is probably the most conceptual one by using also seq and in_seq from the standard library.

You can prove it also by induction on n (with L generalized) and then rely on the following results from the standard library: in_split and NoDup_remove.

1 Like

I made proof using @olaure01’s suggestion. Soon I will try @nojb’s approach too, for training purposes.

Definition permutation_list n := { L: list nat | (forall x, In x L <-> x < n) /\ NoDup L }.
Theorem permutation_list_length n (p: permutation_list n): length (proj1_sig p) = n.
Proof.
destruct p as [L [H H0]]. simpl. revert L H H0. induction n.
+ intros. destruct L; auto. simpl in *. assert (n < 0) by (apply H; auto). inversion H1.
+ intros. assert (In n L) by (apply H; auto). destruct (in_split n L H1) as [L1 [L2 H2]].
subst. apply NoDup_remove in H0. destruct H0 as [H0 H2].
assert (forall x, In x (L1 ++ L2) <-> x < n).
- intuition.
* destruct (H x) as [H4 H5]. assert (In x (L1 ++ n :: L2)).
{ apply in_or_app. simpl. apply in_app_or in H3. tauto. }
pose (H4 H6) as H7. inversion H7. subst. tauto. auto.
* assert (x < S n) by intuition. apply H in H4.
apply in_app_or in H4. simpl in H4. destruct H4 as [H4 | [H5 | H6]].
++ apply in_or_app; auto.
++ omega.
++ apply in_or_app; auto.
- apply IHn in H3; auto. rewrite app_length. simpl. rewrite app_length in H3. omega.
Qed.

If you continue looking at this kind of questions, you might be interested in:

1 Like

I would use a slightly different solution relying on library functions:

Theorem permutation_list_length
n l (H: forall x, (x \in l) = (x < n)) (H0: uniq l): size l = n.
Proof.
have hl : iota 0 n =i l by move=> x; rewrite mem_iota H.
by have/esym/eqP := uniq_size_uniq (iota_uniq 0 n) hl; rewrite H0 size_iota.
Qed.


“From mathcomp Require Import all_ssreflect.”, right?
I haven’t started studying SSReflect and MathComp library yet. I’ve planned to do that some day, though.

Definitely will look at development suggested by olaure01.
I’ve made github repository too, although it’s a bit messy right now. Please ignore the slightly ambitious name of it.

Using theorems from Standard Library, nojb’s approach gives shorter proof.

Require Import List Omega.
Theorem permutation_list_length n L (H: forall x, In x L <-> x < n) (H0: NoDup L): length L = n.
Proof.
assert (incl L (seq 0 n)).
{ unfold incl. intros. apply in_seq. simpl. intuition. apply H; auto. }
assert (incl (seq 0 n) L).
{ unfold incl. intros. apply in_seq in H2. apply H. intuition. }
pose (seq_NoDup n 0).
pose (NoDup_incl_length H0 H1).
pose (NoDup_incl_length n0 H2).
assert (length L = length (seq 0 n)) by omega.
rewrite seq_length in H3. auto.
Qed.