From 0125db40a2505f8574b384f1f2ebf13ab9ce8bca Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 23 Feb 2022 16:26:27 -0800
Subject: [PATCH] fix: remove `[..]` annotation from `if` simp theorems

fixes #1025
---
 src/Init/Core.lean       | 10 +++++-----
 tests/lean/run/1025.lean | 20 ++++++++++++++++++++
 2 files changed, 25 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/run/1025.lean

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 9fa94ec949..3d1f9bda33 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -409,28 +409,28 @@ instance {p q} [Decidable p] [Decidable q] : Decidable (p ↔ q) :=
 
 /- if-then-else expression theorems -/
 
-theorem if_pos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t e : α} : (ite c t e) = t :=
+theorem if_pos {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t e : α} : (ite c t e) = t :=
   match h with
   | isTrue  hc  => rfl
   | isFalse hnc => absurd hc hnc
 
-theorem if_neg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t e : α} : (ite c t e) = e :=
+theorem if_neg {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t e : α} : (ite c t e) = e :=
   match h with
   | isTrue hc   => absurd hc hnc
   | isFalse hnc => rfl
 
-theorem dif_pos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t : c → α} {e : ¬ c → α} : (dite c t e) = t hc :=
+theorem dif_pos {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t : c → α} {e : ¬ c → α} : (dite c t e) = t hc :=
   match h with
   | isTrue  hc  => rfl
   | isFalse hnc => absurd hc hnc
 
-theorem dif_neg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t : c → α} {e : ¬ c → α} : (dite c t e) = e hnc :=
+theorem dif_neg {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t : c → α} {e : ¬ c → α} : (dite c t e) = e hnc :=
   match h with
   | isTrue hc   => absurd hc hnc
   | isFalse hnc => rfl
 
 -- Remark: dite and ite are "defally equal" when we ignore the proofs.
-theorem dif_eq_if (c : Prop) [h : Decidable c] {α : Sort u} (t : α) (e : α) : dite c (fun h => t) (fun h => e) = ite c t e :=
+theorem dif_eq_if (c : Prop) {h : Decidable c} {α : Sort u} (t : α) (e : α) : dite c (fun h => t) (fun h => e) = ite c t e :=
   match h with
   | isTrue hc   => rfl
   | isFalse hnc => rfl
diff --git a/tests/lean/run/1025.lean b/tests/lean/run/1025.lean
new file mode 100644
index 0000000000..d855b4446e
--- /dev/null
+++ b/tests/lean/run/1025.lean
@@ -0,0 +1,20 @@
+inductive Vector (α : Type u): Nat → Type u where
+| nil : Vector α 0
+| cons (head : α) (tail : Vector α n) : Vector α (n+1)
+
+namespace Vector
+  def mem (a : α) : Vector α n → Prop
+  | nil => False
+  | cons b l => a = b ∨ mem a l
+
+  def foldr (f : α → β → β) (init : β) : Vector α n → β
+  | nil     => init
+  | cons a l => f a (foldr f init l)
+
+  theorem foldr_max [LE β] [LT β] [DecidableRel (. < . : β → β → Prop)] {v: Vector α n} (f : α → β) (init : β)
+    (h: v.mem y):
+    f y ≤ v.foldr (λ x acc => max (f x) acc) init := by
+    induction v <;> simp only[foldr,max]
+    . admit
+    . split <;> admit
+end Vector