Stream: new members

Topic: list zip nodup

Kayla Thomas (Nov 20 2022 at 02:28):

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 (Nov 20 2022 at 02:30):

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 (Nov 20 2022 at 02:32):

docs#list.nodup.sublist

Eric Rodriguez (Nov 20 2022 at 02:33):

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

Eric Rodriguez (Nov 20 2022 at 02:34):

oh, that's not true, silly

Eric Rodriguez (Nov 20 2022 at 02:34):

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

Hmm. Ok.

Thank you.

Kayla Thomas (Nov 20 2022 at 02:47):

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

Kayla Thomas (Nov 20 2022 at 02:57):

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 (Nov 20 2022 at 02:59):

is docs#list.map_fst_zip relevant here?

Kayla Thomas (Nov 20 2022 at 03:02):

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.

gotcha

Kayla Thomas (Nov 20 2022 at 04:07):

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 (Nov 20 2022 at 04:12):

The lemma stated is not true. For example,

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


Oh, huh. Oops.

Kayla Thomas (Nov 20 2022 at 04:16):

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

Kayla Thomas (Nov 20 2022 at 04:32):

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 (Nov 20 2022 at 04:53):

Should this hold?

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


Matt Diamond (Nov 20 2022 at 04:56):

did you mean <+ instead of <+:?

Matt Diamond (Nov 20 2022 at 04:56):

and I feel like that should hold

Kayla Thomas (Nov 20 2022 at 04:57):

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

Matt Diamond (Nov 20 2022 at 04:57):

ohh, I thought you meant sublist... nvm

Kayla Thomas (Nov 20 2022 at 05:00):

Ok, I think I have it.

Matt Diamond (Nov 20 2022 at 05:01):

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

Kayla Thomas (Nov 20 2022 at 05:01):

Yes, that is what I just realized :)

Last updated: Dec 20 2023 at 11:08 UTC