Merge branch 'master' into inhabitation

.github/ISSUE_TEMPLATE/bug_report.md

@@ -39,7 +39,7 @@ Please put an X between the brackets as you perform the following steps:
 
 ### Versions
 
-[Output of `#eval Lean.versionString`]
+[Output of `#version` or `#eval Lean.versionString`]
 [OS version, if not using live.lean-lang.org.]
 
 ### Additional Information

doc/monads/applicatives.lean

@@ -138,8 +138,8 @@ definition:
 
 -/
 instance : Applicative List where
-  pure := List.pure
-  seq f x := List.bind f fun y => Functor.map y (x ())
+  pure := List.singleton
+  seq f x := List.flatMap f fun y => Functor.map y (x ())
 /-!
 
 Notice you can now sequence a _list_ of functions and a _list_ of items.

doc/monads/laws.lean

@@ -128,8 +128,8 @@ Applying the identity function through an applicative structure should not chang
 values or structure.  For example:
 -/
 instance : Applicative List where
-  pure := List.pure
-  seq f x := List.bind f fun y => Functor.map y (x ())
+  pure := List.singleton
+  seq f x := List.flatMap f fun y => Functor.map y (x ())
 
 #eval pure id <*> [1, 2, 3]  -- [1, 2, 3]
 /-!
@@ -235,8 +235,8 @@ structure or its values.
 Left identity is `x >>= pure = x` and is demonstrated by the following examples on a monadic `List`:
 -/
 instance : Monad List  where
-  pure := List.pure
-  bind := List.bind
+  pure := List.singleton
+  bind := List.flatMap
 
 def a := ["apple", "orange"]
 

doc/monads/monads.lean

@@ -192,8 +192,8 @@ implementation of `pure` and `bind`.
 
 -/
 instance : Monad List  where
-  pure := List.pure
-  bind := List.bind
+  pure := List.singleton
+  bind := List.flatMap
 /-!
 
 Like you saw with the applicative `seq` operator, the `bind` operator applies the given function

src/Init/Control/Basic.lean

@@ -8,6 +8,28 @@ import Init.Core
 
 universe u v w
 
+/--
+A `ForIn'` instance, which handles `for h : x in c do`,
+can also handle `for x in x do` by ignoring `h`, and so provides a `ForIn` instance.
+-/
+instance (priority := low) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α where
+  forIn x b f := forIn' x b fun a _ => f a
+
+@[simp] theorem forIn'_eq_forIn [d : Membership α ρ] [ForIn' m ρ α d] {β} [Monad m] (x : ρ) (b : β)
+    (f : (a : α) → a ∈ x → β → m (ForInStep β)) (g : (a : α) → β → m (ForInStep β))
+    (h : ∀ a m b, f a m b = g a b) :
+    forIn' x b f = forIn x b g := by
+  simp [instForInOfForIn']
+  congr
+  apply funext
+  intro a
+  apply funext
+  intro m
+  apply funext
+  intro b
+  simp [h]
+  rfl
+
 @[reducible]
 def Functor.mapRev {f : Type u → Type v} [Functor f] {α β : Type u} : f α → (α → β) → f β :=
   fun a f => f <$> a

src/Init/Core.lean

@@ -324,7 +324,6 @@ class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)
 
 export ForIn' (forIn')
 
-
 /--
 Auxiliary type used to compile `do` notation. It is used when compiling a do block
 nested inside a combinator like `tryCatch`. It encodes the possible ways the

src/Init/Data/Array/Basic.lean

@@ -25,7 +25,7 @@ variable {α : Type u}
 
 namespace Array
 
-@[deprecated size (since := "2024-10-13")] abbrev data := @toList
+@[deprecated toList (since := "2024-10-13")] abbrev data := @toList
 
 /-! ### Preliminary theorems -/
 
@@ -82,6 +82,22 @@ theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
 
 @[simp] theorem getElem_toList {a : Array α} {i : Nat} (h : i < a.size) : a.toList[i] = a[i] := rfl
 
+/-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`. -/
+-- NB: This is defined as a structure rather than a plain def so that a lemma
+-- like `sizeOf_lt_of_mem` will not apply with no actual arrays around.
+structure Mem (as : Array α) (a : α) : Prop where
+  val : a ∈ as.toList
+
+instance : Membership α (Array α) where
+  mem := Mem
+
+theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
+  ⟨fun | .mk h => h, Array.Mem.mk⟩
+
+@[simp] theorem getElem_mem {l : Array α} {i : Nat} (h : i < l.size) : l[i] ∈ l := by
+  rw [Array.mem_def, ← getElem_toList]
+  apply List.getElem_mem
+
 end Array
 
 namespace List
@@ -316,6 +332,37 @@ protected def forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m
 instance : ForIn m (Array α) α where
   forIn := Array.forIn
 
+/-- See comment at `forInUnsafe` -/
+@[inline] unsafe def forIn'Unsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β :=
+  let sz := as.usize
+  let rec @[specialize] loop (i : USize) (b : β) : m β := do
+    if i < sz then
+      let a := as.uget i lcProof
+      match (← f a lcProof b) with
+      | ForInStep.done  b => pure b
+      | ForInStep.yield b => loop (i+1) b
+    else
+      pure b
+  loop 0 b
+
+/-- Reference implementation for `forIn'` -/
+@[implemented_by Array.forIn'Unsafe]
+protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β :=
+  let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := do
+    match i, h with
+    | 0,   _ => pure b
+    | i+1, h =>
+      have h' : i < as.size            := Nat.lt_of_lt_of_le (Nat.lt_succ_self i) h
+      have : as.size - 1 < as.size     := Nat.sub_lt (Nat.zero_lt_of_lt h') (by decide)
+      have : as.size - 1 - i < as.size := Nat.lt_of_le_of_lt (Nat.sub_le (as.size - 1) i) this
+      match (← f as[as.size - 1 - i] (getElem_mem this) b) with
+      | ForInStep.done b  => pure b
+      | ForInStep.yield b => loop i (Nat.le_of_lt h') b
+  loop as.size (Nat.le_refl _) b
+
+instance : ForIn' m (Array α) α inferInstance where
+  forIn' := Array.forIn'
+
 /-- See comment at `forInUnsafe` -/
 @[inline]
 unsafe def foldlMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (as : Array α) (start := 0) (stop := as.size) : m β :=
@@ -645,7 +692,7 @@ instance : HAppend (Array α) (List α) (Array α) := ⟨Array.appendList⟩
 def flatMapM [Monad m] (f : α → m (Array β)) (as : Array α) : m (Array β) :=
   as.foldlM (init := empty) fun bs a => do return bs ++ (← f a)
 
-@[deprecated concatMapM (since := "2024-10-16")] abbrev concatMapM := @flatMapM
+@[deprecated flatMapM (since := "2024-10-16")] abbrev concatMapM := @flatMapM
 
 @[inline]
 def flatMap (f : α → Array β) (as : Array α) : Array β :=

src/Init/Data/Array/Lemmas.lean

@@ -21,8 +21,7 @@ namespace Array
 
 @[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) : (Array.mk xs)[i] = xs[i] := rfl
 
-theorem getElem_eq_getElem_toList {a : Array α} (h : i < a.size) : a[i] = a.toList[i] := by
-  by_cases i < a.size <;> (try simp [*]) <;> rfl
+theorem getElem_eq_getElem_toList {a : Array α} (h : i < a.size) : a[i] = a.toList[i] := rfl
 
 theorem getElem?_eq_getElem {a : Array α} {i : Nat} (h : i < a.size) : a[i]? = some a[i] :=
   getElem?_pos ..
@@ -85,6 +84,9 @@ We prefer to pull `List.toArray` outwards.
     (a.toArrayAux b).size = b.size + a.length := by
   simp [size]
 
+@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
+  simp [mem_def]
+
 @[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
   apply ext'
   simp
@@ -121,6 +123,30 @@ We prefer to pull `List.toArray` outwards.
   rw [Array.forIn, forIn_loop_toArray]
   simp
 
+@[simp] theorem forIn'_loop_toArray [Monad m] (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (i : Nat)
+    (h : i ≤ l.length) (b : β) :
+    Array.forIn'.loop l.toArray f i h b =
+      forIn' (l.drop (l.length - i)) b (fun a m b => f a (by simpa using mem_of_mem_drop m) b) := by
+  induction i generalizing l b with
+  | zero =>
+    simp [Array.forIn'.loop]
+  | succ i ih =>
+    simp only [Array.forIn'.loop, size_toArray, getElem_toArray, ih, forIn_eq_forIn]
+    have t : drop (l.length - (i + 1)) l = l[l.length - i - 1] :: drop (l.length - i) l := by
+      simp only [Nat.sub_add_eq]
+      rw [List.drop_sub_one (by omega), List.getElem?_eq_getElem (by omega)]
+      simp only [Option.toList_some, singleton_append]
+    simp [t]
+    have t : l.length - 1 - i = l.length - i - 1 := by omega
+    simp only [t]
+    congr
+
+@[simp] theorem forIn'_toArray [Monad m] (l : List α) (b : β) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) :
+    forIn' l.toArray b f = forIn' l b (fun a m b => f a (mem_toArray.mpr m) b) := by
+  change Array.forIn' _ _ _ = List.forIn' _ _ _
+  rw [Array.forIn', forIn'_loop_toArray]
+  simp [List.forIn_eq_forIn]
+
 theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) :
     l.toArray.foldrM f init = l.foldrM f init := by
   rw [foldrM_eq_reverse_foldlM_toList]
@@ -268,9 +294,6 @@ 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.toList :=
-  ⟨fun | .mk h => h, Array.Mem.mk⟩
-
 @[simp] theorem not_mem_empty (a : α) : ¬(a ∈ #[]) := by
   simp [mem_def]
 
@@ -460,10 +483,6 @@ theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size}
     idx < a.size :=
   hidx
 
-@[simp] theorem getElem_mem {l : Array α} {i : Nat} (h : i < l.size) : l[i] ∈ l := by
-  erw [Array.mem_def, getElem_eq_getElem_toList]
-  apply List.get_mem
-
 theorem getElem_fin_eq_getElem_toList (a : Array α) (i : Fin a.size) : a[i] = a.toList[i] := rfl
 
 @[simp] theorem ugetElem_eq_getElem (a : Array α) {i : USize} (h : i.toNat < a.size) :
@@ -728,6 +747,11 @@ theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Arra
   cases as
   simp
 
+@[simp] theorem forIn'_toList [Monad m] (as : Array α) (b : β) (f : (a : α) → a ∈ as.toList → β → m (ForInStep β)) :
+    forIn' as.toList b f = forIn' as b (fun a m b => f a (mem_toList.mpr m) b) := by
+  cases as
+  simp
+
 /-! ### foldl / foldr -/
 
 @[simp] theorem foldlM_loop_empty [Monad m] (f : β → α → m β) (init : β) (i j : Nat) :
@@ -1411,9 +1435,6 @@ namespace List
 Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
 -/
 
-@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
-  simp [mem_def]
-
 @[simp] theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse := by
   simp
 

src/Init/Data/Array/Mem.lean

@@ -10,15 +10,6 @@ import Init.Data.List.BasicAux
 
 namespace Array
 
-/-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`. -/
--- NB: This is defined as a structure rather than a plain def so that a lemma
--- like `sizeOf_lt_of_mem` will not apply with no actual arrays around.
-structure Mem (as : Array α) (a : α) : Prop where
-  val : a ∈ as.toList
-
-instance : Membership α (Array α) where
-  mem := Mem
-
 theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a < sizeOf as := by
   cases as with | _ as =>
   exact Nat.lt_trans (List.sizeOf_lt_of_mem h.val) (by simp_arith)

src/Init/Data/BitVec/Basic.lean

@@ -634,6 +634,16 @@ def twoPow (w : Nat) (i : Nat) : BitVec w := 1#w <<< i
 
 end bitwise
 
+/-- Compute a hash of a bitvector, combining 64-bit words using `mixHash`. -/
+def hash (bv : BitVec n) : UInt64 :=
+  if n ≤ 64 then
+    bv.toFin.val.toUInt64
+  else
+    mixHash (bv.toFin.val.toUInt64) (hash ((bv >>> 64).setWidth (n - 64)))
+
+instance : Hashable (BitVec n) where
+  hash := hash
+
 section normalization_eqs
 /-! We add simp-lemmas that rewrite bitvector operations into the equivalent notation -/
 @[simp] theorem append_eq (x : BitVec w) (y : BitVec v)   : BitVec.append x y = x ++ y        := rfl