## Stream: new members

### Topic: Nodup Indices

#### Marcus Rossel (Jan 31 2021 at 18:41):

How would you prove this lemma?

import data.list.indexes
import data.list.nodup

example (l : list ℕ) (p : ℕ → Prop) [decidable_pred p] : (l.find_indexes p).nodup :=
begin
rw list.find_indexes_eq_map_indexes_values,
suffices h : (list.indexes_values p l).nodup, from list.nodup_map sorry h,
rw list.indexes_values_eq_filter_enum,
suffices h : l.enum.nodup, from list.nodup_filter _ h,
-- ...?
end


I've been able to reduce it to showing that l.enum.nodup, but I don't know how to continue from here. And also I feel like there must be some easier way to show this result.
Is there anything I'm missing?
Thanks

#### Riccardo Brasca (Jan 31 2021 at 18:46):

Why is this true? If the list has duplicates and p is always true...

#### Kevin Buzzard (Jan 31 2021 at 18:48):

#eval [1,1,1,1].find_indexes (λ n, true) -- [0, 1, 2, 3]


#### Marcus Rossel (Jan 31 2021 at 18:49):

Riccardo Brasca said:

Why is this true? If the list has duplicates and p is always true...

I was assuming that list.find_indexes would return the indices of all those elements in the list that satisfy some predicate. So any given index would show up at most once, making the list nodup.

#### Riccardo Brasca (Jan 31 2021 at 18:51):

Ah sure, it finds the indexes, not the elements! Sorry, my fault

#### Adam Topaz (Jan 31 2021 at 18:55):

I would prove that the list this function produces is strictly increasing as a separate lemma, and go from there.

#### Marcus Rossel (Jan 31 2021 at 19:33):

I would prove that the list this function produces is strictly increasing as a separate lemma, and go from there.

I've separated this subproof out into its own lemma:

lemma list.enum_cons_mem {α : Type*} {l : list α} {hd : ℕ × α} {tl : list (ℕ × α)} :
l.enum = hd :: tl → hd ∉ tl :=
begin
sorry
end


But I'm failing at actually applying it:

lemma list.find_indexes_nodup {α : Type*} (p : α → Prop) [decidable_pred p] (l : list α) :
(l.find_indexes p).nodup :=
begin
rw list.find_indexes_eq_map_indexes_values,
suffices h : (list.indexes_values p l).nodup, from list.nodup_map sorry h,
rw list.indexes_values_eq_filter_enum,
suffices h : l.enum.nodup, from list.nodup_filter _ h,
induction l.enum with hd tl ih,
case list.nil { simp },
case list.cons {
apply list.nodup_cons.mpr,
suffices h : hd ∉ tl, from and.intro h ih,
have h : l.enum = hd :: tl, from sorry,
exact list.enum_cons_mem h
}
end


I don't know how to fix the second sorry. I thought a refl would work, but it seems that the fact that l.enum = hd :: tl isn't being propagated into the induction.

#### Adam Topaz (Jan 31 2021 at 19:56):

@Marcus Rossel What I had in mind is splitting up as follows.
I bet mathlib already has something like this to_func thing...

import order.basic
import data.list.indexes
import data.list.nodup

def list.to_func {α : Type*} (l : list α) : fin l.length → α := λ i, l.nth_le i.1 i.2

lemma foo (l : list ℕ) (p : ℕ → Prop) [decidable_pred p] : strict_mono (l.find_indexes p).to_func := sorry

lemma bar {l : list ℕ} : strict_mono l.to_func → l.nodup := sorry

example (l : list ℕ) (p : ℕ → Prop) [decidable_pred p] : (l.find_indexes p).nodup := bar \$ foo _ _


#### Ryan Lahfa (Jan 31 2021 at 20:03):

Marcus Rossel said:

I would prove that the list this function produces is strictly increasing as a separate lemma, and go from there.

I've separated this subproof out into its own lemma:

lemma list.enum_cons_mem {α : Type*} {l : list α} {hd : ℕ × α} {tl : list (ℕ × α)} :
l.enum = hd :: tl → hd ∉ tl :=
begin
sorry
end


But I'm failing at actually applying it:

lemma list.find_indexes_nodup {α : Type*} (p : α → Prop) [decidable_pred p] (l : list α) :
(l.find_indexes p).nodup :=
begin
rw list.find_indexes_eq_map_indexes_values,
suffices h : (list.indexes_values p l).nodup, from list.nodup_map sorry h,
rw list.indexes_values_eq_filter_enum,
suffices h : l.enum.nodup, from list.nodup_filter _ h,
induction l.enum with hd tl ih,
case list.nil { simp },
case list.cons {
apply list.nodup_cons.mpr,
suffices h : hd ∉ tl, from and.intro h ih,
have h : l.enum = hd :: tl, from sorry,
exact list.enum_cons_mem h
}
end


I don't know how to fix the second sorry. I thought a refl would work, but it seems that the fact that l.enum = hd :: tl isn't being propagated into the induction.

It looks like to me you're trying to prove something false in the induction

#### Ryan Lahfa (Jan 31 2021 at 20:03):

Maybe I may be wrong but doing induction on l.enum is like: take an arbitrary list and prove what I want I think

#### Ryan Lahfa (Jan 31 2021 at 20:04):

If you do it on l, it might work, as you will prove (0, hd) notin enum_from 1 tl and (enum_from 1 tl).nodup

#### Ryan Lahfa (Jan 31 2021 at 20:06):

And the first is provable because you can show the first component of enum_from 1 tl is greater or equal than 1, thus (0, something) cannot be there, and the second is just the fact that applying an injective function to a nodup list won't change its nodup property, and you just translate the first component of the induction hypothesis, there might be a lot better way to do it though

#### Ryan Lahfa (Jan 31 2021 at 20:16):

Though, indeed, this is a bit strange

#### Yakov Pechersky (Jan 31 2021 at 22:18):

lemma nodup_zip_of_left {α β : Type*} {l : list α} (h : nodup l) (l' : list β) :
nodup (l.zip l') :=
begin
induction l with hd tl hl generalizing l',
{ simp },
{ cases l' with hd' tl',
{ simp },
{ rw [nodup_cons] at h,
rw [zip_cons_cons, nodup_cons],
exact ⟨λ H, h.left (mem_zip H).left, hl h.right _⟩ } }
end

lemma nodup_zip_of_right {α β : Type*} (l : list α) {l' : list β} (h : nodup l) :
nodup (l.zip l') :=
begin
induction l' with hd tl hl generalizing l,
{ simp },
{ cases l with hd' tl',
{ simp },
{ rw [nodup_cons] at h,
rw [zip_cons_cons, nodup_cons],
exact ⟨λ H, h.left (mem_zip H).left, hl _ h.right⟩ } }
end

@[simp] lemma nodup_enum {l : list α} : nodup l.enum :=
by { rw enum_eq_zip_range, exact nodup_zip_of_left (nodup_range _) _ }


#### Yakov Pechersky (Jan 31 2021 at 22:18):

You said you needed l.enum.nodup -- there you go.

#### Yakov Pechersky (Jan 31 2021 at 22:18):

That's after import list.range

@Marcus Rossel

#### Marcus Rossel (Feb 01 2021 at 09:44):

Wow, thanks! @Yakov Pechersky
I feel like some of this should make its way into Mathlib, since IMHO find_indexes being nodup should be easily available and not require 4 lemmata. Does anyone know how I could get the ball rolling on that?

#### Kevin Buzzard (Feb 01 2021 at 09:53):

If you have a github account then announce what it is and ask the maintainers for push access to non-master branches of mathlib, and then put the lemmas in an appropriate place on a branch of mathlib and then make a PR

#### Yakov Pechersky (Feb 01 2021 at 13:59):

The initial premise that find_indexes is nodup is faulty (using your proof strategy), as you can tell by the fact that you have to sorry the proof that prod.fst is injective. Because it isn't.

#### Yakov Pechersky (Feb 01 2021 at 16:16):

Here you go:

import data.list.indexes
import data.list.range

open list

variables {α β γ δ ε : Type*}

@[simp] lemma foldr_with_index_nil (f : ℕ → α → β → β) (b : β) : foldr_with_index f b nil = b := rfl

@[simp] lemma foldr_with_index_singleton (f : ℕ → α → β → β) (b : β) (a : α) :
foldr_with_index f b [a] = f 0 a b := rfl

@[simp] lemma function.uncurry_comp_prod_map_id_left (f : α → β → γ) (g : δ → α) :
function.uncurry f ∘ prod.map g id = function.uncurry (f ∘ g) :=
by { ext ⟨d, e⟩, simp }

lemma foldr_with_index_cons (f : ℕ → α → β → β) (b : β) (a : α) (l : list α) :
foldr_with_index f b (a :: l) = f 0 a (foldr_with_index (f ∘ nat.succ) b l) :=
by simp [foldr_with_index_eq_foldr_enum, enum_eq_zip_range, range_succ_eq_map, zip_map_left]

@[simp] lemma find_indexes_nil (p : α → Prop) [decidable_pred p] : find_indexes p nil = nil := rfl

@[simp] lemma find_indexes_cons_true (p : α → Prop) [decidable_pred p] (a : α) (l : list α)
(h : p a) :
find_indexes p (a :: l) = 0 :: (find_indexes p l).map nat.succ :=
begin
suffices : map (prod.fst ∘ prod.map nat.succ id) (filter ((p ∘ prod.snd) ∘ prod.map nat.succ id)
((range l.length).zip l)) = map (nat.succ ∘ prod.fst)
(filter (p ∘ prod.snd) ((range l.length).zip l)),
{ simpa [find_indexes_eq_map_indexes_values, indexes_values_eq_filter_enum, enum_eq_zip_range,
range_succ_eq_map, h, filter, zip_map_left, filter_of_map] },
congr
end

@[simp] lemma find_indexes_cons_false (p : α → Prop) [decidable_pred p] (a : α) (l : list α)
(h : ¬ p a) :
find_indexes p (a :: l) = (find_indexes p l).map nat.succ :=
begin
suffices : map (prod.fst ∘ prod.map nat.succ id) (filter ((p ∘ prod.snd) ∘ prod.map nat.succ id)
((range l.length).zip l)) = map (nat.succ ∘ prod.fst)
(filter (p ∘ prod.snd) ((range l.length).zip l)),
{ simpa [find_indexes_eq_map_indexes_values, indexes_values_eq_filter_enum, enum_eq_zip_range,
range_succ_eq_map, h, filter, zip_map_left, filter_of_map] },
congr
end

@[simp] lemma nodup_find_indexes (l : list ℕ) (p : ℕ → Prop) [decidable_pred p] : (l.find_indexes p).nodup :=
begin
induction l with hd tl hl,
{ simp },
{ by_cases h : p hd;
simpa [h, nat.succ_ne_zero] using nodup_map nat.succ_injective hl }
end


Last updated: May 16 2021 at 05:21 UTC