Yet another simple theorem

Using Coq
1

Hello!
Any hints how to prove this? Thanks in advance.

Require Import List Permutation.
Theorem thm n (L1 L2: list nat) (H1: Permutation L1 (seq 0 n)) (H2: Permutation L2 (seq 0 n)):
    NoDup (map (fun i => nth i L1 0) L2).

This is the missing part of attempt to prove

Theorem perm_mult_thm n (L1 L2: list nat) (H1: Permutation L1 (seq 0 n)) (H2: Permutation L2 (seq 0 n)):
    Permutation (map (fun i => nth i L1 0) L2) (seq 0 n).
2

Hi!

Here is how I would approach it.

  1. for any lists L1, L2 and a function f, Permutation L1 L2 -> Permutation (map f L1) (map f L2).
  2. for any list L of length n, L = map (fun i => nth i L 0) (seq 0 n).
  3. let f i = nth i L1 0, and write L1 ~ L2 for Permutation L1 L2. Then
    map f L2 ~ map f (seq 0 n) ~ L1 ~ seq 0 n
    (the first ~ is by (1), the second one by (2) and the third one by hypothesis).

Cheers!
Nicolás

1 Like
3

This is mostly the goal of:

1 Like
4

@nojb Any hints for the part (2)?

It seems super-obvious that

forall n L, length L = n -> map (fun i => nth i L 0) (seq 0 n) = L

but how to do induction to prove it?

Induction by L or by n doesn’t work (for me). Induction by n feels the closest to the correct solution because of (seq 0 n). Should I somehow generalize the statement?

5

I would guess reverse induction on L.

6

I would use the following (easy to prove) two lemmas:

Lemma list_eq_nth (X : Type) (def : X) (xs ys : list X) :
  (forall n, n < length xs -> nth n xs def = nth n ys def) ->
  length xs = length ys ->
  xs = ys.

Lemma map_nth' (A B : Type) (f : A -> B) (l : list A) (d1 : B) (d2 : A) (n : nat) :
  n < length l ->
  nth n (map f l) d1 = f (nth n l d2).
1 Like
7

Just to relate with List in standard library:

This one is a natural strengthening of nth_ext (in List in master). I have a running pull request on some statements of List, I will try to incorporate this modification (with two default values def and def').

This one is mostly map_nth with nth_indep for d1 <> f d2.

1 Like
8

Thank you all! I have managed to prove it.

Require Import List Permutation.
Set Implicit Arguments.

Lemma list_eq_nth (X : Type) (def : X) (xs ys : list X) :
  (forall n, n < length xs -> nth n xs def = nth n ys def) ->
  length xs = length ys ->
  xs = ys.
Proof.
  revert ys. induction xs; intros; destruct ys.
  + auto.
  + inversion H0.
  + inversion H0.
  + simpl in H0. inversion H0. change a with (nth 0 (a :: xs) def).
    change x with (nth 0 (x :: ys) def). rewrite H; simpl.
    - f_equal. apply IHxs; auto. intros. simpl in H. apply Peano.le_n_S in H1.
      pose (H _ H1). simpl in e. auto.
    - apply le_n_S. apply le_0_n.
Qed.

Theorem thm01 (L: list nat): map (fun i => nth i L 0) (seq 0 (length L)) = L.
Proof.
  apply (list_eq_nth 0).
  + intros. rewrite map_length in H. rewrite seq_length in H.
    erewrite nth_indep.
    - rewrite map_nth. rewrite seq_nth; simpl; auto.
    - rewrite map_length. rewrite seq_length. auto.
  + simpl. rewrite map_length. rewrite seq_length. auto.
  Unshelve. exact 0.
Qed.

Definition permutation_mult n (L1 L2: list nat) (H1: Permutation L1 (seq 0 n)) (H2: Permutation L2 (seq 0 n)):
  Permutation (map (fun i => nth i L1 0) L2) (seq 0 n).
Proof.
  assert (Permutation (map (fun i => nth i L1 0) L2) (map (fun i => nth i L1 0) (seq 0 n))).
    apply Permutation_map. auto.
  assert (Permutation (map (fun i => nth i L1 0) (seq 0 n)) L1).
    pose (thm01 L1). pose (Permutation_length H1). rewrite seq_length in e0. rewrite e0 in e. rewrite e. apply Permutation_refl.
  pose (Permutation_trans H H0) as H3. pose (Permutation_trans H3 H1). auto.
Qed.
1 Like
9

I like Olivier’s suggestion of doing reverse induction on L. I left the SearchAbout commands I used to find the names of the right lemmas in the library in the script, because they might be instructive:

Require Import List Permutation Omega.
Set Implicit Arguments.

Theorem thm01 (L: list nat): map (fun i => nth i L 0) (seq 0 (length L)) = L.
Proof.
  induction L using rev_ind.
  - reflexivity.
  - rewrite app_length, seq_app, map_app.
    Search app nth length.
    cbn. rewrite  app_nth2, Nat.sub_diag. 
    + rewrite <- IHL at 2.
      f_equal.
      Search map "ext".
      apply map_ext_in.
      intros n [_ H] % in_seq.
      now apply app_nth1.
    + omega.
Qed.
2 Likes