Stream: new members

Topic: zip_append not as general as it could be

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!

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.

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

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.

Eric Wieser (Jan 02 2021 at 10:27):

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

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