Compare commits

..

78 Commits

Author SHA1 Message Date
Scott Morrison
c4a41ef1a3 update test 2024-03-20 22:19:49 +11:00
Scott Morrison
c140e2e527 Update src/Init/Data/List/Lemmas.lean
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
2024-03-20 21:17:38 +11:00
Scott Morrison
bb859dc642 correct doc-string 2024-03-20 14:18:53 +11:00
Scott Morrison
34cf5b36c2 feat: BitVec.ofBoolListLE and theorems 2024-03-20 14:16:50 +11:00
Kitamado
7abc1fdaac doc: fix docstring of List.span (#3707)
see
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/docstring.20of.20.60List.2Espan.60.20is.20wrong
2024-03-18 10:26:47 +00:00
Liu Yuxi
2d18eff544 doc: lake: fix typo (#3704)
Closes #3703
2024-03-17 18:23:21 +00:00
Scott Morrison
66541b00a6 feat: upstream Std's rfl tactic (#3671)
This allows tagging lemmas with `@[refl]`, that will then by used by
`rfl`.

This is preparatory to upstreaming Mathlib's `convert` tactic.
2024-03-17 07:06:13 +00:00
Scott Morrison
f1f9b57df9 feat: upstream apply helper tactics from Mathlib (#3670)
These are used in Mathlib's `congr!` and `convert` tactics, which will
be upstreamed soon.

---------

Co-authored-by: Kyle Miller <kmill31415@gmail.com>
2024-03-17 06:47:56 +00:00
Scott Morrison
88b1751b54 chore: fix namespaces in recently upstreamed tactics (#3672) 2024-03-17 06:41:40 +00:00
Timo Carlin-Burns
8e96d7ba1d refactor: clean up public API around Array.eraseIdx (#3676)
- Removes the public definitions `Array.eraseIdxAux` and
`Array.eraseIdxSzAux` which were implementation details.
- Motivation: `Array.eraseIdxAux` and `Array.eraseIdxSzAux` were clearly
not intended to remain public, but simply making them private would make
it inconvenient to unfold them when writing proofs in Std.
- Adds documentation comments to the public `Array.eraseIdx`-related
definitions which remain.
- Removes `Array.eraseIdx'` which was just `Array.feraseIdx` wrapped in
a subtype and adds `Array.size_feraseIdx` to prove the subtype property
as a standalone theorem.

Co-Authored-By: Daniel Windham <daniel@atlascomputing.org>
2024-03-17 06:25:10 +00:00
Scott Morrison
9ee10aa3eb chore: in combined CI, check for required Std tag, then Mathlib (#3702) 2024-03-17 01:29:47 +00:00
Scott Morrison
811bedfa76 chore: fix combined CI for mathlib (#3700)
Previously, if there was a `nightly-testing-YYYY-MM-DD` tag at Std, but
not Mathlib, we were erroneously proceeding with Mathlib CI, and hence
using a probably-broken version of Mathlib.
2024-03-16 23:42:45 +00:00
Joachim Breitner
0b01ceb3bb fix: substVars in functional inductions removed valuable information (#3695)
using the `substVars` tactic on the goal can remove too much
information, as it does not take into account that the `motive` may
depend on the fixed parameters.

This is fixed by etracting `substVar` from `subst` which expects the
`x`, not the `h : x = rhs`, and then using this tactic on the local
declarations _after_ the `motive` exclusively.
2024-03-16 14:55:31 +00:00
Joachim Breitner
4c57da4b0f feat: infer termination arguments like xs.size - i (#3666)
a common pattern for recursive functions is
```
def countUp (n i acc : Nat) : Nat :=
  if i < n then
    countUp n (i+1) (acc + i)
  else
    acc
```
where we increase a value `i` until it hits an upper bound. This is
particularly common with array processing functions:
```
$ git grep 'termination_by.*size.*-' src/|wc -l
26
```

GuessLex now recognizes this pattern. The general approach is:

For every recursive call, check if the context contains hypotheses of
the form `e₁ < e₂` (or similar comparisions), and then consider `e₂ -
e₁` as a termination argument.

Currently, this only fires when `e₁` and `e₂` only depend on the
functions parameters, but not local let-bindings or variables bound in
local pattern matches.

Duplicates are removed.

In the table showing the termination argument failures, long termination
arguments are now given a number and abbreviated as e.g. `#4` in the
table headers.

More examples in the test file, here as some highlights:
```
def distinct (xs : Array Nat) : Bool :=
  let rec loop (i j : Nat) : Bool :=
    if _ : i < xs.size then
      if _ : j < i then
        if xs[j] = xs[i] then
          false
        else
          loop i (j+1)
      else
        loop (i+1) 0
    else
      true
  loop 0 0
```
infers
```
termination_by (Array.size xs - i, i - j)
```
and the weird functions where `i` goes up or down
```
def weird (xs : Array Nat) (i : Nat) : Bool :=
  if _ : i < xs.size then
    if _ : 0 < i then
      if xs[i] = 42 then
        weird xs.pop (i - 1)
      else
        weird xs (i+1)
    else
      weird xs (i+1)
  else
    true
decreasing_by all_goals simp_wf; omega
```
infers
```
termination_by (Array.size xs - i, i)
```
but unfortunately needs `decreasing_by` pending the “big
decreasing_tactic refactor” that
I expect we’ll want to do at some point.
2024-03-16 12:27:35 +00:00
Joachim Breitner
f0ff01ae28 refactor: pass Measures around as Expr in GuessLex (#3665)
this refactor prepares GuessLex to be able to infer more complex
termination arguments.

As a side-effect it fixes an (obscure) bug where `sizeOf` would be
applied to a term of the wrong type and thus a wrong `SizeOf` instance
could be inferred.
2024-03-16 10:25:55 +00:00
Joe Hendrix
0ec8862103 chore: migrate find functionality into LazyDiscrTree (#3685)
This migrates some lookup functionality from library_search to a more
generic version in LazyDiscrTree.

It is a step towards `rw?` in core.
2024-03-16 01:01:53 +00:00
Lean stage0 autoupdater
f70895ede5 chore: update stage0 2024-03-15 16:30:21 +00:00
Sebastian Ullrich
557777dd37 chore: CI: mark "Build matrix complete" as cancelled if builds cancelled (#3690) 2024-03-15 12:30:48 +00:00
Marc Huisinga
e47d8ca5cd fix: periodically refresh semantic tokens (#3691)
Based on #3619 that was reverted because of nondeterministic test
failures. This PR should resolve those.
2024-03-15 11:58:50 +00:00
Sebastian Ullrich
3b4b2cc89d fix: do not dllexport symbols in core static libraries (#3601)
On Windows, we now compile all core `.o`s twice, once with and without
`dllexport`, for use in the shipped dynamic and static libraries,
respectively. On other platforms, we export always as before to avoid
the duplicate work.

---------

Co-authored-by: tydeu <tydeu@hatpress.net>
2024-03-15 11:58:34 +00:00
Marc Huisinga
14654d802d chore: revert periodically refresh semantic tokens (#3619) (#3689)
This reverts commit 4e3a8468c3 for PR
#3619. It looks like the CI in that commit didn't inform me that a test
was broken by the PR, so I managed to commit it despite the broken test.
2024-03-15 09:17:53 +00:00
Leonardo de Moura
173b956961 feat: reserved names (#3675)
- Add support for reserved declaration names. We use them for theorems
generated on demand.
- Equation theorems are not private declarations anymore.
- Generate equation theorems on demand when resolving symbols.
- Prevent users from creating declarations using reserved names. Users
can bypass it using meta-programming.

See next test for examples.
2024-03-15 00:33:22 +00:00
Joachim Breitner
022b2e4d96 refactor: termination arguments as Expr, not Syntax (#3658)
Before, the termination argument as inferred by `GuessLex` was passed
further
on as `Syntax`, to be elaborated later in `WF.Rel`.

This didn’t feel quite right anymore. In particular if we want to teach
`GuessLex` about guessing more complex termination arguments like
`xs.size -
i`, using `Expr` here is more natural.

So this introduces `TerminationArgument` based on an `Expr` to be used
here.

A side-effect of how the termination arguments are elaborated is that
the unused
variables linter will now look at `termination_by` variables, and that
parameters
past the colon are not even invisibly in scope, so `‹_›` will not find
them
See https://github.com/leanprover-community/mathlib4/pull/11370/files
for examples
of fixing these changes.
2024-03-14 23:51:53 +00:00
Marc Huisinga
4e3a8468c3 fix: periodically refresh semantic tokens (#3619)
This PR fixes an issue where the file worker would not provide the
client with semantic tokens until the file had been elaborated
completely. The file worker now also tells the client to refresh its
semantic tokens after running "Restart File". This PR is based on #3271.
2024-03-14 17:10:04 +00:00
Marc Huisinga
78a72741c6 fix: jump to correct definition when names overlap (#3656)
Fixes #1170.

This PR adds the module name to `RefIdent` in order to distinguish
conflicting names from different files. This also fixes related issues
in find-references or the call hierarchy feature.
It also adds some docstrings and stylistically refactors a bunch of
code.
2024-03-14 16:21:19 +00:00
Marc Huisinga
795e332fb3 feat: server -> client requests (#3271)
This PR adds support for requests from the server to the client in the
language server. It is based on #3014 and was developed during an
experiment for #3247 that unfortunately did not go anywhere.
2024-03-14 16:00:32 +00:00
Joe Hendrix
1151d73a55 fix: use builtin_initialize in library_search (#3677)
This replaces a few uses of initialize with builtin_initialize, and
removes some unneeded functionality added when it was unclear if lazy
discriminator trees would be efficient enough.
2024-03-14 15:28:00 +00:00
Sebastian Ullrich
fb2ec54b60 chore: build Lean .os in parallel to rest of core (#3682)
Previously, we only did `Init/*.{o,olean}+Lean/*.olean` in parallel
2024-03-14 15:14:37 +00:00
Joachim Breitner
f89ed40618 refactor: ArgsPacker (#3621)
This introduces the `ArgsPacker` module and abstraction, to replace the
exising `PackDomain`/`PackMutual` code. The motivation was that we now
have more uses besides `Fix.lean` (`GuessLex` and `FunInd`), and the
code was spread in various places.

The goals are

* consistent function naming withing the the `PSigma` handling, the
`PSum` handling, and the combined interface
* avoid taking a type apart just based on the `PSigma`/`PSum` nesting,
to be robust in case the user happens to be using `PSigma`/`PSum`
somewhere. Therefore, always pass an `arity` or `numFuncs` or `varNames`
around.
* keep all the `PSigma`/`PSum` encoding logic contained within one
module (`ArgsPacker`), and keep that module independent of its users (so
no `EqnInfos` visible here).
 * pick good variable names when matching on a packed argument
* the unary function now is either called `fun1._unary` or
`fun1._mutual`, never `fun1._unary._mutual`.

This file has less heavy dependencies than `PackMutual` had, so build
parallelism is improved as well.
2024-03-14 14:59:40 +00:00
Sebastian Ullrich
68eaf33e86 feat: snapshot trees and language processors (#3014)
This is the foundation for work on making processing in the language
server both more fine-grained (incremental tactics) as well as parallel.
2024-03-14 13:40:08 +00:00
Sebastian Ullrich
0959bc45d2 chore: CI: temporarily disable fsanitize build 2024-03-14 15:36:28 +01:00
Leonardo de Moura
995726f75f chore: fix tests 2024-03-13 21:15:48 -07:00
Leonardo de Moura
214179b6b9 chore: update stage0 2024-03-13 21:15:48 -07:00
Leonardo de Moura
9ee1ff2435 chore: remove bootstrapping workaround 2024-03-13 21:15:48 -07:00
Leonardo de Moura
653eb5f66e chore: update stage0 2024-03-13 21:15:48 -07:00
Leonardo de Moura
2c8fd7fb95 chore: avoid reserved name
TODO: update state0 and cleanup
2024-03-13 21:15:48 -07:00
Leonardo de Moura
8d2adf521d feat: allow duplicate theorems to be imported 2024-03-13 12:57:41 -07:00
Leonardo de Moura
612d97440b chore: incorrectly annotated theorems 2024-03-13 12:37:58 -07:00
Leonardo de Moura
0f19332618 chore: update stage0 2024-03-13 12:37:58 -07:00
Leonardo de Moura
84b0919a11 feat: type of theorems must be propositions 2024-03-13 12:37:58 -07:00
Hongyu Ouyang
e61d082a95 doc: fix typo in USize.size docstring (#3664) 2024-03-13 10:51:24 +00:00
Leonardo de Moura
600412838c fix: auxiliary definition nested in theorem should be def if its type is not a proposition (#3662) 2024-03-13 09:38:37 +00:00
Joachim Breitner
a81205c290 feat: conv => calc (#3659)
`calc` is great for explicit rewriting, `conv` is great to say where to
rewrite, so it's natural to want `calc` as a `conv` tactic.

Zulip disucssion at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/idiom.20for.20using.20calc.20to.20rewrite.20the.20goal/near/424269608

Fixes #3557.
2024-03-13 09:03:39 +00:00
Leonardo de Moura
2003814085 chore: rename automatically generated equational theorems (#3661)
cc @nomeata
2024-03-13 07:56:27 +00:00
Scott Morrison
317adf42e9 chore: add @[simp] to Nat.succ_eq_add_one, and cleanup downstream (#3579) 2024-03-13 05:35:52 +00:00
Leonardo de Moura
5aca09abca fix: add Canonicalizer.lean and use it to canonicalize terms in omega (#3639) 2024-03-12 23:18:56 +00:00
Joachim Breitner
07dac67847 feat: guard_msgs to escapes trailing newlines (#3617)
This makes trailing whitespace visible and protectes them against
trimming by the editor, by appending the symbol ⏎ to such a line (and
also to any line that ends with such a symbol, to avoid ambiguities in
the case the message already had that symbol).

(Only the code action output / docstring parsing is affected; the error
message as sent
to the InfoView is unaffected.)

Fixes #3571
2024-03-12 16:35:14 +00:00
thorimur
5cf4db7fbf fix: make dsimp? use and report simprocs (#3654)
Modifies `dsimpLocation'` (which implements `dsimp?`) to take a
`simprocs : SimprocsArray` argument, like `simpLocation` and
`dsimpLocation`. This ensures that the behavior of `dsimp` matches
`dsimp?`.

---

Closes #3653
2024-03-12 05:17:58 +00:00
Mac Malone
b2ae4bd5c1 feat: allow noncomputable unsafe definitions (#3647)
Enables the combination of `noncomputable unsafe` to be used for
definitions. Outside of pure theory, `noncomputable` is also useful to
prevent Lean from compiling a definition which will be implemented with
external code later. Such definitions may also wish to be marked
`unsafe` if they perform morally impure or memory-unsafe functions.
2024-03-12 02:46:42 +00:00
Joe Hendrix
c43a6b5341 chore: upstream Std.Data.Int (#3635)
This depends on #3634.
2024-03-11 21:40:48 +00:00
Lean stage0 autoupdater
1388f6bc83 chore: update stage0 2024-03-11 17:22:37 +00:00
Joachim Breitner
d9b6794e2f refactor: termination_by parser to use binderIdent (#3652)
this way we should be able to use `elabBinders` to parse the binders.
2024-03-11 16:29:56 +00:00
Mac Malone
ebefee0b7d chore: response file to avoid arg limits in lean static lib build (#3612) 2024-03-11 16:14:24 +00:00
Joachim Breitner
32dcc6eb89 feat: GuessLex: avoid writing sizeOf in termination argument when not needed (#3630)
this makes `termination_by?` even slicker.

The heuristics is agressive in the non-mutual case (will omit `sizeOf`
if the argument is non-dependent and the `WellFoundedRelation` relation
is via `sizeOfWFRel`.

In the mutual case we'd also have to check the arguments, as they line
up in the termination argument, have the same types. I did not bother at
this point; in the mutual case we omit `sizeOf` only if the argument
type is `Nat`.

As a drive-by fix, `termination_by?` now also works on functions that
have only one plausible measure.
2024-03-10 22:57:10 +00:00
Leonardo de Moura
1d3ef577c2 chore: disable some tests on Windows (#3642)
This is a temporary workaround for a limitation on Windows shared
libraries. We are getting errors of the form:
```
ld.lld: error: too many exported symbols (got 65572, max 65535)
```
2024-03-09 23:48:41 +00:00
Kyle Miller
45fccc5906 feat: custom eliminators for induction and cases tactics, and beautiful eliminators for Nat (#3629)
Replaces `@[eliminator]` with two attributes `@[induction_eliminator]`
and `@[cases_eliminator]` for defining custom eliminators for the
`induction` and `cases` tactics, respectively.

Adds `Nat.recAux` and `Nat.casesAuxOn`, which are eliminators that are
defeq to `Nat.rec` and `Nat.casesOn`, but these use `0` and `n + 1`
rather than `Nat.zero` and `Nat.succ n`.

For example, using `induction` to prove that the factorial function is
positive now has the following goal states (thanks also to #3616 for the
goal state after unfolding).
```lean
example : 0 < fact x := by
  induction x with
  | zero => decide
  | succ x ih =>
    /-
    x : Nat
    ih : 0 < fact x
    ⊢ 0 < fact (x + 1)
    -/
    unfold fact
    /-
    ...
    ⊢ 0 < (x + 1) * fact x
    -/
    simpa using ih
```

Thanks to @adamtopaz for initial work on splitting the `@[eliminator]`
attribute.
2024-03-09 15:31:51 +00:00
Kyle Miller
3acd77a154 fix: make elabTermEnsuringType respect errToSorry when there is a type mismatch (#3633)
Floris van Doorn [reported on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/have.20tactic.20error.20recovery/near/425283053)
that it is confusing that the `have : T := e` tactic completely fails if
the body `e` is not of type `T`. This is in contrast to `have : T := by
exact e`, which does not completely fail when `e` is not of type `T`.

This ends up being caused by `elabTermEnsuringType` throwing an error
when it fails to insert a coercion. Now, it detects this case, and it
checks the `errToSorry` flag to decide whether to throw the error or to
log the error and insert a `sorry`.

This is justified by `elabTermEnsuringType` being a frontend to
`elabTerm`, which inserts `sorry` on error.

An alternative would be to make `ensureType` respect `errToSorry`, but
there exists code that expects being able to catch when `ensureType`
fails. Making such code manipulate `errToSorry` seems error prone, and
this function is not a main entry point to the term elaborator, unlike
`elabTermEnsuringType`.
2024-03-09 15:30:47 +00:00
Leonardo de Moura
b39042b32c fix: eta-expanded instances at SynthInstance.lean (#3638)
Remark: this commit removes the `jason1.lean` test. Motivation: It
breaks all the time due to changes we make, and it is not clear anymore
what it is testing.

---------

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
2024-03-08 20:37:38 +00:00
Joe Hendrix
6dd4f4b423 chore: upstream Std.Data.Nat (#3634)
This migrates lemmas about Nat `compare`, `min`, `max`, `dvd`, `gcd`,
`lcm` and `div`/`mod` from Std to Lean itself.

Std still has some additional recursors, `CoPrime` and a few additional
definitions that might merit further discussion prior to upstreaming.
2024-03-08 17:00:46 +00:00
Mac Malone
123dcb964c feat: lake: LEAN_GITHASH override (#3609)
If the `LEAN_GITHASH` environment variable is set, Lake will now use it
instead of the detected Lean's githash when computing traces for builds
and the elaborated Lake configuration. This override allows one to
replace the Lean version used by a library
(e.g., Mathlib) without completely rebuilding it, which is useful for
testing custom builds of Lean.
2024-03-08 15:03:07 +00:00
Patrick Massot
ccac989dda doc: expand an error message about compacting closures (#3627)
Provide a hint of where the error message may come from.
2024-03-07 20:02:23 +00:00
Kyle Miller
f336525f31 fix: make delabConstWithSignature avoid using inaccessible names (#3625)
The `delabConstWithSignature` delaborator is responsible for pretty
printing constants with a declaration-like signature, with binders, a
colon, and a type. This is used by the `#check` command when it is given
just an identifier.

It used to accumulate binders from pi types indiscriminately, but this
led to unfriendly behavior. For example, `#check String.append` would
give
```
String.append (a✝ : String) (a✝¹ : String) : String
```
with inaccessible names. These appear because `String.append` is defined
using patterns, so it never names these parameters.

Now the delaborator stops accumulating binders once it reaches an
inaccessible name, and for example `#check String.append` now gives
```
String.append : String → String → String
```
We do not synthesize names for the sake of enabling binder syntax
because the binder names are part of the API of a function — one can use
`(arg := ...)` syntax to pass arguments by name. The delaborator also
now stops accumulating binders once it reaches a parameter with a name
already seen before — we then rely on the main delaborator to provide
that parameter with a fresh name when pretty printing the pi type.

As a special case, instance parameters with inaccessible names are
included as binders, pretty printing like `[LT α]`, rather than
relegating them (and all the remaining parameters) to after the colon.
It would be more accurate to pretty print this as `[inst✝ : LT α]`, but
we make the simplifying assumption that such instance parameters are
generally used via typeclass inference. Likely `inst✝` would not
directly appear in pretty printer output, and even if it appears in a
hover, users can likely figure out what is going on. (We may consider
making such `inst✝` variables pretty print as `‹LT α›` or
`infer_instance` in the future, to make this more consistent.)

Something we note here is that we do not do anything to make sure
parameters that can be used as named arguments actually appear named
after the colon (nor do we assure that the names are the correct names).
For example, one sees `foo : String → String → String` rather than `foo
: String → (baz : String) → String`. We can investigate this later if it
is wanted.

We also give `delabConstWithSignature` a `universes` flag to enable
turning off pretty printing universe levels parameters.

Closes #2846
2024-03-07 18:14:06 +00:00
Sebastian Ullrich
3921257ece feat: thread initialization for reverse FFI (#3632)
Makes it possible to properly allocate and free thread-local runtime
resources for threads not started by Lean itself
2024-03-07 17:02:47 +00:00
Sebastian Ullrich
6af7a01af6 fix: stray dbgTraceVal in trace children elision (#3622) 2024-03-07 09:44:25 +00:00
Leonardo de Moura
611b174689 fix: ofScientific at simp (#3628)
closes #2159
2024-03-07 00:11:31 +00:00
Leonardo de Moura
d731854d5a chore: update stage0 2024-03-06 15:29:04 -08:00
Leonardo de Moura
3218b25974 doc: for issue #2835 2024-03-06 15:29:04 -08:00
Leonardo de Moura
ef33882e2f test: issue #2835
closes #2835
2024-03-06 15:29:04 -08:00
Leonardo de Moura
4208c44939 chore: update stage0 2024-03-06 15:29:04 -08:00
Leonardo de Moura
423fed79a9 feat: simplify .arrow ctor at DiscrTree.lean 2024-03-06 15:29:04 -08:00
Leonardo de Moura
5302b7889a fix: fold raw Nat literals at dsimp (#3624)
closes #2916

Remark: this PR also renames `Expr.natLit?` ==> `Expr.rawNatLit?`.
Motivation: consistent naming convention: `Expr.isRawNatLit`.
2024-03-06 18:29:20 +00:00
Joe Hendrix
46cc00d5db chore: add example to explanation cond_decide is not simp (#3615)
This just adds a concrete example to the `cond_decide` lemma to explain
why it is not a simp rule.
2024-03-06 16:58:12 +00:00
Joachim Breitner
0072d13bd4 feat: MatcherApp.transform: Try to preserve alt’s variable name (#3620)
this makes the ugly `fst`/`snd` variable names in the functional
induction principles go away.

Ironically I thought in order to fix these name, I should touch the
mutual/n-ary argument packing code used for well-founded recursion, and
embarked on a big refactor/rewrite of that code, only to find that at
least this particular instance of the issue was somewhere else. Hence
breaking this into its own PR; the refactoring will follow (and will
also improve some other variable names.)
2024-03-06 15:56:17 +00:00
Leonardo de Moura
09bc477016 feat: better support for reducing Nat.rec (#3616)
closes #3022

With this commit, given the declaration
```
def foo : Nat → Nat
  | 0 => 2
  | n + 1 => foo n
```
when we unfold `foo (n+1)`, we now obtain `foo n` instead of `foo
(Nat.add n 0)`.
2024-03-06 13:28:07 +00:00
Sebastian Ullrich
f0a762ea4d chore: CI: temporarily disable test binary check on Windows 2024-03-06 09:00:38 +01:00
Leonardo de Moura
30a61a57c3 chore: disable compiler tests on Windows 2024-03-05 20:24:01 -08:00
Leonardo de Moura
794228a982 refactor: Offset.lean and related files (#3614)
Motivation: avoid the unfold and check idiom.
This commit also minimize dependencies at `Offset.lean`.

closes #2615
2024-03-05 19:40:15 -08:00
Joe Hendrix
6cf82c3763 fix: update LazyDiscrTree to not reuse names when caching (#3610)
This fixes an issue discovered in Mathlib with the meta cache being
poisoned by using a name generator. It is difficult to reproduce due to
the name collisions being rare, but here is a minimal module with
definitions that result in an error:

```lean
prelude
universe u

inductive Unit2 : Type where
  | unit : Unit2

inductive Eq2 {α : Sort u} : α → α → Prop where
  | refl (a : α) : Eq2 a a

structure Subtype2 {α : Sort u} (p : α → Prop) where
  val : α

def End (α) := α → α
theorem end_app_eq (α : Type u) (f : End α) (a : α) : Eq2 (f a) (f a) := Eq2.refl _
theorem Set.coe_eq_subtype {α : Type u} (s : α → Prop) : Eq2 (Subtype2 s) (Subtype2 s) := Eq2.refl _
def succAboveCases {_ : Unit2} {α : Unit2 → Sort u} (i : Unit2) (v : α i) : α i := v
theorem succAbove_cases_eq_insertNth : Eq2 @succAboveCases.{u + 1} @succAboveCases.{u + 1} := Eq2.refl _
```

Removing any of thee last 5 definitions avoids the error. Testing
against Mathlib shows this PR fixes the issue.
2024-03-06 02:32:22 +00:00
553 changed files with 8927 additions and 3870 deletions

View File

@@ -98,7 +98,8 @@ jobs:
// exclude seriously slow tests
"CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
},
{
// TODO: suddenly started failing in CI
/*{
"name": "Linux fsanitize",
"os": "ubuntu-latest",
"quick": false,
@@ -106,7 +107,7 @@ jobs:
"CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_FLAGS='-fsanitize=address,undefined -fsanitize-link-c++-runtime' -DSMALL_ALLOCATOR=OFF -DBSYMBOLIC=OFF",
// exclude seriously slow/problematic tests (laketests crash)
"CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
},
},*/
{
"name": "macOS",
"os": "macos-latest",
@@ -140,8 +141,7 @@ jobs:
"shell": "msys2 {0}",
"CMAKE_OPTIONS": "-G \"Unix Makefiles\" -DUSE_GMP=OFF",
// for reasons unknown, interactivetests are flaky on Windows
// also, the liasolver test hits “too many exported symbols”
"CTEST_OPTIONS": "--repeat until-pass:2 -E 'leanbenchtest_liasolver.lean'",
"CTEST_OPTIONS": "--repeat until-pass:2",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
"prepare-llvm": "../script/prepare-llvm-mingw.sh lean-llvm*",
"binary-check": "ldd"
@@ -446,9 +446,10 @@ jobs:
name: Build matrix complete
runs-on: ubuntu-latest
needs: build
if: ${{ always() }}
# mark as merely cancelled not failed if builds are cancelled
if: ${{ !cancelled() }}
steps:
- if: contains(needs.*.result, 'failure') || contains(needs.*.result, 'cancelled')
- if: contains(needs.*.result, 'failure')
uses: actions/github-script@v7
with:
script: |

View File

@@ -126,21 +126,19 @@ jobs:
if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then
echo "The merge base of this PR coincides with the nightly release"
MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE=""
else
echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
fi
STD_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover/std4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
if [[ -n "$STD_REMOTE_TAGS" ]]; then
echo "... and Std has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE=""
if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
else
echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
fi
else
echo "... but Std does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE="- ❗ Std CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Std CI should run now."

View File

@@ -13,6 +13,7 @@
/src/Lean/Data/Lsp/ @mhuisi
/src/Lean/Elab/Deriving/ @semorrison
/src/Lean/Elab/Tactic/ @semorrison
/src/Lean/Language/ @Kha
/src/Lean/Meta/Tactic/ @leodemoura
/src/Lean/Parser/ @Kha
/src/Lean/PrettyPrinter/ @Kha

View File

@@ -11,6 +11,16 @@ of each version.
v4.8.0 (development in progress)
---------
* **Executables configured with `supportInterpreter := true` on Windows should now be run via `lake exe` to function properly.**
The way Lean is built on Windows has changed (see PR [#3601](https://github.com/leanprover/lean4/pull/3601)). As a result, Lake now dynamically links executables with `supportInterpreter := true` on Windows to `libleanshared.dll` and `libInit_shared.dll`. Therefore, such executables will not run unless those shared libraries are co-located with the executables or part of `PATH`. Running the executable via `lake exe` will ensure these libraries are part of `PATH`.
In a related change, the signature of the `nativeFacets` Lake configuration options has changed from a static `Array` to a function `(shouldExport : Bool) → Array`. See its docstring or Lake's [README](src/lake/README.md) for further details on the changed option.
* Lean now generates an error if the type of a theorem is **not** a proposition.
* Importing two different files containing proofs of the same theorem is no longer considered an error. This feature is particularly useful for theorems that are automatically generated on demand (e.g., equational theorems).
* New command `derive_functinal_induction`:
Derived from the definition of a (possibly mutually) recursive function
@@ -31,6 +41,46 @@ v4.8.0 (development in progress)
(x x : Nat) : motive x x
```
* The termination checker now recognizes more recursion patterns without an
explicit `terminatin_by`. In particular the idiom of counting up to an upper
bound, as in
```
def Array.sum (arr : Array Nat) (i acc : Nat) : Nat :=
if _ : i < arr.size then
Array.sum arr (i+1) (acc + arr[i])
else
acc
```
is recognized without having to say `termination_by arr.size - i`.
Breaking changes:
* Automatically generated equational theorems are now named using suffix `.eq_<idx>` instead of `._eq_<idx>`, and `.def` instead of `._unfold`. Example:
```
def fact : Nat → Nat
| 0 => 1
| n+1 => (n+1) * fact n
theorem ex : fact 0 = 1 := by unfold fact; decide
#check fact.eq_1
-- fact.eq_1 : fact 0 = 1
#check fact.eq_2
-- fact.eq_2 (n : Nat) : fact (Nat.succ n) = (n + 1) * fact n
#check fact.def
/-
fact.def :
∀ (x : Nat),
fact x =
match x with
| 0 => 1
| Nat.succ n => (n + 1) * fact n
-/
```
v4.7.0
---------

View File

@@ -111,6 +111,15 @@ if (lean_io_result_is_ok(res)) {
lean_io_mark_end_initialization();
```
In addition, any other thread not spawned by the Lean runtime itself must be initialized for Lean use by calling
```c
void lean_initialize_thread();
```
and should be finalized in order to free all thread-local resources by calling
```c
void lean_finalize_thread();
```
## `@[extern]` in the Interpreter
The interpreter can run Lean declarations for which symbols are available in loaded shared libraries, which includes `@[extern]` declarations.

View File

@@ -176,7 +176,7 @@ with builtins; let
# make local "copy" so `drv`'s Nix store path doesn't end up in ccache's hash
ln -s ${drv.c}/${drv.cPath} src.c
# on the other hand, a debug build is pretty fast anyway, so preserve the path for gdb
leanc -c -o $out/$oPath $leancFlags -fPIC ${if debug then "${drv.c}/${drv.cPath} -g" else "src.c -O3 -DNDEBUG"}
leanc -c -o $out/$oPath $leancFlags -fPIC ${if debug then "${drv.c}/${drv.cPath} -g" else "src.c -O3 -DNDEBUG -DLEAN_EXPORTING"}
'';
};
mkMod = mod: deps:

View File

@@ -503,13 +503,13 @@ file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib)
# set up libInit_shared only on Windows; see also stdlib.make.in
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
set(INIT_SHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a")
set(INIT_SHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libInit.a.export ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a")
endif()
if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
elseif(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lLean -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libLean.a.export -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
else()
set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
endif()

View File

@@ -156,7 +156,6 @@ match [a, b] with
simplifies to `a`. -/
syntax (name := simpMatch) "simp_match" : conv
/-- Executes the given tactic block without converting `conv` goal into a regular goal. -/
syntax (name := nestedTacticCore) "tactic'" " => " tacticSeq : conv

View File

@@ -19,7 +19,7 @@ which applies to all applications of the function).
-/
@[simp] def inline {α : Sort u} (a : α) : α := a
theorem id.def {α : Sort u} (a : α) : id a = a := rfl
theorem id_def {α : Sort u} (a : α) : id a = a := rfl
/--
`flip f a b` is `f b a`. It is useful for "point-free" programming,
@@ -737,13 +737,16 @@ theorem beq_false_of_ne [BEq α] [LawfulBEq α] {a b : α} (h : a ≠ b) : (a ==
section
variable {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ}
theorem HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} β Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : HEq a b) : motive b :=
/-- Non-dependent recursor for `HEq` -/
noncomputable def HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} β Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : HEq a b) : motive b :=
h.rec m
theorem HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} β Sort u1} {β : Sort u2} {b : β} (h : HEq a b) (m : motive a) : motive b :=
/-- `HEq.ndrec` variant -/
noncomputable def HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} β Sort u1} {β : Sort u2} {b : β} (h : HEq a b) (m : motive a) : motive b :=
h.rec m
theorem HEq.elim {α : Sort u} {a : α} {p : α Sort v} {b : α} (h₁ : HEq a b) (h₂ : p a) : p b :=
/-- `HEq.ndrec` variant -/
noncomputable def HEq.elim {α : Sort u} {a : α} {p : α Sort v} {b : α} (h₁ : HEq a b) (h₂ : p a) : p b :=
eq_of_heq h₁ h₂
theorem HEq.subst {p : (T : Sort u) T Prop} (h₁ : HEq a b) (h₂ : p α a) : p β b :=

View File

@@ -106,7 +106,7 @@ def norm [info : ContextInformation α] (ctx : α) (e : Expr) : List Nat :=
let xs := if info.isComm ctx then sort xs else xs
if info.isIdem ctx then mergeIdem xs else xs
theorem List.two_step_induction
noncomputable def List.two_step_induction
{motive : List Nat Sort u}
(l : List Nat)
(empty : motive [])

View File

@@ -727,33 +727,38 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
termination_by as.size - i
go 0 #[]
def eraseIdxAux (i : Nat) (a : Array α) : Array α :=
if h : i < a.size then
let idx : Fin a.size := i, h;
let idx1 : Fin a.size := i - 1, by exact Nat.lt_of_le_of_lt (Nat.pred_le i) h;
let a' := a.swap idx idx1
eraseIdxAux (i+1) a'
/-- Remove the element at a given index from an array without bounds checks, using a `Fin` index.
This function takes worst case O(n) time because
it has to backshift all elements at positions greater than `i`.-/
def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
if h : i.val + 1 < a.size then
let a' := a.swap i.val + 1, h i
let i' : Fin a'.size := i.val + 1, by simp [a', h]
have : a'.size - i' < a.size - i := by
simp [a', Nat.sub_succ_lt_self _ _ i.isLt]
a'.feraseIdx i'
else
a.pop
termination_by a.size - i
termination_by a.size - i.val
def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
eraseIdxAux (i.val + 1) a
derive_functional_induction feraseIdx
theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
induction a, i using feraseIdx.induct with
| @case1 a i h a' _ _ ih =>
unfold feraseIdx
simp [h, a', ih]
| case2 a i h =>
unfold feraseIdx
simp [h]
/-- Remove the element at a given index from an array, or do nothing if the index is out of bounds.
This function takes worst case O(n) time because
it has to backshift all elements at positions greater than `i`.-/
def eraseIdx (a : Array α) (i : Nat) : Array α :=
if i < a.size then eraseIdxAux (i+1) a else a
def eraseIdxSzAux (a : Array α) (i : Nat) (r : Array α) (heq : r.size = a.size) : { r : Array α // r.size = a.size - 1 } :=
if h : i < r.size then
let idx : Fin r.size := i, h;
let idx1 : Fin r.size := i - 1, by exact Nat.lt_of_le_of_lt (Nat.pred_le i) h;
eraseIdxSzAux a (i+1) (r.swap idx idx1) ((size_swap r idx idx1).trans heq)
else
r.pop, (size_pop r).trans (heq rfl)
termination_by r.size - i
def eraseIdx' (a : Array α) (i : Fin a.size) : { r : Array α // r.size = a.size - 1 } :=
eraseIdxSzAux a (i.val + 1) a rfl
if h : i < a.size then a.feraseIdx i, h else a
def erase [BEq α] (as : Array α) (a : α) : Array α :=
match as.indexOf? a with
@@ -809,7 +814,7 @@ where
rfl
go (i : Nat) (hi : i as.size) : toListLitAux as n hsz i hi (as.data.drop i) = as.data := by
cases i <;> simp [getLit_eq, List.get_drop_eq_drop, toListLitAux, List.drop, go]
induction i <;> simp [getLit_eq, List.get_drop_eq_drop, toListLitAux, List.drop, *]
def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size bs.size) (i : Nat) : Bool :=
if h : i < as.size then

View File

@@ -73,6 +73,9 @@ protected def toNat (a : BitVec n) : Nat := a.toFin.val
/-- Return the bound in terms of toNat. -/
theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
@[deprecated isLt]
theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.isLt
/-- 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
@@ -615,4 +618,14 @@ section normalization_eqs
@[simp] theorem zero_eq : BitVec.zero n = 0#n := rfl
end normalization_eqs
/-- Converts a list of `Bool`s to a big-endian `BitVec`. -/
def ofBoolListBE : (bs : List Bool) BitVec bs.length
| [] => 0#0
| b :: bs => cons b (ofBoolListBE bs)
/-- Converts a list of `Bool`s to a little-endian `BitVec`. -/
def ofBoolListLE : (bs : List Bool) BitVec bs.length
| [] => 0#0
| b :: bs => concat (ofBoolListLE bs) b
end BitVec

View File

@@ -29,8 +29,6 @@ theorem eq_of_toNat_eq {n} : ∀ {i j : BitVec n}, i.toNat = j.toNat → i = j
@[bv_toNat] theorem toNat_ne (x y : BitVec n) : x y x.toNat y.toNat := by
rw [Ne, toNat_eq]
theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.toFin.2
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsb i := rfl
@[simp] theorem getLsb_ofFin (x : Fin (2^n)) (i : Nat) :
@@ -43,12 +41,36 @@ theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsb i := rfl
have p : 2^w 2^i := Nat.pow_le_pow_of_le_right (by omega) ge
omega
@[simp] theorem getMsb_ge (x : BitVec w) (i : Nat) (ge : w i) : getMsb x i = false := by
rw [getMsb]
simp only [Bool.and_eq_false_imp, decide_eq_true_eq]
omega
theorem lt_of_getLsb (x : BitVec w) (i : Nat) : getLsb x i = true i < w := by
if h : i < w then
simp [h]
else
simp [Nat.ge_of_not_lt h]
theorem lt_of_getMsb (x : BitVec w) (i : Nat) : getMsb x i = true i < w := by
if h : i < w then
simp [h]
else
simp [Nat.ge_of_not_lt h]
theorem getMsb_eq_getLsb (x : BitVec w) (i : Nat) : x.getMsb i = (decide (i < w) && x.getLsb (w - 1 - i)) := by
rw [getMsb]
theorem getLsb_eq_getMsb (x : BitVec w) (i : Nat) : x.getLsb i = (decide (i < w) && x.getMsb (w - 1 - i)) := by
rw [getMsb]
by_cases h₁ : i < w <;> by_cases h₂ : w - 1 - i < w <;>
simp only [h₁, h₂] <;> simp only [decide_True, decide_False, Bool.false_and, Bool.and_false, Bool.true_and, Bool.and_true]
· congr
omega
all_goals
apply getLsb_ge
omega
-- We choose `eq_of_getLsb_eq` as the `@[ext]` theorem for `BitVec`
-- somewhat arbitrarily over `eq_of_getMsg_eq`.
@[ext] theorem eq_of_getLsb_eq {x y : BitVec w}
@@ -72,7 +94,7 @@ theorem eq_of_getMsb_eq {x y : BitVec w}
else
have w_pos := Nat.pos_of_ne_zero w_zero
have r : i w - 1 := by
simp [Nat.le_sub_iff_add_le w_pos, Nat.add_succ]
simp [Nat.le_sub_iff_add_le w_pos]
exact i_lt
have q_lt : w - 1 - i < w := by
simp only [Nat.sub_sub]
@@ -292,6 +314,19 @@ theorem nat_eq_toNat (x : BitVec w) (y : Nat)
getLsb (zeroExtend' ge x) i = getLsb x i := by
simp [getLsb, toNat_zeroExtend']
@[simp] theorem getMsb_zeroExtend' (ge : m n) (x : BitVec n) (i : Nat) :
getMsb (zeroExtend' ge x) i = (decide (i m - n) && getMsb x (i - (m - n))) := by
simp only [getMsb, getLsb_zeroExtend', gt_iff_lt]
by_cases h₁ : decide (i < m) <;> by_cases h₂ : decide (i m - n) <;> by_cases h₃ : decide (i - (m - n) < n) <;>
by_cases h₄ : n - 1 - (i - (m - n)) = m - 1 - i
all_goals
simp only [h₁, h₂, h₃, h₄]
simp_all only [ge_iff_le, decide_eq_true_eq, Nat.not_le, Nat.not_lt, Bool.true_and,
Bool.false_and, Bool.and_self] <;>
(try apply getLsb_ge) <;>
(try apply (getLsb_ge _ _ _).symm) <;>
omega
@[simp] theorem getLsb_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) :
getLsb (zeroExtend m x) i = (decide (i < m) && getLsb x i) := by
simp [getLsb, toNat_zeroExtend, Nat.testBit_mod_two_pow]
@@ -458,12 +493,12 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
| y+1 =>
rw [Nat.succ_eq_add_one] at h
rw [ h]
rw [Nat.testBit_two_pow_sub_succ (toNat_lt _)]
rw [Nat.testBit_two_pow_sub_succ (isLt _)]
· cases w : decide (i < v)
· simp at w
simp [w]
rw [Nat.testBit_lt_two_pow]
calc BitVec.toNat x < 2 ^ v := toNat_lt _
calc BitVec.toNat x < 2 ^ v := isLt _
_ 2 ^ i := Nat.pow_le_pow_of_le_right Nat.zero_lt_two w
· simp
@@ -520,7 +555,7 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
· simp
rw [Nat.mod_eq_of_lt]
rw [Nat.shiftLeft_eq, Nat.pow_add]
exact Nat.mul_lt_mul_of_pos_right (BitVec.toNat_lt x) (Nat.two_pow_pos _)
exact Nat.mul_lt_mul_of_pos_right x.isLt (Nat.two_pow_pos _)
· omega
@[simp] theorem getLsb_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :
@@ -531,6 +566,11 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
<;> simp_all
<;> (rw [getLsb_ge]; omega)
@[simp] theorem getMsb_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :
getMsb (shiftLeftZeroExtend x n) i = getMsb x i := by
have : n i + n := by omega
simp_all [shiftLeftZeroExtend_eq]
@[simp] theorem msb_shiftLeftZeroExtend (x : BitVec w) (i : Nat) :
(shiftLeftZeroExtend x i).msb = x.msb := by
simp [shiftLeftZeroExtend_eq, BitVec.msb]
@@ -555,11 +595,18 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
@[simp] theorem getLsb_append {v : BitVec n} {w : BitVec m} :
getLsb (v ++ w) i = bif i < m then getLsb w i else getLsb v (i - m) := by
simp [append_def]
simp only [append_def, getLsb_or, getLsb_shiftLeftZeroExtend, getLsb_zeroExtend']
by_cases h : i < m
· simp [h]
· simp [h]; simp_all
@[simp] theorem getMsb_append {v : BitVec n} {w : BitVec m} :
getMsb (v ++ w) i = bif n i then getMsb w (i - n) else getMsb v i := by
simp [append_def]
by_cases h : n i
· simp [h]
· simp [h]
theorem msb_append {x : BitVec w} {y : BitVec v} :
(x ++ y).msb = bif (w == 0) then (y.msb) else (x.msb) := by
rw [ append_eq, append]
@@ -632,6 +679,13 @@ theorem toNat_cons' {x : BitVec w} :
@[simp] theorem msb_cons : (cons a x).msb = a := by
simp [cons, msb_cast, msb_append]
@[simp] theorem getMsb_cons_zero : (cons a x).getMsb 0 = a := by
rw [ BitVec.msb, msb_cons]
@[simp] theorem getMsb_cons_succ : (cons a x).getMsb (i + 1) = x.getMsb i := by
simp [cons, cond_eq_if]
omega
theorem truncate_succ (x : BitVec w) :
truncate (i+1) x = cons (getLsb x i) (truncate i x) := by
apply eq_of_getLsb_eq
@@ -827,7 +881,7 @@ protected theorem lt_of_le_ne (x y : BitVec n) (h1 : x <= y) (h2 : ¬ x = y) : x
simp
exact Nat.lt_of_le_of_ne
/- ! ### intMax -/
/-! ### intMax -/
/-- The bitvector of width `w` that has the largest value when interpreted as an integer. -/
def intMax (w : Nat) : BitVec w := (2^w - 1)#w
@@ -841,4 +895,20 @@ theorem toNat_intMax_eq : (intMax w).toNat = 2^w - 1 := by
omega
simp [intMax, Nat.shiftLeft_eq, Nat.one_mul, natCast_eq_ofNat, toNat_ofNat, Nat.mod_eq_of_lt h]
/-! ### ofBoolList -/
@[simp] theorem getMsb_ofBoolListBE : (ofBoolListBE bs).getMsb i = bs.getD i false := by
induction bs generalizing i <;> cases i <;> simp_all [ofBoolListBE]
@[simp] theorem getLsb_ofBoolListBE :
(ofBoolListBE bs).getLsb i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by
simp [getLsb_eq_getMsb]
@[simp] theorem getLsb_ofBoolListLE : (ofBoolListLE bs).getLsb i = bs.getD i false := by
induction bs generalizing i <;> cases i <;> simp_all [ofBoolListLE]
@[simp] theorem getMsb_ofBoolListLE :
(ofBoolListLE bs).getMsb i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by
simp [getMsb_eq_getLsb]
end BitVec

View File

@@ -41,7 +41,7 @@ Sends a message on an `Channel`.
This function does not block.
-/
def Channel.send (v : α) (ch : Channel α) : BaseIO Unit :=
def Channel.send (ch : Channel α) (v : α) : BaseIO Unit :=
ch.atomically do
let st get
if st.closed then return

View File

@@ -11,3 +11,4 @@ import Init.Data.Int.DivModLemmas
import Init.Data.Int.Gcd
import Init.Data.Int.Lemmas
import Init.Data.Int.Order
import Init.Data.Int.Pow

View File

@@ -160,6 +160,12 @@ instance : Mod Int where
@[simp, norm_cast] theorem ofNat_ediv (m n : Nat) : ((m / n) : Int) = m / n := rfl
theorem ofNat_div (m n : Nat) : (m / n) = div m n := rfl
theorem ofNat_fdiv : m n : Nat, (m / n) = fdiv m n
| 0, _ => by simp [fdiv]
| succ _, _ => rfl
/-!
# `bmod` ("balanced" mod)

File diff suppressed because it is too large Load Diff

View File

@@ -6,7 +6,12 @@ Authors: Mario Carneiro
prelude
import Init.Data.Int.Basic
import Init.Data.Nat.Gcd
import Init.Data.Nat.Lcm
import Init.Data.Int.DivModLemmas
/-!
Definition and lemmas for gcd and lcm over Int
-/
namespace Int
/-! ## gcd -/
@@ -14,4 +19,37 @@ namespace Int
/-- Computes the greatest common divisor of two integers, as a `Nat`. -/
def gcd (m n : Int) : Nat := m.natAbs.gcd n.natAbs
theorem gcd_dvd_left {a b : Int} : (gcd a b : Int) a := by
have := Nat.gcd_dvd_left a.natAbs b.natAbs
rw [ Int.ofNat_dvd] at this
exact Int.dvd_trans this natAbs_dvd_self
theorem gcd_dvd_right {a b : Int} : (gcd a b : Int) b := by
have := Nat.gcd_dvd_right a.natAbs b.natAbs
rw [ Int.ofNat_dvd] at this
exact Int.dvd_trans this natAbs_dvd_self
@[simp] theorem one_gcd {a : Int} : gcd 1 a = 1 := by simp [gcd]
@[simp] theorem gcd_one {a : Int} : gcd a 1 = 1 := by simp [gcd]
@[simp] theorem neg_gcd {a b : Int} : gcd (-a) b = gcd a b := by simp [gcd]
@[simp] theorem gcd_neg {a b : Int} : gcd a (-b) = gcd a b := by simp [gcd]
/-! ## lcm -/
/-- Computes the least common multiple of two integers, as a `Nat`. -/
def lcm (m n : Int) : Nat := m.natAbs.lcm n.natAbs
theorem lcm_ne_zero (hm : m 0) (hn : n 0) : lcm m n 0 := by
simp only [lcm]
apply Nat.lcm_ne_zero <;> simpa
theorem dvd_lcm_left {a b : Int} : a lcm a b :=
Int.dvd_trans dvd_natAbs_self (Int.ofNat_dvd.mpr (Nat.dvd_lcm_left a.natAbs b.natAbs))
theorem dvd_lcm_right {a b : Int} : b lcm a b :=
Int.dvd_trans dvd_natAbs_self (Int.ofNat_dvd.mpr (Nat.dvd_lcm_right a.natAbs b.natAbs))
@[simp] theorem lcm_self {a : Int} : lcm a a = a.natAbs := Nat.lcm_self _
end Int

View File

@@ -153,7 +153,7 @@ theorem subNatNat_sub (h : n ≤ m) (k : Nat) : subNatNat (m - n) k = subNatNat
theorem subNatNat_add (m n k : Nat) : subNatNat (m + n) k = m + subNatNat n k := by
cases n.lt_or_ge k with
| inl h' =>
simp [subNatNat_of_lt h', succ_pred_eq_of_pos (Nat.sub_pos_of_lt h')]
simp [subNatNat_of_lt h', sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h')]
conv => lhs; rw [ Nat.sub_add_cancel (Nat.le_of_lt h')]
apply subNatNat_add_add
| inr h' => simp [subNatNat_of_le h',
@@ -169,12 +169,11 @@ theorem subNatNat_add_negSucc (m n k : Nat) :
rw [subNatNat_sub h', Nat.add_comm]
| inl h' =>
have h₂ : m < n + succ k := Nat.lt_of_lt_of_le h' (le_add_right _ _)
have h₃ : m n + k := le_of_succ_le_succ h₂
rw [subNatNat_of_lt h', subNatNat_of_lt h₂]
simp [Nat.add_comm]
rw [ add_succ, succ_pred_eq_of_pos (Nat.sub_pos_of_lt h'), add_succ, succ_sub h₃,
Nat.pred_succ]
rw [Nat.add_comm n, Nat.add_sub_assoc (Nat.le_of_lt h')]
simp only [pred_eq_sub_one, negSucc_add_negSucc, succ_eq_add_one, negSucc.injEq]
rw [Nat.add_right_comm, sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h'), Nat.sub_sub,
Nat.add_assoc, succ_sub_succ_eq_sub, Nat.add_comm n,Nat.add_sub_assoc (Nat.le_of_lt h'),
Nat.add_comm]
protected theorem add_assoc : a b c : Int, a + b + c = a + (b + c)
| (m:Nat), (n:Nat), c => aux1 ..
@@ -188,15 +187,15 @@ protected theorem add_assoc : ∀ a b c : Int, a + b + c = a + (b + c)
| (m:Nat), -[n+1], -[k+1] => by
rw [Int.add_comm, Int.add_comm m, Int.add_comm m, aux2, Int.add_comm -[k+1]]
| -[m+1], -[n+1], -[k+1] => by
simp [add_succ, Nat.add_comm, Nat.add_left_comm, neg_ofNat_succ]
simp [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]
where
aux1 (m n : Nat) : c : Int, m + n + c = m + (n + c)
| (k:Nat) => by simp [Nat.add_assoc]
| -[k+1] => by simp [subNatNat_add]
aux2 (m n k : Nat) : -[m+1] + -[n+1] + k = -[m+1] + (-[n+1] + k) := by
simp [add_succ]
simp
rw [Int.add_comm, subNatNat_add_negSucc]
simp [add_succ, succ_add, Nat.add_comm]
simp [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]
protected theorem add_left_comm (a b c : Int) : a + (b + c) = b + (a + c) := by
rw [ Int.add_assoc, Int.add_comm a, Int.add_assoc]
@@ -391,7 +390,7 @@ theorem ofNat_mul_subNatNat (m n k : Nat) :
| inl h =>
have h' : succ m * n < succ m * k := Nat.mul_lt_mul_of_pos_left h (Nat.succ_pos m)
simp [subNatNat_of_lt h, subNatNat_of_lt h']
rw [succ_pred_eq_of_pos (Nat.sub_pos_of_lt h), neg_ofNat_succ, Nat.mul_sub_left_distrib,
rw [sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h), neg_ofNat_succ, Nat.mul_sub_left_distrib,
succ_pred_eq_of_pos (Nat.sub_pos_of_lt h')]; rfl
| inr h =>
have h' : succ m * k succ m * n := Nat.mul_le_mul_left _ h
@@ -406,7 +405,7 @@ theorem negSucc_mul_subNatNat (m n k : Nat) :
| inl h =>
have h' : succ m * n < succ m * k := Nat.mul_lt_mul_of_pos_left h (Nat.succ_pos m)
rw [subNatNat_of_lt h, subNatNat_of_le (Nat.le_of_lt h')]
simp [succ_pred_eq_of_pos (Nat.sub_pos_of_lt h), Nat.mul_sub_left_distrib]
simp [sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h), Nat.mul_sub_left_distrib]
| inr h => cases Nat.lt_or_ge k n with
| inl h' =>
have h₁ : succ m * n > succ m * k := Nat.mul_lt_mul_of_pos_left h' (Nat.succ_pos m)
@@ -422,12 +421,12 @@ protected theorem mul_add : ∀ a b c : Int, a * (b + c) = a * b + a * c
simp [negOfNat_eq_subNatNat_zero]; rw [ subNatNat_add]; rfl
| (m:Nat), -[n+1], (k:Nat) => by
simp [negOfNat_eq_subNatNat_zero]; rw [Int.add_comm, subNatNat_add]; rfl
| (m:Nat), -[n+1], -[k+1] => by simp; rw [ Nat.left_distrib, succ_add]; rfl
| (m:Nat), -[n+1], -[k+1] => by simp [ Nat.left_distrib, Nat.add_left_comm, Nat.add_assoc]
| -[m+1], (n:Nat), (k:Nat) => by simp [Nat.mul_comm]; rw [ Nat.right_distrib, Nat.mul_comm]
| -[m+1], (n:Nat), -[k+1] => by
simp [negOfNat_eq_subNatNat_zero]; rw [Int.add_comm, subNatNat_add]; rfl
| -[m+1], -[n+1], (k:Nat) => by simp [negOfNat_eq_subNatNat_zero]; rw [ subNatNat_add]; rfl
| -[m+1], -[n+1], -[k+1] => by simp; rw [ Nat.left_distrib, succ_add]; rfl
| -[m+1], -[n+1], -[k+1] => by simp [ Nat.left_distrib, Nat.add_left_comm, Nat.add_assoc]
protected theorem add_mul (a b c : Int) : (a + b) * c = a * c + b * c := by
simp [Int.mul_comm, Int.mul_add]
@@ -499,33 +498,6 @@ theorem eq_one_of_mul_eq_self_left {a b : Int} (Hpos : a ≠ 0) (H : b * a = a)
theorem eq_one_of_mul_eq_self_right {a b : Int} (Hpos : b 0) (H : b * a = b) : a = 1 :=
Int.eq_of_mul_eq_mul_left Hpos <| by rw [Int.mul_one, H]
/-! # pow -/
protected theorem pow_zero (b : Int) : b^0 = 1 := rfl
protected theorem pow_succ (b : Int) (e : Nat) : b ^ (e+1) = (b ^ e) * b := rfl
protected theorem pow_succ' (b : Int) (e : Nat) : b ^ (e+1) = b * (b ^ e) := by
rw [Int.mul_comm, Int.pow_succ]
theorem pow_le_pow_of_le_left {n m : Nat} (h : n m) : (i : Nat), n^i m^i
| 0 => Nat.le_refl _
| succ i => Nat.mul_le_mul (pow_le_pow_of_le_left h i) h
theorem pow_le_pow_of_le_right {n : Nat} (hx : n > 0) {i : Nat} : {j}, i j n^i n^j
| 0, h =>
have : i = 0 := eq_zero_of_le_zero h
this.symm Nat.le_refl _
| succ j, h =>
match le_or_eq_of_le_succ h with
| Or.inl h => show n^i n^j * n from
have : n^i * 1 n^j * n := Nat.mul_le_mul (pow_le_pow_of_le_right hx h) hx
Nat.mul_one (n^i) this
| Or.inr h =>
h.symm Nat.le_refl _
theorem pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n^m :=
pow_le_pow_of_le_right h (Nat.zero_le _)
/-! NatCast lemmas -/
/-!
@@ -545,10 +517,4 @@ theorem natCast_one : ((1 : Nat) : Int) = (1 : Int) := rfl
@[simp] theorem natCast_mul (a b : Nat) : ((a * b : Nat) : Int) = (a : Int) * (b : Int) := by
simp
theorem natCast_pow (b n : Nat) : ((b^n : Nat) : Int) = (b : Int) ^ n := by
match n with
| 0 => rfl
| n + 1 =>
simp only [Nat.pow_succ, Int.pow_succ, natCast_mul, natCast_pow _ n]
end Int

View File

@@ -6,6 +6,7 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
prelude
import Init.Data.Int.Lemmas
import Init.ByCases
import Init.RCases
/-!
# Results about the order properties of the integers, and the integers as an ordered ring.
@@ -498,3 +499,524 @@ theorem toNat_add_nat {a : Int} (ha : 0 ≤ a) (n : Nat) : (a + n).toNat = a.toN
@[simp] theorem toNat_neg_nat : n : Nat, (-(n : Int)).toNat = 0
| 0 => rfl
| _+1 => rfl
/-! ### toNat' -/
theorem mem_toNat' : (a : Int) (n : Nat), toNat' a = some n a = n
| (m : Nat), n => by simp [toNat', Int.ofNat_inj]
| -[m+1], n => by constructor <;> nofun
/-! ## Order properties of the integers -/
protected theorem lt_of_not_ge {a b : Int} : ¬a b b < a := Int.not_le.mp
protected theorem not_le_of_gt {a b : Int} : b < a ¬a b := Int.not_le.mpr
protected theorem le_of_not_le {a b : Int} : ¬ a b b a := (Int.le_total a b).resolve_left
@[simp] theorem negSucc_not_pos (n : Nat) : 0 < -[n+1] False := by
simp only [Int.not_lt, iff_false]; constructor
theorem eq_negSucc_of_lt_zero : {a : Int}, a < 0 n : Nat, a = -[n+1]
| ofNat _, h => absurd h (Int.not_lt.2 (ofNat_zero_le _))
| -[n+1], _ => n, rfl
protected theorem lt_of_add_lt_add_left {a b c : Int} (h : a + b < a + c) : b < c := by
have : -a + (a + b) < -a + (a + c) := Int.add_lt_add_left h _
simp [Int.neg_add_cancel_left] at this
assumption
protected theorem lt_of_add_lt_add_right {a b c : Int} (h : a + b < c + b) : a < c :=
Int.lt_of_add_lt_add_left (a := b) <| by rwa [Int.add_comm b a, Int.add_comm b c]
protected theorem add_lt_add_iff_left (a : Int) : a + b < a + c b < c :=
Int.lt_of_add_lt_add_left, (Int.add_lt_add_left · _)
protected theorem add_lt_add_iff_right (c : Int) : a + c < b + c a < b :=
Int.lt_of_add_lt_add_right, (Int.add_lt_add_right · _)
protected theorem add_lt_add {a b c d : Int} (h₁ : a < b) (h₂ : c < d) : a + c < b + d :=
Int.lt_trans (Int.add_lt_add_right h₁ c) (Int.add_lt_add_left h₂ b)
protected theorem add_lt_add_of_le_of_lt {a b c d : Int} (h₁ : a b) (h₂ : c < d) :
a + c < b + d :=
Int.lt_of_le_of_lt (Int.add_le_add_right h₁ c) (Int.add_lt_add_left h₂ b)
protected theorem add_lt_add_of_lt_of_le {a b c d : Int} (h₁ : a < b) (h₂ : c d) :
a + c < b + d :=
Int.lt_of_lt_of_le (Int.add_lt_add_right h₁ c) (Int.add_le_add_left h₂ b)
protected theorem lt_add_of_pos_right (a : Int) {b : Int} (h : 0 < b) : a < a + b := by
have : a + 0 < a + b := Int.add_lt_add_left h a
rwa [Int.add_zero] at this
protected theorem lt_add_of_pos_left (a : Int) {b : Int} (h : 0 < b) : a < b + a := by
have : 0 + a < b + a := Int.add_lt_add_right h a
rwa [Int.zero_add] at this
protected theorem add_nonneg {a b : Int} (ha : 0 a) (hb : 0 b) : 0 a + b :=
Int.zero_add 0 Int.add_le_add ha hb
protected theorem add_pos {a b : Int} (ha : 0 < a) (hb : 0 < b) : 0 < a + b :=
Int.zero_add 0 Int.add_lt_add ha hb
protected theorem add_pos_of_pos_of_nonneg {a b : Int} (ha : 0 < a) (hb : 0 b) : 0 < a + b :=
Int.zero_add 0 Int.add_lt_add_of_lt_of_le ha hb
protected theorem add_pos_of_nonneg_of_pos {a b : Int} (ha : 0 a) (hb : 0 < b) : 0 < a + b :=
Int.zero_add 0 Int.add_lt_add_of_le_of_lt ha hb
protected theorem add_nonpos {a b : Int} (ha : a 0) (hb : b 0) : a + b 0 :=
Int.zero_add 0 Int.add_le_add ha hb
protected theorem add_neg {a b : Int} (ha : a < 0) (hb : b < 0) : a + b < 0 :=
Int.zero_add 0 Int.add_lt_add ha hb
protected theorem add_neg_of_neg_of_nonpos {a b : Int} (ha : a < 0) (hb : b 0) : a + b < 0 :=
Int.zero_add 0 Int.add_lt_add_of_lt_of_le ha hb
protected theorem add_neg_of_nonpos_of_neg {a b : Int} (ha : a 0) (hb : b < 0) : a + b < 0 :=
Int.zero_add 0 Int.add_lt_add_of_le_of_lt ha hb
protected theorem lt_add_of_le_of_pos {a b c : Int} (hbc : b c) (ha : 0 < a) : b < c + a :=
Int.add_zero b Int.add_lt_add_of_le_of_lt hbc ha
theorem add_one_le_iff {a b : Int} : a + 1 b a < b := .rfl
theorem lt_add_one_iff {a b : Int} : a < b + 1 a b := Int.add_le_add_iff_right _
@[simp] theorem succ_ofNat_pos (n : Nat) : 0 < (n : Int) + 1 :=
lt_add_one_iff.2 (ofNat_zero_le _)
theorem le_add_one {a b : Int} (h : a b) : a b + 1 :=
Int.le_of_lt (Int.lt_add_one_iff.2 h)
protected theorem nonneg_of_neg_nonpos {a : Int} (h : -a 0) : 0 a :=
Int.le_of_neg_le_neg <| by rwa [Int.neg_zero]
protected theorem nonpos_of_neg_nonneg {a : Int} (h : 0 -a) : a 0 :=
Int.le_of_neg_le_neg <| by rwa [Int.neg_zero]
protected theorem lt_of_neg_lt_neg {a b : Int} (h : -b < -a) : a < b :=
Int.neg_neg a Int.neg_neg b Int.neg_lt_neg h
protected theorem pos_of_neg_neg {a : Int} (h : -a < 0) : 0 < a :=
Int.lt_of_neg_lt_neg <| by rwa [Int.neg_zero]
protected theorem neg_of_neg_pos {a : Int} (h : 0 < -a) : a < 0 :=
have : -0 < -a := by rwa [Int.neg_zero]
Int.lt_of_neg_lt_neg this
protected theorem le_neg_of_le_neg {a b : Int} (h : a -b) : b -a := by
have h := Int.neg_le_neg h
rwa [Int.neg_neg] at h
protected theorem neg_le_of_neg_le {a b : Int} (h : -a b) : -b a := by
have h := Int.neg_le_neg h
rwa [Int.neg_neg] at h
protected theorem lt_neg_of_lt_neg {a b : Int} (h : a < -b) : b < -a := by
have h := Int.neg_lt_neg h
rwa [Int.neg_neg] at h
protected theorem neg_lt_of_neg_lt {a b : Int} (h : -a < b) : -b < a := by
have h := Int.neg_lt_neg h
rwa [Int.neg_neg] at h
protected theorem sub_nonpos_of_le {a b : Int} (h : a b) : a - b 0 := by
have h := Int.add_le_add_right h (-b)
rwa [Int.add_right_neg] at h
protected theorem le_of_sub_nonpos {a b : Int} (h : a - b 0) : a b := by
have h := Int.add_le_add_right h b
rwa [Int.sub_add_cancel, Int.zero_add] at h
protected theorem sub_neg_of_lt {a b : Int} (h : a < b) : a - b < 0 := by
have h := Int.add_lt_add_right h (-b)
rwa [Int.add_right_neg] at h
protected theorem lt_of_sub_neg {a b : Int} (h : a - b < 0) : a < b := by
have h := Int.add_lt_add_right h b
rwa [Int.sub_add_cancel, Int.zero_add] at h
protected theorem add_le_of_le_neg_add {a b c : Int} (h : b -a + c) : a + b c := by
have h := Int.add_le_add_left h a
rwa [Int.add_neg_cancel_left] at h
protected theorem le_neg_add_of_add_le {a b c : Int} (h : a + b c) : b -a + c := by
have h := Int.add_le_add_left h (-a)
rwa [Int.neg_add_cancel_left] at h
protected theorem add_le_of_le_sub_left {a b c : Int} (h : b c - a) : a + b c := by
have h := Int.add_le_add_left h a
rwa [ Int.add_sub_assoc, Int.add_comm a c, Int.add_sub_cancel] at h
protected theorem le_sub_left_of_add_le {a b c : Int} (h : a + b c) : b c - a := by
have h := Int.add_le_add_right h (-a)
rwa [Int.add_comm a b, Int.add_neg_cancel_right] at h
protected theorem add_le_of_le_sub_right {a b c : Int} (h : a c - b) : a + b c := by
have h := Int.add_le_add_right h b
rwa [Int.sub_add_cancel] at h
protected theorem le_sub_right_of_add_le {a b c : Int} (h : a + b c) : a c - b := by
have h := Int.add_le_add_right h (-b)
rwa [Int.add_neg_cancel_right] at h
protected theorem le_add_of_neg_add_le {a b c : Int} (h : -b + a c) : a b + c := by
have h := Int.add_le_add_left h b
rwa [Int.add_neg_cancel_left] at h
protected theorem neg_add_le_of_le_add {a b c : Int} (h : a b + c) : -b + a c := by
have h := Int.add_le_add_left h (-b)
rwa [Int.neg_add_cancel_left] at h
protected theorem le_add_of_sub_left_le {a b c : Int} (h : a - b c) : a b + c := by
have h := Int.add_le_add_right h b
rwa [Int.sub_add_cancel, Int.add_comm] at h
protected theorem le_add_of_sub_right_le {a b c : Int} (h : a - c b) : a b + c := by
have h := Int.add_le_add_right h c
rwa [Int.sub_add_cancel] at h
protected theorem sub_right_le_of_le_add {a b c : Int} (h : a b + c) : a - c b := by
have h := Int.add_le_add_right h (-c)
rwa [Int.add_neg_cancel_right] at h
protected theorem le_add_of_neg_add_le_left {a b c : Int} (h : -b + a c) : a b + c := by
rw [Int.add_comm] at h
exact Int.le_add_of_sub_left_le h
protected theorem neg_add_le_left_of_le_add {a b c : Int} (h : a b + c) : -b + a c := by
rw [Int.add_comm]
exact Int.sub_left_le_of_le_add h
protected theorem le_add_of_neg_add_le_right {a b c : Int} (h : -c + a b) : a b + c := by
rw [Int.add_comm] at h
exact Int.le_add_of_sub_right_le h
protected theorem neg_add_le_right_of_le_add {a b c : Int} (h : a b + c) : -c + a b := by
rw [Int.add_comm] at h
exact Int.neg_add_le_left_of_le_add h
protected theorem le_add_of_neg_le_sub_left {a b c : Int} (h : -a b - c) : c a + b :=
Int.le_add_of_neg_add_le_left (Int.add_le_of_le_sub_right h)
protected theorem neg_le_sub_left_of_le_add {a b c : Int} (h : c a + b) : -a b - c := by
have h := Int.le_neg_add_of_add_le (Int.sub_left_le_of_le_add h)
rwa [Int.add_comm] at h
protected theorem le_add_of_neg_le_sub_right {a b c : Int} (h : -b a - c) : c a + b :=
Int.le_add_of_sub_right_le (Int.add_le_of_le_sub_left h)
protected theorem neg_le_sub_right_of_le_add {a b c : Int} (h : c a + b) : -b a - c :=
Int.le_sub_left_of_add_le (Int.sub_right_le_of_le_add h)
protected theorem sub_le_of_sub_le {a b c : Int} (h : a - b c) : a - c b :=
Int.sub_left_le_of_le_add (Int.le_add_of_sub_right_le h)
protected theorem sub_le_sub_left {a b : Int} (h : a b) (c : Int) : c - b c - a :=
Int.add_le_add_left (Int.neg_le_neg h) c
protected theorem sub_le_sub_right {a b : Int} (h : a b) (c : Int) : a - c b - c :=
Int.add_le_add_right h (-c)
protected theorem sub_le_sub {a b c d : Int} (hab : a b) (hcd : c d) : a - d b - c :=
Int.add_le_add hab (Int.neg_le_neg hcd)
protected theorem add_lt_of_lt_neg_add {a b c : Int} (h : b < -a + c) : a + b < c := by
have h := Int.add_lt_add_left h a
rwa [Int.add_neg_cancel_left] at h
protected theorem lt_neg_add_of_add_lt {a b c : Int} (h : a + b < c) : b < -a + c := by
have h := Int.add_lt_add_left h (-a)
rwa [Int.neg_add_cancel_left] at h
protected theorem add_lt_of_lt_sub_left {a b c : Int} (h : b < c - a) : a + b < c := by
have h := Int.add_lt_add_left h a
rwa [ Int.add_sub_assoc, Int.add_comm a c, Int.add_sub_cancel] at h
protected theorem lt_sub_left_of_add_lt {a b c : Int} (h : a + b < c) : b < c - a := by
have h := Int.add_lt_add_right h (-a)
rwa [Int.add_comm a b, Int.add_neg_cancel_right] at h
protected theorem add_lt_of_lt_sub_right {a b c : Int} (h : a < c - b) : a + b < c := by
have h := Int.add_lt_add_right h b
rwa [Int.sub_add_cancel] at h
protected theorem lt_sub_right_of_add_lt {a b c : Int} (h : a + b < c) : a < c - b := by
have h := Int.add_lt_add_right h (-b)
rwa [Int.add_neg_cancel_right] at h
protected theorem lt_add_of_neg_add_lt {a b c : Int} (h : -b + a < c) : a < b + c := by
have h := Int.add_lt_add_left h b
rwa [Int.add_neg_cancel_left] at h
protected theorem neg_add_lt_of_lt_add {a b c : Int} (h : a < b + c) : -b + a < c := by
have h := Int.add_lt_add_left h (-b)
rwa [Int.neg_add_cancel_left] at h
protected theorem lt_add_of_sub_left_lt {a b c : Int} (h : a - b < c) : a < b + c := by
have h := Int.add_lt_add_right h b
rwa [Int.sub_add_cancel, Int.add_comm] at h
protected theorem sub_left_lt_of_lt_add {a b c : Int} (h : a < b + c) : a - b < c := by
have h := Int.add_lt_add_right h (-b)
rwa [Int.add_comm b c, Int.add_neg_cancel_right] at h
protected theorem lt_add_of_sub_right_lt {a b c : Int} (h : a - c < b) : a < b + c := by
have h := Int.add_lt_add_right h c
rwa [Int.sub_add_cancel] at h
protected theorem sub_right_lt_of_lt_add {a b c : Int} (h : a < b + c) : a - c < b := by
have h := Int.add_lt_add_right h (-c)
rwa [Int.add_neg_cancel_right] at h
protected theorem lt_add_of_neg_add_lt_left {a b c : Int} (h : -b + a < c) : a < b + c := by
rw [Int.add_comm] at h
exact Int.lt_add_of_sub_left_lt h
protected theorem neg_add_lt_left_of_lt_add {a b c : Int} (h : a < b + c) : -b + a < c := by
rw [Int.add_comm]
exact Int.sub_left_lt_of_lt_add h
protected theorem lt_add_of_neg_add_lt_right {a b c : Int} (h : -c + a < b) : a < b + c := by
rw [Int.add_comm] at h
exact Int.lt_add_of_sub_right_lt h
protected theorem neg_add_lt_right_of_lt_add {a b c : Int} (h : a < b + c) : -c + a < b := by
rw [Int.add_comm] at h
exact Int.neg_add_lt_left_of_lt_add h
protected theorem lt_add_of_neg_lt_sub_left {a b c : Int} (h : -a < b - c) : c < a + b :=
Int.lt_add_of_neg_add_lt_left (Int.add_lt_of_lt_sub_right h)
protected theorem neg_lt_sub_left_of_lt_add {a b c : Int} (h : c < a + b) : -a < b - c := by
have h := Int.lt_neg_add_of_add_lt (Int.sub_left_lt_of_lt_add h)
rwa [Int.add_comm] at h
protected theorem lt_add_of_neg_lt_sub_right {a b c : Int} (h : -b < a - c) : c < a + b :=
Int.lt_add_of_sub_right_lt (Int.add_lt_of_lt_sub_left h)
protected theorem neg_lt_sub_right_of_lt_add {a b c : Int} (h : c < a + b) : -b < a - c :=
Int.lt_sub_left_of_add_lt (Int.sub_right_lt_of_lt_add h)
protected theorem sub_lt_of_sub_lt {a b c : Int} (h : a - b < c) : a - c < b :=
Int.sub_left_lt_of_lt_add (Int.lt_add_of_sub_right_lt h)
protected theorem sub_lt_sub_left {a b : Int} (h : a < b) (c : Int) : c - b < c - a :=
Int.add_lt_add_left (Int.neg_lt_neg h) c
protected theorem sub_lt_sub_right {a b : Int} (h : a < b) (c : Int) : a - c < b - c :=
Int.add_lt_add_right h (-c)
protected theorem sub_lt_sub {a b c d : Int} (hab : a < b) (hcd : c < d) : a - d < b - c :=
Int.add_lt_add hab (Int.neg_lt_neg hcd)
protected theorem sub_lt_sub_of_le_of_lt {a b c d : Int}
(hab : a b) (hcd : c < d) : a - d < b - c :=
Int.add_lt_add_of_le_of_lt hab (Int.neg_lt_neg hcd)
protected theorem sub_lt_sub_of_lt_of_le {a b c d : Int}
(hab : a < b) (hcd : c d) : a - d < b - c :=
Int.add_lt_add_of_lt_of_le hab (Int.neg_le_neg hcd)
protected theorem add_le_add_three {a b c d e f : Int}
(h₁ : a d) (h₂ : b e) (h₃ : c f) : a + b + c d + e + f :=
Int.add_le_add (Int.add_le_add h₁ h₂) h₃
theorem exists_eq_neg_ofNat {a : Int} (H : a 0) : n : Nat, a = -(n : Int) :=
let n, h := eq_ofNat_of_zero_le (Int.neg_nonneg_of_nonpos H)
n, Int.eq_neg_of_eq_neg h.symm
theorem lt_of_add_one_le {a b : Int} (H : a + 1 b) : a < b := H
theorem lt_add_one_of_le {a b : Int} (H : a b) : a < b + 1 := Int.add_le_add_right H 1
theorem le_of_lt_add_one {a b : Int} (H : a < b + 1) : a b := Int.le_of_add_le_add_right H
theorem sub_one_lt_of_le {a b : Int} (H : a b) : a - 1 < b :=
Int.sub_right_lt_of_lt_add <| lt_add_one_of_le H
theorem le_of_sub_one_lt {a b : Int} (H : a - 1 < b) : a b :=
le_of_lt_add_one <| Int.lt_add_of_sub_right_lt H
theorem le_sub_one_of_lt {a b : Int} (H : a < b) : a b - 1 := Int.le_sub_right_of_add_le H
theorem lt_of_le_sub_one {a b : Int} (H : a b - 1) : a < b := Int.add_le_of_le_sub_right H
/- ### Order properties and multiplication -/
protected theorem mul_lt_mul {a b c d : Int}
(h₁ : a < c) (h₂ : b d) (h₃ : 0 < b) (h₄ : 0 c) : a * b < c * d :=
Int.lt_of_lt_of_le (Int.mul_lt_mul_of_pos_right h₁ h₃) (Int.mul_le_mul_of_nonneg_left h₂ h₄)
protected theorem mul_lt_mul' {a b c d : Int}
(h₁ : a c) (h₂ : b < d) (h₃ : 0 b) (h₄ : 0 < c) : a * b < c * d :=
Int.lt_of_le_of_lt (Int.mul_le_mul_of_nonneg_right h₁ h₃) (Int.mul_lt_mul_of_pos_left h₂ h₄)
protected theorem mul_neg_of_pos_of_neg {a b : Int} (ha : 0 < a) (hb : b < 0) : a * b < 0 := by
have h : a * b < a * 0 := Int.mul_lt_mul_of_pos_left hb ha
rwa [Int.mul_zero] at h
protected theorem mul_neg_of_neg_of_pos {a b : Int} (ha : a < 0) (hb : 0 < b) : a * b < 0 := by
have h : a * b < 0 * b := Int.mul_lt_mul_of_pos_right ha hb
rwa [Int.zero_mul] at h
protected theorem mul_nonneg_of_nonpos_of_nonpos {a b : Int}
(ha : a 0) (hb : b 0) : 0 a * b := by
have : 0 * b a * b := Int.mul_le_mul_of_nonpos_right ha hb
rwa [Int.zero_mul] at this
protected theorem mul_lt_mul_of_neg_left {a b c : Int} (h : b < a) (hc : c < 0) : c * a < c * b :=
have : -c > 0 := Int.neg_pos_of_neg hc
have : -c * b < -c * a := Int.mul_lt_mul_of_pos_left h this
have : -(c * b) < -(c * a) := by
rwa [ Int.neg_mul_eq_neg_mul, Int.neg_mul_eq_neg_mul] at this
Int.lt_of_neg_lt_neg this
protected theorem mul_lt_mul_of_neg_right {a b c : Int} (h : b < a) (hc : c < 0) : a * c < b * c :=
have : -c > 0 := Int.neg_pos_of_neg hc
have : b * -c < a * -c := Int.mul_lt_mul_of_pos_right h this
have : -(b * c) < -(a * c) := by
rwa [ Int.neg_mul_eq_mul_neg, Int.neg_mul_eq_mul_neg] at this
Int.lt_of_neg_lt_neg this
protected theorem mul_pos_of_neg_of_neg {a b : Int} (ha : a < 0) (hb : b < 0) : 0 < a * b := by
have : 0 * b < a * b := Int.mul_lt_mul_of_neg_right ha hb
rwa [Int.zero_mul] at this
protected theorem mul_self_le_mul_self {a b : Int} (h1 : 0 a) (h2 : a b) : a * a b * b :=
Int.mul_le_mul h2 h2 h1 (Int.le_trans h1 h2)
protected theorem mul_self_lt_mul_self {a b : Int} (h1 : 0 a) (h2 : a < b) : a * a < b * b :=
Int.mul_lt_mul' (Int.le_of_lt h2) h2 h1 (Int.lt_of_le_of_lt h1 h2)
/- ## sign -/
@[simp] theorem sign_zero : sign 0 = 0 := rfl
@[simp] theorem sign_one : sign 1 = 1 := rfl
theorem sign_neg_one : sign (-1) = -1 := rfl
@[simp] theorem sign_of_add_one (x : Nat) : Int.sign (x + 1) = 1 := rfl
@[simp] theorem sign_negSucc (x : Nat) : Int.sign (Int.negSucc x) = -1 := rfl
theorem natAbs_sign (z : Int) : z.sign.natAbs = if z = 0 then 0 else 1 :=
match z with | 0 | succ _ | -[_+1] => rfl
theorem natAbs_sign_of_nonzero {z : Int} (hz : z 0) : z.sign.natAbs = 1 := by
rw [Int.natAbs_sign, if_neg hz]
theorem sign_ofNat_of_nonzero {n : Nat} (hn : n 0) : Int.sign n = 1 :=
match n, Nat.exists_eq_succ_of_ne_zero hn with
| _, n, rfl => Int.sign_of_add_one n
@[simp] theorem sign_neg (z : Int) : Int.sign (-z) = -Int.sign z := by
match z with | 0 | succ _ | -[_+1] => rfl
theorem sign_mul_natAbs : a : Int, sign a * natAbs a = a
| 0 => rfl
| succ _ => Int.one_mul _
| -[_+1] => (Int.neg_eq_neg_one_mul _).symm
@[simp] theorem sign_mul : a b, sign (a * b) = sign a * sign b
| a, 0 | 0, b => by simp [Int.mul_zero, Int.zero_mul]
| succ _, succ _ | succ _, -[_+1] | -[_+1], succ _ | -[_+1], -[_+1] => rfl
theorem sign_eq_one_of_pos {a : Int} (h : 0 < a) : sign a = 1 :=
match a, eq_succ_of_zero_lt h with
| _, _, rfl => rfl
theorem sign_eq_neg_one_of_neg {a : Int} (h : a < 0) : sign a = -1 :=
match a, eq_negSucc_of_lt_zero h with
| _, _, rfl => rfl
theorem eq_zero_of_sign_eq_zero : {a : Int}, sign a = 0 a = 0
| 0, _ => rfl
theorem pos_of_sign_eq_one : {a : Int}, sign a = 1 0 < a
| (_ + 1 : Nat), _ => ofNat_lt.2 (Nat.succ_pos _)
theorem neg_of_sign_eq_neg_one : {a : Int}, sign a = -1 a < 0
| (_ + 1 : Nat), h => nomatch h
| 0, h => nomatch h
| -[_+1], _ => negSucc_lt_zero _
theorem sign_eq_one_iff_pos (a : Int) : sign a = 1 0 < a :=
pos_of_sign_eq_one, sign_eq_one_of_pos
theorem sign_eq_neg_one_iff_neg (a : Int) : sign a = -1 a < 0 :=
neg_of_sign_eq_neg_one, sign_eq_neg_one_of_neg
@[simp] theorem sign_eq_zero_iff_zero (a : Int) : sign a = 0 a = 0 :=
eq_zero_of_sign_eq_zero, fun h => by rw [h, sign_zero]
@[simp] theorem sign_sign : sign (sign x) = sign x := by
match x with
| 0 => rfl
| .ofNat (_ + 1) => rfl
| .negSucc _ => rfl
@[simp] theorem sign_nonneg : 0 sign x 0 x := by
match x with
| 0 => rfl
| .ofNat (_ + 1) =>
simp (config := { decide := true }) only [sign, true_iff]
exact Int.le_add_one (ofNat_nonneg _)
| .negSucc _ => simp (config := { decide := true }) [sign]
theorem mul_sign : i : Int, i * sign i = natAbs i
| succ _ => Int.mul_one _
| 0 => Int.mul_zero _
| -[_+1] => Int.mul_neg_one _
/- ## natAbs -/
theorem natAbs_ne_zero {a : Int} : a.natAbs 0 a 0 := not_congr Int.natAbs_eq_zero
theorem natAbs_mul_self : {a : Int}, (natAbs a * natAbs a) = a * a
| ofNat _ => rfl
| -[_+1] => rfl
theorem eq_nat_or_neg (a : Int) : n : Nat, a = n a = -n := _, natAbs_eq a
theorem natAbs_mul_natAbs_eq {a b : Int} {c : Nat}
(h : a * b = (c : Int)) : a.natAbs * b.natAbs = c := by rw [ natAbs_mul, h, natAbs]
@[simp] theorem natAbs_mul_self' (a : Int) : (natAbs a * natAbs a : Int) = a * a := by
rw [ Int.ofNat_mul, natAbs_mul_self]
theorem natAbs_eq_iff {a : Int} {n : Nat} : a.natAbs = n a = n a = -n := by
rw [ Int.natAbs_eq_natAbs_iff, Int.natAbs_ofNat]
theorem natAbs_add_le (a b : Int) : natAbs (a + b) natAbs a + natAbs b := by
suffices a b : Nat, natAbs (subNatNat a b.succ) (a + b).succ by
match a, b with
| (a:Nat), (b:Nat) => rw [ofNat_add_ofNat, natAbs_ofNat]; apply Nat.le_refl
| (a:Nat), -[b+1] => rw [natAbs_ofNat, natAbs_negSucc]; apply this
| -[a+1], (b:Nat) =>
rw [natAbs_negSucc, natAbs_ofNat, Nat.succ_add, Nat.add_comm a b]; apply this
| -[a+1], -[b+1] => rw [natAbs_negSucc, succ_add]; apply Nat.le_refl
refine fun a b => subNatNat_elim a b.succ
(fun m n i => n = b.succ natAbs i (m + b).succ) ?_
(fun i n (e : (n + i).succ = _) => ?_) rfl
· rintro i n rfl
rw [Nat.add_comm _ i, Nat.add_assoc]
exact Nat.le_add_right i (b.succ + b).succ
· apply succ_le_succ
rw [ succ.inj e, Nat.add_assoc, Nat.add_comm]
apply Nat.le_add_right
theorem natAbs_sub_le (a b : Int) : natAbs (a - b) natAbs a + natAbs b := by
rw [ Int.natAbs_neg b]; apply natAbs_add_le
theorem negSucc_eq' (m : Nat) : -[m+1] = -m - 1 := by simp only [negSucc_eq, Int.neg_add]; rfl
theorem natAbs_lt_natAbs_of_nonneg_of_lt {a b : Int}
(w₁ : 0 a) (w₂ : a < b) : a.natAbs < b.natAbs :=
match a, b, eq_ofNat_of_zero_le w₁, eq_ofNat_of_zero_le (Int.le_trans w₁ (Int.le_of_lt w₂)) with
| _, _, _, rfl, _, rfl => ofNat_lt.1 w₂
theorem eq_natAbs_iff_mul_eq_zero : natAbs a = n (a - n) * (a + n) = 0 := by
rw [natAbs_eq_iff, Int.mul_eq_zero, Int.sub_neg, Int.sub_eq_zero, Int.sub_eq_zero]
end Int

View File

@@ -0,0 +1,44 @@
/-
Copyright (c) 2016 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
-/
prelude
import Init.Data.Int.Lemmas
namespace Int
/-! # pow -/
protected theorem pow_zero (b : Int) : b^0 = 1 := rfl
protected theorem pow_succ (b : Int) (e : Nat) : b ^ (e+1) = (b ^ e) * b := rfl
protected theorem pow_succ' (b : Int) (e : Nat) : b ^ (e+1) = b * (b ^ e) := by
rw [Int.mul_comm, Int.pow_succ]
theorem pow_le_pow_of_le_left {n m : Nat} (h : n m) : (i : Nat), n^i m^i
| 0 => Nat.le_refl _
| i + 1 => Nat.mul_le_mul (pow_le_pow_of_le_left h i) h
theorem pow_le_pow_of_le_right {n : Nat} (hx : n > 0) {i : Nat} : {j}, i j n^i n^j
| 0, h =>
have : i = 0 := Nat.eq_zero_of_le_zero h
this.symm Nat.le_refl _
| j + 1, h =>
match Nat.le_or_eq_of_le_succ h with
| Or.inl h => show n^i n^j * n from
have : n^i * 1 n^j * n := Nat.mul_le_mul (pow_le_pow_of_le_right hx h) hx
Nat.mul_one (n^i) this
| Or.inr h =>
h.symm Nat.le_refl _
theorem pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n^m :=
pow_le_pow_of_le_right h (Nat.zero_le _)
theorem natCast_pow (b n : Nat) : ((b^n : Nat) : Int) = (b : Int) ^ n := by
match n with
| 0 => rfl
| n + 1 =>
simp only [Nat.pow_succ, Int.pow_succ, natCast_mul, natCast_pow _ n]
end Int

View File

@@ -458,7 +458,7 @@ contains the longest initial segment for which `p` returns true
and the second part is everything else.
* `span (· > 5) [6, 8, 9, 5, 2, 9] = ([6, 8, 9], [5, 2, 9])`
* `span (· > 10) [6, 8, 9, 5, 2, 9] = ([6, 8, 9, 5, 2, 9], [])`
* `span (· > 10) [6, 8, 9, 5, 2, 9] = ([], [6, 8, 9, 5, 2, 9])`
-/
@[inline] def span (p : α Bool) (as : List α) : List α × List α :=
loop as []

View File

@@ -266,6 +266,12 @@ theorem get?_reverse {l : List α} (i) (h : i < length l) :
rw [Nat.add_sub_of_le (Nat.le_sub_one_of_lt h),
Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) h)]
@[simp] theorem getD_nil : getD [] n d = d := rfl
@[simp] theorem getD_cons_zero : getD (x :: xs) 0 d = x := rfl
@[simp] theorem getD_cons_succ : getD (x :: xs) (n + 1) d = getD xs n d := rfl
/-! ### take and drop -/
@[simp] theorem take_append_drop : (n : Nat) (l : List α), take n l ++ drop n l = l

View File

@@ -17,3 +17,5 @@ import Init.Data.Nat.Linear
import Init.Data.Nat.SOM
import Init.Data.Nat.Lemmas
import Init.Data.Nat.Mod
import Init.Data.Nat.Lcm
import Init.Data.Nat.Compare

View File

@@ -10,6 +10,29 @@ universe u
namespace Nat
/-- Compiled version of `Nat.rec` so that we can define `Nat.recAux` to be defeq to `Nat.rec`.
This is working around the fact that the compiler does not currently support recursors. -/
private def recCompiled {motive : Nat Sort u} (zero : motive zero) (succ : (n : Nat) motive n motive (Nat.succ n)) : (t : Nat) motive t
| .zero => zero
| .succ n => succ n (recCompiled zero succ n)
@[csimp]
private theorem rec_eq_recCompiled : @Nat.rec = @Nat.recCompiled :=
funext fun _ => funext fun _ => funext fun succ => funext fun t =>
Nat.recOn t rfl (fun n ih => congrArg (succ n) ih)
/-- Recursor identical to `Nat.rec` but uses notations `0` for `Nat.zero` and `· + 1` for `Nat.succ`.
Used as the default `Nat` eliminator by the `induction` tactic. -/
@[elab_as_elim, induction_eliminator]
protected abbrev recAux {motive : Nat Sort u} (zero : motive 0) (succ : (n : Nat) motive n motive (n + 1)) (t : Nat) : motive t :=
Nat.rec zero succ t
/-- Recursor identical to `Nat.casesOn` but uses notations `0` for `Nat.zero` and `· + 1` for `Nat.succ`.
Used as the default `Nat` eliminator by the `cases` tactic. -/
@[elab_as_elim, cases_eliminator]
protected abbrev casesAuxOn {motive : Nat Sort u} (t : Nat) (zero : motive 0) (succ : (n : Nat) motive (n + 1)) : motive t :=
Nat.casesOn t zero succ
/--
`Nat.fold` evaluates `f` on the numbers up to `n` exclusive, in increasing order:
* `Nat.fold f 3 init = init |> f 0 |> f 1 |> f 2`
@@ -125,9 +148,12 @@ theorem add_succ (n m : Nat) : n + succ m = succ (n + m) :=
theorem add_one (n : Nat) : n + 1 = succ n :=
rfl
theorem succ_eq_add_one (n : Nat) : succ n = n + 1 :=
@[simp] theorem succ_eq_add_one (n : Nat) : succ n = n + 1 :=
rfl
@[simp] theorem add_one_ne_zero (n : Nat) : n + 1 0 := nofun
@[simp] theorem zero_ne_add_one (n : Nat) : 0 n + 1 := nofun
protected theorem add_comm : (n m : Nat), n + m = m + n
| n, 0 => Eq.symm (Nat.zero_add n)
| n, m+1 => by
@@ -209,6 +235,9 @@ protected theorem mul_assoc : ∀ (n m k : Nat), (n * m) * k = n * (m * k)
protected theorem mul_left_comm (n m k : Nat) : n * (m * k) = m * (n * k) := by
rw [ Nat.mul_assoc, Nat.mul_comm n m, Nat.mul_assoc]
protected theorem mul_two (n) : n * 2 = n + n := by rw [Nat.mul_succ, Nat.mul_one]
protected theorem two_mul (n) : 2 * n = n + n := by rw [Nat.succ_mul, Nat.one_mul]
/-! # Inequalities -/
attribute [simp] Nat.le_refl
@@ -257,7 +286,7 @@ theorem succ_sub_succ (n m : Nat) : succ n - succ m = n - m :=
theorem sub_add_eq (a b c : Nat) : a - (b + c) = a - b - c := by
induction c with
| zero => simp
| succ c ih => simp [Nat.add_succ, Nat.sub_succ, ih]
| succ c ih => simp only [Nat.add_succ, Nat.sub_succ, ih]
protected theorem lt_of_lt_of_le {n m k : Nat} : n < m m k n < k :=
Nat.le_trans
@@ -606,8 +635,6 @@ protected theorem zero_ne_one : 0 ≠ (1 : Nat) :=
@[simp] theorem succ_ne_zero (n : Nat) : succ n 0 :=
fun h => Nat.noConfusion h
theorem add_one_ne_zero (n) : n + 1 0 := succ_ne_zero _
/-! # mul + order -/
theorem mul_le_mul_left {n m : Nat} (k : Nat) (h : n m) : k * n k * m :=
@@ -716,6 +743,11 @@ theorem succ_pred {a : Nat} (h : a ≠ 0) : a.pred.succ = a := by
theorem succ_pred_eq_of_pos : {n}, 0 < n succ (pred n) = n
| _+1, _ => rfl
theorem sub_one_add_one_eq_of_pos : {n}, 0 < n (n - 1) + 1 = n
| _+1, _ => rfl
@[simp] theorem pred_eq_sub_one : pred n = n - 1 := rfl
/-! # sub theorems -/
theorem add_sub_self_left (a b : Nat) : (a + b) - a = b := by
@@ -738,7 +770,7 @@ theorem zero_lt_sub_of_lt (h : i < a) : 0 < a - i := by
| zero => contradiction
| succ a ih =>
match Nat.eq_or_lt_of_le h with
| Or.inl h => injection h with h; subst h; rw [Nat.add_one, Nat.add_sub_self_left]; decide
| Or.inl h => injection h with h; subst h; rw [Nat.add_sub_self_left]; decide
| Or.inr h =>
have : 0 < a - i := ih (Nat.lt_of_succ_lt_succ h)
exact Nat.lt_of_lt_of_le this (Nat.sub_le_succ_sub _ _)
@@ -752,7 +784,7 @@ theorem sub_succ_lt_self (a i : Nat) (h : i < a) : a - (i + 1) < a - i := by
theorem sub_ne_zero_of_lt : {a b : Nat} a < b b - a 0
| 0, 0, h => absurd h (Nat.lt_irrefl 0)
| 0, succ b, _ => by simp
| 0, succ b, _ => by simp only [Nat.sub_zero, ne_eq, not_false_eq_true]
| succ a, 0, h => absurd h (Nat.not_lt_zero a.succ)
| succ a, succ b, h => by rw [Nat.succ_sub_succ]; exact sub_ne_zero_of_lt (Nat.lt_of_succ_lt_succ h)
@@ -770,7 +802,7 @@ theorem add_sub_of_le {a b : Nat} (h : a ≤ b) : a + (b - a) = b := by
protected theorem add_sub_add_right (n k m : Nat) : (n + k) - (m + k) = n - m := by
induction k with
| zero => simp
| succ k ih => simp [add_succ, add_succ, succ_sub_succ, ih]
| succ k ih => simp [ Nat.add_assoc, ih]
protected theorem add_sub_add_left (k n m : Nat) : (k + n) - (k + m) = n - m := by
rw [Nat.add_comm k n, Nat.add_comm k m, Nat.add_sub_add_right]
@@ -883,7 +915,7 @@ protected theorem sub_pos_of_lt (h : m < n) : 0 < n - m :=
protected theorem sub_sub (n m k : Nat) : n - m - k = n - (m + k) := by
induction k with
| zero => simp
| succ k ih => rw [Nat.add_succ, Nat.sub_succ, Nat.sub_succ, ih]
| succ k ih => rw [Nat.add_succ, Nat.sub_succ, Nat.add_succ, Nat.sub_succ, ih]
protected theorem sub_le_sub_left (h : n m) (k : Nat) : k - m k - n :=
match m, le.dest h with

View File

@@ -63,7 +63,7 @@ theorem shiftRight_succ (m n) : m >>> (n + 1) = (m >>> n) / 2 := rfl
theorem shiftRight_add (m n : Nat) : k, m >>> (n + k) = (m >>> n) >>> k
| 0 => rfl
| k + 1 => by simp [add_succ, shiftRight_add, shiftRight_succ]
| k + 1 => by simp [ Nat.add_assoc, shiftRight_add _ _ k, shiftRight_succ]
theorem shiftRight_eq_div_pow (m : Nat) : n, m >>> n = m / 2 ^ n
| 0 => (Nat.div_one _).symm

View File

@@ -6,6 +6,7 @@ Authors: Joe Hendrix
prelude
import Init.Data.Bool
import Init.Data.Int.Pow
import Init.Data.Nat.Bitwise.Basic
import Init.Data.Nat.Lemmas
import Init.TacticsExtra

View File

@@ -0,0 +1,57 @@
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
-/
prelude
import Init.Classical
import Init.Data.Ord
/-! # Basic lemmas about comparing natural numbers
This file introduce some basic lemmas about compare as applied to natural
numbers.
-/
namespace Nat
theorem compare_def_lt (a b : Nat) :
compare a b = if a < b then .lt else if b < a then .gt else .eq := by
simp only [compare, compareOfLessAndEq]
split
· rfl
· next h =>
match Nat.lt_or_eq_of_le (Nat.not_lt.1 h) with
| .inl h => simp [h, Nat.ne_of_gt h]
| .inr rfl => simp
theorem compare_def_le (a b : Nat) :
compare a b = if a b then if b a then .eq else .lt else .gt := by
rw [compare_def_lt]
split
· next hlt => simp [Nat.le_of_lt hlt, Nat.not_le.2 hlt]
· next hge =>
split
· next hgt => simp [Nat.le_of_lt hgt, Nat.not_le.2 hgt]
· next hle => simp [Nat.not_lt.1 hge, Nat.not_lt.1 hle]
protected theorem compare_swap (a b : Nat) : (compare a b).swap = compare b a := by
simp only [compare_def_le]; (repeat' split) <;> try rfl
next h1 h2 => cases h1 (Nat.le_of_not_le h2)
protected theorem compare_eq_eq {a b : Nat} : compare a b = .eq a = b := by
rw [compare_def_lt]; (repeat' split) <;> simp [Nat.ne_of_lt, Nat.ne_of_gt, *]
next hlt hgt => exact Nat.le_antisymm (Nat.not_lt.1 hgt) (Nat.not_lt.1 hlt)
protected theorem compare_eq_lt {a b : Nat} : compare a b = .lt a < b := by
rw [compare_def_lt]; (repeat' split) <;> simp [*]
protected theorem compare_eq_gt {a b : Nat} : compare a b = .gt b < a := by
rw [compare_def_lt]; (repeat' split) <;> simp [Nat.le_of_lt, *]
protected theorem compare_ne_gt {a b : Nat} : compare a b .gt a b := by
rw [compare_def_le]; (repeat' split) <;> simp [*]
protected theorem compare_ne_lt {a b : Nat} : compare a b .lt b a := by
rw [compare_def_le]; (repeat' split) <;> simp [Nat.le_of_not_le, *]
end Nat

View File

@@ -10,6 +10,13 @@ import Init.Data.Nat.Basic
namespace Nat
/--
Divisibility of natural numbers. `a b` (typed as `\|`) says that
there is some `c` such that `b = a * c`.
-/
instance : Dvd Nat where
dvd a b := Exists (fun c => b = a * c)
theorem div_rec_lemma {x y : Nat} : 0 < y y x x - y < x :=
fun ypos, ylex => sub_lt (Nat.lt_of_lt_of_le ypos ylex) ypos
@@ -28,7 +35,7 @@ theorem div_eq (x y : Nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 e
rw [Nat.div]
rfl
theorem div.inductionOn.{u}
def div.inductionOn.{u}
{motive : Nat Nat Sort u}
(x y : Nat)
(ind : x y, 0 < y y x motive (x - y) y motive x y)
@@ -95,7 +102,7 @@ protected theorem modCore_eq_mod (x y : Nat) : Nat.modCore x y = x % y := by
theorem mod_eq (x y : Nat) : x % y = if 0 < y y x then (x - y) % y else x := by
rw [Nat.modCore_eq_mod, Nat.modCore_eq_mod, Nat.modCore]
theorem mod.inductionOn.{u}
def mod.inductionOn.{u}
{motive : Nat Nat Sort u}
(x y : Nat)
(ind : x y, 0 < y y x motive (x - y) y motive x y)
@@ -198,11 +205,11 @@ theorem le_div_iff_mul_le (k0 : 0 < k) : x ≤ y / k ↔ x * k ≤ y := by
induction y, k using mod.inductionOn generalizing x with
(rw [div_eq]; simp [h]; cases x with | zero => simp [zero_le] | succ x => ?_)
| base y k h =>
simp [not_succ_le_zero x, succ_mul, Nat.add_comm]
refine Nat.lt_of_lt_of_le ?_ (Nat.le_add_right ..)
simp only [add_one, succ_mul, false_iff, Nat.not_le]
refine Nat.lt_of_lt_of_le ?_ (Nat.le_add_left ..)
exact Nat.not_le.1 fun h' => h k0, h'
| ind y k h IH =>
rw [ add_one, Nat.add_le_add_iff_right, IH k0, succ_mul,
rw [Nat.add_le_add_iff_right, IH k0, succ_mul,
Nat.add_sub_cancel (x*k) k, Nat.sub_le_sub_iff_right h.2, Nat.add_sub_cancel]
protected theorem div_div_eq_div_mul (m n k : Nat) : m / n / k = m / (n * k) := by
@@ -286,7 +293,7 @@ theorem sub_mul_div (x n p : Nat) (h₁ : n*p ≤ x) : (x - n*p) / n = x / n - p
rw [mul_succ] at h₁
exact h₁
rw [sub_succ, IH h₂, div_eq_sub_div h₀ h₃]
simp [add_one, Nat.pred_succ, mul_succ, Nat.sub_sub]
simp [Nat.pred_succ, mul_succ, Nat.sub_sub]
theorem mul_sub_div (x n p : Nat) (h₁ : x < n*p) : (n * p - succ x) / n = p - succ (x / n) := by
have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun n0 => by
@@ -327,4 +334,50 @@ theorem div_eq_of_lt (h₀ : a < b) : a / b = 0 := by
intro h₁
apply Nat.not_le_of_gt h₀ h₁.right
protected theorem mul_div_cancel (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m := by
let t := add_mul_div_right 0 m H
rwa [Nat.zero_add, Nat.zero_div, Nat.zero_add] at t
protected theorem mul_div_cancel_left (m : Nat) {n : Nat} (H : 0 < n) : n * m / n = m := by
rw [Nat.mul_comm, Nat.mul_div_cancel _ H]
protected theorem div_le_of_le_mul {m n : Nat} : {k}, m k * n m / k n
| 0, _ => by simp [Nat.div_zero, n.zero_le]
| succ k, h => by
suffices succ k * (m / succ k) succ k * n from
Nat.le_of_mul_le_mul_left this (zero_lt_succ _)
have h1 : succ k * (m / succ k) m % succ k + succ k * (m / succ k) := Nat.le_add_left _ _
have h2 : m % succ k + succ k * (m / succ k) = m := by rw [mod_add_div]
have h3 : m succ k * n := h
rw [ h2] at h3
exact Nat.le_trans h1 h3
@[simp] theorem mul_div_right (n : Nat) {m : Nat} (H : 0 < m) : m * n / m = n := by
induction n <;> simp_all [mul_succ]
@[simp] theorem mul_div_left (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m := by
rw [Nat.mul_comm, mul_div_right _ H]
protected theorem div_self (H : 0 < n) : n / n = 1 := by
let t := add_div_right 0 H
rwa [Nat.zero_add, Nat.zero_div] at t
protected theorem div_eq_of_eq_mul_left (H1 : 0 < n) (H2 : m = k * n) : m / n = k :=
by rw [H2, Nat.mul_div_cancel _ H1]
protected theorem div_eq_of_eq_mul_right (H1 : 0 < n) (H2 : m = n * k) : m / n = k :=
by rw [H2, Nat.mul_div_cancel_left _ H1]
protected theorem mul_div_mul_left {m : Nat} (n k : Nat) (H : 0 < m) :
m * n / (m * k) = n / k := by rw [ Nat.div_div_eq_div_mul, Nat.mul_div_cancel_left _ H]
protected theorem mul_div_mul_right {m : Nat} (n k : Nat) (H : 0 < m) :
n * m / (k * m) = n / k := by rw [Nat.mul_comm, Nat.mul_comm k, Nat.mul_div_mul_left _ _ H]
theorem mul_div_le (m n : Nat) : n * (m / n) m := by
match n, Nat.eq_zero_or_pos n with
| _, Or.inl rfl => rw [Nat.zero_mul]; exact m.zero_le
| n, Or.inr h => rw [Nat.mul_comm, Nat.le_div_iff_mul_le h]; exact Nat.le_refl _
end Nat

View File

@@ -5,17 +5,10 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
-/
prelude
import Init.Data.Nat.Div
import Init.TacticsExtra
import Init.Meta
namespace Nat
/--
Divisibility of natural numbers. `a b` (typed as `\|`) says that
there is some `c` such that `b = a * c`.
-/
instance : Dvd Nat where
dvd a b := Exists (fun c => b = a * c)
protected theorem dvd_refl (a : Nat) : a a := 1, by simp
protected theorem dvd_zero (a : Nat) : a 0 := 0, by simp
@@ -104,4 +97,36 @@ protected theorem div_mul_cancel {n m : Nat} (H : n m) : m / n * n = m := by
subst h
rw [Nat.mul_assoc, add_mul_mod_self_left]
protected theorem dvd_of_mul_dvd_mul_left
(kpos : 0 < k) (H : k * m k * n) : m n := by
let l, H := H
rw [Nat.mul_assoc] at H
exact _, Nat.eq_of_mul_eq_mul_left kpos H
protected theorem dvd_of_mul_dvd_mul_right (kpos : 0 < k) (H : m * k n * k) : m n := by
rw [Nat.mul_comm m k, Nat.mul_comm n k] at H; exact Nat.dvd_of_mul_dvd_mul_left kpos H
theorem dvd_sub {k m n : Nat} (H : n m) (h₁ : k m) (h₂ : k n) : k m - n :=
(Nat.dvd_add_iff_left h₂).2 <| by rwa [Nat.sub_add_cancel H]
protected theorem mul_dvd_mul {a b c d : Nat} : a b c d a * c b * d
| e, he, f, hf =>
e * f, by simp [he, hf, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm]
protected theorem mul_dvd_mul_left (a : Nat) (h : b c) : a * b a * c :=
Nat.mul_dvd_mul (Nat.dvd_refl a) h
protected theorem mul_dvd_mul_right (h: a b) (c : Nat) : a * c b * c :=
Nat.mul_dvd_mul h (Nat.dvd_refl c)
@[simp] theorem dvd_one {n : Nat} : n 1 n = 1 :=
eq_one_of_dvd_one, fun h => h.symm Nat.dvd_refl _
protected theorem mul_div_assoc (m : Nat) (H : k n) : m * n / k = m * (n / k) := by
match Nat.eq_zero_or_pos k with
| .inl h0 => rw [h0, Nat.div_zero, Nat.div_zero, Nat.mul_zero]
| .inr hpos =>
have h1 : m * n / k = m * (n / k * k) / k := by rw [Nat.div_mul_cancel H]
rw [h1, Nat.mul_assoc, Nat.mul_div_cancel _ hpos]
end Nat

View File

@@ -1,10 +1,12 @@
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
-/
prelude
import Init.Data.Nat.Dvd
import Init.NotationExtra
import Init.RCases
namespace Nat
@@ -14,8 +16,8 @@ def gcd (m n : @& Nat) : Nat :=
n
else
gcd (n % m) m
termination_by m
decreasing_by simp_wf; apply mod_lt _ (zero_lt_of_ne_zero _); assumption
termination_by m
decreasing_by simp_wf; apply mod_lt _ (zero_lt_of_ne_zero _); assumption
@[simp] theorem gcd_zero_left (y : Nat) : gcd 0 y = y :=
rfl
@@ -69,4 +71,166 @@ theorem dvd_gcd : k m → k n → k gcd m n := by
| H0 n => rw [gcd_zero_left]; exact kn
| H1 n m _ IH => rw [gcd_rec]; exact IH ((dvd_mod_iff km).2 kn) km
theorem dvd_gcd_iff : k gcd m n k m k n :=
fun h => let h₁, h₂ := gcd_dvd m n; Nat.dvd_trans h h₁, Nat.dvd_trans h h₂,
fun h₁, h₂ => dvd_gcd h₁ h₂
theorem gcd_comm (m n : Nat) : gcd m n = gcd n m :=
Nat.dvd_antisymm
(dvd_gcd (gcd_dvd_right m n) (gcd_dvd_left m n))
(dvd_gcd (gcd_dvd_right n m) (gcd_dvd_left n m))
theorem gcd_eq_left_iff_dvd : m n gcd m n = m :=
fun h => by rw [gcd_rec, mod_eq_zero_of_dvd h, gcd_zero_left],
fun h => h gcd_dvd_right m n
theorem gcd_eq_right_iff_dvd : m n gcd n m = m := by
rw [gcd_comm]; exact gcd_eq_left_iff_dvd
theorem gcd_assoc (m n k : Nat) : gcd (gcd m n) k = gcd m (gcd n k) :=
Nat.dvd_antisymm
(dvd_gcd
(Nat.dvd_trans (gcd_dvd_left (gcd m n) k) (gcd_dvd_left m n))
(dvd_gcd (Nat.dvd_trans (gcd_dvd_left (gcd m n) k) (gcd_dvd_right m n))
(gcd_dvd_right (gcd m n) k)))
(dvd_gcd
(dvd_gcd (gcd_dvd_left m (gcd n k))
(Nat.dvd_trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_left n k)))
(Nat.dvd_trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_right n k)))
@[simp] theorem gcd_one_right (n : Nat) : gcd n 1 = 1 := (gcd_comm n 1).trans (gcd_one_left n)
theorem gcd_mul_left (m n k : Nat) : gcd (m * n) (m * k) = m * gcd n k := by
induction n, k using gcd.induction with
| H0 k => simp
| H1 n k _ IH => rwa [ mul_mod_mul_left, gcd_rec, gcd_rec] at IH
theorem gcd_mul_right (m n k : Nat) : gcd (m * n) (k * n) = gcd m k * n := by
rw [Nat.mul_comm m n, Nat.mul_comm k n, Nat.mul_comm (gcd m k) n, gcd_mul_left]
theorem gcd_pos_of_pos_left {m : Nat} (n : Nat) (mpos : 0 < m) : 0 < gcd m n :=
pos_of_dvd_of_pos (gcd_dvd_left m n) mpos
theorem gcd_pos_of_pos_right (m : Nat) {n : Nat} (npos : 0 < n) : 0 < gcd m n :=
pos_of_dvd_of_pos (gcd_dvd_right m n) npos
theorem div_gcd_pos_of_pos_left (b : Nat) (h : 0 < a) : 0 < a / a.gcd b :=
(Nat.le_div_iff_mul_le <| Nat.gcd_pos_of_pos_left _ h).2 (Nat.one_mul _ Nat.gcd_le_left _ h)
theorem div_gcd_pos_of_pos_right (a : Nat) (h : 0 < b) : 0 < b / a.gcd b :=
(Nat.le_div_iff_mul_le <| Nat.gcd_pos_of_pos_right _ h).2 (Nat.one_mul _ Nat.gcd_le_right _ h)
theorem eq_zero_of_gcd_eq_zero_left {m n : Nat} (H : gcd m n = 0) : m = 0 :=
match eq_zero_or_pos m with
| .inl H0 => H0
| .inr H1 => absurd (Eq.symm H) (ne_of_lt (gcd_pos_of_pos_left _ H1))
theorem eq_zero_of_gcd_eq_zero_right {m n : Nat} (H : gcd m n = 0) : n = 0 := by
rw [gcd_comm] at H
exact eq_zero_of_gcd_eq_zero_left H
theorem gcd_ne_zero_left : m 0 gcd m n 0 := mt eq_zero_of_gcd_eq_zero_left
theorem gcd_ne_zero_right : n 0 gcd m n 0 := mt eq_zero_of_gcd_eq_zero_right
theorem gcd_div {m n k : Nat} (H1 : k m) (H2 : k n) :
gcd (m / k) (n / k) = gcd m n / k :=
match eq_zero_or_pos k with
| .inl H0 => by simp [H0]
| .inr H3 => by
apply Nat.eq_of_mul_eq_mul_right H3
rw [Nat.div_mul_cancel (dvd_gcd H1 H2), gcd_mul_right,
Nat.div_mul_cancel H1, Nat.div_mul_cancel H2]
theorem gcd_dvd_gcd_of_dvd_left {m k : Nat} (n : Nat) (H : m k) : gcd m n gcd k n :=
dvd_gcd (Nat.dvd_trans (gcd_dvd_left m n) H) (gcd_dvd_right m n)
theorem gcd_dvd_gcd_of_dvd_right {m k : Nat} (n : Nat) (H : m k) : gcd n m gcd n k :=
dvd_gcd (gcd_dvd_left n m) (Nat.dvd_trans (gcd_dvd_right n m) H)
theorem gcd_dvd_gcd_mul_left (m n k : Nat) : gcd m n gcd (k * m) n :=
gcd_dvd_gcd_of_dvd_left _ (Nat.dvd_mul_left _ _)
theorem gcd_dvd_gcd_mul_right (m n k : Nat) : gcd m n gcd (m * k) n :=
gcd_dvd_gcd_of_dvd_left _ (Nat.dvd_mul_right _ _)
theorem gcd_dvd_gcd_mul_left_right (m n k : Nat) : gcd m n gcd m (k * n) :=
gcd_dvd_gcd_of_dvd_right _ (Nat.dvd_mul_left _ _)
theorem gcd_dvd_gcd_mul_right_right (m n k : Nat) : gcd m n gcd m (n * k) :=
gcd_dvd_gcd_of_dvd_right _ (Nat.dvd_mul_right _ _)
theorem gcd_eq_left {m n : Nat} (H : m n) : gcd m n = m :=
Nat.dvd_antisymm (gcd_dvd_left _ _) (dvd_gcd (Nat.dvd_refl _) H)
theorem gcd_eq_right {m n : Nat} (H : n m) : gcd m n = n := by
rw [gcd_comm, gcd_eq_left H]
@[simp] theorem gcd_mul_left_left (m n : Nat) : gcd (m * n) n = n :=
Nat.dvd_antisymm (gcd_dvd_right _ _) (dvd_gcd (Nat.dvd_mul_left _ _) (Nat.dvd_refl _))
@[simp] theorem gcd_mul_left_right (m n : Nat) : gcd n (m * n) = n := by
rw [gcd_comm, gcd_mul_left_left]
@[simp] theorem gcd_mul_right_left (m n : Nat) : gcd (n * m) n = n := by
rw [Nat.mul_comm, gcd_mul_left_left]
@[simp] theorem gcd_mul_right_right (m n : Nat) : gcd n (n * m) = n := by
rw [gcd_comm, gcd_mul_right_left]
@[simp] theorem gcd_gcd_self_right_left (m n : Nat) : gcd m (gcd m n) = gcd m n :=
Nat.dvd_antisymm (gcd_dvd_right _ _) (dvd_gcd (gcd_dvd_left _ _) (Nat.dvd_refl _))
@[simp] theorem gcd_gcd_self_right_right (m n : Nat) : gcd m (gcd n m) = gcd n m := by
rw [gcd_comm n m, gcd_gcd_self_right_left]
@[simp] theorem gcd_gcd_self_left_right (m n : Nat) : gcd (gcd n m) m = gcd n m := by
rw [gcd_comm, gcd_gcd_self_right_right]
@[simp] theorem gcd_gcd_self_left_left (m n : Nat) : gcd (gcd m n) m = gcd m n := by
rw [gcd_comm m n, gcd_gcd_self_left_right]
theorem gcd_add_mul_self (m n k : Nat) : gcd m (n + k * m) = gcd m n := by
simp [gcd_rec m (n + k * m), gcd_rec m n]
theorem gcd_eq_zero_iff {i j : Nat} : gcd i j = 0 i = 0 j = 0 :=
fun h => eq_zero_of_gcd_eq_zero_left h, eq_zero_of_gcd_eq_zero_right h,
fun h => by simp [h]
/-- Characterization of the value of `Nat.gcd`. -/
theorem gcd_eq_iff (a b : Nat) :
gcd a b = g g a g b ( c, c a c b c g) := by
constructor
· rintro rfl
exact gcd_dvd_left _ _, gcd_dvd_right _ _, fun _ => Nat.dvd_gcd
· rintro ha, hb, hc
apply Nat.dvd_antisymm
· apply hc
· exact gcd_dvd_left a b
· exact gcd_dvd_right a b
· exact Nat.dvd_gcd ha hb
/-- Represent a divisor of `m * n` as a product of a divisor of `m` and a divisor of `n`. -/
def prod_dvd_and_dvd_of_dvd_prod {k m n : Nat} (H : k m * n) :
{d : {m' // m' m} × {n' // n' n} // k = d.1.val * d.2.val} :=
if h0 : gcd k m = 0 then
0, eq_zero_of_gcd_eq_zero_right h0 Nat.dvd_refl 0,
n, Nat.dvd_refl n,
eq_zero_of_gcd_eq_zero_left h0 (Nat.zero_mul n).symm
else by
have hd : gcd k m * (k / gcd k m) = k := Nat.mul_div_cancel' (gcd_dvd_left k m)
refine gcd k m, gcd_dvd_right k m, k / gcd k m, ?_, hd.symm
apply Nat.dvd_of_mul_dvd_mul_left (Nat.pos_of_ne_zero h0)
rw [hd, gcd_mul_right]
exact Nat.dvd_gcd (Nat.dvd_mul_right _ _) H
theorem gcd_mul_dvd_mul_gcd (k m n : Nat) : gcd k (m * n) gcd k m * gcd k n := by
let m', hm', n', hn', (h : gcd k (m * n) = m' * n') :=
prod_dvd_and_dvd_of_dvd_prod <| gcd_dvd_right k (m * n)
rw [h]
have h' : m' * n' k := h gcd_dvd_left ..
exact Nat.mul_dvd_mul
(dvd_gcd (Nat.dvd_trans (Nat.dvd_mul_right m' n') h') hm')
(dvd_gcd (Nat.dvd_trans (Nat.dvd_mul_left n' m') h') hn')
end Nat

View File

@@ -0,0 +1,66 @@
/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
-/
prelude
import Init.Data.Nat.Gcd
import Init.Data.Nat.Lemmas
namespace Nat
/-- The least common multiple of `m` and `n`, defined using `gcd`. -/
def lcm (m n : Nat) : Nat := m * n / gcd m n
theorem lcm_comm (m n : Nat) : lcm m n = lcm n m := by
rw [lcm, lcm, Nat.mul_comm n m, gcd_comm n m]
@[simp] theorem lcm_zero_left (m : Nat) : lcm 0 m = 0 := by simp [lcm]
@[simp] theorem lcm_zero_right (m : Nat) : lcm m 0 = 0 := by simp [lcm]
@[simp] theorem lcm_one_left (m : Nat) : lcm 1 m = m := by simp [lcm]
@[simp] theorem lcm_one_right (m : Nat) : lcm m 1 = m := by simp [lcm]
@[simp] theorem lcm_self (m : Nat) : lcm m m = m := by
match eq_zero_or_pos m with
| .inl h => rw [h, lcm_zero_left]
| .inr h => simp [lcm, Nat.mul_div_cancel _ h]
theorem dvd_lcm_left (m n : Nat) : m lcm m n :=
n / gcd m n, by rw [ Nat.mul_div_assoc m (Nat.gcd_dvd_right m n)]; rfl
theorem dvd_lcm_right (m n : Nat) : n lcm m n := lcm_comm n m dvd_lcm_left n m
theorem gcd_mul_lcm (m n : Nat) : gcd m n * lcm m n = m * n := by
rw [lcm, Nat.mul_div_cancel' (Nat.dvd_trans (gcd_dvd_left m n) (Nat.dvd_mul_right m n))]
theorem lcm_dvd {m n k : Nat} (H1 : m k) (H2 : n k) : lcm m n k := by
match eq_zero_or_pos k with
| .inl h => rw [h]; exact Nat.dvd_zero _
| .inr kpos =>
apply Nat.dvd_of_mul_dvd_mul_left (gcd_pos_of_pos_left n (pos_of_dvd_of_pos H1 kpos))
rw [gcd_mul_lcm, gcd_mul_right, Nat.mul_comm n k]
exact dvd_gcd (Nat.mul_dvd_mul_left _ H2) (Nat.mul_dvd_mul_right H1 _)
theorem lcm_assoc (m n k : Nat) : lcm (lcm m n) k = lcm m (lcm n k) :=
Nat.dvd_antisymm
(lcm_dvd
(lcm_dvd (dvd_lcm_left m (lcm n k))
(Nat.dvd_trans (dvd_lcm_left n k) (dvd_lcm_right m (lcm n k))))
(Nat.dvd_trans (dvd_lcm_right n k) (dvd_lcm_right m (lcm n k))))
(lcm_dvd
(Nat.dvd_trans (dvd_lcm_left m n) (dvd_lcm_left (lcm m n) k))
(lcm_dvd (Nat.dvd_trans (dvd_lcm_right m n) (dvd_lcm_left (lcm m n) k))
(dvd_lcm_right (lcm m n) k)))
theorem lcm_ne_zero (hm : m 0) (hn : n 0) : lcm m n 0 := by
intro h
have h1 := gcd_mul_lcm m n
rw [h, Nat.mul_zero] at h1
match mul_eq_zero.1 h1.symm with
| .inl hm1 => exact hm hm1
| .inr hn1 => exact hn hn1
end Nat

View File

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
-/
prelude
import Init.Data.Nat.Dvd
import Init.Data.Nat.MinMax
import Init.Data.Nat.Log2
import Init.Data.Nat.Power2
import Init.Omega
/-! # Basic lemmas about natural numbers
@@ -19,7 +19,6 @@ and later these lemmas should be organised into other files more systematically.
-/
namespace Nat
/-! ## add -/
protected theorem add_add_add_comm (a b c d : Nat) : (a + b) + (c + d) = (a + c) + (b + d) := by
@@ -335,6 +334,32 @@ protected theorem sub_max_sub_right : ∀ (a b c : Nat), max (a - c) (b - c) = m
| _, _, 0 => rfl
| _, _, _+1 => Eq.trans (Nat.pred_max_pred ..) <| congrArg _ (Nat.sub_max_sub_right ..)
protected theorem sub_min_sub_left (a b c : Nat) : min (a - b) (a - c) = a - max b c := by
omega
protected theorem sub_max_sub_left (a b c : Nat) : max (a - b) (a - c) = a - min b c := by
omega
protected theorem mul_max_mul_right (a b c : Nat) : max (a * c) (b * c) = max a b * c := by
induction a generalizing b with
| zero => simp
| succ i ind =>
cases b <;> simp [succ_eq_add_one, Nat.succ_mul, Nat.add_max_add_right, ind]
protected theorem mul_min_mul_right (a b c : Nat) : min (a * c) (b * c) = min a b * c := by
induction a generalizing b with
| zero => simp
| succ i ind =>
cases b <;> simp [succ_eq_add_one, Nat.succ_mul, Nat.add_min_add_right, ind]
protected theorem mul_max_mul_left (a b c : Nat) : max (a * b) (a * c) = a * max b c := by
repeat rw [Nat.mul_comm a]
exact Nat.mul_max_mul_right ..
protected theorem mul_min_mul_left (a b c : Nat) : min (a * b) (a * c) = a * min b c := by
repeat rw [Nat.mul_comm a]
exact Nat.mul_min_mul_right ..
-- protected theorem sub_min_sub_left (a b c : Nat) : min (a - b) (a - c) = a - max b c := by
-- induction b, c using Nat.recDiagAux with
-- | zero_left => rw [Nat.sub_zero, Nat.zero_max]; exact Nat.min_eq_right (Nat.sub_le ..)
@@ -383,10 +408,6 @@ protected theorem mul_right_comm (n m k : Nat) : n * m * k = n * k * m := by
protected theorem mul_mul_mul_comm (a b c d : Nat) : (a * b) * (c * d) = (a * c) * (b * d) := by
rw [Nat.mul_assoc, Nat.mul_assoc, Nat.mul_left_comm b]
protected theorem mul_two (n) : n * 2 = n + n := by rw [Nat.mul_succ, Nat.mul_one]
protected theorem two_mul (n) : 2 * n = n + n := by rw [Nat.succ_mul, Nat.one_mul]
theorem mul_eq_zero : {m n}, n * m = 0 n = 0 m = 0
| 0, _ => fun _ => .inr rfl, fun _ => rfl
| _, 0 => fun _ => .inl rfl, fun _ => Nat.zero_mul ..
@@ -484,51 +505,6 @@ protected theorem pos_of_mul_pos_right {a b : Nat} (h : 0 < a * b) : 0 < a := by
/-! ### div/mod -/
protected theorem div_le_of_le_mul {m n : Nat} : {k}, m k * n m / k n
| 0, _ => by simp [Nat.div_zero, n.zero_le]
| succ k, h => by
suffices succ k * (m / succ k) succ k * n from
Nat.le_of_mul_le_mul_left this (zero_lt_succ _)
have h1 : succ k * (m / succ k) m % succ k + succ k * (m / succ k) := Nat.le_add_left _ _
have h2 : m % succ k + succ k * (m / succ k) = m := by rw [mod_add_div]
have h3 : m succ k * n := h
rw [ h2] at h3
exact Nat.le_trans h1 h3
@[simp] theorem mul_div_right (n : Nat) {m : Nat} (H : 0 < m) : m * n / m = n := by
induction n <;> simp_all [mul_succ]
@[simp] theorem mul_div_left (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m := by
rw [Nat.mul_comm, mul_div_right _ H]
protected theorem div_self (H : 0 < n) : n / n = 1 := by
let t := add_div_right 0 H
rwa [Nat.zero_add, Nat.zero_div] at t
protected theorem mul_div_cancel (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m := by
let t := add_mul_div_right 0 m H
rwa [Nat.zero_add, Nat.zero_div, Nat.zero_add] at t
protected theorem mul_div_cancel_left (m : Nat) {n : Nat} (H : 0 < n) : n * m / n = m :=
by rw [Nat.mul_comm, Nat.mul_div_cancel _ H]
protected theorem div_eq_of_eq_mul_left (H1 : 0 < n) (H2 : m = k * n) : m / n = k :=
by rw [H2, Nat.mul_div_cancel _ H1]
protected theorem div_eq_of_eq_mul_right (H1 : 0 < n) (H2 : m = n * k) : m / n = k :=
by rw [H2, Nat.mul_div_cancel_left _ H1]
protected theorem mul_div_mul_left {m : Nat} (n k : Nat) (H : 0 < m) :
m * n / (m * k) = n / k := by rw [ Nat.div_div_eq_div_mul, Nat.mul_div_cancel_left _ H]
protected theorem mul_div_mul_right {m : Nat} (n k : Nat) (H : 0 < m) :
n * m / (k * m) = n / k := by rw [Nat.mul_comm, Nat.mul_comm k, Nat.mul_div_mul_left _ _ H]
theorem mul_div_le (m n : Nat) : n * (m / n) m := by
match n, Nat.eq_zero_or_pos n with
| _, Or.inl rfl => rw [Nat.zero_mul]; exact m.zero_le
| n, Or.inr h => rw [Nat.mul_comm, Nat.le_div_iff_mul_le h]; exact Nat.le_refl _
theorem mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 n % 2 = 1 :=
match n % 2, @Nat.mod_lt n 2 (by decide) with
| 0, _ => .inl rfl
@@ -719,37 +695,17 @@ theorem lt_log2_self : n < 2 ^ (n.log2 + 1) :=
/-! ### dvd -/
theorem dvd_sub {k m n : Nat} (H : n m) (h₁ : k m) (h₂ : k n) : k m - n :=
(Nat.dvd_add_iff_left h₂).2 <| by rwa [Nat.sub_add_cancel H]
protected theorem eq_mul_of_div_eq_right {a b c : Nat} (H1 : b a) (H2 : a / b = c) :
a = b * c := by
rw [ H2, Nat.mul_div_cancel' H1]
protected theorem mul_dvd_mul {a b c d : Nat} : a b c d a * c b * d
| e, he, f, hf =>
e * f, by simp [he, hf, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm]
protected theorem div_eq_iff_eq_mul_right {a b c : Nat} (H : 0 < b) (H' : b a) :
a / b = c a = b * c :=
Nat.eq_mul_of_div_eq_right H', Nat.div_eq_of_eq_mul_right H
protected theorem mul_dvd_mul_left (a : Nat) (h : b c) : a * b a * c :=
Nat.mul_dvd_mul (Nat.dvd_refl a) h
protected theorem mul_dvd_mul_right (h: a b) (c : Nat) : a * c b * c :=
Nat.mul_dvd_mul h (Nat.dvd_refl c)
@[simp] theorem dvd_one {n : Nat} : n 1 n = 1 :=
eq_one_of_dvd_one, fun h => h.symm Nat.dvd_refl _
protected theorem mul_div_assoc (m : Nat) (H : k n) : m * n / k = m * (n / k) := by
match Nat.eq_zero_or_pos k with
| .inl h0 => rw [h0, Nat.div_zero, Nat.div_zero, Nat.mul_zero]
| .inr hpos =>
have h1 : m * n / k = m * (n / k * k) / k := by rw [Nat.div_mul_cancel H]
rw [h1, Nat.mul_assoc, Nat.mul_div_cancel _ hpos]
protected theorem dvd_of_mul_dvd_mul_left
(kpos : 0 < k) (H : k * m k * n) : m n := by
let l, H := H
rw [Nat.mul_assoc] at H
exact _, Nat.eq_of_mul_eq_mul_left kpos H
protected theorem dvd_of_mul_dvd_mul_right (kpos : 0 < k) (H : m * k n * k) : m n := by
rw [Nat.mul_comm m k, Nat.mul_comm n k] at H; exact Nat.dvd_of_mul_dvd_mul_left kpos H
protected theorem div_eq_iff_eq_mul_left {a b c : Nat} (H : 0 < b) (H' : b a) :
a / b = c a = c * b := by
rw [Nat.mul_comm]; exact Nat.div_eq_iff_eq_mul_right H H'
theorem pow_dvd_pow_iff_pow_le_pow {k l : Nat} :
{x : Nat}, 0 < x (x ^ k x ^ l x ^ k x ^ l)
@@ -773,18 +729,6 @@ theorem pow_dvd_pow_iff_le_right {x k l : Nat} (w : 1 < x) : x ^ k x ^ l ↔
theorem pow_dvd_pow_iff_le_right' {b k l : Nat} : (b + 2) ^ k (b + 2) ^ l k l :=
pow_dvd_pow_iff_le_right (Nat.lt_of_sub_eq_succ rfl)
protected theorem eq_mul_of_div_eq_right {a b c : Nat} (H1 : b a) (H2 : a / b = c) :
a = b * c := by
rw [ H2, Nat.mul_div_cancel' H1]
protected theorem div_eq_iff_eq_mul_right {a b c : Nat} (H : 0 < b) (H' : b a) :
a / b = c a = b * c :=
Nat.eq_mul_of_div_eq_right H', Nat.div_eq_of_eq_mul_right H
protected theorem div_eq_iff_eq_mul_left {a b c : Nat} (H : 0 < b) (H' : b a) :
a / b = c a = c * b := by
rw [Nat.mul_comm]; exact Nat.div_eq_iff_eq_mul_right H H'
protected theorem pow_dvd_pow {m n : Nat} (a : Nat) (h : m n) : a ^ m a ^ n := by
cases Nat.exists_eq_add_of_le h
case intro k p =>
@@ -836,7 +780,7 @@ theorem shiftRight_succ_inside : ∀m n, m >>> (n+1) = (m/2) >>> n
theorem shiftLeft_shiftLeft (m n : Nat) : k, (m <<< n) <<< k = m <<< (n + k)
| 0 => rfl
| k + 1 => by simp [add_succ, shiftLeft_shiftLeft _ _ k, shiftLeft_succ]
| k + 1 => by simp [ Nat.add_assoc, shiftLeft_shiftLeft _ _ k, shiftLeft_succ]
theorem mul_add_div {m : Nat} (m_pos : m > 0) (x y : Nat) : (m * x + y) / m = x + y / m := by
match x with

View File

@@ -37,6 +37,13 @@ def toMonad [Monad m] [Alternative m] : Option α → m α
| none, _ => none
| some a, b => b a
/-- Runs `f` on `o`'s value, if any, and returns its result, or else returns `none`. -/
@[inline] protected def bindM [Monad m] (f : α m (Option β)) (o : Option α) : m (Option β) := do
if let some a := o then
return ( f a)
else
return none
@[inline] protected def mapM [Monad m] (f : α m β) (o : Option α) : m (Option β) := do
if let some a := o then
return some ( f a)

View File

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
-/
prelude
import Init.System.IO
import Init.Data.Int
universe u
/-!

View File

@@ -9,6 +9,7 @@ prelude
import Init.Meta
import Init.Data.Array.Subarray
import Init.Data.ToString
import Init.Conv
namespace Lean
macro "Macro.trace[" id:ident "]" s:interpolatedStr(term) : term =>
@@ -123,7 +124,7 @@ calc abc
_ = xyz := pwxyz
```
`calc` has term mode and tactic mode variants. This is the term mode variant.
`calc` works as a term, as a tactic or as a `conv` tactic.
See [Theorem Proving in Lean 4][tpil4] for more information.
@@ -131,45 +132,13 @@ See [Theorem Proving in Lean 4][tpil4] for more information.
-/
syntax (name := calc) "calc" calcSteps : term
/-- Step-wise reasoning over transitive relations.
```
calc
a = b := pab
b = c := pbc
...
y = z := pyz
```
proves `a = z` from the given step-wise proofs. `=` can be replaced with any
relation implementing the typeclass `Trans`. Instead of repeating the right-
hand sides, subsequent left-hand sides can be replaced with `_`.
```
calc
a = b := pab
_ = c := pbc
...
_ = z := pyz
```
It is also possible to write the *first* relation as `<lhs>\n _ = <rhs> :=
<proof>`. This is useful for aligning relation symbols:
```
calc abc
_ = bce := pabce
_ = cef := pbcef
...
_ = xyz := pwxyz
```
`calc` has term mode and tactic mode variants. This is the tactic mode variant,
which supports an additional feature: it works even if the goal is `a = z'`
for some other `z'`; in this case it will not close the goal but will instead
leave a subgoal proving `z = z'`.
See [Theorem Proving in Lean 4][tpil4] for more information.
[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#calculational-proofs
-/
@[inherit_doc «calc»]
syntax (name := calcTactic) "calc" calcSteps : tactic
@[inherit_doc «calc»]
macro tk:"calc" steps:calcSteps : conv =>
`(conv| tactic => calc%$tk $steps)
@[app_unexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
| `($(_)) => `(())

View File

@@ -6,7 +6,6 @@ Authors: Scott Morrison
prelude
import Init.Data.Int.DivMod
import Init.Data.Int.Order
import Init.Data.Nat.Basic
/-!
# Lemmas about `Nat`, `Int`, and `Fin` needed internally by `omega`.

View File

@@ -6,7 +6,7 @@ Authors: Scott Morrison
prelude
import Init.Data.List.Lemmas
import Init.Data.Int.DivModLemmas
import Init.Data.Int.Gcd
import Init.Data.Nat.Gcd
namespace Lean.Omega

View File

@@ -1485,6 +1485,7 @@ instance [ShiftRight α] : HShiftRight α α α where
hShiftRight a b := ShiftRight.shiftRight a b
open HAdd (hAdd)
open HSub (hSub)
open HMul (hMul)
open HPow (hPow)
open HAppend (hAppend)
@@ -2035,7 +2036,7 @@ instance : Inhabited UInt64 where
default := UInt64.ofNatCore 0 (by decide)
/--
The size of type `UInt16`, that is, `2^System.Platform.numBits`, which may
The size of type `USize`, that is, `2^System.Platform.numBits`, which may
be either `2^32` or `2^64` depending on the platform's architecture.
Remark: we define `USize.size` using `(2^numBits - 1) + 1` to ensure the
@@ -2053,7 +2054,7 @@ instance : OfNat (Fin (n+1)) i where
ofNat := Fin.ofNat i
```
-/
abbrev USize.size : Nat := Nat.succ (Nat.sub (hPow 2 System.Platform.numBits) 1)
abbrev USize.size : Nat := hAdd (hSub (hPow 2 System.Platform.numBits) 1) 1
theorem usize_size_eq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) :=
show Or (Eq (Nat.succ (Nat.sub (hPow 2 System.Platform.numBits) 1)) 4294967296) (Eq (Nat.succ (Nat.sub (hPow 2 System.Platform.numBits) 1)) 18446744073709551616) from
@@ -4580,6 +4581,12 @@ def resolveNamespace (n : Name) : MacroM (List Name) := do
Resolves the given name to an overload list of global definitions.
The `List String` in each alternative is the deduced list of projections
(which are ambiguous with name components).
Remark: it will not trigger actions associated with reserved names. Recall that Lean
has reserved names. For example, a definition `foo` has a reserved name `foo.def` for theorem
containing stating that `foo` is equal to its definition. The action associated with `foo.def`
automatically proves the theorem. At the macro level, the name is resolved, but the action is not
executed. The actions are executed by the elaborator when converting `Syntax` into `Expr`.
-/
def resolveGlobalName (n : Name) : MacroM (List (Prod Name (List String))) := do
( getMethods).resolveGlobalName n

View File

@@ -21,7 +21,10 @@ set_option linter.missingDocs true -- keep it documented
| rfl, rfl, _ => rfl
@[simp] theorem eq_true_eq_id : Eq True = id := by
funext _; simp only [true_iff, id.def, eq_iff_iff]
funext _; simp only [true_iff, id_def, eq_iff_iff]
theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : HEq hp hq := by
cases propext (iff_of_true hp hq); rfl
/-! ## not -/

View File

@@ -45,7 +45,7 @@ def apply {α : Sort u} {r : αα → Prop} (wf : WellFounded r) (a : α) :
section
variable {α : Sort u} {r : α α Prop} (hwf : WellFounded r)
theorem recursion {C : α Sort v} (a : α) (h : x, ( y, r y x C y) C x) : C a := by
noncomputable def recursion {C : α Sort v} (a : α) (h : x, ( y, r y x C y) C x) : C a := by
induction (apply hwf a) with
| intro x₁ _ ih => exact h x₁ ih
@@ -166,13 +166,13 @@ def lt_wfRel : WellFoundedRelation Nat where
| Or.inl e => subst e; assumption
| Or.inr e => exact Acc.inv ih e
protected theorem strongInductionOn
protected noncomputable def strongInductionOn
{motive : Nat Sort u}
(n : Nat)
(ind : n, ( m, m < n motive m) motive n) : motive n :=
Nat.lt_wfRel.wf.fix ind n
protected theorem caseStrongInductionOn
protected noncomputable def caseStrongInductionOn
{motive : Nat Sort u}
(a : Nat)
(zero : motive 0)

View File

@@ -24,6 +24,7 @@ import Lean.Eval
import Lean.Structure
import Lean.PrettyPrinter
import Lean.CoreM
import Lean.ReservedNameAction
import Lean.InternalExceptionId
import Lean.Server
import Lean.ScopedEnvExtension

View File

@@ -17,7 +17,7 @@ builtin_initialize implementedByAttr : ParametricAttribute Name ← registerPara
getParam := fun declName stx => do
let decl getConstInfo declName
let fnNameStx Attribute.Builtin.getIdent stx
let fnName Elab.resolveGlobalConstNoOverloadWithInfo fnNameStx
let fnName Elab.realizeGlobalConstNoOverloadWithInfo fnNameStx
let fnDecl getConstInfo fnName
unless decl.levelParams.length == fnDecl.levelParams.length do
throwError "invalid 'implemented_by' argument '{fnName}', '{fnName}' has {fnDecl.levelParams.length} universe level parameter(s), but '{declName}' has {decl.levelParams.length}"

View File

@@ -44,7 +44,7 @@ unsafe def registerInitAttrUnsafe (attrName : Name) (runAfterImport : Bool) (ref
let decl getConstInfo declName
match ( Attribute.Builtin.getIdent? stx) with
| some initFnName =>
let initFnName Elab.resolveGlobalConstNoOverloadWithInfo initFnName
let initFnName Elab.realizeGlobalConstNoOverloadWithInfo initFnName
let initDecl getConstInfo initFnName
match getIOTypeArg initDecl.type with
| none => throwError "initialization function '{initFnName}' must have type of the form `IO <type>`"

View File

@@ -116,6 +116,22 @@ def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapI
else
(expand size' buckets', false)
@[inline] def insertIfNew [beq : BEq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β × Option β :=
match m with
| size, buckets =>
let i, h := mkIdx (hash a) buckets.property
let bkt := buckets.val[i]
if let some b := bkt.find? a then
(m, some b)
else
let size' := size + 1
let buckets' := buckets.update i (AssocList.cons a b bkt) h
if numBucketsForCapacity size' buckets.val.size then
({ size := size', buckets := buckets' }, none)
else
(expand size' buckets', none)
def erase [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : HashMapImp α β :=
match m with
| size, buckets =>
@@ -125,9 +141,10 @@ def erase [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : HashMapImp α
else m
inductive WellFormed [BEq α] [Hashable α] : HashMapImp α β Prop where
| mkWff : n, WellFormed (mkHashMapImp n)
| insertWff : m a b, WellFormed m WellFormed (insert m a b |>.1)
| eraseWff : m a, WellFormed m WellFormed (erase m a)
| mkWff : n, WellFormed (mkHashMapImp n)
| insertWff : m a b, WellFormed m WellFormed (insert m a b |>.1)
| insertIfNewWff : m a b, WellFormed m WellFormed (insertIfNew m a b |>.1)
| eraseWff : m a, WellFormed m WellFormed (erase m a)
end HashMapImp
@@ -156,13 +173,22 @@ def insert (m : HashMap α β) (a : α) (b : β) : HashMap α β :=
match h:m.insert a b with
| (m', _) => m', by have aux := WellFormed.insertWff m a b hw; rw [h] at aux; assumption
/-- Similar to `insert`, but also returns a Boolean flad indicating whether an existing entry has been replaced with `a -> b`. -/
/-- Similar to `insert`, but also returns a Boolean flag indicating whether an existing entry has been replaced with `a -> b`. -/
def insert' (m : HashMap α β) (a : α) (b : β) : HashMap α β × Bool :=
match m with
| m, hw =>
match h:m.insert a b with
| (m', replaced) => ( m', by have aux := WellFormed.insertWff m a b hw; rw [h] at aux; assumption , replaced)
/--
Similar to `insert`, but returns `some old` if the map already had an entry `α → old`.
If the result is `some old`, the the resulting map is equal to `m`. -/
def insertIfNew (m : HashMap α β) (a : α) (b : β) : HashMap α β × Option β :=
match m with
| m, hw =>
match h:m.insertIfNew a b with
| (m', old) => ( m', by have aux := WellFormed.insertIfNewWff m a b hw; rw [h] at aux; assumption , old)
@[inline] def erase (m : HashMap α β) (a : α) : HashMap α β :=
match m with
| m, hw => m.erase a, WellFormed.eraseWff m a hw

View File

@@ -183,6 +183,9 @@ structure ResponseError (α : Type u) where
instance [ToJson α] : CoeOut (ResponseError α) Message :=
fun r => Message.responseError r.id r.code r.message (r.data?.map toJson)
instance : CoeOut (ResponseError Unit) Message :=
fun r => Message.responseError r.id r.code r.message none
instance : Coe String RequestID := RequestID.str
instance : Coe JsonNumber RequestID := RequestID.num

View File

@@ -24,44 +24,50 @@ Identifier of a reference.
-/
inductive RefIdent where
/-- Named identifier. These are used in all references that are globally available. -/
| const : Name RefIdent
| const (moduleName : Name) (identName : Name) : RefIdent
/-- Unnamed identifier. These are used for all local references. -/
| fvar : FVarId RefIdent
| fvar (moduleName : Name) (id : FVarId) : RefIdent
deriving BEq, Hashable, Inhabited
namespace RefIdent
/-- Converts the reference identifier to a string by prefixing it with a symbol. -/
def toString : RefIdent String
| RefIdent.const n => s!"c:{n}"
| RefIdent.fvar id => s!"f:{id.name}"
instance : ToJson FVarId where
toJson id := toJson id.name
/--
Converts the string representation of a reference identifier back to a reference identifier.
The string representation must have been created by `RefIdent.toString`.
-/
def fromString (s : String) : Except String RefIdent := do
let sPrefix := s.take 2
let sName := s.drop 2
-- See `FromJson Name`
let name match sName with
| "[anonymous]" => pure Name.anonymous
| _ =>
let n := sName.toName
if n.isAnonymous then throw s!"expected a Name, got {sName}"
else pure n
match sPrefix with
| "c:" => return RefIdent.const name
| "f:" => return RefIdent.fvar <| FVarId.mk name
| _ => throw "string must start with 'c:' or 'f:'"
instance : FromJson FVarId where
fromJson? s := return fromJson? s
/-- Shortened representation of `RefIdent` for more compact serialization. -/
inductive RefIdentJsonRepr
/-- Shortened representation of `RefIdent.const` for more compact serialization. -/
| c (m n : Name)
/-- Shortened representation of `RefIdent.fvar` for more compact serialization. -/
| f (m : Name) (i : FVarId)
deriving FromJson, ToJson
/-- Converts `id` to its compact serialization representation. -/
def toJsonRepr : (id : RefIdent) RefIdentJsonRepr
| const moduleName identName => .c moduleName identName
| fvar moduleName id => .f moduleName id
/-- Converts `repr` to `RefIdent`. -/
def fromJsonRepr : (repr : RefIdentJsonRepr) RefIdent
| .c m n => const m n
| .f m i => fvar m i
/-- Converts `RefIdent` from a JSON for `RefIdentJsonRepr`. -/
def fromJson? (s : Json) : Except String RefIdent :=
return fromJsonRepr ( Lean.FromJson.fromJson? s)
/-- Converts `RefIdent` to a JSON for `RefIdentJsonRepr`. -/
def toJson (id : RefIdent) : Json :=
Lean.ToJson.toJson <| toJsonRepr id
instance : FromJson RefIdent where
fromJson?
| (s : String) => fromString s
| j => Except.error s!"expected a String, got {j}"
fromJson? := fromJson?
instance : ToJson RefIdent where
toJson ident := toString ident
toJson := toJson
end RefIdent
@@ -84,6 +90,7 @@ structure RefInfo.Location where
range : Lsp.Range
/-- Parent declaration of the reference. `none` if the reference is itself a declaration. -/
parentDecl? : Option RefInfo.ParentDecl
deriving Inhabited
/-- Definition site and usage sites of a reference. Obtained from `Lean.Server.RefInfo`. -/
structure RefInfo where
@@ -146,13 +153,13 @@ instance : FromJson RefInfo where
def ModuleRefs := HashMap RefIdent RefInfo
instance : ToJson ModuleRefs where
toJson m := Json.mkObj <| m.toList.map fun (ident, info) => (ident.toString, toJson info)
toJson m := Json.mkObj <| m.toList.map fun (ident, info) => (ident.toJson.compress, toJson info)
instance : FromJson ModuleRefs where
fromJson? j := do
let node j.getObj?
node.foldM (init := HashMap.empty) fun m k v =>
return m.insert ( RefIdent.fromString k) ( fromJson? v)
return m.insert ( RefIdent.fromJson? ( Json.parse k)) ( fromJson? v)
/-- `$/lean/ileanInfoUpdate` and `$/lean/ileanInfoFinal` watchdog<-worker notifications.

View File

@@ -64,9 +64,10 @@ def readRequestAs (expectedMethod : String) (α) [FromJson α] : IpcM (Request
(stdout).readLspRequestAs expectedMethod α
/--
Reads response, discarding notifications in between. This function is meant
purely for testing where we use `collectDiagnostics` explicitly if we do care
about such notifications. -/
Reads response, discarding notifications and server-to-client requests in between.
This function is meant purely for testing where we use `collectDiagnostics` explicitly
if we do care about such notifications.
-/
partial def readResponseAs (expectedID : RequestID) (α) [FromJson α] :
IpcM (Response α) := do
let m (stdout).readLspMessage
@@ -79,20 +80,28 @@ partial def readResponseAs (expectedID : RequestID) (α) [FromJson α] :
else
throw $ userError s!"Expected id {expectedID}, got id {id}"
| .notification .. => readResponseAs expectedID α
| _ => throw $ userError s!"Expected JSON-RPC response, got: '{(toJson m).compress}'"
| .request .. => readResponseAs expectedID α
| .responseError .. => throw $ userError s!"Expected JSON-RPC response, got: '{(toJson m).compress}'"
def waitForExit : IpcM UInt32 := do
(read).wait
/-- Waits for the worker to emit all diagnostics for the current document version
and returns them as a list. -/
/--
Waits for the worker to emit all diagnostic notifications for the current document version and
returns the last notification, if any.
We used to return all notifications but with debouncing in the server, this would not be
deterministic anymore as what messages are dropped depends on wall-clock timing.
-/
partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target : DocumentUri) (version : Nat)
: IpcM (List (Notification PublishDiagnosticsParams)) := do
: IpcM (Option (Notification PublishDiagnosticsParams)) := do
writeRequest waitForDiagnosticsId, "textDocument/waitForDiagnostics", WaitForDiagnosticsParams.mk target version
let rec loop : IpcM (List (Notification PublishDiagnosticsParams)) := do
loop
where
loop := do
match (readMessage) with
| Message.response id _ =>
if id == waitForDiagnosticsId then return []
if id == waitForDiagnosticsId then return none
else loop
| Message.responseError id _ msg _ =>
if id == waitForDiagnosticsId then
@@ -100,10 +109,9 @@ partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target :
else loop
| Message.notification "textDocument/publishDiagnostics" (some param) =>
match fromJson? (toJson param) with
| Except.ok diagnosticParam => return "textDocument/publishDiagnostics", diagnosticParam :: (loop)
| Except.ok diagnosticParam => return ( loop).getD "textDocument/publishDiagnostics", diagnosticParam
| Except.error inner => throw $ userError s!"Cannot decode publishDiagnostics parameters\n{inner}"
| _ => loop
loop
def runWith (lean : System.FilePath) (args : Array String := #[]) (test : IpcM α) : IO α := do
let proc Process.spawn {

View File

@@ -0,0 +1,48 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Marc Huisinga
-/
prelude
import Lean.Data.Json
open Lean
inductive MessageType where
| error
| warning
| info
| log
instance : FromJson MessageType where
fromJson?
| (1 : Nat) => .ok .error
| (2 : Nat) => .ok .warning
| (3 : Nat) => .ok .info
| (4 : Nat) => .ok .log
| _ => .error "Unknown MessageType ID"
instance : ToJson MessageType where
toJson
| .error => 1
| .warning => 2
| .info => 3
| .log => 4
structure ShowMessageParams where
type : MessageType
message : String
deriving FromJson, ToJson
structure MessageActionItem where
title : String
deriving FromJson, ToJson
structure ShowMessageRequestParams where
type : MessageType
message : String
actions? : Option (Array MessageActionItem)
deriving FromJson, ToJson
def ShowMessageResponse := Option MessageActionItem
deriving FromJson, ToJson

View File

@@ -226,8 +226,10 @@ partial def eraseAux [BEq α] : Node α β → USize → α → Node α β × Bo
| n@(Node.collision keys vals heq), _, k =>
match keys.indexOf? k with
| some idx =>
let keys', keq := keys.eraseIdx' idx
let vals', veq := vals.eraseIdx' (Eq.ndrec idx heq)
let keys' := keys.feraseIdx idx
have keq := keys.size_feraseIdx idx
let vals' := vals.feraseIdx (Eq.ndrec idx heq)
have veq := vals.size_feraseIdx (Eq.ndrec idx heq)
have : keys.size - 1 = vals.size - 1 := by rw [heq]
(Node.collision keys' vals' (keq.trans (this.trans veq.symm)), true)
| none => (n, false)

View File

@@ -48,14 +48,14 @@ def addDeclarationRanges [MonadEnv m] (declName : Name) (declRanges : Declaratio
def findDeclarationRangesCore? [Monad m] [MonadEnv m] (declName : Name) : m (Option DeclarationRanges) :=
return declRangeExt.find? ( getEnv) declName
def findDeclarationRanges? [Monad m] [MonadEnv m] [MonadLiftT IO m] (declName : Name) : m (Option DeclarationRanges) := do
def findDeclarationRanges? [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] (declName : Name) : m (Option DeclarationRanges) := do
let env getEnv
let ranges if isAuxRecursor env declName || isNoConfusion env declName || ( isRec declName) then
findDeclarationRangesCore? declName.getPrefix
else
findDeclarationRangesCore? declName
match ranges with
| none => return ( builtinDeclRanges.get (m := IO)).find? declName
| none => return ( builtinDeclRanges.get (m := BaseIO)).find? declName
| some _ => return ranges
end Lean

View File

@@ -536,7 +536,7 @@ def elabCheckCore (ignoreStuckTC : Bool) : CommandElab
-- show signature for `#check id`/`#check @id`
if let `($id:ident) := term then
try
for c in ( resolveGlobalConstWithInfos term) do
for c in ( realizeGlobalConstWithInfos term) do
addCompletionInfo <| .id term id.getId (danglingDot := false) {} none
logInfoAt tk <| .ofPPFormat { pp := fun
| some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature c
@@ -760,7 +760,7 @@ def elabRunMeta : CommandElab := fun stx =>
@[builtin_command_elab Parser.Command.addDocString] def elabAddDeclDoc : CommandElab := fun stx => do
match stx with
| `($doc:docComment add_decl_doc $id) =>
let declName resolveGlobalConstNoOverloadWithInfo id
let declName liftCoreM <| realizeGlobalConstNoOverloadWithInfo id
unless (( getEnv).getModuleIdxFor? declName).isNone do
throwError "invalid 'add_decl_doc', declaration is in an imported module"
if let .none findDeclarationRangesCore? declName then

View File

@@ -223,7 +223,7 @@ def elabScientificLit : TermElab := fun stx expectedType? => do
| none => throwIllFormedSyntax
@[builtin_term_elab doubleQuotedName] def elabDoubleQuotedName : TermElab := fun stx _ =>
return toExpr ( resolveGlobalConstNoOverloadWithInfo stx[2])
return toExpr ( realizeGlobalConstNoOverloadWithInfo stx[2])
@[builtin_term_elab declName] def elabDeclName : TermElab := adaptExpander fun _ => do
let some declName getDeclName?

View File

@@ -141,7 +141,8 @@ private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceStat
let mut log := log
let traces' := traces.toArray.qsort fun ((a, _), _) ((b, _), _) => a < b
for ((pos, endPos), traceMsg) in traces' do
log := log.add <| mkMessageCore ctx.fileName ctx.fileMap (.joinSep traceMsg.toList "\n") .information pos endPos
let data := .tagged `_traceMsg <| .joinSep traceMsg.toList "\n"
log := log.add <| mkMessageCore ctx.fileName ctx.fileMap data .information pos endPos
return log
private def addTraceAsMessages : CommandElabM Unit := do
@@ -268,11 +269,6 @@ instance : MonadRecDepth CommandElabM where
getRecDepth := return ( read).currRecDepth
getMaxRecDepth := return ( get).maxRecDepth
register_builtin_option showPartialSyntaxErrors : Bool := {
defValue := false
descr := "show elaboration errors from partial syntax trees (i.e. after parser recovery)"
}
builtin_initialize registerTraceClass `Elab.command
partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
@@ -321,11 +317,6 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
-- note the order: first process current messages & info trees, then add back old messages & trees,
-- then convert new traces to messages
let mut msgs := ( get).messages
-- `stx.hasMissing` should imply `initMsgs.hasErrors`, but the latter should be cheaper to check in general
if !showPartialSyntaxErrors.get ( getOptions) && initMsgs.hasErrors && stx.hasMissing then
-- discard elaboration errors, except for a few important and unlikely misleading ones, on parse error
msgs := msgs.msgs.filter fun msg =>
msg.data.hasTag (fun tag => tag == `Elab.synthPlaceholder || tag == `Tactic.unsolvedGoals || (`_traceMsg).isSuffixOf tag)
for tree in ( getInfoTrees) do
trace[Elab.info] ( tree.format)
modify fun st => { st with

View File

@@ -27,6 +27,8 @@ def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadError m] [MonadInfo
match privateToUserName? declName with
| none => throwError "'{declName}' has already been declared"
| some declName => throwError "private declaration '{declName}' has already been declared"
if isReservedName env declName then
throwError "'{declName}' is a reserved name"
if env.contains (mkPrivateName env declName) then
addInfo (mkPrivateName env declName)
throwError "a private declaration '{declName}' has already been declared"

View File

@@ -42,7 +42,7 @@ private def isNamedDef (stx : Syntax) : Bool :=
let decl := stx[1]
let k := decl.getKind
k == ``Lean.Parser.Command.abbrev ||
k == ``Lean.Parser.Command.def ||
k == ``Lean.Parser.Command.definition ||
k == ``Lean.Parser.Command.theorem ||
k == ``Lean.Parser.Command.opaque ||
k == ``Lean.Parser.Command.axiom ||
@@ -166,7 +166,7 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Comm
return { ref := ctor, modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
let computedFields (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := cf[3], matchAlts := cf[4] }
let classes getOptDerivingClasses decl[6]
let classes liftCoreM <| getOptDerivingClasses decl[6]
return {
ref := decl
shortDeclName := name
@@ -354,7 +354,7 @@ def elabMutual : CommandElab := fun stx => do
-/
let declNames
try
resolveGlobalConst ident
realizeGlobalConst ident
catch _ =>
let name := ident.getId.eraseMacroScopes
if ( Simp.isBuiltinSimproc name) then

View File

@@ -142,7 +142,7 @@ def mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView :=
def isDefLike (stx : Syntax) : Bool :=
let declKind := stx.getKind
declKind == ``Parser.Command.abbrev ||
declKind == ``Parser.Command.def ||
declKind == ``Parser.Command.definition ||
declKind == ``Parser.Command.theorem ||
declKind == ``Parser.Command.opaque ||
declKind == ``Parser.Command.instance ||
@@ -152,7 +152,7 @@ def mkDefView (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView :=
let declKind := stx.getKind
if declKind == ``Parser.Command.«abbrev» then
return mkDefViewOfAbbrev modifiers stx
else if declKind == ``Parser.Command.def then
else if declKind == ``Parser.Command.definition then
return mkDefViewOfDef modifiers stx
else if declKind == ``Parser.Command.theorem then
return mkDefViewOfTheorem modifiers stx

View File

@@ -100,10 +100,10 @@ private def tryApplyDefHandler (className : Name) (declName : Name) : CommandEla
@[builtin_command_elab «deriving»] def elabDeriving : CommandElab
| `(deriving instance $[$classes $[with $argss?]?],* for $[$declNames],*) => do
let declNames declNames.mapM resolveGlobalConstNoOverloadWithInfo
let declNames liftCoreM <| declNames.mapM realizeGlobalConstNoOverloadWithInfo
for cls in classes, args? in argss? do
try
let className resolveGlobalConstNoOverloadWithInfo cls
let className liftCoreM <| realizeGlobalConstNoOverloadWithInfo cls
withRef cls do
if declNames.size == 1 && args?.isNone then
if ( tryApplyDefHandler className declNames[0]!) then
@@ -118,12 +118,12 @@ structure DerivingClassView where
className : Name
args? : Option (TSyntax ``Parser.Term.structInst)
def getOptDerivingClasses [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadInfoTree m] (optDeriving : Syntax) : m (Array DerivingClassView) := do
def getOptDerivingClasses (optDeriving : Syntax) : CoreM (Array DerivingClassView) := do
match optDeriving with
| `(Parser.Command.optDeriving| deriving $[$classes $[with $argss?]?],*) =>
let mut ret := #[]
for cls in classes, args? in argss? do
let className resolveGlobalConstNoOverloadWithInfo cls
let className realizeGlobalConstNoOverloadWithInfo cls
ret := ret.push { ref := cls, className := className, args? }
return ret
| _ => return #[]

View File

@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
prelude
import Lean.Elab.Import
import Lean.Elab.Command
import Lean.Language.Lean
import Lean.Util.Profile
import Lean.Server.References
@@ -40,7 +39,19 @@ def setCommandState (commandState : Command.State) : FrontendM Unit :=
def elabCommandAtFrontend (stx : Syntax) : FrontendM Unit := do
runCommandElabM do
let initMsgs modifyGet fun st => (st.messages, { st with messages := {} })
Command.elabCommandTopLevel stx
let mut msgs := ( get).messages
-- `stx.hasMissing` should imply `initMsgs.hasErrors`, but the latter should be cheaper to check
-- in general
if !Language.Lean.showPartialSyntaxErrors.get ( getOptions) && initMsgs.hasErrors &&
stx.hasMissing then
-- discard elaboration errors, except for a few important and unlikely misleading ones, on
-- parse error
msgs := msgs.msgs.filter fun msg =>
msg.data.hasTag (fun tag => tag == `Elab.synthPlaceholder ||
tag == `Tactic.unsolvedGoals || (`_traceMsg).isSuffixOf tag)
modify ({ · with messages := initMsgs ++ msgs })
def updateCmdPos : FrontendM Unit := do
modify fun s => { s with cmdPos := s.parserState.pos }
@@ -86,12 +97,8 @@ def process (input : String) (env : Environment) (opts : Options) (fileName : Op
pure (s.commandState.env, s.commandState.messages)
builtin_initialize
registerOption `printMessageEndPos { defValue := false, descr := "print end position of each message in addition to start position" }
registerTraceClass `Elab.info
def getPrintMessageEndPos (opts : Options) : Bool :=
opts.getBool `printMessageEndPos false
@[export lean_run_frontend]
def runFrontend
(input : String)
@@ -102,26 +109,50 @@ def runFrontend
(ileanFileName? : Option String := none)
: IO (Environment × Bool) := do
let inputCtx := Parser.mkInputContext input fileName
let (header, parserState, messages) Parser.parseHeader inputCtx
-- allow `env` to be leaked, which would live until the end of the process anyway
let (env, messages) processHeader (leakEnv := true) header opts messages inputCtx trustLevel
let env := env.setMainModule mainModuleName
let mut commandState := Command.mkState env messages opts
-- TODO: replace with `#lang` processing
if /- Lean #lang? -/ true then
-- Temporarily keep alive old cmdline driver for the Lean language so that we don't pay the
-- overhead of passing the environment between snapshots until we actually make good use of it
-- outside the server
let (header, parserState, messages) Parser.parseHeader inputCtx
-- allow `env` to be leaked, which would live until the end of the process anyway
let (env, messages) processHeader (leakEnv := true) header opts messages inputCtx trustLevel
let env := env.setMainModule mainModuleName
let mut commandState := Command.mkState env messages opts
if ileanFileName?.isSome then
-- Collect InfoTrees so we can later extract and export their info to the ilean file
commandState := { commandState with infoState.enabled := true }
if ileanFileName?.isSome then
-- Collect InfoTrees so we can later extract and export their info to the ilean file
commandState := { commandState with infoState.enabled := true }
let s IO.processCommands inputCtx parserState commandState
for msg in s.commandState.messages.toList do
IO.print ( msg.toString (includeEndPos := getPrintMessageEndPos opts))
let s IO.processCommands inputCtx parserState commandState
for msg in s.commandState.messages.toList do
IO.print ( msg.toString (includeEndPos := Language.printMessageEndPos.get opts))
if let some ileanFileName := ileanFileName? then
let trees := s.commandState.infoState.trees.toArray
let references
Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false) |>.toLspModuleRefs
let ilean := { module := mainModuleName, references : Lean.Server.Ilean }
IO.FS.writeFile ileanFileName $ Json.compress $ toJson ilean
return (s.commandState.env, !s.commandState.messages.hasErrors)
let ctx := { inputCtx with mainModuleName, opts, trustLevel }
let processor := Language.Lean.process
let snap processor none ctx
let snaps := Language.toSnapshotTree snap
snaps.runAndReport opts
if let some ileanFileName := ileanFileName? then
let trees := s.commandState.infoState.trees.toArray
let trees := snaps.getAll.concatMap (match ·.infoTree? with | some t => #[t] | _ => #[])
let references := Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false)
let ilean := { module := mainModuleName, references := references.toLspModuleRefs : Lean.Server.Ilean }
IO.FS.writeFile ileanFileName $ Json.compress $ toJson ilean
pure (s.commandState.env, !s.commandState.messages.hasErrors)
let hasErrors := snaps.getAll.any (·.diagnostics.msgLog.hasErrors)
-- TODO: remove default when reworking cmdline interface in Lean; currently the only case
-- where we use the environment despite errors in the file is `--stats`
let env := Language.Lean.waitForFinalEnv? snap |>.getD ( mkEmptyEnvironment)
pure (env, !hasErrors)
end Lean.Elab

View File

@@ -10,8 +10,8 @@ import Lean.Meta.Injective
namespace Lean.Elab.Command
@[builtin_command_elab genInjectiveTheorems] def elabGenInjectiveTheorems : CommandElab := fun stx => do
let declName resolveGlobalConstNoOverloadWithInfo stx[1]
liftTermElabM do
let declName realizeGlobalConstNoOverloadWithInfo stx[1]
Meta.mkInjectiveTheorems declName
end Lean.Elab.Command

View File

@@ -73,9 +73,28 @@ structure GuardMsgFailure where
res : String
deriving TypeName
/--
Makes trailing whitespace visible and protectes them against trimming by the editor, by appending
the symbol ⏎ to such a line (and also to any line that ends with such a symbol, to avoid
ambiguities in the case the message already had that symbol).
-/
def revealTrailingWhitespace (s : String) : String :=
s.replace "\n" "⏎⏎\n" |>.replace "\t\n" "\t⏎\n" |>.replace " \n" "\n"
/- The inverse of `revealTrailingWhitespace` -/
def removeTrailingWhitespaceMarker (s : String) : String :=
s.replace "\n" "\n"
/--
Strings are compared up to newlines, to allow users to break long lines.
-/
def equalUpToNewlines (exp res : String) : Bool :=
exp.replace "\n" " " == res.replace "\n" " "
@[builtin_command_elab Lean.guardMsgsCmd] def elabGuardMsgs : CommandElab
| `(command| $[$dc?:docComment]? #guard_msgs%$tk $(spec?)? in $cmd) => do
let expected : String := ( dc?.mapM (getDocStringText ·)).getD "" |>.trim
let expected : String := ( dc?.mapM (getDocStringText ·)).getD ""
|>.trim |> removeTrailingWhitespaceMarker
let specFn parseGuardMsgsSpec spec?
let initMsgs modifyGet fun st => (st.messages, { st with messages := {} })
elabCommandTopLevel cmd
@@ -88,8 +107,7 @@ deriving TypeName
| .drop => pure ()
| .passthrough => toPassthrough := toPassthrough.add msg
let res := "---\n".intercalate ( toCheck.toList.mapM (messageToStringWithoutPos ·)) |>.trim
-- We do some whitespace normalization here to allow users to break long lines.
if expected.replace "\n" " " == res.replace "\n" " " then
if equalUpToNewlines expected res then
-- Passed. Only put toPassthrough messages back on the message log
modify fun st => { st with messages := initMsgs ++ toPassthrough }
else
@@ -119,6 +137,7 @@ def guardMsgsCodeAction : CommandCodeAction := fun _ _ _ node => do
lazy? := some do
let some start := stx.getPos? true | return eager
let some tail := stx.setArg 0 mkNullNode |>.getPos? true | return eager
let res := revealTrailingWhitespace res
let newText := if res.isEmpty then
""
else if res.length 100-7 && !res.contains '\n' then -- TODO: configurable line length?

View File

@@ -6,6 +6,7 @@ Authors: Wojciech Nawrocki, Leonardo de Moura, Sebastian Ullrich
-/
prelude
import Lean.Meta.PPGoal
import Lean.ReservedNameAction
namespace Lean.Elab.CommandContextInfo
@@ -94,16 +95,18 @@ partial def InfoTree.substitute (tree : InfoTree) (assignment : PersistentHashMa
| none => hole id
| some tree => substitute tree assignment
def ContextInfo.runMetaM (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) : IO α := do
let x := x.run { lctx := lctx } { mctx := info.mctx }
/-- Embeds a `CoreM` action in `IO` by supplying the information stored in `info`. -/
def ContextInfo.runCoreM (info : ContextInfo) (x : CoreM α) : IO α := do
/-
We must execute `x` using the `ngen` stored in `info`. Otherwise, we may create `MVarId`s and `FVarId`s that
have been used in `lctx` and `info.mctx`.
-/
let ((a, _), _)
(·.1) <$>
x.toIO { options := info.options, currNamespace := info.currNamespace, openDecls := info.openDecls, fileName := "<InfoTree>", fileMap := default }
{ env := info.env, ngen := info.ngen }
return a
def ContextInfo.runMetaM (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) : IO α := do
(·.1) <$> info.runCoreM (x.run { lctx := lctx } { mctx := info.mctx })
def ContextInfo.toPPContext (info : ContextInfo) (lctx : LocalContext) : PPContext :=
{ env := info.env, mctx := info.mctx, lctx := lctx,
@@ -279,31 +282,28 @@ def addConstInfo [MonadEnv m] [MonadError m]
expectedType?
}
/-- This does the same job as `resolveGlobalConstNoOverload`; resolving an identifier
/-- This does the same job as `realizeGlobalConstNoOverload`; resolving an identifier
syntax to a unique fully resolved name or throwing if there are ambiguities.
But also adds this resolved name to the infotree. This means that when you hover
over a name in the sourcefile you will see the fully resolved name in the hover info.-/
def resolveGlobalConstNoOverloadWithInfo [MonadResolveName m] [MonadEnv m] [MonadError m]
(id : Syntax) (expectedType? : Option Expr := none) : m Name := do
let n resolveGlobalConstNoOverload id
def realizeGlobalConstNoOverloadWithInfo (id : Syntax) (expectedType? : Option Expr := none) : CoreM Name := do
let n realizeGlobalConstNoOverload id
if ( getInfoState).enabled then
-- we do not store a specific elaborator since identifiers are special-cased by the server anyway
addConstInfo id n expectedType?
return n
/-- Similar to `resolveGlobalConstNoOverloadWithInfo`, except if there are multiple name resolutions then it returns them as a list. -/
def resolveGlobalConstWithInfos [MonadResolveName m] [MonadEnv m] [MonadError m]
(id : Syntax) (expectedType? : Option Expr := none) : m (List Name) := do
let ns resolveGlobalConst id
/-- Similar to `realizeGlobalConstNoOverloadWithInfo`, except if there are multiple name resolutions then it returns them as a list. -/
def realizeGlobalConstWithInfos (id : Syntax) (expectedType? : Option Expr := none) : CoreM (List Name) := do
let ns realizeGlobalConst id
if ( getInfoState).enabled then
for n in ns do
addConstInfo id n expectedType?
return ns
/-- Similar to `resolveGlobalName`, but it also adds the resolved name to the info tree. -/
def resolveGlobalNameWithInfos [MonadResolveName m] [MonadEnv m] [MonadError m]
(ref : Syntax) (id : Name) : m (List (Name × List String)) := do
let ns resolveGlobalName id
/-- Similar to `realizeGlobalName`, but it also adds the resolved name to the info tree. -/
def realizeGlobalNameWithInfos (ref : Syntax) (id : Name) : CoreM (List (Name × List String)) := do
let ns realizeGlobalName id
if ( getInfoState).enabled then
for (n, _) in ns do
addConstInfo ref n

View File

@@ -20,7 +20,7 @@ builtin_initialize
| `(attr| inherit_doc $[$id?:ident]?) => withRef stx[0] do
let some id := id?
| throwError "invalid `[inherit_doc]` attribute, could not infer doc source"
let declName Elab.resolveGlobalConstNoOverloadWithInfo id
let declName Elab.realizeGlobalConstNoOverloadWithInfo id
if ( findDocString? ( getEnv) decl).isSome then
logWarning m!"{← mkConstWithLevelParams decl} already has a doc string"
let some doc findDocString? ( getEnv) declName

View File

@@ -68,8 +68,6 @@ private def check (prevHeaders : Array DefViewElabHeader) (newHeader : DefViewEl
throwError "'partial' theorems are not allowed, 'partial' is a code generation directive"
if newHeader.kind.isTheorem && newHeader.modifiers.isNoncomputable then
throwError "'theorem' subsumes 'noncomputable', code is not generated for theorems"
if newHeader.modifiers.isNoncomputable && newHeader.modifiers.isUnsafe then
throwError "'noncomputable unsafe' is not allowed"
if newHeader.modifiers.isNoncomputable && newHeader.modifiers.isPartial then
throwError "'noncomputable partial' is not allowed"
if newHeader.modifiers.isPartial && newHeader.modifiers.isUnsafe then
@@ -646,6 +644,9 @@ def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr) (mainHea
let termination := termination.rememberExtraParams header.numParams mainVals[i]!
let value mkLambdaFVars sectionVars mainVals[i]!
let type mkForallFVars sectionVars header.type
if header.kind.isTheorem then
unless ( isProp type) do
throwErrorAt header.ref "type of theorem '{header.declName}' is not a proposition{indentExpr type}"
return preDefs.push {
ref := getDeclarationSelectionRef header.ref
kind := header.kind
@@ -659,10 +660,14 @@ def pushLetRecs (preDefs : Array PreDefinition) (letRecClosures : List LetRecClo
letRecClosures.foldlM (init := preDefs) fun preDefs c => do
let type := Closure.mkForall c.localDecls c.toLift.type
let value := Closure.mkLambda c.localDecls c.toLift.val
-- Convert any proof let recs inside a `def` to `theorem` kind
let kind if kind.isDefOrAbbrevOrOpaque then
-- Convert any proof let recs inside a `def` to `theorem` kind
withLCtx c.toLift.lctx c.toLift.localInstances do
return if ( inferType c.toLift.type).isProp then .theorem else kind
else if kind.isTheorem then
-- Convert any non-proof let recs inside a `theorem` to `def` kind
withLCtx c.toLift.lctx c.toLift.localInstances do
return if ( inferType c.toLift.type).isProp then .theorem else .def
else
pure kind
return preDefs.push {
@@ -828,7 +833,7 @@ where
for header in headers, view in views do
if let some classNamesStx := view.deriving? then
for classNameStx in classNamesStx do
let className resolveGlobalConstNoOverload classNameStx
let className realizeGlobalConstNoOverload classNameStx
withRef classNameStx do
unless ( processDefDeriving className header.declName) do
throwError "failed to synthesize instance '{className}' for '{header.declName}'"

View File

@@ -317,14 +317,6 @@ def whnfReducibleLHS? (mvarId : MVarId) : MetaM (Option MVarId) := mvarId.withCo
def tryContradiction (mvarId : MVarId) : MetaM Bool := do
mvarId.contradictionCore { genDiseq := true }
structure UnfoldEqnExtState where
map : PHashMap Name Name := {}
deriving Inhabited
/- We generate the unfold equation on demand, and do not save them on .olean files. -/
builtin_initialize unfoldEqnExt : EnvExtension UnfoldEqnExtState
registerEnvExtension (pure {})
/--
Auxiliary method for `mkUnfoldEq`. The structure is based on `mkEqnTypes`.
`mvarId` is the goal to be proved. It is a goal of the form
@@ -370,9 +362,8 @@ partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
/-- Generate the "unfold" lemma for `declName`. -/
def mkUnfoldEq (declName : Name) (info : EqnInfoCore) : MetaM Name := withLCtx {} {} do
let env getEnv
withOptions (tactic.hygienic.set · false) do
let baseName := mkPrivateName env declName
let baseName := declName
lambdaTelescope info.value fun xs body => do
let us := info.levelParams.map mkLevelParam
let type mkEq (mkAppN (Lean.mkConst declName us) xs) body
@@ -380,7 +371,7 @@ def mkUnfoldEq (declName : Name) (info : EqnInfoCore) : MetaM Name := withLCtx {
mkUnfoldProof declName goal.mvarId!
let type mkForallFVars xs type
let value mkLambdaFVars xs ( instantiateMVars goal)
let name := baseName ++ `_unfold
let name := baseName ++ `def
addDecl <| Declaration.thmDecl {
name, type, value
levelParams := info.levelParams
@@ -388,13 +379,8 @@ def mkUnfoldEq (declName : Name) (info : EqnInfoCore) : MetaM Name := withLCtx {
return name
def getUnfoldFor? (declName : Name) (getInfo? : Unit Option EqnInfoCore) : MetaM (Option Name) := do
let env getEnv
if let some eq := unfoldEqnExt.getState env |>.map.find? declName then
return some eq
else if let some info := getInfo? () then
let eq mkUnfoldEq declName info
modifyEnv fun env => unfoldEqnExt.modifyState env fun s => { s with map := s.map.insert declName eq }
return some eq
if let some info := getInfo? () then
return some ( mkUnfoldEq declName info)
else
return none

View File

@@ -105,6 +105,7 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
See issue #2321
-/
let preDef eraseRecAppSyntax preDefs[0]!
ensureEqnReservedNamesAvailable preDef.declName
if preDef.modifiers.isNoncomputable then
addNonRec preDef
else

View File

@@ -63,12 +63,12 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
let target mkEq (mkAppN (Lean.mkConst info.declName us) xs) body
let goal mkFreshExprSyntheticOpaqueMVar target
mkEqnTypes #[info.declName] goal.mvarId!
let baseName := mkPrivateName ( getEnv) info.declName
let baseName := info.declName
let mut thmNames := #[]
for i in [: eqnTypes.size] do
let type := eqnTypes[i]!
trace[Elab.definition.structural.eqns] "{eqnTypes[i]!}"
let name := baseName ++ (`_eq).appendIndexAfter (i+1)
let name := baseName ++ (`eq).appendIndexAfter (i+1)
thmNames := thmNames.push name
let value mkProof info.declName type
let (type, value) removeUnusedEqnHypotheses type value
@@ -81,6 +81,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo mkMapDeclarationExtension
def registerEqnsInfo (preDef : PreDefinition) (recArgPos : Nat) : CoreM Unit := do
ensureEqnReservedNamesAvailable preDef.declName
modifyEnv fun env => eqnInfoExt.insert env preDef.declName { preDef with recArgPos }
def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do

View File

@@ -8,6 +8,7 @@ import Lean.Meta.Tactic.Rewrite
import Lean.Meta.Tactic.Split
import Lean.Elab.PreDefinition.Basic
import Lean.Elab.PreDefinition.Eqns
import Lean.Meta.ArgsPacker.Basic
namespace Lean.Elab.WF
open Meta
@@ -17,6 +18,7 @@ structure EqnInfo extends EqnInfoCore where
declNames : Array Name
declNameNonRec : Name
fixedPrefixSize : Nat
argsPacker : ArgsPacker
deriving Inhabited
private partial def deltaLHSUntilFix (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
@@ -107,7 +109,7 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
withOptions (tactic.hygienic.set · false) do
let baseName := mkPrivateName ( getEnv) declName
let baseName := declName
let eqnTypes withNewMCtxDepth <| lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
let us := info.levelParams.map mkLevelParam
let target mkEq (mkAppN (Lean.mkConst declName us) xs) body
@@ -117,7 +119,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
for i in [: eqnTypes.size] do
let type := eqnTypes[i]!
trace[Elab.definition.wf.eqns] "{eqnTypes[i]!}"
let name := baseName ++ (`_eq).appendIndexAfter (i+1)
let name := baseName ++ (`eq).appendIndexAfter (i+1)
thmNames := thmNames.push name
let value mkProof declName type
let (type, value) removeUnusedEqnHypotheses type value
@@ -129,7 +131,9 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo mkMapDeclarationExtension
def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat) : MetaM Unit := do
def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat)
(argsPacker : ArgsPacker) : MetaM Unit := do
preDefs.forM fun preDef => ensureEqnReservedNamesAvailable preDef.declName
/-
See issue #2327.
Remark: we could do better for mutual declarations that mix theorems and definitions. However, this is a rare
@@ -140,7 +144,8 @@ def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fi
let declNames := preDefs.map (·.declName)
modifyEnv fun env =>
preDefs.foldl (init := env) fun env preDef =>
eqnInfoExt.insert env preDef.declName { preDef with declNames, declNameNonRec, fixedPrefixSize }
eqnInfoExt.insert env preDef.declName { preDef with
declNames, declNameNonRec, fixedPrefixSize, argsPacker }
def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
if let some info := eqnInfoExt.find? ( getEnv) declName then

View File

@@ -8,12 +8,12 @@ import Lean.Util.HasConstCache
import Lean.Meta.Match.Match
import Lean.Meta.Tactic.Simp.Main
import Lean.Meta.Tactic.Cleanup
import Lean.Meta.ArgsPacker
import Lean.Elab.Tactic.Basic
import Lean.Elab.RecAppSyntax
import Lean.Elab.PreDefinition.Basic
import Lean.Elab.PreDefinition.Structural.Basic
import Lean.Elab.PreDefinition.Structural.BRecOn
import Lean.Elab.PreDefinition.WF.PackMutual
import Lean.Data.Array
namespace Lean.Elab.WF
@@ -172,26 +172,28 @@ know which function is making the call.
The close coupling with how arguments are packed and termination goals look like is not great,
but it works for now.
-/
def groupGoalsByFunction (numFuncs : Nat) (goals : Array MVarId) : MetaM (Array (Array MVarId)) := do
def groupGoalsByFunction (argsPacker : ArgsPacker) (numFuncs : Nat) (goals : Array MVarId) : MetaM (Array (Array MVarId)) := do
let mut r := mkArray numFuncs #[]
for goal in goals do
let (.mdata _ (.app _ param)) goal.getType
| throwError "MVar does not look like like a recursive call"
let (funidx, _) unpackMutualArg numFuncs param
let type goal.getType
let (.mdata _ (.app _ param)) := type
| throwError "MVar does not look like a recursive call:{indentExpr type}"
let (funidx, _) argsPacker.unpack param
r := r.modify funidx (·.push goal)
return r
def solveDecreasingGoals (decrTactics : Array (Option DecreasingBy)) (value : Expr) : MetaM Expr := do
def solveDecreasingGoals (argsPacker : ArgsPacker) (decrTactics : Array (Option DecreasingBy)) (value : Expr) : MetaM Expr := do
let goals getMVarsNoDelayed value
let goals assignSubsumed goals
let goalss groupGoalsByFunction decrTactics.size goals
let goalss groupGoalsByFunction argsPacker decrTactics.size goals
for goals in goalss, decrTactic? in decrTactics do
Lean.Elab.Term.TermElabM.run' do
match decrTactic? with
| none => do
for goal in goals do
let type goal.getType
let some ref := getRecAppSyntax? ( goal.getType)
| throwError "MVar does not look like like a recursive call"
| throwError "MVar not annotated as a recursive call:{indentExpr type}"
withRef ref <| applyDefaultDecrTactic goal
| some decrTactic => withRef decrTactic.ref do
unless goals.isEmpty do -- unlikely to be empty
@@ -205,8 +207,8 @@ def solveDecreasingGoals (decrTactics : Array (Option DecreasingBy)) (value : Ex
Term.reportUnsolvedGoals remainingGoals
instantiateMVars value
def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (wfRel : Expr)
(decrTactics : Array (Option DecreasingBy)) : TermElabM Expr := do
def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (argsPacker : ArgsPacker)
(wfRel : Expr) (decrTactics : Array (Option DecreasingBy)) : TermElabM Expr := do
let type instantiateForall preDef.type prefixArgs
let (wfFix, varName) forallBoundedTelescope type (some 1) fun x type => do
let x := x[0]!
@@ -229,7 +231,7 @@ def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (wfRel : Expr)
let val := preDef.value.beta (prefixArgs.push x)
let val processSumCasesOn x F val fun x F val => do
processPSigmaCasesOn x F val (replaceRecApps preDef.declName prefixArgs.size)
let val solveDecreasingGoals decrTactics val
let val solveDecreasingGoals argsPacker decrTactics val
mkLambdaFVars prefixArgs (mkApp wfFix ( mkLambdaFVars #[x, F] val))
end Lean.Elab.WF

View File

@@ -9,19 +9,20 @@ import Lean.Meta.Match.MatcherApp.Transform
import Lean.Meta.Tactic.Cleanup
import Lean.Meta.Tactic.Refl
import Lean.Meta.Tactic.TryThis
import Lean.Meta.ArgsPacker
import Lean.Elab.Quotation
import Lean.Elab.RecAppSyntax
import Lean.Elab.PreDefinition.Basic
import Lean.Elab.PreDefinition.Structural.Basic
import Lean.Elab.PreDefinition.WF.TerminationHint
import Lean.Elab.PreDefinition.WF.PackMutual
import Lean.Elab.PreDefinition.WF.TerminationArgument
import Lean.Data.Array
/-!
This module finds lexicographic termination arguments for well-founded recursion.
Starting with basic measures (`sizeOf xᵢ` for all parameters `xᵢ`), it tries all combinations
Starting with basic measures (`sizeOf xᵢ` for all parameters `xᵢ`), and complex measures
(e.g. `e₂ - e₁` if `e₁ < e₂` is found in the context of a recursive call) it tries all combinations
until it finds one where all proof obligations go through with the given tactic (`decerasing_by`),
if given, or the default `decreasing_tactic`.
@@ -59,6 +60,10 @@ The following optimizations are applied to make this feasible:
The logic here is based on “Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL”
by Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow, 10.1007/978-3-540-74591-4_5
<https://www21.in.tum.de/~nipkow/pubs/tphols07.pdf>.
We got the idea of considering the measure `e₂ - e₁` if we see `e₁ < e₂` from
“Termination Analysis with Calling Context Graphs” by Panagiotis Manolios &
Daron Vroon, https://doi.org/10.1007/11817963_36.
-/
set_option autoImplicit false
@@ -84,11 +89,11 @@ def originalVarNames (preDef : PreDefinition) : MetaM (Array Name) := do
lambdaTelescope preDef.value fun xs _ => xs.mapM (·.fvarId!.getUserName)
/--
Given the original paramter names from `originalVarNames`, remove the fixed prefix and find
Given the original parameter names from `originalVarNames`, find
good variable names to be used when talking about termination arguments:
Use user-given parameter names if present; use x1...xn otherwise.
The names ought to accessible (no macro scopes) and new names fresh wrt to the current environment,
The names ought to accessible (no macro scopes) and fresh wrt to the current environment,
so that with `showInferredTerminationBy` we can print them to the user reliably.
We do that by appending `'` as needed.
@@ -97,8 +102,7 @@ shadow each other, and the guessed relation refers to the wrong one. In that
case, the user gets to keep both pieces (and may have to rename variables).
-/
partial
def naryVarNames (fixedPrefixSize : Nat) (xs : Array Name) : MetaM (Array Name) := do
let xs := xs.extract fixedPrefixSize xs.size
def naryVarNames (xs : Array Name) : MetaM (Array Name) := do
let mut ns : Array Name := #[]
for h : i in [:xs.size] do
let n := xs[i]
@@ -115,6 +119,77 @@ def naryVarNames (fixedPrefixSize : Nat) (xs : Array Name) : MetaM (Array Name)
else
freshen ns (n.appendAfter "'")
/-- A termination measure with extra fields for use within GuessLex -/
structure Measure extends TerminationArgument where
/--
Like `.fn`, but unconditionally with `sizeOf` at the right type.
We use this one when in `evalRecCall`
-/
natFn : Expr
deriving Inhabited
/-- String desription of this measure -/
def Measure.toString (measure : Measure) : MetaM String := do
lambdaTelescope measure.fn fun xs e => do
let e mkLambdaFVars xs[measure.arity:] e -- undo overshooting
return ( ppExpr e).pretty
/--
Determine if the measure for parameter `x` should be `sizeOf x` or just `x`.
For non-mutual definitions, we omit `sizeOf` when the argument does not depend on
the other varying parameters, and its `WellFoundedRelation` instance goes via `SizeOf`.
For mutual definitions, we omit `sizeOf` only when the argument is (at reducible transparency!) of
type `Nat` (else we'd have to worry about differently-typed measures from different functions to
line up).
-/
def mayOmitSizeOf (is_mutual : Bool) (args : Array Expr) (x : Expr) : MetaM Bool := do
let t inferType x
if is_mutual
then
withReducible (isDefEq t (.const `Nat []))
else
try
if t.hasAnyFVar (fun fvar => args.contains (.fvar fvar)) then
pure false
else
let u getLevel t
let wfi synthInstance (.app (.const ``WellFoundedRelation [u]) t)
let soi synthInstance (.app (.const ``SizeOf [u]) t)
isDefEq wfi (mkApp2 (.const ``sizeOfWFRel [u]) t soi)
catch _ =>
pure false
/-- Sets the user names for the given freevars in `xs`. -/
def withUserNames {α} (xs : Array Expr) (ns : Array Name) (k : MetaM α) : MetaM α := do
let mut lctx getLCtx
for x in xs, n in ns do lctx := lctx.setUserName x.fvarId! n
withTheReader Meta.Context (fun ctx => { ctx with lctx }) k
/-- Create one measure for each (eligible) parameter of the given predefintion. -/
def simpleMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
(userVarNamess : Array (Array Name)) : MetaM (Array (Array Measure)) := do
let is_mutual : Bool := preDefs.size > 1
preDefs.mapIdxM fun funIdx preDef => do
lambdaTelescope preDef.value fun xs _ => do
withUserNames xs[fixedPrefixSize:] userVarNamess[funIdx]! do
let mut ret : Array Measure := #[]
for x in xs[fixedPrefixSize:] do
-- If the `SizeOf` instance produces a constant (e.g. because it's type is a `Prop` or
-- `Type`), then ignore this parameter
let sizeOf whnfD ( mkAppM ``sizeOf #[x])
if sizeOf.isLit then continue
let natFn mkLambdaFVars xs ( mkAppM ``sizeOf #[x])
-- Determine if we need to exclude `sizeOf` in the measure we show/pass on.
let fn
if mayOmitSizeOf is_mutual xs[fixedPrefixSize:] x
then mkLambdaFVars xs x
else pure natFn
let extraParams := preDef.termination.extraParams
ret := ret.push { ref := .missing, fn, natFn, arity := xs.size, extraParams }
return ret
/-- Internal monad used by `withRecApps` -/
abbrev M (recFnName : Name) (α β : Type) : Type :=
@@ -225,11 +300,11 @@ structure RecCallWithContext where
ref : Syntax
/-- Function index of caller -/
caller : Nat
/-- Parameters of caller -/
/-- Parameters of caller (including fixed prefix) -/
params : Array Expr
/-- Function index of callee -/
callee : Nat
/-- Arguments to callee -/
/-- Arguments to callee (including fixed prefix) -/
args : Array Expr
ctxt : SavedLocalContext
@@ -261,25 +336,72 @@ def filterSubsumed (rcs : Array RecCallWithContext ) : Array RecCallWithContext
return (false, true)
return (true, true)
/-- Traverse a unary PreDefinition, and returns a `WithRecCall` closure for each recursive
/--
Traverse a unary `PreDefinition`, and returns a `WithRecCall` closure for each recursive
call site.
-/
def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) (arities : Array Nat)
: MetaM (Array RecCallWithContext) := withoutModifyingState do
def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat)
(argsPacker : ArgsPacker) : MetaM (Array RecCallWithContext) := withoutModifyingState do
addAsAxiom unaryPreDef
lambdaTelescope unaryPreDef.value fun xs body => do
unless xs.size == fixedPrefixSize + 1 do
-- Maybe cleaner to have lambdaBoundedTelescope?
throwError "Unexpected number of lambdas in unary pre-definition"
let ys := xs[:fixedPrefixSize]
let param := xs[fixedPrefixSize]!
withRecApps unaryPreDef.declName fixedPrefixSize param body fun param args => do
unless args.size fixedPrefixSize + 1 do
throwError "Insufficient arguments in recursive call"
let arg := args[fixedPrefixSize]!
trace[Elab.definition.wf] "collectRecCalls: {unaryPreDef.declName} ({param}) → {unaryPreDef.declName} ({arg})"
let (caller, params) unpackArg arities param
let (callee, args) unpackArg arities arg
RecCallWithContext.create ( getRef) caller params callee args
let (caller, params) argsPacker.unpack param
let (callee, args) argsPacker.unpack arg
RecCallWithContext.create ( getRef) caller (ys ++ params) callee (ys ++ args)
/-- Is the expression a `<`-like comparison of `Nat` expressions -/
def isNatCmp (e : Expr) : Option (Expr × Expr) :=
match_expr e with
| LT.lt α _ e₁ e₂ => if α.isConstOf ``Nat then some (e₁, e₂) else none
| LE.le α _ e₁ e₂ => if α.isConstOf ``Nat then some (e₁, e₂) else none
| GT.gt α _ e₁ e₂ => if α.isConstOf ``Nat then some (e₂, e₁) else none
| GE.ge α _ e₁ e₂ => if α.isConstOf ``Nat then some (e₂, e₁) else none
| _ => none
def complexMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
(userVarNamess : Array (Array Name)) (recCalls : Array RecCallWithContext) :
MetaM (Array (Array Measure)) := do
preDefs.mapIdxM fun funIdx preDef => do
let arity lambdaTelescope preDef.value fun xs _ => pure xs.size
let mut measures := #[]
for rc in recCalls do
-- Only look at calls from the current function
unless rc.caller = funIdx do continue
-- Only look at calls where the parameters have not been refined
unless rc.params.all (·.isFVar) do continue
let xs := rc.params.map (·.fvarId!)
let varyingParams : Array FVarId := xs[fixedPrefixSize:]
measures rc.ctxt.run do
withUserNames rc.params[fixedPrefixSize:] userVarNamess[funIdx]! do
trace[Elab.definition.wf] "rc: {rc.caller} ({rc.params}) → {rc.callee} ({rc.args})"
let mut measures := measures
for ldecl in getLCtx do
if let some (e₁, e₂) := isNatCmp ldecl.type then
-- We only want to consider these expressions if they depend only on the function's
-- immediate arguments, so check that
if e₁.hasAnyFVar (! xs.contains ·) then continue
if e₂.hasAnyFVar (! xs.contains ·) then continue
-- If e₁ does not depend on any varying parameters, simply ignore it
let e₁_is_const := ! e₁.hasAnyFVar (varyingParams.contains ·)
let body := if e₁_is_const then e₂ else mkNatSub e₂ e₁
-- Avoid adding simple measures
unless body.isFVar do
let fn mkLambdaFVars rc.params body
-- Avoid duplicates
unless measures.anyM (isDefEq ·.fn fn) do
let extraParams := preDef.termination.extraParams
measures := measures.push { ref := .missing, fn, natFn := fn, arity, extraParams }
return measures
return measures
/-- A `GuessLexRel` described how a recursive call affects a measure; whether it
decreases strictly, non-strictly, is equal, or else. -/
@@ -302,27 +424,18 @@ def GuessLexRel.toNatRel : GuessLexRel → Expr
| le => mkAppN (mkConst ``LE.le [levelZero]) #[mkConst ``Nat, mkConst ``instLENat]
| no_idea => unreachable!
/-- Given an expression `e`, produce `sizeOf e` with a suitable instance. -/
def mkSizeOf (e : Expr) : MetaM Expr := do
let ty inferType e
let lvl getLevel ty
let inst synthInstance (mkAppN (mkConst ``SizeOf [lvl]) #[ty])
let res := mkAppN (mkConst ``sizeOf [lvl]) #[ty, inst, e]
check res
return res
/--
For a given recursive call, and a choice of parameter and argument index,
try to prove equality, < or ≤.
-/
def evalRecCall (decrTactic? : Option DecreasingBy) (rcc : RecCallWithContext) (paramIdx argIdx : Nat) :
MetaM GuessLexRel := do
def evalRecCall (decrTactic? : Option DecreasingBy) (callerMeasures calleeMeasures : Array Measure)
(rcc : RecCallWithContext) (callerMeasureIdx calleeMeasureIdx : Nat) : MetaM GuessLexRel := do
rcc.ctxt.run do
let param := rcc.params[paramIdx]!
let arg := rcc.args[argIdx]!
let callerMeasure := callerMeasures[callerMeasureIdx]!
let calleeMeasure := calleeMeasures[calleeMeasureIdx]!
let param := callerMeasure.natFn.beta rcc.params
let arg := calleeMeasure.natFn.beta rcc.args
trace[Elab.definition.wf] "inspectRecCall: {rcc.caller} ({param}) → {rcc.callee} ({arg})"
let arg mkSizeOf rcc.args[argIdx]!
let param mkSizeOf rcc.params[paramIdx]!
for rel in [GuessLexRel.eq, .lt, .le] do
let goalExpr := mkAppN rel.toNatRel #[arg, param]
trace[Elab.definition.wf] "Goal for {rel}: {goalExpr}"
@@ -355,32 +468,35 @@ def evalRecCall (decrTactic? : Option DecreasingBy) (rcc : RecCallWithContext) (
/- A cache for `evalRecCall` -/
structure RecCallCache where mk'' ::
decrTactic? : Option DecreasingBy
callerMeasures : Array Measure
calleeMeasures : Array Measure
rcc : RecCallWithContext
cache : IO.Ref (Array (Array (Option GuessLexRel)))
/-- Create a cache to memoize calls to `evalRecCall descTactic? rcc` -/
def RecCallCache.mk (decrTactics : Array (Option DecreasingBy))
def RecCallCache.mk (decrTactics : Array (Option DecreasingBy)) (measuress : Array (Array Measure))
(rcc : RecCallWithContext) :
BaseIO RecCallCache := do
let decrTactic? := decrTactics[rcc.caller]!
let cache IO.mkRef <| Array.mkArray rcc.params.size (Array.mkArray rcc.args.size Option.none)
return { decrTactic?, rcc, cache }
let callerMeasures := measuress[rcc.caller]!
let calleeMeasures := measuress[rcc.callee]!
let cache IO.mkRef <| Array.mkArray callerMeasures.size (Array.mkArray calleeMeasures.size Option.none)
return { decrTactic?, callerMeasures, calleeMeasures, rcc, cache }
/-- Run `evalRecCall` and cache there result -/
def RecCallCache.eval (rc: RecCallCache) (paramIdx argIdx : Nat) : MetaM GuessLexRel := do
def RecCallCache.eval (rc: RecCallCache) (callerMeasureIdx calleeMeasureIdx : Nat) : MetaM GuessLexRel := do
-- Check the cache first
if let Option.some res := ( rc.cache.get)[paramIdx]![argIdx]! then
if let Option.some res := ( rc.cache.get)[callerMeasureIdx]![calleeMeasureIdx]! then
return res
else
let res evalRecCall rc.decrTactic? rc.rcc paramIdx argIdx
rc.cache.modify (·.modify paramIdx (·.set! argIdx res))
let res evalRecCall rc.decrTactic? rc.callerMeasures rc.calleeMeasures rc.rcc callerMeasureIdx calleeMeasureIdx
rc.cache.modify (·.modify callerMeasureIdx (·.set! calleeMeasureIdx res))
return res
/-- Print a single cache entry as a string, without forcing it -/
def RecCallCache.prettyEntry (rcc : RecCallCache) (paramIdx argIdx : Nat) : MetaM String := do
def RecCallCache.prettyEntry (rcc : RecCallCache) (callerMeasureIdx calleeMeasureIdx : Nat) : MetaM String := do
let cachedEntries rcc.cache.get
return match cachedEntries[paramIdx]![argIdx]! with
return match cachedEntries[callerMeasureIdx]![calleeMeasureIdx]! with
| .some rel => toString rel
| .none => "_"
@@ -394,10 +510,10 @@ inductive MutualMeasure where
/-- Evaluate a recursive call at a given `MutualMeasure` -/
def inspectCall (rc : RecCallCache) : MutualMeasure MetaM GuessLexRel
| .args argIdxs => do
let paramIdx := argIdxs[rc.rcc.caller]!
let argIdx := argIdxs[rc.rcc.callee]!
rc.eval paramIdx argIdx
| .args taIdxs => do
let callerMeasureIdx := taIdxs[rc.rcc.caller]!
let calleeMeasureIdx := taIdxs[rc.rcc.callee]!
rc.eval callerMeasureIdx calleeMeasureIdx
| .func funIdx => do
if rc.rcc.caller == funIdx && rc.rcc.callee != funIdx then
return .lt
@@ -406,56 +522,29 @@ def inspectCall (rc : RecCallCache) : MutualMeasure → MetaM GuessLexRel
else
return .eq
/--
Given a predefinition with value `fun (x_₁ ... xₙ) (y_₁ : α₁)... (yₘ : αₘ) => ...`,
where `n = fixedPrefixSize`, return an array `A` s.t. `i ∈ A` iff `sizeOf yᵢ` reduces to a literal.
This is the case for types such as `Prop`, `Type u`, etc.
These arguments should not be considered when guessing a well-founded relation.
See `generateCombinations?`
-/
def getForbiddenByTrivialSizeOf (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Nat) :=
lambdaTelescope preDef.value fun xs _ => do
let mut result := #[]
for x in xs[fixedPrefixSize:], i in [:xs.size] do
try
let sizeOf whnfD ( mkAppM ``sizeOf #[x])
if sizeOf.isLit then
result := result.push i
catch _ =>
result := result.push i
return result
/--
Generate all combination of arguments, skipping those that are forbidden.
Generate all combination of measures. Assumes we have numbered the measures of each function,
and their counts is in `numMeasures`.
Sorts the uniform combinations ([0,0,0], [1,1,1]) to the front; they are commonly most useful to
This puts the uniform combinations ([0,0,0], [1,1,1]) to the front; they are commonly most useful to
try first, when the mutually recursive functions have similar argument structures
-/
partial def generateCombinations? (forbiddenArgs : Array (Array Nat)) (numArgs : Array Nat)
(threshold : Nat := 32) : Option (Array (Array Nat)) :=
partial def generateCombinations? (numMeasures : Array Nat) (threshold : Nat := 32) :
Option (Array (Array Nat)) :=
(do goUniform 0; go 0 #[]) |>.run #[] |>.2
where
isForbidden (fidx : Nat) (argIdx : Nat) : Bool :=
if h : fidx < forbiddenArgs.size then
forbiddenArgs[fidx] |>.contains argIdx
else
false
-- Enumerate all permissible uniform combinations
goUniform (argIdx : Nat) : OptionT (StateM (Array (Array Nat))) Unit := do
if numArgs.all (argIdx < ·) then
unless forbiddenArgs.any (·.contains argIdx) do
modify (·.push (Array.mkArray numArgs.size argIdx))
goUniform (argIdx + 1)
goUniform (idx : Nat) : OptionT (StateM (Array (Array Nat))) Unit := do
if numMeasures.all (idx < ·) then
modify (·.push (Array.mkArray numMeasures.size idx))
goUniform (idx + 1)
-- Enumerate all other permissible combinations
go (fidx : Nat) : OptionT (ReaderT (Array Nat) (StateM (Array (Array Nat)))) Unit := do
if h : fidx < numArgs.size then
let n := numArgs[fidx]
for argIdx in [:n] do
unless isForbidden fidx argIdx do
withReader (·.push argIdx) (go (fidx + 1))
if h : fidx < numMeasures.size then
let n := numMeasures[fidx]
for idx in [:n] do withReader (·.push idx) (go (fidx + 1))
else
let comb read
unless comb.all (· == comb[0]!) do
@@ -463,19 +552,19 @@ where
if ( get).size > threshold then
failure
/--
Enumerate all meausures we want to try: All arguments (resp. combinations thereof) and
Enumerate all meausures we want to try.
All arguments (resp. combinations thereof) and
possible orderings of functions (if more than one)
-/
def generateMeasures (forbiddenArgs : Array (Array Nat)) (arities : Array Nat) :
MetaM (Array MutualMeasure) := do
let some arg_measures := generateCombinations? forbiddenArgs arities
def generateMeasures (numTermArgs : Array Nat) : MetaM (Array MutualMeasure) := do
let some arg_measures := generateCombinations? numTermArgs
| throwError "Too many combinations"
let func_measures :=
if arities.size > 1 then
(List.range arities.size).toArray
if numTermArgs.size > 1 then
(List.range numTermArgs.size).toArray
else
#[]
@@ -520,58 +609,6 @@ partial def solve {m} {α} [Monad m] (measures : Array α)
-- None found, we have to give up
return .none
/--
Create Tuple syntax (`()` if the array is empty, and just the value if its a singleton)
-/
def mkTupleSyntax : Array Term MetaM Term
| #[] => `(())
| #[e] => return e
| es => `(($(es[0]!), $(es[1:]),*))
/--
Given an array of `MutualMeasures`, creates a `TerminationWF` that specifies the lexicographic
combination of these measures. The parameters are
* `originalVarNamess`: For each function in the clique, the original parameter names, _including_
the fixed prefix. Used to determine if we need to fully qualify `sizeOf`.
* `varNamess`: For each function in the clique, the parameter names to be used in the
termination relation. Excludes the fixed prefix. Includes names like `x1` for unnamed parameters.
* `measures`: The measures to be used.
-/
def buildTermWF (originalVarNamess : Array (Array Name)) (varNamess : Array (Array Name))
(measures : Array MutualMeasure) : MetaM TerminationWF := do
varNamess.mapIdxM fun funIdx varNames => do
let idents := varNames.map mkIdent
let measureStxs measures.mapM fun
| .args varIdxs => do
let varIdx := varIdxs[funIdx]!
let v := idents[varIdx]!
-- Print `sizeOf` as such, unless it is shadowed.
-- Shadowing by a `def` in the current namespace is handled by `unresolveNameGlobal`.
-- But it could also be shadowed by an earlier parameter (including the fixed prefix),
-- so look for unqualified (single tick) occurrences in `originalVarNames`
let sizeOfIdent :=
if originalVarNamess[funIdx]!.any (· = `sizeOf) then
mkIdent ``sizeOf -- fully qualified
else
mkIdent ( unresolveNameGlobal ``sizeOf)
`($sizeOfIdent $v)
| .func funIdx' => if funIdx' == funIdx then `(1) else `(0)
let body mkTupleSyntax measureStxs
return { ref := .missing, vars := idents, body, synthetic := true }
/--
The TerminationWF produced by GuessLex may mention more variables than allowed in the surface
syntax (in case of unnamed or shadowed parameters). So how to print this to the user? Invalid
syntax with more information, or valid syntax with (possibly) unresolved variable names?
The latter works fine in many cases, and is still useful to the user in the tricky corner cases, so
we do that.
-/
def trimTermWF (extraParams : Array Nat) (elems : TerminationWF) : TerminationWF :=
elems.mapIdx fun funIdx elem => { elem with
vars := elem.vars[elem.vars.size - extraParams[funIdx]! : elem.vars.size]
synthetic := false }
/--
Given a matrix (row-major) of strings, arranges them in tabular form.
First column is left-aligned, others right-aligned.
@@ -616,21 +653,43 @@ def RecCallWithContext.posString (rcc : RecCallWithContext) : MetaM String := do
return s!"{position.line}:{position.column}{endPosStr}"
/-- How to present the measure in the table header, possibly abbreviated. -/
def measureHeader (measure : Measure) : StateT (Nat × String) MetaM String := do
let s measure.toString
if s.length > 5 then
let (i, footer) get
let i := i + 1
let footer := footer ++ s!"#{i}: {s}\n"
set (i, footer)
pure s!"#{i}"
else
pure s
def collectHeaders {α} (a : StateT (Nat × String) MetaM α) : MetaM (α × String) := do
let (x, (_, footer)) a.run (0, "")
pure (x,footer)
/-- Explain what we found out about the recursive calls (non-mutual case) -/
def explainNonMutualFailure (varNames : Array Name) (rcs : Array RecCallCache) : MetaM Format := do
let header := varNames.map (·.eraseMacroScopes.toString)
def explainNonMutualFailure (measures : Array Measure) (rcs : Array RecCallCache) : MetaM Format := do
let (header, footer) collectHeaders (measures.mapM measureHeader)
let mut table : Array (Array String) := #[#[""] ++ header]
for i in [:rcs.size], rc in rcs do
let mut row := #[s!"{i+1}) {← rc.rcc.posString}"]
for argIdx in [:varNames.size] do
for argIdx in [:measures.size] do
row := row.push ( rc.prettyEntry argIdx argIdx)
table := table.push row
return formatTable table
let out := formatTable table
if footer.isEmpty then
return out
else
return out ++ "\n\n" ++ footer
/-- Explain what we found out about the recursive calls (mutual case) -/
def explainMutualFailure (declNames : Array Name) (varNamess : Array (Array Name))
def explainMutualFailure (declNames : Array Name) (measuress : Array (Array Measure))
(rcs : Array RecCallCache) : MetaM Format := do
let (headerss, footer) collectHeaders (measuress.mapM (·.mapM measureHeader))
let mut r := Format.nil
for rc in rcs do
@@ -639,40 +698,74 @@ def explainMutualFailure (declNames : Array Name) (varNamess : Array (Array Name
r := r ++ f!"Call from {declNames[caller]!} to {declNames[callee]!} " ++
f!"at {← rc.rcc.posString}:\n"
let header := varNamess[caller]!.map (·.eraseMacroScopes.toString)
let mut table : Array (Array String) := #[#[""] ++ header]
let mut table : Array (Array String) := #[#[""] ++ headerss[caller]!]
if caller = callee then
-- For self-calls, only the diagonal is interesting, so put it into one row
let mut row := #[""]
for argIdx in [:varNamess[caller]!.size] do
for argIdx in [:measuress[caller]!.size] do
row := row.push ( rc.prettyEntry argIdx argIdx)
table := table.push row
else
for argIdx in [:varNamess[callee]!.size] do
for argIdx in [:measuress[callee]!.size] do
let mut row := #[]
row := row.push varNamess[callee]![argIdx]!.eraseMacroScopes.toString
for paramIdx in [:varNamess[caller]!.size] do
row := row.push headerss[callee]![argIdx]!
for paramIdx in [:measuress[caller]!.size] do
row := row.push ( rc.prettyEntry paramIdx argIdx)
table := table.push row
r := r ++ formatTable table ++ "\n"
unless footer.isEmpty do
r := r ++ "\n\n" ++ footer
return r
def explainFailure (declNames : Array Name) (varNamess : Array (Array Name))
def explainFailure (declNames : Array Name) (measuress : Array (Array Measure))
(rcs : Array RecCallCache) : MetaM Format := do
let mut r : Format := "The arguments relate at each recursive call as follows:\n" ++
"(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)\n"
if declNames.size = 1 then
r := r ++ ( explainNonMutualFailure varNamess[0]! rcs)
r := r ++ ( explainNonMutualFailure measuress[0]! rcs)
else
r := r ++ ( explainMutualFailure declNames varNamess rcs)
r := r ++ ( explainMutualFailure declNames measuress rcs)
return r
end Lean.Elab.WF.GuessLex
/--
For `#[x₁, .., xₙ]` create `(x₁, .., xₙ)`.
-/
def mkProdElem (xs : Array Expr) : MetaM Expr := do
match xs.size with
| 0 => return default
| 1 => return xs[0]!
| _ =>
let n := xs.size
xs[0:n-1].foldrM (init:=xs[n-1]!) fun x p => mkAppM ``Prod.mk #[x,p]
namespace Lean.Elab.WF
def toTerminationArguments (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
(userVarNamess : Array (Array Name)) (measuress : Array (Array Measure))
(solution : Array MutualMeasure) : MetaM TerminationArguments := do
preDefs.mapIdxM fun funIdx preDef => do
let measures := measuress[funIdx]!
lambdaTelescope preDef.value fun xs _ => do
withUserNames xs[fixedPrefixSize:] userVarNamess[funIdx]! do
let args := solution.map fun
| .args taIdxs => measures[taIdxs[funIdx]!]!.fn.beta xs
| .func funIdx' => mkNatLit <| if funIdx' == funIdx then 1 else 0
let fn mkLambdaFVars xs ( mkProdElem args)
let extraParams := preDef.termination.extraParams
return { ref := .missing, arity := xs.size, extraParams, fn}
open Lean.Elab.WF.GuessLex
/--
Shows the inferred termination argument to the user, and implements `termination_by?`
-/
def reportTermArgs (preDefs : Array PreDefinition) (termArgs : TerminationArguments) : MetaM Unit := do
for preDef in preDefs, termArg in termArgs do
if showInferredTerminationBy.get ( getOptions) then
logInfoAt preDef.ref m!"Inferred termination argument:\n{← termArg.delab}"
if let some ref := preDef.termination.terminationBy?? then
Tactic.TryThis.addSuggestion ref ( termArg.delab)
end GuessLex
open GuessLex
/--
Main entry point of this module:
@@ -681,45 +774,41 @@ Try to find a lexicographic ordering of the arguments for which the recursive de
terminates. See the module doc string for a high-level overview.
-/
def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
(fixedPrefixSize : Nat) :
MetaM TerminationWF := do
let extraParamss := preDefs.map (·.termination.extraParams)
let originalVarNamess preDefs.mapM originalVarNames
let varNamess originalVarNamess.mapM (naryVarNames fixedPrefixSize ·)
let arities := varNamess.map (·.size)
trace[Elab.definition.wf] "varNames is: {varNamess}"
(fixedPrefixSize : Nat) (argsPacker : ArgsPacker) :
MetaM TerminationArguments := do
let userVarNamess argsPacker.varNamess.mapM (naryVarNames ·)
trace[Elab.definition.wf] "varNames is: {userVarNamess}"
let forbiddenArgs preDefs.mapM fun preDef =>
getForbiddenByTrivialSizeOf fixedPrefixSize preDef
-- Collect all recursive calls and extract their context
let recCalls collectRecCalls unaryPreDef fixedPrefixSize argsPacker
let recCalls := filterSubsumed recCalls
-- For every function, the measures we want to use
-- (One for each non-forbiddend arg)
let meassures₁ simpleMeasures preDefs fixedPrefixSize userVarNamess
let meassures₂ complexMeasures preDefs fixedPrefixSize userVarNamess recCalls
let measuress := Array.zipWith meassures₁ meassures₂ (· ++ ·)
-- The list of measures, including the measures that order functions.
-- The function ordering measures come last
let measures generateMeasures forbiddenArgs arities
let measures generateMeasures (measuress.map (·.size))
-- If there is only one plausible measure, use that
if let #[solution] := measures then
return buildTermWF originalVarNamess varNamess #[solution]
let termArgs toTerminationArguments preDefs fixedPrefixSize userVarNamess measuress #[solution]
reportTermArgs preDefs termArgs
return termArgs
-- Collect all recursive calls and extract their context
let recCalls collectRecCalls unaryPreDef fixedPrefixSize arities
let recCalls := filterSubsumed recCalls
let rcs recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasingBy?)) ·)
let rcs recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasingBy?)) measuress ·)
let callMatrix := rcs.map (inspectCall ·)
match liftMetaM <| solve measures callMatrix with
| .some solution => do
let wf buildTermWF originalVarNamess varNamess solution
let wf' := trimTermWF extraParamss wf
for preDef in preDefs, term in wf' do
if showInferredTerminationBy.get ( getOptions) then
logInfoAt preDef.ref m!"Inferred termination argument:\n{← term.unexpand}"
if let some ref := preDef.termination.terminationBy?? then
Tactic.TryThis.addSuggestion ref ( term.unexpand)
return wf
let termArgs toTerminationArguments preDefs fixedPrefixSize userVarNamess measuress solution
reportTermArgs preDefs termArgs
return termArgs
| .none =>
let explanation explainFailure (preDefs.map (·.declName)) varNamess rcs
let explanation explainFailure (preDefs.map (·.declName)) measuress rcs
Lean.throwError <| "Could not find a decreasing measure.\n" ++
explanation ++ "\n" ++
"Please use `termination_by` to specify a decreasing measure."

View File

@@ -5,8 +5,7 @@ Authors: Leonardo de Moura
-/
prelude
import Lean.Elab.PreDefinition.Basic
import Lean.Elab.PreDefinition.WF.TerminationHint
import Lean.Elab.PreDefinition.WF.PackDomain
import Lean.Elab.PreDefinition.WF.TerminationArgument
import Lean.Elab.PreDefinition.WF.PackMutual
import Lean.Elab.PreDefinition.WF.Preprocess
import Lean.Elab.PreDefinition.WF.Rel
@@ -19,29 +18,15 @@ namespace Lean.Elab
open WF
open Meta
private partial def addNonRecPreDefs (preDefs : Array PreDefinition) (preDefNonRec : PreDefinition) (fixedPrefixSize : Nat) : TermElabM Unit := do
private partial def addNonRecPreDefs (fixedPrefixSize : Nat) (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) (preDefNonRec : PreDefinition) : TermElabM Unit := do
let us := preDefNonRec.levelParams.map mkLevelParam
let all := preDefs.toList.map (·.declName)
for fidx in [:preDefs.size] do
let preDef := preDefs[fidx]!
let value lambdaTelescope preDef.value fun xs _ => do
let packedArgs : Array Expr := xs[fixedPrefixSize:]
let mkProd (type : Expr) : MetaM Expr := do
mkUnaryArg type packedArgs
let rec mkSum (i : Nat) (type : Expr) : MetaM Expr := do
if i == preDefs.size - 1 then
mkProd type
else
( whnfD type).withApp fun f args => do
assert! args.size == 2
if i == fidx then
return mkApp3 (mkConst ``PSum.inl f.constLevels!) args[0]! args[1]! ( mkProd args[0]!)
else
let r mkSum (i+1) args[1]!
return mkApp3 (mkConst ``PSum.inr f.constLevels!) args[0]! args[1]! r
let Expr.forallE _ domain _ _ := ( instantiateForall preDefNonRec.type xs[:fixedPrefixSize]) | unreachable!
let arg mkSum 0 domain
mkLambdaFVars xs (mkApp (mkAppN (mkConst preDefNonRec.declName us) xs[:fixedPrefixSize]) arg)
let value forallBoundedTelescope preDef.type (some fixedPrefixSize) fun xs _ => do
let value := mkAppN (mkConst preDefNonRec.declName us) xs
let value argsPacker.curryProj value fidx
mkLambdaFVars xs value
trace[Elab.definition.wf] "{preDef.declName} := {value}"
addNonRec { preDef with value } (applyAttrAfterCompilation := false) (all := all)
@@ -81,25 +66,49 @@ private def isOnlyOneUnaryDef (preDefs : Array PreDefinition) (fixedPrefixSize :
else
return false
/--
Collect the names of the varying variables (after the fixed prefix); this also determines the
arity for the well-founded translations, and is turned into an `ArgsPacker`.
We use the term to determine the arity, but take the name from the type, for better names in the
```
fun : (n : Nat) → Nat | 0 => 0 | n+1 => fun n
```
idiom.
-/
def varyingVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Name) := do
-- We take the arity from the term, but the names from the types
let arity lambdaTelescope preDef.value fun xs _ => return xs.size
assert! fixedPrefixSize arity
if arity = fixedPrefixSize then
throwError "well-founded recursion cannot be used, '{preDef.declName}' does not take any (non-fixed) arguments"
forallBoundedTelescope preDef.type arity fun xs _ => do
assert! xs.size = arity
let xs : Array Expr := xs[fixedPrefixSize:]
xs.mapM (·.fvarId!.getUserName)
def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
let preDefs preDefs.mapM fun preDef =>
return { preDef with value := ( preprocess preDef.value) }
let (unaryPreDef, fixedPrefixSize) withoutModifyingEnv do
let (fixedPrefixSize, argsPacker, unaryPreDef) withoutModifyingEnv do
for preDef in preDefs do
addAsAxiom preDef
let fixedPrefixSize getFixedPrefix preDefs
trace[Elab.definition.wf] "fixed prefix: {fixedPrefixSize}"
let varNamess preDefs.mapM (varyingVarNames fixedPrefixSize ·)
let argsPacker := { varNamess }
let preDefsDIte preDefs.mapM fun preDef => return { preDef with value := ( iteToDIte preDef.value) }
let unaryPreDefs packDomain fixedPrefixSize preDefsDIte
return ( packMutual fixedPrefixSize preDefs unaryPreDefs, fixedPrefixSize)
return (fixedPrefixSize, argsPacker, packMutual fixedPrefixSize argsPacker preDefsDIte)
let wf do
let wf : TerminationArguments do
let (preDefsWith, preDefsWithout) := preDefs.partition (·.termination.terminationBy?.isSome)
if preDefsWith.isEmpty then
-- No termination_by anywhere, so guess one
guessLex preDefs unaryPreDef fixedPrefixSize
guessLex preDefs unaryPreDef fixedPrefixSize argsPacker
else if preDefsWithout.isEmpty then
pure <| preDefsWith.map (·.termination.terminationBy?.get!)
preDefsWith.mapIdxM fun funIdx predef => do
let arity := fixedPrefixSize + argsPacker.varNamess[funIdx]!.size
let hints := predef.termination
TerminationArgument.elab predef.declName predef.type arity hints.extraParams hints.terminationBy?.get!
else
-- Some have, some do not, so report errors
preDefsWithout.forM fun preDef => do
@@ -109,12 +118,14 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
let preDefNonRec forallBoundedTelescope unaryPreDef.type fixedPrefixSize fun prefixArgs type => do
let type whnfForall type
unless type.isForall do
throwError "wfRecursion: expected unary function type: {type}"
let packedArgType := type.bindingDomain!
elabWFRel preDefs unaryPreDef.declName fixedPrefixSize packedArgType wf fun wfRel => do
elabWFRel preDefs unaryPreDef.declName prefixArgs argsPacker packedArgType wf fun wfRel => do
trace[Elab.definition.wf] "wfRel: {wfRel}"
let (value, envNew) withoutModifyingEnv' do
addAsAxiom unaryPreDef
let value mkFix unaryPreDef prefixArgs wfRel (preDefs.map (·.termination.decreasingBy?))
let value mkFix unaryPreDef prefixArgs argsPacker wfRel (preDefs.map (·.termination.decreasingBy?))
eraseRecAppSyntaxExpr value
/- `mkFix` invokes `decreasing_tactic` which may add auxiliary theorems to the environment. -/
let value unfoldDeclsFrom envNew value
@@ -126,12 +137,12 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
else
withEnableInfoTree false do
addNonRec preDefNonRec (applyAttrAfterCompilation := false)
addNonRecPreDefs preDefs preDefNonRec fixedPrefixSize
addNonRecPreDefs fixedPrefixSize argsPacker preDefs preDefNonRec
-- We create the `_unsafe_rec` before we abstract nested proofs.
-- Reason: the nested proofs may be referring to the _unsafe_rec.
addAndCompilePartialRec preDefs
let preDefs preDefs.mapM (abstractNestedProofs ·)
registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize
registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker
for preDef in preDefs do
applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation

View File

@@ -1,191 +0,0 @@
/-
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.Tactic.Cases
import Lean.Elab.PreDefinition.Basic
namespace Lean.Elab.WF
open Meta
/--
Given a (dependent) tuple `t` (using `PSigma`) of the given arity.
Return an array containing its "elements".
Example: `mkTupleElems a 4` returns `#[a.1, a.2.1, a.2.2.1, a.2.2.2]`.
-/
private def mkTupleElems (t : Expr) (arity : Nat) : Array Expr := Id.run do
let mut result := #[]
let mut t := t
for _ in [:arity - 1] do
result := result.push (mkProj ``PSigma 0 t)
t := mkProj ``PSigma 1 t
result.push t
/-- Create a unary application by packing the given arguments using `PSigma.mk` -/
partial def mkUnaryArg (type : Expr) (args : Array Expr) : MetaM Expr := do
go 0 type
where
go (i : Nat) (type : Expr) : MetaM Expr := do
if i < args.size - 1 then
let arg := args[i]!
assert! type.isAppOfArity ``PSigma 2
let us := type.getAppFn.constLevels!
let α := type.appFn!.appArg!
let β := type.appArg!
assert! β.isLambda
let type := β.bindingBody!.instantiate1 arg
let rest go (i+1) type
return mkApp4 (mkConst ``PSigma.mk us) α β arg rest
else
return args[i]!
/-- Unpacks a unary packed argument created with `mkUnaryArg`. -/
def unpackUnaryArg {m} [Monad m] [MonadError m] (arity : Nat) (e : Expr) : m (Array Expr) := do
let mut e := e
let mut args := #[]
while args.size + 1 < arity do
if e.isAppOfArity ``PSigma.mk 4 then
args := args.push (e.getArg! 2)
e := e.getArg! 3
else
throwError "Unexpected expression while unpacking n-ary argument"
args := args.push e
return args
private partial def mkPSigmaCasesOn (y : Expr) (codomain : Expr) (xs : Array Expr) (value : Expr) : MetaM Expr := do
let mvar mkFreshExprSyntheticOpaqueMVar codomain
let rec go (mvarId : MVarId) (y : FVarId) (ys : Array Expr) : MetaM Unit := do
if ys.size < xs.size - 1 then
let xDecl xs[ys.size]!.fvarId!.getDecl
let xDecl' xs[ys.size + 1]!.fvarId!.getDecl
let #[s] mvarId.cases y #[{ varNames := [xDecl.userName, xDecl'.userName] }] | unreachable!
go s.mvarId s.fields[1]!.fvarId! (ys.push s.fields[0]!)
else
let ys := ys.push (mkFVar y)
mvarId.assign (value.replaceFVars xs ys)
go mvar.mvarId! y.fvarId! #[]
instantiateMVars mvar
/--
Convert the given pre-definitions into unary functions.
We "pack" the arguments using `PSigma`.
-/
partial def packDomain (fixedPrefix : Nat) (preDefs : Array PreDefinition) : MetaM (Array PreDefinition) := do
let mut preDefsNew := #[]
let mut arities := #[]
let mut modified := false
for preDef in preDefs do
let (preDefNew, arity, modifiedCurr) lambdaTelescope preDef.value fun xs _ => do
if xs.size == fixedPrefix then
throwError "well-founded recursion cannot be used, '{preDef.declName}' does not take any (non-fixed) arguments"
let arity := xs.size
if arity > fixedPrefix + 1 then
let bodyType instantiateForall preDef.type xs
let mut d inferType xs.back
let ys : Array Expr := xs[:fixedPrefix]
let xs : Array Expr := xs[fixedPrefix:]
for x in xs.pop.reverse do
d mkAppOptM ``PSigma #[some ( inferType x), some ( mkLambdaFVars #[x] d)]
withLocalDeclD ( mkFreshUserName `_x) d fun tuple => do
let elems := mkTupleElems tuple xs.size
let codomain := bodyType.replaceFVars xs elems
let preDefNew:= { preDef with
declName := preDef.declName ++ `_unary
type := ( mkForallFVars (ys.push tuple) codomain)
}
addAsAxiom preDefNew
return (preDefNew, arity, true)
else
return (preDef, arity, false)
modified := modified || modifiedCurr
arities := arities.push arity
preDefsNew := preDefsNew.push preDefNew
if !modified then
return preDefs
-- Update values
for i in [:preDefs.size] do
let preDef := preDefs[i]!
let preDefNew := preDefsNew[i]!
let valueNew lambdaTelescope preDef.value fun xs body => do
let ys : Array Expr := xs[:fixedPrefix]
let xs : Array Expr := xs[fixedPrefix:]
let type instantiateForall preDefNew.type ys
forallBoundedTelescope type (some 1) fun z codomain => do
let z := z[0]!
let newBody mkPSigmaCasesOn z codomain xs body
mkLambdaFVars (ys.push z) ( packApplications newBody arities preDefsNew)
let isBad (e : Expr) : Bool :=
match isAppOfPreDef? e with
| none => false
| some i => e.getAppNumArgs > fixedPrefix + 1 || preDefsNew[i]!.declName != preDefs[i]!.declName
if let some bad := valueNew.find? isBad then
if let some i := isAppOfPreDef? bad then
throwErrorAt preDef.ref "well-founded recursion cannot be used, function '{preDef.declName}' contains application of function '{preDefs[i]!.declName}' with #{bad.getAppNumArgs} argument(s), but function has arity {arities[i]!}"
preDefsNew := preDefsNew.set! i { preDefNew with value := valueNew }
return preDefsNew
where
/-- Return `some i` if `e` is a `preDefs[i]` application -/
isAppOfPreDef? (e : Expr) : Option Nat := do
let f := e.getAppFn
guard f.isConst
preDefs.findIdx? (·.declName == f.constName!)
packApplications (e : Expr) (arities : Array Nat) (preDefsNew : Array PreDefinition) : MetaM Expr := do
let pack (e : Expr) (funIdx : Nat) : MetaM Expr := do
let f := e.getAppFn
let args := e.getAppArgs
let fNew := mkConst preDefsNew[funIdx]!.declName f.constLevels!
let fNew := mkAppN fNew args[:fixedPrefix]
let Expr.forallE _ d .. whnf ( inferType fNew) | unreachable!
-- NB: Use whnf in case the type is not a manifest forall, but a definition around it
let argNew mkUnaryArg d args[fixedPrefix:]
return mkApp fNew argNew
let rec
visit (e : Expr) : MonadCacheT ExprStructEq Expr MetaM Expr := do
checkCache { val := e : ExprStructEq } fun _ => Meta.withIncRecDepth do
match e with
| Expr.lam n d b c =>
withLocalDecl n c ( visit d) fun x => do
mkLambdaFVars (usedLetOnly := false) #[x] ( visit (b.instantiate1 x))
| Expr.forallE n d b c =>
withLocalDecl n c ( visit d) fun x => do
mkForallFVars (usedLetOnly := false) #[x] ( visit (b.instantiate1 x))
| Expr.letE n t v b _ =>
withLetDecl n ( visit t) ( visit v) fun x => do
mkLambdaFVars (usedLetOnly := false) #[x] ( visit (b.instantiate1 x))
| Expr.proj n i s .. => return mkProj n i ( visit s)
| Expr.mdata d b => return mkMData d ( visit b)
| Expr.app .. => visitApp e
| Expr.const .. => visitApp e
| e => return e,
visitApp (e : Expr) : MonadCacheT ExprStructEq Expr MetaM Expr := e.withApp fun f args => do
let args args.mapM visit
if let some funIdx := isAppOfPreDef? f then
let numArgs := args.size
let arity := arities[funIdx]!
if numArgs < arity then
-- Partial application
let extra := arity - numArgs
withDefault do forallBoundedTelescope ( inferType e) extra fun xs _ => do
if xs.size != extra then
return (mkAppN f args) -- It will fail later
else
mkLambdaFVars xs ( pack (mkAppN (mkAppN f args) xs) funIdx)
else if numArgs > arity then
-- Over application
let r pack (mkAppN f args[:arity]) funIdx
let rType inferType r
-- Make sure the new auxiliary definition has only one argument.
withLetDecl ( mkFreshUserName `aux) rType r fun aux =>
mkLetFVars #[aux] (mkAppN aux args[arity:])
else
pack (mkAppN f args) funIdx
else if args.isEmpty then
return f
else
return mkAppN ( visit f) args
visit e |>.run
end Lean.Elab.WF

View File

@@ -4,93 +4,28 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Meta.Tactic.Cases
import Lean.Meta.ArgsPacker
import Lean.Elab.PreDefinition.Basic
import Lean.Elab.PreDefinition.WF.PackDomain
namespace Lean.Elab.WF
open Meta
/-- Combine different function domains `ds` using `PSum`s -/
private def mkNewDomain (ds : Array Expr) : MetaM Expr := do
let mut r := ds.back
for d in ds.pop.reverse do
r mkAppM ``PSum #[d, r]
return r
private def getCodomainLevel (preDefType : Expr) : MetaM Level :=
forallBoundedTelescope preDefType (some 1) fun _ body => getLevel body
/--
Return the universe level for the codomain of the given definitions.
This method produces an error if the codomains are in different universe levels.
Checks that all codomians have the same level, throws an error otherwise.
-/
private def getCodomainsLevel (preDefsOriginal : Array PreDefinition) (preDefTypes : Array Expr) : MetaM Level := do
let r getCodomainLevel preDefTypes[0]!
for i in [1:preDefTypes.size] do
let preDef := preDefTypes[i]!
unless ( isLevelDefEq r ( getCodomainLevel preDef)) do
let arity₀ lambdaTelescope preDefsOriginal[0]!.value fun xs _ => return xs.size
let arityᵢ lambdaTelescope preDefsOriginal[i]!.value fun xs _ => return xs.size
forallBoundedTelescope preDefsOriginal[0]!.type arity₀ fun _ type₀ =>
forallBoundedTelescope preDefsOriginal[i]!.type arityᵢ fun _ typeᵢ =>
private def checkCodomainsLevel (fixedPrefixSize : Nat) (arities : Array Nat)
(preDefs : Array PreDefinition) : MetaM Unit := do
forallBoundedTelescope preDefs[0]!.type (fixedPrefixSize + arities[0]!) fun _ type₀ => do
let u₀ getLevel type₀
for i in [1:preDefs.size] do
forallBoundedTelescope preDefs[i]!.type (fixedPrefixSize + arities[i]!) fun _ typeᵢ =>
unless isLevelDefEq u₀ ( getLevel typeᵢ) do
withOptions (fun o => pp.sanitizeNames.set o false) do
throwError "invalid mutual definition, result types must be in the same universe level, resulting type for `{preDefsOriginal[0]!.declName}` is{indentExpr type₀} : {← inferType type₀}\nand for `{preDefsOriginal[i]!.declName}` is{indentExpr typeᵢ} : {← inferType typeᵢ}"
return r
/--
Create the codomain for the new function that "combines" different `preDef` types
See: `packMutual`
-/
private partial def mkNewCoDomain (preDefsOriginal : Array PreDefinition) (preDefTypes : Array Expr) (x : Expr) : MetaM Expr := do
let u getCodomainsLevel preDefsOriginal preDefTypes
let rec go (x : Expr) (i : Nat) : MetaM Expr := do
if i < preDefTypes.size - 1 then
let xType whnfD ( inferType x)
assert! xType.isAppOfArity ``PSum 2
let xTypeArgs := xType.getAppArgs
let casesOn := mkConst (mkCasesOnName ``PSum) (mkLevelSucc u :: xType.getAppFn.constLevels!)
let casesOn := mkAppN casesOn xTypeArgs -- parameters
let casesOn := mkApp casesOn ( mkLambdaFVars #[x] (mkSort u)) -- motive
let casesOn := mkApp casesOn x -- major
let minor1 withLocalDeclD ( mkFreshUserName `_x) xTypeArgs[0]! fun x => do
mkLambdaFVars #[x] (( whnf preDefTypes[i]!).bindingBody!.instantiate1 x)
let minor2 withLocalDeclD ( mkFreshUserName `_x) xTypeArgs[1]! fun x => do
mkLambdaFVars #[x] ( go x (i+1))
return mkApp2 casesOn minor1 minor2
else
return ( whnf preDefTypes[i]!).bindingBody!.instantiate1 x
go x 0
/--
Combine/pack the values of the different definitions in a single value
`x` is `PSum`, and we use `PSum.casesOn` to select the appropriate `preDefs.value`.
See: `packMutual`.
Remark: this method does not replace the nested recursive `preDefValues` applications.
This step is performed by `transform` with the following `post` method.
-/
private partial def packValues (x : Expr) (codomain : Expr) (preDefValues : Array Expr) : MetaM Expr := do
let varNames := preDefValues.map fun val =>
assert! val.isLambda
val.bindingName!
let mvar mkFreshExprSyntheticOpaqueMVar codomain
let rec go (mvarId : MVarId) (x : FVarId) (i : Nat) : MetaM Unit := do
if i < preDefValues.size - 1 then
/-
Names for the `cases` tactics. The names are important to preserve the user provided names (unary functions).
-/
let givenNames : Array AltVarNames :=
if i == preDefValues.size - 2 then
#[{ varNames := [varNames[i]!] }, { varNames := [varNames[i+1]!] }]
else
#[{ varNames := [varNames[i]!] }]
let #[s₁, s₂] mvarId.cases x (givenNames := givenNames) | unreachable!
s₁.mvarId.assign (mkApp preDefValues[i]! s₁.fields[0]!).headBeta
go s₂.mvarId s₂.fields[0]!.fvarId! (i+1)
else
mvarId.assign (mkApp preDefValues[i]! (mkFVar x)).headBeta
go mvar.mvarId! x.fvarId! 0
instantiateMVars mvar
throwError m!"invalid mutual definition, result types must be in the same universe " ++
m!"level, resulting type " ++
m!"for `{preDefs[0]!.declName}` is{indentExpr type₀} : {← inferType type₀}\n" ++
m!"and for `{preDefs[i]!.declName}` is{indentExpr typeᵢ} : {← inferType typeᵢ}"
/--
Pass the first `n` arguments of `e` to the continuation, and apply the result to the
@@ -112,141 +47,54 @@ def withAppN (n : Nat) (e : Expr) (k : Array Expr → MetaM Expr) : MetaM Expr :
mkLambdaFVars xs e'
/--
If `arg` is the argument to the `fidx`th of the `numFuncs` in the recursive group,
then `mkMutualArg` packs that argument in `PSum.inl` and `PSum.inr` constructors
to create the mutual-packed argument of type `domain`.
A `post` for `Meta.transform` to replace recursive calls to the original `preDefs` with calls
to the new unary function `newfn`.
-/
partial def mkMutualArg (numFuncs : Nat) (domain : Expr) (fidx : Nat) (arg : Expr) : MetaM Expr := do
let rec go (i : Nat) (type : Expr) : MetaM Expr := do
if i == numFuncs - 1 then
return arg
else
( whnfD type).withApp fun f args => do
assert! args.size == 2
if i == fidx then
return mkApp3 (mkConst ``PSum.inl f.constLevels!) args[0]! args[1]! arg
else
let r go (i+1) args[1]!
return mkApp3 (mkConst ``PSum.inr f.constLevels!) args[0]! args[1]! r
go 0 domain
/--
Unpacks a mutually packed argument, returning the argument and function index.
Inverse of `mkMutualArg`. Cf. `unpackUnaryArg` and `unpackArg`, which does both
-/
def unpackMutualArg {m} [Monad m] [MonadError m] (numFuncs : Nat) (e : Expr) : m (Nat × Expr) := do
let mut funidx := 0
let mut e := e
while funidx + 1 < numFuncs do
if e.isAppOfArity ``PSum.inr 3 then
e := e.getArg! 2
funidx := funidx + 1
else if e.isAppOfArity ``PSum.inl 3 then
e := e.getArg! 2
break
else
throwError "Unexpected expression while unpacking mutual argument"
return (funidx, e)
/--
Given the packed argument of a (possibly) mutual and (possibly) nary call,
return the function index that is called and the arguments individually.
We expect precisely the expressions produced by `packMutual`, with manifest
`PSum.inr`, `PSum.inl` and `PSigma.mk` constructors, and thus take them apart
rather than using projectinos.
-/
def unpackArg {m} [Monad m] [MonadError m] (arities : Array Nat) (e : Expr) :
m (Nat × Array Expr) := do
let (funidx, e) unpackMutualArg arities.size e
let args unpackUnaryArg arities[funidx]! e
return (funidx, args)
/--
Auxiliary function for replacing nested `preDefs` recursive calls in `e` with the new function `newFn`.
See: `packMutual`
-/
private partial def post (fixedPrefix : Nat) (preDefs : Array PreDefinition) (domain : Expr) (newFn : Name) (e : Expr) : MetaM TransformStep := do
private partial def post (fixedPrefix : Nat) (argsPacker : ArgsPacker) (funNames : Array Name)
(domain : Expr) (newFn : Name) (e : Expr) : MetaM TransformStep := do
let f := e.getAppFn
if !f.isConst then
return TransformStep.done e
let declName := f.constName!
let us := f.constLevels!
if let some fidx := preDefs.findIdx? (·.declName == declName) then
let e' withAppN (fixedPrefix + 1) e fun args => do
if let some fidx := funNames.getIdx? declName then
let arity := fixedPrefix + argsPacker.varNamess[fidx]!.size
let e' withAppN arity e fun args => do
let fixedArgs := args[:fixedPrefix]
let arg := args[fixedPrefix]!
let packedArg mkMutualArg preDefs.size domain fidx arg
let packedArg argsPacker.pack domain fidx args[fixedPrefix:]
return mkApp (mkAppN (mkConst newFn us) fixedArgs) packedArg
return TransformStep.done e'
return TransformStep.done e
partial def withFixedPrefix (fixedPrefix : Nat) (preDefs : Array PreDefinition) (k : Array Expr Array Expr Array Expr MetaM α) : MetaM α :=
go fixedPrefix #[] (preDefs.map (·.value))
where
go (i : Nat) (fvars : Array Expr) (vals : Array Expr) : MetaM α := do
match i with
| 0 => k fvars ( preDefs.mapM fun preDef => instantiateForall preDef.type fvars) vals
| i+1 =>
withLocalDecl vals[0]!.bindingName! vals[0]!.binderInfo vals[0]!.bindingDomain! fun x =>
go i (fvars.push x) (vals.map fun val => val.bindingBody!.instantiate1 x)
/--
If `preDefs.size > 1`, combine different functions in a single one using `PSum`.
This method assumes all `preDefs` have arity 1, and have already been processed using `packDomain`.
Here is a small example. Suppose the input is
```
f x :=
match x.2.1, x.2.2.1, x.2.2.2 with
| 0, a, b => a
| Nat.succ n, a, b => (g ⟨x.1, n, a, b⟩).fst
g x :=
match x.2.1, x.2.2.1, x.2.2.2 with
| 0, a, b => (a, b)
| Nat.succ n, a, b => (h ⟨x.1, n, a, b⟩, a)
h x =>
match x.2.1, x.2.2.1, x.2.2.2 with
| 0, a, b => b
| Nat.succ n, a, b => f ⟨x.1, n, a, b⟩
```
this method produces the following pre definition
```
f._mutual x :=
PSum.casesOn x
(fun val =>
match val.2.1, val.2.2.1, val.2.2.2 with
| 0, a, b => a
| Nat.succ n, a, b => (f._mutual (PSum.inr (PSum.inl ⟨val.1, n, a, b⟩))).fst
fun val =>
PSum.casesOn val
(fun val =>
match val.2.1, val.2.2.1, val.2.2.2 with
| 0, a, b => (a, b)
| Nat.succ n, a, b => (f._mutual (PSum.inr (PSum.inr ⟨val.1, n, a, b⟩)), a)
fun val =>
match val.2.1, val.2.2.1, val.2.2.2 with
| 0, a, b => b
| Nat.succ n, a, b =>
f._mutual (PSum.inl ⟨val.1, n, a, b⟩)
```
Creates a single unary function from the given `preDefs`, using the machinery in the `ArgPacker`
module.
-/
def packMutual (fixedPrefix : Nat) (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) : MetaM PreDefinition := do
let arities := argsPacker.arities
if let #[1] := arities then return preDefs[0]!
let newFn := if argsPacker.numFuncs > 1 then preDefs[0]!.declName ++ `_mutual
else preDefs[0]!.declName ++ `_unary
Remark: `preDefsOriginal` is used for error reporting, it contains the definitions before applying `packDomain`.
-/
def packMutual (fixedPrefix : Nat) (preDefsOriginal : Array PreDefinition) (preDefs : Array PreDefinition) : MetaM PreDefinition := do
if preDefs.size == 1 then return preDefs[0]!
withFixedPrefix fixedPrefix preDefs fun ys types vals => do
let domains types.mapM fun type => do pure ( whnf type).bindingDomain!
let domain mkNewDomain domains
withLocalDeclD ( mkFreshUserName `_x) domain fun x => do
let codomain mkNewCoDomain preDefsOriginal types x
let type mkForallFVars (ys.push x) codomain
let value packValues x codomain vals
let newFn := preDefs[0]!.declName ++ `_mutual
let preDefNew := { preDefs[0]! with declName := newFn, type, value }
addAsAxiom preDefNew
let value transform value (skipConstInApp := true) (post := post fixedPrefix preDefs domain newFn)
let value mkLambdaFVars (ys.push x) value
return { preDefNew with value }
checkCodomainsLevel fixedPrefix argsPacker.arities preDefs
-- Bring the fixed Prefix into scope
forallBoundedTelescope preDefs[0]!.type (some fixedPrefix) fun ys _ => do
let types preDefs.mapM (instantiateForall ·.type ys)
let vals preDefs.mapM (instantiateLambda ·.value ys)
let type argsPacker.uncurryType types
let packedDomain := type.bindingDomain!
-- Temporarily add the unary function as an axiom, so that all expressions
-- are still type correct
let type mkForallFVars ys type
let preDefNew := { preDefs[0]! with declName := newFn, type }
addAsAxiom preDefNew
let value argsPacker.uncurry vals
let value transform value (skipConstInApp := true)
(post := post fixedPrefix argsPacker (preDefs.map (·.declName)) packedDomain newFn)
let value mkLambdaFVars ys value
return { preDefNew with value }
end Lean.Elab.WF

View File

@@ -9,76 +9,58 @@ import Lean.Meta.Tactic.Cases
import Lean.Meta.Tactic.Rename
import Lean.Elab.SyntheticMVars
import Lean.Elab.PreDefinition.Basic
import Lean.Elab.PreDefinition.WF.TerminationHint
import Lean.Elab.PreDefinition.WF.TerminationArgument
import Lean.Meta.ArgsPacker
namespace Lean.Elab.WF
open Meta
open Term
private partial def unpackMutual (preDefs : Array PreDefinition) (mvarId : MVarId) (fvarId : FVarId) : TermElabM (Array (FVarId × MVarId)) := do
let rec go (i : Nat) (mvarId : MVarId) (fvarId : FVarId) (result : Array (FVarId × MVarId)) : TermElabM (Array (FVarId × MVarId)) := do
if i < preDefs.size - 1 then
let #[s₁, s₂] mvarId.cases fvarId | unreachable!
go (i + 1) s₂.mvarId s₂.fields[0]!.fvarId! (result.push (s₁.fields[0]!.fvarId!, s₁.mvarId))
else
return result.push (fvarId, mvarId)
go 0 mvarId fvarId #[]
/--
The termination arguments must not depend on the varying parameters of the function, and in
a mutual clique, they must be the same for all functions.
private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mvarId : MVarId)
(fvarId : FVarId) (element : TerminationBy) : TermElabM MVarId := do
element.checkVars preDef.declName preDef.termination.extraParams
-- If `synthetic := false`, then this is user-provided, and should be interpreted
-- as left to right. Else it is provided by GuessLex, and may rename non-extra paramters as well.
-- (Not pretty, but it works for now)
let implicit_underscores :=
if element.synthetic then 0 else preDef.termination.extraParams - element.vars.size
let varNames lambdaTelescope preDef.value fun xs _ => do
let mut varNames xs.mapM fun x => x.fvarId!.getUserName
for h : i in [:element.vars.size] do
let varStx := element.vars[i]
if let `($ident:ident) := varStx then
let j := varNames.size - implicit_underscores - element.vars.size + i
varNames := varNames.set! j ident.getId
return varNames
let mut mvarId := mvarId
for localDecl in ( Term.getMVarDecl mvarId).lctx, varName in varNames[:prefixSize] do
unless localDecl.userName == varName do
mvarId mvarId.rename localDecl.fvarId varName
let numPackedArgs := varNames.size - prefixSize
let rec go (i : Nat) (mvarId : MVarId) (fvarId : FVarId) : TermElabM MVarId := do
trace[Elab.definition.wf] "i: {i}, varNames: {varNames}, goal: {mvarId}"
if i < numPackedArgs - 1 then
let #[s] mvarId.cases fvarId #[{ varNames := [varNames[prefixSize + i]!] }] | unreachable!
go (i+1) s.mvarId s.fields[1]!.fvarId!
else
mvarId.rename fvarId varNames.back
go 0 mvarId fvarId
This ensures the preconditions for `ArgsPacker.uncurryND`.
-/
def checkCodomains (names : Array Name) (prefixArgs : Array Expr) (arities : Array Nat)
(termArgs : TerminationArguments) : TermElabM Expr := do
let mut codomains := #[]
for name in names, arity in arities, termArg in termArgs do
let type inferType (termArg.fn.beta prefixArgs)
let codomain forallBoundedTelescope type arity fun xs codomain => do
let fvars := xs.map (·.fvarId!)
if codomain.hasAnyFVar (fvars.contains ·) then
throwErrorAt termArg.ref m!"The termination argument's type must not depend on the " ++
m!"function's varying parameters, but {name}'s termination argument does:{indentExpr type}\n" ++
"Try using `sizeOf` explicitly"
pure codomain
codomains := codomains.push codomain
def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (fixedPrefixSize : Nat)
(argType : Expr) (wf : TerminationWF) (k : Expr TermElabM α) : TermElabM α := do
let codomain0 := codomains[0]!
for h : i in [1 : codomains.size] do
unless isDefEqGuarded codomain0 codomains[i] do
throwErrorAt termArgs[i]!.ref m!"The termination arguments of mutually recursive functions " ++
m!"must have the same return type, but the termination argument of {names[0]!} has type" ++
m!"{indentExpr codomain0}\n" ++
m!"while the termination argument of {names[i]!} has type{indentExpr codomains[i]}\n" ++
"Try using `sizeOf` explicitly"
return codomain0
/--
If the `termArgs` map the packed argument `argType` to `β`, then this function passes to the
continuation a value of type `WellFoundedRelation argType` that is derived from the instance
for `WellFoundedRelation β` using `invImage`.
-/
def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (prefixArgs : Array Expr)
(argsPacker : ArgsPacker) (argType : Expr) (termArgs : TerminationArguments)
(k : Expr TermElabM α) : TermElabM α := withDeclName unaryPreDefName do
let α := argType
let u getLevel α
let expectedType := mkApp (mkConst ``WellFoundedRelation [u]) α
trace[Elab.definition.wf] "elabWFRel start: {(← mkFreshTypeMVar).mvarId!}"
withDeclName unaryPreDefName do
let mainMVarId := ( mkFreshExprSyntheticOpaqueMVar expectedType).mvarId!
let [fMVarId, wfRelMVarId, _] mainMVarId.apply ( mkConstWithFreshMVarLevels ``invImage) | throwError "failed to apply 'invImage'"
let (d, fMVarId) fMVarId.intro1
let subgoals unpackMutual preDefs fMVarId d
for (d, mvarId) in subgoals, element in wf, preDef in preDefs do
let mvarId unpackUnary preDef fixedPrefixSize mvarId d element
mvarId.withContext do
let errorMsgHeader? := if preDefs.size > 1 then
"The termination argument types differ for the different functions, or depend on the " ++
"function's varying parameters. Try using `sizeOf` explicitly:\nThe termination argument"
else
"The termination argument depends on the function's varying parameters. Try using " ++
"`sizeOf` explicitly:\nThe termination argument"
let value Term.withSynthesize <| elabTermEnsuringType element.body ( mvarId.getType)
(errorMsgHeader? := errorMsgHeader?)
mvarId.assign value
let wfRelVal synthInstance ( inferType (mkMVar wfRelMVarId))
wfRelMVarId.assign wfRelVal
k ( instantiateMVars (mkMVar mainMVarId))
let β checkCodomains (preDefs.map (·.declName)) prefixArgs argsPacker.arities termArgs
let v getLevel β
let packedF argsPacker.uncurryND (termArgs.map (·.fn.beta prefixArgs))
let inst synthInstance (.app (.const ``WellFoundedRelation [v]) β)
let rel instantiateMVars (mkApp4 (.const ``invImage [u,v]) α β packedF inst)
k rel
end Lean.Elab.WF

View File

@@ -0,0 +1,106 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Joachim Breitner
-/
prelude
import Lean.Parser.Term
import Lean.Elab.Term
import Lean.Elab.Binders
import Lean.Elab.SyntheticMVars
import Lean.Elab.PreDefinition.WF.TerminationHint
import Lean.PrettyPrinter.Delaborator
/-!
This module contains the data type `TerminationArgument`, the elaborated form of a `TerminationBy`
clause, the `TerminationArguments` type for a clique and the elaboration functions.
-/
set_option autoImplicit false
namespace Lean.Elab.WF
open Lean Meta Elab Term
/--
Elaborated form for a `termination_by` clause.
The `fn` has the same (value) arity as the recursive functions (stored in
`arity`), and maps its arguments (including fixed prefix, in unpacked form) to
the termination argument.
-/
structure TerminationArgument where
ref : Syntax
arity : Nat
extraParams : Nat
fn : Expr
deriving Inhabited
/-- A complete set of `TerminationArgument`s, as applicable to a single clique. -/
abbrev TerminationArguments := Array TerminationArgument
/--
Elaborates a `TerminationBy` to an `TerminationArgument`.
* `type` is the full type of the original recursive function, including fixed prefix.
* `arity` is the value arity of the recursive function; the termination argument cannot take more.
* `extraParams` is the the number of parameters the function has after the colon; together with
`arity` indicates how many parameters of the function are before the colon and thus in scope.
* `hint : TerminationBy` is the syntactic `TerminationBy`.
-/
def TerminationArgument.elab (funName : Name) (type : Expr) (arity extraParams : Nat)
(hint : TerminationBy) : TermElabM TerminationArgument := withDeclName funName do
assert! extraParams arity
if hint.vars.size > extraParams then
let mut msg := m!"{parameters hint.vars.size} bound in `termination_by`, but the body of " ++
m!"{funName} only binds {parameters extraParams}."
if let `($ident:ident) := hint.vars[0]! then
if ident.getId.isSuffixOf funName then
msg := msg ++ m!" (Since Lean v4.6.0, the `termination_by` clause no longer " ++
"expects the function name here.)"
throwErrorAt hint.ref msg
-- Bring parameters before the colon into scope
let r withoutErrToSorry <|
forallBoundedTelescope type (arity - extraParams) fun ys type' => do
-- Bring the variables bound by `termination_by` into scope.
elabFunBinders hint.vars (some type') fun xs type' => do
-- Elaborate the body in this local environment
let body Lean.Elab.Term.withSynthesize <| elabTermEnsuringType hint.body none
-- Now abstract also over the remaining extra parameters
forallBoundedTelescope type'.get! (extraParams - hint.vars.size) fun zs _ => do
mkLambdaFVars (ys ++ xs ++ zs) body
-- logInfo m!"elabTermValue: {r}"
check r
pure { ref := hint.ref, arity, extraParams, fn := r}
where
parameters : Nat MessageData
| 1 => "one parameter"
| n => m!"{n} parameters"
open PrettyPrinter Delaborator SubExpr Parser.Termination Parser.Term in
def TerminationArgument.delab (termArg : TerminationArgument) : MetaM (TSyntax ``terminationBy) := do
lambdaTelescope termArg.fn fun ys e => do
let e mkLambdaFVars ys[termArg.arity - termArg.extraParams:] e -- undo overshooting by lambdaTelescope
pure ( delabCore e (delab := go termArg.extraParams #[])).1
where
go : Nat TSyntaxArray [`ident, `Lean.Parser.Term.hole] DelabM (TSyntax ``terminationBy)
| 0, vars => do
-- drop trailing underscores
let mut vars := vars
while ! vars.isEmpty && vars.back.raw.isOfKind ``hole do vars := vars.pop
if vars.isEmpty then
`(terminationBy|termination_by $( Delaborator.delab))
else
`(terminationBy|termination_by $vars* => $( Delaborator.delab))
| i+1, vars => do
let e getExpr
unless e.isLambda do return go 0 vars -- should not happen
-- Delaborate unused parameters with `_`
if e.bindingBody!.hasLooseBVar 0 then
withBindingBodyUnusedName fun n => go i (vars.push n)
else
descend e.bindingBody! 1 (go i (vars.push ( `(hole|_))))

View File

@@ -26,18 +26,6 @@ structure TerminationBy where
synthetic : Bool := false
deriving Inhabited
open Parser.Termination in
def TerminationBy.unexpand (wf : TerminationBy) : MetaM (TSyntax ``terminationBy) := do
-- TODO: Why can I not just use $wf.vars in the quotation below?
let vars : TSyntaxArray `ident := wf.vars.map (·.raw)
if vars.isEmpty then
`(terminationBy|termination_by $wf.body)
else
`(terminationBy|termination_by $vars* => $wf.body)
/-- A complete set of `termination_by` hints, as applicable to a single clique. -/
abbrev TerminationWF := Array TerminationBy
/-- A single `decreasing_by` clause -/
structure DecreasingBy where
ref : Syntax

View File

@@ -80,7 +80,7 @@ private def printIdCore (id : Name) : CommandElabM Unit := do
private def printId (id : Syntax) : CommandElabM Unit := do
addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none
let cs resolveGlobalConstWithInfos id
let cs liftCoreM <| realizeGlobalConstWithInfos id
cs.forM printIdCore
@[builtin_command_elab «print»] def elabPrint : CommandElab
@@ -125,7 +125,7 @@ private def printAxiomsOf (constName : Name) : CommandElabM Unit := do
@[builtin_command_elab «printAxioms»] def elabPrintAxioms : CommandElab
| `(#print%$tk axioms $id) => withRef tk do
let cs resolveGlobalConstWithInfos id
let cs liftCoreM <| realizeGlobalConstWithInfos id
cs.forM printAxiomsOf
| _ => throwUnsupportedSyntax
@@ -140,7 +140,7 @@ private def printEqnsOf (constName : Name) : CommandElabM Unit := do
@[builtin_command_elab «printEqns»] def elabPrintEqns : CommandElab := fun stx => do
let id := stx[2]
let cs resolveGlobalConstWithInfos id
let cs liftCoreM <| realizeGlobalConstWithInfos id
cs.forM printEqnsOf
end Lean.Elab.Command

View File

@@ -92,7 +92,7 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do
notation "x++" => x.foo
```
-/
if let _::_ resolveGlobalNameWithInfos stx val then
if let _::_ realizeGlobalNameWithInfos stx val then
return
if ( read).quotLCtx.contains val then
return

View File

@@ -892,7 +892,7 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
let exts := stx[3]
let parents := if exts.isNone then #[] else exts[0][1].getSepArgs
let optType := stx[4]
let derivingClassViews getOptDerivingClasses stx[6]
let derivingClassViews liftCoreM <| getOptDerivingClasses stx[6]
let type if optType.isNone then `(Sort _) else pure optType[0][1]
let declName
runTermElabM fun scopeVars => do

View File

@@ -382,7 +382,6 @@ def addMacroScopeIfLocal [MonadQuotation m] [Monad m] (name : Name) (attrKind :
let name ← match name? with
| some name => pure name.getId
| none => addMacroScopeIfLocal (← liftMacroM <| mkNameFromParserSyntax cat syntaxParser) attrKind
trace[Meta.debug] "name: {name}"
let prio ← liftMacroM <| evalOptPrio prio?
let idRef := (name?.map (·.raw)).getD tk
let stxNodeKind := (← getCurrNamespace) ++ name

View File

@@ -38,3 +38,4 @@ import Lean.Elab.Tactic.Symm
import Lean.Elab.Tactic.SolveByElim
import Lean.Elab.Tactic.LibrarySearch
import Lean.Elab.Tactic.ShowTerm
import Lean.Elab.Tactic.Rfl

View File

@@ -11,7 +11,7 @@ namespace Lean.Elab.Tactic.Conv
open Meta
@[builtin_tactic Lean.Parser.Tactic.Conv.delta] def evalDelta : Tactic := fun stx => withMainContext do
let declNames stx[1].getArgs.mapM resolveGlobalConstNoOverloadWithInfo
let declNames stx[1].getArgs.mapM fun stx => realizeGlobalConstNoOverloadWithInfo stx
let lhsNew deltaExpand ( instantiateMVars ( getLhs)) declNames.contains
changeLhs lhsNew

View File

@@ -12,7 +12,7 @@ open Meta
@[builtin_tactic Lean.Parser.Tactic.Conv.unfold] def evalUnfold : Tactic := fun stx => withMainContext do
for declNameId in stx[1].getArgs do
let declName resolveGlobalConstNoOverloadWithInfo declNameId
let declName realizeGlobalConstNoOverloadWithInfo declNameId
applySimpResult ( unfold ( getLhs) declName)
end Lean.Elab.Tactic.Conv

View File

@@ -29,7 +29,7 @@ def deltaTarget (declNames : Array Name) : TacticM Unit := do
/-- "delta " ident+ (location)? -/
@[builtin_tactic Lean.Parser.Tactic.delta] def evalDelta : Tactic := fun stx => do
let declNames stx[1].getArgs.mapM resolveGlobalConstNoOverloadWithInfo
let declNames stx[1].getArgs.mapM fun stx => realizeGlobalConstNoOverloadWithInfo stx
let loc := expandOptLocation stx[2]
withLocation loc (deltaLocalDecl declNames) (deltaTarget declNames)
(throwTacticEx `delta · m!"did not delta reduce {declNames}")

View File

@@ -153,7 +153,7 @@ elaborating to `x.1 = y.1 → x.2 = y.2 → x = y`, for example.
@[builtin_term_elab extType] def elabExtType : TermElab := fun stx _ => do
match stx with
| `(ext_type% $flat:term $struct:ident) => do
withExtHyps ( resolveGlobalConstNoOverloadWithInfo struct) flat fun params x y hyps => do
withExtHyps ( realizeGlobalConstNoOverloadWithInfo struct) flat fun params x y hyps => do
let ty := hyps.foldr (init := mkEq x y) fun (f, h) ty =>
mkForall f BinderInfo.default h ty
mkForallFVars (params |>.push x |>.push y) ty
@@ -166,7 +166,7 @@ elaborating to `x = y ↔ x.1 = y.1 ∧ x.2 = y.2`, for example.
@[builtin_term_elab extIffType] def elabExtIffType : TermElab := fun stx _ => do
match stx with
| `(ext_iff_type% $flat:term $struct:ident) => do
withExtHyps ( resolveGlobalConstNoOverloadWithInfo struct) flat fun params x y hyps => do
withExtHyps ( realizeGlobalConstNoOverloadWithInfo struct) flat fun params x y hyps => do
mkForallFVars (params |>.push x |>.push y) <|
mkIff ( mkEq x y) <| mkAndN (hyps.map (·.2)).toList
| _ => throwUnsupportedSyntax

View File

@@ -534,9 +534,9 @@ private def elabTermForElim (stx : Syntax) : TermElabM Expr := do
return e
-- `optElimId` is of the form `("using" term)?`
private def getElimNameInfo (optElimId : Syntax) (targets : Array Expr) (induction : Bool): TacticM ElimInfo := do
private def getElimNameInfo (optElimId : Syntax) (targets : Array Expr) (induction : Bool) : TacticM ElimInfo := do
if optElimId.isNone then
if let some elimName getCustomEliminator? targets then
if let some elimName getCustomEliminator? targets induction then
return getElimInfo elimName
unless targets.size == 1 do
throwError "eliminator must be provided when multiple targets are used (use 'using <eliminator-name>'), and no default eliminator has been registered using attribute `[eliminator]`"

View File

@@ -268,7 +268,7 @@ open Command in
match stx with
| `(norm_cast_add_elim $id:ident) =>
Elab.Command.liftCoreM do MetaM.run' do
addElim ( resolveGlobalConstNoOverload id)
addElim ( realizeGlobalConstNoOverload id)
| _ => throwUnsupportedSyntax
end Lean.Elab.Tactic.NormCast

View File

@@ -5,8 +5,10 @@ Authors: Scott Morrison
-/
prelude
import Init.BinderPredicates
import Init.Data.Int.Order
import Init.Data.List.Lemmas
import Init.Data.Nat.MinMax
import Init.Data.Option.Lemmas
import Init.Data.Nat.Bitwise.Lemmas
/-!
# `List.nonzeroMinimum`, `List.minNatAbs`, `List.maxNatAbs`

View File

@@ -7,8 +7,9 @@ prelude
import Init.Omega.LinearCombo
import Init.Omega.Int
import Init.Omega.Logic
import Init.Data.BitVec
import Init.Data.BitVec.Basic
import Lean.Meta.AppBuilder
import Lean.Meta.Canonicalizer
/-!
# The `OmegaM` state monad.
@@ -54,7 +55,7 @@ structure State where
atoms : HashMap Expr Nat := {}
/-- An intermediate layer in the `OmegaM` monad. -/
abbrev OmegaM' := StateRefT State (ReaderT Context MetaM)
abbrev OmegaM' := StateRefT State (ReaderT Context CanonM)
/--
Cache of expressions that have been visited, and their reflection as a linear combination.
@@ -70,7 +71,7 @@ abbrev OmegaM := StateRefT Cache OmegaM'
/-- Run a computation in the `OmegaM` monad, starting with no recorded atoms. -/
def OmegaM.run (m : OmegaM α) (cfg : OmegaConfig) : MetaM α :=
m.run' HashMap.empty |>.run' {} { cfg }
m.run' HashMap.empty |>.run' {} { cfg } |>.run
/-- Retrieve the user-specified configuration options. -/
def cfg : OmegaM OmegaConfig := do pure ( read).cfg
@@ -176,7 +177,7 @@ def analyzeAtom (e : Expr) : OmegaM (HashSet Expr) := do
| _, (``Fin.val, #[n, i]) =>
r := r.insert (mkApp2 (.const ``Fin.isLt []) n i)
| _, (``BitVec.toNat, #[n, x]) =>
r := r.insert (mkApp2 (.const ``BitVec.toNat_lt []) n x)
r := r.insert (mkApp2 (.const ``BitVec.isLt []) n x)
| _, _ => pure ()
return r
| (``HDiv.hDiv, #[_, _, _, _, x, k]) => match natCast? k with
@@ -244,6 +245,7 @@ Return its index, and, if it is new, a collection of interesting facts about the
-/
def lookup (e : Expr) : OmegaM (Nat × Option (HashSet Expr)) := do
let c getThe State
let e canon e
match c.atoms.find? e with
| some i => return (i, none)
| none =>

View File

@@ -51,11 +51,13 @@ def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool)
x symm term
else
-- Try to get equation theorems for `id`.
let declName try resolveGlobalConstNoOverload id catch _ => return ( x symm term)
let declName try realizeGlobalConstNoOverload id catch _ => return ( x symm term)
let some eqThms getEqnsFor? declName (nonRec := true) | x symm term
let rec go : List Name TacticM Unit
| [] => throwError "failed to rewrite using equation theorems for '{declName}'"
| eqThm::eqThms => (x symm (mkIdentFrom id eqThm)) <|> go eqThms
-- Remark: we prefix `eqThm` with `_root_` to ensure it is resolved correctly.
-- See test: `rwPrioritizesLCtxOverEnv.lean`
| eqThm::eqThms => (x symm (mkIdentFrom id (`_root_ ++ eqThm))) <|> go eqThms
go eqThms.toList
discard <| Term.addTermInfo id ( mkConstWithFreshMVarLevels declName) (lctx? := getLCtx)
match term with

View File

@@ -0,0 +1,26 @@
/-
Copyright (c) 2022 Newell Jensen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Newell Jensen, Thomas Murrills
-/
prelude
import Lean.Meta.Tactic.Rfl
import Lean.Elab.Tactic.Basic
/-!
# `rfl` tactic extension for reflexive relations
This extends the `rfl` tactic so that it works on any reflexive relation,
provided the reflexivity lemma has been marked as `@[refl]`.
-/
namespace Lean.Elab.Tactic.Rfl
/--
This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
-/
elab_rules : tactic
| `(tactic| rfl) => withMainContext do liftMetaFinishingTactic (·.applyRfl)
end Lean.Elab.Tactic.Rfl

View File

@@ -7,7 +7,7 @@ prelude
import Lean.Elab.ElabRules
import Lean.Meta.Tactic.TryThis
namespace Std.Tactic
namespace Lean.Elab.Tactic.ShowTerm
open Lean Elab Term Tactic Meta.Tactic.TryThis Parser.Tactic
@[builtin_tactic showTerm] def evalShowTerm : Tactic := fun stx =>
@@ -26,3 +26,5 @@ open Lean Elab Term Tactic Meta.Tactic.TryThis Parser.Tactic
addTermSuggestion tk ( instantiateMVars e).headBeta (origSpan? := getRef)
pure e
| _, _ => throwUnsupportedSyntax
end Lean.Elab.Tactic.ShowTerm

View File

@@ -179,7 +179,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
thms := thms.eraseCore (.fvar fvar.fvarId!)
else
let id := arg[1]
let declNames? try pure (some ( resolveGlobalConst id)) catch _ => pure none
let declNames? try pure (some ( realizeGlobalConst id)) catch _ => pure none
if let some declNames := declNames? then
let declName ensureNonAmbiguous id declNames
if ( Simp.isSimproc declName) then

View File

@@ -56,7 +56,8 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
| _ => throwUnsupportedSyntax
/-- Implementation of `dsimp?`. -/
def dsimpLocation' (ctx : Simp.Context) (loc : Location) : TacticM Simp.UsedSimps := do
def dsimpLocation' (ctx : Simp.Context) (simprocs : SimprocsArray) (loc : Location) :
TacticM Simp.UsedSimps := do
match loc with
| Location.targets hyps simplifyTarget =>
withMainContext do
@@ -69,8 +70,8 @@ where
/-- Implementation of `dsimp?`. -/
go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.UsedSimps := do
let mvarId getMainGoal
let (result?, usedSimps)
dsimpGoal mvarId ctx (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp)
let (result?, usedSimps) dsimpGoal mvarId ctx simprocs (simplifyTarget := simplifyTarget)
(fvarIdsToSimp := fvarIdsToSimp)
match result? with
| none => replaceMainGoal []
| some mvarId => replaceMainGoal [mvarId]
@@ -83,8 +84,9 @@ where
`(tactic| dsimp!%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?)
else
`(tactic| dsimp%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?)
let { ctx, .. } withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
let usedSimps dsimpLocation' ctx <| (loc.map expandLocation).getD (.targets #[] true)
let { ctx, simprocs, .. }
withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
let usedSimps dsimpLocation' ctx simprocs <| (loc.map expandLocation).getD (.targets #[] true)
let stx mkSimpCallStx stx usedSimps
addSuggestion tk stx (origSpan? := getRef)
| _ => throwUnsupportedSyntax

View File

@@ -18,7 +18,7 @@ register_option linter.unnecessarySimpa : Bool := {
descr := "enable the 'unnecessary simpa' linter"
}
namespace Std.Tactic.Simpa
namespace Lean.Elab.Tactic.Simpa
open Lean Parser.Tactic Elab Meta Term Tactic Simp Linter
@@ -86,3 +86,5 @@ deriving instance Repr for UseImplicitLambdaResult
| _ => unreachable!
TryThis.addSuggestion tk stx (origSpan? := getRef)
| _ => throwUnsupportedSyntax
end Lean.Elab.Tactic.Simpa

View File

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
-/
prelude
import Init.Simproc
import Lean.ReservedNameAction
import Lean.Meta.Tactic.Simp.Simproc
import Lean.Elab.Binders
import Lean.Elab.SyntheticMVars
@@ -37,16 +38,16 @@ namespace Command
@[builtin_command_elab Lean.Parser.simprocPattern] def elabSimprocPattern : CommandElab := fun stx => do
let `(simproc_pattern% $pattern => $declName) := stx | throwUnsupportedSyntax
let declName resolveGlobalConstNoOverload declName
liftTermElabM do
let declName realizeGlobalConstNoOverload declName
discard <| checkSimprocType declName
let keys elabSimprocKeys pattern
registerSimproc declName keys
@[builtin_command_elab Lean.Parser.simprocPatternBuiltin] def elabSimprocPatternBuiltin : CommandElab := fun stx => do
let `(builtin_simproc_pattern% $pattern => $declName) := stx | throwUnsupportedSyntax
let declName resolveGlobalConstNoOverload declName
liftTermElabM do
let declName realizeGlobalConstNoOverload declName
let dsimp checkSimprocType declName
let keys elabSimprocKeys pattern
let registerProcName := if dsimp then ``registerBuiltinDSimproc else ``registerBuiltinSimproc

View File

@@ -24,7 +24,7 @@ def unfoldTarget (declName : Name) : TacticM Unit := do
go declNameId loc
where
go (declNameId : Syntax) (loc : Location) : TacticM Unit := do
let declName resolveGlobalConstNoOverloadWithInfo declNameId
let declName realizeGlobalConstNoOverloadWithInfo declNameId
withLocation loc (unfoldLocalDecl declName) (unfoldTarget declName) (throwTacticEx `unfold · m!"did not unfold '{declName}'")
end Lean.Elab.Tactic

View File

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
prelude
import Lean.ReservedNameAction
import Lean.Meta.AppBuilder
import Lean.Meta.CollectMVars
import Lean.Meta.Coe
@@ -793,10 +794,10 @@ def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgH
| _ => throwTypeMismatchError errorMsgHeader? expectedType ( inferType e) e f?
/--
If `expectedType?` is `some t`, then ensure `t` and `eType` are definitionally equal.
If they are not, then try coercions.
If `expectedType?` is `some t`, then ensures `t` and `eType` are definitionally equal by inserting a coercion if necessary.
Argument `f?` is used only for generating error messages. -/
Argument `f?` is used only for generating error messages when inserting coercions fails.
-/
def ensureHasType (expectedType? : Option Expr) (e : Expr)
(errorMsgHeader? : Option String := none) (f? : Option Expr := none) : TermElabM Expr := do
let some expectedType := expectedType? | return e
@@ -1432,9 +1433,22 @@ def addDotCompletionInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr)
def elabTerm (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (implicitLambda := true) : TermElabM Expr :=
withRef stx <| elabTermAux expectedType? catchExPostpone implicitLambda stx
/--
Similar to `Lean.Elab.Term.elabTerm`, but ensures that the type of the elaborated term is `expectedType?`
by inserting coercions if necessary.
If `errToSorry` is true, then if coercion insertion fails, this function returns `sorry` and logs the error.
Otherwise, it throws the error.
-/
def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (implicitLambda := true) (errorMsgHeader? : Option String := none) : TermElabM Expr := do
let e elabTerm stx expectedType? catchExPostpone implicitLambda
withRef stx <| ensureHasType expectedType? e errorMsgHeader?
try
withRef stx <| ensureHasType expectedType? e errorMsgHeader?
catch ex =>
if ( read).errToSorry && ex matches .error .. then
exceptionToSorry ex expectedType?
else
throw ex
/-- Execute `x` and return `some` if no new errors were recorded or exceptions were thrown. Otherwise, return `none`. -/
def commitIfNoErrors? (x : TermElabM α) : TermElabM (Option α) := do
@@ -1640,7 +1654,7 @@ def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved
if let some (e, projs) := preresolved.findSome? fun (n, projs) => ctx.sectionFVars.find? n |>.map (·, projs) then
return [(e, projs)] -- section variables should shadow global decls
if preresolved.isEmpty then
process ( resolveGlobalName n)
process ( realizeGlobalName n)
else
process preresolved
where

View File

@@ -209,8 +209,13 @@ def getModuleIdxFor? (env : Environment) (declName : Name) : Option ModuleIdx :=
def isConstructor (env : Environment) (declName : Name) : Bool :=
match env.find? declName with
| ConstantInfo.ctorInfo _ => true
| _ => false
| some (.ctorInfo _) => true
| _ => false
def isSafeDefinition (env : Environment) (declName : Name) : Bool :=
match env.find? declName with
| some (.defnInfo { safety := .safe, .. }) => true
| _ => false
def getModuleIdx? (env : Environment) (moduleName : Name) : Option ModuleIdx :=
env.header.moduleNames.findIdx? (· == moduleName)
@@ -230,6 +235,7 @@ inductive KernelException where
| exprTypeMismatch (env : Environment) (lctx : LocalContext) (expr : Expr) (expectedType : Expr)
| appTypeMismatch (env : Environment) (lctx : LocalContext) (app : Expr) (funType : Expr) (argType : Expr)
| invalidProj (env : Environment) (lctx : LocalContext) (proj : Expr)
| thmTypeIsNotProp (env : Environment) (name : Name) (type : Expr)
| other (msg : String)
| deterministicTimeout
| excessiveMemory
@@ -769,6 +775,33 @@ partial def importModulesCore (imports : Array Import) : ImportStateM Unit := do
moduleNames := s.moduleNames.push i.module
}
/--
Return `true` if `cinfo₁` and `cinfo₂` are theorems with the same name, universe parameters,
and types. We allow different modules to prove the same theorem.
Motivation: We want to generate equational theorems on demand and potentially
in different files, and we want them to have non-private names.
We may add support for other kinds of definitions in the future. For now, theorems are
sufficient for our purposes.
We may have to revise this design decision and eagerly generate equational theorems when
we implement the module system.
Remark: we do not check whether the theorem `value` field match. This feature is useful and
ensures the proofs for equational theorems do not need to be identical. This decision
relies on the fact that theorem types are propositions, we have proof irrelevance,
and theorems are (mostly) opaque in Lean. For `Acc.rec`, we may unfold theorems
during type-checking, but we are assuming this is not an issue in practice,
and we are planning to address this issue in the future.
-/
private def equivInfo (cinfo₁ cinfo₂ : ConstantInfo) : Bool := Id.run do
let .thmInfo tval₁ := cinfo₁ | false
let .thmInfo tval₂ := cinfo₂ | false
return tval₁.name == tval₂.name
&& tval₁.type == tval₂.type
&& tval₁.levelParams == tval₂.levelParams
&& tval₁.all == tval₂.all
/--
Construct environment from `importModulesCore` results.
@@ -787,11 +820,13 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
for h:modIdx in [0:s.moduleData.size] do
let mod := s.moduleData[modIdx]'h.upper
for cname in mod.constNames, cinfo in mod.constants do
match constantMap.insert' cname cinfo with
| (constantMap', replaced) =>
match constantMap.insertIfNew cname cinfo with
| (constantMap', cinfoPrev?) =>
constantMap := constantMap'
if replaced then
throwAlreadyImported s const2ModIdx modIdx cname
if let some cinfoPrev := cinfoPrev? then
-- Recall that the map has not been modified when `cinfoPrev? = some _`.
unless equivInfo cinfoPrev cinfo do
throwAlreadyImported s const2ModIdx modIdx cname
const2ModIdx := const2ModIdx.insert cname modIdx
for cname in mod.extraConstNames do
const2ModIdx := const2ModIdx.insert cname modIdx

View File

@@ -924,7 +924,7 @@ def isRawNatLit : Expr → Bool
| lit (Literal.natVal _) => true
| _ => false
def natLit? : Expr Option Nat
def rawNatLit? : Expr Option Nat
| lit (Literal.natVal v) => v
| _ => none
@@ -2003,4 +2003,46 @@ def mkEM (p : Expr) : Expr := mkApp (mkConst ``Classical.em) p
/-- Return `p ↔ q` -/
def mkIff (p q : Expr) : Expr := mkApp2 (mkConst ``Iff) p q
private def natAddFn : Expr :=
let nat := mkConst ``Nat
mkApp4 (mkConst ``HAdd.hAdd [0, 0, 0]) nat nat nat (mkApp2 (mkConst ``instHAdd [0]) nat (mkConst ``instAddNat))
private def natSubFn : Expr :=
let nat := mkConst ``Nat
mkApp4 (mkConst ``HSub.hSub [0, 0, 0]) nat nat nat (mkApp2 (mkConst ``instHSub [0]) nat (mkConst ``instSubNat))
private def natMulFn : Expr :=
let nat := mkConst ``Nat
mkApp4 (mkConst ``HMul.hMul [0, 0, 0]) nat nat nat (mkApp2 (mkConst ``instHMul [0]) nat (mkConst ``instMulNat))
/-- Given `a : Nat`, returns `Nat.succ a` -/
def mkNatSucc (a : Expr) : Expr :=
mkApp (mkConst ``Nat.succ) a
/-- Given `a b : Nat`, returns `a + b` -/
def mkNatAdd (a b : Expr) : Expr :=
mkApp2 natAddFn a b
/-- Given `a b : Nat`, returns `a - b` -/
def mkNatSub (a b : Expr) : Expr :=
mkApp2 natSubFn a b
/-- Given `a b : Nat`, returns `a * b` -/
def mkNatMul (a b : Expr) : Expr :=
mkApp2 natMulFn a b
private def natLEPred : Expr :=
mkApp2 (mkConst ``LE.le [0]) (mkConst ``Nat) (mkConst ``instLENat)
/-- 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)
/-- Given `a b : Nat`, return `a = b` -/
def mkNatEq (a b : Expr) : Expr :=
mkApp2 natEqPred a b
end Lean

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