Merge remote-tracking branch 'upstream/nightly-with-mathlib' into improve-ord-api

Author: Rob23oba

src/CMakeLists.txt

@@ -689,7 +689,7 @@ add_custom_target(make_stdlib ALL
   # The actual rule is in a separate makefile because we want to prefix it with '+' to use the Make job server
   # for a parallelized nested build, but CMake doesn't let us do that.
   # We use `lean` from the previous stage, but `leanc`, headers, etc. from the current stage
-  COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init Std Lean
+  COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init Std Lean Leanc
   VERBATIM)
 
 # if we have LLVM enabled, then build `lean.h.bc` which has the LLVM bitcode
@@ -768,7 +768,7 @@ if(${STAGE} GREATER 0 AND EXISTS ${LEAN_SOURCE_DIR}/Leanc.lean AND NOT ${CMAKE_S
   add_custom_target(leanc ALL
     WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/leanc
     DEPENDS leanshared
-    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Leanc
+    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanc
     VERBATIM)
 endif()
 
@@ -823,7 +823,6 @@ endif()
 
 # Escape for `make`. Yes, twice.
 string(REPLACE "$" "\\\$$" CMAKE_EXE_LINKER_FLAGS_MAKE "${CMAKE_EXE_LINKER_FLAGS}")
-string(REPLACE "$" "$$" CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE "${CMAKE_EXE_LINKER_FLAGS_MAKE}")
 configure_file(${LEAN_SOURCE_DIR}/stdlib.make.in ${CMAKE_BINARY_DIR}/stdlib.make)
 
 # hacky

src/Init/Classical.lean

@@ -107,8 +107,8 @@ noncomputable def epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α
 theorem epsilon_spec_aux {α : Sort u} (h : Nonempty α) (p : α → Prop) : (∃ y, p y) → p (@epsilon α h p) :=
   (strongIndefiniteDescription p h).property
 
-theorem epsilon_spec {α : Sort u} {p : α → Prop} (hex : ∃ y, p y) : p (@epsilon α (nonempty_of_exists hex) p) :=
-  epsilon_spec_aux (nonempty_of_exists hex) p hex
+theorem epsilon_spec {α : Sort u} {p : α → Prop} (hex : ∃ y, p y) : p (@epsilon α hex.nonempty p) :=
+  epsilon_spec_aux hex.nonempty p hex
 
 theorem epsilon_singleton {α : Sort u} (x : α) : @epsilon α ⟨x⟩ (fun y => y = x) = x :=
   @epsilon_spec α (fun y => y = x) ⟨x, rfl⟩

src/Init/Core.lean

@@ -1212,10 +1212,7 @@ abbrev noConfusionEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f :
 instance : Inhabited Prop where
   default := True
 
-deriving instance Inhabited for NonScalar, PNonScalar, True, ForInStep
-
-theorem nonempty_of_exists {α : Sort u} {p : α → Prop} : Exists (fun x => p x) → Nonempty α
-  | ⟨w, _⟩ => ⟨w⟩
+deriving instance Inhabited for NonScalar, PNonScalar, True
 
 /-! # Subsingleton -/
 
@@ -1389,16 +1386,7 @@ instance Sum.nonemptyLeft [h : Nonempty α] : Nonempty (Sum α β) :=
 instance Sum.nonemptyRight [h : Nonempty β] : Nonempty (Sum α β) :=
   Nonempty.elim h (fun b => ⟨Sum.inr b⟩)
 
-instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (Sum α β) := fun a b =>
-  match a, b with
-  | Sum.inl a, Sum.inl b =>
-    if h : a = b then isTrue (h ▸ rfl)
-    else isFalse fun h' => Sum.noConfusion h' fun h' => absurd h' h
-  | Sum.inr a, Sum.inr b =>
-    if h : a = b then isTrue (h ▸ rfl)
-    else isFalse fun h' => Sum.noConfusion h' fun h' => absurd h' h
-  | Sum.inr _, Sum.inl _ => isFalse fun h => Sum.noConfusion h
-  | Sum.inl _, Sum.inr _ => isFalse fun h => Sum.noConfusion h
+deriving instance DecidableEq for Sum
 
 end
 

src/Init/Data/Array/Lex/Lemmas.lean

@@ -23,9 +23,9 @@ namespace Array
 @[simp, grind =] theorem lt_toList [LT α] {xs ys : Array α} : xs.toList < ys.toList ↔ xs < ys := Iff.rfl
 @[simp, grind =] theorem le_toList [LT α] {xs ys : Array α} : xs.toList ≤ ys.toList ↔ xs ≤ ys := Iff.rfl
 
-protected theorem not_lt_iff_ge [LT α] {l₁ l₂ : List α} : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
-protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} :
-    ¬ l₁ ≤ l₂ ↔ l₂ < l₁ :=
+protected theorem not_lt_iff_ge [LT α] {xs ys : Array α} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
+protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {xs ys : Array α} :
+    ¬ xs ≤ ys ↔ ys < xs :=
   Decidable.not_not
 
 @[simp] theorem lex_empty [BEq α] {lt : α → α → Bool} {xs : Array α} : xs.lex #[] lt = false := by

src/Init/Data/Array/OfFn.lean

@@ -26,12 +26,11 @@ theorem ofFn_succ {f : Fin (n+1) → α} :
     ofFn f = (ofFn (fun (i : Fin n) => f i.castSucc)).push (f ⟨n, by omega⟩) := by
   ext i h₁ h₂
   · simp
-  · simp [getElem_push]
-    split <;> rename_i h₃
-    · rfl
-    · congr
-      simp at h₁ h₂
-      omega
+  · simp only [getElem_ofFn, getElem_push, size_ofFn, Fin.castSucc_mk, left_eq_dite_iff,
+      Nat.not_lt]
+    simp only [size_ofFn] at h₁
+    intro h₃
+    simp only [show i = n by omega]
 
 @[simp] theorem _root_.List.toArray_ofFn {f : Fin n → α} : (List.ofFn f).toArray = Array.ofFn f := by
   ext <;> simp

src/Init/Data/BitVec/Lemmas.lean

@@ -2261,7 +2261,7 @@ theorem msb_sshiftRight {n : Nat} {x : BitVec w} :
 theorem sshiftRight_add {x : BitVec w} {m n : Nat} :
     x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n := by
   ext i
-  simp [getElem_sshiftRight, getLsbD_sshiftRight, Nat.add_assoc]
+  simp only [getElem_sshiftRight, Nat.add_assoc, msb_sshiftRight, dite_eq_ite]
   by_cases h₂ : n + i < w
   · simp [h₂]
   · simp only [h₂, ↓reduceIte]

src/Init/Data/Float.lean

@@ -161,8 +161,7 @@ This function does not reduce in the kernel. It is compiled to the C inequality
   match a, b with
   | ⟨a⟩, ⟨b⟩ => floatSpec.decLe a b
 
-instance floatDecLt (a b : Float) : Decidable (a < b) := Float.decLt a b
-instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b
+attribute [instance] Float.decLt Float.decLe
 
 /--
 Converts a floating-point number to a string.

src/Init/Data/Float32.lean

@@ -145,7 +145,7 @@ Compares two floating point numbers for strict inequality.
 
 This function does not reduce in the kernel. It is compiled to the C inequality operator.
 -/
-@[extern "lean_float32_decLt"] opaque Float32.decLt (a b : Float32) : Decidable (a < b) :=
+@[extern "lean_float32_decLt", instance] opaque Float32.decLt (a b : Float32) : Decidable (a < b) :=
   match a, b with
   | ⟨a⟩, ⟨b⟩ => float32Spec.decLt a b
 
@@ -154,13 +154,10 @@ Compares two floating point numbers for non-strict inequality.
 
 This function does not reduce in the kernel. It is compiled to the C inequality operator.
 -/
-@[extern "lean_float32_decLe"] opaque Float32.decLe (a b : Float32) : Decidable (a ≤ b) :=
+@[extern "lean_float32_decLe", instance] opaque Float32.decLe (a b : Float32) : Decidable (a ≤ b) :=
   match a, b with
   | ⟨a⟩, ⟨b⟩ => float32Spec.decLe a b
 
-instance float32DecLt (a b : Float32) : Decidable (a < b) := Float32.decLt a b
-instance float32DecLe (a b : Float32) : Decidable (a ≤ b) := Float32.decLe a b
-
 /--
 Converts a floating-point number to a string.
 

src/Init/Data/Hashable.lean

@@ -57,9 +57,6 @@ instance : Hashable UInt64 where
 instance : Hashable USize where
   hash n := n.toUInt64
 
-instance : Hashable ByteArray where
-  hash as := as.foldl (fun r a => mixHash r (hash a)) 7
-
 instance : Hashable (Fin n) where
   hash v := v.val.toUInt64
 

src/Init/Data/Int/LemmasAux.lean

@@ -121,7 +121,7 @@ theorem toNat_lt_toNat {n m : Int} (hn : 0 < m) : n.toNat < m.toNat ↔ n < m :=
 /-! ### min and max -/
 
 @[simp] protected theorem min_assoc : ∀ (a b c : Int), min (min a b) c = min a (min b c) := by omega
-instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩
+instance : Std.Associative (α := Int) min := ⟨Int.min_assoc⟩
 
 @[simp] protected theorem min_self_assoc {m n : Int} : min m (min m n) = min m n := by
   rw [← Int.min_assoc, Int.min_self]
@@ -130,7 +130,7 @@ instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩
   rw [Int.min_comm m n, ← Int.min_assoc, Int.min_self]
 
 @[simp] protected theorem max_assoc (a b c : Int) : max (max a b) c = max a (max b c) := by omega
-instance : Std.Associative (α := Nat) max := ⟨Nat.max_assoc⟩
+instance : Std.Associative (α := Int) max := ⟨Int.max_assoc⟩
 
 @[simp] protected theorem max_self_assoc {m n : Int} : max m (max m n) = max m n := by
   rw [← Int.max_assoc, Int.max_self]