# Yet another simple theorem

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

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

This is mostly the goal of:

1 Like

@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?

I would guess reverse induction on `L`.

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

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

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

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