max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: variables appearing on both sides of an iff should be implicit (#5254)

Browse source
This commit is contained in:
Kim Morrison 2024-09-04 18:33:24 +10:00 • committed by GitHub
parent f1b2850aa4
commit d08051cf0b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
37 changed files with 235 additions and 239 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Classical.lean
View file

@ -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))

10
src/Init/Core.lean
View file

@ -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

16
src/Init/Data/Array/Lemmas.lean
View file

@ -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

4
src/Init/Data/BEq.lean
View file

@ -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

36
src/Init/Data/BitVec/Lemmas.lean
View file

@ -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]

100
src/Init/Data/Bool.lean
View file

@ -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]

10
src/Init/Data/Fin/Lemmas.lean
View file

@ -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]⟩

6
src/Init/Data/Int/DivModLemmas.lean
View file

@ -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

10
src/Init/Data/Int/Lemmas.lean
View file

@ -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 :=

22
src/Init/Data/Int/Order.lean
View file

@ -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

4
src/Init/Data/List/Attach.lean
View file

@ -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) :

10
src/Init/Data/List/Count.lean
View file

@ -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]

8
src/Init/Data/List/Erase.lean
View file

@ -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

16
src/Init/Data/List/Find.lean
View file

@ -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

34
src/Init/Data/List/Lemmas.lean
View file

@ -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

12
src/Init/Data/List/MinMax.lean
View file

@ -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

4
src/Init/Data/List/Nat/Basic.lean
View file

@ -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 -/

16
src/Init/Data/List/Nat/Range.lean
View file

@ -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,

8
src/Init/Data/List/Nat/Sublist.lean
View file

@ -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'

6
src/Init/Data/List/Pairwise.lean
View file

@ -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

4
src/Init/Data/List/Range.lean
View file

@ -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]

14
src/Init/Data/List/Sublist.lean
View file

@ -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]

4
src/Init/Data/List/Zip.lean
View file

@ -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

4
src/Init/Data/Nat/Basic.lean
View file

@ -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

2
src/Init/Data/Nat/Div.lean
View file

@ -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₁ =>

4
src/Init/Data/Nat/Dvd.lean
View file

@ -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

2
src/Init/Data/Nat/Gcd.lean
View file

@ -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

6
src/Init/Data/Nat/Lemmas.lean
View file

@ -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

4
src/Init/Data/Nat/Mod.lean
View file

@ -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

2
src/Init/Data/String/Basic.lean
View file

@ -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

18
src/Init/Omega/Int.lean
View file

@ -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) :

4
src/Init/Omega/IntList.lean
View file

@ -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

2
src/Init/Omega/Logic.lean
View file

@ -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

48
src/Init/PropLemmas.lean
View file

@ -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

18
src/Init/SimpLemmas.lean
View file

@ -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

2
src/Init/WF.lean
View file

@ -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

2
src/lake/Lake/Util/Name.lean
View file

@ -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]