From c7f8df2dc0fb62faaa1000497d410f0bc1065a0e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 29 Mar 2025 14:21:35 -0700 Subject: [PATCH] fix: missing `grind` normalization rule (#7724) This PR adds `dite_eq_ite` normalization rule to `grind`. This rule is important to adjust mismatches between a definition and its function induction principle. --- src/Init/Grind/Norm.lean | 1 + tests/lean/run/grind_t1.lean | 3 +++ 2 files changed, 4 insertions(+) diff --git a/src/Init/Grind/Norm.lean b/src/Init/Grind/Norm.lean index 8a35d84467..78a25ff386 100644 --- a/src/Init/Grind/Norm.lean +++ b/src/Init/Grind/Norm.lean @@ -106,6 +106,7 @@ init_grind_norm or_true true_or or_false false_or or_assoc -- ite ite_true ite_false ite_true_false ite_false_true + dite_eq_ite -- Forall forall_and -- Exists diff --git a/tests/lean/run/grind_t1.lean b/tests/lean/run/grind_t1.lean index 848f6fff2c..6a4691b9e3 100644 --- a/tests/lean/run/grind_t1.lean +++ b/tests/lean/run/grind_t1.lean @@ -393,3 +393,6 @@ example [Decidable p] : a = true → p → decide p = a := by example [Decidable p] : false = a → ¬p → decide p = a := by grind + +example (a : Nat) (p q r : Prop) (h₁ : if _ : a < 1 then p else q) (h₂ : r) : (if a < 1 then p else q) ↔ r := by + grind (splits := 0)