feat: decidable quantifers for BitVec

The `xor_allOnes` theorems end up in the `not` section, as the relevant
simplification lemmas are otherwise not defined.

doc/dev/release_checklist.md

@@ -71,6 +71,12 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - Toolchain bump PR including updated Lake manifest
       - Create and push the tag
       - There is no `stable` branch; skip this step
+    - [Verso](https://github.com/leanprover/verso)
+      - Dependencies: exist, but they're not part of the release workflow
+      - The `SubVerso` dependency should be compatible with _every_ Lean release simultaneously, rather than following this workflow
+      - Toolchain bump PR including updated Lake manifest
+      - Create and push the tag
+      - There is no `stable` branch; skip this step
     - [import-graph](https://github.com/leanprover-community/import-graph)
       - Toolchain bump PR including updated Lake manifest
       - Create and push the tag

src/Init/Data/Array.lean

@@ -15,3 +15,4 @@ import Init.Data.Array.BasicAux
 import Init.Data.Array.Lemmas
 import Init.Data.Array.TakeDrop
 import Init.Data.Array.Bootstrap
+import Init.Data.Array.GetLit

src/Init/Data/Array/Basic.lean

@@ -13,43 +13,76 @@ import Init.Data.ToString.Basic
 import Init.GetElem
 universe u v w
 
-namespace Array
+/-! ### Array literal syntax -/
+
+syntax "#[" withoutPosition(sepBy(term, ", ")) "]" : term
+
+macro_rules
+  | `(#[ $elems,* ]) => `(List.toArray [ $elems,* ])
+
 variable {α : Type u}
 
+namespace Array
+
+/-! ### Preliminary theorems -/
+
+@[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
+  List.length_set ..
+
+@[simp] theorem size_push (a : Array α) (v : α) : (push a v).size = a.size + 1 :=
+  List.length_concat ..
+
+theorem ext (a b : Array α)
+    (h₁ : a.size = b.size)
+    (h₂ : (i : Nat) → (hi₁ : i < a.size) → (hi₂ : i < b.size) → a[i] = b[i])
+    : a = b := by
+  let rec extAux (a b : List α)
+      (h₁ : a.length = b.length)
+      (h₂ : (i : Nat) → (hi₁ : i < a.length) → (hi₂ : i < b.length) → a.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩)
+      : a = b := by
+    induction a generalizing b with
+    | nil =>
+      cases b with
+      | nil       => rfl
+      | cons b bs => rw [List.length_cons] at h₁; injection h₁
+    | cons a as ih =>
+      cases b with
+      | nil => rw [List.length_cons] at h₁; injection h₁
+      | cons b bs =>
+        have hz₁ : 0 < (a::as).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
+        have hz₂ : 0 < (b::bs).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
+        have headEq : a = b := h₂ 0 hz₁ hz₂
+        have h₁' : as.length = bs.length := by rw [List.length_cons, List.length_cons] at h₁; injection h₁
+        have h₂' : (i : Nat) → (hi₁ : i < as.length) → (hi₂ : i < bs.length) → as.get ⟨i, hi₁⟩ = bs.get ⟨i, hi₂⟩ := by
+          intro i hi₁ hi₂
+          have hi₁' : i+1 < (a::as).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
+          have hi₂' : i+1 < (b::bs).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
+          have : (a::as).get ⟨i+1, hi₁'⟩ = (b::bs).get ⟨i+1, hi₂'⟩ := h₂ (i+1) hi₁' hi₂'
+          apply this
+        have tailEq : as = bs := ih bs h₁' h₂'
+        rw [headEq, tailEq]
+  cases a; cases b
+  apply congrArg
+  apply extAux
+  assumption
+  assumption
+
+theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
+  cases as; cases bs; simp at h; rw [h]
+
+@[simp] theorem toArrayAux_eq (as : List α) (acc : Array α) : (as.toArrayAux acc).toList = acc.toList ++ as := by
+  induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append]
+
+@[simp] theorem toList_toArray (as : List α) : as.toArray.toList = as := by
+  simp [List.toArray, Array.mkEmpty]
+
+@[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
+
+@[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @toList_toArray
+
 @[deprecated Array.toList (since := "2024-09-10")] abbrev Array.data := @Array.toList
 
-@[extern "lean_mk_array"]
-def mkArray {α : Type u} (n : Nat) (v : α) : Array α where
-  toList := List.replicate n v
-
-/--
-`ofFn f` with `f : Fin n → α` returns the list whose ith element is `f i`.
-```
-ofFn f = #[f 0, f 1, ... , f(n - 1)]
-``` -/
-def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
-  /-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]` -/
-  go (i : Nat) (acc : Array α) : Array α :=
-    if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
-termination_by n - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-/-- The array `#[0, 1, ..., n - 1]`. -/
-def range (n : Nat) : Array Nat :=
-  n.fold (flip Array.push) (mkEmpty n)
-
-@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
-  List.length_replicate ..
-
-instance : EmptyCollection (Array α) := ⟨Array.empty⟩
-instance : Inhabited (Array α) where
-  default := Array.empty
-
-@[simp] def isEmpty (a : Array α) : Bool :=
-  a.size = 0
-
-def singleton (v : α) : Array α :=
-  mkArray 1 v
+/-! ### Externs -/
 
 /-- Low-level version of `size` that directly queries the C array object cached size.
     While this is not provable, `usize` always returns the exact size of the array since
@@ -65,29 +98,6 @@ def usize (a : @& Array α) : USize := a.size.toUSize
 def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
   a[i.toNat]
 
-instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
-  getElem xs i h := xs.uget i h
-
-def back [Inhabited α] (a : Array α) : α :=
-  a.get! (a.size - 1)
-
-def get? (a : Array α) (i : Nat) : Option α :=
-  if h : i < a.size then some a[i] else none
-
-def back? (a : Array α) : Option α :=
-  a.get? (a.size - 1)
-
--- auxiliary declaration used in the equation compiler when pattern matching array literals.
-abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size = n) (h₂ : i < n) : α :=
-  have := h₁.symm ▸ h₂
-  a[i]
-
-@[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
-  List.length_set ..
-
-@[simp] theorem size_push (a : Array α) (v : α) : (push a v).size = a.size + 1 :=
-  List.length_concat ..
-
 /-- Low-level version of `fset` which is as fast as a C array fset.
    `Fin` values are represented as tag pointers in the Lean runtime. Thus,
    `fset` may be slightly slower than `uset`. -/
@@ -95,6 +105,19 @@ abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size =
 def uset (a : Array α) (i : USize) (v : α) (h : i.toNat < a.size) : Array α :=
   a.set ⟨i.toNat, h⟩ v
 
+@[extern "lean_array_pop"]
+def pop (a : Array α) : Array α where
+  toList := a.toList.dropLast
+
+@[simp] theorem size_pop (a : Array α) : a.pop.size = a.size - 1 := by
+  match a with
+  | ⟨[]⟩ => rfl
+  | ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub, size]
+
+@[extern "lean_mk_array"]
+def mkArray {α : Type u} (n : Nat) (v : α) : Array α where
+  toList := List.replicate n v
+
 /--
 Swaps two entries in an array.
 
@@ -108,6 +131,10 @@ def swap (a : Array α) (i j : @& Fin a.size) : Array α :=
   let a'  := a.set i v₂
   a'.set (size_set a i v₂ ▸ j) v₁
 
+@[simp] theorem size_swap (a : Array α) (i j : Fin a.size) : (a.swap i j).size = a.size := by
+  show ((a.set i (a.get j)).set (size_set a i _ ▸ j) (a.get i)).size = a.size
+  rw [size_set, size_set]
+
 /--
 Swaps two entries in an array, or returns the array unchanged if either index is out of bounds.
 
@@ -121,6 +148,66 @@ def swap! (a : Array α) (i j : @& Nat) : Array α :=
   else a
   else a
 
+/-! ### GetElem instance for `USize`, backed by `uget` -/
+
+instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
+  getElem xs i h := xs.uget i h
+
+/-! ### Definitions -/
+
+instance : EmptyCollection (Array α) := ⟨Array.empty⟩
+instance : Inhabited (Array α) where
+  default := Array.empty
+
+@[simp] def isEmpty (a : Array α) : Bool :=
+  a.size = 0
+
+-- TODO(Leo): cleanup
+@[specialize]
+def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (i : Nat) : Bool :=
+  if h : i < a.size then
+     have : i < b.size := hsz ▸ h
+     p a[i] b[i] && isEqvAux a b hsz p (i+1)
+  else
+    true
+decreasing_by simp_wf; decreasing_trivial_pre_omega
+
+@[inline] def isEqv (a b : Array α) (p : α → α → Bool) : Bool :=
+  if h : a.size = b.size then
+    isEqvAux a b h p 0
+  else
+    false
+
+instance [BEq α] : BEq (Array α) :=
+  ⟨fun a b => isEqv a b BEq.beq⟩
+
+/--
+`ofFn f` with `f : Fin n → α` returns the list whose ith element is `f i`.
+```
+ofFn f = #[f 0, f 1, ... , f(n - 1)]
+``` -/
+def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
+  /-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]` -/
+  go (i : Nat) (acc : Array α) : Array α :=
+    if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
+decreasing_by simp_wf; decreasing_trivial_pre_omega
+
+/-- The array `#[0, 1, ..., n - 1]`. -/
+def range (n : Nat) : Array Nat :=
+  n.fold (flip Array.push) (mkEmpty n)
+
+def singleton (v : α) : Array α :=
+  mkArray 1 v
+
+def back [Inhabited α] (a : Array α) : α :=
+  a.get! (a.size - 1)
+
+def get? (a : Array α) (i : Nat) : Option α :=
+  if h : i < a.size then some a[i] else none
+
+def back? (a : Array α) : Option α :=
+  a.get? (a.size - 1)
+
 @[inline] def swapAt (a : Array α) (i : Fin a.size) (v : α) : α × Array α :=
   let e := a.get i
   let a := a.set i v
@@ -134,10 +221,6 @@ def swapAt! (a : Array α) (i : Nat) (v : α) : α × Array α :=
     have : Inhabited α := ⟨v⟩
     panic! ("index " ++ toString i ++ " out of bounds")
 
-@[extern "lean_array_pop"]
-def pop (a : Array α) : Array α where
-  toList := a.toList.dropLast
-
 def shrink (a : Array α) (n : Nat) : Array α :=
   let rec loop
     | 0,   a => a
@@ -311,7 +394,6 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
       map (i+1) (r.push (← f as[i]))
     else
       pure r
-  termination_by as.size - i
   decreasing_by simp_wf; decreasing_trivial_pre_omega
   map 0 (mkEmpty as.size)
 
@@ -384,7 +466,6 @@ def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as :
           loop (j+1)
       else
         pure false
-      termination_by stop - j
       decreasing_by simp_wf; decreasing_trivial_pre_omega
     loop start
   if h : stop ≤ as.size then
@@ -470,12 +551,22 @@ def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
     if h : j < as.size then
       if p as[j] then some j else loop (j + 1)
     else none
-    termination_by as.size - j
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   loop 0
 
 def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
-a.findIdx? fun a => a == v
+  a.findIdx? fun a => a == v
+
+def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
+  if h : i < a.size then
+    let idx : Fin a.size := ⟨i, h⟩;
+    if a.get idx == v then some idx
+    else indexOfAux a v (i+1)
+  else none
+decreasing_by simp_wf; decreasing_trivial_pre_omega
+
+def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
+  indexOfAux a v 0
 
 @[inline]
 def any (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool :=
@@ -491,13 +582,6 @@ def contains [BEq α] (as : Array α) (a : α) : Bool :=
 def elem [BEq α] (a : α) (as : Array α) : Bool :=
   as.contains a
 
-@[inline] def getEvenElems (as : Array α) : Array α :=
-  (·.2) <| as.foldl (init := (true, Array.empty)) fun (even, r) a =>
-    if even then
-      (false, r.push a)
-    else
-      (true, r)
-
 /-- Convert a `Array α` into an `List α`. This is O(n) in the size of the array.  -/
 -- This function is exported to C, where it is called by `Array.toList`
 -- (the projection) to implement this functionality.
@@ -510,17 +594,6 @@ def toListImpl (as : Array α) : List α :=
 def toListAppend (as : Array α) (l : List α) : List α :=
   as.foldr List.cons l
 
-instance {α : Type u} [Repr α] : Repr (Array α) where
-  reprPrec a _ :=
-    let _ : Std.ToFormat α := ⟨repr⟩
-    if a.size == 0 then
-      "#[]"
-    else
-      Std.Format.bracketFill "#[" (Std.Format.joinSep (toList a) ("," ++ Std.Format.line)) "]"
-
-instance [ToString α] : ToString (Array α) where
-  toString a := "#" ++ toString a.toList
-
 protected def append (as : Array α) (bs : Array α) : Array α :=
   bs.foldl (init := as) fun r v => r.push v
 
@@ -546,44 +619,13 @@ def concatMap (f : α → Array β) (as : Array α) : Array β :=
 def flatten (as : Array (Array α)) : Array α :=
   as.foldl (init := empty) fun r a => r ++ a
 
-end Array
-
-export Array (mkArray)
-
-syntax "#[" withoutPosition(sepBy(term, ", ")) "]" : term
-
-macro_rules
-  | `(#[ $elems,* ]) => `(List.toArray [ $elems,* ])
-
-namespace Array
-
--- TODO(Leo): cleanup
-@[specialize]
-def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (i : Nat) : Bool :=
-  if h : i < a.size then
-     have : i < b.size := hsz ▸ h
-     p a[i] b[i] && isEqvAux a b hsz p (i+1)
-  else
-    true
-termination_by a.size - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-@[inline] def isEqv (a b : Array α) (p : α → α → Bool) : Bool :=
-  if h : a.size = b.size then
-    isEqvAux a b h p 0
-  else
-    false
-
-instance [BEq α] : BEq (Array α) :=
-  ⟨fun a b => isEqv a b BEq.beq⟩
-
 @[inline]
 def filter (p : α → Bool) (as : Array α) (start := 0) (stop := as.size) : Array α :=
   as.foldl (init := #[]) (start := start) (stop := stop) fun r a =>
     if p a then r.push a else r
 
 @[inline]
-def filterM [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m (Array α) :=
+def filterM {α : Type} [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m (Array α) :=
   as.foldlM (init := #[]) (start := start) (stop := stop) fun r a => do
     if (← p a) then return r.push a else return r
 
@@ -618,92 +660,23 @@ def partition (p : α → Bool) (as : Array α) : Array α × Array α := Id.run
       cs := cs.push a
   return (bs, cs)
 
-theorem ext (a b : Array α)
-    (h₁ : a.size = b.size)
-    (h₂ : (i : Nat) → (hi₁ : i < a.size) → (hi₂ : i < b.size) → a[i] = b[i])
-    : a = b := by
-  let rec extAux (a b : List α)
-      (h₁ : a.length = b.length)
-      (h₂ : (i : Nat) → (hi₁ : i < a.length) → (hi₂ : i < b.length) → a.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩)
-      : a = b := by
-    induction a generalizing b with
-    | nil =>
-      cases b with
-      | nil       => rfl
-      | cons b bs => rw [List.length_cons] at h₁; injection h₁
-    | cons a as ih =>
-      cases b with
-      | nil => rw [List.length_cons] at h₁; injection h₁
-      | cons b bs =>
-        have hz₁ : 0 < (a::as).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
-        have hz₂ : 0 < (b::bs).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
-        have headEq : a = b := h₂ 0 hz₁ hz₂
-        have h₁' : as.length = bs.length := by rw [List.length_cons, List.length_cons] at h₁; injection h₁
-        have h₂' : (i : Nat) → (hi₁ : i < as.length) → (hi₂ : i < bs.length) → as.get ⟨i, hi₁⟩ = bs.get ⟨i, hi₂⟩ := by
-          intro i hi₁ hi₂
-          have hi₁' : i+1 < (a::as).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
-          have hi₂' : i+1 < (b::bs).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
-          have : (a::as).get ⟨i+1, hi₁'⟩ = (b::bs).get ⟨i+1, hi₂'⟩ := h₂ (i+1) hi₁' hi₂'
-          apply this
-        have tailEq : as = bs := ih bs h₁' h₂'
-        rw [headEq, tailEq]
-  cases a; cases b
-  apply congrArg
-  apply extAux
-  assumption
-  assumption
-
-theorem extLit {n : Nat}
-    (a b : Array α)
-    (hsz₁ : a.size = n) (hsz₂ : b.size = n)
-    (h : (i : Nat) → (hi : i < n) → a.getLit i hsz₁ hi = b.getLit i hsz₂ hi) : a = b :=
-  Array.ext a b (hsz₁.trans hsz₂.symm) fun i hi₁ _ => h i (hsz₁ ▸ hi₁)
-
-end Array
-
--- CLEANUP the following code
-namespace Array
-
-def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
-  if h : i < a.size then
-    let idx : Fin a.size := ⟨i, h⟩;
-    if a.get idx == v then some idx
-    else indexOfAux a v (i+1)
-  else none
-termination_by a.size - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
-  indexOfAux a v 0
-
-@[simp] theorem size_swap (a : Array α) (i j : Fin a.size) : (a.swap i j).size = a.size := by
-  show ((a.set i (a.get j)).set (size_set a i _ ▸ j) (a.get i)).size = a.size
-  rw [size_set, size_set]
-
-@[simp] theorem size_pop (a : Array α) : a.pop.size = a.size - 1 := by
-  match a with
-  | ⟨[]⟩ => rfl
-  | ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub, size]
-
-theorem reverse.termination {i j : Nat} (h : i < j) : j - 1 - (i + 1) < j - i := by
-  rw [Nat.sub_sub, Nat.add_comm]
-  exact Nat.lt_of_le_of_lt (Nat.pred_le _) (Nat.sub_succ_lt_self _ _ h)
-
 def reverse (as : Array α) : Array α :=
   if h : as.size ≤ 1 then
     as
   else
     loop as 0 ⟨as.size - 1, Nat.pred_lt (mt (fun h : as.size = 0 => h ▸ by decide) h)⟩
 where
+  termination {i j : Nat} (h : i < j) : j - 1 - (i + 1) < j - i := by
+    rw [Nat.sub_sub, Nat.add_comm]
+    exact Nat.lt_of_le_of_lt (Nat.pred_le _) (Nat.sub_succ_lt_self _ _ h)
   loop (as : Array α) (i : Nat) (j : Fin as.size) :=
     if h : i < j then
-      have := reverse.termination h
+      have := termination h
       let as := as.swap ⟨i, Nat.lt_trans h j.2⟩ j
       have : j-1 < as.size := by rw [size_swap]; exact Nat.lt_of_le_of_lt (Nat.pred_le _) j.2
       loop as (i+1) ⟨j-1, this⟩
     else
       as
-termination_by j - i
 
 def popWhile (p : α → Bool) (as : Array α) : Array α :=
   if h : as.size > 0 then
@@ -713,7 +686,6 @@ def popWhile (p : α → Bool) (as : Array α) : Array α :=
       as
   else
     as
-termination_by as.size
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def takeWhile (p : α → Bool) (as : Array α) : Array α :=
@@ -726,7 +698,6 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
         r
     else
       r
-    termination_by as.size - i
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   go 0 #[]
 
@@ -744,6 +715,7 @@ def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
 termination_by a.size - i.val
 decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ i.isLt
 
+-- This is required in `Lean.Data.PersistentHashMap`.
 theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
   induction a, i using Array.feraseIdx.induct with
   | @case1 a i h a' _ ih =>
@@ -774,7 +746,6 @@ def erase [BEq α] (as : Array α) (a : α) : Array α :=
       loop as ⟨j', by rw [size_swap]; exact j'.2⟩
     else
       as
-    termination_by j.1
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   let j := as.size
   let as := as.push a
@@ -786,41 +757,6 @@ def insertAt! (as : Array α) (i : Nat) (a : α) : Array α :=
     insertAt as ⟨i, Nat.lt_succ_of_le h⟩ a
   else panic! "invalid index"
 
-def toListLitAux (a : Array α) (n : Nat) (hsz : a.size = n) : ∀ (i : Nat), i ≤ a.size → List α → List α
-  | 0,     _,  acc => acc
-  | (i+1), hi, acc => toListLitAux a n hsz i (Nat.le_of_succ_le hi) (a.getLit i hsz (Nat.lt_of_lt_of_eq (Nat.lt_of_lt_of_le (Nat.lt_succ_self i) hi) hsz) :: acc)
-
-def toArrayLit (a : Array α) (n : Nat) (hsz : a.size = n) : Array α :=
-  List.toArray <| toListLitAux a n hsz n (hsz ▸ Nat.le_refl _) []
-
-theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
-  cases as; cases bs; simp at h; rw [h]
-
-@[simp] theorem toArrayAux_eq (as : List α) (acc : Array α) : (as.toArrayAux acc).toList = acc.toList ++ as := by
-  induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append]
-
-@[simp] theorem toList_toArray (as : List α) : as.toArray.toList = as := by
-  simp [List.toArray, Array.mkEmpty]
-
-@[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @toList_toArray
-
-@[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
-
-theorem toArrayLit_eq (as : Array α) (n : Nat) (hsz : as.size = n) : as = toArrayLit as n hsz := by
-  apply ext'
-  simp [toArrayLit, toList_toArray]
-  have hle : n ≤ as.size := hsz ▸ Nat.le_refl _
-  have hge : as.size ≤ n := hsz ▸ Nat.le_refl _
-  have := go n hle
-  rw [List.drop_eq_nil_of_le hge] at this
-  rw [this]
-where
-  getLit_eq (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = getElem as.toList i ((id (α := as.toList.length = n) h₁) ▸ h₂) :=
-    rfl
-
-  go (i : Nat) (hi : i ≤ as.size) : toListLitAux as n hsz i hi (as.toList.drop i) = as.toList := by
-    induction i <;> simp [getLit_eq, List.get_drop_eq_drop, toListLitAux, List.drop, *]
-
 def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : Nat) : Bool :=
   if h : i < as.size then
     let a := as[i]
@@ -832,7 +768,6 @@ def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : N
       false
   else
     true
-termination_by as.size - i
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 /-- Return true iff `as` is a prefix of `bs`.
@@ -843,23 +778,6 @@ def isPrefixOf [BEq α] (as bs : Array α) : Bool :=
   else
     false
 
-private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat), i < as.size → Bool
-  | 0,   _ => true
-  | i+1, h =>
-    have : i < as.size := Nat.lt_trans (Nat.lt_succ_self _) h;
-    a != as[i] && allDiffAuxAux as a i this
-
-private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
-  if h : i < as.size then
-    allDiffAuxAux as as[i] i h && allDiffAux as (i+1)
-  else
-    true
-termination_by as.size - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-def allDiff [BEq α] (as : Array α) : Bool :=
-  allDiffAux as 0
-
 @[specialize] def zipWithAux (f : α → β → γ) (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) : Array γ :=
   if h : i < as.size then
     let a := as[i]
@@ -870,7 +788,6 @@ def allDiff [BEq α] (as : Array α) : Bool :=
       cs
   else
     cs
-termination_by as.size - i
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 @[inline] def zipWith (as : Array α) (bs : Array β) (f : α → β → γ) : Array γ :=
@@ -886,4 +803,47 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α :=
   as.foldl (init := (#[], #[])) fun (as, bs) a =>
     if p a then (as.push a, bs) else (as, bs.push a)
 
+/-! ### Auxiliary functions used in metaprogramming.
+
+We do not intend to provide verification theorems for these functions.
+-/
+
+private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat), i < as.size → Bool
+  | 0,   _ => true
+  | i+1, h =>
+    have : i < as.size := Nat.lt_trans (Nat.lt_succ_self _) h;
+    a != as[i] && allDiffAuxAux as a i this
+
+private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
+  if h : i < as.size then
+    allDiffAuxAux as as[i] i h && allDiffAux as (i+1)
+  else
+    true
+decreasing_by simp_wf; decreasing_trivial_pre_omega
+
+def allDiff [BEq α] (as : Array α) : Bool :=
+  allDiffAux as 0
+
+@[inline] def getEvenElems (as : Array α) : Array α :=
+  (·.2) <| as.foldl (init := (true, Array.empty)) fun (even, r) a =>
+    if even then
+      (false, r.push a)
+    else
+      (true, r)
+
+/-! ### Repr and ToString -/
+
+instance {α : Type u} [Repr α] : Repr (Array α) where
+  reprPrec a _ :=
+    let _ : Std.ToFormat α := ⟨repr⟩
+    if a.size == 0 then
+      "#[]"
+    else
+      Std.Format.bracketFill "#[" (Std.Format.joinSep (toList a) ("," ++ Std.Format.line)) "]"
+
+instance [ToString α] : ToString (Array α) where
+  toString a := "#" ++ toString a.toList
+
 end Array
+
+export Array (mkArray)

src/Init/Data/Array/GetLit.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+
+prelude
+import Init.Data.Array.Basic
+
+namespace Array
+
+/-! ### getLit -/
+
+-- auxiliary declaration used in the equation compiler when pattern matching array literals.
+abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size = n) (h₂ : i < n) : α :=
+  have := h₁.symm ▸ h₂
+  a[i]
+
+theorem extLit {n : Nat}
+    (a b : Array α)
+    (hsz₁ : a.size = n) (hsz₂ : b.size = n)
+    (h : (i : Nat) → (hi : i < n) → a.getLit i hsz₁ hi = b.getLit i hsz₂ hi) : a = b :=
+  Array.ext a b (hsz₁.trans hsz₂.symm) fun i hi₁ _ => h i (hsz₁ ▸ hi₁)
+
+def toListLitAux (a : Array α) (n : Nat) (hsz : a.size = n) : ∀ (i : Nat), i ≤ a.size → List α → List α
+  | 0,     _,  acc => acc
+  | (i+1), hi, acc => toListLitAux a n hsz i (Nat.le_of_succ_le hi) (a.getLit i hsz (Nat.lt_of_lt_of_eq (Nat.lt_of_lt_of_le (Nat.lt_succ_self i) hi) hsz) :: acc)
+
+def toArrayLit (a : Array α) (n : Nat) (hsz : a.size = n) : Array α :=
+  List.toArray <| toListLitAux a n hsz n (hsz ▸ Nat.le_refl _) []
+
+theorem toArrayLit_eq (as : Array α) (n : Nat) (hsz : as.size = n) : as = toArrayLit as n hsz := by
+  apply ext'
+  simp [toArrayLit, toList_toArray]
+  have hle : n ≤ as.size := hsz ▸ Nat.le_refl _
+  have hge : as.size ≤ n := hsz ▸ Nat.le_refl _
+  have := go n hle
+  rw [List.drop_eq_nil_of_le hge] at this
+  rw [this]
+where
+  getLit_eq (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = getElem as.toList i ((id (α := as.toList.length = n) h₁) ▸ h₂) :=
+    rfl
+  go (i : Nat) (hi : i ≤ as.size) : toListLitAux as n hsz i hi (as.toList.drop i) = as.toList := by
+    induction i <;> simp [getLit_eq, List.get_drop_eq_drop, toListLitAux, List.drop, *]
+
+end Array

src/Init/Data/Array/Lemmas.lean

@@ -271,6 +271,9 @@ termination_by n - i
 
 /-- # mkArray -/
 
+@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
+  List.length_replicate ..
+
 @[simp] theorem toList_mkArray (n : Nat) (v : α) : (mkArray n v).toList = List.replicate n v := rfl
 
 @[deprecated toList_mkArray (since := "2024-09-09")]
@@ -495,7 +498,6 @@ abbrev size_eq_length_data := @size_eq_length_toList
   let rec go (as : Array α) (i j) : (reverse.loop as i j).size = as.size := by
     rw [reverse.loop]
     if h : i < j then
-      have := reverse.termination h
       simp [(go · (i+1) ⟨j-1, ·⟩), h]
     else simp [h]
     termination_by j - i
@@ -527,9 +529,8 @@ set_option linter.deprecated false in
       (H : ∀ k, as.toList.get? k = if i ≤ k ∧ k ≤ j then a.toList.get? k else a.toList.reverse.get? k)
       (k) : (reverse.loop as i ⟨j, hj⟩).toList.get? k = a.toList.reverse.get? k := by
     rw [reverse.loop]; dsimp; split <;> rename_i h₁
-    · have p := reverse.termination h₁
-      match j with | j+1 => ?_
-      simp only [Nat.add_sub_cancel] at p ⊢
+    · match j with | j+1 => ?_
+      simp only [Nat.add_sub_cancel]
       rw [(go · (i+1) j)]
       · rwa [Nat.add_right_comm i]
       · simp [size_swap, h₂]
@@ -1113,5 +1114,4 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
     · split <;> simp_all
     · split <;> simp_all
 
-
 end Array

src/Init/Data/BitVec/Lemmas.lean

@@ -710,6 +710,26 @@ theorem or_comm (x y : BitVec w) :
   simp [Bool.or_comm]
 instance : Std.Commutative (fun (x y : BitVec w) => x ||| y) := ⟨BitVec.or_comm⟩
 
+@[simp] theorem or_self {x : BitVec w} : x ||| x = x := by
+  ext i
+  simp
+
+@[simp] theorem or_zero {x : BitVec w} : x ||| 0#w = x := by
+  ext i
+  simp
+
+@[simp] theorem zero_or {x : BitVec w} : 0#w ||| x = x := by
+  ext i
+  simp
+
+@[simp] theorem or_allOnes {x : BitVec w} : x ||| allOnes w = allOnes w := by
+  ext i
+  simp
+
+@[simp] theorem allOnes_or {x : BitVec w} : allOnes w ||| x = allOnes w := by
+  ext i
+  simp
+
 /-! ### and -/
 
 @[simp] theorem toNat_and (x y : BitVec v) :
@@ -751,6 +771,26 @@ theorem and_comm (x y : BitVec w) :
   simp [Bool.and_comm]
 instance : Std.Commutative (fun (x y : BitVec w) => x &&& y) := ⟨BitVec.and_comm⟩
 
+@[simp] theorem and_self {x : BitVec w} : x &&& x = x := by
+  ext i
+  simp
+
+@[simp] theorem and_zero {x : BitVec w} : x &&& 0#w = 0#w := by
+  ext i
+  simp
+
+@[simp] theorem zero_and {x : BitVec w} : 0#w &&& x = 0#w := by
+  ext i
+  simp
+
+@[simp] theorem and_allOnes {x : BitVec w} : x &&& allOnes w = x := by
+  ext i
+  simp
+
+@[simp] theorem allOnes_and {x : BitVec w} : allOnes w &&& x = x := by
+  ext i
+  simp
+
 /-! ### xor -/
 
 @[simp] theorem toNat_xor (x y : BitVec v) :
@@ -795,6 +835,18 @@ theorem xor_comm (x y : BitVec w) :
   simp [Bool.xor_comm]
 instance : Std.Commutative (fun (x y : BitVec w) => x ^^^ y) := ⟨BitVec.xor_comm⟩
 
+@[simp] theorem xor_self {x : BitVec w} : x ^^^ x = 0#w := by
+  ext i
+  simp
+
+@[simp] theorem xor_zero {x : BitVec w} : x ^^^ 0#w = x := by
+  ext i
+  simp
+
+@[simp] theorem zero_xor {x : BitVec w} : 0#w ^^^ x = x := by
+  ext i
+  simp
+
 /-! ### not -/
 
 theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
@@ -843,6 +895,14 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   ext
   simp
 
+@[simp] theorem xor_allOnes {x : BitVec w} : x ^^^ allOnes w = ~~~ x := by
+  ext i
+  simp
+
+@[simp] theorem allOnes_xor {x : BitVec w} : allOnes w ^^^ x = ~~~ x := by
+  ext i
+  simp
+
 /-! ### cast -/
 
 @[simp] theorem not_cast {x : BitVec w} (h : w = w') : ~~~(cast h x) = cast h (~~~x) := by
@@ -1416,7 +1476,7 @@ theorem setWidth_succ (x : BitVec w) :
     have j_lt : j.val < i := Nat.lt_of_le_of_ne (Nat.le_of_succ_le_succ j.isLt) j_eq
     simp [j_eq, j_lt]
 
-theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w)) := by
+@[simp] theorem cons_msb_setWidth (x : BitVec (w+1)) : (cons x.msb (x.setWidth w)) = x := by
   ext i
   simp
   split <;> rename_i h
@@ -1425,6 +1485,10 @@ theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w)
     · simp_all
     · omega
 
+@[deprecated "Use the reverse direction of `cons_msb_setWidth`"]
+theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w)) := by
+  simp
+
 @[simp] theorem not_cons (x : BitVec w) (b : Bool) : ~~~(cons b x) = cons (!b) (~~~x) := by
   simp [cons]
 
@@ -2126,6 +2190,71 @@ theorem toNat_sub_of_le {x y : BitVec n} (h : y ≤ x) :
   · have : 2 ^ n - y.toNat + x.toNat = 2 ^ n + (x.toNat - y.toNat) := by omega
     rw [this, Nat.add_mod_left, Nat.mod_eq_of_lt (by omega)]
 
+/-! ### Decidable quantifiers -/
+
+theorem forall_zero_iff {P : BitVec 0 → Prop} :
+    (∀ v, P v) ↔ P 0#0 := by
+  constructor
+  · intro h
+    apply h
+  · intro h v
+    obtain (rfl : v = 0#0) := (by ext ⟨i, h⟩; simp at h)
+    apply h
+
+theorem forall_cons_iff {P : BitVec (n + 1) → Prop} :
+    (∀ v : BitVec (n + 1), P v) ↔ (∀ (x : Bool) (v : BitVec n), P (v.cons x)) := by
+  constructor
+  · intro h _ _
+    apply h
+  · intro h v
+    have w : v = (v.setWidth n).cons v.msb := by simp
+    rw [w]
+    apply h
+
+instance instDecidableForallBitVecZero (P : BitVec 0 → Prop) :
+    ∀ [Decidable (P 0#0)], Decidable (∀ v, P v)
+  | .isTrue h => .isTrue fun v => by
+    obtain (rfl : v = 0#0) := (by ext ⟨i, h⟩; cases h)
+    exact h
+  | .isFalse h => .isFalse (fun w => h (w _))
+
+instance instDecidableForallBitVecSucc (P : BitVec (n+1) → Prop) [DecidablePred P]
+    [Decidable (∀ (x : Bool) (v : BitVec n), P (v.cons x))] : Decidable (∀ v, P v) :=
+  decidable_of_iff' (∀ x (v : BitVec n), P (v.cons x)) forall_cons_iff
+
+instance instDecidableExistsBitVecZero (P : BitVec 0 → Prop) [Decidable (P 0#0)] :
+    Decidable (∃ v, P v) :=
+  decidable_of_iff (¬ ∀ v, ¬ P v) Classical.not_forall_not
+
+instance instDecidableExistsBitVecSucc (P : BitVec (n+1) → Prop) [DecidablePred P]
+    [Decidable (∀ (x : Bool) (v : BitVec n), ¬ P (v.cons x))] : Decidable (∃ v, P v) :=
+  decidable_of_iff (¬ ∀ v, ¬ P v) Classical.not_forall_not
+
+/--
+For small numerals this isn't necessary (as typeclass search can use the above two instances),
+but for large numerals this provides a shortcut.
+Note, however, that for large numerals the decision procedure may be very slow,
+and you should use `bv_decide` if possible.
+-/
+instance instDecidableForallBitVec :
+    ∀ (n : Nat) (P : BitVec n → Prop) [DecidablePred P], Decidable (∀ v, P v)
+  | 0, _, _ => inferInstance
+  | n + 1, _, _ =>
+    have := instDecidableForallBitVec n
+    inferInstance
+
+/--
+For small numerals this isn't necessary (as typeclass search can use the above two instances),
+but for large numerals this provides a shortcut.
+Note, however, that for large numerals the decision procedure may be very slow.
+-/
+instance instDecidableExistsBitVec :
+    ∀ (n : Nat) (P : BitVec n → Prop) [DecidablePred P], Decidable (∃ v, P v)
+  | 0, _, _ => inferInstance
+  | n + 1, _, _ =>
+    have := instDecidableExistsBitVec n
+    inferInstance
+
 /-! ### Deprecations -/
 
 set_option linter.missingDocs false

src/Init/Data/List/Lemmas.lean

@@ -938,6 +938,38 @@ def foldrRecOn {motive : β → Sort _} : ∀ (l : List α) (op : α → β →
         x (mem_cons_self x l) :=
   rfl
 
+/--
+We can prove that two folds over the same list are related (by some arbitrary relation)
+if we know that the initial elements are related and the folding function, for each element of the list,
+preserves the relation.
+-/
+theorem foldl_rel {l : List α} {f g : β → α → β} {a b : β} (r : β → β → Prop)
+    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)) :
+    r (l.foldl (fun acc a => f acc a) a) (l.foldl (fun acc a => g acc a) b) := by
+  induction l generalizing a b with
+  | nil => simp_all
+  | cons a l ih =>
+    simp only [foldl_cons]
+    apply ih
+    · simp_all
+    · exact fun a m c c' h => h' _ (by simp_all) _ _ h
+
+/--
+We can prove that two folds over the same list are related (by some arbitrary relation)
+if we know that the initial elements are related and the folding function, for each element of the list,
+preserves the relation.
+-/
+theorem foldr_rel {l : List α} {f g : α → β → β} {a b : β} (r : β → β → Prop)
+    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) :
+    r (l.foldr (fun a acc => f a acc) a) (l.foldr (fun a acc => g a acc) b) := by
+  induction l generalizing a b with
+  | nil => simp_all
+  | cons a l ih =>
+    simp only [foldr_cons]
+    apply h'
+    · simp
+    · exact ih h fun a m c c' h => h' _ (by simp_all) _ _ h
+
 /-! ### getLast -/
 
 theorem getLast_eq_getElem : ∀ (l : List α) (h : l ≠ []),

src/Init/Meta.lean

@@ -7,7 +7,7 @@ Additional goodies for writing macros
 -/
 prelude
 import Init.MetaTypes
-import Init.Data.Array.Basic
+import Init.Data.Array.GetLit
 import Init.Data.Option.BasicAux
 
 namespace Lean

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean

@@ -35,7 +35,7 @@ Reconstruct bit by bit which value expression must have had which `BitVec` value
 expression - pair values.
 -/
 def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Array (Bool × Nat))
-    (aigSize : Nat) (atomsAssignment : Std.HashMap Nat Expr) :
+    (aigSize : Nat) (atomsAssignment : Std.HashMap Nat (Nat × Expr)) :
     Array (Expr × BVExpr.PackedBitVec) := Id.run do
   let mut sparseMap : Std.HashMap Nat (RBMap Nat Bool Ord.compare) := {}
   for (bitVar, cnfVar) in var2Cnf.toArray do
@@ -70,7 +70,7 @@ def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Ar
       if bitValue then
         value := value ||| (1 <<< currentBit)
       currentBit := currentBit + 1
-    let atomExpr := atomsAssignment.get! bitVecVar
+    let atomExpr := atomsAssignment.get! bitVecVar |>.snd
     finalMap := finalMap.push (atomExpr, ⟨BitVec.ofNat currentBit value⟩)
   return finalMap
 
@@ -83,14 +83,14 @@ structure UnsatProver.Result where
   proof : Expr
   lratCert : LratCert
 
-abbrev UnsatProver := ReflectionResult → Std.HashMap Nat Expr → MetaM UnsatProver.Result
+abbrev UnsatProver := ReflectionResult → Std.HashMap Nat (Nat × Expr) → MetaM UnsatProver.Result
 
 /--
 Contains values that will be used to diagnose spurious counter examples.
 -/
 structure DiagnosisInput where
   unusedHypotheses : Std.HashSet FVarId
-  atomsAssignment : Std.HashMap Nat Expr
+  atomsAssignment : Std.HashMap Nat (Nat × Expr)
 
 /--
 The result of a spurious counter example diagnosis.
@@ -104,14 +104,14 @@ abbrev DiagnosisM : Type → Type := ReaderT DiagnosisInput <| StateRefT Diagnos
 namespace DiagnosisM
 
 def run (x : DiagnosisM Unit) (unusedHypotheses : Std.HashSet FVarId)
-    (atomsAssignment : Std.HashMap Nat Expr) : MetaM Diagnosis := do
+    (atomsAssignment : Std.HashMap Nat (Nat × Expr)) : MetaM Diagnosis := do
   let (_, issues) ← ReaderT.run x { unusedHypotheses, atomsAssignment } |>.run {}
   return issues
 
 def unusedHyps : DiagnosisM (Std.HashSet FVarId) := do
   return (← read).unusedHypotheses
 
-def atomsAssignment : DiagnosisM (Std.HashMap Nat Expr) := do
+def atomsAssignment : DiagnosisM (Std.HashMap Nat (Nat × Expr)) := do
   return (← read).atomsAssignment
 
 def addUninterpretedSymbol (e : Expr) : DiagnosisM Unit :=
@@ -131,7 +131,7 @@ Diagnose spurious counter examples, currently this checks:
 - Whether all hypotheses which contain any variable that was bitblasted were included
 -/
 def diagnose : DiagnosisM Unit := do
-  for (_, expr) in ← atomsAssignment do
+  for (_, (_, expr)) in ← atomsAssignment do
     match_expr expr with
     | BitVec.ofBool x =>
       match x with
@@ -158,7 +158,7 @@ def explainers : List (Diagnosis → Option MessageData) :=
   [uninterpretedExplainer, unusedRelevantHypothesesExplainer]
 
 def explainCounterExampleQuality (unusedHypotheses : Std.HashSet FVarId)
-    (atomsAssignment : Std.HashMap Nat Expr) : MetaM MessageData := do
+    (atomsAssignment : Std.HashMap Nat (Nat × Expr)) : MetaM MessageData := do
   let diagnosis ← DiagnosisM.run DiagnosisM.diagnose unusedHypotheses atomsAssignment
   let folder acc explainer := if let some m := explainer diagnosis then acc.push m else acc
   let explanations := explainers.foldl (init := #[]) folder
@@ -172,7 +172,7 @@ def explainCounterExampleQuality (unusedHypotheses : Std.HashSet FVarId)
     return err
 
 def lratBitblaster (cfg : TacticContext) (reflectionResult : ReflectionResult)
-    (atomsAssignment : Std.HashMap Nat Expr) :
+    (atomsAssignment : Std.HashMap Nat (Nat × Expr)) :
     MetaM UnsatProver.Result := do
   let bvExpr := reflectionResult.bvExpr
   let entry ←
@@ -242,7 +242,7 @@ def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :
         reflectBV g
     trace[Meta.Tactic.bv] "Reflected bv logical expression: {reflectionResult.bvExpr}"
 
-    let atomsPairs := (← getThe State).atoms.toList.map (fun (expr, _, ident) => (ident, expr))
+    let atomsPairs := (← getThe State).atoms.toList.map (fun (expr, ⟨width, ident⟩) => (ident, (width, expr)))
     let atomsAssignment := Std.HashMap.ofList atomsPairs
     let ⟨bvExprUnsat, cert⟩ ← unsatProver reflectionResult atomsAssignment
     let proveFalse ← reflectionResult.proveFalse bvExprUnsat

src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean

@@ -141,10 +141,11 @@ This will obtain an `LratCert` if the formula is UNSAT and throw errors otherwis
 def runExternal (cnf : CNF Nat) (solver : System.FilePath) (lratPath : System.FilePath)
     (trimProofs : Bool) (timeout : Nat) (binaryProofs : Bool)
     : MetaM (Except (Array (Bool × Nat)) LratCert) := do
-  IO.FS.withTempFile fun _ cnfPath => do
+  IO.FS.withTempFile fun cnfHandle cnfPath => do
     withTraceNode `sat (fun _ => return "Serializing SAT problem to DIMACS file") do
       -- lazyPure to prevent compiler lifting
-      IO.FS.writeFile cnfPath (← IO.lazyPure (fun _ => cnf.dimacs))
+      cnfHandle.putStr  (← IO.lazyPure (fun _ => cnf.dimacs))
+      cnfHandle.flush
 
     let res ←
       withTraceNode `sat (fun _ => return "Running SAT solver") do

src/Lean/Elab/Tactic/Basic.lean

@@ -49,6 +49,9 @@ instance : Monad TacticM :=
   let i := inferInstanceAs (Monad TacticM);
   { pure := i.pure, bind := i.bind }
 
+instance : Inhabited (TacticM α) where
+  default := fun _ _ => default
+
 def getGoals : TacticM (List MVarId) :=
   return (← get).goals
 

src/Lean/Meta/Instances.lean

@@ -113,8 +113,34 @@ For example:
     (because A B are out-params and are only filled in once we synthesize 2)
 
 (The type of `inst` must not contain mvars.)
+
+Remark: `projInfo?` is `some` if the instance is a projection.
+We need this information because of the heuristic we use to annotate binder
+information in projections. See PR #5376 and issue #5333. Before PR
+#5376, given a class `C` at
+```
+class A (n : Nat) where
+
+instance [A n] : A n.succ where
+
+class B [A 20050] where
+
+class C [A 20000] extends B where
+```
+we would get the following instance
+```
+C.toB [inst : A 20000] [self : @C inst] : @B ...
+```
+After the PR, we have
+```
+C.toB {inst : A 20000} [self : @C inst] : @B ...
+```
+Note the attribute `inst` is now just a regular implicit argument.
+To ensure `computeSynthOrder` works as expected, we should take
+this change into account while processing field `self`.
+This field is the one at position `projInfo?.numParams`.
 -/
-private partial def computeSynthOrder (inst : Expr) : MetaM (Array Nat) :=
+private partial def computeSynthOrder (inst : Expr) (projInfo? : Option ProjectionFunctionInfo) : MetaM (Array Nat) :=
   withReducible do
   let instTy ← inferType inst
 
@@ -151,7 +177,8 @@ private partial def computeSynthOrder (inst : Expr) : MetaM (Array Nat) :=
   let tyOutParams ← getSemiOutParamPositionsOf ty
   let tyArgs := ty.getAppArgs
   for tyArg in tyArgs, i in [:tyArgs.size] do
-    unless tyOutParams.contains i do assignMVarsIn tyArg
+    unless tyOutParams.contains i do
+      assignMVarsIn tyArg
 
   -- Now we successively try to find the next ready subgoal, where all
   -- non-out-params are mvar-free.
@@ -159,7 +186,13 @@ private partial def computeSynthOrder (inst : Expr) : MetaM (Array Nat) :=
   let mut toSynth := List.range argMVars.size |>.filter (argBIs[·]! == .instImplicit) |>.toArray
   while !toSynth.isEmpty do
     let next? ← toSynth.findM? fun i => do
-      forallTelescopeReducing (← instantiateMVars (← inferType argMVars[i]!)) fun _ argTy => do
+      let argTy ← instantiateMVars (← inferType argMVars[i]!)
+      if let some projInfo := projInfo? then
+        if projInfo.numParams == i then
+          -- See comment regarding `projInfo?` at the beginning of this function
+          assignMVarsIn argTy
+          return true
+      forallTelescopeReducing argTy fun _ argTy => do
       let argTy ← whnf argTy
       let argOutParams ← getSemiOutParamPositionsOf argTy
       let argTyArgs := argTy.getAppArgs
@@ -195,7 +228,8 @@ def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : Meta
   let c ← mkConstWithLevelParams declName
   let keys ← mkInstanceKey c
   addGlobalInstance declName attrKind
-  let synthOrder ← computeSynthOrder c
+  let projInfo? ← getProjectionFnInfo? declName
+  let synthOrder ← computeSynthOrder c projInfo?
   instanceExtension.add { keys, val := c, priority := prio, globalName? := declName, attrKind, synthOrder } attrKind
 
 builtin_initialize

src/Lean/Meta/Tactic/Refl.lean

@@ -12,6 +12,9 @@ namespace Lean.Meta
 
 /--
 Close given goal using `Eq.refl`.
+
+See `Lean.MVarId.applyRfl` for the variant that also consults `@[refl]` lemmas, and which
+backs the `rfl` tactic.
 -/
 def _root_.Lean.MVarId.refl (mvarId : MVarId) : MetaM Unit := do
   mvarId.withContext do

src/Lean/Meta/Tactic/Rfl.lean

@@ -50,33 +50,59 @@ open Elab Tactic
 
 /-- `MetaM` version of the `rfl` tactic.
 
-This tactic applies to a goal whose target has the form `x ~ x`,
-where `~` is a reflexive relation other than `=`,
-that is, a relation which has a reflexive lemma tagged with the attribute @[refl].
+This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
+relation, that is, equality or another relation which has a reflexive lemma tagged with the
+attribute [refl].
 -/
-def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := do
-  let .app (.app rel _) _ ← whnfR <|← instantiateMVars <|← goal.getType
-    | throwError "reflexivity lemmas only apply to binary relations, not{
-        indentExpr (← goal.getType)}"
-  if let .app (.const ``Eq [_]) _ := rel then
-    throwError "MVarId.applyRfl does not solve `=` goals. Use `MVarId.refl` instead."
+def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext do
+  -- NB: uses whnfR, we do not want to unfold the relation itself
+  let t ← whnfR <|← instantiateMVars <|← goal.getType
+  if t.getAppNumArgs < 2 then
+    throwError "rfl can only be used on binary relations, not{indentExpr (← goal.getType)}"
+
+  -- Special case HEq here as it has a different argument order.
+  if t.isAppOfArity ``HEq 4 then
+    let gs ← goal.applyConst ``HEq.refl
+    unless gs.isEmpty do
+      throwError MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
+        goalsToMessageData gs}"
+    return
+
+  let rel := t.appFn!.appFn!
+  let lhs := t.appFn!.appArg!
+  let rhs := t.appArg!
+
+  let success ← approxDefEq <| isDefEqGuarded lhs rhs
+  unless success do
+    let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) do
+      let (lhs, rhs) ← addPPExplicitToExposeDiff lhs rhs
+      return m!"The lhs{indentExpr lhs}\nis not definitionally equal to rhs{indentExpr rhs}"
+    throwTacticEx `apply_rfl goal explanation
+
+  if rel.isAppOfArity `Eq 1 then
+    -- The common case is equality: just use `Eq.refl`
+    let us := rel.appFn!.constLevels!
+    let α :=  rel.appArg!
+    goal.assign (mkApp2 (mkConst ``Eq.refl us) α lhs)
   else
+    -- Else search through `@refl` keyed by the relation
     let s ← saveState
     let mut ex? := none
     for lem in ← (reflExt.getState (← getEnv)).getMatch rel reflExt.config do
       try
         let gs ← goal.apply (← mkConstWithFreshMVarLevels lem)
         if gs.isEmpty then return () else
-          logError <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
+          throwError MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
             goalsToMessageData gs}"
       catch e =>
-        ex? := ex? <|> (some (← saveState, e)) -- stash the first failure of `apply`
+        unless ex?.isSome do
+          ex? := some (← saveState, e) -- stash the first failure of `apply`
       s.restore
     if let some (sErr, e) := ex? then
       sErr.restore
       throw e
     else
-      throwError "rfl failed, no lemma with @[refl] applies"
+      throwError "rfl failed, no @[refl] lemma registered for relation{indentExpr rel}"
 
 /-- Helper theorem for `Lean.MVarId.liftReflToEq`. -/
 private theorem rel_of_eq_and_refl {α : Sort _} {R : α → α → Prop}

src/Lean/ProjFns.lean

@@ -21,7 +21,7 @@ structure ProjectionFunctionInfo where
   i : Nat
   /-- `true` if the structure is a class. -/
   fromClass : Bool
-  deriving Inhabited
+  deriving Inhabited, Repr
 
 @[export lean_mk_projection_info]
 def mkProjectionInfoEx (ctorName : Name) (numParams : Nat) (i : Nat) (fromClass : Bool) : ProjectionFunctionInfo :=

src/Std/Data/DHashMap/Basic.lean

@@ -186,6 +186,15 @@ section Unverified
     (init : δ) (b : DHashMap α β) : δ :=
   b.1.fold f init
 
+/-- Partition a hashset into two hashsets based on a predicate. -/
+@[inline] def partition (f : (a : α) → β a → Bool)
+    (m : DHashMap α β) : DHashMap α β × DHashMap α β :=
+  m.fold (init := (∅, ∅)) fun ⟨l, r⟩  a b =>
+    if f a b then
+      (l.insert a b, r)
+    else
+      (l, r.insert a b)
+
 @[inline, inherit_doc Raw.forM] def forM (f : (a : α) → β a → m PUnit)
     (b : DHashMap α β) : m PUnit :=
   b.1.forM f
@@ -260,6 +269,10 @@ instance [BEq α] [Hashable α] : ForIn m (DHashMap α β) ((a : α) × β a) wh
     DHashMap α (fun _ => Unit) :=
   Const.insertManyUnit ∅ l
 
+@[inline, inherit_doc Raw.Const.unitOfArray] def Const.unitOfArray [BEq α] [Hashable α] (l : Array α) :
+    DHashMap α (fun _ => Unit) :=
+  Const.insertManyUnit ∅ l
+
 @[inherit_doc Raw.Internal.numBuckets] def Internal.numBuckets
     (m : DHashMap α β) : Nat :=
   Raw.Internal.numBuckets m.1

src/Std/Data/DHashMap/Raw.lean

@@ -411,6 +411,14 @@ This is mainly useful to implement `HashSet.ofList`, so if you are considering u
     Raw α (fun _ => Unit) :=
   Const.insertManyUnit ∅ l
 
+/-- Creates a hash map from an array of keys, associating the value `()` with each key.
+
+This is mainly useful to implement `HashSet.ofArray`, so if you are considering using this,
+`HashSet` or `HashSet.Raw` might be a better fit for you. -/
+@[inline] def Const.unitOfArray [BEq α] [Hashable α] (l : Array α) :
+    Raw α (fun _ => Unit) :=
+  Const.insertManyUnit ∅ l
+
 /--
 Returns the number of buckets in the internal representation of the hash map. This function may be
 useful for things like monitoring system health, but it should be considered an internal

src/Std/Data/HashMap/Basic.lean

@@ -190,6 +190,11 @@ section Unverified
     (m : HashMap α β) : HashMap α β :=
   ⟨m.inner.filter f⟩
 
+@[inline, inherit_doc DHashMap.partition] def partition (f : α → β → Bool)
+    (m : HashMap α β) : HashMap α β × HashMap α β :=
+  let ⟨l, r⟩ := m.inner.partition f
+  ⟨⟨l⟩, ⟨r⟩⟩
+
 @[inline, inherit_doc DHashMap.foldM] def foldM {m : Type w → Type w}
     [Monad m] {γ : Type w} (f : γ → α → β → m γ) (init : γ) (b : HashMap α β) : m γ :=
   b.inner.foldM f init
@@ -250,6 +255,10 @@ instance [BEq α] [Hashable α] {m : Type w → Type w} : ForIn m (HashMap α β
     HashMap α Unit :=
   ⟨DHashMap.Const.unitOfList l⟩
 
+@[inline, inherit_doc DHashMap.Const.unitOfArray] def unitOfArray [BEq α] [Hashable α] (l : Array α) :
+    HashMap α Unit :=
+  ⟨DHashMap.Const.unitOfArray l⟩
+
 @[inline, inherit_doc DHashMap.Internal.numBuckets] def Internal.numBuckets
     (m : HashMap α β) : Nat :=
   DHashMap.Internal.numBuckets m.inner

src/Std/Data/HashSet/Basic.lean

@@ -158,6 +158,11 @@ section Unverified
 @[inline] def filter (f : α → Bool) (m : HashSet α) : HashSet α :=
   ⟨m.inner.filter fun a _ => f a⟩
 
+/-- Partition a hashset into two hashsets based on a predicate. -/
+@[inline] def partition (f : α → Bool) (m : HashSet α) : HashSet α × HashSet α :=
+  let ⟨l, r⟩ := m.inner.partition fun a _ => f a
+  ⟨⟨l⟩, ⟨r⟩⟩
+
 /--
 Monadically computes a value by folding the given function over the elements in the hash set in some
 order.
@@ -212,6 +217,14 @@ in the collection will be present in the returned hash set.
 @[inline] def ofList [BEq α] [Hashable α] (l : List α) : HashSet α :=
   ⟨HashMap.unitOfList l⟩
 
+/--
+Creates a hash set from an array of elements. Note that unlike repeatedly calling `insert`, if the
+collection contains multiple elements that are equal (with regard to `==`), then the last element
+in the collection will be present in the returned hash set.
+-/
+@[inline] def ofArray [BEq α] [Hashable α] (l : Array α) : HashSet α :=
+  ⟨HashMap.unitOfArray l⟩
+
 /-- Computes the union of the given hash sets. -/
 @[inline] def union [BEq α] [Hashable α] (m₁ m₂ : HashSet α) : HashSet α :=
   m₂.fold (init := m₁) fun acc x => acc.insert x

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean

@@ -142,8 +142,8 @@ def toString : BVUnOp → String
   | not => "~"
   | shiftLeftConst n => s!"<< {n}"
   | shiftRightConst n => s!">> {n}"
-  | rotateLeft n => s! "rotL {n}"
-  | rotateRight n => s! "rotR {n}"
+  | rotateLeft n => s!"rotL {n}"
+  | rotateRight n => s!"rotR {n}"
   | arithShiftRightConst n => s!">>a {n}"
 
 instance : ToString BVUnOp := ⟨toString⟩
@@ -238,7 +238,7 @@ def toString : BVExpr w → String
   | .var idx => s!"var{idx}"
   | .const val => ToString.toString val
   | .zeroExtend v expr => s!"(zext {v} {expr.toString})"
-  | .extract hi lo expr => s!"{expr.toString}[{hi}:{lo}]"
+  | .extract start len expr => s!"{expr.toString}[{start}, {len}]"
   | .bin lhs op rhs => s!"({lhs.toString} {op.toString} {rhs.toString})"
   | .un op operand => s!"({op.toString} {toString operand})"
   | .append lhs rhs => s!"({toString lhs} ++ {toString rhs})"

src/library/constructions/projection.cpp

@@ -63,6 +63,8 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
             // 1. The original binder before `mk_outparam_args_implicit` is not an instance implicit.
             // 2. It is not originally an outparam. Outparams must be implicit.
             bi = mk_binder_info();
+        } else if (is_inst_implicit(bi_orig) && inst_implicit) {
+            bi = mk_implicit_binder_info();
         }
         expr param = lctx.mk_local_decl(ngen, binding_name(cnstr_type), type, bi);
         cnstr_type = instantiate(binding_body(cnstr_type), param);

tests/lean/run/5333.lean

@@ -0,0 +1,20 @@
+class A (n : Nat) where
+
+instance [A n] : A n.succ where
+
+class B [A 20050] where
+
+set_option trace.Meta.debug true
+
+class C [A 20000] extends B where
+
+#check C.toB
+
+instance : A 20050 where
+
+class D where
+
+instance inst1 : D where
+instance inst2 [B] : D where
+
+#synth D

tests/lean/run/bitvec.lean

@@ -75,17 +75,17 @@ open BitVec
 
 -- get/extract
 
-#guard !getMsb 0b0101#4 0
-#guard getMsb 0b0101#4 1
-#guard !getMsb 0b0101#4 2
-#guard getMsb 0b0101#4 3
-#guard !getMsb 0b1111#4 4
+#guard !getMsbD 0b0101#4 0
+#guard getMsbD 0b0101#4 1
+#guard !getMsbD 0b0101#4 2
+#guard getMsbD 0b0101#4 3
+#guard !getMsbD 0b1111#4 4
 
-#guard getLsb 0b0101#4 0
-#guard !getLsb 0b0101#4 1
-#guard getLsb 0b0101#4 2
-#guard !getLsb 0b0101#4 3
-#guard !getLsb 0b1111#4 4
+#guard getLsbD 0b0101#4 0
+#guard !getLsbD 0b0101#4 1
+#guard getLsbD 0b0101#4 2
+#guard !getLsbD 0b0101#4 3
+#guard !getLsbD 0b1111#4 4
 
 #guard extractLsb 3 0 0x1234#16 = 4
 #guard extractLsb 7 4 0x1234#16 = 3
@@ -114,3 +114,10 @@ def testMatch8 (i : BitVec 32) :=
 
 example (n w : Nat) (p : n < 2^w) : { toFin := { val := n, isLt := p } : BitVec w} = .ofNat w n := by
   simp only [ofFin_eq_ofNat]
+
+-- Decidable quantifiers
+
+example : ∀ v : BitVec 2, (v[1] && v[0]) = (v[0] && v[1]) := by decide
+
+ -- `bv_decide` doesn't yet do existentials:
+example : ∃ x y : BitVec 5, x ^^^ y = allOnes 5 := by decide

tests/lean/run/rflApplyFoApprox.lean

@@ -0,0 +1,15 @@
+
+opaque f : Nat → Nat
+-- A rewrite with a free variable on the RHS
+
+opaque P : Nat → (Nat → Nat) → Prop
+opaque Q : Nat → Prop
+opaque foo (g : Nat → Nat) (x : Nat) : P x f ↔ Q (g x) := sorry
+
+example : P x f ↔ Q (x + 10) := by
+  rewrite [foo]
+  -- we have an mvar now
+  with_reducible rfl -- should should instantiate it with the lambda on the RHS and close the goal
+  -- same as
+  -- with_reducible (apply (Iff.refl _))
+  -- NB: apply, not exact! Different defEq flags.

tests/lean/run/rflTacticErrors.lean

@@ -0,0 +1,445 @@
+
+/-!
+This file tests the `rfl` tactic:
+ * Extensibility
+ * Error messages
+ * Effect of `with_reducible`
+-/
+
+-- First, let's see what `rfl` does:
+
+/--
+error: The rfl tactic failed. Possible reasons:
+- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
+- The arguments of the relation are not equal.
+Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
+`exact HEq.rfl` etc.
+⊢ false = true
+-/
+#guard_msgs in
+example : false = true := by rfl
+
+-- Now to `apply_rfl`.
+
+-- A plain reflexive predicate
+inductive P : α → α → Prop where | refl : P a a
+attribute [refl] P.refl
+
+-- Plain error
+
+/--
+error: tactic 'apply_rfl' failed, The lhs
+  42
+is not definitionally equal to rhs
+  23
+⊢ P 42 23
+-/
+#guard_msgs in
+example : P 42 23 := by apply_rfl
+
+-- Revealing implicit arguments
+
+opaque withImplicitNat {n : Nat} : Nat
+
+/--
+error: tactic 'apply_rfl' failed, The lhs
+  @withImplicitNat 42
+is not definitionally equal to rhs
+  @withImplicitNat 23
+⊢ P withImplicitNat withImplicitNat
+-/
+#guard_msgs in
+example : P (@withImplicitNat 42) (@withImplicitNat 23) := by apply_rfl
+
+
+-- Exhaustive testing of various combinations:
+
+-- In addition to Eq, HEq and Iff  we test four relations:
+
+
+-- Defeq to relation `P` at reducible transparency
+abbrev Q : α → α → Prop := P
+
+-- Defeq to relation `P` at default transparency
+def Q' : α → α → Prop := P
+
+-- No refl attribute
+inductive R : α → α → Prop where | refl : R a a
+
+
+/-
+Now we systematically test all relations with
+* syntactic equal arguments
+* reducibly equal arguments
+* semireducibly equal arguments
+* nonequal arguments
+
+and all using `apply_rfl` and `with_reducible apply_rfl`
+-/
+
+
+-- Syntactic equal
+
+example : true = true   := by apply_rfl
+example : HEq true true := by apply_rfl
+example : True ↔ True   := by apply_rfl
+example : P true true   := by apply_rfl
+example : Q true true   := by apply_rfl
+/--
+error: rfl failed, no @[refl] lemma registered for relation
+  Q'
+-/
+#guard_msgs in example : Q' true true  := by apply_rfl -- Error
+/--
+error: rfl failed, no @[refl] lemma registered for relation
+  R
+-/
+#guard_msgs in example : R true true   := by apply_rfl -- Error
+
+example : true = true   := by with_reducible apply_rfl
+example : HEq true true := by with_reducible apply_rfl
+example : True ↔ True   := by with_reducible apply_rfl
+example : P true true   := by with_reducible apply_rfl
+example : Q true true   := by with_reducible apply_rfl
+/--
+error: rfl failed, no @[refl] lemma registered for relation
+  Q'
+-/
+#guard_msgs in
+example : Q' true true  := by with_reducible apply_rfl -- Error
+/--
+error: rfl failed, no @[refl] lemma registered for relation
+  R
+-/
+#guard_msgs in
+example : R true true   := by with_reducible apply_rfl -- Error
+
+-- Reducibly equal
+
+abbrev true' := true
+abbrev True' := True
+
+example : true' = true   := by apply_rfl
+example : HEq true' true := by apply_rfl
+example : True' ↔ True   := by apply_rfl
+example : P true' true   := by apply_rfl
+example : Q true' true   := by apply_rfl
+/--
+error: rfl failed, no @[refl] lemma registered for relation
+  Q'
+-/
+#guard_msgs in
+example : Q' true' true  := by apply_rfl -- Error
+/--
+error: rfl failed, no @[refl] lemma registered for relation
+  R
+-/
+#guard_msgs in
+example : R true' true   := by apply_rfl -- Error
+
+example : true' = true   := by with_reducible apply_rfl
+example : HEq true' true := by with_reducible apply_rfl
+example : True' ↔ True   := by with_reducible apply_rfl
+example : P true' true   := by with_reducible apply_rfl
+example : Q true' true   := by with_reducible apply_rfl -- NB: No error, Q and true' reducible
+/--
+error: rfl failed, no @[refl] lemma registered for relation
+  Q'
+-/
+#guard_msgs in
+example : Q' true' true  := by with_reducible apply_rfl -- Error
+/--
+error: rfl failed, no @[refl] lemma registered for relation
+  R
+-/
+#guard_msgs in
+example : R true' true   := by with_reducible apply_rfl -- Error
+
+-- Equal at default transparency only
+
+def true'' := true
+def True'' := True
+
+example : true'' = true   := by apply_rfl
+example : HEq true'' true := by apply_rfl
+example : True'' ↔ True   := by apply_rfl
+example : P true'' true   := by apply_rfl
+example : Q true'' true   := by apply_rfl
+/--
+error: rfl failed, no @[refl] lemma registered for relation
+  Q'
+-/
+#guard_msgs in
+example : Q' true'' true  := by apply_rfl -- Error
+/--
+error: rfl failed, no @[refl] lemma registered for relation
+  R
+-/
+#guard_msgs in
+example : R true'' true   := by apply_rfl -- Error
+
+/--
+error: tactic 'apply_rfl' failed, The lhs
+  true''
+is not definitionally equal to rhs
+  true
+⊢ true'' = true
+-/
+#guard_msgs in
+example : true'' = true   := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'apply' failed, failed to unify
+  @HEq ?α ?a ?α ?a
+with
+  @HEq Bool true'' Bool true
+⊢ HEq true'' true
+-/
+#guard_msgs in
+example : HEq true'' true := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'apply_rfl' failed, The lhs
+  True''
+is not definitionally equal to rhs
+  True
+⊢ True'' ↔ True
+-/
+#guard_msgs in
+example : True'' ↔ True   := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'apply_rfl' failed, The lhs
+  true''
+is not definitionally equal to rhs
+  true
+⊢ P true'' true
+-/
+#guard_msgs in
+example : P true'' true   := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'apply_rfl' failed, The lhs
+  true''
+is not definitionally equal to rhs
+  true
+⊢ Q true'' true
+-/
+#guard_msgs in
+example : Q true'' true   := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'apply_rfl' failed, The lhs
+  true''
+is not definitionally equal to rhs
+  true
+⊢ Q' true'' true
+-/
+#guard_msgs in
+example : Q' true'' true  := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'apply_rfl' failed, The lhs
+  true''
+is not definitionally equal to rhs
+  true
+⊢ R true'' true
+-/
+#guard_msgs in
+example : R true'' true   := by with_reducible apply_rfl -- Error
+
+-- Unequal
+/--
+error: tactic 'apply_rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ false = true
+-/
+#guard_msgs in
+example : false = true   := by apply_rfl -- Error
+/--
+error: tactic 'apply' failed, failed to unify
+  HEq ?a ?a
+with
+  HEq false true
+⊢ HEq false true
+-/
+#guard_msgs in
+example : HEq false true := by apply_rfl -- Error
+/--
+error: tactic 'apply_rfl' failed, The lhs
+  False
+is not definitionally equal to rhs
+  True
+⊢ False ↔ True
+-/
+#guard_msgs in
+example : False ↔ True   := by apply_rfl -- Error
+/--
+error: tactic 'apply_rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ P false true
+-/
+#guard_msgs in
+example : P false true   := by apply_rfl -- Error
+/--
+error: tactic 'apply_rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ Q false true
+-/
+#guard_msgs in
+example : Q false true   := by apply_rfl -- Error
+/--
+error: tactic 'apply_rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ Q' false true
+-/
+#guard_msgs in
+example : Q' false true  := by apply_rfl -- Error
+/--
+error: tactic 'apply_rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ R false true
+-/
+#guard_msgs in
+example : R false true   := by apply_rfl -- Error
+
+/--
+error: tactic 'apply_rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ false = true
+-/
+#guard_msgs in
+example : false = true   := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'apply' failed, failed to unify
+  HEq ?a ?a
+with
+  HEq false true
+⊢ HEq false true
+-/
+#guard_msgs in
+example : HEq false true := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'apply_rfl' failed, The lhs
+  False
+is not definitionally equal to rhs
+  True
+⊢ False ↔ True
+-/
+#guard_msgs in
+example : False ↔ True   := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'apply_rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ P false true
+-/
+#guard_msgs in
+example : P false true   := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'apply_rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ Q false true
+-/
+#guard_msgs in
+example : Q false true   := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'apply_rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ Q' false true
+-/
+#guard_msgs in
+example : Q' false true  := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'apply_rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ R false true
+-/
+#guard_msgs in
+example : R false true   := by with_reducible apply_rfl -- Error
+
+-- Inheterogeneous unequal
+
+/--
+error: tactic 'apply' failed, failed to unify
+  HEq ?a ?a
+with
+  HEq true 1
+⊢ HEq true 1
+-/
+#guard_msgs in
+example : HEq true 1 := by apply_rfl -- Error
+/--
+error: tactic 'apply' failed, failed to unify
+  HEq ?a ?a
+with
+  HEq true 1
+⊢ HEq true 1
+-/
+#guard_msgs in
+example : HEq true 1 := by with_reducible apply_rfl -- Error
+
+-- Rfl lemma with side condition:
+-- Error message should show left-over goal
+
+inductive S : Bool → Bool → Prop where | refl : a = true → S a a
+attribute [refl] S.refl
+/--
+error: tactic 'apply_rfl' failed, The lhs
+  true
+is not definitionally equal to rhs
+  false
+⊢ S true false
+-/
+#guard_msgs in
+example : S true false  := by apply_rfl -- Error
+/--
+error: tactic 'apply_rfl' failed, The lhs
+  true
+is not definitionally equal to rhs
+  false
+⊢ S true false
+-/
+#guard_msgs in
+example : S true false  := by with_reducible apply_rfl -- Error
+/--
+error: unsolved goals
+case a
+⊢ true = true
+-/
+#guard_msgs in
+example : S true true   := by apply_rfl -- Error (left-over goal)
+/--
+error: unsolved goals
+case a
+⊢ true = true
+-/
+#guard_msgs in
+example : S true true   := by with_reducible apply_rfl -- Error (left-over goal)
+/--
+error: unsolved goals
+case a
+⊢ false = true
+-/
+#guard_msgs in
+example : S false false := by apply_rfl -- Error (left-over goal)
+/--
+error: unsolved goals
+case a
+⊢ false = true
+-/
+#guard_msgs in
+example : S false false := by with_reducible apply_rfl -- Error (left-over goal)

tests/lean/run/synthOrderRegression.lean

@@ -0,0 +1,19 @@
+-- Artificial example for exposing a regression introduced while working on PR #5376
+-- fix: modify projection instance binder info
+
+class Foo (α : Type) [Add α] where
+   bla : [Mul α] → BEq α
+
+attribute [instance] Foo.bla
+
+inductive Boo where
+  | unit
+
+instance : Add Boo where
+  add _ _ := .unit
+
+instance : Mul Boo where
+  mul _ _ := .unit
+
+def f [Foo Boo] (a b : Boo) : Bool :=
+  a == b

tests/lean/synthorder.lean.expected.out

@@ -11,13 +11,10 @@ all remaining arguments have metavariables:
       Foo A B
       Foo B C
 [Meta.synthOrder] synthesizing the arguments of @instFooOption in the order []:
-[Meta.synthOrder] synthesizing the arguments of @TwoHalf.toTwo in the order [1, 2]:
-      One α
+[Meta.synthOrder] synthesizing the arguments of @TwoHalf.toTwo in the order [2]:
       TwoHalf α
-[Meta.synthOrder] synthesizing the arguments of @Four.toThree in the order [4, 2, 3]:
+[Meta.synthOrder] synthesizing the arguments of @Four.toThree in the order [4]:
       Four α β
-      One β
-      TwoHalf β
 [Meta.synthOrder] synthesizing the arguments of @instFourOfThree in the order [4, 2, 3]:
       Three α β
       One β