feat: BitVec simprocs

closes #2670

.github/workflows/nix-ci.yml

@@ -71,12 +71,6 @@ jobs:
         run: |
           sudo chown -R root:nixbld /nix/var/cache
           sudo chmod -R 770 /nix/var/cache
-      - name: Install Cachix
-        uses: cachix/cachix-action@v12
-        with:
-          name: lean4
-          authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
-          skipPush: true  # we push specific outputs only
       - name: Build
         run: |
           nix build $NIX_BUILD_ARGS .#cacheRoots -o push-build
@@ -98,9 +92,6 @@ jobs:
           # gmplib.org consistently times out from GH actions
           # the GitHub token is to avoid rate limiting
           args: --base './dist' --no-progress --github-token ${{ secrets.GITHUB_TOKEN }} --exclude 'gmplib.org' './dist/**/*.html'
-      - name: Push to Cachix
-        run: |
-          [ -z "${{ secrets.CACHIX_AUTH_TOKEN }}" ] || cachix push -j4 lean4 ./push-* || true
       - name: Rebuild Nix Store Cache
         run: |
           rm -rf nix-store-cache || true

.github/workflows/update-stage0.yml

@@ -40,18 +40,32 @@ jobs:
       run: |
           git config --global user.name "Lean stage0 autoupdater"
           git config --global user.email "<>"
-    - if: env.should_update_stage0 == 'yes'
-      uses: DeterminateSystems/nix-installer-action@main
     # Would be nice, but does not work yet:
     # https://github.com/DeterminateSystems/magic-nix-cache/issues/39
     # This action does not run that often and building runs in a few minutes, so ok for now
     #- if: env.should_update_stage0 == 'yes'
     #  uses: DeterminateSystems/magic-nix-cache-action@v2
     - if: env.should_update_stage0 == 'yes'
-      name: Install Cachix
-      uses: cachix/cachix-action@v12
+      name: Restore Build Cache
+      uses: actions/cache/restore@v3
       with:
-        name: lean4
+        path: nix-store-cache
+        key: Nix Linux-nix-store-cache-${{ github.sha }}
+        # fall back to (latest) previous cache
+        restore-keys: |
+          Nix Linux-nix-store-cache
+    - if: env.should_update_stage0 == 'yes'
+      name: Further Set Up Nix Cache
+      shell: bash -euxo pipefail {0}
+      run: |
+        # Nix seems to mutate the cache, so make a copy
+        cp -r nix-store-cache nix-store-cache-copy || true
+    - if: env.should_update_stage0 == 'yes'
+      name: Install Nix
+      uses: DeterminateSystems/nix-installer-action@main
+      with:
+        extra-conf: |
+          substituters = file://${{ github.workspace }}/nix-store-cache-copy?priority=10&trusted=true https://cache.nixos.org  
     - if: env.should_update_stage0 == 'yes'
       run: nix run .#update-stage0-commit
     - if: env.should_update_stage0 == 'yes'

CODEOWNERS

@@ -6,7 +6,6 @@
 
 /.github/ @Kha @semorrison
 /RELEASES.md @semorrison
-/src/ @leodemoura @Kha
 /src/Init/IO.lean @joehendrix
 /src/kernel/ @leodemoura
 /src/lake/ @tydeu

RELEASES.md

@@ -18,6 +18,74 @@ v4.7.0 (development in progress)
 
 * `pp.proofs.withType` is now set to false by default to reduce noise in the info view.
 
+* New `simp` (and `dsimp`) configuration option: `zetaDelta`. It is `false` by default.
+  The `zeta` option is still `true` by default, but their meaning has changed.
+  - When `zeta := true`, `simp` and `dsimp` reduce terms of the form
+    `let x := val; e[x]` into `e[val]`.
+  - When `zetaDelta := true`, `simp` and `dsimp` will expand let-variables in
+    the context. For example, suppose the context contains `x := val`. Then,
+    any occurrence of `x` is replaced with `val`.
+
+  See issue [#2682](https://github.com/leanprover/lean4/pull/2682) for additional details. Here are some examples:
+  ```
+  example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
+    intro x
+    simp
+    /-
+    New goal:
+    h : z = 9; x := 5 |- x + 4 = z
+    -/
+    rw [h]
+
+  example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
+    intro x
+    -- Using both `zeta` and `zetaDelta`.
+    simp (config := { zetaDelta := true })
+    /-
+    New goal:
+    h : z = 9; x := 5 |- 9 = z
+    -/
+    rw [h]
+
+  example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
+    intro x
+    simp [x] -- asks `simp` to unfold `x`
+    /-
+    New goal:
+    h : z = 9; x := 5 |- 9 = z
+    -/
+    rw [h]
+
+  example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
+    intro x
+    simp (config := { zetaDelta := true, zeta := false })
+    /-
+    New goal:
+    h : z = 9; x := 5 |- let y := 4; 5 + y = z
+    -/
+    rw [h]
+  ```
+
+* When adding new local theorems to `simp`, the system assumes that the function application arguments
+  have been annotated with `no_index`. This modification, which addresses issue [#2670](https://github.com/leanprover/lean4/issues/2670),
+  restores the Lean 3 behavior that users expect. With this modification, the following examples are now operational:
+  ```
+  example {α β : Type} {f : α × β → β → β} (h : ∀ p : α × β, f p p.2 = p.2)
+    (a : α) (b : β) : f (a, b) b = b := by
+    simp [h]
+
+  example {α β : Type} {f : α × β → β → β}
+    (a : α) (b : β) (h : f (a,b) (a,b).2 = (a,b).2) : f (a, b) b = b := by
+    simp [h]
+  ```
+  In both cases, `h` is applicable because `simp` does not index f-arguments anymore when adding `h` to the `simp`-set.
+  It's important to note, however, that global theorems continue to be indexed in the usual manner.
+
+Breaking changes:
+* `Lean.withTraceNode` and variants got a stronger `MonadAlwaysExcept` assumption to
+  fix trace trees not being built on elaboration runtime exceptions. Instances for most elaboration
+  monads built on `EIO Exception` should be synthesized automatically.
+
 v4.6.0
 ---------
 

src/Init.lean

@@ -32,3 +32,4 @@ import Init.Simproc
 import Init.SizeOfLemmas
 import Init.BinderPredicates
 import Init.Ext
+import Init.Omega

src/Init/Conv.lean

@@ -54,6 +54,10 @@ syntax (name := lhs) "lhs" : conv
 (In general, for an `n`-ary operator, it traverses into the last argument.) -/
 syntax (name := rhs) "rhs" : conv
 
+/-- Traverses into the function of a (unary) function application.
+For example, `| f a b` turns into `| f a`. (Use `arg 0` to traverse into `f`.)  -/
+syntax (name := «fun») "fun" : conv
+
 /-- Reduces the target to Weak Head Normal Form. This reduces definitions
 in "head position" until a constructor is exposed. For example, `List.map f [a, b, c]`
 weak head normalizes to `f a :: List.map f [b, c]`. -/
@@ -74,7 +78,8 @@ syntax (name := congr) "congr" : conv
 * `arg i` traverses into the `i`'th argument of the target. For example if the
   target is `f a b c d` then `arg 1` traverses to `a` and `arg 3` traverses to `c`.
 * `arg @i` is the same as `arg i` but it counts all arguments instead of just the
-  explicit arguments. -/
+  explicit arguments.
+* `arg 0` traverses into the function. If the target is `f a b c d`, `arg 0` traverses into `f`. -/
 syntax (name := arg) "arg " "@"? num : conv
 
 /-- `ext x` traverses into a binder (a `fun x => e` or `∀ x, e` expression)

src/Init/Data.lean

@@ -6,6 +6,8 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Basic
 import Init.Data.Nat
+import Init.Data.Bool
+import Init.Data.BitVec
 import Init.Data.Cast
 import Init.Data.Char
 import Init.Data.String

src/Init/Data/Array/Lemmas.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 prelude
-import Init.Data.Nat
+import Init.Data.Nat.MinMax
 import Init.Data.List.Lemmas
 import Init.Data.Fin.Basic
 import Init.Data.Array.Mem

src/Init/Data/BitVec.lean

@@ -0,0 +1,5 @@
+prelude
+import Init.Data.BitVec.Basic
+import Init.Data.BitVec.Bitblast
+import Init.Data.BitVec.Folds
+import Init.Data.BitVec.Lemmas

src/Init/Data/BitVec/Basic.lean

@@ -0,0 +1,535 @@
+/-
+Copyright (c) 2022 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex Keizer
+-/
+prelude
+import Init.Data.Fin.Basic
+import Init.Data.Nat.Bitwise.Lemmas
+import Init.Data.Nat.Power2
+
+namespace Std
+
+/-!
+We define bitvectors. We choose the `Fin` representation over others for its relative efficiency
+(Lean has special support for `Nat`), alignment with `UIntXY` types which are also represented
+with `Fin`, and the fact that bitwise operations on `Fin` are already defined. Some other possible
+representations are `List Bool`, `{ l : List Bool // l.length = w }`, `Fin w → Bool`.
+
+We define many of the bitvector operations from the
+[`QF_BV` logic](https://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV).
+of SMT-LIBv2.
+-/
+
+/--
+A bitvector of the specified width. This is represented as the underlying `Nat` number
+in both the runtime and the kernel, inheriting all the special support for `Nat`.
+-/
+structure BitVec (w : Nat) where
+  /-- Construct a `BitVec w` from a number less than `2^w`.
+  O(1), because we use `Fin` as the internal representation of a bitvector. -/
+  ofFin ::
+  /-- Interpret a bitvector as a number less than `2^w`.
+  O(1), because we use `Fin` as the internal representation of a bitvector. -/
+  toFin : Fin (2^w)
+  deriving DecidableEq
+
+namespace BitVec
+
+/-- `cast eq i` embeds `i` into an equal `BitVec` type. -/
+@[inline] def cast (eq : n = m) (i : BitVec n) : BitVec m :=
+  .ofFin (Fin.cast (congrArg _ eq) i.toFin)
+
+/-- The `BitVec` with value `i mod 2^n`. Treated as an operation on bitvectors,
+this is truncation of the high bits when downcasting and zero-extension when upcasting. -/
+protected def ofNat (n : Nat) (i : Nat) : BitVec n where
+  toFin := Fin.ofNat' i (Nat.two_pow_pos n)
+
+instance : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩
+
+/-- Given a bitvector `a`, return the underlying `Nat`. This is O(1) because `BitVec` is a
+(zero-cost) wrapper around a `Nat`. -/
+protected def toNat (a : BitVec n) : Nat := a.toFin.val
+
+/-- Return the bound in terms of toNat. -/
+theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
+
+/-- Return the `i`-th least significant bit or `false` if `i ≥ w`. -/
+@[inline] def getLsb (x : BitVec w) (i : Nat) : Bool := x.toNat.testBit i
+
+/-- Return the `i`-th most significant bit or `false` if `i ≥ w`. -/
+@[inline] def getMsb (x : BitVec w) (i : Nat) : Bool := i < w && getLsb x (w-1-i)
+
+/-- Return most-significant bit in bitvector. -/
+@[inline] protected def msb (a : BitVec n) : Bool := getMsb a 0
+
+/-- Interpret the bitvector as an integer stored in two's complement form. -/
+protected def toInt (a : BitVec n) : Int :=
+  if a.msb then Int.ofNat a.toNat - Int.ofNat (2^n) else a.toNat
+
+/-- Return a bitvector `0` of size `n`. This is the bitvector with all zero bits. -/
+protected def zero (n : Nat) : BitVec n := ⟨0, Nat.two_pow_pos n⟩
+
+instance : Inhabited (BitVec n) where default := .zero n
+
+instance instOfNat : OfNat (BitVec n) i where ofNat := .ofNat n i
+
+/-- Notation for bit vector literals. `i#n` is a shorthand for `BitVec.ofNat n i`. -/
+scoped syntax:max term:max noWs "#" noWs term:max : term
+macro_rules | `($i#$n) => `(BitVec.ofNat $n $i)
+
+/- Support for `i#n` notation in patterns.  -/
+attribute [match_pattern] BitVec.ofNat
+
+/-- Unexpander for bit vector literals. -/
+@[app_unexpander BitVec.ofNat] def unexpandBitVecOfNat : Lean.PrettyPrinter.Unexpander
+  | `($(_) $n $i) => `($i#$n)
+  | _ => throw ()
+
+/-- Convert bitvector into a fixed-width hex number. -/
+protected def toHex {n : Nat} (x : BitVec n) : String :=
+  let s := (Nat.toDigits 16 x.toNat).asString
+  let t := (List.replicate ((n+3) / 4 - s.length) '0').asString
+  t ++ s
+
+instance : Repr (BitVec n) where reprPrec a _ := "0x" ++ (a.toHex : Format) ++ "#" ++ repr n
+
+instance : ToString (BitVec n) where toString a := toString (repr a)
+
+/-- Theorem for normalizing the bit vector literal representation. -/
+-- TODO: This needs more usage data to assess which direction the simp should go.
+@[simp] theorem ofNat_eq_ofNat : @OfNat.ofNat (BitVec n) i _ = BitVec.ofNat n i := rfl
+@[simp] theorem natCast_eq_ofNat : Nat.cast x = x#w := rfl
+
+/--
+Addition for bit vectors. This can be interpreted as either signed or unsigned addition
+modulo `2^n`.
+
+SMT-Lib name: `bvadd`.
+-/
+protected def add (x y : BitVec n) : BitVec n where toFin := x.toFin + y.toFin
+instance : Add (BitVec n) := ⟨BitVec.add⟩
+
+/--
+Subtraction for bit vectors. This can be interpreted as either signed or unsigned subtraction
+modulo `2^n`.
+-/
+protected def sub (x y : BitVec n) : BitVec n where toFin := x.toFin - y.toFin
+instance : Sub (BitVec n) := ⟨BitVec.sub⟩
+
+/--
+Negation for bit vectors. This can be interpreted as either signed or unsigned negation
+modulo `2^n`.
+
+SMT-Lib name: `bvneg`.
+-/
+protected def neg (x : BitVec n) : BitVec n := .sub 0 x
+instance : Neg (BitVec n) := ⟨.neg⟩
+
+/-- Bit vector of size `n` where all bits are `1`s -/
+def allOnes (n : Nat) : BitVec n := -1
+
+/--
+Return the absolute value of a signed bitvector.
+-/
+protected def abs (s : BitVec n) : BitVec n := if s.msb then .neg s else s
+
+/--
+Multiplication for bit vectors. This can be interpreted as either signed or unsigned negation
+modulo `2^n`.
+
+SMT-Lib name: `bvmul`.
+-/
+protected def mul (x y : BitVec n) : BitVec n := ofFin <| x.toFin * y.toFin
+instance : Mul (BitVec n) := ⟨.mul⟩
+
+/--
+Unsigned division for bit vectors using the Lean convention where division by zero returns zero.
+-/
+def udiv (x y : BitVec n) : BitVec n := ofFin <| x.toFin / y.toFin
+instance : Div (BitVec n) := ⟨.udiv⟩
+
+/--
+Unsigned modulo for bit vectors.
+
+SMT-Lib name: `bvurem`.
+-/
+def umod (x y : BitVec n) : BitVec n := ofFin <| x.toFin % y.toFin
+instance : Mod (BitVec n) := ⟨.umod⟩
+
+/--
+Unsigned division for bit vectors using the
+[SMT-Lib convention](http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml)
+where division by zero returns the `allOnes` bitvector.
+
+SMT-Lib name: `bvudiv`.
+-/
+def smtUDiv (x y : BitVec n) : BitVec n := if y = 0 then -1 else .udiv x y
+
+/--
+Signed t-division for bit vectors using the Lean convention where division
+by zero returns zero.
+
+```lean
+sdiv 7#4 2 = 3#4
+sdiv (-9#4) 2 = -4#4
+sdiv 5#4 -2 = -2#4
+sdiv (-7#4) (-2) = 3#4
+```
+-/
+def sdiv (s t : BitVec n) : BitVec n :=
+  match s.msb, t.msb with
+  | false, false => udiv s t
+  | false, true  => .neg (udiv s (.neg t))
+  | true,  false => .neg (udiv (.neg s) t)
+  | true,  true  => udiv (.neg s) (.neg t)
+
+/--
+Signed division for bit vectors using SMTLIB rules for division by zero.
+
+Specifically, `smtSDiv x 0 = if x >= 0 then -1 else 1`
+
+SMT-Lib name: `bvsdiv`.
+-/
+def smtSDiv (s t : BitVec n) : BitVec n :=
+  match s.msb, t.msb with
+  | false, false => smtUDiv s t
+  | false, true  => .neg (smtUDiv s (.neg t))
+  | true,  false => .neg (smtUDiv (.neg s) t)
+  | true,  true  => smtUDiv (.neg s) (.neg t)
+
+/--
+Remainder for signed division rounding to zero.
+
+SMT_Lib name: `bvsrem`.
+-/
+def srem (s t : BitVec n) : BitVec n :=
+  match s.msb, t.msb with
+  | false, false => umod s t
+  | false, true  => umod s (.neg t)
+  | true,  false => .neg (umod (.neg s) t)
+  | true,  true  => .neg (umod (.neg s) (.neg t))
+
+/--
+Remainder for signed division rounded to negative infinity.
+
+SMT_Lib name: `bvsmod`.
+-/
+def smod (s t : BitVec m) : BitVec m :=
+  match s.msb, t.msb with
+  | false, false => .umod s t
+  | false, true =>
+    let u := .umod s (.neg t)
+    (if u = BitVec.ofNat m 0 then u else .add u t)
+  | true, false =>
+    let u := .umod (.neg s) t
+    (if u = BitVec.ofNat m 0 then u else .sub t u)
+  | true, true => .neg (.umod (.neg s) (.neg t))
+
+/--
+Unsigned less-than for bit vectors.
+
+SMT-Lib name: `bvult`.
+-/
+protected def ult (x y : BitVec n) : Bool := x.toFin < y.toFin
+instance : LT (BitVec n) where lt x y := x.toFin < y.toFin
+instance (x y : BitVec n) : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.toFin < y.toFin))
+
+/--
+Unsigned less-than-or-equal-to for bit vectors.
+
+SMT-Lib name: `bvule`.
+-/
+protected def ule (x y : BitVec n) : Bool := x.toFin ≤ y.toFin
+
+instance : LE (BitVec n) where le x y := x.toFin ≤ y.toFin
+instance (x y : BitVec n) : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.toFin ≤ y.toFin))
+
+/--
+Signed less-than for bit vectors.
+
+```lean
+BitVec.slt 6#4 7 = true
+BitVec.slt 7#4 8 = false
+```
+SMT-Lib name: `bvslt`.
+-/
+protected def slt (x y : BitVec n) : Bool := x.toInt < y.toInt
+
+/--
+Signed less-than-or-equal-to for bit vectors.
+
+SMT-Lib name: `bvsle`.
+-/
+protected def sle (x y : BitVec n) : Bool := x.toInt ≤ y.toInt
+
+/--
+Bitwise AND for bit vectors.
+
+```lean
+0b1010#4 &&& 0b0110#4 = 0b0010#4
+```
+
+SMT-Lib name: `bvand`.
+-/
+protected def and (x y : BitVec n) : BitVec n where toFin :=
+   ⟨x.toNat &&& y.toNat, Nat.and_lt_two_pow x.toNat y.isLt⟩
+instance : AndOp (BitVec w) := ⟨.and⟩
+
+/--
+Bitwise OR for bit vectors.
+
+```lean
+0b1010#4 ||| 0b0110#4 = 0b1110#4
+```
+
+SMT-Lib name: `bvor`.
+-/
+protected def or (x y : BitVec n) : BitVec n where toFin :=
+   ⟨x.toNat ||| y.toNat, Nat.or_lt_two_pow x.isLt y.isLt⟩
+instance : OrOp (BitVec w) := ⟨.or⟩
+
+/--
+ Bitwise XOR for bit vectors.
+
+```lean
+0b1010#4 ^^^ 0b0110#4 = 0b1100#4
+```
+
+SMT-Lib name: `bvxor`.
+-/
+protected def xor (x y : BitVec n) : BitVec n where toFin :=
+   ⟨x.toNat ^^^ y.toNat, Nat.xor_lt_two_pow x.isLt y.isLt⟩
+instance : Xor (BitVec w) := ⟨.xor⟩
+
+/--
+Bitwise NOT for bit vectors.
+
+```lean
+~~~(0b0101#4) == 0b1010
+```
+SMT-Lib name: `bvnot`.
+-/
+protected def not (x : BitVec n) : BitVec n :=
+  allOnes n ^^^ x
+instance : Complement (BitVec w) := ⟨.not⟩
+
+/-- The `BitVec` with value `(2^n + (i mod 2^n)) mod 2^n`.  -/
+protected def ofInt (n : Nat) (i : Int) : BitVec n :=
+  match i with
+  | Int.ofNat a => .ofNat n a
+  | Int.negSucc a => ~~~.ofNat n a
+
+instance : IntCast (BitVec w) := ⟨BitVec.ofInt w⟩
+
+/--
+Left shift for bit vectors. The low bits are filled with zeros. As a numeric operation, this is
+equivalent to `a * 2^s`, modulo `2^n`.
+
+SMT-Lib name: `bvshl` except this operator uses a `Nat` shift value.
+-/
+protected def shiftLeft (a : BitVec n) (s : Nat) : BitVec n := .ofNat n (a.toNat <<< s)
+instance : HShiftLeft (BitVec w) Nat (BitVec w) := ⟨.shiftLeft⟩
+
+/--
+(Logical) right shift for bit vectors. The high bits are filled with zeros.
+As a numeric operation, this is equivalent to `a / 2^s`, rounding down.
+
+SMT-Lib name: `bvlshr` except this operator uses a `Nat` shift value.
+-/
+def ushiftRight (a : BitVec n) (s : Nat) : BitVec n :=
+  ⟨a.toNat >>> s, by
+  let ⟨a, lt⟩ := a
+  simp only [BitVec.toNat, Nat.shiftRight_eq_div_pow, Nat.div_lt_iff_lt_mul (Nat.two_pow_pos s)]
+  rw [←Nat.mul_one a]
+  exact Nat.mul_lt_mul_of_lt_of_le' lt (Nat.two_pow_pos s) (Nat.le_refl 1)⟩
+
+instance : HShiftRight (BitVec w) Nat (BitVec w) := ⟨.ushiftRight⟩
+
+/--
+Arithmetic right shift for bit vectors. The high bits are filled with the
+most-significant bit.
+As a numeric operation, this is equivalent to `a.toInt >>> s`.
+
+SMT-Lib name: `bvashr` except this operator uses a `Nat` shift value.
+-/
+def sshiftRight (a : BitVec n) (s : Nat) : BitVec n := .ofInt n (a.toInt >>> s)
+
+instance {n} : HShiftLeft  (BitVec m) (BitVec n) (BitVec m) := ⟨fun x y => x <<< y.toNat⟩
+instance {n} : HShiftRight (BitVec m) (BitVec n) (BitVec m) := ⟨fun x y => x >>> y.toNat⟩
+
+/--
+Rotate left for bit vectors. All the bits of `x` are shifted to higher positions, with the top `n`
+bits wrapping around to fill the low bits.
+
+```lean
+rotateLeft  0b0011#4 3 = 0b1001
+```
+SMT-Lib name: `rotate_left` except this operator uses a `Nat` shift amount.
+-/
+def rotateLeft (x : BitVec w) (n : Nat) : BitVec w := x <<< n ||| x >>> (w - n)
+
+/--
+Rotate right for bit vectors. All the bits of `x` are shifted to lower positions, with the
+bottom `n` bits wrapping around to fill the high bits.
+
+```lean
+rotateRight 0b01001#5 1 = 0b10100
+```
+SMT-Lib name: `rotate_right` except this operator uses a `Nat` shift amount.
+-/
+def rotateRight (x : BitVec w) (n : Nat) : BitVec w := x >>> n ||| x <<< (w - n)
+
+/--
+A version of `zeroExtend` that requires a proof, but is a noop.
+-/
+def zeroExtend' {n w : Nat} (le : n ≤ w) (x : BitVec n)  : BitVec w :=
+  ⟨x.toNat, by
+    apply Nat.lt_of_lt_of_le x.isLt
+    exact Nat.pow_le_pow_of_le_right (by trivial) le⟩
+
+/--
+`shiftLeftZeroExtend x n` returns `zeroExtend (w+n) x <<< n` without
+needing to compute `x % 2^(2+n)`.
+-/
+def shiftLeftZeroExtend (msbs : BitVec w) (m : Nat) : BitVec (w+m) :=
+  let shiftLeftLt {x : Nat} (p : x < 2^w) (m : Nat) : x <<< m < 2^(w+m) := by
+        simp [Nat.shiftLeft_eq, Nat.pow_add]
+        apply Nat.mul_lt_mul_of_pos_right p
+        exact (Nat.two_pow_pos m)
+  ⟨msbs.toNat <<< m, shiftLeftLt msbs.isLt m⟩
+
+/--
+Concatenation of bitvectors. This uses the "big endian" convention that the more significant
+input is on the left, so `0xAB#8 ++ 0xCD#8 = 0xABCD#16`.
+
+SMT-Lib name: `concat`.
+-/
+def append (msbs : BitVec n) (lsbs : BitVec m) : BitVec (n+m) :=
+  shiftLeftZeroExtend msbs m ||| zeroExtend' (Nat.le_add_left m n) lsbs
+
+instance : HAppend (BitVec w) (BitVec v) (BitVec (w + v)) := ⟨.append⟩
+
+/--
+Extraction of bits `start` to `start + len - 1` from a bit vector of size `n` to yield a
+new bitvector of size `len`. If `start + len > n`, then the vector will be zero-padded in the
+high bits.
+-/
+def extractLsb' (start len : Nat) (a : BitVec n) : BitVec len := .ofNat _ (a.toNat >>> start)
+
+/--
+Extraction of bits `hi` (inclusive) down to `lo` (inclusive) from a bit vector of size `n` to
+yield a new bitvector of size `hi - lo + 1`.
+
+SMT-Lib name: `extract`.
+-/
+def extractLsb (hi lo : Nat) (a : BitVec n) : BitVec (hi - lo + 1) := extractLsb' lo _ a
+
+-- TODO: write this using multiplication
+/-- `replicate i x` concatenates `i` copies of `x` into a new vector of length `w*i`. -/
+def replicate : (i : Nat) → BitVec w → BitVec (w*i)
+  | 0,   _ => 0
+  | n+1, x =>
+    have hEq : w + w*n = w*(n + 1) := by
+      rw [Nat.mul_add, Nat.add_comm, Nat.mul_one]
+    hEq ▸ (x ++ replicate n x)
+
+/-- Fills a bitvector with `w` copies of the bit `b`. -/
+def fill (w : Nat) (b : Bool) : BitVec w := bif b then -1 else 0
+
+/--
+Zero extend vector `x` of length `w` by adding zeros in the high bits until it has length `v`.
+If `v < w` then it truncates the high bits instead.
+
+SMT-Lib name: `zero_extend`.
+-/
+def zeroExtend (v : Nat) (x : BitVec w) : BitVec v :=
+  if h : w ≤ v then
+    zeroExtend' h x
+  else
+    .ofNat v x.toNat
+
+/--
+Truncate the high bits of bitvector `x` of length `w`, resulting in a vector of length `v`.
+If `v > w` then it zero-extends the vector instead.
+-/
+abbrev truncate := @zeroExtend
+
+/--
+Sign extend a vector of length `w`, extending with `i` additional copies of the most significant
+bit in `x`. If `x` is an empty vector, then the sign is treated as zero.
+
+SMT-Lib name: `sign_extend`.
+-/
+def signExtend (v : Nat) (x : BitVec w) : BitVec v := .ofInt v x.toInt
+
+/-! 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
+@[simp] theorem shiftLeft_eq (x : BitVec w) (n : Nat)     : BitVec.shiftLeft x n = x <<< n    := rfl
+@[simp] theorem ushiftRight_eq (x : BitVec w) (n : Nat)   : BitVec.ushiftRight x n = x >>> n  := rfl
+@[simp] theorem not_eq (x : BitVec w)                     : BitVec.not x = ~~~x               := rfl
+@[simp] theorem and_eq (x y : BitVec w)                   : BitVec.and x y = x &&& y          := rfl
+@[simp] theorem or_eq (x y : BitVec w)                    : BitVec.or x y = x ||| y           := rfl
+@[simp] theorem xor_eq (x y : BitVec w)                   : BitVec.xor x y = x ^^^ y          := rfl
+@[simp] theorem neg_eq (x : BitVec w)                     : BitVec.neg x = -x                 := rfl
+@[simp] theorem add_eq (x y : BitVec w)                   : BitVec.add x y = x + y            := rfl
+@[simp] theorem sub_eq (x y : BitVec w)                   : BitVec.sub x y = x - y            := rfl
+@[simp] theorem mul_eq (x y : BitVec w)                   : BitVec.mul x y = x * y            := rfl
+@[simp] theorem zero_eq                                   : BitVec.zero n = 0#n               := rfl
+
+@[simp] theorem cast_ofNat {n m : Nat} (h : n = m) (x : Nat) :
+    cast h (BitVec.ofNat n x) = BitVec.ofNat m x := by
+  subst h; rfl
+
+@[simp] theorem cast_cast {n m k : Nat} (h₁ : n = m) (h₂ : m = k) (x : BitVec n) :
+    cast h₂ (cast h₁ x) = cast (h₁ ▸ h₂) x :=
+  rfl
+
+@[simp] theorem cast_eq {n : Nat} (h : n = n) (x : BitVec n) :
+    cast h x = x :=
+  rfl
+
+/-- Turn a `Bool` into a bitvector of length `1` -/
+def ofBool (b : Bool) : BitVec 1 := cond b 1 0
+
+@[simp] theorem ofBool_false : ofBool false = 0 := by trivial
+@[simp] theorem ofBool_true  : ofBool true  = 1 := by trivial
+
+/-- The empty bitvector -/
+abbrev nil : BitVec 0 := 0
+
+/-!
+### Cons and Concat
+We give special names to the operations of adding a single bit to either end of a bitvector.
+We follow the precedent of `Vector.cons`/`Vector.concat` both for the name, and for the decision
+to have the resulting size be `n + 1` for both operations (rather than `1 + n`, which would be the
+result of appending a single bit to the front in the naive implementation).
+-/
+
+/-- Append a single bit to the end of a bitvector, using big endian order (see `append`).
+    That is, the new bit is the least significant bit. -/
+def concat {n} (msbs : BitVec n) (lsb : Bool) : BitVec (n+1) := msbs ++ (ofBool lsb)
+
+/-- Prepend a single bit to the front of a bitvector, using big endian order (see `append`).
+    That is, the new bit is the most significant bit. -/
+def cons {n} (msb : Bool) (lsbs : BitVec n) : BitVec (n+1) :=
+  ((ofBool msb) ++ lsbs).cast (Nat.add_comm ..)
+
+/-- All empty bitvectors are equal -/
+instance : Subsingleton (BitVec 0) where
+  allEq := by intro ⟨0, _⟩ ⟨0, _⟩; rfl
+
+/-- Every bitvector of length 0 is equal to `nil`, i.e., there is only one empty bitvector -/
+theorem eq_nil : ∀ (x : BitVec 0), x = nil
+  | ofFin ⟨0, _⟩ => rfl
+
+theorem append_ofBool (msbs : BitVec w) (lsb : Bool) :
+    msbs ++ ofBool lsb = concat msbs lsb :=
+  rfl
+
+theorem ofBool_append (msb : Bool) (lsbs : BitVec w) :
+    ofBool msb ++ lsbs = (cons msb lsbs).cast (Nat.add_comm ..) :=
+  rfl

src/Init/Data/BitVec/Bitblast.lean

@@ -0,0 +1,173 @@
+/-
+Copyright (c) 2023 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Harun Khan, Abdalrhman M Mohamed, Joe Hendrix
+-/
+prelude
+import Init.Data.BitVec.Folds
+
+/-!
+# Bitblasting of bitvectors
+
+This module provides theorems for showing the equivalence between BitVec operations using
+the `Fin 2^n` representation and Boolean vectors.  It is still under development, but
+intended to provide a path for converting SAT and SMT solver proofs about BitVectors
+as vectors of bits into proofs about Lean `BitVec` values.
+
+The module is named for the bit-blasting operation in an SMT solver that converts bitvector
+expressions into expressions about individual bits in each vector.
+
+## Main results
+* `x + y : BitVec w` is `(adc x y false).2`.
+
+
+## Future work
+All other operations are to be PR'ed later and are already proved in
+https://github.com/mhk119/lean-smt/blob/bitvec/Smt/Data/Bitwise.lean.
+
+-/
+
+open Nat Bool
+
+/-! ### Preliminaries -/
+
+namespace Std.BitVec
+
+private theorem testBit_limit {x i : Nat} (x_lt_succ : x < 2^(i+1)) :
+    testBit x i = decide (x ≥ 2^i) := by
+  cases xi : testBit x i with
+  | true =>
+    simp [testBit_implies_ge xi]
+  | false =>
+    simp
+    cases Nat.lt_or_ge x (2^i) with
+    | inl x_lt =>
+      exact x_lt
+    | inr x_ge =>
+      have ⟨j, ⟨j_ge, jp⟩⟩  := ge_two_pow_implies_high_bit_true x_ge
+      cases Nat.lt_or_eq_of_le j_ge with
+      | inr x_eq =>
+        simp [x_eq, jp] at xi
+      | inl x_lt =>
+        exfalso
+        apply Nat.lt_irrefl
+        calc x < 2^(i+1) := x_lt_succ
+             _ ≤ 2 ^ j := Nat.pow_le_pow_of_le_right Nat.zero_lt_two x_lt
+             _ ≤ x := testBit_implies_ge jp
+
+private theorem mod_two_pow_succ (x i : Nat) :
+  x % 2^(i+1) = 2^i*(x.testBit i).toNat + x % (2 ^ i):= by
+  apply Nat.eq_of_testBit_eq
+  intro j
+  simp only [Nat.mul_add_lt_is_or, testBit_or, testBit_mod_two_pow, testBit_shiftLeft,
+    Nat.testBit_bool_to_nat, Nat.sub_eq_zero_iff_le, Nat.mod_lt, Nat.two_pow_pos,
+    testBit_mul_pow_two]
+  rcases Nat.lt_trichotomy i j with i_lt_j | i_eq_j | j_lt_i
+  · have i_le_j : i ≤ j := Nat.le_of_lt i_lt_j
+    have not_j_le_i : ¬(j ≤ i) := Nat.not_le_of_lt i_lt_j
+    have not_j_lt_i : ¬(j < i) := Nat.not_lt_of_le i_le_j
+    have not_j_lt_i_succ : ¬(j < i + 1) :=
+          Nat.not_le_of_lt (Nat.succ_lt_succ i_lt_j)
+    simp [i_le_j, not_j_le_i, not_j_lt_i, not_j_lt_i_succ]
+  · simp [i_eq_j]
+  · have j_le_i : j ≤ i := Nat.le_of_lt j_lt_i
+    have j_le_i_succ : j < i + 1 := Nat.succ_le_succ j_le_i
+    have not_j_ge_i : ¬(j ≥ i) := Nat.not_le_of_lt j_lt_i
+    simp [j_lt_i, j_le_i, not_j_ge_i, j_le_i_succ]
+
+private theorem mod_two_pow_lt (x i : Nat) : x % 2 ^ i < 2^i := Nat.mod_lt _ (Nat.two_pow_pos _)
+
+/-! ### Addition -/
+
+/-- carry w x y c returns true if the `w` carry bit is true when computing `x + y + c`. -/
+def carry (w x y : Nat) (c : Bool) : Bool := decide (x % 2^w + y % 2^w + c.toNat ≥ 2^w)
+
+@[simp] theorem carry_zero : carry 0 x y c = c := by
+  cases c <;> simp [carry, mod_one]
+
+/-- At least two out of three booleans are true. -/
+abbrev atLeastTwo (a b c : Bool) : Bool := a && b || a && c || b && c
+
+/-- Carry function for bitwise addition. -/
+def adcb (x y c : Bool) : Bool × Bool := (atLeastTwo x y c, Bool.xor x (Bool.xor y c))
+
+/-- Bitwise addition implemented via a ripple carry adder. -/
+def adc (x y : BitVec w) : Bool → Bool × BitVec w :=
+  iunfoldr fun (i : Fin w) c => adcb (x.getLsb i) (y.getLsb i) c
+
+theorem adc_overflow_limit (x y i : Nat) (c : Bool) : x % 2^i + (y % 2^i + c.toNat) < 2^(i+1) := by
+  have : c.toNat ≤ 1 := Bool.toNat_le_one c
+  rw [Nat.pow_succ]
+  omega
+
+theorem carry_succ (w x y : Nat) (c : Bool) :
+    carry (succ w) x y c = atLeastTwo (x.testBit w) (y.testBit w) (carry w x y c) := by
+  simp only [carry, mod_two_pow_succ, atLeastTwo]
+  simp only [Nat.pow_succ']
+  generalize testBit x w = xh
+  generalize testBit y w = yh
+  have sum_bnd : x%2^w + (y%2^w + c.toNat) < 2*2^w := by
+          simp only [← Nat.pow_succ']
+          exact adc_overflow_limit x y w c
+  cases xh <;> cases yh <;> (simp; omega)
+
+theorem getLsb_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool) :
+    getLsb (x + y + zeroExtend w (ofBool c)) i =
+      Bool.xor (getLsb x i) (Bool.xor (getLsb y i) (carry i x.toNat y.toNat c)) := by
+  let ⟨x, x_lt⟩ := x
+  let ⟨y, y_lt⟩ := y
+  simp only [getLsb, toNat_add, toNat_zeroExtend, i_lt, toNat_ofFin, toNat_ofBool,
+    Nat.mod_add_mod, Nat.add_mod_mod]
+  apply Eq.trans
+  rw [← Nat.div_add_mod x (2^i), ← Nat.div_add_mod y (2^i)]
+  simp only
+    [ Nat.testBit_mod_two_pow,
+      Nat.testBit_mul_two_pow_add_eq,
+      i_lt,
+      decide_True,
+      Bool.true_and,
+      Nat.add_assoc,
+      Nat.add_left_comm (_%_) (_ * _) _,
+      testBit_limit (adc_overflow_limit x y i c)
+    ]
+  simp [testBit_to_div_mod, carry, Nat.add_assoc]
+
+theorem getLsb_add {i : Nat} (i_lt : i < w) (x y : BitVec w) :
+    getLsb (x + y) i =
+      Bool.xor (getLsb x i) (Bool.xor (getLsb y i) (carry i x.toNat y.toNat false)) := by
+  simpa using getLsb_add_add_bool i_lt x y false
+
+theorem adc_spec (x y : BitVec w) (c : Bool) :
+    adc x y c = (carry w x.toNat y.toNat c, x + y + zeroExtend w (ofBool c)) := by
+  simp only [adc]
+  apply iunfoldr_replace
+          (fun i => carry i x.toNat y.toNat c)
+          (x + y + zeroExtend w (ofBool c))
+          c
+  case init =>
+    simp [carry, Nat.mod_one]
+    cases c <;> rfl
+  case step =>
+    intro ⟨i, lt⟩
+    simp only [adcb, Prod.mk.injEq, carry_succ]
+    apply And.intro
+    case left =>
+      rw [testBit_toNat, testBit_toNat]
+    case right =>
+      simp [getLsb_add_add_bool lt]
+
+theorem add_eq_adc (w : Nat) (x y : BitVec w) : x + y = (adc x y false).snd := by
+  simp [adc_spec]
+
+/-! ### add -/
+
+/-- Adding a bitvector to its own complement yields the all ones bitpattern -/
+@[simp] theorem add_not_self (x : BitVec w) : x + ~~~x = allOnes w := by
+  rw [add_eq_adc, adc, iunfoldr_replace (fun _ => false) (allOnes w)]
+  · rfl
+  · simp [adcb, atLeastTwo]
+
+/-- Subtracting `x` from the all ones bitvector is equivalent to taking its complement -/
+theorem allOnes_sub_eq_not (x : BitVec w) : allOnes w - x = ~~~x := by
+  rw [← add_not_self x, BitVec.add_comm, add_sub_cancel]

src/Init/Data/BitVec/Folds.lean

@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joe Hendrix
+-/
+prelude
+import Init.Data.BitVec.Lemmas
+import Init.Data.Nat.Lemmas
+import Init.Data.Fin.Iterate
+
+namespace Std.BitVec
+
+/--
+iunfoldr is an iterative operation that applies a function `f` repeatedly.
+
+It produces a sequence of state values `[s_0, s_1 .. s_w]` and a bitvector
+`v` where `f i s_i = (s_{i+1}, b_i)` and `b_i` is bit `i`th least-significant bit
+in `v` (e.g., `getLsb v i = b_i`).
+
+Theorems involving `iunfoldr` can be eliminated using `iunfoldr_replace` below.
+-/
+def iunfoldr (f : Fin w -> α → α × Bool) (s : α) : α × BitVec w :=
+  Fin.hIterate (fun i => α × BitVec i) (s, nil) fun i q =>
+    (fun p => ⟨p.fst, cons p.snd q.snd⟩) (f i q.fst)
+
+theorem iunfoldr.fst_eq
+    {f : Fin w → α → α × Bool} (state : Nat → α) (s : α)
+    (init : s = state 0)
+    (ind : ∀(i : Fin w), (f i (state i.val)).fst = state (i.val+1)) :
+    (iunfoldr f s).fst = state w := by
+  unfold iunfoldr
+  apply Fin.hIterate_elim (fun i (p : α × BitVec i) => p.fst = state i)
+  case init =>
+    exact init
+  case step =>
+    intro i ⟨s, v⟩ p
+    simp_all [ind i]
+
+private theorem iunfoldr.eq_test
+    {f : Fin w → α → α × Bool} (state : Nat → α) (value : BitVec w) (a : α)
+    (init : state 0 = a)
+    (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsb i.val)) :
+    iunfoldr f a = (state w, BitVec.truncate w value) := by
+  apply Fin.hIterate_eq (fun i => ((state i, BitVec.truncate i value) : α × BitVec i))
+  case init =>
+    simp only [init, eq_nil]
+  case step =>
+    intro i
+    simp_all [truncate_succ]
+
+/--
+Correctness theorem for `iunfoldr`.
+-/
+theorem iunfoldr_replace
+    {f : Fin w → α → α × Bool} (state : Nat → α) (value : BitVec w) (a : α)
+    (init : state 0 = a)
+    (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsb i.val)) :
+    iunfoldr f a = (state w, value) := by
+  simp [iunfoldr.eq_test state value a init step]

src/Init/Data/BitVec/Lemmas.lean

@@ -0,0 +1,534 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joe Hendrix
+-/
+prelude
+import Init.Data.Bool
+import Init.Data.BitVec.Basic
+import Init.Data.Fin.Lemmas
+import Init.Data.Nat.Lemmas
+
+namespace Std.BitVec
+
+/--
+This normalized a bitvec using `ofFin` to `ofNat`.
+-/
+theorem ofFin_eq_ofNat : @BitVec.ofFin w (Fin.mk x lt) = BitVec.ofNat w x := by
+  simp only [BitVec.ofNat, Fin.ofNat', lt, Nat.mod_eq_of_lt]
+
+/-- Prove equality of bitvectors in terms of nat operations. -/
+theorem eq_of_toNat_eq {n} : ∀ {i j : BitVec n}, i.toNat = j.toNat → i = j
+  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
+
+@[simp] theorem val_toFin (x : BitVec w) : x.toFin.val = x.toNat := rfl
+
+theorem toNat_eq (x y : BitVec n) : x = y ↔ x.toNat = y.toNat :=
+  Iff.intro (congrArg BitVec.toNat) eq_of_toNat_eq
+
+theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.toFin.2
+
+theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsb i := rfl
+
+@[simp] theorem getLsb_ofFin (x : Fin (2^n)) (i : Nat) :
+  getLsb (BitVec.ofFin x) i = x.val.testBit i := rfl
+
+@[simp] theorem getLsb_ge (x : BitVec w) (i : Nat) (ge : i ≥ w) : getLsb x i = false := by
+  let ⟨x, x_lt⟩ := x
+  simp
+  apply Nat.testBit_lt_two_pow
+  have p : 2^w ≤ 2^i := Nat.pow_le_pow_of_le_right (by omega) ge
+  omega
+
+theorem lt_of_getLsb (x : BitVec w) (i : Nat) : getLsb x i = true → i < w := by
+  if h : i < w then
+    simp [h]
+  else
+    simp [Nat.ge_of_not_lt h]
+
+-- We choose `eq_of_getLsb_eq` as the `@[ext]` theorem for `BitVec`
+-- somewhat arbitrarily over `eq_of_getMsg_eq`.
+@[ext] theorem eq_of_getLsb_eq {x y : BitVec w}
+    (pred : ∀(i : Fin w), x.getLsb i.val = y.getLsb i.val) : x = y := by
+  apply eq_of_toNat_eq
+  apply Nat.eq_of_testBit_eq
+  intro i
+  if i_lt : i < w then
+    exact pred ⟨i, i_lt⟩
+  else
+    have p : i ≥ w := Nat.le_of_not_gt i_lt
+    simp [testBit_toNat, getLsb_ge _ _ p]
+
+theorem eq_of_getMsb_eq {x y : BitVec w}
+    (pred : ∀(i : Fin w), x.getMsb i = y.getMsb i.val) : x = y := by
+  simp only [getMsb] at pred
+  apply eq_of_getLsb_eq
+  intro ⟨i, i_lt⟩
+  if w_zero : w = 0 then
+    simp [w_zero]
+  else
+    have w_pos := Nat.pos_of_ne_zero w_zero
+    have r : i ≤ w - 1 := by
+      simp [Nat.le_sub_iff_add_le w_pos, Nat.add_succ]
+      exact i_lt
+    have q_lt : w - 1 - i < w := by
+      simp only [Nat.sub_sub]
+      apply Nat.sub_lt w_pos
+      simp [Nat.succ_add]
+    have q := pred ⟨w - 1 - i, q_lt⟩
+    simpa [q_lt, Nat.sub_sub_self, r] using q
+
+theorem eq_of_toFin_eq : ∀ {x y : BitVec w}, x.toFin = y.toFin → x = y
+  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
+
+@[simp] theorem toNat_ofBool (b : Bool) : (ofBool b).toNat = b.toNat := by
+  cases b <;> rfl
+
+theorem ofNat_one (n : Nat) : BitVec.ofNat 1 n = BitVec.ofBool (n % 2 = 1) :=  by
+  rcases (Nat.mod_two_eq_zero_or_one n) with h | h <;> simp [h, BitVec.ofNat, Fin.ofNat']
+
+theorem ofBool_eq_iff_eq : ∀(b b' : Bool), BitVec.ofBool b = BitVec.ofBool b' ↔ b = b' := by
+  decide
+
+@[simp] theorem toNat_ofFin (x : Fin (2^n)) : (BitVec.ofFin x).toNat = x.val := rfl
+
+@[simp] theorem toNat_ofNat (x w : Nat) : (x#w).toNat = x % 2^w := by
+  simp [BitVec.toNat, BitVec.ofNat, Fin.ofNat']
+
+-- Remark: we don't use `[simp]` here because simproc` subsumes it for literals.
+-- If `x` and `n` are not literals, applying this theorem eagerly may not be a good idea.
+theorem getLsb_ofNat (n : Nat) (x : Nat) (i : Nat) :
+  getLsb (x#n) i = (i < n && x.testBit i) := by
+  simp [getLsb, BitVec.ofNat, Fin.val_ofNat']
+
+@[deprecated toNat_ofNat] theorem toNat_zero (n : Nat) : (0#n).toNat = 0 := by trivial
+
+@[simp] theorem toNat_mod_cancel (x : BitVec n) : x.toNat % (2^n) = x.toNat :=
+  Nat.mod_eq_of_lt x.isLt
+
+private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) : x < 2 ^ n :=
+  Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_of_le_right (by trivial : 0 < 2) le)
+
+@[simp] theorem ofNat_toNat (m : Nat) (x : BitVec n) : x.toNat#m = truncate m x := by
+  let ⟨x, lt_n⟩ := x
+  unfold truncate
+  unfold zeroExtend
+  if h : n ≤ m then
+    unfold zeroExtend'
+    have lt_m : x < 2 ^ m := lt_two_pow_of_le lt_n h
+    simp [h, lt_m, Nat.mod_eq_of_lt, BitVec.toNat, BitVec.ofNat, Fin.ofNat']
+  else
+    simp [h]
+
+
+/-! ### msb -/
+
+theorem msb_eq_decide (x : BitVec (Nat.succ w)) : BitVec.msb x = decide (2 ^ w ≤ x.toNat) := by
+  simp only [BitVec.msb, getMsb, Nat.zero_lt_succ,
+    decide_True, getLsb, Nat.testBit, Nat.succ_sub_succ_eq_sub,
+    Nat.sub_zero, Nat.and_one_is_mod, Bool.true_and, Nat.shiftRight_eq_div_pow]
+  rcases (Nat.lt_or_ge (BitVec.toNat x) (2 ^ w)) with h | h
+  · simp [Nat.div_eq_of_lt h, h]
+  · simp only [h]
+    rw [Nat.div_eq_sub_div (Nat.two_pow_pos w) h, Nat.div_eq_of_lt]
+    · decide
+    · have : BitVec.toNat x < 2^w + 2^w := by simpa [Nat.pow_succ, Nat.mul_two] using x.isLt
+      omega
+
+/-! ### cast -/
+
+@[simp] theorem toNat_cast (h : w = v) (x : BitVec w) : (cast h x).toNat = x.toNat := rfl
+@[simp] theorem toFin_cast (h : w = v) (x : BitVec w) :
+    (cast h x).toFin = x.toFin.cast (by rw [h]) :=
+  rfl
+
+@[simp] theorem getLsb_cast (h : w = v) (x : BitVec w) : (cast h x).getLsb i = x.getLsb i := by
+  subst h; simp
+
+@[simp] theorem getMsb_cast (h : w = v) (x : BitVec w) : (cast h x).getMsb i = x.getMsb i := by
+  subst h; simp
+@[simp] theorem msb_cast (h : w = v) (x : BitVec w) : (cast h x).msb = x.msb := by
+  simp [BitVec.msb]
+
+/-! ### zeroExtend and truncate -/
+
+@[simp] theorem toNat_zeroExtend' {m n : Nat} (p : m ≤ n) (x : BitVec m) :
+    (zeroExtend' p x).toNat = x.toNat := by
+  unfold zeroExtend'
+  simp [p, x.isLt, Nat.mod_eq_of_lt]
+
+theorem toNat_zeroExtend (i : Nat) (x : BitVec n) :
+    BitVec.toNat (zeroExtend i x) = x.toNat % 2^i := by
+  let ⟨x, lt_n⟩ := x
+  simp only [zeroExtend]
+  if n_le_i : n ≤ i then
+    have x_lt_two_i : x < 2 ^ i := lt_two_pow_of_le lt_n n_le_i
+    simp [n_le_i, Nat.mod_eq_of_lt, x_lt_two_i]
+  else
+    simp [n_le_i, toNat_ofNat]
+
+@[simp] theorem zeroExtend_eq (x : BitVec n) : zeroExtend n x = x := by
+  apply eq_of_toNat_eq
+  let ⟨x, lt_n⟩ := x
+  simp [truncate, zeroExtend]
+
+@[simp] theorem zeroExtend_zero (m n : Nat) : zeroExtend m (0#n) = 0#m := by
+  apply eq_of_toNat_eq
+  simp [toNat_zeroExtend]
+
+@[simp] theorem truncate_eq (x : BitVec n) : truncate n x = x := zeroExtend_eq x
+
+@[simp] theorem toNat_truncate (x : BitVec n) : (truncate i x).toNat = x.toNat % 2^i :=
+  toNat_zeroExtend i x
+
+@[simp] theorem getLsb_zeroExtend' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
+    getLsb (zeroExtend' ge x) i = getLsb x i := by
+  simp [getLsb, toNat_zeroExtend']
+
+@[simp] theorem getLsb_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) :
+    getLsb (zeroExtend m x) i = (decide (i < m) && getLsb x i) := by
+  simp [getLsb, toNat_zeroExtend, Nat.testBit_mod_two_pow]
+
+@[simp] theorem getLsb_truncate (m : Nat) (x : BitVec n) (i : Nat) :
+    getLsb (truncate m x) i = (decide (i < m) && getLsb x i) :=
+  getLsb_zeroExtend m x i
+
+/-! ## extractLsb -/
+
+@[simp]
+protected theorem extractLsb_ofFin {n} (x : Fin (2^n)) (hi lo : Nat) :
+  extractLsb hi lo (@BitVec.ofFin n x) = .ofNat (hi-lo+1) (x.val >>> lo) := rfl
+
+@[simp]
+protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
+  extractLsb hi lo x#n = .ofNat (hi - lo + 1) ((x % 2^n) >>> lo) := by
+  apply eq_of_getLsb_eq
+  intro ⟨i, _lt⟩
+  simp [BitVec.ofNat]
+
+@[simp] theorem extractLsb'_toNat (s m : Nat) (x : BitVec n) :
+  (extractLsb' s m x).toNat = (x.toNat >>> s) % 2^m := rfl
+
+@[simp] theorem extractLsb_toNat (hi lo : Nat) (x : BitVec n) :
+  (extractLsb hi lo x).toNat = (x.toNat >>> lo) % 2^(hi-lo+1) := rfl
+
+@[simp] theorem getLsb_extract (hi lo : Nat) (x : BitVec n) (i : Nat) :
+    getLsb (extractLsb hi lo x) i = (i ≤ (hi-lo) && getLsb x (lo+i)) := by
+  unfold getLsb
+  simp [Nat.lt_succ]
+
+/-! ### allOnes -/
+
+private theorem allOnes_def :
+    allOnes v = .ofFin (⟨0, Nat.two_pow_pos v⟩ - ⟨1 % 2^v, Nat.mod_lt _ (Nat.two_pow_pos v)⟩) := by
+  rfl
+
+@[simp] theorem toNat_allOnes : (allOnes v).toNat = 2^v - 1 := by
+  simp only [allOnes_def, toNat_ofFin, Fin.coe_sub, Nat.zero_add]
+  by_cases h : v = 0
+  · subst h
+    rfl
+  · rw [Nat.mod_eq_of_lt (Nat.one_lt_two_pow h), Nat.mod_eq_of_lt]
+    exact Nat.pred_lt_self (Nat.two_pow_pos v)
+
+@[simp] theorem getLsb_allOnes : (allOnes v).getLsb i = decide (i < v) := by
+  simp only [allOnes_def, getLsb_ofFin, Fin.coe_sub, Nat.zero_add, Nat.testBit_mod_two_pow]
+  if h : i < v then
+    simp only [h, decide_True, Bool.true_and]
+    match i, v, h with
+    | i, (v + 1), h =>
+      rw [Nat.mod_eq_of_lt (by simp), Nat.testBit_two_pow_sub_one]
+      simp [h]
+  else
+    simp [h]
+
+@[simp] theorem negOne_eq_allOnes : -1#w = allOnes w :=
+  rfl
+
+/-! ### or -/
+
+@[simp] theorem toNat_or (x y : BitVec v) :
+    BitVec.toNat (x ||| y) = BitVec.toNat x ||| BitVec.toNat y := rfl
+
+@[simp] theorem toFin_or (x y : BitVec v) :
+    BitVec.toFin (x ||| y) = BitVec.toFin x ||| BitVec.toFin y := by
+  simp only [HOr.hOr, OrOp.or, BitVec.or, Fin.lor, val_toFin, Fin.mk.injEq]
+  exact (Nat.mod_eq_of_lt <| Nat.or_lt_two_pow x.isLt y.isLt).symm
+
+
+@[simp] theorem getLsb_or {x y : BitVec v} : (x ||| y).getLsb i = (x.getLsb i || y.getLsb i) := by
+  rw [← testBit_toNat, getLsb, getLsb]
+  simp
+
+/-! ### and -/
+
+@[simp] theorem toNat_and (x y : BitVec v) :
+    BitVec.toNat (x &&& y) = BitVec.toNat x &&& BitVec.toNat y := rfl
+
+@[simp] theorem toFin_and (x y : BitVec v) :
+    BitVec.toFin (x &&& y) = BitVec.toFin x &&& BitVec.toFin y := by
+  simp only [HAnd.hAnd, AndOp.and, BitVec.and, Fin.land, val_toFin, Fin.mk.injEq]
+  exact (Nat.mod_eq_of_lt <| Nat.and_lt_two_pow _ y.isLt).symm
+
+@[simp] theorem getLsb_and {x y : BitVec v} : (x &&& y).getLsb i = (x.getLsb i && y.getLsb i) := by
+  rw [← testBit_toNat, getLsb, getLsb]
+  simp
+
+/-! ### xor -/
+
+@[simp] theorem toNat_xor (x y : BitVec v) :
+    BitVec.toNat (x ^^^ y) = BitVec.toNat x ^^^ BitVec.toNat y := rfl
+
+@[simp] theorem toFin_xor (x y : BitVec v) :
+    BitVec.toFin (x ^^^ y) = BitVec.toFin x ^^^ BitVec.toFin y := by
+  simp only [HXor.hXor, Xor.xor, BitVec.xor, Fin.xor, val_toFin, Fin.mk.injEq]
+  exact (Nat.mod_eq_of_lt <| Nat.xor_lt_two_pow x.isLt y.isLt).symm
+
+@[simp] theorem getLsb_xor {x y : BitVec v} :
+    (x ^^^ y).getLsb i = (xor (x.getLsb i) (y.getLsb i)) := by
+  rw [← testBit_toNat, getLsb, getLsb]
+  simp
+
+/-! ### not -/
+
+theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
+
+@[simp] theorem toNat_not {x : BitVec v} : (~~~x).toNat = 2^v - 1 - x.toNat := by
+  rw [Nat.sub_sub, Nat.add_comm, not_def, toNat_xor]
+  apply Nat.eq_of_testBit_eq
+  intro i
+  simp only [toNat_allOnes, Nat.testBit_xor, Nat.testBit_two_pow_sub_one]
+  match h : BitVec.toNat x with
+  | 0 => simp
+  | y+1 =>
+    rw [Nat.succ_eq_add_one] at h
+    rw [← h]
+    rw [Nat.testBit_two_pow_sub_succ (toNat_lt _)]
+    · cases w : decide (i < v)
+      · simp at w
+        simp [w]
+        rw [Nat.testBit_lt_two_pow]
+        calc BitVec.toNat x < 2 ^ v := toNat_lt _
+          _ ≤ 2 ^ i := Nat.pow_le_pow_of_le_right Nat.zero_lt_two w
+      · simp
+
+@[simp] theorem toFin_not (x : BitVec w) :
+    (~~~x).toFin = x.toFin.rev := by
+  apply Fin.val_inj.mp
+  simp only [val_toFin, toNat_not, Fin.val_rev]
+  omega
+
+@[simp] theorem getLsb_not {x : BitVec v} : (~~~x).getLsb i = (decide (i < v) && ! x.getLsb i) := by
+  by_cases h' : i < v <;> simp_all [not_def]
+
+/-! ### shiftLeft -/
+
+@[simp] theorem toNat_shiftLeft {x : BitVec v} :
+    BitVec.toNat (x <<< n) = BitVec.toNat x <<< n % 2^v :=
+  BitVec.toNat_ofNat _ _
+
+@[simp] theorem toFin_shiftLeft {n : Nat} (x : BitVec w) :
+    BitVec.toFin (x <<< n) = Fin.ofNat' (x.toNat <<< n) (Nat.two_pow_pos w) := rfl
+
+@[simp] theorem getLsb_shiftLeft (x : BitVec m) (n) :
+    getLsb (x <<< n) i = (decide (i < m) && !decide (i < n) && getLsb x (i - n)) := by
+  rw [← testBit_toNat, getLsb]
+  simp only [toNat_shiftLeft, Nat.testBit_mod_two_pow, Nat.testBit_shiftLeft, ge_iff_le]
+  -- This step could be a case bashing tactic.
+  cases h₁ : decide (i < m) <;> cases h₂ : decide (n ≤ i) <;> cases h₃ : decide (i < n)
+  all_goals { simp_all <;> omega }
+
+theorem shiftLeftZeroExtend_eq {x : BitVec w} :
+    shiftLeftZeroExtend x n = zeroExtend (w+n) x <<< n := by
+  apply eq_of_toNat_eq
+  rw [shiftLeftZeroExtend, zeroExtend]
+  split
+  · simp
+    rw [Nat.mod_eq_of_lt]
+    rw [Nat.shiftLeft_eq, Nat.pow_add]
+    exact Nat.mul_lt_mul_of_pos_right (BitVec.toNat_lt x) (Nat.two_pow_pos _)
+  · omega
+
+@[simp] theorem getLsb_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :
+    getLsb (shiftLeftZeroExtend x n) i = ((! decide (i < n)) && getLsb x (i - n)) := by
+  rw [shiftLeftZeroExtend_eq]
+  simp only [getLsb_shiftLeft, getLsb_zeroExtend]
+  cases h₁ : decide (i < n) <;> cases h₂ : decide (i - n < m + n) <;> cases h₃ : decide (i < m + n)
+    <;> simp_all
+    <;> (rw [getLsb_ge]; omega)
+
+/-! ### ushiftRight -/
+
+@[simp] theorem toNat_ushiftRight (x : BitVec n) (i : Nat) :
+    (x >>> i).toNat = x.toNat >>> i := rfl
+
+@[simp] theorem getLsb_ushiftRight (x : BitVec n) (i j : Nat) :
+    getLsb (x >>> i) j = getLsb x (i+j) := by
+  unfold getLsb ; simp
+
+/-! ### append -/
+
+theorem append_def (x : BitVec v) (y : BitVec w) :
+    x ++ y = (shiftLeftZeroExtend x w ||| zeroExtend' (Nat.le_add_left w v) y) := rfl
+
+@[simp] theorem toNat_append (x : BitVec m) (y : BitVec n) :
+    (x ++ y).toNat = x.toNat <<< n ||| y.toNat :=
+  rfl
+
+@[simp] theorem getLsb_append {v : BitVec n} {w : BitVec m} :
+    getLsb (v ++ w) i = bif i < m then getLsb w i else getLsb v (i - m) := by
+  simp [append_def]
+  by_cases h : i < m
+  · simp [h]
+  · simp [h]; simp_all
+
+/-! ### rev -/
+
+theorem getLsb_rev (x : BitVec w) (i : Fin w) :
+    x.getLsb i.rev = x.getMsb i := by
+  simp [getLsb, getMsb]
+  congr 1
+  omega
+
+theorem getMsb_rev (x : BitVec w) (i : Fin w) :
+    x.getMsb i.rev = x.getLsb i := by
+  simp only [← getLsb_rev]
+  simp only [Fin.rev]
+  congr
+  omega
+
+/-! ### cons -/
+
+@[simp] theorem toNat_cons (b : Bool) (x : BitVec w) :
+    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat := by
+  let ⟨x, _⟩ := x
+  simp [cons, toNat_append, toNat_ofBool]
+
+@[simp] theorem getLsb_cons (b : Bool) {n} (x : BitVec n) (i : Nat) :
+    getLsb (cons b x) i = if i = n then b else getLsb x i := by
+  simp only [getLsb, toNat_cons, Nat.testBit_or]
+  rw [Nat.testBit_shiftLeft]
+  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
+  · have p1 : ¬(n ≤ i) := by omega
+    have p2 : i ≠ n := by omega
+    simp [p1, p2]
+  · simp [i_eq_n, testBit_toNat]
+    cases b <;> trivial
+  · have p1 : i ≠ n := by omega
+    have p2 : i - n ≠ 0 := by omega
+    simp [p1, p2, Nat.testBit_bool_to_nat]
+
+theorem truncate_succ (x : BitVec w) :
+    truncate (i+1) x = cons (getLsb x i) (truncate i x) := by
+  apply eq_of_getLsb_eq
+  intro j
+  simp only [getLsb_truncate, getLsb_cons, j.isLt, decide_True, Bool.true_and]
+  if j_eq : j.val = i then
+    simp [j_eq]
+  else
+    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]
+
+/-! ### add -/
+
+theorem add_def {n} (x y : BitVec n) : x + y = .ofNat n (x.toNat + y.toNat) := rfl
+
+/--
+Definition of bitvector addition as a nat.
+-/
+@[simp] theorem toNat_add (x y : BitVec w) : (x + y).toNat = (x.toNat + y.toNat) % 2^w := rfl
+@[simp] theorem toFin_add (x y : BitVec w) : (x + y).toFin = toFin x + toFin y := rfl
+@[simp] theorem ofFin_add (x : Fin (2^n)) (y : BitVec n) :
+  .ofFin x + y = .ofFin (x + y.toFin) := rfl
+@[simp] theorem add_ofFin (x : BitVec n) (y : Fin (2^n)) :
+  x + .ofFin y = .ofFin (x.toFin + y) := rfl
+@[simp] theorem ofNat_add_ofNat {n} (x y : Nat) : x#n + y#n = (x + y)#n := by
+  apply eq_of_toNat_eq ; simp [BitVec.ofNat]
+
+protected theorem add_assoc (x y z : BitVec n) : x + y + z = x + (y + z) := by
+  apply eq_of_toNat_eq ; simp [Nat.add_assoc]
+
+protected theorem add_comm (x y : BitVec n) : x + y = y + x := by
+  simp [add_def, Nat.add_comm]
+
+@[simp] protected theorem add_zero (x : BitVec n) : x + 0#n = x := by simp [add_def]
+
+@[simp] protected theorem zero_add (x : BitVec n) : 0#n + x = x := by simp [add_def]
+
+
+/-! ### sub/neg -/
+
+theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n (x.toNat + (2^n - y.toNat)) := by rfl
+
+@[simp] theorem toNat_sub {n} (x y : BitVec n) :
+  (x - y).toNat = ((x.toNat + (2^n - y.toNat)) % 2^n) := rfl
+@[simp] theorem toFin_sub (x y : BitVec n) : (x - y).toFin = toFin x - toFin y := rfl
+
+@[simp] theorem ofFin_sub (x : Fin (2^n)) (y : BitVec n) : .ofFin x - y = .ofFin (x - y.toFin) :=
+  rfl
+@[simp] theorem sub_ofFin (x : BitVec n) (y : Fin (2^n)) : x - .ofFin y = .ofFin (x.toFin - y) :=
+  rfl
+-- Remark: we don't use `[simp]` here because simproc` subsumes it for literals.
+-- If `x` and `n` are not literals, applying this theorem eagerly may not be a good idea.
+theorem ofNat_sub_ofNat {n} (x y : Nat) : x#n - y#n = .ofNat n (x + (2^n - y % 2^n)) := by
+  apply eq_of_toNat_eq ; simp [BitVec.ofNat]
+
+@[simp] protected theorem sub_zero (x : BitVec n) : x - (0#n) = x := by apply eq_of_toNat_eq ; simp
+
+@[simp] protected theorem sub_self (x : BitVec n) : x - x = 0#n := by
+  apply eq_of_toNat_eq
+  simp only [toNat_sub]
+  rw [Nat.add_sub_of_le]
+  · simp
+  · exact Nat.le_of_lt x.isLt
+
+@[simp] theorem toNat_neg (x : BitVec n) : (- x).toNat = (2^n - x.toNat) % 2^n := by
+  simp [Neg.neg, BitVec.neg]
+
+theorem sub_toAdd {n} (x y : BitVec n) : x - y = x + - y := by
+  apply eq_of_toNat_eq
+  simp
+
+@[simp] theorem neg_zero (n:Nat) : -0#n = 0#n := by apply eq_of_toNat_eq ; simp
+
+theorem add_sub_cancel (x y : BitVec w) : x + y - y = x := by
+  apply eq_of_toNat_eq
+  have y_toNat_le := Nat.le_of_lt y.toNat_lt
+  rw [toNat_sub, toNat_add, Nat.mod_add_mod, Nat.add_assoc, ← Nat.add_sub_assoc y_toNat_le,
+    Nat.add_sub_cancel_left, Nat.add_mod_right, toNat_mod_cancel]
+
+/-! ### mul -/
+
+theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl
+
+theorem toNat_mul (x y : BitVec n) : (x * y).toNat = (x.toNat * y.toNat) % 2 ^ n := rfl
+@[simp] theorem toFin_mul (x y : BitVec n) : (x * y).toFin = (x.toFin * y.toFin) := rfl
+
+/-! ### le and lt -/
+
+theorem le_def (x y : BitVec n) :
+  x ≤ y ↔ x.toNat ≤ y.toNat := Iff.rfl
+
+@[simp] theorem le_ofFin (x : BitVec n) (y : Fin (2^n)) :
+  x ≤ BitVec.ofFin y ↔ x.toFin ≤ y := Iff.rfl
+@[simp] theorem ofFin_le (x : Fin (2^n)) (y : BitVec n) :
+  BitVec.ofFin x ≤ y ↔ x ≤ y.toFin := Iff.rfl
+@[simp] theorem ofNat_le_ofNat {n} (x y : Nat) : (x#n) ≤ (y#n) ↔ x % 2^n ≤ y % 2^n := by
+  simp [le_def]
+
+theorem lt_def (x y : BitVec n) :
+  x < y ↔ x.toNat < y.toNat := Iff.rfl
+
+@[simp] theorem lt_ofFin (x : BitVec n) (y : Fin (2^n)) :
+  x < BitVec.ofFin y ↔ x.toFin < y := Iff.rfl
+@[simp] theorem ofFin_lt (x : Fin (2^n)) (y : BitVec n) :
+  BitVec.ofFin x < y ↔ x < y.toFin := Iff.rfl
+@[simp] theorem ofNat_lt_ofNat {n} (x y : Nat) : (x#n) < (y#n) ↔ x % 2^n < y % 2^n := by
+  simp [lt_def]
+
+protected theorem lt_of_le_ne (x y : BitVec n) (h1 : x <= y) (h2 : ¬ x = y) : x < y := by
+  revert h1 h2
+  let ⟨x, lt⟩ := x
+  let ⟨y, lt⟩ := y
+  simp
+  exact Nat.lt_of_le_of_ne

src/Init/Data/Bool.lean

@@ -0,0 +1,231 @@
+/-
+Copyright (c) 2023 F. G. Dorais. No rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: F. G. Dorais
+-/
+prelude
+import Init.BinderPredicates
+
+/-- Boolean exclusive or -/
+abbrev xor : Bool → Bool → Bool := bne
+
+namespace Bool
+
+/- Namespaced versions that can be used instead of prefixing `_root_` -/
+@[inherit_doc not] protected abbrev not := not
+@[inherit_doc or]  protected abbrev or  := or
+@[inherit_doc and] protected abbrev and := and
+@[inherit_doc xor] protected abbrev xor := xor
+
+instance (p : Bool → Prop) [inst : DecidablePred p] : Decidable (∀ x, p x) :=
+  match inst true, inst false with
+  | isFalse ht, _ => isFalse fun h => absurd (h _) ht
+  | _, isFalse hf => isFalse fun h => absurd (h _) hf
+  | isTrue ht, isTrue hf => isTrue fun | true => ht | false => hf
+
+instance (p : Bool → Prop) [inst : DecidablePred p] : Decidable (∃ x, p x) :=
+  match inst true, inst false with
+  | isTrue ht, _ => isTrue ⟨_, ht⟩
+  | _, isTrue hf => isTrue ⟨_, hf⟩
+  | isFalse ht, isFalse hf => isFalse fun | ⟨true, h⟩ => absurd h ht | ⟨false, h⟩ => absurd h hf
+
+instance : LE Bool := ⟨(. → .)⟩
+instance : LT Bool := ⟨(!. && .)⟩
+
+instance (x y : Bool) : Decidable (x ≤ y) := inferInstanceAs (Decidable (x → y))
+instance (x y : Bool) : Decidable (x < y) := inferInstanceAs (Decidable (!x && y))
+
+instance : Max Bool := ⟨or⟩
+instance : Min Bool := ⟨and⟩
+
+theorem false_ne_true : false ≠ true := Bool.noConfusion
+
+theorem eq_false_or_eq_true : (b : Bool) → b = true ∨ b = false := by decide
+
+theorem eq_false_iff : {b : Bool} → b = false ↔ b ≠ true := by decide
+
+theorem ne_false_iff : {b : Bool} → b ≠ false ↔ b = true := by decide
+
+theorem eq_iff_iff {a b : Bool} : a = b ↔ (a ↔ b) := by cases b <;> simp
+
+/-! ### and -/
+
+@[simp] theorem not_and_self : ∀ (x : Bool), (!x && x) = false := by decide
+
+@[simp] theorem and_not_self : ∀ (x : Bool), (x && !x) = false := by decide
+
+theorem and_comm : ∀ (x y : Bool), (x && y) = (y && x) := by decide
+
+theorem and_left_comm : ∀ (x y z : Bool), (x && (y && z)) = (y && (x && z)) := by decide
+
+theorem and_right_comm : ∀ (x y z : Bool), ((x && y) && z) = ((x && z) && y) := by decide
+
+theorem and_or_distrib_left : ∀ (x y z : Bool), (x && (y || z)) = ((x && y) || (x && z)) := by
+  decide
+
+theorem and_or_distrib_right : ∀ (x y z : Bool), ((x || y) && z) = ((x && z) || (y && z)) := by
+  decide
+
+theorem and_xor_distrib_left : ∀ (x y z : Bool), (x && xor y z) = xor (x && y) (x && z) := by decide
+
+theorem and_xor_distrib_right : ∀ (x y z : Bool), (xor x y && z) = xor (x && z) (y && z) := by
+  decide
+
+/-- De Morgan's law for boolean and -/
+theorem not_and : ∀ (x y : Bool), (!(x && y)) = (!x || !y) := by decide
+
+theorem and_eq_true_iff : ∀ (x y : Bool), (x && y) = true ↔ x = true ∧ y = true := by decide
+
+theorem and_eq_false_iff : ∀ (x y : Bool), (x && y) = false ↔ x = false ∨ y = false := by decide
+
+/-! ### or -/
+
+@[simp] theorem not_or_self : ∀ (x : Bool), (!x || x) = true := by decide
+
+@[simp] theorem or_not_self : ∀ (x : Bool), (x || !x) = true := by decide
+
+theorem or_comm : ∀ (x y : Bool), (x || y) = (y || x) := by decide
+
+theorem or_left_comm : ∀ (x y z : Bool), (x || (y || z)) = (y || (x || z)) := by decide
+
+theorem or_right_comm : ∀ (x y z : Bool), ((x || y) || z) = ((x || z) || y) := by decide
+
+theorem or_and_distrib_left : ∀ (x y z : Bool), (x || (y && z)) = ((x || y) && (x || z)) := by
+  decide
+
+theorem or_and_distrib_right : ∀ (x y z : Bool), ((x && y) || z) = ((x || z) && (y || z)) := by
+  decide
+
+/-- De Morgan's law for boolean or -/
+theorem not_or : ∀ (x y : Bool), (!(x || y)) = (!x && !y) := by decide
+
+theorem or_eq_true_iff : ∀ (x y : Bool), (x || y) = true ↔ x = true ∨ y = true := by decide
+
+theorem or_eq_false_iff : ∀ (x y : Bool), (x || y) = false ↔ x = false ∧ y = false := by decide
+
+/-! ### xor -/
+
+@[simp] theorem false_xor : ∀ (x : Bool), xor false x = x := by decide
+
+@[simp] theorem xor_false : ∀ (x : Bool), xor x false = x := by decide
+
+@[simp] theorem true_xor : ∀ (x : Bool), xor true x = !x := by decide
+
+@[simp] theorem xor_true : ∀ (x : Bool), xor x true = !x := by decide
+
+@[simp] theorem not_xor_self : ∀ (x : Bool), xor (!x) x = true := by decide
+
+@[simp] theorem xor_not_self : ∀ (x : Bool), xor x (!x) = true := by decide
+
+theorem not_xor : ∀ (x y : Bool), xor (!x) y = !(xor x y) := by decide
+
+theorem xor_not : ∀ (x y : Bool), xor x (!y) = !(xor x y) := by decide
+
+@[simp] theorem not_xor_not : ∀ (x y : Bool), xor (!x) (!y) = (xor x y) := by decide
+
+theorem xor_self : ∀ (x : Bool), xor x x = false := by decide
+
+theorem xor_comm : ∀ (x y : Bool), xor x y = xor y x := by decide
+
+theorem xor_left_comm : ∀ (x y z : Bool), xor x (xor y z) = xor y (xor x z) := by decide
+
+theorem xor_right_comm : ∀ (x y z : Bool), xor (xor x y) z = xor (xor x z) y := by decide
+
+theorem xor_assoc : ∀ (x y z : Bool), xor (xor x y) z = xor x (xor y z) := by decide
+
+@[simp]
+theorem xor_left_inj : ∀ (x y z : Bool), xor x y = xor x z ↔ y = z := by decide
+
+@[simp]
+theorem xor_right_inj : ∀ (x y z : Bool), xor x z = xor y z ↔ x = y := by decide
+
+/-! ### le/lt -/
+
+@[simp] protected theorem le_true : ∀ (x : Bool), x ≤ true := by decide
+
+@[simp] protected theorem false_le : ∀ (x : Bool), false ≤ x := by decide
+
+@[simp] protected theorem le_refl : ∀ (x : Bool), x ≤ x := by decide
+
+@[simp] protected theorem lt_irrefl : ∀ (x : Bool), ¬ x < x := by decide
+
+protected theorem le_trans : ∀ {x y z : Bool}, x ≤ y → y ≤ z → x ≤ z := by decide
+
+protected theorem le_antisymm : ∀ {x y : Bool}, x ≤ y → y ≤ x → x = y := by decide
+
+protected theorem le_total : ∀ (x y : Bool), x ≤ y ∨ y ≤ x := by decide
+
+protected theorem lt_asymm : ∀ {x y : Bool}, x < y → ¬ y < x := by decide
+
+protected theorem lt_trans : ∀ {x y z : Bool}, x < y → y < z → x < z := by decide
+
+protected theorem lt_iff_le_not_le : ∀ {x y : Bool}, x < y ↔ x ≤ y ∧ ¬ y ≤ x := by decide
+
+protected theorem lt_of_le_of_lt : ∀ {x y z : Bool}, x ≤ y → y < z → x < z := by decide
+
+protected theorem lt_of_lt_of_le : ∀ {x y z : Bool}, x < y → y ≤ z → x < z := by decide
+
+protected theorem le_of_lt : ∀ {x y : Bool}, x < y → x ≤ y := by decide
+
+protected theorem le_of_eq : ∀ {x y : Bool}, x = y → x ≤ y := by decide
+
+protected theorem ne_of_lt : ∀ {x y : Bool}, x < y → x ≠ y := by decide
+
+protected theorem lt_of_le_of_ne : ∀ {x y : Bool}, x ≤ y → x ≠ y → x < y := by decide
+
+protected theorem le_of_lt_or_eq : ∀ {x y : Bool}, x < y ∨ x = y → x ≤ y := by decide
+
+protected theorem eq_true_of_true_le : ∀ {x : Bool}, true ≤ x → x = true := by decide
+
+protected theorem eq_false_of_le_false : ∀ {x : Bool}, x ≤ false → x = false := by decide
+
+/-! ### min/max -/
+
+@[simp] protected theorem max_eq_or : max = or := rfl
+
+@[simp] protected theorem min_eq_and : min = and := rfl
+
+/-! ### injectivity lemmas -/
+
+theorem not_inj : ∀ {x y : Bool}, (!x) = (!y) → x = y := by decide
+
+theorem not_inj_iff : ∀ {x y : Bool}, (!x) = (!y) ↔ x = y := by decide
+
+theorem and_or_inj_right : ∀ {m x y : Bool}, (x && m) = (y && m) → (x || m) = (y || m) → x = y := by
+  decide
+
+theorem and_or_inj_right_iff :
+    ∀ {m x y : Bool}, (x && m) = (y && m) ∧ (x || m) = (y || m) ↔ x = y := by decide
+
+theorem and_or_inj_left : ∀ {m x y : Bool}, (m && x) = (m && y) → (m || x) = (m || y) → x = y := by
+  decide
+
+theorem and_or_inj_left_iff :
+    ∀ {m x y : Bool}, (m && x) = (m && y) ∧ (m || x) = (m || y) ↔ x = y := by decide
+
+/-! ## toNat -/
+
+/-- convert a `Bool` to a `Nat`, `false -> 0`, `true -> 1` -/
+def toNat (b:Bool) : Nat := cond b 1 0
+
+@[simp] theorem toNat_false : false.toNat = 0 := rfl
+
+@[simp] theorem toNat_true : true.toNat = 1 := rfl
+
+theorem toNat_le_one (c:Bool) : c.toNat ≤ 1 := by
+  cases c <;> trivial
+
+end Bool
+
+/-! ### cond -/
+
+theorem cond_eq_if : (bif b then x else y) = (if b then x else y) := by
+  cases b <;> simp
+
+/-! ### decide -/
+
+@[simp] theorem false_eq_decide_iff {p : Prop} [h : Decidable p] : false = decide p ↔ ¬p := by
+  cases h with | _ q => simp [q]
+
+@[simp] theorem true_eq_decide_iff {p : Prop} [h : Decidable p] : true = decide p ↔ p := by
+  cases h with | _ q => simp [q]

src/Init/Data/Fin.lean

@@ -6,3 +6,6 @@ Author: Leonardo de Moura
 prelude
 import Init.Data.Fin.Basic
 import Init.Data.Fin.Log2
+import Init.Data.Fin.Iterate
+import Init.Data.Fin.Fold
+import Init.Data.Fin.Lemmas

src/Init/Data/Fin/Basic.lean

@@ -1,11 +1,11 @@
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura
+Author: Leonardo de Moura, Robert Y. Lewis, Keeley Hoek, Mario Carneiro
 -/
 prelude
 import Init.Data.Nat.Div
-import Init.Data.Nat.Bitwise
+import Init.Data.Nat.Bitwise.Basic
 import Init.Coe
 
 open Nat
@@ -117,6 +117,45 @@ theorem modn_lt : ∀ {m : Nat} (i : Fin n), m > 0 → (modn i m).val < m
 theorem val_lt_of_le (i : Fin b) (h : b ≤ n) : i.val < n :=
   Nat.lt_of_lt_of_le i.isLt h
 
+protected theorem pos (i : Fin n) : 0 < n :=
+  Nat.lt_of_le_of_lt (Nat.zero_le _) i.2
+
+/-- The greatest value of `Fin (n+1)`. -/
+@[inline] def last (n : Nat) : Fin (n + 1) := ⟨n, n.lt_succ_self⟩
+
+/-- `castLT i h` embeds `i` into a `Fin` where `h` proves it belongs into.  -/
+@[inline] def castLT (i : Fin m) (h : i.1 < n) : Fin n := ⟨i.1, h⟩
+
+/-- `castLE h i` embeds `i` into a larger `Fin` type.  -/
+@[inline] def castLE (h : n ≤ m) (i : Fin n) : Fin m := ⟨i, Nat.lt_of_lt_of_le i.2 h⟩
+
+/-- `cast eq i` embeds `i` into an equal `Fin` type. -/
+@[inline] def cast (eq : n = m) (i : Fin n) : Fin m := ⟨i, eq ▸ i.2⟩
+
+/-- `castAdd m i` embeds `i : Fin n` in `Fin (n+m)`. See also `Fin.natAdd` and `Fin.addNat`. -/
+@[inline] def castAdd (m) : Fin n → Fin (n + m) :=
+  castLE <| Nat.le_add_right n m
+
+/-- `castSucc i` embeds `i : Fin n` in `Fin (n+1)`. -/
+@[inline] def castSucc : Fin n → Fin (n + 1) := castAdd 1
+
+/-- `addNat m i` adds `m` to `i`, generalizes `Fin.succ`. -/
+def addNat (i : Fin n) (m) : Fin (n + m) := ⟨i + m, Nat.add_lt_add_right i.2 _⟩
+
+/-- `natAdd n i` adds `n` to `i` "on the left". -/
+def natAdd (n) (i : Fin m) : Fin (n + m) := ⟨n + i, Nat.add_lt_add_left i.2 _⟩
+
+/-- Maps `0` to `n-1`, `1` to `n-2`, ..., `n-1` to `0`. -/
+@[inline] def rev (i : Fin n) : Fin n := ⟨n - (i + 1), Nat.sub_lt i.pos (Nat.succ_pos _)⟩
+
+/-- `subNat i h` subtracts `m` from `i`, generalizes `Fin.pred`. -/
+@[inline] def subNat (m) (i : Fin (n + m)) (h : m ≤ i) : Fin n :=
+  ⟨i - m, Nat.sub_lt_right_of_lt_add h i.2⟩
+
+/-- Predecessor of a nonzero element of `Fin (n+1)`. -/
+@[inline] def pred {n : Nat} (i : Fin (n + 1)) (h : i ≠ 0) : Fin n :=
+  subNat 1 i <| Nat.pos_of_ne_zero <| mt (Fin.eq_of_val_eq (j := 0)) h
+
 end Fin
 
 instance [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where

src/Init/Data/Fin/Fold.lean

@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2023 François G. Dorais. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: François G. Dorais
+-/
+prelude
+import Init.Data.Nat.Linear
+
+/-- Folds over `Fin n` from the left: `foldl 3 f x = f (f (f x 0) 1) 2`. -/
+@[inline] def foldl (n) (f : α → Fin n → α) (init : α) : α := loop init 0 where
+  /-- Inner loop for `Fin.foldl`. `Fin.foldl.loop n f x i = f (f (f x i) ...) (n-1)`  -/
+  loop (x : α) (i : Nat) : α :=
+    if h : i < n then loop (f x ⟨i, h⟩) (i+1) else x
+  termination_by n - i
+
+/-- Folds over `Fin n` from the right: `foldr 3 f x = f 0 (f 1 (f 2 x))`. -/
+@[inline] def foldr (n) (f : Fin n → α → α) (init : α) : α := loop ⟨n, Nat.le_refl n⟩ init where
+  /-- Inner loop for `Fin.foldr`. `Fin.foldr.loop n f i x = f 0 (f ... (f (i-1) x))`  -/
+  loop : {i // i ≤ n} → α → α
+  | ⟨0, _⟩, x => x
+  | ⟨i+1, h⟩, x => loop ⟨i, Nat.le_of_lt h⟩ (f ⟨i, h⟩ x)

src/Init/Data/Fin/Iterate.lean

@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2023 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joe Hendrix
+-/
+prelude
+import Init.PropLemmas
+import Init.Data.Fin.Basic
+
+namespace Fin
+
+/--
+`hIterateFrom f i bnd a` applies `f` over indices `[i:n]` to compute `P n`
+from `P i`.
+
+See `hIterate` below for more details.
+-/
+def hIterateFrom (P : Nat → Sort _) {n} (f : ∀(i : Fin n), P i.val → P (i.val+1))
+      (i : Nat) (ubnd : i ≤ n) (a : P i) : P n :=
+  if g : i < n then
+    hIterateFrom P f (i+1) g (f ⟨i, g⟩ a)
+  else
+    have p : i = n := (or_iff_left g).mp (Nat.eq_or_lt_of_le ubnd)
+    _root_.cast (congrArg P p) a
+  termination_by n - i
+
+/--
+`hIterate` is a heterogenous iterative operation that applies a
+index-dependent function `f` to a value `init : P start` a total of
+`stop - start` times to produce a value of type `P stop`.
+
+Concretely, `hIterate start stop f init` is equal to
+```lean
+  init |> f start _ |> f (start+1) _ ... |> f (end-1) _
+```
+
+Because it is heterogenous and must return a value of type `P stop`,
+`hIterate` requires proof that `start ≤ stop`.
+
+One can prove properties of `hIterate` using the general theorem
+`hIterate_elim` or other more specialized theorems.
+ -/
+def hIterate (P : Nat → Sort _) {n : Nat} (init : P 0) (f : ∀(i : Fin n), P i.val → P (i.val+1)) :
+    P n :=
+  hIterateFrom P f 0 (Nat.zero_le n) init
+
+private theorem hIterateFrom_elim {P : Nat → Sort _}(Q : ∀(i : Nat), P i → Prop)
+    {n  : Nat}
+    (f : ∀(i : Fin n), P i.val → P (i.val+1))
+    {i : Nat} (ubnd : i ≤ n)
+    (s : P i)
+    (init : Q i s)
+    (step : ∀(k : Fin n) (s : P k.val), Q k.val s → Q (k.val+1) (f k s)) :
+    Q n (hIterateFrom P f i ubnd s) := by
+  let ⟨j, p⟩ := Nat.le.dest ubnd
+  induction j generalizing i ubnd init with
+  | zero =>
+    unfold hIterateFrom
+    have g : ¬ (i < n) := by simp at p; simp [p]
+    have r : Q n (_root_.cast (congrArg P p) s) :=
+      @Eq.rec Nat i (fun k eq => Q k (_root_.cast (congrArg P eq) s)) init n p
+    simp only [g, r, dite_false]
+  | succ j inv =>
+    unfold hIterateFrom
+    have d : Nat.succ i + j = n := by simp [Nat.succ_add]; exact p
+    have g : i < n := Nat.le.intro d
+    simp only [g]
+    exact inv _ _ (step ⟨i,g⟩ s init) d
+
+/-
+`hIterate_elim` provides a mechanism for showing that the result of
+`hIterate` satisifies a property `Q stop` by showing that the states
+at the intermediate indices `i : start ≤ i < stop` satisfy `Q i`.
+-/
+theorem hIterate_elim {P : Nat → Sort _} (Q : ∀(i : Nat), P i → Prop)
+    {n : Nat} (f : ∀(i : Fin n), P i.val → P (i.val+1)) (s : P 0) (init : Q 0 s)
+    (step : ∀(k : Fin n) (s : P k.val), Q k.val s → Q (k.val+1) (f k s)) :
+    Q n (hIterate P s f) := by
+  exact hIterateFrom_elim _ _ _ _ init step
+
+/-
+`hIterate_eq`provides a mechanism for replacing `hIterate P s f` with a
+function `state` showing that matches the steps performed by `hIterate`.
+
+This allows rewriting incremental code using `hIterate` with a
+non-incremental state function.
+-/
+theorem hIterate_eq {P : Nat → Sort _} (state : ∀(i : Nat), P i)
+    {n : Nat} (f : ∀(i : Fin n), P i.val → P (i.val+1)) (s : P 0)
+    (init : s = state 0)
+    (step : ∀(i : Fin n), f i (state i) = state (i+1)) :
+    hIterate P s f = state n := by
+  apply hIterate_elim (fun i s => s = state i) f s init
+  intro i s s_eq
+  simp only [s_eq, step]

src/Init/Data/Fin/Lemmas.lean

@@ -0,0 +1,830 @@
+/-
+Copyright (c) 2022 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+prelude
+import Init.Data.Fin.Basic
+import Init.Data.Nat.Lemmas
+import Init.Ext
+import Init.ByCases
+import Init.Conv
+import Init.Omega
+
+namespace Fin
+
+/-- If you actually have an element of `Fin n`, then the `n` is always positive -/
+theorem size_pos (i : Fin n) : 0 < n := Nat.lt_of_le_of_lt (Nat.zero_le _) i.2
+
+theorem mod_def (a m : Fin n) : a % m = Fin.mk (a % m) (Nat.lt_of_le_of_lt (Nat.mod_le _ _) a.2) :=
+  rfl
+
+theorem mul_def (a b : Fin n) : a * b = Fin.mk ((a * b) % n) (Nat.mod_lt _ a.size_pos) := rfl
+
+theorem sub_def (a b : Fin n) : a - b = Fin.mk ((a + (n - b)) % n) (Nat.mod_lt _ a.size_pos) := rfl
+
+theorem size_pos' : ∀ [Nonempty (Fin n)], 0 < n | ⟨i⟩ => i.size_pos
+
+@[simp] theorem is_lt (a : Fin n) : (a : Nat) < n := a.2
+
+theorem pos_iff_nonempty {n : Nat} : 0 < n ↔ Nonempty (Fin n) :=
+  ⟨fun h => ⟨⟨0, h⟩⟩, fun ⟨i⟩ => i.pos⟩
+
+/-! ### coercions and constructions -/
+
+@[simp] protected theorem eta (a : Fin n) (h : a < n) : (⟨a, h⟩ : Fin n) = a := rfl
+
+@[ext] theorem ext {a b : Fin n} (h : (a : Nat) = b) : a = b := eq_of_val_eq h
+
+theorem val_inj {a b : Fin n} : a.1 = b.1 ↔ a = b := ⟨Fin.eq_of_val_eq, Fin.val_eq_of_eq⟩
+
+theorem ext_iff {a b : Fin n} : a = b ↔ a.1 = b.1 := val_inj.symm
+
+theorem val_ne_iff {a b : Fin n} : a.1 ≠ b.1 ↔ a ≠ b := not_congr val_inj
+
+theorem exists_iff {p : Fin n → Prop} : (∃ i, p i) ↔ ∃ i h, p ⟨i, h⟩ :=
+  ⟨fun ⟨⟨i, hi⟩, hpi⟩ => ⟨i, hi, hpi⟩, fun ⟨i, hi, hpi⟩ => ⟨⟨i, hi⟩, hpi⟩⟩
+
+theorem forall_iff {p : Fin n → Prop} : (∀ i, p i) ↔ ∀ i h, p ⟨i, h⟩ :=
+  ⟨fun h i hi => h ⟨i, hi⟩, fun h ⟨i, hi⟩ => h i hi⟩
+
+protected theorem mk.inj_iff {n a b : Nat} {ha : a < n} {hb : b < n} :
+    (⟨a, ha⟩ : Fin n) = ⟨b, hb⟩ ↔ a = b := ext_iff
+
+theorem val_mk {m n : Nat} (h : m < n) : (⟨m, h⟩ : Fin n).val = m := rfl
+
+theorem eq_mk_iff_val_eq {a : Fin n} {k : Nat} {hk : k < n} :
+    a = ⟨k, hk⟩ ↔ (a : Nat) = k := ext_iff
+
+theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
+
+@[simp] theorem val_ofNat' (a : Nat) (is_pos : n > 0) :
+  (Fin.ofNat' a is_pos).val = a % n := rfl
+
+@[deprecated ofNat'_zero_val] theorem ofNat'_zero_val : (Fin.ofNat' 0 h).val = 0 := Nat.zero_mod _
+
+@[simp] theorem mod_val (a b : Fin n) : (a % b).val = a.val % b.val :=
+  rfl
+
+@[simp] theorem div_val (a b : Fin n) : (a / b).val = a.val / b.val :=
+  rfl
+
+@[simp] theorem modn_val (a : Fin n) (b : Nat) : (a.modn b).val = a.val % b :=
+  rfl
+
+theorem ite_val {n : Nat} {c : Prop} [Decidable c] {x : c → Fin n} (y : ¬c → Fin n) :
+    (if h : c then x h else y h).val = if h : c then (x h).val else (y h).val := by
+  by_cases c <;> simp [*]
+
+theorem dite_val {n : Nat} {c : Prop} [Decidable c] {x y : Fin n} :
+    (if c then x else y).val = if c then x.val else y.val := by
+  by_cases c <;> simp [*]
+
+/-! ### order -/
+
+theorem le_def {a b : Fin n} : a ≤ b ↔ a.1 ≤ b.1 := .rfl
+
+theorem lt_def {a b : Fin n} : a < b ↔ a.1 < b.1 := .rfl
+
+theorem lt_iff_val_lt_val {a b : Fin n} : a < b ↔ a.val < b.val := Iff.rfl
+
+@[simp] protected theorem not_le {a b : Fin n} : ¬ a ≤ b ↔ b < a := Nat.not_le
+
+@[simp] protected theorem not_lt {a b : Fin n} : ¬ a < b ↔ b ≤ a := Nat.not_lt
+
+protected theorem ne_of_lt {a b : Fin n} (h : a < b) : a ≠ b := Fin.ne_of_val_ne (Nat.ne_of_lt h)
+
+protected theorem ne_of_gt {a b : Fin n} (h : a < b) : b ≠ a := Fin.ne_of_val_ne (Nat.ne_of_gt h)
+
+protected theorem le_of_lt {a b : Fin n} (h : a < b) : a ≤ b := Nat.le_of_lt h
+
+theorem is_le (i : Fin (n + 1)) : i ≤ n := Nat.le_of_lt_succ i.is_lt
+
+@[simp] theorem is_le' {a : Fin n} : a ≤ n := Nat.le_of_lt a.is_lt
+
+theorem mk_lt_of_lt_val {b : Fin n} {a : Nat} (h : a < b) :
+    (⟨a, Nat.lt_trans h b.is_lt⟩ : Fin n) < b := h
+
+theorem mk_le_of_le_val {b : Fin n} {a : Nat} (h : a ≤ b) :
+    (⟨a, Nat.lt_of_le_of_lt h b.is_lt⟩ : Fin n) ≤ b := h
+
+@[simp] theorem mk_le_mk {x y : Nat} {hx hy} : (⟨x, hx⟩ : Fin n) ≤ ⟨y, hy⟩ ↔ x ≤ y := .rfl
+
+@[simp] theorem mk_lt_mk {x y : Nat} {hx hy} : (⟨x, hx⟩ : Fin n) < ⟨y, hy⟩ ↔ x < y := .rfl
+
+@[simp] theorem val_zero (n : Nat) : (0 : Fin (n + 1)).1 = 0 := rfl
+
+@[simp] theorem mk_zero : (⟨0, Nat.succ_pos n⟩ : Fin (n + 1)) = 0 := rfl
+
+@[simp] theorem zero_le (a : Fin (n + 1)) : 0 ≤ a := Nat.zero_le a.val
+
+theorem zero_lt_one : (0 : Fin (n + 2)) < 1 := Nat.zero_lt_one
+
+@[simp] theorem not_lt_zero (a : Fin (n + 1)) : ¬a < 0 := nofun
+
+theorem pos_iff_ne_zero {a : Fin (n + 1)} : 0 < a ↔ a ≠ 0 := by
+  rw [lt_def, val_zero, Nat.pos_iff_ne_zero, ← val_ne_iff]; rfl
+
+theorem eq_zero_or_eq_succ {n : Nat} : ∀ i : Fin (n + 1), i = 0 ∨ ∃ j : Fin n, i = j.succ
+  | 0 => .inl rfl
+  | ⟨j + 1, h⟩ => .inr ⟨⟨j, Nat.lt_of_succ_lt_succ h⟩, rfl⟩
+
+theorem eq_succ_of_ne_zero {n : Nat} {i : Fin (n + 1)} (hi : i ≠ 0) : ∃ j : Fin n, i = j.succ :=
+  (eq_zero_or_eq_succ i).resolve_left hi
+
+@[simp] theorem val_rev (i : Fin n) : rev i = n - (i + 1) := rfl
+
+@[simp] theorem rev_rev (i : Fin n) : rev (rev i) = i := ext <| by
+  rw [val_rev, val_rev, ← Nat.sub_sub, Nat.sub_sub_self (by exact i.2), Nat.add_sub_cancel]
+
+@[simp] theorem rev_le_rev {i j : Fin n} : rev i ≤ rev j ↔ j ≤ i := by
+  simp only [le_def, val_rev, Nat.sub_le_sub_iff_left (Nat.succ_le.2 j.is_lt)]
+  exact Nat.succ_le_succ_iff
+
+@[simp] theorem rev_inj {i j : Fin n} : rev i = rev j ↔ i = j :=
+  ⟨fun h => by simpa using congrArg rev h, congrArg _⟩
+
+theorem rev_eq {n a : Nat} (i : Fin (n + 1)) (h : n = a + i) :
+    rev i = ⟨a, Nat.lt_succ_of_le (h ▸ Nat.le_add_right ..)⟩ := by
+  ext; dsimp
+  conv => lhs; congr; rw [h]
+  rw [Nat.add_assoc, Nat.add_sub_cancel]
+
+@[simp] theorem rev_lt_rev {i j : Fin n} : rev i < rev j ↔ j < i := by
+  rw [← Fin.not_le, ← Fin.not_le, rev_le_rev]
+
+@[simp] theorem val_last (n : Nat) : last n = n := rfl
+
+theorem le_last (i : Fin (n + 1)) : i ≤ last n := Nat.le_of_lt_succ i.is_lt
+
+theorem last_pos : (0 : Fin (n + 2)) < last (n + 1) := Nat.succ_pos _
+
+theorem eq_last_of_not_lt {i : Fin (n + 1)} (h : ¬(i : Nat) < n) : i = last n :=
+  ext <| Nat.le_antisymm (le_last i) (Nat.not_lt.1 h)
+
+theorem val_lt_last {i : Fin (n + 1)} : i ≠ last n → (i : Nat) < n :=
+  Decidable.not_imp_comm.1 eq_last_of_not_lt
+
+@[simp] theorem rev_last (n : Nat) : rev (last n) = 0 := ext <| by simp
+
+@[simp] theorem rev_zero (n : Nat) : rev 0 = last n := by
+  rw [← rev_rev (last _), rev_last]
+
+/-! ### addition, numerals, and coercion from Nat -/
+
+@[simp] theorem val_one (n : Nat) : (1 : Fin (n + 2)).val = 1 := rfl
+
+@[simp] theorem mk_one : (⟨1, Nat.succ_lt_succ (Nat.succ_pos n)⟩ : Fin (n + 2)) = (1 : Fin _) := rfl
+
+theorem subsingleton_iff_le_one : Subsingleton (Fin n) ↔ n ≤ 1 := by
+  (match n with | 0 | 1 | n+2 => ?_) <;> try simp
+  · exact ⟨nofun⟩
+  · exact ⟨fun ⟨0, _⟩ ⟨0, _⟩ => rfl⟩
+  · exact iff_of_false (fun h => Fin.ne_of_lt zero_lt_one (h.elim ..)) (of_decide_eq_false rfl)
+
+instance subsingleton_zero : Subsingleton (Fin 0) := subsingleton_iff_le_one.2 (by decide)
+
+instance subsingleton_one : Subsingleton (Fin 1) := subsingleton_iff_le_one.2 (by decide)
+
+theorem fin_one_eq_zero (a : Fin 1) : a = 0 := Subsingleton.elim a 0
+
+theorem add_def (a b : Fin n) : a + b = Fin.mk ((a + b) % n) (Nat.mod_lt _ a.size_pos) := rfl
+
+theorem val_add (a b : Fin n) : (a + b).val = (a.val + b.val) % n := rfl
+
+theorem val_add_one_of_lt {n : Nat} {i : Fin n.succ} (h : i < last _) : (i + 1).1 = i + 1 := by
+  match n with
+  | 0 => cases h
+  | n+1 => rw [val_add, val_one, Nat.mod_eq_of_lt (by exact Nat.succ_lt_succ h)]
+
+@[simp] theorem last_add_one : ∀ n, last n + 1 = 0
+  | 0 => rfl
+  | n + 1 => by ext; rw [val_add, val_zero, val_last, val_one, Nat.mod_self]
+
+theorem val_add_one {n : Nat} (i : Fin (n + 1)) :
+    ((i + 1 : Fin (n + 1)) : Nat) = if i = last _ then (0 : Nat) else i + 1 := by
+  match Nat.eq_or_lt_of_le (le_last i) with
+  | .inl h => cases Fin.eq_of_val_eq h; simp
+  | .inr h => simpa [Fin.ne_of_lt h] using val_add_one_of_lt h
+
+@[simp] theorem val_two {n : Nat} : (2 : Fin (n + 3)).val = 2 := rfl
+
+theorem add_one_pos (i : Fin (n + 1)) (h : i < Fin.last n) : (0 : Fin (n + 1)) < i + 1 := by
+  match n with
+  | 0 => cases h
+  | n+1 =>
+    rw [Fin.lt_def, val_last, ← Nat.add_lt_add_iff_right] at h
+    rw [Fin.lt_def, val_add, val_zero, val_one, Nat.mod_eq_of_lt h]
+    exact Nat.zero_lt_succ _
+
+theorem one_pos : (0 : Fin (n + 2)) < 1 := Nat.succ_pos 0
+
+theorem zero_ne_one : (0 : Fin (n + 2)) ≠ 1 := Fin.ne_of_lt one_pos
+
+/-! ### succ and casts into larger Fin types -/
+
+@[simp] theorem val_succ (j : Fin n) : (j.succ : Nat) = j + 1 := rfl
+
+@[simp] theorem succ_pos (a : Fin n) : (0 : Fin (n + 1)) < a.succ := by
+  simp [Fin.lt_def, Nat.succ_pos]
+
+@[simp] theorem succ_le_succ_iff {a b : Fin n} : a.succ ≤ b.succ ↔ a ≤ b := Nat.succ_le_succ_iff
+
+@[simp] theorem succ_lt_succ_iff {a b : Fin n} : a.succ < b.succ ↔ a < b := Nat.succ_lt_succ_iff
+
+@[simp] theorem succ_inj {a b : Fin n} : a.succ = b.succ ↔ a = b := by
+  refine ⟨fun h => ext ?_, congrArg _⟩
+  apply Nat.le_antisymm <;> exact succ_le_succ_iff.1 (h ▸ Nat.le_refl _)
+
+theorem succ_ne_zero {n} : ∀ k : Fin n, Fin.succ k ≠ 0
+  | ⟨k, _⟩, heq => Nat.succ_ne_zero k <| ext_iff.1 heq
+
+@[simp] theorem succ_zero_eq_one : Fin.succ (0 : Fin (n + 1)) = 1 := rfl
+
+/-- Version of `succ_one_eq_two` to be used by `dsimp` -/
+@[simp] theorem succ_one_eq_two : Fin.succ (1 : Fin (n + 2)) = 2 := rfl
+
+@[simp] theorem succ_mk (n i : Nat) (h : i < n) :
+    Fin.succ ⟨i, h⟩ = ⟨i + 1, Nat.succ_lt_succ h⟩ := rfl
+
+theorem mk_succ_pos (i : Nat) (h : i < n) :
+    (0 : Fin (n + 1)) < ⟨i.succ, Nat.add_lt_add_right h 1⟩ := by
+  rw [lt_def, val_zero]; exact Nat.succ_pos i
+
+theorem one_lt_succ_succ (a : Fin n) : (1 : Fin (n + 2)) < a.succ.succ := by
+  let n+1 := n
+  rw [← succ_zero_eq_one, succ_lt_succ_iff]; exact succ_pos a
+
+@[simp] theorem add_one_lt_iff {n : Nat} {k : Fin (n + 2)} : k + 1 < k ↔ k = last _ := by
+  simp only [lt_def, val_add, val_last, ext_iff]
+  let ⟨k, hk⟩ := k
+  match Nat.eq_or_lt_of_le (Nat.le_of_lt_succ hk) with
+  | .inl h => cases h; simp [Nat.succ_pos]
+  | .inr hk' => simp [Nat.ne_of_lt hk', Nat.mod_eq_of_lt (Nat.succ_lt_succ hk'), Nat.le_succ]
+
+@[simp] theorem add_one_le_iff {n : Nat} : ∀ {k : Fin (n + 1)}, k + 1 ≤ k ↔ k = last _ := by
+  match n with
+  | 0 =>
+    intro (k : Fin 1)
+    exact iff_of_true (Subsingleton.elim (α := Fin 1) (k+1) _ ▸ Nat.le_refl _) (fin_one_eq_zero ..)
+  | n + 1 =>
+    intro (k : Fin (n+2))
+    rw [← add_one_lt_iff, lt_def, le_def, Nat.lt_iff_le_and_ne, and_iff_left]
+    rw [val_add_one]
+    split <;> simp [*, (Nat.succ_ne_zero _).symm, Nat.ne_of_gt (Nat.lt_succ_self _)]
+
+@[simp] theorem last_le_iff {n : Nat} {k : Fin (n + 1)} : last n ≤ k ↔ k = last n := by
+  rw [ext_iff, Nat.le_antisymm_iff, le_def, and_iff_right (by apply le_last)]
+
+@[simp] theorem lt_add_one_iff {n : Nat} {k : Fin (n + 1)} : k < k + 1 ↔ k < last n := by
+  rw [← Decidable.not_iff_not]; simp
+
+@[simp] theorem le_zero_iff {n : Nat} {k : Fin (n + 1)} : k ≤ 0 ↔ k = 0 :=
+  ⟨fun h => Fin.eq_of_val_eq <| Nat.eq_zero_of_le_zero h, (· ▸ Nat.le_refl _)⟩
+
+theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
+  Fin.ne_of_gt (one_lt_succ_succ a)
+
+@[simp] theorem coe_castLT (i : Fin m) (h : i.1 < n) : (castLT i h : Nat) = i := rfl
+
+@[simp] theorem castLT_mk (i n m : Nat) (hn : i < n) (hm : i < m) : castLT ⟨i, hn⟩ hm = ⟨i, hm⟩ :=
+  rfl
+
+@[simp] theorem coe_castLE (h : n ≤ m) (i : Fin n) : (castLE h i : Nat) = i := rfl
+
+@[simp] theorem castLE_mk (i n m : Nat) (hn : i < n) (h : n ≤ m) :
+    castLE h ⟨i, hn⟩ = ⟨i, Nat.lt_of_lt_of_le hn h⟩ := rfl
+
+@[simp] theorem castLE_zero {n m : Nat} (h : n.succ ≤ m.succ) : castLE h 0 = 0 := by simp [ext_iff]
+
+@[simp] theorem castLE_succ {m n : Nat} (h : m + 1 ≤ n + 1) (i : Fin m) :
+    castLE h i.succ = (castLE (Nat.succ_le_succ_iff.mp h) i).succ := by simp [ext_iff]
+
+@[simp] theorem castLE_castLE {k m n} (km : k ≤ m) (mn : m ≤ n) (i : Fin k) :
+    Fin.castLE mn (Fin.castLE km i) = Fin.castLE (Nat.le_trans km mn) i :=
+  Fin.ext (by simp only [coe_castLE])
+
+@[simp] theorem castLE_comp_castLE {k m n} (km : k ≤ m) (mn : m ≤ n) :
+    Fin.castLE mn ∘ Fin.castLE km = Fin.castLE (Nat.le_trans km mn) :=
+  funext (castLE_castLE km mn)
+
+@[simp] theorem coe_cast (h : n = m) (i : Fin n) : (cast h i : Nat) = i := rfl
+
+@[simp] theorem cast_last {n' : Nat} {h : n + 1 = n' + 1} : cast h (last n) = last n' :=
+  ext (by rw [coe_cast, val_last, val_last, Nat.succ.inj h])
+
+@[simp] theorem cast_mk (h : n = m) (i : Nat) (hn : i < n) : cast h ⟨i, hn⟩ = ⟨i, h ▸ hn⟩ := rfl
+
+@[simp] theorem cast_trans {k : Nat} (h : n = m) (h' : m = k) {i : Fin n} :
+    cast h' (cast h i) = cast (Eq.trans h h') i := rfl
+
+theorem castLE_of_eq {m n : Nat} (h : m = n) {h' : m ≤ n} : castLE h' = Fin.cast h := rfl
+
+@[simp] theorem coe_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
+
+@[simp] theorem castAdd_zero : (castAdd 0 : Fin n → Fin (n + 0)) = cast rfl := rfl
+
+theorem castAdd_lt {m : Nat} (n : Nat) (i : Fin m) : (castAdd n i : Nat) < m := by simp
+
+@[simp] theorem castAdd_mk (m : Nat) (i : Nat) (h : i < n) :
+    castAdd m ⟨i, h⟩ = ⟨i, Nat.lt_add_right m h⟩ := rfl
+
+@[simp] theorem castAdd_castLT (m : Nat) (i : Fin (n + m)) (hi : i.val < n) :
+    castAdd m (castLT i hi) = i := rfl
+
+@[simp] theorem castLT_castAdd (m : Nat) (i : Fin n) :
+    castLT (castAdd m i) (castAdd_lt m i) = i := rfl
+
+/-- For rewriting in the reverse direction, see `Fin.cast_castAdd_left`. -/
+theorem castAdd_cast {n n' : Nat} (m : Nat) (i : Fin n') (h : n' = n) :
+    castAdd m (Fin.cast h i) = Fin.cast (congrArg (. + m) h) (castAdd m i) := ext rfl
+
+theorem cast_castAdd_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
+    cast h (castAdd m i) = castAdd m (cast (Nat.add_right_cancel h) i) := rfl
+
+@[simp] theorem cast_castAdd_right {n m m' : Nat} (i : Fin n) (h : n + m' = n + m) :
+    cast h (castAdd m' i) = castAdd m i := rfl
+
+theorem castAdd_castAdd {m n p : Nat} (i : Fin m) :
+    castAdd p (castAdd n i) = cast (Nat.add_assoc ..).symm (castAdd (n + p) i) := rfl
+
+/-- The cast of the successor is the successor of the cast. See `Fin.succ_cast_eq` for rewriting in
+the reverse direction. -/
+@[simp] theorem cast_succ_eq {n' : Nat} (i : Fin n) (h : n.succ = n'.succ) :
+    cast h i.succ = (cast (Nat.succ.inj h) i).succ := rfl
+
+theorem succ_cast_eq {n' : Nat} (i : Fin n) (h : n = n') :
+    (cast h i).succ = cast (by rw [h]) i.succ := rfl
+
+@[simp] theorem coe_castSucc (i : Fin n) : (Fin.castSucc i : Nat) = i := rfl
+
+@[simp] theorem castSucc_mk (n i : Nat) (h : i < n) : castSucc ⟨i, h⟩ = ⟨i, Nat.lt.step h⟩ := rfl
+
+@[simp] theorem cast_castSucc {n' : Nat} {h : n + 1 = n' + 1} {i : Fin n} :
+    cast h (castSucc i) = castSucc (cast (Nat.succ.inj h) i) := rfl
+
+theorem castSucc_lt_succ (i : Fin n) : Fin.castSucc i < i.succ :=
+  lt_def.2 <| by simp only [coe_castSucc, val_succ, Nat.lt_succ_self]
+
+theorem le_castSucc_iff {i : Fin (n + 1)} {j : Fin n} : i ≤ Fin.castSucc j ↔ i < j.succ := by
+  simpa [lt_def, le_def] using Nat.succ_le_succ_iff.symm
+
+theorem castSucc_lt_iff_succ_le {n : Nat} {i : Fin n} {j : Fin (n + 1)} :
+    Fin.castSucc i < j ↔ i.succ ≤ j := .rfl
+
+@[simp] theorem succ_last (n : Nat) : (last n).succ = last n.succ := rfl
+
+@[simp] theorem succ_eq_last_succ {n : Nat} (i : Fin n.succ) :
+    i.succ = last (n + 1) ↔ i = last n := by rw [← succ_last, succ_inj]
+
+@[simp] theorem castSucc_castLT (i : Fin (n + 1)) (h : (i : Nat) < n) :
+    castSucc (castLT i h) = i := rfl
+
+@[simp] theorem castLT_castSucc {n : Nat} (a : Fin n) (h : (a : Nat) < n) :
+    castLT (castSucc a) h = a := rfl
+
+@[simp] theorem castSucc_lt_castSucc_iff {a b : Fin n} :
+    Fin.castSucc a < Fin.castSucc b ↔ a < b := .rfl
+
+theorem castSucc_inj {a b : Fin n} : castSucc a = castSucc b ↔ a = b := by simp [ext_iff]
+
+theorem castSucc_lt_last (a : Fin n) : castSucc a < last n := a.is_lt
+
+@[simp] theorem castSucc_zero : castSucc (0 : Fin (n + 1)) = 0 := rfl
+
+@[simp] theorem castSucc_one {n : Nat} : castSucc (1 : Fin (n + 2)) = 1 := rfl
+
+/-- `castSucc i` is positive when `i` is positive -/
+theorem castSucc_pos {i : Fin (n + 1)} (h : 0 < i) : 0 < castSucc i := by
+  simpa [lt_def] using h
+
+@[simp] theorem castSucc_eq_zero_iff (a : Fin (n + 1)) : castSucc a = 0 ↔ a = 0 := by simp [ext_iff]
+
+theorem castSucc_ne_zero_iff (a : Fin (n + 1)) : castSucc a ≠ 0 ↔ a ≠ 0 :=
+  not_congr <| castSucc_eq_zero_iff a
+
+theorem castSucc_fin_succ (n : Nat) (j : Fin n) :
+    castSucc (Fin.succ j) = Fin.succ (castSucc j) := by simp [Fin.ext_iff]
+
+@[simp]
+theorem coeSucc_eq_succ {a : Fin n} : castSucc a + 1 = a.succ := by
+  cases n
+  · exact a.elim0
+  · simp [ext_iff, add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ a.is_lt)]
+
+theorem lt_succ {a : Fin n} : castSucc a < a.succ := by
+  rw [castSucc, lt_def, coe_castAdd, val_succ]; exact Nat.lt_succ_self a.val
+
+theorem exists_castSucc_eq {n : Nat} {i : Fin (n + 1)} : (∃ j, castSucc j = i) ↔ i ≠ last n :=
+  ⟨fun ⟨j, hj⟩ => hj ▸ Fin.ne_of_lt j.castSucc_lt_last,
+   fun hi => ⟨i.castLT <| Fin.val_lt_last hi, rfl⟩⟩
+
+theorem succ_castSucc {n : Nat} (i : Fin n) : i.castSucc.succ = castSucc i.succ := rfl
+
+@[simp] theorem coe_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
+
+@[simp] theorem addNat_one {i : Fin n} : addNat i 1 = i.succ := rfl
+
+theorem le_coe_addNat (m : Nat) (i : Fin n) : m ≤ addNat i m :=
+  Nat.le_add_left _ _
+
+@[simp] theorem addNat_mk (n i : Nat) (hi : i < m) :
+    addNat ⟨i, hi⟩ n = ⟨i + n, Nat.add_lt_add_right hi n⟩ := rfl
+
+@[simp] theorem cast_addNat_zero {n n' : Nat} (i : Fin n) (h : n + 0 = n') :
+    cast h (addNat i 0) = cast ((Nat.add_zero _).symm.trans h) i := rfl
+
+/-- For rewriting in the reverse direction, see `Fin.cast_addNat_left`. -/
+theorem addNat_cast {n n' m : Nat} (i : Fin n') (h : n' = n) :
+    addNat (cast h i) m = cast (congrArg (. + m) h) (addNat i m) := rfl
+
+theorem cast_addNat_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
+    cast h (addNat i m) = addNat (cast (Nat.add_right_cancel h) i) m := rfl
+
+@[simp] theorem cast_addNat_right {n m m' : Nat} (i : Fin n) (h : n + m' = n + m) :
+    cast h (addNat i m') = addNat i m :=
+  ext <| (congrArg ((· + ·) (i : Nat)) (Nat.add_left_cancel h) : _)
+
+@[simp] theorem coe_natAdd (n : Nat) {m : Nat} (i : Fin m) : (natAdd n i : Nat) = n + i := rfl
+
+@[simp] theorem natAdd_mk (n i : Nat) (hi : i < m) :
+    natAdd n ⟨i, hi⟩ = ⟨n + i, Nat.add_lt_add_left hi n⟩ := rfl
+
+theorem le_coe_natAdd (m : Nat) (i : Fin n) : m ≤ natAdd m i := Nat.le_add_right ..
+
+theorem natAdd_zero {n : Nat} : natAdd 0 = cast (Nat.zero_add n).symm := by ext; simp
+
+/-- For rewriting in the reverse direction, see `Fin.cast_natAdd_right`. -/
+theorem natAdd_cast {n n' : Nat} (m : Nat) (i : Fin n') (h : n' = n) :
+    natAdd m (cast h i) = cast (congrArg _ h) (natAdd m i) := rfl
+
+theorem cast_natAdd_right {n n' m : Nat} (i : Fin n') (h : m + n' = m + n) :
+    cast h (natAdd m i) = natAdd m (cast (Nat.add_left_cancel h) i) := rfl
+
+@[simp] theorem cast_natAdd_left {n m m' : Nat} (i : Fin n) (h : m' + n = m + n) :
+    cast h (natAdd m' i) = natAdd m i :=
+  ext <| (congrArg (· + (i : Nat)) (Nat.add_right_cancel h) : _)
+
+theorem castAdd_natAdd (p m : Nat) {n : Nat} (i : Fin n) :
+    castAdd p (natAdd m i) = cast (Nat.add_assoc ..).symm (natAdd m (castAdd p i)) := rfl
+
+theorem natAdd_castAdd (p m : Nat) {n : Nat} (i : Fin n) :
+    natAdd m (castAdd p i) = cast (Nat.add_assoc ..) (castAdd p (natAdd m i)) := rfl
+
+theorem natAdd_natAdd (m n : Nat) {p : Nat} (i : Fin p) :
+    natAdd m (natAdd n i) = cast (Nat.add_assoc ..) (natAdd (m + n) i) :=
+  ext <| (Nat.add_assoc ..).symm
+
+@[simp]
+theorem cast_natAdd_zero {n n' : Nat} (i : Fin n) (h : 0 + n = n') :
+    cast h (natAdd 0 i) = cast ((Nat.zero_add _).symm.trans h) i :=
+  ext <| Nat.zero_add _
+
+@[simp]
+theorem cast_natAdd (n : Nat) {m : Nat} (i : Fin m) :
+    cast (Nat.add_comm ..) (natAdd n i) = addNat i n := ext <| Nat.add_comm ..
+
+@[simp]
+theorem cast_addNat {n : Nat} (m : Nat) (i : Fin n) :
+    cast (Nat.add_comm ..) (addNat i m) = natAdd m i := ext <| Nat.add_comm ..
+
+@[simp] theorem natAdd_last {m n : Nat} : natAdd n (last m) = last (n + m) := rfl
+
+theorem natAdd_castSucc {m n : Nat} {i : Fin m} : natAdd n (castSucc i) = castSucc (natAdd n i) :=
+  rfl
+
+theorem rev_castAdd (k : Fin n) (m : Nat) : rev (castAdd m k) = addNat (rev k) m := ext <| by
+  rw [val_rev, coe_castAdd, coe_addNat, val_rev, Nat.sub_add_comm (Nat.succ_le_of_lt k.is_lt)]
+
+theorem rev_addNat (k : Fin n) (m : Nat) : rev (addNat k m) = castAdd m (rev k) := by
+  rw [← rev_rev (castAdd ..), rev_castAdd, rev_rev]
+
+theorem rev_castSucc (k : Fin n) : rev (castSucc k) = succ (rev k) := k.rev_castAdd 1
+
+theorem rev_succ (k : Fin n) : rev (succ k) = castSucc (rev k) := k.rev_addNat 1
+
+/-! ### pred -/
+
+@[simp] theorem coe_pred (j : Fin (n + 1)) (h : j ≠ 0) : (j.pred h : Nat) = j - 1 := rfl
+
+@[simp] theorem succ_pred : ∀ (i : Fin (n + 1)) (h : i ≠ 0), (i.pred h).succ = i
+  | ⟨0, h⟩, hi => by simp only [mk_zero, ne_eq, not_true] at hi
+  | ⟨n + 1, h⟩, hi => rfl
+
+@[simp]
+theorem pred_succ (i : Fin n) {h : i.succ ≠ 0} : i.succ.pred h = i := by
+  cases i
+  rfl
+
+theorem pred_eq_iff_eq_succ {n : Nat} (i : Fin (n + 1)) (hi : i ≠ 0) (j : Fin n) :
+    i.pred hi = j ↔ i = j.succ :=
+  ⟨fun h => by simp only [← h, Fin.succ_pred], fun h => by simp only [h, Fin.pred_succ]⟩
+
+theorem pred_mk_succ (i : Nat) (h : i < n + 1) :
+    Fin.pred ⟨i + 1, Nat.add_lt_add_right h 1⟩ (ne_of_val_ne (Nat.ne_of_gt (mk_succ_pos i h))) =
+      ⟨i, h⟩ := by
+  simp only [ext_iff, coe_pred, Nat.add_sub_cancel]
+
+@[simp] theorem pred_mk_succ' (i : Nat) (h₁ : i + 1 < n + 1 + 1) (h₂) :
+    Fin.pred ⟨i + 1, h₁⟩ h₂ = ⟨i, Nat.lt_of_succ_lt_succ h₁⟩ := pred_mk_succ i _
+
+-- This is not a simp theorem by default, because `pred_mk_succ` is nicer when it applies.
+theorem pred_mk {n : Nat} (i : Nat) (h : i < n + 1) (w) : Fin.pred ⟨i, h⟩ w =
+    ⟨i - 1, Nat.sub_lt_right_of_lt_add (Nat.pos_iff_ne_zero.2 (Fin.val_ne_of_ne w)) h⟩ :=
+  rfl
+
+@[simp] theorem pred_le_pred_iff {n : Nat} {a b : Fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0} :
+    a.pred ha ≤ b.pred hb ↔ a ≤ b := by rw [← succ_le_succ_iff, succ_pred, succ_pred]
+
+@[simp] theorem pred_lt_pred_iff {n : Nat} {a b : Fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0} :
+    a.pred ha < b.pred hb ↔ a < b := by rw [← succ_lt_succ_iff, succ_pred, succ_pred]
+
+@[simp] theorem pred_inj :
+    ∀ {a b : Fin (n + 1)} {ha : a ≠ 0} {hb : b ≠ 0}, a.pred ha = b.pred hb ↔ a = b
+  | ⟨0, _⟩, _, ha, _ => by simp only [mk_zero, ne_eq, not_true] at ha
+  | ⟨i + 1, _⟩, ⟨0, _⟩, _, hb => by simp only [mk_zero, ne_eq, not_true] at hb
+  | ⟨i + 1, hi⟩, ⟨j + 1, hj⟩, ha, hb => by simp [ext_iff]
+
+@[simp] theorem pred_one {n : Nat} :
+    Fin.pred (1 : Fin (n + 2)) (Ne.symm (Fin.ne_of_lt one_pos)) = 0 := rfl
+
+theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
+    pred (i + 1) (Fin.ne_of_gt (add_one_pos _ (lt_def.2 h))) = castLT i h := by
+  rw [ext_iff, coe_pred, coe_castLT, val_add, val_one, Nat.mod_eq_of_lt, Nat.add_sub_cancel]
+  exact Nat.add_lt_add_right h 1
+
+@[simp] theorem coe_subNat (i : Fin (n + m)) (h : m ≤ i) : (i.subNat m h : Nat) = i - m := rfl
+
+@[simp] theorem subNat_mk {i : Nat} (h₁ : i < n + m) (h₂ : m ≤ i) :
+    subNat m ⟨i, h₁⟩ h₂ = ⟨i - m, Nat.sub_lt_right_of_lt_add h₂ h₁⟩ := rfl
+
+@[simp] theorem pred_castSucc_succ (i : Fin n) :
+    pred (castSucc i.succ) (Fin.ne_of_gt (castSucc_pos i.succ_pos)) = castSucc i := rfl
+
+@[simp] theorem addNat_subNat {i : Fin (n + m)} (h : m ≤ i) : addNat (subNat m i h) m = i :=
+  ext <| Nat.sub_add_cancel h
+
+@[simp] theorem subNat_addNat (i : Fin n) (m : Nat) (h : m ≤ addNat i m := le_coe_addNat m i) :
+    subNat m (addNat i m) h = i := ext <| Nat.add_sub_cancel i m
+
+@[simp] theorem natAdd_subNat_cast {i : Fin (n + m)} (h : n ≤ i) :
+    natAdd n (subNat n (cast (Nat.add_comm ..) i) h) = i := by simp [← cast_addNat]; rfl
+
+/-! ### recursion and induction principles -/
+
+/-- Define `motive n i` by induction on `i : Fin n` interpreted as `(0 : Fin (n - i)).succ.succ…`.
+This function has two arguments: `zero n` defines `0`-th element `motive (n+1) 0` of an
+`(n+1)`-tuple, and `succ n i` defines `(i+1)`-st element of `(n+1)`-tuple based on `n`, `i`, and
+`i`-th element of `n`-tuple. -/
+-- FIXME: Performance review
+@[elab_as_elim] def succRec {motive : ∀ n, Fin n → Sort _}
+    (zero : ∀ n, motive n.succ (0 : Fin (n + 1)))
+    (succ : ∀ n i, motive n i → motive n.succ i.succ) : ∀ {n : Nat} (i : Fin n), motive n i
+  | 0, i => i.elim0
+  | Nat.succ n, ⟨0, _⟩ => by rw [mk_zero]; exact zero n
+  | Nat.succ _, ⟨Nat.succ i, h⟩ => succ _ _ (succRec zero succ ⟨i, Nat.lt_of_succ_lt_succ h⟩)
+
+/-- Define `motive n i` by induction on `i : Fin n` interpreted as `(0 : Fin (n - i)).succ.succ…`.
+This function has two arguments:
+`zero n` defines the `0`-th element `motive (n+1) 0` of an `(n+1)`-tuple, and
+`succ n i` defines the `(i+1)`-st element of an `(n+1)`-tuple based on `n`, `i`,
+and the `i`-th element of an `n`-tuple.
+
+A version of `Fin.succRec` taking `i : Fin n` as the first argument. -/
+-- FIXME: Performance review
+@[elab_as_elim] def succRecOn {n : Nat} (i : Fin n) {motive : ∀ n, Fin n → Sort _}
+    (zero : ∀ n, motive (n + 1) 0) (succ : ∀ n i, motive n i → motive (Nat.succ n) i.succ) :
+    motive n i := i.succRec zero succ
+
+@[simp] theorem succRecOn_zero {motive : ∀ n, Fin n → Sort _} {zero succ} (n) :
+    @Fin.succRecOn (n + 1) 0 motive zero succ = zero n := by
+  cases n <;> rfl
+
+@[simp] theorem succRecOn_succ {motive : ∀ n, Fin n → Sort _} {zero succ} {n} (i : Fin n) :
+    @Fin.succRecOn (n + 1) i.succ motive zero succ = succ n i (Fin.succRecOn i zero succ) := by
+  cases i; rfl
+
+/-- Define `motive i` by induction on `i : Fin (n + 1)` via induction on the underlying `Nat` value.
+This function has two arguments: `zero` handles the base case on `motive 0`,
+and `succ` defines the inductive step using `motive i.castSucc`.
+-/
+-- FIXME: Performance review
+@[elab_as_elim] def induction {motive : Fin (n + 1) → Sort _} (zero : motive 0)
+    (succ : ∀ i : Fin n, motive (castSucc i) → motive i.succ) :
+    ∀ i : Fin (n + 1), motive i
+  | ⟨0, hi⟩ => by rwa [Fin.mk_zero]
+  | ⟨i+1, hi⟩ => succ ⟨i, Nat.lt_of_succ_lt_succ hi⟩ (induction zero succ ⟨i, Nat.lt_of_succ_lt hi⟩)
+
+@[simp] theorem induction_zero {motive : Fin (n + 1) → Sort _} (zero : motive 0)
+    (hs : ∀ i : Fin n, motive (castSucc i) → motive i.succ) :
+    (induction zero hs : ∀ i : Fin (n + 1), motive i) 0 = zero := rfl
+
+@[simp] theorem induction_succ {motive : Fin (n + 1) → Sort _} (zero : motive 0)
+    (succ : ∀ i : Fin n, motive (castSucc i) → motive i.succ) (i : Fin n) :
+    induction (motive := motive) zero succ i.succ = succ i (induction zero succ (castSucc i)) := rfl
+
+/-- Define `motive i` by induction on `i : Fin (n + 1)` via induction on the underlying `Nat` value.
+This function has two arguments: `zero` handles the base case on `motive 0`,
+and `succ` defines the inductive step using `motive i.castSucc`.
+
+A version of `Fin.induction` taking `i : Fin (n + 1)` as the first argument.
+-/
+-- FIXME: Performance review
+@[elab_as_elim] def inductionOn (i : Fin (n + 1)) {motive : Fin (n + 1) → Sort _} (zero : motive 0)
+    (succ : ∀ i : Fin n, motive (castSucc i) → motive i.succ) : motive i := induction zero succ i
+
+/-- Define `f : Π i : Fin n.succ, motive i` by separately handling the cases `i = 0` and
+`i = j.succ`, `j : Fin n`. -/
+@[elab_as_elim] def cases {motive : Fin (n + 1) → Sort _}
+    (zero : motive 0) (succ : ∀ i : Fin n, motive i.succ) :
+    ∀ i : Fin (n + 1), motive i := induction zero fun i _ => succ i
+
+@[simp] theorem cases_zero {n} {motive : Fin (n + 1) → Sort _} {zero succ} :
+    @Fin.cases n motive zero succ 0 = zero := rfl
+
+@[simp] theorem cases_succ {n} {motive : Fin (n + 1) → Sort _} {zero succ} (i : Fin n) :
+    @Fin.cases n motive zero succ i.succ = succ i := rfl
+
+@[simp] theorem cases_succ' {n} {motive : Fin (n + 1) → Sort _} {zero succ}
+    {i : Nat} (h : i + 1 < n + 1) :
+    @Fin.cases n motive zero succ ⟨i.succ, h⟩ = succ ⟨i, Nat.lt_of_succ_lt_succ h⟩ := rfl
+
+theorem forall_fin_succ {P : Fin (n + 1) → Prop} : (∀ i, P i) ↔ P 0 ∧ ∀ i : Fin n, P i.succ :=
+  ⟨fun H => ⟨H 0, fun _ => H _⟩, fun ⟨H0, H1⟩ i => Fin.cases H0 H1 i⟩
+
+theorem exists_fin_succ {P : Fin (n + 1) → Prop} : (∃ i, P i) ↔ P 0 ∨ ∃ i : Fin n, P i.succ :=
+  ⟨fun ⟨i, h⟩ => Fin.cases Or.inl (fun i hi => Or.inr ⟨i, hi⟩) i h, fun h =>
+    (h.elim fun h => ⟨0, h⟩) fun ⟨i, hi⟩ => ⟨i.succ, hi⟩⟩
+
+theorem forall_fin_one {p : Fin 1 → Prop} : (∀ i, p i) ↔ p 0 :=
+  ⟨fun h => h _, fun h i => Subsingleton.elim i 0 ▸ h⟩
+
+theorem exists_fin_one {p : Fin 1 → Prop} : (∃ i, p i) ↔ p 0 :=
+  ⟨fun ⟨i, h⟩ => Subsingleton.elim i 0 ▸ h, fun h => ⟨_, h⟩⟩
+
+theorem forall_fin_two {p : Fin 2 → Prop} : (∀ i, p i) ↔ p 0 ∧ p 1 :=
+  forall_fin_succ.trans <| and_congr_right fun _ => forall_fin_one
+
+theorem exists_fin_two {p : Fin 2 → Prop} : (∃ i, p i) ↔ p 0 ∨ p 1 :=
+  exists_fin_succ.trans <| or_congr_right exists_fin_one
+
+theorem fin_two_eq_of_eq_zero_iff : ∀ {a b : Fin 2}, (a = 0 ↔ b = 0) → a = b := by
+  simp only [forall_fin_two]; decide
+
+/--
+Define `motive i` by reverse induction on `i : Fin (n + 1)` via induction on the underlying `Nat`
+value. This function has two arguments: `last` handles the base case on `motive (Fin.last n)`,
+and `cast` defines the inductive step using `motive i.succ`, inducting downwards.
+-/
+@[elab_as_elim] def reverseInduction {motive : Fin (n + 1) → Sort _} (last : motive (Fin.last n))
+    (cast : ∀ i : Fin n, motive i.succ → motive (castSucc i)) (i : Fin (n + 1)) : motive i :=
+  if hi : i = Fin.last n then _root_.cast (congrArg motive hi.symm) last
+  else
+    let j : Fin n := ⟨i, Nat.lt_of_le_of_ne (Nat.le_of_lt_succ i.2) fun h => hi (Fin.ext h)⟩
+    cast _ (reverseInduction last cast j.succ)
+termination_by n + 1 - i
+decreasing_by decreasing_with
+  -- FIXME: we put the proof down here to avoid getting a dummy `have` in the definition
+  exact Nat.add_sub_add_right .. ▸ Nat.sub_lt_sub_left i.2 (Nat.lt_succ_self i)
+
+@[simp] theorem reverseInduction_last {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} :
+    (reverseInduction zero succ (Fin.last n) : motive (Fin.last n)) = zero := by
+  rw [reverseInduction]; simp; rfl
+
+@[simp] theorem reverseInduction_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ}
+    (i : Fin n) : reverseInduction (motive := motive) zero succ (castSucc i) =
+      succ i (reverseInduction zero succ i.succ) := by
+  rw [reverseInduction, dif_neg (Fin.ne_of_lt (Fin.castSucc_lt_last i))]; rfl
+
+/-- Define `f : Π i : Fin n.succ, motive i` by separately handling the cases `i = Fin.last n` and
+`i = j.castSucc`, `j : Fin n`. -/
+@[elab_as_elim] def lastCases {n : Nat} {motive : Fin (n + 1) → Sort _} (last : motive (Fin.last n))
+    (cast : ∀ i : Fin n, motive (castSucc i)) (i : Fin (n + 1)) : motive i :=
+  reverseInduction last (fun i _ => cast i) i
+
+@[simp] theorem lastCases_last {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast} :
+    (Fin.lastCases last cast (Fin.last n) : motive (Fin.last n)) = last :=
+  reverseInduction_last ..
+
+@[simp] theorem lastCases_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast}
+    (i : Fin n) : (Fin.lastCases last cast (Fin.castSucc i) : motive (Fin.castSucc i)) = cast i :=
+  reverseInduction_castSucc ..
+
+/-- Define `f : Π i : Fin (m + n), motive i` by separately handling the cases `i = castAdd n i`,
+`j : Fin m` and `i = natAdd m j`, `j : Fin n`. -/
+@[elab_as_elim] def addCases {m n : Nat} {motive : Fin (m + n) → Sort u}
+    (left : ∀ i, motive (castAdd n i)) (right : ∀ i, motive (natAdd m i))
+    (i : Fin (m + n)) : motive i :=
+  if hi : (i : Nat) < m then (castAdd_castLT n i hi) ▸ (left (castLT i hi))
+  else (natAdd_subNat_cast (Nat.le_of_not_lt hi)) ▸ (right _)
+
+@[simp] theorem addCases_left {m n : Nat} {motive : Fin (m + n) → Sort _} {left right} (i : Fin m) :
+    addCases (motive := motive) left right (Fin.castAdd n i) = left i := by
+  rw [addCases, dif_pos (castAdd_lt _ _)]; rfl
+
+@[simp]
+theorem addCases_right {m n : Nat} {motive : Fin (m + n) → Sort _} {left right} (i : Fin n) :
+    addCases (motive := motive) left right (natAdd m i) = right i := by
+  have : ¬(natAdd m i : Nat) < m := Nat.not_lt.2 (le_coe_natAdd ..)
+  rw [addCases, dif_neg this]; exact eq_of_heq <| (eqRec_heq _ _).trans (by congr 1; simp)
+
+/-! ### add -/
+
+@[simp] theorem ofNat'_add (x : Nat) (lt : 0 < n) (y : Fin n) :
+    Fin.ofNat' x lt + y = Fin.ofNat' (x + y.val) lt := by
+  apply Fin.eq_of_val_eq
+  simp [Fin.ofNat', Fin.add_def]
+
+@[simp] theorem add_ofNat' (x : Fin n) (y : Nat) (lt : 0 < n) :
+    x + Fin.ofNat' y lt = Fin.ofNat' (x.val + y) lt := by
+  apply Fin.eq_of_val_eq
+  simp [Fin.ofNat', Fin.add_def]
+
+/-! ### sub -/
+
+protected theorem coe_sub (a b : Fin n) : ((a - b : Fin n) : Nat) = (a + (n - b)) % n := by
+  cases a; cases b; rfl
+
+@[simp] theorem ofNat'_sub (x : Nat) (lt : 0 < n) (y : Fin n) :
+    Fin.ofNat' x lt - y = Fin.ofNat' (x + (n - y.val)) lt := by
+  apply Fin.eq_of_val_eq
+  simp [Fin.ofNat', Fin.sub_def]
+
+@[simp] theorem sub_ofNat' (x : Fin n) (y : Nat) (lt : 0 < n) :
+    x - Fin.ofNat' y lt = Fin.ofNat' (x.val + (n - y % n)) lt := by
+  apply Fin.eq_of_val_eq
+  simp [Fin.ofNat', Fin.sub_def]
+
+private theorem _root_.Nat.mod_eq_sub_of_lt_two_mul {x n} (h₁ : n ≤ x) (h₂ : x < 2 * n) :
+    x % n = x - n := by
+  rw [Nat.mod_eq, if_pos (by omega), Nat.mod_eq_of_lt (by omega)]
+
+theorem coe_sub_iff_le {a b : Fin n} : (↑(a - b) : Nat) = a - b ↔ b ≤ a := by
+  rw [sub_def, le_def]
+  dsimp only
+  if h : n ≤ a + (n - b) then
+    rw [Nat.mod_eq_sub_of_lt_two_mul h]
+    all_goals omega
+  else
+    rw [Nat.mod_eq_of_lt]
+    all_goals omega
+
+theorem coe_sub_iff_lt {a b : Fin n} : (↑(a - b) : Nat) = n + a - b ↔ a < b := by
+  rw [sub_def, lt_def]
+  dsimp only
+  if h : n ≤ a + (n - b) then
+    rw [Nat.mod_eq_sub_of_lt_two_mul h]
+    all_goals omega
+  else
+    rw [Nat.mod_eq_of_lt]
+    all_goals omega
+
+/-! ### mul -/
+
+theorem val_mul {n : Nat} : ∀ a b : Fin n, (a * b).val = a.val * b.val % n
+  | ⟨_, _⟩, ⟨_, _⟩ => rfl
+
+theorem coe_mul {n : Nat} : ∀ a b : Fin n, ((a * b : Fin n) : Nat) = a * b % n
+  | ⟨_, _⟩, ⟨_, _⟩ => rfl
+
+protected theorem mul_one (k : Fin (n + 1)) : k * 1 = k := by
+  match n with
+  | 0 => exact Subsingleton.elim (α := Fin 1) ..
+  | n+1 => simp [ext_iff, mul_def, Nat.mod_eq_of_lt (is_lt k)]
+
+protected theorem mul_comm (a b : Fin n) : a * b = b * a :=
+  ext <| by rw [mul_def, mul_def, Nat.mul_comm]
+
+protected theorem one_mul (k : Fin (n + 1)) : (1 : Fin (n + 1)) * k = k := by
+  rw [Fin.mul_comm, Fin.mul_one]
+
+protected theorem mul_zero (k : Fin (n + 1)) : k * 0 = 0 := by simp [ext_iff, mul_def]
+
+protected theorem zero_mul (k : Fin (n + 1)) : (0 : Fin (n + 1)) * k = 0 := by
+  simp [ext_iff, mul_def]
+
+end Fin
+
+namespace USize
+
+@[simp] theorem lt_def {a b : USize} : a < b ↔ a.toNat < b.toNat := .rfl
+
+@[simp] theorem le_def {a b : USize} : a ≤ b ↔ a.toNat ≤ b.toNat := .rfl
+
+@[simp] theorem zero_toNat : (0 : USize).toNat = 0 := Nat.zero_mod _
+
+@[simp] theorem mod_toNat (a b : USize) : (a % b).toNat = a.toNat % b.toNat :=
+  Fin.mod_val ..
+
+@[simp] theorem div_toNat (a b : USize) : (a / b).toNat = a.toNat / b.toNat :=
+  Fin.div_val ..
+
+@[simp] theorem modn_toNat (a : USize) (b : Nat) : (a.modn b).toNat = a.toNat % b :=
+  Fin.modn_val ..
+
+theorem mod_lt (a b : USize) (h : 0 < b) : a % b < b := USize.modn_lt _ (by simp at h; exact h)
+
+theorem toNat.inj : ∀ {a b : USize}, a.toNat = b.toNat → a = b
+  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
+
+end USize

src/Init/Data/Int/Bitwise.lean

@@ -5,7 +5,7 @@ Authors: Mario Carneiro
 -/
 prelude
 import Init.Data.Int.Basic
-import Init.Data.Nat.Bitwise
+import Init.Data.Nat.Bitwise.Basic
 
 namespace Int
 

src/Init/Data/Int/DivMod.lean

@@ -131,7 +131,8 @@ Integer division. This version of `Int.div` uses the E-rounding convention
 (euclidean division), in which `Int.emod x y` satisfies `0 ≤ mod x y < natAbs y` for `y ≠ 0`
 and `Int.ediv` is the unique function satisfying `emod x y + (ediv x y) * y = x`.
 -/
-def ediv : Int → Int → Int
+@[extern "lean_int_ediv"]
+def ediv : (@& Int) → (@& Int) → Int
   | ofNat m, ofNat n => ofNat (m / n)
   | ofNat m, -[n+1]  => -ofNat (m / succ n)
   | -[_+1],  0       => 0
@@ -143,7 +144,8 @@ Integer modulus. This version of `Int.mod` uses the E-rounding convention
 (euclidean division), in which `Int.emod x y` satisfies `0 ≤ emod x y < natAbs y` for `y ≠ 0`
 and `Int.ediv` is the unique function satisfying `emod x y + (ediv x y) * y = x`.
 -/
-def emod : Int → Int → Int
+@[extern "lean_int_emod"]
+def emod : (@& Int) → (@& Int) → Int
   | ofNat m, n => ofNat (m % natAbs n)
   | -[m+1],  n => subNatNat (natAbs n) (succ (m % natAbs n))
 

src/Init/Data/List/Basic.lean

@@ -889,6 +889,33 @@ def minimum? [Min α] : List α → Option α
   | []    => none
   | a::as => some <| as.foldl min a
 
+/-- Inserts an element into a list without duplication. -/
+@[inline] protected def insert [BEq α] (a : α) (l : List α) : List α :=
+  if l.elem a then l else a :: l
+
+instance decidableBEx (p : α → Prop) [DecidablePred p] :
+    ∀ l : List α, Decidable (Exists fun x => x ∈ l ∧ p x)
+  | [] => isFalse nofun
+  | x :: xs =>
+    if h₁ : p x then isTrue ⟨x, .head .., h₁⟩ else
+      match decidableBEx p xs with
+      | isTrue h₂ => isTrue <| let ⟨y, hm, hp⟩ := h₂; ⟨y, .tail _ hm, hp⟩
+      | isFalse h₂ => isFalse fun
+        | ⟨y, .tail _ h, hp⟩ => h₂ ⟨y, h, hp⟩
+        | ⟨_, .head .., hp⟩ => h₁ hp
+
+instance decidableBAll (p : α → Prop) [DecidablePred p] :
+    ∀ l : List α, Decidable (∀ x, x ∈ l → p x)
+  | [] => isTrue nofun
+  | x :: xs =>
+    if h₁ : p x then
+      match decidableBAll p xs with
+      | isTrue h₂ => isTrue fun
+        | y, .tail _ h => h₂ y h
+        | _, .head .. => h₁
+      | isFalse h₂ => isFalse fun H => h₂ fun y hm => H y (.tail _ hm)
+    else isFalse fun H => h₁ <| H x (.head ..)
+
 instance [BEq α] [LawfulBEq α] : LawfulBEq (List α) where
   eq_of_beq {as bs} := by
     induction as generalizing bs with

src/Init/Data/Nat.lean

@@ -15,3 +15,4 @@ import Init.Data.Nat.Log2
 import Init.Data.Nat.Power2
 import Init.Data.Nat.Linear
 import Init.Data.Nat.SOM
+import Init.Data.Nat.Lemmas

src/Init/Data/Nat/Basic.lean

@@ -621,7 +621,7 @@ theorem add_sub_of_le {a b : Nat} (h : a ≤ b) : a + (b - a) = b := by
     have : a ≤ b := Nat.le_of_succ_le h
     rw [sub_succ, Nat.succ_add, ← Nat.add_succ, Nat.succ_pred hne, ih this]
 
-protected theorem sub_add_cancel {n m : Nat} (h : m ≤ n) : n - m + m = n := by
+@[simp] protected theorem sub_add_cancel {n m : Nat} (h : m ≤ n) : n - m + m = n := by
   rw [Nat.add_comm, Nat.add_sub_of_le h]
 
 protected theorem add_sub_add_right (n k m : Nat) : (n + k) - (m + k) = n - m := by

src/Init/Data/Nat/Bitwise.lean

@@ -1,54 +1,3 @@
-/-
-Copyright (c) 2019 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.Nat.Basic
-import Init.Data.Nat.Div
-import Init.Coe
-
-namespace Nat
-
-theorem bitwise_rec_lemma {n : Nat} (hNe : n ≠ 0) : n / 2 < n :=
-  Nat.div_lt_self (Nat.zero_lt_of_ne_zero hNe) (Nat.lt_succ_self _)
-
-def bitwise (f : Bool → Bool → Bool) (n m : Nat) : Nat :=
-  if n = 0 then
-    if f false true then m else 0
-  else if m = 0 then
-    if f true false then n else 0
-  else
-    let n' := n / 2
-    let m' := m / 2
-    let b₁ := n % 2 = 1
-    let b₂ := m % 2 = 1
-    let r  := bitwise f n' m'
-    if f b₁ b₂ then
-      r+r+1
-    else
-      r+r
-decreasing_by apply bitwise_rec_lemma; assumption
-
-@[extern "lean_nat_land"]
-def land : @& Nat → @& Nat → Nat := bitwise and
-@[extern "lean_nat_lor"]
-def lor  : @& Nat → @& Nat → Nat := bitwise or
-@[extern "lean_nat_lxor"]
-def xor  : @& Nat → @& Nat → Nat := bitwise bne
-@[extern "lean_nat_shiftl"]
-def shiftLeft : @& Nat → @& Nat → Nat
-  | n, 0 => n
-  | n, succ m => shiftLeft (2*n) m
-@[extern "lean_nat_shiftr"]
-def shiftRight : @& Nat → @& Nat → Nat
-  | n, 0 => n
-  | n, succ m => shiftRight n m / 2
-
-instance : AndOp Nat := ⟨Nat.land⟩
-instance : OrOp Nat := ⟨Nat.lor⟩
-instance : Xor Nat := ⟨Nat.xor⟩
-instance : ShiftLeft Nat := ⟨Nat.shiftLeft⟩
-instance : ShiftRight Nat := ⟨Nat.shiftRight⟩
-
-end Nat
+import Init.Data.Nat.Bitwise.Basic
+import Init.Data.Nat.Bitwise.Lemmas

src/Init/Data/Nat/Bitwise/Basic.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2019 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.Nat.Basic
+import Init.Data.Nat.Div
+import Init.Coe
+
+namespace Nat
+
+theorem bitwise_rec_lemma {n : Nat} (hNe : n ≠ 0) : n / 2 < n :=
+  Nat.div_lt_self (Nat.zero_lt_of_ne_zero hNe) (Nat.lt_succ_self _)
+
+def bitwise (f : Bool → Bool → Bool) (n m : Nat) : Nat :=
+  if n = 0 then
+    if f false true then m else 0
+  else if m = 0 then
+    if f true false then n else 0
+  else
+    let n' := n / 2
+    let m' := m / 2
+    let b₁ := n % 2 = 1
+    let b₂ := m % 2 = 1
+    let r  := bitwise f n' m'
+    if f b₁ b₂ then
+      r+r+1
+    else
+      r+r
+decreasing_by apply bitwise_rec_lemma; assumption
+
+@[extern "lean_nat_land"]
+def land : @& Nat → @& Nat → Nat := bitwise and
+@[extern "lean_nat_lor"]
+def lor  : @& Nat → @& Nat → Nat := bitwise or
+@[extern "lean_nat_lxor"]
+def xor  : @& Nat → @& Nat → Nat := bitwise bne
+@[extern "lean_nat_shiftl"]
+def shiftLeft : @& Nat → @& Nat → Nat
+  | n, 0 => n
+  | n, succ m => shiftLeft (2*n) m
+@[extern "lean_nat_shiftr"]
+def shiftRight : @& Nat → @& Nat → Nat
+  | n, 0 => n
+  | n, succ m => shiftRight n m / 2
+
+instance : AndOp Nat := ⟨Nat.land⟩
+instance : OrOp Nat := ⟨Nat.lor⟩
+instance : Xor Nat := ⟨Nat.xor⟩
+instance : ShiftLeft Nat := ⟨Nat.shiftLeft⟩
+instance : ShiftRight Nat := ⟨Nat.shiftRight⟩
+
+/-!
+### testBit
+We define an operation for testing individual bits in the binary representation
+of a number.
+-/
+
+/-- `testBit m n` returns whether the `(n+1)` least significant bit is `1` or `0`-/
+def testBit (m n : Nat) : Bool := (m >>> n) &&& 1 != 0
+
+end Nat

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -0,0 +1,503 @@
+/-
+Copyright (c) 2023 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joe Hendrix
+-/
+
+prelude
+import Init.Data.Bool
+import Init.Data.Nat.Bitwise.Basic
+import Init.Data.Nat.Lemmas
+import Init.TacticsExtra
+import Init.Omega
+
+/-
+This module defines properties of the bitwise operations on Natural numbers.
+
+It is primarily intended to support the bitvector library.
+-/
+
+namespace Nat
+
+@[local simp]
+private theorem one_div_two : 1/2 = 0 := by trivial
+
+private theorem two_pow_succ_sub_succ_div_two : (2 ^ (n+1) - (x + 1)) / 2 = 2^n - (x/2 + 1) := by
+  if h : x + 1 ≤ 2 ^ (n + 1) then
+    apply fun x => (Nat.sub_eq_of_eq_add x).symm
+    apply Eq.trans _
+    apply Nat.add_mul_div_left _ _ Nat.zero_lt_two
+    rw [← Nat.sub_add_comm h]
+    rw [Nat.add_sub_assoc (by omega)]
+    rw [Nat.pow_succ']
+    rw [Nat.mul_add_div Nat.zero_lt_two]
+    simp [show (2 * (x / 2 + 1) - (x + 1)) / 2 = 0 by omega]
+  else
+    rw [Nat.pow_succ'] at *
+    omega
+
+private theorem two_pow_succ_sub_one_div_two : (2 ^ (n+1) - 1) / 2 = 2^n - 1 :=
+  two_pow_succ_sub_succ_div_two
+
+private theorem two_mul_sub_one {n : Nat} (n_pos : n > 0) : (2*n - 1) % 2 = 1 := by
+  match n with
+  | 0 => contradiction
+  | n + 1 => simp [Nat.mul_succ, Nat.mul_add_mod, mod_eq_of_lt]
+
+/-! ### Preliminaries -/
+
+/--
+An induction principal that works on divison by two.
+-/
+noncomputable def div2Induction {motive : Nat → Sort u}
+    (n : Nat) (ind : ∀(n : Nat), (n > 0 → motive (n/2)) → motive n) : motive n := by
+  induction n using Nat.strongInductionOn with
+  | ind n hyp =>
+    apply ind
+    intro n_pos
+    if n_eq : n = 0 then
+      simp [n_eq] at n_pos
+    else
+      apply hyp
+      exact Nat.div_lt_self n_pos (Nat.le_refl _)
+
+@[simp] theorem zero_and (x : Nat) : 0 &&& x = 0 := by rfl
+
+@[simp] theorem and_zero (x : Nat) : x &&& 0 = 0 := by
+  simp only [HAnd.hAnd, AndOp.and, land]
+  unfold bitwise
+  simp
+
+@[simp] theorem and_one_is_mod (x : Nat) : x &&& 1 = x % 2 := by
+  if xz : x = 0 then
+    simp [xz, zero_and]
+  else
+    have andz := and_zero (x/2)
+    simp only [HAnd.hAnd, AndOp.and, land] at andz
+    simp only [HAnd.hAnd, AndOp.and, land]
+    unfold bitwise
+    cases mod_two_eq_zero_or_one x with | _ p =>
+      simp [xz, p, andz, one_div_two, mod_eq_of_lt]
+
+/-! ### testBit -/
+
+@[simp] theorem zero_testBit (i : Nat) : testBit 0 i = false := by
+  simp only [testBit, zero_shiftRight, zero_and, bne_self_eq_false]
+
+@[simp] theorem testBit_zero (x : Nat) : testBit x 0 = decide (x % 2 = 1) := by
+  cases mod_two_eq_zero_or_one x with | _ p => simp [testBit, p]
+
+@[simp] theorem testBit_succ (x i : Nat) : testBit x (succ i) = testBit (x/2) i := by
+  unfold testBit
+  simp [shiftRight_succ_inside]
+
+theorem testBit_to_div_mod {x : Nat} : testBit x i = decide (x / 2^i % 2 = 1) := by
+  induction i generalizing x with
+  | zero =>
+    unfold testBit
+    cases mod_two_eq_zero_or_one x with | _ xz => simp [xz]
+  | succ i hyp =>
+    simp [hyp, Nat.div_div_eq_div_mul, Nat.pow_succ']
+
+theorem ne_zero_implies_bit_true {x : Nat} (xnz : x ≠ 0) : ∃ i, testBit x i := by
+  induction x using div2Induction with
+  | ind x hyp =>
+    have x_pos : x > 0 := Nat.pos_of_ne_zero xnz
+    match mod_two_eq_zero_or_one x with
+    | Or.inl mod2_eq =>
+      rw [←div_add_mod x 2] at xnz
+      simp only [mod2_eq, ne_eq, Nat.mul_eq_zero, Nat.add_zero, false_or] at xnz
+      have ⟨d, dif⟩   := hyp x_pos xnz
+      apply Exists.intro (d+1)
+      simp_all
+    | Or.inr mod2_eq =>
+      apply Exists.intro 0
+      simp_all
+
+theorem ne_implies_bit_diff {x y : Nat} (p : x ≠ y) : ∃ i, testBit x i ≠ testBit y i := by
+  induction y using Nat.div2Induction generalizing x with
+  | ind y hyp =>
+    cases Nat.eq_zero_or_pos y with
+    | inl yz =>
+      simp only [yz, Nat.zero_testBit, Bool.eq_false_iff]
+      simp only [yz] at p
+      have ⟨i,ip⟩  := ne_zero_implies_bit_true p
+      apply Exists.intro i
+      simp [ip]
+    | inr ypos =>
+      if lsb_diff : x % 2 = y % 2 then
+        rw [←Nat.div_add_mod x 2, ←Nat.div_add_mod y 2] at p
+        simp only [ne_eq, lsb_diff, Nat.add_right_cancel_iff,
+          Nat.zero_lt_succ, Nat.mul_left_cancel_iff] at p
+        have ⟨i, ieq⟩  := hyp ypos p
+        apply Exists.intro (i+1)
+        simpa
+      else
+        apply Exists.intro 0
+        simp only [testBit_zero]
+        revert lsb_diff
+        cases mod_two_eq_zero_or_one x with | _ p =>
+          cases mod_two_eq_zero_or_one y with | _ q =>
+            simp [p,q]
+
+/--
+`eq_of_testBit_eq` allows proving two natural numbers are equal
+if their bits are all equal.
+-/
+theorem eq_of_testBit_eq {x y : Nat} (pred : ∀i, testBit x i = testBit y i) : x = y := by
+  if h : x = y then
+    exact h
+  else
+    let ⟨i,eq⟩ := ne_implies_bit_diff h
+    have p := pred i
+    contradiction
+
+theorem ge_two_pow_implies_high_bit_true {x : Nat} (p : x ≥ 2^n) : ∃ i, i ≥ n ∧ testBit x i := by
+  induction x using div2Induction generalizing n with
+  | ind x hyp =>
+    have x_pos : x > 0 := Nat.lt_of_lt_of_le (Nat.two_pow_pos n) p
+    have x_ne_zero : x ≠ 0 := Nat.ne_of_gt x_pos
+    match n with
+    | zero =>
+      let ⟨j, jp⟩ := ne_zero_implies_bit_true x_ne_zero
+      exact Exists.intro j (And.intro (Nat.zero_le _) jp)
+    | succ n =>
+      have x_ge_n : x / 2 ≥ 2 ^ n := by
+          simpa [le_div_iff_mul_le, ← Nat.pow_succ'] using p
+      have ⟨j, jp⟩ := @hyp x_pos n x_ge_n
+      apply Exists.intro (j+1)
+      apply And.intro
+      case left =>
+        exact (Nat.succ_le_succ jp.left)
+      case right =>
+        simpa using jp.right
+
+theorem testBit_implies_ge {x : Nat} (p : testBit x i = true) : x ≥ 2^i := by
+  simp only [testBit_to_div_mod] at p
+  apply Decidable.by_contra
+  intro not_ge
+  have x_lt : x < 2^i := Nat.lt_of_not_le not_ge
+  simp [div_eq_of_lt x_lt] at p
+
+theorem testBit_lt_two_pow {x i : Nat} (lt : x < 2^i) : x.testBit i = false := by
+  match p : x.testBit i with
+  | false => trivial
+  | true =>
+    exfalso
+    exact Nat.not_le_of_gt lt (testBit_implies_ge p)
+
+theorem lt_pow_two_of_testBit (x : Nat) (p : ∀i, i ≥ n → testBit x i = false) : x < 2^n := by
+  apply Decidable.by_contra
+  intro not_lt
+  have x_ge_n := Nat.ge_of_not_lt not_lt
+  have ⟨i, ⟨i_ge_n, test_true⟩⟩ := ge_two_pow_implies_high_bit_true x_ge_n
+  have test_false := p _ i_ge_n
+  simp only [test_true] at test_false
+
+/-! ### testBit -/
+
+private theorem succ_mod_two : succ x % 2 = 1 - x % 2 := by
+  induction x with
+  | zero =>
+    trivial
+  | succ x hyp =>
+    have p : 2 ≤ x + 2 := Nat.le_add_left _ _
+    simp [Nat.mod_eq (x+2) 2, p, hyp]
+    cases Nat.mod_two_eq_zero_or_one x with | _ p => simp [p]
+
+private theorem testBit_succ_zero : testBit (x + 1) 0 = not (testBit x 0) := by
+  simp [testBit_to_div_mod, succ_mod_two]
+  cases Nat.mod_two_eq_zero_or_one x with | _ p =>
+    simp [p]
+
+theorem testBit_two_pow_add_eq (x i : Nat) : testBit (2^i + x) i = not (testBit x i) := by
+  simp [testBit_to_div_mod, add_div_left, Nat.two_pow_pos, succ_mod_two]
+  cases mod_two_eq_zero_or_one (x / 2 ^ i) with
+  | _ p => simp [p]
+
+theorem testBit_mul_two_pow_add_eq (a b i : Nat) :
+    testBit (2^i*a + b) i = Bool.xor (a%2 = 1) (testBit b i) := by
+  match a with
+  | 0 => simp
+  | a+1 =>
+    simp [Nat.mul_succ, Nat.add_assoc,
+          testBit_mul_two_pow_add_eq a,
+          testBit_two_pow_add_eq,
+          Nat.succ_mod_two]
+    cases mod_two_eq_zero_or_one a with
+    | _ p => simp [p]
+
+theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
+    testBit (2^i + x) j = testBit x j := by
+  have i_def : i = j + (i-j) := (Nat.add_sub_cancel' (Nat.le_of_lt j_lt_i)).symm
+  rw [i_def]
+  simp only [testBit_to_div_mod, Nat.pow_add,
+        Nat.add_comm x, Nat.mul_add_div (Nat.two_pow_pos _)]
+  match i_sub_j_eq : i - j with
+  | 0 =>
+    exfalso
+    rw [Nat.sub_eq_zero_iff_le] at i_sub_j_eq
+    exact Nat.not_le_of_gt j_lt_i i_sub_j_eq
+  | d+1 =>
+    simp [pow_succ, Nat.mul_comm _ 2,  Nat.mul_add_mod]
+
+@[simp] theorem testBit_mod_two_pow (x j i : Nat) :
+    testBit (x % 2^j) i = (decide (i < j) && testBit x i) := by
+  induction x using Nat.strongInductionOn generalizing j i with
+  | ind x hyp =>
+    rw [mod_eq]
+    rcases Nat.lt_or_ge x (2^j) with x_lt_j | x_ge_j
+    · have not_j_le_x := Nat.not_le_of_gt x_lt_j
+      simp [not_j_le_x]
+      rcases Nat.lt_or_ge i j with i_lt_j | i_ge_j
+      · simp [i_lt_j]
+      · have x_lt : x < 2^i :=
+            calc x < 2^j := x_lt_j
+                _ ≤ 2^i := Nat.pow_le_pow_of_le_right Nat.zero_lt_two i_ge_j
+        simp [Nat.testBit_lt_two_pow x_lt]
+    · generalize y_eq : x - 2^j = y
+      have x_eq : x = y + 2^j := Nat.eq_add_of_sub_eq x_ge_j y_eq
+      simp only [Nat.two_pow_pos, x_eq, Nat.le_add_left, true_and, ite_true]
+      have y_lt_x : y < x := by
+            simp [x_eq]
+            exact Nat.lt_add_of_pos_right (Nat.two_pow_pos j)
+      simp only [hyp y y_lt_x]
+      if i_lt_j : i < j then
+        rw [ Nat.add_comm _ (2^_), testBit_two_pow_add_gt i_lt_j]
+      else
+        simp [i_lt_j]
+
+theorem testBit_one_zero : testBit 1 0 = true := by trivial
+
+theorem testBit_two_pow_sub_succ (h₂ : x < 2 ^ n) (i : Nat) :
+    testBit (2^n - (x + 1)) i = (decide (i < n) && ! testBit x i) := by
+  induction i generalizing n x with
+  | zero =>
+    simp only [testBit_zero, zero_eq, Bool.and_eq_true, decide_eq_true_eq,
+      Bool.not_eq_true']
+    match n with
+    | 0 => simp
+    | n+1 =>
+      -- just logic + omega:
+      simp only [zero_lt_succ, decide_True, Bool.true_and]
+      rw [Nat.pow_succ', ← decide_not, decide_eq_decide]
+      rw [Nat.pow_succ'] at h₂
+      omega
+  | succ i ih =>
+    simp only [testBit_succ]
+    match n with
+    | 0 =>
+      simp only [pow_zero, succ_sub_succ_eq_sub, Nat.zero_sub, Nat.zero_div, zero_testBit]
+      rw [decide_eq_false] <;> simp
+    | n+1 =>
+      rw [Nat.two_pow_succ_sub_succ_div_two, ih]
+      · simp [Nat.succ_lt_succ_iff]
+      · rw [Nat.pow_succ'] at h₂
+        omega
+
+@[simp] theorem testBit_two_pow_sub_one (n i : Nat) : testBit (2^n-1) i = decide (i < n) := by
+  rw [testBit_two_pow_sub_succ]
+  · simp
+  · exact Nat.two_pow_pos _
+
+theorem testBit_bool_to_nat (b : Bool) (i : Nat) :
+    testBit (Bool.toNat b) i = (decide (i = 0) && b) := by
+  cases b <;> cases i <;>
+  simp [testBit_to_div_mod, Nat.pow_succ, Nat.mul_comm _ 2,
+        ←Nat.div_div_eq_div_mul _ 2, one_div_two,
+        Nat.mod_eq_of_lt]
+
+/-! ### bitwise -/
+
+theorem testBit_bitwise
+  (false_false_axiom : f false false = false) (x y i : Nat)
+: (bitwise f x y).testBit i = f (x.testBit i) (y.testBit i) := by
+  induction i using Nat.strongInductionOn generalizing x y with
+  | ind i hyp =>
+    unfold bitwise
+    if x_zero : x = 0 then
+      cases p : f false true <;>
+        cases yi : testBit y i <;>
+          simp [x_zero, p, yi, false_false_axiom]
+    else if y_zero : y = 0 then
+      simp [x_zero, y_zero]
+      cases p : f true false <;>
+        cases xi : testBit x i <;>
+          simp [p, xi, false_false_axiom]
+    else
+      simp only [x_zero, y_zero, ←Nat.two_mul]
+      cases i with
+      | zero =>
+        cases p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) <;>
+          simp [p, Nat.mul_add_mod, mod_eq_of_lt]
+      | succ i =>
+        have hyp_i := hyp i (Nat.le_refl (i+1))
+        cases p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) <;>
+          simp [p, one_div_two, hyp_i, Nat.mul_add_div]
+
+/-! ### bitwise -/
+
+@[local simp]
+private theorem eq_0_of_lt_one (x : Nat) : x < 1 ↔ x = 0 :=
+  Iff.intro
+    (fun p =>
+      match x with
+      | 0 => Eq.refl 0
+      | _+1 => False.elim (not_lt_zero _ (Nat.lt_of_succ_lt_succ p)))
+    (fun p => by simp [p, Nat.zero_lt_succ])
+
+private theorem eq_0_of_lt (x : Nat) : x < 2^ 0 ↔ x = 0 := eq_0_of_lt_one x
+
+@[local simp]
+private theorem zero_lt_pow (n : Nat) : 0 < 2^n := by
+  induction n
+  case zero => simp [eq_0_of_lt]
+  case succ n hyp => simpa [pow_succ]
+
+private theorem div_two_le_of_lt_two {m n : Nat} (p : m < 2 ^ succ n) : m / 2 < 2^n := by
+  simp [div_lt_iff_lt_mul Nat.zero_lt_two]
+  exact p
+
+/-- This provides a bound on bitwise operations. -/
+theorem bitwise_lt_two_pow (left : x < 2^n) (right : y < 2^n) : (Nat.bitwise f x y) < 2^n := by
+  induction n generalizing x y with
+  | zero =>
+    simp only [eq_0_of_lt] at left right
+    unfold bitwise
+    simp [left, right]
+  | succ n hyp =>
+    unfold bitwise
+    if x_zero : x = 0 then
+      simp only [x_zero, if_pos]
+      by_cases p : f false true = true <;> simp [p, right]
+    else if y_zero : y = 0 then
+      simp only [x_zero, y_zero, if_neg, if_pos]
+      by_cases p : f true false = true <;> simp [p, left]
+    else
+      simp only [x_zero, y_zero, if_neg]
+      have hyp1 := hyp (div_two_le_of_lt_two left) (div_two_le_of_lt_two right)
+      by_cases p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) = true <;>
+        simp [p, pow_succ, mul_succ, Nat.add_assoc]
+      case pos =>
+        apply lt_of_succ_le
+        simp only [← Nat.succ_add]
+        apply Nat.add_le_add <;> exact hyp1
+      case neg =>
+        apply Nat.add_lt_add <;> exact hyp1
+
+/-! ### and -/
+
+@[simp] theorem testBit_and (x y i : Nat) : (x &&& y).testBit i = (x.testBit i && y.testBit i) := by
+  simp [HAnd.hAnd, AndOp.and, land, testBit_bitwise ]
+
+theorem and_lt_two_pow (x : Nat) {y n : Nat} (right : y < 2^n) : (x &&& y) < 2^n := by
+  apply lt_pow_two_of_testBit
+  intro i i_ge_n
+  have yf : testBit y i = false := by
+          apply Nat.testBit_lt_two_pow
+          apply Nat.lt_of_lt_of_le right
+          exact pow_le_pow_of_le_right Nat.zero_lt_two i_ge_n
+  simp [testBit_and, yf]
+
+@[simp] theorem and_pow_two_is_mod (x n : Nat) : x &&& (2^n-1) = x % 2^n := by
+  apply eq_of_testBit_eq
+  intro i
+  simp only [testBit_and, testBit_mod_two_pow]
+  cases testBit x i <;> simp
+
+theorem and_pow_two_identity {x : Nat} (lt : x < 2^n) : x &&& 2^n-1 = x := by
+  rw [and_pow_two_is_mod]
+  apply Nat.mod_eq_of_lt lt
+
+/-! ### lor -/
+
+@[simp] theorem or_zero (x : Nat) : 0 ||| x = x := by
+  simp only [HOr.hOr, OrOp.or, lor]
+  unfold bitwise
+  simp [@eq_comm _ 0]
+
+@[simp] theorem zero_or (x : Nat) : x ||| 0 = x := by
+  simp only [HOr.hOr, OrOp.or, lor]
+  unfold bitwise
+  simp [@eq_comm _ 0]
+
+@[simp] theorem testBit_or (x y i : Nat) : (x ||| y).testBit i = (x.testBit i || y.testBit i) := by
+  simp [HOr.hOr, OrOp.or, lor, testBit_bitwise ]
+
+theorem or_lt_two_pow {x y n : Nat} (left : x < 2^n) (right : y < 2^n) : x ||| y < 2^n :=
+  bitwise_lt_two_pow left right
+
+/-! ### xor -/
+
+@[simp] theorem testBit_xor (x y i : Nat) :
+    (x ^^^ y).testBit i = Bool.xor (x.testBit i) (y.testBit i) := by
+  simp [HXor.hXor, Xor.xor, xor, testBit_bitwise ]
+
+theorem xor_lt_two_pow {x y n : Nat} (left : x < 2^n) (right : y < 2^n) : x ^^^ y < 2^n :=
+  bitwise_lt_two_pow left right
+
+/-! ### Arithmetic -/
+
+theorem testBit_mul_pow_two_add (a : Nat) {b i : Nat} (b_lt : b < 2^i) (j : Nat) :
+    testBit (2 ^ i * a + b) j =
+      if j < i then
+        testBit b j
+      else
+        testBit a (j - i) := by
+  cases Nat.lt_or_ge j i with
+  | inl j_lt =>
+    simp only [j_lt]
+    have i_ge := Nat.le_of_lt j_lt
+    have i_sub_j_nez : i-j ≠ 0 := Nat.sub_ne_zero_of_lt j_lt
+    have i_def : i = j + succ (pred (i-j)) :=
+          calc i = j + (i-j) := (Nat.add_sub_cancel' i_ge).symm
+               _ = j + succ (pred (i-j)) := by
+                 rw [← congrArg (j+·) (Nat.succ_pred i_sub_j_nez)]
+    rw [i_def]
+    simp only [testBit_to_div_mod, Nat.pow_add, Nat.mul_assoc]
+    simp only [Nat.mul_add_div (Nat.two_pow_pos _), Nat.mul_add_mod]
+    simp [Nat.pow_succ, Nat.mul_comm _ 2, Nat.mul_assoc, Nat.mul_add_mod]
+  | inr j_ge =>
+    have j_def : j = i + (j-i) := (Nat.add_sub_cancel' j_ge).symm
+    simp only [
+        testBit_to_div_mod,
+        Nat.not_lt_of_le,
+        j_ge,
+        ite_false]
+    simp [congrArg (2^·) j_def, Nat.pow_add,
+          ←Nat.div_div_eq_div_mul,
+          Nat.mul_add_div,
+          Nat.div_eq_of_lt b_lt,
+          Nat.two_pow_pos i]
+
+theorem testBit_mul_pow_two :
+    testBit (2 ^ i * a) j = (decide (j ≥ i) && testBit a (j-i)) := by
+  have gen := testBit_mul_pow_two_add a (Nat.two_pow_pos i) j
+  simp at gen
+  rw [gen]
+  cases Nat.lt_or_ge j i with
+  | _ p => simp [p, Nat.not_le_of_lt, Nat.not_lt_of_le]
+
+theorem mul_add_lt_is_or {b : Nat} (b_lt : b < 2^i) (a : Nat) : 2^i * a + b = 2^i * a ||| b := by
+  apply eq_of_testBit_eq
+  intro j
+  simp only [testBit_mul_pow_two_add _ b_lt,
+        testBit_or, testBit_mul_pow_two]
+  if j_lt : j < i then
+    simp [Nat.not_le_of_lt, j_lt]
+  else
+    have i_le : i ≤ j := Nat.le_of_not_lt j_lt
+    have b_lt_j :=
+            calc b < 2 ^ i := b_lt
+                 _ ≤ 2 ^ j := Nat.pow_le_pow_of_le_right Nat.zero_lt_two i_le
+    simp [i_le, j_lt, testBit_lt_two_pow, b_lt_j]
+
+/-! ### shiftLeft and shiftRight -/
+
+@[simp] theorem testBit_shiftLeft (x : Nat) : testBit (x <<< i) j =
+    (decide (j ≥ i) && testBit x (j-i)) := by
+  simp [shiftLeft_eq, Nat.mul_comm _ (2^_), testBit_mul_pow_two]
+
+@[simp] theorem testBit_shiftRight (x : Nat) : testBit (x >>> i) j = testBit x (i+j) := by
+  simp [testBit, ←shiftRight_add]

src/Init/Meta.lean

@@ -1285,6 +1285,41 @@ structure Config where
 
 end Rewrite
 
+namespace Omega
+
+/-- Configures the behaviour of the `omega` tactic. -/
+structure OmegaConfig where
+  /--
+  Split disjunctions in the context.
+
+  Note that with `splitDisjunctions := false` omega will not be able to solve `x = y` goals
+  as these are usually handled by introducing `¬ x = y` as a hypothesis, then replacing this with
+  `x < y ∨ x > y`.
+
+  On the other hand, `omega` does not currently detect disjunctions which, when split,
+  introduce no new useful information, so the presence of irrelevant disjunctions in the context
+  can significantly increase run time.
+  -/
+  splitDisjunctions : Bool := true
+  /--
+  Whenever `((a - b : Nat) : Int)` is found, register the disjunction
+  `b ≤ a ∧ ((a - b : Nat) : Int) = a - b ∨ a < b ∧ ((a - b : Nat) : Int) = 0`
+  for later splitting.
+  -/
+  splitNatSub : Bool := true
+  /--
+  Whenever `Int.natAbs a` is found, register the disjunction
+  `0 ≤ a ∧ Int.natAbs a = a ∨ a < 0 ∧ Int.natAbs a = - a` for later splitting.
+  -/
+  splitNatAbs : Bool := true
+  /--
+  Whenever `min a b` or `max a b` is found, rewrite in terms of the definition
+  `if a ≤ b ...`, for later case splitting.
+  -/
+  splitMinMax : Bool := true
+
+end Omega
+
 end Meta
 
 namespace Parser.Tactic

src/Init/MetaTypes.lean

@@ -43,6 +43,7 @@ inductive EtaStructMode where
 namespace DSimp
 
 structure Config where
+  /-- `let x := v; e[x]` reduces to `e[v]`. -/
   zeta              : Bool := true
   beta              : Bool := true
   eta               : Bool := true
@@ -57,6 +58,8 @@ structure Config where
   /-- If `unfoldPartialApp := true`, then calls to `simp`, `dsimp`, or `simp_all`
   will unfold even partial applications of `f` when we request `f` to be unfolded. -/
   unfoldPartialApp  : Bool := false
+  /-- Given a local context containing entry `x : t := e`, free variable `x` reduces to `e`. -/
+  zetaDelta         : Bool := false
   deriving Inhabited, BEq
 
 end DSimp
@@ -71,6 +74,7 @@ structure Config where
   contextual        : Bool := false
   memoize           : Bool := true
   singlePass        : Bool := false
+  /-- `let x := v; e[x]` reduces to `e[v]`. -/
   zeta              : Bool := true
   beta              : Bool := true
   eta               : Bool := true
@@ -95,6 +99,8 @@ structure Config where
   /-- If `unfoldPartialApp := true`, then calls to `simp`, `dsimp`, or `simp_all`
   will unfold even partial applications of `f` when we request `f` to be unfolded. -/
   unfoldPartialApp  : Bool := false
+  /-- Given a local context containing entry `x : t := e`, free variable `x` reduces to `e`. -/
+  zetaDelta         : Bool := false
   deriving Inhabited, BEq
 
 -- Configuration object for `simp_all`
@@ -111,6 +117,7 @@ def neutralConfig : Simp.Config := {
   arith             := false
   autoUnfold        := false
   ground            := false
+  zetaDelta         := false
 }
 
 end Simp

src/Init/Omega.lean

@@ -0,0 +1,6 @@
+prelude
+import Init.Omega.Int
+import Init.Omega.IntList
+import Init.Omega.LinearCombo
+import Init.Omega.Constraint
+import Init.Omega.Logic

src/Init/Omega/Coeffs.lean

@@ -0,0 +1,112 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+prelude
+import Init.Omega.IntList
+
+/-!
+# `Coeffs` as a wrapper for `IntList`
+
+Currently `omega` uses a dense representation for coefficients.
+However, we can swap this out for a sparse representation.
+
+This file sets up `Coeffs` as a type synonym for `IntList`,
+and abbreviations for the functions in the `IntList` namespace which we need to use in the
+`omega` algorithm.
+
+There is an equivalent file setting up `Coeffs` as a type synonym for `AssocList Nat Int`,
+currently in a private branch.
+Not all the theorems about the algebraic operations on that representation have been proved yet.
+When they are ready, we can replace the implementation in `omega` simply by importing
+`Std.Tactic.Omega.Coeffs.IntDict` instead of `Std.Tactic.Omega.Coeffs.IntList`.
+
+For small problems, the sparse representation is actually slightly slower,
+so it is not urgent to make this replacement.
+-/
+
+namespace Lean.Omega
+
+/-- Type synonym for `IntList := List Int`. -/
+abbrev Coeffs := IntList
+
+namespace Coeffs
+
+/-- Identity, turning `Coeffs` into `List Int`. -/
+abbrev toList (xs : Coeffs) : List Int := xs
+/-- Identity, turning `List Int` into `Coeffs`. -/
+abbrev ofList (xs : List Int) : Coeffs := xs
+/-- Are the coefficients all zero? -/
+abbrev isZero (xs : Coeffs) : Prop := ∀ x, x ∈ xs → x = 0
+/-- Shim for `IntList.set`. -/
+abbrev set (xs : Coeffs) (i : Nat) (y : Int) : Coeffs := IntList.set xs i y
+/-- Shim for `IntList.get`. -/
+abbrev get (xs : Coeffs) (i : Nat) : Int := IntList.get xs i
+/-- Shim for `IntList.gcd`. -/
+abbrev gcd (xs : Coeffs) : Nat := IntList.gcd xs
+/-- Shim for `IntList.smul`. -/
+abbrev smul (xs : Coeffs) (g : Int) : Coeffs := IntList.smul xs g
+/-- Shim for `IntList.sdiv`. -/
+abbrev sdiv (xs : Coeffs) (g : Int) : Coeffs := IntList.sdiv xs g
+/-- Shim for `IntList.dot`. -/
+abbrev dot (xs ys : Coeffs) : Int := IntList.dot xs ys
+/-- Shim for `IntList.add`. -/
+abbrev add (xs ys : Coeffs) : Coeffs := IntList.add xs ys
+/-- Shim for `IntList.sub`. -/
+abbrev sub (xs ys : Coeffs) : Coeffs := IntList.sub xs ys
+/-- Shim for `IntList.neg`. -/
+abbrev neg (xs : Coeffs) : Coeffs := IntList.neg xs
+/-- Shim for `IntList.combo`. -/
+abbrev combo (a : Int) (xs : Coeffs) (b : Int) (ys : Coeffs) : Coeffs := IntList.combo a xs b ys
+/-- Shim for `List.length`. -/
+abbrev length (xs : Coeffs) := List.length xs
+/-- Shim for `IntList.leading`. -/
+abbrev leading (xs : Coeffs) : Int := IntList.leading xs
+/-- Shim for `List.map`. -/
+abbrev map (f : Int → Int) (xs : Coeffs) : Coeffs := List.map f xs
+/-- Shim for `.enum.find?`. -/
+abbrev findIdx? (f : Int → Bool) (xs : Coeffs) : Option Nat :=
+  -- List.findIdx? f xs
+  -- We could avoid `Std.Data.List.Basic` by using the less efficient:
+  xs.enum.find? (f ·.2) |>.map (·.1)
+/-- Shim for `IntList.bmod`. -/
+abbrev bmod (x : Coeffs) (m : Nat) : Coeffs := IntList.bmod x m
+/-- Shim for `IntList.bmod_dot_sub_dot_bmod`. -/
+abbrev bmod_dot_sub_dot_bmod (m : Nat) (a b : Coeffs) : Int :=
+  IntList.bmod_dot_sub_dot_bmod m a b
+theorem bmod_length (x : Coeffs) (m : Nat) : (bmod x m).length ≤ x.length :=
+  IntList.bmod_length x m
+theorem dvd_bmod_dot_sub_dot_bmod (m : Nat) (xs ys : Coeffs) :
+    (m : Int) ∣ bmod_dot_sub_dot_bmod m xs ys := IntList.dvd_bmod_dot_sub_dot_bmod m xs ys
+
+theorem get_of_length_le {i : Nat} {xs : Coeffs} (h : length xs ≤ i) : get xs i = 0 :=
+  IntList.get_of_length_le h
+theorem dot_set_left (xs ys : Coeffs) (i : Nat) (z : Int) :
+    dot (set xs i z) ys = dot xs ys + (z - get xs i) * get ys i :=
+  IntList.dot_set_left xs ys i z
+theorem dot_sdiv_left (xs ys : Coeffs) {d : Int} (h : d ∣ xs.gcd) :
+    dot (xs.sdiv d) ys = (dot xs ys) / d :=
+  IntList.dot_sdiv_left xs ys h
+theorem dot_smul_left (xs ys : Coeffs) (i : Int) : dot (i * xs) ys = i * dot xs ys :=
+  IntList.dot_smul_left xs ys i
+theorem dot_distrib_left (xs ys zs : Coeffs) : (xs + ys).dot zs = xs.dot zs + ys.dot zs :=
+  IntList.dot_distrib_left xs ys zs
+theorem sub_eq_add_neg (xs ys : Coeffs) : xs - ys = xs + -ys :=
+  IntList.sub_eq_add_neg xs ys
+theorem combo_eq_smul_add_smul (a : Int) (xs : Coeffs) (b : Int) (ys : Coeffs) :
+    combo a xs b ys = (a * xs) + (b * ys) :=
+  IntList.combo_eq_smul_add_smul a xs b ys
+theorem gcd_dvd_dot_left (xs ys : Coeffs) : (gcd xs : Int) ∣ dot xs ys :=
+  IntList.gcd_dvd_dot_left xs ys
+theorem map_length {xs : Coeffs} : (xs.map f).length ≤ xs.length :=
+  Nat.le_of_eq (List.length_map xs f)
+
+theorem dot_nil_right {xs : Coeffs} : dot xs .nil = 0 := IntList.dot_nil_right
+theorem get_nil : get .nil i = 0 := IntList.get_nil
+theorem dot_neg_left (xs ys : IntList) : dot (-xs) ys = -dot xs ys :=
+  IntList.dot_neg_left xs ys
+
+end Coeffs
+
+end Lean.Omega

src/Init/Omega/Constraint.lean

@@ -0,0 +1,395 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+prelude
+import Init.Omega.LinearCombo
+import Init.Omega.Int
+
+/-!
+A `Constraint` consists of an optional lower and upper bound (inclusive),
+constraining a value to a set of the form `∅`, `{x}`, `[x, y]`, `[x, ∞)`, `(-∞, y]`, or `(-∞, ∞)`.
+-/
+
+namespace Lean.Omega
+
+/-- An optional lower bound on a integer. -/
+abbrev LowerBound : Type := Option Int
+/-- An optional upper bound on a integer. -/
+abbrev UpperBound : Type := Option Int
+
+/-- A lower bound at `x` is satisfied at `t` if `x ≤ t`. -/
+abbrev LowerBound.sat (b : LowerBound) (t : Int) := b.all fun x => x ≤ t
+/-- A upper bound at `y` is satisfied at `t` if `t ≤ y`. -/
+abbrev UpperBound.sat (b : UpperBound) (t : Int) := b.all fun y => t ≤ y
+
+/--
+A `Constraint` consists of an optional lower and upper bound (inclusive),
+constraining a value to a set of the form `∅`, `{x}`, `[x, y]`, `[x, ∞)`, `(-∞, y]`, or `(-∞, ∞)`.
+-/
+structure Constraint where
+  /-- A lower bound. -/
+  lowerBound : LowerBound
+  /-- An upper bound. -/
+  upperBound : UpperBound
+deriving BEq, DecidableEq, Repr
+
+namespace Constraint
+
+instance : ToString Constraint where
+  toString := fun
+  | ⟨none, none⟩ => "(-∞, ∞)"
+  | ⟨none, some y⟩ => s!"(-∞, {y}]"
+  | ⟨some x, none⟩ => s!"[{x}, ∞)"
+  | ⟨some x, some y⟩ =>
+    if y < x then "∅" else if x = y then s!"\{{x}}" else s!"[{x}, {y}]"
+
+/-- A constraint is satisfied at `t` is both the lower bound and upper bound are satisfied. -/
+def sat (c : Constraint) (t : Int) : Bool := c.lowerBound.sat t ∧ c.upperBound.sat t
+
+/-- Apply a function to both the lower bound and upper bound. -/
+def map (c : Constraint) (f : Int → Int) : Constraint where
+  lowerBound := c.lowerBound.map f
+  upperBound := c.upperBound.map f
+
+/-- Translate a constraint. -/
+def translate (c : Constraint) (t : Int) : Constraint := c.map (· + t)
+
+theorem translate_sat : {c : Constraint} → {v : Int} → sat c v → sat (c.translate t) (v + t) := by
+  rintro ⟨_ | l, _ | u⟩ v w <;> simp_all [sat, translate, map]
+  · exact Int.add_le_add_right w t
+  · exact Int.add_le_add_right w t
+  · rcases w with ⟨w₁, w₂⟩; constructor
+    · exact Int.add_le_add_right w₁ t
+    · exact Int.add_le_add_right w₂ t
+
+/--
+Flip a constraint.
+This operation is not useful by itself, but is used to implement `neg` and `scale`.
+-/
+def flip (c : Constraint) : Constraint where
+  lowerBound := c.upperBound
+  upperBound := c.lowerBound
+
+/--
+Negate a constraint. `[x, y]` becomes `[-y, -x]`.
+-/
+def neg (c : Constraint) : Constraint := c.flip.map (- ·)
+
+theorem neg_sat : {c : Constraint} → {v : Int} → sat c v → sat (c.neg) (-v) := by
+  rintro ⟨_ | l, _ | u⟩ v w <;> simp_all [sat, neg, flip, map]
+  · exact Int.neg_le_neg w
+  · exact Int.neg_le_neg w
+  · rcases w with ⟨w₁, w₂⟩; constructor
+    · exact Int.neg_le_neg w₂
+    · exact Int.neg_le_neg w₁
+
+/-- The trivial constraint, satisfied everywhere. -/
+def trivial : Constraint := ⟨none, none⟩
+/-- The impossible constraint, unsatisfiable. -/
+def impossible : Constraint := ⟨some 1, some 0⟩
+/-- An exact constraint. -/
+def exact (r : Int) : Constraint := ⟨some r, some r⟩
+
+@[simp] theorem trivial_say : trivial.sat t := by
+  simp [sat, trivial]
+
+@[simp] theorem exact_sat (r : Int) (t : Int) : (exact r).sat t = decide (r = t) := by
+  simp only [sat, exact, Option.all_some, decide_eq_true_eq, decide_eq_decide]
+  exact Int.eq_iff_le_and_ge.symm
+
+/-- Check if a constraint is unsatisfiable. -/
+def isImpossible : Constraint → Bool
+  | ⟨some x, some y⟩ => y < x
+  | _ => false
+
+/-- Check if a constraint requires an exact value. -/
+def isExact : Constraint → Bool
+  | ⟨some x, some y⟩ => x = y
+  | _ => false
+
+theorem not_sat_of_isImpossible (h : isImpossible c) {t} : ¬ c.sat t := by
+  rcases c with ⟨_ | l, _ | u⟩ <;> simp [isImpossible, sat] at h ⊢
+  intro w
+  rw [Int.not_le]
+  exact Int.lt_of_lt_of_le h w
+
+/--
+Scale a constraint by multiplying by an integer.
+* If `k = 0` this is either impossible, if the original constraint was impossible,
+  or the `= 0` exact constraint.
+* If `k` is positive this takes `[x, y]` to `[k * x, k * y]`
+* If `k` is negative this takes `[x, y]` to `[k * y, k * x]`.
+-/
+def scale (k : Int) (c : Constraint) : Constraint :=
+  if k = 0 then
+    if c.isImpossible then c else ⟨some 0, some 0⟩
+  else if 0 < k then
+    c.map (k * ·)
+  else
+    c.flip.map (k * ·)
+
+theorem scale_sat {c : Constraint} (k) (w : c.sat t) : (scale k c).sat (k * t) := by
+  simp [scale]
+  split
+  · split
+    · simp_all [not_sat_of_isImpossible]
+    · simp_all [sat]
+  · rcases c with ⟨_ | l, _ | u⟩ <;> split <;> rename_i h <;> simp_all [sat, flip, map]
+    · replace h := Int.le_of_lt h
+      exact Int.mul_le_mul_of_nonneg_left w h
+    · rw [Int.not_lt] at h
+      exact Int.mul_le_mul_of_nonpos_left h w
+    · replace h := Int.le_of_lt h
+      exact Int.mul_le_mul_of_nonneg_left w h
+    · rw [Int.not_lt] at h
+      exact Int.mul_le_mul_of_nonpos_left h w
+    · constructor
+      · exact Int.mul_le_mul_of_nonneg_left w.1 (Int.le_of_lt h)
+      · exact Int.mul_le_mul_of_nonneg_left w.2 (Int.le_of_lt h)
+    · replace h := Int.not_lt.mp h
+      constructor
+      · exact Int.mul_le_mul_of_nonpos_left h w.2
+      · exact Int.mul_le_mul_of_nonpos_left h w.1
+
+/-- The sum of two constraints. `[a, b] + [c, d] = [a + c, b + d]`. -/
+def add (x y : Constraint) : Constraint where
+  lowerBound := x.lowerBound.bind fun a => y.lowerBound.map fun b => a + b
+  upperBound := x.upperBound.bind fun a => y.upperBound.map fun b => a + b
+
+theorem add_sat (w₁ : c₁.sat x₁) (w₂ : c₂.sat x₂) : (add c₁ c₂).sat (x₁ + x₂) := by
+  rcases c₁ with ⟨_ | l₁, _ | u₁⟩ <;> rcases c₂ with ⟨_ | l₂, _ | u₂⟩
+    <;> simp [sat, LowerBound.sat, UpperBound.sat, add] at *
+  · exact Int.add_le_add w₁ w₂
+  · exact Int.add_le_add w₁ w₂.2
+  · exact Int.add_le_add w₁ w₂
+  · exact Int.add_le_add w₁ w₂.1
+  · exact Int.add_le_add w₁.2 w₂
+  · exact Int.add_le_add w₁.1 w₂
+  · constructor
+    · exact Int.add_le_add w₁.1 w₂.1
+    · exact Int.add_le_add w₁.2 w₂.2
+
+/-- A linear combination of two constraints. -/
+def combo (a : Int) (x : Constraint) (b : Int) (y : Constraint) : Constraint :=
+  add (scale a x) (scale b y)
+
+theorem combo_sat (a) (w₁ : c₁.sat x₁) (b) (w₂ : c₂.sat x₂) :
+    (combo a c₁ b c₂).sat (a * x₁ + b * x₂) :=
+  add_sat (scale_sat a w₁) (scale_sat b w₂)
+
+/-- The conjunction of two constraints. -/
+def combine (x y : Constraint) : Constraint where
+  lowerBound := max x.lowerBound y.lowerBound
+  upperBound := min x.upperBound y.upperBound
+
+theorem combine_sat : (c : Constraint) → (c' : Constraint) → (t : Int) →
+    (c.combine c').sat t = (c.sat t ∧ c'.sat t) := by
+  rintro ⟨_ | l₁, _ | u₁⟩ <;> rintro ⟨_ | l₂, _ | u₂⟩ t
+    <;> simp [sat, LowerBound.sat, UpperBound.sat, combine, Int.le_min, Int.max_le] at *
+  · rw [And.comm]
+  · rw [← and_assoc, And.comm (a := l₂ ≤ t), and_assoc]
+  · rw [and_assoc]
+  · rw [and_assoc]
+  · rw [and_assoc, and_assoc, And.comm (a := l₂ ≤ t)]
+  · rw [and_assoc, ← and_assoc (a := l₂ ≤ t), And.comm (a := l₂ ≤ t), and_assoc, and_assoc]
+
+/--
+Dividing a constraint by a natural number, and tightened to integer bounds.
+Thus the lower bound is rounded up, and the upper bound is rounded down.
+-/
+def div (c : Constraint) (k : Nat) : Constraint where
+  lowerBound := c.lowerBound.map fun x => (- ((- x) / k))
+  upperBound := c.upperBound.map fun y => y / k
+
+theorem div_sat (c : Constraint) (t : Int) (k : Nat) (n : k ≠ 0) (h : (k : Int) ∣ t) (w : c.sat t) :
+    (c.div k).sat (t / k) := by
+  replace n : (k : Int) > 0 := Int.ofNat_lt.mpr (Nat.pos_of_ne_zero n)
+  rcases c with ⟨_ | l, _ | u⟩
+  · simp_all [sat, div]
+  · simp [sat, div] at w ⊢
+    apply Int.le_of_sub_nonneg
+    rw [← Int.sub_ediv_of_dvd _ h, ← ge_iff_le, Int.div_nonneg_iff_of_pos n]
+    exact Int.sub_nonneg_of_le w
+  · simp [sat, div] at w ⊢
+    apply Int.le_of_sub_nonneg
+    rw [Int.sub_neg, ← Int.add_ediv_of_dvd_left h, ← ge_iff_le,
+      Int.div_nonneg_iff_of_pos n]
+    exact Int.sub_nonneg_of_le w
+  · simp [sat, div] at w ⊢
+    constructor
+    · apply Int.le_of_sub_nonneg
+      rw [Int.sub_neg, ← Int.add_ediv_of_dvd_left h, ← ge_iff_le,
+        Int.div_nonneg_iff_of_pos n]
+      exact Int.sub_nonneg_of_le w.1
+    · apply Int.le_of_sub_nonneg
+      rw [← Int.sub_ediv_of_dvd _ h, ← ge_iff_le, Int.div_nonneg_iff_of_pos n]
+      exact Int.sub_nonneg_of_le w.2
+
+/--
+It is convenient below to say that a constraint is satisfied at the dot product of two vectors,
+so we make an abbreviation `sat'` for this.
+-/
+abbrev sat' (c : Constraint) (x y : Coeffs) := c.sat (Coeffs.dot x y)
+
+theorem combine_sat' {s t : Constraint} {x y} (ws : s.sat' x y) (wt : t.sat' x y) :
+    (s.combine t).sat' x y := (combine_sat _ _ _).mpr ⟨ws, wt⟩
+
+theorem div_sat' {c : Constraint} {x y} (h : Coeffs.gcd x ≠ 0) (w : c.sat (Coeffs.dot x y)) :
+    (c.div (Coeffs.gcd x)).sat' (Coeffs.sdiv x (Coeffs.gcd x)) y := by
+  dsimp [sat']
+  rw [Coeffs.dot_sdiv_left _ _ (Int.dvd_refl _)]
+  exact div_sat c _ (Coeffs.gcd x) h (Coeffs.gcd_dvd_dot_left x y) w
+
+theorem not_sat'_of_isImpossible (h : isImpossible c) {x y} : ¬ c.sat' x y :=
+  not_sat_of_isImpossible h
+
+theorem addInequality_sat (w : c + Coeffs.dot x y ≥ 0) :
+    Constraint.sat' { lowerBound := some (-c), upperBound := none } x y := by
+  simp [Constraint.sat', Constraint.sat]
+  rw [← Int.zero_sub c]
+  exact Int.sub_left_le_of_le_add w
+
+theorem addEquality_sat (w : c + Coeffs.dot x y = 0) :
+    Constraint.sat' { lowerBound := some (-c), upperBound := some (-c) } x y := by
+  simp [Constraint.sat', Constraint.sat]
+  rw [Int.eq_iff_le_and_ge] at w
+  rwa [Int.add_le_zero_iff_le_neg', Int.add_nonnneg_iff_neg_le', and_comm] at w
+
+end Constraint
+
+/--
+Normalize a constraint, by dividing through by the GCD.
+
+Return `none` if there is nothing to do, to avoid adding unnecessary steps to the proof term.
+-/
+def normalize? : Constraint × Coeffs → Option (Constraint × Coeffs)
+  | ⟨s, x⟩ =>
+    let gcd := Coeffs.gcd x -- TODO should we be caching this?
+    if gcd = 0 then
+      if s.sat 0 then
+        some (.trivial, x)
+      else
+        some (.impossible, x)
+    else if gcd = 1 then
+      none
+    else
+      some (s.div gcd, Coeffs.sdiv x gcd)
+
+/-- Normalize a constraint, by dividing through by the GCD. -/
+def normalize (p : Constraint × Coeffs) : Constraint × Coeffs :=
+  normalize? p |>.getD p
+
+/-- Shorthand for the first component of `normalize`. -/
+-- This `noncomputable` (and others below) is a safeguard that we only use this in proofs.
+noncomputable abbrev normalizeConstraint (s : Constraint) (x : Coeffs) : Constraint :=
+  (normalize (s, x)).1
+/-- Shorthand for the second component of `normalize`. -/
+noncomputable abbrev normalizeCoeffs (s : Constraint) (x : Coeffs) : Coeffs :=
+  (normalize (s, x)).2
+
+theorem normalize?_eq_some (w : normalize? (s, x) = some (s', x')) :
+    normalizeConstraint s x = s' ∧ normalizeCoeffs s x = x' := by
+  simp_all [normalizeConstraint, normalizeCoeffs, normalize]
+
+theorem normalize_sat {s x v} (w : s.sat' x v) :
+    (normalizeConstraint s x).sat' (normalizeCoeffs s x) v := by
+  dsimp [normalizeConstraint, normalizeCoeffs, normalize, normalize?]
+  split <;> rename_i h
+  · split
+    · simp
+    · dsimp [Constraint.sat'] at w
+      simp_all
+  · split
+    · exact w
+    · exact Constraint.div_sat' h w
+
+/-- Multiply by `-1` if the leading coefficient is negative, otherwise return `none`. -/
+def positivize? : Constraint × Coeffs → Option (Constraint × Coeffs)
+  | ⟨s, x⟩ =>
+    if 0 ≤ x.leading then
+      none
+    else
+      (s.neg, Coeffs.smul x (-1))
+
+/-- Multiply by `-1` if the leading coefficient is negative, otherwise do nothing. -/
+noncomputable def positivize (p : Constraint × Coeffs) : Constraint × Coeffs :=
+  positivize? p |>.getD p
+
+/-- Shorthand for the first component of `positivize`. -/
+noncomputable abbrev positivizeConstraint (s : Constraint) (x : Coeffs) : Constraint :=
+  (positivize (s, x)).1
+/-- Shorthand for the second component of `positivize`. -/
+noncomputable abbrev positivizeCoeffs (s : Constraint) (x : Coeffs) : Coeffs :=
+  (positivize (s, x)).2
+
+theorem positivize?_eq_some (w : positivize? (s, x) = some (s', x')) :
+    positivizeConstraint s x = s' ∧ positivizeCoeffs s x = x' := by
+  simp_all [positivizeConstraint, positivizeCoeffs, positivize]
+
+theorem positivize_sat {s x v} (w : s.sat' x v) :
+    (positivizeConstraint s x).sat' (positivizeCoeffs s x) v := by
+  dsimp [positivizeConstraint, positivizeCoeffs, positivize, positivize?]
+  split
+  · exact w
+  · simp [Constraint.sat']
+    erw [Coeffs.dot_smul_left, ← Int.neg_eq_neg_one_mul]
+    exact Constraint.neg_sat w
+
+/-- `positivize` and `normalize`, returning `none` if neither does anything. -/
+def tidy? : Constraint × Coeffs → Option (Constraint × Coeffs)
+  | ⟨s, x⟩ =>
+    match positivize? (s, x) with
+    | none => match normalize? (s, x) with
+      | none => none
+      | some (s', x') => some (s', x')
+    | some (s', x') => normalize (s', x')
+
+/-- `positivize` and `normalize` -/
+def tidy (p : Constraint × Coeffs) : Constraint × Coeffs :=
+  tidy? p |>.getD p
+
+/-- Shorthand for the first component of `tidy`. -/
+abbrev tidyConstraint (s : Constraint) (x : Coeffs) : Constraint := (tidy (s, x)).1
+/-- Shorthand for the second component of `tidy`. -/
+abbrev tidyCoeffs (s : Constraint) (x : Coeffs) : Coeffs := (tidy (s, x)).2
+
+theorem tidy_sat {s x v} (w : s.sat' x v) : (tidyConstraint s x).sat' (tidyCoeffs s x) v := by
+  dsimp [tidyConstraint, tidyCoeffs, tidy, tidy?]
+  split <;> rename_i hp
+  · split <;> rename_i hn
+    · simp_all
+    · rcases normalize?_eq_some hn with ⟨rfl, rfl⟩
+      exact normalize_sat w
+  · rcases positivize?_eq_some hp with ⟨rfl, rfl⟩
+    exact normalize_sat (positivize_sat w)
+
+theorem combo_sat' (s t : Constraint)
+    (a : Int) (x : Coeffs) (b : Int) (y : Coeffs) (v : Coeffs)
+    (wx : s.sat' x v) (wy : t.sat' y v) :
+    (Constraint.combo a s b t).sat' (Coeffs.combo a x b y) v := by
+  rw [Constraint.sat', Coeffs.combo_eq_smul_add_smul, Coeffs.dot_distrib_left,
+    Coeffs.dot_smul_left, Coeffs.dot_smul_left]
+  exact Constraint.combo_sat a wx b wy
+
+/-- The value of the new variable introduced when solving a hard equality. -/
+abbrev bmod_div_term (m : Nat) (a b : Coeffs) : Int := Coeffs.bmod_dot_sub_dot_bmod m a b / m
+
+/-- The coefficients of the new equation generated when solving a hard equality. -/
+def bmod_coeffs (m : Nat) (i : Nat) (x : Coeffs) : Coeffs :=
+  Coeffs.set (Coeffs.bmod x m) i m
+
+theorem bmod_sat (m : Nat) (r : Int) (i : Nat) (x v : Coeffs)
+    (h : x.length ≤ i)  -- during proof reconstruction this will be by `decide`
+    (p : Coeffs.get v i = bmod_div_term m x v) -- and this will be by `rfl`
+    (w : (Constraint.exact r).sat' x v) :
+    (Constraint.exact (Int.bmod r m)).sat' (bmod_coeffs m i x) v := by
+  simp at w
+  simp only [p, bmod_coeffs, Constraint.exact_sat, Coeffs.dot_set_left, decide_eq_true_eq]
+  replace h := Nat.le_trans (Coeffs.bmod_length x m) h
+  rw [Coeffs.get_of_length_le h, Int.sub_zero,
+    Int.mul_ediv_cancel' (Coeffs.dvd_bmod_dot_sub_dot_bmod _ _ _), w,
+    ← Int.add_sub_assoc, Int.add_comm, Int.add_sub_assoc, Int.sub_self, Int.add_zero]
+
+end Lean.Omega

src/Init/Omega/Int.lean

@@ -0,0 +1,174 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+prelude
+import Init.Data.Int.Order
+
+/-!
+# Lemmas about `Nat` and `Int` needed internally by `omega`.
+
+These statements are useful for constructing proof expressions,
+but unlikely to be widely useful, so are inside the `Std.Tactic.Omega` namespace.
+
+If you do find a use for them, please move them into the appropriate file and namespace!
+-/
+
+namespace Lean.Omega
+
+namespace Int
+
+theorem ofNat_pow (a b : Nat) : ((a ^ b : Nat) : Int) = (a : Int) ^ b := by
+  induction b with
+  | zero => rfl
+  | succ b ih => rw [Nat.pow_succ, Int.ofNat_mul, ih]; rfl
+
+theorem pos_pow_of_pos (a : Int) (b : Nat) (h : 0 < a) : 0 < a ^ b := by
+  rw [Int.eq_natAbs_of_zero_le (Int.le_of_lt h), ← Int.ofNat_zero, ← Int.ofNat_pow, Int.ofNat_lt]
+  exact Nat.pos_pow_of_pos _ (Int.natAbs_pos.mpr (Int.ne_of_gt h))
+
+theorem ofNat_pos {a : Nat} : 0 < (a : Int) ↔ 0 < a := by
+  rw [← Int.ofNat_zero, Int.ofNat_lt]
+
+theorem ofNat_pos_of_pos {a : Nat} (h : 0 < a) : 0 < (a : Int) :=
+  ofNat_pos.mpr h
+
+theorem natCast_ofNat {x : Nat} :
+    @Nat.cast Int instNatCastInt (no_index (OfNat.ofNat x)) = OfNat.ofNat x := rfl
+
+theorem ofNat_lt_of_lt {x y : Nat} (h : x < y) : (x : Int) < (y : Int) :=
+  Int.ofNat_lt.mpr h
+
+theorem ofNat_le_of_le {x y : Nat} (h : x ≤ y) : (x : Int) ≤ (y : Int) :=
+  Int.ofNat_le.mpr h
+
+-- FIXME these are insane:
+theorem lt_of_not_ge {x y : Int} (h : ¬ (x ≤ y)) : y < x := Int.not_le.mp h
+theorem lt_of_not_le {x y : Int} (h : ¬ (x ≤ y)) : y < x := Int.not_le.mp h
+theorem not_le_of_lt {x y : Int} (h : y < x) : ¬ (x ≤ y) := Int.not_le.mpr h
+theorem lt_le_asymm {x y : Int} (h₁ : y < x) (h₂ : x ≤ y) : False := Int.not_le.mpr h₁ h₂
+theorem le_lt_asymm {x y : Int} (h₁ : y ≤ x) (h₂ : x < y) : False := Int.not_lt.mpr h₁ h₂
+
+theorem le_of_not_gt {x y : Int} (h : ¬ (y > x)) : y ≤ x := Int.not_lt.mp h
+theorem not_lt_of_ge {x y : Int} (h : y ≥ x) : ¬ (y < x) := Int.not_lt.mpr h
+theorem le_of_not_lt {x y : Int} (h : ¬ (x < y)) : y ≤ x := Int.not_lt.mp h
+theorem not_lt_of_le {x y : Int} (h : y ≤ x) : ¬ (x < y) := Int.not_lt.mpr h
+
+theorem add_congr {a b c d : Int} (h₁ : a = b) (h₂ : c = d) : a + c = b + d := by
+  subst h₁; subst h₂; rfl
+
+theorem mul_congr {a b c d : Int} (h₁ : a = b) (h₂ : c = d) : a * c = b * d := by
+  subst h₁; subst h₂; rfl
+
+theorem mul_congr_left {a b : Int} (h₁ : a = b)  (c : Int) : a * c = b * c := by
+  subst h₁; rfl
+
+theorem sub_congr {a b c d : Int} (h₁ : a = b) (h₂ : c = d) : a - c = b - d := by
+  subst h₁; subst h₂; rfl
+
+theorem neg_congr {a b : Int} (h₁ : a = b) : -a = -b := by
+  subst h₁; rfl
+
+theorem lt_of_gt {x y : Int} (h : x > y) : y < x := gt_iff_lt.mp h
+theorem le_of_ge {x y : Int} (h : x ≥ y) : y ≤ x := ge_iff_le.mp h
+
+theorem ofNat_sub_eq_zero {b a : Nat} (h : ¬ b ≤ a) : ((a - b : Nat) : Int) = 0 :=
+  Int.ofNat_eq_zero.mpr (Nat.sub_eq_zero_of_le (Nat.le_of_lt (Nat.not_le.mp h)))
+
+theorem ofNat_sub_dichotomy {a b : Nat} :
+    b ≤ a ∧ ((a - b : Nat) : Int) = a - b ∨ a < b ∧ ((a - b : Nat) : Int) = 0 := by
+  by_cases h : b ≤ a
+  · left
+    have t := Int.ofNat_sub h
+    simp at t
+    exact ⟨h, t⟩
+  · right
+    have t := Nat.not_le.mp h
+    simp [Int.ofNat_sub_eq_zero h]
+    exact t
+
+theorem ofNat_congr {a b : Nat} (h : a = b) : (a : Int) = (b : Int) := congrArg _ h
+
+theorem ofNat_sub_sub {a b c : Nat} : ((a - b - c : Nat) : Int) = ((a - (b + c) : Nat) : Int) :=
+  congrArg _ (Nat.sub_sub _ _ _)
+
+theorem ofNat_min (a b : Nat) : ((min a b : Nat) : Int) = min (a : Int) (b : Int) := by
+  simp only [Nat.min_def, Int.min_def, Int.ofNat_le]
+  split <;> rfl
+
+theorem ofNat_max (a b : Nat) : ((max a b : Nat) : Int) = max (a : Int) (b : Int) := by
+  simp only [Nat.max_def, Int.max_def, Int.ofNat_le]
+  split <;> rfl
+
+theorem ofNat_natAbs (a : Int) : (a.natAbs : Int) = if 0 ≤ a then a else -a := by
+  rw [Int.natAbs]
+  split <;> rename_i n
+  · simp only [Int.ofNat_eq_coe]
+    rw [if_pos (Int.ofNat_nonneg n)]
+  · simp; rfl
+
+theorem natAbs_dichotomy {a : Int} : 0 ≤ a ∧ a.natAbs = a ∨ a < 0 ∧ a.natAbs = -a := by
+  by_cases h : 0 ≤ a
+  · left
+    simp_all [Int.natAbs_of_nonneg]
+  · right
+    rw [Int.not_le] at h
+    rw [Int.ofNat_natAbs_of_nonpos (Int.le_of_lt h)]
+    simp_all
+
+theorem neg_le_natAbs {a : Int} : -a ≤ a.natAbs := by
+  have t := Int.le_natAbs (a := -a)
+  simp at t
+  exact t
+
+theorem add_le_iff_le_sub (a b c : Int) : a + b ≤ c ↔ a ≤ c - b := by
+  conv =>
+    lhs
+    rw [← Int.add_zero c, ← Int.sub_self (-b), Int.sub_eq_add_neg, ← Int.add_assoc, Int.neg_neg,
+      Int.add_le_add_iff_right]
+
+theorem le_add_iff_sub_le (a b c : Int) : a ≤ b + c ↔ a - c ≤ b := by
+  conv =>
+    lhs
+    rw [← Int.neg_neg c, ← Int.sub_eq_add_neg, ← add_le_iff_le_sub]
+
+theorem add_le_zero_iff_le_neg (a b : Int) : a + b ≤ 0 ↔ a ≤ - b := by
+  rw [add_le_iff_le_sub, Int.zero_sub]
+theorem add_le_zero_iff_le_neg' (a b : Int) : a + b ≤ 0 ↔ b ≤ -a := by
+  rw [Int.add_comm, add_le_zero_iff_le_neg]
+theorem add_nonnneg_iff_neg_le (a b : Int) : 0 ≤ a + b ↔ -b ≤ a := by
+  rw [le_add_iff_sub_le, Int.zero_sub]
+theorem add_nonnneg_iff_neg_le' (a b : Int) : 0 ≤ a + b ↔ -a ≤ b := by
+  rw [Int.add_comm, add_nonnneg_iff_neg_le]
+
+theorem ofNat_fst_mk {β} {x : Nat} {y : β} : (Prod.mk x y).fst = (x : Int) := rfl
+theorem ofNat_snd_mk {α} {x : α} {y : Nat} : (Prod.mk x y).snd = (y : Int) := rfl
+
+
+end Int
+
+namespace Nat
+
+theorem lt_of_gt {x y : Nat} (h : x > y) : y < x := gt_iff_lt.mp h
+theorem le_of_ge {x y : Nat} (h : x ≥ y) : y ≤ x := ge_iff_le.mp h
+
+end Nat
+
+namespace Prod
+
+theorem of_lex (w : Prod.Lex r s p q) : r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd :=
+  (Prod.lex_def r s).mp w
+
+theorem of_not_lex {α} {r : α → α → Prop} [DecidableEq α] {β} {s : β → β → Prop}
+    {p q : α × β} (w : ¬ Prod.Lex r s p q) :
+    ¬ r p.fst q.fst ∧ (p.fst ≠ q.fst ∨ ¬ s p.snd q.snd) := by
+  rw [Prod.lex_def, not_or, Decidable.not_and_iff_or_not_not] at w
+  exact w
+
+theorem fst_mk : (Prod.mk x y).fst = x := rfl
+theorem snd_mk : (Prod.mk x y).snd = y := rfl
+
+end Prod
+
+end Lean.Omega

src/Init/Omega/IntList.lean

@@ -0,0 +1,412 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+prelude
+import Init.Data.List.Lemmas
+
+namespace Lean.Omega
+
+/--
+A type synonym for `List Int`, used by `omega` for dense representation of coefficients.
+
+We define algebraic operations,
+interpreting `List Int` as a finitely supported function `Nat → Int`.
+-/
+abbrev IntList := List Int
+
+namespace IntList
+
+/-- Get the `i`-th element (interpreted as `0` if the list is not long enough). -/
+def get (xs : IntList) (i : Nat) : Int := (xs.get? i).getD 0
+
+@[simp] theorem get_nil : get ([] : IntList) i = 0 := rfl
+@[simp] theorem get_cons_zero : get (x :: xs) 0 = x := rfl
+@[simp] theorem get_cons_succ : get (x :: xs) (i+1) = get xs i := rfl
+
+theorem get_map {xs : IntList} (h : f 0 = 0) : get (xs.map f) i = f (xs.get i) := by
+  simp only [get, List.get?_map]
+  cases xs.get? i <;> simp_all
+
+theorem get_of_length_le {xs : IntList} (h : xs.length ≤ i) : xs.get i = 0 := by
+  rw [get, List.get?_eq_none.mpr h]
+  rfl
+
+-- theorem lt_length_of_get_nonzero {xs : IntList} (h : xs.get i ≠ 0) : i < xs.length := by
+--   revert h
+--   simpa using mt get_of_length_le
+
+/-- Like `List.set`, but right-pad with zeroes as necessary first. -/
+def set (xs : IntList) (i : Nat) (y : Int) : IntList :=
+  match xs, i with
+  | [], 0 => [y]
+  | [], (i+1) => 0 :: set [] i y
+  | _ :: xs, 0 => y :: xs
+  | x :: xs, (i+1) => x :: set xs i y
+
+@[simp] theorem set_nil_zero : set [] 0 y = [y] := rfl
+@[simp] theorem set_nil_succ : set [] (i+1) y = 0 :: set [] i y := rfl
+@[simp] theorem set_cons_zero : set (x :: xs) 0 y = y :: xs := rfl
+@[simp] theorem set_cons_succ : set (x :: xs) (i+1) y = x :: set xs i y := rfl
+
+/-- Returns the leading coefficient, i.e. the first non-zero entry. -/
+def leading (xs : IntList) : Int := xs.find? (! · == 0) |>.getD 0
+
+/-- Implementation of `+` on `IntList`. -/
+def add (xs ys : IntList) : IntList :=
+  List.zipWithAll (fun x y => x.getD 0 + y.getD 0) xs ys
+
+instance : Add IntList := ⟨add⟩
+
+theorem add_def (xs ys : IntList) :
+    xs + ys = List.zipWithAll (fun x y => x.getD 0 + y.getD 0) xs ys :=
+  rfl
+
+@[simp] theorem add_get (xs ys : IntList) (i : Nat) : (xs + ys).get i = xs.get i + ys.get i := by
+  simp only [add_def, get, List.zipWithAll_get?, List.get?_eq_none]
+  cases xs.get? i <;> cases ys.get? i <;> simp
+
+@[simp] theorem add_nil (xs : IntList) : xs + [] = xs := by simp [add_def]
+@[simp] theorem nil_add (xs : IntList) : [] + xs = xs := by simp [add_def]
+@[simp] theorem cons_add_cons (x) (xs : IntList) (y) (ys : IntList) :
+    (x :: xs) + (y :: ys) = (x + y) :: (xs + ys) := by simp [add_def]
+
+/-- Implementation of `*` on `IntList`. -/
+def mul (xs ys : IntList) : IntList := List.zipWith (· * ·) xs ys
+
+instance : Mul IntList := ⟨mul⟩
+
+theorem mul_def (xs ys : IntList) : xs * ys = List.zipWith (· * ·) xs ys :=
+  rfl
+
+@[simp] theorem mul_get (xs ys : IntList) (i : Nat) : (xs * ys).get i = xs.get i * ys.get i := by
+  simp only [mul_def, get, List.zipWith_get?]
+  cases xs.get? i <;> cases ys.get? i <;> simp
+
+@[simp] theorem mul_nil_left : ([] : IntList) * ys = [] := rfl
+@[simp] theorem mul_nil_right : xs * ([] : IntList) = [] := List.zipWith_nil_right
+@[simp] theorem mul_cons₂ : (x::xs : IntList) * (y::ys) = (x * y) :: (xs * ys) := rfl
+
+/-- Implementation of negation on `IntList`. -/
+def neg (xs : IntList) : IntList := xs.map fun x => -x
+
+instance : Neg IntList := ⟨neg⟩
+
+theorem neg_def (xs : IntList) : - xs = xs.map fun x => -x := rfl
+
+@[simp] theorem neg_get (xs : IntList) (i : Nat) : (- xs).get i = - xs.get i := by
+  simp only [neg_def, get, List.get?_map]
+  cases xs.get? i <;> simp
+
+@[simp] theorem neg_nil : (- ([] : IntList)) = [] := rfl
+@[simp] theorem neg_cons : (- (x::xs : IntList)) = -x :: -xs := rfl
+
+/-- Implementation of subtraction on `IntList`. -/
+def sub (xs ys : IntList) : IntList :=
+  List.zipWithAll (fun x y => x.getD 0 - y.getD 0) xs ys
+
+instance : Sub IntList := ⟨sub⟩
+
+theorem sub_def (xs ys : IntList) :
+    xs - ys = List.zipWithAll (fun x y => x.getD 0 - y.getD 0) xs ys :=
+  rfl
+
+/-- Implementation of scalar multiplication by an integer on `IntList`. -/
+def smul (xs : IntList) (i : Int) : IntList :=
+  xs.map fun x => i * x
+
+instance : HMul Int IntList IntList where
+  hMul i xs := xs.smul i
+
+theorem smul_def (xs : IntList) (i : Int) : i * xs = xs.map fun x => i * x := rfl
+
+@[simp] theorem smul_get (xs : IntList) (a : Int) (i : Nat) : (a * xs).get i = a * xs.get i := by
+  simp only [smul_def, get, List.get?_map]
+  cases xs.get? i <;> simp
+
+@[simp] theorem smul_nil {i : Int} : i * ([] : IntList) = [] := rfl
+@[simp] theorem smul_cons {i : Int} : i * (x::xs : IntList) = i * x :: i * xs := rfl
+
+/-- A linear combination of two `IntList`s. -/
+def combo (a : Int) (xs : IntList) (b : Int) (ys : IntList) : IntList :=
+  List.zipWithAll (fun x y => a * x.getD 0 + b * y.getD 0) xs ys
+
+theorem combo_eq_smul_add_smul (a : Int) (xs : IntList) (b : Int) (ys : IntList) :
+    combo a xs b ys = a * xs + b * ys := by
+  dsimp [combo]
+  induction xs generalizing ys with
+  | nil => simp; rfl
+  | cons x xs ih =>
+    cases ys with
+    | nil => simp; rfl
+    | cons y ys => simp_all
+
+attribute [local simp] add_def mul_def in
+theorem mul_distrib_left (xs ys zs : IntList) : (xs + ys) * zs = xs * zs + ys * zs := by
+  induction xs generalizing ys zs with
+  | nil =>
+    cases ys with
+    | nil => simp
+    | cons _ _ =>
+      cases zs with
+      | nil => simp
+      | cons _ _ => simp_all [Int.add_mul]
+  | cons x xs ih₁ =>
+    cases ys with
+    | nil => simp_all
+    | cons _ _ =>
+      cases zs with
+      | nil => simp
+      | cons _ _ => simp_all [Int.add_mul]
+
+theorem mul_neg_left (xs ys : IntList) : (-xs) * ys = -(xs * ys) := by
+  induction xs generalizing ys with
+  | nil => simp
+  | cons x xs ih =>
+    cases ys with
+    | nil => simp
+    | cons y ys => simp_all [Int.neg_mul]
+
+attribute [local simp] add_def neg_def sub_def in
+theorem sub_eq_add_neg (xs ys : IntList) : xs - ys = xs + (-ys) := by
+  induction xs generalizing ys with
+  | nil => simp; rfl
+  | cons x xs ih =>
+    cases ys with
+    | nil => simp
+    | cons y ys => simp_all [Int.sub_eq_add_neg]
+
+@[simp] theorem mul_smul_left {i : Int} {xs ys : IntList} : (i * xs) * ys = i * (xs * ys) := by
+  induction xs generalizing ys with
+  | nil => simp
+  | cons x xs ih =>
+    cases ys with
+    | nil => simp
+    | cons y ys => simp_all [Int.mul_assoc]
+
+/-- The sum of the entries of an `IntList`. -/
+def sum (xs : IntList) : Int := xs.foldr (· + ·) 0
+
+@[simp] theorem sum_nil : sum ([] : IntList) = 0 := rfl
+@[simp] theorem sum_cons : sum (x::xs : IntList) = x + sum xs := rfl
+
+attribute [local simp] sum add_def in
+theorem sum_add (xs ys : IntList) : (xs + ys).sum = xs.sum + ys.sum := by
+  induction xs generalizing ys with
+  | nil => simp
+  | cons x xs ih =>
+    cases ys with
+    | nil => simp
+    | cons y ys => simp_all [Int.add_assoc, Int.add_left_comm]
+
+@[simp]
+theorem sum_neg (xs : IntList) : (-xs).sum = -(xs.sum) := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih => simp_all [Int.neg_add]
+
+@[simp]
+theorem sum_smul (i : Int) (xs : IntList) : (i * xs).sum = i * (xs.sum) := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih => simp_all [Int.mul_add]
+
+/-- The dot product of two `IntList`s. -/
+def dot (xs ys : IntList) : Int := (xs * ys).sum
+
+example : IntList.dot [a, b, c] [x, y, z] = IntList.dot [a, b, c, d] [x, y, z] := rfl
+example : IntList.dot [a, b, c] [x, y, z] = IntList.dot [a, b, c] [x, y, z, w] := rfl
+
+@[local simp] theorem dot_nil_left : dot ([] : IntList) ys = 0 := rfl
+@[simp] theorem dot_nil_right : dot xs ([] : IntList) = 0 := by simp [dot]
+@[simp] theorem dot_cons₂ : dot (x::xs) (y::ys) = x * y + dot xs ys := rfl
+
+-- theorem dot_comm (xs ys : IntList) : dot xs ys = dot ys xs := by
+--   rw [dot, dot, mul_comm]
+
+@[simp] theorem dot_set_left (xs ys : IntList) (i : Nat) (z : Int) :
+    dot (xs.set i z) ys = dot xs ys + (z - xs.get i) * ys.get i := by
+  induction xs generalizing i ys with
+  | nil =>
+    induction i generalizing ys with
+    | zero => cases ys <;> simp
+    | succ i => cases ys <;> simp_all
+  | cons x xs ih =>
+    induction i generalizing ys with
+    | zero =>
+      cases ys with
+      | nil => simp
+      | cons y ys =>
+        simp only [Nat.zero_eq, set_cons_zero, dot_cons₂, get_cons_zero, Int.sub_mul]
+        rw [Int.add_right_comm, Int.add_comm (x * y), Int.sub_add_cancel]
+    | succ i =>
+      cases ys with
+      | nil => simp
+      | cons y ys => simp_all [Int.add_assoc]
+
+theorem dot_distrib_left (xs ys zs : IntList) : (xs + ys).dot zs = xs.dot zs + ys.dot zs := by
+  simp [dot, mul_distrib_left, sum_add]
+
+@[simp] theorem dot_neg_left (xs ys : IntList) : (-xs).dot ys = -(xs.dot ys) := by
+  simp [dot, mul_neg_left]
+
+@[simp] theorem dot_smul_left (xs ys : IntList) (i : Int) : (i * xs).dot ys = i * xs.dot ys := by
+  simp [dot]
+
+theorem dot_of_left_zero (w : ∀ x, x ∈ xs → x = 0) : dot xs ys = 0 := by
+  induction xs generalizing ys with
+  | nil => simp
+  | cons x xs ih =>
+    cases ys with
+    | nil => simp
+    | cons y ys =>
+      rw [dot_cons₂, w x (by simp), ih]
+      · simp
+      · intro x m
+        apply w
+        exact List.mem_cons_of_mem _ m
+
+/-- Division of an `IntList` by a integer. -/
+def sdiv (xs : IntList) (g : Int) : IntList := xs.map fun x => x / g
+
+@[simp] theorem sdiv_nil : sdiv [] g = [] := rfl
+@[simp] theorem sdiv_cons : sdiv (x::xs) g = (x / g) :: sdiv xs g := rfl
+
+/-- The gcd of the absolute values of the entries of an `IntList`. -/
+def gcd (xs : IntList) : Nat := xs.foldr (fun x g => Nat.gcd x.natAbs g) 0
+
+@[simp] theorem gcd_nil : gcd [] = 0 := rfl
+@[simp] theorem gcd_cons : gcd (x :: xs) = Nat.gcd x.natAbs (gcd xs) := rfl
+
+theorem gcd_cons_div_left : (gcd (x::xs) : Int) ∣ x := by
+  simp only [gcd, List.foldr_cons, Int.ofNat_dvd_left]
+  apply Nat.gcd_dvd_left
+
+theorem gcd_cons_div_right : gcd (x::xs) ∣ gcd xs := by
+  simp only [gcd, List.foldr_cons]
+  apply Nat.gcd_dvd_right
+
+theorem gcd_cons_div_right' : (gcd (x::xs) : Int) ∣ (gcd xs : Int) := by
+  rw [Int.ofNat_dvd_left, Int.natAbs_ofNat]
+  exact gcd_cons_div_right
+
+theorem gcd_dvd (xs : IntList) {a : Int} (m : a ∈ xs) : (xs.gcd : Int) ∣ a := by
+  rw [Int.ofNat_dvd_left]
+  induction m with
+  | head =>
+    simp only [gcd_cons]
+    apply Nat.gcd_dvd_left
+  | tail b m ih =>   -- FIXME: why is the argument of tail implicit?
+    simp only [gcd_cons]
+    exact Nat.dvd_trans (Nat.gcd_dvd_right _ _) ih
+
+theorem dvd_gcd (xs : IntList) (c : Nat) (w : ∀ {a : Int}, a ∈ xs → (c : Int) ∣ a) :
+    c ∣ xs.gcd := by
+  simp only [Int.ofNat_dvd_left] at w
+  induction xs with
+  | nil => have := Nat.dvd_zero c; simp at this; exact this
+  | cons x xs ih =>
+    simp
+    apply Nat.dvd_gcd
+    · apply w
+      simp
+    · apply ih
+      intro b m
+      apply w
+      exact List.mem_cons_of_mem x m
+
+theorem gcd_eq_iff (xs : IntList) (g : Nat) :
+    xs.gcd = g ↔
+      (∀ {a : Int}, a ∈ xs → (g : Int) ∣ a) ∧
+        (∀ (c : Nat), (∀ {a : Int}, a ∈ xs → (c : Int) ∣ a) → c ∣ g) := by
+  constructor
+  · rintro rfl
+    exact ⟨gcd_dvd _, dvd_gcd _⟩
+  · rintro ⟨hi, hg⟩
+    apply Nat.dvd_antisymm
+    · apply hg
+      intro i m
+      exact gcd_dvd xs m
+    · exact dvd_gcd xs g hi
+
+attribute [simp] Int.zero_dvd
+
+@[simp] theorem gcd_eq_zero (xs : IntList) : xs.gcd = 0 ↔ ∀ x, x ∈ xs → x = 0 := by
+  simp [gcd_eq_iff, Nat.dvd_zero]
+
+@[simp] theorem dot_mod_gcd_left (xs ys : IntList) : dot xs ys % xs.gcd = 0 := by
+  induction xs generalizing ys with
+  | nil => simp
+  | cons x xs ih =>
+    cases ys with
+    | nil => simp
+    | cons y ys =>
+      rw [dot_cons₂, Int.add_emod,
+        ← Int.emod_emod_of_dvd (x * y) (gcd_cons_div_left),
+        ← Int.emod_emod_of_dvd (dot xs ys) (Int.ofNat_dvd.mpr gcd_cons_div_right)]
+      simp_all
+
+theorem gcd_dvd_dot_left (xs ys : IntList) : (xs.gcd : Int) ∣ dot xs ys :=
+  Int.dvd_of_emod_eq_zero (dot_mod_gcd_left xs ys)
+
+@[simp]
+theorem dot_eq_zero_of_left_eq_zero {xs ys : IntList} (h : ∀ x, x ∈ xs → x = 0) : dot xs ys = 0 := by
+  induction xs generalizing ys with
+  | nil => rfl
+  | cons x xs ih =>
+    cases ys with
+    | nil => rfl
+    | cons y ys =>
+      rw [dot_cons₂, h x (List.mem_cons_self _ _), ih (fun x m => h x (List.mem_cons_of_mem _ m)),
+        Int.zero_mul, Int.add_zero]
+
+theorem dot_sdiv_left (xs ys : IntList) {d : Int} (h : d ∣ xs.gcd) :
+    dot (xs.sdiv d) ys = (dot xs ys) / d := by
+  induction xs generalizing ys with
+  | nil => simp
+  | cons x xs ih =>
+    cases ys with
+    | nil => simp
+    | cons y ys =>
+      have wx : d ∣ x := Int.dvd_trans h (gcd_cons_div_left)
+      have wxy : d ∣ x * y := Int.dvd_trans wx (Int.dvd_mul_right x y)
+      have w : d ∣ (IntList.gcd xs : Int) := Int.dvd_trans h (gcd_cons_div_right')
+      simp_all [Int.add_ediv_of_dvd_left, Int.mul_ediv_assoc']
+
+/-- Apply "balanced mod" to each entry in an `IntList`. -/
+abbrev bmod (x : IntList) (m : Nat) : IntList := x.map (Int.bmod · m)
+
+theorem bmod_length (x : IntList) (m) : (bmod x m).length ≤ x.length :=
+  Nat.le_of_eq (List.length_map _ _)
+
+/--
+The difference between the balanced mod of a dot product,
+and the dot product with balanced mod applied to each entry of the left factor.
+-/
+abbrev bmod_dot_sub_dot_bmod (m : Nat) (a b : IntList) : Int :=
+    (Int.bmod (dot a b) m) - dot (bmod a m) b
+
+theorem dvd_bmod_dot_sub_dot_bmod (m : Nat) (xs ys : IntList) :
+    (m : Int) ∣ bmod_dot_sub_dot_bmod m xs ys := by
+  dsimp [bmod_dot_sub_dot_bmod]
+  rw [Int.dvd_iff_emod_eq_zero]
+  induction xs generalizing ys with
+  | nil => simp
+  | cons x xs ih =>
+    cases ys with
+    | nil => simp
+    | cons y ys =>
+      simp only [IntList.dot_cons₂, List.map_cons]
+      specialize ih ys
+      rw [Int.sub_emod, Int.bmod_emod] at ih
+      rw [Int.sub_emod, Int.bmod_emod, Int.add_emod, Int.add_emod (Int.bmod x m * y),
+        ← Int.sub_emod, ← Int.sub_sub, Int.sub_eq_add_neg, Int.sub_eq_add_neg,
+        Int.add_assoc (x * y % m), Int.add_comm (IntList.dot _ _ % m), ← Int.add_assoc,
+        Int.add_assoc, ← Int.sub_eq_add_neg, ← Int.sub_eq_add_neg, Int.add_emod, ih, Int.add_zero,
+        Int.emod_emod, Int.mul_emod, Int.mul_emod (Int.bmod x m), Int.bmod_emod, Int.sub_self,
+        Int.zero_emod]
+
+end IntList
+
+end Lean.Omega

src/Init/Omega/LinearCombo.lean

@@ -0,0 +1,178 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+prelude
+import Init.Omega.Coeffs
+
+/-!
+# Linear combinations
+
+We use this data structure while processing hypotheses.
+
+-/
+
+namespace Lean.Omega
+
+/-- Internal representation of a linear combination of atoms, and a constant term. -/
+structure LinearCombo where
+  /-- Constant term. -/
+  const : Int := 0
+  /-- Coefficients of the atoms. -/
+  coeffs : Coeffs := []
+deriving DecidableEq, Repr
+
+namespace LinearCombo
+
+instance : ToString LinearCombo where
+  toString lc :=
+    s!"{lc.const}{String.join <| lc.coeffs.toList.enum.map fun ⟨i, c⟩ => s!" + {c} * x{i+1}"}"
+
+instance : Inhabited LinearCombo := ⟨{const := 1}⟩
+
+theorem ext {a b : LinearCombo} (w₁ : a.const = b.const) (w₂ : a.coeffs = b.coeffs) :
+    a = b := by
+  cases a; cases b
+  subst w₁; subst w₂
+  congr
+
+/--
+Evaluate a linear combination `⟨r, [c_1, …, c_k]⟩` at values `[v_1, …, v_k]` to obtain
+`r + (c_1 * x_1 + (c_2 * x_2 + ... (c_k * x_k + 0))))`.
+-/
+def eval (lc : LinearCombo) (values : Coeffs) : Int :=
+  lc.const + lc.coeffs.dot values
+
+@[simp] theorem eval_nil : (lc : LinearCombo).eval .nil = lc.const := by
+  simp [eval]
+
+/-- The `i`-th coordinate function. -/
+def coordinate (i : Nat) : LinearCombo where
+  const := 0
+  coeffs := Coeffs.set .nil i 1
+
+@[simp] theorem coordinate_eval (i : Nat) (v : Coeffs) :
+    (coordinate i).eval v = v.get i := by
+  simp [eval, coordinate]
+
+theorem coordinate_eval_0 : (coordinate 0).eval (.ofList (a0 :: t)) = a0 := by simp
+theorem coordinate_eval_1 : (coordinate 1).eval (.ofList (a0 :: a1 :: t)) = a1 := by simp
+theorem coordinate_eval_2 : (coordinate 2).eval (.ofList (a0 :: a1 :: a2 :: t)) = a2 := by simp
+theorem coordinate_eval_3 :
+    (coordinate 3).eval (.ofList (a0 :: a1 :: a2 :: a3 :: t)) = a3 := by simp
+theorem coordinate_eval_4 :
+    (coordinate 4).eval (.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: t)) = a4 := by simp
+theorem coordinate_eval_5 :
+    (coordinate 5).eval (.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: t)) = a5 := by simp
+theorem coordinate_eval_6 :
+    (coordinate 6).eval (.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: t)) = a6 := by simp
+theorem coordinate_eval_7 :
+    (coordinate 7).eval
+      (.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: t)) = a7 := by simp
+theorem coordinate_eval_8 :
+    (coordinate 8).eval
+      (.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: a8 :: t)) = a8 := by simp
+theorem coordinate_eval_9 :
+    (coordinate 9).eval
+      (.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: a8 :: a9 :: t)) = a9 := by simp
+
+/-- Implementation of addition on `LinearCombo`. -/
+def add (l₁ l₂ : LinearCombo) : LinearCombo where
+  const := l₁.const + l₂.const
+  coeffs := l₁.coeffs + l₂.coeffs
+
+instance : Add LinearCombo := ⟨add⟩
+
+@[simp] theorem add_const {l₁ l₂ : LinearCombo} : (l₁ + l₂).const = l₁.const + l₂.const := rfl
+@[simp] theorem add_coeffs {l₁ l₂ : LinearCombo} : (l₁ + l₂).coeffs = l₁.coeffs + l₂.coeffs := rfl
+
+/-- Implementation of subtraction on `LinearCombo`. -/
+def sub (l₁ l₂ : LinearCombo) : LinearCombo where
+  const := l₁.const - l₂.const
+  coeffs := l₁.coeffs - l₂.coeffs
+
+instance : Sub LinearCombo := ⟨sub⟩
+
+@[simp] theorem sub_const {l₁ l₂ : LinearCombo} : (l₁ - l₂).const = l₁.const - l₂.const := rfl
+@[simp] theorem sub_coeffs {l₁ l₂ : LinearCombo} : (l₁ - l₂).coeffs = l₁.coeffs - l₂.coeffs := rfl
+
+/-- Implementation of negation on `LinearCombo`. -/
+def neg (lc : LinearCombo) : LinearCombo where
+  const := -lc.const
+  coeffs := -lc.coeffs
+
+instance : Neg LinearCombo := ⟨neg⟩
+
+@[simp] theorem neg_const {l : LinearCombo} : (-l).const = -l.const := rfl
+@[simp] theorem neg_coeffs {l : LinearCombo} : (-l).coeffs = -l.coeffs  := rfl
+
+theorem sub_eq_add_neg (l₁ l₂ : LinearCombo) : l₁ - l₂ = l₁ + -l₂ := by
+  rcases l₁ with ⟨a₁, c₁⟩; rcases l₂ with ⟨a₂, c₂⟩
+  apply ext
+  · simp [Int.sub_eq_add_neg]
+  · simp [Coeffs.sub_eq_add_neg]
+
+/-- Implementation of scalar multiplication of a `LinearCombo` by an `Int`. -/
+def smul (lc : LinearCombo) (i : Int) : LinearCombo where
+  const := i * lc.const
+  coeffs := lc.coeffs.smul i
+
+instance : HMul Int LinearCombo LinearCombo := ⟨fun i lc => lc.smul i⟩
+
+@[simp] theorem smul_const {lc : LinearCombo} {i : Int} : (i * lc).const = i * lc.const := rfl
+@[simp] theorem smul_coeffs {lc : LinearCombo} {i : Int} : (i * lc).coeffs = i * lc.coeffs := rfl
+
+@[simp] theorem add_eval (l₁ l₂ : LinearCombo) (v : Coeffs) :
+    (l₁ + l₂).eval v = l₁.eval v + l₂.eval v := by
+  rcases l₁ with ⟨r₁, c₁⟩; rcases l₂ with ⟨r₂, c₂⟩
+  simp only [eval, add_const, add_coeffs, Int.add_assoc, Int.add_left_comm]
+  congr
+  exact Coeffs.dot_distrib_left c₁ c₂ v
+
+@[simp] theorem neg_eval (lc : LinearCombo) (v : Coeffs) : (-lc).eval v = - lc.eval v := by
+  rcases lc with ⟨a, coeffs⟩
+  simp [eval, Int.neg_add]
+
+@[simp] theorem sub_eval (l₁ l₂ : LinearCombo) (v : Coeffs) :
+    (l₁ - l₂).eval v = l₁.eval v - l₂.eval v := by
+  simp [sub_eq_add_neg, Int.sub_eq_add_neg]
+
+@[simp] theorem smul_eval (lc : LinearCombo) (i : Int) (v : Coeffs) :
+    (i * lc).eval v = i * lc.eval v := by
+  rcases lc with ⟨a, coeffs⟩
+  simp [eval, Int.mul_add]
+
+theorem smul_eval_comm (lc : LinearCombo) (i : Int) (v : Coeffs) :
+    (i * lc).eval v = lc.eval v * i := by
+  simp [Int.mul_comm]
+
+/--
+Multiplication of two linear combinations.
+This is useful only if at least one of the linear combinations is constant,
+and otherwise should be considered as a junk value.
+-/
+def mul (l₁ l₂ : LinearCombo) : LinearCombo :=
+  l₂.const * l₁ + l₁.const * l₂ - { const := l₁.const * l₂.const }
+
+theorem mul_eval_of_const_left (l₁ l₂ : LinearCombo) (v : Coeffs) (w : l₁.coeffs.isZero) :
+    (mul l₁ l₂).eval v = l₁.eval v * l₂.eval v := by
+  have : Coeffs.dot l₁.coeffs v = 0 := IntList.dot_of_left_zero w
+  simp [mul, eval, this, Coeffs.sub_eq_add_neg, Coeffs.dot_distrib_left, Int.add_mul, Int.mul_add,
+    Int.mul_comm]
+
+theorem mul_eval_of_const_right (l₁ l₂ : LinearCombo) (v : Coeffs) (w : l₂.coeffs.isZero) :
+    (mul l₁ l₂).eval v = l₁.eval v * l₂.eval v := by
+  have : Coeffs.dot l₂.coeffs v = 0 := IntList.dot_of_left_zero w
+  simp [mul, eval, this, Coeffs.sub_eq_add_neg, Coeffs.dot_distrib_left, Int.add_mul, Int.mul_add,
+    Int.mul_comm]
+
+theorem mul_eval (l₁ l₂ : LinearCombo) (v : Coeffs) (w : l₁.coeffs.isZero ∨ l₂.coeffs.isZero) :
+    (mul l₁ l₂).eval v = l₁.eval v * l₂.eval v := by
+  rcases w with w | w
+  · rw [mul_eval_of_const_left _ _ _ w]
+  · rw [mul_eval_of_const_right _ _ _ w]
+
+end LinearCombo
+
+end Lean.Omega

src/Init/Omega/Logic.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+prelude
+import Init.PropLemmas
+/-!
+# Specializations of basic logic lemmas
+
+These are useful for `omega` while constructing proofs, but not considered generally useful
+so are hidden in the `Std.Tactic.Omega` namespace.
+
+If you find yourself needing them elsewhere, please move them first to another file.
+-/
+
+namespace Lean.Omega
+
+theorem and_not_not_of_not_or (h : ¬ (p ∨ q)) : ¬ p ∧ ¬ q := not_or.mp h
+
+theorem Decidable.or_not_not_of_not_and [Decidable p] [Decidable q]
+    (h : ¬ (p ∧ q)) : ¬ p ∨ ¬ q :=
+  (Decidable.not_and_iff_or_not _ _).mp h
+
+theorem Decidable.and_or_not_and_not_of_iff {p q : Prop} [Decidable q] (h : p ↔ q) :
+    (p ∧ q) ∨ (¬p ∧ ¬q) := Decidable.iff_iff_and_or_not_and_not.mp h
+
+theorem Decidable.not_iff_iff_and_not_or_not_and [Decidable a] [Decidable b] :
+    (¬ (a ↔ b)) ↔ (a ∧ ¬ b) ∨ ((¬ a) ∧ b) :=
+  ⟨fun e => if hb : b then
+    .inr ⟨fun ha => e ⟨fun _ => hb, fun _ => ha⟩, hb⟩
+  else
+    .inl ⟨if ha : a then ha else False.elim (e ⟨fun ha' => absurd ha' ha, fun hb' => absurd hb' hb⟩), hb⟩,
+  Or.rec (And.rec fun ha nb w => nb (w.mp ha)) (And.rec fun na hb w => na (w.mpr hb))⟩
+
+theorem Decidable.and_not_or_not_and_of_not_iff [Decidable a] [Decidable b]
+    (h : ¬ (a ↔ b)) : a ∧ ¬b ∨ ¬a ∧ b :=
+  Decidable.not_iff_iff_and_not_or_not_and.mp h
+
+theorem Decidable.and_not_of_not_imp [Decidable a] (h : ¬(a → b)) : a ∧ ¬b :=
+  Decidable.not_imp_iff_and_not.mp h
+
+theorem ite_disjunction {α : Type u} {P : Prop} [Decidable P] {a b : α} :
+    (P ∧ (if P then a else b) = a) ∨ (¬ P ∧ (if P then a else b) = b) :=
+  if h : P then
+    .inl ⟨h, if_pos h⟩
+  else
+    .inr ⟨h, if_neg h⟩
+
+end Lean.Omega

src/Init/Tactics.lean

@@ -566,6 +566,52 @@ definitionally equal to the input.
 syntax (name := dsimp) "dsimp" (config)? (discharger)? (&" only")?
   (" [" withoutPosition((simpErase <|> simpLemma),*,?) "]")? (location)? : tactic
 
+/--
+A `simpArg` is either a `*`, `-lemma` or a simp lemma specification
+(which includes the `↑` `↓` `←` specifications for pre, post, reverse rewriting).
+-/
+def simpArg := simpStar.binary `orelse (simpErase.binary `orelse simpLemma)
+
+/-- A simp args list is a list of `simpArg`. This is the main argument to `simp`. -/
+syntax simpArgs := " [" simpArg,* "]"
+
+/--
+A `dsimpArg` is similar to `simpArg`, but it does not have the `simpStar` form
+because it does not make sense to use hypotheses in `dsimp`.
+-/
+def dsimpArg := simpErase.binary `orelse simpLemma
+
+/-- A dsimp args list is a list of `dsimpArg`. This is the main argument to `dsimp`. -/
+syntax dsimpArgs := " [" dsimpArg,* "]"
+
+/-- The arguments to the `simpa` family tactics. -/
+syntax simpaArgsRest := (config)? (discharger)? &" only "? (simpArgs)? (" using " term)?
+
+/--
+This is a "finishing" tactic modification of `simp`. It has two forms.
+
+* `simpa [rules, ⋯] using e` will simplify the goal and the type of
+  `e` using `rules`, then try to close the goal using `e`.
+
+  Simplifying the type of `e` makes it more likely to match the goal
+  (which has also been simplified). This construction also tends to be
+  more robust under changes to the simp lemma set.
+
+* `simpa [rules, ⋯]` will simplify the goal and the type of a
+  hypothesis `this` if present in the context, then try to close the goal using
+  the `assumption` tactic.
+-/
+syntax (name := simpa) "simpa" "?"? "!"? simpaArgsRest : tactic
+
+@[inherit_doc simpa] macro "simpa!" rest:simpaArgsRest : tactic =>
+  `(tactic| simpa ! $rest:simpaArgsRest)
+
+@[inherit_doc simpa] macro "simpa?" rest:simpaArgsRest : tactic =>
+  `(tactic| simpa ? $rest:simpaArgsRest)
+
+@[inherit_doc simpa] macro "simpa?!" rest:simpaArgsRest : tactic =>
+  `(tactic| simpa ?! $rest:simpaArgsRest)
+
 /--
 `delta id1 id2 ...` delta-expands the definitions `id1`, `id2`, ....
 This is a low-level tactic, it will expose how recursive definitions have been
@@ -972,6 +1018,40 @@ macro "haveI" d:haveDecl : tactic => `(tactic| refine_lift haveI $d:haveDecl; ?_
 /-- `letI` behaves like `let`, but inlines the value instead of producing a `let_fun` term. -/
 macro "letI" d:haveDecl : tactic => `(tactic| refine_lift letI $d:haveDecl; ?_)
 
+
+/--
+The `omega` tactic, for resolving integer and natural linear arithmetic problems.
+
+It is not yet a full decision procedure (no "dark" or "grey" shadows),
+but should be effective on many problems.
+
+We handle hypotheses of the form `x = y`, `x < y`, `x ≤ y`, and `k ∣ x` for `x y` in `Nat` or `Int`
+(and `k` a literal), along with negations of these statements.
+
+We decompose the sides of the inequalities as linear combinations of atoms.
+
+If we encounter `x / k` or `x % k` for literal integers `k` we introduce new auxiliary variables
+and the relevant inequalities.
+
+On the first pass, we do not perform case splits on natural subtraction.
+If `omega` fails, we recursively perform a case split on
+a natural subtraction appearing in a hypothesis, and try again.
+
+The options
+```
+omega (config :=
+  { splitDisjunctions := true, splitNatSub := true, splitNatAbs := true, splitMinMax := true })
+```
+can be used to:
+* `splitDisjunctions`: split any disjunctions found in the context,
+  if the problem is not otherwise solvable.
+* `splitNatSub`: for each appearance of `((a - b : Nat) : Int)`, split on `a ≤ b` if necessary.
+* `splitNatAbs`: for each appearance of `Int.natAbs a`, split on `0 ≤ a` if necessary.
+* `splitMinMax`: for each occurrence of `min a b`, split on `min a b = a ∨ min a b = b`
+Currently, all of these are on by default.
+-/
+syntax (name := omega) "omega" (config)? : tactic
+
 end Tactic
 
 namespace Attr

src/Init/WFTactics.lean

@@ -11,7 +11,7 @@ import Init.WF
 /-- Unfold definitions commonly used in well founded relation definitions.
 This is primarily intended for internal use in `decreasing_tactic`. -/
 macro "simp_wf" : tactic =>
-  `(tactic| try simp (config := { unfoldPartialApp := true }) [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel])
+  `(tactic| try simp (config := { unfoldPartialApp := true, zetaDelta := true }) [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel])
 
 /-- Extensible helper tactic for `decreasing_tactic`. This handles the "base case"
 reasoning after applying lexicographic order lemmas.

src/Lean/Attributes.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.CoreM
 import Lean.MonadEnv
 

src/Lean/AuxRecursor.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Environment
 
 namespace Lean

src/Lean/Class.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Attributes
 
 namespace Lean

src/Lean/Compiler.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.InlineAttrs
 import Lean.Compiler.Specialize
 import Lean.Compiler.ConstFolding

src/Lean/Compiler/AtMostOnce.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Environment
 
 namespace Lean.Compiler

src/Lean/Compiler/BorrowedAnnotation.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Expr
 namespace Lean
 

src/Lean/Compiler/CSimpAttr.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.ScopedEnvExtension
 import Lean.Util.Recognizers
 import Lean.Util.ReplaceExpr

src/Lean/Compiler/ClosedTermCache.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Environment
 
 namespace Lean

src/Lean/Compiler/ConstFolding.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Expr
 
 /-! Constant folding for primitives that have special runtime support. -/

src/Lean/Compiler/ExportAttr.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Attributes
 
 namespace Lean

src/Lean/Compiler/ExternAttr.lean

@@ -3,6 +3,8 @@ Copyright (c) 2019 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.List.BasicAux
 import Lean.Expr
 import Lean.Environment
 import Lean.Attributes

src/Lean/Compiler/FFI.lean

@@ -3,6 +3,9 @@ Copyright (c) 2021 Sebastian Ullrich. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich
 -/
+prelude
+import Init.Data.Array.Basic
+import Init.System.FilePath
 
 open System
 

src/Lean/Compiler/IR.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.Basic
 import Lean.Compiler.IR.Format
 import Lean.Compiler.IR.CompilerM

src/Lean/Compiler/IR/Basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Data.KVMap
 import Lean.Data.Name
 import Lean.Data.Format

src/Lean/Compiler/IR/Borrow.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.ExportAttr
 import Lean.Compiler.IR.CompilerM
 import Lean.Compiler.IR.NormIds

src/Lean/Compiler/IR/Boxing.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Runtime
 import Lean.Compiler.ClosedTermCache
 import Lean.Compiler.ExternAttr

src/Lean/Compiler/IR/Checker.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.CompilerM
 import Lean.Compiler.IR.Format
 

src/Lean/Compiler/IR/CompilerM.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Environment
 import Lean.Compiler.IR.Basic
 import Lean.Compiler.IR.Format

src/Lean/Compiler/IR/CtorLayout.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Environment
 import Lean.Compiler.IR.Format
 

src/Lean/Compiler/IR/ElimDeadBranches.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.Format
 import Lean.Compiler.IR.Basic
 import Lean.Compiler.IR.CompilerM

src/Lean/Compiler/IR/ElimDeadVars.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.Basic
 import Lean.Compiler.IR.FreeVars
 

src/Lean/Compiler/IR/EmitC.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Runtime
 import Lean.Compiler.NameMangling
 import Lean.Compiler.ExportAttr

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Siddharth Bhat
 -/
-
+prelude
 import Lean.Data.HashMap
 import Lean.Runtime
 import Lean.Compiler.NameMangling

src/Lean/Compiler/IR/EmitUtil.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.InitAttr
 import Lean.Compiler.IR.CompilerM
 

src/Lean/Compiler/IR/ExpandResetReuse.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.CompilerM
 import Lean.Compiler.IR.NormIds
 import Lean.Compiler.IR.FreeVars

src/Lean/Compiler/IR/Format.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.Basic
 
 namespace Lean

src/Lean/Compiler/IR/FreeVars.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.Basic
 
 namespace Lean.IR

src/Lean/Compiler/IR/LLVMBindings.lean

@@ -3,6 +3,8 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Siddharth Bhat
 -/
+prelude
+import Init.System.IO
 
 namespace LLVM
 /-!

src/Lean/Compiler/IR/LiveVars.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.Basic
 import Lean.Compiler.IR.FreeVars
 

src/Lean/Compiler/IR/NormIds.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.Basic
 
 namespace Lean.IR.UniqueIds

src/Lean/Compiler/IR/PushProj.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.Basic
 import Lean.Compiler.IR.FreeVars
 import Lean.Compiler.IR.NormIds

src/Lean/Compiler/IR/RC.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Runtime
 import Lean.Compiler.IR.CompilerM
 import Lean.Compiler.IR.LiveVars

src/Lean/Compiler/IR/ResetReuse.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.Basic
 import Lean.Compiler.IR.LiveVars
 import Lean.Compiler.IR.Format

src/Lean/Compiler/IR/SimpCase.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.Basic
 import Lean.Compiler.IR.Format
 

src/Lean/Compiler/IR/Sorry.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.IR.CompilerM
 
 namespace Lean.IR

src/Lean/Compiler/IR/UnboxResult.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Data.Format
 import Lean.Compiler.IR.Basic
 

src/Lean/Compiler/ImplementedByAttr.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Attributes
 import Lean.Declaration
 import Lean.MonadEnv

src/Lean/Compiler/InitAttr.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Elab.InfoTree.Main
 
 namespace Lean

src/Lean/Compiler/InlineAttrs.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Attributes
 
 

src/Lean/Compiler/LCNF.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.AlphaEqv
 import Lean.Compiler.LCNF.Basic
 import Lean.Compiler.LCNF.Bind

src/Lean/Compiler/LCNF/AlphaEqv.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.Basic
 
 namespace Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/AuxDeclCache.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.CompilerM
 import Lean.Compiler.LCNF.DeclHash
 import Lean.Compiler.LCNF.Internalize

src/Lean/Compiler/LCNF/BaseTypes.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.CompilerM
 import Lean.Compiler.LCNF.Types
 

src/Lean/Compiler/LCNF/Basic.lean

@@ -3,6 +3,8 @@ Copyright (c) 2022 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.List.BasicAux
 import Lean.Expr
 import Lean.Meta.Instances
 import Lean.Compiler.InlineAttrs

src/Lean/Compiler/LCNF/Bind.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.InferType
 
 namespace Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/CSE.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.CompilerM
 import Lean.Compiler.LCNF.ToExpr
 import Lean.Compiler.LCNF.PassManager

src/Lean/Compiler/LCNF/Check.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.InferType
 import Lean.Compiler.LCNF.PrettyPrinter
 import Lean.Compiler.LCNF.CompatibleTypes

src/Lean/Compiler/LCNF/Closure.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Util.ForEachExprWhere
 import Lean.Compiler.LCNF.CompilerM
 

src/Lean/Compiler/LCNF/CompatibleTypes.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.InferType
 
 namespace Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/CompilerM.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.CoreM
 import Lean.Compiler.LCNF.Basic
 import Lean.Compiler.LCNF.LCtx

src/Lean/Compiler/LCNF/ConfigOptions.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Data.Options
 
 namespace Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/DeclHash.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.Basic
 
 namespace Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/DependsOn.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.Basic
 
 namespace Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/ElimDead.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.CompilerM
 
 namespace Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/ElimDeadBranches.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Lean.Compiler.LCNF.CompilerM
 import Lean.Compiler.LCNF.PassManager
 import Lean.Compiler.LCNF.PhaseExt

src/Lean/Compiler/LCNF/FVarUtil.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Lean.Expr
 import Lean.Compiler.LCNF.Basic
 import Lean.Compiler.LCNF.CompilerM

src/Lean/Compiler/LCNF/FixedParams.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.Basic
 import Lean.Compiler.LCNF.Types
 

src/Lean/Compiler/LCNF/FloatLetIn.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Lean.Compiler.LCNF.CompilerM
 import Lean.Compiler.LCNF.FVarUtil
 import Lean.Compiler.LCNF.PassManager

src/Lean/Compiler/LCNF/ForEachExpr.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Util.ForEachExpr
 import Lean.Compiler.LCNF.Basic
 

src/Lean/Compiler/LCNF/InferType.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.CompilerM
 import Lean.Compiler.LCNF.Types
 import Lean.Compiler.LCNF.PhaseExt

src/Lean/Compiler/LCNF/Internalize.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.Compiler.LCNF.Types
 import Lean.Compiler.LCNF.Bind
 import Lean.Compiler.LCNF.CompilerM