From aa568232ad7e90ba89b64af3da65507a4623047e Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Sun, 12 Nov 2023 11:47:13 +1100 Subject: [PATCH] feat: find Decidable instances via unification (#2816) Because `Decidable` carries data, when writing `@[simp]` lemmas which include a `Decidable` instance on the LHS, it is best to use `{_ : Decidable p}` rather than `[Decidable p]` so that non-canonical instances can be found via unification rather than typeclass search. (Previously this behaviour was often being hidden by the default `decide := true` in `simp`.) --- src/Init/Prelude.lean | 6 ++++++ src/Init/SimpLemmas.lean | 6 +++--- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 1987fa1b7cba6..059a562d93f9f 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -806,6 +806,12 @@ decidability instance instead of the proposition, which has no code). If a proposition `p` is `Decidable`, then `(by decide : p)` will prove it by evaluating the decidability instance to `isTrue h` and returning `h`. + +Because `Decidable` carries data, +when writing `@[simp]` lemmas which include a `Decidable` instance on the LHS, +it is best to use `{_ : Decidable p}` rather than `[Decidable p]` +so that non-canonical instances can be found via unification rather than +typeclass search. -/ class inductive Decidable (p : Prop) where /-- Prove that `p` is decidable by supplying a proof of `¬p` -/ diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean index 8e11689814da4..4e1cbfa809cf4 100644 --- a/src/Init/SimpLemmas.lean +++ b/src/Init/SimpLemmas.lean @@ -143,9 +143,9 @@ theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by @[simp] theorem Bool.not_eq_true (b : Bool) : (¬(b = true)) = (b = false) := by cases b <;> decide @[simp] theorem Bool.not_eq_false (b : Bool) : (¬(b = false)) = (b = true) := by cases b <;> decide -@[simp] theorem decide_eq_true_eq [Decidable p] : (decide p = true) = p := propext <| Iff.intro of_decide_eq_true decide_eq_true -@[simp] theorem decide_not [h : Decidable p] : decide (¬ p) = !decide p := by cases h <;> rfl -@[simp] theorem not_decide_eq_true [h : Decidable p] : ((!decide p) = true) = ¬ p := by cases h <;> simp [decide, *] +@[simp] theorem decide_eq_true_eq {_ : Decidable p} : (decide p = true) = p := propext <| Iff.intro of_decide_eq_true decide_eq_true +@[simp] theorem decide_not {h : Decidable p} : decide (¬ p) = !decide p := by cases h <;> rfl +@[simp] theorem not_decide_eq_true {h : Decidable p} : ((!decide p) = true) = ¬ p := by cases h <;> simp [decide, *] @[simp] theorem heq_eq_eq {α : Sort u} (a b : α) : HEq a b = (a = b) := propext <| Iff.intro eq_of_heq heq_of_eq