Email Gateway (Aug 22 2022 at 17:16): Email Gateway (Aug 22 2022 at 17:16):From: Jørgen Villadsen <jovi@dtu.dk>
Hi,
Would it be a good idea to add something like the following lemmas?
lemma sublist_map_fst_zip: obtains zs where "(map fst (zip xs ys)) @ zs = xs"
by (induct xs ys rule:list_induct2') simp_all
lemma sublist_map_snd_zip: obtains zs where "(map snd (zip xs ys)) @ zs = ys"
by (induct xs ys rule:list_induct2') simp_all
At least we found them useful.
Regards,
Jørgen
PS - Here is a little explanation in case it is needed:
text <
@{term zip}ping two lists and retrieving one of them back by mapping @{term fst} or @{term snd}
results in the original list, possibly truncated
>
Email Gateway (Aug 22 2022 at 17:17):From: Lukas Bulwahn <lukas.bulwahn@gmail.com>
Hi Jørgen,
I would propose the following lemma as alternative:
lemma map_fst_zip:
"map fst (zip xs ys) = take (min (length xs) (length ys)) xs"
by (induct xs ys rule: list_induct2') simp_all
The advantage is that it is a refinement of the existing map_fst_zip;
so I would expect that all previous proofs with map_fst_zip would
still complete with this new one (but I have not tried it).
In your proof, you can then simply replace, obtaining some zs, by
naming the witness. zs is drop (min (length xs) (length ys)) xs.
Then, in your proof:
(map fst (zip xs ys)) @ drop (min (length xs) (length ys)) xs
= take (min (length xs) (length ys)) xs @ drop (min (length xs) (length ys)) xs
= xs
This reasoning can be automatically found with (simp add: map_fst_zip).
For map_snd_zip, it is analogous.
I hope this helps.
Best regards,
Lukas
Email Gateway (Aug 22 2022 at 17:17):From: Jørgen Villadsen <jovi@dtu.dk>
Thanks Lukas, it would be great if map_fst_zip and map_snd_zip could be refined as you propose (and no new lemmas needed).
Jørgen
Email Gateway (Aug 22 2022 at 17:17):From: Tobias Nipkow <nipkow@in.tum.de>
Hi Lukas,
Your lemmas look natural but replacing the existing simp-rules with them broke a
number of proofs and didn't help any. Thus I have left things as they are. I
didn't add them as ordinary lemmas because my impression is that in most cases
one zips lists of the same length.
But thanks for the suggestion.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 17:17):From: Jørgen Villadsen <jovi@dtu.dk>
Hi Tobias,
Thanks for the investigations. Any chance that the original lemma suggestions could be added?
lemma sublist_map_fst_zip: obtains zs where "(map fst (zip xs ys)) @ zs = xs"
by (induct xs ys rule:list_induct2') simp_all
lemma sublist_map_snd_zip: obtains zs where "(map snd (zip xs ys)) @ zs = ys"
by (induct xs ys rule:list_induct2') simp_all
At least we found them useful... :-)
Best regards, Jørgen
Email Gateway (Aug 22 2022 at 17:18):From: Tobias Nipkow <nipkow@in.tum.de>
They are too complicated for a library.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 17:18):From: Lukas Bulwahn <lukas.bulwahn@gmail.com>
Too bad.
Is there a chance to put the two lemmas (without simp attribute) in
the More_List theory in HOL-Library?
That might be an acceptable compromise for everyone.
Lukas
Email Gateway (Aug 22 2022 at 17:18):From: Tobias Nipkow <nipkow@in.tum.de>
I had been afraid that if I add these lemmas I would open the floodgates for
many similar generalizations. But having looked at the existing lemmas, I found
that this fear was unjustified and I added them:
http://isabelle.in.tum.de/repos/isabelle/diff/a477f78a9365/src/HOL/List.thy
Thanks
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 17:18):From: Jørgen Villadsen <jovi@dtu.dk>
Thanks for adding them to HOL/List.thy (map_fst_zip_take and map_snd_zip_take).
Jørgen
Last updated: Nov 07 2025 at 08:29 UTC