Topic: congr lemmas for ite/dite
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