From a9e6c41b545b7b53a90e7aa76eca6ea83555309a Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Mon, 9 Sep 2024 21:46:20 +1000
Subject: [PATCH] =?UTF-8?q?feat:=20allow=20simplifying=20dite=5Fnot/decide?=
 =?UTF-8?q?=5Fnot=20with=20only=20Decidable=20(=C2=ACp)=20(#5263)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

These lemmas are mostly useful for ensuring confluence of `simp`, but
rarely useful in proofs. However they don't seem to have any negative
impact.
---
 src/Init/Classical.lean  | 24 ++++++++++++++++++++++++
 src/Init/PropLemmas.lean | 15 +++++++++++++++
 2 files changed, 39 insertions(+)

diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean
index 1dcf28215c80..4d5243ac732c 100644
--- a/src/Init/Classical.lean
+++ b/src/Init/Classical.lean
@@ -134,6 +134,30 @@ The left-to-right direction, double negation elimination (DNE),
 is classically true but not constructively. -/
 @[simp] theorem not_not : ¬¬a ↔ a := Decidable.not_not
 
+/-- Transfer decidability of `¬ p` to decidability of `p`. -/
+-- This can not be an instance as it would be tried everywhere.
+def decidable_of_decidable_not (p : Prop) [h : Decidable (¬ p)] : Decidable p :=
+  match h with
+  | isFalse h => isTrue (Classical.not_not.mp h)
+  | isTrue h => isFalse h
+
+attribute [local instance] decidable_of_decidable_not in
+/-- Negation of the condition `P : Prop` in a `dite` is the same as swapping the branches. -/
+@[simp low] protected theorem dite_not [hn : Decidable (¬p)] (x : ¬p → α) (y : ¬¬p → α) :
+    dite (¬p) x y = dite p (fun h => y (not_not_intro h)) x := by
+  cases hn <;> rename_i g
+  · simp [not_not.mp g]
+  · simp [g]
+
+attribute [local instance] decidable_of_decidable_not in
+/-- Negation of the condition `P : Prop` in a `ite` is the same as swapping the branches. -/
+@[simp low] protected theorem ite_not (p : Prop) [Decidable (¬ p)] (x y : α) : ite (¬p) x y = ite p y x :=
+  dite_not (fun _ => x) (fun _ => y)
+
+attribute [local instance] decidable_of_decidable_not in
+@[simp low] protected theorem decide_not (p : Prop) [Decidable (¬ p)] : decide (¬p) = !decide p :=
+  byCases (fun h : p => by simp_all) (fun h => by simp_all)
+
 @[simp low] theorem not_forall {p : α → Prop} : (¬∀ x, p x) ↔ ∃ x, ¬p x := Decidable.not_forall
 
 theorem not_forall_not {p : α → Prop} : (¬∀ x, ¬p x) ↔ ∃ x, p x := Decidable.not_forall_not
diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean
index 1b49ab341a7c..d754768fd893 100644
--- a/src/Init/PropLemmas.lean
+++ b/src/Init/PropLemmas.lean
@@ -186,6 +186,21 @@ theorem ite_true_same {p q : Prop} [Decidable p] : (if p then p else q) ↔ (¬p
 @[deprecated ite_else_self (since := "2024-08-28")]
 theorem ite_false_same {p q : Prop} [Decidable p] : (if p then q else p) ↔ (p ∧ q) := ite_else_self
 
+/-- If two if-then-else statements only differ by the `Decidable` instances, they are equal. -/
+-- This is useful for ensuring confluence, but rarely otherwise.
+@[simp] theorem ite_eq_ite (p : Prop) {h h' : Decidable p} (x y : α) :
+    (@ite _ p h x y = @ite _ p h' x y) ↔ True := by
+  simp
+  congr
+
+/-- If two if-then-else statements only differ by the `Decidable` instances, they are equal. -/
+-- This is useful for ensuring confluence, but rarely otherwise.
+@[simp] theorem ite_iff_ite (p : Prop) {h h' : Decidable p} (x y : Prop) :
+    (@ite _ p h x y ↔ @ite _ p h' x y) ↔ True := by
+  rw [iff_true]
+  suffices @ite _ p h x y = @ite _ p h' x y by simp [this]
+  congr
+
 /-! ## exists and forall -/
 
 section quantifiers