Zulip Chat Archive

Stream: general

Topic: Proof breakage I don't understand

Anne Baanen (Oct 22 2021 at 08:40):

I added a couple of lemmas on ideal.span in #9852, and even though they are not tagged simp or anything, it caused a file that does not mention ideal or span anywhere to break. The fix was to use by exact original_term, which signifies to me there's some deep magic going on here. Anyone have a clue what is going on?

Ruben Van de Velde (Oct 22 2021 at 08:56):

The fact that that line already had by exact makes me suspicious

Eric Wieser (Oct 22 2021 at 09:02):

Didn't you also change some imports?

Eric Wieser (Oct 22 2021 at 09:02):

That could have introduced arbitrary simp lemmas or instances that didn't yet exist before

Anne Baanen (Oct 22 2021 at 10:22):

Oh yeah there is a new import, but there's still no simping in that have statement.

Reid Barton (Oct 22 2021 at 12:34):

Simplest possibility would be that instance selection chose a different (but defeq) instance

Reid Barton (Oct 22 2021 at 12:37):

I think it's also theoretically possible for changing the simp set to affect definitions even if you never use simp outside of proofs, because the definition body could contain a metavariable (probably an implicit one) which gets assigned by the proof

Last updated: Aug 03 2023 at 10:10 UTC