Zulip Chat Archive

Stream: new members

Topic: zip_append not as general as it could be


view this post on Zulip Chase Meadors (Jan 02 2021 at 10:19):

Hey all,
I encountered a small issue today when I needed to use the zip_append theorem. It seems to me that the way this theorem is posed is a little less general than it could be - in particular, it supposes that the four lists involved have the same type, where only each pair being appended needs to have the same type. I was able to alter it very easily to use {l₁ r₁ : list α} {l₂ r₂ : list β}, which did solve my problem. This is compatible with the general version of list α → list β → list (α × β)

I'm willing to make PR to fix this, but of course thought I'd ask here first as the contributions page recommends. I'm very familiar with [functional] programming & mathematics, but new to formalizing mathematics and Lean, so it's also possible I'm just missing a simple way to leverage this theorem in my situation, so any feedback is appreciated!

view this post on Zulip Eric Wieser (Jan 02 2021 at 10:23):

Looking at the other theorems next to it, I think this wasn't deliberate, and the change you suggest is a good idea and an easy PR.

view this post on Zulip Kevin Buzzard (Jan 02 2021 at 10:25):

The lemma is only used a couple of times in mathlib, so generalise it, check data.multiset.antidiagonal and data.list.perm still compile and you should be fine

view this post on Zulip Bryan Gin-ge Chen (Jan 02 2021 at 10:26):

The only other thing I might suggest (if you're up for it) is to skim the rest of the file to see if there are similar oversights.

view this post on Zulip Eric Wieser (Jan 02 2021 at 10:27):

Note that github will check things in other files still compile for you

view this post on Zulip Chase Meadors (Jan 02 2021 at 10:37):

Sounds good, I'll look into it soon!


Last updated: May 08 2021 at 18:17 UTC