From cf041cccff59df221c92d67ca29378960df2fac0 Mon Sep 17 00:00:00 2001 From: negiizhao Date: Mon, 23 Oct 2023 14:19:51 +0000 Subject: [PATCH] chore: fix the names of some `Bool` lemmas (#7841) --- Mathlib/Combinatorics/SimpleGraph/Basic.lean | 2 +- Mathlib/Computability/RegularExpressions.lean | 4 ++-- Mathlib/Data/Bool/AllAny.lean | 4 ++-- Mathlib/Data/Bool/Basic.lean | 4 ++-- Mathlib/Init/Data/Bool/Lemmas.lean | 12 ++++++------ 5 files changed, 13 insertions(+), 13 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Basic.lean index 89f7dfc4e24ff..5ad90ea3aeb79 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Basic.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Basic.lean @@ -145,7 +145,7 @@ def SimpleGraph.mk' {V : Type u} : simp only [mk.injEq, Subtype.mk.injEq] intro h funext v w - simpa [Bool.coe_bool_iff] using congr_fun₂ h v w + simpa [Bool.coe_iff_coe] using congr_fun₂ h v w /-- We can enumerate simple graphs by enumerating all functions `V → V → Bool` and filtering on whether they are symmetric and irreflexive. -/ diff --git a/Mathlib/Computability/RegularExpressions.lean b/Mathlib/Computability/RegularExpressions.lean index 243b243d255bd..bfbf2132e0760 100644 --- a/Mathlib/Computability/RegularExpressions.lean +++ b/Mathlib/Computability/RegularExpressions.lean @@ -238,7 +238,7 @@ theorem char_rmatch_iff (a : α) (x : List α) : rmatch (char a) x ↔ x = [a] : theorem add_rmatch_iff (P Q : RegularExpression α) (x : List α) : (P + Q).rmatch x ↔ P.rmatch x ∨ Q.rmatch x := by induction' x with _ _ ih generalizing P Q - · simp only [rmatch, matchEpsilon, Bool.or_coe_iff] + · simp only [rmatch, matchEpsilon, Bool.coe_or_iff] · repeat' rw [rmatch] rw [deriv_add] exact ih _ _ @@ -252,7 +252,7 @@ theorem mul_rmatch_iff (P Q : RegularExpression α) (x : List α) : · intro h refine' ⟨[], [], rfl, _⟩ rw [rmatch, rmatch] - rwa [Bool.and_coe_iff] at h + rwa [Bool.coe_and_iff] at h · rintro ⟨t, u, h₁, h₂⟩ cases' List.append_eq_nil.1 h₁.symm with ht hu subst ht diff --git a/Mathlib/Data/Bool/AllAny.lean b/Mathlib/Data/Bool/AllAny.lean index 20dbad8d0daf6..da5bf5194bec1 100644 --- a/Mathlib/Data/Bool/AllAny.lean +++ b/Mathlib/Data/Bool/AllAny.lean @@ -27,7 +27,7 @@ namespace List theorem all_iff_forall {p : α → Bool} : all l p ↔ ∀ a ∈ l, p a := by induction' l with a l ih · exact iff_of_true rfl (forall_mem_nil _) - simp only [all_cons, Bool.and_coe_iff, ih, forall_mem_cons] + simp only [all_cons, Bool.coe_and_iff, ih, forall_mem_cons] #align list.all_iff_forall List.all_iff_forall theorem all_iff_forall_prop : (all l fun a => p a) ↔ ∀ a ∈ l, p a := by @@ -42,7 +42,7 @@ theorem all_iff_forall_prop : (all l fun a => p a) ↔ ∀ a ∈ l, p a := by theorem any_iff_exists {p : α → Bool} : any l p ↔ ∃ a ∈ l, p a := by induction' l with a l ih · exact iff_of_false Bool.not_false' (not_exists_mem_nil _) - simp only [any_cons, Bool.or_coe_iff, ih, exists_mem_cons_iff] + simp only [any_cons, Bool.coe_or_iff, ih, exists_mem_cons_iff] #align list.any_iff_exists List.any_iff_exists theorem any_iff_exists_prop : (any l fun a => p a) ↔ ∃ a ∈ l, p a := by simp [any_iff_exists] diff --git a/Mathlib/Data/Bool/Basic.lean b/Mathlib/Data/Bool/Basic.lean index c78e2e8e4808a..1e42361e9c90c 100644 --- a/Mathlib/Data/Bool/Basic.lean +++ b/Mathlib/Data/Bool/Basic.lean @@ -138,8 +138,8 @@ theorem cond_not {α} (b : Bool) (t e : α) : cond (!b) t e = cond b e t := by c theorem not_ne_id : not ≠ id := fun h ↦ false_ne_true <| congrFun h true #align bool.bnot_ne_id Bool.not_ne_id -theorem coe_bool_iff : ∀ {a b : Bool}, (a ↔ b) ↔ a = b := by decide -#align bool.coe_bool_iff Bool.coe_bool_iff +theorem coe_iff_coe : ∀ {a b : Bool}, (a ↔ b) ↔ a = b := by decide +#align bool.coe_bool_iff Bool.coe_iff_coe theorem eq_true_of_ne_false : ∀ {a : Bool}, a ≠ false → a = true := by decide #align bool.eq_tt_of_ne_ff Bool.eq_true_of_ne_false diff --git a/Mathlib/Init/Data/Bool/Lemmas.lean b/Mathlib/Init/Data/Bool/Lemmas.lean index c74aba3a4dc2b..ce4db27021822 100644 --- a/Mathlib/Init/Data/Bool/Lemmas.lean +++ b/Mathlib/Init/Data/Bool/Lemmas.lean @@ -161,16 +161,16 @@ theorem decide_congr {p q : Prop} [Decidable p] [Decidable q] (h : p ↔ q) : | true => exact decide_true (h.2 <| of_decide_true h') #align to_bool_congr Bool.decide_congr -theorem or_coe_iff (a b : Bool) : a || b ↔ a ∨ b := by simp -#align bor_coe_iff Bool.or_coe_iff +theorem coe_or_iff (a b : Bool) : a || b ↔ a ∨ b := by simp +#align bor_coe_iff Bool.coe_or_iff -theorem and_coe_iff (a b : Bool) : a && b ↔ a ∧ b := by simp -#align band_coe_iff Bool.and_coe_iff +theorem coe_and_iff (a b : Bool) : a && b ↔ a ∧ b := by simp +#align band_coe_iff Bool.coe_and_iff @[simp] -theorem xor_coe_iff (a b : Bool) : xor a b ↔ Xor' (a = true) (b = true) := by +theorem coe_xor_iff (a b : Bool) : xor a b ↔ Xor' (a = true) (b = true) := by cases a <;> cases b <;> exact by decide -#align bxor_coe_iff Bool.xor_coe_iff +#align bxor_coe_iff Bool.coe_xor_iff @[simp] theorem ite_eq_true_distrib (c : Prop) [Decidable c] (a b : Bool) :