Zulip Chat Archive

Stream: lean4

Topic: congr lemmas for ite/dite


view this post on Zulip Gabriel Ebner (Feb 12 2021 at 09:34):

I'm not sure if this is the right place to comment on this, but the old congr lemmas for ite/dite with the non-canonical decidability instance are coming back in https://github.com/leanprover/lean4/commit/c0f5ab1fa51bffaa571d47feb26a97d8b04b7d99
While these congruence lemmas look useful at first glance, they actually make the simplifier less powerful: simp can only prove ite p a b = ite p a b when the decidability instances in the two ites are definitionally equal (because eqSelf needs them to be).
A longer discussion is in lean#159, the PR removing these lemmas from the community edition.
In short, simp can't prove the following if iteCongr is added:

example (x : ) : (if x > 3  true then 1 else 2) = (if x > 3 then 1 else 2) :=
by simp -- fails in Lean <= 3.7

Last updated: May 07 2021 at 12:15 UTC