Zulip Chat Archive

Stream: new members

Topic: Nodup Indices


view this post on Zulip 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

view this post on Zulip Riccardo Brasca (Jan 31 2021 at 18:46):

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

view this post on Zulip Kevin Buzzard (Jan 31 2021 at 18:48):

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

view this post on Zulip 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.

view this post on Zulip Riccardo Brasca (Jan 31 2021 at 18:51):

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

view this post on Zulip 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.

view this post on Zulip Marcus Rossel (Jan 31 2021 at 19:33):

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.

view this post on Zulip 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 _ _

view this post on Zulip Ryan Lahfa (Jan 31 2021 at 20:03):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (Jan 31 2021 at 20:16):

Though, indeed, this is a bit strange

view this post on Zulip 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 _) _ }

view this post on Zulip Yakov Pechersky (Jan 31 2021 at 22:18):

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

view this post on Zulip Yakov Pechersky (Jan 31 2021 at 22:18):

That's after import list.range

view this post on Zulip Yakov Pechersky (Jan 31 2021 at 22:19):

@Marcus Rossel

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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