How to approach this (seemingly) simple theorem?

Using Coq
1

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.

2

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
3

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
4

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

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

1 Like
6

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

“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. :slight_smile:

8

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

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.