list zip nodup

Stream: new members

[Kayla Thomas]

I'm wondering if anyone can point me in right direction to prove this:

lemma list.nodup_imp_fst_zip_nodup
  {α β : Type}
  (l1 : list α)
  (l2 : list β)
  (h1 : l1.nodup) :
  (list.map prod.fst (l1.zip l2)).nodup :=
begin
  sorry,
end

[Kayla Thomas]

I can prove that (list.map prod.fst (l1.zip l2)) ⊆ l1, but I haven't been able to transform that into the final goal.

[Eric Rodriguez]

docs#list.nodup.sublist

[Eric Rodriguez]

I think you'll need to prove that if a ⊆ b for b nodup, then actually a ≤ b

[Eric Rodriguez]

oh, that's not true, silly

[Eric Rodriguez]

if you strengthen your result to ≤, then it's there, though

[Kayla Thomas]

Hmm. Ok.

[Kayla Thomas]

Thank you.

[Kayla Thomas]

Hmm, maybe I don't have that proof, sorry. I thought I had it before.

[Kayla Thomas]

Ok, no, I have it now.

example
  {α β : Type}
  (l1 : list α)
  (l2 : list β) :
  list.map prod.fst (l1.zip l2) ⊆ l1 :=
begin
  induction l1 generalizing l2,
  simp,
  induction l2,
  simp,
  simp at *,
  have s1 : l1_tl ⊆ l1_hd :: l1_tl,
  simp,
  transitivity,
  apply l1_ih,
  apply s1,
end

[Matt Diamond]

is docs#list.map_fst_zip relevant here?

[Kayla Thomas]

I can prove it with the extra assumption on the lengths with it, but I wanted to see if I could drop that assumption, since I don't think it should be needed.

[Matt Diamond]

gotcha

[Kayla Thomas]

With the above result, I just need to prove this, which seems to be more difficult than I had expected:

example
  {α : Type}
  (l1 l2 : list α)
  (h1 : l2.nodup)
  (h2 : l1 ⊆ l2) :
  l1.nodup :=

[Andrew Yang]

The lemma stated is not true. For example,

example : [1, 1] ⊆ [1] := by simp

[Kayla Thomas]

Oh, huh. Oops.

[Kayla Thomas]

I guess I do need to show it is a sublist, not just a subset.

[Kayla Thomas]

I guess what I actually might want to prove is

example
  {α β : Type}
  (l1 : list α)
  (l2 : list β) :
  list.map prod.fst (l1.zip l2) <+: l1 :=

That is, that list.map prod.fst (l1.zip l2) is a prefix of l1.

[Kayla Thomas]

Should this hold?

example
  {α : Type}
  (l1 : list α)
  (l2 : list α)
  (h1 : l1 <+: l2)
  (h2 : l2.nodup) :
  l1.nodup :=

[Matt Diamond]

did you mean <+ instead of <+:?

[Matt Diamond]

and I feel like that should hold

[Kayla Thomas]

I'm not sure. I meant list.is_prefix.

[Matt Diamond]

ohh, I thought you meant sublist... nvm

[Kayla Thomas]

Ok, I think I have it.

[Matt Diamond]

you can also prove it with docs#list.is_prefix.sublist and docs#list.nodup.sublist

[Kayla Thomas]

Yes, that is what I just realized :)