Zulip Chat Archive

Stream: general

Topic: Making simp reduce `alt ![a, b, a]`


view this post on Zulip Eric Wieser (Dec 03 2020 at 10:17):

We now have docs#alternating_map structures in mathlib, which are defined as being equal to zero when two inputs are zero.

However, the lemma docs#alternating_map.map_eq_zero_if_eq takes a bunch of hypotheses (i ne j, v i = v j), which I'm under the impression means it shouldn't be a simp lemma.

Is there any way to state a simp lemma without these hypotheses that would match and simplify f ![a, b, a]?

view this post on Zulip Reid Barton (Dec 03 2020 at 10:24):

simp doesn't seem like the right tool for this

view this post on Zulip Reid Barton (Dec 03 2020 at 10:25):

In practice you probably don't have an explicit list of more than three arguments so just listing the 4 possible lemmas seems fine


Last updated: May 16 2021 at 05:21 UTC