Nodup Indices

Stream: new members

[Marcus Rossel]

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]

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

[Kevin Buzzard]

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

[Marcus Rossel]

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]

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

[Adam Topaz]

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

[Marcus Rossel]

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

[Adam Topaz]

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

Marcus Rossel said:

Adam Topaz 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]

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]

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]

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]

Though, indeed, this is a bit strange

[Yakov Pechersky]

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]

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

[Yakov Pechersky]

That's after import list.range

[Yakov Pechersky]

@Marcus Rossel

[Marcus Rossel]

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]

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]

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]

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