From d08051cf0bf81c87f203f98463a97860f33536a1 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 4 Sep 2024 18:33:24 +1000 Subject: [PATCH] chore: variables appearing on both sides of an iff should be implicit (#5254) --- src/Init/Classical.lean | 2 +- src/Init/Core.lean | 10 +-- src/Init/Data/Array/Lemmas.lean | 16 ++--- src/Init/Data/BEq.lean | 4 +- src/Init/Data/BitVec/Lemmas.lean | 36 +++++----- src/Init/Data/Bool.lean | 100 ++++++++++++++-------------- src/Init/Data/Fin/Lemmas.lean | 10 +-- src/Init/Data/Int/DivModLemmas.lean | 6 +- src/Init/Data/Int/Lemmas.lean | 10 +-- src/Init/Data/Int/Order.lean | 22 +++--- src/Init/Data/List/Attach.lean | 4 +- src/Init/Data/List/Count.lean | 10 +-- src/Init/Data/List/Erase.lean | 8 +-- src/Init/Data/List/Find.lean | 16 ++--- src/Init/Data/List/Lemmas.lean | 34 +++++----- src/Init/Data/List/MinMax.lean | 12 ++-- src/Init/Data/List/Nat/Basic.lean | 4 +- src/Init/Data/List/Nat/Range.lean | 16 ++--- src/Init/Data/List/Nat/Sublist.lean | 8 +-- src/Init/Data/List/Pairwise.lean | 6 +- src/Init/Data/List/Range.lean | 4 +- src/Init/Data/List/Sublist.lean | 14 ++-- src/Init/Data/List/Zip.lean | 4 +- src/Init/Data/Nat/Basic.lean | 4 +- src/Init/Data/Nat/Div.lean | 2 +- src/Init/Data/Nat/Dvd.lean | 4 +- src/Init/Data/Nat/Gcd.lean | 2 +- src/Init/Data/Nat/Lemmas.lean | 6 +- src/Init/Data/Nat/Mod.lean | 4 +- src/Init/Data/String/Basic.lean | 2 +- src/Init/Omega/Int.lean | 18 ++--- src/Init/Omega/IntList.lean | 4 +- src/Init/Omega/Logic.lean | 2 +- src/Init/PropLemmas.lean | 48 ++++++------- src/Init/SimpLemmas.lean | 18 +++-- src/Init/WF.lean | 2 +- src/lake/Lake/Util/Name.lean | 2 +- 37 files changed, 235 insertions(+), 239 deletions(-) diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean index 1c6edb7978..1dcf28215c 100644 --- a/src/Init/Classical.lean +++ b/src/Init/Classical.lean @@ -160,7 +160,7 @@ theorem not_iff : ¬(a ↔ b) ↔ (¬a ↔ b) := Decidable.not_iff @[simp] theorem not_imp : ¬(a → b) ↔ a ∧ ¬b := Decidable.not_imp_iff_and_not -@[simp] theorem imp_and_neg_imp_iff (p q : Prop) : (p → q) ∧ (¬p → q) ↔ q := +@[simp] theorem imp_and_neg_imp_iff (p : Prop) {q : Prop} : (p → q) ∧ (¬p → q) ↔ q := Iff.intro (fun (a : _ ∧ _) => (Classical.em p).rec a.left a.right) (fun a => And.intro (fun _ => a) (fun _ => a)) diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 142745c55f..eb7d29acec 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -800,7 +800,7 @@ theorem cast_heq {α β : Sort u} : (h : α = β) → (a : α) → HEq (cast h a variable {a b c d : Prop} -theorem iff_iff_implies_and_implies (a b : Prop) : (a ↔ b) ↔ (a → b) ∧ (b → a) := +theorem iff_iff_implies_and_implies {a b : Prop} : (a ↔ b) ↔ (a → b) ∧ (b → a) := Iff.intro (fun h => And.intro h.mp h.mpr) (fun h => Iff.intro h.left h.right) theorem Iff.refl (a : Prop) : a ↔ a := @@ -896,7 +896,7 @@ theorem byContradiction [dec : Decidable p] (h : ¬p → False) : p := theorem of_not_not [Decidable p] : ¬ ¬ p → p := fun hnn => byContradiction (fun hn => absurd hn hnn) -theorem not_and_iff_or_not (p q : Prop) [d₁ : Decidable p] [d₂ : Decidable q] : ¬ (p ∧ q) ↔ ¬ p ∨ ¬ q := +theorem not_and_iff_or_not {p q : Prop} [d₁ : Decidable p] [d₂ : Decidable q] : ¬ (p ∧ q) ↔ ¬ p ∨ ¬ q := Iff.intro (fun h => match d₁, d₂ with | isTrue h₁, isTrue h₂ => absurd (And.intro h₁ h₂) h @@ -1351,7 +1351,7 @@ theorem Nat.succ.inj {m n : Nat} : m.succ = n.succ → m = n := theorem Nat.succ.injEq (u v : Nat) : (u.succ = v.succ) = (u = v) := Eq.propIntro Nat.succ.inj (congrArg Nat.succ) -@[simp] theorem beq_iff_eq [BEq α] [LawfulBEq α] (a b : α) : a == b ↔ a = b := +@[simp] theorem beq_iff_eq [BEq α] [LawfulBEq α] {a b : α} : a == b ↔ a = b := ⟨eq_of_beq, by intro h; subst h; exact LawfulBEq.rfl⟩ /-! # Prop lemmas -/ @@ -1416,7 +1416,7 @@ theorem false_of_true_eq_false (h : True = False) : False := false_of_true_iff_ theorem true_eq_false_of_false : False → (True = False) := False.elim -theorem iff_def : (a ↔ b) ↔ (a → b) ∧ (b → a) := iff_iff_implies_and_implies a b +theorem iff_def : (a ↔ b) ↔ (a → b) ∧ (b → a) := iff_iff_implies_and_implies theorem iff_def' : (a ↔ b) ↔ (b → a) ∧ (a → b) := Iff.trans iff_def And.comm theorem true_iff_false : (True ↔ False) ↔ False := iff_false_intro (·.mp True.intro) @@ -1444,7 +1444,7 @@ theorem imp_true_iff (α : Sort u) : (α → True) ↔ True := iff_true_intro (f theorem false_imp_iff (a : Prop) : (False → a) ↔ True := iff_true_intro False.elim -theorem true_imp_iff (α : Prop) : (True → α) ↔ α := imp_iff_right True.intro +theorem true_imp_iff {α : Prop} : (True → α) ↔ α := imp_iff_right True.intro @[simp high] theorem imp_self : (a → a) ↔ True := iff_true_intro id diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 5825040ec1..9c22767fca 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -125,7 +125,7 @@ theorem anyM_stop_le_start [Monad m] (p : α → m Bool) (as : Array α) (start (h : min stop as.size ≤ start) : anyM p as start stop = pure false := by rw [anyM_eq_anyM_loop, anyM.loop, dif_neg (Nat.not_lt.2 h)] -theorem mem_def (a : α) (as : Array α) : a ∈ as ↔ a ∈ as.data := +theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.data := ⟨fun | .mk h => h, Array.Mem.mk⟩ /-! # get -/ @@ -256,7 +256,7 @@ termination_by n - i /-- # mem -/ -theorem mem_data {a : α} {l : Array α} : a ∈ l.data ↔ a ∈ l := (mem_def _ _).symm +theorem mem_data {a : α} {l : Array α} : a ∈ l.data ↔ a ∈ l := mem_def.symm theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun @@ -712,7 +712,7 @@ theorem mem_of_mem_filter {a : α} {l} (h : a ∈ filter p l) : a ∈ l := · simp_all [Id.run, List.filterMap_cons] split <;> simp_all -@[simp] theorem mem_filterMap (f : α → Option β) (l : Array α) {b : β} : +@[simp] theorem mem_filterMap {f : α → Option β} {l : Array α} {b : β} : b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b := by simp only [mem_def, filterMap_data, List.mem_filterMap] @@ -891,7 +891,7 @@ theorem extract_empty_of_size_le_start (as : Array α) {start stop : Nat} (h : a /-! ### any -/ -- Auxiliary for `any_iff_exists`. -theorem anyM_loop_iff_exists (p : α → Bool) (as : Array α) (start stop) (h : stop ≤ as.size) : +theorem anyM_loop_iff_exists {p : α → Bool} {as : Array α} {start stop} (h : stop ≤ as.size) : anyM.loop (m := Id) p as stop h start = true ↔ ∃ i : Fin as.size, start ≤ ↑i ∧ ↑i < stop ∧ p as[i] = true := by unfold anyM.loop @@ -913,7 +913,7 @@ theorem anyM_loop_iff_exists (p : α → Bool) (as : Array α) (start stop) (h : termination_by stop - start -- This could also be proved from `SatisfiesM_anyM_iff_exists` in `Batteries.Data.Array.Init.Monadic` -theorem any_iff_exists (p : α → Bool) (as : Array α) (start stop) : +theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} : any as p start stop ↔ ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop ∧ p as[i] := by dsimp [any, anyM, Id.run] split @@ -925,7 +925,7 @@ theorem any_iff_exists (p : α → Bool) (as : Array α) (start stop) : · rintro ⟨i, ge, _, h⟩ exact ⟨i, by omega, by omega, h⟩ -theorem any_eq_true (p : α → Bool) (as : Array α) : +theorem any_eq_true {p : α → Bool} {as : Array α} : any as p ↔ ∃ i : Fin as.size, p as[i] := by simp [any_iff_exists, Fin.isLt] theorem any_def {p : α → Bool} (as : Array α) : as.any p = as.data.any p := by @@ -939,7 +939,7 @@ theorem all_eq_not_any_not (p : α → Bool) (as : Array α) (start stop) : dsimp [all, allM] rfl -theorem all_iff_forall (p : α → Bool) (as : Array α) (start stop) : +theorem all_iff_forall {p : α → Bool} {as : Array α} {start stop} : all as p start stop ↔ ∀ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop → p as[i] := by rw [all_eq_not_any_not] suffices ¬(any as (!p ·) start stop = true) ↔ @@ -948,7 +948,7 @@ theorem all_iff_forall (p : α → Bool) (as : Array α) (start stop) : rw [any_iff_exists] simp -theorem all_eq_true (p : α → Bool) (as : Array α) : all as p ↔ ∀ i : Fin as.size, p as[i] := by +theorem all_eq_true {p : α → Bool} {as : Array α} : all as p ↔ ∀ i : Fin as.size, p as[i] := by simp [all_iff_forall, Fin.isLt] theorem all_def {p : α → Bool} (as : Array α) : as.all p = as.data.all p := by diff --git a/src/Init/Data/BEq.lean b/src/Init/Data/BEq.lean index 5467f76556..786744b2d9 100644 --- a/src/Init/Data/BEq.lean +++ b/src/Init/Data/BEq.lean @@ -56,5 +56,5 @@ theorem BEq.neq_of_beq_of_neq [BEq α] [PartialEquivBEq α] {a b c : α} : instance (priority := low) [BEq α] [LawfulBEq α] : EquivBEq α where refl := LawfulBEq.rfl - symm h := (beq_iff_eq _ _).2 <| Eq.symm <| (beq_iff_eq _ _).1 h - trans hab hbc := (beq_iff_eq _ _).2 <| ((beq_iff_eq _ _).1 hab).trans <| (beq_iff_eq _ _).1 hbc + symm h := beq_iff_eq.2 <| Eq.symm <| beq_iff_eq.1 h + trans hab hbc := beq_iff_eq.2 <| (beq_iff_eq.1 hab).trans <| beq_iff_eq.1 hbc diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index ba8ebc0e85..3ee9b34ee3 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -99,10 +99,10 @@ theorem eq_of_toNat_eq {n} : ∀ {x y : BitVec n}, x.toNat = y.toNat → x = y @[simp] theorem val_toFin (x : BitVec w) : x.toFin.val = x.toNat := rfl -@[bv_toNat] theorem toNat_eq (x y : BitVec n) : x = y ↔ x.toNat = y.toNat := +@[bv_toNat] theorem toNat_eq {x y : BitVec n} : x = y ↔ x.toNat = y.toNat := Iff.intro (congrArg BitVec.toNat) eq_of_toNat_eq -@[bv_toNat] theorem toNat_ne (x y : BitVec n) : x ≠ y ↔ x.toNat ≠ y.toNat := by +@[bv_toNat] theorem toNat_ne {x y : BitVec n} : x ≠ y ↔ x.toNat ≠ y.toNat := by rw [Ne, toNat_eq] theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i := rfl @@ -229,7 +229,7 @@ theorem eq_of_toFin_eq : ∀ {x y : BitVec w}, x.toFin = y.toFin → x = y theorem ofNat_one (n : Nat) : BitVec.ofNat 1 n = BitVec.ofBool (n % 2 = 1) := by rcases (Nat.mod_two_eq_zero_or_one n) with h | h <;> simp [h, BitVec.ofNat, Fin.ofNat'] -theorem ofBool_eq_iff_eq : ∀(b b' : Bool), BitVec.ofBool b = BitVec.ofBool b' ↔ b = b' := by +theorem ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b' ↔ b = b' := by decide @[simp] theorem not_ofBool : ~~~ (ofBool b) = ofBool (!b) := by cases b <;> rfl @@ -344,10 +344,10 @@ theorem toInt_eq_toNat_cond (x : BitVec n) : (x.toNat : Int) - (2^n : Nat) := rfl -theorem msb_eq_false_iff_two_mul_lt (x : BitVec w) : x.msb = false ↔ 2 * x.toNat < 2^w := by +theorem msb_eq_false_iff_two_mul_lt {x : BitVec w} : x.msb = false ↔ 2 * x.toNat < 2^w := by cases w <;> simp [Nat.pow_succ, Nat.mul_comm _ 2, msb_eq_decide, toNat_of_zero_length] -theorem msb_eq_true_iff_two_mul_ge (x : BitVec w) : x.msb = true ↔ 2 * x.toNat ≥ 2^w := by +theorem msb_eq_true_iff_two_mul_ge {x : BitVec w} : x.msb = true ↔ 2 * x.toNat ≥ 2^w := by simp [← Bool.ne_false_iff, msb_eq_false_iff_two_mul_lt] /-- Characterize `x.toInt` in terms of `x.msb`. -/ @@ -377,10 +377,10 @@ theorem eq_of_toInt_eq {x y : BitVec n} : x.toInt = y.toInt → x = y := by have _ylt := y.isLt split <;> split <;> omega -theorem toInt_inj (x y : BitVec n) : x.toInt = y.toInt ↔ x = y := +theorem toInt_inj {x y : BitVec n} : x.toInt = y.toInt ↔ x = y := Iff.intro eq_of_toInt_eq (congrArg BitVec.toInt) -theorem toInt_ne (x y : BitVec n) : x.toInt ≠ y.toInt ↔ x ≠ y := by +theorem toInt_ne {x y : BitVec n} : x.toInt ≠ y.toInt ↔ x ≠ y := by rw [Ne, toInt_inj] @[simp] theorem toNat_ofInt {n : Nat} (i : Int) : @@ -456,7 +456,7 @@ theorem truncate_eq (x : BitVec n) : truncate n x = x := zeroExtend_eq x simp /-- Moves one-sided left toNat equality to BitVec equality. -/ -theorem toNat_eq_nat (x : BitVec w) (y : Nat) +theorem toNat_eq_nat {x : BitVec w} {y : Nat} : (x.toNat = y) ↔ (y < 2^w ∧ (x = BitVec.ofNat w y)) := by apply Iff.intro · intro eq @@ -465,7 +465,7 @@ theorem toNat_eq_nat (x : BitVec w) (y : Nat) simp [Nat.mod_eq_of_lt, eq] /-- Moves one-sided right toNat equality to BitVec equality. -/ -theorem nat_eq_toNat (x : BitVec w) (y : Nat) +theorem nat_eq_toNat {x : BitVec w} {y : Nat} : (y = x.toNat) ↔ (y < 2^w ∧ (x = BitVec.ofNat w y)) := by rw [@eq_comm _ _ x.toNat] apply toNat_eq_nat @@ -984,7 +984,7 @@ theorem sshiftRight_eq_of_msb_false {x : BitVec w} {s : Nat} (h : x.msb = false) (x.sshiftRight s) = x >>> s := by apply BitVec.eq_of_toNat_eq rw [BitVec.sshiftRight_eq, BitVec.toInt_eq_toNat_cond] - have hxbound : 2 * x.toNat < 2 ^ w := (BitVec.msb_eq_false_iff_two_mul_lt x).mp h + have hxbound : 2 * x.toNat < 2 ^ w := BitVec.msb_eq_false_iff_two_mul_lt.mp h simp only [hxbound, ↓reduceIte, Int.natCast_shiftRight, Int.ofNat_eq_coe, ofInt_natCast, toNat_ofNat, toNat_ushiftRight] replace hxbound : x.toNat >>> s < 2 ^ w := by @@ -1003,7 +1003,7 @@ theorem sshiftRight_eq_of_msb_true {x : BitVec w} {s : Nat} (h : x.msb = true) : rcases w with rfl | w · simp [toNat_of_zero_length] · rw [BitVec.sshiftRight_eq, BitVec.toInt_eq_toNat_cond] - have hxbound : (2 * x.toNat ≥ 2 ^ (w + 1)) := (BitVec.msb_eq_true_iff_two_mul_ge x).mp h + have hxbound : (2 * x.toNat ≥ 2 ^ (w + 1)) := BitVec.msb_eq_true_iff_two_mul_ge.mp h replace hxbound : ¬ (2 * x.toNat < 2 ^ (w + 1)) := by omega simp only [hxbound, ↓reduceIte, toNat_ofInt, toNat_not, toNat_ushiftRight] rw [← Int.subNatNat_eq_coe, Int.subNatNat_of_lt (by omega), @@ -1611,22 +1611,22 @@ theorem ofInt_mul {n} (x y : Int) : BitVec.ofInt n (x * y) = /-! ### le and lt -/ -@[bv_toNat] theorem le_def (x y : BitVec n) : +@[bv_toNat] theorem le_def {x y : BitVec n} : x ≤ y ↔ x.toNat ≤ y.toNat := Iff.rfl -@[simp] theorem le_ofFin (x : BitVec n) (y : Fin (2^n)) : +@[simp] theorem le_ofFin {x : BitVec n} {y : Fin (2^n)} : x ≤ BitVec.ofFin y ↔ x.toFin ≤ y := Iff.rfl -@[simp] theorem ofFin_le (x : Fin (2^n)) (y : BitVec n) : +@[simp] theorem ofFin_le {x : Fin (2^n)} {y : BitVec n} : BitVec.ofFin x ≤ y ↔ x ≤ y.toFin := Iff.rfl -@[simp] theorem ofNat_le_ofNat {n} (x y : Nat) : (BitVec.ofNat n x) ≤ (BitVec.ofNat n y) ↔ x % 2^n ≤ y % 2^n := by +@[simp] theorem ofNat_le_ofNat {n} {x y : Nat} : (BitVec.ofNat n x) ≤ (BitVec.ofNat n y) ↔ x % 2^n ≤ y % 2^n := by simp [le_def] -@[bv_toNat] theorem lt_def (x y : BitVec n) : +@[bv_toNat] theorem lt_def {x y : BitVec n} : x < y ↔ x.toNat < y.toNat := Iff.rfl -@[simp] theorem lt_ofFin (x : BitVec n) (y : Fin (2^n)) : +@[simp] theorem lt_ofFin {x : BitVec n} {y : Fin (2^n)} : x < BitVec.ofFin y ↔ x.toFin < y := Iff.rfl -@[simp] theorem ofFin_lt (x : Fin (2^n)) (y : BitVec n) : +@[simp] theorem ofFin_lt {x : Fin (2^n)} {y : BitVec n} : BitVec.ofFin x < y ↔ x < y.toFin := Iff.rfl @[simp] theorem ofNat_lt_ofNat {n} (x y : Nat) : BitVec.ofNat n x < BitVec.ofNat n y ↔ x % 2^n < y % 2^n := by simp [lt_def] diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean index c83d631afa..e5910ef86e 100644 --- a/src/Init/Data/Bool.lean +++ b/src/Init/Data/Bool.lean @@ -57,14 +57,14 @@ theorem decide_false_eq {b : Bool} [Decidable (false = b)] : decide (false = b) -- These lemmas assist with confluence. @[simp] theorem eq_false_imp_eq_true_iff : - ∀(a b : Bool), ((a = false → b = true) ↔ (b = false → a = true)) = True := by decide + ∀ (a b : Bool), ((a = false → b = true) ↔ (b = false → a = true)) = True := by decide @[simp] theorem eq_true_imp_eq_false_iff : - ∀(a b : Bool), ((a = true → b = false) ↔ (b = true → a = false)) = True := by decide + ∀ (a b : Bool), ((a = true → b = false) ↔ (b = true → a = false)) = True := by decide /-! ### and -/ -@[simp] theorem and_self_left : ∀(a b : Bool), (a && (a && b)) = (a && b) := by decide -@[simp] theorem and_self_right : ∀(a b : Bool), ((a && b) && b) = (a && b) := by decide +@[simp] theorem and_self_left : ∀ (a b : Bool), (a && (a && b)) = (a && b) := by decide +@[simp] theorem and_self_right : ∀ (a b : Bool), ((a && b) && b) = (a && b) := by decide @[simp] theorem not_and_self : ∀ (x : Bool), (!x && x) = false := by decide @[simp] theorem and_not_self : ∀ (x : Bool), (x && !x) = false := by decide @@ -76,8 +76,8 @@ Added for confluence with `not_and_self` `and_not_self` on term 1. `(b = true ∨ !b = true)` via `Bool.and_eq_true` 2. `false = true` via `Bool.and_not_self` -/ -@[simp] theorem eq_true_and_eq_false_self : ∀(b : Bool), (b = true ∧ b = false) ↔ False := by decide -@[simp] theorem eq_false_and_eq_true_self : ∀(b : Bool), (b = false ∧ b = true) ↔ False := by decide +@[simp] theorem eq_true_and_eq_false_self : ∀ (b : Bool), (b = true ∧ b = false) ↔ False := by decide +@[simp] theorem eq_false_and_eq_true_self : ∀ (b : Bool), (b = false ∧ b = true) ↔ False := by decide theorem and_comm : ∀ (x y : Bool), (x && y) = (y && x) := by decide instance : Std.Commutative (· && ·) := ⟨and_comm⟩ @@ -92,20 +92,20 @@ Needed for confluence of term `(a && b) ↔ a` which reduces to `(a && b) = a` v `Bool.coe_iff_coe` and `a → b` via `Bool.and_eq_true` and `and_iff_left_iff_imp`. -/ -@[simp] theorem and_iff_left_iff_imp : ∀(a b : Bool), ((a && b) = a) ↔ (a → b) := by decide -@[simp] theorem and_iff_right_iff_imp : ∀(a b : Bool), ((a && b) = b) ↔ (b → a) := by decide -@[simp] theorem iff_self_and : ∀(a b : Bool), (a = (a && b)) ↔ (a → b) := by decide -@[simp] theorem iff_and_self : ∀(a b : Bool), (b = (a && b)) ↔ (b → a) := by decide +@[simp] theorem and_iff_left_iff_imp : ∀ {a b : Bool}, ((a && b) = a) ↔ (a → b) := by decide +@[simp] theorem and_iff_right_iff_imp : ∀ {a b : Bool}, ((a && b) = b) ↔ (b → a) := by decide +@[simp] theorem iff_self_and : ∀ {a b : Bool}, (a = (a && b)) ↔ (a → b) := by decide +@[simp] theorem iff_and_self : ∀ {a b : Bool}, (b = (a && b)) ↔ (b → a) := by decide -@[simp] theorem not_and_iff_left_iff_imp : ∀ (a b : Bool), ((!a && b) = a) ↔ !a ∧ !b := by decide -@[simp] theorem and_not_iff_right_iff_imp : ∀ (a b : Bool), ((a && !b) = b) ↔ !a ∧ !b := by decide -@[simp] theorem iff_not_self_and : ∀ (a b : Bool), (a = (!a && b)) ↔ !a ∧ !b := by decide -@[simp] theorem iff_and_not_self : ∀ (a b : Bool), (b = (a && !b)) ↔ !a ∧ !b := by decide +@[simp] theorem not_and_iff_left_iff_imp : ∀ {a b : Bool}, ((!a && b) = a) ↔ !a ∧ !b := by decide +@[simp] theorem and_not_iff_right_iff_imp : ∀ {a b : Bool}, ((a && !b) = b) ↔ !a ∧ !b := by decide +@[simp] theorem iff_not_self_and : ∀ {a b : Bool}, (a = (!a && b)) ↔ !a ∧ !b := by decide +@[simp] theorem iff_and_not_self : ∀ {a b : Bool}, (b = (a && !b)) ↔ !a ∧ !b := by decide /-! ### or -/ -@[simp] theorem or_self_left : ∀(a b : Bool), (a || (a || b)) = (a || b) := by decide -@[simp] theorem or_self_right : ∀(a b : Bool), ((a || b) || b) = (a || b) := by decide +@[simp] theorem or_self_left : ∀ (a b : Bool), (a || (a || b)) = (a || b) := by decide +@[simp] theorem or_self_right : ∀ (a b : Bool), ((a || b) || b) = (a || b) := by decide @[simp] theorem not_or_self : ∀ (x : Bool), (!x || x) = true := by decide @[simp] theorem or_not_self : ∀ (x : Bool), (x || !x) = true := by decide @@ -126,15 +126,15 @@ Needed for confluence of term `(a || b) ↔ a` which reduces to `(a || b) = a` v `Bool.coe_iff_coe` and `a → b` via `Bool.or_eq_true` and `and_iff_left_iff_imp`. -/ -@[simp] theorem or_iff_left_iff_imp : ∀(a b : Bool), ((a || b) = a) ↔ (b → a) := by decide -@[simp] theorem or_iff_right_iff_imp : ∀(a b : Bool), ((a || b) = b) ↔ (a → b) := by decide -@[simp] theorem iff_self_or : ∀(a b : Bool), (a = (a || b)) ↔ (b → a) := by decide -@[simp] theorem iff_or_self : ∀(a b : Bool), (b = (a || b)) ↔ (a → b) := by decide +@[simp] theorem or_iff_left_iff_imp : ∀ {a b : Bool}, ((a || b) = a) ↔ (b → a) := by decide +@[simp] theorem or_iff_right_iff_imp : ∀ {a b : Bool}, ((a || b) = b) ↔ (a → b) := by decide +@[simp] theorem iff_self_or : ∀ {a b : Bool}, (a = (a || b)) ↔ (b → a) := by decide +@[simp] theorem iff_or_self : ∀ {a b : Bool}, (b = (a || b)) ↔ (a → b) := by decide -@[simp] theorem not_or_iff_left_iff_imp : ∀ (a b : Bool), ((!a || b) = a) ↔ a ∧ b := by decide -@[simp] theorem or_not_iff_right_iff_imp : ∀ (a b : Bool), ((a || !b) = b) ↔ a ∧ b := by decide -@[simp] theorem iff_not_self_or : ∀ (a b : Bool), (a = (!a || b)) ↔ a ∧ b := by decide -@[simp] theorem iff_or_not_self : ∀ (a b : Bool), (b = (a || !b)) ↔ a ∧ b := by decide +@[simp] theorem not_or_iff_left_iff_imp : ∀ {a b : Bool}, ((!a || b) = a) ↔ a ∧ b := by decide +@[simp] theorem or_not_iff_right_iff_imp : ∀ {a b : Bool}, ((a || !b) = b) ↔ a ∧ b := by decide +@[simp] theorem iff_not_self_or : ∀ {a b : Bool}, (a = (!a || b)) ↔ a ∧ b := by decide +@[simp] theorem iff_or_not_self : ∀ {a b : Bool}, (b = (a || !b)) ↔ a ∧ b := by decide theorem or_comm : ∀ (x y : Bool), (x || y) = (y || x) := by decide instance : Std.Commutative (· || ·) := ⟨or_comm⟩ @@ -159,10 +159,10 @@ theorem and_xor_distrib_right : ∀ (x y z : Bool), (xor x y && z) = xor (x && z /-- De Morgan's law for boolean or -/ @[simp] theorem not_or : ∀ (x y : Bool), (!(x || y)) = (!x && !y) := by decide -theorem and_eq_true_iff (x y : Bool) : (x && y) = true ↔ x = true ∧ y = true := +theorem and_eq_true_iff {x y : Bool} : (x && y) = true ↔ x = true ∧ y = true := Iff.of_eq (and_eq_true x y) -theorem and_eq_false_iff : ∀ (x y : Bool), (x && y) = false ↔ x = false ∨ y = false := by decide +theorem and_eq_false_iff : ∀ {x y : Bool}, (x && y) = false ↔ x = false ∨ y = false := by decide /- New simp rule that replaces `Bool.and_eq_false_eq_eq_false_or_eq_false` in @@ -177,11 +177,11 @@ Consider the term: `¬((b && c) = true)`: 1. Further reduces to `b = false ∨ c = false` via `Bool.and_eq_false_eq_eq_false_or_eq_false`. 2. Further reduces to `b = true → c = false` via `not_and` and `Bool.not_eq_true`. -/ -@[simp] theorem and_eq_false_imp : ∀ (x y : Bool), (x && y) = false ↔ (x = true → y = false) := by decide +@[simp] theorem and_eq_false_imp : ∀ {x y : Bool}, (x && y) = false ↔ (x = true → y = false) := by decide -theorem or_eq_true_iff : ∀ (x y : Bool), (x || y) = true ↔ x = true ∨ y = true := by simp +theorem or_eq_true_iff : ∀ {x y : Bool}, (x || y) = true ↔ x = true ∨ y = true := by simp -@[simp] theorem or_eq_false_iff : ∀ (x y : Bool), (x || y) = false ↔ x = false ∧ y = false := by decide +@[simp] theorem or_eq_false_iff : ∀ {x y : Bool}, (x || y) = false ↔ x = false ∧ y = false := by decide /-! ### eq/beq/bne -/ @@ -241,8 +241,8 @@ theorem not_bne_not : ∀ (x y : Bool), ((!x) != (!y)) = (x != y) := by simp @[simp] theorem bne_assoc : ∀ (x y z : Bool), ((x != y) != z) = (x != (y != z)) := by decide instance : Std.Associative (· != ·) := ⟨bne_assoc⟩ -@[simp] theorem bne_left_inj : ∀ (x y z : Bool), (x != y) = (x != z) ↔ y = z := by decide -@[simp] theorem bne_right_inj : ∀ (x y z : Bool), (x != z) = (y != z) ↔ x = y := by decide +@[simp] theorem bne_left_inj : ∀ {x y z : Bool}, (x != y) = (x != z) ↔ y = z := by decide +@[simp] theorem bne_right_inj : ∀ {x y z : Bool}, (x != z) = (y != z) ↔ x = y := by decide theorem eq_not_of_ne : ∀ {x y : Bool}, x ≠ y → x = !y := by decide @@ -254,8 +254,8 @@ theorem beq_eq_decide_eq [BEq α] [LawfulBEq α] [DecidableEq α] (a b : α) : · simp [ne_of_beq_false h] · simp [eq_of_beq h] -theorem eq_not : ∀ (a b : Bool), (a = (!b)) ↔ (a ≠ b) := by decide -theorem not_eq : ∀ (a b : Bool), ((!a) = b) ↔ (a ≠ b) := by decide +theorem eq_not : ∀ {a b : Bool}, (a = (!b)) ↔ (a ≠ b) := by decide +theorem not_eq : ∀ {a b : Bool}, ((!a) = b) ↔ (a ≠ b) := by decide @[simp] theorem not_eq_not : ∀ {a b : Bool}, ¬a = !b ↔ a = b := by decide @[simp] theorem not_not_eq : ∀ {a b : Bool}, ¬(!a) = b ↔ a = b := by decide @@ -266,16 +266,16 @@ This helps confluence, and also helps combining pairs of `!`s. -/ @[simp] theorem not_eq_eq_eq_not : ∀ {a b : Bool}, ((!a) = b) ↔ (a = !b) := by decide -@[simp] theorem coe_iff_coe : ∀(a b : Bool), (a ↔ b) ↔ a = b := by decide +@[simp] theorem coe_iff_coe : ∀{a b : Bool}, (a ↔ b) ↔ a = b := by decide -@[simp] theorem coe_true_iff_false : ∀(a b : Bool), (a ↔ b = false) ↔ a = (!b) := by decide -@[simp] theorem coe_false_iff_true : ∀(a b : Bool), (a = false ↔ b) ↔ (!a) = b := by decide -@[simp] theorem coe_false_iff_false : ∀(a b : Bool), (a = false ↔ b = false) ↔ (!a) = (!b) := by decide +@[simp] theorem coe_true_iff_false : ∀{a b : Bool}, (a ↔ b = false) ↔ a = (!b) := by decide +@[simp] theorem coe_false_iff_true : ∀{a b : Bool}, (a = false ↔ b) ↔ (!a) = b := by decide +@[simp] theorem coe_false_iff_false : ∀{a b : Bool}, (a = false ↔ b = false) ↔ (!a) = (!b) := by decide /-! ### beq properties -/ theorem beq_comm {α} [BEq α] [LawfulBEq α] {a b : α} : (a == b) = (b == a) := - (Bool.coe_iff_coe (a == b) (b == a)).mp (by simp [@eq_comm α]) + Bool.coe_iff_coe.mp (by simp [@eq_comm α]) /-! ### xor -/ @@ -307,9 +307,9 @@ theorem xor_right_comm : ∀ (x y z : Bool), xor (xor x y) z = xor (xor x z) y : theorem xor_assoc : ∀ (x y z : Bool), xor (xor x y) z = xor x (xor y z) := bne_assoc -theorem xor_left_inj : ∀ (x y z : Bool), xor x y = xor x z ↔ y = z := bne_left_inj +theorem xor_left_inj : ∀ {x y z : Bool}, xor x y = xor x z ↔ y = z := bne_left_inj -theorem xor_right_inj : ∀ (x y z : Bool), xor x z = xor y z ↔ x = y := bne_right_inj +theorem xor_right_inj : ∀ {x y z : Bool}, xor x z = xor y z ↔ x = y := bne_right_inj /-! ### le/lt -/ @@ -390,9 +390,9 @@ theorem toNat_le (c : Bool) : c.toNat ≤ 1 := by theorem toNat_lt (b : Bool) : b.toNat < 2 := Nat.lt_succ_of_le (toNat_le _) -@[simp] theorem toNat_eq_zero (b : Bool) : b.toNat = 0 ↔ b = false := by +@[simp] theorem toNat_eq_zero {b : Bool} : b.toNat = 0 ↔ b = false := by cases b <;> simp -@[simp] theorem toNat_eq_one (b : Bool) : b.toNat = 1 ↔ b = true := by +@[simp] theorem toNat_eq_one {b : Bool} : b.toNat = 1 ↔ b = true := by cases b <;> simp /-! ### ite -/ @@ -438,22 +438,22 @@ lemmas. -/ @[simp] -theorem not_ite_eq_true_eq_true (p : Prop) [h : Decidable p] (b c : Bool) : +theorem not_ite_eq_true_eq_true {p : Prop} [h : Decidable p] {b c : Bool} : ¬(ite p (b = true) (c = true)) ↔ (ite p (b = false) (c = false)) := by cases h with | _ p => simp [p] @[simp] -theorem not_ite_eq_false_eq_false (p : Prop) [h : Decidable p] (b c : Bool) : +theorem not_ite_eq_false_eq_false {p : Prop} [h : Decidable p] {b c : Bool} : ¬(ite p (b = false) (c = false)) ↔ (ite p (b = true) (c = true)) := by cases h with | _ p => simp [p] @[simp] -theorem not_ite_eq_true_eq_false (p : Prop) [h : Decidable p] (b c : Bool) : +theorem not_ite_eq_true_eq_false {p : Prop} [h : Decidable p] {b c : Bool} : ¬(ite p (b = true) (c = false)) ↔ (ite p (b = false) (c = true)) := by cases h with | _ p => simp [p] @[simp] -theorem not_ite_eq_false_eq_true (p : Prop) [h : Decidable p] (b c : Bool) : +theorem not_ite_eq_false_eq_true {p : Prop} [h : Decidable p] {b c : Bool} : ¬(ite p (b = false) (c = true)) ↔ (ite p (b = true) (c = false)) := by cases h with | _ p => simp [p] @@ -462,14 +462,14 @@ It would be nice to have this for confluence between `if_true_left` and `ite_fal `if b = true then True else b = true`. However the discrimination tree key is just `→`, so this is tried too often. -/ -theorem eq_false_imp_eq_true : ∀(b:Bool), (b = false → b = true) ↔ (b = true) := by decide +theorem eq_false_imp_eq_true : ∀ {b : Bool}, (b = false → b = true) ↔ (b = true) := by decide /- It would be nice to have this for confluence between `if_true_left` and `ite_false_same` on `if b = false then True else b = false`. However the discrimination tree key is just `→`, so this is tried too often. -/ -theorem eq_true_imp_eq_false : ∀(b:Bool), (b = true → b = false) ↔ (b = false) := by decide +theorem eq_true_imp_eq_false : ∀ {b : Bool}, (b = true → b = false) ↔ (b = false) := by decide /-! ### forall -/ @@ -524,11 +524,11 @@ theorem cond_decide {α} (p : Prop) [Decidable p] (t e : α) : cond (decide p) t e = if p then t else e := by simp [cond_eq_ite] -@[simp] theorem cond_eq_ite_iff (a : Bool) (p : Prop) [h : Decidable p] (x y u v : α) : +@[simp] theorem cond_eq_ite_iff {a : Bool} {p : Prop} [h : Decidable p] {x y u v : α} : (cond a x y = ite p u v) ↔ ite a x y = ite p u v := by simp [Bool.cond_eq_ite] -@[simp] theorem ite_eq_cond_iff (p : Prop) [h : Decidable p] (a : Bool) (x y u v : α) : +@[simp] theorem ite_eq_cond_iff {p : Prop} {a : Bool} [h : Decidable p] {x y u v : α} : (ite p x y = cond a u v) ↔ ite p x y = ite a u v := by simp [Bool.cond_eq_ite] diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean index 2ee40b879b..fab873d935 100644 --- a/src/Init/Data/Fin/Lemmas.lean +++ b/src/Init/Data/Fin/Lemmas.lean @@ -383,7 +383,7 @@ theorem castSucc_lt_iff_succ_le {n : Nat} {i : Fin n} {j : Fin (n + 1)} : @[simp] theorem succ_last (n : Nat) : (last n).succ = last n.succ := rfl -@[simp] theorem succ_eq_last_succ {n : Nat} (i : Fin n.succ) : +@[simp] theorem succ_eq_last_succ {n : Nat} {i : Fin n.succ} : i.succ = last (n + 1) ↔ i = last n := by rw [← succ_last, succ_inj] @[simp] theorem castSucc_castLT (i : Fin (n + 1)) (h : (i : Nat) < n) : @@ -407,10 +407,10 @@ theorem castSucc_lt_last (a : Fin n) : castSucc a < last n := a.is_lt theorem castSucc_pos {i : Fin (n + 1)} (h : 0 < i) : 0 < castSucc i := by simpa [lt_def] using h -@[simp] theorem castSucc_eq_zero_iff (a : Fin (n + 1)) : castSucc a = 0 ↔ a = 0 := by simp [Fin.ext_iff] +@[simp] theorem castSucc_eq_zero_iff {a : Fin (n + 1)} : castSucc a = 0 ↔ a = 0 := by simp [Fin.ext_iff] -theorem castSucc_ne_zero_iff (a : Fin (n + 1)) : castSucc a ≠ 0 ↔ a ≠ 0 := - not_congr <| castSucc_eq_zero_iff a +theorem castSucc_ne_zero_iff {a : Fin (n + 1)} : castSucc a ≠ 0 ↔ a ≠ 0 := + not_congr <| castSucc_eq_zero_iff theorem castSucc_fin_succ (n : Nat) (j : Fin n) : castSucc (Fin.succ j) = Fin.succ (castSucc j) := by simp [Fin.ext_iff] @@ -525,7 +525,7 @@ theorem pred_succ (i : Fin n) {h : i.succ ≠ 0} : i.succ.pred h = i := by cases i rfl -theorem pred_eq_iff_eq_succ {n : Nat} (i : Fin (n + 1)) (hi : i ≠ 0) (j : Fin n) : +theorem pred_eq_iff_eq_succ {n : Nat} {i : Fin (n + 1)} (hi : i ≠ 0) {j : Fin n} : i.pred hi = j ↔ i = j.succ := ⟨fun h => by simp only [← h, Fin.succ_pred], fun h => by simp only [h, Fin.pred_succ]⟩ diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean index 12e19651a8..a99d0b66a8 100644 --- a/src/Init/Data/Int/DivModLemmas.lean +++ b/src/Init/Data/Int/DivModLemmas.lean @@ -600,7 +600,7 @@ theorem dvd_emod_sub_self {x : Int} {m : Nat} : (m : Int) ∣ x % m - x := by theorem emod_eq_zero_of_dvd : ∀ {a b : Int}, a ∣ b → b % a = 0 | _, _, ⟨_, rfl⟩ => mul_emod_right .. -theorem dvd_iff_emod_eq_zero (a b : Int) : a ∣ b ↔ b % a = 0 := +theorem dvd_iff_emod_eq_zero {a b : Int} : a ∣ b ↔ b % a = 0 := ⟨emod_eq_zero_of_dvd, dvd_of_emod_eq_zero⟩ @[simp] theorem neg_mul_emod_left (a b : Int) : -(a * b) % b = 0 := by @@ -784,7 +784,7 @@ protected theorem lt_ediv_of_mul_lt {a b c : Int} (H1 : 0 ≤ b) (H2 : b ∣ c) a < c / b := Int.lt_of_not_ge <| mt (Int.le_mul_of_ediv_le H1 H2) (Int.not_le_of_gt H3) -protected theorem lt_ediv_iff_mul_lt {a b : Int} (c : Int) (H : 0 < c) (H' : c ∣ b) : +protected theorem lt_ediv_iff_mul_lt {a b : Int} {c : Int} (H : 0 < c) (H' : c ∣ b) : a < b / c ↔ a * c < b := ⟨Int.mul_lt_of_lt_ediv H, Int.lt_ediv_of_mul_lt (Int.le_of_lt H) H'⟩ @@ -918,7 +918,7 @@ theorem mod_nonneg : ∀ {a : Int} (b : Int), 0 ≤ a → 0 ≤ mod a b theorem mod_eq_zero_of_dvd : ∀ {a b : Int}, a ∣ b → mod b a = 0 | _, _, ⟨_, rfl⟩ => mul_mod_right .. -theorem dvd_iff_mod_eq_zero (a b : Int) : a ∣ b ↔ mod b a = 0 := +theorem dvd_iff_mod_eq_zero {a b : Int} : a ∣ b ↔ mod b a = 0 := ⟨mod_eq_zero_of_dvd, dvd_of_mod_eq_zero⟩ @[simp] theorem neg_mul_mod_right (a b : Int) : (-(a * b)).mod a = 0 := by diff --git a/src/Init/Data/Int/Lemmas.lean b/src/Init/Data/Int/Lemmas.lean index ba8ef59721..8f10273f5c 100644 --- a/src/Init/Data/Int/Lemmas.lean +++ b/src/Init/Data/Int/Lemmas.lean @@ -329,22 +329,22 @@ theorem toNat_sub (m n : Nat) : toNat (m - n) = m - n := by /- ## add/sub injectivity -/ @[simp] -protected theorem add_right_inj (i j k : Int) : (i + k = j + k) ↔ i = j := by +protected theorem add_right_inj {i j : Int} (k : Int) : (i + k = j + k) ↔ i = j := by apply Iff.intro · intro p rw [←Int.add_sub_cancel i k, ←Int.add_sub_cancel j k, p] · exact congrArg (· + k) @[simp] -protected theorem add_left_inj (i j k : Int) : (k + i = k + j) ↔ i = j := by +protected theorem add_left_inj {i j : Int} (k : Int) : (k + i = k + j) ↔ i = j := by simp [Int.add_comm k] @[simp] -protected theorem sub_left_inj (i j k : Int) : (k - i = k - j) ↔ i = j := by +protected theorem sub_left_inj {i j : Int} (k : Int) : (k - i = k - j) ↔ i = j := by simp [Int.sub_eq_add_neg, Int.neg_inj] @[simp] -protected theorem sub_right_inj (i j k : Int) : (i - k = j - k) ↔ i = j := by +protected theorem sub_right_inj {i j : Int} (k : Int) : (i - k = j - k) ↔ i = j := by simp [Int.sub_eq_add_neg] /- ## Ring properties -/ @@ -487,7 +487,7 @@ protected theorem mul_eq_zero {a b : Int} : a * b = 0 ↔ a = 0 ∨ b = 0 := by protected theorem mul_ne_zero {a b : Int} (a0 : a ≠ 0) (b0 : b ≠ 0) : a * b ≠ 0 := Or.rec a0 b0 ∘ Int.mul_eq_zero.mp -@[simp] protected theorem mul_ne_zero_iff (a b : Int) : a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0 := by +@[simp] protected theorem mul_ne_zero_iff {a b : Int} : a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0 := by rw [ne_eq, Int.mul_eq_zero, not_or, ne_eq] protected theorem eq_of_mul_eq_mul_right {a b c : Int} (ha : a ≠ 0) (h : b * a = c * a) : b = c := diff --git a/src/Init/Data/Int/Order.lean b/src/Init/Data/Int/Order.lean index 411f7a054a..bb9f043dd7 100644 --- a/src/Init/Data/Int/Order.lean +++ b/src/Init/Data/Int/Order.lean @@ -26,9 +26,9 @@ theorem nonneg_or_nonneg_neg : ∀ (a : Int), NonNeg a ∨ NonNeg (-a) | (_:Nat) => .inl ⟨_⟩ | -[_+1] => .inr ⟨_⟩ -theorem le_def (a b : Int) : a ≤ b ↔ NonNeg (b - a) := .rfl +theorem le_def {a b : Int} : a ≤ b ↔ NonNeg (b - a) := .rfl -theorem lt_iff_add_one_le (a b : Int) : a < b ↔ a + 1 ≤ b := .rfl +theorem lt_iff_add_one_le {a b : Int} : a < b ↔ a + 1 ≤ b := .rfl theorem le.intro_sub {a b : Int} (n : Nat) (h : b - a = n) : a ≤ b := by simp [le_def, h]; constructor @@ -531,7 +531,7 @@ theorem toNat_sub_toNat_neg : ∀ n : Int, ↑n.toNat - ↑(-n).toNat = n /-! ### toNat' -/ -theorem mem_toNat' : ∀ (a : Int) (n : Nat), toNat' a = some n ↔ a = n +theorem mem_toNat' : ∀ {a : Int} {n : Nat}, toNat' a = some n ↔ a = n | (m : Nat), n => by simp [toNat', Int.ofNat_inj] | -[m+1], n => by constructor <;> nofun @@ -829,10 +829,10 @@ protected theorem lt_add_of_neg_lt_sub_right {a b c : Int} (h : -b < a - c) : c protected theorem neg_lt_sub_right_of_lt_add {a b c : Int} (h : c < a + b) : -b < a - c := Int.lt_sub_left_of_add_lt (Int.sub_right_lt_of_lt_add h) -protected theorem add_lt_iff (a b c : Int) : a + b < c ↔ a < -b + c := by +protected theorem add_lt_iff {a b c : Int} : a + b < c ↔ a < -b + c := by rw [← Int.add_lt_add_iff_left (-b), Int.add_comm (-b), Int.add_neg_cancel_right] -protected theorem sub_lt_iff (a b c : Int) : a - b < c ↔ a < c + b := +protected theorem sub_lt_iff {a b c : Int} : a - b < c ↔ a < c + b := Iff.intro Int.lt_add_of_sub_right_lt Int.sub_right_lt_of_lt_add protected theorem sub_lt_of_sub_lt {a b c : Int} (h : a - b < c) : a - c < b := @@ -853,12 +853,10 @@ protected theorem lt_of_sub_lt_sub_left {a b c : Int} (h : c - a < c - b) : b < protected theorem lt_of_sub_lt_sub_right {a b c : Int} (h : a - c < b - c) : a < b := Int.lt_of_add_lt_add_right h -@[simp] protected theorem sub_lt_sub_left_iff (a b c : Int) : - c - a < c - b ↔ b < a := +@[simp] protected theorem sub_lt_sub_left_iff {a b c : Int} : c - a < c - b ↔ b < a := ⟨Int.lt_of_sub_lt_sub_left, (Int.sub_lt_sub_left · c)⟩ -@[simp] protected theorem sub_lt_sub_right_iff (a b c : Int) : - a - c < b - c ↔ a < b := +@[simp] protected theorem sub_lt_sub_right_iff {a b c : Int} : a - c < b - c ↔ a < b := ⟨Int.lt_of_sub_lt_sub_right, (Int.sub_lt_sub_right · c)⟩ protected theorem sub_lt_sub_of_le_of_lt {a b c d : Int} @@ -990,13 +988,13 @@ theorem neg_of_sign_eq_neg_one : ∀ {a : Int}, sign a = -1 → a < 0 | 0, h => nomatch h | -[_+1], _ => negSucc_lt_zero _ -theorem sign_eq_one_iff_pos (a : Int) : sign a = 1 ↔ 0 < a := +theorem sign_eq_one_iff_pos {a : Int} : sign a = 1 ↔ 0 < a := ⟨pos_of_sign_eq_one, sign_eq_one_of_pos⟩ -theorem sign_eq_neg_one_iff_neg (a : Int) : sign a = -1 ↔ a < 0 := +theorem sign_eq_neg_one_iff_neg {a : Int} : sign a = -1 ↔ a < 0 := ⟨neg_of_sign_eq_neg_one, sign_eq_neg_one_of_neg⟩ -@[simp] theorem sign_eq_zero_iff_zero (a : Int) : sign a = 0 ↔ a = 0 := +@[simp] theorem sign_eq_zero_iff_zero {a : Int} : sign a = 0 ↔ a = 0 := ⟨eq_zero_of_sign_eq_zero, fun h => by rw [h, sign_zero]⟩ @[simp] theorem sign_sign : sign (sign x) = sign x := by diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean index 07e8c7bbbd..0182934e8e 100644 --- a/src/Init/Data/List/Attach.lean +++ b/src/Init/Data/List/Attach.lean @@ -128,12 +128,12 @@ theorem length_attach (L : List α) : L.attach.length = L.length := theorem pmap_eq_nil {p : α → Prop} {f : ∀ a, p a → β} {l H} : pmap f l H = [] ↔ l = [] := by rw [← length_eq_zero, length_pmap, length_eq_zero] -theorem pmap_ne_nil {P : α → Prop} (f : (a : α) → P a → β) (xs : List α) +theorem pmap_ne_nil {P : α → Prop} (f : (a : α) → P a → β) {xs : List α} (H : ∀ (a : α), a ∈ xs → P a) : xs.pmap f H ≠ [] ↔ xs ≠ [] := by simp @[simp] -theorem attach_eq_nil (l : List α) : l.attach = [] ↔ l = [] := +theorem attach_eq_nil {l : List α} : l.attach = [] ↔ l = [] := pmap_eq_nil theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) (n : Nat) : diff --git a/src/Init/Data/List/Count.lean b/src/Init/Data/List/Count.lean index c938468c47..b2abc6a9fe 100644 --- a/src/Init/Data/List/Count.lean +++ b/src/Init/Data/List/Count.lean @@ -68,13 +68,13 @@ theorem countP_le_length : countP p l ≤ l.length := by @[simp] theorem countP_append (l₁ l₂) : countP p (l₁ ++ l₂) = countP p l₁ + countP p l₂ := by simp only [countP_eq_length_filter, filter_append, length_append] -theorem countP_pos : 0 < countP p l ↔ ∃ a ∈ l, p a := by +theorem countP_pos {p} : 0 < countP p l ↔ ∃ a ∈ l, p a := by simp only [countP_eq_length_filter, length_pos_iff_exists_mem, mem_filter, exists_prop] -theorem countP_eq_zero : countP p l = 0 ↔ ∀ a ∈ l, ¬p a := by +theorem countP_eq_zero {p} : countP p l = 0 ↔ ∀ a ∈ l, ¬p a := by simp only [countP_eq_length_filter, length_eq_zero, filter_eq_nil] -theorem countP_eq_length : countP p l = l.length ↔ ∀ a ∈ l, p a := by +theorem countP_eq_length {p} : countP p l = l.length ↔ ∀ a ∈ l, p a := by rw [countP_eq_length_filter, filter_length_eq_length] theorem Sublist.countP_le (s : l₁ <+ l₂) : countP p l₁ ≤ countP p l₂ := by @@ -230,14 +230,14 @@ theorem count_erase (a b : α) : | c :: l => by rw [erase_cons] if hc : c = b then - have hc_beq := (beq_iff_eq _ _).mpr hc + have hc_beq := beq_iff_eq.mpr hc rw [if_pos hc_beq, hc, count_cons, Nat.add_sub_cancel] else have hc_beq := beq_false_of_ne hc simp only [hc_beq, if_false, count_cons, count_cons, count_erase a b l, reduceCtorEq] if ha : b = a then rw [ha, eq_comm] at hc - rw [if_pos ((beq_iff_eq _ _).2 ha), if_neg (by simpa using Ne.symm hc), Nat.add_zero, Nat.add_zero] + rw [if_pos (beq_iff_eq.2 ha), if_neg (by simpa using Ne.symm hc), Nat.add_zero, Nat.add_zero] else rw [if_neg (by simpa using ha), Nat.sub_zero, Nat.sub_zero] diff --git a/src/Init/Data/List/Erase.lean b/src/Init/Data/List/Erase.lean index 1f14bbba4f..aa834c9fab 100644 --- a/src/Init/Data/List/Erase.lean +++ b/src/Init/Data/List/Erase.lean @@ -33,7 +33,7 @@ theorem eraseP_of_forall_not {l : List α} (h : ∀ a, a ∈ l → ¬p a) : l.er | nil => rfl | cons _ _ ih => simp [h _ (.head ..), ih (forall_mem_cons.1 h).2] -@[simp] theorem eraseP_eq_nil (xs : List α) (p : α → Bool) : xs.eraseP p = [] ↔ xs = [] ∨ ∃ x, p x ∧ xs = [x] := by +@[simp] theorem eraseP_eq_nil {xs : List α} {p : α → Bool} : xs.eraseP p = [] ↔ xs = [] ∨ ∃ x, p x ∧ xs = [x] := by induction xs with | nil => simp | cons x xs ih => @@ -49,7 +49,7 @@ theorem eraseP_of_forall_not {l : List α} (h : ∀ a, a ∈ l → ¬p a) : l.er rintro x h' rfl simp_all -theorem eraseP_ne_nil (xs : List α) (p : α → Bool) : xs.eraseP p ≠ [] ↔ xs ≠ [] ∧ ∀ x, p x → xs ≠ [x] := by +theorem eraseP_ne_nil {xs : List α} {p : α → Bool} : xs.eraseP p ≠ [] ↔ xs ≠ [] ∧ ∀ x, p x → xs ≠ [x] := by simp theorem exists_of_eraseP : ∀ {l : List α} {a} (al : a ∈ l) (pa : p a), @@ -294,12 +294,12 @@ theorem erase_eq_eraseP [LawfulBEq α] (a : α) : ∀ l : List α, l.erase a = | b :: l => by if h : a = b then simp [h] else simp [h, Ne.symm h, erase_eq_eraseP a l] -@[simp] theorem erase_eq_nil [LawfulBEq α] (xs : List α) (a : α) : +@[simp] theorem erase_eq_nil [LawfulBEq α] {xs : List α} {a : α} : xs.erase a = [] ↔ xs = [] ∨ xs = [a] := by rw [erase_eq_eraseP] simp -theorem erase_ne_nil [LawfulBEq α] (xs : List α) (a : α) : +theorem erase_ne_nil [LawfulBEq α] {xs : List α} {a : α} : xs.erase a ≠ [] ↔ xs ≠ [] ∧ xs ≠ [a] := by rw [erase_eq_eraseP] simp diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean index 41f0dcbb58..1d50c0a009 100644 --- a/src/Init/Data/List/Find.lean +++ b/src/Init/Data/List/Find.lean @@ -38,7 +38,7 @@ theorem exists_of_findSome?_eq_some {l : List α} {f : α → Option β} (w : l. @[simp] theorem findSome?_eq_none : findSome? p l = none ↔ ∀ x ∈ l, p x = none := by induction l <;> simp [findSome?_cons]; split <;> simp [*] -@[simp] theorem findSome?_isSome_iff (f : α → Option β) (l : List α) : +@[simp] theorem findSome?_isSome_iff {f : α → Option β} {l : List α} : (l.findSome? f).isSome ↔ ∃ x, x ∈ l ∧ (f x).isSome := by induction l with | nil => simp @@ -201,7 +201,7 @@ theorem find?_cons_eq_some : (a :: xs).find? p = some b ↔ (p a ∧ a = b) ∨ rw [find?_cons] split <;> simp_all -@[simp] theorem find?_isSome (xs : List α) (p : α → Bool) : (xs.find? p).isSome ↔ ∃ x, x ∈ xs ∧ p x := by +@[simp] theorem find?_isSome {xs : List α} {p : α → Bool} : (xs.find? p).isSome ↔ ∃ x, x ∈ xs ∧ p x := by induction xs with | nil => simp | cons x xs ih => @@ -288,7 +288,7 @@ theorem mem_of_find?_eq_some : ∀ {l}, find? p l = some a → a ∈ l simp only [join_cons, find?_append, findSome?_cons, ih] split <;> simp [*] -theorem find?_join_eq_none (xs : List (List α)) (p : α → Bool) : +theorem find?_join_eq_none {xs : List (List α)} {p : α → Bool} : xs.join.find? p = none ↔ ∀ ys ∈ xs, ∀ x ∈ ys, !p x := by simp @@ -297,7 +297,7 @@ If `find? p` returns `some a` from `xs.join`, then `p a` holds, and some list in `xs` contains `a`, and no earlier element of that list satisfies `p`. Moreover, no earlier list in `xs` has an element satisfying `p`. -/ -theorem find?_join_eq_some (xs : List (List α)) (p : α → Bool) (a : α) : +theorem find?_join_eq_some {xs : List (List α)} {p : α → Bool} {a : α} : xs.join.find? p = some a ↔ p a ∧ ∃ as ys zs bs, xs = as ++ (ys ++ a :: zs) :: bs ∧ (∀ a ∈ as, ∀ x ∈ a, !p x) ∧ (∀ x ∈ ys, !p x) := by @@ -336,7 +336,7 @@ theorem find?_join_eq_some (xs : List (List α)) (p : α → Bool) (a : α) : (xs.bind f).find? p = xs.findSome? (fun x => (f x).find? p) := by simp [bind_def, findSome?_map]; rfl -theorem find?_bind_eq_none (xs : List α) (f : α → List β) (p : β → Bool) : +theorem find?_bind_eq_none {xs : List α} {f : α → List β} {p : β → Bool} : (xs.bind f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by simp @@ -355,11 +355,11 @@ theorem find?_replicate : find? p (replicate n a) = if n = 0 then none else if p simp [find?_replicate, h] -- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`. -theorem find?_replicate_eq_none (n : Nat) (a : α) (p : α → Bool) : +theorem find?_replicate_eq_none {n : Nat} {a : α} {p : α → Bool} : (replicate n a).find? p = none ↔ n = 0 ∨ !p a := by simp [Classical.or_iff_not_imp_left] -@[simp] theorem find?_replicate_eq_some (n : Nat) (a b : α) (p : α → Bool) : +@[simp] theorem find?_replicate_eq_some {n : Nat} {a b : α} {p : α → Bool} : (replicate n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by cases n <;> simp @@ -634,7 +634,7 @@ theorem findIdx?_eq_none_iff_findIdx_eq {xs : List α} {p : α → Bool} : xs.findIdx? p = none ↔ xs.findIdx p = xs.length := by simp -theorem findIdx?_eq_some_iff_getElem (xs : List α) (p : α → Bool) : +theorem findIdx?_eq_some_iff_getElem {xs : List α} {p : α → Bool} {i : Nat} : xs.findIdx? p = some i ↔ ∃ h : i < xs.length, p xs[i] ∧ ∀ j (hji : j < i), ¬p (xs[j]'(Nat.lt_trans hji h)) := by induction xs generalizing i with diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 9452041e1d..c6ad389911 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -80,7 +80,7 @@ open Nat /-! ### nil -/ -@[simp] theorem nil_eq {α} (xs : List α) : [] = xs ↔ xs = [] := by +@[simp] theorem nil_eq {α} {xs : List α} : [] = xs ↔ xs = [] := by cases xs <;> simp /-! ### cons -/ @@ -501,7 +501,7 @@ theorem mem_iff_getElem? {a} {l : List α} : a ∈ l ↔ ∃ n : Nat, l[n]? = so theorem mem_iff_get? {a} {l : List α} : a ∈ l ↔ ∃ n, l.get? n = some a := by simp [getElem?_eq_some, Fin.exists_iff, mem_iff_get] -theorem forall_getElem (l : List α) (p : α → Prop) : +theorem forall_getElem {l : List α} {p : α → Prop} : (∀ (n : Nat) h, p (l[n]'h)) ↔ ∀ a, a ∈ l → p a := by induction l with | nil => simp @@ -530,7 +530,7 @@ theorem forall_getElem (l : List α) (p : α → Prop) : theorem isEmpty_iff {l : List α} : l.isEmpty ↔ l = [] := by cases l <;> simp -theorem isEmpty_false_iff_exists_mem (xs : List α) : +theorem isEmpty_false_iff_exists_mem {xs : List α} : (List.isEmpty xs = false) ↔ ∃ x, x ∈ xs := by cases xs <;> simp @@ -650,7 +650,7 @@ theorem set_eq_of_length_le {l : List α} {n : Nat} (h : l.length ≤ n) {a : α rw [ih] exact Nat.succ_le_succ_iff.mp h -@[simp] theorem set_eq_nil (l : List α) (n : Nat) (a : α) : l.set n a = [] ↔ l = [] := by +@[simp] theorem set_eq_nil {l : List α} (n : Nat) (a : α) : l.set n a = [] ↔ l = [] := by cases l <;> cases n <;> simp [set] theorem set_comm (a b : α) : ∀ {n m : Nat} (l : List α), n ≠ m → @@ -1665,7 +1665,7 @@ theorem set_append {s t : List α} : @[simp] theorem foldr_append (f : α → β → β) (b) (l l' : List α) : (l ++ l').foldr f b = l.foldr f (l'.foldr f b) := by simp [foldr_eq_foldrM] -theorem filterMap_eq_append (f : α → Option β) : +theorem filterMap_eq_append {f : α → Option β} : filterMap f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂ := by constructor · induction l generalizing L₁ with @@ -1691,26 +1691,26 @@ theorem filterMap_eq_append (f : α → Option β) : · rintro ⟨l₁, l₂, rfl, rfl, rfl⟩ simp -theorem append_eq_filterMap (f : α → Option β) : +theorem append_eq_filterMap {f : α → Option β} : L₁ ++ L₂ = filterMap f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂ := by rw [eq_comm, filterMap_eq_append] -theorem filter_eq_append (p : α → Bool) : +theorem filter_eq_append {p : α → Bool} : filter p l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filter p l₁ = L₁ ∧ filter p l₂ = L₂ := by rw [← filterMap_eq_filter, filterMap_eq_append] -theorem append_eq_filter (p : α → Bool) : +theorem append_eq_filter {p : α → Bool} : L₁ ++ L₂ = filter p l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filter p l₁ = L₁ ∧ filter p l₂ = L₂ := by rw [eq_comm, filter_eq_append] @[simp] theorem map_append (f : α → β) : ∀ l₁ l₂, map f (l₁ ++ l₂) = map f l₁ ++ map f l₂ := by intro l₁; induction l₁ <;> intros <;> simp_all -theorem map_eq_append (f : α → β) : +theorem map_eq_append {f : α → β} : map f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂ := by rw [← filterMap_eq_map, filterMap_eq_append] -theorem append_eq_map (f : α → β) : +theorem append_eq_map {f : α → β} : L₁ ++ L₂ = map f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂ := by rw [eq_comm, map_eq_append] @@ -1779,7 +1779,7 @@ theorem join_singleton (l : List α) : [l].join = l := by simp @[deprecated join_eq_nil (since := "2024-08-22")] theorem join_eq_nil_iff {L : List (List α)} : L.join = [] ↔ ∀ l ∈ L, l = [] := join_eq_nil -theorem join_ne_nil (xs : List (List α)) : xs.join ≠ [] ↔ ∃ x, x ∈ xs ∧ x ≠ [] := by +theorem join_ne_nil {xs : List (List α)} : xs.join ≠ [] ↔ ∃ x, x ∈ xs ∧ x ≠ [] := by simp theorem exists_of_mem_join : a ∈ join L → ∃ l, l ∈ L ∧ a ∈ l := mem_join.1 @@ -1850,7 +1850,7 @@ theorem join_concat (L : List (List α)) (l : List α) : join (L ++ [l]) = join theorem join_join {L : List (List (List α))} : join (join L) = join (map join L) := by induction L <;> simp_all -theorem join_eq_cons (xs : List (List α)) (y : α) (ys : List α) : +theorem join_eq_cons {xs : List (List α)} {y : α} {ys : List α} : xs.join = y :: ys ↔ ∃ as bs cs, xs = as ++ (y :: bs) :: cs ∧ (∀ l, l ∈ as → l = []) ∧ ys = bs ++ cs.join := by constructor @@ -1871,7 +1871,7 @@ theorem join_eq_cons (xs : List (List α)) (y : α) (ys : List α) : · rintro ⟨as, bs, cs, rfl, h₁, rfl⟩ simp [join_eq_nil.mpr h₁] -theorem join_eq_append (xs : List (List α)) (ys zs : List α) : +theorem join_eq_append {xs : List (List α)} {ys zs : List α} : xs.join = ys ++ zs ↔ (∃ as bs, xs = as ++ bs ∧ ys = as.join ∧ zs = bs.join) ∨ ∃ as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.join ++ bs ∧ @@ -1888,7 +1888,7 @@ theorem join_eq_append (xs : List (List α)) (ys zs : List α) : simp only [join_cons] at h rw [append_eq_append_iff] at h obtain (⟨ys, rfl, h⟩ | ⟨c', rfl, h⟩) := h - · obtain (⟨as, bs, rfl, rfl, rfl⟩ | ⟨as, bs, c, cs, ds, rfl, rfl, rfl⟩) := ih _ h + · obtain (⟨as, bs, rfl, rfl, rfl⟩ | ⟨as, bs, c, cs, ds, rfl, rfl, rfl⟩) := ih h · exact .inl ⟨x :: as, bs, by simp⟩ · exact .inr ⟨x :: as, bs, c, cs, ds, by simp⟩ · simp only [h] @@ -1901,7 +1901,7 @@ theorem join_eq_append (xs : List (List α)) (ys zs : List α) : /-- Two lists of sublists are equal iff their joins coincide, as well as the lengths of the sublists. -/ -theorem eq_iff_join_eq : ∀ (L L' : List (List α)), +theorem eq_iff_join_eq : ∀ {L L' : List (List α)}, L = L' ↔ L.join = L'.join ∧ map length L = map length L' | _, [] => by simp_all | [], x' :: L' => by simp_all @@ -2023,7 +2023,7 @@ theorem forall_mem_replicate {p : α → Prop} {a : α} {n} : @[simp] theorem replicate_succ_ne_nil (n : Nat) (a : α) : replicate (n+1) a ≠ [] := by simp [replicate_succ] -@[simp] theorem replicate_eq_nil (n : Nat) (a : α) : replicate n a = [] ↔ n = 0 := by +@[simp] theorem replicate_eq_nil {n : Nat} (a : α) : replicate n a = [] ↔ n = 0 := by cases n <;> simp @[simp] theorem getElem_replicate (a : α) {n : Nat} {m} (h : m < (replicate n a).length) : @@ -2440,7 +2440,7 @@ theorem elem_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).elem a = true theorem contains_eq_any_beq [BEq α] (l : List α) (a : α) : l.contains a = l.any (a == ·) := by induction l with simp | cons b l => cases b == a <;> simp [*] -theorem contains_iff_exists_mem_beq [BEq α] (l : List α) (a : α) : +theorem contains_iff_exists_mem_beq [BEq α] {l : List α} {a : α} : l.contains a ↔ ∃ a' ∈ l, a == a' := by induction l <;> simp_all diff --git a/src/Init/Data/List/MinMax.lean b/src/Init/Data/List/MinMax.lean index 9400cb2d7d..b7432cb709 100644 --- a/src/Init/Data/List/MinMax.lean +++ b/src/Init/Data/List/MinMax.lean @@ -51,7 +51,7 @@ theorem minimum?_mem [Min α] (min_eq_or : ∀ a b : α, min a b = a ∨ min a b theorem le_minimum?_iff [Min α] [LE α] (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) : - {xs : List α} → xs.minimum? = some a → ∀ x, x ≤ a ↔ ∀ b, b ∈ xs → x ≤ b + {xs : List α} → xs.minimum? = some a → ∀ {x}, x ≤ a ↔ ∀ b, b ∈ xs → x ≤ b | nil => by simp | cons x xs => by rw [minimum?] @@ -72,13 +72,13 @@ theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ · (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b) (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) {xs : List α} : xs.minimum? = some a ↔ a ∈ xs ∧ ∀ b, b ∈ xs → a ≤ b := by - refine ⟨fun h => ⟨minimum?_mem min_eq_or h, (le_minimum?_iff le_min_iff h _).1 (le_refl _)⟩, ?_⟩ + refine ⟨fun h => ⟨minimum?_mem min_eq_or h, (le_minimum?_iff le_min_iff h).1 (le_refl _)⟩, ?_⟩ intro ⟨h₁, h₂⟩ cases xs with | nil => simp at h₁ | cons x xs => exact congrArg some <| anti.1 - ((le_minimum?_iff le_min_iff (xs := x::xs) rfl _).1 (le_refl _) _ h₁) + ((le_minimum?_iff le_min_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁) (h₂ _ (minimum?_mem min_eq_or (xs := x::xs) rfl)) theorem minimum?_replicate [Min α] {n : Nat} {a : α} (w : min a a = a) : @@ -116,7 +116,7 @@ theorem maximum?_mem [Max α] (min_eq_or : ∀ a b : α, max a b = a ∨ max a b theorem maximum?_le_iff [Max α] [LE α] (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) : - {xs : List α} → xs.maximum? = some a → ∀ x, a ≤ x ↔ ∀ b ∈ xs, b ≤ x + {xs : List α} → xs.maximum? = some a → ∀ {x}, a ≤ x ↔ ∀ b ∈ xs, b ≤ x | nil => by simp | cons x xs => by rw [maximum?]; rintro ⟨⟩ y @@ -131,14 +131,14 @@ theorem maximum?_eq_some_iff [Max α] [LE α] [anti : Antisymm ((· : α) ≤ · (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} : xs.maximum? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, b ≤ a := by - refine ⟨fun h => ⟨maximum?_mem max_eq_or h, (maximum?_le_iff max_le_iff h _).1 (le_refl _)⟩, ?_⟩ + refine ⟨fun h => ⟨maximum?_mem max_eq_or h, (maximum?_le_iff max_le_iff h).1 (le_refl _)⟩, ?_⟩ intro ⟨h₁, h₂⟩ cases xs with | nil => simp at h₁ | cons x xs => exact congrArg some <| anti.1 (h₂ _ (maximum?_mem max_eq_or (xs := x::xs) rfl)) - ((maximum?_le_iff max_le_iff (xs := x::xs) rfl _).1 (le_refl _) _ h₁) + ((maximum?_le_iff max_le_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁) theorem maximum?_replicate [Max α] {n : Nat} {a : α} (w : max a a = a) : (replicate n a).maximum? = if n = 0 then none else some a := by diff --git a/src/Init/Data/List/Nat/Basic.lean b/src/Init/Data/List/Nat/Basic.lean index 849f2a8cdc..292664c15a 100644 --- a/src/Init/Data/List/Nat/Basic.lean +++ b/src/Init/Data/List/Nat/Basic.lean @@ -20,10 +20,10 @@ namespace List /-! ### filter -/ -theorem length_filter_lt_length_iff_exists (l) : +theorem length_filter_lt_length_iff_exists {l} : length (filter p l) < length l ↔ ∃ x ∈ l, ¬p x := by simpa [length_eq_countP_add_countP p l, countP_eq_length_filter] using - countP_pos (fun x => ¬p x) (l := l) + countP_pos (p := fun x => ¬p x) /-! ### reverse -/ diff --git a/src/Init/Data/List/Nat/Range.lean b/src/Init/Data/List/Nat/Range.lean index 4139cb81e4..64493be651 100644 --- a/src/Init/Data/List/Nat/Range.lean +++ b/src/Init/Data/List/Nat/Range.lean @@ -106,7 +106,7 @@ theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = simp_all omega -@[simp] theorem find?_range'_eq_some (s n : Nat) (i : Nat) (p : Nat → Bool) : +@[simp] theorem find?_range'_eq_some {s n : Nat} {i : Nat} {p : Nat → Bool} : (range' s n).find? p = some i ↔ p i ∧ i ∈ range' s n ∧ ∀ j, s ≤ j → j < i → !p j := by rw [find?_eq_some] simp only [Bool.not_eq_true', exists_and_right, mem_range'_1, and_congr_right_iff] @@ -124,7 +124,7 @@ theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = intro a a₁ a₂ exact h₃ a a₁ (by omega) -theorem find?_range'_eq_none (s n : Nat) (p : Nat → Bool) : +theorem find?_range'_eq_none {s n : Nat} {p : Nat → Bool} : (range' s n).find? p = none ↔ ∀ i, s ≤ i → i < s + n → !p i := by simp @@ -181,11 +181,11 @@ theorem take_range (m n : Nat) : take m (range n) = range (min m n) := by theorem nodup_range (n : Nat) : Nodup (range n) := by simp (config := {decide := true}) only [range_eq_range', nodup_range'] -@[simp] theorem find?_range_eq_some (n : Nat) (i : Nat) (p : Nat → Bool) : +@[simp] theorem find?_range_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} : (range n).find? p = some i ↔ p i ∧ i ∈ range n ∧ ∀ j, j < i → !p j := by simp [range_eq_range'] -theorem find?_range_eq_none (n : Nat) (p : Nat → Bool) : +theorem find?_range_eq_none {n : Nat} {p : Nat → Bool} : (range n).find? p = none ↔ ∀ i, i < n → !p i := by simp @@ -200,10 +200,10 @@ theorem iota_eq_reverse_range' : ∀ n : Nat, iota n = reverse (range' 1 n) @[simp] theorem length_iota (n : Nat) : length (iota n) = n := by simp [iota_eq_reverse_range'] -@[simp] theorem iota_eq_nil (n : Nat) : iota n = [] ↔ n = 0 := by +@[simp] theorem iota_eq_nil {n : Nat} : iota n = [] ↔ n = 0 := by cases n <;> simp -theorem iota_ne_nil (n : Nat) : iota n ≠ [] ↔ n ≠ 0 := by +theorem iota_ne_nil {n : Nat} : iota n ≠ [] ↔ n ≠ 0 := by cases n <;> simp @[simp] @@ -272,11 +272,11 @@ theorem nodup_iota (n : Nat) : Nodup (iota n) := rw [getLast_eq_head_reverse] simp -theorem find?_iota_eq_none (n : Nat) (p : Nat → Bool) : +theorem find?_iota_eq_none {n : Nat} (p : Nat → Bool) : (iota n).find? p = none ↔ ∀ i, 0 < i → i ≤ n → !p i := by simp -@[simp] theorem find?_iota_eq_some (n : Nat) (i : Nat) (p : Nat → Bool) : +@[simp] theorem find?_iota_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} : (iota n).find? p = some i ↔ p i ∧ i ∈ iota n ∧ ∀ j, i < j → j ≤ n → !p j := by rw [find?_eq_some] simp only [iota_eq_reverse_range', reverse_eq_append, reverse_cons, append_assoc, diff --git a/src/Init/Data/List/Nat/Sublist.lean b/src/Init/Data/List/Nat/Sublist.lean index 5e2af608f8..6381d5b4be 100644 --- a/src/Init/Data/List/Nat/Sublist.lean +++ b/src/Init/Data/List/Nat/Sublist.lean @@ -126,7 +126,7 @@ theorem prefix_take_le_iff {L : List α} (hm : m < L.length) : simp only [length_cons, Nat.succ_eq_add_one, Nat.add_lt_add_iff_right] at hm simp [← @IH n ls hm, Nat.min_eq_left, Nat.le_of_lt hm] -@[simp] theorem append_left_sublist_self (xs ys : List α) : xs ++ ys <+ ys ↔ xs = [] := by +@[simp] theorem append_left_sublist_self {xs : List α} (ys : List α) : xs ++ ys <+ ys ↔ xs = [] := by constructor · intro h replace h := h.length_le @@ -135,7 +135,7 @@ theorem prefix_take_le_iff {L : List α} (hm : m < L.length) : simp_all · rintro rfl simp -@[simp] theorem append_right_sublist_self (xs ys : List α) : xs ++ ys <+ xs ↔ ys = [] := by +@[simp] theorem append_right_sublist_self (xs : List α) {ys : List α} : xs ++ ys <+ xs ↔ ys = [] := by constructor · intro h replace h := h.length_le @@ -145,7 +145,7 @@ theorem prefix_take_le_iff {L : List α} (hm : m < L.length) : · rintro rfl simp -theorem append_sublist_of_sublist_left (xs ys zs : List α) (h : zs <+ xs) : +theorem append_sublist_of_sublist_left {xs ys zs : List α} (h : zs <+ xs) : xs ++ ys <+ zs ↔ ys = [] ∧ xs = zs := by constructor · intro h' @@ -158,7 +158,7 @@ theorem append_sublist_of_sublist_left (xs ys zs : List α) (h : zs <+ xs) : · rintro ⟨rfl, rfl⟩ simp -theorem append_sublist_of_sublist_right (xs ys zs : List α) (h : zs <+ ys) : +theorem append_sublist_of_sublist_right {xs ys zs : List α} (h : zs <+ ys) : xs ++ ys <+ zs ↔ xs = [] ∧ ys = zs := by constructor · intro h' diff --git a/src/Init/Data/List/Pairwise.lean b/src/Init/Data/List/Pairwise.lean index fc07688069..a755c0a8a7 100644 --- a/src/Init/Data/List/Pairwise.lean +++ b/src/Init/Data/List/Pairwise.lean @@ -113,7 +113,7 @@ theorem Pairwise.map {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, (p : Pairwise R l) : Pairwise S (map f l) := pairwise_map.2 <| p.imp (H _ _) -theorem pairwise_filterMap (f : β → Option α) {l : List β} : +theorem pairwise_filterMap {f : β → Option α} {l : List β} : Pairwise R (filterMap f l) ↔ Pairwise (fun a a' : β => ∀ b ∈ f a, ∀ b' ∈ f a', R b b') l := by let _S (a a' : β) := ∀ b ∈ f a, ∀ b' ∈ f a', R b b' simp only [Option.mem_def] @@ -132,11 +132,11 @@ theorem pairwise_filterMap (f : β → Option α) {l : List β} : theorem Pairwise.filterMap {S : β → β → Prop} (f : α → Option β) (H : ∀ a a' : α, R a a' → ∀ b ∈ f a, ∀ b' ∈ f a', S b b') {l : List α} (p : Pairwise R l) : Pairwise S (filterMap f l) := - (pairwise_filterMap _).2 <| p.imp (H _ _) + pairwise_filterMap.2 <| p.imp (H _ _) @[deprecated Pairwise.filterMap (since := "2024-07-29")] abbrev Pairwise.filter_map := @Pairwise.filterMap -theorem pairwise_filter (p : α → Prop) [DecidablePred p] {l : List α} : +theorem pairwise_filter {p : α → Prop} [DecidablePred p] {l : List α} : Pairwise R (filter p l) ↔ Pairwise (fun x y => p x → p y → R x y) l := by rw [← filterMap_eq_filter, pairwise_filterMap] simp diff --git a/src/Init/Data/List/Range.lean b/src/Init/Data/List/Range.lean index b4f014910b..e31dbecab2 100644 --- a/src/Init/Data/List/Range.lean +++ b/src/Init/Data/List/Range.lean @@ -32,7 +32,7 @@ theorem range'_succ (s n step) : range' s (n + 1) step = s :: range' (s + step) @[simp] theorem range'_eq_nil : range' s n step = [] ↔ n = 0 := by rw [← length_eq_zero, length_range'] -theorem range'_ne_nil (s n : Nat) : range' s n ≠ [] ↔ n ≠ 0 := by +theorem range'_ne_nil (s : Nat) {n : Nat} : range' s n ≠ [] ↔ n ≠ 0 := by cases n <;> simp @[simp] theorem range'_zero : range' s 0 = [] := by @@ -150,7 +150,7 @@ theorem range'_eq_map_range (s n : Nat) : range' s n = map (s + ·) (range n) := @[simp] theorem range_eq_nil {n : Nat} : range n = [] ↔ n = 0 := by rw [← length_eq_zero, length_range] -theorem range_ne_nil (n : Nat) : range n ≠ [] ↔ n ≠ 0 := by +theorem range_ne_nil {n : Nat} : range n ≠ [] ↔ n ≠ 0 := by cases n <;> simp @[simp] diff --git a/src/Init/Data/List/Sublist.lean b/src/Init/Data/List/Sublist.lean index c2207f540d..7a9466d34f 100644 --- a/src/Init/Data/List/Sublist.lean +++ b/src/Init/Data/List/Sublist.lean @@ -504,7 +504,7 @@ theorem sublist_join_iff {L : List (List α)} {l} : · rintro ⟨L', rfl, h⟩ simp only [join_nil, sublist_nil, join_eq_nil] simp only [getElem?_nil, Option.getD_none, sublist_nil] at h - exact (forall_getElem L' (· = [])).1 h + exact (forall_getElem (p := (· = []))).1 h | cons l' L ih => simp only [join_cons, sublist_append_iff, ih] constructor @@ -831,7 +831,7 @@ theorem isPrefix_iff : l₁ <+: l₂ ↔ ∀ i (h : i < l₁.length), l₂[i]? = -- See `Init.Data.List.Nat.Sublist` for `isSuffix_iff` and `ifInfix_iff`. -theorem isPrefix_filterMap_iff {β} (f : α → Option β) {l₁ : List α} {l₂ : List β} : +theorem isPrefix_filterMap_iff {β} {f : α → Option β} {l₁ : List α} {l₂ : List β} : l₂ <+: filterMap f l₁ ↔ ∃ l, l <+: l₁ ∧ l₂ = filterMap f l := by simp only [IsPrefix, append_eq_filterMap] constructor @@ -840,7 +840,7 @@ theorem isPrefix_filterMap_iff {β} (f : α → Option β) {l₁ : List α} {l · rintro ⟨l₁, ⟨l₂, rfl⟩, rfl⟩ exact ⟨_, l₁, l₂, rfl, rfl, rfl⟩ -theorem isSuffix_filterMap_iff {β} (f : α → Option β) {l₁ : List α} {l₂ : List β} : +theorem isSuffix_filterMap_iff {β} {f : α → Option β} {l₁ : List α} {l₂ : List β} : l₂ <:+ filterMap f l₁ ↔ ∃ l, l <:+ l₁ ∧ l₂ = filterMap f l := by simp only [IsSuffix, append_eq_filterMap] constructor @@ -849,7 +849,7 @@ theorem isSuffix_filterMap_iff {β} (f : α → Option β) {l₁ : List α} {l · rintro ⟨l₁, ⟨l₂, rfl⟩, rfl⟩ exact ⟨_, l₂, l₁, rfl, rfl, rfl⟩ -theorem isInfix_filterMap_iff {β} (f : α → Option β) {l₁ : List α} {l₂ : List β} : +theorem isInfix_filterMap_iff {β} {f : α → Option β} {l₁ : List α} {l₂ : List β} : l₂ <:+: filterMap f l₁ ↔ ∃ l, l <:+: l₁ ∧ l₂ = filterMap f l := by simp only [IsInfix, append_eq_filterMap, filterMap_eq_append] constructor @@ -870,15 +870,15 @@ theorem isInfix_filter_iff {p : α → Bool} {l₁ l₂ : List α} : l₂ <:+: l₁.filter p ↔ ∃ l, l <:+: l₁ ∧ l₂ = l.filter p := by rw [← filterMap_eq_filter, isInfix_filterMap_iff] -theorem isPrefix_map_iff {β} (f : α → β) {l₁ : List α} {l₂ : List β} : +theorem isPrefix_map_iff {β} {f : α → β} {l₁ : List α} {l₂ : List β} : l₂ <+: l₁.map f ↔ ∃ l, l <+: l₁ ∧ l₂ = l.map f := by rw [← filterMap_eq_map, isPrefix_filterMap_iff] -theorem isSuffix_map_iff {β} (f : α → β) {l₁ : List α} {l₂ : List β} : +theorem isSuffix_map_iff {β} {f : α → β} {l₁ : List α} {l₂ : List β} : l₂ <:+ l₁.map f ↔ ∃ l, l <:+ l₁ ∧ l₂ = l.map f := by rw [← filterMap_eq_map, isSuffix_filterMap_iff] -theorem isInfix_map_iff {β} (f : α → β) {l₁ : List α} {l₂ : List β} : +theorem isInfix_map_iff {β} {f : α → β} {l₁ : List α} {l₂ : List β} : l₂ <:+: l₁.map f ↔ ∃ l, l <:+: l₁ ∧ l₂ = l.map f := by rw [← filterMap_eq_map, isInfix_filterMap_iff] diff --git a/src/Init/Data/List/Zip.lean b/src/Init/Data/List/Zip.lean index 694421a928..82de8c49e5 100644 --- a/src/Init/Data/List/Zip.lean +++ b/src/Init/Data/List/Zip.lean @@ -136,14 +136,14 @@ theorem getElem?_zipWith' {f : α → β → γ} {i : Nat} : · simp · cases i <;> simp_all -theorem getElem?_zipWith_eq_some (f : α → β → γ) (l₁ : List α) (l₂ : List β) (z : γ) (i : Nat) : +theorem getElem?_zipWith_eq_some {f : α → β → γ} {l₁ : List α} {l₂ : List β} {z : γ} {i : Nat} : (zipWith f l₁ l₂)[i]? = some z ↔ ∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z := by induction l₁ generalizing l₂ i · simp · cases l₂ <;> cases i <;> simp_all -theorem getElem?_zip_eq_some (l₁ : List α) (l₂ : List β) (z : α × β) (i : Nat) : +theorem getElem?_zip_eq_some {l₁ : List α} {l₂ : List β} {z : α × β} {i : Nat} : (zip l₁ l₂)[i]? = some z ↔ l₁[i]? = some z.1 ∧ l₂[i]? = some z.2 := by cases z rw [zip, getElem?_zipWith_eq_some]; constructor diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index 5645095be5..706b2a245e 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -831,8 +831,8 @@ protected theorem pred_succ (n : Nat) : pred n.succ = n := rfl @[simp] protected theorem zero_sub_one : 0 - 1 = 0 := rfl @[simp] protected theorem add_one_sub_one (n : Nat) : n + 1 - 1 = n := rfl -theorem sub_one_eq_self (n : Nat) : n - 1 = n ↔ n = 0 := by cases n <;> simp [ne_add_one] -theorem eq_self_sub_one (n : Nat) : n = n - 1 ↔ n = 0 := by cases n <;> simp [add_one_ne] +theorem sub_one_eq_self {n : Nat} : n - 1 = n ↔ n = 0 := by cases n <;> simp [ne_add_one] +theorem eq_self_sub_one {n : Nat} : n = n - 1 ↔ n = 0 := by cases n <;> simp [add_one_ne] theorem succ_pred {a : Nat} (h : a ≠ 0) : a.pred.succ = a := by induction a with diff --git a/src/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean index ec78992596..9f62649ee9 100644 --- a/src/Init/Data/Nat/Div.lean +++ b/src/Init/Data/Nat/Div.lean @@ -143,7 +143,7 @@ theorem mod_lt (x : Nat) {y : Nat} : y > 0 → x % y < y := by induction x, y using mod.inductionOn with | base x y h₁ => intro h₂ - have h₁ : ¬ 0 < y ∨ ¬ y ≤ x := Iff.mp (Decidable.not_and_iff_or_not _ _) h₁ + have h₁ : ¬ 0 < y ∨ ¬ y ≤ x := Decidable.not_and_iff_or_not.mp h₁ match h₁ with | Or.inl h₁ => exact absurd h₂ h₁ | Or.inr h₁ => diff --git a/src/Init/Data/Nat/Dvd.lean b/src/Init/Data/Nat/Dvd.lean index 6732819ccc..0955d77bf6 100644 --- a/src/Init/Data/Nat/Dvd.lean +++ b/src/Init/Data/Nat/Dvd.lean @@ -74,11 +74,11 @@ theorem dvd_of_mod_eq_zero {m n : Nat} (H : n % m = 0) : m ∣ n := by have := (mod_add_div n m).symm rwa [H, Nat.zero_add] at this -theorem dvd_iff_mod_eq_zero (m n : Nat) : m ∣ n ↔ n % m = 0 := +theorem dvd_iff_mod_eq_zero {m n : Nat} : m ∣ n ↔ n % m = 0 := ⟨mod_eq_zero_of_dvd, dvd_of_mod_eq_zero⟩ instance decidable_dvd : @DecidableRel Nat (·∣·) := - fun _ _ => decidable_of_decidable_of_iff (dvd_iff_mod_eq_zero _ _).symm + fun _ _ => decidable_of_decidable_of_iff dvd_iff_mod_eq_zero.symm theorem emod_pos_of_not_dvd {a b : Nat} (h : ¬ a ∣ b) : 0 < b % a := by rw [dvd_iff_mod_eq_zero] at h diff --git a/src/Init/Data/Nat/Gcd.lean b/src/Init/Data/Nat/Gcd.lean index 540c0f8267..4433b9fb19 100644 --- a/src/Init/Data/Nat/Gcd.lean +++ b/src/Init/Data/Nat/Gcd.lean @@ -227,7 +227,7 @@ theorem gcd_eq_zero_iff {i j : Nat} : gcd i j = 0 ↔ i = 0 ∧ j = 0 := fun h => by simp [h]⟩ /-- Characterization of the value of `Nat.gcd`. -/ -theorem gcd_eq_iff (a b : Nat) : +theorem gcd_eq_iff {a b : Nat} : gcd a b = g ↔ g ∣ a ∧ g ∣ b ∧ (∀ c, c ∣ a → c ∣ b → c ∣ g) := by constructor · rintro rfl diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean index 2bd96124b9..268e89a111 100644 --- a/src/Init/Data/Nat/Lemmas.lean +++ b/src/Init/Data/Nat/Lemmas.lean @@ -453,10 +453,10 @@ protected theorem mul_right_cancel {n m k : Nat} (mp : 0 < m) (h : n * m = k * m simp [Nat.mul_comm _ m] at h apply Nat.mul_left_cancel mp h -protected theorem mul_left_cancel_iff {n: Nat} (p : 0 < n) (m k : Nat) : n * m = n * k ↔ m = k := +protected theorem mul_left_cancel_iff {n : Nat} (p : 0 < n) {m k : Nat} : n * m = n * k ↔ m = k := ⟨Nat.mul_left_cancel p, fun | rfl => rfl⟩ -protected theorem mul_right_cancel_iff {m : Nat} (p : 0 < m) (n k : Nat) : n * m = k * m ↔ n = k := +protected theorem mul_right_cancel_iff {m : Nat} (p : 0 < m) {n k : Nat} : n * m = k * m ↔ n = k := ⟨Nat.mul_right_cancel p, fun | rfl => rfl⟩ protected theorem ne_zero_of_mul_ne_zero_right (h : n * m ≠ 0) : m ≠ 0 := @@ -494,7 +494,7 @@ theorem succ_mul_succ (a b) : succ a * succ b = a * b + a + b + 1 := by theorem add_one_mul_add_one (a b : Nat) : (a + 1) * (b + 1) = a * b + a + b + 1 := by rw [add_one_mul, mul_add_one]; rfl -theorem mul_le_add_right (m k n : Nat) : k * m ≤ m + n ↔ (k-1) * m ≤ n := by +theorem mul_le_add_right {m k n : Nat} : k * m ≤ m + n ↔ (k-1) * m ≤ n := by match k with | 0 => simp diff --git a/src/Init/Data/Nat/Mod.lean b/src/Init/Data/Nat/Mod.lean index 40f015b9ad..81f122859f 100644 --- a/src/Init/Data/Nat/Mod.lean +++ b/src/Init/Data/Nat/Mod.lean @@ -73,10 +73,10 @@ theorem mod_pow_succ {x b k : Nat} : x % b ^ (k + 1) = x % b ^ k + b ^ k * ((x / b ^ k) % b) := by rw [Nat.pow_succ, Nat.mod_mul] -@[simp] theorem two_pow_mod_two_eq_zero (n : Nat) : 2 ^ n % 2 = 0 ↔ 0 < n := by +@[simp] theorem two_pow_mod_two_eq_zero {n : Nat} : 2 ^ n % 2 = 0 ↔ 0 < n := by cases n <;> simp [Nat.pow_succ] -@[simp] theorem two_pow_mod_two_eq_one (n : Nat) : 2 ^ n % 2 = 1 ↔ n = 0 := by +@[simp] theorem two_pow_mod_two_eq_one {n : Nat} : 2 ^ n % 2 = 1 ↔ n = 0 := by cases n <;> simp [Nat.pow_succ] end Nat diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index 8cd21f234c..9cee09cc72 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -1124,7 +1124,7 @@ theorem ext_iff {s₁ s₂ : String} : s₁ = s₂ ↔ s₁.data = s₂.data := attribute [simp] toList -- prefer `String.data` over `String.toList` in lemmas -theorem lt_iff (s t : String) : s < t ↔ s.data < t.data := .rfl +theorem lt_iff {s t : String} : s < t ↔ s.data < t.data := .rfl namespace Pos diff --git a/src/Init/Omega/Int.lean b/src/Init/Omega/Int.lean index 681cb8a960..07e37f7ff7 100644 --- a/src/Init/Omega/Int.lean +++ b/src/Init/Omega/Int.lean @@ -136,26 +136,26 @@ theorem neg_le_natAbs {a : Int} : -a ≤ a.natAbs := by simp at t exact t -theorem add_le_iff_le_sub (a b c : Int) : a + b ≤ c ↔ a ≤ c - b := by +theorem add_le_iff_le_sub {a b c : Int} : a + b ≤ c ↔ a ≤ c - b := by conv => lhs rw [← Int.add_zero c, ← Int.sub_self (-b), Int.sub_eq_add_neg, ← Int.add_assoc, Int.neg_neg, Int.add_le_add_iff_right] - try rfl -- stage0 update TODO: Change this to rfl or remove + rfl -theorem le_add_iff_sub_le (a b c : Int) : a ≤ b + c ↔ a - c ≤ b := by +theorem le_add_iff_sub_le {a b c : Int} : a ≤ b + c ↔ a - c ≤ b := by conv => lhs rw [← Int.neg_neg c, ← Int.sub_eq_add_neg, ← add_le_iff_le_sub] - try rfl -- stage0 update TODO: Change this to rfl or remove + rfl -theorem add_le_zero_iff_le_neg (a b : Int) : a + b ≤ 0 ↔ a ≤ - b := by +theorem add_le_zero_iff_le_neg {a b : Int} : a + b ≤ 0 ↔ a ≤ - b := by rw [add_le_iff_le_sub, Int.zero_sub] -theorem add_le_zero_iff_le_neg' (a b : Int) : a + b ≤ 0 ↔ b ≤ -a := by +theorem add_le_zero_iff_le_neg' {a b : Int} : a + b ≤ 0 ↔ b ≤ -a := by rw [Int.add_comm, add_le_zero_iff_le_neg] -theorem add_nonnneg_iff_neg_le (a b : Int) : 0 ≤ a + b ↔ -b ≤ a := by +theorem add_nonnneg_iff_neg_le {a b : Int} : 0 ≤ a + b ↔ -b ≤ a := by rw [le_add_iff_sub_le, Int.zero_sub] -theorem add_nonnneg_iff_neg_le' (a b : Int) : 0 ≤ a + b ↔ -a ≤ b := by +theorem add_nonnneg_iff_neg_le' {a b : Int} : 0 ≤ a + b ↔ -a ≤ b := by rw [Int.add_comm, add_nonnneg_iff_neg_le] theorem ofNat_fst_mk {β} {x : Nat} {y : β} : (Prod.mk x y).fst = (x : Int) := rfl @@ -206,7 +206,7 @@ end Fin namespace Prod theorem of_lex (w : Prod.Lex r s p q) : r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd := - (Prod.lex_def r s).mp w + Prod.lex_def.mp w theorem of_not_lex {α} {r : α → α → Prop} [DecidableEq α] {β} {s : β → β → Prop} {p q : α × β} (w : ¬ Prod.Lex r s p q) : diff --git a/src/Init/Omega/IntList.lean b/src/Init/Omega/IntList.lean index bdd1634e68..c321787fea 100644 --- a/src/Init/Omega/IntList.lean +++ b/src/Init/Omega/IntList.lean @@ -318,7 +318,7 @@ theorem dvd_gcd (xs : IntList) (c : Nat) (w : ∀ {a : Int}, a ∈ xs → (c : I apply w exact List.mem_cons_of_mem x m -theorem gcd_eq_iff (xs : IntList) (g : Nat) : +theorem gcd_eq_iff {xs : IntList} {g : Nat} : xs.gcd = g ↔ (∀ {a : Int}, a ∈ xs → (g : Int) ∣ a) ∧ (∀ (c : Nat), (∀ {a : Int}, a ∈ xs → (c : Int) ∣ a) → c ∣ g) := by @@ -334,7 +334,7 @@ theorem gcd_eq_iff (xs : IntList) (g : Nat) : attribute [simp] Int.zero_dvd -@[simp] theorem gcd_eq_zero (xs : IntList) : xs.gcd = 0 ↔ ∀ x, x ∈ xs → x = 0 := by +@[simp] theorem gcd_eq_zero {xs : IntList} : xs.gcd = 0 ↔ ∀ x, x ∈ xs → x = 0 := by simp [gcd_eq_iff, Nat.dvd_zero] @[simp] theorem dot_mod_gcd_left (xs ys : IntList) : dot xs ys % xs.gcd = 0 := by diff --git a/src/Init/Omega/Logic.lean b/src/Init/Omega/Logic.lean index 7fc051918a..bdff552546 100644 --- a/src/Init/Omega/Logic.lean +++ b/src/Init/Omega/Logic.lean @@ -20,7 +20,7 @@ theorem and_not_not_of_not_or (h : ¬ (p ∨ q)) : ¬ p ∧ ¬ q := not_or.mp h theorem Decidable.or_not_not_of_not_and [Decidable p] [Decidable q] (h : ¬ (p ∧ q)) : ¬ p ∨ ¬ q := - (Decidable.not_and_iff_or_not _ _).mp h + Decidable.not_and_iff_or_not.mp h theorem Decidable.and_or_not_and_not_of_iff {p q : Prop} [Decidable q] (h : p ↔ q) : (p ∧ q) ∨ (¬p ∧ ¬q) := Decidable.iff_iff_and_or_not_and_not.mp h diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean index 23a522795f..d363a35df0 100644 --- a/src/Init/PropLemmas.lean +++ b/src/Init/PropLemmas.lean @@ -169,22 +169,22 @@ theorem if_true_right [h : Decidable p] : @[simp] theorem ite_not (p : Prop) [Decidable p] (x y : α) : ite (¬p) x y = ite p y x := dite_not (fun _ => x) (fun _ => y) -@[simp] theorem ite_then_self (p q : Prop) [h : Decidable p] : (if p then p else q) = (¬p → q) := by +@[simp] theorem ite_then_self {p q : Prop} [h : Decidable p] : (if p then p else q) ↔ (¬p → q) := by cases h <;> (rename_i g; simp [g]) -@[simp] theorem ite_else_self (p q : Prop) [h : Decidable p] : (if p then q else p) = (p ∧ q) := by +@[simp] theorem ite_else_self {p q : Prop} [h : Decidable p] : (if p then q else p) ↔ (p ∧ q) := by cases h <;> (rename_i g; simp [g]) -@[simp] theorem ite_then_not_self (p : Prop) [Decidable p] (q : Prop) : (if p then ¬p else q) ↔ ¬p ∧ q := by +@[simp] theorem ite_then_not_self {p : Prop} [Decidable p] {q : Prop} : (if p then ¬p else q) ↔ ¬p ∧ q := by split <;> simp_all -@[simp] theorem ite_else_not_self (p : Prop) [Decidable p] (q : Prop) : (if p then q else ¬p) ↔ p → q := by +@[simp] theorem ite_else_not_self {p : Prop} [Decidable p] {q : Prop} : (if p then q else ¬p) ↔ p → q := by split <;> simp_all @[deprecated ite_then_self (since := "2024-08-28")] -theorem ite_true_same (p q : Prop) [Decidable p] : (if p then p else q) = (¬p → q) := ite_then_self p q +theorem ite_true_same {p q : Prop} [Decidable p] : (if p then p else q) ↔ (¬p → q) := ite_then_self @[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 p q +theorem ite_false_same {p q : Prop} [Decidable p] : (if p then q else p) ↔ (p ∧ q) := ite_else_self /-! ## exists and forall -/ @@ -222,7 +222,7 @@ theorem exists_prop_congr {p p' : Prop} {q q' : p → Prop} (hq : ∀ h, q h ↔ theorem exists_prop_of_true {p : Prop} {q : p → Prop} (h : p) : (Exists fun h' : p => q h') ↔ q h := @exists_const (q h) p ⟨h⟩ -@[simp] theorem exists_true_left (p : True → Prop) : Exists p ↔ p True.intro := +@[simp] theorem exists_true_left {p : True → Prop} : Exists p ↔ p True.intro := exists_prop_of_true _ section forall_congr @@ -337,7 +337,7 @@ theorem not_forall_of_exists_not {p : α → Prop} : (∃ x, ¬p x) → ¬∀ x, @[simp] theorem exists_or_eq_left' (y : α) (p : α → Prop) : ∃ x : α, y = x ∨ p x := ⟨y, .inl rfl⟩ @[simp] theorem exists_or_eq_right' (y : α) (p : α → Prop) : ∃ x : α, p x ∨ y = x := ⟨y, .inr rfl⟩ -@[simp] theorem exists_prop' (p : Prop) : (∃ _ : α, p) ↔ Nonempty α ∧ p := +@[simp] theorem exists_prop' {p : Prop} : (∃ _ : α, p) ↔ Nonempty α ∧ p := ⟨fun ⟨a, h⟩ => ⟨⟨a⟩, h⟩, fun ⟨⟨a⟩, h⟩ => ⟨a, h⟩⟩ theorem exists_prop : (∃ _h : a, b) ↔ a ∧ b := @@ -371,7 +371,7 @@ end quantifiers /-! ## Nonempty -/ -@[simp] theorem nonempty_prop (p : Prop) : Nonempty p ↔ p := +@[simp] theorem nonempty_prop {p : Prop} : Nonempty p ↔ p := ⟨fun ⟨h⟩ => h, fun h => ⟨h⟩⟩ /-! ## decidable -/ @@ -407,11 +407,11 @@ if h : p then decidable_of_decidable_of_iff ⟨fun h2 _ => h2, fun al => al h⟩ else isTrue fun h2 => absurd h2 h -theorem decide_eq_true_iff (p : Prop) [Decidable p] : (decide p = true) ↔ p := by simp +theorem decide_eq_true_iff {p : Prop} [Decidable p] : (decide p = true) ↔ p := by simp @[simp, boolToPropSimps] theorem decide_eq_decide {p q : Prop} {_ : Decidable p} {_ : Decidable q} : decide p = decide q ↔ (p ↔ q) := - ⟨fun h => by rw [← decide_eq_true_iff p, h, decide_eq_true_iff], fun h => by simp [h]⟩ + ⟨fun h => by rw [← decide_eq_true_iff (p := p), h, decide_eq_true_iff], fun h => by simp [h]⟩ theorem Decidable.of_not_imp [Decidable a] (h : ¬(a → b)) : a := byContradiction (not_not_of_not_imp h) @@ -483,7 +483,7 @@ theorem Decidable.iff_iff_and_or_not_and_not {a b : Prop} [Decidable b] : theorem Decidable.iff_iff_not_or_and_or_not [Decidable a] [Decidable b] : (a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b) := by - rw [iff_iff_implies_and_implies a b]; simp only [imp_iff_not_or, Or.comm] + rw [iff_iff_implies_and_implies (a := a) (b := b)]; simp only [imp_iff_not_or, Or.comm] theorem Decidable.not_and_not_right [Decidable b] : ¬(a ∧ ¬b) ↔ (a → b) := ⟨fun h ha => not_imp_symm (And.intro ha) h, fun h ⟨ha, hb⟩ => hb <| h ha⟩ @@ -628,38 +628,38 @@ theorem ite_false_decide_same (p : Prop) [Decidable p] (b : Bool) : attribute [local simp] Decidable.imp_iff_left_iff -@[simp] theorem dite_eq_left_iff (p : Prop) [Decidable p] {x : α} {y : ¬ p → α} : (if h : p then x else y h) = x ↔ ∀ h : ¬ p, y h = x := by +@[simp] theorem dite_eq_left_iff {p : Prop} [Decidable p] {x : α} {y : ¬ p → α} : (if h : p then x else y h) = x ↔ ∀ h : ¬ p, y h = x := by split <;> simp_all -@[simp] theorem dite_eq_right_iff (p : Prop) [Decidable p] {x : p → α} {y : α} : (if h : p then x h else y) = y ↔ ∀ h : p, x h = y := by +@[simp] theorem dite_eq_right_iff {p : Prop} [Decidable p] {x : p → α} {y : α} : (if h : p then x h else y) = y ↔ ∀ h : p, x h = y := by split <;> simp_all -@[simp] theorem dite_iff_left_iff (p : Prop) [Decidable p] {x : Prop} {y : ¬ p → Prop} : ((if h : p then x else y h) ↔ x) ↔ ∀ h : ¬ p, y h ↔ x := by +@[simp] theorem dite_iff_left_iff {p : Prop} [Decidable p] {x : Prop} {y : ¬ p → Prop} : ((if h : p then x else y h) ↔ x) ↔ ∀ h : ¬ p, y h ↔ x := by split <;> simp_all -@[simp] theorem dite_iff_right_iff (p : Prop) [Decidable p] {x : p → Prop} {y : Prop} : ((if h : p then x h else y) ↔ y) ↔ ∀ h : p, x h ↔ y := by +@[simp] theorem dite_iff_right_iff {p : Prop} [Decidable p] {x : p → Prop} {y : Prop} : ((if h : p then x h else y) ↔ y) ↔ ∀ h : p, x h ↔ y := by split <;> simp_all -@[simp] theorem ite_eq_left_iff (p : Prop) [Decidable p] (x y : α) : (if p then x else y) = x ↔ ¬ p → y = x := by +@[simp] theorem ite_eq_left_iff {p : Prop} [Decidable p] (x y : α) : (if p then x else y) = x ↔ ¬ p → y = x := by split <;> simp_all -@[simp] theorem ite_eq_right_iff (p : Prop) [Decidable p] (x y : α) : (if p then x else y) = y ↔ p → x = y := by +@[simp] theorem ite_eq_right_iff {p : Prop} [Decidable p] {x y : α} : (if p then x else y) = y ↔ p → x = y := by split <;> simp_all -@[simp] theorem ite_iff_left_iff (p : Prop) [Decidable p] (x y : Prop) : ((if p then x else y) ↔ x) ↔ ¬ p → y = x := by +@[simp] theorem ite_iff_left_iff {p : Prop} [Decidable p] {x y : Prop} : ((if p then x else y) ↔ x) ↔ ¬ p → y = x := by split <;> simp_all -@[simp] theorem ite_iff_right_iff (p : Prop) [Decidable p] (x y : Prop) : ((if p then x else y) ↔ y) ↔ p → x = y := by +@[simp] theorem ite_iff_right_iff {p : Prop} [Decidable p] {x y : Prop} : ((if p then x else y) ↔ y) ↔ p → x = y := by split <;> simp_all -@[simp] theorem dite_then_false (p : Prop) [Decidable p] {x : ¬ p → Prop} : (if h : p then False else x h) ↔ ∃ h : ¬ p, x h := by +@[simp] theorem dite_then_false {p : Prop} [Decidable p] {x : ¬ p → Prop} : (if h : p then False else x h) ↔ ∃ h : ¬ p, x h := by split <;> simp_all -@[simp] theorem dite_else_false (p : Prop) [Decidable p] {x : p → Prop} : (if h : p then x h else False) ↔ ∃ h : p, x h := by +@[simp] theorem dite_else_false {p : Prop} [Decidable p] {x : p → Prop} : (if h : p then x h else False) ↔ ∃ h : p, x h := by split <;> simp_all -@[simp] theorem dite_then_true (p : Prop) [Decidable p] {x : ¬ p → Prop} : (if h : p then True else x h) ↔ ∀ h : ¬ p, x h := by +@[simp] theorem dite_then_true {p : Prop} [Decidable p] {x : ¬ p → Prop} : (if h : p then True else x h) ↔ ∀ h : ¬ p, x h := by split <;> simp_all -@[simp] theorem dite_else_true (p : Prop) [Decidable p] {x : p → Prop} : (if h : p then x h else True) ↔ ∀ h : p, x h := by +@[simp] theorem dite_else_true {p : Prop} [Decidable p] {x : p → Prop} : (if h : p then x h else True) ↔ ∀ h : p, x h := by split <;> simp_all diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean index 38acaa073e..9acffe533e 100644 --- a/src/Init/SimpLemmas.lean +++ b/src/Init/SimpLemmas.lean @@ -188,9 +188,9 @@ theorem or_iff_left_of_imp (hb : b → a) : (a ∨ b) ↔ a := Iff.intro (Or.r @[simp] theorem or_iff_left_iff_imp : (a ∨ b ↔ a) ↔ (b → a) := Iff.intro (·.mp ∘ Or.inr) or_iff_left_of_imp @[simp] theorem or_iff_right_iff_imp : (a ∨ b ↔ b) ↔ (a → b) := by rw [or_comm, or_iff_left_iff_imp] -@[simp] theorem iff_self_or (a b : Prop) : (a ↔ a ∨ b) ↔ (b → a) := +@[simp] theorem iff_self_or {a b : Prop} : (a ↔ a ∨ b) ↔ (b → a) := propext (@Iff.comm _ a) ▸ @or_iff_left_iff_imp a b -@[simp] theorem iff_or_self (a b : Prop) : (b ↔ a ∨ b) ↔ (a → b) := +@[simp] theorem iff_or_self {a b : Prop} : (b ↔ a ∨ b) ↔ (a → b) := propext (@Iff.comm _ b) ▸ @or_iff_right_iff_imp a b /-# Bool -/ @@ -260,8 +260,8 @@ theorem bne_self_eq_false' [DecidableEq α] (a : α) : (a != a) = false := by si @[simp] theorem decide_False : decide False = false := rfl @[simp] theorem decide_True : decide True = true := rfl -@[simp] theorem bne_iff_ne [BEq α] [LawfulBEq α] (a b : α) : a != b ↔ a ≠ b := by - simp [bne]; rw [← beq_iff_eq a b]; simp [-beq_iff_eq] +@[simp] theorem bne_iff_ne [BEq α] [LawfulBEq α] {a b : α} : a != b ↔ a ≠ b := by + simp [bne]; rw [← beq_iff_eq (a := a) (b := b)]; simp [-beq_iff_eq] /- Added for critical pair for `¬((a != b) = true)` @@ -271,14 +271,12 @@ Added for critical pair for `¬((a != b) = true)` These will both normalize to `a = b` with the first via `bne_eq_false_iff_eq`. -/ -@[simp] theorem beq_eq_false_iff_ne [BEq α] [LawfulBEq α] - (a b : α) : (a == b) = false ↔ a ≠ b := by - rw [ne_eq, ← beq_iff_eq a b] +@[simp] theorem beq_eq_false_iff_ne [BEq α] [LawfulBEq α] {a b : α} : (a == b) = false ↔ a ≠ b := by + rw [ne_eq, ← beq_iff_eq (a := a) (b := b)] cases a == b <;> decide -@[simp] theorem bne_eq_false_iff_eq [BEq α] [LawfulBEq α] (a b : α) : - (a != b) = false ↔ a = b := by - rw [bne, ← beq_iff_eq a b] +@[simp] theorem bne_eq_false_iff_eq [BEq α] [LawfulBEq α] {a b : α} : (a != b) = false ↔ a = b := by + rw [bne, ← beq_iff_eq (a := a) (b := b)] cases a == b <;> decide theorem Bool.beq_to_eq (a b : Bool) : (a == b) = (a = b) := by simp diff --git a/src/Init/WF.lean b/src/Init/WF.lean index a9c817084f..cb581e7272 100644 --- a/src/Init/WF.lean +++ b/src/Init/WF.lean @@ -245,7 +245,7 @@ protected inductive Lex : α × β → α × β → Prop where | left {a₁} (b₁) {a₂} (b₂) (h : ra a₁ a₂) : Prod.Lex (a₁, b₁) (a₂, b₂) | right (a) {b₁ b₂} (h : rb b₁ b₂) : Prod.Lex (a, b₁) (a, b₂) -theorem lex_def (r : α → α → Prop) (s : β → β → Prop) {p q : α × β} : +theorem lex_def {r : α → α → Prop} {s : β → β → Prop} {p q : α × β} : Prod.Lex r s p q ↔ r p.1 q.1 ∨ p.1 = q.1 ∧ s p.2 q.2 := ⟨fun h => by cases h <;> simp [*], fun h => match p, q, h with diff --git a/src/lake/Lake/Util/Name.lean b/src/lake/Lake/Util/Name.lean index e9d3133293..fd391aa0cd 100644 --- a/src/lake/Lake/Util/Name.lean +++ b/src/lake/Lake/Util/Name.lean @@ -53,7 +53,7 @@ namespace Name open Lean.Name @[simp] protected theorem beq_false (m n : Name) : (m == n) = false ↔ ¬ (m = n) := by - rw [← beq_iff_eq m n]; cases m == n <;> simp (config := { decide := true }) + rw [← beq_iff_eq (a := m) (b := n)]; cases m == n <;> simp (config := { decide := true }) @[simp] theorem isPrefixOf_self {n : Name} : n.isPrefixOf n := by cases n <;> simp [isPrefixOf]