Compare commits

...

58 Commits

Author SHA1 Message Date
Leonardo de Moura
1ce0d263a5 chore: cleanup 2025-02-12 14:45:32 -08:00
Leonardo de Moura
0e77743faf chore: refactor 2025-02-12 14:44:07 -08:00
Leonardo de Moura
c803f65283 chore: move 2025-02-12 14:35:37 -08:00
Leonardo de Moura
1d82c7ae22 chore: move to Offset subdir 2025-02-12 14:32:18 -08:00
Leonardo de Moura
e50a91a967 chore: move to Offset subdir 2025-02-12 14:29:28 -08:00
Leonardo de Moura
5896e70244 chore: move to Offset subdir 2025-02-12 14:26:02 -08:00
Lean stage0 autoupdater
b9894b40af chore: update stage0 2025-02-12 17:09:23 +00:00
Markus Himmel
9ff4d53d0b chore: rename UIntX.mk -> UIntX.ofBitVec (#7046)
This PR renames `UIntX.mk` to `UIntX.ofBitVec` and adds deprecations.
2025-02-12 16:08:03 +00:00
Markus Himmel
1e262c2c0e chore: add UIntX.ofNatLT (#7057)
This PR adds the function `UIntX.ofNatLT`. This is supposed to be a
replacement for `UIntX.ofNatCore` and `UIntX.ofNat'`, but for
bootstrapping reasons we need this function to exist in stage0 before we
can proceed with the renaming and deprecations, so this PR just adds the
function.
2025-02-12 15:12:29 +00:00
Markus Himmel
b08fc5dfda feat: IntX.ofBitVec (#7048)
This PR adds the functions `IntX.ofBitVec`.
2025-02-12 14:49:31 +00:00
Joachim Breitner
761c88f10e feat: propagate wfParam through let (#7039)
This PR improves the well-founded definition preprocessing to propagate
`wfParam` through let expressions.

Fixes #7038.
2025-02-12 13:22:08 +00:00
Sebastian Ullrich
07b0e5b7fe chore: compile against glibc 2.26 (#7037)
This PR relaxes the minimum required glibc version for Lean and Lean
executables to 2.26 on x86-64 Linux
2025-02-12 09:29:51 +00:00
Sebastian Ullrich
f7e207a824 chore: remove save tactic (#7047)
This PR removes the `save` and `checkpoint` tactics that have been
superseded by incremental elaboration
2025-02-12 09:19:30 +00:00
Cameron Zwarich
f61e2989a2 fix: make several LCNF environment extensions have asyncMode of .sync (#7041)
This PR marks several LCNF-specific environment extensions as having an
asyncMode of .sync rather than the default of .mainOnly, so they work
correctly even in async contexts.
2025-02-12 09:13:49 +00:00
Joachim Breitner
bdf4b792a8 feat: wf_preprocess for {List,Array}.Monadic functions (#7034)
This PR adds `wf_preprocess` theorems for
`{List,Array}.{foldlM,foldrM,mapM,filterMapM,flatMapM}`
2025-02-12 09:06:12 +00:00
Sebastian Ullrich
d3af1268a7 test: fix simp_arith1 benchmark (#7049) 2025-02-12 10:22:32 +00:00
Lean stage0 autoupdater
01be97309e chore: update stage0 2025-02-12 09:15:43 +00:00
Kim Morrison
3cf6fb2405 chore: fix linter.listVariables naming (#7044) 2025-02-12 05:17:39 +00:00
Leonardo de Moura
2a67a49f31 chore: simp_arith has been deprecated (#7043)
This PR deprecates the tactics `simp_arith`, `simp_arith!`,
`simp_all_arith` and `simp_all_arith!`. Users can just use the `+arith`
option.
2025-02-12 03:55:45 +00:00
Leonardo de Moura
fb2e5e5555 chore: remove dead code from Nat/Linear.lean (#7042) 2025-02-12 02:14:00 +00:00
Leonardo de Moura
b87c01b1c0 feat: simp +arith sorts linear atoms (#7040)
This PR ensures that terms such as `f (2*x + y)` and `f (y + x + x)`
have the same normal form when using `simp +arith`
2025-02-11 23:37:30 +00:00
Paul Reichert
0f1133fe69 feat: tree map data structures and operations (#6914)
This PR introduces ordered map data structures, namely `DTreeMap`,
`TreeMap`, `TreeSet` and their `.Raw` variants, into the standard
library. There are still some operations missing that the hash map has.
As of now, the operations are unverified, but the corresponding lemmas
will follow in subsequent PRs. While the tree map has already been
optimized, more micro-optimization will follow as soon as the new code
generator is ready.

---------

Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
2025-02-11 14:47:47 +00:00
Henrik Böving
f348a082da feat: present bv_decide counter examples for UIntX and enums better (#7033)
This PR improves presentation of counter examples for UIntX and enum
inductives in bv_decide.
2025-02-11 11:01:40 +00:00
Leonardo de Moura
befee896b3 feat: linear integer inequality normalization using gcd of coefficients (#7030)
This PR adds completes the linear integer inequality normalizer for
`grind`. The missing normalization step replaces a linear inequality of
the form `a_1*x_1 + ... + a_n*x_n + b <= 0` with `a_1/k * x_1 + ... +
a_n/k * x_n + ceil(b/k) <= 0` where `k = gcd(a_1, ..., a_n)`.
`ceil(b/k)` is implemented using the helper `cdiv b k`.
2025-02-11 03:45:25 +00:00
Mac Malone
e7fa5891ea feat: lake: provide help on Elan's + option (#7024)
This PR documents how to use Elan's `+` option with `lake new|init`. It
also provides an more informative error message if a `+` option leaks
into Lake (e.g., if a user provides the option to a Lake run without
Elan).
2025-02-11 00:43:38 +00:00
Sebastian Ullrich
3927445973 chore: build Lean with Elab.async (#6989) 2025-02-10 18:16:20 +00:00
Henrik Böving
7d1d761148 feat: bv_decide rewrite multiplication with power of two to shift (#7029)
This PR adds simprocs to bv_decide's preprocessor that rewrite
multiplication with powers of two to constant shifts.
2025-02-10 17:42:59 +00:00
Sebastian Ullrich
7790420cae chore: trivial changes from async-proofs branch (#7028) 2025-02-10 16:44:05 +00:00
Joachim Breitner
4016a80f66 feat: nested well-founded recursion via automatic preprocessing (#6744)
This PR extend the preprocessing of well-founded recursive definitions
to bring assumptions like `h✝ : x ∈ xs` into scope automatically.

This fixes #5471, and follows (roughly) the design written there.
See the module docs at `src/Lean/Elab/PreDefinition/WF/AutoAttach.lean`
for details on the implementation.

This only works for higher-order functions that have a suitable setup.
See for example section “Well-founded recursion preprocessing setup” in
`src/Init/Data/List/Attach.lean`.

This does not change the `decreasing_tactic`, so in some cases there is
still the need for a manual termination proof some cases. We expect a
better termination tactic in the near future.
2025-02-10 16:43:41 +00:00
Lean stage0 autoupdater
feb8cc2d4a chore: update stage0 2025-02-10 16:30:51 +00:00
Markus Himmel
5eed373feb doc: misc. style guide and naming scheme additions (#7026)
This PR clarifies the styling of `do` blocks, and enhanes the naming
conventions with information about the `ext` and `mono` name components
as well as advice about primed names and naming of simp sets.
2025-02-10 15:27:30 +00:00
Sebastian Ullrich
895cdce9bc fix: codegen was allowed improper env ext accesses (#7023) 2025-02-10 15:08:02 +00:00
Kim Morrison
3411518548 chore: rename simp sets (#7017)
This PR renames the simp set `boolToPropSimps` to `bool_to_prop` and
`bv_toNat` to `bitvec_to_nat`. I'll be adding more similarly named simp
sets.
2025-02-10 14:20:18 +00:00
Kim Morrison
13b4b11657 chore: deprecated compile_time_search_path% (#7022)
This PR deprecates `compile_time_search_path%`; it didn't prove useful,
and we've shot ourselves in the foot with it more than once.
2025-02-10 13:49:17 +00:00
Henrik Böving
fa05bccd58 feat: add basic extract theorems for bv_decide (#7021)
This PR adds theorems for interactions of extractLsb with `&&&`, `^^^`,
`~~~` and `bif` to bv_decide's preprocessor.
2025-02-10 13:48:20 +00:00
Kim Morrison
c307e8a04f feat: improvements to simp confluence (#7013)
This PR makes improvements to the simp set for List/Array/Vector/Option
to improve confluence, in preparation for `simp_lc`.
2025-02-10 12:17:44 +00:00
Henrik Böving
2aca375cd9 fix: correct trace nodes in bv_decide (#7019)
This PR properly spells out the trace nodes in bv_decide so they are
visible with just `trace.Meta.Tactic.bv` and `trace.Meta.Tactic.sat`
instead of always having to enable the profiler.
2025-02-10 11:24:52 +00:00
Lean stage0 autoupdater
46ae4c0d7c chore: update stage0 2025-02-10 11:58:06 +00:00
Sebastian Ullrich
6f445a1c05 chore: Task.get block profiling (#7016)
* `--profile` now reports `blocking` time spent in `Task.get` inside
other profiling categories
* environment variable `LEAN_TRACE_TASK_GET_BLOCKED` when set makes
`lean` dump stack traces of `Task.get` blocks
2025-02-10 10:56:49 +00:00
Kim Morrison
80cf782bc6 chore: rename simp sets (#7018)
This is preliminary to #7017; we'll need an update-stage0 before the
actual rename can take place.
2025-02-10 10:56:20 +00:00
Kim Morrison
1622f578c9 chore: replace HashMap.get_ lemmas with getElem_ versions (#7004)
This PR replaces various `HashMap.get_X` with `getElem_X` versions. Now
the left hand sides are in simp normal form (and this fixes some
confluence problems).
2025-02-10 10:37:21 +00:00
Kim Morrison
47814f9da1 chore: add @[simp] to List.flatten_toArray (#7014) 2025-02-10 10:30:41 +00:00
Henrik Böving
0d95bf68cc feat: basic support for handling enum inductives in bv_decide (#6946)
This PR implements basic support for handling of enum inductives in
`bv_decide`. It now supports equality on enum inductive variables (or
other uninterpreted atoms) and constants.
2025-02-10 10:00:20 +00:00
Leonardo de Moura
d61f506da2 feat: simp +arith normalizes coefficient in linear integer polynomials (#7015)
This PR makes sure `simp +arith` normalizes coefficients in linear
integer polynomials. There is still one todo: tightening the bound of
inequalities.
2025-02-10 06:13:28 +00:00
Kim Morrison
7f3e170509 chore: unprotect List.foldlM (#7003) 2025-02-09 22:54:51 +00:00
Leonardo de Moura
bcffbdd3a1 chore: improve withAbstractAtoms (#7012)
We should not abstract free variables
2025-02-09 22:46:09 +00:00
Leonardo de Moura
e14c593003 feat: simp +arith for integers (#7011)
This PR adds `simp +arith` for integers. It uses the new `grind`
normalizer for linear integer arithmetic. We still need to implement
support for dividing the coefficients by their GCD. It also fixes
several bugs in the normalizer.
2025-02-09 21:41:58 +00:00
Leonardo de Moura
bcde913a96 chore: improve expose_names doc string (#7010) 2025-02-09 17:24:07 +00:00
Leonardo de Moura
33b45132a4 feat: bv_decide hint (#7009)
This PR ensures users get an error message saying which module to import
when they try to use `bv_decide`.
2025-02-09 17:11:28 +00:00
Kim Morrison
ef4c6ed83c chore: remove unused Int simp lemmas (#7005) 2025-02-09 16:20:38 +00:00
Leonardo de Moura
cd3eb9125c feat: linear integer arith normalizer (#7002)
This PR implements the normalizer for linear integer arithmetic
expressions. It is not connect to `simp +arith` yet because of some
spurious `[simp]` attributes.
2025-02-09 04:32:54 +00:00
Leonardo de Moura
f6c5aed7ef feat: add Int.Linear normalization support (#7000)
This PR adds helper theorems for justifying the linear integer
normalizer.
2025-02-08 23:01:01 +00:00
Kyle Miller
dd293d1fbd doc: mention Props are equal to True or False (#6998)
This PR modifies the `Prop` docstring to point out that every
proposition is propositionally equal to either `True` or `False`. This
will help point users toward seeing that `Prop` is like `Bool`.

I considered mentioning `Classical.propComplete`, but it's probably
better not making it seem like that's how you should work with
propositions.
2025-02-08 18:11:26 +00:00
Bolton Bailey
4989a60af3 chore: change Lake configuration error message (#6829)
This PR changes the error message for Lake configuration failure to
reflect that issues do not always arise from an invalid lakefile, but
sometimes arise from other issues like network errors. The new error
message encompasses all of these possibilities.

Closes #6827
2025-02-08 15:04:39 +00:00
Joachim Breitner
7c809a94af refactor: elaborate forIn notation without extra let (#6977)
This PR avoids a `let` in the elaboration of `forIn`. It was introduced
in https://github.com/leanprover/lean4/commit/f51328ff112 but nothing
seems to break when I simplify the code. This removes an unexpected `let
col✝ :=…` from the “Expected type” view in the Info View and from the
termination proofs.
2025-02-08 10:32:34 +00:00
Leonardo de Moura
5eca093a89 feat: exact? in try? (#6995)
This PR implements support for `exact?` in the `try?` tactic.
2025-02-07 22:43:30 +00:00
Leonardo de Moura
6d46e31ad8 feat: compress try? suggestions (#6994)
This PR adds the `Try.Config.merge` flag (`true` by default) to the
`try?` tactic. When set to `true`, `try?` compresses suggestions such
as:
```lean
· induction xs, ys using bla.induct
    · grind only [List.length_reverse]
    · grind only [bla]
```
into:
```lean
induction xs, ys using bla.induct <;> grind only [List.length_reverse, bla]
```

This PR also ensures `try?` does not generate suggestions that mixes
`grind` and `grind only`, or `simp` and `simp only` tactics.

This PR also adds the `try? +harder` option (previously called `lib`),
but it has not been fully implemented yet.
2025-02-07 19:17:25 +00:00
Leonardo de Moura
605b9e63c9 chore: disable broken test
It is timing out on OSX, and `master` is failing to build.
This is a temporary "fix."
2025-02-07 11:13:50 -08:00
658 changed files with 11048 additions and 1742 deletions

View File

@@ -137,7 +137,6 @@ jobs:
let large = ${{ github.repository == 'leanprover/lean4' }};
let matrix = [
{
// portable release build: use channel with older glibc (2.27)
"name": "Linux LLVM",
"os": "ubuntu-latest",
"release": false,
@@ -152,6 +151,7 @@ jobs:
"CMAKE_OPTIONS": "-DLLVM=ON -DLLVM_CONFIG=${GITHUB_WORKSPACE}/build/llvm-host/bin/llvm-config"
},
{
// portable release build: use channel with older glibc (2.26)
"name": "Linux release",
"os": large ? "nscloud-ubuntu-22.04-amd64-4x8" : "ubuntu-latest",
"release": true,

View File

@@ -179,7 +179,7 @@ local macro "have_eq " lhs:term:max rhs:term:max : tactic =>
`(tactic|
(have h : $lhs = $rhs :=
-- TODO: replace with linarith
by simp_arith at *; apply Nat.le_antisymm <;> assumption
by simp +arith at *; apply Nat.le_antisymm <;> assumption
try subst $lhs))
/-!

View File

@@ -4,7 +4,7 @@
Platforms built & tested by our CI, available as binary releases via elan (see below)
* x86-64 Linux with glibc 2.27+
* x86-64 Linux with glibc 2.26+
* x86-64 macOS 10.15+
* aarch64 (Apple Silicon) macOS 10.15+
* x86-64 Windows 11 (any version), Windows 10 (version 1903 or higher), Windows Server 2022

View File

@@ -57,13 +57,13 @@ for deciding where to place a theorem, and is, on occasion, a good reason to dup
New types that are added will usually be placed in the `Std` namespace and in the `Std/` source directory, unless there are good reasons to place
them elsewhere.
Inside the `Std`, all internal declarations should be `private` or else have a name component that clearly marks them as internal, preferably
Inside the `Std` namespace, all internal declarations should be `private` or else have a name component that clearly marks them as internal, preferably
`Internal`.
## Naming convention for data
When defining data, i.e., a (possibly 0-ary) function whose codomain is not Sort u, but has type Type u for some u, it should be named in lowerCamelCase. Examples include List.append and List.isPrefixOf.
When defining data, i.e., a (possibly 0-ary) function whose codomain is not Sort u, but has type Type u for some u, it should be named in lowerCamelCase. Examples include `List.append` and `List.isPrefixOf`.
If your data is morally fully specified by its type, then use the naming procedure for theorems described below and convert the result to lower camel case.
If your function returns an `Option`, consider adding `?` as a suffix. If your function may panic, consider adding `!` as a suffix. In many cases, there will be multiple variants of a function; one returning an option, one that may panic and possibly one that takes a proof argument.
@@ -187,10 +187,12 @@ There are certain special “keywords” that may appear in identifiers.
| `distrib` | Theorems of the form `f (g a b) = g (f a) (f b)` | `Nat.add_left_distrib` |
| `self` | May be used if a variable appears multiple times in the conclusion | `List.mem_cons_self` |
| `inj` | Theorems of the form `f a = f b ↔ a = b`. | `Int.neg_inj`, `Nat.add_left_inj` |
| `cancel` | Theorems which have one of the forms `f a = f b →a = b` or `g (f a) = a`, where `f` and `g` usually involve a binary operator | `Nat.add_sub_cancel` |
| `cancel` | Theorems which have one of the forms `f a = f b → a = b` or `g (f a) = a`, where `f` and `g` usually involve a binary operator | `Nat.add_sub_cancel` |
| `cancel_iff` | Same as `inj`, but with different conventions for left and right (see below) | `Nat.add_right_cancel_iff` |
| `ext` | Theorems of the form `f a = f b → a = b`, where `f` usually involves some kind of projection | `List.ext_getElem`
| `mono` | Theorems of the form `a R b → f a R f b`, where `R` is a transitive relation | `List.countP_mono_left`
## Left and right
### Left and right
The keywords left and right are useful to disambiguate symmetric variants of theorems.
@@ -221,6 +223,10 @@ theorem Nat.add_sub_self_right (a b : Nat) : (a + b) - b = a := sorry
theorem Nat.add_sub_cancel (n m : Nat) : (n + m) - m = n := sorry
```
## Primed names
Avoid disambiguating variants of a concept by appending the `'` character (e.g., introducing both `BitVec.sshiftRight` and `BitVec.sshiftRight'`), as it is impossible to tell the difference without looking at the type signature, the documentation or even the code, and even if you know what the two variants are there is no way to tell which is which. Prefer descriptive pairs `BitVec.sshiftRightNat`/`BitVec.sshiftRight`.
## Acronyms
For acronyms which are three letters or shorter, all letters should use the same case as dictated by the convention. For example, `IO` is a correct name for a type and the name `IO.Ref` may become `IORef` when used as part of a definition name and `ioRef` when used as part of a theorem name.
@@ -228,3 +234,8 @@ For acronyms which are three letters or shorter, all letters should use the same
For acronyms which are at least four letters long, switch to lower case starting from the second letter. For example, `Json` is a correct name for a type, as is `JsonRPC`.
If an acronym is typically spelled using mixed case, this mixed spelling may be used in identifiers (for example `Std.Net.IPv4Addr`).
## Simp sets
Simp sets centered around a conversion function should be called `source_to_target`. For example, a simp set for the `BitVec.toNat` function, which goes from `BitVec` to
`Nat`, should be called `bitvec_to_nat`.

View File

@@ -424,6 +424,8 @@ Prefer highly automated tactics (like `grind` and `omega`) over low-level proofs
## `do` notation
The `do` keyword goes on the same line as the corresponding `:=` (or `=>`, or similar). `Id.run do` should be treated as if it was a bare `do`.
Use early `return` statements to reduce nesting depth and make the non-exceptional control flow of a function easier to see.
Alternatives for `let` matches may be placed in the same line or in the next line, indented by two spaces. If the term that is
@@ -455,3 +457,24 @@ def getFunDecl (fvarId : FVarId) : CompilerM FunDecl := do
return decl
```
Correct:
```lean
def tagUntaggedGoals (parentTag : Name) (newSuffix : Name) (newGoals : List MVarId) : TacticM Unit := do
let mctx getMCtx
let mut numAnonymous := 0
for g in newGoals do
if mctx.isAnonymousMVar g then
numAnonymous := numAnonymous + 1
modifyMCtx fun mctx => Id.run do
let mut mctx := mctx
let mut idx := 1
for g in newGoals do
if mctx.isAnonymousMVar g then
if numAnonymous == 1 then
mctx := mctx.setMVarUserName g parentTag
else
mctx := mctx.setMVarUserName g (parentTag ++ newSuffix.appendIndexAfter idx)
idx := idx + 1
pure mctx
```

20
flake.lock generated
View File

@@ -67,12 +67,30 @@
"type": "github"
}
},
"nixpkgs-older": {
"flake": false,
"locked": {
"lastModified": 1523316493,
"narHash": "sha256-5qJS+i5ECICPAKA6FhPLIWkhPKDnOZsZbh2PHYF1Kbs=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "0b307aa73804bbd7a7172899e59ae0b8c347a62d",
"type": "github"
},
"original": {
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "0b307aa73804bbd7a7172899e59ae0b8c347a62d",
"type": "github"
}
},
"root": {
"inputs": {
"flake-utils": "flake-utils",
"nixpkgs": "nixpkgs",
"nixpkgs-cadical": "nixpkgs-cadical",
"nixpkgs-old": "nixpkgs-old"
"nixpkgs-old": "nixpkgs-old",
"nixpkgs-older": "nixpkgs-older"
}
},
"systems": {

View File

@@ -5,17 +5,20 @@
# old nixpkgs used for portable release with older glibc (2.27)
inputs.nixpkgs-old.url = "github:NixOS/nixpkgs/nixos-19.03";
inputs.nixpkgs-old.flake = false;
# old nixpkgs used for portable release with older glibc (2.26)
inputs.nixpkgs-older.url = "github:NixOS/nixpkgs/0b307aa73804bbd7a7172899e59ae0b8c347a62d";
inputs.nixpkgs-older.flake = false;
# for cadical 1.9.5; sync with CMakeLists.txt
inputs.nixpkgs-cadical.url = "github:NixOS/nixpkgs/12bf09802d77264e441f48e25459c10c93eada2e";
inputs.flake-utils.url = "github:numtide/flake-utils";
outputs = { self, nixpkgs, nixpkgs-old, flake-utils, ... }@inputs: flake-utils.lib.eachDefaultSystem (system:
outputs = inputs: inputs.flake-utils.lib.eachDefaultSystem (system:
let
pkgs = import nixpkgs { inherit system; };
pkgs = import inputs.nixpkgs { inherit system; };
# An old nixpkgs for creating releases with an old glibc
pkgsDist-old = import nixpkgs-old { inherit system; };
pkgsDist-old = import inputs.nixpkgs-older { inherit system; };
# An old nixpkgs for creating releases with an old glibc
pkgsDist-old-aarch = import nixpkgs-old { localSystem.config = "aarch64-unknown-linux-gnu"; };
pkgsDist-old-aarch = import inputs.nixpkgs-old { localSystem.config = "aarch64-unknown-linux-gnu"; };
pkgsCadical = import inputs.nixpkgs-cadical { inherit system; };
cadical = if pkgs.stdenv.isLinux then
# use statically-linked cadical on Linux to avoid glibc versioning troubles

View File

@@ -38,7 +38,8 @@ theorem apply_ite (f : α → β) (P : Prop) [Decidable P] (x y : α) :
apply_dite f P (fun _ => x) (fun _ => y)
/-- A `dite` whose results do not actually depend on the condition may be reduced to an `ite`. -/
@[simp] theorem dite_eq_ite [Decidable P] : (dite P (fun _ => a) fun _ => b) = ite P a b := rfl
@[simp] theorem dite_eq_ite [Decidable P] :
(dite P (fun _ => a) (fun _ => b)) = ite P a b := rfl
@[deprecated "Use `ite_eq_right_iff`" (since := "2024-09-18")]
theorem ite_some_none_eq_none [Decidable P] :

View File

@@ -5,6 +5,7 @@ Author: Leonardo de Moura, Sebastian Ullrich
-/
prelude
import Init.Core
import Init.BinderNameHint
universe u v w
@@ -35,6 +36,12 @@ instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α
simp [h]
rfl
@[wf_preprocess] theorem forIn_eq_forin' [d : Membership α ρ] [ForIn' m ρ α d] {β} [Monad m]
(x : ρ) (b : β) (f : (a : α) β m (ForInStep β)) :
forIn x b f = forIn' x b (fun x h => binderNameHint x f <| binderNameHint h () <| f x) := by
simp [binderNameHint]
rfl -- very strange why `simp` did not close it
/-- Extract the value from a `ForInStep`, ignoring whether it is `done` or `yield`. -/
def ForInStep.value (x : ForInStep α) : α :=
match x with

View File

@@ -70,7 +70,7 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
@[csimp] private theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
funext α β p f L h'
cases L
simp only [pmap, pmapImpl, List.attachWith_toArray, List.map_toArray, mk.injEq, List.map_attachWith]
simp only [pmap, pmapImpl, List.attachWith_toArray, List.map_toArray, mk.injEq, List.map_attachWith_eq_pmap]
apply List.pmap_congr_left
intro a m h₁ h₂
congr
@@ -318,7 +318,7 @@ See however `foldl_subtype` below.
theorem foldl_attach (l : Array α) (f : β α β) (b : β) :
l.attach.foldl (fun acc t => f acc t.1) b = l.foldl f b := by
rcases l with l
simp only [List.attach_toArray, List.attachWith_mem_toArray, List.map_attach, size_toArray,
simp only [List.attach_toArray, List.attachWith_mem_toArray, size_toArray,
List.length_pmap, List.foldl_toArray', mem_toArray, List.foldl_subtype]
congr
ext
@@ -337,7 +337,7 @@ See however `foldr_subtype` below.
theorem foldr_attach (l : Array α) (f : α β β) (b : β) :
l.attach.foldr (fun t acc => f t.1 acc) b = l.foldr f b := by
rcases l with l
simp only [List.attach_toArray, List.attachWith_mem_toArray, List.map_attach, size_toArray,
simp only [List.attach_toArray, List.attachWith_mem_toArray, size_toArray,
List.length_pmap, List.foldr_toArray', mem_toArray, List.foldr_subtype]
congr
ext
@@ -354,7 +354,12 @@ theorem attachWith_map {l : Array α} (f : α → β) {P : β → Prop} {H : ∀
cases l
simp [List.attachWith_map]
theorem map_attachWith {l : Array α} {P : α Prop} {H : (a : α), a l P a}
@[simp] theorem map_attachWith {l : Array α} {P : α Prop} {H : (a : α), a l P a}
(f : { x // P x } β) :
(l.attachWith P H).map f = l.attach.map fun x, h => f x, H _ h := by
cases l <;> simp_all
theorem map_attachWith_eq_pmap {l : Array α} {P : α Prop} {H : (a : α), a l P a}
(f : { x // P x } β) :
(l.attachWith P H).map f =
l.pmap (fun a (h : a l P a) => f a, H _ h.1) (fun a h => h, H a h) := by
@@ -362,11 +367,14 @@ theorem map_attachWith {l : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈
ext <;> simp
/-- See also `pmap_eq_map_attach` for writing `pmap` in terms of `map` and `attach`. -/
theorem map_attach {l : Array α} (f : { x // x l } β) :
theorem map_attach_eq_pmap {l : Array α} (f : { x // x l } β) :
l.attach.map f = l.pmap (fun a h => f a, h) (fun _ => id) := by
cases l
ext <;> simp
@[deprecated map_attach_eq_pmap (since := "2025-02-09")]
abbrev map_attach := @map_attach_eq_pmap
theorem attach_filterMap {l : Array α} {f : α Option β} :
(l.filterMap f).attach = l.attach.filterMap
fun x, h => (f x).pbind (fun b m => some b, mem_filterMap.mpr x, h, m) := by
@@ -505,7 +513,7 @@ theorem count_attach [DecidableEq α] (l : Array α) (a : {x // x ∈ l}) :
l.attach.count a = l.count a := by
rcases l with l
simp only [List.attach_toArray, List.attachWith_mem_toArray, List.count_toArray]
rw [List.map_attach, List.count_eq_countP]
rw [List.map_attach_eq_pmap, List.count_eq_countP]
simp only [Subtype.beq_iff]
rw [List.countP_pmap, List.countP_attach (p := (fun x => x == a.1)), List.count]
@@ -642,6 +650,16 @@ and simplifies these to the function directly taking the value.
rw [List.filterMap_subtype]
simp [hf]
@[simp] theorem flatMap_subtype {p : α Prop} {l : Array { x // p x }}
{f : { x // p x } Array β} {g : α Array β} (hf : x h, f x, h = g x) :
(l.flatMap f) = l.unattach.flatMap g := by
cases l
simp only [size_toArray, List.flatMap_toArray, List.unattach_toArray, List.length_unattach,
mk.injEq]
rw [List.flatMap_subtype]
simp [hf]
@[simp] theorem findSome?_subtype {p : α Prop} {l : Array { x // p x }}
{f : { x // p x } Option β} {g : α Option β} (hf : x h, f x, h = g x) :
l.findSome? f = l.unattach.findSome? g := by
@@ -687,4 +705,67 @@ and simplifies these to the function directly taking the value.
(Array.mkArray n x).unattach = Array.mkArray n x.1 := by
simp [unattach]
/-! ### Well-founded recursion preprocessing setup -/
@[wf_preprocess] theorem Array.map_wfParam (xs : Array α) (f : α β) :
(wfParam xs).map f = xs.attach.unattach.map f := by
simp [wfParam]
@[wf_preprocess] theorem Array.map_unattach (P : α Prop) (xs : Array (Subtype P)) (f : α β) :
xs.unattach.map f = xs.map fun x, h =>
binderNameHint x f <| binderNameHint h () <| f (wfParam x) := by
simp [wfParam]
@[wf_preprocess] theorem foldl_wfParam (xs : Array α) (f : β α β) (x : β) :
(wfParam xs).foldl f x = xs.attach.unattach.foldl f x := by
simp [wfParam]
@[wf_preprocess] theorem foldl_unattach (P : α Prop) (xs : Array (Subtype P)) (f : β α β) (x : β):
xs.unattach.foldl f x = xs.foldl (fun s x, h =>
binderNameHint s f <| binderNameHint x (f s) <| binderNameHint h () <| f s (wfParam x)) x := by
simp [wfParam]
@[wf_preprocess] theorem foldr_wfParam (xs : Array α) (f : α β β) (x : β) :
(wfParam xs).foldr f x = xs.attach.unattach.foldr f x := by
simp [wfParam]
@[wf_preprocess] theorem foldr_unattach (P : α Prop) (xs : Array (Subtype P)) (f : α β β) (x : β):
xs.unattach.foldr f x = xs.foldr (fun x, h s =>
binderNameHint x f <| binderNameHint s (f x) <| binderNameHint h () <| f (wfParam x) s) x := by
simp [wfParam]
@[wf_preprocess] theorem filter_wfParam (xs : Array α) (f : α Bool) :
(wfParam xs).filter f = xs.attach.unattach.filter f:= by
simp [wfParam]
@[wf_preprocess] theorem filter_unattach (P : α Prop) (xs : Array (Subtype P)) (f : α Bool) :
xs.unattach.filter f = (xs.filter (fun x, h =>
binderNameHint x f <| binderNameHint h () <| f (wfParam x))).unattach := by
simp [wfParam]
@[wf_preprocess] theorem reverse_wfParam (xs : Array α) :
(wfParam xs).reverse = xs.attach.unattach.reverse := by simp [wfParam]
@[wf_preprocess] theorem reverse_unattach (P : α Prop) (xs : Array (Subtype P)) :
xs.unattach.reverse = xs.reverse.unattach := by simp
@[wf_preprocess] theorem filterMap_wfParam (xs : Array α) (f : α Option β) :
(wfParam xs).filterMap f = xs.attach.unattach.filterMap f := by
simp [wfParam]
@[wf_preprocess] theorem filterMap_unattach (P : α Prop) (xs : Array (Subtype P)) (f : α Option β) :
xs.unattach.filterMap f = xs.filterMap fun x, h =>
binderNameHint x f <| binderNameHint h () <| f (wfParam x) := by
simp [wfParam]
@[wf_preprocess] theorem flatMap_wfParam (xs : Array α) (f : α Array β) :
(wfParam xs).flatMap f = xs.attach.unattach.flatMap f := by
simp [wfParam]
@[wf_preprocess] theorem flatMap_unattach (P : α Prop) (xs : Array (Subtype P)) (f : α Array β) :
xs.unattach.flatMap f = xs.flatMap fun x, h =>
binderNameHint x f <| binderNameHint h () <| f (wfParam x) := by
simp [wfParam]
end Array

View File

@@ -17,13 +17,13 @@ theorem Array.of_push_eq_push {as bs : Array α} (h : as.push a = bs.push b) : a
private theorem List.size_toArrayAux (as : List α) (bs : Array α) : (as.toArrayAux bs).size = as.length + bs.size := by
induction as generalizing bs with
| nil => simp [toArrayAux]
| cons a as ih => simp_arith [toArrayAux, *]
| cons a as ih => simp +arith [toArrayAux, *]
private theorem List.of_toArrayAux_eq_toArrayAux {as bs : List α} {cs ds : Array α} (h : as.toArrayAux cs = bs.toArrayAux ds) (hlen : cs.size = ds.size) : as = bs cs = ds := by
match as, bs with
| [], [] => simp [toArrayAux] at h; simp [h]
| a::as, [] => simp [toArrayAux] at h; rw [ h] at hlen; simp_arith [size_toArrayAux] at hlen
| [], b::bs => simp [toArrayAux] at h; rw [h] at hlen; simp_arith [size_toArrayAux] at hlen
| a::as, [] => simp [toArrayAux] at h; rw [ h] at hlen; simp +arith [size_toArrayAux] at hlen
| [], b::bs => simp [toArrayAux] at h; rw [h] at hlen; simp +arith [size_toArrayAux] at hlen
| a::as, b::bs =>
simp [toArrayAux] at h
have : (cs.push a).size = (ds.push b).size := by simp [*]

View File

@@ -163,7 +163,7 @@ theorem count_le_size (a : α) (l : Array α) : count a l ≤ l.size := countP_l
theorem count_le_count_push (a b : α) (l : Array α) : count a l count a (l.push b) := by
simp [count_push]
@[simp] theorem count_singleton (a b : α) : count a #[b] = if b == a then 1 else 0 := by
theorem count_singleton (a b : α) : count a #[b] = if b == a then 1 else 0 := by
simp [count_eq_countP]
@[simp] theorem count_append (a : α) : l₁ l₂, count a (l₁ ++ l₂) = count a l₁ + count a l₂ :=

View File

@@ -1350,8 +1350,9 @@ theorem map_filter_eq_foldl (f : α → β) (p : α → Bool) (l : Array α) :
simp only [List.filter_cons, List.foldr_cons]
split <;> simp_all
@[simp] theorem filter_append {p : α Bool} (l₁ l₂ : Array α) :
filter p (l₁ ++ l₂) = filter p l₁ ++ filter p l₂ := by
@[simp] theorem filter_append {p : α Bool} (l₁ l₂ : Array α) (w : stop = l₁.size + l₂.size) :
filter p (l₁ ++ l₂) 0 stop = filter p l₁ ++ filter p l₂ := by
subst w
rcases l₁ with l₁
rcases l₂ with l₂
simp [List.filter_append]
@@ -1440,12 +1441,18 @@ theorem _root_.List.filterMap_toArray (f : α → Option β) (l : List α) :
rcases l with l
simp [h]
@[simp] theorem filterMap_eq_map (f : α β) (w : stop = as.size ) :
@[simp] theorem filterMap_eq_map (f : α β) (w : stop = as.size) :
filterMap (some f) as 0 stop = map f as := by
subst w
cases as
simp
/-- Variant of `filterMap_eq_map` with `some ∘ f` expanded out to a lambda. -/
@[simp]
theorem filterMap_eq_map' (f : α β) (w : stop = as.size) :
filterMap (fun x => some (f x)) as 0 stop = map f as :=
filterMap_eq_map f w
theorem filterMap_some_fun : filterMap (some : α Option α) = id := by
funext l
cases l
@@ -1514,8 +1521,9 @@ theorem forall_mem_filterMap {f : α → Option β} {l : Array α} {P : β → P
intro a
rw [forall_comm]
@[simp] theorem filterMap_append {α β : Type _} (l l' : Array α) (f : α Option β) :
filterMap f (l ++ l') = filterMap f l ++ filterMap f l' := by
@[simp] theorem filterMap_append {α β : Type _} (l l' : Array α) (f : α Option β) (w : stop = l.size + l'.size) :
filterMap f (l ++ l') 0 stop = filterMap f l ++ filterMap f l' := by
subst w
cases l
cases l'
simp
@@ -1557,7 +1565,12 @@ theorem filterMap_eq_push_iff {f : α → Option β} {l : Array α} {l' : Array
@[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
simp only [size, toList_append, List.length_append]
@[simp] theorem append_push {as bs : Array α} {a : α} : as ++ bs.push a = (as ++ bs).push a := by
@[simp] theorem push_append {a : α} {xs ys : Array α} : (xs ++ ys).push a = xs ++ ys.push a := by
cases xs
cases ys
simp
theorem append_push {as bs : Array α} {a : α} : as ++ bs.push a = (as ++ bs).push a := by
cases as
cases bs
simp
@@ -1662,12 +1675,15 @@ theorem getElem_append_right' (l₁ : Array α) {l₂ : Array α} {i : Nat} (hi
rw [getElem_append_right] <;> simp [*, Nat.le_add_left]
theorem getElem_of_append {l l₁ l₂ : Array α} (eq : l = l₁.push a ++ l₂) (h : l₁.size = i) :
l[i]'(eq h by simp_arith) = a := Option.some.inj <| by
l[i]'(eq h by simp +arith) = a := Option.some.inj <| by
rw [ getElem?_eq_getElem, eq, getElem?_append_left (by simp; omega), h]
simp
@[simp] theorem append_singleton {a : α} {as : Array α} : as ++ #[a] = as.push a := rfl
@[simp] theorem append_singleton_assoc {a : α} {as bs : Array α} : as ++ (#[a] ++ bs) = as.push a ++ bs := by
rw [ append_assoc, append_singleton]
theorem push_eq_append {a : α} {as : Array α} : as.push a = as ++ #[a] := rfl
theorem append_inj {s₁ s₂ t₁ t₂ : Array α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : s₁.size = s₂.size) :
@@ -1878,7 +1894,8 @@ theorem append_eq_map_iff {f : α → β} :
rw [ flatten_map_toArray]
simp
theorem flatten_toArray (l : List (Array α)) :
-- We set this to lower priority so that `flatten_toArray_map` is applied first when relevant.
@[simp 500] theorem flatten_toArray (l : List (Array α)) :
l.toArray.flatten = (l.map Array.toList).flatten.toArray := by
apply ext'
simp
@@ -1930,15 +1947,17 @@ theorem flatten_eq_flatMap {L : Array (Array α)} : flatten L = L.flatMap id :=
Function.comp_def]
rw [ Function.comp_def, List.map_map, flatten_toArray_map]
@[simp] theorem filterMap_flatten (f : α Option β) (L : Array (Array α)) :
filterMap f (flatten L) = flatten (map (filterMap f) L) := by
@[simp] theorem filterMap_flatten (f : α Option β) (L : Array (Array α)) (w : stop = L.flatten.size) :
filterMap f (flatten L) 0 stop = flatten (map (filterMap f) L) := by
subst w
induction L using array₂_induction
simp only [flatten_toArray_map, size_toArray, List.length_flatten, List.filterMap_toArray',
List.filterMap_flatten, List.map_toArray, List.map_map, Function.comp_def]
rw [ Function.comp_def, List.map_map, flatten_toArray_map]
@[simp] theorem filter_flatten (p : α Bool) (L : Array (Array α)) :
filter p (flatten L) = flatten (map (filter p) L) := by
@[simp] theorem filter_flatten (p : α Bool) (L : Array (Array α)) (w : stop = L.flatten.size) :
filter p (flatten L) 0 stop = flatten (map (filter p) L) := by
subst w
induction L using array₂_induction
simp only [flatten_toArray_map, size_toArray, List.length_flatten, List.filter_toArray',
List.filter_flatten, List.map_toArray, List.map_map, Function.comp_def]
@@ -2140,7 +2159,8 @@ theorem flatMap_eq_foldl (f : α → Array β) (l : Array α) :
| nil => simp
| cons a l ih =>
intro l'
simp [ih ((l' ++ (f a).toList)), toArray_append]
rw [List.foldl_cons, ih]
simp [toArray_append]
/-! ### mkArray -/
@@ -2317,10 +2337,10 @@ theorem getElem?_swap (a : Array α) (i j : Nat) (hi hj) (k : Nat) : (a.swap i j
getElem?_toList]
split <;> rename_i h₂
· simp only [ h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false]
exact (List.getElem?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
exact (List.getElem?_reverse' (j+1) i (Eq.trans (by simp +arith) h)).symm
split <;> rename_i h₃
· simp only [ h₃, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, false_and]
exact (List.getElem?_reverse' i (j+1) (Eq.trans (by simp_arith) h)).symm
exact (List.getElem?_reverse' i (j+1) (Eq.trans (by simp +arith) h)).symm
simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃),
Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))]
· rw [H]; split <;> rename_i h₂
@@ -2395,11 +2415,25 @@ theorem reverse_eq_iff {as bs : Array α} : as.reverse = bs ↔ as = bs.reverse
@[simp] theorem map_reverse (f : α β) (l : Array α) : l.reverse.map f = (l.map f).reverse := by
cases l <;> simp [*]
@[simp] theorem filter_reverse (p : α Bool) (l : Array α) : (l.reverse.filter p) = (l.filter p).reverse := by
/-- Variant of `filter_reverse` with a hypothesis giving the stop condition. -/
@[simp] theorem filter_reverse' (p : α Bool) (l : Array α) (w : stop = l.size) :
(l.reverse.filter p 0 stop) = (l.filter p).reverse := by
subst w
cases l
simp
@[simp] theorem filterMap_reverse (f : α Option β) (l : Array α) : (l.reverse.filterMap f) = (l.filterMap f).reverse := by
theorem filter_reverse (p : α Bool) (l : Array α) : (l.reverse.filter p) = (l.filter p).reverse := by
cases l
simp
/-- Variant of `filterMap_reverse` with a hypothesis giving the stop condition. -/
@[simp] theorem filterMap_reverse' (f : α Option β) (l : Array α) (w : stop = l.size) :
(l.reverse.filterMap f 0 stop) = (l.filterMap f).reverse := by
subst w
cases l
simp
theorem filterMap_reverse (f : α Option β) (l : Array α) : (l.reverse.filterMap f) = (l.filterMap f).reverse := by
cases l
simp
@@ -2875,17 +2909,57 @@ rather than `(arr.push a).size` as the argument.
(h : start = arr.size + 1) : (arr.push a).foldr f init start = arr.foldr f (f a init) :=
foldrM_push' _ _ _ _ h
@[simp] theorem foldl_push_eq_append (l l' : Array α) : l.foldl push l' = l' ++ l := by
cases l
cases l'
@[simp] theorem foldl_push_eq_append {as : Array α} {bs : Array β} {f : α β} (w : stop = as.size) :
as.foldl (fun b a => Array.push b (f a)) bs 0 stop = bs ++ as.map f := by
subst w
rcases as with as
rcases bs with bs
simp only [List.foldl_toArray']
induction as generalizing bs <;> simp [*]
@[simp] theorem foldl_cons_eq_append {as : Array α} {bs : List β} {f : α β} (w : stop = as.size) :
as.foldl (fun b a => (f a) :: b) bs 0 stop = (as.map f).reverse.toList ++ bs := by
subst w
rcases as with as
simp
@[simp] theorem foldr_flip_push_eq_append (l l' : Array α) :
l.foldr (fun x y => push y x) l' = l' ++ l.reverse := by
cases l
cases l'
@[simp] theorem foldr_cons_eq_append {as : Array α} {bs : List β} {f : α β} (w : start = as.size) :
as.foldr (fun a b => (f a) :: b) bs start 0 = (as.map f).toList ++ bs := by
subst w
rcases as with as
simp
/-- Variant of `foldr_cons_eq_append` specialized to `f = id`. -/
@[simp] theorem foldr_cons_eq_append' {as : Array α} {bs : List α} (w : start = as.size) :
as.foldr List.cons bs start 0 = as.toList ++ bs := by
subst w
rcases as with as
simp
@[simp] theorem foldr_append_eq_append (l : Array α) (f : α Array β) (l' : Array β) :
l.foldr (f · ++ ·) l' = (l.map f).flatten ++ l' := by
rcases l with l
rcases l' with l'
induction l <;> simp_all [Function.comp_def, flatten_toArray]
@[simp] theorem foldl_append_eq_append (l : Array α) (f : α Array β) (l' : Array β) :
l.foldl (· ++ f ·) l' = l' ++ (l.map f).flatten := by
rcases l with l
rcases l' with l'
induction l generalizing l'<;> simp_all [Function.comp_def, flatten_toArray]
@[simp] theorem foldr_flip_append_eq_append (l : Array α) (f : α Array β) (l' : Array β) :
l.foldr (fun x y => y ++ f x) l' = l' ++ (l.map f).reverse.flatten := by
rcases l with l
rcases l' with l'
induction l generalizing l' <;> simp_all [Function.comp_def, flatten_toArray]
@[simp] theorem foldl_flip_append_eq_append (l : Array α) (f : α Array β) (l' : Array β) :
l.foldl (fun x y => f y ++ x) l' = (l.map f).reverse.flatten ++ l':= by
rcases l with l
rcases l' with l'
induction l generalizing l' <;> simp_all [Function.comp_def, flatten_toArray]
theorem foldl_map' (f : β₁ β₂) (g : α β₂ α) (l : Array β₁) (init : α) (w : stop = l.size) :
(l.map f).foldl g init 0 stop = l.foldl (fun x y => g x (f y)) init := by
subst w
@@ -3038,6 +3112,13 @@ theorem foldl_eq_foldr_reverse (l : Array α) (f : β → α → β) (b) :
theorem foldr_eq_foldl_reverse (l : Array α) (f : α β β) (b) :
l.foldr f b = l.reverse.foldl (fun x y => f y x) b := by simp
@[simp] theorem foldr_push_eq_append {as : Array α} {bs : Array β} {f : α β} (w : start = as.size) :
as.foldr (fun a b => Array.push b (f a)) bs start 0 = bs ++ (as.map f).reverse := by
subst w
rw [foldr_eq_foldl_reverse, foldl_push_eq_append rfl, map_reverse]
@[deprecated foldr_push_eq_append (since := "2025-02-09")] abbrev foldr_flip_push_eq_append := @foldr_push_eq_append
theorem foldl_assoc {op : α α α} [ha : Std.Associative op] {l : Array α} {a₁ a₂} :
l.foldl op (op a₁ a₂) = op a₁ (l.foldl op a₂) := by
rcases l with l
@@ -3443,11 +3524,11 @@ theorem map_induction (as : Array α) (f : α → β) (motive : Nat → Prop) (h
(motive := fun i arr => motive i arr.size = i i h2, p i arr[i.1])
(init := #[]) (f := fun r a => r.push (f a)) ?_ ?_
obtain m, eq, w := t
· refine m, by simpa [map_eq_foldl] using eq, ?_
· refine m, by simp, ?_
intro i h
simp only [eq] at w
specialize w i, h h
simpa [map_eq_foldl] using w
simpa using w
· exact h0, rfl, nofun
· intro i b m, eq, w
refine ?_, ?_, ?_
@@ -3653,7 +3734,7 @@ theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse := by
l.toArray.mapM f = List.toArray <$> l.mapM f := by
simp only [ mapM'_eq_mapM, mapM_eq_foldlM]
suffices init : Array β,
foldlM (fun bs a => bs.push <$> f a) init l.toArray = (init ++ toArray ·) <$> mapM' f l by
Array.foldlM (fun bs a => bs.push <$> f a) init l.toArray = (init ++ toArray ·) <$> mapM' f l by
simpa using this #[]
intro init
induction l generalizing init with

View File

@@ -8,7 +8,7 @@ import Init.Data.Array.Basic
import Init.Data.Nat.Lemmas
import Init.Data.Range
-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
namespace Array

View File

@@ -12,11 +12,11 @@ namespace Array
theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a as) : sizeOf a < sizeOf as := by
cases as with | _ as =>
exact Nat.lt_trans (List.sizeOf_lt_of_mem h.val) (by simp_arith)
exact Nat.lt_trans (List.sizeOf_lt_of_mem h.val) (by simp +arith)
theorem sizeOf_get [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) : sizeOf (as.get i h) < sizeOf as := by
cases as with | _ as =>
simpa using Nat.lt_trans (List.sizeOf_get _ i, h) (by simp_arith)
simpa using Nat.lt_trans (List.sizeOf_get _ i, h) (by simp +arith)
@[simp] theorem sizeOf_getElem [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) :
sizeOf (as[i]'h) < sizeOf as := sizeOf_get _ _ h
@@ -29,8 +29,8 @@ macro "array_get_dec" : tactic =>
-- subsumed by simp
-- | with_reducible apply sizeOf_get
-- | with_reducible apply sizeOf_getElem
| (with_reducible apply Nat.lt_of_lt_of_le (sizeOf_get ..)); simp_arith
| (with_reducible apply Nat.lt_of_lt_of_le (sizeOf_getElem ..)); simp_arith
| (with_reducible apply Nat.lt_of_lt_of_le (sizeOf_get ..)); simp +arith
| (with_reducible apply Nat.lt_of_lt_of_le (sizeOf_getElem ..)); simp +arith
)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_get_dec)
@@ -45,7 +45,7 @@ macro "array_mem_dec" : tactic =>
| with_reducible
apply Nat.lt_of_lt_of_le (Array.sizeOf_lt_of_mem ?h)
case' h => assumption
simp_arith)
simp +arith)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_mem_dec)

View File

@@ -351,6 +351,16 @@ and simplifies these to the function directly taking the value.
simp
rw [List.foldlM_subtype hf]
@[wf_preprocess] theorem foldlM_wfParam [Monad m] (xs : Array α) (f : β α m β) :
(wfParam xs).foldlM f = xs.attach.unattach.foldlM f := by
simp [wfParam]
@[wf_preprocess] theorem foldlM_unattach [Monad m] (P : α Prop) (xs : Array (Subtype P)) (f : β α m β) :
xs.unattach.foldlM f = xs.foldlM fun b x, h =>
binderNameHint b f <| binderNameHint x (f b) <| binderNameHint h () <|
f b (wfParam x) := by
simp [wfParam]
/--
This lemma identifies monadic folds over lists of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
@@ -364,6 +374,17 @@ and simplifies these to the function directly taking the value.
simp
rw [List.foldrM_subtype hf]
@[wf_preprocess] theorem foldrM_wfParam [Monad m] [LawfulMonad m] (xs : Array α) (f : α β m β) :
(wfParam xs).foldrM f = xs.attach.unattach.foldrM f := by
simp [wfParam]
@[wf_preprocess] theorem foldrM_unattach [Monad m] [LawfulMonad m] (P : α Prop) (xs : Array (Subtype P)) (f : α β m β) :
xs.unattach.foldrM f = xs.foldrM fun x, h b =>
binderNameHint x f <| binderNameHint h () <| binderNameHint b (f x) <|
f (wfParam x) b := by
simp [wfParam]
/--
This lemma identifies monadic maps over lists of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
@@ -375,6 +396,15 @@ and simplifies these to the function directly taking the value.
simp
rw [List.mapM_subtype hf]
@[wf_preprocess] theorem mapM_wfParam [Monad m] [LawfulMonad m] (xs : Array α) (f : α m β) :
(wfParam xs).mapM f = xs.attach.unattach.mapM f := by
simp [wfParam]
@[wf_preprocess] theorem mapM_unattach [Monad m] [LawfulMonad m] (P : α Prop) (xs : Array (Subtype P)) (f : α m β) :
xs.unattach.mapM f = xs.mapM fun x, h =>
binderNameHint x f <| binderNameHint h () <| f (wfParam x) := by
simp [wfParam]
@[simp] theorem filterMapM_subtype [Monad m] [LawfulMonad m] {p : α Prop} {l : Array { x // p x }}
{f : { x // p x } m (Option β)} {g : α m (Option β)} (hf : x h, f x, h = g x) (w : stop = l.size) :
l.filterMapM f 0 stop = l.unattach.filterMapM g := by
@@ -383,6 +413,18 @@ and simplifies these to the function directly taking the value.
simp
rw [List.filterMapM_subtype hf]
@[wf_preprocess] theorem filterMapM_wfParam [Monad m] [LawfulMonad m]
(xs : Array α) (f : α m (Option β)) :
(wfParam xs).filterMapM f = xs.attach.unattach.filterMapM f := by
simp [wfParam]
@[wf_preprocess] theorem filterMapM_unattach [Monad m] [LawfulMonad m]
(P : α Prop) (xs : Array (Subtype P)) (f : α m (Option β)) :
xs.unattach.filterMapM f = xs.filterMapM fun x, h =>
binderNameHint x f <| binderNameHint h () <| f (wfParam x) := by
simp [wfParam]
@[simp] theorem flatMapM_subtype [Monad m] [LawfulMonad m] {p : α Prop} {l : Array { x // p x }}
{f : { x // p x } m (Array β)} {g : α m (Array β)} (hf : x h, f x, h = g x) :
(l.flatMapM f) = l.unattach.flatMapM g := by
@@ -391,4 +433,16 @@ and simplifies these to the function directly taking the value.
rw [List.flatMapM_subtype]
simp [hf]
@[wf_preprocess] theorem flatMapM_wfParam [Monad m] [LawfulMonad m]
(xs : Array α) (f : α m (Array β)) :
(wfParam xs).flatMapM f = xs.attach.unattach.flatMapM f := by
simp [wfParam]
@[wf_preprocess] theorem flatMapM_unattach [Monad m] [LawfulMonad m]
(P : α Prop) (xs : Array (Subtype P)) (f : α m (Array β)) :
xs.unattach.flatMapM f = xs.flatMapM fun x, h =>
binderNameHint x f <| binderNameHint h () <| f (wfParam x) := by
simp [wfParam]
end Array

View File

@@ -31,7 +31,7 @@ instance natCastInst : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩
/-- Theorem for normalizing the bit vector literal representation. -/
-- TODO: This needs more usage data to assess which direction the simp should go.
@[simp, bv_toNat] theorem ofNat_eq_ofNat : @OfNat.ofNat (BitVec n) i _ = .ofNat n i := rfl
@[simp, bitvec_to_nat] theorem ofNat_eq_ofNat : @OfNat.ofNat (BitVec n) i _ = .ofNat n i := rfl
-- Note. Mathlib would like this to go the other direction.
@[simp] theorem natCast_eq_ofNat (w x : Nat) : @Nat.cast (BitVec w) _ x = .ofNat w x := rfl

View File

@@ -1280,4 +1280,17 @@ theorem getMsbD_umod {n d : BitVec w}:
simp [BitVec.getMsbD_eq_getLsbD, hi]
· simp [show w i by omega]
/-! ### Mappings to and from BitVec -/
theorem eq_iff_eq_of_inv (f : α BitVec w) (g : BitVec w α) (h : x, g (f x) = x) :
x y, x = y f x = f y := by
intro x y
constructor
· intro h'
rw [h']
· intro h'
have := congrArg g h'
simpa [h] using this
end BitVec

View File

@@ -108,10 +108,10 @@ theorem toNat_ne_iff_ne {n} {x y : BitVec n} : x.toNat ≠ y.toNat ↔ x ≠ y :
@[simp] theorem val_toFin (x : BitVec w) : x.toFin.val = x.toNat := rfl
@[bv_toNat] theorem toNat_eq {x y : BitVec n} : x = y x.toNat = y.toNat :=
@[bitvec_to_nat] theorem toNat_eq {x y : BitVec n} : x = y x.toNat = y.toNat :=
Iff.intro (congrArg BitVec.toNat) eq_of_toNat_eq
@[bv_toNat] theorem toNat_ne {x y : BitVec n} : x y x.toNat y.toNat := by
@[bitvec_to_nat] theorem toNat_ne {x y : BitVec n} : x y x.toNat y.toNat := by
rw [Ne, toNat_eq]
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i := rfl
@@ -272,7 +272,7 @@ theorem ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b'
@[simp] theorem ofBool_xor_ofBool : ofBool b ^^^ ofBool b' = ofBool (b ^^ b') := by
cases b <;> cases b' <;> rfl
@[simp, bv_toNat] theorem toNat_ofFin (x : Fin (2^n)) : (BitVec.ofFin x).toNat = x.val := rfl
@[simp, bitvec_to_nat] theorem toNat_ofFin (x : Fin (2^n)) : (BitVec.ofFin x).toNat = x.val := rfl
@[simp] theorem toNat_ofNatLt (x : Nat) (p : x < 2^w) : (x#'p).toNat = x := rfl
@@ -284,7 +284,7 @@ theorem ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b'
getMsbD (x#'h) i = (decide (i < n) && x.testBit (n - 1 - i)) := by
simp [getMsbD, getLsbD]
@[simp, bv_toNat] theorem toNat_ofNat (x w : Nat) : (BitVec.ofNat w x).toNat = x % 2^w := by
@[simp, bitvec_to_nat] theorem toNat_ofNat (x w : Nat) : (BitVec.ofNat w x).toNat = x % 2^w := by
simp [BitVec.toNat, BitVec.ofNat, Fin.ofNat']
@[simp] theorem toFin_ofNat (x : Nat) : toFin (BitVec.ofNat w x) = Fin.ofNat' (2^w) x := rfl
@@ -407,7 +407,7 @@ theorem msb_eq_getLsbD_last (x : BitVec w) :
· simp [BitVec.eq_nil x]
· simp
@[bv_toNat] theorem getLsbD_last (x : BitVec w) :
@[bitvec_to_nat] theorem getLsbD_last (x : BitVec w) :
x.getLsbD (w-1) = decide (2 ^ (w-1) x.toNat) := by
rcases w with rfl | w
· simp [toNat_of_zero_length]
@@ -419,10 +419,10 @@ theorem msb_eq_getLsbD_last (x : BitVec w) :
· simp
· omega
@[bv_toNat] theorem getLsbD_succ_last (x : BitVec (w + 1)) :
@[bitvec_to_nat] theorem getLsbD_succ_last (x : BitVec (w + 1)) :
x.getLsbD w = decide (2 ^ w x.toNat) := getLsbD_last x
@[bv_toNat] theorem msb_eq_decide (x : BitVec w) : BitVec.msb x = decide (2 ^ (w-1) x.toNat) := by
@[bitvec_to_nat] theorem msb_eq_decide (x : BitVec w) : BitVec.msb x = decide (2 ^ (w-1) x.toNat) := by
simp [msb_eq_getLsbD_last, getLsbD_last]
theorem toNat_ge_of_msb_true {x : BitVec n} (p : BitVec.msb x = true) : x.toNat 2^(n-1) := by
@@ -439,7 +439,7 @@ theorem msb_eq_getMsbD_zero (x : BitVec w) : x.msb = x.getMsbD 0 := by
/-! ### cast -/
@[simp, bv_toNat] theorem toNat_cast (h : w = v) (x : BitVec w) : (x.cast h).toNat = x.toNat := rfl
@[simp, bitvec_to_nat] theorem toNat_cast (h : w = v) (x : BitVec w) : (x.cast h).toNat = x.toNat := rfl
@[simp] theorem toFin_cast (h : w = v) (x : BitVec w) :
(x.cast h).toFin = x.toFin.cast (by rw [h]) :=
rfl
@@ -513,7 +513,7 @@ theorem toInt_inj {x y : BitVec n} : x.toInt = y.toInt ↔ x = y :=
theorem toInt_ne {x y : BitVec n} : x.toInt y.toInt x y := by
rw [Ne, toInt_inj]
@[simp, bv_toNat] theorem toNat_ofInt {n : Nat} (i : Int) :
@[simp, bitvec_to_nat] theorem toNat_ofInt {n : Nat} (i : Int) :
(BitVec.ofInt n i).toNat = (i % (2^n : Nat)).toNat := by
unfold BitVec.ofInt
simp
@@ -614,11 +614,11 @@ theorem truncate_eq_setWidth {v : Nat} {x : BitVec w} :
theorem zeroExtend_eq_setWidth {v : Nat} {x : BitVec w} :
zeroExtend v x = setWidth v x := rfl
@[simp, bv_toNat] theorem toNat_setWidth' {m n : Nat} (p : m n) (x : BitVec m) :
@[simp, bitvec_to_nat] theorem toNat_setWidth' {m n : Nat} (p : m n) (x : BitVec m) :
(setWidth' p x).toNat = x.toNat := by
simp [setWidth']
@[simp, bv_toNat] theorem toNat_setWidth (i : Nat) (x : BitVec n) :
@[simp, bitvec_to_nat] theorem toNat_setWidth (i : Nat) (x : BitVec n) :
BitVec.toNat (setWidth i x) = x.toNat % 2^i := by
let x, lt_n := x
simp only [setWidth]
@@ -1189,7 +1189,7 @@ theorem extractLsb_xor {x : BitVec w} {hi lo : Nat} :
theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
@[simp, bv_toNat] theorem toNat_not {x : BitVec v} : (~~~x).toNat = 2^v - 1 - x.toNat := by
@[simp, bitvec_to_nat] theorem toNat_not {x : BitVec v} : (~~~x).toNat = 2^v - 1 - x.toNat := by
rw [Nat.sub_sub, Nat.add_comm, not_def, toNat_xor]
apply Nat.eq_of_testBit_eq
intro i
@@ -1344,7 +1344,7 @@ theorem extractLsb_not_of_lt {x : BitVec w} {hi lo : Nat} (hlo : lo ≤ hi) (hhi
/-! ### shiftLeft -/
@[simp, bv_toNat] theorem toNat_shiftLeft {x : BitVec v} :
@[simp, bitvec_to_nat] theorem toNat_shiftLeft {x : BitVec v} :
(x <<< n).toNat = x.toNat <<< n % 2^v :=
BitVec.toNat_ofNat _ _
@@ -1363,7 +1363,7 @@ theorem shiftLeft_zero (x : BitVec w) : x <<< 0 = x := by
@[simp]
theorem zero_shiftLeft (n : Nat) : 0#w <<< n = 0#w := by
simp [bv_toNat]
simp [bitvec_to_nat]
@[simp] theorem getLsbD_shiftLeft (x : BitVec m) (n) :
getLsbD (x <<< n) i = (decide (i < m) && !decide (i < n) && getLsbD x (i - n)) := by
@@ -1501,7 +1501,7 @@ theorem shiftLeft_ofNat_eq {x : BitVec w} {k : Nat} : x <<< (BitVec.ofNat w k) =
/-! ### ushiftRight -/
@[simp, bv_toNat] theorem toNat_ushiftRight (x : BitVec n) (i : Nat) :
@[simp, bitvec_to_nat] theorem toNat_ushiftRight (x : BitVec n) (i : Nat) :
(x >>> i).toNat = x.toNat >>> i := rfl
@[simp] theorem getLsbD_ushiftRight (x : BitVec n) (i j : Nat) :
@@ -1529,11 +1529,11 @@ theorem ushiftRight_or_distrib (x y : BitVec w) (n : Nat) :
@[simp]
theorem ushiftRight_zero (x : BitVec w) : x >>> 0 = x := by
simp [bv_toNat]
simp [bitvec_to_nat]
@[simp]
theorem zero_ushiftRight {n : Nat} : 0#w >>> n = 0#w := by
simp [bv_toNat]
simp [bitvec_to_nat]
/--
Shifting right by `n < w` yields a bitvector whose value is less than `2 ^ (w - n)`.
@@ -2414,7 +2414,7 @@ theorem shiftRight_sub_one_eq_shiftConcat (n : BitVec w) (hwn : 0 < wn) :
· simp [*]
· congr 1; omega
@[simp, bv_toNat]
@[simp, bitvec_to_nat]
theorem toNat_shiftConcat {x : BitVec w} {b : Bool} :
(x.shiftConcat b).toNat
= (x.toNat <<< 1 + b.toNat) % 2 ^ w := by
@@ -2428,7 +2428,7 @@ theorem toNat_shiftConcat_eq_of_lt {x : BitVec w} {b : Bool} {k : Nat}
simp only [toNat_shiftConcat, Nat.shiftLeft_eq, Nat.pow_one]
have : 2 ^ k < 2 ^ w := Nat.pow_lt_pow_of_lt (by omega) (by omega)
have : 2 ^ k * 2 2 ^ w := (Nat.pow_lt_pow_iff_pow_mul_le_pow (by omega)).mp this
rw [Nat.mod_eq_of_lt (by cases b <;> simp [bv_toNat] <;> omega)]
rw [Nat.mod_eq_of_lt (by cases b <;> simp [bitvec_to_nat] <;> omega)]
theorem toNat_shiftConcat_lt_of_lt {x : BitVec w} {b : Bool} {k : Nat}
(hk : k < w) (hx : x.toNat < 2 ^ k) :
@@ -2458,7 +2458,7 @@ theorem add_def {n} (x y : BitVec n) : x + y = .ofNat n (x.toNat + y.toNat) := r
/--
Definition of bitvector addition as a nat.
-/
@[simp, bv_toNat] theorem toNat_add (x y : BitVec w) : (x + y).toNat = (x.toNat + y.toNat) % 2^w := rfl
@[simp, bitvec_to_nat] theorem toNat_add (x y : BitVec w) : (x + y).toNat = (x.toNat + y.toNat) % 2^w := rfl
@[simp] theorem toFin_add (x y : BitVec w) : (x + y).toFin = toFin x + toFin y := rfl
@[simp] theorem ofFin_add (x : Fin (2^n)) (y : BitVec n) :
.ofFin x + y = .ofFin (x + y.toFin) := rfl
@@ -2490,9 +2490,9 @@ instance : Std.LawfulIdentity (α := BitVec n) (· + ·) 0#n where
theorem setWidth_add (x y : BitVec w) (h : i w) :
(x + y).setWidth i = x.setWidth i + y.setWidth i := by
have dvd : 2^i 2^w := Nat.pow_dvd_pow _ h
simp [bv_toNat, h, Nat.mod_mod_of_dvd _ dvd]
simp [bitvec_to_nat, h, Nat.mod_mod_of_dvd _ dvd]
@[simp, bv_toNat] theorem toInt_add (x y : BitVec w) :
@[simp, bitvec_to_nat] theorem toInt_add (x y : BitVec w) :
(x + y).toInt = (x.toInt + y.toInt).bmod (2^w) := by
simp [toInt_eq_toNat_bmod]
@@ -2522,14 +2522,14 @@ theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toN
@[simp] theorem toNat_sub {n} (x y : BitVec n) :
(x - y).toNat = (((2^n - y.toNat) + x.toNat) % 2^n) := rfl
@[simp, bv_toNat] theorem toInt_sub {x y : BitVec w} :
@[simp, bitvec_to_nat] theorem toInt_sub {x y : BitVec w} :
(x - y).toInt = (x.toInt - y.toInt).bmod (2 ^ w) := by
simp [toInt_eq_toNat_bmod, @Int.ofNat_sub y.toNat (2 ^ w) (by omega)]
-- We prefer this lemma to `toNat_sub` for the `bv_toNat` simp set.
-- We prefer this lemma to `toNat_sub` for the `bitvec_to_nat` simp set.
-- For reasons we don't yet understand, unfolding via `toNat_sub` sometimes
-- results in `omega` generating proof terms that are very slow in the kernel.
@[bv_toNat] theorem toNat_sub' {n} (x y : BitVec n) :
@[bitvec_to_nat] theorem toNat_sub' {n} (x y : BitVec n) :
(x - y).toNat = ((x.toNat + (2^n - y.toNat)) % 2^n) := by
rw [toNat_sub, Nat.add_comm]
@@ -2557,7 +2557,7 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y =
· simp
· exact Nat.le_of_lt x.isLt
@[simp, bv_toNat] theorem toNat_neg (x : BitVec n) : (- x).toNat = (2^n - x.toNat) % 2^n := by
@[simp, bitvec_to_nat] theorem toNat_neg (x : BitVec n) : (- x).toNat = (2^n - x.toNat) % 2^n := by
simp [Neg.neg, BitVec.neg]
theorem toNat_neg_of_pos {x : BitVec n} (h : 0#n < x) :
@@ -2622,7 +2622,7 @@ theorem neg_eq_not_add (x : BitVec w) : -x = ~~~x + 1#w := by
theorem neg_neg {x : BitVec w} : - - x = x := by
by_cases h : x = 0#w
· simp [h]
· simp [bv_toNat, h]
· simp [bitvec_to_nat, h]
@[simp]
protected theorem neg_inj {x y : BitVec w} : -x = -y x = y :=
@@ -2765,7 +2765,7 @@ theorem fill_false {w : Nat} : fill w false = 0#w := by
theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl
@[simp, bv_toNat] theorem toNat_mul (x y : BitVec n) : (x * y).toNat = (x.toNat * y.toNat) % 2 ^ n := rfl
@[simp, bitvec_to_nat] theorem toNat_mul (x y : BitVec n) : (x * y).toNat = (x.toNat * y.toNat) % 2 ^ n := rfl
@[simp] theorem toFin_mul (x y : BitVec n) : (x * y).toFin = (x.toFin * y.toFin) := rfl
protected theorem mul_comm (x y : BitVec w) : x * y = y * x := by
@@ -2813,7 +2813,7 @@ theorem mul_two {x : BitVec w} : x * 2#w = x + x := by
theorem two_mul {x : BitVec w} : 2#w * x = x + x := by rw [BitVec.mul_comm, mul_two]
@[simp, bv_toNat] theorem toInt_mul (x y : BitVec w) :
@[simp, bitvec_to_nat] theorem toInt_mul (x y : BitVec w) :
(x * y).toInt = (x.toInt * y.toInt).bmod (2^w) := by
simp [toInt_eq_toNat_bmod]
@@ -2840,7 +2840,7 @@ protected theorem neg_mul_comm (x y : BitVec w) : -x * y = x * -y := by simp
/-! ### le and lt -/
@[bv_toNat] theorem le_def {x y : BitVec n} :
@[bitvec_to_nat] theorem le_def {x y : BitVec n} :
x y x.toNat y.toNat := Iff.rfl
@[simp] theorem le_ofFin {x : BitVec n} {y : Fin (2^n)} :
@@ -2850,7 +2850,7 @@ protected theorem neg_mul_comm (x y : BitVec w) : -x * y = x * -y := by simp
@[simp] theorem ofNat_le_ofNat {n} {x y : Nat} : (BitVec.ofNat n x) (BitVec.ofNat n y) x % 2^n y % 2^n := by
simp [le_def]
@[bv_toNat] theorem lt_def {x y : BitVec n} :
@[bitvec_to_nat] theorem lt_def {x y : BitVec n} :
x < y x.toNat < y.toNat := Iff.rfl
@[simp] theorem lt_ofFin {x : BitVec n} {y : Fin (2^n)} :
@@ -2947,19 +2947,19 @@ theorem allOnes_le_iff {x : BitVec w} : allOnes w ≤ x ↔ x = allOnes w := by
theorem udiv_def {x y : BitVec n} : x / y = BitVec.ofNat n (x.toNat / y.toNat) := by
have h : x.toNat / y.toNat < 2 ^ n := Nat.lt_of_le_of_lt (Nat.div_le_self ..) (by omega)
rw [ udiv_eq]
simp [udiv, bv_toNat, h, Nat.mod_eq_of_lt]
simp [udiv, bitvec_to_nat, h, Nat.mod_eq_of_lt]
@[simp]
theorem toFin_udiv {x y : BitVec n} : (x / y).toFin = x.toFin / y.toFin := by
rfl
@[simp, bv_toNat]
@[simp, bitvec_to_nat]
theorem toNat_udiv {x y : BitVec n} : (x / y).toNat = x.toNat / y.toNat := by
rfl
@[simp]
theorem zero_udiv {x : BitVec w} : (0#w) / x = 0#w := by
simp [bv_toNat]
simp [bitvec_to_nat]
@[simp]
theorem udiv_zero {x : BitVec n} : x / 0#n = 0#n := by
@@ -3036,9 +3036,9 @@ theorem umod_def {x y : BitVec n} :
x % y = BitVec.ofNat n (x.toNat % y.toNat) := by
rw [ umod_eq]
have h : x.toNat % y.toNat < 2 ^ n := Nat.lt_of_le_of_lt (Nat.mod_le _ _) x.isLt
simp [umod, bv_toNat, Nat.mod_eq_of_lt h]
simp [umod, bitvec_to_nat, Nat.mod_eq_of_lt h]
@[simp, bv_toNat]
@[simp, bitvec_to_nat]
theorem toNat_umod {x y : BitVec n} :
(x % y).toNat = x.toNat % y.toNat := rfl
@@ -3052,7 +3052,7 @@ theorem umod_zero {x : BitVec n} : x % 0#n = x := by
@[simp]
theorem zero_umod {x : BitVec w} : (0#w) % x = 0#w := by
simp [bv_toNat]
simp [bitvec_to_nat]
@[simp]
theorem umod_one {x : BitVec w} : x % (1#w) = 0#w := by
@@ -3063,7 +3063,7 @@ theorem umod_one {x : BitVec w} : x % (1#w) = 0#w := by
@[simp]
theorem umod_self {x : BitVec w} : x % x = 0#w := by
simp [bv_toNat]
simp [bitvec_to_nat]
@[simp]
theorem umod_eq_and {x y : BitVec 1} : x % y = x &&& (~~~y) := by
@@ -3142,7 +3142,7 @@ theorem sdiv_eq (x y : BitVec w) : x.sdiv y =
rw [BitVec.sdiv]
rcases x.msb <;> rcases y.msb <;> simp
@[bv_toNat]
@[bitvec_to_nat]
theorem toNat_sdiv {x y : BitVec w} : (x.sdiv y).toNat =
match x.msb, y.msb with
| false, false => (udiv x y).toNat
@@ -3228,7 +3228,7 @@ theorem smod_eq (x y : BitVec w) : x.smod y =
rw [BitVec.smod]
rcases x.msb <;> rcases y.msb <;> simp
@[bv_toNat]
@[bitvec_to_nat]
theorem toNat_smod {x y : BitVec w} : (x.smod y).toNat =
match x.msb, y.msb with
| false, false => (x.umod y).toNat
@@ -3584,7 +3584,7 @@ theorem toNat_rotateRight {x : BitVec w} {r : Nat} :
theorem twoPow_eq (w : Nat) (i : Nat) : twoPow w i = 1#w <<< i := by
dsimp [twoPow]
@[simp, bv_toNat]
@[simp, bitvec_to_nat]
theorem toNat_twoPow (w : Nat) (i : Nat) : (twoPow w i).toNat = 2^i % 2^w := by
rcases w with rfl | w
· simp [Nat.mod_one, toNat_of_zero_length]
@@ -3680,7 +3680,7 @@ when `k` is less than the bitwidth `w`.
-/
theorem udiv_twoPow_eq_of_lt {w : Nat} {x : BitVec w} {k : Nat} (hk : k < w) : x / (twoPow w k) = x >>> k := by
have : 2^k < 2^w := Nat.pow_lt_pow_of_lt (by decide) hk
simp [bv_toNat, Nat.shiftRight_eq_div_pow, Nat.mod_eq_of_lt this]
simp [bitvec_to_nat, Nat.shiftRight_eq_div_pow, Nat.mod_eq_of_lt this]
/- ### cons -/
@@ -3807,7 +3807,7 @@ theorem replicate_succ' {x : BitVec w} :
def intMin (w : Nat) := twoPow w (w - 1)
theorem getLsbD_intMin (w : Nat) : (intMin w).getLsbD i = decide (i + 1 = w) := by
simp only [intMin, getLsbD_twoPow, boolToPropSimps]
simp only [intMin, getLsbD_twoPow, bool_to_prop]
omega
theorem getMsbD_intMin {w i : Nat} :
@@ -3821,7 +3821,7 @@ theorem getMsbD_intMin {w i : Nat} :
/--
The RHS is zero in case `w = 0` which is modeled by wrapping the expression in `... % 2 ^ w`.
-/
@[simp, bv_toNat]
@[simp, bitvec_to_nat]
theorem toNat_intMin : (intMin w).toNat = 2 ^ (w - 1) % 2 ^ w := by
simp [intMin]
@@ -3858,13 +3858,13 @@ theorem intMin_sle (x : BitVec w) : (intMin w).sle x := by
@[simp]
theorem neg_intMin {w : Nat} : -intMin w = intMin w := by
by_cases h : 0 < w
· simp [bv_toNat, h]
· simp [bitvec_to_nat, h]
· simp only [Nat.not_lt, Nat.le_zero_eq] at h
simp [bv_toNat, h]
simp [bitvec_to_nat, h]
@[simp]
theorem abs_intMin {w : Nat} : (intMin w).abs = intMin w := by
simp [BitVec.abs, bv_toNat]
simp [BitVec.abs, bitvec_to_nat]
theorem toInt_neg_of_ne_intMin {x : BitVec w} (rs : x intMin w) :
(-x).toInt = -(x.toInt) := by
@@ -3896,7 +3896,7 @@ theorem msb_intMin {w : Nat} : (intMin w).msb = decide (0 < w) := by
/-- The bitvector of width `w` that has the largest value when interpreted as an integer. -/
def intMax (w : Nat) := (twoPow w (w - 1)) - 1
@[simp, bv_toNat]
@[simp, bitvec_to_nat]
theorem toNat_intMax : (intMax w).toNat = 2 ^ (w - 1) - 1 := by
simp only [intMax]
by_cases h : w = 0
@@ -3999,7 +3999,7 @@ theorem msb_eq_toNat {x : BitVec w}:
theorem abs_eq (x : BitVec w) : x.abs = if x.msb then -x else x := by rfl
@[simp, bv_toNat]
@[simp, bitvec_to_nat]
theorem toNat_abs {x : BitVec w} : x.abs.toNat = if x.msb then 2^w - x.toNat else x.toNat := by
simp only [BitVec.abs, neg_eq]
by_cases h : x.msb = true

View File

@@ -370,14 +370,14 @@ theorem and_or_inj_left_iff :
/-- convert a `Bool` to a `Nat`, `false -> 0`, `true -> 1` -/
def toNat (b : Bool) : Nat := cond b 1 0
@[simp, bv_toNat] theorem toNat_false : false.toNat = 0 := rfl
@[simp, bitvec_to_nat] theorem toNat_false : false.toNat = 0 := rfl
@[simp, bv_toNat] theorem toNat_true : true.toNat = 1 := rfl
@[simp, bitvec_to_nat] theorem toNat_true : true.toNat = 1 := rfl
theorem toNat_le (c : Bool) : c.toNat 1 := by
cases c <;> trivial
@[bv_toNat]
@[bitvec_to_nat]
theorem toNat_lt (b : Bool) : b.toNat < 2 :=
Nat.lt_succ_of_le (toNat_le _)
@@ -580,17 +580,17 @@ protected theorem decide_coe (b : Bool) [Decidable (b = true)] : decide (b = tru
decide (p q) = (decide p == decide q) := by
cases dp with | _ p => simp [p]
@[boolToPropSimps]
@[bool_to_prop]
theorem and_eq_decide (p q : Prop) [dpq : Decidable (p q)] [dp : Decidable p] [dq : Decidable q] :
(p && q) = decide (p q) := by
cases dp with | _ p => simp [p]
@[boolToPropSimps]
@[bool_to_prop]
theorem or_eq_decide (p q : Prop) [dpq : Decidable (p q)] [dp : Decidable p] [dq : Decidable q] :
(p || q) = decide (p q) := by
cases dp with | _ p => simp [p]
@[boolToPropSimps]
@[bool_to_prop]
theorem decide_beq_decide (p q : Prop) [dpq : Decidable (p q)] [dp : Decidable p] [dq : Decidable q] :
(decide p == decide q) = decide (p q) := by
cases dp with | _ p => simp [p]

View File

@@ -14,3 +14,4 @@ import Init.Data.Int.LemmasAux
import Init.Data.Int.Order
import Init.Data.Int.Pow
import Init.Data.Int.Cooper
import Init.Data.Int.Linear

View File

@@ -225,7 +225,7 @@ attribute [local simp] subNatNat_self
@[local simp] protected theorem add_right_neg (a : Int) : a + -a = 0 := by
rw [Int.add_comm, Int.add_left_neg]
@[simp] protected theorem neg_eq_of_add_eq_zero {a b : Int} (h : a + b = 0) : -a = b := by
protected theorem neg_eq_of_add_eq_zero {a b : Int} (h : a + b = 0) : -a = b := by
rw [ Int.add_zero (-a), h, Int.add_assoc, Int.add_left_neg, Int.zero_add]
protected theorem eq_neg_of_eq_neg {a b : Int} (h : a = -b) : b = -a := by
@@ -328,24 +328,20 @@ theorem toNat_sub (m n : Nat) : toNat (m - n) = m - n := by
/- ## add/sub injectivity -/
@[simp]
protected theorem add_left_inj {i j : Int} (k : Int) : (i + k = j + k) i = j := by
apply Iff.intro
· intro p
rw [Int.add_sub_cancel i k, Int.add_sub_cancel j k, p]
· exact congrArg (· + k)
@[simp]
protected theorem add_right_inj {i j : Int} (k : Int) : (k + i = k + j) i = j := by
simp [Int.add_comm k]
simp [Int.add_comm k, Int.add_left_inj]
@[simp]
protected theorem sub_right_inj {i j : Int} (k : Int) : (k - i = k - j) i = j := by
simp [Int.sub_eq_add_neg, Int.neg_inj]
simp [Int.sub_eq_add_neg, Int.neg_inj, Int.add_right_inj]
@[simp]
protected theorem sub_left_inj {i j : Int} (k : Int) : (i - k = j - k) i = j := by
simp [Int.sub_eq_add_neg]
simp [Int.sub_eq_add_neg, Int.add_left_inj]
/- ## Ring properties -/

View File

@@ -0,0 +1,545 @@
/-
Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.ByCases
import Init.Data.Prod
import Init.Data.Int.Lemmas
import Init.Data.Int.LemmasAux
import Init.Data.Int.DivModLemmas
import Init.Data.RArray
namespace Int.Linear
/-! Helper definitions and theorems for constructing linear arithmetic proofs. -/
abbrev Var := Nat
abbrev Context := Lean.RArray Int
def Var.denote (ctx : Context) (v : Var) : Int :=
ctx.get v
inductive Expr where
| num (v : Int)
| var (i : Var)
| add (a b : Expr)
| sub (a b : Expr)
| neg (a : Expr)
| mulL (k : Int) (a : Expr)
| mulR (a : Expr) (k : Int)
deriving Inhabited, BEq
def Expr.denote (ctx : Context) : Expr Int
| .add a b => Int.add (denote ctx a) (denote ctx b)
| .sub a b => Int.sub (denote ctx a) (denote ctx b)
| .neg a => Int.neg (denote ctx a)
| .num k => k
| .var v => v.denote ctx
| .mulL k e => Int.mul k (denote ctx e)
| .mulR e k => Int.mul (denote ctx e) k
inductive Poly where
| num (k : Int)
| add (k : Int) (v : Var) (p : Poly)
deriving BEq
def Poly.denote (ctx : Context) (p : Poly) : Int :=
match p with
| .num k => k
| .add k v p => Int.add (Int.mul k (v.denote ctx)) (denote ctx p)
def Poly.addConst (p : Poly) (k : Int) : Poly :=
match p with
| .num k' => .num (k+k')
| .add k' v' p => .add k' v' (addConst p k)
def Poly.insert (k : Int) (v : Var) (p : Poly) : Poly :=
match p with
| .num k' => .add k v (.num k')
| .add k' v' p =>
bif Nat.blt v v' then
.add k v <| .add k' v' p
else bif Nat.beq v v' then
if Int.add k k' == 0 then
p
else
.add (Int.add k k') v' p
else
.add k' v' (insert k v p)
def Poly.norm (p : Poly) : Poly :=
match p with
| .num k => .num k
| .add k v p => (norm p).insert k v
def Expr.toPoly' (e : Expr) :=
go 1 e (.num 0)
where
go (coeff : Int) : Expr (Poly Poly)
| .num k => bif k == 0 then id else (Poly.addConst · (Int.mul coeff k))
| .var v => (.add coeff v ·)
| .add a b => go coeff a go coeff b
| .sub a b => go coeff a go (-coeff) b
| .mulL k a
| .mulR a k => bif k == 0 then id else go (Int.mul coeff k) a
| .neg a => go (-coeff) a
def Expr.toPoly (e : Expr) : Poly :=
e.toPoly'.norm
inductive PolyCnstr where
| eq (p : Poly)
| le (p : Poly)
deriving BEq
def PolyCnstr.denote (ctx : Context) : PolyCnstr Prop
| .eq p => p.denote ctx = 0
| .le p => p.denote ctx 0
def cdiv (a b : Int) : Int :=
-((-a)/b)
def cmod (a b : Int) : Int :=
-((-a)%b)
theorem cdiv_add_cmod (a b : Int) : b*(cdiv a b) + cmod a b = a := by
unfold cdiv cmod
have := Int.ediv_add_emod (-a) b
have := congrArg (Neg.neg) this
simp at this
conv => rhs; rw[ this]
rw [Int.neg_add, Int.neg_mul, Int.neg_mul_comm]
theorem cmod_gt_of_pos (a : Int) {b : Int} (h : 0 < b) : cmod a b > -b :=
Int.neg_lt_neg (Int.emod_lt_of_pos (-a) h)
theorem cmod_nonpos (a : Int) {b : Int} (h : b 0) : cmod a b 0 := by
have := Int.neg_le_neg (Int.emod_nonneg (-a) h)
simp at this
assumption
theorem cmod_eq_zero_iff_emod_eq_zero (a b : Int) : cmod a b = 0 a%b = 0 := by
unfold cmod
have := @Int.emod_eq_emod_iff_emod_sub_eq_zero b b a
simp at this
simp [Int.neg_emod, this, Eq.comm]
theorem cdiv_eq_div_of_divides {a b : Int} (h : (a/b)*b = a) : a/b = cdiv a b := by
have hz : a % b = 0 := by
have := Int.ediv_add_emod a b
conv at this => rhs; rw [ Int.add_zero a]
rw [Int.mul_comm, h] at this
exact Int.add_left_cancel this
have hcz : cmod a b = 0 := cmod_eq_zero_iff_emod_eq_zero a b |>.mpr hz
have : (cdiv a b)*b = a := by
have := cdiv_add_cmod a b
simp [hcz] at this
rw [Int.mul_comm] at this
assumption
have : (a/b)*b = (cdiv a b)*b := Eq.trans h this.symm
by_cases h : b = 0
next => simp[cdiv, h]
next => rw [Int.mul_eq_mul_right_iff h] at this; assumption
def Poly.div (k : Int) : Poly Poly
| .num k' => .num (cdiv k' k)
| .add k' x p => .add (k'/k) x (div k p)
def Poly.divAll (k : Int) : Poly Bool
| .num k' => (k'/k)*k == k'
| .add k' _ p => (k'/k)*k == k' && divAll k p
def Poly.divCoeffs (k : Int) : Poly Bool
| .num _ => true
| .add k' _ p => (k'/k)*k == k' && divCoeffs k p
def Poly.getConst : Poly Int
| .num k => k
| .add _ _ p => getConst p
def PolyCnstr.norm : PolyCnstr PolyCnstr
| .eq p => .eq p.norm
| .le p => .le p.norm
def PolyCnstr.divAll (k : Int) : PolyCnstr Bool
| .eq p | .le p => p.divAll k
def PolyCnstr.divCoeffs (k : Int) : PolyCnstr Bool
| .eq p | .le p => p.divCoeffs k
def PolyCnstr.isLe : PolyCnstr Bool
| .eq _ => false
| .le _ => true
def PolyCnstr.div (k : Int) : PolyCnstr PolyCnstr
| .eq p => .eq <| p.div k
| .le p => .le <| p.div k
inductive ExprCnstr where
| eq (p₁ p₂ : Expr)
| le (p₁ p₂ : Expr)
deriving Inhabited, BEq
def ExprCnstr.isLe : ExprCnstr Bool
| .eq .. => false
| .le .. => true
def ExprCnstr.denote (ctx : Context) : ExprCnstr Prop
| .eq e₁ e₂ => e₁.denote ctx = e₂.denote ctx
| .le e₁ e₂ => e₁.denote ctx e₂.denote ctx
def ExprCnstr.toPoly : ExprCnstr PolyCnstr
| .eq e₁ e₂ => .eq (e₁.sub e₂).toPoly.norm
| .le e₁ e₂ => .le (e₁.sub e₂).toPoly.norm
-- Certificate for normalizing the coefficients of a constraint
def divBy (e e' : ExprCnstr) (k : Int) : Bool :=
k > 0 && e.toPoly.divAll k && e'.toPoly == e.toPoly.div k
attribute [local simp] Int.add_comm Int.add_assoc Int.add_left_comm Int.add_mul Int.mul_add
attribute [local simp] Poly.insert Poly.denote Poly.norm Poly.addConst
theorem Poly.denote_addConst (ctx : Context) (p : Poly) (k : Int) : (p.addConst k).denote ctx = p.denote ctx + k := by
induction p <;> simp [*]
attribute [local simp] Poly.denote_addConst
theorem Poly.denote_insert (ctx : Context) (k : Int) (v : Var) (p : Poly) :
(p.insert k v).denote ctx = p.denote ctx + k * v.denote ctx := by
induction p <;> simp [*]
next k' v' p' ih =>
by_cases h₁ : Nat.blt v v' <;> simp [*]
by_cases h₂ : Nat.beq v v' <;> simp [*]
by_cases h₃ : k + k' = 0 <;> simp [*, Nat.eq_of_beq_eq_true h₂]
rw [ Int.add_mul]
simp [*]
attribute [local simp] Poly.denote_insert
theorem Poly.denote_norm (ctx : Context) (p : Poly) : p.norm.denote ctx = p.denote ctx := by
induction p <;> simp [*]
attribute [local simp] Poly.denote_norm
private theorem sub_fold (a b : Int) : a.sub b = a - b := rfl
private theorem neg_fold (a : Int) : a.neg = -a := rfl
attribute [local simp] sub_fold neg_fold
attribute [local simp] Poly.div Poly.divAll PolyCnstr.denote
theorem Poly.denote_div_eq_of_divAll (ctx : Context) (p : Poly) (k : Int) : p.divAll k (p.div k).denote ctx * k = p.denote ctx := by
induction p with
| num _ => simp; intro h; rw [ cdiv_eq_div_of_divides h]; assumption
| add k' v p ih =>
simp; intro h₁ h₂
have ih := ih h₂
simp [ih]
apply congrArg (denote ctx p + ·)
rw [Int.mul_right_comm, h₁]
attribute [local simp] Poly.divCoeffs Poly.getConst
theorem Poly.denote_div_eq_of_divCoeffs (ctx : Context) (p : Poly) (k : Int) : p.divCoeffs k (p.div k).denote ctx * k + cmod p.getConst k = p.denote ctx := by
induction p with
| num k' => simp; rw [Int.mul_comm, cdiv_add_cmod]
| add k' v p ih =>
simp; intro h₁ h₂
rw [ ih h₂]
rw [Int.mul_right_comm, h₁, Int.add_assoc]
attribute [local simp] ExprCnstr.denote ExprCnstr.toPoly Expr.denote
theorem Expr.denote_toPoly'_go (ctx : Context) (e : Expr) :
(toPoly'.go k e p).denote ctx = k * e.denote ctx + p.denote ctx := by
induction k, e using Expr.toPoly'.go.induct generalizing p with
| case1 k k' =>
simp only [toPoly'.go]
by_cases h : k' == 0
· simp [h, eq_of_beq h]
· simp [h, Var.denote]
| case2 k i => simp [toPoly'.go]
| case3 k a b iha ihb => simp [toPoly'.go, iha, ihb]
| case4 k a b iha ihb =>
simp [toPoly'.go, iha, ihb, Int.mul_sub]
rw [Int.sub_eq_add_neg, Int.neg_mul, Int.add_assoc]
| case5 k k' a ih
| case6 k a k' ih =>
simp only [toPoly'.go]
by_cases h : k' == 0
· simp [h, eq_of_beq h]
· simp [h, cond_false, Int.mul_assoc]
simp at ih
rw [ih]
rw [Int.mul_assoc, Int.mul_comm k']
| case7 k a ih => simp [toPoly'.go, ih]
theorem Expr.denote_toPoly (ctx : Context) (e : Expr) : e.toPoly.denote ctx = e.denote ctx := by
simp [toPoly, toPoly', Expr.denote_toPoly'_go]
attribute [local simp] Expr.denote_toPoly PolyCnstr.denote
theorem ExprCnstr.denote_toPoly (ctx : Context) (c : ExprCnstr) : c.toPoly.denote ctx = c.denote ctx := by
cases c <;> simp
· rw [Int.sub_eq_zero]
· constructor
· exact Int.le_of_sub_nonpos
· exact Int.sub_nonpos_of_le
instance : LawfulBEq Poly where
eq_of_beq {a} := by
induction a <;> intro b <;> cases b <;> simp_all! [BEq.beq]
· rename_i k₁ v₁ p₁ k₂ v₂ p₂ ih
intro _ _ h
exact ih h
rfl := by
intro a
induction a <;> simp! [BEq.beq]
· rename_i k v p ih
exact ih
instance : LawfulBEq PolyCnstr where
eq_of_beq {a b} := by
cases a <;> cases b <;> rename_i p₁ p₂ <;> simp_all! [BEq.beq]
· show (p₁ == p₂) = true _
simp
· show (p₁ == p₂) = true _
simp
rfl {a} := by
cases a <;> rename_i p <;> show (p == p) = true
<;> simp
theorem Expr.eq_of_toPoly_eq (ctx : Context) (e e' : Expr) (h : e.toPoly == e'.toPoly) : e.denote ctx = e'.denote ctx := by
have h := congrArg (Poly.denote ctx) (eq_of_beq h)
simp [Poly.norm] at h
assumption
theorem ExprCnstr.eq_of_toPoly_eq (ctx : Context) (c c' : ExprCnstr) (h : c.toPoly == c'.toPoly) : c.denote ctx = c'.denote ctx := by
have h := congrArg (PolyCnstr.denote ctx) (eq_of_beq h)
rw [denote_toPoly, denote_toPoly] at h
assumption
theorem ExprCnstr.eq_of_toPoly_eq_var (ctx : Context) (x y : Var) (c : ExprCnstr) (h : c.toPoly == .eq (.add 1 x (.add (-1) y (.num 0))))
: c.denote ctx = (x.denote ctx = y.denote ctx) := by
have h := congrArg (PolyCnstr.denote ctx) (eq_of_beq h)
rw [denote_toPoly] at h
rw [h]; simp
rw [ Int.sub_eq_add_neg, Int.sub_eq_zero]
theorem ExprCnstr.eq_of_toPoly_eq_const (ctx : Context) (x : Var) (k : Int) (c : ExprCnstr) (h : c.toPoly == .eq (.add 1 x (.num (-k))))
: c.denote ctx = (x.denote ctx = k) := by
have h := congrArg (PolyCnstr.denote ctx) (eq_of_beq h)
rw [denote_toPoly] at h
rw [h]; simp
rw [Int.add_comm, Int.sub_eq_add_neg, Int.sub_eq_zero]
private theorem mul_eq_zero_iff_eq_zero (a b : Int) : b 0 (a * b = 0 a = 0) := by
intro h
constructor
· intro h'
cases Int.mul_eq_zero.mp h'
· assumption
· contradiction
· intro; simp [*]
private theorem eq_mul_le_zero {a b : Int} : 0 < b (a 0 a * b 0) := by
intro h
have : 0 = 0 * b := by simp
constructor
· intro h'
rw [this]
apply Int.mul_le_mul h' <;> try simp
apply Int.le_of_lt h
· intro h'
rw [this] at h'
exact Int.le_of_mul_le_mul_right h' h
attribute [local simp] PolyCnstr.divAll PolyCnstr.div
theorem ExprCnstr.eq_of_toPoly_eq_of_divBy' (ctx : Context) (e e' : ExprCnstr) (p : PolyCnstr) (k : Int) : k > 0 p.divAll k e.toPoly = p e'.toPoly = p.div k e.denote ctx = e'.denote ctx := by
intro h₀ h₁ h₂ h₃
have hz : k 0 := Int.ne_of_gt h₀
cases p <;> simp at h₁
next p =>
replace h₁ := Poly.denote_div_eq_of_divAll ctx p k h₁
replace h₂ := congrArg (PolyCnstr.denote ctx) h₂
simp only [PolyCnstr.denote.eq_1, h₁] at h₂
replace h₃ := congrArg (PolyCnstr.denote ctx) h₃
simp only [PolyCnstr.denote.eq_1, PolyCnstr.div] at h₃
rw [mul_eq_zero_iff_eq_zero _ _ hz] at h₂
have := Eq.trans h₂ h₃.symm
rw [denote_toPoly, denote_toPoly] at this
exact this
next p =>
-- TODO: this is correct but we can simplify `p ≤ 0` if `p.divCoeffs k` and `p.getConst % k > 0`. Here, we are simplifying only the case `p.getConst % k = 0`
replace h₁ := Poly.denote_div_eq_of_divAll ctx p k h₁
replace h₂ := congrArg (PolyCnstr.denote ctx) h₂
simp only [PolyCnstr.denote.eq_2, h₁] at h₂
replace h₃ := congrArg (PolyCnstr.denote ctx) h₃
simp only [PolyCnstr.denote.eq_2, PolyCnstr.div] at h₃
rw [eq_mul_le_zero h₀] at h₃
have := Eq.trans h₂ h₃.symm
rw [denote_toPoly, denote_toPoly] at this
exact this
theorem ExprCnstr.eq_of_divBy (ctx : Context) (e e' : ExprCnstr) (k : Int) : divBy e e' k e.denote ctx = e'.denote ctx := by
intro h
simp only [divBy, Bool.and_eq_true, bne_iff_ne, ne_eq, beq_iff_eq, decide_eq_true_eq] at h
have h₁, h₂, h₃ := h
exact ExprCnstr.eq_of_toPoly_eq_of_divBy' ctx e e' e.toPoly k h₁ h₂ rfl h₃
private theorem mul_add_cmod_le_iff {a k b : Int} (h : k > 0) : a*k + cmod b k 0 a 0 := by
constructor
· intro h'
have h₁ : a*k -cmod b k := by
have := Int.le_sub_right_of_add_le h'
simp at this
assumption
have h₂ : -cmod b k < k := by
have := cmod_gt_of_pos b h
have := Int.neg_lt_neg this
simp at this
assumption
have h₃ : a*k < k := Int.lt_of_le_of_lt h₁ h₂
have h₄ : a < 1 := by
conv at h₃ => rhs; rw [ Int.one_mul k]
have := Int.lt_of_mul_lt_mul_right h₃ (Int.le_of_lt h)
assumption
exact Int.le_of_lt_add_one (h₄ : a < 0 + 1)
· intro h'
have : a * k 0 := Int.mul_nonpos_of_nonpos_of_nonneg h' (Int.le_of_lt h)
have := Int.add_le_add this (cmod_nonpos b (Int.ne_of_gt h))
simp at this
assumption
theorem ExprCnstr.eq_of_toPoly_eq_of_divCoeffs (ctx : Context) (e e' : ExprCnstr) (p : PolyCnstr) (k : Int) : k > 0 p.divCoeffs k p.isLe e.toPoly = p e'.toPoly = p.div k e.denote ctx = e'.denote ctx := by
intro h₀ h₁ h₂ h₃ h₄
have hz : k 0 := Int.ne_of_gt h₀
cases p <;> simp [PolyCnstr.isLe] at h₂
clear h₂
next p =>
simp [PolyCnstr.divCoeffs] at h₁
replace h₁ := Poly.denote_div_eq_of_divCoeffs ctx p k h₁
replace h₃ := congrArg (PolyCnstr.denote ctx) h₃
simp only [PolyCnstr.denote.eq_2, h₁] at h₃
replace h₄ := congrArg (PolyCnstr.denote ctx) h₄
simp only [PolyCnstr.denote.eq_2, PolyCnstr.div] at h₄
rw [denote_toPoly] at h₃ h₄
rw [h₃, h₄]
apply propext
apply mul_add_cmod_le_iff
exact h₀
-- Certificate for normalizing the coefficients of inequality constraint with bound tightening
def divByLe (e e' : ExprCnstr) (k : Int) : Bool :=
k > 0 && e.isLe && e.toPoly.divCoeffs k && e'.toPoly == e.toPoly.div k
theorem ExprCnstr.eq_of_divByLe (ctx : Context) (e e' : ExprCnstr) (k : Int) : divByLe e e' k e.denote ctx = e'.denote ctx := by
intro h
simp only [divByLe, Bool.and_eq_true, bne_iff_ne, ne_eq, beq_iff_eq, decide_eq_true_eq] at h
have h₀, h₁, h₂, h₃ := h
have hle : e.toPoly.isLe := by
cases e <;> simp [ExprCnstr.isLe] at h₁
simp [PolyCnstr.isLe]
apply ExprCnstr.eq_of_toPoly_eq_of_divCoeffs ctx e e' e.toPoly k h₀ h₂ hle rfl h₃
def PolyCnstr.isUnsat : PolyCnstr Bool
| .eq (.num k) => k != 0
| .eq _ => false
| .le (.num k) => k > 0
| .le _ => false
theorem PolyCnstr.eq_false_of_isUnsat (ctx : Context) (p : PolyCnstr) : p.isUnsat p.denote ctx = False := by
unfold isUnsat <;> split <;> simp <;> try contradiction
apply Int.not_le_of_gt
theorem ExprCnstr.eq_false_of_isUnsat (ctx : Context) (c : ExprCnstr) (h : c.toPoly.isUnsat) : c.denote ctx = False := by
have := PolyCnstr.eq_false_of_isUnsat ctx (c.toPoly) h
rw [ExprCnstr.denote_toPoly] at this
assumption
def PolyCnstr.isUnsatCoeff (k : Int) : PolyCnstr Bool
| .eq p => p.divCoeffs k && k > 0 && cmod p.getConst k < 0
| .le _ => false
private theorem contra_old {a b k : Int} (h₀ : 0 < k) (h₁ : 0 < b) (h₂ : b < k) (h₃ : a*k + b = 0) : False := by
have : b = -a*k := by
rw [ Int.neg_eq_of_add_eq_zero h₃, Int.neg_mul]
rw [this] at h₁ h₂
conv at h₂ => rhs; rw [ Int.one_mul k]
have high := Int.lt_of_mul_lt_mul_right h₂ (Int.le_of_lt h₀)
rw [ Int.zero_mul k] at h₁
have low := Int.lt_of_mul_lt_mul_right h₁ (Int.le_of_lt h₀)
replace low : 1 -a := low
have : (1 : Int) < 1 := Int.lt_of_le_of_lt low high
contradiction
private theorem contra {a b k : Int} (h₀ : 0 < k) (h₁ : -k < b) (h₂ : b < 0) (h₃ : a*k + b = 0) : False := by
have : b = -a*k := by
rw [ Int.neg_eq_of_add_eq_zero h₃, Int.neg_mul]
rw [this, Int.neg_mul] at h₁ h₂
replace h₁ := Int.lt_of_neg_lt_neg h₁
replace h₂ : -(a*k) < -0 := h₂
replace h₂ := Int.lt_of_neg_lt_neg h₂
replace h₁ : a * k < 1 * k := by simp [h₁]
replace h₁ : a < 1 := Int.lt_of_mul_lt_mul_right h₁ (Int.le_of_lt h₀)
replace h₂ : 0 * k < a * k := by simp [h₂]
replace h₂ : 0 < a := Int.lt_of_mul_lt_mul_right h₂ (Int.le_of_lt h₀)
replace h₂ : 1 a := h₂
have : (1 : Int) < 1 := Int.lt_of_le_of_lt h₂ h₁
contradiction
private theorem PolyCnstr.eq_false (ctx : Context) (p : Poly) (k : Int) : p.divCoeffs k k > 0 cmod p.getConst k < 0 (PolyCnstr.eq p).denote ctx = False := by
simp
intro h₁ h₂ h₃ h
have hnz : k 0 := by intro h; rw [h] at h₂; contradiction
have := Poly.denote_div_eq_of_divCoeffs ctx p k h₁
rw [h] at this
have low := cmod_gt_of_pos p.getConst h₂
have high := h₃
exact contra h₂ low high this
theorem ExprCnstr.eq_false_of_isUnsat_coeff (ctx : Context) (c : ExprCnstr) (k : Int) : c.toPoly.isUnsatCoeff k c.denote ctx = False := by
intro h
cases c <;> simp [toPoly, PolyCnstr.isUnsatCoeff] at h
next e₁ e₂ =>
have h₁, h₂, h₃ := h
have := PolyCnstr.eq_false ctx _ _ h₁ h₂ h₃
simp at this
simp
intro he
simp [he] at this
def PolyCnstr.isValid : PolyCnstr Bool
| .eq (.num k) => k == 0
| .eq _ => false
| .le (.num k) => k 0
| .le _ => false
theorem PolyCnstr.eq_true_of_isValid (ctx : Context) (p : PolyCnstr) : p.isValid p.denote ctx = True := by
unfold isValid <;> split <;> simp
theorem ExprCnstr.eq_true_of_isValid (ctx : Context) (c : ExprCnstr) (h : c.toPoly.isValid) : c.denote ctx = True := by
have := PolyCnstr.eq_true_of_isValid ctx (c.toPoly) h
rw [ExprCnstr.denote_toPoly] at this
assumption
end Int.Linear
theorem Int.not_le_eq (a b : Int) : (¬a b) = (b + 1 a) := by
apply propext; constructor
· intro h; have h := Int.add_one_le_of_lt (Int.lt_of_not_ge h); assumption
· intro h; apply Int.not_le_of_gt; exact h
theorem Int.not_ge_eq (a b : Int) : (¬a b) = (a + 1 b) := by
apply Int.not_le_eq
theorem Int.not_lt_eq (a b : Int) : (¬a < b) = (b a) := by
apply propext; constructor
· intro h; simp [Int.not_lt] at h; assumption
· intro h; apply Int.not_le_of_gt; simp [Int.lt_add_one_iff, *]
theorem Int.not_gt_eq (a b : Int) : (¬a > b) = (a b) := by
apply Int.not_lt_eq

View File

@@ -6,6 +6,7 @@ Authors: Mario Carneiro
prelude
import Init.Data.List.Count
import Init.Data.Subtype
import Init.BinderNameHint
namespace List
@@ -416,7 +417,12 @@ theorem attachWith_map {l : List α} (f : α → β) {P : β → Prop} {H : ∀
fun x, h => f x, h := by
induction l <;> simp [*]
theorem map_attachWith {l : List α} {P : α Prop} {H : (a : α), a l P a}
@[simp] theorem map_attachWith {l : List α} {P : α Prop} {H : (a : α), a l P a}
(f : { x // P x } β) :
(l.attachWith P H).map f = l.attach.map fun x, h => f x, H _ h := by
induction l <;> simp_all
theorem map_attachWith_eq_pmap {l : List α} {P : α Prop} {H : (a : α), a l P a}
(f : { x // P x } β) :
(l.attachWith P H).map f =
l.pmap (fun a (h : a l P a) => f a, H _ h.1) (fun a h => h, H a h) := by
@@ -428,7 +434,7 @@ theorem map_attachWith {l : List α} {P : α → Prop} {H : ∀ (a : α), a ∈
simp
/-- See also `pmap_eq_map_attach` for writing `pmap` in terms of `map` and `attach`. -/
theorem map_attach {l : List α} (f : { x // x l } β) :
theorem map_attach_eq_pmap {l : List α} (f : { x // x l } β) :
l.attach.map f = l.pmap (fun a h => f a, h) (fun _ => id) := by
induction l with
| nil => rfl
@@ -437,6 +443,9 @@ theorem map_attach {l : List α} (f : { x // x ∈ l } → β) :
apply pmap_congr_left
simp
@[deprecated map_attach_eq_pmap (since := "2025-02-09")]
abbrev map_attach := @map_attach_eq_pmap
theorem attach_filterMap {l : List α} {f : α Option β} :
(l.filterMap f).attach = l.attach.filterMap
fun x, h => (f x).pbind (fun b m => some b, mem_filterMap.mpr x, h, m) := by
@@ -788,4 +797,66 @@ and simplifies these to the function directly taking the value.
(List.replicate n x).unattach = List.replicate n x.1 := by
simp [unattach, -map_subtype]
/-! ### Well-founded recursion preprocessing setup -/
@[wf_preprocess] theorem map_wfParam (xs : List α) (f : α β) :
(wfParam xs).map f = xs.attach.unattach.map f := by
simp [wfParam]
@[wf_preprocess] theorem map_unattach (P : α Prop) (xs : List (Subtype P)) (f : α β) :
xs.unattach.map f = xs.map fun x, h =>
binderNameHint x f <| binderNameHint h () <| f (wfParam x) := by
simp [wfParam]
@[wf_preprocess] theorem foldl_wfParam (xs : List α) (f : β α β) (x : β) :
(wfParam xs).foldl f x = xs.attach.unattach.foldl f x := by
simp [wfParam]
@[wf_preprocess] theorem foldl_unattach (P : α Prop) (xs : List (Subtype P)) (f : β α β) (x : β):
xs.unattach.foldl f x = xs.foldl (fun s x, h =>
binderNameHint s f <| binderNameHint x (f s) <| binderNameHint h () <| f s (wfParam x)) x := by
simp [wfParam]
@[wf_preprocess] theorem foldr_wfParam (xs : List α) (f : α β β) (x : β) :
(wfParam xs).foldr f x = xs.attach.unattach.foldr f x := by
simp [wfParam]
@[wf_preprocess] theorem foldr_unattach (P : α Prop) (xs : List (Subtype P)) (f : α β β) (x : β):
xs.unattach.foldr f x = xs.foldr (fun x, h s =>
binderNameHint x f <| binderNameHint s (f x) <| binderNameHint h () <| f (wfParam x) s) x := by
simp [wfParam]
@[wf_preprocess] theorem filter_wfParam (xs : List α) (f : α Bool) :
(wfParam xs).filter f = xs.attach.unattach.filter f:= by
simp [wfParam]
@[wf_preprocess] theorem filter_unattach (P : α Prop) (xs : List (Subtype P)) (f : α Bool) :
xs.unattach.filter f = (xs.filter (fun x, h =>
binderNameHint x f <| binderNameHint h () <| f (wfParam x))).unattach := by
simp [wfParam]
@[wf_preprocess] theorem reverse_wfParam (xs : List α) :
(wfParam xs).reverse = xs.attach.unattach.reverse := by simp [wfParam]
@[wf_preprocess] theorem reverse_unattach (P : α Prop) (xs : List (Subtype P)) :
xs.unattach.reverse = xs.reverse.unattach := by simp
@[wf_preprocess] theorem filterMap_wfParam (xs : List α) (f : α Option β) :
(wfParam xs).filterMap f = xs.attach.unattach.filterMap f := by
simp [wfParam]
@[wf_preprocess] theorem filterMap_unattach (P : α Prop) (xs : List (Subtype P)) (f : α Option β) :
xs.unattach.filterMap f = xs.filterMap fun x, h =>
binderNameHint x f <| binderNameHint h () <| f (wfParam x) := by
simp [wfParam]
@[wf_preprocess] theorem flatMap_wfParam (xs : List α) (f : α List β) :
(wfParam xs).flatMap f = xs.attach.unattach.flatMap f := by
simp [wfParam]
@[wf_preprocess] theorem flatMap_unattach (P : α Prop) (xs : List (Subtype P)) (f : α List β) :
xs.unattach.flatMap f = xs.flatMap fun x, h =>
binderNameHint x f <| binderNameHint h () <| f (wfParam x) := by
simp [wfParam]
end List

View File

@@ -225,10 +225,23 @@ def lex [BEq α] (l₁ l₂ : List α) (lt : αα → Bool := by exact (·
| _, [] => false
| a :: as, b :: bs => lt a b || (a == b && lex as bs lt)
@[simp] theorem lex_nil_nil [BEq α] : lex ([] : List α) [] lt = false := rfl
@[simp] theorem lex_nil_cons [BEq α] {b} {bs : List α} : lex [] (b :: bs) lt = true := rfl
@[simp] theorem lex_cons_nil [BEq α] {a} {as : List α} : lex (a :: as) [] lt = false := rfl
@[simp] theorem lex_cons_cons [BEq α] {a b} {as bs : List α} :
theorem nil_lex_nil [BEq α] : lex ([] : List α) [] lt = false := rfl
@[simp] theorem nil_lex_cons [BEq α] {b} {bs : List α} : lex [] (b :: bs) lt = true := rfl
theorem cons_lex_nil [BEq α] {a} {as : List α} : lex (a :: as) [] lt = false := rfl
@[simp] theorem cons_lex_cons [BEq α] {a b} {as bs : List α} :
lex (a :: as) (b :: bs) lt = (lt a b || (a == b && lex as bs lt)) := rfl
@[simp] theorem lex_nil [BEq α] {as : List α} : lex as [] lt = false := by
cases as <;> simp [nil_lex_nil, cons_lex_nil]
@[deprecated nil_lex_nil (since := "2025-02-10")]
theorem lex_nil_nil [BEq α] : lex ([] : List α) [] lt = false := rfl
@[deprecated nil_lex_cons (since := "2025-02-10")]
theorem lex_nil_cons [BEq α] {b} {bs : List α} : lex [] (b :: bs) lt = true := rfl
@[deprecated cons_lex_nil (since := "2025-02-10")]
theorem lex_cons_nil [BEq α] {a} {as : List α} : lex (a :: as) [] lt = false := rfl
@[deprecated cons_lex_cons (since := "2025-02-10")]
theorem lex_cons_cons [BEq α] {a b} {as bs : List α} :
lex (a :: as) (b :: bs) lt = (lt a b || (a == b && lex as bs lt)) := rfl
/-! ## Alternative getters -/

View File

@@ -178,15 +178,15 @@ theorem get_last {as : List α} {i : Fin (length (as ++ [a]))} (h : ¬ i.1 < as.
induction as generalizing i with
| nil => cases i with
| zero => simp [List.get]
| succ => simp_arith at h'
| succ => simp +arith at h'
| cons a as ih =>
cases i with simp at h
| succ i => apply ih; simp [h]
theorem sizeOf_lt_of_mem [SizeOf α] {as : List α} (h : a as) : sizeOf a < sizeOf as := by
induction h with
| head => simp_arith
| tail _ _ ih => exact Nat.lt_trans ih (by simp_arith)
| head => simp +arith
| tail _ _ ih => exact Nat.lt_trans ih (by simp +arith)
/-- This tactic, added to the `decreasing_trivial` toolbox, proves that
`sizeOf a < sizeOf as` when `a ∈ as`, which is useful for well founded recursions
@@ -197,7 +197,7 @@ macro "sizeOf_list_dec" : tactic =>
| with_reducible
apply Nat.lt_of_lt_of_le (sizeOf_lt_of_mem ?h)
case' h => assumption
simp_arith)
simp +arith)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| sizeOf_list_dec)
@@ -211,8 +211,8 @@ theorem append_cancel_left {as bs cs : List α} (h : as ++ bs = as ++ cs) : bs =
theorem append_cancel_right {as bs cs : List α} (h : as ++ bs = cs ++ bs) : as = cs := by
match as, cs with
| [], [] => rfl
| [], c::cs => have aux := congrArg length h; simp_arith at aux
| a::as, [] => have aux := congrArg length h; simp_arith at aux
| [], c::cs => have aux := congrArg length h; simp +arith at aux
| a::as, [] => have aux := congrArg length h; simp +arith at aux
| a::as, c::cs => injection h with h₁ h₂; subst h₁; rw [append_cancel_right h₂]
@[simp] theorem append_cancel_left_eq (as bs cs : List α) : (as ++ bs = as ++ cs) = (bs = cs) := by
@@ -227,11 +227,11 @@ theorem append_cancel_right {as bs cs : List α} (h : as ++ bs = cs ++ bs) : as
theorem sizeOf_get [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as := by
match as, i with
| a::as, 0, _ => simp_arith [get]
| a::as, 0, _ => simp +arith [get]
| a::as, i+1, h =>
have ih := sizeOf_get as i, Nat.le_of_succ_le_succ h
apply Nat.lt_trans ih
simp_arith
simp +arith
theorem not_lex_antisymm [DecidableEq α] {r : α α Prop} [DecidableRel r]
(antisymm : x y : α, ¬ r x y ¬ r y x x = y)

View File

@@ -161,7 +161,7 @@ foldlM f x₀ [a, b, c] = do
```
-/
@[specialize]
protected def foldlM {m : Type u Type v} [Monad m] {s : Type u} {α : Type w} : (f : s α m s) (init : s) List α m s
def foldlM {m : Type u Type v} [Monad m] {s : Type u} {α : Type w} : (f : s α m s) (init : s) List α m s
| _, s, [] => pure s
| f, s, a :: as => do
let s' f s a

View File

@@ -1344,6 +1344,11 @@ theorem head_filter_of_pos {p : α → Bool} {l : List α} (w : l ≠ []) (h : p
theorem filterMap_eq_map (f : α β) : filterMap (some f) = map f := by
funext l; induction l <;> simp [*, filterMap_cons]
/-- Variant of `filterMap_eq_map` with `some ∘ f` expanded out to a lambda. -/
@[simp]
theorem filterMap_eq_map' (f : α β) : filterMap (fun x => some (f x)) = map f :=
filterMap_eq_map f
@[simp] theorem filterMap_some_fun : filterMap (some : α Option α) = id := by
funext l
erw [filterMap_eq_map]
@@ -1558,7 +1563,7 @@ theorem getElem_append_right' (l₁ : List α) {l₂ : List α} {i : Nat} (hi :
rw [getElem_append_right] <;> simp [*, le_add_left]
theorem getElem_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = i) :
l[i]'(eq h by simp_arith) = a := Option.some.inj <| by
l[i]'(eq h by simp +arith) = a := Option.some.inj <| by
rw [ getElem?_eq_getElem, eq, getElem?_append_right (h Nat.le_refl _), h]
simp
@@ -2516,12 +2521,35 @@ theorem foldr_eq_foldrM (f : α → β → β) (b) (l : List α) :
/-! ### foldl and foldr -/
@[simp] theorem foldr_cons_eq_append (l : List α) : l.foldr cons l' = l ++ l' := by
@[simp] theorem foldr_cons_eq_append (l : List α) (f : α β) (l' : List β) :
l.foldr (fun x y => f x :: y) l' = l.map f ++ l' := by
induction l <;> simp [*]
/-- Variant of `foldr_cons_eq_append` specalized to `f = id`. -/
@[simp] theorem foldr_cons_eq_append' (l l' : List β) :
l.foldr cons l' = l ++ l' := by
induction l <;> simp [*]
@[deprecated foldr_cons_eq_append (since := "2024-08-22")] abbrev foldr_self_append := @foldr_cons_eq_append
@[simp] theorem foldl_flip_cons_eq_append (l : List α) : l.foldl (fun x y => y :: x) l' = l.reverse ++ l' := by
@[simp] theorem foldl_flip_cons_eq_append (l : List α) (f : α β) (l' : List β) :
l.foldl (fun x y => f y :: x) l' = (l.map f).reverse ++ l' := by
induction l generalizing l' <;> simp [*]
@[simp] theorem foldr_append_eq_append (l : List α) (f : α List β) (l' : List β) :
l.foldr (f · ++ ·) l' = (l.map f).flatten ++ l' := by
induction l <;> simp [*]
@[simp] theorem foldl_append_eq_append (l : List α) (f : α List β) (l' : List β) :
l.foldl (· ++ f ·) l' = l' ++ (l.map f).flatten := by
induction l generalizing l'<;> simp [*]
@[simp] theorem foldr_flip_append_eq_append (l : List α) (f : α List β) (l' : List β) :
l.foldr (fun x y => y ++ f x) l' = l' ++ (l.map f).reverse.flatten := by
induction l generalizing l' <;> simp [*]
@[simp] theorem foldl_flip_append_eq_append (l : List α) (f : α List β) (l' : List β) :
l.foldl (fun x y => f y ++ x) l' = (l.map f).reverse.flatten ++ l' := by
induction l generalizing l' <;> simp [*]
theorem foldr_cons_nil (l : List α) : l.foldr cons [] = l := by simp

View File

@@ -48,7 +48,9 @@ instance ltIrrefl [LT α] [Std.Irrefl (· < · : αα → Prop)] : Std.Irre
@[simp] theorem le_nil [LT α] (l : List α) : l [] l = [] := not_nil_lex_iff
@[simp] theorem nil_lex_cons : Lex r [] (a :: l) := Lex.nil
-- This is named with a prime to avoid conflict with `lex [] (b :: bs) lt = true`.
-- Better naming for the `Lex` vs `lex` distinction would be welcome.
@[simp] theorem nil_lex_cons' : Lex r [] (a :: l) := Lex.nil
@[simp] theorem nil_lt_cons [LT α] (a : α) (l : List α) : [] < a :: l := Lex.nil
@@ -333,7 +335,7 @@ theorem lex_eq_true_iff_exists [BEq α] (lt : αα → Bool) :
cases l₂ with
| nil => simp [lex]
| cons b l₂ =>
simp [lex_cons_cons, Bool.or_eq_true, Bool.and_eq_true, ih, isEqv, length_cons]
simp [cons_lex_cons, Bool.or_eq_true, Bool.and_eq_true, ih, isEqv, length_cons]
constructor
· rintro (hab | hab, h₁, h₂ | i, h₁, h₂, w₁, w₂)
· exact .inr 0, by simp [hab]
@@ -397,7 +399,7 @@ theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : αα
cases l₂ with
| nil => simp [lex]
| cons b l₂ =>
simp [lex_cons_cons, Bool.or_eq_false_iff, Bool.and_eq_false_imp, ih, isEqv,
simp [cons_lex_cons, Bool.or_eq_false_iff, Bool.and_eq_false_imp, ih, isEqv,
Bool.and_eq_true, length_cons]
constructor
· rintro hab, h

View File

@@ -11,7 +11,7 @@ import Init.Data.List.Attach
# Lemmas about `List.mapM` and `List.forM`.
-/
-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
namespace List
@@ -425,11 +425,21 @@ and simplifies these to the function directly taking the value.
| nil => simp
| cons a l ih => simp [ih, hf]
@[wf_preprocess] theorem foldlM_wfParam [Monad m] (xs : List α) (f : β α m β) :
(wfParam xs).foldlM f = xs.attach.unattach.foldlM f := by
simp [wfParam]
@[wf_preprocess] theorem foldlM_unattach [Monad m] (P : α Prop) (xs : List (Subtype P)) (f : β α m β) :
xs.unattach.foldlM f = xs.foldlM fun b x, h =>
binderNameHint b f <| binderNameHint x (f b) <| binderNameHint h () <|
f b (wfParam x) := by
simp [wfParam]
/--
This lemma identifies monadic folds over lists of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
-/
@[simp] theorem foldrM_subtype [Monad m] [LawfulMonad m]{p : α Prop} {l : List { x // p x }}
@[simp] theorem foldrM_subtype [Monad m] [LawfulMonad m] {p : α Prop} {l : List { x // p x }}
{f : { x // p x } β m β} {g : α β m β} {x : β}
(hf : x h b, f x, h b = g x b) :
l.foldrM f x = l.unattach.foldrM g x := by
@@ -442,6 +452,16 @@ and simplifies these to the function directly taking the value.
funext b
simp [hf]
@[wf_preprocess] theorem foldrM_wfParam [Monad m] [LawfulMonad m] (xs : List α) (f : α β m β) :
(wfParam xs).foldrM f = xs.attach.unattach.foldrM f := by
simp [wfParam]
@[wf_preprocess] theorem foldrM_unattach [Monad m] [LawfulMonad m] (P : α Prop) (xs : List (Subtype P)) (f : α β m β) :
xs.unattach.foldrM f = xs.foldrM fun x, h b =>
binderNameHint x f <| binderNameHint h () <| binderNameHint b (f x) <|
f (wfParam x) b := by
simp [wfParam]
/--
This lemma identifies monadic maps over lists of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
@@ -455,6 +475,15 @@ and simplifies these to the function directly taking the value.
| nil => simp
| cons a l ih => simp [ih, hf]
@[wf_preprocess] theorem mapM_wfParam [Monad m] [LawfulMonad m] (xs : List α) (f : α m β) :
(wfParam xs).mapM f = xs.attach.unattach.mapM f := by
simp [wfParam]
@[wf_preprocess] theorem mapM_unattach [Monad m] [LawfulMonad m] (P : α Prop) (xs : List (Subtype P)) (f : α m β) :
xs.unattach.mapM f = xs.mapM fun x, h =>
binderNameHint x f <| binderNameHint h () <| f (wfParam x) := by
simp [wfParam]
@[simp] theorem filterMapM_subtype [Monad m] [LawfulMonad m] {p : α Prop} {l : List { x // p x }}
{f : { x // p x } m (Option β)} {g : α m (Option β)} (hf : x h, f x, h = g x) :
l.filterMapM f = l.unattach.filterMapM g := by
@@ -463,6 +492,17 @@ and simplifies these to the function directly taking the value.
| nil => simp
| cons a l ih => simp [ih, hf, filterMapM_cons]
@[wf_preprocess] theorem filterMapM_wfParam [Monad m] [LawfulMonad m]
(xs : List α) (f : α m (Option β)) :
(wfParam xs).filterMapM f = xs.attach.unattach.filterMapM f := by
simp [wfParam]
@[wf_preprocess] theorem filterMapM_unattach [Monad m] [LawfulMonad m]
(P : α Prop) (xs : List (Subtype P)) (f : α m (Option β)) :
xs.unattach.filterMapM f = xs.filterMapM fun x, h =>
binderNameHint x f <| binderNameHint h () <| f (wfParam x) := by
simp [wfParam]
@[simp] theorem flatMapM_subtype [Monad m] [LawfulMonad m] {p : α Prop} {l : List { x // p x }}
{f : { x // p x } m (List β)} {g : α m (List β)} (hf : x h, f x, h = g x) :
(l.flatMapM f) = l.unattach.flatMapM g := by
@@ -471,4 +511,15 @@ and simplifies these to the function directly taking the value.
| nil => simp
| cons a l ih => simp [ih, hf]
@[wf_preprocess] theorem flatMapM_wfParam [Monad m] [LawfulMonad m]
(xs : List α) (f : α m (List β)) :
(wfParam xs).flatMapM f = xs.attach.unattach.flatMapM f := by
simp [wfParam]
@[wf_preprocess] theorem flatMapM_unattach [Monad m] [LawfulMonad m]
(P : α Prop) (xs : List (Subtype P)) (f : α m (List β)) :
xs.unattach.flatMapM f = xs.flatMapM fun x, h =>
binderNameHint x f <| binderNameHint h () <| f (wfParam x) := by
simp [wfParam]
end List

View File

@@ -11,7 +11,7 @@ import Init.Data.Nat.Div.Basic
-/
set_option linter.missingDocs true -- keep it documented
-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
open Decidable List

View File

@@ -11,7 +11,7 @@ import Init.Data.Fin.Fold
# Theorems about `List.ofFn`
-/
-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
namespace List

View File

@@ -11,7 +11,7 @@ import Init.Data.List.Attach
# Lemmas about `List.Pairwise` and `List.Nodup`.
-/
-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
namespace List

View File

@@ -18,7 +18,7 @@ another.
The notation `~` is used for permutation equivalence.
-/
-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
open Nat

View File

@@ -14,7 +14,7 @@ Most of the results are deferred to `Data.Init.List.Nat.Range`, where more resul
natural arithmetic are available.
-/
-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
namespace List

View File

@@ -152,8 +152,8 @@ theorem cons_merge_cons (s : αα → Bool) (a b l r) :
| a::l, b::r =>
rw [cons_merge_cons]
split
· simp_arith [length_merge s l (b::r)]
· simp_arith [length_merge s (a::l) r]
· simp +arith [length_merge s l (b::r)]
· simp +arith [length_merge s (a::l) r]
/--
The elements of `merge le xs ys` are exactly the elements of `xs` and `ys`.

View File

@@ -11,7 +11,7 @@ import Init.Data.List.TakeDrop
# Lemmas about `List.Subset`, `List.Sublist`, `List.IsPrefix`, `List.IsSuffix`, and `List.IsInfix`.
-/
-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
namespace List

View File

@@ -10,7 +10,7 @@ import Init.Data.List.Lemmas
# Lemmas about `List.take` and `List.drop`.
-/
-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
namespace List

View File

@@ -15,7 +15,7 @@ import Init.Data.Array.Lex.Basic
We prefer to pull `List.toArray` outwards past `Array` operations.
-/
-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
namespace Array

View File

@@ -6,7 +6,7 @@ Authors: Henrik Böving
prelude
import Init.Data.List.Basic
-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
/--

View File

@@ -11,7 +11,7 @@ import Init.Data.Function
# Lemmas about `List.zip`, `List.zipWith`, `List.zipWithAll`, and `List.unzip`.
-/
-- set_option linter.listName true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
namespace List

View File

@@ -1011,7 +1011,7 @@ theorem mul_add_div {m : Nat} (m_pos : m > 0) (x y : Nat) : (m * x + y) / m = x
| 0 => simp
| x + 1 =>
rw [Nat.mul_succ, Nat.add_assoc _ m, mul_add_div m_pos x (m+y), div_eq]
simp_arith [m_pos]; rw [Nat.add_comm, Nat.add_sub_cancel]
simp +arith [m_pos]; rw [Nat.add_comm, Nat.add_sub_cancel]
theorem mul_add_mod (m x y : Nat) : (m * x + y) % m = y % m := by
match x with

View File

@@ -35,11 +35,11 @@ inductive Expr where
deriving Inhabited
def Expr.denote (ctx : Context) : Expr Nat
| Expr.add a b => Nat.add (denote ctx a) (denote ctx b)
| Expr.num k => k
| Expr.var v => v.denote ctx
| Expr.mulL k e => Nat.mul k (denote ctx e)
| Expr.mulR e k => Nat.mul (denote ctx e) k
| .add a b => Nat.add (denote ctx a) (denote ctx b)
| .num k => k
| .var v => v.denote ctx
| .mulL k e => Nat.mul k (denote ctx e)
| .mulR e k => Nat.mul (denote ctx e) k
abbrev Poly := List (Nat × Var)
@@ -66,18 +66,6 @@ where
| [] => r
| (k, v) :: p => go p (r.insert k v)
def Poly.mul (k : Nat) (p : Poly) : Poly :=
bif k == 0 then
[]
else bif k == 1 then
p
else
go p
where
go : Poly Poly
| [] => []
| (k', v) :: p => (Nat.mul k k', v) :: go p
def Poly.cancelAux (fuel : Nat) (m₁ m₂ r₁ r₂ : Poly) : Poly × Poly :=
match fuel with
| 0 => (r₁.reverse ++ m₁, r₂.reverse ++ m₂)
@@ -122,41 +110,23 @@ def Poly.denote_eq (ctx : Context) (mp : Poly × Poly) : Prop := mp.1.denote ctx
def Poly.denote_le (ctx : Context) (mp : Poly × Poly) : Prop := mp.1.denote ctx mp.2.denote ctx
def Poly.combineAux (fuel : Nat) (p₁ p₂ : Poly) : Poly :=
match fuel with
| 0 => p₁ ++ p₂
| fuel + 1 =>
match p₁, p₂ with
| p₁, [] => p₁
| [], p₂ => p₂
| (k₁, v₁) :: p₁, (k₂, v₂) :: p₂ =>
bif Nat.blt v₁ v₂ then
(k₁, v₁) :: combineAux fuel p₁ ((k₂, v₂) :: p₂)
else bif Nat.blt v₂ v₁ then
(k₂, v₂) :: combineAux fuel ((k₁, v₁) :: p₁) p₂
else
(Nat.add k₁ k₂, v₁) :: combineAux fuel p₁ p₂
def Poly.combine (p₁ p₂ : Poly) : Poly :=
combineAux hugeFuel p₁ p₂
def Expr.toPoly (e : Expr) :=
go 1 e []
where
-- Implementation note: This assembles the result using difference lists
-- to avoid `++` on lists.
go (coeff : Nat) : Expr (Poly Poly)
| Expr.num k => bif k == 0 then id else ((coeff * k, fixedVar) :: ·)
| Expr.var i => ((coeff, i) :: ·)
| Expr.add a b => go coeff a go coeff b
| Expr.mulL k a
| Expr.mulR a k => bif k == 0 then id else go (coeff * k) a
| .num k => bif k == 0 then id else ((coeff * k, fixedVar) :: ·)
| .var i => ((coeff, i) :: ·)
| .add a b => go coeff a go coeff b
| .mulL k a
| .mulR a k => bif k == 0 then id else go (coeff * k) a
def Expr.toNormPoly (e : Expr) : Poly :=
e.toPoly.norm
def Expr.inc (e : Expr) : Expr :=
Expr.add e (Expr.num 1)
.add e (.num 1)
structure PolyCnstr where
eq : Bool
@@ -178,13 +148,6 @@ instance : LawfulBEq PolyCnstr where
show (eq == eq && (lhs == lhs && rhs == rhs)) = true
simp [LawfulBEq.rfl]
def PolyCnstr.mul (k : Nat) (c : PolyCnstr) : PolyCnstr :=
{ c with lhs := c.lhs.mul k, rhs := c.rhs.mul k }
def PolyCnstr.combine (c₁ c₂ : PolyCnstr) : PolyCnstr :=
let (lhs, rhs) := Poly.cancel (c₁.lhs.combine c₂.lhs) (c₁.rhs.combine c₂.rhs)
{ eq := c₁.eq && c₂.eq, lhs, rhs }
structure ExprCnstr where
eq : Bool
lhs : Expr
@@ -225,47 +188,29 @@ def ExprCnstr.toNormPoly (c : ExprCnstr) : PolyCnstr :=
let (lhs, rhs) := Poly.cancel c.lhs.toNormPoly c.rhs.toNormPoly
{ c with lhs, rhs }
abbrev Certificate := List (Nat × ExprCnstr)
def Certificate.combineHyps (c : PolyCnstr) (hs : Certificate) : PolyCnstr :=
match hs with
| [] => c
| (k, c') :: hs => combineHyps (PolyCnstr.combine c (c'.toNormPoly.mul (Nat.add k 1))) hs
def Certificate.combine (hs : Certificate) : PolyCnstr :=
match hs with
| [] => { eq := true, lhs := [], rhs := [] }
| (k, c) :: hs => combineHyps (c.toNormPoly.mul (Nat.add k 1)) hs
def Certificate.denote (ctx : Context) (c : Certificate) : Prop :=
match c with
| [] => False
| (_, c)::hs => c.denote ctx denote ctx hs
def monomialToExpr (k : Nat) (v : Var) : Expr :=
bif v == fixedVar then
Expr.num k
.num k
else bif k == 1 then
Expr.var v
.var v
else
Expr.mulL k (Expr.var v)
.mulL k (.var v)
def Poly.toExpr (p : Poly) : Expr :=
match p with
| [] => Expr.num 0
| [] => .num 0
| (k, v) :: p => go (monomialToExpr k v) p
where
go (e : Expr) (p : Poly) : Expr :=
match p with
| [] => e
| (k, v) :: p => go (Expr.add e (monomialToExpr k v)) p
| (k, v) :: p => go (.add e (monomialToExpr k v)) p
def PolyCnstr.toExpr (c : PolyCnstr) : ExprCnstr :=
{ c with lhs := c.lhs.toExpr, rhs := c.rhs.toExpr }
attribute [local simp] Nat.add_comm Nat.add_assoc Nat.add_left_comm Nat.right_distrib Nat.left_distrib Nat.mul_assoc Nat.mul_comm
attribute [local simp] Poly.denote Expr.denote Poly.insert Poly.norm Poly.norm.go Poly.cancelAux
attribute [local simp] Poly.mul Poly.mul.go
theorem Poly.denote_insert (ctx : Context) (k : Nat) (v : Var) (p : Poly) :
(p.insert k v).denote ctx = p.denote ctx + k * v.denote ctx := by
@@ -320,21 +265,11 @@ theorem Poly.denote_reverse (ctx : Context) (p : Poly) : denote ctx (List.revers
attribute [local simp] Poly.denote_reverse
theorem Poly.denote_mul (ctx : Context) (k : Nat) (p : Poly) : (p.mul k).denote ctx = k * p.denote ctx := by
simp
by_cases h : k == 0 <;> simp [h]; simp [eq_of_beq h]
by_cases h : k == 1 <;> simp [h]; simp [eq_of_beq h]
induction p with
| nil => simp
| cons kv m ih => cases kv with | _ k' v => simp [ih]
private theorem eq_of_not_blt_eq_true (h₁ : ¬ (Nat.blt x y = true)) (h₂ : ¬ (Nat.blt y x = true)) : x = y :=
have h₁ : ¬ x < y := fun h => h₁ (Nat.blt_eq.mpr h)
have h₂ : ¬ y < x := fun h => h₂ (Nat.blt_eq.mpr h)
Nat.le_antisymm (Nat.ge_of_not_lt h₂) (Nat.ge_of_not_lt h₁)
attribute [local simp] Poly.denote_mul
theorem Poly.denote_eq_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁ r₂ : Poly)
(h : denote_eq ctx (r₁.reverse ++ m₁, r₂.reverse ++ m₂)) : denote_eq ctx (cancelAux fuel m₁ m₂ r₁ r₂) := by
induction fuel generalizing m₁ m₂ r₁ r₂ with
@@ -493,21 +428,6 @@ theorem Poly.denote_le_cancel_eq (ctx : Context) (m₁ m₂ : Poly) : denote_le
attribute [local simp] Poly.denote_le_cancel_eq
theorem Poly.denote_combineAux (ctx : Context) (fuel : Nat) (p₁ p₂ : Poly) : (p₁.combineAux fuel p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
induction fuel generalizing p₁ p₂ with simp [combineAux]
| succ fuel ih =>
split <;> simp
rename_i k₁ v₁ p₁ k₂ v₂ p₂
by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv, ih]
by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv, ih]
have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv
simp [heqv]
theorem Poly.denote_combine (ctx : Context) (p₁ p₂ : Poly) : (p₁.combine p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
simp [combine, denote_combineAux]
attribute [local simp] Poly.denote_combine
theorem Expr.denote_toPoly_go (ctx : Context) (e : Expr) :
(toPoly.go k e p).denote ctx = k * e.denote ctx + p.denote ctx := by
induction k, e using Expr.toPoly.go.induct generalizing p with
@@ -572,51 +492,6 @@ theorem ExprCnstr.denote_toNormPoly (ctx : Context) (c : ExprCnstr) : c.toNormPo
attribute [local simp] ExprCnstr.denote_toNormPoly
theorem Poly.mul.go_denote (ctx : Context) (k : Nat) (p : Poly) : (Poly.mul.go k p).denote ctx = k * p.denote ctx := by
match p with
| [] => rfl
| (k', v) :: p => simp [Poly.mul.go, go_denote]
attribute [local simp] Poly.mul.go_denote
section
attribute [-simp] Nat.right_distrib Nat.left_distrib
theorem PolyCnstr.denote_mul (ctx : Context) (k : Nat) (c : PolyCnstr) : (c.mul (k+1)).denote ctx = c.denote ctx := by
cases c; rename_i eq lhs rhs
have : k 0 k + 1 1 := by intro h; match k with | 0 => contradiction | k+1 => simp [Nat.succ.injEq]
have : ¬ (k == 0) (k + 1 == 1) = false := fun h => beq_false_of_ne (this (ne_of_beq_false (Bool.of_not_eq_true h)))
have : ¬ ((k + 1 == 0) = true) := fun h => absurd (eq_of_beq h) (Nat.succ_ne_zero k)
by_cases he : eq = true <;> simp [he, PolyCnstr.mul, PolyCnstr.denote, Poly.denote_le, Poly.denote_eq]
<;> by_cases hk : k == 0 <;> (try simp [eq_of_beq hk]) <;> simp [*] <;> apply Iff.intro <;> intro h
· exact Nat.eq_of_mul_eq_mul_left (Nat.zero_lt_succ _) h
· rw [h]
· exact Nat.le_of_mul_le_mul_left h (Nat.zero_lt_succ _)
· apply Nat.mul_le_mul_left _ h
end
attribute [local simp] PolyCnstr.denote_mul
theorem PolyCnstr.denote_combine {ctx : Context} {c₁ c₂ : PolyCnstr} (h₁ : c₁.denote ctx) (h₂ : c₂.denote ctx) : (c₁.combine c₂).denote ctx := by
cases c₁; cases c₂; rename_i eq₁ lhs₁ rhs₁ eq₂ lhs₂ rhs₂
simp [denote] at h₁ h₂
simp [PolyCnstr.combine, denote]
by_cases he₁ : eq₁ = true <;> by_cases he₂ : eq₂ = true <;> simp [he₁, he₂] at h₁ h₂ |-
· rw [Poly.denote_eq_cancel_eq]; simp [Poly.denote_eq] at h₁ h₂ |-; simp [h₁, h₂]
· rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-; rw [h₁]; apply Nat.add_le_add_left h₂
· rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-; rw [h₂]; apply Nat.add_le_add_right h₁
· rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-; apply Nat.add_le_add h₁ h₂
attribute [local simp] PolyCnstr.denote_combine
theorem Poly.isNum?_eq_some (ctx : Context) {p : Poly} {k : Nat} : p.isNum? = some k p.denote ctx = k := by
simp [isNum?]
split
next => intro h; injection h
next k v => by_cases h : v == fixedVar <;> simp [h]; intros; simp [Var.denote, eq_of_beq h]; assumption
next => intros; contradiction
theorem Poly.of_isZero (ctx : Context) {p : Poly} (h : isZero p = true) : p.denote ctx = 0 := by
simp [isZero] at h
split at h
@@ -662,50 +537,6 @@ theorem ExprCnstr.eq_true_of_isValid (ctx : Context) (c : ExprCnstr) (h : c.toNo
simp [-eq_iff_iff] at this
assumption
theorem Certificate.of_combineHyps (ctx : Context) (c : PolyCnstr) (cs : Certificate) (h : (combineHyps c cs).denote ctx False) : c.denote ctx cs.denote ctx := by
match cs with
| [] => simp [combineHyps, denote] at *; exact h
| (k, c')::cs =>
intro h₁ h₂
have := PolyCnstr.denote_combine (ctx := ctx) (c₂ := PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c')) h₁
simp at this
have := this h₂
have ih := of_combineHyps ctx (PolyCnstr.combine c (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c'))) cs
exact ih h this
theorem Certificate.of_combine (ctx : Context) (cs : Certificate) (h : cs.combine.denote ctx False) : cs.denote ctx := by
match cs with
| [] => simp [combine, PolyCnstr.denote, Poly.denote_eq] at h
| (k, c)::cs =>
simp [denote, combine] at *
intro h'
apply of_combineHyps (h := h)
simp [h']
theorem Certificate.of_combine_isUnsat (ctx : Context) (cs : Certificate) (h : cs.combine.isUnsat) : cs.denote ctx :=
have h := PolyCnstr.eq_false_of_isUnsat ctx h
of_combine ctx cs (fun h' => Eq.mp h h')
theorem denote_monomialToExpr (ctx : Context) (k : Nat) (v : Var) : (monomialToExpr k v).denote ctx = k * v.denote ctx := by
simp [monomialToExpr]
by_cases h : v == fixedVar <;> simp [h, Expr.denote]
· simp [eq_of_beq h, Var.denote]
· by_cases h : k == 1 <;> simp [h, Expr.denote]; simp [eq_of_beq h]
attribute [local simp] denote_monomialToExpr
theorem Poly.denote_toExpr_go (ctx : Context) (e : Expr) (p : Poly) : (toExpr.go e p).denote ctx = e.denote ctx + p.denote ctx := by
induction p generalizing e with
| nil => simp [toExpr.go, Poly.denote]
| cons kv p ih => cases kv; simp [toExpr.go, ih, Expr.denote, Poly.denote]
attribute [local simp] Poly.denote_toExpr_go
theorem Poly.denote_toExpr (ctx : Context) (p : Poly) : p.toExpr.denote ctx = p.denote ctx := by
match p with
| [] => simp [toExpr, Expr.denote, Poly.denote]
| (k, v) :: p => simp [toExpr, Expr.denote, Poly.denote]
theorem ExprCnstr.eq_of_toNormPoly_eq (ctx : Context) (c d : ExprCnstr) (h : c.toNormPoly == d.toPoly) : c.denote ctx = d.denote ctx := by
have h := congrArg (PolyCnstr.denote ctx) (eq_of_beq h)
simp [-eq_iff_iff] at h

View File

@@ -9,7 +9,7 @@ import Init.Data.Nat.Linear
namespace Nat
theorem nextPowerOfTwo_dec {n power : Nat} (h₁ : power > 0) (h₂ : power < n) : n - power * 2 < n - power := by
have : power * 2 = power + power := by simp_arith
have : power * 2 = power + power := by simp +arith
rw [this, Nat.sub_add_eq]
exact Nat.sub_lt (Nat.zero_lt_sub_of_lt h₂) h₁

View File

@@ -134,16 +134,29 @@ theorem attachWith_map {o : Option α} (f : α → β) {P : β → Prop} {H :
fun x, h => f x, h := by
cases o <;> simp
theorem map_attach {o : Option α} (f : { x // x o } β) :
theorem map_attach_eq_pmap {o : Option α} (f : { x // x o } β) :
o.attach.map f = o.pmap (fun a (h : a o) => f a, h) (fun _ h => h) := by
cases o <;> simp
theorem map_attachWith {o : Option α} {P : α Prop} {H : (a : α), a o P a}
@[deprecated map_attach_eq_pmap (since := "2025-02-09")]
abbrev map_attach := @map_attach_eq_pmap
@[simp] theorem map_attachWith {l : Option α} {P : α Prop} {H : (a : α), a l P a}
(f : { x // P x } β) :
(l.attachWith P H).map f = l.attach.map fun x, h => f x, H _ h := by
cases l <;> simp_all
theorem map_attachWith_eq_pmap {o : Option α} {P : α Prop} {H : (a : α), a o P a}
(f : { x // P x } β) :
(o.attachWith P H).map f =
o.pmap (fun a (h : a o P a) => f a, h.2) (fun a h => h, H a h) := by
cases o <;> simp
@[simp]
theorem map_attach_eq_attachWith {o : Option α} {p : α Prop} (f : a, a o p a) :
o.attach.map (fun x => x.1, f x.1 x.2) = o.attachWith p f := by
cases o <;> simp_all [Function.comp_def]
theorem attach_bind {o : Option α} {f : α Option β} :
(o.bind f).attach =
o.attach.bind fun x, h => (f x).attach.map fun y, h' => y, mem_bind_iff.mpr x, h, h' := by

View File

@@ -375,6 +375,9 @@ end choice
@[simp] theorem some_or : (some a).or o = some a := rfl
@[simp] theorem none_or : none.or o = o := rfl
theorem or_eq_right_of_none {o o' : Option α} (h : o = none) : o.or o' = o' := by
cases h; simp
@[deprecated some_or (since := "2024-11-03")] theorem or_some : (some a).or o = some a := rfl
/-- This will be renamed to `or_some` once the existing deprecated lemma is removed. -/
@@ -403,6 +406,10 @@ instance : Std.Associative (or (α := α)) := ⟨@or_assoc _⟩
@[simp]
theorem or_none : or o none = o := by
cases o <;> rfl
theorem or_eq_left_of_none {o o' : Option α} (h : o' = none) : o.or o' = o := by
cases h; simp
instance : Std.LawfulIdentity (or (α := α)) none where
left_id := @none_or _
right_id := @or_none _

View File

@@ -59,4 +59,12 @@ namespace Option
o.toList.foldr f a = o.elim a (fun b => f b a) := by
cases o <;> simp
@[simp]
theorem pairwise_toList {P : α α Prop} {o : Option α} : o.toList.Pairwise P := by
cases o <;> simp
@[simp]
theorem head?_toList {o : Option α} : o.toList.head? = o := by
cases o <;> simp
end Option

View File

@@ -85,6 +85,8 @@ This function has the same behavior as `Int.toNat` for negative numbers.
If you want to obtain the 2's complement representation use `toBitVec`.
-/
@[inline] def Int8.toNat (i : Int8) : Nat := i.toInt.toNat
/-- Obtains the `Int8` whose 2's complement representation is the given `BitVec 8`. -/
@[inline] def Int8.ofBitVec (b : BitVec 8) : Int8 := b
@[extern "lean_int8_neg"]
def Int8.neg (i : Int8) : Int8 := -i.toBitVec
@@ -185,6 +187,8 @@ This function has the same behavior as `Int.toNat` for negative numbers.
If you want to obtain the 2's complement representation use `toBitVec`.
-/
@[inline] def Int16.toNat (i : Int16) : Nat := i.toInt.toNat
/-- Obtains the `Int16` whose 2's complement representation is the given `BitVec 16`. -/
@[inline] def Int16.ofBitVec (b : BitVec 16) : Int16 := b
@[extern "lean_int16_to_int8"]
def Int16.toInt8 (a : Int16) : Int8 := a.toBitVec.signExtend 8
@[extern "lean_int8_to_int16"]
@@ -289,6 +293,8 @@ This function has the same behavior as `Int.toNat` for negative numbers.
If you want to obtain the 2's complement representation use `toBitVec`.
-/
@[inline] def Int32.toNat (i : Int32) : Nat := i.toInt.toNat
/-- Obtains the `Int32` whose 2's complement representation is the given `BitVec 32`. -/
@[inline] def Int32.ofBitVec (b : BitVec 32) : Int32 := b
@[extern "lean_int32_to_int8"]
def Int32.toInt8 (a : Int32) : Int8 := a.toBitVec.signExtend 8
@[extern "lean_int32_to_int16"]
@@ -397,6 +403,8 @@ This function has the same behavior as `Int.toNat` for negative numbers.
If you want to obtain the 2's complement representation use `toBitVec`.
-/
@[inline] def Int64.toNat (i : Int64) : Nat := i.toInt.toNat
/-- Obtains the `Int64` whose 2's complement representation is the given `BitVec 64`. -/
@[inline] def Int64.ofBitVec (b : BitVec 64) : Int64 := b
@[extern "lean_int64_to_int8"]
def Int64.toInt8 (a : Int64) : Int8 := a.toBitVec.signExtend 8
@[extern "lean_int64_to_int16"]
@@ -509,6 +517,8 @@ This function has the same behavior as `Int.toNat` for negative numbers.
If you want to obtain the 2's complement representation use `toBitVec`.
-/
@[inline] def ISize.toNat (i : ISize) : Nat := i.toInt.toNat
/-- Obtains the `ISize` whose 2's complement representation is the given `BitVec`. -/
@[inline] def ISize.ofBitVec (b : BitVec System.Platform.numBits) : ISize := b
@[extern "lean_isize_to_int32"]
def ISize.toInt32 (a : ISize) : Int32 := a.toBitVec.signExtend 32
/--

View File

@@ -9,6 +9,10 @@ import Init.Data.BitVec.Basic
open Nat
@[deprecated UInt8.ofBitVec (since := "2025-02-12"), inherit_doc UInt8.ofBitVec]
def UInt8.mk (bitVec : BitVec 8) : UInt8 :=
UInt8.ofBitVec bitVec
@[extern "lean_uint8_add"]
def UInt8.add (a b : UInt8) : UInt8 := a.toBitVec + b.toBitVec
@[extern "lean_uint8_sub"]
@@ -72,6 +76,10 @@ instance (a b : UInt8) : Decidable (a ≤ b) := UInt8.decLe a b
instance : Max UInt8 := maxOfLe
instance : Min UInt8 := minOfLe
@[deprecated UInt16.ofBitVec (since := "2025-02-12"), inherit_doc UInt16.ofBitVec]
def UInt16.mk (bitVec : BitVec 16) : UInt16 :=
UInt16.ofBitVec bitVec
@[extern "lean_uint16_add"]
def UInt16.add (a b : UInt16) : UInt16 := a.toBitVec + b.toBitVec
@[extern "lean_uint16_sub"]
@@ -137,6 +145,10 @@ instance (a b : UInt16) : Decidable (a ≤ b) := UInt16.decLe a b
instance : Max UInt16 := maxOfLe
instance : Min UInt16 := minOfLe
@[deprecated UInt32.ofBitVec (since := "2025-02-12"), inherit_doc UInt32.ofBitVec]
def UInt32.mk (bitVec : BitVec 32) : UInt32 :=
UInt32.ofBitVec bitVec
@[extern "lean_uint32_add"]
def UInt32.add (a b : UInt32) : UInt32 := a.toBitVec + b.toBitVec
@[extern "lean_uint32_sub"]
@@ -187,6 +199,10 @@ instance : ShiftRight UInt32 := ⟨UInt32.shiftRight⟩
@[extern "lean_bool_to_uint32"]
def Bool.toUInt32 (b : Bool) : UInt32 := if b then 1 else 0
@[deprecated UInt64.ofBitVec (since := "2025-02-12"), inherit_doc UInt64.ofBitVec]
def UInt64.mk (bitVec : BitVec 64) : UInt64 :=
UInt64.ofBitVec bitVec
@[extern "lean_uint64_add"]
def UInt64.add (a b : UInt64) : UInt64 := a.toBitVec + b.toBitVec
@[extern "lean_uint64_sub"]
@@ -250,6 +266,10 @@ instance (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a b
instance : Max UInt64 := maxOfLe
instance : Min UInt64 := minOfLe
@[deprecated USize.ofBitVec (since := "2025-02-12"), inherit_doc USize.ofBitVec]
def USize.mk (bitVec : BitVec System.Platform.numBits) : USize :=
USize.ofBitVec bitVec
theorem usize_size_le : USize.size 18446744073709551616 := by
cases usize_size_eq <;> next h => rw [h]; decide

View File

@@ -22,7 +22,10 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
theorem mod_def (a b : $typeName) : a % b = a.toBitVec % b.toBitVec := rfl
theorem add_def (a b : $typeName) : a + b = a.toBitVec + b.toBitVec := rfl
@[simp] theorem toNat_mk : (mk a).toNat = a.toNat := rfl
@[simp] theorem toNat_ofBitVec : (ofBitVec a).toNat = a.toNat := rfl
@[deprecated toNat_ofBitVec (since := "2025-02-12")]
theorem toNat_mk : (ofBitVec a).toNat = a.toNat := rfl
@[simp] theorem toNat_ofNat {n : Nat} : (ofNat n).toNat = n % 2 ^ $bits := BitVec.toNat_ofNat ..
@@ -32,7 +35,11 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
theorem toNat_toBitVec_eq_toNat (x : $typeName) : x.toBitVec.toNat = x.toNat := rfl
@[simp] theorem mk_toBitVec_eq : (a : $typeName), mk a.toBitVec = a
@[simp] theorem ofBitVec_toBitVec_eq : (a : $typeName), ofBitVec a.toBitVec = a
| _, _ => rfl
@[deprecated ofBitVec_toBitVec_eq (since := "2025-02-12")]
theorem mk_toBitVec_eq : (a : $typeName), ofBitVec a.toBitVec = a
| _, _ => rfl
theorem toBitVec_eq_of_lt {a : Nat} : a < size (ofNat a).toBitVec.toNat = a :=
@@ -177,7 +184,10 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
theorem toBitVec_ofNat (n : Nat) : toBitVec (no_index (OfNat.ofNat n)) = BitVec.ofNat _ n := rfl
@[simp]
theorem mk_ofNat (n : Nat) : mk (BitVec.ofNat _ n) = OfNat.ofNat n := rfl
theorem ofBitVec_ofNat (n : Nat) : ofBitVec (BitVec.ofNat _ n) = OfNat.ofNat n := rfl
@[deprecated ofBitVec_ofNat (since := "2025-02-12")]
theorem mk_ofNat (n : Nat) : ofBitVec (BitVec.ofNat _ n) = OfNat.ofNat n := rfl
)
if let some nbits := bits.raw.isNatLit? then

View File

@@ -81,7 +81,7 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
@[csimp] private theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
funext α β n p f L h'
rcases L with L, rfl
simp only [pmap, pmapImpl, attachWith_mk, map_mk, Array.map_attachWith, eq_mk]
simp only [pmap, pmapImpl, attachWith_mk, map_mk, Array.map_attachWith_eq_pmap, eq_mk]
apply Array.pmap_congr_left
intro a m h₁ h₂
congr
@@ -133,7 +133,7 @@ theorem attachWith_congr {l₁ l₂ : Vector α n} (w : l₁ = l₂) {P : α
(l.push a).attach =
(l.attach.map (fun x, h => x, mem_push_of_mem a h)).push a, by simp := by
rcases l with l, rfl
simp [Array.map_attachWith]
simp [Array.map_attach_eq_pmap]
@[simp] theorem attachWith_push {a : α} {l : Vector α n} {P : α Prop} {H : x l.push a, P x} :
(l.push a).attachWith P H =
@@ -145,7 +145,7 @@ theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (l : Vector
pmap f l H = l.attach.map fun x => f x.1 (H _ x.2) := by
rcases l with l, rfl
simp only [pmap_mk, Array.pmap_eq_map_attach, attach_mk, map_mk, eq_mk]
rw [Array.map_attach, Array.map_attachWith]
rw [Array.map_attach_eq_pmap, Array.map_attachWith]
ext i hi₁ hi₂ <;> simp
@[simp]
@@ -299,7 +299,13 @@ theorem attachWith_map {l : Vector α n} (f : α → β) {P : β → Prop} {H :
rcases l with l, rfl
simp [Array.attachWith_map]
theorem map_attachWith {l : Vector α n} {P : α Prop} {H : (a : α), a l P a}
@[simp] theorem map_attachWith {l : Vector α n} {P : α Prop} {H : (a : α), a l P a}
(f : { x // P x } β) :
(l.attachWith P H).map f = l.attach.map fun x, h => f x, H _ h := by
rcases l with l, rfl
simp [Array.map_attachWith]
theorem map_attachWith_eq_pmap {l : Vector α n} {P : α Prop} {H : (a : α), a l P a}
(f : { x // P x } β) :
(l.attachWith P H).map f =
l.pmap (fun a (h : a l P a) => f a, H _ h.1) (fun a h => h, H a h) := by
@@ -307,11 +313,14 @@ theorem map_attachWith {l : Vector α n} {P : α → Prop} {H : ∀ (a : α), a
ext <;> simp
/-- See also `pmap_eq_map_attach` for writing `pmap` in terms of `map` and `attach`. -/
theorem map_attach {l : Vector α n} (f : { x // x l } β) :
theorem map_attach_eq_pmap {l : Vector α n} (f : { x // x l } β) :
l.attach.map f = l.pmap (fun a h => f a, h) (fun _ => id) := by
cases l
ext <;> simp
@[deprecated map_attach_eq_pmap (since := "2025-02-09")]
abbrev map_attach := @map_attach_eq_pmap
theorem pmap_pmap {p : α Prop} {q : β Prop} (g : a, p a β) (f : b, q b γ) (l : Vector α n) (H₁ H₂) :
pmap f (pmap g l H₁) H₂ =
pmap (α := { x // x l }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) l.attach
@@ -339,7 +348,7 @@ theorem pmap_append' {p : α → Prop} (f : ∀ a : α, p a → β) (l₁ : Vect
ys.attach.map (fun y, h => (y, mem_append_right xs h : { y // y xs ++ ys })) := by
rcases xs with xs, rfl
rcases ys with ys, rfl
simp [Array.map_attachWith]
simp [Array.map_attach_eq_pmap]
@[simp] theorem attachWith_append {P : α Prop} {xs : Vector α n} {ys : Vector α m}
{H : (a : α), a xs ++ ys P a} :
@@ -379,7 +388,7 @@ theorem reverse_attachWith {P : α → Prop} {xs : Vector α n}
theorem reverse_attach (xs : Vector α n) :
xs.attach.reverse = xs.reverse.attach.map fun x, h => x, by simpa using h := by
cases xs
simp [Array.map_attachWith]
simp [Array.map_attach_eq_pmap]
@[simp] theorem back?_pmap {P : α Prop} (f : (a : α) P a β) (xs : Vector α n)
(H : (a : α), a xs P a) :

View File

@@ -1471,7 +1471,7 @@ theorem vector₂_induction (P : Vector (Vector α n) m → Prop)
P (mk (xss.attach.map (fun xs, m => mk xs (h₂ xs m))) (by simpa using h₁)))
(ass : Vector (Vector α n) m) : P ass := by
specialize of (ass.map toArray).toArray (by simp) (by simp)
simpa [Array.map_attach, Array.pmap_map] using of
simpa [Array.map_attach_eq_pmap, Array.pmap_map] using of
/--
Use this as `induction ass using vector₃_induction` on a hypothesis of the form `ass : Vector (Vector (Vector α n) m) k`.
@@ -1489,7 +1489,7 @@ theorem vector₃_induction (P : Vector (Vector (Vector α n) m) k → Prop)
mk x (h₃ xs m x m'))) (by simpa using h₂ xs m))) (by simpa using h₁)))
(ass : Vector (Vector (Vector α n) m) k) : P ass := by
specialize of (ass.map (fun as => (as.map toArray).toArray)).toArray (by simp) (by simp) (by simp)
simpa [Array.map_attach, Array.pmap_map] using of
simpa [Array.map_attach_eq_pmap, Array.pmap_map] using of
/-! ### singleton -/
@@ -1800,7 +1800,7 @@ theorem flatten_flatten {L : Vector (Vector (Vector α n) m) k} :
induction L using vector₃_induction with
| of xss h₁ h₂ h₃ =>
-- simp [Array.flatten_flatten] -- FIXME: `simp` produces a bad proof here!
simp [Array.map_attach, Array.flatten_flatten, Array.map_pmap]
simp [Array.map_attach_eq_pmap, Array.flatten_flatten, Array.map_pmap]
/-- Two vectors of constant length vectors are equal iff their flattens coincide. -/
theorem eq_iff_flatten_eq {L L' : Vector (Vector α n) m} :

View File

@@ -1509,25 +1509,35 @@ This will rewrite with all equation lemmas, which can be used to
partially evaluate many definitions. -/
declare_simp_like_tactic simpAutoUnfold "simp! " (autoUnfold := true)
/-- `simp_arith` is shorthand for `simp` with `arith := true` and `decide := true`.
This enables the use of normalization by linear arithmetic. -/
declare_simp_like_tactic simpArith "simp_arith " (arith := true) (decide := true)
/--
`simp_arith` has been deprecated. It was a shorthand for `simp +arith +decide`.
Note that `+decide` is not needed for reducing arithmetic terms since simprocs have been added to Lean.
-/
syntax (name := simpArith) "simp_arith " optConfig (discharger)? (&" only")? (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
/-- `simp_arith!` is shorthand for `simp_arith` with `autoUnfold := true`.
This will rewrite with all equation lemmas, which can be used to
partially evaluate many definitions. -/
declare_simp_like_tactic simpArithAutoUnfold "simp_arith! " (arith := true) (autoUnfold := true) (decide := true)
/--
`simp_arith!` has been deprecated. It was a shorthand for `simp! +arith +decide`.
Note that `+decide` is not needed for reducing arithmetic terms since simprocs have been added to Lean.
-/
syntax (name := simpArithBang) "simp_arith! " optConfig (discharger)? (&" only")? (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
/-- `simp_all!` is shorthand for `simp_all` with `autoUnfold := true`.
This will rewrite with all equation lemmas, which can be used to
partially evaluate many definitions. -/
declare_simp_like_tactic (all := true) simpAllAutoUnfold "simp_all! " (autoUnfold := true)
/-- `simp_all_arith` combines the effects of `simp_all` and `simp_arith`. -/
declare_simp_like_tactic (all := true) simpAllArith "simp_all_arith " (arith := true) (decide := true)
/--
`simp_all_arith` has been deprecated. It was a shorthand for `simp_all +arith +decide`.
Note that `+decide` is not needed for reducing arithmetic terms since simprocs have been added to Lean.
-/
syntax (name := simpAllArith) "simp_all_arith" optConfig (discharger)? (&" only")? (" [" (simpErase <|> simpLemma),* "]")? : tactic
/--
`simp_all_arith!` has been deprecated. It was a shorthand for `simp_all! +arith +decide`.
Note that `+decide` is not needed for reducing arithmetic terms since simprocs have been added to Lean.
-/
syntax (name := simpAllArithBang) "simp_all_arith!" optConfig (discharger)? (&" only")? (" [" (simpErase <|> simpLemma),* "]")? : tactic
/-- `simp_all_arith!` combines the effects of `simp_all`, `simp_arith` and `simp!`. -/
declare_simp_like_tactic (all := true) simpAllArithAutoUnfold "simp_all_arith! " (arith := true) (autoUnfold := true) (decide := true)
/-- `dsimp!` is shorthand for `dsimp` with `autoUnfold := true`.
This will rewrite with all equation lemmas, which can be used to

View File

@@ -1927,11 +1927,16 @@ The type of unsigned 8-bit integers. This type has special support in the
compiler to make it actually 8 bits rather than wrapping a `Nat`.
-/
structure UInt8 where
/-- Unpack a `UInt8` as a `BitVec 8`.
This function is overridden with a native implementation. -/
/--
Create a `UInt8` from a `BitVec 8`. This function is overridden with a native implementation.
-/
ofBitVec ::
/--
Unpack a `UInt8` as a `BitVec 8`. This function is overridden with a native implementation.
-/
toBitVec : BitVec 8
attribute [extern "lean_uint8_of_nat_mk"] UInt8.mk
attribute [extern "lean_uint8_of_nat_mk"] UInt8.ofBitVec
attribute [extern "lean_uint8_to_nat"] UInt8.toBitVec
/--
@@ -1942,6 +1947,14 @@ This function is overridden with a native implementation.
def UInt8.ofNatCore (n : @& Nat) (h : LT.lt n UInt8.size) : UInt8 where
toBitVec := BitVec.ofNatLt n h
/--
Pack a `Nat` less than `2^8` into a `UInt8`.
This function is overridden with a native implementation.
-/
@[extern "lean_uint8_of_nat"]
def UInt8.ofNatLT (n : @& Nat) (h : LT.lt n UInt8.size) : UInt8 where
toBitVec := BitVec.ofNatLt n h
set_option bootstrap.genMatcherCode false in
/--
Decides equality on `UInt8`.
@@ -1968,11 +1981,16 @@ The type of unsigned 16-bit integers. This type has special support in the
compiler to make it actually 16 bits rather than wrapping a `Nat`.
-/
structure UInt16 where
/-- Unpack a `UInt16` as a `BitVec 16`.
This function is overridden with a native implementation. -/
/--
Create a `UInt16` from a `BitVec 16`. This function is overridden with a native implementation.
-/
ofBitVec ::
/--
Unpack a `UInt16` as a `BitVec 16`. This function is overridden with a native implementation.
-/
toBitVec : BitVec 16
attribute [extern "lean_uint16_of_nat_mk"] UInt16.mk
attribute [extern "lean_uint16_of_nat_mk"] UInt16.ofBitVec
attribute [extern "lean_uint16_to_nat"] UInt16.toBitVec
/--
@@ -1983,6 +2001,14 @@ This function is overridden with a native implementation.
def UInt16.ofNatCore (n : @& Nat) (h : LT.lt n UInt16.size) : UInt16 where
toBitVec := BitVec.ofNatLt n h
/--
Pack a `Nat` less than `2^16` into a `UInt16`.
This function is overridden with a native implementation.
-/
@[extern "lean_uint16_of_nat"]
def UInt16.ofNatLT (n : @& Nat) (h : LT.lt n UInt16.size) : UInt16 where
toBitVec := BitVec.ofNatLt n h
set_option bootstrap.genMatcherCode false in
/--
Decides equality on `UInt16`.
@@ -2009,11 +2035,16 @@ The type of unsigned 32-bit integers. This type has special support in the
compiler to make it actually 32 bits rather than wrapping a `Nat`.
-/
structure UInt32 where
/-- Unpack a `UInt32` as a `BitVec 32.
This function is overridden with a native implementation. -/
/--
Create a `UInt32` from a `BitVec 32`. This function is overridden with a native implementation.
-/
ofBitVec ::
/--
Unpack a `UInt32` as a `BitVec 32`. This function is overridden with a native implementation.
-/
toBitVec : BitVec 32
attribute [extern "lean_uint32_of_nat_mk"] UInt32.mk
attribute [extern "lean_uint32_of_nat_mk"] UInt32.ofBitVec
attribute [extern "lean_uint32_to_nat"] UInt32.toBitVec
/--
@@ -2024,6 +2055,14 @@ This function is overridden with a native implementation.
def UInt32.ofNatCore (n : @& Nat) (h : LT.lt n UInt32.size) : UInt32 where
toBitVec := BitVec.ofNatLt n h
/--
Pack a `Nat` less than `2^32` into a `UInt32`.
This function is overridden with a native implementation.
-/
@[extern "lean_uint32_of_nat"]
def UInt32.ofNatLT (n : @& Nat) (h : LT.lt n UInt32.size) : UInt32 where
toBitVec := BitVec.ofNatLt n h
/--
Unpack a `UInt32` as a `Nat`.
This function is overridden with a native implementation.
@@ -2081,11 +2120,16 @@ The type of unsigned 64-bit integers. This type has special support in the
compiler to make it actually 64 bits rather than wrapping a `Nat`.
-/
structure UInt64 where
/-- Unpack a `UInt64` as a `BitVec 64`.
This function is overridden with a native implementation. -/
/--
Create a `UInt64` from a `BitVec 64`. This function is overridden with a native implementation.
-/
ofBitVec ::
/--
Unpack a `UInt64` as a `BitVec 64`. This function is overridden with a native implementation.
-/
toBitVec: BitVec 64
attribute [extern "lean_uint64_of_nat_mk"] UInt64.mk
attribute [extern "lean_uint64_of_nat_mk"] UInt64.ofBitVec
attribute [extern "lean_uint64_to_nat"] UInt64.toBitVec
/--
@@ -2096,6 +2140,14 @@ This function is overridden with a native implementation.
def UInt64.ofNatCore (n : @& Nat) (h : LT.lt n UInt64.size) : UInt64 where
toBitVec := BitVec.ofNatLt n h
/--
Pack a `Nat` less than `2^64` into a `UInt64`.
This function is overridden with a native implementation.
-/
@[extern "lean_uint64_of_nat"]
def UInt64.ofNatLT (n : @& Nat) (h : LT.lt n UInt64.size) : UInt64 where
toBitVec := BitVec.ofNatLt n h
set_option bootstrap.genMatcherCode false in
/--
Decides equality on `UInt64`.
@@ -2136,11 +2188,18 @@ For example, if running on a 32-bit machine, USize is equivalent to UInt32.
Or on a 64-bit machine, UInt64.
-/
structure USize where
/-- Unpack a `USize` as a `BitVec System.Platform.numBits`.
This function is overridden with a native implementation. -/
/--
Create a `USize` from a `BitVec System.Platform.numBits`. This function is overridden with a
native implementation.
-/
ofBitVec ::
/--
Unpack a `USize` as a `BitVec System.Platform.numBits`. This function is overridden with a native
implementation.
-/
toBitVec : BitVec System.Platform.numBits
attribute [extern "lean_usize_of_nat_mk"] USize.mk
attribute [extern "lean_usize_of_nat_mk"] USize.ofBitVec
attribute [extern "lean_usize_to_nat"] USize.toBitVec
/--
@@ -2151,6 +2210,14 @@ This function is overridden with a native implementation.
def USize.ofNatCore (n : @& Nat) (h : LT.lt n USize.size) : USize where
toBitVec := BitVec.ofNatLt n h
/--
Pack a `Nat` less than `USize.size` into a `USize`.
This function is overridden with a native implementation.
-/
@[extern "lean_usize_of_nat"]
def USize.ofNatLT (n : @& Nat) (h : LT.lt n USize.size) : USize where
toBitVec := BitVec.ofNatLt n h
set_option bootstrap.genMatcherCode false in
/--
Decides equality on `USize`.
@@ -2168,6 +2235,7 @@ instance : DecidableEq USize := USize.decEq
instance : Inhabited USize where
default := USize.ofNatCore 0 usize_size_pos
/--
A `Nat` denotes a valid unicode codepoint if it is less than `0x110000`, and
it is also not a "surrogate" character (the range `0xd800` to `0xdfff` inclusive).

View File

@@ -452,7 +452,7 @@ else isTrue fun h2 => absurd h2 h
theorem decide_eq_true_iff {p : Prop} [Decidable p] : (decide p = true) p := by simp
@[simp, boolToPropSimps] theorem decide_eq_decide {p q : Prop} {_ : Decidable p} {_ : Decidable q} :
@[simp, bool_to_prop] theorem decide_eq_decide {p q : Prop} {_ : Decidable p} {_ : Decidable q} :
decide p = decide q (p q) :=
fun h => by rw [ decide_eq_true_iff (p := p), h, decide_eq_true_iff], fun h => by simp [h]

View File

@@ -9,28 +9,28 @@ import Init.SizeOf
import Init.Data.Nat.Linear
@[simp] protected theorem Fin.sizeOf (a : Fin n) : sizeOf a = a.val + 1 := by
cases a; simp_arith
cases a; simp +arith
@[simp] protected theorem BitVec.sizeOf (a : BitVec w) : sizeOf a = sizeOf a.toFin + 1 := by
cases a; simp_arith
cases a; simp +arith
@[simp] protected theorem UInt8.sizeOf (a : UInt8) : sizeOf a = a.toNat + 3 := by
cases a; simp_arith [UInt8.toNat, BitVec.toNat]
cases a; simp +arith [UInt8.toNat, BitVec.toNat]
@[simp] protected theorem UInt16.sizeOf (a : UInt16) : sizeOf a = a.toNat + 3 := by
cases a; simp_arith [UInt16.toNat, BitVec.toNat]
cases a; simp +arith [UInt16.toNat, BitVec.toNat]
@[simp] protected theorem UInt32.sizeOf (a : UInt32) : sizeOf a = a.toNat + 3 := by
cases a; simp_arith [UInt32.toNat, BitVec.toNat]
cases a; simp +arith [UInt32.toNat, BitVec.toNat]
@[simp] protected theorem UInt64.sizeOf (a : UInt64) : sizeOf a = a.toNat + 3 := by
cases a; simp_arith [UInt64.toNat, BitVec.toNat]
cases a; simp +arith [UInt64.toNat, BitVec.toNat]
@[simp] protected theorem USize.sizeOf (a : USize) : sizeOf a = a.toNat + 3 := by
cases a; simp_arith [USize.toNat, BitVec.toNat]
cases a; simp +arith [USize.toNat, BitVec.toNat]
@[simp] protected theorem Char.sizeOf (a : Char) : sizeOf a = a.toNat + 4 := by
cases a; simp_arith [Char.toNat]
cases a; simp +arith [Char.toNat]
@[simp] protected theorem Subtype.sizeOf {α : Sort u_1} {p : α Prop} (s : Subtype p) : sizeOf s = sizeOf s.val + 1 := by
cases s; simp

View File

@@ -1014,31 +1014,6 @@ example : ∀ x : Nat, x = x := by unhygienic
-/
macro "unhygienic " t:tacticSeq : tactic => `(tactic| set_option tactic.hygienic false in $t)
/--
`checkpoint tac` acts the same as `tac`, but it caches the input and output of `tac`,
and if the file is re-elaborated and the input matches, the tactic is not re-run and
its effects are reapplied to the state. This is useful for improving responsiveness
when working on a long tactic proof, by wrapping expensive tactics with `checkpoint`.
See the `save` tactic, which may be more convenient to use.
(TODO: do this automatically and transparently so that users don't have to use
this combinator explicitly.)
-/
syntax (name := checkpoint) "checkpoint " tacticSeq : tactic
/--
`save` is defined to be the same as `skip`, but the elaborator has
special handling for occurrences of `save` in tactic scripts and will transform
`by tac1; save; tac2` to `by (checkpoint tac1); tac2`, meaning that the effect of `tac1`
will be cached and replayed. This is useful for improving responsiveness
when working on a long tactic proof, by using `save` after expensive tactics.
(TODO: do this automatically and transparently so that users don't have to use
this combinator explicitly.)
-/
macro (name := save) "save" : tactic => `(tactic| skip)
/--
The tactic `sleep ms` sleeps for `ms` milliseconds and does nothing.
It is used for debugging purposes only.
@@ -1310,10 +1285,10 @@ syntax (name := omega) "omega" optConfig : tactic
/--
`bv_omega` is `omega` with an additional preprocessor that turns statements about `BitVec` into statements about `Nat`.
Currently the preprocessor is implemented as `try simp only [bv_toNat] at *`.
`bv_toNat` is a `@[simp]` attribute that you can (cautiously) add to more theorems.
Currently the preprocessor is implemented as `try simp only [bitvec_to_nat] at *`.
`bitvec_to_nat` is a `@[simp]` attribute that you can (cautiously) add to more theorems.
-/
macro "bv_omega" : tactic => `(tactic| (try simp only [bv_toNat] at *) <;> omega)
macro "bv_omega" : tactic => `(tactic| (try simp only [bitvec_to_nat] at *) <;> omega)
/-- Implementation of `ac_nf` (the full `ac_nf` calls `trivial` afterwards). -/
syntax (name := acNf0) "ac_nf0" (location)? : tactic
@@ -1603,11 +1578,68 @@ using `show_term`.
macro (name := by?) tk:"by?" t:tacticSeq : term => `(show_term%$tk by%$tk $t)
/--
`expose_names` creates a new goal whose local context has been "exposed" so that every local declaration has a clear,
accessible name. If no local declarations require renaming, the original goal is returned unchanged.
`expose_names` renames all inaccessible variables with accessible names, making them available
for reference in generated tactics. However, this renaming introduces machine-generated names
that are not fully under user control. `expose_names` is primarily intended as a preamble for
auto-generated end-game tactic scripts. It is also useful as an alternative to
`set_option tactic.hygienic false`. If explicit control over renaming is needed in the
middle of a tactic script, consider using structured tactic scripts with
`match .. with`, `induction .. with`, or `intro` with explicit user-defined names,
as well as tactics such as `next`, `case`, and `rename_i`.
-/
syntax (name := exposeNames) "expose_names" : tactic
/--
Close fixed-width `BitVec` and `Bool` goals by obtaining a proof from an external SAT solver and
verifying it inside Lean. The solvable goals are currently limited to
- the Lean equivalent of [`QF_BV`](https://smt-lib.org/logics-all.shtml#QF_BV)
- automatically splitting up `structure`s that contain information about `BitVec` or `Bool`
```lean
example : ∀ (a b : BitVec 64), (a &&& b) + (a ^^^ b) = a ||| b := by
intros
bv_decide
```
If `bv_decide` encounters an unknown definition it will be treated like an unconstrained `BitVec`
variable. Sometimes this enables solving goals despite not understanding the definition because
the precise properties of the definition do not matter in the specific proof.
If `bv_decide` fails to close a goal it provides a counter-example, containing assignments for all
terms that were considered as variables.
In order to avoid calling a SAT solver every time, the proof can be cached with `bv_decide?`.
If solving your problem relies inherently on using associativity or commutativity, consider enabling
the `bv.ac_nf` option.
Note: `bv_decide` uses `ofReduceBool` and thus trusts the correctness of the code generator.
Note: include `import Std.Tactic.BVDecide`
-/
macro (name := bvDecideMacro) (priority:=low) "bv_decide" optConfig : tactic =>
Macro.throwError "to use `bv_decide`, please include `import Std.Tactic.BVDecide`"
/--
Suggest a proof script for a `bv_decide` tactic call. Useful for caching LRAT proofs.
Note: include `import Std.Tactic.BVDecide`
-/
macro (name := bvTraceMacro) (priority:=low) "bv_decide?" optConfig : tactic =>
Macro.throwError "to use `bv_decide?`, please include `import Std.Tactic.BVDecide`"
/--
Run the normalization procedure of `bv_decide` only. Sometimes this is enough to solve basic
`BitVec` goals already.
Note: include `import Std.Tactic.BVDecide`
-/
macro (name := bvNormalizeMacro) (priority:=low) "bv_normalize" optConfig : tactic =>
Macro.throwError "to use `bv_normalize`, please include `import Std.Tactic.BVDecide`"
end Tactic
namespace Attr
@@ -1740,7 +1772,7 @@ macro_rules | `($type) => `((by assumption : $type))
by the notation `arr[i]` to prove any side conditions that arise when
constructing the term (e.g. the index is in bounds of the array).
The default behavior is to just try `trivial` (which handles the case
where `i < arr.size` is in the context) and `simp_arith` and `omega`
where `i < arr.size` is in the context) and `simp +arith` and `omega`
(for doing linear arithmetic in the index).
-/
syntax "get_elem_tactic_trivial" : tactic

View File

@@ -15,8 +15,6 @@ structure Config where
main := true
/-- If `name` is `true`, all functions in the same namespace are considere for function induction, unfolding, etc. -/
name := true
/-- If `lib` is `true`, uses `libSearch` results. -/
lib := true
/-- If `targetOnly` is `true`, `try?` collects information using the goal target only. -/
targetOnly := false
/-- Maximum number of suggestions. -/
@@ -25,6 +23,21 @@ structure Config where
missing := false
/-- If `only` is `true`, generates solutions using `grind only` and `simp only`. -/
only := true
/-- If `harder` is `true`, more expensive tactics and operations are tried. -/
harder := false
/--
If `merge` is `true`, it tries to compress suggestions such as
```
induction a
· grind only [= f]
· grind only [→ g]
```
as
```
induction a <;> grind only [= f, → g]
```
-/
merge := true
deriving Inhabited
end Lean.Try

View File

@@ -5,6 +5,7 @@ Author: Leonardo de Moura
-/
prelude
import Init.SizeOf
import Init.BinderNameHint
import Init.Data.Nat.Basic
universe u v
@@ -414,3 +415,18 @@ theorem mkSkipLeft {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β
end
end PSigma
/--
The `wfParam` gadget is used internally during the construction of recursive functions by
wellfounded recursion, to keep track of the parameter for which the automatic introduction
of `List.attach` (or similar) is plausible.
-/
def wfParam {α : Sort u} (a : α) : α := a
/--
Reverse direction of `dite_eq_ite`. Used by the well-founded definition preprocessor to extend the
context of a termination proof inside `if-then-else` with the condition.
-/
@[wf_preprocess] theorem ite_eq_dite [Decidable P] :
ite P a b = (dite P (fun h => binderNameHint h () a) (fun h => binderNameHint h () b)) := by
rfl

View File

@@ -37,3 +37,4 @@ import Lean.SubExpr
import Lean.LabelAttribute
import Lean.AddDecl
import Lean.Replay
import Lean.PrivateName

View File

@@ -13,7 +13,8 @@ structure ClosedTermCache where
constNames : NameSet := {}
deriving Inhabited
builtin_initialize closedTermCacheExt : EnvExtension ClosedTermCache registerEnvExtension (pure {})
builtin_initialize closedTermCacheExt : EnvExtension ClosedTermCache
registerEnvExtension (pure {}) (asyncMode := .sync) -- compilation is non-parallel anyway
@[export lean_cache_closed_term_name]
def cacheClosedTermName (env : Environment) (e : Expr) (n : Name) : Environment :=

View File

@@ -142,6 +142,7 @@ builtin_initialize functionSummariesExt : SimplePersistentEnvExtension (FunId ×
addImportedFn := fun _ => {}
addEntryFn := fun s e, n => s.insert e n
toArrayFn := fun s => sortEntries s.toArray
asyncMode := .sync -- compilation is non-parallel anyway
}
def addFunctionSummary (env : Environment) (fid : FunId) (v : Value) : Environment :=

View File

@@ -69,7 +69,7 @@ def eqvLetValue (e₁ e₂ : LetValue) : EqvM Bool := do
let rec @[specialize] go (i : Nat) : EqvM Bool := do
if h : i < params₁.size then
let p₁ := params₁[i]
have : i < params₂.size := by simp_all_arith
have : i < params₂.size := by simp_all +arith
let p₂ := params₂[i]
unless ( eqvType p₁.type p₂.type) do return false
withFVar p₁.fvarId p₂.fvarId do

View File

@@ -20,7 +20,7 @@ structure BaseTypeExtState where
deriving Inhabited
builtin_initialize baseTypeExt : EnvExtension BaseTypeExtState
registerEnvExtension (pure {})
registerEnvExtension (pure {}) (asyncMode := .sync) -- compilation is non-parallel anyway
def getOtherDeclBaseType (declName : Name) (us : List Level) : CoreM Expr := do
let info getConstInfo declName

View File

@@ -248,6 +248,7 @@ builtin_initialize functionSummariesExt : SimplePersistentEnvExtension (Name ×
addImportedFn := fun _ => {}
addEntryFn := fun s e, n => s.insert e n
toArrayFn := fun s => s.toArray.qsort decLt
asyncMode := .sync -- compilation is non-parallel anyway
}
/--

View File

@@ -117,7 +117,7 @@ structure MonoTypeExtState where
deriving Inhabited
builtin_initialize monoTypeExt : EnvExtension MonoTypeExtState
registerEnvExtension (pure {})
registerEnvExtension (pure {}) (asyncMode := .sync) -- compilation is non-parallel anyway
def getOtherDeclMonoType (declName : Name) : CoreM Expr := do
match monoTypeExt.getState ( getEnv) |>.mono.find? declName with

View File

@@ -47,7 +47,7 @@ structure Pass where
Resulting phase.
-/
phaseOut : Phase := phase
phaseInv : phaseOut phase := by simp_arith
phaseInv : phaseOut phase := by simp +arith +decide
/--
The name of the `Pass`
-/

View File

@@ -94,6 +94,7 @@ builtin_initialize passManagerExt : PersistentEnvExtension Name (Name × PassMan
addImportedFn := fun ns => return ([], ImportM.runCoreM <| runImportedDecls ns)
addEntryFn := fun (installerDeclNames, _) (installerDeclName, managerNew) => (installerDeclName :: installerDeclNames, managerNew)
exportEntriesFn := fun s => s.1.reverse.toArray
asyncMode := .sync
}
def getPassManager : CoreM PassManager :=

View File

@@ -410,6 +410,7 @@ builtin_initialize folderExt : PersistentEnvExtension FolderOleanEntry FolderEnt
return ([], folders.switch)
addEntryFn := fun (entries, map) entry => (entry.toFolderOleanEntry :: entries, map.insert entry.declName entry.folder)
exportEntriesFn := fun (entries, _) => entries.reverse.toArray
asyncMode := .sync
}
def registerFolder (declName : Name) (folderDeclName : Name) : CoreM Unit := do

View File

@@ -85,6 +85,7 @@ builtin_initialize specExtension : SimplePersistentEnvExtension SpecEntry SpecSt
addEntryFn := SpecState.addEntry
addImportedFn := fun _ => {}
toArrayFn := fun s => sortEntries s.toArray
asyncMode := .sync
}
/--

View File

@@ -32,6 +32,7 @@ builtin_initialize specCacheExt : SimplePersistentEnvExtension CacheEntry Cache
registerSimplePersistentEnvExtension {
addEntryFn := addEntry
addImportedFn := fun es => (mkStateFromImportedEntries addEntry {} es).switch
asyncMode := .sync
}
def cacheSpec (key : Expr) (declName : Name) : CoreM Unit :=

View File

@@ -527,16 +527,17 @@ partial def compileDecls (decls : List Name) (ref? : Option Declaration := none)
doCompile
return
let env getEnv
let (postEnv, prom) env.promiseChecked
let res env.promiseChecked
setEnv res.mainEnv
let checkAct Core.wrapAsyncAsSnapshot fun _ => do
setEnv res.asyncEnv
try
doCompile
finally
prom.resolve ( getEnv)
res.commitChecked ( getEnv)
let t BaseIO.mapTask (fun _ => checkAct) env.checked
let endRange? := ( getRef).getTailPos?.map fun pos => pos, pos
Core.logSnapshotTask { range? := endRange?, task := t }
setEnv postEnv
where doCompile := do
-- don't compile if kernel errored; should be converted into a task dependency when compilation
-- is made async as well

View File

@@ -95,7 +95,6 @@ structure Context where
macroStack : MacroStack := []
currMacroScope : MacroScope := firstFrontendMacroScope
ref : Syntax := Syntax.missing
tacticCache? : Option (IO.Ref Tactic.Cache)
/--
Snapshot for incremental reuse and reporting of command elaboration. Currently only used for
(mutual) defs and contained tactics, in which case the `DynamicSnapshot` is a
@@ -619,8 +618,7 @@ private def mkTermContext (ctx : Context) (s : State) : CommandElabM Term.Contex
return {
macroStack := ctx.macroStack
sectionVars := sectionVars
isNoncomputableSection := scope.isNoncomputable
tacticCache? := ctx.tacticCache? }
isNoncomputableSection := scope.isNoncomputable }
/--
Lift the `TermElabM` monadic action `x` into a `CommandElabM` monadic action.
@@ -759,7 +757,6 @@ private def liftCommandElabMCore (cmd : CommandElabM α) (throwOnError : Bool) :
currRecDepth := ctx.currRecDepth
currMacroScope := ctx.currMacroScope
ref := ctx.ref
tacticCache? := none
snap? := none
cancelTk? := ctx.cancelTk?
suppressElabErrors := ctx.suppressElabErrors

View File

@@ -26,12 +26,10 @@ private def throwForInFailure (forInInstance : Expr) : TermElabM Expr :=
@[builtin_term_elab forInMacro] def elabForIn : TermElab := fun stx expectedType? => do
match stx with
| `(for_in% $col $init $body) =>
match ( isLocalIdent? col) with
| none => elabTerm ( `(let col := $col; for_in% col $init $body)) expectedType?
| some colFVar =>
tryPostponeIfNoneOrMVar expectedType?
let colE elabTerm col none
let m getMonadForIn expectedType?
let colType inferType colFVar
let colType inferType colE
let elemType mkFreshExprMVar (mkSort (mkLevelSucc ( mkFreshLevelMVar)))
let forInInstance try
mkAppM ``ForIn #[m, colType, elemType]
@@ -42,7 +40,7 @@ private def throwForInFailure (forInInstance : Expr) : TermElabM Expr :=
let forInFn mkConst ``forIn
elabAppArgs forInFn
(namedArgs := #[{ name := `m, val := Arg.expr m}, { name := `α, val := Arg.expr elemType }, { name := `self, val := Arg.expr inst }])
(args := #[Arg.stx col, Arg.stx init, Arg.stx body])
(args := #[Arg.expr colE, Arg.stx init, Arg.stx body])
(expectedType? := expectedType?)
(explicit := false) (ellipsis := false) (resultIsOutParamSupport := false)
| .undef => tryPostpone; throwForInFailure forInInstance
@@ -52,12 +50,10 @@ private def throwForInFailure (forInInstance : Expr) : TermElabM Expr :=
@[builtin_term_elab forInMacro'] def elabForIn' : TermElab := fun stx expectedType? => do
match stx with
| `(for_in'% $col $init $body) =>
match ( isLocalIdent? col) with
| none => elabTerm ( `(let col := $col; for_in'% col $init $body)) expectedType?
| some colFVar =>
tryPostponeIfNoneOrMVar expectedType?
let colE elabTerm col none
let m getMonadForIn expectedType?
let colType inferType colFVar
let colType inferType colE
let elemType mkFreshExprMVar (mkSort (mkLevelSucc ( mkFreshLevelMVar)))
let forInInstance
try
@@ -70,7 +66,7 @@ private def throwForInFailure (forInInstance : Expr) : TermElabM Expr :=
let forInFn mkConst ``forIn'
elabAppArgs forInFn
(namedArgs := #[{ name := `m, val := Arg.expr m}, { name := `α, val := Arg.expr elemType}, { name := `self, val := Arg.expr inst }])
(args := #[Arg.expr colFVar, Arg.stx init, Arg.stx body])
(args := #[Arg.expr colE, Arg.stx init, Arg.stx body])
(expectedType? := expectedType?)
(explicit := false) (ellipsis := false) (resultIsOutParamSupport := false)
| .undef => tryPostpone; throwForInFailure forInInstance

View File

@@ -33,7 +33,6 @@ def setCommandState (commandState : Command.State) : FrontendM Unit :=
cmdPos := s.cmdPos
fileName := ctx.inputCtx.fileName
fileMap := ctx.inputCtx.fileMap
tacticCache? := none
snap? := none
cancelTk? := none
}

View File

@@ -1,19 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joachim Breitner
-/
prelude
import Lean.Meta.Transform
import Lean.Meta.Match.MatcherApp.Basic
import Lean.Elab.Tactic.Simp
open Lean Meta
namespace Lean.Elab.WF
builtin_initialize wfPreprocessSimpExtension : SimpExtension
registerSimpAttr `wf_preprocess
"(not yet functional)"
end Lean.Elab.WF

View File

@@ -0,0 +1,36 @@
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Meta.Transform
import Lean.Elab.RecAppSyntax
namespace Lean.Elab.WF
open Meta
/--
Preprocesses the expressions to improve the effectiveness of `wfRecursion`.
* Floats out the RecApp markers.
Example:
```
def f : Nat → Nat
| 0 => 1
| i+1 => (f x) i
```
Unlike `Lean.Elab.Structural.preprocess`, do _not_ beta-reduce, as it could
remove `let_fun`-lambdas that contain explicit termination proofs.
-/
def floatRecApp (e : Expr) : CoreM Expr :=
Core.transform e
(post := fun e => do
if e.isApp && e.getAppFn.isMData then
let .mdata m f := e.getAppFn | unreachable!
if m.isRecApp then
return .done (.mdata m (f.beta e.getAppArgs))
return .continue)
end Lean.Elab.WF

View File

@@ -1,30 +0,0 @@
/-
Copyright (c) 2022 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Meta.Transform
namespace Lean.Meta
/--
Convert `ite` expressions in `e` to `dite`s.
It is useful to make this conversion in the `WF` module because the condition is often used in
termination proofs. -/
def iteToDIte (e : Expr) : MetaM Expr := do
-- TODO: move this file to `Meta` if we decide to use it in other places.
let post (e : Expr) : MetaM TransformStep := do
if e.isAppOfArity ``ite 5 then
let f := e.getAppFn
let args := e.getAppArgs
let c := args[1]!
let h mkFreshUserName `h
let args := args.set! 3 (Lean.mkLambda h BinderInfo.default c args[3]!)
let args := args.set! 4 (Lean.mkLambda h BinderInfo.default (mkNot c) args[4]!)
return .done <| mkAppN (mkConst ``dite f.constLevels!) args
else
return .done e
transform e (post := post)
end Lean.Meta

View File

@@ -8,12 +8,11 @@ import Lean.Elab.PreDefinition.Basic
import Lean.Elab.PreDefinition.TerminationMeasure
import Lean.Elab.PreDefinition.Mutual
import Lean.Elab.PreDefinition.WF.PackMutual
import Lean.Elab.PreDefinition.WF.Preprocess
import Lean.Elab.PreDefinition.WF.FloatRecApp
import Lean.Elab.PreDefinition.WF.Rel
import Lean.Elab.PreDefinition.WF.Fix
import Lean.Elab.PreDefinition.WF.Unfold
import Lean.Elab.PreDefinition.WF.Ite
import Lean.Elab.PreDefinition.WF.AutoAttach
import Lean.Elab.PreDefinition.WF.Preprocess
import Lean.Elab.PreDefinition.WF.GuessLex
namespace Lean.Elab
@@ -23,8 +22,8 @@ open Meta
def wfRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (Option TerminationMeasure)) : TermElabM Unit := do
let termMeasures? := termMeasure?s.mapM id -- Either all or none, checked by `elabTerminationByHints`
let preDefs preDefs.mapM fun preDef =>
return { preDef with value := ( preprocess preDef.value) }
let (fixedPrefixSize, argsPacker, unaryPreDef) withoutModifyingEnv do
return { preDef with value := ( floatRecApp preDef.value) }
let (fixedPrefixSize, argsPacker, unaryPreDef, wfPreprocessProofs) withoutModifyingEnv do
for preDef in preDefs do
addAsAxiom preDef
let fixedPrefixSize Mutual.getFixedPrefix preDefs
@@ -34,8 +33,10 @@ def wfRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (Option T
if varNames.isEmpty then
throwError "well-founded recursion cannot be used, '{preDef.declName}' does not take any (non-fixed) arguments"
let argsPacker := { varNamess }
let preDefsDIte preDefs.mapM fun preDef => return { preDef with value := ( iteToDIte preDef.value) }
return (fixedPrefixSize, argsPacker, packMutual fixedPrefixSize argsPacker preDefsDIte)
let (preDefsAttached, wfPreprocessProofs) Array.unzip <$> preDefs.mapM fun preDef => do
let result preprocess preDef.value
return ({preDef with value := result.expr}, result)
return (fixedPrefixSize, argsPacker, packMutual fixedPrefixSize argsPacker preDefsAttached, wfPreprocessProofs)
let wf : TerminationMeasures do
if let some tms := termMeasures? then pure tms else
@@ -62,10 +63,10 @@ def wfRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (Option T
Mutual.addPreDefsFromUnary preDefs preDefsNonrec preDefNonRec
let preDefs Mutual.cleanPreDefs preDefs
registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker
for preDef in preDefs do
for preDef in preDefs, wfPreprocessProof in wfPreprocessProofs do
unless preDef.kind.isTheorem do
unless ( isProp preDef.type) do
WF.mkUnfoldEq preDef preDefNonRec.declName
WF.mkUnfoldEq preDef preDefNonRec.declName wfPreprocessProof
Mutual.addPreDefAttributes preDefs
builtin_initialize registerTraceClass `Elab.definition.wf

View File

@@ -1,42 +1,149 @@
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
Authors: Joachim Breitner
-/
prelude
import Lean.Meta.Transform
import Lean.Elab.RecAppSyntax
import Lean.Meta.Match.MatcherApp.Basic
import Lean.Elab.Tactic.Simp
/-!
This module implements the preprocessing of function definitions involved in well-founded recursion.
The goal is to change higher order functions to add more information to the context, e.g. change
`List.map (fun x => …) xs` to `List.map (fun ⟨x, h⟩ => …) xs.attach`. This extra information can
then be used by the termination proof tactic to determine that a recursive call is indeed
decreasing.
The process proceeds in these steps, to guide the transformation:
1. The parameters of the function are annotated with the `wfParam` gadget.
We could be more selective here and only annotate those that have a `SizeOf` instance.
We cannot (easily) only consider the parameters that appear in the termination measure, as that
is not known yet.
2. The `wfParam` gadget is pushed around:
- `f (wfParam x) ==> wfParam (f x)` if `f` is a projection
- `match (wfParam x) with con y => alt[y] ==> match x with con y => alt[wfParam y]`
In a match with multiple targets it suffices for any of the targets to be annotated with
`wfParam`, and all parameters of the match arms are annotated with `wfParam`. This is an
overapproximation.
3. The `wf_preprocess` simpset is applied to do the actual transformation. It typically contains two
rules for each higher-order function of interest
- `(wfParam xs).map f = xs.attach.unattach.map f`
- `xs.unattach.map f = xs.map (fun ⟨x, h⟩ => binderNameHint x f (f (wfParam x)))`
The first rule “activates” the call, the second rule actually performs it. They are separated like
this so that for chains of the form `(xs.reverse.filter p).map f` the `.attach` is attached
to `xs` and we get the basic `x ∈ xs` in the context of `f`.
The `binderNameHint` preserves the user-chosen name in `f` if that is a lambda.
The `wfParam` on the right hand side ensurses that doubly-nested recursion works.
4. All left-over `wfParam` gadgets are removed.
The simplifier is used to perform steps 2 (using simprocs) and 3 (using rewrite rules) together.
-/
open Lean Meta
register_builtin_option wf.preprocess : Bool := {
defValue := true
descr := "pre-process definitions defined by well-founded recursion with the `wf_preprocess` simp set"
}
namespace Lean.Elab.WF
open Meta
private def shouldBetaReduce (e : Expr) (recFnNames : Array Name) : Bool :=
if e.isHeadBetaTarget then
e.getAppFn.find? (fun e => recFnNames.any (e.isConstOf ·)) |>.isSome
builtin_initialize wfPreprocessSimpExtension : SimpExtension
registerSimpAttr `wf_preprocess
"simp lemma used in the preprocessing of well-founded recursive function definitions, in \
particular to add additional hypotheses to the context. Also see `wfParam`."
private def getSimpContext : MetaM Simp.Context := do
let simpTheorems wfPreprocessSimpExtension.getTheorems
Simp.mkContext
(simpTheorems := #[simpTheorems])
(congrTheorems := {})
(config := { Simp.neutralConfig with dsimp := false })
def isWfParam? (e : Expr) : Option Expr :=
if e.isAppOfArity ``wfParam 2 then
e.appArg!
else
false
none
/--
Preprocesses the expressions to improve the effectiveness of `wfRecursion`.
def mkWfParam (e : Expr) : MetaM Expr :=
mkAppM ``wfParam #[e]
* Floats out the RecApp markers.
Example:
```
def f : Nat → Nat
| 0 => 1
| i+1 => (f x) i
```
/-- `f (wfParam x) ==> wfParam (f x)` if `f` is a projection -/
builtin_dsimproc paramProj (_) := fun e => do
if h : e.isApp then
let some a' := isWfParam? (e.appArg h) | return .continue
let f := e.getAppFn
unless f.isConst do return .continue
unless ( isProjectionFn f.constName!) do return .continue
let e' mkWfParam (.app (e.appFn h) a')
return .done e'
else
return .continue
Unlike `Lean.Elab.Structural.preprocess`, do _not_ beta-reduce, as it could
remove `let_fun`-lambdas that contain explicit termination proofs.
-/
def preprocess (e : Expr) : CoreM Expr :=
Core.transform e
(post := fun e => do
if e.isApp && e.getAppFn.isMData then
let .mdata m f := e.getAppFn | unreachable!
if m.isRecApp then
return .done (.mdata m (f.beta e.getAppArgs))
return .continue)
/-- `match (wfParam x) with con y => alt[y] ==> match x with con y => alt[wfParam y] -/
builtin_dsimproc paramMatcher (_) := fun e => do
let some matcherApp matchMatcherApp? e (alsoCasesOn := true) | return .continue
unless matcherApp.discrs.any (isWfParam? · |>.isSome) do return .continue
let discrs' := matcherApp.discrs.map (fun e => isWfParam? e |>.getD e)
let alts' matcherApp.alts.mapM fun alt =>
lambdaTelescope alt fun xs body => do
-- Annotate all xs with `wfParam`
let xs' xs.mapM (mkWfParam ·)
let body' := body.replaceFVars xs xs'
mkLambdaFVars xs body'
let matcherApp' := { matcherApp with discrs := discrs', alts := alts' }
return .continue <| matcherApp'.toExpr
/-- `let x := (wfParam e); body[x] ==> let x := e; body[wfParam y] -/
builtin_dsimproc paramLet (_) := fun e => do
unless e.isLet do return .continue
let some v := isWfParam? e.letValue! | return .continue
let u getLevel e.letType!
let body' := e.letBody!.instantiate1 <|
mkApp2 (.const ``wfParam [u]) e.letType! (.bvar 0)
return .continue <| e.updateLet! e.letType! v body'
def preprocess (e : Expr) : MetaM Simp.Result := do
unless wf.preprocess.get ( getOptions) do
return { expr := e }
lambdaTelescope e fun xs _ => do
-- Annotate all xs with `wfParam`
let xs' xs.mapM mkWfParam
let e' := e.beta xs'
-- Now run the simplifier
let simprocs : Simprocs := {}
let simprocs simprocs.add ``paramProj (post := true)
let simprocs simprocs.add ``paramMatcher (post := false)
let simprocs simprocs.add ``paramLet (post := true)
let (result, _) Meta.simp e' ( getSimpContext) (simprocs := #[simprocs])
-- Remove left-over markers
let e'' Core.transform result.expr fun e =>
e.withApp fun f as => do
if f.isConstOf ``wfParam then
if h : as.size 2 then
return .continue (mkAppN as[1] as[2:])
return .continue
let result := { result with expr := e'' }
trace[Elab.definition.wf] "Attach-introduction:{indentExpr e}\nto{indentExpr e'}\ncleaned up as{indentExpr e''}"
result.addLambdas xs
end Lean.Elab.WF

View File

@@ -37,60 +37,60 @@ private def rwFixEq (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
mvarId.assign ( mkEqTrans h mvarNew)
return mvarNew.mvarId!
private partial def mkUnfoldProof (declName declNameNonRec : Name) (type : Expr) : MetaM Expr := do
trace[Elab.definition.wf.eqns] "proving: {type}"
withNewMCtxDepth do
let main mkFreshExprSyntheticOpaqueMVar type
let (_, mvarId) main.mvarId!.intros
let rec go (mvarId : MVarId) : MetaM Unit := do
trace[Elab.definition.wf.eqns] "step\n{MessageData.ofGoal mvarId}"
if withAtLeastTransparency .all (tryURefl mvarId) then
trace[Elab.definition.wf.eqns] "refl!"
return ()
else if ( tryContradiction mvarId) then
trace[Elab.definition.wf.eqns] "contradiction!"
return ()
else if let some mvarId simpMatch? mvarId then
trace[Elab.definition.wf.eqns] "simpMatch!"
go mvarId
else if let some mvarId simpIf? mvarId then
trace[Elab.definition.wf.eqns] "simpIf!"
go mvarId
else if let some mvarId whnfReducibleLHS? mvarId then
trace[Elab.definition.wf.eqns] "whnfReducibleLHS!"
go mvarId
private partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
trace[Elab.definition.wf.eqns] "step\n{MessageData.ofGoal mvarId}"
if withAtLeastTransparency .all (tryURefl mvarId) then
trace[Elab.definition.wf.eqns] "refl!"
return ()
else if ( tryContradiction mvarId) then
trace[Elab.definition.wf.eqns] "contradiction!"
return ()
else if let some mvarId simpMatch? mvarId then
trace[Elab.definition.wf.eqns] "simpMatch!"
mkUnfoldProof declName mvarId
else if let some mvarId simpIf? mvarId then
trace[Elab.definition.wf.eqns] "simpIf!"
mkUnfoldProof declName mvarId
else if let some mvarId whnfReducibleLHS? mvarId then
trace[Elab.definition.wf.eqns] "whnfReducibleLHS!"
mkUnfoldProof declName mvarId
else
let ctx Simp.mkContext (config := { dsimp := false, etaStruct := .none })
match ( simpTargetStar mvarId ctx (simprocs := {})).1 with
| TacticResultCNM.closed => return ()
| TacticResultCNM.modified mvarId =>
trace[Elab.definition.wf.eqns] "simp only!"
mkUnfoldProof declName mvarId
| TacticResultCNM.noChange =>
if let some mvarIds casesOnStuckLHS? mvarId then
trace[Elab.definition.wf.eqns] "case split into {mvarIds.size} goals"
mvarIds.forM (mkUnfoldProof declName)
else if let some mvarIds splitTarget? mvarId then
trace[Elab.definition.wf.eqns] "splitTarget into {mvarIds.length} goals"
mvarIds.forM (mkUnfoldProof declName)
else
let ctx Simp.mkContext (config := { dsimp := false, etaStruct := .none })
match ( simpTargetStar mvarId ctx (simprocs := {})).1 with
| TacticResultCNM.closed => return ()
| TacticResultCNM.modified mvarId =>
trace[Elab.definition.wf.eqns] "simp only!"
go mvarId
| TacticResultCNM.noChange =>
if let some mvarIds casesOnStuckLHS? mvarId then
trace[Elab.definition.wf.eqns] "case split into {mvarIds.size} goals"
mvarIds.forM go
else if let some mvarIds splitTarget? mvarId then
trace[Elab.definition.wf.eqns] "splitTarget into {mvarIds.length} goals"
mvarIds.forM go
else
-- At some point in the past, we looked for occurrences of Wf.fix to fold on the
-- LHS (introduced in 096e4eb), but it seems that code path was never used,
-- so #3133 removed it again (and can be recovered from there if this was premature).
throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"
-- At some point in the past, we looked for occurrences of Wf.fix to fold on the
-- LHS (introduced in 096e4eb), but it seems that code path was never used,
-- so #3133 removed it again (and can be recovered from there if this was premature).
throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"
let mvarId if declName != declNameNonRec then deltaLHS mvarId else pure mvarId
let mvarId rwFixEq mvarId
go mvarId
instantiateMVars main
def mkUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) : MetaM Unit := do
def mkUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) (wfPreprocessProof : Simp.Result) : MetaM Unit := do
withOptions (tactic.hygienic.set · false) do
let baseName := preDef.declName
lambdaTelescope preDef.value fun xs body => do
let us := preDef.levelParams.map mkLevelParam
let type mkEq (mkAppN (Lean.mkConst preDef.declName us) xs) body
let value mkUnfoldProof preDef.declName unaryPreDefName type
let lhs := mkAppN (Lean.mkConst preDef.declName us) xs
let type mkEq lhs body
let main mkFreshExprSyntheticOpaqueMVar type
let mvarId := main.mvarId!
let wfPreprocessProof Simp.mkCongr { expr := type.appFn! } ( wfPreprocessProof.addExtraArgs xs)
let mvarId applySimpResultToTarget mvarId type wfPreprocessProof
let mvarId if preDef.declName != unaryPreDefName then deltaLHS mvarId else pure mvarId
let mvarId rwFixEq mvarId
mkUnfoldProof preDef.declName mvarId
let value instantiateMVars main
let type mkForallFVars xs type
let value mkLambdaFVars xs value
let name := Name.str baseName unfoldThmSuffix

View File

@@ -22,7 +22,6 @@ import Lean.Elab.Tactic.Conv
import Lean.Elab.Tactic.Delta
import Lean.Elab.Tactic.Meta
import Lean.Elab.Tactic.Unfold
import Lean.Elab.Tactic.Cache
import Lean.Elab.Tactic.Calc
import Lean.Elab.Tactic.Congr
import Lean.Elab.Tactic.Guard
@@ -50,3 +49,4 @@ import Lean.Elab.Tactic.Try
import Lean.Elab.Tactic.AsAuxLemma
import Lean.Elab.Tactic.TreeTacAttr
import Lean.Elab.Tactic.ExposeNames
import Lean.Elab.Tactic.SimpArith

View File

@@ -42,7 +42,7 @@ def lratChecker (ctx : TacticContext) (bvExpr : BVLogicalExpr) : MetaM Expr := d
@[inherit_doc Lean.Parser.Tactic.bvCheck]
def bvCheck (g : MVarId) (ctx : TacticContext) : MetaM Unit := do
let unsatProver : UnsatProver := fun _ reflectionResult _ => do
withTraceNode `sat (fun _ => return "Preparing LRAT reflection term") do
withTraceNode `Meta.Tactic.sat (fun _ => return "Preparing LRAT reflection term") do
let proof lratChecker ctx reflectionResult.bvExpr
return .ok proof, ""
let _ closeWithBVReflection g unsatProver

View File

@@ -114,6 +114,7 @@ The result of a spurious counter example diagnosis.
structure Diagnosis where
uninterpretedSymbols : Std.HashSet Expr := {}
unusedRelevantHypotheses : Std.HashSet FVarId := {}
derivedEquations : Array (Expr × Expr) := #[]
abbrev DiagnosisM : Type Type := ReaderT CounterExample <| StateRefT Diagnosis MetaM
@@ -124,18 +125,26 @@ def run (x : DiagnosisM Unit) (counterExample : CounterExample) : MetaM Diagnosi
let (_, issues) ReaderT.run x counterExample |>.run {}
return issues
@[inline]
def unusedHyps : DiagnosisM (Std.HashSet FVarId) := do
return ( read).unusedHypotheses
@[inline]
def equations : DiagnosisM (Array (Expr × BVExpr.PackedBitVec)) := do
return ( read).equations
@[inline]
def addUninterpretedSymbol (e : Expr) : DiagnosisM Unit :=
modify fun s => { s with uninterpretedSymbols := s.uninterpretedSymbols.insert e }
@[inline]
def addUnusedRelevantHypothesis (fvar : FVarId) : DiagnosisM Unit :=
modify fun s => { s with unusedRelevantHypotheses := s.unusedRelevantHypotheses.insert fvar }
@[inline]
def addDerivedEquation (var : Expr) (value : Expr) : DiagnosisM Unit :=
modify fun s => { s with derivedEquations := s.derivedEquations.push (var, value) }
def checkRelevantHypsUsed (fvar : FVarId) : DiagnosisM Unit := do
for hyp in unusedHyps do
if ( hyp.getType).containsFVar fvar then
@@ -147,26 +156,51 @@ Diagnose spurious counter examples, currently this checks:
- Whether all hypotheses which contain any variable that was bitblasted were included
-/
def diagnose : DiagnosisM Unit := do
for (expr, _) in equations do
match findRelevantFVar expr with
| some fvarId => checkRelevantHypsUsed fvarId
| none => addUninterpretedSymbol expr
for (var, value) in equations do
let (var, value) transformEquation var value
addDerivedEquation var value
match var with
| .fvar fvarId => checkRelevantHypsUsed fvarId
| _ => addUninterpretedSymbol var
where
findRelevantFVar (expr : Expr) : Option FVarId :=
match fvarId? expr with
| some fvarId => some fvarId
| none =>
match_expr expr with
| BitVec.ofBool x => fvarId? x
| UInt8.toBitVec x => fvarId? x
| UInt16.toBitVec x => fvarId? x
| UInt32.toBitVec x => fvarId? x
| UInt64.toBitVec x => fvarId? x
| _ => none
fvarId? (expr : Expr) : Option FVarId :=
match expr with
| .fvar fvarId => some fvarId
| _ => none
transformEquation (var : Expr) (value : BVExpr.PackedBitVec) : DiagnosisM (Expr × Expr) := do
if var.isFVar then
return (var, toExpr value.bv)
else
match_expr var with
| BitVec.ofBool x =>
return (x, toExpr <| value.bv == 1)
| UInt8.toBitVec x =>
if h : value.w = 8 then
return (x, toExpr <| UInt8.ofBitVec (h value.bv))
else
throwError m!"Value for UInt8 was not 8 bit but {value.w} bit"
| UInt16.toBitVec x =>
if h : value.w = 16 then
return (x, toExpr <| UInt16.ofBitVec (h value.bv))
else
throwError m!"Value for UInt16 was not 16 bit but {value.w} bit"
| UInt32.toBitVec x =>
if h : value.w = 32 then
return (x, toExpr <| UInt32.ofBitVec (h value.bv))
else
throwError m!"Value for UInt32 was not 32 bit but {value.w} bit"
| UInt64.toBitVec x =>
if h : value.w = 64 then
return (x, toExpr <| UInt64.ofBitVec (h value.bv))
else
throwError m!"Value for UInt64 was not 64 bit but {value.w} bit"
| _ =>
match var with
| .app (.const (.str p s) []) arg =>
if s == Normalize.enumToBitVecSuffix then
let .inductInfo inductiveInfo getConstInfo p | unreachable!
let ctors := inductiveInfo.ctors
let enumVal := mkConst ctors[value.bv.toNat]!
return (arg, enumVal)
else
return (var, toExpr value.bv)
| _ => return (var, toExpr value.bv)
end DiagnosisM
@@ -189,20 +223,26 @@ def explainCounterExampleQuality (counterExample : CounterExample) : MetaM Messa
let folder acc explainer := if let some m := explainer diagnosis then acc.push m else acc
let explanations := explainers.foldl (init := #[]) folder
let mut err := m!""
if explanations.isEmpty then
return m!"The prover found a counterexample, consider the following assignment:\n"
err := err ++ m!"The prover found a counterexample, consider the following assignment:\n"
else
let mut err := m!"The prover found a potentially spurious counterexample:\n"
err := err ++ m!"The prover found a potentially spurious counterexample:\n"
err := err ++ explanations.foldl (init := m!"") (fun acc exp => acc ++ m!"- " ++ exp ++ m!"\n")
err := err ++ m!"Consider the following assignment:\n"
return err
let folder := fun error (var, value) => error ++ m!"{var} = {value}\n"
err := diagnosis.derivedEquations.foldl (init := err) folder
return err
def lratBitblaster (goal : MVarId) (ctx : TacticContext) (reflectionResult : ReflectionResult)
(atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool)) :
MetaM (Except CounterExample UnsatProver.Result) := do
let bvExpr := reflectionResult.bvExpr
let entry
withTraceNode `bv (fun _ => return "Bitblasting BVLogicalExpr to AIG") do
withTraceNode `Meta.Tactic.bv (fun _ => return "Bitblasting BVLogicalExpr to AIG") do
-- lazyPure to prevent compiler lifting
IO.lazyPure (fun _ => bvExpr.bitblast)
let aigSize := entry.aig.decls.size
@@ -212,7 +252,7 @@ def lratBitblaster (goal : MVarId) (ctx : TacticContext) (reflectionResult : Ref
IO.FS.writeFile ("." / "aig.gv") <| AIG.toGraphviz entry
let (cnf, map)
withTraceNode `sat (fun _ => return "Converting AIG to CNF") do
withTraceNode `Meta.Tactic.sat (fun _ => return "Converting AIG to CNF") do
-- lazyPure to prevent compiler lifting
IO.lazyPure (fun _ =>
let (entry, map) := entry.relabelNat'
@@ -221,7 +261,7 @@ def lratBitblaster (goal : MVarId) (ctx : TacticContext) (reflectionResult : Ref
)
let res
withTraceNode `sat (fun _ => return "Obtaining external proof certificate") do
withTraceNode `Meta.Tactic.sat (fun _ => return "Obtaining external proof certificate") do
runExternal cnf ctx.solver ctx.lratPath ctx.config.trimProofs ctx.config.timeout ctx.config.binaryProofs
match res with
@@ -264,7 +304,7 @@ def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :
MetaM (Except CounterExample LratCert) := M.run do
g.withContext do
let reflectionResult
withTraceNode `bv (fun _ => return "Reflecting goal into BVLogicalExpr") do
withTraceNode `Meta.Tactic.bv (fun _ => return "Reflecting goal into BVLogicalExpr") do
reflectBV g
trace[Meta.Tactic.bv] "Reflected bv logical expression: {reflectionResult.bvExpr}"
@@ -280,7 +320,7 @@ def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :
def bvUnsat (g : MVarId) (ctx : TacticContext) : MetaM (Except CounterExample LratCert) := M.run do
let unsatProver : UnsatProver := fun g reflectionResult atomsAssignment => do
withTraceNode `bv (fun _ => return "Preparing LRAT reflection term") do
withTraceNode `Meta.Tactic.bv (fun _ => return "Preparing LRAT reflection term") do
lratBitblaster g ctx reflectionResult atomsAssignment
closeWithBVReflection g unsatProver
@@ -314,9 +354,7 @@ def bvDecide (g : MVarId) (ctx : TacticContext) : MetaM Result := do
| .error counterExample =>
counterExample.goal.withContext do
let error explainCounterExampleQuality counterExample
let folder := fun error (var, value) => error ++ m!"{var} = {value.bv}\n"
let errorMessage := counterExample.equations.foldl (init := error) folder
throwError ( addMessageContextFull errorMessage)
throwError ( addMessageContextFull error)
@[builtin_tactic Lean.Parser.Tactic.bvDecide]
def evalBvDecide : Tactic := fun

View File

@@ -99,7 +99,7 @@ instance : ToExpr LRAT.IntAction where
def LratCert.load (lratPath : System.FilePath) (trimProofs : Bool) : CoreM (Array LRAT.IntAction) := do
let proofInput IO.FS.readBinFile lratPath
let proof
withTraceNode `sat (fun _ => return s!"Parsing LRAT file") do
withTraceNode `Meta.Tactic.sat (fun _ => return s!"Parsing LRAT file") do
-- lazyPure to prevent compiler lifting
let proof? IO.lazyPure (fun _ => LRAT.parseLRATProof proofInput)
match proof? with
@@ -110,7 +110,7 @@ def LratCert.load (lratPath : System.FilePath) (trimProofs : Bool) : CoreM (Arra
let proof
if trimProofs then
withTraceNode `sat (fun _ => return "Trimming LRAT proof") do
withTraceNode `Meta.Tactic.sat (fun _ => return "Trimming LRAT proof") do
-- lazyPure to prevent compiler lifting
let trimmed IO.lazyPure (fun _ => LRAT.trim proof)
IO.ofExcept trimmed
@@ -137,19 +137,19 @@ def runExternal (cnf : CNF Nat) (solver : System.FilePath) (lratPath : System.Fi
(trimProofs : Bool) (timeout : Nat) (binaryProofs : Bool) :
CoreM (Except (Array (Bool × Nat)) LratCert) := do
IO.FS.withTempFile fun cnfHandle cnfPath => do
withTraceNode `sat (fun _ => return "Serializing SAT problem to DIMACS file") do
withTraceNode `Meta.Tactic.sat (fun _ => return "Serializing SAT problem to DIMACS file") do
-- lazyPure to prevent compiler lifting
cnfHandle.putStr ( IO.lazyPure (fun _ => cnf.dimacs))
cnfHandle.flush
let res
withTraceNode `sat (fun _ => return "Running SAT solver") do
withTraceNode `Meta.Tactic.sat (fun _ => return "Running SAT solver") do
External.satQuery solver cnfPath lratPath timeout binaryProofs
if let .sat assignment := res then
return .error assignment
let lratProof
withTraceNode `sat (fun _ => return "Obtaining LRAT certificate") do
withTraceNode `Meta.Tactic.sat (fun _ => return "Obtaining LRAT certificate") do
LratCert.ofFile lratPath trimProofs
return .ok lratProof
@@ -177,18 +177,18 @@ function together with a correctness theorem for it.
-/
def LratCert.toReflectionProof [ToExpr α] (cert : LratCert) (cfg : TacticContext) (reflected : α)
(verifier : Name) (unsat_of_verifier_eq_true : Name) : MetaM Expr := do
withTraceNode `sat (fun _ => return "Compiling expr term") do
withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling expr term") do
mkAuxDecl cfg.exprDef (toExpr reflected) (toTypeExpr α)
let certType := toTypeExpr LratCert
withTraceNode `sat (fun _ => return "Compiling proof certificate term") do
withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling proof certificate term") do
mkAuxDecl cfg.certDef (toExpr cert) certType
let reflectedExpr := mkConst cfg.exprDef
let certExpr := mkConst cfg.certDef
withTraceNode `sat (fun _ => return "Compiling reflection proof term") do
withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling reflection proof term") do
let auxValue := mkApp2 (mkConst verifier) reflectedExpr certExpr
mkAuxDecl cfg.reflectionDef auxValue (mkConst ``Bool)
@@ -203,7 +203,7 @@ def LratCert.toReflectionProof [ToExpr α] (cert : LratCert) (cfg : TacticContex
let auxLemma
-- disable async TC so we can catch its exceptions
withOptions (Elab.async.set · false) do
withTraceNode `sat (fun _ => return "Verifying LRAT certificate") do
withTraceNode `Meta.Tactic.sat (fun _ => return "Verifying LRAT certificate") do
mkAuxLemma [] auxType auxProof
return mkApp3 (mkConst unsat_of_verifier_eq_true) reflectedExpr certExpr (mkConst auxLemma)
catch e =>

View File

@@ -13,6 +13,7 @@ import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.EmbeddedConstraint
import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.AC
import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Structures
import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.IntToBitVec
import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Enums
import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.TypeAnalysis
/-!
@@ -42,7 +43,7 @@ def passPipeline : PreProcessM (List Pass) := do
return passPipeline
def bvNormalize (g : MVarId) (cfg : BVDecideConfig) : MetaM (Option MVarId) := do
withTraceNode `bv (fun _ => return "Preprocessing goal") do
withTraceNode `Meta.Tactic.bv (fun _ => return "Preprocessing goal") do
(go g).run cfg g
where
go (g : MVarId) : PreProcessM (Option MVarId) := do
@@ -59,6 +60,10 @@ where
let some g' structuresPass.run g | return none
g := g'
if cfg.enums then
let some g' enumsPass.run g | return none
g := g'
if cfg.fixedInt then
let some g' intToBitVecPass.run g | return none
g := g'

View File

@@ -109,7 +109,7 @@ namespace Pass
@[inline]
def run (pass : Pass) (goal : MVarId) : PreProcessM (Option MVarId) := do
withTraceNode `bv (fun _ => return m!"Running pass: {pass.name} on\n{goal}") do
withTraceNode `Meta.Tactic.bv (fun _ => return m!"Running pass: {pass.name} on\n{goal}") do
pass.run' goal
/--

View File

@@ -0,0 +1,312 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
prelude
import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Basic
import Lean.Meta.Tactic.Simp
/-!
This module contains the implementation of the pre processing pass for handling equality on
enum inductive types.
The implementation generates mappings from enum inductives occuring in the goal to sufficiently
large `BitVec` and replaces equality on the enum inductives with equality on these mapping
functions.
-/
namespace Lean.Elab.Tactic.BVDecide
namespace Frontend.Normalize
open Lean.Meta
private def getBitVecSize (domainSize : Nat) : Nat :=
let bvSize := Nat.log2 domainSize
if 2^bvSize == domainSize then
bvSize
else
bvSize + 1
def enumToBitVecSuffix : String := "enumToBitVec"
def eqIffEnumToBitVecEqSuffix : String := "eq_iff_enumToBitVec_eq"
def enumToBitVecLeSuffix : String := "enumToBitVec_le"
/--
Assuming that `declName` is an enum inductive construct a function of type `declName → BitVec w`
that maps `declName` constructors to their numeric indices as `BitVec`.
-/
def getEnumToBitVecFor (declName : Name) : MetaM Name := do
let env getEnv
let enumToBitVecName := Name.str declName enumToBitVecSuffix
if env.contains enumToBitVecName then
return enumToBitVecName
else
let .inductInfo inductiveInfo getConstInfo declName | throwError m!"{declName} is not an inductive."
if !( isEnumType declName) then
throwError m!"{declName} is not an enum inductive."
let domainSize := inductiveInfo.ctors.length
let bvSize := getBitVecSize domainSize
let bvType := mkApp (mkConst ``BitVec) (toExpr bvSize)
let declType := mkConst declName
let translator
withLocalDeclD `x declType fun x => do
let motive := mkLambda .anonymous .default declType bvType
let recOn := mkApp2 (mkConst (mkRecOnName declName) [1]) motive x
let translator :=
Nat.fold
domainSize
(init := recOn)
(fun i _ acc => mkApp acc <| toExpr <| BitVec.ofNat bvSize i)
mkLambdaFVars #[x] translator
addDecl <| .defnDecl {
name := enumToBitVecName
type := ( mkArrow declType bvType)
levelParams := []
value := translator
hints := .regular (getMaxHeight env translator + 1)
safety := .safe
}
return enumToBitVecName
/--
Assuming that `declName` is an enum inductive, construct a proof of
`∀ (x y : declName) : x = y ↔ x.enumToBitVec = y.enumToBitVec`.
-/
def getEqIffEnumToBitVecEqFor (declName : Name) : MetaM Name := do
let env getEnv
let eqIffEnumToBitVecEqName := Name.str declName eqIffEnumToBitVecEqSuffix
if env.contains eqIffEnumToBitVecEqName then
return eqIffEnumToBitVecEqName
else
/-
We prove the lemma by constructing an inverse to `enumToBitVec` and use the fact that all
invertible functions respect equality.
-/
let enumToBitVec := mkConst ( getEnumToBitVecFor declName)
let .inductInfo inductiveInfo getConstInfo declName | unreachable!
let ctors := inductiveInfo.ctors
let domainSize := ctors.length
let bvSize := getBitVecSize domainSize
let bvType := mkApp (mkConst ``BitVec) (toExpr bvSize)
let declType := mkConst declName
-- ∀ (x y : declName), x = y ↔ enumToBitVec x = enumToBitVec y
let type
withLocalDeclD `x declType fun x =>
withLocalDeclD `y declType fun y => do
let lhs := mkApp3 (mkConst ``Eq [1]) declType x y
let rhs :=
mkApp3
(mkConst ``Eq [1])
bvType
(mkApp enumToBitVec x)
(mkApp enumToBitVec y)
let statement := mkApp2 (mkConst ``Iff) lhs rhs
mkForallFVars #[x, y] statement
-- the inverse of enumToBitVec
let inverseValue
withLocalDeclD `x bvType fun x => do
let instBeq synthInstance (mkApp (mkConst ``BEq [0]) bvType)
let inv := mkInverse x declType instBeq ctors (BitVec.ofNat bvSize 0) (mkConst ctors.head!)
mkLambdaFVars #[x] inv
let value
withLetDecl `inverse ( mkArrow bvType declType) inverseValue fun inv => do
let invProof
withLocalDeclD `x declType fun x => do
let toBvToEnum e := mkApp inv (mkApp enumToBitVec e)
let motive
withLocalDeclD `y declType fun y =>
mkLambdaFVars #[y] <| mkApp3 (mkConst ``Eq [1]) declType (toBvToEnum y) y
let recOn := mkApp2 (mkConst (mkRecOnName declName) [0]) motive x
let folder acc ctor :=
let case := mkApp2 (mkConst ``Eq.refl [1]) declType (toBvToEnum (mkConst ctor))
mkApp acc case
let proof := List.foldl (init := recOn) folder ctors
mkLambdaFVars #[x] proof
let value :=
mkApp5
(mkConst ``BitVec.eq_iff_eq_of_inv [1])
declType
(toExpr bvSize)
enumToBitVec
inv
invProof
mkLetFVars #[inv] value
addDecl <| .thmDecl {
name := eqIffEnumToBitVecEqName
levelParams := []
type := type
value := value
}
return eqIffEnumToBitVecEqName
where
mkInverse {w : Nat} (input : Expr) (retType : Expr) (instBEq : Expr) (ctors : List Name)
(counter : BitVec w) (acc : Expr) :
Expr :=
match ctors with
| [] => acc
| ctor :: ctors =>
let eq :=
mkApp4
(mkConst ``BEq.beq [0])
(toTypeExpr <| BitVec w)
instBEq
input
(toExpr counter)
let acc := mkApp4 (mkConst ``cond [0]) retType eq (mkConst ctor) acc
mkInverse input retType instBEq ctors (counter + 1) acc
/--
Assuming that `declName` is an enum inductive, construct a proof of
`∀ (x : declName) : x.enumToBitVec ≤ domainSize - 1` where `domainSize` is the amount of
constructors of `declName`.
-/
def getEnumToBitVecLeFor (declName : Name) : MetaM Name := do
let env getEnv
let enumToBitVecLeName := Name.str declName enumToBitVecLeSuffix
if env.contains enumToBitVecLeName then
return enumToBitVecLeName
else
let enumToBitVec := mkConst ( getEnumToBitVecFor declName)
let .inductInfo inductiveInfo getConstInfo declName | unreachable!
let ctors := inductiveInfo.ctors
let domainSize := ctors.length
let bvSize := getBitVecSize domainSize
let bvType := mkApp (mkConst ``BitVec) (toExpr bvSize)
let declType := mkConst declName
let maxValue := toExpr (BitVec.ofNat bvSize (domainSize - 1))
let instLe synthInstance (mkApp (mkConst ``LE [0]) bvType)
let mkStatement e := mkApp4 (mkConst ``LE.le [0]) bvType instLe (mkApp enumToBitVec e) maxValue
-- ∀ (x : declName), enumToBitVec x ≤ BitVec.ofNat bvSize (domainSize - 1)
let (type, motive)
withLocalDeclD `x declType fun x => do
let statement := mkStatement x
return ( mkForallFVars #[x] statement, mkLambdaFVars #[x] statement)
let value
withLocalDeclD `x declType fun x => do
let recOn := mkApp2 (mkConst (mkRecOnName declName) [0]) motive x
let folder acc ctor := do
let statement := mkStatement (mkConst ctor)
let proof mkDecideProof statement
return mkApp acc proof
let cases List.foldlM (init := recOn) folder ctors
mkLambdaFVars #[x] cases
addDecl <| .thmDecl {
name := enumToBitVecLeName
levelParams := []
type := type
value := value
}
return enumToBitVecLeName
builtin_initialize
registerReservedNamePredicate fun _ name => Id.run do
let .str _ s := name | return false
s == enumToBitVecSuffix || s == eqIffEnumToBitVecEqSuffix || s == enumToBitVecLeSuffix
builtin_initialize
registerReservedNameAction fun name => do
let .str p s := name | return false
unless isEnumType p do return false
if s == enumToBitVecSuffix then
discard <| MetaM.run' (getEnumToBitVecFor p)
return true
else if s == eqIffEnumToBitVecEqSuffix then
discard <| MetaM.run' (getEqIffEnumToBitVecEqFor p)
return true
else if s == enumToBitVecLeSuffix then
discard <| MetaM.run' (getEnumToBitVecLeFor p)
return true
else
return false
builtin_simproc enumsPassPost ((_ : BitVec _) = (_ : BitVec _)) := fun e => do
let_expr Eq α lhs rhs := e | return .continue
let transform (e : Expr) : MetaM (Option Expr) := do
let .app (.const fn []) (.const arg []) := e | return none
let .str p s := fn | return none
if s != enumToBitVecSuffix then return none
if !( isEnumType p) then return none
let .inductInfo inductiveInfo getConstInfo p | unreachable!
let ctors := inductiveInfo.ctors
let some ctorIdx := ctors.findIdx? (· == arg) | return none
let bvSize := getBitVecSize ctors.length
return some <| toExpr <| BitVec.ofNat bvSize ctorIdx
let newLhs? : Option Expr transform lhs
let newRhs? : Option Expr transform rhs
match newLhs?, newRhs? with
| .none, .none => return .continue
| newLhs?, newRhs? =>
let newLhs := newLhs?.getD lhs
let newRhs := newRhs?.getD rhs
return .visit { expr := mkApp3 (mkConst ``Eq [1]) α newLhs newRhs }
partial def enumsPass : Pass where
name := `enums
run' goal :=
goal.withContext do
let interesting := ( PreProcessM.getTypeAnalysis).interestingEnums
if interesting.isEmpty then return goal
let mut relevantLemmas : SimpTheoremsArray := #[]
relevantLemmas relevantLemmas.addTheorem (.decl ``ne_eq) ( mkConstWithLevelParams ``ne_eq)
for type in interesting do
let lemma getEqIffEnumToBitVecEqFor type
relevantLemmas relevantLemmas.addTheorem (.decl lemma) (mkConst lemma)
let cfg PreProcessM.getConfig
let simpCtx Simp.mkContext
(config := { failIfUnchanged := false, maxSteps := cfg.maxSteps })
(simpTheorems := relevantLemmas)
(congrTheorems := getSimpCongrTheorems)
let simprocs Simp.SimprocsArray.add #[] ``enumsPassPost true
let result?, _
simpGoal
goal
(ctx := simpCtx)
(simprocs := simprocs)
(fvarIdsToSimp := getPropHyps)
let some (_, newGoal) := result? | return none
postprocess newGoal |>.run' {}
where
postprocess (goal : MVarId) : StateRefT (Array Hypothesis) MetaM MVarId :=
goal.withContext do
let filter e :=
if let .app (.const (.str _ s) []) _ := e then
s == enumToBitVecSuffix
else
false
let processor e := do
let .app (.const (.str enumType _) []) val := e | unreachable!
let lemma := mkConst ( getEnumToBitVecLeFor enumType)
let value := mkApp lemma val
let type inferType value
let hyp := { userName := .anonymous, type, value }
modify fun s => s.push hyp
for hyp in getPropHyps do
( hyp.getType).forEachWhere (stopWhenVisited := true) filter processor
let hyps get
if hyps.isEmpty then
return goal
else
let (_, goal) goal.assertHypotheses hyps
return goal
end Frontend.Normalize
end Lean.Elab.Tactic.BVDecide

View File

@@ -218,5 +218,53 @@ builtin_simproc [bv_normalize] bv_allOnes_eq_and ((_ : BitVec _) == (_ : BitVec
rrhs
return .visit { expr := expr, proof? := some proof }
builtin_simproc [bv_normalize] bv_extractLsb'_not (BitVec.extractLsb' _ _ (~~~(_ : BitVec _))) :=
fun e => do
let_expr BitVec.extractLsb' initialWidth start len inner := e | return .continue
let some initialWidthVal getNatValue? initialWidth | return .continue
let some startVal getNatValue? start | return .continue
let some lenVal getNatValue? len | return .continue
if !(startVal + lenVal) < initialWidthVal then return .continue
let_expr Complement.complement _ _ inner := inner | return .continue
let newInner := mkApp4 (mkConst ``BitVec.extractLsb') initialWidth start len inner
let expr mkAppM ``Complement.complement #[newInner]
let lt mkDecideProof ( mkAppM ``LT.lt #[( mkAppM ``HAdd.hAdd #[start, len]), initialWidth])
let proof := mkApp5 (mkConst ``BitVec.extractLsb'_not_of_lt) initialWidth inner start len lt
return .visit { expr := expr, proof? := some proof }
def isTwoPow (x : BitVec w) : Option Nat :=
if x == 0#w then
none
else
go x 0
where
go {w : Nat} (x : BitVec w) (counter : Nat) : Option Nat :=
if counter < w then
let attempt := 1#w <<< counter
if attempt == x then
some counter
else
go x (counter + 1)
else
none
builtin_simproc [bv_normalize] bv_twoPow_mul ((BitVec.ofNat _ _) * (_ : BitVec _)) :=
fun e => do
let_expr HMul.hMul _ _ _ _ lhsExpr rhs := e | return .continue
let some w, lhs getBitVecValue? lhsExpr | return .continue
let some pow := isTwoPow lhs | return .continue
let expr mkAppM ``HShiftLeft.hShiftLeft #[rhs, toExpr pow]
let proof := mkApp3 (mkConst ``BitVec.twoPow_mul_eq_shiftLeft) (toExpr w) rhs (toExpr pow)
return .visit { expr := expr, proof? := some proof }
builtin_simproc [bv_normalize] bv_mul_twoPow ((_ : BitVec _) * (BitVec.ofNat _ _)) :=
fun e => do
let_expr HMul.hMul _ _ _ _ lhs rhsExpr := e | return .continue
let some w, rhs getBitVecValue? rhsExpr | return .continue
let some pow := isTwoPow rhs | return .continue
let expr mkAppM ``HShiftLeft.hShiftLeft #[lhs, toExpr pow]
let proof := mkApp3 (mkConst ``BitVec.mul_twoPow_eq_shiftLeft) (toExpr w) lhs (toExpr pow)
return .visit { expr := expr, proof? := some proof }
end Frontend.Normalize
end Lean.Elab.Tactic.BVDecide

View File

@@ -7,6 +7,11 @@ Authors: Tobias Grosser
prelude
import Lean.Meta.Tactic.Simp.Attr
builtin_initialize bool_to_prop : Lean.Meta.SimpExtension
Lean.Meta.registerSimpAttr `bool_to_prop
"simp lemmas converting boolean expressions in terms of `decide` into propositional statements"
@[deprecated bool_to_prop (since := "2025-02-10")]
builtin_initialize boolToPropSimps : Lean.Meta.SimpExtension
Lean.Meta.registerSimpAttr `boolToPropSimps
"simp lemmas converting boolean expressions in terms of `decide` into propositional statements"

View File

@@ -135,70 +135,6 @@ where
@[builtin_tactic paren, builtin_incremental] def evalParen : Tactic :=
Term.withNarrowedArgTacticReuse 1 evalTactic
def isCheckpointableTactic (arg : Syntax) : TacticM Bool := do
-- TODO: make it parametric
let kind := arg.getKind
return kind == ``Lean.Parser.Tactic.save
/--
Takes a `sepByIndent tactic "; "`, and inserts `checkpoint` blocks for `save` tactics.
Input:
```
a
b
save
c
d
save
e
```
Output:
```
checkpoint
a
b
save
checkpoint
c
d
save
e
```
-/
-- Note that we need to preserve the separators to show the right goals after semicolons.
def addCheckpoints (stx : Syntax) : TacticM Syntax := do
if !( stx.getSepArgs.anyM isCheckpointableTactic) then return stx
-- do not checkpoint checkpointable tactic by itself to prevent infinite recursion
-- TODO: rethink approach if we add non-trivial checkpointable tactics
if stx.getNumArgs <= 2 then return stx
let mut currentCheckpointBlock := #[]
let mut output := #[]
-- `+ 1` to account for optional trailing separator
for i in [:(stx.getArgs.size + 1) / 2] do
let tac := stx[2*i]
let sep? := stx.getArgs[2*i+1]?
if ( isCheckpointableTactic tac) then
let checkpoint : Syntax :=
mkNode ``checkpoint #[
mkAtomFrom tac "checkpoint",
mkNode ``tacticSeq #[
mkNode ``tacticSeq1Indented #[
-- HACK: null node is not a valid tactic, but prevents infinite loop
mkNullNode (currentCheckpointBlock.push (mkNullNode #[tac]))
]
]
]
currentCheckpointBlock := #[]
output := output.push checkpoint
if let some sep := sep? then output := output.push sep
else
currentCheckpointBlock := currentCheckpointBlock.push tac
if let some sep := sep? then currentCheckpointBlock := currentCheckpointBlock.push sep
output := output ++ currentCheckpointBlock
return stx.setArgs output
@[builtin_tactic tacticSeq1Indented, builtin_incremental]
def evalTacticSeq1Indented : Tactic :=
Term.withNarrowedArgTacticReuse (argIdx := 0) evalSepTactics

View File

@@ -1,81 +0,0 @@
/-
Copyright (c) 2022 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Elab.Tactic.Basic
namespace Lean.Elab.Tactic
open Meta
private def equivMVarDecl (d₁ d₂ : MetavarDecl) : Bool :=
d₁.type == d₂.type
-- The following additional check does not seem to be necessary
/-
&&
d₁.lctx.decls.size == d₂.lctx.decls.size &&
Id.run do
for i in [:d₁.lctx.decls.size] do
match d₁.lctx.decls[i], d₂.lctx.decls[i] with
| some localDecl₁, some localDecl₂ => if localDecl₁.type != localDecl₂.type then return false
| none, none => pure ()
| _, _ => return false
return true
-/
register_builtin_option tactic.dbg_cache : Bool := {
defValue := false
group := "tactic"
descr := "enable tactic cache debug messages (remark: they are sent to the standard error)"
}
private def dbg_cache (msg : String) : TacticM Unit := do
if tactic.dbg_cache.get ( getOptions) then
dbg_trace msg
private def dbg_cache' (cacheRef : IO.Ref Cache) (pos : String.Pos) (mvarId : MVarId) (msg : String) : TacticM Unit := do
if tactic.dbg_cache.get ( getOptions) then
let {line, column} := ( getFileMap).toPosition pos
dbg_trace "{msg}, line: {line}, column: {column}, contains entry: {(← cacheRef.get).pre.find? { mvarId, pos } |>.isSome}"
private def findCache? (cacheRef : IO.Ref Cache) (mvarId : MVarId) (stx : Syntax) (pos : String.Pos) : TacticM (Option Snapshot) := do
let some s := ( cacheRef.get).pre.find? { mvarId, pos } | do dbg_cache "cache key not found"; return none
let mvarDecl mvarId.getDecl
let some mvarDeclOld := s.meta.mctx.findDecl? mvarId | return none
if equivMVarDecl mvarDecl mvarDeclOld then
if stx == s.stx then
return some s
else
dbg_cache "syntax is different"
return none
else
dbg_cache "cached state is not compatible"
return none
@[builtin_tactic checkpoint] def evalCheckpoint : Tactic := fun stx =>
focus do
let mvarId getMainGoal
let some cacheRef := ( readThe Term.Context).tacticCache? | evalTactic stx[1]
let some pos := stx.getPos? | evalTactic stx[1]
match ( findCache? cacheRef mvarId stx[1] pos) with
| some s =>
cacheRef.modify fun { pre, post } => { pre, post := post.insert { mvarId, pos } s }
set s.core
set s.meta
set s.term
set s.tactic
dbg_cache' cacheRef pos mvarId "cache hit"
| none =>
evalTactic stx[1]
let s := {
stx := stx[1]
core := ( getThe Core.State)
meta := ( getThe Meta.State)
term := ( getThe Term.State)
tactic := ( get)
}
dbg_cache' cacheRef pos mvarId "cache miss"
cacheRef.modify fun { pre, post } => { pre, post := post.insert { mvarId, pos } s }
end Lean.Elab.Tactic

View File

@@ -174,8 +174,27 @@ def evalGrindCore
replaceMainGoal []
return result
/-- Position for the `[..]` child syntax in the `grind` tactic. -/
def grindParamsPos := 3
/-- Position for the `only` child syntax in the `grind` tactic. -/
def grindOnlyPos := 2
def isGrindOnly (stx : TSyntax `tactic) : Bool :=
stx.raw.getKind == ``Parser.Tactic.grind && !stx.raw[grindOnlyPos].isNone
def setGrindParams (stx : TSyntax `tactic) (params : Array Syntax) : TSyntax `tactic :=
if params.isEmpty then
stx.raw.setArg grindParamsPos (mkNullNode)
else
let paramsStx := #[mkAtom "[", (mkAtom ",").mkSep params, mkAtom "]"]
stx.raw.setArg grindParamsPos (mkNullNode paramsStx)
def getGrindParams (stx : TSyntax `tactic) : Array Syntax :=
stx.raw[grindParamsPos][1].getSepArgs
def mkGrindOnly
(config : TSyntax `Lean.Parser.Tactic.optConfig)
(config : TSyntax ``Lean.Parser.Tactic.optConfig)
(fallback? : Option Term)
(trace : Grind.Trace)
: MetaM (TSyntax `tactic) := do
@@ -218,11 +237,7 @@ def mkGrindOnly
`(tactic| grind $config:optConfig only on_failure $fallback)
else
`(tactic| grind $config:optConfig only)
if params.isEmpty then
return result
else
let paramsStx := #[mkAtom "[", (mkAtom ",").mkSep params, mkAtom "]"]
return result.raw.setArg 3 (mkNullNode paramsStx)
return setGrindParams result params
@[builtin_tactic Lean.Parser.Tactic.grind] def evalGrind : Tactic := fun stx => do
match stx with

View File

@@ -689,6 +689,11 @@ def evalOmega : Tactic
omegaTactic cfg
| _ => throwUnsupportedSyntax
builtin_initialize bitvec_to_nat : SimpExtension
registerSimpAttr `bitvec_to_nat
"simp lemmas converting `BitVec` goals to `Nat` goals"
@[deprecated bitvec_to_nat (since := "2025-02-10")]
builtin_initialize bvOmegaSimpExtension : SimpExtension
registerSimpAttr `bv_toNat
"simp lemmas converting `BitVec` goals to `Nat` goals, for the `bv_omega` preprocessor"

View File

@@ -294,6 +294,25 @@ where
s := s.insert fvarId
return s
/-- Position for the `[..]` child syntax in the `simp` tactic. -/
def simpParamsPos := 4
/-- Position for the `only` child syntax in the `simp` tactic. -/
def simpOnlyPos := 3
def isSimpOnly (stx : TSyntax `tactic) : Bool :=
stx.raw.getKind == ``Parser.Tactic.simp && !stx.raw[simpOnlyPos].isNone
def getSimpParams (stx : TSyntax `tactic) : Array Syntax :=
stx.raw[simpParamsPos][1].getSepArgs
def setSimpParams (stx : TSyntax `tactic) (params : Array Syntax) : TSyntax `tactic :=
if params.isEmpty then
stx.raw.setArg simpParamsPos (mkNullNode)
else
let paramsStx := #[mkAtom "[", (mkAtom ",").mkSep params, mkAtom "]"]
stx.raw.setArg simpParamsPos (mkNullNode paramsStx)
@[inline] def simpOnlyBuiltins : List Name := [``eq_self, ``iff_self]
structure MkSimpContextResult where
@@ -321,7 +340,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp)
if kind == SimpKind.dsimp then
throwError "'dsimp' tactic does not support 'discharger' option"
let dischargeWrapper mkDischargeWrapper stx[2]
let simpOnly := !stx[3].isNone
let simpOnly := !stx[simpOnlyPos].isNone
let simpTheorems if simpOnly then
simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
else
@@ -412,8 +431,7 @@ def mkSimpOnly (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Syntax := do
args := args ++ ( locals.mapM fun id => `(Parser.Tactic.simpLemma| $(mkIdent id):ident))
else
args := args.push ( `(Parser.Tactic.simpStar| *))
let argsStx := if args.isEmpty then #[] else #[mkAtom "[", (mkAtom ",").mkSep args, mkAtom "]"]
return stx.setArg 4 (mkNullNode argsStx)
return setSimpParams stx args
def traceSimpCall (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Unit := do
logInfoAt stx[0] m!"Try this: {← mkSimpOnly stx usedSimps}"

View File

@@ -0,0 +1,53 @@
/-
Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Elab.Tactic.Simp
import Lean.Meta.Tactic.TryThis
namespace Lean.Elab.Tactic
private def addConfigItem (stx : Syntax) (item : Syntax) : Syntax :=
let optConfig := stx[1]
let optConfig := optConfig.modifyArg 0 fun arg => mkNullNode (#[item] ++ arg.getArgs)
stx.setArg 1 optConfig
set_option hygiene false in
private def addArith (stx : Syntax) : CoreM Syntax :=
return addConfigItem stx ( `(Lean.Parser.Tactic.configItem| +arith))
set_option hygiene false in
private def addDecide (stx : Syntax) : CoreM Syntax :=
return addConfigItem stx ( `(Lean.Parser.Tactic.configItem| +decide))
private def setKind (stx : Syntax) (str : String) (kind : SyntaxNodeKind) : Syntax :=
let stx := stx.setKind kind
stx.setArg 0 (mkAtom str)
private def addSuggestions (stx : Syntax) (tokenNew : String) (kindNew : SyntaxNodeKind) : MetaM Unit := do
let stx' := setKind stx tokenNew kindNew
let stx' := stx'.unsetTrailing
let s₁ : TSyntax `tactic := addArith stx'
let s₂ : TSyntax `tactic := addArith ( addDecide stx')
Meta.Tactic.TryThis.addSuggestions stx[0] #[s₁, s₂] (origSpan? := ( getRef))
@[builtin_tactic Lean.Parser.Tactic.simpArith] def evalSimpArith : Tactic := fun stx => do
addSuggestions stx "simp" ``Parser.Tactic.simp
throwError "`simp_arith` has been deprecated. It was a shorthand for `simp +arith +decide`, but most of the time, `+decide` was redundant since simprocs have been implemented."
@[builtin_tactic Lean.Parser.Tactic.simpArithBang] def evalSimpArithBang : Tactic := fun stx => do
addSuggestions stx "simp!" ``Parser.Tactic.simpAutoUnfold
throwError "`simp_arith!` has been deprecated. It was a shorthand for `simp! +arith +decide`, but most of the time, `+decide` was redundant since simprocs have been implemented."
@[builtin_tactic Lean.Parser.Tactic.simpAllArith] def evalSimpAllArith : Tactic := fun stx => do
addSuggestions stx "simp_all" ``Parser.Tactic.simpAll
throwError "`simp_all_arith` has been deprecated. It was a shorthand for `simp_all +arith +decide`, but most of the time, `+decide` was redundant since simprocs have been implemented."
@[builtin_tactic Lean.Parser.Tactic.simpAllArithBang] def evalSimpAllArithBang : Tactic := fun stx => do
addSuggestions stx "simp_all!" ``Parser.Tactic.simpAllAutoUnfold
throwError "`simp_all_arith!` has been deprecated. It was a shorthand for `simp_all! +arith +decide`, but most of the time, `+decide` was redundant since simprocs have been implemented."
end Lean.Elab.Tactic

View File

@@ -11,6 +11,7 @@ import Lean.Meta.Tactic.Try
import Lean.Meta.Tactic.TryThis
import Lean.Elab.Tactic.Config
import Lean.Elab.Tactic.SimpTrace
import Lean.Elab.Tactic.LibrarySearch
import Lean.Elab.Tactic.Grind
namespace Lean.Elab.Tactic
@@ -28,6 +29,59 @@ namespace Try
combinatiors such as `first`, `attempt_all`, `<;>`, `;`, and `try`.
-/
/-- Returns `true` if `fvarId` has an accessible name. -/
private def isAccessible (fvarId : FVarId) : MetaM Bool := do
let localDecl fvarId.getDecl
if localDecl.userName.hasMacroScopes then
return false
else
-- Check whether variable has been shadowed
let some localDecl' := ( getLCtx).findFromUserName? localDecl.userName
| return false
return localDecl'.fvarId == localDecl.fvarId
/-- Returns `true` if all free variables occurring in `e` are accessible. -/
private def isExprAccessible (e : Expr) : MetaM Bool := do
let (_, s) e.collectFVars |>.run {}
s.fvarIds.allM isAccessible
/-- Creates a temporary local context where all names are exposed, and executes `k`-/
private def withExposedNames (k : MetaM α) : MetaM α := do
withNewMCtxDepth do
-- Create a helper goal to apply
let mvarId := ( mkFreshExprMVar (mkConst ``True)).mvarId!
let mvarId mvarId.exposeNames
mvarId.withContext do k
/-- Executes `tac` in the saved state. This function is used to validate a tactic before suggesting it. -/
def checkTactic (savedState : SavedState) (tac : TSyntax `tactic) : TacticM Unit := do
let currState saveState
savedState.restore
try
evalTactic tac
finally
currState.restore
def evalSuggestExact : TacticM (TSyntax `tactic) := do
let savedState saveState
let mvarId :: mvarIds getGoals
| throwError "no goals"
mvarId.withContext do
let tactic := fun exfalso => LibrarySearch.solveByElim [] (exfalso := exfalso) (maxDepth := 6)
let allowFailure := fun _ => return false
let .none LibrarySearch.librarySearch mvarId tactic allowFailure
| throwError "`exact?` failed"
let proof := ( instantiateMVars (mkMVar mvarId)).headBeta
let tac if ( isExprAccessible proof) then
let stx PrettyPrinter.delab proof
`(tactic| exact $stx)
else withExposedNames do
let stx PrettyPrinter.delab proof
`(tactic| (expose_names; exact $stx))
checkTactic savedState tac
setGoals mvarIds
return tac
/-- Returns the suggestions represented by `tac`. -/
private def getSuggestionOfTactic (tac : TSyntax `tactic) : Array (TSyntax `tactic) :=
match tac with
@@ -53,6 +107,29 @@ private def filterSkipDone (tacs : Array (TSyntax `tactic)) : Array (TSyntax `ta
| `(tactic| done) | `(tactic| skip) => false
| _ => true
private def getTacSeqElems? (tseq : TSyntax ``Parser.Tactic.tacticSeq) : Option (Array (TSyntax `tactic)) :=
match tseq with
| `(tacticSeq| { $t;* }) => some t.getElems
| `(tacticSeq| $t;*) => some t.getElems
| _ => none
private def isCDotTac (tac : TSyntax `tactic) : Bool :=
match tac with
| `(tactic| · $_:tacticSeq) => true
| _ => false
private def appendSeq (tacs : Array (TSyntax `tactic)) (tac : TSyntax `tactic) : Array (TSyntax `tactic) := Id.run do
match tac with
| `(tactic| ($tseq:tacticSeq)) =>
if let some tacs' := getTacSeqElems? tseq then
return tacs ++ tacs'
| `(tactic| · $tseq:tacticSeq) =>
if let some tacs' := getTacSeqElems? tseq then
if !tacs'.any isCDotTac then
return tacs ++ tacs'
| _ => pure ()
return tacs.push tac
private def mkSeq (tacs : Array (TSyntax `tactic)) (terminal : Bool) : CoreM (TSyntax `tactic) := do
let tacs := filterSkipDone tacs
if tacs.size = 0 then
@@ -169,6 +246,69 @@ def observing (x : M α) : M (TacticResult α) := do
s.restore (restoreInfo := true)
return .error ex sNew
private def mergeParams (ps1 ps2 : Array Syntax) : Array Syntax := Id.run do
let mut r := ps1
for p in ps2 do
unless r.contains p do
r := r.push p
return r
private def mergeSimp? (tac1 tac2 : TSyntax `tactic) : Option (TSyntax `tactic) := Id.run do
if setSimpParams tac1 #[] != setSimpParams tac2 #[] then return none
let ps1 := getSimpParams tac1
let ps2 := getSimpParams tac2
return some (setSimpParams tac1 (mergeParams ps1 ps2))
private def mergeGrind? (tac1 tac2 : TSyntax `tactic) : Option (TSyntax `tactic) := Id.run do
if setGrindParams tac1 #[] != setGrindParams tac2 #[] then return none
let ps1 := getGrindParams tac1
let ps2 := getGrindParams tac2
return some (setGrindParams tac1 (mergeParams ps1 ps2))
private def merge? (tac1 tac2 : TSyntax `tactic) : Option (TSyntax `tactic) :=
let k := tac1.raw.getKind
-- TODO: we can make this extensible by having a command that allows users to register
-- `merge?` functions for different tactics.
if k == ``Parser.Tactic.simp then
mergeSimp? tac1 tac2
else if k == ``Parser.Tactic.grind then
mergeGrind? tac1 tac2
else
none
private def mergeAll? (tacs : Array (TSyntax `tactic)) : M (Option (TSyntax `tactic)) := do
if !( read).config.merge || tacs.isEmpty then
return none
let tac0 := tacs[0]!
if tacs.any fun tac => tac.raw.getKind != tac0.raw.getKind then
return none
let mut tac := tac0
for h : i in [1:tacs.size] do
let some tac' := merge? tac tacs[i]
| return none
tac := tac'
return some tac
/--
Returns `true` IF `tacs2` contains only tactics of the same kind, and one of the following
- contains `simp only ...` and `simp ...`
- contains `grind only ..` and `grind ...`
We say suggestions mixing `only` and non-`only` tactics are suboptimal and should not be displayed to
the user.
-/
-- TODO: we may add a mechanism for making this extensible.
private def isOnlyAndNonOnly (tacs2 : Array (TSyntax `tactic)) : Bool := Id.run do
if tacs2.isEmpty then return false
let k := tacs2[0]!.raw.getKind
unless tacs2.all fun tac => tac.raw.getKind == k do return false
if k == ``Parser.Tactic.simp then
return tacs2.any (isSimpOnly ·) && tacs2.any (!isSimpOnly ·)
else if k == ``Parser.Tactic.grind then
return tacs2.any (isGrindOnly ·) && tacs2.any (!isGrindOnly ·)
else
return false
private def mkChainResult (tac1 : TSyntax `tactic) (tacss2 : Array (TSyntax `tactic)) : M (TSyntax `tactic) := do
let tacss2 := tacss2.map getSuggestionsCore
if ( isTracingEnabledFor `try.debug) then
@@ -213,17 +353,27 @@ where
return ()
else if h : i < tacss2.size then
if tacss2[i].isEmpty then
go tacss2 (i+1) (( `(tactic| · sorry)) :: acc) kind?
go tacss2 (i+1) (( `(tactic| sorry)) :: acc) kind?
else
for tac in tacss2[i] do
if let some kind := kind? then
if tac.raw.getKind == kind then
go tacss2 (i+1) (( `(tactic| · $tac:tactic)) :: acc) kind?
go tacss2 (i+1) (tac :: acc) kind?
else
go tacss2 (i+1) (( `(tactic| · $tac:tactic)) :: acc) kind?
go tacss2 (i+1) (tac :: acc) kind?
else
let tac `(tactic| · $tac1:tactic
$(acc.toArray.reverse)*)
let tacs2 := acc.toArray.reverse
if kind?.isSome && isOnlyAndNonOnly tacs2 then
-- Suboptimal combination. See comment at `isOnlyAndNonOnly`
return ()
let tac if let some tac2 mergeAll? tacs2 then
-- TODO: when merging tactics, there is a possibility the compressed version will not work.
-- TODO: if this is a big issue in practice, we should "replay" the tactic here.
`(tactic| $tac1:tactic <;> $tac2:tactic)
else
let tacs2 tacs2.mapM fun tac2 => `(tactic| · $tac2:tactic)
`(tactic| · $tac1:tactic
$tacs2*)
modify (·.push tac)
private def evalSuggestGrindTrace (tac : TSyntax `tactic) : M (TSyntax `tactic) := do
@@ -281,9 +431,9 @@ private def evalSuggestSeq (tacs : Array (TSyntax `tactic)) : M (TSyntax `tactic
if ( read).terminal then
let mut result := #[]
for i in [:tacs.size - 1] do
result := result.push ( withNonTerminal <| evalSuggest tacs[i]!)
result := appendSeq result ( withNonTerminal <| evalSuggest tacs[i]!)
let suggestions getSuggestionOfTactic ( evalSuggest tacs.back!) |>.mapM fun tac =>
mkSeq (result.push tac) (terminal := true)
mkSeq (appendSeq result tac) (terminal := true)
mkTrySuggestions suggestions
else
mkSeq ( tacs.mapM evalSuggest) (terminal := false)
@@ -300,6 +450,8 @@ private def evalSuggestTacticSeq (s : TSyntax ``Parser.Tactic.tacticSeq) : M (TS
/-- `evalSuggest` for `first` tactic. -/
private partial def evalSuggestFirst (tacs : Array (TSyntax ``Parser.Tactic.tacticSeq)) : M (TSyntax `tactic) := do
if tacs.size == 0 then
throwError "`first` expects at least one argument"
go 0
where
go (i : Nat) : M (TSyntax `tactic) := do
@@ -341,6 +493,7 @@ where
-- `evalSuggest` implementation
@[export lean_eval_suggest_tactic]
private partial def evalSuggestImpl (tac : TSyntax `tactic) : M (TSyntax `tactic) := do
trace[try.debug] "{tac}"
match tac with
| `(tactic| $tac1 <;> $tac2) => evalSuggestChain tac1 tac2
| `(tactic| first $[| $tacs]*) => evalSuggestFirst tacs
@@ -356,6 +509,8 @@ private partial def evalSuggestImpl (tac : TSyntax `tactic) : M (TSyntax `tactic
evalSuggestGrindTrace tac
else if k == ``Parser.Tactic.simpTrace then
evalSuggestSimpTrace tac
else if k == ``Parser.Tactic.exact? then
evalSuggestExact
else
evalSuggestAtomic tac
if ( read).terminal then
@@ -363,6 +518,8 @@ private partial def evalSuggestImpl (tac : TSyntax `tactic) : M (TSyntax `tactic
throwError "unsolved goals"
return r
/-! `evalAndSuggest` frontend -/
private def toSuggestion (t : TSyntax `tactic) : Tactic.TryThis.Suggestion :=
t
@@ -432,35 +589,20 @@ private def mkGrindStx (info : Try.Info) : MetaM (TSyntax `tactic) := do
set_option hygiene false in -- Avoid tagger at `+arith`
/-- `simp` tactic syntax generator -/
private def mkSimpStx : CoreM (TSyntax `tactic) :=
`(tactic| first | simp? | simp? +arith | simp_all)
`(tactic| first | simp? | simp? [*] | simp? +arith | simp? +arith [*])
/-- `simple` tactics -/
private def mkSimpleTacStx : CoreM (TSyntax `tactic) :=
`(tactic| attempt_all | rfl | assumption | contradiction)
`(tactic| attempt_all | rfl | assumption)
/-! Function induction generators -/
private def allAccessible (majors : Array FVarId) : MetaM Bool :=
majors.allM fun major => do
let localDecl major.getDecl
if localDecl.userName.hasMacroScopes then
return false
else
-- Check whether variable has been shadowed
let some localDecl' := ( getLCtx).findFromUserName? localDecl.userName
| return false
return localDecl'.fvarId == localDecl.fvarId
open Try.Collector in
private def mkFunIndStx (c : FunIndCandidate) (cont : TSyntax `tactic) : MetaM (TSyntax `tactic) := do
if ( allAccessible c.majors) then
if ( c.majors.allM isAccessible) then
go
else withNewMCtxDepth do
-- Create a helper goal to apply
let mvarId := ( mkFreshExprMVar (mkConst ``True)).mvarId!
let mvarId mvarId.exposeNames
mvarId.withContext do
`(tactic| (expose_names; $( go):tactic))
else withExposedNames do
`(tactic| (expose_names; $( go):tactic))
where
go : MetaM (TSyntax `tactic) := do
let mut terms := #[]
@@ -481,13 +623,13 @@ private def mkTryEvalSuggestStx (info : Try.Info) : MetaM (TSyntax `tactic) := d
let simple mkSimpleTacStx
let simp mkSimpStx
let grind mkGrindStx info
let atomic `(tactic| attempt_all | $simple:tactic | $simp:tactic | $grind:tactic)
let atomic `(tactic| attempt_all | $simple:tactic | $simp:tactic | $grind:tactic | simp_all)
let funInds mkAllFunIndStx info atomic
`(tactic| first | $atomic:tactic | $funInds:tactic)
let extra `(tactic| (intros; first | $simple:tactic | $simp:tactic | exact?))
`(tactic| first | $atomic:tactic | $funInds:tactic | $extra:tactic)
-- TODO: vanilla `induction`.
-- TODO: make it extensible.
-- TODO: librarySearch integration.
-- TODO: premise selection.
@[builtin_tactic Lean.Parser.Tactic.tryTrace] def evalTryTrace : Tactic := fun stx => do

View File

@@ -306,8 +306,6 @@ structure Context where
ignoreTCFailures : Bool := false
/-- `true` when elaborating patterns. It affects how we elaborate named holes. -/
inPattern : Bool := false
/-- Cache for the `save` tactic. It is only `some` in the LSP server. -/
tacticCache? : Option (IO.Ref Tactic.Cache) := none
/--
Snapshot for incremental processing of current tactic, if any.
@@ -943,6 +941,7 @@ private def applyAttributesCore
return
withDeclName declName do
for attr in attrs do
withTraceNode `Elab.attribute (fun _ => pure m!"applying [{attr.stx}]") do
withRef attr.stx do withLogging do
let env getEnv
match getAttributeImpl env attr.name with

View File

@@ -462,10 +462,6 @@ private def modifyCheckedAsync (env : Environment) (f : Kernel.Environment → K
private def setCheckedSync (env : Environment) (newChecked : Kernel.Environment) : Environment :=
{ env with checked := .pure newChecked, checkedWithoutAsync := newChecked }
def promiseChecked (env : Environment) : BaseIO (Environment × IO.Promise Environment) := do
let prom IO.Promise.new
return ({ env with checked := prom.result?.bind (sync := true) (·.getD env |>.checked) }, prom)
/--
Checks whether the given declaration name may potentially added, or have been added, to the current
environment branch, which is the case either if this is the main branch or if the declaration name
@@ -595,6 +591,47 @@ def dbgFormatAsyncState (env : Environment) : BaseIO String :=
def dbgFormatCheckedSyncState (env : Environment) : BaseIO String :=
return s!"checked.get.constants.map₂: {repr <| env.checked.get.constants.map₂.toList.map (·.1)}"
/-- Result of `Lean.Environment.promiseChecked`. -/
structure PromiseCheckedResult where
/--
Resulting "main branch" environment. Accessing the kernel environment will block until
`PromiseCheckedResult.commitChecked` has been called.
-/
mainEnv : Environment
/--
Resulting "async branch" environment which should be used in a new task and then to call
`PromiseCheckedResult.commitChecked` to commit results back to the main environment. If it is not
called and the `PromiseCheckedResult` object is dropped, the kernel environment will be left
unchanged.
-/
asyncEnv : Environment
private checkedEnvPromise : IO.Promise Kernel.Environment
/--
Starts an asynchronous modification of the kernel environment. The environment is split into a
"main" branch that will block on access to the kernel environment until
`PromiseCheckedResult.commitChecked` has been called on the "async" environment branch.
-/
def promiseChecked (env : Environment) : BaseIO PromiseCheckedResult := do
let checkedEnvPromise IO.Promise.new
return {
mainEnv := { env with
checked := checkedEnvPromise.result?.bind (sync := true) fun
| some kenv => .pure kenv
| none => env.checked }
asyncEnv := { env with
-- Do not allow adding new constants
asyncCtx? := some { declPrefix := `__reserved__Environment_promiseChecked }
}
checkedEnvPromise
}
/-- Commits the kernel environment of the given environment back to the main branch. -/
def PromiseCheckedResult.commitChecked (res : PromiseCheckedResult) (env : Environment) :
BaseIO Unit :=
assert! env.asyncCtx?.isSome
res.checkedEnvPromise.resolve env.toKernelEnv
/--
Result of `Lean.Environment.addConstAsync` which is necessary to complete the asynchronous addition.
-/

View File

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
-/
prelude
import Init.Data.Hashable
import Init.Data.Int
import Lean.Data.KVMap
import Lean.Data.SMap
import Lean.Level
@@ -508,7 +509,11 @@ with
(t.data.hasLevelMVar || v.data.hasLevelMVar || b.data.hasLevelMVar)
(t.data.hasLevelParam || v.data.hasLevelParam || b.data.hasLevelParam)
| .lit l => mkData (mixHash 3 (hash l))
deriving Inhabited, Repr
deriving Repr
instance : Inhabited Expr where
-- use a distinctive name to aid debugging
default := .const `_inhabitedExprDummy []
namespace Expr
@@ -2140,16 +2145,13 @@ def mkInstLE : Expr := mkConst ``instLENat
end Nat
private def natAddFn : Expr :=
let nat := mkConst ``Nat
mkApp4 (mkConst ``HAdd.hAdd [0, 0, 0]) nat nat nat Nat.mkInstHAdd
mkApp4 (mkConst ``HAdd.hAdd [0, 0, 0]) Nat.mkType Nat.mkType Nat.mkType Nat.mkInstHAdd
private def natSubFn : Expr :=
let nat := mkConst ``Nat
mkApp4 (mkConst ``HSub.hSub [0, 0, 0]) nat nat nat Nat.mkInstHSub
mkApp4 (mkConst ``HSub.hSub [0, 0, 0]) Nat.mkType Nat.mkType Nat.mkType Nat.mkInstHSub
private def natMulFn : Expr :=
let nat := mkConst ``Nat
mkApp4 (mkConst ``HMul.hMul [0, 0, 0]) nat nat nat Nat.mkInstHMul
mkApp4 (mkConst ``HMul.hMul [0, 0, 0]) Nat.mkType Nat.mkType Nat.mkType Nat.mkInstHMul
/-- Given `a : Nat`, returns `Nat.succ a` -/
def mkNatSucc (a : Expr) : Expr :=
@@ -2168,17 +2170,97 @@ def mkNatMul (a b : Expr) : Expr :=
mkApp2 natMulFn a b
private def natLEPred : Expr :=
mkApp2 (mkConst ``LE.le [0]) (mkConst ``Nat) Nat.mkInstLE
mkApp2 (mkConst ``LE.le [0]) Nat.mkType Nat.mkInstLE
/-- Given `a b : Nat`, return `a ≤ b` -/
def mkNatLE (a b : Expr) : Expr :=
mkApp2 natLEPred a b
private def natEqPred : Expr :=
mkApp (mkConst ``Eq [1]) (mkConst ``Nat)
mkApp (mkConst ``Eq [1]) Nat.mkType
/-- Given `a b : Nat`, return `a = b` -/
def mkNatEq (a b : Expr) : Expr :=
mkApp2 natEqPred a b
/-! Constants for Int typeclasses. -/
namespace Int
protected def mkType : Expr := mkConst ``Int
def mkInstNeg : Expr := mkConst ``Int.instNegInt
def mkInstAdd : Expr := mkConst ``Int.instAdd
def mkInstHAdd : Expr := mkApp2 (mkConst ``instHAdd [levelZero]) Int.mkType mkInstAdd
def mkInstSub : Expr := mkConst ``Int.instSub
def mkInstHSub : Expr := mkApp2 (mkConst ``instHSub [levelZero]) Int.mkType mkInstSub
def mkInstMul : Expr := mkConst ``Int.instMul
def mkInstHMul : Expr := mkApp2 (mkConst ``instHMul [levelZero]) Int.mkType mkInstMul
def mkInstDiv : Expr := mkConst ``Int.instDiv
def mkInstHDiv : Expr := mkApp2 (mkConst ``instHDiv [levelZero]) Int.mkType mkInstDiv
def mkInstMod : Expr := mkConst ``Int.instMod
def mkInstHMod : Expr := mkApp2 (mkConst ``instHMod [levelZero]) Int.mkType mkInstMod
def mkInstPow : Expr := mkConst ``Int.instNatPow
def mkInstPowNat : Expr := mkApp2 (mkConst ``instPowNat [levelZero]) Int.mkType mkInstPow
def mkInstHPow : Expr := mkApp3 (mkConst ``instHPow [levelZero, levelZero]) Int.mkType Nat.mkType mkInstPowNat
def mkInstLT : Expr := mkConst ``Int.instLTInt
def mkInstLE : Expr := mkConst ``Int.instLEInt
end Int
private def intNegFn : Expr :=
mkApp2 (mkConst ``Neg.neg [0]) Int.mkType Int.mkInstNeg
private def intAddFn : Expr :=
mkApp4 (mkConst ``HAdd.hAdd [0, 0, 0]) Int.mkType Int.mkType Int.mkType Int.mkInstHAdd
private def intSubFn : Expr :=
mkApp4 (mkConst ``HSub.hSub [0, 0, 0]) Int.mkType Int.mkType Int.mkType Int.mkInstHSub
private def intMulFn : Expr :=
mkApp4 (mkConst ``HMul.hMul [0, 0, 0]) Int.mkType Int.mkType Int.mkType Int.mkInstHMul
/-- Given `a : Int`, returns `- a` -/
def mkIntNeg (a : Expr) : Expr :=
mkApp intNegFn a
/-- Given `a b : Int`, returns `a + b` -/
def mkIntAdd (a b : Expr) : Expr :=
mkApp2 intAddFn a b
/-- Given `a b : Int`, returns `a - b` -/
def mkIntSub (a b : Expr) : Expr :=
mkApp2 intSubFn a b
/-- Given `a b : Int`, returns `a * b` -/
def mkIntMul (a b : Expr) : Expr :=
mkApp2 intMulFn a b
private def intLEPred : Expr :=
mkApp2 (mkConst ``LE.le [0]) Int.mkType Int.mkInstLE
/-- Given `a b : Int`, return `a ≤ b` -/
def mkIntLE (a b : Expr) : Expr :=
mkApp2 intLEPred a b
private def intEqPred : Expr :=
mkApp (mkConst ``Eq [1]) Int.mkType
/-- Given `a b : Int`, return `a = b` -/
def mkIntEq (a b : Expr) : Expr :=
mkApp2 intEqPred a b
def mkIntLit (n : Nat) : Expr :=
let r := mkRawNatLit n
mkApp3 (mkConst ``OfNat.ofNat [levelZero]) Int.mkType r (mkApp (mkConst ``instOfNat) r)
def reflBoolTrue : Expr :=
mkApp2 (mkConst ``Eq.refl [levelOne]) (mkConst ``Bool) (mkConst ``Bool.true)
end Lean

Some files were not shown because too many files have changed in this diff Show More