cleanup

better unrolling
feat: refactor of BitVec/Bitblast.lean
2026-03-20 20:04:23 +00:00 · 2024-03-06 09:17:05 +11:00 · 2024-03-06 09:09:06 +11:00 · 2024-03-05 22:37:10 +11:00 · 2024-03-05 09:11:19 +00:00 · 2024-03-05 04:59:58 +00:00
31 changed files with 2631 additions and 172 deletions
--- a/.github/workflows/nix-ci.yml
+++ b/.github/workflows/nix-ci.yml
@@ -6,6 +6,7 @@ on:
    tags:
      - '*'
  pull_request:
+    types: [opened, synchronize, reopened, labeled]
  merge_group:

 concurrency:
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -8,6 +8,9 @@ This file contains work-in-progress notes for the upcoming release, as well as p
 Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
 of each version.

+v4.8.0 (development in progress)
+---------
+
 v4.7.0
 ---------

@@ -126,7 +129,7 @@ v4.7.0
  There is now kernel support for these functions.
  [#3376](https://github.com/leanprover/lean4/pull/3376).

-* `omega`, our integer linear arithmetic tactic, is now available in the core langauge.
+* `omega`, our integer linear arithmetic tactic, is now availabe in the core langauge.
  * It is supplemented by a preprocessing tactic `bv_omega` which can solve goals about `BitVec`
    which naturally translate into linear arithmetic problems.
    [#3435](https://github.com/leanprover/lean4/pull/3435).
@@ -172,29 +175,34 @@ Breaking changes:


 Other improvements:
-* Several bug fixes for `simp`:
+* several bug fixes for `simp`:
  * we should not crash when `simp` loops [#3269](https://github.com/leanprover/lean4/pull/3269)
  * `simp` gets stuck on `autoParam` [#3315](https://github.com/leanprover/lean4/pull/3315)
  * `simp` fails when custom discharger makes no progress [#3317](https://github.com/leanprover/lean4/pull/3317)
  * `simp` fails to discharge `autoParam` premises even when it can reduce them to `True` [#3314](https://github.com/leanprover/lean4/pull/3314)
  * `simp?` suggests generated equations lemma names, fixes [#3547](https://github.com/leanprover/lean4/pull/3547) [#3573](https://github.com/leanprover/lean4/pull/3573)
-* Fixes for `match` expressions:
+* fixes for `match` expressions:
  * fix regression with builtin literals [#3521](https://github.com/leanprover/lean4/pull/3521)
  * accept `match` when patterns cover all cases of a `BitVec` finite type [#3538](https://github.com/leanprover/lean4/pull/3538)
  * fix matching `Int` literals [#3504](https://github.com/leanprover/lean4/pull/3504)
  * patterns containing int values and constructors [#3496](https://github.com/leanprover/lean4/pull/3496)
-* Improve `termination_by` error messages [#3255](https://github.com/leanprover/lean4/pull/3255)
-* Fix `rename_i` in macros, fixes [#3553](https://github.com/leanprover/lean4/pull/3553) [#3581](https://github.com/leanprover/lean4/pull/3581)
-* Fix excessive resource usage in `generalize`, fixes [#3524](https://github.com/leanprover/lean4/pull/3524) [#3575](https://github.com/leanprover/lean4/pull/3575)
-* An equation lemma with autoParam arguments fails to rewrite, fixing [#2243](https://github.com/leanprover/lean4/pull/2243) [#3316](https://github.com/leanprover/lean4/pull/3316)
+* improve `termination_by` error messages [#3255](https://github.com/leanprover/lean4/pull/3255)
+* fix `rename_i` in macros, fixes [#3553](https://github.com/leanprover/lean4/pull/3553) [#3581](https://github.com/leanprover/lean4/pull/3581)
+* fix excessive resource usage in `generalize`, fixes [#3524](https://github.com/leanprover/lean4/pull/3524) [#3575](https://github.com/leanprover/lean4/pull/3575)
+* an equation lemma with autoParam arguments fails to rewrite, fixing [#2243](https://github.com/leanprover/lean4/pull/2243) [#3316](https://github.com/leanprover/lean4/pull/3316)
 * `add_decl_doc` should check that declarations are local [#3311](https://github.com/leanprover/lean4/pull/3311)
-* Instantiate the types of inductives with the right parameters, closing [#3242](https://github.com/leanprover/lean4/pull/3242) [#3246](https://github.com/leanprover/lean4/pull/3246)
+* instantiate the types of inductives with the right parameters, closing [#3242](https://github.com/leanprover/lean4/pull/3242) [#3246](https://github.com/leanprover/lean4/pull/3246)
 * New simprocs for many basic types. [#3407](https://github.com/leanprover/lean4/pull/3407)

 Lake fixes:
 * Warn on fetch cloud release failure [#3401](https://github.com/leanprover/lean4/pull/3401)
 * Cloud release trace & `lake build :release` errors [#3248](https://github.com/leanprover/lean4/pull/3248)

+v4.6.1
+---------
+* Backport of [#3552](https://github.com/leanprover/lean4/pull/3552) fixing a performance regression
+  in server startup.
+
 v4.6.0
 ---------

--- a/doc/SUMMARY.md
+++ b/doc/SUMMARY.md
@@ -89,5 +89,6 @@
 - [Testing](./dev/testing.md)
 - [Debugging](./dev/debugging.md)
 - [Commit Convention](./dev/commit_convention.md)
+- [Release checklist](./dev/release_checklist.md)
 - [Building This Manual](./dev/mdbook.md)
 - [Foreign Function Interface](./dev/ffi.md)
--- a/doc/dev/release_checklist.md
+++ b/doc/dev/release_checklist.md
@@ -0,0 +1,201 @@
+# Releasing a stable version
+
+This checklist walks you through releasing a stable version.
+See below for the checklist for release candidates.
+
+We'll use `v4.6.0` as the intended release version as a running example.
+
+- One week before the planned release, ensure that someone has written the first draft of the release blog post
+- `git checkout releases/v4.6.0`
+  (This branch should already exist, from the release candidates.)
+- `git pull`
+- In `src/CMakeLists.txt`, verify you see
+  - `set(LEAN_VERSION_MINOR 6)` (for whichever `6` is appropriate)
+  - `set(LEAN_VERSION_IS_RELEASE 1)`
+  - (both of these should already be in place from the release candidates)
+- It is possible that the `v4.6.0` section of `RELEASES.md` is out of sync between
+  `releases/v4.6.0` and `master`. This should be reconciled:
+  - Run `git diff master RELEASES.md`.
+  - You should expect to see additons on `master` in the `v4.7.0-rc1` section; ignore these.
+    (i.e. the new release notes for the upcoming release candidate).
+  - Reconcile discrepancies in the `v4.6.0` section,
+    usually via copy and paste and a commit to `releases/v4.6.0`.
+- `git tag v4.6.0`
+- `git push origin v4.6.0`
+- Now wait, while CI runs.
+  - You can monitor this at `https://github.com/leanprover/lean4/actions/workflows/ci.yml`,
+    looking for the `v4.6.0` tag.
+  - This step can take up to an hour.
+  - If you are intending to cut the next release candidate on the same day,
+    you may want to start on the release candidate checklist now.
+- Go to https://github.com/leanprover/lean4/releases and verify that the `v4.6.0` release appears.
+  - Edit the release notes on Github to select the "Set as the latest release".
+  - Copy and paste the Github release notes from the previous releases candidate for this version
+    (e.g. `v4.6.0-rc1`), and quickly sanity check.
+- Next, we will move a curated list of downstream repos to the latest stable release.
+  - For each of the repositories listed below:
+    - Make a PR to `master`/`main` changing the toolchain to `v4.6.0`.
+      The PR title should be "chore: bump toolchain to v4.6.0".
+      Since the `v4.6.0` release should be functionally identical to the last release candidate,
+      which the repository should already be on, this PR is a no-op besides changing the toolchain.
+    - Once this is merged, create the tag `v4.6.0` from `master`/`main` and push it.
+    - Merge the tag `v4.6.0` into the stable branch.
+  - We do this for the repositories:
+    - [lean4checker](https://github.com/leanprover/lean4checker)
+      - `lean4checker` uses a different version tagging scheme: use `toolchain/v4.6.0` rather than `v4.6.0`.
+    - [Std](https://github.com/leanprover-community/repl)
+    - [ProofWidgets4](https://github.com/leanprover-community/ProofWidgets4)
+      - `ProofWidgets` uses a sequential version tagging scheme, e.g. `v0.0.29`,
+        which does not refer to the toolchain being used.
+      - Make a new release in this sequence after merging the toolchain bump PR.
+      - `ProofWidgets` does not maintain a `stable` branch.
+    - [Aesop](https://github.com/leanprover-community/aesop)
+    - [Mathlib](https://github.com/leanprover-community/mathlib4)
+      - In addition to updating the `lean-toolchain` and `lakefile.lean`,
+        in `.github/workflows/build.yml.in` in the `lean4checker` section update the line
+        `git checkout toolchain/v4.6.0` to the appropriate tag,
+        and then run `.github/workflows/mk_build_yml.sh`.
+    - [REPL](https://github.com/leanprover-community/repl)
+      - Note that there are two copies of `lean-toolchain`/`lakefile.lean`:
+        in the root, and in `test/Mathlib/`.
+  - Note that there are dependencies between these packages:
+    you should update the lakefile so that you are using the `v4.6.0` tag of upstream repositories
+    (or the sequential tag for `ProofWidgets4`), and run `lake update` before committing.
+  - This means that this process is sequential; each repository must have its bump PR merged,
+    and the new tag pushed, before you can make the PR for the downstream repositories.
+    - `lean4checker` has no dependencies
+    - `Std` has no dependencies
+    - `Aesop` depends on `Std`
+    - `ProofWidgets4` depends on `Std`
+    - `Mathlib` depends on `Aesop`, `ProofWidgets4`, and `lean4checker` (and transitively on `Std`)
+    - `REPL` depends on `Mathlib` (this dependency is only for testing).
+- Merge the release announcement PR for the Lean website - it will be deployed automatically
+- Finally, make an announcement!
+  This should go in https://leanprover.zulipchat.com/#narrow/stream/113486-announce, with topic `v4.6.0`.
+  Please see previous announcements for suggested language.
+  You will want a few bullet points for main topics from the release notes.
+  Link to the blog post from the Zulip announcement.
+  Please also make sure that whoever is handling social media knows the release is out.
+
+## Optimistic(?) time estimates:
+- Initial checks and push the tag: 30 minutes.
+- Note that if `RELEASES.md` has discrepancies this could take longer!
+- Waiting for the release: 60 minutes.
+- Fixing release notes: 10 minutes.
+- Bumping toolchains in downstream repositories, up to creating the Mathlib PR: 30 minutes.
+- Waiting for Mathlib CI and bors: 120 minutes.
+- Finalizing Mathlib tags and stable branch, and updating REPL: 15 minutes.
+- Posting announcement and/or blog post: 20 minutes.
+
+# Creating a release candidate.
+
+This checklist walks you through creating the first release candidate for a version of Lean.
+
+We'll use `v4.7.0-rc1` as the intended release version in this example.
+
+- Decide which nightly release you want to turn into a release candidate.
+  We will use `nightly-2024-02-29` in this example.
+- It is essential that Std and Mathlib already have reviewed branches compatible with this nightly.
+  - Check that both Std and Mathlib's `bump/v4.7.0` branch contain `nightly-2024-02-29`
+    in their `lean-toolchain`.
+  - The steps required to reach that state are beyond the scope of this checklist, but see below!
+- Create the release branch from this nightly tag:
+    ```
+    git remote add nightly https://github.com/leanprover/lean4-nightly.git
+    git fetch nightly tag nightly-2024-02-29
+    git checkout nightly-2024-02-29
+    git checkout -b releases/v4.7.0
+    ```
+- In `RELEASES.md` remove `(development in progress)` from the `v4.7.0` section header.
+- Our current goal is to have written release notes only about major language features or breaking changes,
+  and to rely on automatically generated release notes for bugfixes and minor changes.
+  - Do not wait on `RELEASES.md` being perfect before creating the `release/v4.7.0` branch. It is essential to choose the nightly which will become the release candidate as early as possible, to avoid confusion.
+  - If there are major changes not reflected in `RELEASES.md` already, you may need to solicit help from the authors.
+  - Minor changes and bug fixes do not need to be documented in `RELEASES.md`: they will be added automatically on the Github release page.
+  - Commit your changes to `RELEASES.md`, and push.
+  - Remember that changes to `RELEASES.md` after you have branched `releases/v4.7.0` should also be cherry-picked back to `master`.
+- In `src/CMakeLists.txt`,
+  - verify that you see `set(LEAN_VERSION_MINOR 7)` (for whichever `7` is appropriate); this should already have been updated when the development cycle began.
+  - `set(LEAN_VERSION_IS_RELEASE 1)` (this should be a change; on `master` and nightly releases it is always `0`).
+  - Commit your changes to `src/CMakeLists.txt`, and push.
+- `git tag v4.7.0-rc1`
+- `git push origin v4.7.0-rc1`
+- Now wait, while CI runs.
+  - You can monitor this at `https://github.com/leanprover/lean4/actions/workflows/ci.yml`, looking for the `v4.7.0-rc1` tag.
+  - This step can take up to an hour.
+- Once the release appears at https://github.com/leanprover/lean4/releases/
+  - Edit the release notes on Github to select the "Set as a pre-release box".
+  - Copy the section of `RELEASES.md` for this version into the Github release notes.
+  - Use the title "Changes since v4.6.0 (from RELEASES.md)"
+  - Then in the "previous tag" dropdown, select `v4.6.0`, and click "Generate release notes".
+  - This will add a list of all the commits since the last stable version.
+    - Delete anything already mentioned in the hand-written release notes above.
+    - Delete "update stage0" commits, and anything with a completely inscrutable commit message.
+    - Briefly rearrange the remaining items by category (e.g. `simp`, `lake`, `bug fixes`),
+      but for minor items don't put any work in expanding on commit messages.
+  - (How we want to release notes to look is evolving: please update this section if it looks wrong!)
+- Next, we will move a curated list of downstream repos to the release candidate.
+  - This assumes that there is already a *reviewed* branch `bump/v4.7.0` on each repository
+    containing the required adaptations (or no adaptations are required).
+    The preparation of this branch is beyond the scope of this document.
+  - For each of the target repositories:
+    - Checkout the `bump/v4.7.0` branch.
+    - Verify that the `lean-toolchain` is set to the nightly from which the release candidate was created.
+    - `git merge origin/master`
+    - Change the `lean-toolchain` to `leanprover/lean4:v4.7.0-rc1`
+    - In `lakefile.lean`, change any dependencies which were using `nightly-testing` or `bump/v4.7.0` branches
+      back to `master` or `main`, and run `lake update` for those dependencies.
+    - Run `lake build` to ensure that dependencies are found (but it's okay to stop it after a moment).
+    - `git commit`
+    - `git push`
+    - Open a PR from `bump/v4.7.0` to `master`, and either merge it yourself after CI, if appropriate,
+      or notify the maintainers that it is ready to go.
+    - Once this PR has been merged, tag `master` with `v4.7.0-rc1` and push this tag.
+  - We do this for the same list of repositories as for stable releases, see above.
+    As above, there are dependencies between these, and so the process above is iterative.
+    It greatly helps if you can merge the `bump/v4.7.0` PRs yourself!
+  - For Std/Aesop/Mathlib, which maintain a `nightly-testing` branch, make sure there is a tag
+    `nightly-testing-2024-02-29` with date corresponding to the nightly used for the release
+    (create it if not), and then on the `nightly-testing` branch `git reset --hard master`, and force push.
+- Make an announcement!
+  This should go in https://leanprover.zulipchat.com/#narrow/stream/113486-announce, with topic `v4.7.0-rc1`.
+  Please see previous announcements for suggested language.
+  You will want a few bullet points for main topics from the release notes.
+  Please also make sure that whoever is handling social media knows the release is out.
+- Begin the next development cycle (i.e. for `v4.8.0`) on the Lean repository, by making a PR that:
+  - Updates `src/CMakeLists.txt` to say `set(LEAN_VERSION_MINOR 8)`
+  - Removes `(in development)` from the section heading in `RELEASES.md` for `v4.7.0`,
+    and creates a new `v4.8.0 (in development)` section heading.
+
+## Time estimates:
+Slightly longer than the corresponding steps for a stable release.
+Similar process, but more things go wrong.
+In particular, updating the downstream repositories is significantly more work
+(because we need to merge existing `bump/v4.7.0` branches, not just update a toolchain).
+
+# Preparing `bump/v4.7.0` branches
+
+While not part of the release process per se,
+this is a brief summary of the work that goes into updating Std/Aesop/Mathlib to new versions.
+
+Please read https://leanprover-community.github.io/contribute/tags_and_branches.html
+
+* Each repo has an unreviewed `nightly-testing` branch that
+  receives commits automatically from `master`, and
+  has its toolchain updated automatically for every nightly.
+  (Note: the aesop branch is not automated, and is updated on an as needed basis.)
+  As a consequence this branch is often broken.
+  A bot posts in the (private!) "Mathlib reviewers" stream on Zulip about the status of these branches.
+* We fix the breakages by committing directly to `nightly-testing`: there is no PR process.
+  * This can either be done by the person managing this process directly,
+    or by soliciting assistance from authors of files, or generally helpful people on Zulip!
+* Each repo has a `bump/v4.7.0` which accumulates reviewed changes adapting to new versions.
+* Once `nightly-testing` is working on a given nightly, say `nightly-2024-02-15`, we:
+  * Make sure `bump/v4.7.0` is up to date with `master` (by merging `master`, no PR necessary)
+  * Create from `bump/v4.7.0` a `bump/nightly-2024-02-15` branch.
+  * In that branch, `git merge --squash nightly-testing` to bring across changes from `nightly-testing`.
+  * Sanity check changes, commit, and make a PR to `bump/v4.7.0` from the `bump/nightly-2024-02-15` branch.
+  * Solicit review, merge the PR into `bump/v4,7,0`.
+* It is always okay to merge in the following directions:
+  `master` -> `bump/v4.7.0` -> `bump/nightly-2024-02-15` -> `nightly-testing`.
+  Please remember to push any merges you make to intermediate steps!
--- a/doc/examples/bintree.lean
+++ b/doc/examples/bintree.lean
@@ -277,14 +277,13 @@ theorem BinTree.find_insert (b : BinTree β) (k : Nat) (v : β)
    . by_cases' key < k
      cases h; apply ihr; assumption

-theorem BinTree.find_insert_of_ne (b : BinTree β) (h : k ≠ k') (v : β)
+theorem BinTree.find_insert_of_ne (b : BinTree β) (ne : k ≠ k') (v : β)
        : (b.insert k v).find? k' = b.find? k' := by
  let ⟨t, h⟩ := b; simp
  induction t with simp
  | leaf =>
-    intros
-    have_eq k k'
-    contradiction
+    intros le
+    exact Nat.lt_of_le_of_ne le ne
  | node left key value right ihl ihr =>
    let .node hl hr bl br := h
    specialize ihl bl
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -9,9 +9,9 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 7)
+set(LEAN_VERSION_MINOR 8)
 set(LEAN_VERSION_PATCH 0)
-set(LEAN_VERSION_IS_RELEASE 1)  # This number is 1 in the release revision, and 0 otherwise.
+set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
 set(LEAN_VERSION_STRING "${LEAN_VERSION_MAJOR}.${LEAN_VERSION_MINOR}.${LEAN_VERSION_PATCH}")
 if (LEAN_SPECIAL_VERSION_DESC)
--- a/src/Init/ByCases.lean
+++ b/src/Init/ByCases.lean
@@ -37,15 +37,6 @@ theorem apply_ite (f : α → β) (P : Prop) [Decidable P] (x y : α) :
    f (ite P x y) = ite P (f x) (f y) :=
  apply_dite f P (fun _ => x) (fun _ => y)

-/-- Negation of the condition `P : Prop` in a `dite` is the same as swapping the branches. -/
-@[simp] theorem dite_not (P : Prop) {_ : Decidable P}  (x : ¬P → α) (y : ¬¬P → α) :
-    dite (¬P) x y = dite P (fun h => y (not_not_intro h)) x := by
-  by_cases h : P <;> simp [h]
-
-/-- Negation of the condition `P : Prop` in a `ite` is the same as swapping the branches. -/
-@[simp] theorem ite_not (P : Prop) {_ : Decidable P} (x y : α) : ite (¬P) x y = ite P y x :=
-  dite_not P (fun _ => x) (fun _ => y)
-
@[simp] theorem dite_eq_left_iff {P : Prop} [Decidable P] {B : ¬ P → α} :
    dite P (fun _ => a) B = a ↔ ∀ h, B h = a := by
  by_cases P <;> simp [*, forall_prop_of_true, forall_prop_of_false]
--- a/src/Init/Classical.lean
+++ b/src/Init/Classical.lean
@@ -125,16 +125,15 @@ theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
 /-- The Double Negation Theorem: `¬¬P` is equivalent to `P`.
 The left-to-right direction, double negation elimination (DNE),
 is classically true but not constructively. -/
-@[scoped simp] theorem not_not : ¬¬a ↔ a := Decidable.not_not
+@[simp] theorem not_not : ¬¬a ↔ a := Decidable.not_not

-@[simp] theorem not_forall {p : α → Prop} : (¬∀ x, p x) ↔ ∃ x, ¬p x := Decidable.not_forall
+@[simp low] theorem not_forall {p : α → Prop} : (¬∀ x, p x) ↔ ∃ x, ¬p x := Decidable.not_forall

 theorem not_forall_not {p : α → Prop} : (¬∀ x, ¬p x) ↔ ∃ x, p x := Decidable.not_forall_not
 theorem not_exists_not {p : α → Prop} : (¬∃ x, ¬p x) ↔ ∀ x, p x := Decidable.not_exists_not

 theorem forall_or_exists_not (P : α → Prop) : (∀ a, P a) ∨ ∃ a, ¬ P a := by
  rw [← not_forall]; exact em _
-
 theorem exists_or_forall_not (P : α → Prop) : (∃ a, P a) ∨ ∀ a, ¬ P a := by
  rw [← not_exists]; exact em _

@@ -147,8 +146,22 @@ theorem not_and_iff_or_not_not : ¬(a ∧ b) ↔ ¬a ∨ ¬b := Decidable.not_an

 theorem not_iff : ¬(a ↔ b) ↔ (¬a ↔ b) := Decidable.not_iff

+@[simp] theorem imp_iff_left_iff  : (b ↔ a → b) ↔ a ∨ b := Decidable.imp_iff_left_iff
+@[simp] theorem imp_iff_right_iff : (a → b ↔ b) ↔ a ∨ b := Decidable.imp_iff_right_iff
+
+@[simp] theorem and_or_imp : a ∧ b ∨ (a → c) ↔ a → b ∨ c := Decidable.and_or_imp
+
+@[simp] theorem not_imp : ¬(a → b) ↔ a ∧ ¬b := Decidable.not_imp_iff_and_not
+
+@[simp] theorem imp_and_neg_imp_iff (p q : Prop) : (p → q) ∧ (¬p → q) ↔ q :=
+  Iff.intro (fun (a : _ ∧ _) => (Classical.em p).rec a.left a.right)
+            (fun a => And.intro (fun _ => a) (fun _ => a))
+
 end Classical

+/- Export for Mathlib compat. -/
+export Classical (imp_iff_right_iff imp_and_neg_imp_iff and_or_imp not_imp)
+
 /-- Extract an element from a existential statement, using `Classical.choose`. -/
 -- This enables projection notation.
@[reducible] noncomputable def Exists.choose {p : α → Prop} (P : ∃ a, p a) : α := Classical.choose P
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -677,7 +677,7 @@ You can prove theorems about the resulting element by induction on `h`, since
 theorem Eq.substr {α : Sort u} {p : α → Prop} {a b : α} (h₁ : b = a) (h₂ : p a) : p b :=
  h₁ ▸ h₂

-theorem cast_eq {α : Sort u} (h : α = α) (a : α) : cast h a = a :=
+@[simp] theorem cast_eq {α : Sort u} (h : α = α) (a : α) : cast h a = a :=
  rfl

 /--
@@ -1403,9 +1403,9 @@ theorem false_imp_iff (a : Prop) : (False → a) ↔ True := iff_true_intro Fals

 theorem true_imp_iff (α : Prop) : (True → α) ↔ α := imp_iff_right True.intro

-@[simp] theorem imp_self : (a → a) ↔ True := iff_true_intro id
+@[simp high] theorem imp_self : (a → a) ↔ True := iff_true_intro id

-theorem imp_false : (a → False) ↔ ¬a := Iff.rfl
+@[simp] theorem imp_false : (a → False) ↔ ¬a := Iff.rfl

 theorem imp.swap : (a → b → c) ↔ (b → a → c) := Iff.intro flip flip

--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -5,6 +5,7 @@ Authors: Harun Khan, Abdalrhman M Mohamed, Joe Hendrix
 -/
 prelude
 import Init.Data.BitVec.Folds
+import Init.Data.Nat.Mod

 /-!
 # Bitblasting of bitvectors
@@ -70,24 +71,8 @@ private theorem testBit_limit {x i : Nat} (x_lt_succ : x < 2^(i+1)) :
             _ ≤ 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]
+    x % 2^(i+1) = 2^i*(x.testBit i).toNat + x % (2 ^ i):= by
+  rw [Nat.mod_pow_succ, Nat.add_comm, Nat.toNat_testBit]

 private theorem mod_two_pow_add_mod_two_pow_add_bool_lt_two_pow_succ
     (x y i : Nat) (c : Bool) : x % 2^i + (y % 2^i + c.toNat) < 2^(i+1) := by
@@ -113,6 +98,128 @@ theorem carry_succ (i : Nat) (x y : BitVec w) (c : Bool) :
    exact mod_two_pow_add_mod_two_pow_add_bool_lt_two_pow_succ ..
  cases x.toNat.testBit i <;> cases y.toNat.testBit i <;> (simp; omega)

+/--
+Does the addition of two `BitVec`s overflow?
+
+The nice feature of this definition is that
+it can be unfolded recursively to a circuit:
+```
+example (x y : BitVec 4) :
+    addOverflow x y =
+      atLeastTwo (x.getLsb 3) (y.getLsb 3) (atLeastTwo (x.getLsb 2) (y.getLsb 2)
+        (atLeastTwo (x.getLsb 1) (y.getLsb 1) (x.getLsb 0 && y.getLsb 0))) := by
+  simp [addOverflow, msb_truncate, BitVec.msb, getMsb]
+```
+-/
+def addOverflow (x y : BitVec w) (c : Bool := false) : Bool :=
+  match w with
+  | 0 => c
+  | (w + 1) => atLeastTwo x.msb y.msb (addOverflow (x.truncate w) (y.truncate w) c)
+
+@[simp] theorem addOverflow_length_zero {x y : BitVec 0} : addOverflow x y c = c := rfl
+
+theorem addOverflow_length_succ {x y : BitVec (w+1)} :
+    addOverflow x y c = atLeastTwo x.msb y.msb (addOverflow (x.truncate w) (y.truncate w) c) :=
+  rfl
+
+@[simp] theorem addOverflow_zero_left_succ :
+    addOverflow 0#(w+1) y c = (y.msb && addOverflow 0#w (y.truncate w) c) := by
+  simp [addOverflow]
+
+@[simp] theorem addOverflow_zero_right_succ {x : BitVec (w+1)} :
+    addOverflow x 0#(w+1) c = (x.msb && addOverflow (x.truncate w) 0#w c) := by
+  simp [addOverflow]
+
+@[simp] theorem addOverflow_zero_zero :
+    addOverflow 0#i 0#i c = (decide (i = 0) && c) := by
+  cases i <;> simp
+
+theorem carry_eq_addOverflow (i) (x y : BitVec w) (c) :
+    carry i x y c = addOverflow (x.truncate i) (y.truncate i) c := by
+  match i with
+  | 0 => simp
+  | (i + 1) =>
+    rw [addOverflow_length_succ, carry_succ, carry_eq_addOverflow]
+    simp [msb_zeroExtend, Nat.le_succ]
+
+theorem addOverflow_eq_carry {x y : BitVec w} :
+    addOverflow x y c = carry w x y c := by
+  have := carry_eq_addOverflow w x y c
+  simpa using this.symm
+
+theorem addOverflow_cons_cons :
+    addOverflow (cons a x) (cons b y) = atLeastTwo a b (addOverflow x y) := by
+  simp [addOverflow]
+
+theorem add_cons_cons (w) (x y : BitVec w) :
+    (cons a x) + (cons b y) = cons (Bool.xor a (Bool.xor b (addOverflow x y))) (x + y) := by
+  have pos : 0 < 2^w := Nat.pow_pos Nat.zero_lt_two
+  apply eq_of_toNat_eq
+  simp only [toNat_add, toNat_cons']
+  rw [addOverflow_eq_carry, carry]
+  simp [Nat.mod_pow_succ]
+  by_cases h : 2 ^ w ≤ x.toNat + y.toNat
+  · simp [h]
+    have p : (x.toNat + y.toNat) / 2 ^ w = 1 := by
+      apply Nat.div_eq_of_lt_le <;> omega
+    cases a <;> cases b
+      <;> simp [Nat.one_shiftLeft, Nat.add_left_comm x.toNat, Nat.add_assoc, p, pos]
+      <;> simp [Nat.add_comm]
+  · simp [h]
+    have p : (x.toNat + y.toNat) / 2 ^ w = 0 := by
+      apply Nat.div_eq_of_lt_le <;> omega
+    cases a <;> cases b
+      <;> simp [Nat.one_shiftLeft, Nat.add_left_comm x.toNat, Nat.add_assoc, p, pos]
+      <;> simp [Nat.add_comm]
+
+theorem msb_add (x y : BitVec w) :
+    (x + y).msb =
+      Bool.xor x.msb (Bool.xor y.msb (addOverflow (x.truncate (w-1)) (y.truncate (w-1)))) := by
+  cases w with
+  | zero => simp
+  | succ w =>
+    conv =>
+      lhs
+      rw [eq_msb_cons_truncate x, eq_msb_cons_truncate y, add_cons_cons]
+    simp [succ_eq_add_one, Nat.add_one_sub_one]
+
+/--
+Variant of `getLsb_add` in terms of `addOverflow` rather than `carry`.
+-/
+theorem getLsb_add' (i : Nat) (x y : BitVec w) :
+    getLsb (x + y) i = (decide (i < w) && Bool.xor (x.getLsb i)
+      (Bool.xor (y.getLsb i) (addOverflow (x.truncate i) (y.truncate i)))) := by
+  by_cases h : i < w
+  · rw [← msb_truncate (x + y), truncate_add, msb_add, msb_truncate, msb_truncate]
+    rw [Nat.add_one_sub_one, truncate_truncate_of_le, truncate_truncate_of_le]
+    simp [h]
+    all_goals omega
+  · simp [h]
+    simp at h
+    simp [h]
+
+theorem addOverflow_eq_false_of_and_eq_zero {x y : BitVec w} (h : x &&& y = 0#w) :
+    addOverflow x y = false := by
+  induction w with
+  | zero => rfl
+  | succ w ih =>
+    have h₁ := congrArg BitVec.msb h
+    have h₂ := congrArg (·.truncate w) h
+    simp at h₁ h₂
+    simp_all [addOverflow_length_succ]
+
+theorem or_eq_add_of_and_eq_zero (x y : BitVec w) (h : x &&& y = 0) :
+    x ||| y = x + y := by
+  ext i
+  have h₁ := congrArg (getLsb · i) h
+  have h₂ := congrArg (truncate i) h
+  simp at h₁ h₂
+  simp only [getLsb_add', getLsb_or]
+  rw [addOverflow_eq_false_of_and_eq_zero h₂]
+  -- sat
+  revert h₁
+  cases x.getLsb i <;> cases y.getLsb i <;> simp
+
 /-- Carry function for bitwise addition. -/
 def adcb (x y c : Bool) : Bool × Bool := (atLeastTwo x y c, Bool.xor x (Bool.xor y c))

--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -36,7 +36,7 @@ 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
+@[simp] theorem getLsb_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsb x i = false := by
  let ⟨x, x_lt⟩ := x
  simp
  apply Nat.testBit_lt_two_pow
@@ -89,6 +89,9 @@ theorem eq_of_toFin_eq : ∀ {x y : BitVec w}, x.toFin = y.toFin → x = y
@[simp] theorem toNat_ofBool (b : Bool) : (ofBool b).toNat = b.toNat := by
  cases b <;> rfl

+@[simp] theorem msb_ofBool (b : Bool) : (ofBool b).msb = b := by
+  cases b <;> simp [BitVec.msb]
+
 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']

@@ -116,6 +119,8 @@ theorem getLsb_ofNat (n : Nat) (x : Nat) (i : Nat) :

@[simp] theorem getLsb_zero : (0#w).getLsb i = false := by simp [getLsb]

+@[simp] theorem getMsb_zero : (0#w).getMsb i = false := by simp [getMsb]
+
@[simp] theorem toNat_mod_cancel (x : BitVec n) : x.toNat % (2^n) = x.toNat :=
  Nat.mod_eq_of_lt x.isLt

@@ -241,6 +246,12 @@ theorem toInt_ofNat {n : Nat} (x : Nat) :
  else
    simp [n_le_i, toNat_ofNat]

+theorem zeroExtend'_eq {x : BitVec w} (h : w ≤ v) : x.zeroExtend' h = x.zeroExtend v := by
+  apply eq_of_toNat_eq
+  rw [toNat_zeroExtend, toNat_zeroExtend']
+  rw [Nat.mod_eq_of_lt]
+  exact Nat.lt_of_lt_of_le x.isLt (Nat.pow_le_pow_right (Nat.zero_lt_two) h)
+
@[simp, bv_toNat] theorem toNat_truncate (x : BitVec n) : (truncate i x).toNat = x.toNat % 2^i :=
  toNat_zeroExtend i x

@@ -285,10 +296,25 @@ theorem nat_eq_toNat (x : BitVec w) (y : Nat)
    getLsb (zeroExtend m x) i = (decide (i < m) && getLsb x i) := by
  simp [getLsb, toNat_zeroExtend, Nat.testBit_mod_two_pow]

+@[simp] theorem getMsb_zeroExtend_add {x : BitVec w} (h : k ≤ i) :
+    (x.zeroExtend (w + k)).getMsb i = x.getMsb (i - k) := by
+  by_cases h : w = 0
+  · subst h; simp
+  simp only [getMsb, getLsb_zeroExtend]
+  by_cases h₁ : i < w + k <;> by_cases h₂ : i - k < w <;> by_cases h₃ : w + k - 1 - i < w + k
+    <;> simp [h₁, h₂, h₃]
+  · congr 1
+    omega
+  all_goals (first | apply getLsb_ge | apply Eq.symm; apply getLsb_ge)
+    <;> omega
+
@[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

+theorem msb_truncate (x : BitVec w) : (x.truncate (k + 1)).msb = x.getLsb k := by
+  simp [BitVec.msb, getMsb]
+
@[simp] theorem zeroExtend_zeroExtend_of_le (x : BitVec w) (h : k ≤ l) :
    (x.zeroExtend l).zeroExtend k = x.zeroExtend k := by
  ext i
@@ -301,11 +327,18 @@ theorem nat_eq_toNat (x : BitVec w) (y : Nat)
    (x.truncate l).truncate k = x.truncate k :=
  zeroExtend_zeroExtend_of_le x h

+@[simp] theorem truncate_cast {h : w = v} : (cast h x).truncate k = x.truncate k := by
+  apply eq_of_getLsb_eq
+  simp
+
 theorem msb_zeroExtend (x : BitVec w) : (x.zeroExtend v).msb = (decide (0 < v) && x.getLsb (v - 1)) := by
  rw [msb_eq_getLsb_last]
  simp only [getLsb_zeroExtend]
  cases getLsb x (v - 1) <;> simp; omega

+theorem msb_zeroExtend' (x : BitVec w) (h : w ≤ v) : (x.zeroExtend' h).msb = (decide (0 < v) && x.getLsb (v - 1)) := by
+  rw [zeroExtend'_eq, msb_zeroExtend]
+
 /-! ## extractLsb -/

@[simp]
@@ -353,6 +386,18 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
  rw [← testBit_toNat, getLsb, getLsb]
  simp

+@[simp] theorem getMsb_or {x y : BitVec w} : (x ||| y).getMsb i = (x.getMsb i || y.getMsb i) := by
+  simp only [getMsb]
+  by_cases h : i < w <;> simp [h]
+
+@[simp] theorem msb_or {x y : BitVec w} : (x ||| y).msb = (x.msb || y.msb) := by
+  simp [BitVec.msb]
+
+@[simp] theorem truncate_or {x y : BitVec w} :
+    (x ||| y).truncate k = x.truncate k ||| y.truncate k := by
+  ext
+  simp
+
 /-! ### and -/

@[simp] theorem toNat_and (x y : BitVec v) :
@@ -367,6 +412,18 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
  rw [← testBit_toNat, getLsb, getLsb]
  simp

+@[simp] theorem getMsb_and {x y : BitVec w} : (x &&& y).getMsb i = (x.getMsb i && y.getMsb i) := by
+  simp only [getMsb]
+  by_cases h : i < w <;> simp [h]
+
+@[simp] theorem msb_and {x y : BitVec w} : (x &&& y).msb = (x.msb && y.msb) := by
+  simp [BitVec.msb]
+
+@[simp] theorem truncate_and {x y : BitVec w} :
+    (x &&& y).truncate k = x.truncate k &&& y.truncate k := by
+  ext
+  simp
+
 /-! ### xor -/

@[simp] theorem toNat_xor (x y : BitVec v) :
@@ -382,6 +439,11 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
  rw [← testBit_toNat, getLsb, getLsb]
  simp

+@[simp] theorem truncate_xor {x y : BitVec w} :
+    (x ^^^ y).truncate k = x.truncate k ^^^ y.truncate k := by
+  ext
+  simp
+
 /-! ### not -/

 theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
@@ -414,6 +476,12 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
@[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]

+@[simp] theorem truncate_not {x : BitVec w} (h : k ≤ w) :
+    (~~~x).truncate k = ~~~(x.truncate k) := by
+  ext
+  simp [h]
+  omega
+
 /-! ### shiftLeft -/

@[simp, bv_toNat] theorem toNat_shiftLeft {x : BitVec v} :
@@ -431,6 +499,19 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
  cases h₁ : decide (i < m) <;> cases h₂ : decide (n ≤ i) <;> cases h₃ : decide (i < n)
  all_goals { simp_all <;> omega }

+@[simp] theorem getMsb_shiftLeft (x : BitVec w) (i) :
+    (x <<< i).getMsb k = x.getMsb (k + i) := by
+  simp only [getMsb, getLsb_shiftLeft]
+  by_cases h : w = 0
+  · subst h; simp
+  have t : w - 1 - k < w := by omega
+  simp only [t]
+  simp only [decide_True, Nat.sub_sub, Bool.true_and, Nat.add_assoc]
+  by_cases h₁ : k < w <;> by_cases h₂ : w - (1 + k) < i <;> by_cases h₃ : k + i < w
+    <;> simp [h₁, h₂, h₃]
+    <;> (first | apply getLsb_ge | apply Eq.symm; apply getLsb_ge)
+    <;> omega
+
 theorem shiftLeftZeroExtend_eq {x : BitVec w} :
    shiftLeftZeroExtend x n = zeroExtend (w+n) x <<< n := by
  apply eq_of_toNat_eq
@@ -450,6 +531,10 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
    <;> simp_all
    <;> (rw [getLsb_ge]; omega)

+@[simp] theorem msb_shiftLeftZeroExtend (x : BitVec w) (i : Nat) :
+    (shiftLeftZeroExtend x i).msb = x.msb := by
+  simp [shiftLeftZeroExtend_eq, BitVec.msb]
+
 /-! ### ushiftRight -/

@[simp, bv_toNat] theorem toNat_ushiftRight (x : BitVec n) (i : Nat) :
@@ -475,6 +560,34 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
  · simp [h]
  · simp [h]; simp_all

+theorem msb_append {x : BitVec w} {y : BitVec v} :
+    (x ++ y).msb = bif (w == 0) then (y.msb) else (x.msb) := by
+  rw [← append_eq, append]
+  simp [msb_zeroExtend']
+  by_cases h : w = 0
+  · subst h
+    simp [BitVec.msb, getMsb]
+  · rw [cond_eq_if]
+    have q : 0 < w + v := by omega
+    have t : y.getLsb (w + v - 1) = false := getLsb_ge _ _ (by omega)
+    simp [h, q, t, BitVec.msb, getMsb]
+
+@[simp] theorem truncate_append {x : BitVec w} {y : BitVec v} :
+    (x ++ y).truncate k = if h : k ≤ v then y.truncate k else (x.truncate (k - v) ++ y).cast (by omega) := by
+  apply eq_of_getLsb_eq
+  intro i
+  simp only [getLsb_zeroExtend, Fin.is_lt, decide_True, getLsb_append, Bool.true_and]
+  split
+  · have t : i < v := by omega
+    simp [t]
+  · by_cases t : i < v
+    · simp [t]
+    · have t' : i - v < k - v := by omega
+      simp [t, t']
+
+@[simp] theorem truncate_cons {x : BitVec w} : (cons a x).truncate w = x := by
+  simp [cons]
+
 /-! ### rev -/

 theorem getLsb_rev (x : BitVec w) (i : Fin w) :
@@ -497,6 +610,11 @@ theorem getMsb_rev (x : BitVec w) (i : Fin w) :
  let ⟨x, _⟩ := x
  simp [cons, toNat_append, toNat_ofBool]

+/-- Variant of `toNat_cons` using `+` instead of `|||`. -/
+theorem toNat_cons' {x : BitVec w} :
+    (cons a x).toNat = (a.toNat <<< w) + x.toNat := by
+  simp [cons, Nat.shiftLeft_eq, Nat.mul_comm _ (2^w), Nat.mul_add_lt_is_or, x.isLt]
+
@[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]
@@ -511,6 +629,9 @@ theorem getMsb_rev (x : BitVec w) (i : Fin w) :
    have p2 : i - n ≠ 0 := by omega
    simp [p1, p2, Nat.testBit_bool_to_nat]

+@[simp] theorem msb_cons : (cons a x).msb = a := by
+  simp [cons, msb_cast, msb_append]
+
 theorem truncate_succ (x : BitVec w) :
    truncate (i+1) x = cons (getLsb x i) (truncate i x) := by
  apply eq_of_getLsb_eq
@@ -522,6 +643,15 @@ theorem truncate_succ (x : BitVec w) :
    have j_lt : j.val < i := Nat.lt_of_le_of_ne (Nat.le_of_succ_le_succ j.isLt) j_eq
    simp [j_eq, j_lt]

+theorem eq_msb_cons_truncate (x : BitVec (w+1)) : x = (cons x.msb (x.truncate w)) := by
+  ext i
+  simp
+  split <;> rename_i h
+  · simp [BitVec.msb, getMsb, h]
+  · by_cases h' : i < w
+    · simp_all
+    · omega
+
 /-! ### concat -/

@[simp] theorem toNat_concat (x : BitVec w) (b : Bool) :
@@ -546,6 +676,21 @@ theorem getLsb_concat (x : BitVec w) (b : Bool) (i : Nat) :
@[simp] theorem getLsb_concat_succ : (concat x b).getLsb (i + 1) = x.getLsb i := by
  simp [getLsb_concat]

+@[simp] theorem not_concat (x : BitVec w) (b : Bool) : ~~~(concat x b) = concat (~~~x) !b := by
+  ext i; cases i using Fin.succRecOn <;> simp [*, Nat.succ_lt_succ]
+
+@[simp] theorem concat_or_concat (x y : BitVec w) (a b : Bool) :
+    (concat x a) ||| (concat y b) = concat (x ||| y) (a || b) := by
+  ext i; cases i using Fin.succRecOn <;> simp
+
+@[simp] theorem concat_and_concat (x y : BitVec w) (a b : Bool) :
+    (concat x a) &&& (concat y b) = concat (x &&& y) (a && b) := by
+  ext i; cases i using Fin.succRecOn <;> simp
+
+@[simp] theorem concat_xor_concat (x y : BitVec w) (a b : Bool) :
+    (concat x a) ^^^ (concat y b) = concat (x ^^^ y) (xor a b) := by
+  ext i; cases i using Fin.succRecOn <;> simp
+
 /-! ### add -/

 theorem add_def {n} (x y : BitVec n) : x + y = .ofNat n (x.toNat + y.toNat) := rfl
@@ -572,6 +717,10 @@ protected theorem add_comm (x y : BitVec n) : x + y = y + x := by

@[simp] protected theorem zero_add (x : BitVec n) : 0#n + x = x := by simp [add_def]

+theorem truncate_add (x y : BitVec w) (h : i ≤ w) :
+    (x + y).truncate i = x.truncate i + y.truncate i := by
+  have dvd : 2^i ∣ 2^w := Nat.pow_dvd_pow _ h
+  simp [bv_toNat, h, Nat.mod_mod_of_dvd _ dvd]

 /-! ### sub/neg -/

--- a/src/Init/Data/Bool.lean
+++ b/src/Init/Data/Bool.lean
@@ -29,6 +29,8 @@ instance (p : Bool → Prop) [inst : DecidablePred p] : Decidable (∃ x, p x) :
  | _, isTrue hf => isTrue ⟨_, hf⟩
  | isFalse ht, isFalse hf => isFalse fun | ⟨true, h⟩ => absurd h ht | ⟨false, h⟩ => absurd h hf

+@[simp] theorem default_bool : default = false := rfl
+
 instance : LE Bool := ⟨(. → .)⟩
 instance : LT Bool := ⟨(!. && .)⟩

@@ -48,85 +50,202 @@ 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

-@[simp] theorem decide_eq_true {b : Bool} : decide (b = true) = b := by cases b <;> simp
-@[simp] theorem decide_eq_false {b : Bool} : decide (b = false) = !b := by cases b <;> simp
-@[simp] theorem decide_true_eq {b : Bool} : decide (true = b) = b := by cases b <;> simp
-@[simp] theorem decide_false_eq {b : Bool} : decide (false = b) = !b := by cases b <;> simp
+@[simp] theorem decide_eq_true  {b : Bool} [Decidable (b = true)]  : decide (b = true)  =  b := by cases b <;> simp
+@[simp] theorem decide_eq_false {b : Bool} [Decidable (b = false)] : decide (b = false) = !b := by cases b <;> simp
+@[simp] theorem decide_true_eq  {b : Bool} [Decidable (true = b)]  : decide (true  = b) =  b := by cases b <;> simp
+@[simp] theorem decide_false_eq {b : Bool} [Decidable (false = b)] : decide (false = b) = !b := by cases b <;> simp

 /-! ### and -/

-@[simp] theorem not_and_self : ∀ (x : Bool), (!x && x) = false := by decide
+@[simp] theorem and_self_left  : ∀(a b : Bool), (a && (a && b)) = (a && b) := by decide
+@[simp] theorem and_self_right : ∀(a b : Bool), ((a && b) && b) = (a && b) := by decide

+@[simp] theorem not_and_self : ∀ (x : Bool), (!x && x) = false := by decide
@[simp] theorem and_not_self : ∀ (x : Bool), (x && !x) = false := by decide

+/-
+Added for confluence with `not_and_self` `and_not_self` on term
+`(b && !b) = true` due to reductions:
+
+1. `(b = true ∨ !b = true)` via `Bool.and_eq_true`
+2. `false = true` via `Bool.and_not_self`
+-/
+@[simp] theorem eq_true_and_eq_false_self : ∀(b : Bool), (b = true ∧ b = false) ↔ False := by decide
+@[simp] theorem eq_false_and_eq_true_self : ∀(b : Bool), (b = false ∧ b = true) ↔ 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
+/-
+Bool version `and_iff_left_iff_imp`.

-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
+Needed for confluence of term `(a && b) ↔ a` which reduces to `(a && b) = a` via
+`Bool.coe_iff_coe` and `a → b` via `Bool.and_eq_true` and
+`and_iff_left_iff_imp`.
+-/
+@[simp] theorem and_iff_left_iff_imp  : ∀(a b : Bool), ((a && b) = a) ↔ (a → b) := by decide
+@[simp] theorem and_iff_right_iff_imp : ∀(a b : Bool), ((a && b) = b) ↔ (b → a) := by decide
+@[simp] theorem iff_self_and : ∀(a b : Bool), (a = (a && b)) ↔ (a → b) := by decide
+@[simp] theorem iff_and_self : ∀(a b : Bool), (b = (a && b)) ↔ (b → a) := by decide

 /-! ### or -/

-@[simp] theorem not_or_self : ∀ (x : Bool), (!x || x) = true := by decide
+@[simp] theorem or_self_left  : ∀(a b : Bool), (a || (a || b)) = (a || b) := by decide
+@[simp] theorem or_self_right : ∀(a b : Bool), ((a || b) || b) = (a || b) := by decide

+@[simp] theorem not_or_self : ∀ (x : Bool), (!x || x) = true := by decide
@[simp] theorem or_not_self : ∀ (x : Bool), (x || !x) = true := by decide

+/-
+Added for confluence with `not_or_self` `or_not_self` on term
+`(b || !b) = true` due to reductions:
+1. `(b = true ∨ !b = true)` via `Bool.or_eq_true`
+2. `true = true` via `Bool.or_not_self`
+-/
+@[simp] theorem eq_true_or_eq_false_self : ∀(b : Bool), (b = true ∨ b = false) ↔ True := by decide
+@[simp] theorem eq_false_or_eq_true_self : ∀(b : Bool), (b = false ∨ b = true) ↔ True := by decide
+
+/-
+Bool version `or_iff_left_iff_imp`.
+
+Needed for confluence of term `(a || b) ↔ a` which reduces to `(a || b) = a` via
+`Bool.coe_iff_coe` and `a → b` via `Bool.or_eq_true` and
+`and_iff_left_iff_imp`.
+-/
+@[simp] theorem or_iff_left_iff_imp  : ∀(a b : Bool), ((a || b) = a) ↔ (b → a) := by decide
+@[simp] theorem or_iff_right_iff_imp : ∀(a b : Bool), ((a || b) = b) ↔ (a → b) := by decide
+@[simp] theorem iff_self_or : ∀(a b : Bool), (a = (a || b)) ↔ (b → a) := by decide
+@[simp] theorem iff_or_self : ∀(a b : Bool), (b = (a || b)) ↔ (a → b) := 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
+/-! ### distributivity -/

-theorem or_and_distrib_right : ∀ (x y z : Bool), ((x && y) || z) = ((x || z) && (y || z)) := 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 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 and -/
+@[simp] theorem not_and : ∀ (x y : Bool), (!(x && y)) = (!x || !y) := by decide

 /-- De Morgan's law for boolean or -/
-theorem not_or : ∀ (x y : Bool), (!(x || y)) = (!x && !y) := by decide
+@[simp] 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 and_eq_true_iff (x y : Bool) : (x && y) = true ↔ x = true ∧ y = true :=
+  Iff.of_eq (and_eq_true x y)

-theorem or_eq_false_iff : ∀ (x y : Bool), (x || y) = false ↔ x = false ∧ y = false := by decide
+theorem and_eq_false_iff : ∀ (x y : Bool), (x && y) = false ↔ x = false ∨ y = false := by decide
+
+/-
+New simp rule that replaces `Bool.and_eq_false_eq_eq_false_or_eq_false` in
+Mathlib due to confluence:
+
+Consider the term: `¬((b && c) = true)`:
+
+1. Reduces to `((b && c) = false)` via `Bool.not_eq_true`
+2. Reduces to `¬(b = true ∧ c = true)` via `Bool.and_eq_true`.
+
+
+1. Further reduces to `b = false ∨ c = false` via `Bool.and_eq_false_eq_eq_false_or_eq_false`.
+2. Further reduces to `b = true → c = false` via `not_and` and `Bool.not_eq_true`.
+-/
+@[simp] theorem and_eq_false_imp : ∀ (x y : Bool), (x && y) = false ↔ (x = true → y = false) := by decide
+
+@[simp] theorem or_eq_true_iff : ∀ (x y : Bool), (x || y) = true ↔ x = true ∨ y = true := by decide
+
+@[simp] theorem or_eq_false_iff : ∀ (x y : Bool), (x || y) = false ↔ x = false ∧ y = false := by decide
+
+/-! ### eq/beq/bne -/
+
+/--
+These two rules follow trivially by simp, but are needed to avoid non-termination
+in false_eq and true_eq.
+-/
+@[simp] theorem false_eq_true : (false = true) = False := by simp
+@[simp] theorem true_eq_false : (true = false) = False := by simp
+
+-- The two lemmas below normalize terms with a constant to the
+-- right-hand side but risk non-termination if `false_eq_true` and
+-- `true_eq_false` are disabled.
+@[simp low] theorem false_eq (b : Bool) : (false = b) = (b = false) := by
+  cases b <;> simp
+
+@[simp low] theorem true_eq (b : Bool) : (true = b) = (b = true) := by
+  cases b <;> simp
+
+@[simp] theorem true_beq  : ∀b, (true  == b) =  b := by decide
+@[simp] theorem false_beq : ∀b, (false == b) = !b := by decide
+@[simp] theorem beq_true  : ∀b, (b == true)  =  b := by decide
+@[simp] theorem beq_false : ∀b, (b == false) = !b := by decide
+
+@[simp] theorem true_bne  : ∀(b : Bool), (true  != b) = !b := by decide
+@[simp] theorem false_bne : ∀(b : Bool), (false != b) =  b := by decide
+@[simp] theorem bne_true  : ∀(b : Bool), (b != true)  = !b := by decide
+@[simp] theorem bne_false : ∀(b : Bool), (b != false) =  b := by decide
+
+@[simp] theorem not_beq_self : ∀ (x : Bool), ((!x) == x) = false := by decide
+@[simp] theorem beq_not_self : ∀ (x : Bool), (x   == !x) = false := by decide
+
+@[simp] theorem not_bne_self : ∀ (x : Bool), ((!x) != x) = true := by decide
+@[simp] theorem bne_not_self : ∀ (x : Bool), (x   != !x) = true := by decide
+
+/-
+Added for equivalence with `Bool.not_beq_self` and needed for confluence
+due to `beq_iff_eq`.
+-/
+@[simp] theorem not_eq_self : ∀(b : Bool), ((!b) = b) ↔ False := by decide
+@[simp] theorem eq_not_self : ∀(b : Bool), (b = (!b)) ↔ False := by decide
+
+@[simp] theorem beq_self_left  : ∀(a b : Bool), (a == (a == b)) = b := by decide
+@[simp] theorem beq_self_right : ∀(a b : Bool), ((a == b) == b) = a := by decide
+@[simp] theorem bne_self_left  : ∀(a b : Bool), (a != (a != b)) = b := by decide
+@[simp] theorem bne_self_right : ∀(a b : Bool), ((a != b) != b) = a := by decide
+
+@[simp] theorem not_bne_not : ∀ (x y : Bool), ((!x) != (!y)) = (x != y) := by decide
+
+@[simp] theorem bne_assoc : ∀ (x y z : Bool), ((x != y) != z) = (x != (y != z)) := by decide
+
+@[simp] theorem bne_left_inj  : ∀ (x y z : Bool), (x != y) = (x != z) ↔ y = z := by decide
+@[simp] theorem bne_right_inj : ∀ (x y z : Bool), (x != z) = (y != z) ↔ x = y := by decide
+
+/-! ### coercision related normal forms -/
+
+@[simp] theorem not_eq_not : ∀ {a b : Bool}, ¬a = !b ↔ a = b := by decide
+
+@[simp] theorem not_not_eq : ∀ {a b : Bool}, ¬(!a) = b ↔ a = b := by decide
+
+@[simp] theorem coe_iff_coe : ∀(a b : Bool), (a ↔ b) ↔ a = b := by decide
+
+@[simp] theorem coe_true_iff_false  : ∀(a b : Bool), (a ↔ b = false) ↔ a = (!b) := by decide
+@[simp] theorem coe_false_iff_true  : ∀(a b : Bool), (a = false ↔ b) ↔ (!a) = b := by decide
+@[simp] theorem coe_false_iff_false : ∀(a b : Bool), (a = false ↔ b = false) ↔ (!a) = (!b) := by decide

 /-! ### xor -/

-@[simp] theorem false_xor : ∀ (x : Bool), xor false x = x := by decide
+theorem false_xor : ∀ (x : Bool), xor false x = x := false_bne

-@[simp] theorem xor_false : ∀ (x : Bool), xor x false = x := by decide
+theorem xor_false : ∀ (x : Bool), xor x false = x := bne_false

-@[simp] theorem true_xor : ∀ (x : Bool), xor true x = !x := by decide
+theorem true_xor : ∀ (x : Bool), xor true x = !x := true_bne

-@[simp] theorem xor_true : ∀ (x : Bool), xor x true = !x := by decide
+theorem xor_true : ∀ (x : Bool), xor x true = !x := bne_true

-@[simp] theorem not_xor_self : ∀ (x : Bool), xor (!x) x = true := by decide
+theorem not_xor_self : ∀ (x : Bool), xor (!x) x = true := not_bne_self

-@[simp] theorem xor_not_self : ∀ (x : Bool), xor x (!x) = true := by decide
+theorem xor_not_self : ∀ (x : Bool), xor x (!x) = true := bne_not_self

 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 not_xor_not : ∀ (x y : Bool), xor (!x) (!y) = (xor x y) := not_bne_not

 theorem xor_self : ∀ (x : Bool), xor x x = false := by decide

@@ -136,13 +255,11 @@ theorem xor_left_comm : ∀ (x y z : Bool), xor x (xor y z) = xor y (xor x z) :=

 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
+theorem xor_assoc : ∀ (x y z : Bool), xor (xor x y) z = xor x (xor y z) := bne_assoc

-@[simp]
-theorem xor_left_inj : ∀ (x y z : Bool), xor x y = xor x z ↔ y = z := by decide
+theorem xor_left_inj : ∀ (x y z : Bool), xor x y = xor x z ↔ y = z := bne_left_inj

-@[simp]
-theorem xor_right_inj : ∀ (x y z : Bool), xor x z = xor y z ↔ x = y := by decide
+theorem xor_right_inj : ∀ (x y z : Bool), xor x z = xor y z ↔ x = y := bne_right_inj

 /-! ### le/lt -/

@@ -227,16 +344,147 @@ theorem toNat_lt (b : Bool) : b.toNat < 2 :=

@[simp] theorem toNat_eq_zero (b : Bool) : b.toNat = 0 ↔ b = false := by
  cases b <;> simp
-@[simp] theorem toNat_eq_one (b : Bool) : b.toNat = 1 ↔ b = true := by
+@[simp] theorem toNat_eq_one  (b : Bool) : b.toNat = 1 ↔ b = true := by
  cases b <;> simp

-end Bool
+/-! ### ite -/
+
+@[simp] theorem if_true_left  (p : Prop) [h : Decidable p] (f : Bool) :
+    (ite p true f) = (p || f) := by cases h with | _ p => simp [p]
+
+@[simp] theorem if_false_left  (p : Prop) [h : Decidable p] (f : Bool) :
+    (ite p false f) = (!p && f) := by cases h with | _ p => simp [p]
+
+@[simp] theorem if_true_right  (p : Prop) [h : Decidable p] (t : Bool) :
+    (ite p t true) = (!(p : Bool) || t) := by cases h with | _ p => simp [p]
+
+@[simp] theorem if_false_right  (p : Prop) [h : Decidable p] (t : Bool) :
+    (ite p t false) = (p && t) := by cases h with | _ p => simp [p]
+
+@[simp] theorem ite_eq_true_distrib (p : Prop) [h : Decidable p] (t f : Bool) :
+    (ite p t f = true) = ite p (t = true) (f = true) := by
+  cases h with | _ p => simp [p]
+
+@[simp] theorem ite_eq_false_distrib (p : Prop) [h : Decidable p] (t f : Bool) :
+    (ite p t f = false) = ite p (t = false) (f = false) := by
+  cases h with | _ p => simp [p]
+
+/-
+`not_ite_eq_true_eq_true` and related theorems below are added for
+non-confluence.  A motivating example is
+`¬((if u then b else c) = true)`.
+
+This reduces to:
+1. `¬((if u then (b = true) else (c = true))` via `ite_eq_true_distrib`
+2. `(if u then b c) = false)` via `Bool.not_eq_true`.
+
+Similar logic holds for `¬((if u then b else c) = false)` and related
+lemmas.
+-/
+
+@[simp]
+theorem not_ite_eq_true_eq_true (p : Prop) [h : Decidable p] (b c : Bool) :
+  ¬(ite p (b = true) (c = true)) ↔ (ite p (b = false) (c = false)) := by
+  cases h with | _ p => simp [p]
+
+@[simp]
+theorem not_ite_eq_false_eq_false (p : Prop) [h : Decidable p] (b c : Bool) :
+  ¬(ite p (b = false) (c = false)) ↔ (ite p (b = true) (c = true)) := by
+  cases h with | _ p => simp [p]
+
+@[simp]
+theorem not_ite_eq_true_eq_false (p : Prop) [h : Decidable p] (b c : Bool) :
+  ¬(ite p (b = true) (c = false)) ↔ (ite p (b = false) (c = true)) := by
+  cases h with | _ p => simp [p]
+
+@[simp]
+theorem not_ite_eq_false_eq_true (p : Prop) [h : Decidable p] (b c : Bool) :
+  ¬(ite p (b = false) (c = true)) ↔ (ite p (b = true) (c = false)) := by
+  cases h with | _ p => simp [p]
+
+/-
+Added for confluence between `if_true_left` and `ite_false_same` on
+`if b = true then True else b = true`
+-/
+@[simp] theorem eq_false_imp_eq_true : ∀(b:Bool), (b = false → b = true) ↔ (b = true) := by decide
+
+/-
+Added for confluence between `if_true_left` and `ite_false_same` on
+`if b = false then True else b = false`
+-/
+@[simp] theorem eq_true_imp_eq_false : ∀(b:Bool), (b = true → b = false) ↔ (b = false) := by decide
+

 /-! ### cond -/

-theorem cond_eq_if : (bif b then x else y) = (if b then x else y) := by
+theorem cond_eq_ite {α} (b : Bool) (t e : α) : cond b t e = if b then t else e := by
  cases b <;> simp

+theorem cond_eq_if : (bif b then x else y) = (if b then x else y) := cond_eq_ite b x y
+
+@[simp] theorem cond_not (b : Bool) (t e : α) : cond (!b) t e = cond b e t := by
+  cases b <;> rfl
+
+@[simp] theorem cond_self (c : Bool) (t : α) : cond c t t = t := by cases c <;> rfl
+
+/-
+This is a simp rule in Mathlib, but results in non-confluence that is
+difficult to fix as decide distributes over propositions.
+
+A possible fix would be to completely simplify away `cond`, but that
+is not taken since it could result in major rewriting of code that is
+otherwise purely about `Bool`.
+-/
+theorem cond_decide {α} (p : Prop) [Decidable p] (t e : α) :
+    cond (decide p) t e = if p then t else e := by
+  simp [cond_eq_ite]
+
+@[simp] theorem cond_eq_ite_iff (a : Bool) (p : Prop) [h : Decidable p] (x y u v : α) :
+  (cond a x y = ite p u v) ↔ ite a x y = ite p u v := by
+  simp [Bool.cond_eq_ite]
+
+@[simp] theorem ite_eq_cond_iff (p : Prop) [h : Decidable p] (a : Bool) (x y u v : α) :
+  (ite p x y = cond a u v) ↔ ite p x y = ite a u v := by
+  simp [Bool.cond_eq_ite]
+
+@[simp] theorem cond_eq_true_distrib : ∀(c t f : Bool),
+    (cond c t f = true) = ite (c = true) (t = true) (f = true) := by
+  decide
+
+@[simp] theorem cond_eq_false_distrib : ∀(c t f : Bool),
+    (cond c t f = false) = ite (c = true) (t = false) (f = false) := by decide
+
+protected theorem cond_true  {α : Type u} {a b : α} : cond true  a b = a := cond_true  a b
+protected theorem cond_false {α : Type u} {a b : α} : cond false a b = b := cond_false a b
+
+@[simp] theorem cond_true_left   : ∀(c f : Bool), cond c true f  = ( c || f) := by decide
+@[simp] theorem cond_false_left  : ∀(c f : Bool), cond c false f = (!c && f) := by decide
+@[simp] theorem cond_true_right  : ∀(c t : Bool), cond c t true  = (!c || t) := by decide
+@[simp] theorem cond_false_right : ∀(c t : Bool), cond c t false = ( c && t) := by decide
+
+@[simp] theorem cond_true_same  : ∀(c b : Bool), cond c c b = (c || b) := by decide
+@[simp] theorem cond_false_same : ∀(c b : Bool), cond c b c = (c && b) := by decide
+
+/-# decidability -/
+
+protected theorem decide_coe (b : Bool) [Decidable (b = true)] : decide (b = true) = b := decide_eq_true
+
+@[simp] theorem decide_and (p q : Prop) [dpq : Decidable (p ∧ q)] [dp : Decidable p] [dq : Decidable q] :
+    decide (p ∧ q) = (p && q) := by
+  cases dp with | _ p => simp [p]
+
+@[simp] theorem decide_or (p q : Prop) [dpq : Decidable (p ∨ q)] [dp : Decidable p] [dq : Decidable q] :
+    decide (p ∨ q) = (p || q) := by
+  cases dp with | _ p => simp [p]
+
+@[simp] theorem decide_iff_dist (p q : Prop) [dpq : Decidable (p ↔ q)] [dp : Decidable p] [dq : Decidable q] :
+    decide (p ↔ q) = (decide p == decide q) := by
+  cases dp with | _ p => simp [p]
+
+end Bool
+
+export Bool (cond_eq_if)
+
 /-! ### decide -/

@[simp] theorem false_eq_decide_iff {p : Prop} [h : Decidable p] : false = decide p ↔ ¬p := by
--- a/src/Init/Data/Fin/Lemmas.lean
+++ b/src/Init/Data/Fin/Lemmas.lean
@@ -687,7 +687,7 @@ decreasing_by decreasing_with

@[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
+  rw [reverseInduction]; simp

@[simp] theorem reverseInduction_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ}
    (i : Fin n) : reverseInduction (motive := motive) zero succ (castSucc i) =
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -69,7 +69,7 @@ theorem mem_cons_self (a : α) (l : List α) : a ∈ a :: l := .head ..
 theorem mem_cons_of_mem (y : α) {a : α} {l : List α} : a ∈ l → a ∈ y :: l := .tail _

 theorem eq_nil_iff_forall_not_mem {l : List α} : l = [] ↔ ∀ a, a ∉ l := by
-  cases l <;> simp
+  cases l <;> simp [-not_or]

 /-! ### append -/

@@ -451,9 +451,9 @@ theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x := by
  induction as with
  | nil => simp [filter]
  | cons a as ih =>
-    by_cases h : p a <;> simp [*, or_and_right]
-    · exact or_congr_left (and_iff_left_of_imp fun | rfl => h).symm
-    · exact (or_iff_right fun ⟨rfl, h'⟩ => h h').symm
+    by_cases h : p a
+    · simp_all [or_and_left]
+    · simp_all [or_and_right]

 theorem filter_eq_nil {l} : filter p l = [] ↔ ∀ a, a ∈ l → ¬p a := by
  simp only [eq_nil_iff_forall_not_mem, mem_filter, not_and]
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -86,6 +86,11 @@ theorem testBit_to_div_mod {x : Nat} : testBit x i = decide (x / 2^i % 2 = 1) :=
  | succ i hyp =>
    simp [hyp, Nat.div_div_eq_div_mul, Nat.pow_succ']

+theorem toNat_testBit (x i : Nat) :
+    (x.testBit i).toNat = x / 2 ^ i % 2 := by
+  rw [Nat.testBit_to_div_mod]
+  rcases Nat.mod_two_eq_zero_or_one (x / 2^i) <;> simp_all
+
 theorem ne_zero_implies_bit_true {x : Nat} (xnz : x ≠ 0) : ∃ i, testBit x i := by
  induction x using div2Induction with
  | ind x hyp =>
@@ -256,25 +261,24 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :

 theorem testBit_one_zero : testBit 1 0 = true := by trivial

+theorem not_decide_mod_two_eq_one (x : Nat)
+    : (!decide (x % 2 = 1)) = decide (x % 2 = 0) := by
+  cases Nat.mod_two_eq_zero_or_one x <;> (rename_i p; simp [p])
+
 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 [← decide_not, decide_eq_decide]
+      simp [not_decide_mod_two_eq_one]
      omega
  | succ i ih =>
    simp only [testBit_succ]
    match n with
    | 0 =>
-      simp only [Nat.pow_zero, succ_sub_succ_eq_sub, Nat.zero_sub, Nat.zero_div, zero_testBit]
-      rw [decide_eq_false] <;> simp
+      simp [decide_eq_false]
    | n+1 =>
      rw [Nat.two_pow_succ_sub_succ_div_two, ih]
      · simp [Nat.succ_lt_succ_iff]
--- a/src/Init/PropLemmas.lean
+++ b/src/Init/PropLemmas.lean
@@ -11,6 +11,18 @@ import Init.Core
 import Init.NotationExtra
 set_option linter.missingDocs true -- keep it documented

+/-! ## cast and equality -/
+
+@[simp] theorem eq_mp_eq_cast  (h : α = β) : Eq.mp  h = cast h := rfl
+@[simp] theorem eq_mpr_eq_cast (h : α = β) : Eq.mpr h = cast h.symm := rfl
+
+@[simp] theorem cast_cast : ∀ (ha : α = β) (hb : β = γ) (a : α),
+    cast hb (cast ha a) = cast (ha.trans hb) a
+  | rfl, rfl, _ => rfl
+
+@[simp] theorem eq_true_eq_id : Eq True = id := by
+  funext _; simp only [true_iff, id.def, eq_iff_iff]
+
 /-! ## not -/

 theorem not_not_em (a : Prop) : ¬¬(a ∨ ¬a) := fun h => h (.inr (h ∘ .inl))
@@ -104,10 +116,62 @@ theorem and_or_right : (a ∧ b) ∨ c ↔ (a ∨ c) ∧ (b ∨ c) := by rw [@or

 theorem or_imp : (a ∨ b → c) ↔ (a → c) ∧ (b → c) :=
  Iff.intro (fun h => ⟨h ∘ .inl, h ∘ .inr⟩) (fun ⟨ha, hb⟩ => Or.rec ha hb)
-theorem not_or : ¬(p ∨ q) ↔ ¬p ∧ ¬q := or_imp
+
+/-
+`not_or` is made simp for confluence with `¬((b || c) = true)`:
+
+Critical pair:
+1. `¬(b = true ∨ c = true)` via `Bool.or_eq_true`.
+2. `(b || c = false)` via `Bool.not_eq_true` which then
+   reduces to `b = false ∧ c = false` via Mathlib simp lemma
+   `Bool.or_eq_false_eq_eq_false_and_eq_false`.
+
+Both reduce to `b = false ∧ c = false` via `not_or`.
+-/
+@[simp] theorem not_or : ¬(p ∨ q) ↔ ¬p ∧ ¬q := or_imp

 theorem not_and_of_not_or_not (h : ¬a ∨ ¬b) : ¬(a ∧ b) := h.elim (mt (·.1)) (mt (·.2))

+
+/-! ## Ite -/
+
+@[simp]
+theorem if_false_left [h : Decidable p] :
+    ite p False q ↔ ¬p ∧ q := by cases h <;> (rename_i g; simp [g])
+
+@[simp]
+theorem if_false_right [h : Decidable p] :
+    ite p q False ↔ p ∧ q := by cases h <;> (rename_i g; simp [g])
+
+/-
+`if_true_left` and `if_true_right` are lower priority because
+they introduce disjunctions and we prefer `if_false_left` and
+`if_false_right` if they overlap.
+-/
+
+@[simp low]
+theorem if_true_left [h : Decidable p] :
+    ite p True q ↔ ¬p → q := by cases h <;> (rename_i g; simp [g])
+
+@[simp low]
+theorem if_true_right [h : Decidable p] :
+    ite p q True ↔ p → q := by cases h <;> (rename_i g; simp [g])
+
+/-- Negation of the condition `P : Prop` in a `dite` is the same as swapping the branches. -/
+@[simp] theorem dite_not [hn : Decidable (¬p)] [h : Decidable p]  (x : ¬p → α) (y : ¬¬p → α) :
+    dite (¬p) x y = dite p (fun h => y (not_not_intro h)) x := by
+  cases h <;> (rename_i g; simp [g])
+
+/-- Negation of the condition `P : Prop` in a `ite` is the same as swapping the branches. -/
+@[simp] theorem ite_not (p : Prop) [Decidable p] (x y : α) : ite (¬p) x y = ite p y x :=
+  dite_not (fun _ => x) (fun _ => y)
+
+@[simp] theorem ite_true_same (p q : Prop) [h : Decidable p] : (if p then p else q) = (¬p → q) := by
+  cases h <;> (rename_i g; simp [g])
+
+@[simp] theorem ite_false_same (p q : Prop) [h : Decidable p] : (if p then q else p) = (p ∧ q) := by
+  cases h <;> (rename_i g; simp [g])
+
 /-! ## exists and forall -/

 section quantifiers
@@ -268,7 +332,14 @@ end quantifiers

 /-! ## decidable -/

-theorem Decidable.not_not [Decidable p] : ¬¬p ↔ p := ⟨of_not_not, not_not_intro⟩
+@[simp] theorem Decidable.not_not [Decidable p] : ¬¬p ↔ p := ⟨of_not_not, not_not_intro⟩
+
+/-- Excluded middle.  Added as alias for Decidable.em -/
+abbrev Decidable.or_not_self := em
+
+/-- Excluded middle commuted.  Added as alias for Decidable.em -/
+theorem Decidable.not_or_self (p : Prop) [h : Decidable p] : ¬p ∨ p := by
+  cases h <;> simp [*]

 theorem Decidable.by_contra [Decidable p] : (¬p → False) → p := of_not_not

@@ -310,7 +381,7 @@ theorem Decidable.not_imp_symm [Decidable a] (h : ¬a → b) (hb : ¬b) : a :=
 theorem Decidable.not_imp_comm [Decidable a] [Decidable b] : (¬a → b) ↔ (¬b → a) :=
  ⟨not_imp_symm, not_imp_symm⟩

-theorem Decidable.not_imp_self [Decidable a] : (¬a → a) ↔ a := by
+@[simp] theorem Decidable.not_imp_self [Decidable a] : (¬a → a) ↔ a := by
  have := @imp_not_self (¬a); rwa [not_not] at this

 theorem Decidable.or_iff_not_imp_left [Decidable a] : a ∨ b ↔ (¬a → b) :=
@@ -389,8 +460,12 @@ theorem Decidable.and_iff_not_or_not [Decidable a] [Decidable b] : a ∧ b ↔
  rw [← not_and_iff_or_not_not, not_not]

 theorem Decidable.imp_iff_right_iff [Decidable a] : (a → b ↔ b) ↔ a ∨ b :=
-  ⟨fun H => (Decidable.em a).imp_right fun ha' => H.1 fun ha => (ha' ha).elim,
-   fun H => H.elim imp_iff_right fun hb => iff_of_true (fun _ => hb) hb⟩
+  Iff.intro
+    (fun h => (Decidable.em a).imp_right fun ha' => h.mp fun ha => (ha' ha).elim)
+    (fun ab => ab.elim imp_iff_right fun hb => iff_of_true (fun _ => hb) hb)
+
+theorem Decidable.imp_iff_left_iff  [Decidable a] : (b ↔ a → b) ↔ a ∨ b :=
+  propext (@Iff.comm (a → b) b) ▸ (@Decidable.imp_iff_right_iff a b _)

 theorem Decidable.and_or_imp [Decidable a] : a ∧ b ∨ (a → c) ↔ a → b ∨ c :=
  if ha : a then by simp only [ha, true_and, true_imp_iff]
@@ -435,3 +510,53 @@ protected theorem Decidable.not_forall_not {p : α → Prop} [Decidable (∃ x,
 protected theorem Decidable.not_exists_not {p : α → Prop} [∀ x, Decidable (p x)] :
    (¬∃ x, ¬p x) ↔ ∀ x, p x := by
  simp only [not_exists, Decidable.not_not]
+
+export Decidable (not_imp_self)
+
+/-
+`decide_implies` simp justification.
+
+We have a critical pair from `decide (¬(p ∧ q))`:
+
+ 1. `decide (p → ¬q)` via `not_and`
+ 2. `!decide (p ∧ q)` via `decide_not` This further refines to
+    `!(decide p) || !(decide q)` via `Bool.decide_and` (in Mathlib) and
+    `Bool.not_and` (made simp in Mathlib).
+
+We introduce `decide_implies` below and then both normalize to
+`!(decide p) || !(decide q)`.
+-/
+@[simp]
+theorem decide_implies (u v : Prop)
+    [duv : Decidable (u → v)] [du : Decidable u] {dv : u → Decidable v}
+  : decide (u → v) = dite u (fun h => @decide v (dv h)) (fun _ => true) :=
+  if h : u then by
+    simp [h]
+  else by
+    simp [h]
+
+/-
+`decide_ite` is needed to resolve critical pair with
+
+We have a critical pair from `decide (ite p b c = true)`:
+
+ 1. `ite p b c` via `decide_coe`
+ 2. `decide (ite p (b = true) (c = true))` via `Bool.ite_eq_true_distrib`.
+
+We introduce `decide_ite` so both normalize to `ite p b c`.
+-/
+@[simp]
+theorem decide_ite (u : Prop) [du : Decidable u] (p q : Prop)
+      [dpq : Decidable (ite u p q)] [dp : Decidable p] [dq : Decidable q] :
+    decide (ite u p q) = ite u (decide p) (decide q) := by
+  cases du <;> simp [*]
+
+/- Confluence for `ite_true_same` and `decide_ite`. -/
+@[simp] theorem ite_true_decide_same (p : Prop) [h : Decidable p] (b : Bool) :
+  (if p then decide p else b) = (decide p || b) := by
+  cases h <;> (rename_i pt; simp [pt])
+
+/- Confluence for `ite_false_same` and `decide_ite`. -/
+@[simp] theorem ite_false_decide_same (p : Prop) [h : Decidable p] (b : Bool) :
+  (if p then b else decide p) = (decide p && b) := by
+  cases h <;> (rename_i pt; simp [pt])
--- a/src/Init/SimpLemmas.lean
+++ b/src/Init/SimpLemmas.lean
@@ -15,12 +15,15 @@ theorem of_eq_false (h : p = False) : ¬ p := fun hp => False.elim (h.mp hp)
 theorem eq_true (h : p) : p = True :=
  propext ⟨fun _ => trivial, fun _ => h⟩

+-- Adding this attribute needs `eq_true`.
+attribute [simp] cast_heq
+
 theorem eq_false (h : ¬ p) : p = False :=
  propext ⟨fun h' => absurd h' h, fun h' => False.elim h'⟩

 theorem eq_false' (h : p → False) : p = False := eq_false h

-theorem eq_true_of_decide {p : Prop} {_ : Decidable p} (h : decide p = true) : p = True :=
+theorem eq_true_of_decide {p : Prop} [Decidable p] (h : decide p = true) : p = True :=
  eq_true (of_decide_eq_true h)

 theorem eq_false_of_decide {p : Prop} {_ : Decidable p} (h : decide p = false) : p = False :=
@@ -124,6 +127,7 @@ end SimprocHelperLemmas
@[simp] theorem not_true_eq_false : (¬ True) = False := by decide

@[simp] theorem not_iff_self : ¬(¬a ↔ a) | H => iff_not_self H.symm
+attribute [simp] iff_not_self

 /-! ## and -/

@@ -173,6 +177,11 @@ theorem or_iff_left_of_imp  (hb : b → a) : (a ∨ b) ↔ a  := Iff.intro (Or.r
@[simp] theorem or_iff_left_iff_imp  : (a ∨ b ↔ a) ↔ (b → a) := Iff.intro (·.mp ∘ Or.inr) or_iff_left_of_imp
@[simp] theorem or_iff_right_iff_imp : (a ∨ b ↔ b) ↔ (a → b) := by rw [or_comm, or_iff_left_iff_imp]

+@[simp] theorem iff_self_or (a b : Prop) : (a ↔ a ∨ b) ↔ (b → a) :=
+  propext (@Iff.comm _ a) ▸ @or_iff_left_iff_imp a b
+@[simp] theorem iff_or_self (a b : Prop) : (b ↔ a ∨ b) ↔ (a → b) :=
+  propext (@Iff.comm _ b) ▸ @or_iff_right_iff_imp a b
+
 /-# Bool -/

@[simp] theorem Bool.or_false (b : Bool) : (b || false) = b  := by cases b <;> rfl
@@ -199,9 +208,9 @@ theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by
@[simp] theorem Bool.not_not (b : Bool) : (!!b) = b := by cases b <;> rfl
@[simp] theorem Bool.not_true  : (!true) = false := by decide
@[simp] theorem Bool.not_false : (!false) = true := by decide
-@[simp] theorem Bool.not_beq_true (b : Bool) : (!(b == true)) = (b == false) := by cases b <;> rfl
+@[simp] theorem Bool.not_beq_true  (b : Bool) : (!(b == true)) = (b == false) := by cases b <;> rfl
@[simp] theorem Bool.not_beq_false (b : Bool) : (!(b == false)) = (b == true) := by cases b <;> rfl
-@[simp] theorem Bool.not_eq_true' (b : Bool) : ((!b) = true) = (b = false) := by cases b <;> simp
+@[simp] theorem Bool.not_eq_true'  (b : Bool) : ((!b) = true) = (b = false) := by cases b <;> simp
@[simp] theorem Bool.not_eq_false' (b : Bool) : ((!b) = false) = (b = true) := by cases b <;> simp

@[simp] theorem Bool.beq_to_eq (a b : Bool) :
@@ -212,11 +221,14 @@ theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by
@[simp] theorem Bool.not_eq_true (b : Bool) : (¬(b = true)) = (b = false) := by cases b <;> decide
@[simp] theorem Bool.not_eq_false (b : Bool) : (¬(b = false)) = (b = true) := by cases b <;> decide

-@[simp] theorem decide_eq_true_eq {_ : Decidable p} : (decide p = true) = p := propext <| Iff.intro of_decide_eq_true decide_eq_true
-@[simp] theorem decide_not {h : Decidable p} : decide (¬ p) = !decide p := by cases h <;> rfl
-@[simp] theorem not_decide_eq_true {h : Decidable p} : ((!decide p) = true) = ¬ p := by cases h <;> simp [decide, *]
+@[simp] theorem decide_eq_true_eq [Decidable p] : (decide p = true) = p :=
+  propext <| Iff.intro of_decide_eq_true decide_eq_true
+@[simp] theorem decide_not [g : Decidable p] [h : Decidable (Not p)] : decide (Not p) = !(decide p) := by
+  cases g <;> (rename_i gp; simp [gp]; rfl)
+@[simp] theorem not_decide_eq_true [h : Decidable p] : ((!decide p) = true) = ¬ p := by
+  cases h <;> (rename_i hp; simp [decide, hp])

-@[simp] theorem heq_eq_eq {α : Sort u} (a b : α) : HEq a b = (a = b) := propext <| Iff.intro eq_of_heq heq_of_eq
+@[simp] theorem heq_eq_eq (a b : α) : HEq a b = (a = b) := propext <| Iff.intro eq_of_heq heq_of_eq

@[simp] theorem cond_true (a b : α) : cond true a b = a := rfl
@[simp] theorem cond_false (a b : α) : cond false a b = b := rfl
@@ -228,11 +240,29 @@ theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by
@[simp] theorem bne_self_eq_false' [DecidableEq α] (a : α) : (a != a) = false := by simp [bne]

@[simp] theorem decide_False : decide False = false := rfl
-@[simp] theorem decide_True : decide True = true := rfl
+@[simp] theorem decide_True  : decide True  = true := rfl

@[simp] theorem bne_iff_ne [BEq α] [LawfulBEq α] (a b : α) : a != b ↔ a ≠ b := by
  simp [bne]; rw [← beq_iff_eq a b]; simp [-beq_iff_eq]

+/-
+Added for critical pair for `¬((a != b) = true)`
+
+1. `(a != b) = false` via `Bool.not_eq_true`
+2. `¬(a ≠ b)` via `bne_iff_ne`
+
+These will both normalize to `a = b` with the first via `bne_eq_false_iff_eq`.
+-/
+@[simp] theorem beq_eq_false_iff_ne [BEq α] [LawfulBEq α]
+    (a b : α) : (a == b) = false ↔ a ≠ b := by
+  rw [ne_eq, ← beq_iff_eq a b]
+  cases a == b <;> decide
+
+@[simp] theorem bne_eq_false_iff_eq [BEq α] [LawfulBEq α] (a b : α) :
+    (a != b) = false ↔ a = b := by
+  rw [bne, ← beq_iff_eq a b]
+  cases a == b <;> decide
+
 /-# Nat -/

@[simp] theorem Nat.le_zero_eq (a : Nat) : (a ≤ 0) = (a = 0) :=
--- a/src/Lean/Elab/CheckTactic.lean
+++ b/src/Lean/Elab/CheckTactic.lean
@@ -7,6 +7,7 @@ prelude
 import Lean.Elab.Tactic.ElabTerm
 import Lean.Elab.Command
 import Lean.Elab.Tactic.Meta
+import Lean.Meta.CheckTactic

 /-!
 Commands to validate tactic results.
@@ -18,15 +19,6 @@ open Lean.Meta CheckTactic
 open Lean.Elab.Tactic
 open Lean.Elab.Command

-private def matchCheckGoalType (stx : Syntax) (goalType : Expr) : MetaM (Expr × Expr × Level) := do
-  let u ← mkFreshLevelMVar
-  let type ← mkFreshExprMVar (some (.sort u))
-  let val  ← mkFreshExprMVar (some type)
-  let extType := mkAppN (.const ``CheckGoalType [u]) #[type, val]
-  if !(← isDefEq goalType extType) then
-    throwErrorAt stx "Goal{indentExpr goalType}\nis expected to match {indentExpr extType}"
-  pure (val, type, u)
-
@[builtin_command_elab Lean.Parser.checkTactic]
 def elabCheckTactic : CommandElab := fun stx => do
  let `(#check_tactic $t ~> $result by $tac) := stx | throwUnsupportedSyntax
@@ -34,11 +26,10 @@ def elabCheckTactic : CommandElab := fun stx => do
    runTermElabM $ fun _vars => do
      let u ← Lean.Elab.Term.elabTerm t none
      let type ← inferType u
-      let lvl ← mkFreshLevelMVar
-      let checkGoalType : Expr := mkApp2 (mkConst ``CheckGoalType [lvl]) type u
+      let checkGoalType ← mkCheckGoalType u type
      let mvar ← mkFreshExprMVar (.some checkGoalType)
-      let (goals, _) ← Lean.Elab.runTactic mvar.mvarId! tac.raw
      let expTerm ← Lean.Elab.Term.elabTerm result (.some type)
+      let (goals, _) ← Lean.Elab.runTactic mvar.mvarId! tac.raw
      match goals with
      | [] =>
        throwErrorAt stx
@@ -51,7 +42,6 @@ def elabCheckTactic : CommandElab := fun stx => do
      | _ => do
        throwErrorAt stx
          m!"{tac} produced multiple goals, but is expected to reduce to {indentExpr expTerm}."
-      pure ()

@[builtin_command_elab Lean.Parser.checkTacticFailure]
 def elabCheckTacticFailure : CommandElab := fun stx => do
@@ -60,8 +50,7 @@ def elabCheckTacticFailure : CommandElab := fun stx => do
    runTermElabM $ fun _vars => do
      let val ← Lean.Elab.Term.elabTerm t none
      let type ← inferType val
-      let lvl ← mkFreshLevelMVar
-      let checkGoalType : Expr := mkApp2 (mkConst ``CheckGoalType [lvl]) type val
+      let checkGoalType ← mkCheckGoalType val type
      let mvar ← mkFreshExprMVar (.some checkGoalType)
      let act := Lean.Elab.runTactic mvar.mvarId! tactic.raw
      match ← try (Term.withoutErrToSorry (some <$> act)) catch _ => pure none with
@@ -73,12 +62,12 @@ def elabCheckTacticFailure : CommandElab := fun stx => do
                pure m!"{indentExpr val}"
          let msg ←
            match gls with
-              | [] => pure m!"{tactic} expected to fail on {val}, but closed goal."
+              | [] => pure m!"{tactic} expected to fail on {t}, but closed goal."
              | [g] =>
-                pure <| m!"{tactic} expected to fail on {val}, but returned: {←ppGoal g}"
+                pure <| m!"{tactic} expected to fail on {t}, but returned: {←ppGoal g}"
              | gls =>
                let app m g := do pure <| m ++ (←ppGoal g)
-                let init := m!"{tactic} expected to fail on {val}, but returned goals:"
+                let init := m!"{tactic} expected to fail on {t}, but returned goals:"
                gls.foldlM (init := init) app
          throwErrorAt stx msg

--- a/src/Lean/Meta.lean
+++ b/src/Lean/Meta.lean
@@ -47,3 +47,4 @@ import Lean.Meta.CoeAttr
 import Lean.Meta.Iterator
 import Lean.Meta.LazyDiscrTree
 import Lean.Meta.LitValues
+import Lean.Meta.CheckTactic
--- a/src/Lean/Meta/CheckTactic.lean
+++ b/src/Lean/Meta/CheckTactic.lean
@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joe Hendrix
+-/
+prelude
+import Lean.Meta.Basic
+
+namespace Lean.Meta.CheckTactic
+
+def mkCheckGoalType (val type : Expr) : MetaM Expr := do
+  let lvl ← mkFreshLevelMVar
+  pure <| mkApp2 (mkConst ``CheckGoalType [lvl]) type val
+
+def matchCheckGoalType (stx : Syntax) (goalType : Expr) : MetaM (Expr × Expr × Level) := do
+  let u ← mkFreshLevelMVar
+  let type ← mkFreshExprMVar (some (.sort u))
+  let val  ← mkFreshExprMVar (some type)
+  let extType := mkAppN (.const ``CheckGoalType [u]) #[type, val]
+  if !(← isDefEq goalType extType) then
+    throwErrorAt stx "Goal{indentExpr goalType}\nis expected to match {indentExpr extType}"
+  pure (val, type, u)
+
+end Lean.Meta.CheckTactic
--- a/src/Lean/Meta/Injective.lean
+++ b/src/Lean/Meta/Injective.lean
@@ -26,8 +26,10 @@ private def mkAnd? (args : Array Expr) : Option Expr := Id.run do

 def elimOptParam (type : Expr) : CoreM Expr := do
  Core.transform type fun e =>
-    let_expr optParam _ a := e | return .continue
-    return TransformStep.visit a
+    if e.isAppOfArity ``optParam 2 then
+      return TransformStep.visit (e.getArg! 0)
+    else
+      return .continue

 private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useEq : Bool) : MetaM (Option Expr) := do
  let us := ctorVal.levelParams.map mkLevelParam
--- a/src/Lean/Meta/LazyDiscrTree.lean
+++ b/src/Lean/Meta/LazyDiscrTree.lean
@@ -698,14 +698,15 @@ private structure ImportFailure where
  /-- Exception that triggers error. -/
  exception : Exception

-#print Lean.Meta.Cache
 /-- Information generation from imported modules. -/
 private structure ImportData where
+  cache : IO.Ref (Lean.Meta.Cache)
  errors : IO.Ref (Array ImportFailure)

 private def ImportData.new : BaseIO ImportData := do
+  let cache ← IO.mkRef {}
  let errors ← IO.mkRef #[]
-  pure { errors }
+  pure { cache, errors }

 private def addConstImportData
    (env : Environment)
@@ -716,7 +717,8 @@ private def addConstImportData
    (name : Name) (constInfo : ConstantInfo) : BaseIO (PreDiscrTree α) := do
  if constInfo.isUnsafe then return tree
  if !allowCompletion env name then return tree
-  let mstate : Meta.State := { cache := {} }
+  let mstate : Meta.State := { cache := ←d.cache.get }
+  d.cache.set {}
  let ctx : Meta.Context := { config := { transparency := .reducible } }
  let cm := (act name constInfo).run ctx mstate
  let cctx : Core.Context := {
@@ -725,7 +727,8 @@ private def addConstImportData
  }
  let cstate : Core.State := {env}
  match ←(cm.run cctx cstate).toBaseIO with
-  | .ok ((a, _), _) =>
+  | .ok ((a, ms), _) =>
+    d.cache.set ms.cache
    pure <| a.foldl (fun t e => t.push e.key e.entry) tree
  | .error e =>
    let i : ImportFailure := {
--- a/tests/bench/server_startup.lean
+++ b/tests/bench/server_startup.lean
@@ -0,0 +1,13 @@
+import Lean.Data.Lsp
+open IO Lean Lsp
+
+def main : IO Unit := do
+  Ipc.runWith (←IO.appPath) #["--server"] do
+    let hIn ← Ipc.stdin
+    hIn.write (←FS.readBinFile "server_startup.log")
+    hIn.flush
+    let initResp ← Ipc.readResponseAs 0 InitializeResult
+    let regWatchReq ← Ipc.readRequestAs "client/registerCapability" Json
+    Ipc.writeNotification ⟨"initialized", InitializedParams.mk⟩
+
+    Ipc.shutdown 1
--- a/tests/bench/server_startup.log
+++ b/tests/bench/server_startup.log
@@ -0,0 +1,3 @@
+Content-Length: 2850
+
+{"jsonrpc":"2.0","id":0,"method":"initialize","params":{"processId":99878,"clientInfo":{"name":"vscode","version":"1.47.1"},"rootPath":null,"rootUri":null,"capabilities":{"workspace":{"applyEdit":true,"workspaceEdit":{"documentChanges":true,"resourceOperations":["create","rename","delete"],"failureHandling":"textOnlyTransactional"},"didChangeConfiguration":{"dynamicRegistration":true},"didChangeWatchedFiles":{"dynamicRegistration":true},"symbol":{"dynamicRegistration":true,"symbolKind":{"valueSet":[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26]}},"executeCommand":{"dynamicRegistration":true},"configuration":true,"workspaceFolders":true},"textDocument":{"publishDiagnostics":{"relatedInformation":true,"versionSupport":false,"tagSupport":{"valueSet":[1,2]}},"synchronization":{"dynamicRegistration":true,"willSave":true,"willSaveWaitUntil":true,"didSave":true},"completion":{"dynamicRegistration":true,"contextSupport":true,"completionItem":{"snippetSupport":true,"commitCharactersSupport":true,"documentationFormat":["markdown","plaintext"],"deprecatedSupport":true,"preselectSupport":true,"tagSupport":{"valueSet":[1]}},"completionItemKind":{"valueSet":[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25]}},"hover":{"dynamicRegistration":true,"contentFormat":["markdown","plaintext"]},"signatureHelp":{"dynamicRegistration":true,"signatureInformation":{"documentationFormat":["markdown","plaintext"],"parameterInformation":{"labelOffsetSupport":true}},"contextSupport":true},"definition":{"dynamicRegistration":true,"linkSupport":true},"references":{"dynamicRegistration":true},"documentHighlight":{"dynamicRegistration":true},"documentSymbol":{"dynamicRegistration":true,"symbolKind":{"valueSet":[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26]},"hierarchicalDocumentSymbolSupport":true},"codeAction":{"dynamicRegistration":true,"isPreferredSupport":true,"codeActionLiteralSupport":{"codeActionKind":{"valueSet":["","quickfix","refactor","refactor.extract","refactor.inline","refactor.rewrite","source","source.organizeImports"]}}},"codeLens":{"dynamicRegistration":true},"formatting":{"dynamicRegistration":true},"rangeFormatting":{"dynamicRegistration":true},"onTypeFormatting":{"dynamicRegistration":true},"rename":{"dynamicRegistration":true,"prepareSupport":true},"documentLink":{"dynamicRegistration":true,"tooltipSupport":true},"typeDefinition":{"dynamicRegistration":true,"linkSupport":true},"implementation":{"dynamicRegistration":true,"linkSupport":true},"colorProvider":{"dynamicRegistration":true},"foldingRange":{"dynamicRegistration":true,"rangeLimit":5000,"lineFoldingOnly":true},"declaration":{"dynamicRegistration":true,"linkSupport":true},"selectionRange":{"dynamicRegistration":true}},"window":{"workDoneProgress":true}},"trace":"off","workspaceFolders":null}}
--- a/tests/bench/speedcenter.exec.velcom.yaml
+++ b/tests/bench/speedcenter.exec.velcom.yaml
@@ -226,6 +226,12 @@
      ulimit -s unlimited
      lake self-check
      "
+- attributes:
+    description: language server startup
+    tags: [fast]
+  run_config:
+    <<: *time
+    cmd: lean -Dlinter.all=false --run server_startup.lean
 - attributes:
    description: liasolver
    tags: [fast, suite]
--- a/tests/lean/1079.lean.expected.out
+++ b/tests/lean/1079.lean.expected.out
@@ -5,32 +5,4 @@
      ?a = ?a
    with
      Ordering.eq = Ordering.lt
-[Meta.Tactic.simp.unify] @forall_exists_index:1000, failed to unify
-      ∀ (h : ∃ x, ?p x), ?q h
-    with
-      False → False
-[Meta.Tactic.simp.unify] @forall_eq:1000, failed to unify
-      ∀ (a : ?α), a = ?a' → ?p a
-    with
-      False → False
-[Meta.Tactic.simp.unify] @forall_eq':1000, failed to unify
-      ∀ (a : ?α), ?a' = a → ?p a
-    with
-      False → False
-[Meta.Tactic.simp.unify] @forall_eq_or_imp:1000, failed to unify
-      ∀ (a : ?α), a = ?a' ∨ ?q a → ?p a
-    with
-      False → False
-[Meta.Tactic.simp.unify] @forall_apply_eq_imp_iff:1000, failed to unify
-      ∀ (b : ?β) (a : ?α), ?f a = b → ?p b
-    with
-      False → False
-[Meta.Tactic.simp.unify] @forall_eq_apply_imp_iff:1000, failed to unify
-      ∀ (b : ?β) (a : ?α), b = ?f a → ?p b
-    with
-      False → False
-[Meta.Tactic.simp.unify] @forall_apply_eq_imp_iff₂:1000, failed to unify
-      ∀ (b : ?β) (a : ?α), ?p a → ?f a = b → ?q b
-    with
-      False → False
-[Meta.Tactic.simp.rewrite] @imp_self:1000, False → False ==> True
+[Meta.Tactic.simp.rewrite] @imp_self:10000, False → False ==> True
--- a/tests/lean/bool_simp.lean
+++ b/tests/lean/bool_simp.lean
@@ -0,0 +1,389 @@
+variable (p q : Prop)
+variable (b c d : Bool)
+variable (u v w : Prop) [Decidable u] [Decidable v] [Decidable w]
+
+-- Specific regressions found when introducing Boolean normalization
+#check_simp (b != !c) = false ~> b = !c
+#check_simp ¬(u → v ∨ w) ~> u ∧ ¬v ∧ ¬w
+#check_simp decide (u ∧ (v → False)) ~> decide u && !decide v
+#check_simp decide (cond true b c = true) ~> b
+#check_simp decide (ite u b c = true) ~> ite u b c
+#check_simp true ≠ (b || c) ~> b = false ∧ c = false
+#check_simp ¬((!b = false) ∧ (c = false)) ~> b = true → c = true
+#check_simp (((!b) && c) ≠ false) ~> b = false ∧ c = true
+#check_simp (cond b false c ≠ false) ~> b = false ∧ c
+#check_simp (b && c) = false ~> b → c = false
+#check_simp (b && c) ≠   false ~> b ∧ c
+#check_simp decide (u → False) ~> !decide u
+#check_simp decide (¬u) ~> !decide u
+#check_simp (b = true) ≠ (c = false) ~> b = c
+#check_simp (b != c) != (false != d) ~> b != (c != d)
+#check_simp (b == false) ≠ (c != d) ~> b = (c != d)
+#check_simp (b = true) ≠ (c = false) ~> b = c
+#check_simp ¬b = !c ~> b = c
+#check_simp (b == c) = false ~> ¬(b = c)
+#check_simp (true ≠ if u then b else c) ~> (if u then b = false else c = false)
+#check_simp (u ∧ v → False) ~> u → v → False
+#check_simp (u = (v ≠ w)) ~> (u ↔ ¬(v ↔ w))
+#check_simp ((b = false) = (c = false)) ~> (!b) = (!c)
+#check_simp True ≠ (c = false) ~> c = true
+#check_simp u ∧ u ∧ v ~> u ∧ v
+#check_simp b || (b || c) ~> b || c
+#check_simp ((b ≠ c) : Bool) ~> !(decide (b = c))
+#check_simp ((u ≠ v) : Bool) ~> !((u : Bool) == (v : Bool))
+#check_simp decide (u → False) ~> !(decide u)
+#check_simp decide (¬u) ~> !u
+-- Specific regressions done
+
+-- Round trip isomorphisms
+#check_simp (decide (b : Prop)) ~> b
+#check_simp ((u : Bool) : Prop) ~> u
+
+/- # not -/
+
+variable [Decidable u]
+
+-- Ground
+#check_simp (¬True) ~> False
+#check_simp (¬true) ~> False
+#check_simp (!True) ~> false
+#check_simp (!true) ~> false
+
+#check_simp (¬False) ~> True
+#check_simp (!False) ~> true
+#check_simp (¬false) ~> True
+#check_simp (!false) ~> true
+
+/- # Coercions and not -/
+
+#check_simp ¬p !~>
+#check_simp !b !~>
+
+#check_simp (¬u : Prop) !~>
+#check_simp (¬u : Bool) ~> !u
+#check_simp (!u : Prop) ~> ¬u
+#check_simp (!u : Bool) !~>
+#check_simp (¬b : Prop) ~> b = false
+#check_simp (¬b : Bool) ~> !b
+#check_simp (!b : Prop) ~> b = false
+#check_simp (!b : Bool) !~>
+
+#check_simp (¬¬u) ~> u
+
+/- # and -/
+
+-- Validate coercions
+#check_simp (u ∧  v : Prop) !~>
+#check_simp (u ∧  v : Bool) ~> u && v
+#check_simp (u && v : Prop) ~> u ∧  v
+#check_simp (u && v : Bool) !~>
+#check_simp (b ∧  c : Prop) !~>
+#check_simp (b ∧  c : Bool) ~> b && c
+#check_simp (b && c : Prop) ~> b ∧  c
+#check_simp (b && c : Bool) !~>
+
+-- Partial evaluation
+#check_simp (True ∧  v : Prop) ~> v
+#check_simp (True ∧  v : Bool) ~> (v : Bool)
+#check_simp (True && v : Prop) ~> v
+#check_simp (True && v : Bool) ~> (v : Bool)
+#check_simp (true ∧  c : Prop) ~> (c : Prop)
+#check_simp (true ∧  c : Bool) ~> c
+#check_simp (true && c : Prop) ~> (c : Prop)
+#check_simp (true && c : Bool) ~> c
+
+#check_simp (u ∧  True : Prop) ~> u
+#check_simp (u ∧  True : Bool) ~> (u : Bool)
+#check_simp (u && True : Prop) ~> u
+#check_simp (u && True : Bool) ~> (u : Bool)
+#check_simp (b ∧  true : Prop) ~> (b : Prop)
+#check_simp (b ∧  true : Bool) ~> b
+#check_simp (b && true : Prop) ~> (b : Prop)
+#check_simp (b && true : Bool) ~> b
+
+#check_simp (False ∧  v : Prop) ~> False
+#check_simp (False ∧  v : Bool) ~> false
+#check_simp (False && v : Prop) ~> False
+#check_simp (False && v : Bool) ~> false
+#check_simp (false ∧  c : Prop) ~> False
+#check_simp (false ∧  c : Bool) ~> false
+#check_simp (false && c : Prop) ~> False
+#check_simp (false && c : Bool) ~> false
+
+#check_simp (u ∧  False : Prop) ~> False
+#check_simp (u ∧  False : Bool) ~> false
+#check_simp (u && False : Prop) ~> False
+#check_simp (u && False : Bool) ~> false
+#check_simp (b ∧  false : Prop) ~> False
+#check_simp (b ∧  false : Bool) ~> false
+#check_simp (b && false : Prop) ~> False
+#check_simp (b && false : Bool) ~> false
+
+-- Idempotence
+#check_simp (u ∧  u) ~> u
+#check_simp (u && u) ~> (u : Bool)
+#check_simp (b ∧  b) ~> (b : Prop)
+#check_simp (b && b) ~> b
+
+-- Cancelation
+#check_simp (u ∧ ¬u)  ~> False
+#check_simp (¬u ∧ u)  ~> False
+#check_simp (b && ¬b) ~> false
+#check_simp (¬b && b) ~> false
+
+-- Check we swap operators, but do apply deMorgan etc
+#check_simp ¬(u ∧ v)  ~> u → ¬v
+#check_simp decide (¬(u ∧ v))  ~> !u || !v
+#check_simp !(u ∧ v)  ~> !u || !v
+#check_simp ¬(b ∧ c)  ~> b → c = false
+#check_simp !(b ∧ c)  ~> !b || !c
+#check_simp ¬(u && v) ~> u → ¬ v
+#check_simp ¬(b && c) ~> b = true → c = false
+#check_simp !(u && v) ~> !u || !v
+#check_simp !(b && c) ~> !b || !c
+#check_simp ¬u ∧  ¬v !~>
+#check_simp ¬b ∧  ¬c  ~> ((b = false) ∧ (c = false))
+#check_simp ¬u && ¬v  ~> (!u && !v)
+#check_simp ¬b && ¬c  ~> (!b && !c)
+
+-- Some ternary test cases
+#check_simp (u ∧ (v ∧ w) : Prop) !~>
+#check_simp (u ∧ (v ∧ w) : Bool) ~> (u && (v && w))
+#check_simp ((u ∧ v) ∧ w : Prop) !~>
+#check_simp ((u ∧ v) ∧ w : Bool)  ~> ((u && v) && w)
+#check_simp (b && (c && d) : Prop) ~> (b ∧ c ∧ d)
+#check_simp (b && (c && d) : Bool) !~>
+#check_simp ((b && c) && d : Prop)  ~> ((b ∧ c) ∧ d)
+#check_simp ((b && c) && d : Bool) !~>
+
+/- # or -/
+
+-- Validate coercions
+#check_simp p ∨ q !~>
+#check_simp q ∨ p !~>
+#check_simp (u ∨ v : Prop) !~>
+#check_simp (u ∨ v : Bool)  ~> u || v
+#check_simp (u || v : Prop) ~> u ∨  v
+#check_simp (u || v : Bool) !~>
+#check_simp (b ∨ c : Prop)  !~>
+#check_simp (b ∨ c : Bool)  ~> b || c
+#check_simp (b || c : Prop) ~> b ∨  c
+#check_simp (b || c : Bool) !~>
+
+-- Partial evaluation
+#check_simp (True ∨ v : Prop)  ~> True
+#check_simp (True ∨ v : Bool)  ~> true
+#check_simp (True || v : Prop) ~> True
+#check_simp (True || v : Bool) ~> true
+#check_simp (true ∨  c : Prop) ~> True
+#check_simp (true ∨  c : Bool) ~> true
+#check_simp (true || c : Prop) ~> True
+#check_simp (true || c : Bool) ~> true
+
+#check_simp (u ∨  True : Prop) ~> True
+#check_simp (u ∨  True : Bool) ~> true
+#check_simp (u || True : Prop) ~> True
+#check_simp (u || True : Bool) ~> true
+#check_simp (b ∨  true : Prop) ~> True
+#check_simp (b ∨  true : Bool) ~> true
+#check_simp (b || true : Prop) ~> True
+#check_simp (b || true : Bool) ~> true
+
+#check_simp (False ∨ v : Prop)  ~> v
+#check_simp (False ∨ v : Bool)  ~> (v : Bool)
+#check_simp (False || v : Prop) ~> v
+#check_simp (False || v : Bool) ~> (v : Bool)
+#check_simp (false ∨ c : Prop)  ~> (c : Prop)
+#check_simp (false ∨ c : Bool)  ~> c
+#check_simp (false || c : Prop) ~> (c : Prop)
+#check_simp (false || c : Bool) ~> c
+
+#check_simp (u ∨ False : Prop)  ~> u
+#check_simp (u ∨ False : Bool)  ~> (u : Bool)
+#check_simp (u || False : Prop) ~> u
+#check_simp (u || False : Bool) ~> (u : Bool)
+#check_simp (b ∨ false : Prop)  ~> (b : Prop)
+#check_simp (b ∨ false : Bool)  ~> b
+#check_simp (b || false : Prop) ~> (b : Prop)
+#check_simp (b || false : Bool) ~> b
+
+-- Idempotence
+#check_simp (u ∨ u)  ~> u
+#check_simp (u || u) ~> (u : Bool)
+#check_simp (b ∨  b) ~> (b : Prop)
+#check_simp (b || b) ~> b
+
+-- Complement
+-- Note. We may want to revisit this.
+--   Decidable excluded middle currently does not simplify.
+#check_simp ( u ∨  ¬u) !~>
+#check_simp (¬u ∨   u) !~>
+#check_simp ( b || ¬b)  ~> true
+#check_simp (¬b ||  b)  ~> true
+
+-- Check we swap operators, but do apply deMorgan etc
+#check_simp ¬(u ∨ v)  ~> ¬u ∧ ¬v
+#check_simp !(u ∨ v)  ~> !u && !v
+#check_simp ¬(b ∨ c)  ~> b = false ∧ c =false
+#check_simp !(b ∨ c)  ~> !b && !c
+#check_simp ¬(u || v) ~> ¬u ∧ ¬v
+#check_simp ¬(b || c) ~> b = false ∧ c = false
+#check_simp !(u || v) ~> !u && !v
+#check_simp !(b || c) ~> !b && !c
+#check_simp ¬u ∨  ¬v !~>
+#check_simp (¬b) ∨ (¬c)  ~> b = false ∨ c = false
+#check_simp ¬u || ¬v  ~> (!u || !v)
+#check_simp ¬b || ¬c  ~> (!b || !c)
+
+-- Some ternary test cases
+#check_simp (u ∨ (v ∨ w) : Prop) !~>
+#check_simp (u ∨ (v ∨ w) : Bool)   ~> (u || (v || w))
+#check_simp ((u ∨ v) ∨ w : Prop) !~>
+#check_simp ((u ∨ v) ∨ w : Bool)   ~> ((u || v) || w)
+#check_simp (b || (c || d) : Prop) ~> (b ∨ c ∨ d)
+#check_simp (b || (c || d) : Bool) !~>
+#check_simp ((b || c) || d : Prop) ~> ((b ∨ c) ∨ d)
+#check_simp ((b || c) || d : Bool) !~>
+
+/- # and/or -/
+
+-- We don't currently do automatic simplification across and/or/not
+-- This tests for non-unexpected reductions.
+
+#check_simp p ∧ (p ∨ q) !~>
+#check_simp (p ∨ q) ∧ p !~>
+
+#check_simp u ∧ (v ∨ w) !~>
+#check_simp u ∨ (v ∧ w) !~>
+#check_simp (v ∨ w) ∧ u !~>
+#check_simp (v ∧ w) ∨ u !~>
+#check_simp b && (c || d) !~>
+#check_simp b || (c && d) !~>
+#check_simp (c || d) && b !~>
+#check_simp (c && d) || b !~>
+
+/- # implication -/
+
+#check_simp (b → c) !~>
+#check_simp (u → v) !~>
+#check_simp p → q !~>
+#check_simp decide (u → ¬v)  ~> !u || !v
+
+/- # iff -/
+
+#check_simp (u = v : Prop) ~> u ↔ v
+#check_simp (u = v : Bool) ~> u == v
+#check_simp (u ↔ v : Prop) !~>
+#check_simp (u ↔ v : Bool) ~> u == v
+#check_simp (u == v : Prop) ~> u ↔ v
+#check_simp (u == v : Bool) !~>
+
+#check_simp (b = c : Prop) !~>
+#check_simp (b = c : Bool) !~>
+#check_simp (b ↔ c : Prop) ~> b = c
+#check_simp (b ↔ c : Bool) ~> decide (b = c)
+#check_simp (b == c : Prop) ~> b = c
+#check_simp (b == c : Bool) !~>
+
+-- Partial evaluation
+#check_simp (True = v : Prop)  ~> v
+#check_simp (True = v : Bool)  ~> (v : Bool)
+#check_simp (True ↔ v : Prop)  ~> v
+#check_simp (True ↔ v : Bool)  ~> (v : Bool)
+#check_simp (True == v : Prop) ~> v
+#check_simp (True == v : Bool) ~> (v : Bool)
+#check_simp (true =  c : Prop) ~> c = true
+#check_simp (true =  c : Bool) ~> c
+#check_simp (true ↔  c : Prop) ~> c = true
+#check_simp (true ↔  c : Bool) ~> c
+#check_simp (true == c : Prop) ~> (c : Prop)
+#check_simp (true == c : Bool) ~> c
+
+#check_simp (v = True : Prop)  ~> v
+#check_simp (v = True : Bool)  ~> (v : Bool)
+#check_simp (v ↔ True : Prop)  ~> v
+#check_simp (v ↔ True : Bool)  ~> (v : Bool)
+#check_simp (v == True : Prop) ~> v
+#check_simp (v == True : Bool) ~> (v : Bool)
+#check_simp (c = true : Prop) !~>
+#check_simp (c = true : Bool) ~> c
+#check_simp (c ↔ true : Prop) ~> c = true
+#check_simp (c ↔ true : Bool) ~> c
+#check_simp (c == true : Prop) ~> c = true
+#check_simp (c == true : Bool) ~> c
+
+#check_simp (True = v : Prop)  ~> v
+#check_simp (True = v : Bool)  ~> (v : Bool)
+#check_simp (True ↔ v : Prop)  ~> v
+#check_simp (True ↔ v : Bool)  ~> (v : Bool)
+#check_simp (True == v : Prop) ~> v
+#check_simp (True == v : Bool) ~> (v : Bool)
+#check_simp (true =  c : Prop) ~> c = true
+#check_simp (true =  c : Bool) ~> c
+#check_simp (true ↔  c : Prop) ~> c = true
+#check_simp (true ↔  c : Bool) ~> c
+#check_simp (true == c : Prop) ~> (c : Prop)
+#check_simp (true == c : Bool) ~> c
+
+#check_simp (v = False : Prop)  ~> ¬v
+#check_simp (v = False : Bool)  ~> !v
+#check_simp (v ↔ False : Prop)  ~> ¬v
+#check_simp (v ↔ False : Bool)  ~> !v
+#check_simp (v == False : Prop) ~> ¬v
+#check_simp (v == False : Bool) ~> !v
+#check_simp (c = false : Prop) !~>
+#check_simp (c = false : Bool) ~> !c
+#check_simp (c ↔ false : Prop) ~> c = false
+#check_simp (c ↔ false : Bool) ~> !c
+#check_simp (c == false : Prop) ~> c = false
+#check_simp (c == false : Bool) ~> !c
+
+#check_simp (False = v : Prop)  ~> ¬v
+#check_simp (False = v : Bool)  ~> !v
+#check_simp (False ↔ v : Prop)  ~> ¬v
+#check_simp (False ↔ v : Bool)  ~> !v
+#check_simp (False == v : Prop) ~> ¬v
+#check_simp (False == v : Bool) ~> !v
+#check_simp (false =  c : Prop) ~> c = false
+#check_simp (false =  c : Bool) ~> !c
+#check_simp (false ↔  c : Prop) ~> c = false
+#check_simp (false ↔  c : Bool) ~> !c
+#check_simp (false == c : Prop) ~> c = false
+#check_simp (false == c : Bool) ~> !c
+
+-- Ternary (expand these)
+
+#check_simp (u == (v =  w)) ~> u == (v == w)
+#check_simp (u == (v == w)) !~>
+
+/- # bne -/
+
+#check_simp p ≠ q ~> ¬(p ↔ q)
+#check_simp (b != c : Bool) !~>
+#check_simp ¬(p = q) ~> ¬(p ↔ q)
+#check_simp b ≠ c    ~> b ≠ c
+#check_simp ¬(b = c) !~>
+#check_simp ¬(b ↔ c) ~> ¬(b = c)
+#check_simp (b != c : Prop) ~> b ≠ c
+#check_simp u ≠ v    ~> ¬(u ↔ v)
+#check_simp ¬(u = v) ~> ¬(u ↔ v)
+#check_simp ¬(u ↔ v) !~>
+#check_simp ((u:Bool) != v : Bool) !~>
+#check_simp ((u:Bool) != v : Prop) ~> ¬(u ↔ v)
+
+/- # equality and and/or interactions -/
+
+#check_simp (u == (v ∨ w)) ~>  u == (v || w)
+#check_simp (u == (v || w)) !~>
+#check_simp ((u ∧ v) == w) ~> (u && v) == w
+
+/- # ite/cond -/
+
+#check_simp if b then c else d !~>
+#check_simp if b then p else q !~>
+#check_simp if u then p else q !~>
+#check_simp if u then b else c !~>
+#check_simp if u then u else q ~> ¬u → q
+#check_simp if u then q else u ~> u ∧ q
+#check_simp if u then q else q  ~> q
+#check_simp cond b c d !~>
--- a/tests/lean/bool_simp.lean.expected.out
+++ b/tests/lean/bool_simp.lean.expected.out
--- a/tests/lean/run/bitblast.lean
+++ b/tests/lean/run/bitblast.lean
@@ -0,0 +1,66 @@
+open BitVec
+
+/-!
+This is not how you should implement a `bitblast` tactic!
+Relying on the simplifier to unroll the bitwise quantifier is not efficient.
+
+A proper bitblaster is in the works.
+
+Nevertheless this is a simple test bed for BitVec lemmas.
+-/
+
+theorem Fin.forall_eq_forall_lt (p : Fin n → Prop) [DecidablePred p] :
+    (∀ (x : Fin n), p x) ↔ (∀ (x : Fin n), x < n → p x) := by
+  simp
+
+theorem Fin.forall_lt_succ (p : Fin n → Prop) [DecidablePred p] (k : Nat) :
+    (∀ (x : Fin n), x < (k + 1) → p x) ↔
+      if h : k < n then
+        (p ⟨k, h⟩ ∧ ∀ (x : Fin n), x < k → p x)
+      else
+        ∀ (x : Fin n), x < k → p x := by
+  constructor
+  · intro w
+    split <;> rename_i h
+    · constructor
+      · exact w ⟨k, h⟩ (by dsimp; omega)
+      · intro x q
+        exact w x (by omega)
+    · intro x q
+      exact w _ (by omega)
+  · intro w x q
+    split at w <;> rename_i h
+    · by_cases r : x = k
+      · subst r
+        apply w.1
+      · apply w.2
+        omega
+    · exact w _ (by omega)
+
+theorem Fin.forall_lt_zero (p : Fin n → Prop) [DecidablePred p] :
+    (∀ (x : Fin n), x < (0 : Nat) → p x) ↔ True :=
+  ⟨fun _ => trivial, nofun⟩
+
+macro "bitblast" : tactic => `(tactic|
+  ( apply eq_of_getLsb_eq
+    rw [Fin.forall_eq_forall_lt]
+    repeat rw [Fin.forall_lt_succ, dif_pos (by decide)]
+    rw [Fin.forall_lt_zero]
+    simp [getLsb_add', addOverflow, msb_eq_getLsb_last]))
+
+-- Examples not involving addition:
+example (x : BitVec 64) :
+    (x <<< 32 >>> 32) = (x.truncate 32).zeroExtend 64 := by
+  bitblast
+
+example (x : BitVec 64) : (x <<< 32) &&& (x >>> 32) = 0 := by
+  bitblast
+
+-- Examples involving addition:
+-- (Notice here we are limited to small widths, because of the bad implementation.)
+example (x y : BitVec 32) : (x + y) <<< 1 = (x <<< 1) + (y <<< 1) := by
+  bitblast
+
+example (x y : BitVec 32) :
+    (x + y) &&& 255#32 = (x.truncate 8 + y.truncate 8).zeroExtend 32 := by
+  bitblast
--- a/tests/lean/run/elimOptParam.lean
+++ b/tests/lean/run/elimOptParam.lean
@@ -0,0 +1,14 @@
+import Lean
+
+def f (x := 0) (y := 1) : Nat :=
+  x + y
+
+open Lean Meta
+
+/--
+info: Nat → Nat → Nat
+-/
+#guard_msgs in
+run_meta do
+  let info ← getConstInfo ``f
+  logInfo (← elimOptParam info.type)
--- a/tests/playground/bool_exhaust_test.lean
+++ b/tests/playground/bool_exhaust_test.lean
Author	SHA1	Message	Date
Scott Morrison	0faf31008f	cleanup	2024-03-06 09:17:05 +11:00
Scott Morrison	1f9f87d2f5	better unrolling	2024-03-06 09:09:06 +11:00
Scott Morrison	ae4123d9c0	feat: refactor of BitVec/Bitblast.lean	2024-03-05 22:37:10 +11:00
Joachim Breitner	fbd9c076c0	chore: run nix-ci whenever we run ci (#3600 ) this unifies the `on` settings between nix-ci and ci, less confusion when adding a label doesn’t trigger all the CI stuff.	2024-03-05 09:11:19 +00:00
Scott Morrison	ae492265fe	chore: cleanup a bitblast proof (#3598 )	2024-03-05 04:59:58 +00:00
Scott Morrison	c4a784d6a3	feat: more BitVec lemmas (#3597 )	2024-03-05 04:47:53 +00:00
Scott Morrison	def564183c	feat: checklist for release process (#3536 ) This is still WIP: the checklist for release candidates will get finished as I do the release of `v4.7.0-rc1`. --------- Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>	2024-03-05 02:55:17 +00:00
Alex Keizer	46bf4b69b6	feat: add lemmas about `BitVec.concat` and bitwise ops (#3487 ) Show how the various bitwise ops (`and`, `or`, `not`, and `xor`) distribute over `concat`.	2024-03-05 02:48:10 +00:00
Scott Morrison	89ec60befe	feat: lemmas about BitVec (#3593 ) Basic API lemmas for BitVec, motivated by thinking about bitblasting.	2024-03-05 02:41:47 +00:00
Scott Morrison	f48079eb90	chore: begin development cycle for v4.8.0 (#3596 )	2024-03-05 02:15:37 +00:00
Joe Hendrix	01104cc81e	chore: bool and prop lemmas for Mathlib compatibility and improved confluence (#3508 ) This adds a number of lemmas for simplification of `Bool` and `Prop` terms. It pulls lemmas from Mathlib and adds additional lemmas where confluence or consistency suggested they are needed. It has been tested against Mathlib using some automated test infrastructure. That testing module is not yet included in this PR, but will be included as part of this. Note. There are currently some comments saying the origin of the simp rule. These will be removed prior to merging, but are added to clarify where the rule came from during review. --------- Co-authored-by: Scott Morrison <scott.morrison@gmail.com>	2024-03-04 23:56:30 +00:00
Leonardo de Moura	37450d47e2	fix: bug at `elimOptParam` (#3595 ) `let_expr` uses `cleanupAnnotations` which consumes `optParam` type annotations. cc @nomeata	2024-03-04 23:56:00 +00:00
Scott Morrison	e814fc859e	chore: cherry-picking v4.6.1 release notes (#3592 )	2024-03-04 12:59:00 +00:00
Marc Huisinga	093e1cf22a	test: add language server startup benchmark (#3558 ) Benchmark to catch future regressions as the one fixed in #3552.	2024-03-04 09:01:51 +00:00