This PR changes elaboration of `structure` parents so that each must be
fully elaborated before the next one is processed.
In particular, it re-adds synthesizing synthetic mvars between
`structure` parents, in the same manner as other fields. This synthesis
step was removed in #5842 because I had thought parents were like type
parameters and would participate in header elaboration, but in the end
it made more sense elaborating parents after the headers are done, since
they're like fields.
We want this enabled because it will help ensure that all the necessary
reductions are done to types of fields as they're added to the
structure.
This PR introduces the `assert!` variant `debug_assert!` that is
activated when compiled with `buildType` `debug`.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
This PR ensures that names suggested by tactics like `simp?` are not
shadowed by auxiliary declarations in the local context and that names
of `let rec` and `where` declarations are correctly resolved in tactic
blocks.
This PR contains the following potentially breaking changes:
* Moves the `auxDeclToFullName` map from `TermElab.Context` to
`LocalContext`.
* Refactors `Lean.Elab.Term.resolveLocalName : Name → TermElabM …` to
`Lean.resolveLocalName [MonadResolveName m] [MonadEnv m] [MonadLCtx m] :
Name → m …`.
* Refactors the `TermElabM` action `Lean.Elab.Term.withAuxDecl` to a
monad-polymorphic action `Lean.Meta.withAuxDecl`.
* Adds an optional `filter` argument to `Lean.unresolveNameGlobal`.
Closes#6706, closes#7073.
The performance win here is pretty negligible (and of course irrelevant
with the small allocator enabled), but this is consistent with it being
used elsewhere.
Follow-up to #6598
This PR translates `lean::mk_projections` into Lean, adding
`Lean.Meta.mkProjections`. It also puts `hasLooseBVarInExplicitDomain`
back in sync with the kernel version. Deletes
`src/library/constructions/projection.{h,cpp}`.
This PR adds support theorems for the Cooper-Right conflict resolution
rule used in the cutsat procedure. During model construction, when
attempting to extend the model to a variable x, cutsat may find a
conflict that involves two inequalities (the lower and upper bounds for
x). This is a special case of Cooper-Dvd-Right when there is no
divisibility constraint.
This PR changes the Lake job monitor to display the last (i.e., newest)
running/unfinished job rather than the first. This avoids the monitor
focusing too long on any one job (e.g., "Running job computation").
This PR adds support theorems for the **Cooper-Dvd-Right** conflict
resolution rule used in the cutsat procedure. During model construction,
when attempting to extend the model to a variable `x`, cutsat may find a
conflict that involves two inequalities (the lower and upper bounds for
`x`) and a divisibility constraint.
This PR adds support theorems for the **Cooper-Left** conflict
resolution rule used in the cutsat procedure. During model
construction,when attempting to extend the model to a variable `x`,
cutsat may find a conflict that involves two inequalities (the lower and
upper bounds for `x`). This is a special case of Cooper-Dvd-Left when
there is no divisibility constraint.
This PR implements non-choronological backtracking for the cutsat
procedure. The procedure has two main kinds of case-splits:
disequalities and Cooper resolvents. This PR focus on the first kind.
This PR adds support theorems for the **Cooper-Dvd-Left** conflict
resolution rule used in the cutsat procedure. During model construction,
when attempting to extend the model to a variable `x`, cutsat may find a
conflict that involves two inequalities (the lower and upper bounds for
`x`) and a divisibility constraint:
```lean
a * x + p ≤ 0
b * x + q ≤ 0
d ∣ c * x + s
```
We apply Cooper's quantifier elimination to produce:
```lean
OrOver (Int.lcm a (a * d / Int.gcd(a * d) c)) fun k =>
b * p + (-a) * q + b * k ≤ 0 ∧
a ∣ p + k ∧
a * d ∣ c * p + (-a) * s + c * k
```
Here, `OrOver` is a "big-or" operator. This PR introduces the following
theorem, which encapsulates the above approach via reflection:
```lean
theorem cooper_dvd_left (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (n : Nat)
: cooper_dvd_left_cert p₁ p₂ p₃ d n
→ p₁.denote' ctx ≤ 0
→ p₂.denote' ctx ≤ 0
→ d ∣ p₃.denote' ctx
→ OrOver n (cooper_dvd_left_split ctx p₁ p₂ p₃ d) :=
```
For each `0 <= k < n`, we generate the three implied facts using:
```lean
theorem cooper_dvd_left_split_ineq (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (b : Int) (p' : Poly)
: cooper_dvd_left_split ctx p₁ p₂ p₃ d k
→ cooper_dvd_left_split_ineq_cert p₁ p₂ k b p'
→ p'.denote ctx ≤ 0
theorem cooper_dvd_left_split_dvd1 (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (a : Int) (p' : Poly)
: cooper_dvd_left_split ctx p₁ p₂ p₃ d k
→ cooper_dvd_left_split_dvd1_cert p₁ p' a k
→ a ∣ p'.denote ctx
theorem cooper_dvd_left_split_dvd2 (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (d' : Int) (p' : Poly)
: cooper_dvd_left_split ctx p₁ p₂ p₃ d k
→ cooper_dvd_left_split_dvd2_cert p₁ p₃ d k d' p'
→ d' ∣ p'.denote ctx
```
Two helper `OrOver` theorems are used to process the `OrOver`:
```lean
theorem orOver_unsat {p} : ¬ OrOver 0 p
theorem orOver_resolve {n p} : OrOver (n+1) p → ¬ p n → OrOver n p
```
Where `p` is instantiated using `cooper_dvd_left_split ctx p₁ p₂ p₃ d`.
This PR changes the order of arguments of the folding function expected
by the tree map's `foldr` and `foldrM` functions so that they are
consistent with the API of `List`.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This PR provides lemmas about the tree map functions `keys` and `toList`
and their interactions with other functions for which lemmas already
exist. Moreover, a bug in `foldr` (calling `foldlM` instead of `foldrM`)
is fixed.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This PR contains theorems about `IntX` that are required for `bv_decide`
and the `IntX` simprocs.
A more comprehensive set of theorems about `IntX` will be part of future
PRs.
This PR improves the cutsat search procedure. It adds support for find
an approximate rational solution, checks disequalities, and adds stubs
for all missing cases.
This PR improves performance of LRAT trimming in bv_decide.
The underlying idea is taken from LRAT trimming as implemented in
[`lrat-trim`](https://github.com/arminbiere/lrat-trim/t): As we only
filter about half to two thirds of the LRAT proof steps anyway, there is
no need to use tree or hash maps to store information about them and we
can instead use arrays indexed by the proof step directly. This does not
meaningfully increase the amount of memory required but makes the
trimming step basically disappear from profiles, e.g.
`smt/non-incremental/QF_BV/20210312-Bouvier/vlsat3_a72.smt2` [used
to](https://share.firefox.dev/41kJTle) have 8% of its time spent in
trimming [now](https://share.firefox.dev/3QAKI4w) 1.5%.
This PR provides proofs that the raw tree map operations are well-formed
and refactors the file structure of the tree map, introducing new
modules `Std.{DTreeMap,TreeMap,TreeSet}.Raw` and splittting
`AdditionalOperations` into separate files for bundled and raw types.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This PR takes Array-specific lemmas at the end of `Array/Lemmas.lean`
(i.e. material that does not have exact correspondences with
`List/Lemmas.lean`) and moves them to more appropriate homes. More to
come.
This PR fixes the definition of `Min (Option α)`. This is a breaking
change. This treats `none` as the least element,
so `min none x = min x none = none` for all `x : Option α`. Prior to
nightly-2025-02-27, we instead had `min none (some x) = min (some x)
none = some x`. Also adds basic lemmas relating `min`, `max`, `≤` and
`<` on `Option`.
This PR changes the Lake DSL to use builtin elaborators, macros, and
initializers.
This works out of the box for the Lake executable and is supported in
interactive contexts through the Lake plugin.
