From 46cc00d5db647c88632ec203ecfb20d64b6ff954 Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Wed, 6 Mar 2024 08:58:12 -0800 Subject: [PATCH] chore: add example to explanation `cond_decide` is not simp (#3615) This just adds a concrete example to the `cond_decide` lemma to explain why it is not a simp rule. --- src/Init/Data/Bool.lean | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean index 927208ddf0..63ccd5d2b8 100644 --- a/src/Init/Data/Bool.lean +++ b/src/Init/Data/Bool.lean @@ -431,12 +431,17 @@ theorem cond_eq_if : (bif b then x else y) = (if b then x else y) := cond_eq_ite @[simp] theorem cond_self (c : Bool) (t : α) : cond c t t = t := by cases c <;> rfl /- -This is a simp rule in Mathlib, but results in non-confluence that is -difficult to fix as decide distributes over propositions. +This is a simp rule in Mathlib, but results in non-confluence that is difficult +to fix as decide distributes over propositions. As an example, observe that +`cond (decide (p ∧ q)) t f` could simplify to either: -A possible fix would be to completely simplify away `cond`, but that -is not taken since it could result in major rewriting of code that is -otherwise purely about `Bool`. +* `if p ∧ q then t else f` via `Bool.cond_decide` or +* `cond (decide p && decide q) t f` via `Bool.decide_and`. + +A possible approach to improve normalization between `cond` and `ite` would be +to completely simplify away `cond` by making `cond_eq_ite` a `simp` rule, but +that has not been taken since it could surprise users to migrate pure `Bool` +operations like `cond` to a mix of `Prop` and `Bool`. -/ theorem cond_decide {α} (p : Prop) [Decidable p] (t e : α) : cond (decide p) t e = if p then t else e := by