From 3a9b57c42ffba439bff1c6de6c350fb12b858f82 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Sun, 29 Oct 2023 15:52:05 +0000 Subject: [PATCH] chore: update Mathlib for leanprover/std4#183 (#7982) Co-authored-by: Scott Morrison Co-authored-by: Eric Wieser --- Mathlib/Analysis/BoxIntegral/Basic.lean | 4 +- Mathlib/Data/Bool/Basic.lean | 107 +++++------------------- Mathlib/Init/Data/Bool/Basic.lean | 14 +--- Mathlib/Init/Data/Bool/Lemmas.lean | 12 ++- Mathlib/Init/Data/Nat/Bitwise.lean | 5 +- Mathlib/Order/BoundedOrder.lean | 4 +- lake-manifest.json | 16 ++-- 7 files changed, 43 insertions(+), 119 deletions(-) diff --git a/Mathlib/Analysis/BoxIntegral/Basic.lean b/Mathlib/Analysis/BoxIntegral/Basic.lean index 036a07ecfaa51..2fc0e3a4a2cbf 100644 --- a/Mathlib/Analysis/BoxIntegral/Basic.lean +++ b/Mathlib/Analysis/BoxIntegral/Basic.lean @@ -819,8 +819,8 @@ theorem HasIntegral.of_le_Henstock_of_forall_isLittleO (hl : l ≤ Henstock) (B ∃ δ > 0, ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x δ → x ∈ Box.Icc J → (l.bDistortion → J.distortion ≤ c) → dist (vol J (f x)) (g J) ≤ ε * B J) : HasIntegral I l f vol (g I) := - have A : l.bHenstock := hl.2.1.resolve_left (by decide) - HasIntegral.of_bRiemann_eq_false_of_forall_isLittleO (hl.1.resolve_right (by decide)) B hB0 _ s hs + have A : l.bHenstock := Bool.eq_true_of_true_le hl.2.1 + HasIntegral.of_bRiemann_eq_false_of_forall_isLittleO (Bool.eq_false_of_le_false hl.1) B hB0 _ s hs (fun _ => A) H₁ <| by simpa only [A, true_imp_iff] using H₂ set_option linter.uppercaseLean3 false in #align box_integral.has_integral_of_le_Henstock_of_forall_is_o BoxIntegral.HasIntegral.of_le_Henstock_of_forall_isLittleO diff --git a/Mathlib/Data/Bool/Basic.lean b/Mathlib/Data/Bool/Basic.lean index 3855031a3272a..36acaf4200450 100644 --- a/Mathlib/Data/Bool/Basic.lean +++ b/Mathlib/Data/Bool/Basic.lean @@ -145,12 +145,8 @@ theorem eq_true_of_ne_false : ∀ {a : Bool}, a ≠ false → a = true := by dec theorem eq_false_of_ne_true : ∀ {a : Bool}, a ≠ true → a = false := by decide #align bool.eq_ff_of_ne_tt Bool.eq_false_of_ne_true -theorem or_comm : ∀ a b, (a || b) = (b || a) := by decide #align bool.bor_comm Bool.or_comm - #align bool.bor_assoc Bool.or_assoc - -theorem or_left_comm : ∀ a b c, (a || (b || c)) = (b || (a || c)) := by decide #align bool.bor_left_comm Bool.or_left_comm theorem or_inl {a b : Bool} (H : a) : a || b := by simp [H] @@ -159,12 +155,8 @@ theorem or_inl {a b : Bool} (H : a) : a || b := by simp [H] theorem or_inr {a b : Bool} (H : b) : a || b := by cases a <;> simp [H] #align bool.bor_inr Bool.or_inr -theorem and_comm : ∀ a b, (a && b) = (b && a) := by decide #align bool.band_comm Bool.and_comm - #align bool.band_assoc Bool.and_assoc - -theorem and_left_comm : ∀ a b c, (a && (b && c)) = (b && (a && c)) := by decide #align bool.band_left_comm Bool.and_left_comm theorem and_elim_left : ∀ {a b : Bool}, a && b → a := by decide @@ -176,22 +168,10 @@ theorem and_intro : ∀ {a b : Bool}, a → b → a && b := by decide theorem and_elim_right : ∀ {a b : Bool}, a && b → b := by decide #align bool.band_elim_right Bool.and_elim_right -theorem and_or_distrib_left (a b c : Bool) : (a && (b || c)) = (a && b || a && c) := by - cases a <;> simp #align bool.band_bor_distrib_left Bool.and_or_distrib_left - -theorem and_or_distrib_right (a b c : Bool) : ((a || b) && c) = (a && c || b && c) := by - cases a <;> cases b <;> cases c <;> simp #align bool.band_bor_distrib_right Bool.and_or_distrib_right - -theorem or_and_distrib_left (a b c : Bool) : (a || b && c) = ((a || b) && (a || c)) := by - cases a <;> simp #align bool.bor_band_distrib_left Bool.or_and_distrib_left - -theorem or_and_distrib_right (a b c : Bool) : (a && b || c) = ((a || c) && (b || c)) := by - cases a <;> cases b <;> cases c <;> simp #align bool.bor_band_distrib_right Bool.or_and_distrib_right - #align bool.bnot_ff Bool.not_false #align bool.bnot_tt Bool.not_true @@ -241,60 +221,39 @@ theorem eq_false_of_not_eq_true' {a : Bool} : !a = true → a = false := by cases a <;> decide #align bool.eq_ff_of_bnot_eq_tt Bool.eq_false_of_not_eq_true' -@[simp] -theorem and_not_self : ∀ x, (x && !x) = false := by decide +-- TODO: undo the rename in leanprover/std4#183? +alias and_not_self := and_not_self_right #align bool.band_bnot_self Bool.and_not_self -@[simp] -theorem not_and_self : ∀ x, (!x && x) = false := by decide +-- TODO: undo the rename in leanprover/std4#183? +alias not_and_self := and_not_self_left #align bool.bnot_band_self Bool.not_and_self -@[simp] -theorem or_not_self : ∀ x, (x || !x) = true := by decide +-- TODO: undo the rename in leanprover/std4#183? +alias or_not_self := or_not_self_right #align bool.bor_bnot_self Bool.or_not_self -@[simp] -theorem not_or_self : ∀ x, (!x || x) = true := by decide +-- TODO: undo the rename in leanprover/std4#183? +alias not_or_self := or_not_self_left #align bool.bnot_bor_self Bool.not_or_self theorem bne_eq_xor : bne = xor := by funext a b; revert a b; decide -theorem xor_comm : ∀ a b, xor a b = xor b a := by decide #align bool.bxor_comm Bool.xor_comm -@[simp] -theorem xor_assoc : ∀ a b c, xor (xor a b) c = xor a (xor b c) := by decide +attribute [simp] xor_assoc #align bool.bxor_assoc Bool.xor_assoc -theorem xor_left_comm : ∀ a b c, xor a (xor b c) = xor b (xor a c) := by decide #align bool.bxor_left_comm Bool.xor_left_comm - -@[simp] -theorem xor_not_left : ∀ a, xor (!a) a = true := by decide #align bool.bxor_bnot_left Bool.xor_not_left - -@[simp] -theorem xor_not_right : ∀ a, xor a (!a) = true := by decide #align bool.bxor_bnot_right Bool.xor_not_right -@[simp] -theorem xor_not_not : ∀ a b, xor (!a) (!b) = xor a b := by decide +attribute [simp] xor_not_not #align bool.bxor_bnot_bnot Bool.xor_not_not -@[simp] -theorem xor_false_left : ∀ a, xor false a = a := by decide #align bool.bxor_ff_left Bool.xor_false_left - -@[simp] -theorem xor_false_right : ∀ a, xor a false = a := by decide #align bool.bxor_ff_right Bool.xor_false_right - -theorem and_xor_distrib_left (a b c : Bool) : (a && xor b c) = xor (a && b) (a && c) := by - cases a <;> simp #align bool.band_bxor_distrib_left Bool.and_xor_distrib_left - -theorem and_xor_distrib_right (a b c : Bool) : (xor a b && c) = xor (a && c) (b && c) := by - cases a <;> cases b <;> cases c <;> simp #align bool.band_bxor_distrib_right Bool.and_xor_distrib_right theorem xor_iff_ne : ∀ {x y : Bool}, xor x y = true ↔ x ≠ y := by decide @@ -302,46 +261,26 @@ theorem xor_iff_ne : ∀ {x y : Bool}, xor x y = true ↔ x ≠ y := by decide /-! ### De Morgan's laws for booleans-/ -@[simp] -theorem not_and : ∀ a b : Bool, (!(a && b)) = (!a || !b) := by decide +attribute [simp] not_and #align bool.bnot_band Bool.not_and -@[simp] -theorem not_or : ∀ a b : Bool, (!(a || b)) = (!a && !b) := by decide +attribute [simp] not_or #align bool.bnot_bor Bool.not_or -theorem not_inj : ∀ {a b : Bool}, (!a) = !b → a = b := by decide #align bool.bnot_inj Bool.not_inj --- Porting note: having to unfold here is not pretty. --- There is a discussion on zulip about this at --- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/LinearOrder.20in.20mathlib3.2F4/near/308228493 instance linearOrder : LinearOrder Bool where - le := fun a b ↦ a = false ∨ b = true - le_refl := by unfold LE.le; decide - le_trans := by unfold LE.le; decide - le_antisymm := by unfold LE.le Preorder.toLE; decide - le_total := by unfold LE.le Preorder.toLE PartialOrder.toPreorder; decide - decidableLE := by unfold LE.le Preorder.toLE PartialOrder.toPreorder; exact inferInstance - decidableEq := inferInstance - max := or - max_def := λ a b => by cases a <;> cases b <;> decide - min := and - min_def := λ a b => by cases a <;> cases b <;> decide + le_refl := Bool.le_refl + le_trans _ _ _ := Bool.le_trans + le_antisymm _ _ := Bool.le_antisymm + le_total := Bool.le_total + decidableLE := inferInstance + lt_iff_le_not_le _ _ := Bool.lt_iff_le_not_le #align bool.linear_order Bool.linearOrder -@[simp] theorem max_eq_or : max = or := rfl - -@[simp] theorem min_eq_and : min = and := rfl +attribute [simp] Bool.max_eq_or Bool.min_eq_and -@[simp] -theorem false_le {x : Bool} : false ≤ x := - Or.intro_left _ rfl #align bool.ff_le Bool.false_le - -@[simp] -theorem le_true {x : Bool} : x ≤ true := - Or.intro_right _ rfl #align bool.le_tt Bool.le_true theorem lt_iff : ∀ {x y : Bool}, x < y ↔ x = false ∧ y = true := by decide @@ -386,17 +325,15 @@ def ofNat (n : Nat) : Bool := theorem ofNat_le_ofNat {n m : Nat} (h : n ≤ m) : ofNat n ≤ ofNat m := by simp only [ofNat, ne_eq, _root_.decide_not] cases Nat.decEq n 0 with - | isTrue hn => rw [decide_eq_true hn]; exact false_le + | isTrue hn => rw [decide_eq_true hn]; exact Bool.false_le _ | isFalse hn => cases Nat.decEq m 0 with - | isFalse hm => rw [decide_eq_false hm]; exact le_true + | isFalse hm => rw [decide_eq_false hm]; exact Bool.le_true _ | isTrue hm => subst hm; have h := le_antisymm h (Nat.zero_le n); contradiction #align bool.of_nat_le_of_nat Bool.ofNat_le_ofNat theorem toNat_le_toNat {b₀ b₁ : Bool} (h : b₀ ≤ b₁) : toNat b₀ ≤ toNat b₁ := by - cases h with - | inl h => subst h; exact Nat.zero_le _ - | inr h => subst h; cases b₀ <;> simp + cases b₀ <;> cases b₁ <;> simp_all #align bool.to_nat_le_to_nat Bool.toNat_le_toNat theorem ofNat_toNat (b : Bool) : ofNat (toNat b) = b := by diff --git a/Mathlib/Init/Data/Bool/Basic.lean b/Mathlib/Init/Data/Bool/Basic.lean index b5af62ef4ed96..c974d399d6d7e 100644 --- a/Mathlib/Init/Data/Bool/Basic.lean +++ b/Mathlib/Init/Data/Bool/Basic.lean @@ -4,24 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ import Mathlib.Mathport.Rename +import Std.Data.Bool /-! # Boolean operations -In Lean 3 this file also contained the definitions of `cond`, `bor`, `band` and `bnot`, -the boolean functions. These are in Lean 4 core (as `cond`, `or`, `and` and `not`), but -apparently `xor` didn't make the cut. - +In Lean 3 this file contained the definitions of `cond`, `bor`, `band` and `bnot`, +the boolean functions. These are now in Lean 4 core or Std (as `cond`, `or`, `and`, `not`, `xor`). -/ #align bor or #align band and #align bnot not - -/-- Boolean XOR -/ -@[inline] -def xor : Bool → Bool → Bool - | true, false => true - | false, true => true - | _, _ => false #align bxor xor diff --git a/Mathlib/Init/Data/Bool/Lemmas.lean b/Mathlib/Init/Data/Bool/Lemmas.lean index ce4db27021822..fcda57bdc23e7 100644 --- a/Mathlib/Init/Data/Bool/Lemmas.lean +++ b/Mathlib/Init/Data/Bool/Lemmas.lean @@ -47,19 +47,18 @@ namespace Bool theorem cond_self.{u} {α : Type u} (b : Bool) (a : α) : cond b a a = a := by cases b <;> rfl #align cond_a_a Bool.cond_self -@[simp] -theorem xor_self (b : Bool) : xor b b = false := by cases b <;> simp +attribute [simp] xor_self #align bxor_self Bool.xor_self -@[simp] -theorem xor_true (b : Bool) : xor b true = not b := by cases b <;> simp +-- TODO: undo the rename in leanprover/std4#183? +alias xor_true := xor_true_right #align bxor_tt Bool.xor_true theorem xor_false (b : Bool) : xor b false = b := by cases b <;> simp #align bxor_ff Bool.xor_false -@[simp] -theorem true_xor (b : Bool) : xor true b = not b := by cases b <;> simp +-- TODO: undo the rename in leanprover/std4#183? +alias true_xor := xor_true_left #align tt_bxor Bool.true_xor theorem false_xor (b : Bool) : xor false b = b := by cases b <;> simp @@ -167,7 +166,6 @@ theorem coe_or_iff (a b : Bool) : a || b ↔ a ∨ b := by simp theorem coe_and_iff (a b : Bool) : a && b ↔ a ∧ b := by simp #align band_coe_iff Bool.coe_and_iff -@[simp] 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.coe_xor_iff diff --git a/Mathlib/Init/Data/Nat/Bitwise.lean b/Mathlib/Init/Data/Nat/Bitwise.lean index 4d12513f11fc3..1c034d672565c 100644 --- a/Mathlib/Init/Data/Nat/Bitwise.lean +++ b/Mathlib/Init/Data/Nat/Bitwise.lean @@ -73,10 +73,7 @@ theorem bodd_succ (n : ℕ) : bodd (succ n) = not (bodd n) := by @[simp] theorem bodd_add (m n : ℕ) : bodd (m + n) = bxor (bodd m) (bodd n) := by - induction' n with n IH - · simp - · simp [add_succ, IH] - cases bodd m <;> cases bodd n <;> rfl + induction n <;> simp_all [add_succ] #align nat.bodd_add Nat.bodd_add @[simp] diff --git a/Mathlib/Order/BoundedOrder.lean b/Mathlib/Order/BoundedOrder.lean index 9a806f27bea35..75a44a714c647 100644 --- a/Mathlib/Order/BoundedOrder.lean +++ b/Mathlib/Order/BoundedOrder.lean @@ -942,9 +942,9 @@ open Bool instance Bool.boundedOrder : BoundedOrder Bool where top := true - le_top _ := le_true + le_top := Bool.le_true bot := false - bot_le _ := false_le + bot_le := Bool.false_le @[simp] theorem top_eq_true : ⊤ = true := diff --git a/lake-manifest.json b/lake-manifest.json index 3d10158900918..bd8a29e85b68a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -2,14 +2,6 @@ "packagesDir": "lake-packages", "packages": [{"git": - {"url": "https://github.com/leanprover/std4", - "subDir?": null, - "rev": "bd60d932e2c786c7347e57576598568b2816e316", - "opts": {}, - "name": "std", - "inputRev?": "main", - "inherited": false}}, - {"git": {"url": "https://github.com/leanprover-community/quote4", "subDir?": null, "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2", @@ -40,5 +32,13 @@ "opts": {}, "name": "proofwidgets", "inputRev?": "v0.0.21", + "inherited": false}}, + {"git": + {"url": "https://github.com/leanprover/std4", + "subDir?": null, + "rev": "0da0e81a141cd26364f8799fb31ae7866ec43fb7", + "opts": {}, + "name": "std", + "inputRev?": "main", "inherited": false}}], "name": "mathlib"}