Compare commits

..

56 Commits

Author SHA1 Message Date
Rob Simmons
d8488666c1 Add new tests 2025-12-04 18:51:01 -05:00
Rob Simmons
06580e2636 feat: hint when an autobound variable's type fails to be a function or equality 2025-12-04 18:25:30 -05:00
Wojciech Różowski
42ded564bd feat: add difference on ExtDHashMap/ExtHashMap/ExtHashSet (#11399)
This PR adds support for the difference operation for
`ExtDHashMap`/`ExtHashMap`/`ExtHashSet` and proves several lemmas about
it.

---------

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
2025-12-04 16:06:31 +00:00
Joachim Breitner
f0738c2cd1 perf: in CaseValues, subst only once (#11510)
This PR avoids running substCore twice in caseValues.
2025-12-04 15:43:46 +00:00
Lean stage0 autoupdater
5f561bfee2 chore: update stage0 2025-12-04 15:52:42 +00:00
Joachim Breitner
af6d2077a0 refactor: use match compilation to generate splitter (#11220)
This PR changes how match splitters are generated: Rather than rewriting
the match statement, the match compilation pipeline is used again.


The benefits are:

* Re-doing the match compilation means we can do more intelligent book
keeping, e.g. prove overlap assumptions only once and re-use the proof,
or prune the context of the MVar to speed up `contradiction`. This may
have allowed a different solution than #11200.
 
* It would unblock #11105, as the existing splitter implementation would
have trouble dealing with the matchers produced that way.
 
* It provides the necessary machinery also for source-exposed “none of
the above” bindings, a feature that we probably want at some point (and
we mostly need to find good syntax for, see #3136, although maybe I
should open a dedicated RFC).

* It allows us to skip costly things during matcher creation that would
only be useful for the splitter, and thus allows performance
improvements like #11508.
 
 * We can drop the existing implementation.
 
It’s not entirely free:

* We have to run `simpH` twice, once for the match equations and once
for the splitter.
2025-12-04 15:03:13 +00:00
Paul Reichert
31d629cb67 feat: more Nat range lemmas (#11321)
This PR provides specialized lemmas about `Nat` ranges, including `simp`
annotations and induction principles for proving properties for all
ranges.
2025-12-04 14:14:45 +00:00
Joachim Breitner
d60ef53d54 refactor: make CCPO class Prop-valued (#11425)
This PR changes `Lean.Order.CCPO` and `.CompleteLattice` to carry a
Prop. This avoids the `CCPO IO` instance from being `noncomputable`.
2025-12-04 13:33:36 +00:00
Robert J. Simmons
dd57725244 feat: @[suggest_for] attribute to inform replacements (#11367)
This PR introduces a new annotation that allows definitions to describe
plausible-but-wrong name variants for the purpose of improving error
messages.

This PR just adds the notation and extra functionality; a stage0 update
will allow standard Lean functions to have suggestion annotations.
(Hence the changelog-no tag: this should go in the changelog when some
preliminary annotations are actually added.)

## Example

```lean4
inductive MyBool where | tt | ff

attribute [suggest_for MyBool.true] MyBool.tt
attribute [suggest_for MyBool.false] MyBool.ff

@[suggest_for MyBool.not]
def MyBool.swap : MyBool → MyBool
  | tt => ff
  | ff => tt

/--
error: Unknown constant `MyBool.true`

Hint: Perhaps you meant `MyBool.tt` in place of `MyBool.true`:
  M̵y̵B̵o̵o̵l̵.̵t̵r̵u̵e̵M̲y̲B̲o̲o̲l̲.̲t̲t̲
-/
#guard_msgs in
example := MyBool.true

/--
error: Invalid field `not`: The environment does not contain `MyBool.not`, so it is not possible to project the field `not` from an expression
  MyBool.tt
of type `MyBool`

Hint: Perhaps you meant one of these in place of `MyBool.not`:
  [apply] `MyBool.swap`: MyBool.tt.swap
-/
#guard_msgs in
example := MyBool.tt.not
```
2025-12-04 13:20:37 +00:00
Markus Himmel
e548fa414c fix: Char -> Bool as default instance for string search (#11503)
This PR marks `Char -> Bool` patterns as default instances for string
search. This means that things like `" ".find (·.isWhitespace)` can now
be elaborated without error.

Previously, it was necessary to write `" ".find Char.isWhitespace`.

Thank you to David Christiansen for the idea of using a default
instance.
2025-12-04 09:25:16 +00:00
Joachim Breitner
b94cf2c9be test: add big match on nat lit benchmarks (#11502)
This PR adds two benchmarks for elaborating match statements of many
`Nat` literals, one without and one with splitter generation.
2025-12-04 08:21:56 +00:00
Robert J. Simmons
dd28f00588 feat: hint alternatives when field-projecting from an unknown type (#11482)
This PR gives suggestions based on the currently-available constants
when projecting from an unknown type.

## Example: single suggestion in namespace

This was the originally motivating example, as the string refactor led
to a number of anonymous-lambda-expressions with `Char` functions that
were no longer recognized as such.

```lean4
example := (·.isWhitespace)
```
Before:
```
Invalid field notation: Type of
  x✝
is not known; cannot resolve field `isWhitespace`
```
The message is unchanged, but this PR adds a hint:
```
Hint: Consider replacing the field projection `.isWhitespace` with a call to the function `Char.isWhitespace`.
```

## Example: single suggestion in namespace

```lean4
example := fun n => n.succ
```
Before:
```
Invalid field notation: Type of
  n
is not known; cannot resolve field `succ`
```
The message is unchanged, but this PR adds a hint:
```
Hint: Consider replacing the field projection with a call to one of the following:
  • `Fin.succ`
  • `Nat.succ`
  • `Std.PRange.succ`
```
2025-12-03 20:48:34 +00:00
Joachim Breitner
54fbe931ab refactor: make MatchEqs a leaf module (#11493)
This PR makes `Match.MatchEqs` a leaf module, to be less restricted in
which features we can use there.
2025-12-03 09:15:36 +00:00
Joachim Breitner
fb261921b9 refactor: use withImplicitBinderInfos and mkArrowN in more places (#11492)
This PR uses the the helper functions withImplicitBinderInfos and
mkArrowN in more places.
2025-12-03 08:42:16 +00:00
Leonardo de Moura
0173444d24 feat: heterogeneous contructor injectivity in grind (#11491)
This PR implements heterogeneous contructor injectivity in `grind`.

Example:
```lean
opaque double : Nat → Nat

inductive Parity : Nat -> Type
  | even (n) : Parity (double n)
  | odd  (n) : Parity (Nat.succ (double n))

opaque q : Nat → Nat → Prop
axiom qax : q a b → double a = double b
attribute [grind →] qax

example
  (motive : (x : Nat) → Parity x → Sort u_1)
  (h_2 : (j : Nat) → motive (double j) (Parity.even j))
  (j n : Nat)
  (heq_1 : q j n) -- Implies that `double j = double n`
  (heq_2 : Parity.even n ≍ Parity.even j):
  h_2 n ≍ h_2 j := by
grind
```

Closes #11449
2025-12-03 04:01:19 +00:00
Leonardo de Moura
1377da0c76 feat: heterogeneous constructor injectivity theorems (#11487)
This PR adds a heterogeneous version of the constructor injectivity
theorems. These theorems are useful for indexed families, and will be
used in `grind`.
2025-12-03 01:42:46 +00:00
Mac Malone
5db4f96699 feat: lake: resolve module clashes on import (#11270)
This PR adds a module resolution procedure to Lake to disambiguate
modules that are defined in multiple packages.

On an `import`, Lake will now check if multiple packages within the
workspace define the module. If so, it will verify that modules have
sufficiently similar definitions (i.e., artifacts with the same content
hashes). If not, Lake will report an error.

This verification is currently only done for direct imports. Transitive
imports are not checked for consistency. An overhaul of transitive
imports will come later.
2025-12-03 00:46:20 +00:00
Leonardo de Moura
8bc3eb1265 fix: grind pattern validation (#11484)
This PR fixes a bug in the `grind` pattern validation. The bug affected
type classes that were propositions.

Closes #11477
2025-12-02 19:57:58 +00:00
Lean stage0 autoupdater
cac2c47376 chore: update stage0 2025-12-02 20:03:50 +00:00
David Thrane Christiansen
3fe368e8e7 feat: allow Verso docstrings to suppose the existence of instances (#11476)
This PR adds a `` {givenInstance}`C` `` documentation role that adds an
instance of `C` to the document's local assumptions.
2025-12-02 19:16:35 +00:00
Leonardo de Moura
f8866dcc59 fix: grind? dropping options (#11481)
This PR fixes a bug in `grind?`. The suggestion using the `grind`
interactive mode was dropping the configuration options provided by the
user. In the following account, the third suggestion was dropping the
`-reducible` option.

```lean
/--
info: Try these:
  [apply] grind -reducible only [Equiv.congr_fun, #5103]
  [apply] grind -reducible only [Equiv.congr_fun]
  [apply] grind -reducible => cases #5103 <;> instantiate only [Equiv.congr_fun]
-/
example :
    (Equiv.sigmaCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂)
    = (Equiv.sigmaEquivProd α₁ β₁).trans (prodCongrRight e) := by
  grind? -reducible [Equiv.congr_fun]
```
2025-12-02 19:00:29 +00:00
Leonardo de Moura
9263a6cc9c feat: add Grind.Config.reducible (#11480)
This PR adds the `grind` option `reducible` (default: `true`). When
enabled, definitional equality tests expand only declarations marked as
`@[reducible]`.
Use `grind -reducible` to allow expansion of non-reducible declarations
during definitional equality tests.
This option affects only definitional equality; the canonicalizer and
theorem pattern internalization always unfold reducible declarations
regardless of this setting.
2025-12-02 18:10:55 +00:00
Robert J. Simmons
edcef51434 feat: improve error messages for invalid field access (#11456)
This PR refines several error error messages, mostly involving invalid
use of field notation, generalized field notation, and numeric
projection. Provides a new error explanation for field notation.

## Error message changes

In general:
- Uses a slightly different convention for expression-type pairs, where
the expression is always given `indentExpr` and the type is given
`inlineExpr` treatment. This is something of a workaround for the fact
that the `Format` type is awkward for embedding possibly-linebreaking
expressions in not-linebreaking text, which may be a separate issue
worth addressing.
- Tries to give slightly more "why" reasoning — the environment does not
contain `String.parse`, and _therefore you can't project `.parse` from a
`String`_.

Some specific examples:

### No such projection function
```lean4
#check "".parse
```
before:
```
error: Invalid field `parse`: The environment does not contain `String.parse`
  ""
has type
  String
```
after:
```
error: Invalid field `parse`: The environment does not contain `String.parse`, so it is not possible to project the field `parse` from an expression
  ""
of type `String`
```

### Type does not have the correct form
```lean4
example (x : α) := (foo x).foo
```
before:
```
error: Invalid field notation: Type is not of the form `C ...` where C is a constant
  foo x
has type
  α
```
after:
```
error: Invalid field notation: Field projection operates on types of the form `C ...` where C is a constant. The expression
  foo x
has type `α` which does not have the necessary form.
```

## Refactoring
Includes some refactoring changes as well:
- factors out multiple uses of number (1, 2, 3, 212, 222) to ordinal
("first", "second", "third", "212th", "222nd") conversion into
Lean.Elab.ErrorUtils
- significant refactoring of `resolveLValAux` in `Lean.Elab.App` — in
place of five helper functions, a special-case function case analysis,
and a case analysis on the projection type and structure, there's now a
single case analysis on the projection type and structure. This allows
several error messages to be more explicit (there were a number of cases
where index projection was being described as field projection in an
error messages) and gave the opportunity to slightly improve positining
for several errors: field *notation* errors should appear on `foo.bar`,
but field *projection* errors should appear only on the `bar` part of
`foo.bar`.
2025-12-02 17:46:12 +00:00
Mac Malone
79838834c1 refactor: port shell option processing to Lean (v2) (#11434)
This PR moves the processing of options passed to the CLI from
`shell.cpp` to `Shell.lean`.

As with previous ports, this attempts to mirror as much of the original
behavior as possible, Benefits to be gained from the ported code can
come in later PRs. There should be no significant behavioral changes
from this port. Nonetheless, error reporting has changed some, hopefully
for the better. For instance, errors for improper argument
configurations has been made more consistent (e.g., Lean will now error
if numeric arguments fall outside the expected range for an option).

(Redo of #11345 to fix Windows issue.)
2025-12-02 17:41:51 +00:00
Joachim Breitner
edf804c70f feat: heterogeneous noConfusion (#11474)
This PR generalizes the `noConfusion` constructions to heterogeneous
equalities (assuming propositional equalities between the indices). This
lays ground work for better support for applying injection to
heterogeneous equalities in grind.

The `Meta.mkNoConfusion` app builder shields most of the code from these
changes.

Since the per-constructor noConfusion principles are now more
expressive, `Meta.mkNoConfusion` no longer uses the general one.

In `Init.Prelude` some proofs are more pedestrian because `injection`
now needs a bit more machinery.

This is a breaking change for whoever uses the `noConfusion` principle
manually and explicitly for a type with indices.

Fixes #11450.
2025-12-02 15:19:47 +00:00
Wojciech Różowski
8b7cbe7d2e feat: add mem_of_get_eq and of_getElem_eq (#11452)
This PR adds lemmas stating that if a get operation returns a value,
then the queried key must be contained in the collection. These lemmas
are added for HashMap and TreeMap-based collections, with a similar
lemma also added for `Init.getElem`.
2025-12-02 15:00:00 +00:00
Sebastian Ullrich
a0c503cf2b fix: cadical dynamic dependencies (#11475)
#11423 led to cadical being built with the wrong sysroot flags, which
resulted in it linking against the more recent system glibc
2025-12-02 13:54:26 +00:00
David Thrane Christiansen
0e83422fb6 doc: add missing docstrings for Rxy.Sliceable (#11472)
This PR adds missing docstrings for the `mkSlice` methods.
2025-12-02 08:42:36 +00:00
Henrik Böving
3dd99fc29c perf: eta contract instead of lambda lifting if possible (#11451)
This PR adapts the lambda lifter in LCNF to eta contract instead of
lambda lift if possible. This prevents the creation of a few hundred
unnecessary lambdas across the code base.
2025-12-02 08:39:24 +00:00
Wojciech Różowski
0646bc5979 refactor: move Inhabited instances in constant DTreeMap queries (#11448)
This PR moves the `Inhabited` instances in constant `DTreeMap` (and
related) queries, such as `Const.get!`, where the `Inhabited` instance
can be provided before proving a key.
2025-12-02 08:30:33 +00:00
Kim Morrison
2eca5ca6e4 fix: getEqnsFor? should not panic on matchers (#11463)
This PR fixes a panic in `getEqnsFor?` when called on matchers generated
from match expressions in theorem types.

When a theorem's type contains a match expression (e.g., `theorem bar :
(match ... with ...) = 0`), the compiler generates a matcher like
`bar.match_1`. Calling `getEqnsFor?` on this matcher would panic with:

```
PANIC: duplicate normalized declaration name bar.match_1.eq_1 vs. _private...bar.match_1.eq_1
```

This also affected the `try?` tactic, which internally uses
`getEqnsFor?`.

We make `shouldGenerateEqnThms` return `false` for matchers, since their
equations are already generated separately by
`Lean.Meta.Match.MatchEqs`. This prevents the equation generation
machinery from attempting to create duplicate equation theorems.

Closes #11461
Closes #10390


🤖 Prepared with Claude Code

Co-authored-by: Claude <noreply@anthropic.com>
2025-12-02 07:53:50 +00:00
Leonardo de Moura
1fc4768b68 fix: incorrect reducibility setting in grind interactive mode (#11471)
This PR fixes an incorrect reducibility setting when using `grind`
interactive mode.

Signed-off-by: Leonardo de Moura <leomoura@amazon.com>
2025-12-02 07:04:04 +00:00
Alok Singh
1e1ed16a05 doc: correct typos in documentation and comments (#11465)
This PR fixes various typos across the codebase in documentation and
comments.

- `infered` → `inferred` (ParserCompiler.lean)
- `declartation` → `declaration` (Cleanup.lean)
- `certian` → `certain` (CasesInfo.lean)
- `wil` → `will` (Cache.lean)
- `the the` → `the` (multiple files - PrefixTree.lean, Sum/Basic.lean,
List/Nat/Perm.lean, Time.lean, Bounded.lean, Lake files)
- `to to` → `to` (MutualInductive.lean, simp_bubblesort_256.lean)
- Grammar improvements in Bounded.lean and Time.lean

All changes are to comments and documentation only - no functional
changes.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude <noreply@anthropic.com>
2025-12-02 06:38:05 +00:00
Kim Morrison
226a90f1eb feat: exact? +grind and exact? +try? discharger options (#11469)
This PR adds `+grind` and `+try?` options to `exact?` and `apply?`
tactics.

## `+grind` option

When `+grind` is enabled, `grind` is used as a fallback discharger for
subgoals that `solve_by_elim` cannot close. The proof is wrapped in
`Grind.Marker` so suggestions display `(by grind)` instead of the
complex grind proof term.

Example:
```lean
axiom foo (x : Nat) : x < 37 → 5 < x → x.log2 < 6

/--
info: Try this:
  [apply] exact foo x (by grind) (by grind)
-/
#guard_msgs in
example (x : Nat) (h₁ : x < 30) (h₂ : 8 < x) : x.log2 < 6 := by
  exact? +grind
```

## `+try?` option

When `+try?` is enabled, `try?` is used as a fallback discharger for
subgoals. This is useful when subgoals require induction or other
strategies that `try?` can find but `solve_by_elim` and `grind` cannot.

Example:
```lean
inductive MyList (α : Type _) where
  | nil : MyList α
  | cons : α → MyList α → MyList α

axiom MyListProp : MyList α → Prop
@[grind .] axiom mylist_nil : MyListProp (MyList.nil : MyList α)
@[grind .] axiom mylist_cons : ∀ (x : α) (xs : MyList α), MyListProp xs → MyListProp (MyList.cons x xs)

axiom qux (xs : MyList α) (p : MyListProp xs) : MyListProp2 xs

/--
info: Try this:
  [apply] exact qux xs (by try?)
-/
example (xs : MyList α) : MyListProp2 xs := by
  exact? +try?
```

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude <noreply@anthropic.com>
2025-12-02 06:31:56 +00:00
Kim Morrison
519ccf5d9d feat: add solve_by_elim +suggestions (#11468)
This PR adds `+suggestions` support to `solve_by_elim`, following the
pattern established by `grind +suggestions` and `simp_all +suggestions`.

Gracefully handles invalid/nonexistent suggestions by filtering them out

🤖 Prepared with Claude Code

Co-authored-by: Claude <noreply@anthropic.com>
2025-12-02 02:11:32 +00:00
Kim Morrison
1c1c534a03 feat: add solve_by_elim to try? tactic pipeline (#11462)
This PR adds `solve_by_elim` as a fallback in the `try?` tactic's simple
tactics. When `rfl` and `assumption` both fail but `solve_by_elim`
succeeds (e.g., for goals requiring hypothesis chaining or
backtracking), `try?` will now suggest `solve_by_elim`.

The structure is `first | (attempt_all | rfl | assumption) |
solve_by_elim`, so `solve_by_elim` only runs when the faster tactics
fail.

This is a prerequisite for removing the "first pass" `solve_by_elim`
from `apply?`. Currently `apply?` calls `solve_by_elim` twice: once
before library search, and once after each lemma application. The first
pass can be removed once `try?` includes `solve_by_elim`.

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude <noreply@anthropic.com>
2025-12-02 02:09:59 +00:00
Kim Morrison
8b103f33cf feat: remove solve_by_elim first pass from exact?/apply? (#11466)
This PR removes the "first pass" behavior where `exact?` and `apply?`
would try `solve_by_elim` on the original goal before doing library
search. This simplifies the `librarySearch` API and focuses these
tactics on their primary purpose: finding library lemmas.

Users who want to find proofs using local hypotheses should use `try?`
instead, which now includes `solve_by_elim` in its pipeline (see
https://github.com/leanprover/lean4/pull/11462).

Changes:
- Removed first pass from `librarySearch`
- Simplified `tactic` parameter from `Bool → List MVarId → MetaM (List
MVarId)` to `List MVarId → MetaM (List MVarId)`
- Updated test expectations

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude <noreply@anthropic.com>
2025-12-02 02:05:27 +00:00
Kim Morrison
a0c8404ab8 fix: improve "no library suggestions engine registered" error message (#11464)
This PR improves the error message when no library suggestions engine is
registered to recommend importing `Lean.LibrarySuggestions.Default` for
the built-in engine.

**Before:**
```
No library suggestions engine registered. (Note that Lean does not provide a default library suggestions engine, these must be provided by a downstream library, and configured using `set_library_suggestions`.)
```

**After:**
```
No library suggestions engine registered. (Add `import Lean.LibrarySuggestions.Default` to use Lean's built-in engine, or use `set_library_suggestions` to configure a custom one.)
```

🤖 Prepared with Claude Code

Co-authored-by: Claude <noreply@anthropic.com>
2025-12-02 00:55:46 +00:00
Lean stage0 autoupdater
c0d5b9b52c chore: update stage0 2025-12-01 21:07:38 +00:00
Sebastian Ullrich
96461a4b03 feat: recordIndirectModUse (#11437)
This PR adds recording functionality such that `shake` can more
precisely track whether an import should be preserved solely for its
`attribute` commands.
2025-12-01 20:02:38 +00:00
Henrik Böving
310abce62b fix: boxing may have to correct let binder types (#11426)
This PR closes #11356.
2025-12-01 17:22:32 +00:00
Wojciech Różowski
2da5b528b7 feat: add difference on DTreeMap/TreeMap/TreeSet (#11407)
This PR adds the difference operation on `DTreeMap`/`TreeMap`/`TreeSet`
and proves several lemmas about it.

---------

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
2025-12-01 16:43:34 +00:00
Garmelon
ca23ed0c17 chore: fix "tests/compiler//sum binary sizes" benchmark (#11444)
The bench script expected no output on stdout from `compile.sh`, which
was not always the case. Now, it separates the compilation and size
measurement steps.
2025-12-01 16:20:34 +00:00
Henrik Böving
5e165e358c fix: better types when creating boxed decls (#11445)
This PR slightly improves the types involved in creating boxed
declarations. Previously the type of
the vdecl used for the return was always `tobj` when returning a boxed
scalar. This is not the most
precise annotation we can give.
2025-12-01 15:11:15 +00:00
Robert J. Simmons
429734c02f feat: suggest deriving an instance when the instance might be derivable (#11346)
This PR modifies the error message for type synthesis failure for the
case where the type class in question is potentially derivable using a
`deriving` command. Also changes the error explanation for type class
instance synthesis failure with an illustration of this pattern.

## Example

```lean4
inductive MyColor where
  | chartreuse | sienna | thistle
def forceColor (oc : Option MyColor) :=
  oc.get!
```

Before this PR, this gives the potentially confusing impression that
Lean may have decided that `MyColor` is _not_ inhabited — people used to
Rust may be especially inclined towards this confusion.
```
failed to synthesize instance of type class
  Inhabited MyColor

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
```

After this PR, a targeted hint suggests precisely the command that will
fix the issue:
```
error: failed to synthesize instance of type class
  Inhabited MyColor

Hint: Adding the command `deriving instance Inhabited for MyColor` may allow Lean to derive the missing instance.
```
2025-12-01 14:28:15 +00:00
Lean stage0 autoupdater
35a36ae343 chore: update stage0 2025-12-01 13:35:51 +00:00
Joachim Breitner
f9dc77673b feat: dedicated fix operator for well-founded recursion on Nat (#7965)
This PR lets recursive functions defined by well-founded recursion use a
different `fix` function when the termination measure is of type `Nat`.
This fix-point operator use structural recursion on “fuel”, initialized
by the given measure, and is thus reasonable to reduce, e.g. in `by
decide` proofs.

Extra provisions are in place that the fixpoint operator only starts
reducing when the fuel is fully known, to prevent “accidential” defeqs
when the remaining fuel for the recursive calls match the initial fuel
for that recursive argument.

To opt-out, the idiom `termination_by (n,0)` can be used.

We still use `@[irreducible]` as the default for such recursive
definitions, to avoid unexpected `defeq` lemmas. Making these functions
`@[semireducible]` by default showed performance regressions in lean.
When the measure is of type `Nat`, the system will accept an explicit
`@[semireducible]` without the usual warning.

Fixes #5234. Fixes: #11181.
2025-12-01 12:51:55 +00:00
Markus Himmel
1ae680c5e2 chore: minor String API improvements (#11439)
This PR performs minor maintenance on the String API

- Rename `String.Pos.toCopy` to `String.Pos.copy` to adhere to the
naming convention
- Rename `String.Pos.extract` to `String.extract` to get sane dot
notation again
- Add `String.Slice.Pos.extract`
2025-12-01 11:44:14 +00:00
Lean stage0 autoupdater
057b70b443 chore: update stage0 2025-12-01 11:47:18 +00:00
David Thrane Christiansen
677561522d fix: add missing import (#11441)
This PR fixes an issue that prevented the manual from building due to
the missing explanation of an error.
2025-12-01 11:02:03 +00:00
Marc Huisinga
af5b47295f feat: reduce server memory consumption (#11162)
This PR reduces the memory consumption of the language server (the
watchdog process in particular). In Mathlib, it reduces memory
consumption by about 1GB.

It also fixes two bugs in the call hierarchy:
- When an open file had import errors (e.g. from a transitive build
failure), the call hierarchy would not display any usages in that file.
Now we use the reference information from the .ilean instead.
- When a command would not set a parent declaration (e.g. `#check`), the
result was filtered from the call hierarchy. Now we display it as
`[anonymous]` instead.
2025-12-01 10:53:23 +00:00
Sebastian Ullrich
3282ac6f96 chore: CI: exclude additional slow test (#11440) 2025-12-01 10:53:16 +00:00
Joachim Breitner
5bd331e85d perf: kernel-optimize Mon.mul (#11422)
This PR uses a kernel-reduction optimized variant of Mon.mul in grind.
2025-11-30 23:59:59 +00:00
Jon Eugster
856825a4d2 fix: typo in docstring of #guard_msgs (#11432)
This PR fixes a typo in the docstring of `#guard_mgs`.

Closes #11431
2025-11-30 14:44:35 +00:00
Leonardo de Moura
16508196e0 doc: add docstring for grind_pattern command (#11429)
This PR documents the `grind_pattern` command for manually selecting
theorem instantiation patterns, including multi-patterns and the
constraint system (`=/=`, `=?=`, `size`, `depth`, `is_ground`,
`is_value`, `is_strict_value`, `gen`, `max_insts`, `guard`, `check`).
2025-11-30 01:01:48 +00:00
Sebastian Ullrich
4eba5ea96d fix: shake: only record non-builtin simprocs (#11344) 2025-11-29 15:58:29 +00:00
1205 changed files with 10886 additions and 2358 deletions

View File

@@ -271,7 +271,8 @@ jobs:
// `reverse-ffi` fails to link in sanitizers
// `interactive` and `async_select_channel` fail nondeterministically, would need to
// be investigated.
"CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi|interactive|async_select_channel'"
// 9366 is too close to timeout
"CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi|interactive|async_select_channel|9366'"
},
{
"name": "macOS",

View File

@@ -44,7 +44,9 @@ if (NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
set(CADICAL_CXX c++)
if (CADICAL_USE_CUSTOM_CXX)
set(CADICAL_CXX ${CMAKE_CXX_COMPILER})
set(CADICAL_CXXFLAGS "${LEAN_EXTRA_CXX_FLAGS}")
# Use same platform flags as for Lean executables, in particular from `prepare-llvm-linux.sh`,
# but not Lean-specific `LEAN_EXTRA_CXX_FLAGS` such as fsanitize.
set(CADICAL_CXXFLAGS "${CMAKE_CXX_FLAGS}")
set(CADICAL_LDFLAGS "-Wl,-rpath=\\$$ORIGIN/../lib")
endif()
find_program(CCACHE ccache)

View File

@@ -448,8 +448,8 @@ if(LLVM AND ${STAGE} GREATER 0)
# - In particular, `host/bin/llvm-config` produces flags like `-Lllvm-host/lib/libLLVM`, while
# we need the path to be `-Lllvm/lib/libLLVM`. Thus, we perform this replacement here.
string(REPLACE "llvm-host" "llvm" LEANSHARED_LINKER_FLAGS ${LEANSHARED_LINKER_FLAGS})
string(REPLACE "llvm-host" "llvm" LEAN_EXTRA_CXX_FLAGS ${LEAN_EXTRA_CXX_FLAGS})
message(VERBOSE "leanshared linker flags: '${LEANSHARED_LINKER_FLAGS}' | lean extra cxx flags '${LEAN_EXTR_CXX_FLAGS}'")
string(REPLACE "llvm-host" "llvm" CMAKE_CXX_FLAGS ${CMAKE_CXX_FLAGS})
message(VERBOSE "leanshared linker flags: '${LEANSHARED_LINKER_FLAGS}' | lean extra cxx flags '${CMAKE_CXX_FLAGS}'")
endif()
# get rid of unused parts of C++ stdlib

View File

@@ -73,19 +73,11 @@ private theorem cons_lex_cons [BEq α] {lt : αα → Bool} {a b : α} {xs
(lt a b || a == b && xs.lex ys lt) := by
simp only [lex, size_append, List.size_toArray, List.length_cons, List.length_nil, Nat.zero_add,
Nat.add_min_add_left, Nat.add_lt_add_iff_left, Std.Rco.forIn'_eq_forIn'_toList]
conv =>
lhs; congr; congr
rw [cons_lex_cons.forIn'_congr_aux Std.Rco.toList_eq_if_roo rfl (fun _ _ _ => rfl)]
simp only [bind_pure_comp, map_pure]
rw [cons_lex_cons.forIn'_congr_aux (if_pos (by omega)) rfl (fun _ _ _ => rfl)]
simp only [Std.toList_roo_eq_toList_rco_of_isSome_succ? (lo := 0) (h := rfl),
Std.PRange.UpwardEnumerable.succ?, Nat.add_comm 1, Std.PRange.Nat.toList_rco_succ_succ,
Option.get_some, List.forIn'_cons, List.size_toArray, List.length_cons, List.length_nil,
Nat.lt_add_one, getElem_append_left, List.getElem_toArray, List.getElem_cons_zero]
cases lt a b
· rw [bne]
cases a == b <;> simp
· simp
rw [cons_lex_cons.forIn'_congr_aux (Nat.toList_rco_eq_cons (by omega)) rfl (fun _ _ _ => rfl)]
simp only [bind_pure_comp, map_pure, Nat.toList_rco_succ_succ, Nat.add_comm 1]
cases h : lt a b
· cases h' : a == b <;> simp [bne, *]
· simp [*]
@[simp, grind =] theorem _root_.List.lex_toArray [BEq α] {lt : α α Bool} {l₁ l₂ : List α} :
l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt := by

View File

@@ -278,7 +278,11 @@ set_option bootstrap.genMatcherCode false in
def decNonneg (m : @& Int) : Decidable (NonNeg m) :=
match m with
| ofNat m => isTrue <| NonNeg.mk m
| -[_ +1] => isFalse <| fun h => nomatch h
| -[i +1] => isFalse <| fun h =>
have : j, (j = -[i +1]) NonNeg j False := fun _ hj hnn =>
Int.NonNeg.casesOn (motive := fun j _ => j = -[i +1] False) hnn
(fun _ h => Int.noConfusion h) hj
this -[i +1] rfl h
/-- Decides whether `a ≤ b`.

View File

@@ -60,14 +60,14 @@ theorem set_set_perm {as : List α} {i j : Nat} (h₁ : i < as.length) (h₂ : j
namespace Perm
/-- Variant of `List.Perm.take` specifying the the permutation is constant after `i` elementwise. -/
/-- Variant of `List.Perm.take` specifying that the permutation is constant after `i` elementwise. -/
theorem take_of_getElem? {l₁ l₂ : List α} (h : l₁ ~ l₂) {i : Nat} (w : j, i j l₁[j]? = l₂[j]?) :
l₁.take i ~ l₂.take i := by
refine h.take (Perm.of_eq ?_)
ext1 j
simpa using w (i + j) (by omega)
/-- Variant of `List.Perm.drop` specifying the the permutation is constant before `i` elementwise. -/
/-- Variant of `List.Perm.drop` specifying that the permutation is constant before `i` elementwise. -/
theorem drop_of_getElem? {l₁ l₂ : List α} (h : l₁ ~ l₂) {i : Nat} (w : j, j < i l₁[j]? = l₂[j]?) :
l₁.drop i ~ l₂.drop i := by
refine h.drop (Perm.of_eq ?_)

View File

@@ -37,7 +37,7 @@ open Nat
rw [ length_eq_zero_iff, length_range']
theorem range'_ne_nil_iff (s : Nat) {n step : Nat} : range' s n step [] n 0 := by
cases n <;> simp
simp
theorem range'_eq_cons_iff : range' s n step = a :: xs s = a 0 < n xs = range' (a + step) (n - 1) step := by
induction n generalizing s with

View File

@@ -467,6 +467,23 @@ public theorem Rxo.Iterator.toArray_eq_match [LT α] [DecidableLT α]
· rfl
· split <;> simp
public theorem Rxc.Iterator.toList_eq_toList_rxoIterator [LE α] [DecidableLE α] [LT α] [DecidableLT α]
[UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
[LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α]
[InfinitelyUpwardEnumerable α] [LinearlyUpwardEnumerable α] {it : Iter (α := Rxc.Iterator α) α}:
it.toList = (it.internalState.next, succ it.internalState.upperBound : Iter (α := Rxo.Iterator α) α).toList := by
induction it using Iter.inductSteps with | step it ihy ihs
rw [Rxc.Iterator.toList_eq_match, Rxo.Iterator.toList_eq_match]
split
· simp [*]
· simp only [UpwardEnumerable.le_iff, UpwardEnumerable.lt_iff, *]
split <;> rename_i h
· rw [ihy]; rotate_left
· simp [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
Iterator.Monadic.step, Iter.toIterM, *]; rfl
· simpa [UpwardEnumerable.lt_iff, UpwardEnumerable.le_iff, UpwardEnumerable.lt_succ_iff] using h
· simpa [UpwardEnumerable.lt_iff, UpwardEnumerable.le_iff, UpwardEnumerable.lt_succ_iff] using h
public theorem Rxi.Iterator.toList_eq_match
[UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
{it : Iter (α := Rxi.Iterator α) α} :
@@ -561,22 +578,6 @@ namespace Rcc
variable {r : Rcc α}
public theorem toList_eq_if_roo [UpwardEnumerable α] [LE α] [DecidableLE α]
[LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerableLE α] :
r.toList = if r.lower r.upper then r.lower :: (r.lower<...=r.upper).toList else [] := by
rw [Internal.toList_eq_toList_iter, Rxc.Iterator.toList_eq_match]; rfl
@[deprecated toList_eq_if_roo (since := "2025-10-29")]
def toList_eq_if_Roo := @toList_eq_if_roo
public theorem toArray_eq_if_roo [UpwardEnumerable α] [LE α] [DecidableLE α]
[LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerableLE α] :
r.toArray = if r.lower r.upper then #[r.lower] ++ (r.lower<...=r.upper).toArray else #[] := by
rw [Internal.toArray_eq_toArray_iter, Rxc.Iterator.toArray_eq_match]; rfl
@[deprecated toArray_eq_if_roo (since := "2025-10-29")]
def toArray_eq_if_Roo := @toArray_eq_if_roo
public theorem toList_eq_if_roc [LE α] [DecidableLE α] [UpwardEnumerable α]
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] :
r.toList = if r.lower r.upper then
@@ -585,6 +586,16 @@ public theorem toList_eq_if_roc [LE α] [DecidableLE α] [UpwardEnumerable α]
[] := by
rw [Internal.toList_eq_toList_iter, Rxc.Iterator.toList_eq_match]; rfl
@[simp]
public theorem toList_eq_toList_rco [LE α] [DecidableLE α] [LT α] [DecidableLT α]
[UpwardEnumerable α] [LawfulUpwardEnumerable α]
[LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α]
[Rxc.IsAlwaysFinite α] [Rxo.IsAlwaysFinite α]
[InfinitelyUpwardEnumerable α] [LinearlyUpwardEnumerable α] :
r.toList = (r.lower...(succ r.upper)).toList := by
simp [Internal.toList_eq_toList_iter, Rco.Internal.toList_eq_toList_iter,
Internal.iter, Rco.Internal.iter, Rxc.Iterator.toList_eq_toList_rxoIterator]
@[deprecated toList_eq_if_roc (since := "2025-10-29")]
def toList_eq_match := @toList_eq_if_roc
@@ -816,6 +827,23 @@ public theorem toArray_eq_if_roo [UpwardEnumerable α] [LT α] [DecidableLT α]
#[] := by
rw [Internal.toArray_eq_toArray_iter, Rxo.Iterator.toArray_eq_match]; rfl
public theorem toList_eq_if_rco [UpwardEnumerable α] [LT α] [DecidableLT α]
[LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerableLT α] :
r.toList = if r.lower < r.upper then
match UpwardEnumerable.succ? r.lower with
| none => [r.lower]
| some next => r.lower :: (next...r.upper).toList
else
[] := by
rw [Internal.toList_eq_toList_iter, Rxo.Iterator.toList_eq_match]
simp only [Internal.iter]
split
· split
· simp [Rxo.Iterator.toList_eq_match, *]
· simp only [*]
rfl
· rfl
public theorem toArray_eq_if_rco [UpwardEnumerable α] [LT α] [DecidableLT α]
[LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerableLT α] :
r.toArray = if r.lower < r.upper then
@@ -1272,6 +1300,16 @@ public theorem toArray_eq_match_rcc [LE α] [DecidableLE α] [UpwardEnumerable
simp only [ Internal.toList_eq_toList_iter, toList_eq_match_rcc]
split <;> simp
@[simp]
public theorem toList_eq_toList_roo [LE α] [DecidableLE α] [LT α] [DecidableLT α]
[UpwardEnumerable α] [LawfulUpwardEnumerable α]
[LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α]
[Rxc.IsAlwaysFinite α] [Rxo.IsAlwaysFinite α]
[InfinitelyUpwardEnumerable α] [LinearlyUpwardEnumerable α] :
r.toList = (r.lower<...(succ r.upper)).toList := by
simp [Internal.toList_eq_toList_iter, Roo.Internal.toList_eq_toList_iter,
Internal.iter, Roo.Internal.iter, Rxc.Iterator.toList_eq_toList_rxoIterator]
@[simp]
public theorem toArray_toList [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
[Rxc.IsAlwaysFinite α] :
@@ -2856,7 +2894,7 @@ public theorem length_toList [LE α] [DecidableLE α] [UpwardEnumerable α]
· simpa [toList_eq_nil_iff, size_eq_if_roc] using h
· rename_i n ih
rw [size_eq_if_rcc] at h
simp only [toList_eq_if_roo, h]
simp only [toList_eq_if_roc, h]
simp only [Roc.toList_eq_match_rcc]
split
· split

File diff suppressed because it is too large Load Diff

View File

@@ -318,7 +318,7 @@ This function uses an `UpwardEnumerable α` instance.
If no other implementation is provided in UpwardEnumerable instance, succMany? repeatedly applies succ?.
-/
@[always_inline, inline]
@[always_inline, inline, expose]
def UpwardEnumerable.succMany {α : Type u} [UpwardEnumerable α]
[LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α]
(n : Nat) (a : α) :=

View File

@@ -9,6 +9,7 @@ prelude
public import Init.Data.Range.Polymorphic.PRange
set_option doc.verso true
set_option linter.missingDocs true
public section
@@ -30,6 +31,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
The type of the resulting slices is {lit}`γ`.
-/
class Rcc.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
/--
Slices {name}`carrier` from {lean}`range.lower` to {lean}`range.upper`, both inclusive.
-/
mkSlice (carrier : α) (range : Rcc β) : γ
/--
@@ -39,6 +43,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
The type of resulting the slices is {lit}`γ`.
-/
class Rco.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
/--
Slices {name}`carrier` from {lean}`range.lower` (inclusive) to {lean}`range.upper` (exclusive).
-/
mkSlice (carrier : α) (range : Rco β) : γ
/--
@@ -48,6 +55,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
The type of the resulting slices is {lit}`γ`.
-/
class Rci.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
/--
Slices {name}`carrier` from {lean}`range.lower` (inclusive).
-/
mkSlice (carrier : α) (range : Rci β) : γ
/--
@@ -57,6 +67,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
The type of the resulting slices is {lit}`γ`.
-/
class Roc.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
/--
Slices {name}`carrier` from {lean}`range.lower` (exclusive) to {lean}`range.upper` (inclusive).
-/
mkSlice (carrier : α) (range : Roc β) : γ
/--
@@ -66,6 +79,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
The type of the resulting slices is {lit}`γ`.
-/
class Roo.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
/--
Slices {name}`carrier` from {lean}`range.lower` to {lean}`range.upper`, both exclusive.
-/
mkSlice (carrier : α) (range : Roo β) : γ
/--
@@ -75,6 +91,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
The type of the resulting slices is {lit}`γ`.
-/
class Roi.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
/--
Slices {name}`carrier` from {lean}`range.lower` (exclusive).
-/
mkSlice (carrier : α) (range : Roi β) : γ
/--
@@ -84,6 +103,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
The type of the resulting slices is {lit}`γ`.
-/
class Ric.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
/--
Slices {name}`carrier` up to {lean}`range.upper` (inclusive).
-/
mkSlice (carrier : α) (range : Ric β) : γ
/--
@@ -93,6 +115,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
The type of the resulting slices is {lit}`γ`.
-/
class Rio.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
/--
Slices {name}`carrier` up to {lean}`range.upper` (exclusive).
-/
mkSlice (carrier : α) (range : Rio β) : γ
/--
@@ -102,6 +127,9 @@ index type {lit}`β`.
The type of the resulting slices is {lit}`γ`.
-/
class Rii.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
/--
Slices {name}`carrier` with no bounds.
-/
mkSlice (carrier : α) (range : Rii β) : γ
macro_rules

View File

@@ -824,16 +824,25 @@ The region of `s` from `b` (inclusive) to `e` (exclusive) is copied to a newly-a
If `b`'s offset is greater than or equal to that of `e`, then the resulting string is `""`.
If possible, prefer `String.slice`, which avoids the allocation.
-/
@[extern "lean_string_utf8_extract"]
def Pos.extract {s : @& String} (b e : @& s.Pos) : String where
def extract {s : @& String} (b e : @& s.Pos) : String where
toByteArray := s.toByteArray.extract b.offset.byteIdx e.offset.byteIdx
isValidUTF8 := b.isValidUTF8_extract e
@[deprecated String.extract (since := "2025-12-01")]
def Pos.extract {s : String} (b e : @& s.Pos) : String :=
s.extract b e
@[simp]
theorem toByteArray_extract {s : String} {b e : s.Pos} :
(s.extract b e).toByteArray = s.toByteArray.extract b.offset.byteIdx e.offset.byteIdx := (rfl)
/-- Creates a `String` from a `String.Slice` by copying the bytes. -/
@[inline]
def Slice.copy (s : Slice) : String :=
s.startInclusive.extract s.endExclusive
s.str.extract s.startInclusive s.endExclusive
theorem Slice.toByteArray_copy {s : Slice} :
s.copy.toByteArray = s.str.toByteArray.extract s.startInclusive.offset.byteIdx s.endExclusive.offset.byteIdx := (rfl)
@@ -1387,54 +1396,58 @@ theorem Pos.offset_ofCopy {s : Slice} {pos : s.copy.Pos} : pos.ofCopy.offset = p
/-- Given a slice `s` and a position on `s`, obtain the corresponding position on `s.copy.` -/
@[inline]
def Slice.Pos.toCopy {s : Slice} (pos : s.Pos) : s.copy.Pos where
def Slice.Pos.copy {s : Slice} (pos : s.Pos) : s.copy.Pos where
offset := pos.offset
isValid := Pos.Raw.isValid_copy_iff.2 pos.isValidForSlice
@[simp]
theorem Slice.Pos.offset_toCopy {s : Slice} {pos : s.Pos} : pos.toCopy.offset = pos.offset := (rfl)
@[deprecated Slice.Pos.copy (since := "2025-12-01")]
def Slice.Pos.toCopy {s : Slice} (pos : s.Pos) : s.copy.Pos :=
pos.copy
@[simp]
theorem Slice.Pos.ofCopy_toCopy {s : Slice} {pos : s.Pos} : pos.toCopy.ofCopy = pos :=
theorem Slice.Pos.offset_copy {s : Slice} {pos : s.Pos} : pos.copy.offset = pos.offset := (rfl)
@[simp]
theorem Slice.Pos.ofCopy_copy {s : Slice} {pos : s.Pos} : pos.copy.ofCopy = pos :=
Slice.Pos.ext (by simp)
@[simp]
theorem Pos.toCopy_ofCopy {s : Slice} {pos : s.copy.Pos} : pos.ofCopy.toCopy = pos :=
theorem Pos.copy_ofCopy {s : Slice} {pos : s.copy.Pos} : pos.ofCopy.copy = pos :=
Pos.ext (by simp)
theorem Pos.ofCopy_inj {s : Slice} {pos pos' : s.copy.Pos} : pos.ofCopy = pos'.ofCopy pos = pos' :=
fun h => by simpa using congrArg Slice.Pos.toCopy h, (· rfl)
fun h => by simpa using congrArg Slice.Pos.copy h, (· rfl)
@[simp]
theorem Slice.startPos_copy {s : Slice} : s.copy.startPos = s.startPos.toCopy :=
theorem Slice.startPos_copy {s : Slice} : s.copy.startPos = s.startPos.copy :=
String.Pos.ext (by simp)
@[simp]
theorem Slice.endPos_copy {s : Slice} : s.copy.endPos = s.endPos.toCopy :=
theorem Slice.endPos_copy {s : Slice} : s.copy.endPos = s.endPos.copy :=
String.Pos.ext (by simp)
theorem Slice.Pos.get_toCopy {s : Slice} {pos : s.Pos} (h) :
pos.toCopy.get h = pos.get (by rintro rfl; simp at h) := by
theorem Slice.Pos.get_copy {s : Slice} {pos : s.Pos} (h) :
pos.copy.get h = pos.get (by rintro rfl; simp at h) := by
rw [String.Pos.get, Slice.Pos.get_eq_utf8DecodeChar, Slice.Pos.get_eq_utf8DecodeChar]
simp only [str_toSlice, toByteArray_copy, startInclusive_toSlice, startPos_copy, offset_toCopy,
simp only [str_toSlice, toByteArray_copy, startInclusive_toSlice, startPos_copy, offset_copy,
Slice.offset_startPos, Pos.Raw.byteIdx_zero, Pos.offset_toSlice, Nat.zero_add]
rw [ByteArray.utf8DecodeChar_eq_utf8DecodeChar_extract]
conv => lhs; congr; rw [ByteArray.extract_extract]
conv => rhs; rw [ByteArray.utf8DecodeChar_eq_utf8DecodeChar_extract]
exact ByteArray.utf8DecodeChar_extract_congr _ _ _
theorem Slice.Pos.get_eq_get_toCopy {s : Slice} {pos : s.Pos} {h} :
pos.get h = pos.toCopy.get (ne_of_apply_ne Pos.ofCopy (by simp [h])) :=
(get_toCopy _).symm
theorem Slice.Pos.get_eq_get_copy {s : Slice} {pos : s.Pos} {h} :
pos.get h = pos.copy.get (ne_of_apply_ne Pos.ofCopy (by simp [h])) :=
(get_copy _).symm
theorem Slice.Pos.byte_toCopy {s : Slice} {pos : s.Pos} (h) :
pos.toCopy.byte h = pos.byte (by rintro rfl; simp at h) := by
theorem Slice.Pos.byte_copy {s : Slice} {pos : s.Pos} (h) :
pos.copy.byte h = pos.byte (by rintro rfl; simp at h) := by
rw [String.Pos.byte, Slice.Pos.byte, Slice.Pos.byte]
simp [getUTF8Byte, String.getUTF8Byte, toByteArray_copy, ByteArray.getElem_extract]
theorem Slice.Pos.byte_eq_byte_toCopy {s : Slice} {pos : s.Pos} {h} :
pos.byte h = pos.toCopy.byte (ne_of_apply_ne Pos.ofCopy (by simp [h])) :=
(byte_toCopy _).symm
theorem Slice.Pos.byte_eq_byte_copy {s : Slice} {pos : s.Pos} {h} :
pos.byte h = pos.copy.byte (ne_of_apply_ne Pos.ofCopy (by simp [h])) :=
(byte_copy _).symm
/-- Given a position in `s.sliceFrom p₀`, obtain the corresponding position in `s`. -/
@[inline]
@@ -1521,7 +1534,7 @@ theorem Slice.Pos.copy_eq_append_get {s : Slice} {pos : s.Pos} (h : pos ≠ s.en
t₁ t₂ : String, s.copy = t₁ ++ singleton (pos.get h) ++ t₂ t₁.utf8ByteSize = pos.offset.byteIdx := by
obtain t₂, ht₂ := (s.sliceFrom pos).copy.eq_singleton_append (by simpa [ Pos.ofCopy_inj, ofSliceFrom_inj])
refine (s.sliceTo pos).copy, t₂, ?_, by simp
simp only [Slice.startPos_copy, get_toCopy, get_eq_get_ofSliceFrom, ofSliceFrom_startPos] at ht₂
simp only [Slice.startPos_copy, get_copy, get_eq_get_ofSliceFrom, ofSliceFrom_startPos] at ht₂
rw [append_assoc, ht₂, copy_eq_copy_sliceTo]
theorem Slice.Pos.utf8ByteSize_byte {s : Slice} {pos : s.Pos} {h : pos s.endPos} :
@@ -1751,8 +1764,8 @@ theorem Pos.offset_cast {s t : String} {pos : s.Pos} {h : s = t} :
theorem Pos.cast_rfl {s : String} {pos : s.Pos} : pos.cast rfl = pos :=
Pos.ext (by simp)
theorem Pos.toCopy_toSlice_eq_cast {s : String} (p : s.Pos) :
p.toSlice.toCopy = p.cast copy_toSlice.symm :=
theorem Pos.copy_toSlice_eq_cast {s : String} (p : s.Pos) :
p.toSlice.copy = p.cast copy_toSlice.symm :=
Pos.ext (by simp)
/-- Given a byte position within a string slice, obtains the smallest valid position that is
@@ -2435,6 +2448,35 @@ def Pos.slice! {s : String} (pos : s.Pos) (p₀ p₁ : s.Pos) :
(s.slice! p₀ p₁).Pos :=
Slice.Pos.slice! pos.toSlice _ _
theorem extract_eq_copy_slice {s : String} (p₀ p₁ : s.Pos) (h : p₀ p₁) :
s.extract p₀ p₁ = (s.slice p₀ p₁ h).copy := by
simp [ toByteArray_inj, Slice.toByteArray_copy]
/--
Copies a region of a slice to a new string.
The region of `s` from `b` (inclusive) to `e` (exclusive) is copied to a newly-allocated `String`.
If `b`'s offset is greater than or equal to that of `e`, then the resulting string is `""`.
If possible, prefer `Slice.slice`, which avoids the allocation.
-/
@[inline]
def Slice.extract (s : Slice) (p₀ p₁ : s.Pos) : String :=
s.str.extract p₀.str p₁.str
@[simp]
theorem Slice.Pos.str_le_str_iff {s : Slice} {p q : s.Pos} : p.str q.str p q := by
simp [String.Pos.le_iff, Slice.Pos.le_iff, Pos.Raw.le_iff]
@[simp]
theorem Slice.Pos.str_lt_str_iff {s : Slice} {p q : s.Pos} : p.str < q.str p < q := by
simp [String.Pos.lt_iff, Slice.Pos.lt_iff, Pos.Raw.lt_iff]
theorem Slice.extract_eq_copy_slice {s : Slice} (p₀ p₁ : s.Pos) (h : p₀ p₁) :
s.extract p₀ p₁ = (s.slice p₀ p₁ h).copy := by
simp [ toByteArray_inj, Slice.toByteArray_copy, Slice.extract]
/--
Advances the position `p` `n` times.
@@ -2734,10 +2776,6 @@ where
| [], _, _ => []
| c::cs, i, e => if i = e then [] else c :: go₂ cs (i + c) e
@[extern "lean_string_utf8_extract", expose, deprecated Pos.Raw.extract (since := "2025-10-14")]
def extract : (@& String) (@& Pos.Raw) (@& Pos.Raw) String
| s, b, e => Pos.Raw.extract s b e
def Pos.Raw.offsetOfPosAux (s : String) (pos : Pos.Raw) (i : Pos.Raw) (offset : Nat) : Nat :=
if i >= pos then offset
else if h : i.atEnd s then

View File

@@ -40,7 +40,7 @@ theorem singleton_ne_empty {c : Char} : singleton c ≠ "" := by
simp [singleton]
@[simp]
theorem Slice.Pos.toCopy_inj {s : Slice} {p₁ p₂ : s.Pos} : p₁.toCopy = p₂.toCopy p₁ = p₂ := by
theorem Slice.Pos.copy_inj {s : Slice} {p₁ p₂ : s.Pos} : p₁.copy = p₂.copy p₁ = p₂ := by
simp [String.Pos.ext_iff, Pos.ext_iff]
@[simp]

View File

@@ -56,25 +56,25 @@ theorem Slice.Pos.Splits.cast {s₁ s₂ : Slice} {p : s₁.Pos} {t₁ t₂ : St
p.Splits t₁ t₂ (p.cast h).Splits t₁ t₂ :=
splits_cast_iff.mpr
theorem Slice.Pos.Splits.toCopy {s : Slice} {p : s.Pos} {t₁ t₂ : String}
(h : p.Splits t₁ t₂) : p.toCopy.Splits t₁ t₂ where
theorem Slice.Pos.Splits.copy {s : Slice} {p : s.Pos} {t₁ t₂ : String}
(h : p.Splits t₁ t₂) : p.copy.Splits t₁ t₂ where
eq_append := h.eq_append
offset_eq_rawEndPos := by simpa using h.offset_eq_rawEndPos
theorem Slice.Pos.splits_of_splits_toCopy {s : Slice} {p : s.Pos} {t₁ t₂ : String}
(h : p.toCopy.Splits t₁ t₂) : p.Splits t₁ t₂ where
theorem Slice.Pos.splits_of_splits_copy {s : Slice} {p : s.Pos} {t₁ t₂ : String}
(h : p.copy.Splits t₁ t₂) : p.Splits t₁ t₂ where
eq_append := h.eq_append
offset_eq_rawEndPos := by simpa using h.offset_eq_rawEndPos
@[simp]
theorem Slice.Pos.splits_toCopy_iff {s : Slice} {p : s.Pos} {t₁ t₂ : String} :
p.toCopy.Splits t₁ t₂ p.Splits t₁ t₂ :=
splits_of_splits_toCopy, (·.toCopy)
theorem Slice.Pos.splits_copy_iff {s : Slice} {p : s.Pos} {t₁ t₂ : String} :
p.copy.Splits t₁ t₂ p.Splits t₁ t₂ :=
splits_of_splits_copy, (·.copy)
@[simp]
theorem Pos.splits_toSlice_iff {s : String} {p : s.Pos} {t₁ t₂ : String} :
p.toSlice.Splits t₁ t₂ p.Splits t₁ t₂ := by
rw [ Slice.Pos.splits_toCopy_iff, p.toCopy_toSlice_eq_cast, splits_cast_iff]
rw [ Slice.Pos.splits_copy_iff, p.copy_toSlice_eq_cast, splits_cast_iff]
theorem Pos.Splits.toSlice {s : String} {p : s.Pos} {t₁ t₂ : String}
(h : p.Splits t₁ t₂) : p.toSlice.Splits t₁ t₂ :=
@@ -112,15 +112,15 @@ theorem Pos.Splits.eq {s : String} {p : s.Pos} {t₁ t₂ t₃ t₄}
theorem Slice.Pos.Splits.eq_left {s : Slice} {p : s.Pos} {t₁ t₂ t₃ t₄}
(h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₁ = t₃ :=
(splits_toCopy_iff.2 h₁).eq_left (splits_toCopy_iff.2 h₂)
(splits_copy_iff.2 h₁).eq_left (splits_copy_iff.2 h₂)
theorem Slice.Pos.Splits.eq_right {s : Slice} {p : s.Pos} {t₁ t₂ t₃ t₄}
(h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₂ = t₄ :=
(splits_toCopy_iff.2 h₁).eq_right (splits_toCopy_iff.2 h₂)
(splits_copy_iff.2 h₁).eq_right (splits_copy_iff.2 h₂)
theorem Slice.Pos.Splits.eq {s : Slice} {p : s.Pos} {t₁ t₂ t₃ t₄}
(h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₁ = t₃ t₂ = t₄ :=
(splits_toCopy_iff.2 h₁).eq (splits_toCopy_iff.2 h₂)
(splits_copy_iff.2 h₁).eq (splits_copy_iff.2 h₂)
@[simp]
theorem splits_endPos (s : String) : s.endPos.Splits s "" where
@@ -161,11 +161,11 @@ theorem Slice.splits_endPos (s : Slice) : s.endPos.Splits s.copy "" where
@[simp]
theorem Slice.splits_endPos_iff {s : Slice} :
s.endPos.Splits t₁ t₂ t₁ = s.copy t₂ = "" := by
rw [ Pos.splits_toCopy_iff, endPos_copy, String.splits_endPos_iff]
rw [ Pos.splits_copy_iff, endPos_copy, String.splits_endPos_iff]
theorem Slice.Pos.Splits.eq_endPos_iff {s : Slice} {p : s.Pos} (h : p.Splits t₁ t₂) :
p = s.endPos t₂ = "" := by
rw [ toCopy_inj, endPos_copy, h.toCopy.eq_endPos_iff]
rw [ copy_inj, endPos_copy, h.copy.eq_endPos_iff]
@[simp]
theorem Slice.splits_startPos (s : Slice) : s.startPos.Splits "" s.copy where
@@ -175,11 +175,11 @@ theorem Slice.splits_startPos (s : Slice) : s.startPos.Splits "" s.copy where
@[simp]
theorem Slice.splits_startPos_iff {s : Slice} :
s.startPos.Splits t₁ t₂ t₁ = "" t₂ = s.copy := by
rw [ Pos.splits_toCopy_iff, startPos_copy, String.splits_startPos_iff]
rw [ Pos.splits_copy_iff, startPos_copy, String.splits_startPos_iff]
theorem Slice.Pos.Splits.eq_startPos_iff {s : Slice} {p : s.Pos} (h : p.Splits t₁ t₂) :
p = s.startPos t₁ = "" := by
rw [ toCopy_inj, startPos_copy, h.toCopy.eq_startPos_iff]
rw [ copy_inj, startPos_copy, h.copy.eq_startPos_iff]
theorem Pos.splits_next_right {s : String} (p : s.Pos) (hp : p s.endPos) :
p.Splits (s.sliceTo p).copy (singleton (p.get hp) ++ (s.sliceFrom (p.next hp)).copy) where

View File

@@ -79,9 +79,11 @@ instance : Std.Iterators.Finite (ForwardCharPredSearcher p s) Id :=
instance : Std.Iterators.IteratorLoop (ForwardCharPredSearcher p s) Id Id :=
.defaultImplementation
@[default_instance]
instance {p : Char Bool} : ToForwardSearcher p (ForwardCharPredSearcher p) where
toSearcher := iter p
@[default_instance]
instance {p : Char Bool} : ForwardPattern p := .defaultImplementation
instance {p : Char Prop} [DecidablePred p] : ToForwardSearcher p (ForwardCharPredSearcher p) where
@@ -153,9 +155,11 @@ instance : Std.Iterators.Finite (BackwardCharPredSearcher s) Id :=
instance : Std.Iterators.IteratorLoop (BackwardCharPredSearcher s) Id Id :=
.defaultImplementation
@[default_instance]
instance {p : Char Bool} : ToBackwardSearcher p BackwardCharPredSearcher where
toSearcher := iter p
@[default_instance]
instance {p : Char Bool} : BackwardPattern p := ToBackwardSearcher.defaultImplementation
instance {p : Char Prop} [DecidablePred p] : ToBackwardSearcher p BackwardCharPredSearcher where

View File

@@ -223,13 +223,13 @@ end Pos
namespace Slice.Pos
@[simp]
theorem remainingBytes_toCopy {s : Slice} {p : s.Pos} :
p.toCopy.remainingBytes = p.remainingBytes := by
theorem remainingBytes_copy {s : Slice} {p : s.Pos} :
p.copy.remainingBytes = p.remainingBytes := by
simp [remainingBytes_eq, String.Pos.remainingBytes_eq, Slice.utf8ByteSize_eq]
theorem Splits.remainingBytes_eq {s : Slice} {p : s.Pos} {t₁ t₂} (h : p.Splits t₁ t₂) :
p.remainingBytes = t₂.utf8ByteSize := by
simpa using h.toCopy.remainingBytes_eq
simpa using h.copy.remainingBytes_eq
end Slice.Pos

View File

@@ -13,7 +13,7 @@ public section
/-!
# Disjoint union of types
This file defines basic operations on the the sum type `α ⊕ β`.
This file defines basic operations on the sum type `α ⊕ β`.
`α ⊕ β` is the type made of a copy of `α` and a copy of `β`. It is also called *disjoint union*.

View File

@@ -240,6 +240,9 @@ theorem getElem_of_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx
{c : cont} {i : idx} [Decidable (dom c i)] (h : c[i]? = some e) : Exists fun h : dom c i => c[i] = e :=
getElem?_eq_some_iff.mp h
theorem of_getElem_eq [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
{c : cont} {i : idx} [Decidable (dom c i)] {h} (_ : c[i] = e) : dom c i := h
@[simp] theorem some_getElem_eq_getElem?_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
{c : cont} {i : idx} [Decidable (dom c i)] (h : dom c i):
(some c[i] = c[i]?) True := by

View File

@@ -202,6 +202,15 @@ structure Config where
```
-/
funCC := true
/--
When `true`, use reducible transparency when trying to close goals.
In this setting, only declarations marked with `@[reducible]` are unfolded during
definitional equality tests.
This option does not affect the canonicalizer or how theorem patterns are internalized;
reducible declarations are always unfolded in those contexts.
-/
reducible := true
deriving Inhabited, BEq
/--

View File

@@ -180,6 +180,53 @@ where
else
.mult { x := pw₁.x, k := pw₁.k + pw₂.k } (go fuel m₁ m₂)
noncomputable def Mon.mul_k : Mon Mon Mon :=
Nat.rec
(fun m₁ m₂ => concat m₁ m₂)
(fun _ ih m₁ m₂ =>
Mon.rec (t := m₂)
m₁
(fun pw₂ m₂' _ => Mon.rec (t := m₁)
m₂
(fun pw₁ m₁' _ =>
Bool.rec (t := pw₁.varLt pw₂)
(Bool.rec (t := pw₂.varLt pw₁)
(.mult { x := pw₁.x, k := Nat.add pw₁.k pw₂.k } (ih m₁' m₂'))
(.mult pw₂ (ih (.mult pw₁ m₁') m₂')))
(.mult pw₁ (ih m₁' (.mult pw₂ m₂'))))))
hugeFuel
theorem Mon.mul_k_eq_mul : Mon.mul_k m₁ m₂ = Mon.mul m₁ m₂ := by
unfold mul_k mul
generalize hugeFuel = fuel
fun_induction mul.go
· rfl
· rfl
case case3 m₂ _ =>
cases m₂
· contradiction
· dsimp
case case4 fuel pw₁ m₁ pw₂ m₂ h ih =>
dsimp only
rw [h]
dsimp only
rw [ih]
case case5 fuel pw₁ m₁ pw₂ m₂ h₁ h₂ ih =>
dsimp only
rw [h₁]
dsimp only
rw [h₂]
dsimp only
rw [ih]
case case6 fuel pw₁ m₁ pw₂ m₂ h₁ h₂ ih =>
dsimp only
rw [h₁]
dsimp only
rw [h₂]
dsimp only
rw [ih]
rfl
def Mon.mul_nc (m₁ m₂ : Mon) : Mon :=
match m₁ with
| .unit => m₂
@@ -190,6 +237,28 @@ def Mon.degree : Mon → Nat
| .unit => 0
| .mult pw m => pw.k + degree m
noncomputable def Mon.degree_k : Mon Nat :=
Nat.rec
(fun m => m.degree)
(fun _ ih m =>
Mon.rec (t := m)
0
(fun pw m' _ => Nat.add pw.k (ih m')))
hugeFuel
theorem Mon.degree_k_eq_degree : Mon.degree_k m = Mon.degree m := by
unfold degree_k
generalize hugeFuel = fuel
induction fuel generalizing m with
| zero => rfl
| succ fuel ih =>
conv => rhs; unfold degree
split
· rfl
· dsimp only
rw [ ih]
rfl
def Var.revlex (x y : Var) : Ordering :=
bif x.blt y then .gt
else bif y.blt x then .lt
@@ -270,7 +339,7 @@ noncomputable def Mon.grevlex_k (m₁ m₂ : Mon) : Ordering :=
Bool.rec
(Bool.rec .gt .lt (Nat.blt m₁.degree m₂.degree))
(revlex_k m₁ m₂)
(Nat.beq m₁.degree m₂.degree)
(Nat.beq m₁.degree_k m₂.degree_k)
theorem Mon.revlex_k_eq_revlex (m₁ m₂ : Mon) : m₁.revlex_k m₂ = m₁.revlex m₂ := by
unfold revlex_k revlex
@@ -302,18 +371,18 @@ theorem Mon.grevlex_k_eq_grevlex (m₁ m₂ : Mon) : m₁.grevlex_k m₂ = m₁.
next h =>
have h₁ : Nat.blt m₁.degree m₂.degree = true := by simp [h]
have h₂ : Nat.beq m₁.degree m₂.degree = false := by rw [ Bool.not_eq_true, Nat.beq_eq]; omega
simp [h₁, h₂]
simp [degree_k_eq_degree, h₁, h₂]
next h =>
split
next h' =>
have h₂ : Nat.beq m₁.degree m₂.degree = true := by rw [Nat.beq_eq, h']
simp [h₂]
simp [degree_k_eq_degree, h₂]
next h' =>
have h₁ : Nat.blt m₁.degree m₂.degree = false := by
rw [ Bool.not_eq_true, Nat.blt_eq]; assumption
have h₂ : Nat.beq m₁.degree m₂.degree = false := by
rw [ Bool.not_eq_true, Nat.beq_eq]; assumption
simp [h₁, h₂]
simp [degree_k_eq_degree, h₁, h₂]
inductive Poly where
| num (k : Int)
@@ -481,7 +550,7 @@ noncomputable def Poly.mulMon_k (k : Int) (m : Mon) (p : Poly) : Poly :=
(Bool.rec
(Poly.rec
(fun k' => Bool.rec (.add (Int.mul k k') m (.num 0)) (.num 0) (Int.beq' k' 0))
(fun k' m' _ ih => .add (Int.mul k k') (m.mul m') ih)
(fun k' m' _ ih => .add (Int.mul k k') (m.mul_k m') ih)
p)
(p.mulConst_k k)
(Mon.beq' m .unit))
@@ -511,7 +580,7 @@ noncomputable def Poly.mulMon_k (k : Int) (m : Mon) (p : Poly) : Poly :=
next =>
have h : Int.beq' k 0 = false := by simp [*]
simp [h]
next ih => simp [ ih]
next ih => simp [ ih, Mon.mul_k_eq_mul]
def Poly.mulMon_nc (k : Int) (m : Mon) (p : Poly) : Poly :=
bif k == 0 then

View File

@@ -122,4 +122,15 @@ See comment at `alreadyNorm`
theorem em (p : Prop) : alreadyNorm p alreadyNorm (¬ p) :=
Classical.em p
/--
Marker for grind-solved subproofs in `exact? +grind` suggestions.
When `exact?` uses grind as a discharger, it wraps the proof in this marker
so that the unexpander can replace it with `(by grind)` in the suggestion.
-/
@[inline] def Marker {α : Sort u} (a : α) : α := a
@[app_unexpander Marker]
meta def markerUnexpander : PrettyPrinter.Unexpander := fun _ => do
`(by grind)
end Lean.Grind

View File

@@ -64,10 +64,25 @@ This is intended to be used in the construction of `partial_fixpoint`, and not m
-/
def chain (c : α Prop) : Prop := x y , c x c y x y y x
def is_sup {α : Sort u} [PartialOrder α] (c : α Prop) (s : α) : Prop :=
x, s x ( y, c y y x)
theorem is_sup_unique {α} [PartialOrder α] {c : α Prop} {s₁ s₂ : α}
(h₁ : is_sup c s₁) (h₂ : is_sup c s₂) : s₁ = s₂ := by
apply PartialOrder.rel_antisymm
· apply (h₁ s₂).mpr
intro y hy
apply (h₂ s₂).mp PartialOrder.rel_refl y hy
· apply (h₂ s₁).mpr
intro y hy
apply (h₁ s₁).mp PartialOrder.rel_refl y hy
end PartialOrder
section CCPO
open PartialOrder
/--
A chain-complete partial order (CCPO) is a partial order where every chain has a least upper bound.
@@ -76,67 +91,75 @@ otherwise.
-/
class CCPO (α : Sort u) extends PartialOrder α where
/--
The least upper bound of a chain.
This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used
otherwise.
The least upper bound of chains exists.
-/
csup : (α Prop) α
/--
`csup c` is the least upper bound of the chain `c` when all elements `x` that are at
least as large as `csup c` are at least as large as all elements of `c`, and vice versa.
-/
csup_spec {c : α Prop} (hc : chain c) : csup c x ( y, c y y x)
has_csup {c : α Prop} (hc : chain c) : Exists (is_sup c)
open PartialOrder CCPO
open CCPO
variable {α : Sort u} [CCPO α]
theorem csup_le {c : α Prop} (hchain : chain c) : ( y, c y y x) csup c x :=
(csup_spec hchain).mpr
noncomputable def CCPO.csup {c : α Prop} (hc : chain c) : α :=
Classical.choose (CCPO.has_csup hc)
theorem le_csup {c : α Prop} (hchain : chain c) {y : α} (hy : c y) : y csup c :=
(csup_spec hchain).mp rel_refl y hy
theorem CCPO.csup_spec {c : α Prop} (hc : chain c) : is_sup c (csup hc) :=
@fun x => Classical.choose_spec (CCPO.has_csup hc) x
theorem csup_le {c : α Prop} (hc : chain c) : ( y, c y y x) csup hc x :=
(csup_spec hc x).mpr
theorem le_csup {c : α Prop} (hc : chain c) {y : α} (hy : c y) : y csup hc :=
(csup_spec hc (csup hc)).mp rel_refl y hy
def empty_chain (α) : α Prop := fun _ => False
def chain_empty (α : Sort u) [PartialOrder α] : chain (empty_chain α) := by
intro x y hx hy; contradiction
/--
The bottom element is the least upper bound of the empty chain.
This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
-/
def bot : α := csup (fun _ => False)
noncomputable def bot : α := csup (chain_empty α)
scoped notation "" => bot
theorem bot_le (x : α) : x := by
apply csup_le
· intro x y hx hy; contradiction
· intro x hx; contradiction
intro x y; contradiction
end CCPO
section CompleteLattice
/--
A complete lattice is a partial order where every subset has a least upper bound.
-/
class CompleteLattice (α : Sort u) extends PartialOrder α where
/--
The least upper bound of an arbitrary subset in the complete_lattice.
The least upper bound of an arbitrary subset exists.
-/
sup : (α Prop) α
sup_spec {c : α Prop} : sup c x ( y, c y y x)
has_sup (c : α Prop) : Exists (is_sup c)
open PartialOrder CompleteLattice
variable {α : Sort u} [CompleteLattice α]
theorem sup_le {c : α Prop} : ( y, c y y x) sup c x :=
(sup_spec).mpr
noncomputable def CompleteLattice.sup (c : α Prop) : α :=
Classical.choose (CompleteLattice.has_sup c)
theorem le_sup {c : α Prop} {y : α} (hy : c y) : y sup c :=
sup_spec.mp rel_refl y hy
theorem CompleteLattice.sup_spec (c : α Prop) : is_sup c (sup c) :=
@fun x => Classical.choose_spec (CompleteLattice.has_sup c) x
def inf (c : α Prop) : α := sup ( y, c y · y)
theorem sup_le (c : α Prop) : ( y, c y y x) sup c x :=
Iff.mpr (sup_spec c x)
theorem le_sup (c : α Prop) {y : α} (hy : c y) : y sup c :=
Iff.mp (sup_spec c (sup c)) rel_refl y hy
noncomputable def inf (c : α Prop) : α := sup ( y, c y · y)
theorem inf_spec {c : α Prop} : x inf c ( y, c y x y) where
mp := by
@@ -204,7 +227,7 @@ from this definition, and `P ⊥` is a separate condition of the induction predi
This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
-/
def admissible (P : α Prop) :=
(c : α Prop), chain c ( x, c x P x) P (csup c)
(c : α Prop) (hc : chain c), ( x, c x P x) P (csup hc)
theorem admissible_const_true : admissible (fun (_ : α) => True) :=
fun _ _ _ => trivial
@@ -220,7 +243,7 @@ theorem chain_conj (c P : α → Prop) (hchain : chain c) : chain (fun x => c x
exact hchain x y hcx hcy
theorem csup_conj (c P : α Prop) (hchain : chain c) (h : x, c x y, c y x y P y) :
csup c = csup (fun x => c x P x) := by
csup hchain = csup (chain_conj c P hchain) := by
apply rel_antisymm
· apply csup_le hchain
intro x hcx
@@ -281,12 +304,12 @@ variable {c : α → Prop}
-- Note that monotonicity is not required for the definition of `lfp`
-- but it is required to show that `lfp` is a fixpoint of `f`.
def lfp (f : α α) : α :=
noncomputable def lfp (f : α α) : α :=
inf (fun c => f c c)
set_option linter.unusedVariables false in
-- The following definition takes a witness that a function is monotone
def lfp_monotone (f : α α) (hm : monotone f) : α :=
noncomputable def lfp_monotone (f : α α) (hm : monotone f) : α :=
lfp f
-- Showing that `lfp` is a prefixed point makes use of monotonicity
@@ -355,7 +378,7 @@ This is intended to be used in the construction of `partial_fixpoint`, and not m
-/
inductive iterates (f : α α) : α Prop where
| step : iterates f x iterates f (f x)
| sup {c : α Prop} (hc : chain c) (hi : x, c x iterates f x) : iterates f (csup c)
| sup {c : α Prop} (hc : chain c) (hi : x, c x iterates f x) : iterates f (csup hc)
theorem chain_iterates {f : α α} (hf : monotone f) : chain (iterates f) := by
intro x y hx hy
@@ -367,7 +390,7 @@ theorem chain_iterates {f : αα} (hf : monotone f) : chain (iterates f) :=
· left; apply hf; assumption
· right; apply hf; assumption
case sup c hchain hi ih2 =>
change f x csup c csup c f x
change f x csup hchain csup hchain f x
by_cases h : z, c z f x z
· left
obtain z, hz, hfz := h
@@ -384,7 +407,7 @@ theorem chain_iterates {f : αα} (hf : monotone f) : chain (iterates f) :=
next => contradiction
next => assumption
case sup c hchain hi ih =>
change rel (csup c) y rel y (csup c)
change rel (csup hchain) y rel y (csup hchain)
by_cases h : z, c z rel y z
· right
obtain z, hz, hfz := h
@@ -423,7 +446,7 @@ definition is not very meaningful and it simplifies applying theorems like `fix_
This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
-/
def fix (f : α α) (hmono : monotone f) := csup (iterates f)
noncomputable def fix (f : α α) (hmono : monotone f) := csup (chain_iterates hmono)
/--
The main fixpoint theorem for fixed points of monotone functions in chain-complete partial orders.
@@ -488,49 +511,66 @@ theorem chain_apply [∀ x, PartialOrder (β x)] {c : (∀ x, β x) → Prop} (h
next h => left; apply h x
next h => right; apply h x
def fun_csup [ x, CCPO (β x)] (c : ( x, β x) Prop) (x : α) :=
CCPO.csup (fun y => f, c f f x = y)
noncomputable def fun_csup [ x, CCPO (β x)] (c : ( x, β x) Prop) (hc : chain c) (x : α) :=
CCPO.csup (chain_apply hc x)
def fun_sup [ x, CompleteLattice (β x)] (c : ( x, β x) Prop) (x : α) :=
CompleteLattice.sup (fun y => f, c f f x = y)
theorem fun_csup_is_sup [ x, CCPO (β x)] (c : ( x, β x) Prop) (hc : chain c) :
is_sup c (fun_csup c hc) := by
intro f
constructor
next =>
intro hf g hg x
apply rel_trans _ (hf x); clear hf
apply le_csup (chain_apply hc x)
exact g, hg, rfl
next =>
intro h x
apply csup_le (chain_apply hc x)
intro y z, hz, hyz
subst y
apply h z hz
instance instCCPOPi [ x, CCPO (β x)] : CCPO ( x, β x) where
csup := fun_csup
csup_spec := by
intro f c hc
constructor
next =>
intro hf g hg x
apply rel_trans _ (hf x); clear hf
apply le_csup (chain_apply hc x)
exact g, hg, rfl
next =>
intro h x
apply csup_le (chain_apply hc x)
intro y z, hz, hyz
subst y
apply h z hz
has_csup hc := fun_csup _ hc, fun_csup_is_sup _ hc
theorem fun_csup_eq [ x, CCPO (β x)] (c : ( x, β x) Prop) (hc : chain c) :
fun_csup c hc = CCPO.csup hc := by
apply is_sup_unique (c := c)
· apply fun_csup_is_sup
· apply CCPO.csup_spec
noncomputable def fun_sup [ x, CompleteLattice (β x)] (c : ( x, β x) Prop) (x : α) :=
CompleteLattice.sup (fun y => f, c f f x = y)
theorem fun_sup_is_sup [ x, CompleteLattice (β x)] (c : ( x, β x) Prop) :
is_sup c (fun_sup c) := by
intro f
constructor
case mp =>
intro hf g hg x
apply rel_trans _ (hf x)
apply le_sup
exact g, hg, rfl
case mpr =>
intro h x
apply sup_le
intro y z, hz, hyz
subst y
apply h z hz
instance instCompleteLatticePi [ x, CompleteLattice (β x)] : CompleteLattice ( x, β x) where
sup := fun_sup
sup_spec := by
intro f c
constructor
case mp =>
intro hf g hg x
apply rel_trans _ (hf x)
apply le_sup
exact g, hg, rfl
case mpr =>
intro h x
apply sup_le
intro y z, hz, hyz
subst y
apply h z hz
has_sup c := fun_sup c, fun_sup_is_sup c
theorem fun_sup_eq [ x, CompleteLattice (β x)] (c : ( x, β x) Prop) :
fun_sup c = CompleteLattice.sup c := by
apply is_sup_unique (c := c)
· apply fun_sup_is_sup
· apply CompleteLattice.sup_spec
def admissible_apply [ x, CCPO (β x)] (P : x, β x Prop) (x : α)
(hadm : admissible (P x)) : admissible (fun (f : x, β x) => P x (f x)) := by
intro c hchain h
rw [ fun_csup_eq]
apply hadm _ (chain_apply hchain x)
rintro _ f, hcf, rfl
apply h _ hcf
@@ -622,67 +662,84 @@ theorem PProd.chain.chain_snd [CCPO α] [CCPO β] {c : α ×' β → Prop} (hcha
case inl h => left; exact h.2
case inr h => right; exact h.2
instance instCompleteLatticePProd [CompleteLattice α] [CompleteLattice β] : CompleteLattice (α ×' β) where
sup c := CompleteLattice.sup (PProd.fst c), CompleteLattice.sup (PProd.snd c)
sup_spec := by
intro a, b c
constructor
case mp =>
intro h₁, h₂ a', b' cab
constructor <;> dsimp only at *
· apply rel_trans ?_ h₁
unfold PProd.fst at *
apply le_sup
apply Exists.intro b'
exact cab
. apply rel_trans ?_ h₂
apply le_sup
unfold PProd.snd at *
apply Exists.intro a'
exact cab
case mpr =>
intro h
constructor <;> dsimp only
. apply sup_le
unfold PProd.fst
intro y' ex
apply Exists.elim ex
intro b' hc
apply (h y', b' hc).1
. apply sup_le
unfold PProd.snd
intro b' ex
apply Exists.elim ex
intro y' hc
apply (h y', b' hc).2
noncomputable def prod_csup [CCPO α] [CCPO β] (c : α ×' β Prop) (hchain : chain c) : α ×' β :=
CCPO.csup (PProd.chain.chain_fst hchain), CCPO.csup (PProd.chain.chain_snd hchain)
theorem prod_csup_is_sup [CCPO α] [CCPO β] (c : α ×' β Prop) (hchain : chain c) :
is_sup c (prod_csup c hchain) := by
intro a, b
constructor
next =>
intro h₁, h₂ a', b' cab
constructor <;> dsimp at *
· apply rel_trans ?_ h₁
apply le_csup (PProd.chain.chain_fst hchain)
exact b', cab
· apply rel_trans ?_ h₂
apply le_csup (PProd.chain.chain_snd hchain)
exact a', cab
next =>
intro h
constructor <;> dsimp
· apply csup_le (PProd.chain.chain_fst hchain)
intro a' b', hcab
apply (h _ hcab).1
· apply csup_le (PProd.chain.chain_snd hchain)
intro b' a', hcab
apply (h _ hcab).2
instance instCCPOPProd [CCPO α] [CCPO β] : CCPO (α ×' β) where
csup c := CCPO.csup (PProd.chain.fst c), CCPO.csup (PProd.chain.snd c)
csup_spec := by
intro a, b c hchain
constructor
next =>
intro h₁, h₂ a', b' cab
constructor <;> dsimp at *
· apply rel_trans ?_ h₁
apply le_csup (PProd.chain.chain_fst hchain)
exact b', cab
· apply rel_trans ?_ h₂
apply le_csup (PProd.chain.chain_snd hchain)
exact a', cab
next =>
intro h
constructor <;> dsimp
· apply csup_le (PProd.chain.chain_fst hchain)
intro a' b', hcab
apply (h _ hcab).1
· apply csup_le (PProd.chain.chain_snd hchain)
intro b' a', hcab
apply (h _ hcab).2
has_csup hchain := prod_csup _ hchain, prod_csup_is_sup _ hchain
theorem prod_csup_eq [CCPO α] [CCPO β] (c : α ×' β Prop) (hchain : chain c) :
prod_csup c hchain = CCPO.csup hchain := by
apply is_sup_unique (c := c)
· apply prod_csup_is_sup
· apply CCPO.csup_spec
noncomputable def prod_sup [CompleteLattice α] [CompleteLattice β] (c : α ×' β Prop) : α ×' β :=
CompleteLattice.sup (PProd.fst c), CompleteLattice.sup (PProd.snd c)
theorem prod_sup_is_sup [CompleteLattice α] [CompleteLattice β] (c : α ×' β Prop) :
is_sup c (prod_sup c) := by
intro a, b
constructor
case mp =>
intro h₁, h₂ a', b' cab
constructor <;> dsimp only at *
· apply rel_trans ?_ h₁
unfold prod_sup PProd.fst at *
apply le_sup
apply Exists.intro b'
exact cab
. apply rel_trans ?_ h₂
apply le_sup
unfold PProd.snd at *
apply Exists.intro a'
exact cab
case mpr =>
intro h
constructor <;> dsimp only
. apply sup_le
unfold PProd.fst
intro y' ex
apply Exists.elim ex
intro b' hc
apply (h y', b' hc).1
. apply sup_le
unfold PProd.snd
intro b' ex
apply Exists.elim ex
intro y' hc
apply (h y', b' hc).2
instance instCompleteLatticePProd [CompleteLattice α] [CompleteLattice β] : CompleteLattice (α ×' β) where
has_sup c := prod_sup c, prod_sup_is_sup c
theorem admissible_pprod_fst {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (P : α Prop)
(hadm : admissible P) : admissible (fun (x : α ×' β) => P x.1) := by
intro c hchain h
rw [<- prod_csup_eq]
apply hadm _ (PProd.chain.chain_fst hchain)
intro x y, hxy
apply h x,y hxy
@@ -690,6 +747,7 @@ theorem admissible_pprod_fst {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (P
theorem admissible_pprod_snd {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (P : β Prop)
(hadm : admissible P) : admissible (fun (x : α ×' β) => P x.2) := by
intro c hchain h
rw [<- prod_csup_eq]
apply hadm _ (PProd.chain.chain_snd hchain)
intro y x, hxy
apply h x,y hxy
@@ -736,49 +794,57 @@ noncomputable def flat_csup (c : FlatOrder b → Prop) : FlatOrder b := by
· exact Classical.choose h
· exact b
noncomputable instance FlatOrder.instCCPO : CCPO (FlatOrder b) where
csup := flat_csup
csup_spec := by
intro x c hc
unfold flat_csup
split
next hex =>
apply Classical.some_spec₂ (q := (· x ( y, c y y x)))
clear hex
intro z hz, hnb
constructor
· intro h y hy
apply PartialOrder.rel_trans _ h; clear h
cases hc y z hy hz
next => assumption
next h =>
cases h
· contradiction
· constructor
· intro h
cases h z hz
theorem flat_csup_is_sup (c : FlatOrder b Prop) (hc : chain c) :
is_sup c (flat_csup c) := by
intro x
unfold flat_csup
split
next hex =>
apply Classical.some_spec₂ (q := (· x ( y, c y y x)))
clear hex
intro z hz, hnb
constructor
· intro h y hy
apply PartialOrder.rel_trans _ h; clear h
cases hc y z hy hz
next => assumption
next h =>
cases h
· contradiction
· constructor
next hnotex =>
constructor
· intro h y hy; clear h
suffices y = b by rw [this]; exact rel.bot
rw [not_exists] at hnotex
specialize hnotex y
rw [not_and] at hnotex
specialize hnotex hy
rw [@Classical.not_not] at hnotex
assumption
· intro; exact rel.bot
· intro h
cases h z hz
· contradiction
· constructor
next hnotex =>
constructor
· intro h y hy; clear h
suffices y = b by rw [this]; exact FlatOrder.rel.bot
rw [not_exists] at hnotex
specialize hnotex y
rw [not_and] at hnotex
specialize hnotex hy
rw [@Classical.not_not] at hnotex
assumption
· intro; exact FlatOrder.rel.bot
instance FlatOrder.instCCPO : CCPO (FlatOrder b) where
has_csup hchain := flat_csup _ , flat_csup_is_sup _ hchain
theorem flat_csup_eq (c : FlatOrder b Prop) (hchain : chain c) :
flat_csup c = CCPO.csup hchain := by
apply is_sup_unique (c := c)
· apply flat_csup_is_sup _ hchain
· apply CCPO.csup_spec
theorem admissible_flatOrder (P : FlatOrder b Prop) (hnot : P b) : admissible P := by
intro c hchain h
by_cases h' : (x : FlatOrder b), c x x b
· simp [CCPO.csup, flat_csup, h']
· simp [ flat_csup_eq, flat_csup, h']
apply Classical.some_spec₂ (q := (P ·))
intro x hcx, hneb
apply h x hcx
· simp [CCPO.csup, flat_csup, h', hnot]
· simp [ flat_csup_eq, flat_csup, h', hnot]
end flat_order
@@ -809,8 +875,8 @@ theorem monotone_bind
· apply MonoBind.bind_mono_right (fun y => monotone_apply y _ hmono₂ _ _ hx₁₂)
instance : PartialOrder (Option α) := inferInstanceAs (PartialOrder (FlatOrder none))
noncomputable instance : CCPO (Option α) := inferInstanceAs (CCPO (FlatOrder none))
noncomputable instance : MonoBind Option where
instance : CCPO (Option α) := inferInstanceAs (CCPO (FlatOrder none))
instance : MonoBind Option where
bind_mono_left h := by
cases h
· exact FlatOrder.rel.bot
@@ -921,12 +987,22 @@ theorem monotone_stateTRun [PartialOrder γ]
monotone (fun (x : γ) => StateT.run (f x) s) :=
monotone_apply s _ hmono
-- TODO: axiomatize these instances (ideally without `Nonempty ε`) when EIO and friends are opaque
noncomputable def EST.bot [Nonempty ε] : EST ε σ α :=
fun s => .error Classical.ofNonempty (Classical.choice s)
noncomputable instance [Nonempty ε] : CCPO (EST ε σ α) :=
inferInstanceAs (CCPO ((s : _) FlatOrder (.error Classical.ofNonempty (Classical.choice s))))
-- Essentially
-- instance [Nonempty ε] : CCPO (EST ε σ α) :=
-- inferInstanceAs (CCPO ((s : _) → FlatOrder (EST.bot s)))
-- but hat would incur a noncomputable on the instance
noncomputable instance [Nonempty ε] : MonoBind (EST ε σ) where
instance [Nonempty ε] : CCPO (EST ε σ α) where
rel := PartialOrder.rel (α := s, FlatOrder (EST.bot s))
rel_refl := PartialOrder.rel_refl
rel_antisymm := PartialOrder.rel_antisymm
rel_trans := PartialOrder.rel_trans
has_csup hchain := CCPO.has_csup (α := s, FlatOrder (EST.bot s)) hchain
instance [Nonempty ε] : MonoBind (EST ε σ) where
bind_mono_left {_ _ a₁ a₂ f} h₁₂ := by
intro s
specialize h₁₂ s
@@ -944,18 +1020,18 @@ noncomputable instance [Nonempty ε] : MonoBind (EST ε σ) where
· apply h₁₂
· exact .refl
noncomputable instance [Nonempty α] : CCPO (ST σ α) :=
inferInstanceAs (CCPO ((s : _) FlatOrder (.mk Classical.ofNonempty (Classical.choice s))))
noncomputable instance [Nonempty α] : CCPO (BaseIO α) :=
inferInstanceAs (CCPO (ST IO.RealWorld α))
noncomputable instance [Nonempty ε] : CCPO (EIO ε α) :=
instance [Nonempty ε] : CCPO (EIO ε α) :=
inferInstanceAs (CCPO (EST ε IO.RealWorld α))
noncomputable instance [Nonempty ε] : MonoBind (EIO ε) :=
instance [Nonempty ε] : MonoBind (EIO ε) :=
inferInstanceAs (MonoBind (EST ε IO.RealWorld))
instance : CCPO (IO α) :=
inferInstanceAs (CCPO (EIO IO.Error α))
instance : MonoBind IO :=
inferInstanceAs (MonoBind (EIO IO.Error))
end mono_bind
section implication_order
@@ -970,9 +1046,9 @@ instance ImplicationOrder.instOrder : PartialOrder ImplicationOrder where
-- This defines a complete lattice on `Prop`, used to define inductive predicates
instance ImplicationOrder.instCompleteLattice : CompleteLattice ImplicationOrder where
sup c := p, c p p
sup_spec := by
intro x c
has_sup c := by
exists p, c p p
intro x
constructor
case mp =>
intro h y cy hy
@@ -1032,9 +1108,9 @@ instance ReverseImplicationOrder.instOrder : PartialOrder ReverseImplicationOrde
-- This defines a complete lattice on `Prop`, used to define coinductive predicates
instance ReverseImplicationOrder.instCompleteLattice : CompleteLattice ReverseImplicationOrder where
sup c := p, c p p
sup_spec := by
intro x c
has_sup c := by
exists p, c p p
intro x
constructor
case mp =>
intro h y cy l

View File

@@ -633,6 +633,20 @@ existing code. It may be removed in a future version of the library.
syntax (name := deprecated) "deprecated" (ppSpace ident)? (ppSpace str)?
(" (" &"since" " := " str ")")? : attr
/--
The attribute `@[suggest_for]` on a declaration suggests likely ways in which
someone might **incorrectly** refer to a definition.
* `@[suggest_for String.endPos]` on the definition of `String.rawEndPos` suggests that `"str".endPos` might be correctable to `"str".rawEndPos`.
* `@[suggest_for Either Result]` on the definition of `Except` suggests that `Either Nat String` might be correctable to `Except Nat String`.
The namespace of the suggestions is always relative to the root namespace. In the namespace `X.Y`,
adding an annotation `@[suggest_for Z.bar]` to `def Z.foo` will suggest `X.Y.Z.foo` only as a
replacement for `Z.foo`. If your intent is to suggest `X.Y.Z.foo` as a replacement for
`X.Y.Z.bar`, you must instead use the annotation `@[suggest_for X.Y.Z.bar]`.
-/
syntax (name := suggest_for) "suggest_for" (ppSpace ident)+ : attr
/--
The `@[coe]` attribute on a function (which should also appear in a
`instance : Coe A B := ⟨myFn⟩` declaration) allows the delaborator to show
@@ -842,7 +856,7 @@ Position reporting:
`#guard_msgs` appears.
- `positions := false` does not report position info.
For example, `#guard_msgs (error, drop all) in cmd` means to check warnings and drop
For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop
everything else.
The command elaborator has special support for `#guard_msgs` for linting.

View File

@@ -1837,6 +1837,8 @@ def Nat.ble : @& Nat → @& Nat → Bool
| succ _, zero => false
| succ n, succ m => ble n m
attribute [gen_constructor_elims] Bool
/--
Non-strict, or weak, inequality of natural numbers, usually accessed via the `≤` operator.
-/
@@ -1860,9 +1862,14 @@ protected def Nat.lt (n m : Nat) : Prop :=
instance instLTNat : LT Nat where
lt := Nat.lt
theorem Nat.not_succ_le_zero : (n : Nat), LE.le (succ n) 0 False
| 0 => nofun
| succ _ => nofun
theorem Nat.not_succ_le_zero (n : Nat) : LE.le (succ n) 0 False :=
-- No injectivity tactic until `attribute [gen_constructor_elims] Nat`
have : m, Eq m 0 LE.le (succ n) m False := fun _ hm hle =>
Nat.le.casesOn (motive := fun m _ => Eq m 0 False) hle
(fun h => Nat.noConfusion h)
(fun _ h => Nat.noConfusion h)
hm
this 0 rfl
theorem Nat.not_lt_zero (n : Nat) : Not (LT.lt n 0) :=
not_succ_le_zero n
@@ -1999,10 +2006,12 @@ protected theorem Nat.lt_of_not_le {a b : Nat} (h : Not (LE.le a b)) : LT.lt b a
protected theorem Nat.add_pos_right :
{b : Nat} (a : Nat) (hb : LT.lt 0 b) LT.lt 0 (HAdd.hAdd a b)
| zero, _, h => (Nat.not_succ_le_zero _ h).elim
| succ _, _, _ => Nat.zero_lt_succ _
protected theorem Nat.mul_pos :
{n m : Nat} (hn : LT.lt 0 n) (hm : LT.lt 0 m) LT.lt 0 (HMul.hMul n m)
| _, zero, _, hb => (Nat.not_succ_le_zero _ hb).elim
| _, succ _, ha, _ => Nat.add_pos_right _ ha
protected theorem Nat.pow_pos {a : Nat} : {n : Nat} (h : LT.lt 0 a) LT.lt 0 (HPow.hPow a n)
@@ -2059,6 +2068,8 @@ protected def Nat.sub : (@& Nat) → (@& Nat) → Nat
| a, 0 => a
| a, succ b => pred (Nat.sub a b)
attribute [gen_constructor_elims] Nat
instance instSubNat : Sub Nat where
sub := Nat.sub
@@ -2216,9 +2227,6 @@ theorem Nat.mod_lt : (x : Nat) → {y : Nat} → (hy : LT.lt 0 y) → LT.lt (HM
| .isTrue _ => Nat.modCore_lt hm
| .isFalse h => Nat.lt_of_not_le h
attribute [gen_constructor_elims] Nat
attribute [gen_constructor_elims] Bool
/--
Gets the word size of the current platform. The word size may be 64 or 32 bits.

View File

@@ -1690,6 +1690,17 @@ a lemma from the list until it gets stuck.
syntax (name := applyRules) "apply_rules" optConfig (&" only")? (args)? (using_)? : tactic
end SolveByElim
/--
Configuration for the `exact?` and `apply?` tactics.
-/
structure LibrarySearchConfig where
/-- If true, use `grind` as a discharger for subgoals that cannot be closed
by `solve_by_elim` alone. -/
grind : Bool := false
/-- If true, use `try?` as a discharger for subgoals that cannot be closed
by `solve_by_elim` alone. -/
try? : Bool := false
/--
Searches environment for definitions or theorems that can solve the goal using `exact`
with conditions resolved by `solve_by_elim`.
@@ -1697,8 +1708,11 @@ with conditions resolved by `solve_by_elim`.
The optional `using` clause provides identifiers in the local context that must be
used by `exact?` when closing the goal. This is most useful if there are multiple
ways to resolve the goal, and one wants to guide which lemma is used.
Use `+grind` to enable `grind` as a fallback discharger for subgoals.
Use `+try?` to enable `try?` as a fallback discharger for subgoals.
-/
syntax (name := exact?) "exact?" (" using " (colGt ident),+)? : tactic
syntax (name := exact?) "exact?" optConfig (" using " (colGt ident),+)? : tactic
/--
Searches environment for definitions or theorems that can refine the goal using `apply`
@@ -1706,8 +1720,11 @@ with conditions resolved when possible with `solve_by_elim`.
The optional `using` clause provides identifiers in the local context that must be
used when closing the goal.
Use `+grind` to enable `grind` as a fallback discharger for subgoals.
Use `+try?` to enable `try?` as a fallback discharger for subgoals.
-/
syntax (name := apply?) "apply?" (" using " (colGt term),+)? : tactic
syntax (name := apply?) "apply?" optConfig (" using " (colGt term),+)? : tactic
/--
Syntax for excluding some names, e.g. `[-my_lemma, -my_theorem]`.

View File

@@ -82,3 +82,18 @@ macro "∎" : tactic => `(tactic| try?)
/-- `∎` (typed as `\qed`) is a macro that expands to `by try? (wrapWithBy := true)` in term mode.
The `wrapWithBy` config option causes suggestions to be prefixed with `by`. -/
macro "" : term => `(by try? (wrapWithBy := true))
namespace Lean.Try
/--
Marker for try?-solved subproofs in `exact? +try?` suggestions.
When `exact?` uses try? as a discharger, it wraps the proof in this marker
so that the unexpander can replace it with `(by try?)` in the suggestion.
-/
@[inline] def Marker {α : Sort u} (a : α) : α := a
@[app_unexpander Marker]
meta def markerUnexpander : PrettyPrinter.Unexpander := fun _ => do
`(by try?)
end Lean.Try

View File

@@ -439,6 +439,53 @@ end
end PSigma
namespace WellFounded
variable {α : Sort u}
variable {motive : α Sort v}
variable (h : α Nat)
variable (F : (x : α) ((y : α) InvImage (· < ·) h y x motive y) motive x)
/-- Helper gadget that prevents reduction of `Nat.eager n` unless `n` evalutes to a ground term. -/
def Nat.eager (n : Nat) : Nat :=
if Nat.beq n n = true then n else n
theorem Nat.eager_eq (n : Nat) : Nat.eager n = n := ite_self n
/--
A well-founded fixpoint operator specialized for `Nat`-valued measures. Given a measure `h`, it expects
its higher order function argument `F` to invoke its argument only on values `y` that are smaller
than `x` with regard to `h`.
In contrast to to `WellFounded.fix`, this fixpoint operator reduces on closed terms. (More precisely:
when `h x` evalutes to a ground value)
-/
def Nat.fix : (x : α) motive x :=
let rec go : (fuel : Nat) (x : α), (h x < fuel) motive x :=
Nat.rec
(fun _ hfuel => (Nat.not_succ_le_zero _ hfuel).elim)
(fun _ ih x hfuel => F x (fun y hy => ih y (Nat.lt_of_lt_of_le hy (Nat.le_of_lt_add_one hfuel))))
fun x => go (Nat.eager (h x + 1)) x (Nat.eager_eq _ Nat.lt_add_one _)
protected theorem Nat.fix.go_congr (x : α) (fuel₁ fuel₂ : Nat) (h₁ : h x < fuel₁) (h₂ : h x < fuel₂) :
Nat.fix.go h F fuel₁ x h₁ = Nat.fix.go h F fuel₂ x h₂ := by
induction fuel₁ generalizing x fuel₂ with
| zero => contradiction
| succ fuel₁ ih =>
cases fuel₂ with
| zero => contradiction
| succ fuel₂ =>
exact congrArg (F x) (funext fun y => funext fun hy => ih y fuel₂ _ _ )
theorem Nat.fix_eq (x : α) :
Nat.fix h F x = F x (fun y _ => Nat.fix h F y) := by
unfold Nat.fix
simp [Nat.eager_eq]
exact congrArg (F x) (funext fun _ => funext fun _ => Nat.fix.go_congr ..)
end WellFounded
/--
The `wfParam` gadget is used internally during the construction of recursive functions by
wellfounded recursion, to keep track of the parameter for which the automatic introduction

View File

@@ -53,7 +53,7 @@ def mkBoxedVersionAux (decl : Decl) : N Decl := do
pure <| reshape newVDecls (.ret (.var r))
else
let newR N.mkFresh
let newVDecls := newVDecls.push (.vdecl newR .tobject (.box decl.resultType r) default)
let newVDecls := newVDecls.push (.vdecl newR decl.resultType.boxed (.box decl.resultType r) default)
pure <| reshape newVDecls (.ret (.var newR))
return Decl.fdecl (mkBoxedName decl.name) qs decl.resultType.boxed body decl.getInfo
@@ -267,8 +267,29 @@ def visitVDeclExpr (x : VarId) (ty : IRType) (e : Expr) (b : FnBody) : M FnBody
| _ =>
return .vdecl x ty e b
/--
Up to this point the type system of IR is quite loose so we can for example encounter situations
such as
```
let y : obj := f x
```
where `f : obj -> uint8`. It is the job of the boxing pass to enforce a stricter obj/scalar
separation and as such it needs to correct situations like this.
-/
def tryCorrectVDeclType (ty : IRType) (e : Expr) : M IRType :=
match e with
| .fap f _ => do
let decl getDecl f
return decl.resultType
| .pap .. => return .object
| .uproj .. => return .usize
| .ctor .. | .reuse .. | .ap .. | .lit .. | .sproj .. | .proj .. | .reset .. =>
return ty
| .unbox .. | .box .. | .isShared .. => unreachable!
partial def visitFnBody : FnBody M FnBody
| .vdecl x t v b => do
let t tryCorrectVDeclType t v
let b withVDecl x t v (visitFnBody b)
visitVDeclExpr x t v b
| .jdecl j xs v b => do

View File

@@ -37,6 +37,7 @@ private def isValidMacroInline (declName : Name) : CoreM Bool := do
let isRec (declName' : Name) : Bool :=
isBRecOnRecursor env declName' ||
declName' == ``WellFounded.fix ||
declName' == ``WellFounded.Nat.fix ||
declName' == declName ++ `_unary -- Auxiliary declaration created by `WF` module
if Option.isSome <| info.value.find? fun e => e.isConst && isRec e.constName! then
-- It contains a `brecOn` or `WellFounded.fix` application. So, it should be recursvie

View File

@@ -40,6 +40,10 @@ structure Context where
We use this feature to implement `@[inline] instance ...` and `@[always_inline] instance ...`
-/
minSize : Nat := 0
/--
Allow for eta contraction instead of lifting to a lambda if possible.
-/
allowEtaContraction : Bool := true
/-- State for the `LiftM` monad. -/
@@ -81,6 +85,13 @@ partial def mkAuxDeclName : LiftM Name := do
if ( getDecl? nameNew).isNone then return nameNew
mkAuxDeclName
def replaceFunDecl (decl : FunDecl) (value : LetValue) : LiftM LetDecl := do
/- We reuse `decl`s `fvarId` to avoid substitution -/
let declNew := { fvarId := decl.fvarId, binderName := decl.binderName, type := decl.type, value }
modifyLCtx fun lctx => lctx.addLetDecl declNew
eraseFunDecl decl
return declNew
open Internalize in
/--
Create a new auxiliary declaration. The array `closure` contains all free variables
@@ -100,11 +111,7 @@ def mkAuxDecl (closure : Array Param) (decl : FunDecl) : LiftM LetDecl := do
auxDecl.erase
pure declName
let value := .const auxDeclName us (closure.map (.fvar ·.fvarId))
/- We reuse `decl`s `fvarId` to avoid substitution -/
let declNew := { fvarId := decl.fvarId, binderName := decl.binderName, type := decl.type, value }
modifyLCtx fun lctx => lctx.addLetDecl declNew
eraseFunDecl decl
return declNew
replaceFunDecl decl value
where
go (nameNew : Name) (safe : Bool) (inlineAttr? : Option InlineAttributeKind) : InternalizeM Decl := do
let params := ( closure.mapM internalizeParam) ++ ( decl.params.mapM internalizeParam)
@@ -115,6 +122,20 @@ where
let decl := { name := nameNew, levelParams := [], params, type, value, safe, inlineAttr?, recursive := false : Decl }
return decl.setLevelParams
def etaContractibleDecl? (decl : FunDecl) : LiftM (Option LetDecl) := do
if !( read).allowEtaContraction then return none
let .let { fvarId := letVar, value := .const declName us args, .. } (.return retVar) := decl.value
| return none
if letVar != retVar then return none
if args.size != decl.params.size then return none
if ( getDecl? declName).isNone then return none
for arg in args, param in decl.params do
let .fvar argVar := arg | return none
if argVar != param.fvarId then return none
let value := .const declName us #[]
replaceFunDecl decl value
mutual
partial def visitFunDecl (funDecl : FunDecl) : LiftM FunDecl := do
let value withParams funDecl.params <| visitCode funDecl.value
@@ -128,9 +149,13 @@ mutual
| .fun decl k =>
let decl visitFunDecl decl
if ( shouldLift decl) then
let scope getScope
let (_, params, _) Closure.run (inScope := scope.contains) <| Closure.collectFunDecl decl
let declNew mkAuxDecl params decl
let declNew do
if let some letDecl etaContractibleDecl? decl then
pure letDecl
else
let scope getScope
let (_, params, _) Closure.run (inScope := scope.contains) <| Closure.collectFunDecl decl
mkAuxDecl params decl
let k withFVar declNew.fvarId <| visitCode k
return .let declNew k
else
@@ -155,8 +180,17 @@ def main (decl : Decl) : LiftM Decl := do
end LambdaLifting
partial def Decl.lambdaLifting (decl : Decl) (liftInstParamOnly : Bool) (suffix : Name) (inheritInlineAttrs := false) (minSize := 0) : CompilerM (Array Decl) := do
let (decl, s) LambdaLifting.main decl |>.run { mainDecl := decl, liftInstParamOnly, suffix, inheritInlineAttrs, minSize } |>.run {} |>.run {}
partial def Decl.lambdaLifting (decl : Decl) (liftInstParamOnly : Bool) (allowEtaContraction : Bool)
(suffix : Name) (inheritInlineAttrs := false) (minSize := 0) : CompilerM (Array Decl) := do
let ctx := {
mainDecl := decl,
liftInstParamOnly,
suffix,
inheritInlineAttrs,
minSize,
allowEtaContraction
}
let (decl, s) LambdaLifting.main decl |>.run ctx |>.run {} |>.run {}
return s.decls.push decl
/--
@@ -166,7 +200,8 @@ def lambdaLifting : Pass where
phase := .mono
name := `lambdaLifting
run := fun decls => do
decls.foldlM (init := #[]) fun decls decl => return decls ++ ( decl.lambdaLifting false (suffix := `_lam))
decls.foldlM (init := #[]) fun decls decl =>
return decls ++ ( decl.lambdaLifting false true (suffix := `_lam))
/--
During eager lambda lifting, we inspect declarations that are not inlineable or instances (doing it
@@ -182,7 +217,7 @@ def eagerLambdaLifting : Pass where
if decl.inlineable || ( Meta.isInstance decl.name) then
return decls.push decl
else
return decls ++ ( decl.lambdaLifting (liftInstParamOnly := true) (suffix := `_elam))
return decls ++ ( decl.lambdaLifting (liftInstParamOnly := true) (allowEtaContraction := false) (suffix := `_elam))
builtin_initialize
registerTraceClass `Compiler.eagerLambdaLifting (inherited := true)

View File

@@ -666,11 +666,11 @@ where
let .const declName _ := e.getAppFn | unreachable!
let typeName := declName.getPrefix
let .inductInfo inductVal getConstInfo typeName | unreachable!
let arity := inductVal.numParams + inductVal.numIndices + 1 /- motive -/ + 2 /- lhs/rhs-/ + 1 /- equality -/
let arity := inductVal.numParams + 1 /- motive -/ + 3*(inductVal.numIndices + 1) /- lhs/rhs and equalities -/
etaIfUnderApplied e arity do
let args := e.getAppArgs
let lhs liftMetaM do Meta.whnf args[inductVal.numParams + inductVal.numIndices + 1]!
let rhs liftMetaM do Meta.whnf args[inductVal.numParams + inductVal.numIndices + 2]!
let lhs liftMetaM do Meta.whnf args[inductVal.numParams + 1 + inductVal.numIndices]!
let rhs liftMetaM do Meta.whnf args[inductVal.numParams + 1 + inductVal.numIndices + 1 + inductVal.numIndices]!
let lhs liftMetaM lhs.toCtorIfLit
let rhs liftMetaM rhs.toCtorIfLit
match ( liftMetaM <| Meta.isConstructorApp? lhs), ( liftMetaM <| Meta.isConstructorApp? rhs) with

View File

@@ -63,8 +63,8 @@ an ILean finalization notification for the worker and the document version desig
Used for test stability in tests that use the .ileans.
-/
structure WaitForILeansParams where
uri : DocumentUri
version : Nat
uri? : Option DocumentUri := none
version? : Option Nat := none
deriving FromJson, ToJson
structure WaitForILeans where

View File

@@ -10,6 +10,7 @@ prelude
public import Lean.Expr
public import Lean.Data.Lsp.Basic
public import Lean.Data.JsonRpc
public import Lean.Data.DeclarationRange
public section
@@ -98,27 +99,129 @@ instance : ToJson RefIdent where
end RefIdent
/-- Information about the declaration surrounding a reference. -/
structure RefInfo.ParentDecl where
/-- Name of the declaration surrounding a reference. -/
name : String
/-- Range of the declaration surrounding a reference. -/
range : Lsp.Range
/-- Selection range of the declaration surrounding a reference. -/
selectionRange : Lsp.Range
deriving ToJson
/-- Position information for a declaration. Inlined to reduce memory consumption. -/
structure DeclInfo where
/-- Start line of range. -/
rangeStartPosLine : Nat
/-- Start character of range. -/
rangeStartPosCharacter : Nat
/-- End line of range. -/
rangeEndPosLine : Nat
/-- End character of range. -/
rangeEndPosCharacter : Nat
/-- Start line of selection range. -/
selectionRangeStartPosLine : Nat
/-- Start character of selection range. -/
selectionRangeStartPosCharacter : Nat
/-- End line of selection range. -/
selectionRangeEndPosLine : Nat
/-- End character of selection range. -/
selectionRangeEndPosCharacter : Nat
/-- Converts a set of `DeclarationRanges` to a `DeclInfo`. -/
def DeclInfo.ofDeclarationRanges (r : DeclarationRanges) : DeclInfo where
rangeStartPosLine := r.range.pos.line - 1
rangeStartPosCharacter := r.range.charUtf16
rangeEndPosLine := r.range.endPos.line - 1
rangeEndPosCharacter := r.range.endCharUtf16
selectionRangeStartPosLine := r.selectionRange.pos.line - 1
selectionRangeStartPosCharacter := r.selectionRange.charUtf16
selectionRangeEndPosLine := r.selectionRange.endPos.line - 1
selectionRangeEndPosCharacter := r.selectionRange.endCharUtf16
/-- Range of this parent decl. -/
def DeclInfo.range (i : DeclInfo) : Lsp.Range :=
i.rangeStartPosLine, i.rangeStartPosCharacter, i.rangeEndPosLine, i.rangeEndPosCharacter
/-- Selection range of this parent decl. -/
def DeclInfo.selectionRange (i : DeclInfo) : Lsp.Range :=
i.selectionRangeStartPosLine, i.selectionRangeStartPosCharacter,
i.selectionRangeEndPosLine, i.selectionRangeEndPosCharacter
instance : ToJson DeclInfo where
toJson i :=
Json.arr #[
i.rangeStartPosLine,
i.rangeStartPosCharacter,
i.rangeEndPosLine,
i.rangeEndPosCharacter,
i.selectionRangeStartPosLine,
i.selectionRangeStartPosCharacter,
i.selectionRangeEndPosLine,
i.selectionRangeEndPosCharacter
]
instance : FromJson DeclInfo where
fromJson?
| .arr xs => do
if xs.size != 8 then
throw s!"Expected list of length 8, not length {xs.size}"
return {
rangeStartPosLine := fromJson? xs[0]!
rangeStartPosCharacter := fromJson? xs[1]!
rangeEndPosLine := fromJson? xs[2]!
rangeEndPosCharacter := fromJson? xs[3]!
selectionRangeStartPosLine := fromJson? xs[4]!
selectionRangeStartPosCharacter := fromJson? xs[5]!
selectionRangeEndPosLine := fromJson? xs[6]!
selectionRangeEndPosCharacter := fromJson? xs[7]!
}
| _ => throw "Expected list"
/-- Declarations of a file with associated position information. -/
@[expose] def Decls := Std.TreeMap String DeclInfo
deriving EmptyCollection, ForIn Id
instance : ToJson Decls where
toJson m := Json.mkObj <| m.toList.map fun (declName, info) => (declName, toJson info)
instance : FromJson Decls where
fromJson? j := do
let node j.getObj?
node.foldlM (init := ) fun m k v =>
return m.insert k ( fromJson? v)
/--
Denotes the range of a reference, as well as the parent declaration of the reference.
If the reference is itself a declaration, then it contains no parent declaration.
The position information is inlined to reduce memory consumption.
-/
structure RefInfo.Location where
/-- Range of the reference. -/
range : Lsp.Range
/-- Parent declaration of the reference. `none` if the reference is itself a declaration. -/
parentDecl? : Option RefInfo.ParentDecl
mk' ::
/-- Start line of the range of this location. -/
startPosLine : Nat
/-- Start character of the range of this location. -/
startPosCharacter : Nat
/-- End line of the range of this location. -/
endPosLine : Nat
/-- End character of the range of this location. -/
endPosCharacter : Nat
/--
Parent declaration of the reference. Empty string if the reference is itself a declaration.
We do not use `Option` for memory consumption reasons.
-/
parentDecl : String
deriving Inhabited
/-- Creates a `RefInfo.Location`. -/
def RefInfo.Location.mk (range : Lsp.Range) (parentDecl? : Option String) : RefInfo.Location where
startPosLine := range.start.line
startPosCharacter := range.start.character
endPosLine := range.end.line
endPosCharacter := range.end.character
parentDecl := parentDecl?.getD ""
/-- Range of this location. -/
def RefInfo.Location.range (l : RefInfo.Location) : Lsp.Range :=
l.startPosLine, l.startPosCharacter, l.endPosLine, l.endPosCharacter
/-- Name of the parent declaration of this location. -/
def RefInfo.Location.parentDecl? (l : RefInfo.Location) : Option String :=
if l.parentDecl.isEmpty then
none
else
some l.parentDecl
/-- Definition site and usage sites of a reference. Obtained from `Lean.Server.RefInfo`. -/
structure RefInfo where
/-- Definition site of the reference. May be `none` when we cannot find a definition site. -/
@@ -128,16 +231,9 @@ structure RefInfo where
instance : ToJson RefInfo where
toJson i :=
let rangeToList (r : Lsp.Range) : List Nat :=
[r.start.line, r.start.character, r.end.line, r.end.character]
let parentDeclToList (d : RefInfo.ParentDecl) : List Json :=
let name := d.name |> toJson
let range := rangeToList d.range |>.map toJson
let selectionRange := rangeToList d.selectionRange |>.map toJson
[name] ++ range ++ selectionRange
let locationToList (l : RefInfo.Location) : List Json :=
let range := rangeToList l.range |>.map toJson
let parentDecl := l.parentDecl?.map parentDeclToList |>.getD []
let range := [l.startPosLine, l.startPosCharacter, l.endPosLine, l.endPosCharacter].map toJson
let parentDecl := l.parentDecl?.map ([toJson ·]) |>.getD []
range ++ parentDecl
Json.mkObj [
("definition", toJson $ i.definition?.map locationToList),
@@ -147,35 +243,30 @@ instance : ToJson RefInfo where
instance : FromJson RefInfo where
-- This implementation is optimized to prevent redundant intermediate allocations.
fromJson? j := do
let toRange (a : Array Json) (i : Nat) : Except String Lsp.Range :=
if h : a.size < i + 4 then
throw s!"Expected list of length 4, not {a.size}"
else
return {
start := {
line := fromJson? a[i]
character := fromJson? a[i+1]
}
«end» := {
line := fromJson? a[i+2]
character := fromJson? a[i+3]
}
}
let toParentDecl (a : Array Json) (i : Nat) : Except String RefInfo.ParentDecl := do
let name fromJson? a[i]!
let range toRange a (i + 1)
let selectionRange toRange a (i + 5)
return name, range, selectionRange
let toLocation (a : Array Json) : Except String RefInfo.Location := do
if a.size != 4 && a.size != 13 then
.error "Expected list of length 4 or 13, not {l.size}"
let range toRange a 0
if a.size == 13 then
let parentDecl toParentDecl a 4
return range, parentDecl
if h : a.size 4 a.size 5 then
.error s!"Expected list of length 4 or 5, not {a.size}"
else
return range, none
let startPosLine fromJson? a[0]
let startPosCharacter fromJson? a[1]
let endPosLine fromJson? a[2]
let endPosCharacter fromJson? a[3]
if h' : a.size = 5 then
return {
startPosLine
startPosCharacter
endPosLine
endPosCharacter
parentDecl := fromJson? a[4]
}
else
return {
startPosLine
startPosCharacter
endPosLine
endPosCharacter
parentDecl := ""
}
let definition? j.getObjValAs? (Option $ Array Json) "definition"
let definition? match definition? with
| none => pure none
@@ -213,15 +304,28 @@ structure LeanILeanHeaderInfoParams where
directImports : Array ImportInfo
deriving FromJson, ToJson
/--
Used in the `$/lean/ileanHeaderSetupInfo` watchdog <- worker notifications.
Contains status information about `lake setup-file`.
-/
structure LeanILeanHeaderSetupInfoParams where
/-- Version of the file these imports are from. -/
version : Nat
/-- Whether setting up the header using `lake setup-file` has failed. -/
isSetupFailure : Bool
deriving FromJson, ToJson
/--
Used in the `$/lean/ileanInfoUpdate` and `$/lean/ileanInfoFinal` watchdog <- worker notifications.
Contains the definitions and references of the file managed by a worker.
-/
structure LeanIleanInfoParams where
/-- Version of the file these references are from. -/
version : Nat
version : Nat
/-- All references for the file. -/
references : ModuleRefs
references : ModuleRefs
/-- All decls for the file. -/
decls : Decls
deriving FromJson, ToJson
/--

View File

@@ -141,6 +141,19 @@ partial def waitForILeans (waitForILeansId : RequestID := 0) (target : DocumentU
| _ =>
pure ()
partial def waitForWatchdogILeans (waitForILeansId : RequestID := 0) : IpcM Unit := do
writeRequest waitForILeansId, "$/lean/waitForILeans", WaitForILeansParams.mk none none
while true do
match ( readMessage) with
| .response id _ =>
if id == waitForILeansId then
return
| .responseError id _ msg _ =>
if id == waitForILeansId then
throw $ userError s!"Waiting for ILeans failed: {msg}"
| _ =>
pure ()
/--
Waits for a diagnostic notification with a specific message to be emitted. Discards all received
messages, so should not be combined with `collectDiagnostics`.

View File

@@ -52,7 +52,7 @@ partial def find? (cmp : αα → Ordering) (t : PrefixTreeNode α β cmp)
| some t => loop t ks
loop t k
/-- Returns the the value of the longest key in `t` that is a prefix of `k`, if any. -/
/-- Returns the value of the longest key in `t` that is a prefix of `k`, if any. -/
@[inline]
partial def findLongestPrefix? (cmp : α α Ordering) (t : PrefixTreeNode α β cmp) (k : List α) : Option β :=
let rec @[specialize] loop acc?

View File

@@ -154,7 +154,7 @@ def SystemLiteral : Parser String :=
/-- https://www.w3.org/TR/xml/#NT-PubidChar -/
def PubidChar : Parser LeanChar :=
asciiLetter <|> digit <|> endl <|> attempt do
let c ← any
let c : _root_.Char := ← any
if "-'()+,./:=?;!*#@$_%".contains c then pure c else fail "PublidChar expected"
/-- https://www.w3.org/TR/xml/#NT-PubidLiteral -/

View File

@@ -124,7 +124,7 @@ def rewriteManualLinksCore (s : String) : Id (Array (Lean.Syntax.Range × String
iter' := iter'.next h'
if urlChar c' && ¬iter'.IsAtEnd then
continue
match rw (start.extract pre') with
match rw (s.extract start pre') with
| .error err =>
errors := errors.push (pre.offset, pre'.offset, err)
out := out.push c

View File

@@ -9,6 +9,8 @@ prelude
public import Lean.Meta.Tactic.ElimInfo
public import Lean.Elab.Binders
public import Lean.Elab.RecAppSyntax
public import Lean.IdentifierSuggestion
import all Lean.Elab.ErrorUtils
public section
@@ -243,7 +245,9 @@ private def synthesizePendingAndNormalizeFunType : M Unit := do
.note m!"Expected a function because this term is being applied to the argument\
{indentD <| toMessageData arg}"
else .nil
throwError "Function expected at{indentExpr s.f}\nbut this term has type{indentExpr fType}{extra}"
throwError "Function expected at{indentExpr s.f}\nbut this term has type{indentExpr fType}\
{extra}\
{← hintAutoImplicitFailure s.f}"
/-- Normalize and return the function type. -/
private def normalizeFunType : M Expr := do
@@ -1252,15 +1256,6 @@ inductive LValResolution where
The `baseName` is the base name of the type to search for in the parameter list. -/
| localRec (baseName : Name) (fvar : Expr)
private def mkLValError (e : Expr) (eType : Expr) (msg : MessageData) : MessageData :=
m!"{msg}{indentExpr e}\nhas type{indentExpr eType}"
private def throwLValErrorAt (ref : Syntax) (e : Expr) (eType : Expr) (msg : MessageData) : TermElabM α :=
throwErrorAt ref (mkLValError e eType msg)
private def throwLValError (e : Expr) (eType : Expr) (msg : MessageData) : TermElabM α := do
throwLValErrorAt ( getRef) e eType msg
/--
`findMethod? S fName` tries the for each namespace `S'` in the resolution order for `S` to resolve the name `S'.fname`.
If it resolves to `name`, returns `(S', name)`.
@@ -1291,9 +1286,6 @@ private partial def findMethod? (structName fieldName : Name) : MetaM (Option (N
return res
return none
private def throwInvalidFieldNotation (e eType : Expr) : TermElabM α :=
throwLValError e eType "Invalid field notation: Type is not of the form `C ...` where C is a constant"
/--
If it seems that the user may be attempting to project out the `n`th element of a tuple, or that the
nesting behavior of n-ary products is otherwise relevant, generates a corresponding hint; otherwise,
@@ -1304,15 +1296,13 @@ private partial def mkTupleHint (eType : Expr) (idx : Nat) (ref : Syntax) : Term
if arity > 1 then
let numComps := arity + 1
if idx numComps && ref.getHeadInfo matches .original .. then
let ordinalSuffix := match idx % 10 with
| 1 => "st" | 2 => "nd" | 3 => "rd" | _ => "th"
let mut projComps := List.replicate (idx - 1) "2"
if idx < numComps then projComps := projComps ++ ["1"]
let proj := ".".intercalate projComps
let sug := { suggestion := proj, span? := ref,
toCodeActionTitle? := some (s!"Change projection `{idx}` to `{·}`") }
MessageData.hint m!"n-tuples in Lean are actually nested pairs. To access the \
{idx}{ordinalSuffix} component of this tuple, use the projection `.{proj}` instead:" #[sug]
{idx.toOrdinal} component of this tuple, use the projection `.{proj}` instead:" #[sug]
else
return MessageData.hint' m!"n-tuples in Lean are actually nested pairs. For example, to access the \
\"third\" component of `(a, b, c)`, write `(a, b, c).2.2` instead of `(a, b, c).3`."
@@ -1325,45 +1315,15 @@ where
| some (_, p2) => prodArity p2 + 1
private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM LValResolution := do
let throwInvalidFieldAt {α : Type} (ref : Syntax) (fieldName : String) (fullName : Name)
(declHint := Name.anonymous) : TermElabM α := do
let msg
-- ordering: put decl hint, if any, last
mkUnknownIdentifierMessage (declHint := declHint)
(mkLValError e eType
m!"Invalid field `{fieldName}`: The environment does not contain `{fullName}`")
-- HACK: Simulate previous embedding of tagged `mkUnknownIdentifierMessage`.
-- The "import unknown identifier" code action requires the tag to be present somewhere in the
-- message. But if it is at the root, the tag will also be shown to the user even though the
-- current help page does not address field notation, which should likely get its own help page
-- (if any).
throwErrorAt ref m!"{msg}{.nil}"
if eType.isForall then
match lval with
| LVal.fieldName ref fieldName suffix? _fullRef =>
let fullName := Name.str `Function fieldName
if ( getEnv).contains fullName then
return LValResolution.const `Function `Function fullName
else if suffix?.isNone || e.getAppFn.isFVar then
/- If there's no suffix, or the head is a function-typed free variable, this could only have
been a field in the `Function` namespace, so we needn't wait to check if this is actually
a constant. If `suffix?` is non-`none`, we prefer to throw the "unknown constant" error
(because of monad namespaces like `IO` and auxiliary declarations like `mutual_induct`) -/
throwInvalidFieldAt ref fieldName fullName
| .fieldIdx .. =>
throwLValError e eType "Invalid projection: Projections cannot be used on functions"
else if eType.getAppFn.isMVar then
let (kind, name) :=
match lval with
| .fieldName _ fieldName _ _ => (m!"field notation", m!"field `{fieldName}`")
| .fieldIdx _ i => (m!"projection", m!"projection `{i}`")
throwError "Invalid {kind}: Type of{indentExpr e}\nis not known; cannot resolve {name}"
match eType.getAppFn.constName?, lval with
| some structName, LVal.fieldIdx ref idx =>
match eType.getAppFn, lval with
| .const structName _, LVal.fieldIdx ref idx =>
if idx == 0 then
throwError "Invalid projection: Index must be greater than 0"
let env getEnv
let failK _ := throwLValError e eType "Invalid projection: Expected a value whose type is a structure"
let failK _ := throwError "Invalid projection: Projection operates on structure-like types \
with fields. The expression{indentExpr e}\nhas type{inlineExpr eType}which does not \
have fields."
matchConstStructure eType.getAppFn failK fun _ _ ctorVal => do
let numFields := ctorVal.numFields
if idx - 1 < numFields then
@@ -1376,17 +1336,15 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
return LValResolution.projIdx structName (idx - 1)
else
if numFields == 0 then
throwLValError e eType m!"Invalid projection: Projections are not supported on this type \
because it has no fields"
let (fields, bounds) := if numFields == 1 then
(m!"field", m!"the only valid index is 1")
else
(m!"fields", m!"it must be between 1 and {numFields}")
throwError m!"Invalid projection: Projection operates on structure-like types with \
fields. The expression{indentExpr e}\nhas type{inlineExpr eType}which has no fields."
let tupleHint mkTupleHint eType idx ref
throwError m!"Invalid projection: Index `{idx}` is invalid for this structure; {bounds}"
++ .note m!"The expression{inlineExpr e}has type{inlineExpr eType}which has only {numFields} {fields}"
throwError m!"Invalid projection: Index `{idx}` is invalid for this structure; \
{numFields.plural "the only valid index is 1" s!"it must be between 1 and {numFields}"}"
++ MessageData.note m!"The expression{indentExpr e}\nhas type{inlineExpr eType}which has only \
{numFields} field{numFields.plural}"
++ tupleHint
| some structName, LVal.fieldName ref fieldName _ _ => withRef ref do
| .const structName _, LVal.fieldName ref fieldName _ _ => withRef ref do
let env getEnv
if isStructure env structName then
if let some baseStructName := findField? env structName (Name.mkSimple fieldName) then
@@ -1406,14 +1364,77 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
-- Suggest a potential unreachable private name as hint. This does not cover structure
-- inheritance, nor `import all`.
(declHint := (mkPrivateName env structName).mkStr fieldName)
| none, LVal.fieldName ref _ (some suffix) _fullRef =>
-- This may be a function constant whose implicit arguments have already been filled in:
let c := e.getAppFn
if c.isConst then
throwUnknownConstantAt ref (c.constName! ++ suffix)
else
throwInvalidFieldNotation e eType
| _, _ => throwInvalidFieldNotation e eType
| .forallE .., LVal.fieldName ref fieldName suffix? _fullRef =>
let fullName := Name.str `Function fieldName
if ( getEnv).contains fullName then
return LValResolution.const `Function `Function fullName
match e.getAppFn, suffix? with
| Expr.const c _, some suffix =>
throwUnknownConstantWithSuggestions (c ++ suffix)
| _, _ =>
throwInvalidFieldAt ref fieldName fullName
| .forallE .., .fieldIdx .. =>
throwError "Invalid projection: Projections cannot be used on functions, and{indentExpr e}\n\
has function type{inlineExprTrailing eType}"
| .mvar .., .fieldName _ fieldName _ _ =>
let possibleConstants := ( getEnv).constants.fold (fun accum name _ =>
match name with
| .str _ s => if s = fieldName && !name.isInternal then accum.push name else accum
| _ => accum) #[]
let hint := match possibleConstants with
| #[] => MessageData.nil
| #[opt] => .hint' m!"Consider replacing the field projection `.{fieldName}` with a call to the function `{.ofConstName opt}`."
| opts => .hint' m!"Consider replacing the field projection with a call to one of the following:\
{MessageData.joinSep (opts.toList.map (indentD m!" `{.ofConstName ·}`")) .nil}"
throwNamedError lean.invalidField (m!"Invalid field notation: Type of{indentExpr e}\nis not \
known; cannot resolve field `{fieldName}`" ++ hint)
| .mvar .., .fieldIdx _ i =>
throwError m!"Invalid projection: Type of{indentExpr e}\nis not known; cannot resolve \
projection `{i}`"
| _, _ =>
match e.getAppFn, lval with
| Expr.const c _, .fieldName _ref _fieldName (some suffix) _fullRef =>
throwUnknownConstantWithSuggestions (c ++ suffix)
| _, .fieldName .. =>
throwNamedError lean.invalidField m!"Invalid field notation: Field projection operates on \
types of the form `C ...` where C is a constant. The expression{indentExpr e}\nhas \
type{inlineExpr eType}which does not have the necessary form."
| _, .fieldIdx .. =>
throwError m!"Invalid projection: Projection operates on types of the form `C ...` where C \
is a constant. The expression{indentExpr e}\nhas type{inlineExpr eType}which does not have \
the necessary form."
where
throwInvalidFieldAt {α : Type} (ref : Syntax) (fieldName : String) (fullName : Name)
(declHint := Name.anonymous) : TermElabM α := do
let msg
-- ordering: put decl hint, if any, last
mkUnknownIdentifierMessage (declHint := declHint)
m!"Invalid field `{fieldName}`: The environment does not contain `{fullName}`, so it is not \
possible to project the field `{fieldName}` from an expression{indentExpr e}\nof \
type{inlineExprTrailing eType}"
-- Possible alternatives provided with `@[suggest_for]` annotations
let suggestions := ( Lean.getSuggestions fullName).filter (·.getPrefix = fullName.getPrefix)
let suggestForHint
if suggestions.size = 0 then
pure .nil
else
m!"Perhaps you meant one of these in place of `{fullName}`:".hint (suggestions.map fun suggestion => {
suggestion := suggestion.getString!,
toCodeActionTitle? := .some (s!"Suggested replacement: {e}.{·}"),
diffGranularity := .all,
messageData? := .some m!"`{.ofConstName suggestion}`: {e}.{suggestion.getString!}",
}) ref
-- By using `mkUnknownIdentifierMessage`, the tag `Lean.unknownIdentifierMessageTag` is
-- incorporated within the message, as required for the "import unknown identifier" code action.
-- The "outermost" lean.invalidField name is the only one that triggers an error explanation.
throwNamedErrorAt ref lean.invalidField (msg ++ suggestForHint)
/-- whnfCore + implicit consumption.
Example: given `e` with `eType := {α : Type} → (fun β => List β) α `, it produces `(e ?m, List ?m)` where `?m` is fresh metavariable. -/

View File

@@ -8,6 +8,7 @@ module
prelude
public import Lean.Elab.MutualDef
import Lean.Compiler.Options
import Lean.Meta.Reduce
public section

View File

@@ -461,7 +461,10 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
let heqType inferType heq
let heqType instantiateMVars heqType
match ( Meta.matchEq? heqType) with
| none => throwError "invalid `▸` notation, argument{indentExpr heq}\nhas type{indentExpr heqType}\nequality expected"
| none => throwError "invalid `▸` notation, argument{indentExpr heq}\n\
has type{indentExpr heqType}\n\
equality expected\
{← Term.hintAutoImplicitFailure heq (expected := "an equality")}"
| some (α, lhs, rhs) =>
let mut lhs := lhs
let mut rhs := rhs

View File

@@ -330,11 +330,11 @@ def elabMutual : CommandElab := fun stx => do
Term.applyAttributes declName attrs
for attrName in toErase do
Attribute.erase declName attrName
if ( getEnv).isImportedConst declName && attrs.any (·.kind == .global) then
-- If an imported declaration is marked with a global attribute, there is no good way to track
-- its use generally and so Shake should conservatively preserve imports of the current
-- module.
recordExtraRevUseOfCurrentModule
if ( getEnv).isImportedConst declName then
if let some attr := attrs.find? (·.kind == .global) then
-- If an imported declaration is marked with a global attribute, Shake must be informed
-- about this indirect reference
recordIndirectModUse attr.name.toString declName
@[builtin_command_elab Lean.Parser.Command.«initialize»] def elabInitialize : CommandElab
| stx@`($declModifiers:declModifiers $kw:initializeKeyword $[$id? : $type? ]? $doSeq) => do

View File

@@ -223,6 +223,7 @@ example, `deriving instance Foo for Bar, Baz` invokes ``fooHandler #[`Bar, `Baz]
def registerDerivingHandler (className : Name) (handler : DerivingHandler) : IO Unit := do
unless ( initializing) do
throw (IO.userError "failed to register deriving handler, it can only be registered during initialization")
Term.registerDerivableClass className
derivingHandlersRef.modify fun m => match m.find? className with
| some handlers => m.insert className (handler :: handlers)
| none => m.insert className [handler]

View File

@@ -86,6 +86,9 @@ structure State where
-/
lctx : LocalContext
/--
-/
localInstances : LocalInstances
/--
The options.
The `MonadLift TermElabM DocM` instance runs the lifted action with these options, so elaboration
@@ -129,10 +132,10 @@ instance : MonadStateOf State DocM :=
instance : MonadLift TermElabM DocM where
monadLift act := private DocM.mk fun _ _ st' => do
let {openDecls, lctx, options, ..} := ( st'.get)
let {openDecls, lctx, options, localInstances, ..} := ( st'.get)
let v
withTheReader Core.Context (fun ρ => { ρ with openDecls, options }) <|
withTheReader Meta.Context (fun ρ => { ρ with lctx }) <|
withTheReader Meta.Context (fun ρ => { ρ with lctx, localInstances }) <|
act
return v
@@ -144,16 +147,19 @@ private builtin_initialize modDocstringStateExt : EnvExtension (Option ModuleDoc
registerEnvExtension (pure none)
private def getModState
[Monad m] [MonadEnv m] [MonadLiftT IO m] [MonadLCtx m]
[Monad m] [MonadEnv m] [MonadLiftT IO m] [MonadLiftT MetaM m] [MonadLCtx m]
[MonadResolveName m] [MonadOptions m] : m ModuleDocstringState := do
if let some st := modDocstringStateExt.getState ( getEnv) then
return st
else
let lctx getLCtx
let openDecls getOpenDecls
let options getOptions
let scopes := [{header := "", isPublic := true}]
let st : ModuleDocstringState := { scopes, openDecls, lctx, options, scopedExts := #[] }
let openDecls getOpenDecls
let lctx getLCtx
let localInstances Meta.getLocalInstances
let options getOptions
let scopedExts := #[]
let st : ModuleDocstringState :=
{ scopes, openDecls, lctx, localInstances, options, scopedExts }
modifyEnv fun env =>
modDocstringStateExt.setState env st
return st
@@ -197,7 +203,7 @@ def DocM.exec (declName : Name) (binders : Syntax) (act : DocM α)
let options getOptions
let scopes := [{header := "", isPublic := true}]
let ((v, _), _) withTheReader Meta.Context (fun ρ => { ρ with localInstances }) <|
act.run { suggestionMode } |>.run {} |>.run { scopes, openDecls, lctx, options }
act.run { suggestionMode } |>.run {} |>.run { scopes, openDecls, lctx, localInstances, options }
pure v
finally
scopedEnvExtensionsRef.set sc

View File

@@ -522,7 +522,6 @@ private def givenContents : ParserFn :=
optionalFn (symbolFn ":" >> termParser.fn)))
(symbolFn ",")
/--
A metavariable to be discussed in the remainder of the docstring.
@@ -612,6 +611,98 @@ def given (type : Option StrLit := none) (typeIsMeta : flag false) («show» : f
|> Inline.concat
else return .empty
private def givenInstanceContents : ParserFn :=
whitespace >>
sepBy1Fn false
(nodeFn nullKind
(optionalFn (atomicFn (identFn >> symbolFn ":")) >>
termParser.fn))
(symbolFn ",")
/--
An instance metavariable to be discussed in the remainder of the docstring.
This is similar to {given}, but the resulting variable is marked for instance synthesis
(with `BinderInfo.instImplicit`), and the name is optional.
There are two syntaxes that can be used:
* `` {givenInstance}`T` `` establishes an unnamed instance of type `T`.
* `` {givenInstance}`x : T` `` establishes a named instance `x` of type `T`.
Additionally, the contents of the code literal can be repeated, with comma separators.
If the `show` flag is `false` (default `true`), then the instance is not shown in the docstring.
-/
@[builtin_doc_role]
def givenInstance («show» : flag true) (xs : TSyntaxArray `inline) :
DocM (Inline ElabInline) := do
let s onlyCode xs
let stxs parseStrLit givenInstanceContents s
let stxs := stxs.getArgs.mapIdx Prod.mk |>.filterMap fun (n, s) =>
if n % 2 = 0 then some s else none
let mut lctx getLCtx
let mut localInstances Meta.getLocalInstances
let mut instCounter := 0
for stx in stxs do
let nameColonOpt := stx[0][0]
let tyStx := stx[1]
let ty' : Expr elabType tyStx
let class? Meta.isClass? ty'
let some className := class?
| throwError m!"Expected a type class, but got `{.ofExpr ty'}`"
-- Generate a fresh name if no name is provided
let (userName, hasUserName)
if nameColonOpt.isMissing then
instCounter := instCounter + 1
let n mkFreshUserName (`inst ++ className)
pure (n, false)
else
pure (nameColonOpt.getId, true)
let fv mkFreshFVarId
lctx := lctx.mkLocalDecl fv userName ty' BinderInfo.instImplicit
localInstances := localInstances.push { fvar := .fvar fv, className }
if hasUserName then
addTermInfo' nameColonOpt[0] (.fvar fv)
(lctx? := some lctx) (isBinder := true) (expectedType? := some ty')
modify fun st => { st with lctx, localInstances }
if «show» then
let text getFileMap
let mut outStrs := #[]
let mut failed := false
for stx in stxs do
let nameColonOpt := stx[0][0]
let thisStr
if let some b', e' := stx[1].getRange? then
-- Has type annotation
if nameColonOpt.isMissing then
-- No name, just show type
pure <| String.Pos.Raw.extract text.source b' e'
else
-- Has name and type, nameColonOpt is `identFn >> symbolFn ":"`
if let some b, e := nameColonOpt[0].getRange? then
pure <| s!"{b.extract text.source e} : {b'.extract text.source e'}"
else
failed := true
break
else
failed := true
break
outStrs := outStrs.push thisStr
if failed then
return .code s.getString
else
return outStrs.map Inline.code
|>.toList |>.intersperse (Inline.text ", ") |>.toArray
|> Inline.concat
else return .empty
private def firstToken? (stx : Syntax) : Option Syntax :=
stx.find? fun

View File

@@ -0,0 +1,99 @@
/-
Copyright (c) 2025 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rob Simmons
-/
module
prelude
import Lean.Message
namespace Lean
/--
Translate numbers (1, 2, 3, 212, 322 ...) to ordinals with appropriate English-language names for
small ordinals (0 through 10 become "zeroth" through "tenth") and postfixes for other numbers
(212 becomes "212th" and 1292 becomes "1292nd").
-/
def _root_.Nat.toOrdinal : Nat -> String
| 0 => "zeroth"
| 1 => "first"
| 2 => "second"
| 3 => "third"
| 4 => "fourth"
| 5 => "fifth"
| 6 => "sixth"
| 7 => "seventh"
| 8 => "eighth"
| 9 => "ninth"
| 10 => "tenth"
| n => if n % 100 > 10 && n % 100 < 20 then
s!"{n}th"
else if n % 10 == 2 then
s!"{n}nd"
else if n % 10 == 3 then
s!"{n}rd"
else
s!"{n}th"
class HasOxfordStrings α where
emp : α
and : α
comma : α
commaAnd : α
instance : HasOxfordStrings String where
emp := ""
and := " and "
comma := ", "
commaAnd := ", and "
instance : HasOxfordStrings MessageData where
emp := ""
and := " and "
comma := ", "
commaAnd := ", and "
/--
Make an oxford-comma-separated list of strings.
- `["eats"].toOxford == "eats"`
- `["eats", "shoots"].toOxford == "eats and shoots"`
- `["eats", "shoots", "leaves"] == "eats, shoots, and leaves"`
-/
def _root_.List.toOxford [Append α] [HasOxfordStrings α] : List α -> α
| [] => HasOxfordStrings.emp
| [a] => a
| [a, b] => a ++ HasOxfordStrings.and ++ b
| [a, b, c] => a ++ HasOxfordStrings.comma ++ b ++ HasOxfordStrings.commaAnd ++ c
| a :: as => a ++ HasOxfordStrings.comma ++ as.toOxford
class HasPluralDefaults α where
singular : α
plural : α α
instance : HasPluralDefaults String where
singular := ""
plural := (· ++ "s")
instance : HasPluralDefaults MessageData where
singular := .nil
plural := (m!"{·}s")
/--
Give alternative forms of a string if the `count` is 1 or not.
- `(1).plural == ""`
- `(2).plural == "s"`
- `(1).plural "wug" == "wug"`
- `(2).plural "wug" == "wugs"`
- `(1).plural "it" "they" == "it"`
- `(2).plural "it" "they" == "they"`
-/
def _root_.Nat.plural [HasPluralDefaults α] (count : Nat)
(singular : α := HasPluralDefaults.singular)
(plural : α := HasPluralDefaults.plural singular) :=
if count = 1 then
singular
else
plural

View File

@@ -199,10 +199,12 @@ def runFrontend
if let some ileanFileName := ileanFileName? then
let trees := snaps.getAll.flatMap (match ·.infoTree? with | some t => #[t] | _ => #[])
let references := Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false)
let (moduleRefs, decls) references.toLspModuleRefs
let ilean := {
module := mainModuleName
directImports := Server.collectImports snap.stx
references := references.toLspModuleRefs
references := moduleRefs
decls
: Lean.Server.Ilean
}
IO.FS.writeFile ileanFileName $ Json.compress $ toJson ilean

View File

@@ -12,6 +12,8 @@ public import Lean.Elab.BindersUtil
public import Lean.Elab.PatternVar
public import Lean.Elab.Quotation.Precheck
public import Lean.Elab.SyntheticMVars
import Lean.Meta.Match.Value
import Lean.Meta.Match.NamedPatterns
public section

View File

@@ -1173,7 +1173,7 @@ private def checkNoInductiveNameConflicts (elabs : Array InductiveElabStep1) (is
let throwErrorsAt (init cur : Syntax) (msg : MessageData) : TermElabM Unit := do
logErrorAt init msg
throwErrorAt cur msg
-- Maps names of inductive types to to `true` and those of constructors to `false`, along with syntax refs
-- Maps names of inductive types to `true` and those of constructors to `false`, along with syntax refs
let mut uniqueNames : Std.HashMap Name (Bool × Syntax) := {}
let declString := if isCoinductive then "coinductive predicate" else "inductive type"
trace[Elab.inductive] "deckString: {declString}"

View File

@@ -8,9 +8,11 @@ module
prelude
import Lean.Elab.PreDefinition.EqnsUtils
import Lean.Meta.Match.MatchEqs
import Lean.Meta.Match.MatchEqsExt
import Lean.Meta.Match.NamedPatterns
import Lean.Meta.Tactic.Simp.Main
import Lean.Meta.Tactic.Split
import Lean.Meta.Tactic.CasesOnStuckLHS
/-!
This module implements the generation of equational theorems, given unfolding theorems.

View File

@@ -9,7 +9,9 @@ module
prelude
public import Lean.Meta.Basic
import Lean.Meta.Tactic.Split
import Lean.Meta.Match.MatchEqs
import Lean.Meta.Match.Match
import Lean.Meta.Tactic.Refl
import Lean.Meta.Tactic.Delta
import Lean.Meta.Tactic.SplitIf
/-!

View File

@@ -8,12 +8,12 @@ module
prelude
public import Lean.Elab.PreDefinition.FixedParams
import Lean.Elab.PreDefinition.EqnsUtils
import Lean.Meta.Tactic.Split
import Lean.Meta.Tactic.CasesOnStuckLHS
import Lean.Meta.Tactic.Delta
import Lean.Meta.Tactic.Simp.Main
import Lean.Elab.PreDefinition.Basic
import Lean.Elab.PreDefinition.Structural.Basic
import Lean.Meta.Match.MatchEqs
import Lean.Meta.Tactic.Rewrite
import Lean.Meta.Tactic.Delta
import Lean.Meta.Tactic.CasesOnStuckLHS
import Lean.Meta.Tactic.Split
namespace Lean.Elab
open Meta

View File

@@ -237,21 +237,32 @@ def solveDecreasingGoals (funNames : Array Name) (argsPacker : ArgsPacker) (decr
Term.reportUnsolvedGoals remainingGoals
instantiateMVars value
def isNatLtWF (wfRel : Expr) : MetaM (Option Expr) := do
match_expr wfRel with
| invImage _ β f wfRelβ =>
unless ( isDefEq β (mkConst ``Nat)) do return none
unless ( isDefEq wfRelβ (mkConst ``Nat.lt_wfRel)) do return none
return f
| _ => return none
def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (argsPacker : ArgsPacker)
(wfRel : Expr) (funNames : Array Name) (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]!
let varName x.fvarId!.getUserName -- See comment below.
let α inferType x
let u getLevel α
let v getLevel type
let motive mkLambdaFVars #[x] type
let rel := mkProj ``WellFoundedRelation 0 wfRel
let wf := mkProj ``WellFoundedRelation 1 wfRel
let wf mkAppM `Lean.opaqueId #[wf]
let varName x.fvarId!.getUserName -- See comment below.
return (mkApp4 (mkConst ``WellFounded.fix [u, v]) α motive rel wf, varName)
if let some measure isNatLtWF wfRel then
return (mkApp3 (mkConst `WellFounded.Nat.fix [u, v]) α motive measure, varName)
else
let rel := mkProj ``WellFoundedRelation 0 wfRel
let wf := mkProj ``WellFoundedRelation 1 wfRel
let wf mkAppM `Lean.opaqueId #[wf]
return (mkApp4 (mkConst ``WellFounded.fix [u, v]) α motive rel wf, varName)
forallBoundedTelescope ( whnf ( inferType wfFix)).bindingDomain! (some 2) fun xs _ => do
let x := xs[0]!
-- Remark: we rename `x` here to make sure we preserve the variable name in the

View File

@@ -17,6 +17,7 @@ public import Lean.Elab.PreDefinition.TerminationMeasure
public import Lean.Elab.PreDefinition.FixedParams
public import Lean.Elab.PreDefinition.WF.Basic
public import Lean.Data.Array
import Lean.Meta.Tactic.Refl
public section

View File

@@ -53,12 +53,6 @@ def wfRecursion (docCtx : LocalContext × LocalInstances) (preDefs : Array PreDe
-- No termination_by here, so use GuessLex to infer one
guessLex preDefs unaryPreDefProcessed fixedParamPerms argsPacker
-- Warn about likely unwanted reducibility attributes
preDefs.forM fun preDef =>
preDef.modifiers.attrs.forM fun a => do
if a.name = `reducible || a.name = `semireducible then
logWarningAt a.stx s!"marking functions defined by well-founded recursion as `{a.name}` is not effective"
let preDefNonRec forallBoundedTelescope unaryPreDef.type fixedParamPerms.numFixed fun fixedArgs type => do
let type whnfForall type
unless type.isForall do
@@ -66,6 +60,14 @@ def wfRecursion (docCtx : LocalContext × LocalInstances) (preDefs : Array PreDe
let packedArgType := type.bindingDomain!
elabWFRel (preDefs.map (·.declName)) unaryPreDef.declName fixedParamPerms fixedArgs argsPacker packedArgType wf fun wfRel => do
trace[Elab.definition.wf] "wfRel: {wfRel}"
let useNatRec := ( isNatLtWF wfRel).isSome
-- Warn about likely unwanted reducibility attributes
unless useNatRec do
preDefs.forM fun preDef =>
preDef.modifiers.attrs.forM fun a => do
if a.name = `reducible || a.name = `semireducible then
logWarningAt a.stx s!"marking functions defined by well-founded recursion as `{a.name}` is not effective"
let (value, envNew) withoutModifyingEnv' do
addAsAxiom unaryPreDef
let value mkFix unaryPreDefProcessed fixedArgs argsPacker wfRel (preDefs.map (·.declName)) (preDefs.map (·.termination.decreasingBy?))

View File

@@ -36,9 +36,14 @@ def rwFixEq (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
-- lhs should be an application of the declNameNonrec, which unfolds to an
-- application of fix in one step
let some lhs' delta? lhs | throwError "rwFixEq: cannot delta-reduce {lhs}"
let_expr WellFounded.fix _α _C _r _hwf F x := lhs'
| throwTacticEx `rwFixEq mvarId "expected saturated fixed-point application in {lhs'}"
let h := mkAppN (mkConst ``WellFounded.fix_eq lhs'.getAppFn.constLevels!) lhs'.getAppArgs
let h match_expr lhs' with
| WellFounded.fix _α _C _r _hwf _F _x =>
pure <| mkAppN (mkConst ``WellFounded.fix_eq lhs'.getAppFn.constLevels!) lhs'.getAppArgs
| WellFounded.Nat.fix _α _C _motive _F _x =>
pure <| mkAppN (mkConst ``WellFounded.Nat.fix_eq lhs'.getAppFn.constLevels!) lhs'.getAppArgs
| _ => throwTacticEx `rwFixEq mvarId m!"expected saturated fixed-point application in {lhs'}"
let F := lhs'.appFn!.appArg!
let x := lhs'.appArg!
-- We used to just rewrite with `fix_eq` and continue with whatever RHS that produces, but that
-- would include more copies of `fix` resulting in large and confusing terms.

View File

@@ -12,6 +12,7 @@ public import Lean.Util.OccursCheck
public import Lean.Elab.Tactic.Basic
public import Lean.Meta.AbstractNestedProofs
public import Init.Data.List.Sort.Basic
import all Lean.Elab.ErrorUtils
public section
@@ -209,33 +210,6 @@ private def synthesizeUsingDefault : TermElabM Bool := do
return true
return false
/--
Translate zero-based indexes (0, 1, 2, ...) to ordinals ("first", "second",
"third", ...). Not appropriate for numbers that could conceivably be larger
than 19 in real examples.
-/
private def toOrdinalString : Nat -> String
| 0 => "first"
| 1 => "second"
| 2 => "third"
| 3 => "fourth"
| 4 => "fifth"
| n => s!"{n+1}th"
/-- Make an oxford-comma-separated list of strings. -/
private def toOxford : List String -> String
| [] => ""
| [a] => a
| [a, b] => a ++ " and " ++ b
| [a, b, c] => a ++ ", " ++ b ++ ", and " ++ c
| a :: as => a ++ ", " ++ toOxford as
/- Give alternative forms of a string if the `count` is 1 or not. -/
private def _root_.Nat.plural (count : Nat) (singular : String) (plural : String) :=
if count = 1 then
singular
else
plural
def explainStuckTypeclassProblem (typeclassProblem : Expr) : TermElabM (Option MessageData) := do
@@ -296,7 +270,7 @@ def explainStuckTypeclassProblem (typeclassProblem : Expr) : TermElabM (Option M
if args.length = 1 then
"the type argument"
else
s!"the {toOxford (stuckArguments.toList.map toOrdinalString)} type {nStuck.plural "argument" "arguments"}"
s!"the {(stuckArguments.toList.map (·.succ.toOrdinal)).toOxford} type {nStuck.plural "argument" "arguments"}"
return .some (.note m!"Lean will not try to resolve this typeclass instance problem because {theTypeArguments} to `{.ofConstName name}` {containMVars}. {nStuck.plural "This argument" "These arguments"} must be fully determined before Lean will try to resolve the typeclass."
++ .hint' m!"Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `{MessageData.ofConstName ``Nat}`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.")

View File

@@ -9,6 +9,7 @@ prelude
public import Lean.Meta.Tactic.FunInd
public import Lean.Meta.Match.MatcherApp.Transform
import Lean.Meta.Tactic.Simp.Rewrite
import Lean.Meta.Tactic.Assumption
public section

View File

@@ -46,7 +46,7 @@ def withExtHyps (struct : Name) (flat : Bool)
throwError "Internal error when constructing `ext` hypotheses: `{struct}` is not a structure"
let structC mkConstWithLevelParams struct
forallTelescope ( inferType structC) fun params _ => do
withNewBinderInfos (params.map (·.fvarId!, BinderInfo.implicit)) do
withImplicitBinderInfos params do
withLocalDecl `x .implicit (mkAppN structC params) fun x => do
withLocalDecl `y .implicit (mkAppN structC params) fun y => do
let mut hyps := #[]

View File

@@ -282,10 +282,13 @@ def tryTactic (tac : GrindTacticM α) : GrindTacticM Bool := do
open Grind
/-
**Note**: Recall that `grind` uses the reducibility specified at `Config.reducible`
-/
def liftGrindM (k : GrindM α) : GrindTacticM α := do
let ctx read
let s get
let (a, state) liftMetaM <| k ctx.methods.toMethodsRef ctx.ctx |>.run s.state
let (a, state) liftMetaM <| (Grind.withGTransparency k) ctx.methods.toMethodsRef ctx.ctx |>.run s.state
modify fun s => { s with state }
return a

View File

@@ -342,10 +342,10 @@ def evalGrindTraceCore (stx : Syntax) (trace := true) (verbose := true) (useSorr
-- let saved ← saveState
match ( finish.run goal) with
| .closed seq =>
let configCtx' := filterSuggestionsFromGrindConfig configStx
let tacs Grind.mkGrindOnlyTactics configCtx' seq
let configStx' := filterSuggestionsFromGrindConfig configStx
let tacs Grind.mkGrindOnlyTactics configStx' seq
let seq := Grind.Action.mkGrindSeq seq
let tac `(tactic| grind => $seq:grindSeq)
let tac `(tactic| grind $configStx':optConfig => $seq:grindSeq)
let tacs := tacs.push tac
return tacs
| .stuck gs =>

View File

@@ -9,6 +9,7 @@ prelude
public import Lean.Meta.Tactic.LibrarySearch
public import Lean.Meta.Tactic.TryThis
public import Lean.Elab.Tactic.ElabTerm
public import Lean.Elab.Tactic.Config
public section
@@ -17,23 +18,27 @@ namespace Lean.Elab.LibrarySearch
open Lean Meta LibrarySearch
open Elab Tactic Term TryThis
declare_config_elab elabLibrarySearchConfig Parser.Tactic.LibrarySearchConfig
/--
Implementation of the `exact?` tactic.
* `ref` contains the input syntax and is used for locations in error reporting.
* `config` contains configuration options (e.g., `grind` for using grind as a discharger).
* `required` contains an optional list of terms that should be used in closing the goal.
* `requireClose` indicates if the goal must be closed.
It is `true` for `exact?` and `false` for `apply?`.
-/
def exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireClose : Bool) :
def exact? (ref : Syntax) (config : Parser.Tactic.LibrarySearchConfig)
(required : Option (Array (TSyntax `term))) (requireClose : Bool) :
TacticM Unit := do
let mvar getMainGoal
let initialState saveState
let (_, goal) ( getMainGoal).intros
goal.withContext do
let required := ( (required.getD #[]).mapM getFVarId).toList.map .fvar
let tactic := fun exfalso =>
solveByElim required (exfalso := exfalso) (maxDepth := 6)
let tactic := fun goals =>
solveByElim required (exfalso := false) goals (maxDepth := 6) (grind := config.grind) (try? := config.try?)
let allowFailure := fun g => do
let g g.withContext (instantiateMVars (.mvar g))
return required.all fun e => e.occurs g
@@ -56,16 +61,18 @@ def exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireCl
@[builtin_tactic Lean.Parser.Tactic.exact?]
def evalExact : Tactic := fun stx => do
let `(tactic| exact? $[using $[$required],*]?) := stx
let `(tactic| exact? $cfg:optConfig $[using $[$required],*]?) := stx
| throwUnsupportedSyntax
exact? ( getRef) required true
let config elabLibrarySearchConfig cfg
exact? ( getRef) config required true
@[builtin_tactic Lean.Parser.Tactic.apply?]
def evalApply : Tactic := fun stx => do
let `(tactic| apply? $[using $[$required],*]?) := stx
let `(tactic| apply? $cfg:optConfig $[using $[$required],*]?) := stx
| throwUnsupportedSyntax
exact? ( getRef) required false
let config elabLibrarySearchConfig cfg
exact? ( getRef) config required false
@[builtin_term_elab Lean.Parser.Syntax.exact?]
def elabExact?Term : TermElab := fun stx expectedType? => do

View File

@@ -8,6 +8,7 @@ module
prelude
public import Lean.Meta.Tactic.SolveByElim
public import Lean.Elab.Tactic.Config
public import Lean.LibrarySuggestions.Basic
public section
@@ -108,6 +109,21 @@ def evalSolveByElim : Tactic
else
pure [ getMainGoal]
let cfg elabConfig cfg
-- Add library suggestions if +suggestions is enabled
let add if cfg.suggestions then
let mainGoal getMainGoal
let suggestions LibrarySuggestions.select mainGoal { caller := some "solve_by_elim" }
let suggestionTerms suggestions.toList.filterMapM fun s => do
-- Only include suggestions for constants that exist
let env getEnv
if env.contains s.name then
let ident := mkCIdentFrom ( getRef) s.name (canonical := true)
return some (ident : Term)
else
return none
pure (add ++ suggestionTerms)
else
pure add
let [] processSyntax cfg o.isSome star add remove use goals |
throwError "Internal error: `solve_by_elim` unexpectedly returned subgoals"
pure ()

View File

@@ -61,7 +61,7 @@ def evalSuggestExact : TacticM (TSyntax `tactic) := do
let mvarId :: mvarIds getGoals
| throwError "no goals"
mvarId.withContext do
let tactic := fun exfalso => LibrarySearch.solveByElim [] (exfalso := exfalso) (maxDepth := 6)
let tactic := fun goals => LibrarySearch.solveByElim [] (exfalso := false) goals (maxDepth := 6)
let allowFailure := fun _ => return false
let .none LibrarySearch.librarySearch mvarId tactic allowFailure
| throwError "`exact?` failed"
@@ -886,7 +886,7 @@ private def mkAtomicWithSuggestionsStx : CoreM (TSyntax `tactic) :=
/-- `simple` tactics -/
private def mkSimpleTacStx : CoreM (TSyntax `tactic) :=
`(tactic| attempt_all | rfl | assumption)
`(tactic| first | (attempt_all | rfl | assumption) | solve_by_elim)
/-! Function induction generators -/

View File

@@ -1119,10 +1119,27 @@ If the `trace.Meta.synthInstance` option is not already set, gives a hint explai
def useTraceSynthMsg : MessageData :=
MessageData.lazy fun ctx =>
if trace.Meta.synthInstance.get ctx.opts then
pure ""
pure .nil
else
pure <| .hint' s!"Type class instance resolution failures can be inspected with the `set_option {trace.Meta.synthInstance.name} true` command."
builtin_initialize derivableRef : IO.Ref NameSet IO.mkRef {}
/--
Registers a deriving handler for the purpose of error message delivery in `synthesizeInstMVarCore`.
This should only be called by `Lean.Elab.Term.registerDerivingHandler`.
-/
def registerDerivableClass (className : Name) : IO Unit := do
unless ( initializing) do
throw (IO.userError "failed to register derivable class, it can only be registered during initialization")
derivableRef.modify fun m => m.insert className
/--
Returns whether `className` has a `deriving` handler installed.
-/
def hasDerivingHandler (className : Name) : IO Bool := do
return ( derivableRef.get).contains className
/--
Try to synthesize metavariable using type class resolution.
This method assumes the local context and local instances of `instMVar` coincide
@@ -1181,7 +1198,16 @@ def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := n
if ( read).ignoreTCFailures then
return false
else
throwNamedError lean.synthInstanceFailed "failed to synthesize instance of type class{indentExpr type}{extraErrorMsg}{useTraceSynthMsg}"
let msg match type with
| .app (.const cls _) (.const typ _) =>
-- This has the structure of a `deriving`-style type class, alter feedback accordingly
if hasDerivingHandler cls then
pure <| extraErrorMsg ++ .hint' m!"Adding the command `deriving instance {cls} for {typ}` may allow Lean to derive the missing instance."
else
pure <| extraErrorMsg ++ useTraceSynthMsg
| _ =>
pure <| extraErrorMsg ++ useTraceSynthMsg
throwNamedError lean.synthInstanceFailed "failed to synthesize instance of type class{indentExpr type}{msg}"
def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgHeader? : Option String := none)
(mkErrorMsg? : Option (MVarId (expectedType e : Expr) MetaM MessageData) := none)
@@ -2143,6 +2169,16 @@ def exprToSyntax (e : Expr) : TermElabM Term := withFreshMacroScope do
mvar.mvarId!.assign e
return result
def hintAutoImplicitFailure (exp : Expr) (expected := "a function") : TermElabM MessageData := do
let autoBound := ( readThe Context).autoBoundImplicitContext
unless autoBound.isSome && exp.isFVar && autoBound.get!.boundVariables.any (· == exp) do
return .nil
return .hint' m!"The identifier `{.ofName (← exp.fvarId!.getUserName)}` is unknown, \
and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly \
bound variable with an unknown type. \
However, the unknown type cannot be {expected}, and {expected} is what Lean expects here. \
This is often the result of a typo or a missing `import` or `open` statement."
end Term
open Term in

View File

@@ -154,6 +154,7 @@ deriving Inhabited, BEq, Repr
structure EffectiveImport extends Import where
/-- Phases for which the import's IR is available. -/
irPhases : IRPhases
deriving Inhabited
/-- Environment fields that are not used often. -/
structure EnvironmentHeader where

View File

@@ -8,11 +8,13 @@ module
prelude
public import Lean.ErrorExplanations.CtorResultingTypeMismatch
public import Lean.ErrorExplanations.DependsOnNoncomputable
public import Lean.ErrorExplanations.InductionWithNoAlts
public import Lean.ErrorExplanations.InductiveParamMismatch
public import Lean.ErrorExplanations.InductiveParamMissing
public import Lean.ErrorExplanations.InferBinderTypeFailed
public import Lean.ErrorExplanations.InferDefTypeFailed
public import Lean.ErrorExplanations.InvalidDottedIdent
public import Lean.ErrorExplanations.InvalidField
public import Lean.ErrorExplanations.ProjNonPropFromProp
public import Lean.ErrorExplanations.PropRecLargeElim
public import Lean.ErrorExplanations.RedundantMatchAlt

View File

@@ -0,0 +1,99 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rob Simmons
-/
module
prelude
public import Lean.ErrorExplanation
meta import Lean.ErrorExplanation
/--
This error indicates that an expression containing a dot followed by an identifier was encountered,
and that it wasn't possible to understand the identifier as a field.
Lean's field notation is very powerful, but this can also make it confusing: the expression
`color.value` can either be a single [identifier](lean-manual://section/identifiers-and-resolution),
it can be a reference to the [field of a structure](lean-manual://section/structure-fiels), and it
and be a calling a function on the value `color` with
[generalized field notation](lean-manual://section/generalized-field-notation).
# Examples
## Incorrect Field Name
```lean broken
#eval (4 + 2).suc
```
```output
Invalid field `suc`: The environment does not contain `Nat.suc`, so it is not possible to project the field `suc` from an expression
4 + 2
of type `Nat`
```
```lean fixed
#eval (4 + 1).succ
```
The simplest reason for an invalid field error is that the function being sought, like `Nat.suc`,
does not exist.
## Projecting from the Wrong Expression
```lean broken
#eval '>'.leftpad 10 ['a', 'b', 'c']
```
```output
Invalid field `leftpad`: The environment does not contain `Char.leftpad`, so it is not possible to project the field `leftpad` from an expression
'>'
of type `Char`
```
```lean fixed
#eval ['a', 'b', 'c'].leftpad 10 '>'
```
The type of the expression before the dot entirely determines the function being called by the field
projection. There is no `Char.leftpad`, and the only way to invoke `List.leftpad` with generalized
field notation is to have the list come before the dot.
## Type is Not Specific
```lean broken
def double_plus_one {α} [Add α] (x : α) :=
(x + x).succ
```
```output
Invalid field notation: Field projection operates on types of the form `C ...` where C is a constant. The expression
x + x
has type `α` which does not have the necessary form.
```
```lean fixed
def double_plus_one (x : Nat) :=
(x + x).succ
```
The `Add` typeclass is sufficient for performing the addition `x + x`, but the `.succ` field notation
cannot operate without knowing more about the actual type from which `succ` is being projected.
## Insufficient Type Information
```lean broken
example := fun (n) => n.succ.succ
```
```output
Invalid field notation: Type of
n
is not known; cannot resolve field `succ`
```
```lean fixed
example := fun (n : Nat) => n.succ.succ
```
Generalized field notation can only be used when it is possible to determine the type that is being
projected. Type annotations may need to be added to make generalized field notation work.
-/
register_error_explanation lean.invalidField {
summary := "Dotted identifier notation used without ."
sinceVersion := "4.22.0"
}

View File

@@ -49,7 +49,7 @@ The binary operation `+` is associated with the `HAdd` type class, and there's n
strings. The binary operation `++`, associated with the `HAppend` type class, is the correct way to
append strings.
## Modifying the Type of an Argument
## Arguments Have the Wrong Type
```lean broken
def x : Int := 3
@@ -69,6 +69,55 @@ def x : Int := 3
Lean does not allow integers and strings to be added directly. The function `ToString.toString` uses
type class overloading to convert values to strings; by successfully searching for an instance of
`ToString Int`, the second example will succeed.
## Missing Type Class Instance
```lean broken
inductive MyColor where
| chartreuse | sienna | thistle
def forceColor (oc : Option MyColor) :=
oc.get!
```
```output
failed to synthesize instance of type class
Inhabited MyColor
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
```
```lean fixed (title := "Fixed (derive instance when defining type)")
inductive MyColor where
| chartreuse | sienna | thistle
deriving Inhabited
def forceColor (oc : Option MyColor) :=
oc.get!
```
```lean fixed (title := "Fixed (derive instance separately)")
inductive MyColor where
| chartreuse | sienna | thistle
deriving instance Inhabited for MyColor
def forceColor (oc : Option MyColor) :=
oc.get!
```
```lean fixed (title := "Fixed (define instance)")
inductive MyColor where
| chartreuse | sienna | thistle
instance : Inhabited MyColor where
default := .sienna
def forceColor (oc : Option MyColor) :=
oc.get!
```
Type class synthesis can fail because an instance of the type class simply needs to be provided.
This commonly happens for type classes like `Repr`, `BEq`, `ToJson` and `Inhabited`. Lean can often
[automatically generate instances of the type class with the `deriving` keyword](lean-manual://section/type-class),
either when the type is defined or with the stand-alone `deriving` command.
-/
register_error_explanation lean.synthInstanceFailed {
summary := "Failed to synthesize instance of type class"

View File

@@ -952,18 +952,30 @@ def isCharLit : Expr → Bool
| app (const c _) a => c == ``Char.ofNat && a.isRawNatLit
| _ => false
/--
If the expression is a constant, return that name.
Otherwise panic.
-/
def constName! : Expr Name
| const n _ => n
| _ => panic! "constant expected"
/--
If the expression is a constant, return that name.
Otherwise return `Option.none`.
-/
def constName? : Expr Option Name
| const n _ => some n
| _ => none
/-- If the expression is a constant, return that name. Otherwise return `Name.anonymous`. -/
/--
If the expression is a constant, return that name.
Otherwise return `Name.anonymous`.
-/
def constName (e : Expr) : Name :=
e.constName?.getD Name.anonymous
def constLevels! : Expr List Level
| const _ ls => ls
| _ => panic! "constant expected"

View File

@@ -8,6 +8,7 @@ module
prelude
public import Lean.CoreM
public import Lean.Compiler.MetaAttr -- TODO: public because of specializations
import Init.Data.Range.Polymorphic.Stream
/-!
Infrastructure for recording extra import dependencies not implied by the environment constants for
@@ -16,6 +17,41 @@ the benefit of `shake`.
namespace Lean
public structure IndirectModUse where
kind : String
declName : Name
deriving BEq
public builtin_initialize indirectModUseExt : SimplePersistentEnvExtension IndirectModUse (Std.HashMap Name (Array ModuleIdx))
registerSimplePersistentEnvExtension {
addEntryFn s _ := s
addImportedFn es := Id.run do
let mut s := {}
for es in es, modIdx in 0...* do
for e in es do
s := s.alter e.declName (·.getD #[] |>.push modIdx)
return s
asyncMode := .sync
}
public def getIndirectModUses (env : Environment) (modIdx : ModuleIdx) : Array IndirectModUse :=
indirectModUseExt.getModuleEntries env modIdx
variable [Monad m] [MonadEnv m] [MonadTrace m] [MonadOptions m] [MonadRef m] [AddMessageContext m]
/--
Lets `shake` know that references to `declName` may also require importing the current module due to
some additional metaprogramming dependency expressed by `kind`. Currently this is always the name of
an attribute applied to `declName`, which is not from the current module, in the current module.
`kind` is not currently used to further filter what references to `declName` require importing the
current module but may in the future.
-/
public def recordIndirectModUse (kind : String) (declName : Name) : m Unit := do
-- We can assume this is called from the main thread only and that the list of entries is short
if !(indirectModUseExt.getEntries (asyncMode := .mainOnly) ( getEnv) |>.contains { kind, declName }) then
trace[extraModUses] "recording indirect mod use of `{declName}` ({kind})"
modifyEnv (indirectModUseExt.addEntry · { kind, declName })
/-- Additional import dependency for elaboration. -/
public structure ExtraModUse where
/-- Dependency's module name. -/
@@ -49,8 +85,6 @@ public def copyExtraModUses (src dest : Environment) : Environment := Id.run do
env := extraModUses.addEntry env entry
env
variable [Monad m] [MonadEnv m] [MonadTrace m] [MonadOptions m] [MonadRef m] [AddMessageContext m]
def recordExtraModUseCore (mod : Name) (isMeta : Bool) (hint : Name := .anonymous) : m Unit := do
let entry := { module := mod, isExported := ( getEnv).isExporting, isMeta }
if !(extraModUses.getState (asyncMode := .local) ( getEnv)).contains entry then
@@ -62,6 +96,9 @@ def recordExtraModUseCore (mod : Name) (isMeta : Bool) (hint : Name := .anonymou
/--
Records an additional import dependency for the current module, using `Environment.isExporting` as
the visibility level.
NOTE: Directly recording a module name does not trigger including indirect dependencies recorded via
`recordIndirectModUse`, prefer `recordExtraModUseFromDecl` instead.
-/
public def recordExtraModUse (modName : Name) (isMeta : Bool) : m Unit := do
if modName != ( getEnv).mainModule then
@@ -78,6 +115,8 @@ public def recordExtraModUseFromDecl (declName : Name) (isMeta : Bool) : m Unit
-- If the declaration itself is already `meta`, no need to mark the import.
let isMeta := isMeta && !isMarkedMeta ( getEnv) declName
recordExtraModUseCore mod.module isMeta (hint := declName)
for modIdx in (indirectModUseExt.getState (asyncMode := .local) env)[declName]?.getD #[] do
recordExtraModUseCore env.header.modules[modIdx]!.module (isMeta := false) (hint := declName)
builtin_initialize isExtraRevModUseExt : SimplePersistentEnvExtension Unit Unit
registerSimplePersistentEnvExtension {

View File

@@ -0,0 +1,86 @@
/-
Copyright (c) 2025 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rob Simmons
-/
module
prelude
public import Lean.Attributes
public import Lean.Exception
public import Lean.Meta.Hint
public import Lean.Elab.DeclModifiers
public import Lean.ResolveName
import all Lean.Elab.ErrorUtils
namespace Lean
set_option doc.verso true
builtin_initialize identifierSuggestionForAttr : ParametricAttribute (Name × Array Name)
registerParametricAttribute {
name := `suggest_for,
descr := "suggest other (incorrect, not-existing) identifiers that someone might use when they actually want this definition",
getParam := fun trueDeclName stx => do
let `(attr| suggest_for $altNames:ident*) := stx
| throwError "Invalid `[suggest_for]` attribute syntax"
let ns := trueDeclName.getPrefix
return (trueDeclName, altNames.map (·.getId))
}
public def getSuggestions [Monad m] [MonadEnv m] (fullName : Name) : m (Array Name) := do
let mut possibleReplacements := #[]
let (_, allSuggestions) := identifierSuggestionForAttr.ext.getState ( getEnv)
for (_, trueName, suggestions) in allSuggestions do
for suggestion in suggestions do
if fullName = suggestion then
possibleReplacements := possibleReplacements.push trueName
return possibleReplacements.qsort (lt := lt)
where
-- Ensure the result of getSuggestions is stable (if arbitrary)
lt : Name -> Name -> Bool
| .anonymous, _ => false
| .str _ _, .anonymous => true
| .num _ _, .anonymous => true
| .str _ _, .num _ _ => true
| .num _ _, .str _ _ => false
| .num a n, .num b m => n < m || n == m && lt a b
| .str a s1, .str b s2 => s1 < s2 || s1 == s2 && lt a b
/--
Throw an unknown constant error message, potentially suggesting alternatives using
{name}`suggest_for` attributes. (Like {name}`throwUnknownConstantAt` but with suggestions.)
The "Unknown constant `<id>`" message will fully qualify the name, whereas the
-/
public def throwUnknownConstantWithSuggestions (constName : Name) : CoreM α := do
let suggestions getSuggestions constName
let ref getRef
let hint if suggestions.size = 0 then
pure MessageData.nil
else
-- Modify suggestions to have the same structure as the user-provided identifier, but only
-- if that doesn't cause ambiguity.
let rawId := ( getRef).getId
let env getEnv
let ns getCurrNamespace
let openDecls getOpenDecls
let modifySuggestion := match constName.eraseSuffix? rawId with
| .none => id
| .some prefixName => fun (suggestion : Name) =>
let candidate := suggestion.replacePrefix prefixName .anonymous
if (ResolveName.resolveGlobalName env {} ns openDecls candidate |>.length) != 1 then
suggestion
else
candidate
let alternative := if h : suggestions.size = 1 then m!"`{.ofConstName suggestions[0]}`" else m!"one of these"
m!"Perhaps you meant {alternative} in place of `{.ofName rawId}`:".hint (suggestions.map fun suggestion =>
let modified := modifySuggestion suggestion
{
suggestion := s!"{modified}",
toCodeActionTitle? := .some (s!"Suggested replacement: {·}"),
diffGranularity := .all,
-- messageData? := .some m!"replace `{.ofName rawId}` with `{.ofName modified}`",
}) ref
throwUnknownIdentifierAt (declHint := constName) ref (m!"Unknown constant `{.ofConstName constName}`" ++ hint)

View File

@@ -300,6 +300,28 @@ structure SetupImportsResult where
/-- Lean plugins to load as part of the environment setup. -/
plugins : Array System.FilePath := #[]
/--
Parses an option value from a string and inserts it into `opts`.
The type of the option is determined from `decl`.
-/
def setOption (opts : Options) (decl : OptionDecl) (name : Name) (val : String) : IO Options := do
match decl.defValue with
| .ofBool _ =>
match val with
| "true" => return opts.insert name true
| "false" => return opts.insert name false
| _ =>
throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
it must be true/false"
| .ofNat _ =>
let some val := val.toNat?
| throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
it must be a natural number"
return opts.insert name val
| .ofString _ => return opts.insert name val
| _ => throw <| .userError s!"invalid -D parameter, configuration option '{name}' \
cannot be set in the command line, use set_option command"
/--
Parses values of options registered during import and left by the C++ frontend as strings.
Removes `weak` prefixes from both parsed and unparsed options and fails if any option names remain
@@ -322,22 +344,7 @@ If the option is defined in a library, use '-D{`weak ++ name}' to set it conditi
let .ofString val := val
| opts' := opts'.insert name val -- Already parsed
match decl.defValue with
| .ofBool _ =>
match val with
| "true" => opts' := opts'.insert name true
| "false" => opts' := opts'.insert name false
| _ =>
throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
it must be true/false"
| .ofNat _ =>
let some val := val.toNat?
| throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
it must be a natural number"
opts' := opts'.insert name val
| .ofString _ => opts' := opts'.insert name val
| _ => throw <| .userError s!"invalid -D parameter, configuration option '{name}' \
cannot be set in the command line, use set_option command"
opts' setOption opts' decl name val
return opts'

View File

@@ -403,9 +403,8 @@ opaque getSelector : MetaM (Option Selector)
def select (m : MVarId) (c : Config := {}) : MetaM (Array Suggestion) := do
let some selector getSelector |
throwError "No library suggestions engine registered. \
(Note that Lean does not provide a default library suggestions engine, \
these must be provided by a downstream library, \
and configured using `set_library_suggestions`.)"
(Add `import Lean.LibrarySuggestions.Default` to use Lean's built-in engine, \
or use `set_library_suggestions` to configure a custom one.)"
selector m c
/-!

View File

@@ -619,18 +619,18 @@ def indentExpr (e : Expr) : MessageData :=
indentD e
/--
Returns the character length of the message when rendered.
Returns the string-formatted version of MessageData.
Note: this is a potentially expensive operation that is only relevant to message data that are
actually rendered. Consider using this function in lazy message data to avoid unnecessary
computation for messages that are not displayed.
-/
private def MessageData.formatLength (ctx : PPContext) (msg : MessageData) : BaseIO Nat := do
private def MessageData.formatExpensively (ctx : PPContext) (msg : MessageData) : BaseIO String := do
let { env, mctx, lctx, opts, currNamespace, openDecls } := ctx
-- Simulate the naming context that will be added to the actual message
let msg := MessageData.withNamingContext { currNamespace, openDecls } msg
let fmt msg.format (some { env, mctx, lctx, opts })
return fmt.pretty.length
return fmt.pretty
/--
@@ -645,7 +645,8 @@ def inlineExpr (e : Expr) (maxInlineLength := 30) : MessageData :=
.lazy
(fun ctx => do
let msg := MessageData.ofExpr e
if ( msg.formatLength ctx) > maxInlineLength then
let render msg.formatExpensively ctx
if render.length > maxInlineLength || render.any (· == '\n') then
return indentD msg ++ "\n"
else
return " `" ++ msg ++ "` ")
@@ -660,7 +661,8 @@ def inlineExprTrailing (e : Expr) (maxInlineLength := 30) : MessageData :=
.lazy
(fun ctx => do
let msg := MessageData.ofExpr e
if ( msg.formatLength ctx) > maxInlineLength then
let render msg.formatExpensively ctx
if render.length > maxInlineLength || render.any (· == '\n') then
return indentD msg
else
return " `" ++ msg ++ "`")

View File

@@ -478,9 +478,9 @@ def mkNoConfusion (target : Expr) (h : Expr) : MetaM Expr := do
let α whnfD α
matchConstInduct α.getAppFn (fun _ => throwAppBuilderException `noConfusion ("inductive type expected" ++ indentExpr α)) fun indVal us => do
let u getLevel target
if let some (ctorA, ys1) constructorApp? a then
if let some (ctorB, ys2) constructorApp? b then
-- Special case for different manifest constructors, where we can use `ctorIdx`
if let some (ctorA, ys1) constructorApp'? a then
if let some (ctorB, ys2) constructorApp'? b then
-- Different constructors: Use use `ctorIdx`
if ctorA.cidx ctorB.cidx then
let ctorIdxName := Name.mkStr indVal.name "ctorIdx"
if ( hasConst ctorIdxName) && ( hasConst `noConfusion_of_Nat) then
@@ -488,36 +488,44 @@ def mkNoConfusion (target : Expr) (h : Expr) : MetaM Expr := do
let v getLevel α
return mkApp2 (mkConst ``False.elim [u]) target <|
mkAppN (mkConst `noConfusion_of_Nat [v]) #[α, ctorIdx, a, b, h]
-- Special case for same constructors, where we can maybe use the per-constructor
-- noConfusion definition with its type already manifest
if ctorA.cidx = ctorB.cidx then
else
throwError "mkNoConfusion: Missing {ctorIdxName} or {`noConfusion_of_Nat}"
else
-- Same constructors: use per-constructor noConfusion
-- Nullary constructors, the construction is trivial
if ctorA.numFields = 0 then
return withLocalDeclD `P target fun P => mkLambdaFVars #[P] P
let noConfusionName := ctorA.name.str "noConfusion"
if ( hasConst noConfusionName) then
let xs := α.getAppArgs[:ctorA.numParams]
let noConfusion := mkAppN (mkConst noConfusionName (u :: us)) xs
let fields1 : Array Expr := ys1[ctorA.numParams:]
let fields2 : Array Expr := ys2[ctorA.numParams:]
let mask occursInCtorTypeMask ctorA.name
assert! mask.size = ctorA.numFields
let mut ok := true
let mut fields2' := #[]
for m in mask, f1 in fields1, f2 in fields2 do
if m then
unless ( isDefEq f1 f2) do
ok := false
break
else
fields2' := fields2'.push f2
if ok then
return mkAppN noConfusion (#[target] ++ fields1 ++ fields2' ++ #[h])
unless ( hasConst noConfusionName) do
throwError "mkNoConfusion: Missing {noConfusionName}"
let noConfusionNameInfo getConstVal noConfusionName
-- Fall back: Use generic theorem
return mkAppN (mkConst (Name.mkStr indVal.name "noConfusion") (u :: us)) (α.getAppArgs ++ #[target, a, b, h])
let xs := α.getAppArgs[:ctorA.numParams]
let noConfusion := mkAppN (mkConst noConfusionName (u :: us)) xs
let fields1 : Array Expr := ys1[ctorA.numParams:]
let fields2 : Array Expr := ys2[ctorA.numParams:]
let mut e := mkAppN noConfusion (#[target] ++ fields1 ++ fields2)
let arity := noConfusionNameInfo.type.getNumHeadForalls
-- Index equalities expected. Can be less than `indVal.numIndices` when this constructor
-- has fixed indices.
assert! arity xs.size + fields1.size + fields2.size + 3
let numIndEqs := arity - (xs.size + fields1.size + fields2.size + 3) -- 3 for `target`, `h` and the continuation
for _ in [:numIndEqs] do
let eq whnf ( whnfForall ( inferType e)).bindingDomain!
if let some (_,i,_,_) := eq.heq? then
e := mkApp e ( mkHEqRefl i)
else if let some (_,i,_) := eq.eq? then
e := mkApp e ( mkEqRefl i)
else
throwError "mkNoConfusion: unexpected equality `{eq}` as next argument to{inlineExpr (← inferType e)}"
let eq := ( whnfForall ( inferType e)).bindingDomain!
if eq.isHEq then
e := mkApp e ( mkHEqOfEq h)
else
e := mkApp e h
return e
throwError "mkNoConfusion: No manifest constructors in {a} = {b}"
/-- Given a `monad` and `e : α`, makes `pure e`.-/
def mkPure (monad : Expr) (e : Expr) : MetaM Expr :=

View File

@@ -1834,6 +1834,9 @@ private def withNewBinderInfosImp (bs : Array (FVarId × BinderInfo)) (k : MetaM
def withNewBinderInfos (bs : Array (FVarId × BinderInfo)) (k : n α) : n α :=
mapMetaM (fun k => withNewBinderInfosImp bs k) k
def withImplicitBinderInfos (bs : Array Expr) (k : n α) : n α :=
withNewBinderInfos (bs.map (·.fvarId!, BinderInfo.implicit)) k
/--
Execute `k` using a local context where any `x` in `xs` that is tagged as
instance implicit is treated as a regular implicit. -/

View File

@@ -26,7 +26,7 @@ It is used in particular by the code generator to replace calls to such function
`cases` construct.
The `getSparseCasesInfo?` function calculates the `CasesInfo` from the type of the declaration, and
makes certian assumptions about their shapes. If this is too fragile, the `sparseCasesOn` env
makes certain assumptions about their shapes. If this is too fragile, the `sparseCasesOn` env
extension could carry more information from which the shape can be calculated..
-/

View File

@@ -339,7 +339,7 @@ where
go (i+1) (rhss.push rhs) (eqs.push none) hyps
| .subsingletonInst =>
-- The `lhs` does not need to instance implicit since it can be inferred from the LHS
withNewBinderInfos #[(lhss[i]!.fvarId!, .implicit)] do
withImplicitBinderInfos #[lhss[i]!] do
let lhs := lhss[i]!
let lhsType inferType lhs
let rhsType := lhsType.replaceFVars (lhss[*...rhss.size]) rhss

View File

@@ -213,7 +213,9 @@ public def mkCasesOnSameCtor (declName : Name) (indName : Name) : MetaM Unit :=
numDiscrs := info.numIndices + 3
altInfos
uElimPos? := some 0
discrInfos := #[{}, {}, {}]}
discrInfos := #[{}, {}, {}]
overlaps := {}
}
-- Compare attributes with `mkMatcherAuxDefinition`
withExporting (isExporting := !isPrivateName declName) do

View File

@@ -46,7 +46,7 @@ public def mkCtorIdx (indName : Name) : MetaM Unit :=
let us := info.levelParams.map mkLevelParam
forallBoundedTelescope info.type (info.numParams + info.numIndices) fun xs _ => do
withNewBinderInfos (xs.map (·.fvarId!, .implicit)) do
withImplicitBinderInfos xs do
let params : Array Expr := xs[:info.numParams]
let indices : Array Expr := xs[info.numParams:]
let indType := mkAppN (mkConst indName us) xs

View File

@@ -10,16 +10,23 @@ public import Lean.Meta.Basic
import Lean.AddDecl
import Lean.Meta.AppBuilder
import Lean.Meta.CompletionName
import Lean.Meta.NatTable
import Lean.Meta.Constructions.CtorIdx
import Lean.Meta.SameCtorUtils
import Lean.Meta.Constructions.CtorIdx
import Lean.Meta.Constructions.CtorElim
import Lean.Meta.Tactic.Subst
namespace Lean
open Meta
def withPrimedNames (xs : Array Expr) (k : MetaM α) : MetaM α := do
let lctx getLCtx
let lctx := lctx.modifyLocalDecls fun decl =>
if xs.contains (mkFVar decl.fvarId) then
decl.setUserName (decl.userName.appendAfter "'")
else
decl
withLCtx lctx ( getLocalInstances) k
/--
Constructs a lambda expression that returns the argument to the `noConfusion` principle for a given
constructor. In particular, returns
@@ -36,6 +43,7 @@ def mkNoConfusionCtorArg (ctorName : Name) (P : Expr) : MetaM Expr := do
forallBoundedTelescope ctorInfo.type ctorInfo.numParams fun xs t => do
forallTelescopeReducing t fun fields1 _ => do
forallTelescopeReducing t fun fields2 _ => do
withPrimedNames fields2 do
let mut t := P
for f1 in fields1.reverse, f2 in fields2.reverse do
if ( isProof f1) then
@@ -87,51 +95,48 @@ def mkNoConfusionType (indName : Name) : MetaM Unit := do
withLocalDeclD `P PType fun P => do
let motive forallTelescope ( whnfD t).bindingDomain! fun ys _ =>
mkLambdaFVars ys PType
let t instantiateForall t #[motive]
let ti instantiateForall t #[motive]
let e := mkApp e motive
forallBoundedTelescope t info.numIndices fun ys t => do
let e := mkAppN e ys
let xType := mkAppN (mkConst indName us) (xs ++ ys)
withLocalDeclD `x1 xType fun x1 => do
withLocalDeclD `x2 xType fun x2 => do
let t instantiateForall t #[x1]
let altTypes arrowDomainsN info.numCtors t
let e := mkApp e x1
let alts altTypes.mapIdxM fun i altType => do
forallTelescope altType fun zs1 _ => do
if useLinearConstruction then
let ctorIdxApp := mkAppN (mkConst (mkCtorIdxName indName) us) (xs ++ ys ++ #[x2])
let alt mkIfNatEq PType (ctorIdxApp) (mkRawNatLit i)
(«else» := fun _ => pure P) fun h => do
let conName := info.ctors[i]!
let withName := mkConstructorElimName indName conName
let e := mkConst withName (v.succ :: us)
let e := mkAppN e (xs ++ #[motive] ++ ys ++ #[x2, h])
let e := mkApp e <|
forallTelescopeReducing (( whnf ( inferType e)).bindingDomain!) fun zs2 _ => do
let k := ( mkNoConfusionCtorArg conName P).beta (xs ++ zs1 ++ zs2)
let t mkArrow k P
mkLambdaFVars zs2 t
pure e
mkLambdaFVars zs1 alt
else
forallBoundedTelescope ti (some (info.numIndices + 1)) fun ysx1 t => do -- indices and major
forallBoundedTelescope ti (some (info.numIndices + 1)) fun ysx2 _ => do -- indices and major
withPrimedNames ysx2 do
let e := mkAppN e ysx1
let altTypes arrowDomainsN info.numCtors t
let alts altTypes.mapIdxM fun i altType => do
forallTelescope altType fun zs1 _ => do
if useLinearConstruction then
let ctorIdxApp := mkAppN (mkConst (mkCtorIdxName indName) us) (xs ++ ysx2)
let alt mkIfNatEq PType (ctorIdxApp) (mkRawNatLit i)
(«else» := fun _ => pure P) fun h => do
let conName := info.ctors[i]!
let alt := mkConst casesOnName (v.succ :: us)
let alt := mkAppN alt (xs ++ #[motive] ++ ys ++ #[x2])
let t2 inferType alt
let altTypes2 arrowDomainsN info.numCtors t2
let alts2 altTypes2.mapIdxM fun j altType2 => do
forallTelescope altType2 fun zs2 _ => do
if i = j then
let k := ( mkNoConfusionCtorArg conName P).beta (xs ++ zs1 ++ zs2)
let t mkArrow k P
mkLambdaFVars zs2 t
else
mkLambdaFVars zs2 P
let alt := mkAppN alt alts2
mkLambdaFVars zs1 alt
let e := mkAppN e alts
mkLambdaFVars (xs ++ ys ++ #[P, x1, x2]) e
let withName := mkConstructorElimName indName conName
let e := mkConst withName (v.succ :: us)
let e := mkAppN e (xs ++ #[motive] ++ ysx2 ++ #[h])
let e := mkApp e <|
forallTelescopeReducing (( whnf ( inferType e)).bindingDomain!) fun zs2 _ => do
let k := ( mkNoConfusionCtorArg conName P).beta (xs ++ zs1 ++ zs2)
let t mkArrow k P
mkLambdaFVars zs2 t
pure e
mkLambdaFVars zs1 alt
else
let conName := info.ctors[i]!
let alt := mkConst casesOnName (v.succ :: us)
let alt := mkAppN alt (xs ++ #[motive] ++ ysx2)
let t2 inferType alt
let altTypes2 arrowDomainsN info.numCtors t2
let alts2 altTypes2.mapIdxM fun j altType2 => do
forallTelescope altType2 fun zs2 _ => do
if i = j then
let k := ( mkNoConfusionCtorArg conName P).beta (xs ++ zs1 ++ zs2)
let t mkArrow k P
mkLambdaFVars zs2 t
else
mkLambdaFVars zs2 P
let alt := mkAppN alt alts2
mkLambdaFVars zs1 alt
let e := mkAppN e alts
mkLambdaFVars (xs ++ #[P] ++ ysx1 ++ ysx2) e
addDecl (.defnDecl ( mkDefinitionValInferringUnsafe
(name := declName)
@@ -144,46 +149,106 @@ def mkNoConfusionType (indName : Name) : MetaM Unit := do
modifyEnv fun env => addProtected env declName
setReducibleAttribute declName
/--
Given arrays `x1,x2,..,xn` and `y1,y2,..,yn`, bring fresh variables and expressions of types `x1 = y1`, `x2 = y2`,
.., `xn = yn` (using `HEq` where necessary) into scope.
-/
def withEqTelescope [Inhabited α] (xs ys : Array Expr) (k : Array Expr MetaM α) : MetaM α := do
go xs.toList ys.toList #[]
where
go | x::xs', y::ys', eqs => do
let eq mkEqHEq x y
let name := if xs.size > 1 then (`eq).appendIndexAfter (eqs.size + 1) else `eq
withLocalDeclD name eq fun v =>
go xs' ys' (eqs.push v)
| _, _, eqs => k eqs
/-
Variant of `withEqTelescope`, but when `xi = yi`, no variable is introduced, and `Eq.refl` is used
for the expression, unless this is the last one. (This special case could be dropped if we do not
generate no-confusion principles for constructors with only prop-valued fields.)
-/
def withNeededEqTelescope [Inhabited α] (xs ys : Array Expr) (k : Array Expr Array Expr MetaM α) : MetaM α := do
go xs.toList ys.toList #[] #[]
where
go | x::xs', y::ys', vs, eqs => do
if !xs'.isEmpty && ( isDefEq x y) then
let eq mkEqRefl x
go xs' ys' vs (eqs.push eq)
else
let eq mkEqHEq x y
let name := if xs.size > 1 then (`eq).appendIndexAfter (eqs.size + 1) else `eq
withLocalDeclD name eq fun v =>
go xs' ys' (vs.push v) (eqs.push v)
| _, _, vs, eqs => k vs eqs
/--
Telescoping `mkEqNDRec`: given
* motive `∀ y1 .. yn, P y1 .. yn`
* expression of type `P x1 .. xn`
* produces an expression of type (x1 = y1) → .. → (xn = yn) → P y1 .. yn
(possibly using `HEq`)
produce an expression of type `motive y1 … yn`
by repeatedly applying `Eq.ndRec` (and `eq_of_heq` if needed).
-/
def mkEqNDRecTelescope (motive : Expr) (e : Expr) (xs ys : Array Expr) : MetaM Expr := do
trace[Meta.mkNoConfusion] m!"mkEqNDRecTelescope: {e}, xs = {xs}, ys = {ys}"
assert! xs.size == ys.size
withEqTelescope xs ys fun eqs => do
let result mkFreshExprMVar (motive.beta ys)
let mut mvarId := result.mvarId!
let mut subst := {}
for eq in eqs do
-- TODO: Can we build this easily and directly tactic-free?
let eq := subst.get eq.fvarId!
mvarId.withContext do trace[Meta.mkNoConfusion] m!"substituting {eq}"
let (subst', mvarId') Meta.substEq mvarId eq.fvarId! (fvarSubst := subst)
subst := subst'
mvarId := mvarId'
let e := e.applyFVarSubst subst
mvarId.withContext do trace[Meta.mkNoConfusion] m!"assigning {e} : {← inferType e} to\n{mvarId}"
mvarId.assign e
mkLambdaFVars eqs ( instantiateMVars result)
def mkNoConfusionCoreImp (indName : Name) : MetaM Unit := do
let declName := Name.mkStr indName "noConfusion"
let noConfusionTypeName := Name.mkStr indName "noConfusionType"
let noConfusionTypeName := mkNoConfusionTypeName indName
let ConstantInfo.inductInfo info getConstInfo indName | unreachable!
let casesOnName := mkCasesOnName indName
let casesOnInfo getConstVal casesOnName
let v::us := casesOnInfo.levelParams.map mkLevelParam | panic! "unexpected universe levels on `casesOn`"
let e forallBoundedTelescope ( inferType (mkConst noConfusionTypeName (v::us))) (info.numParams + info.numIndices) fun xs _ => do
trace[Meta.mkNoConfusion] m!"mkNoConfusionCoreImp for {declName}"
let e forallBoundedTelescope ( inferType (mkConst noConfusionTypeName (v::us))) (some (info.numParams + 1)) fun xs t => do
let params : Array Expr := xs[:info.numParams]
let is : Array Expr := xs[info.numParams:]
let PType := mkSort v
withLocalDecl `P .implicit PType fun P =>
withLocalDecl `x1 .implicit (mkAppN (mkConst indName us) xs) fun x1 =>
withLocalDecl `x2 .implicit (mkAppN (mkConst indName us) xs) fun x2 => do
withLocalDeclD `h12 ( mkEq x1 x2) fun h12 => do
let target1 := mkAppN (mkConst noConfusionTypeName (v :: us)) (xs ++ #[P, x1, x1])
let motive1 mkLambdaFVars (is ++ #[x1]) target1
let e withLocalDeclD `h11 ( mkEq x1 x1) fun h11 => do
let alts info.ctors.mapM fun ctor => do
let ctorType inferType (mkAppN (mkConst ctor us) params)
forallTelescopeReducing ctorType fun fs _ => do
let kType := ( mkNoConfusionCtorArg ctor P).beta (params ++ fs ++ fs)
withLocalDeclD `k kType fun k => do
let mut e := k
let eqns arrowDomainsN kType.getNumHeadForalls kType
for eqn in eqns do
if let some (_, x, _) := eqn.eq? then
e := mkApp e ( mkEqRefl x)
else if let some (_, x, _, _) := eqn.heq? then
e := mkApp e ( mkHEqRefl x)
else
throwError "unexpected equation {eqn} in `mkNoConfusionCtorArg` for {ctor}"
mkLambdaFVars (fs ++ #[k]) e
let e := mkAppN (mkConst casesOnName (v :: us)) (params ++ #[motive1] ++ is ++ #[x1] ++ alts)
mkLambdaFVars #[h11] e
let target2 := mkAppN (mkConst noConfusionTypeName (v :: us)) (xs ++ #[P, x1, x2])
let motive2 mkLambdaFVars #[x2] ( mkArrow ( mkEq x1 x2) target2)
let e mkEqNDRec motive2 e h12
let e := mkApp e h12
mkLambdaFVars (xs ++ #[P, x1, x2, h12]) e
let P := xs[info.numParams]!
forallBoundedTelescope t (some (info.numIndices + 1)) fun ysx1 _ => do -- indices and major
forallBoundedTelescope t (some (info.numIndices + 1)) fun ysx2 _ => do -- indices and major
withPrimedNames ysx2 do
withImplicitBinderInfos ((ysx1 ++ ysx2).push P) do
let target1 := mkAppN (mkConst noConfusionTypeName (v :: us)) (params ++ #[P] ++ ysx1 ++ ysx1)
let motive1 mkLambdaFVars ysx1 target1
let alts info.ctors.mapM fun ctor => do
let ctorType inferType (mkAppN (mkConst ctor us) params)
forallTelescopeReducing ctorType fun fs _ => do
let kType := ( mkNoConfusionCtorArg ctor P).beta (params ++ fs ++ fs)
withLocalDeclD `k kType fun k => do
let mut e := k
let eqns arrowDomainsN kType.getNumHeadForalls kType
for eqn in eqns do
if let some (_, x, _) := eqn.eq? then
e := mkApp e ( mkEqRefl x)
else if let some (_, x, _, _) := eqn.heq? then
e := mkApp e ( mkHEqRefl x)
else
throwError "unexpected equation {eqn} in `mkNoConfusionCtorArg` for {ctor}"
mkLambdaFVars (fs ++ #[k]) e
let e := mkAppN (mkConst casesOnName (v :: us)) (params ++ #[motive1] ++ ysx1 ++ alts)
let target2 := mkAppN (mkConst noConfusionTypeName (v :: us)) (params ++ #[P] ++ ysx1 ++ ysx2)
let motive2 mkLambdaFVars ysx2 target2
let e mkEqNDRecTelescope motive2 e ysx1 ysx2
mkLambdaFVars (params ++ #[P] ++ ysx1 ++ ysx2) e
addDecl (.defnDecl ( mkDefinitionValInferringUnsafe
(name := declName)
@@ -201,20 +266,19 @@ declaration to equalities between two applications of the same constructor, to e
the computation of `noConfusionType` for that constructor:
```
def L.cons.noConfusion.{u_1, u} : {α : Type u} → (P : Sort u_1)
(x : α)(xs : L α)(x' : α)(xs' : L α)
def L.cons.noConfusion.{u_1, u} : {α : Type u} → {P : Sort u_1}
{x : α}{xs : L α}{x' : α}{xs' : L α}
L.cons x xs = L.cons x' xs' →
(x = x' → xs = xs' → P) →
P
def Vec.cons.noConfusion.{u_1, u} : {α : Type u} → {P : Sort u_1} →
{n : Nat} → {x : α} → {xs : Vec α n} →
{n' : Nat} → {x' : α} → {xs' : Vec α n'} →
n + 1 = n' + 1 → Vec.cons x xs ≍ Vec.cons x' xs' →
(n = n' → x = x' → xs ≍ xs' → P)
→ P
```
These definitions are less expressive than the general `noConfusion` principle when there are
complicated indices. In particular they assume that all fields of the constructor that appear
in its type are equal already. The `mkNoConfusion` app builder falls back to the general principle
if the per-constructor one does not apply.
At some point I tried to be clever and remove hypotheses that are trivial (`n = n →`), but that
made it harder for, say, `injection` to know how often to `intro`. So we just keep them.
-/
def mkNoConfusionCtors (declName : Name) : MetaM Unit := do
-- Do not do anything unless can_elim_to_type.
@@ -231,23 +295,35 @@ def mkNoConfusionCtors (declName : Name) : MetaM Unit := do
for ctor in indVal.ctors do
let ctorInfo getConstInfoCtor ctor
if ctorInfo.numFields > 0 then
let e withLocalDeclD `P (.sort v) fun P =>
forallBoundedTelescope ctorInfo.type ctorInfo.numParams fun xs _ => do
let ctorApp := mkAppN (mkConst ctor us) xs
withSharedCtorIndices ctorApp fun ys indices fields1 fields2 => do
let ctor1 := mkAppN ctorApp fields1
let ctor2 := mkAppN ctorApp fields2
let heqType mkEq ctor1 ctor2
withLocalDeclD `h heqType fun h => do
-- When the kernel checks this definitios, it will perform the potentially expensive
-- computation that `noConfusionType h` is equal to `$kType → P`
let kType mkNoConfusionCtorArg ctor P
let kType := kType.beta (xs ++ fields1 ++ fields2)
withLocalDeclD `k kType fun k => do
let e := mkConst noConfusionName (v :: us)
let e := mkAppN e (xs ++ indices ++ #[P, ctor1, ctor2, h, k])
let e mkExpectedTypeHint e P
mkLambdaFVars (xs ++ #[P] ++ ys ++ #[h, k]) e
let e
forallBoundedTelescope ctorInfo.type ctorInfo.numParams fun xs t => do
withLocalDeclD `P (.sort v) fun P =>
forallBoundedTelescope t ctorInfo.numFields fun fields1 _ => do
forallBoundedTelescope t ctorInfo.numFields fun fields2 _ => do
withPrimedNames fields2 do
withImplicitBinderInfos (xs ++ #[P] ++ fields1 ++ fields2) do
let ctor1 := mkAppN (mkConst ctor us) (xs ++ fields1)
let ctor2 := mkAppN (mkConst ctor us) (xs ++ fields2)
let is1 := ( whnf ( inferType ctor1)).getAppArgsN indVal.numIndices
let is2 := ( whnf ( inferType ctor2)).getAppArgsN indVal.numIndices
withNeededEqTelescope (is1.push ctor1) (is2.push ctor2) fun eqvs eqs => do
-- When the kernel checks this definition, it will perform the potentially expensive
-- computation that `noConfusionType h` is equal to `$kType → P`
let kType mkNoConfusionCtorArg ctor P
let kType := kType.beta (xs ++ fields1 ++ fields2)
withLocalDeclD `k kType fun k => do
let mut e := mkConst noConfusionName (v :: us)
e := mkAppN e (xs ++ #[P] ++ is1 ++ #[ctor1] ++ is2 ++ #[ctor2])
-- eqs may have more Eq rather than HEq than expected by `noConfusion`
for eq in eqs do
let needsHEq := ( whnfForall ( inferType e)).bindingDomain!.isHEq
if needsHEq && ( inferType eq).isEq then
e := mkApp e ( mkHEqOfEq eq)
else
e := mkApp e eq
e := mkApp e k
e mkExpectedTypeHint e P
mkLambdaFVars (xs ++ #[P] ++ fields1 ++ fields2 ++ eqvs ++ #[k]) e
let name := ctor.str "noConfusion"
addDecl (.defnDecl ( mkDefinitionValInferringUnsafe
(name := name)

View File

@@ -150,9 +150,13 @@ def registerGetEqnsFn (f : GetEqnsFn) : IO Unit := do
throw (IO.userError "failed to register equation getter, this kind of extension can only be registered during initialization")
getEqnsFnsRef.modify (f :: ·)
/-- Returns `true` iff `declName` is a definition and its type is not a proposition. -/
/-- Returns `true` iff `declName` is a definition and its type is not a proposition.
Returns `false` for matchers since their equations are handled by `Lean.Meta.Match.MatchEqs`. -/
private def shouldGenerateEqnThms (declName : Name) : MetaM Bool := do
if let some { kind := .defn, sig, .. } := ( getEnv).findAsync? declName then
-- Matcher equations are handled separately in Lean.Meta.Match.MatchEqs
if isMatcherCore ( getEnv) declName then
return false
return !( isProp sig.get.type)
else
return false

View File

@@ -319,7 +319,7 @@ public partial def mkBelowMatcher (matcherApp : MatcherApp) (belowParams : Array
(ctx : RecursionContext) (transformAlt : RecursionContext Expr MetaM Expr) :
MetaM (Option (Expr × MetaM Unit)) :=
withTraceNode `Meta.IndPredBelow.match (return m!"{exceptEmoji ·} {matcherApp.toExpr} and {belowParams}") do
let mut input getMkMatcherInputInContext matcherApp
let mut input getMkMatcherInputInContext matcherApp (unfoldNamed := false)
let mut discrs := matcherApp.discrs
let mut matchTypeAdd := #[] -- #[(discrIdx, ), ...]
let mut i := discrs.size

View File

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Lean.Meta.Basic
import Lean.Meta.Tactic.Refl
@@ -12,9 +11,7 @@ import Lean.Meta.Tactic.Cases
import Lean.Meta.Tactic.Assumption
import Lean.Meta.Tactic.Simp.Main
import Lean.Meta.SameCtorUtils
public section
namespace Lean.Meta
private def mkAnd? (args : Array Expr) : Option Expr := Id.run do
@@ -33,20 +30,26 @@ def elimOptParam (type : Expr) : CoreM Expr := do
else
return .continue
private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useEq : Bool) : MetaM (Option Expr) := do
private def mkEqs (args1 args2 : Array Expr) (skipIfPropOrEq : Bool := true) : MetaM (Array Expr) := do
let mut eqs := #[]
for arg1 in args1, arg2 in args2 do
let arg1Type inferType arg1
if !skipIfPropOrEq then
eqs := eqs.push ( mkEqHEq arg1 arg2)
else if !( isProp arg1Type) && arg1 != arg2 then
eqs := eqs.push ( mkEqHEq arg1 arg2)
return eqs
private def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useEq : Bool) : MetaM (Option Expr) := do
let us := ctorVal.levelParams.map mkLevelParam
let type elimOptParam ctorVal.type
forallBoundedTelescope type ctorVal.numParams fun params type =>
forallTelescope type fun args1 resultType => do
let jp (args2 args2New : Array Expr) : MetaM (Option Expr) := do
let k (args2 args2New : Array Expr) : MetaM (Option Expr) := do
let lhs := mkAppN (mkAppN (mkConst ctorVal.name us) params) args1
let rhs := mkAppN (mkAppN (mkConst ctorVal.name us) params) args2
let eq mkEq lhs rhs
let mut eqs := #[]
for arg1 in args1, arg2 in args2 do
let arg1Type inferType arg1
if !( isProp arg1Type) && arg1 != arg2 then
eqs := eqs.push ( mkEqHEq arg1 arg2)
let eqs mkEqs args1 args2
if let some andEqs := mkAnd? eqs then
let result if useEq then
mkEq eq andEqs
@@ -57,22 +60,19 @@ private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useE
return none
let rec mkArgs2 (i : Nat) (type : Expr) (args2 args2New : Array Expr) : MetaM (Option Expr) := do
if h : i < args1.size then
match ( whnf type) with
| Expr.forallE n d b _ =>
let arg1 := args1[i]
if occursOrInType ( getLCtx) arg1 resultType then
mkArgs2 (i + 1) (b.instantiate1 arg1) (args2.push arg1) args2New
else
withLocalDecl n (if useEq then BinderInfo.default else BinderInfo.implicit) d fun arg2 =>
mkArgs2 (i + 1) (b.instantiate1 arg2) (args2.push arg2) (args2New.push arg2)
| _ => throwError "unexpected constructor type for `{ctorVal.name}`"
let .forallE n d b _ whnf type | throwError "unexpected constructor type for `{ctorVal.name}`"
let arg1 := args1[i]
if occursOrInType ( getLCtx) arg1 resultType then
mkArgs2 (i + 1) (b.instantiate1 arg1) (args2.push arg1) args2New
else
withLocalDecl n (if useEq then BinderInfo.default else BinderInfo.implicit) d fun arg2 =>
mkArgs2 (i + 1) (b.instantiate1 arg2) (args2.push arg2) (args2New.push arg2)
else
jp args2 args2New
k args2 args2New
if useEq then
mkArgs2 0 type #[] #[]
else
withNewBinderInfos (params.map fun param => (param.fvarId!, BinderInfo.implicit)) <|
withNewBinderInfos (args1.map fun arg1 => (arg1.fvarId!, BinderInfo.implicit)) <|
withImplicitBinderInfos (params ++ args1) do
mkArgs2 0 type #[] #[]
private def mkInjectiveTheoremType? (ctorVal : ConstructorVal) : MetaM (Option Expr) :=
@@ -84,13 +84,16 @@ private def injTheoremFailureHeader (ctorName : Name) : MessageData :=
private def throwInjectiveTheoremFailure {α} (ctorName : Name) (mvarId : MVarId) : MetaM α :=
throwError "{injTheoremFailureHeader ctorName}{indentD <| MessageData.ofGoal mvarId}"
private def splitAndAssumption (mvarId : MVarId) (ctorName : Name) : MetaM Unit := do
( mvarId.splitAnd).forM fun mvarId =>
unless ( mvarId.assumptionCore) do
throwInjectiveTheoremFailure ctorName mvarId
private def solveEqOfCtorEq (ctorName : Name) (mvarId : MVarId) (h : FVarId) : MetaM Unit := do
trace[Meta.injective] "solving injectivity goal for {ctorName} with hypothesis {mkFVar h} at\n{mvarId}"
match ( injection mvarId h) with
| InjectionResult.solved => unreachable!
| InjectionResult.subgoal mvarId .. =>
( mvarId.splitAnd).forM fun mvarId =>
unless ( mvarId.assumptionCore) do
throwInjectiveTheoremFailure ctorName mvarId
| InjectionResult.subgoal mvarId .. => splitAndAssumption mvarId ctorName
private def mkInjectiveTheoremValue (ctorName : Name) (targetType : Expr) : MetaM Expr :=
forallTelescopeReducing targetType fun xs type => do
@@ -102,10 +105,12 @@ def mkInjectiveTheoremNameFor (ctorName : Name) : Name :=
ctorName ++ `inj
private def mkInjectiveTheorem (ctorVal : ConstructorVal) : MetaM Unit := do
let name := mkInjectiveTheoremNameFor ctorVal.name
withTraceNode `Meta.injective (msg := (return m!"{exceptEmoji ·} generating `{name}`")) do
let some type mkInjectiveTheoremType? ctorVal
| return ()
trace[Meta.injective] "type: {type}"
let value mkInjectiveTheoremValue ctorVal.name type
let name := mkInjectiveTheoremNameFor ctorVal.name
addDecl <| Declaration.thmDecl {
name
levelParams := ctorVal.levelParams
@@ -133,10 +138,12 @@ private def mkInjectiveEqTheoremValue (ctorName : Name) (targetType : Expr) : Me
mkLambdaFVars xs mvar
private def mkInjectiveEqTheorem (ctorVal : ConstructorVal) : MetaM Unit := do
let name := mkInjectiveEqTheoremNameFor ctorVal.name
withTraceNode `Meta.injective (msg := (return m!"{exceptEmoji ·} generating `{name}`")) do
let some type mkInjectiveEqTheoremType? ctorVal
| return ()
trace[Meta.injective] "type: {type}"
let value mkInjectiveEqTheoremValue ctorVal.name type
let name := mkInjectiveEqTheoremNameFor ctorVal.name
addDecl <| Declaration.thmDecl {
name
levelParams := ctorVal.levelParams
@@ -154,7 +161,7 @@ register_builtin_option genInjectivity : Bool := {
def mkInjectiveTheorems (declName : Name) : MetaM Unit := do
if ( getEnv).contains ``Eq.propIntro && genInjectivity.get ( getOptions) && !( isInductivePredicate declName) then
withTraceNode `Meta.injective (fun _ => return m!"{declName}") do
withTraceNode `Meta.injective (return m!"{exceptEmoji ·} {declName}") do
let info getConstInfoInduct declName
unless info.isUnsafe do
-- We need to reset the local context here because `solveEqOfCtorEq` uses
@@ -173,4 +180,101 @@ def mkInjectiveTheorems (declName : Name) : MetaM Unit := do
builtin_initialize
registerTraceClass `Meta.injective
def getCtorAppIndices? (ctorApp : Expr) : MetaM (Option (Array Expr)) := do
let type whnfD ( inferType ctorApp)
type.withApp fun typeFn typeArgs => do
let .const declName _ := typeFn | return none
let .inductInfo val getConstInfo declName | return none
if val.numIndices == 0 then return some #[]
return some typeArgs[val.numParams...*].toArray
private structure MkHInjTypeResult where
thmType : Expr
us : List Level
numIndices : Nat
private def mkHInjType? (ctorVal : ConstructorVal) : MetaM (Option MkHInjTypeResult) := do
let us := ctorVal.levelParams.map mkLevelParam
let type elimOptParam ctorVal.type
forallBoundedTelescope type ctorVal.numParams fun params type =>
forallTelescope type fun args1 _ => do
withImplicitBinderInfos (params ++ args1) do
let k (args2 : Array Expr) : MetaM (Option MkHInjTypeResult) := do
let lhs := mkAppN (mkAppN (mkConst ctorVal.name us) params) args1
let rhs := mkAppN (mkAppN (mkConst ctorVal.name us) params) args2
let eq mkEqHEq lhs rhs
let eqs mkEqs args1 args2
if let some andEqs := mkAnd? eqs then
let result mkArrow eq andEqs
let some idxs1 getCtorAppIndices? lhs | return none
let some idxs2 getCtorAppIndices? rhs | return none
-- **Note**: We dot not skip here because the type of `noConfusion` does not.
let idxEqs mkEqs idxs1 idxs2 (skipIfPropOrEq := false)
let result mkArrowN idxEqs result
let thmType mkForallFVars params ( mkForallFVars args1 ( mkForallFVars args2 result))
return some { thmType, us, numIndices := idxs1.size }
else
return none
let rec mkArgs2 (i : Nat) (type : Expr) (args2 : Array Expr) : MetaM (Option MkHInjTypeResult) := do
if h : i < args1.size then
let .forallE n d b _ whnf type | throwError "unexpected constructor type for `{ctorVal.name}`"
let arg1 := args1[i]
withLocalDecl n .implicit d fun arg2 =>
mkArgs2 (i + 1) (b.instantiate1 arg2) (args2.push arg2)
else
k args2
mkArgs2 0 type #[]
private def failedToGenHInj (ctorVal : ConstructorVal) : MetaM α :=
throwError "failed to generate heterogeneous injectivity theorem for `{ctorVal.name}`"
private partial def mkHInjectiveTheoremValue? (ctorVal : ConstructorVal) (typeInfo : MkHInjTypeResult) : MetaM (Option Expr) := do
forallTelescopeReducing typeInfo.thmType fun xs type => do
let noConfusionName := ctorVal.induct.str "noConfusion"
let params := xs[*...ctorVal.numParams]
let noConfusion := mkAppN (mkConst noConfusionName (0 :: typeInfo.us)) params
let noConfusion := mkApp noConfusion type
let n := xs.size - typeInfo.numIndices - 1
let eqs := xs[n...*].toArray
let eqExprs eqs.mapM fun x => do
match_expr ( inferType x) with
| Eq _ lhs rhs => return (lhs, rhs)
| HEq _ lhs _ rhs => return (lhs, rhs)
| _ => failedToGenHInj ctorVal
let (args₁, args₂) := eqExprs.unzip
let noConfusion := mkAppN (mkAppN (mkAppN noConfusion args₁) args₂) eqs
let .forallE _ d _ _ whnf ( inferType noConfusion) | failedToGenHInj ctorVal
let mvar mkFreshExprSyntheticOpaqueMVar d
let noConfusion := mkApp noConfusion mvar
let mvarId := mvar.mvarId!
let (_, mvarId) mvarId.intros
splitAndAssumption mvarId ctorVal.name
let result instantiateMVars noConfusion
mkLambdaFVars xs result
private def hinjSuffix := "hinj"
def mkHInjectiveTheoremNameFor (ctorName : Name) : Name :=
ctorName.str hinjSuffix
private def mkHInjectiveTheorem? (thmName : Name) (ctorVal : ConstructorVal) : MetaM (Option TheoremVal) := do
let some typeInfo mkHInjType? ctorVal | return none
let some value mkHInjectiveTheoremValue? ctorVal typeInfo | return none
return some { name := thmName, value, levelParams := ctorVal.levelParams, type := typeInfo.thmType }
builtin_initialize registerReservedNamePredicate fun env n =>
match n with
| .str p "hinj" => (env.find? p matches some (.ctorInfo _))
| _ => false
builtin_initialize
registerReservedNameAction fun name => do
let .str p "hinj" := name | return false
let some (.ctorInfo ctorVal) := ( getEnv).find? p | return false
MetaM.run' do
let some thmVal mkHInjectiveTheorem? name ctorVal | return false
realizeConst p name do
addDecl ( mkThmOrUnsafeDef thmVal)
return true
end Lean.Meta

View File

@@ -0,0 +1,128 @@
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Lean.Meta.Basic
public import Lean.Meta.Match.MatcherInfo
import Lean.Meta.Match.NamedPatterns
import Lean.Meta.MatchUtil
import Lean.Meta.AppBuilder
public section
/-!
This module has telescope functions for macher alts. They are primariliy used
in `Match.MatchEqs`, but also in `MatcherApp.Transform`, hence the sparate module.
-/
namespace Lean.Meta.Match
/--
Similar to `forallTelescopeReducing`, but
1. Eliminates arguments for named parameters and the associated equation proofs.
2. Instantiate the `Unit` parameter of an otherwise argumentless alternative.
It does not handle the equality parameters associated with the `h : discr` notation.
The continuation `k` takes four arguments `ys args mask type`.
- `ys` are variables for the hypotheses that have not been eliminated.
- `args` are the arguments for the alternative `alt` that has type `altType`. `ys.size <= args.size`
- `mask[i]` is true if the hypotheses has not been eliminated. `mask.size == args.size`.
- `type` is the resulting type for `altType`.
We use the `mask` to build the splitter proof. See `mkSplitterProof`.
This can be used to use the alternative of a match expression in its splitter.
-/
public partial def forallAltVarsTelescope (altType : Expr) (altInfo : AltParamInfo)
(k : (patVars : Array Expr) (args : Array Expr) (mask : Array Bool) (type : Expr) MetaM α) : MetaM α := do
assert! altInfo.numOverlaps = 0
if altInfo.hasUnitThunk then
let type whnfForall altType
let type Match.unfoldNamedPattern type
let type instantiateForall type #[mkConst ``Unit.unit]
k #[] #[mkConst ``Unit.unit] #[false] type
else
go #[] #[] #[] 0 altType
where
go (ys : Array Expr) (args : Array Expr) (mask : Array Bool) (i : Nat) (type : Expr) : MetaM α := do
let type whnfForall type
if i < altInfo.numFields then
let Expr.forallE n d b .. := type
| throwError "expecting {altInfo.numFields} parameters, but found type{indentExpr altType}"
let d Match.unfoldNamedPattern d
withLocalDeclD n d fun y => do
let typeNew := b.instantiate1 y
if let some (_, lhs, rhs) matchEq? d then
if lhs.isFVar && ys.contains lhs && args.contains lhs && isNamedPatternProof typeNew y then
let some j := ys.finIdxOf? lhs | unreachable!
let ys := ys.eraseIdx j
let some k := args.idxOf? lhs | unreachable!
let mask := mask.set! k false
let args := args.map fun arg => if arg == lhs then rhs else arg
let arg mkEqRefl rhs
let typeNew := typeNew.replaceFVar lhs rhs
return withReplaceFVarId lhs.fvarId! rhs do
withReplaceFVarId y.fvarId! arg do
go ys (args.push arg) (mask.push false) (i+1) typeNew
go (ys.push y) (args.push y) (mask.push true) (i+1) typeNew
else
let type Match.unfoldNamedPattern type
k ys args mask type
isNamedPatternProof (type : Expr) (h : Expr) : Bool :=
Option.isSome <| type.find? fun e =>
if let some e := Match.isNamedPattern? e then
e.appArg! == h
else
false
/--
Extension of `forallAltTelescope` that continues further:
Equality parameters associated with the `h : discr` notation are replaced with `rfl` proofs.
Recall that this kind of parameter always occurs after the parameters corresponding to pattern
variables.
The continuation `k` takes four arguments `ys args mask type`.
- `ys` are variables for the hypotheses that have not been eliminated.
- `eqs` are variables for equality hypotheses associated with discriminants annotated with `h : discr`.
- `args` are the arguments for the alternative `alt` that has type `altType`. `ys.size <= args.size`
- `mask[i]` is true if the hypotheses has not been eliminated. `mask.size == args.size`.
- `type` is the resulting type for `altType`.
We use the `mask` to build the splitter proof. See `mkSplitterProof`.
This can be used to use the alternative of a match expression in its splitter.
-/
public partial def forallAltTelescope (altType : Expr) (altInfo : AltParamInfo) (numDiscrEqs : Nat)
(k : (ys : Array Expr) (eqs : Array Expr) (args : Array Expr) (mask : Array Bool) (type : Expr) MetaM α)
: MetaM α := do
forallAltVarsTelescope altType altInfo fun ys args mask altType => do
go ys #[] args mask 0 altType
where
go (ys : Array Expr) (eqs : Array Expr) (args : Array Expr) (mask : Array Bool) (i : Nat) (type : Expr) : MetaM α := do
let type whnfForall type
if i < numDiscrEqs then
let Expr.forallE n d b .. := type
| throwError "expecting {numDiscrEqs} equalities, but found type{indentExpr altType}"
let arg if let some (_, _, rhs) matchEq? d then
mkEqRefl rhs
else if let some (_, _, _, rhs) matchHEq? d then
mkHEqRefl rhs
else
throwError "unexpected match alternative type{indentExpr altType}"
withLocalDeclD n d fun eq => do
let typeNew := b.instantiate1 eq
go ys (eqs.push eq) (args.push arg) (mask.push false) (i+1) typeNew
else
let type unfoldNamedPattern type
k ys eqs args mask type

View File

@@ -6,27 +6,20 @@ Authors: Leonardo de Moura
module
prelude
public import Lean.Meta.Basic
public import Lean.Meta.Tactic.FVarSubst
public import Lean.Meta.CollectFVars
public import Lean.Meta.Match.CaseArraySizes
import Lean.Meta.Match.Value
import Lean.Meta.AppBuilder
import Lean.Meta.Tactic.Util
import Lean.Meta.Tactic.Assert
import Lean.Meta.Tactic.Subst
import Lean.Meta.Match.NamedPatterns
public section
namespace Lean.Meta.Match
def mkNamedPattern (x h p : Expr) : MetaM Expr :=
mkAppM ``namedPattern #[x, p, h]
def isNamedPattern (e : Expr) : Bool :=
let e := e.consumeMData
e.getAppNumArgs == 4 && e.getAppFn.consumeMData.isConstOf ``namedPattern
def isNamedPattern? (e : Expr) : Option Expr :=
let e := e.consumeMData
if e.getAppNumArgs == 4 && e.getAppFn.consumeMData.isConstOf ``namedPattern then
some e
else
none
inductive Pattern : Type where
| inaccessible (e : Expr) : Pattern
| var (fvarId : FVarId) : Pattern
@@ -163,6 +156,11 @@ structure Alt where
After we perform additional case analysis, their types become definitionally equal.
-/
cnstrs : List (Expr × Expr)
/--
Indices of previous alternatives that this alternative expects a not-that-proofs.
(When producing a splitter, and in the future also for source-level overlap hypotheses.)
-/
notAltIdxs : Array Nat
deriving Inhabited
namespace Alt

View File

@@ -6,32 +6,36 @@ Authors: Leonardo de Moura
module
prelude
public import Lean.Meta.Match.CaseValues
public section
public import Lean.Meta.Basic
public import Lean.Meta.Tactic.FVarSubst
import Lean.Meta.Match.CaseValues
import Lean.Meta.AppBuilder
import Lean.Meta.Tactic.Util
import Lean.Meta.Tactic.Assert
import Lean.Meta.Tactic.Subst
namespace Lean.Meta
structure CaseArraySizesSubgoal where
public structure CaseArraySizesSubgoal where
mvarId : MVarId
elems : Array FVarId := #[]
diseqs : Array FVarId := #[]
subst : FVarSubst := {}
deriving Inhabited
def getArrayArgType (a : Expr) : MetaM Expr := do
public def getArrayArgType (a : Expr) : MetaM Expr := do
let aType inferType a
let aType whnfD aType
unless aType.isAppOfArity ``Array 1 do
throwError "array expected{indentExpr a}"
pure aType.appArg!
private def mkArrayGetLit (a : Expr) (i : Nat) (n : Nat) (h : Expr) : MetaM Expr := do
def mkArrayGetLit (a : Expr) (i : Nat) (n : Nat) (h : Expr) : MetaM Expr := do
let lt mkLt (mkRawNatLit i) (mkRawNatLit n)
let ltPrf mkDecideProof lt
mkAppM `Array.getLit #[a, mkRawNatLit i, h, ltPrf]
private partial def introArrayLit (mvarId : MVarId) (a : Expr) (n : Nat) (xNamePrefix : Name) (aSizeEqN : Expr) : MetaM MVarId := do
partial def introArrayLit (mvarId : MVarId) (a : Expr) (n : Nat) (xNamePrefix : Name) (aSizeEqN : Expr) : MetaM MVarId := do
let α getArrayArgType a
let rec loop (i : Nat) (xs : Array Expr) (args : Array Expr) := do
if i < n then
@@ -61,7 +65,7 @@ private partial def introArrayLit (mvarId : MVarId) (a : Expr) (n : Nat) (xNameP
n) `..., x_1 ... x_{sizes[n-1]} |- C #[x_1, ..., x_{sizes[n-1]}]`
n+1) `..., (h_1 : a.size != sizes[0]), ..., (h_n : a.size != sizes[n-1]) |- C a`
where `n = sizes.size` -/
def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNamePrefix := `x) (hNamePrefix := `h) : MetaM (Array CaseArraySizesSubgoal) :=
public def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNamePrefix := `x) (hNamePrefix := `h) : MetaM (Array CaseArraySizesSubgoal) :=
mvarId.withContext do
let a := mkFVar fvarId
let aSize mkAppM `Array.size #[a]
@@ -72,22 +76,20 @@ def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNam
subgoals.mapIdxM fun i subgoal => do
let subst := subgoal.subst
let mvarId := subgoal.mvarId
let hEqSz := (subst.get hEq).fvarId!
if h : i < sizes.size then
let n := sizes[i]
let mvarId mvarId.clear subgoal.newHs[0]!
let mvarId mvarId.clear (subst.get aSizeFVarId).fvarId!
mvarId.withContext do
let hEqSzSymm mkEqSymm (mkFVar hEqSz)
let mvarId introArrayLit mvarId a n xNamePrefix hEqSzSymm
let (xs, mvarId) mvarId.introN n
let (hEqLit, mvarId) mvarId.intro1
let mvarId mvarId.clear hEqSz
let (subst, mvarId) substCore mvarId hEqLit false subst
pure { mvarId := mvarId, elems := xs, subst := subst }
let hEqSz := (subst.get hEq).fvarId!
let n := sizes[i]
mvarId.withContext do
let hEqSzSymm mkEqSymm (mkFVar hEqSz)
let mvarId introArrayLit mvarId a n xNamePrefix hEqSzSymm
let (xs, mvarId) mvarId.introN n
let (hEqLit, mvarId) mvarId.intro1
let mvarId mvarId.clear hEqSz
let (subst, mvarId) substCore mvarId hEqLit (symm := false) subst
pure { mvarId := mvarId, elems := xs, subst := subst }
else
let (subst, mvarId) substCore mvarId hEq false subst
let diseqs := subgoal.newHs.map fun fvarId => (subst.get fvarId).fvarId!
pure { mvarId := mvarId, diseqs := diseqs, subst := subst }
let (subst, mvarId) substCore mvarId hEq (symm := false) subst
let diseqs := subgoal.newHs.map fun fvarId => (subst.get fvarId).fvarId!
pure { mvarId := mvarId, diseqs := diseqs, subst := subst }
end Lean.Meta

View File

@@ -6,28 +6,25 @@ Authors: Leonardo de Moura
module
prelude
public import Lean.Meta.Tactic.Subst
public import Lean.Meta.Match.Value
public section
public import Lean.Meta.Basic
public import Lean.Meta.Tactic.FVarSubst
import Lean.Meta.Tactic.Subst
namespace Lean.Meta
structure CaseValueSubgoal where
mvarId : MVarId
newH : FVarId
subst : FVarSubst := {}
deriving Inhabited
/--
Split goal `... |- C x` into two subgoals
`..., (h : x = value) |- C value`
`..., (h : x = value) |- C x`
`..., (h : x != value) |- C x`
where `fvarId` is `x`s id.
The type of `x` must have decidable equality.
Remark: `subst` field of the second subgoal is equal to the input `subst`. -/
private def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hName : Name := `h) (subst : FVarSubst := {})
-/
def caseValue (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hName : Name := `h)
: MetaM (CaseValueSubgoal × CaseValueSubgoal) :=
mvarId.withContext do
let tag mvarId.getTag
@@ -42,27 +39,16 @@ private def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hNa
let val mkAppOptM `dite #[none, xEqValue, none, thenMVar, elseMVar]
mvarId.assign val
let (elseH, elseMVarId) elseMVar.mvarId!.intro1P
let elseSubgoal := { mvarId := elseMVarId, newH := elseH, subst := subst : CaseValueSubgoal }
let elseSubgoal := { mvarId := elseMVarId, newH := elseH }
let (thenH, thenMVarId) thenMVar.mvarId!.intro1P
let symm := false
let clearH := false
let (thenSubst, thenMVarId) substCore thenMVarId thenH symm subst clearH
thenMVarId.withContext do
trace[Meta] "subst domain: {thenSubst.domain.map (·.name)}"
let thenH := (thenSubst.get thenH).fvarId!
trace[Meta] "searching for decl"
let _ thenH.getDecl
trace[Meta] "found decl"
let thenSubgoal := { mvarId := thenMVarId, newH := (thenSubst.get thenH).fvarId!, subst := thenSubst : CaseValueSubgoal }
let thenSubgoal := { mvarId := thenMVarId, newH := thenH }
pure (thenSubgoal, elseSubgoal)
def caseValue (mvarId : MVarId) (fvarId : FVarId) (value : Expr) : MetaM (CaseValueSubgoal × CaseValueSubgoal) := do
let s caseValueAux mvarId fvarId value
appendTagSuffix s.1.mvarId `thenBranch
appendTagSuffix s.2.mvarId `elseBranch
pure s
structure CaseValuesSubgoal where
public structure CaseValuesSubgoal where
mvarId : MVarId
newHs : Array FVarId := #[]
subst : FVarSubst := {}
@@ -83,22 +69,15 @@ structure CaseValuesSubgoal where
If `substNewEqs = true`, then the new `h_i` equality hypotheses are substituted in the first `n` cases.
-/
def caseValues (mvarId : MVarId) (fvarId : FVarId) (values : Array Expr) (hNamePrefix := `h) (substNewEqs := false) : MetaM (Array CaseValuesSubgoal) :=
public def caseValues (mvarId : MVarId) (fvarId : FVarId) (values : Array Expr) (hNamePrefix := `h) : MetaM (Array CaseValuesSubgoal) :=
let rec loop : Nat MVarId List Expr Array FVarId Array CaseValuesSubgoal MetaM (Array CaseValuesSubgoal)
| _, mvarId, [], _, _ => throwTacticEx `caseValues mvarId "list of values must not be empty"
| i, mvarId, v::vs, hs, subgoals => do
let (thenSubgoal, elseSubgoal) caseValueAux mvarId fvarId v (hNamePrefix.appendIndexAfter i) {}
let (thenSubgoal, elseSubgoal) caseValue mvarId fvarId v (hNamePrefix.appendIndexAfter i)
appendTagSuffix thenSubgoal.mvarId ((`case).appendIndexAfter i)
let thenMVarId hs.foldlM
(fun thenMVarId h => match thenSubgoal.subst.get h with
| Expr.fvar fvarId => thenMVarId.tryClear fvarId
| _ => pure thenMVarId)
thenSubgoal.mvarId
let subgoals if substNewEqs then
let (subst, mvarId) substCore thenMVarId thenSubgoal.newH false thenSubgoal.subst true
pure <| subgoals.push { mvarId := mvarId, newHs := #[], subst := subst }
else
pure <| subgoals.push { mvarId := thenMVarId, newHs := #[thenSubgoal.newH], subst := thenSubgoal.subst }
let thenMVarId thenSubgoal.mvarId.tryClearMany hs
let (subst, mvarId) substCore thenMVarId thenSubgoal.newH (symm := false) {} (clearH := true)
let subgoals := subgoals.push { mvarId := mvarId, newHs := #[], subst := subst }
match vs with
| [] => do
appendTagSuffix elseSubgoal.mvarId ((`case).appendIndexAfter (i+1))

View File

@@ -12,7 +12,13 @@ public import Lean.Meta.GeneralizeTelescope
public import Lean.Meta.Match.Basic
public import Lean.Meta.Match.MatcherApp.Basic
public import Lean.Meta.Match.MVarRenaming
public import Lean.Meta.Match.MVarRenaming
import Lean.Meta.Match.SimpH
import Lean.Meta.Match.SolveOverlap
import Lean.Meta.HasNotBit
import Lean.Meta.Match.CaseArraySizes
import Lean.Meta.Match.CaseValues
import Lean.Meta.Match.NamedPatterns
public section
@@ -92,34 +98,62 @@ where
/-- Given a list of `AltLHS`, create a minor premise for each one, convert them into `Alt`, and then execute `k` -/
private def withAlts {α} (motive : Expr) (discrs : Array Expr) (discrInfos : Array DiscrInfo)
(lhss : List AltLHS) (k : List Alt Array Expr Array AltParamInfo MetaM α) : MetaM α :=
loop lhss [] #[] #[]
(lhss : List AltLHS) (isSplitter : Option Overlaps)
(k : List Alt Array Expr Array AltParamInfo MetaM α) : MetaM α :=
loop lhss [] #[] #[] #[]
where
mkMinorType (xs : Array Expr) (lhs : AltLHS) : MetaM Expr :=
mkSplitterHyps (idx : Nat) (lhs : AltLHS) (notAlts : Array Expr) : MetaM (Array Expr × Array Nat) := do
withExistingLocalDecls lhs.fvarDecls do
let patterns lhs.patterns.toArray.mapM (Pattern.toExpr · (annotate := true))
let mut hs := #[]
let mut notAltIdxs := #[]
for overlappingIdx in isSplitter.get!.overlapping idx do
let notAlt := notAlts[overlappingIdx]!
let h instantiateForall notAlt patterns
if let some h simpH? h patterns.size then
notAltIdxs := notAltIdxs.push overlappingIdx
hs := hs.push h
trace[Meta.Match.debug] "hs for {lhs.ref}: {hs}"
return (hs, notAltIdxs)
mkMinorType (xs : Array Expr) (lhs : AltLHS) (notAltHs : Array Expr): MetaM Expr :=
withExistingLocalDecls lhs.fvarDecls do
let args lhs.patterns.toArray.mapM (Pattern.toExpr · (annotate := true))
let minorType := mkAppN motive args
withEqs discrs args discrInfos fun eqs => do
mkForallFVars (xs ++ eqs) minorType
let minorType mkForallFVars eqs minorType
let minorType mkArrowN notAltHs minorType
mkForallFVars xs minorType
loop (lhss : List AltLHS) (alts : List Alt) (minors : Array Expr) (altInfos : Array AltParamInfo) : MetaM α := do
mkNotAlt (xs : Array Expr) (lhs : AltLHS) : MetaM Expr := do
withExistingLocalDecls lhs.fvarDecls do
let mut notAlt := mkConst ``False
for discr in discrs.reverse, pattern in lhs.patterns.reverse do
notAlt mkArrow ( mkEqHEq discr ( pattern.toExpr)) notAlt
notAlt mkForallFVars (discrs ++ xs) notAlt
return notAlt
loop (lhss : List AltLHS) (alts : List Alt) (minors : Array Expr) (altInfos : Array AltParamInfo) (notAlts : Array Expr) : MetaM α := do
match lhss with
| [] => k alts.reverse minors altInfos
| lhs::lhss =>
let xs := lhs.fvarDecls.toArray.map LocalDecl.toExpr
let minorType mkMinorType xs lhs
let hasParams := !xs.isEmpty || discrInfos.any fun info => info.hName?.isSome
let minorType := if hasParams then minorType else mkSimpleThunkType minorType
let idx := alts.length
let xs := lhs.fvarDecls.toArray.map LocalDecl.toExpr
let (notAltHs, notAltIdxs) if isSplitter.isSome then mkSplitterHyps idx lhs notAlts else pure (#[], #[])
let minorType mkMinorType xs lhs notAltHs
let notAlt mkNotAlt xs lhs
let hasParams := !xs.isEmpty || !notAltHs.isEmpty || discrInfos.any fun info => info.hName?.isSome
let minorType := if hasParams then minorType else mkSimpleThunkType minorType
let minorName := (`h).appendIndexAfter (idx+1)
trace[Meta.Match.debug] "minor premise {minorName} : {minorType}"
withLocalDeclD minorName minorType fun minor => do
let rhs := if hasParams then mkAppN minor xs else mkApp minor (mkConst `Unit.unit)
let minors := minors.push minor
let altInfos := altInfos.push { numFields := xs.size, numOverlaps := 0, hasUnitThunk := !hasParams }
let altInfos := altInfos.push { numFields := xs.size, numOverlaps := notAltHs.size, hasUnitThunk := !hasParams }
let fvarDecls lhs.fvarDecls.mapM instantiateLocalDeclMVars
let alts := { ref := lhs.ref, idx := idx, rhs := rhs, fvarDecls := fvarDecls, patterns := lhs.patterns, cnstrs := [] } :: alts
loop lhss alts minors altInfos
let alt := { ref := lhs.ref, idx := idx, rhs := rhs, fvarDecls := fvarDecls, patterns := lhs.patterns, cnstrs := [], notAltIdxs := notAltIdxs }
let alts := alt :: alts
loop lhss alts minors altInfos (notAlts.push notAlt)
structure State where
/-- Used alternatives -/
@@ -338,7 +372,7 @@ where
return (p, (lhs, rhs) :: cnstrs)
/--
Solve pending alternative constraints.
Solve pending alternative constraints and overlap assumptions.
If all constraints can be solved perform assignment `mvarId := alt.rhs`, else throw error.
-/
private partial def solveCnstrs (mvarId : MVarId) (alt : Alt) : StateRefT State MetaM Unit := do
@@ -350,13 +384,19 @@ where
| none =>
let alt filterTrivialCnstrs alt
if alt.cnstrs.isEmpty then
let eType inferType alt.rhs
let targetType mvarId.getType
unless ( isDefEqGuarded targetType eType) do
trace[Meta.Match.match] "assignGoalOf failed {eType} =?= {targetType}"
throwErrorAt alt.ref "Dependent elimination failed: Type mismatch when solving this alternative: it {← mkHasTypeButIsExpectedMsg eType targetType}"
mvarId.assign alt.rhs
modify fun s => { s with used := s.used.insert alt.idx }
mvarId.withContext do
let eType inferType alt.rhs
let (notAltsMVarIds, _, eType) forallMetaBoundedTelescope eType alt.notAltIdxs.size
unless notAltsMVarIds.size = alt.notAltIdxs.size do
throwErrorAt alt.ref "Incorrect number of overlap hypotheses in the right-hand-side, expected {alt.notAltIdxs.size}:{indentExpr eType}"
let targetType mvarId.getType
unless ( isDefEqGuarded targetType eType) do
trace[Meta.Match.match] "assignGoalOf failed {eType} =?= {targetType}"
throwErrorAt alt.ref "Dependent elimination failed: Type mismatch when solving this alternative: it {← mkHasTypeButIsExpectedMsg eType targetType}"
for notAltMVarId in notAltsMVarIds do
solveOverlap notAltMVarId.mvarId!
mvarId.assign (mkAppN alt.rhs notAltsMVarIds)
modify fun s => { s with used := s.used.insert alt.idx }
else
trace[Meta.Match.match] "alt has unsolved cnstrs:\n{← alt.toMessageData}"
let mut msg := m!"Dependent match elimination failed: Could not solve constraints"
@@ -636,7 +676,7 @@ private def processConstructor (p : Problem) : MetaM (Array Problem) := do
| .var _ :: _ => expandVarIntoCtor alt ctorName
| .inaccessible _ :: _ => processInaccessibleAsCtor alt ctorName
| _ => unreachable!
return { mvarId := subgoal.mvarId, vars := newVars, alts := newAlts, examples := examples }
return { p with mvarId := subgoal.mvarId, vars := newVars, alts := newAlts, examples := examples }
else
-- A catch-all case
let subst := subgoal.subst
@@ -647,7 +687,7 @@ private def processConstructor (p : Problem) : MetaM (Array Problem) := do
| .ctor .. :: _ => false
| _ => true
let newAlts := newAlts.map fun alt => alt.applyFVarSubst subst
return { mvarId := subgoal.mvarId, alts := newAlts, vars := newVars, examples := examples }
return { p with mvarId := subgoal.mvarId, alts := newAlts, vars := newVars, examples := examples }
private def processNonVariable (p : Problem) : MetaM Problem := withGoalOf p do
let x :: xs := p.vars | unreachable!
@@ -686,7 +726,7 @@ private def processValue (p : Problem) : MetaM (Array Problem) := do
trace[Meta.Match.match] "value step"
let x :: xs := p.vars | unreachable!
let values := collectValues p
let subgoals caseValues p.mvarId x.fvarId! values (substNewEqs := true)
let subgoals caseValues p.mvarId x.fvarId! values
subgoals.mapIdxM fun i subgoal => do
trace[Meta.Match.match] "processValue subgoal\n{MessageData.ofGoal subgoal.mvarId}"
if h : i < values.size then
@@ -708,7 +748,7 @@ private def processValue (p : Problem) : MetaM (Array Problem) := do
alt.replaceFVarId fvarId value
| _ => unreachable!
let newVars := xs.map fun x => x.applyFVarSubst subst
return { mvarId := subgoal.mvarId, vars := newVars, alts := newAlts, examples := examples }
return { p with mvarId := subgoal.mvarId, vars := newVars, alts := newAlts, examples := examples }
else
-- else branch for value
let newAlts := p.alts.filter isFirstPatternVar
@@ -764,7 +804,7 @@ private def processArrayLit (p : Problem) : MetaM (Array Problem) := do
let α getArrayArgType <| subst.apply x
expandVarIntoArrayLit { alt with patterns := ps } fvarId α size
| _ => unreachable!
return { mvarId := subgoal.mvarId, vars := newVars, alts := newAlts, examples := examples }
return { p with mvarId := subgoal.mvarId, vars := newVars, alts := newAlts, examples := examples }
else
-- else branch
let newAlts := p.alts.filter isFirstPatternVar
@@ -1018,7 +1058,7 @@ private builtin_initialize matcherExt : EnvExtension (PHashMap MatcherKey Name)
/-- Similar to `mkAuxDefinition`, but uses the cache `matcherExt`.
It also returns an Boolean that indicates whether a new matcher function was added to the environment or not. -/
def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (Expr × Option (MatcherInfo MetaM Unit)) := do
def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) (isSplitter : Bool) : MetaM (Expr × Option (MatcherInfo MetaM Unit)) := do
trace[Meta.Match.debug] "{name} : {type} := {value}"
let compile := bootstrap.genMatcherCode.get ( getOptions)
let result Closure.mkValueTypeClosure type value (zetaDelta := false)
@@ -1026,10 +1066,12 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (E
let mkMatcherConst name :=
mkAppN (mkConst name result.levelArgs.toList) result.exprArgs
let key := { value := result.value, compile, isPrivate := env.header.isModule && isPrivateName name }
let mut nameNew? := (matcherExt.getState env).find? key
if nameNew?.isNone && key.isPrivate then
-- private contexts may reuse public matchers
nameNew? := (matcherExt.getState env).find? { key with isPrivate := false }
let mut nameNew? := none
unless isSplitter do
nameNew? := (matcherExt.getState env).find? key
if nameNew?.isNone && key.isPrivate then
-- private contexts may reuse public matchers
nameNew? := (matcherExt.getState env).find? { key with isPrivate := false }
match nameNew? with
| some nameNew => return (mkMatcherConst nameNew, none)
| none =>
@@ -1040,8 +1082,9 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (E
-- matcher bodies should always be exported, if not private anyway
withExporting do
addDecl decl
modifyEnv fun env => matcherExt.modifyState env fun s => s.insert key name
addMatcherInfo name mi
unless isSplitter do
modifyEnv fun env => matcherExt.modifyState env fun s => s.insert key name
addMatcherInfo name mi
setInlineAttribute name
enableRealizationsForConst name
if compile then
@@ -1053,6 +1096,7 @@ structure MkMatcherInput where
matchType : Expr
discrInfos : Array DiscrInfo
lhss : List AltLHS
isSplitter : Option Overlaps := none
def MkMatcherInput.numDiscrs (m : MkMatcherInput) :=
m.discrInfos.size
@@ -1093,7 +1137,7 @@ The generated matcher has the structure described at `MatcherInfo`. The motive a
where `v` is a universe parameter or 0 if `B[a_1, ..., a_n]` is a proposition.
-/
def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := withCleanLCtxFor input do
let matcherName, matchType, discrInfos, lhss := input
let {matcherName, matchType, discrInfos, lhss, isSplitter} := input
let numDiscrs := discrInfos.size
checkNumPatterns numDiscrs lhss
forallBoundedTelescope matchType numDiscrs fun discrs matchTypeBody => do
@@ -1116,7 +1160,7 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := withCleanLCtxFor
| negSucc n => succ n
```
which is defined **before** `Int.decLt` -/
let (matcher, addMatcher) mkMatcherAuxDefinition matcherName type val
let (matcher, addMatcher) mkMatcherAuxDefinition matcherName type val (isSplitter := input.isSplitter.isSome)
trace[Meta.Match.debug] "matcher levels: {matcher.getAppFn.constLevels!}, uElim: {uElimGen}"
let uElimPos? getUElimPos? matcher.getAppFn.constLevels! uElimGen
discard <| isLevelDefEq uElimGen uElim
@@ -1152,7 +1196,7 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := withCleanLCtxFor
let isEqMask eqs.mapM fun eq => return ( inferType eq).isEq
return (mvarType, isEqMask)
trace[Meta.Match.debug] "target: {mvarType}"
withAlts motive discrs discrInfos lhss fun alts minors altInfos => do
withAlts motive discrs discrInfos lhss isSplitter fun alts minors altInfos => do
let mvar mkFreshExprMVar mvarType
trace[Meta.Match.debug] "goal\n{mvar.mvarId!}"
let examples := discrs'.toList.map fun discr => Example.var discr.fvarId!
@@ -1176,7 +1220,7 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := withCleanLCtxFor
else
let mvarType := mkAppN motive discrs
trace[Meta.Match.debug] "target: {mvarType}"
withAlts motive discrs discrInfos lhss fun alts minors altInfos => do
withAlts motive discrs discrInfos lhss isSplitter fun alts minors altInfos => do
let mvar mkFreshExprMVar mvarType
let examples := discrs.toList.map fun discr => Example.var discr.fvarId!
let (_, s) (process { mvarId := mvar.mvarId!, vars := discrs.toList, alts := alts, examples := examples }).run {}
@@ -1185,7 +1229,7 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := withCleanLCtxFor
let val mkLambdaFVars args mvar
mkMatcher type val altInfos s
def getMkMatcherInputInContext (matcherApp : MatcherApp) : MetaM MkMatcherInput := do
def getMkMatcherInputInContext (matcherApp : MatcherApp) (unfoldNamed : Bool) : MetaM MkMatcherInput := do
let matcherName := matcherApp.matcherName
let some matcherInfo getMatcherInfo? matcherName
| throwError "Internal error during match expression elaboration: Could not find a matcher named `{matcherName}`"
@@ -1204,6 +1248,7 @@ def getMkMatcherInputInContext (matcherApp : MatcherApp) : MetaM MkMatcherInput
let lhss forallBoundedTelescope matcherType (some matcherApp.alts.size) fun alts _ =>
alts.mapM fun alt => do
let ty inferType alt
let ty if unfoldNamed then unfoldNamedPattern ty else pure ty
forallTelescope ty fun xs body => do
let xs xs.filterM fun x => dependsOn body x.fvarId!
body.withApp fun _ args => do
@@ -1217,18 +1262,17 @@ def getMkMatcherInputInContext (matcherApp : MatcherApp) : MetaM MkMatcherInput
return { matcherName, matchType, discrInfos := matcherInfo.discrInfos, lhss := lhss.toList }
/-- This function is only used for testing purposes -/
def withMkMatcherInput (matcherName : Name) (k : MkMatcherInput MetaM α) : MetaM α := do
def withMkMatcherInput (matcherName : Name) (unfoldNamed : Bool) (k : MkMatcherInput MetaM α) : MetaM α := do
let some matcherInfo getMatcherInfo? matcherName
| throwError "Internal error during match expression elaboration: Could not find a matcher named `{matcherName}`"
| throwError "withMkMatcherInput: {.ofConstName matcherName} is not a matcher"
let matcherConst getConstInfo matcherName
forallBoundedTelescope matcherConst.type (some matcherInfo.arity) fun xs _ => do
let matcherApp mkConstWithLevelParams matcherConst.name
let matcherApp := mkAppN matcherApp xs
let some matcherApp matchMatcherApp? matcherApp
| throwError "Internal error during match expression elaboration: Could not find a matcher app named `{matcherApp}`"
let mkMatcherInput getMkMatcherInputInContext matcherApp
k mkMatcherInput
forallBoundedTelescope matcherConst.type matcherInfo.arity fun xs _ => do
let matcherApp mkConstWithLevelParams matcherConst.name
let matcherApp := mkAppN matcherApp xs
let some matcherApp matchMatcherApp? matcherApp
| throwError "withMkMatcherInput: {.ofConstName matcherName} does not produce a matcher application"
let mkMatcherInput getMkMatcherInputInContext matcherApp unfoldNamed
k mkMatcherInput
end Match

View File

@@ -8,170 +8,18 @@ module
prelude
public import Lean.Meta.Match.Match
public import Lean.Meta.Match.MatchEqsExt
public import Lean.Meta.Tactic.Refl
public import Lean.Meta.Tactic.Delta
import Lean.Meta.Tactic.Refl
import Lean.Meta.Tactic.Delta
import Lean.Meta.Tactic.SplitIf
import Lean.Meta.Tactic.CasesOnStuckLHS
import Lean.Meta.Match.SimpH
import Lean.Meta.Match.AltTelescopes
import Lean.Meta.Match.SolveOverlap
import Lean.Meta.Match.NamedPatterns
public section
namespace Lean.Meta
/--
Helper method for `proveCondEqThm`. Given a goal of the form `C.rec ... xMajor = rhs`,
apply `cases xMajor`. -/
partial def casesOnStuckLHS (mvarId : MVarId) : MetaM (Array MVarId) := do
let target mvarId.getType
if let some (_, lhs, _) matchEq? target then
if let some fvarId findFVar? lhs then
return ( mvarId.cases fvarId).map fun s => s.mvarId
throwError "'casesOnStuckLHS' failed"
where
findFVar? (e : Expr) : MetaM (Option FVarId) := do
match e.getAppFn with
| Expr.proj _ _ e => findFVar? e
| f =>
if !f.isConst then
return none
else
let declName := f.constName!
let args := e.getAppArgs
match ( getProjectionFnInfo? declName) with
| some projInfo =>
if projInfo.numParams < args.size then
findFVar? args[projInfo.numParams]!
else
return none
| none =>
matchConstRec f (fun _ => return none) fun recVal _ => do
if recVal.getMajorIdx >= args.size then
return none
let major := args[recVal.getMajorIdx]!.consumeMData
if major.isFVar then
return some major.fvarId!
else
return none
def casesOnStuckLHS? (mvarId : MVarId) : MetaM (Option (Array MVarId)) := do
try casesOnStuckLHS mvarId catch _ => return none
namespace Match
def unfoldNamedPattern (e : Expr) : MetaM Expr := do
let visit (e : Expr) : MetaM TransformStep := do
if let some e := isNamedPattern? e then
if let some eNew unfoldDefinition? e then
return TransformStep.visit eNew
return .continue
Meta.transform e (pre := visit)
/--
Similar to `forallTelescopeReducing`, but
1. Eliminates arguments for named parameters and the associated equation proofs.
2. Instantiate the `Unit` parameter of an otherwise argumentless alternative.
It does not handle the equality parameters associated with the `h : discr` notation.
The continuation `k` takes four arguments `ys args mask type`.
- `ys` are variables for the hypotheses that have not been eliminated.
- `args` are the arguments for the alternative `alt` that has type `altType`. `ys.size <= args.size`
- `mask[i]` is true if the hypotheses has not been eliminated. `mask.size == args.size`.
- `type` is the resulting type for `altType`.
We use the `mask` to build the splitter proof. See `mkSplitterProof`.
This can be used to use the alternative of a match expression in its splitter.
-/
partial def forallAltVarsTelescope (altType : Expr) (altInfo : AltParamInfo)
(k : (patVars : Array Expr) (args : Array Expr) (mask : Array Bool) (type : Expr) MetaM α) : MetaM α := do
assert! altInfo.numOverlaps = 0
if altInfo.hasUnitThunk then
let type whnfForall altType
let type Match.unfoldNamedPattern type
let type instantiateForall type #[mkConst ``Unit.unit]
k #[] #[mkConst ``Unit.unit] #[false] type
else
go #[] #[] #[] 0 altType
where
go (ys : Array Expr) (args : Array Expr) (mask : Array Bool) (i : Nat) (type : Expr) : MetaM α := do
let type whnfForall type
if i < altInfo.numFields then
let Expr.forallE n d b .. := type
| throwError "expecting {altInfo.numFields} parameters, but found type{indentExpr altType}"
let d Match.unfoldNamedPattern d
withLocalDeclD n d fun y => do
let typeNew := b.instantiate1 y
if let some (_, lhs, rhs) matchEq? d then
if lhs.isFVar && ys.contains lhs && args.contains lhs && isNamedPatternProof typeNew y then
let some j := ys.finIdxOf? lhs | unreachable!
let ys := ys.eraseIdx j
let some k := args.idxOf? lhs | unreachable!
let mask := mask.set! k false
let args := args.map fun arg => if arg == lhs then rhs else arg
let arg mkEqRefl rhs
let typeNew := typeNew.replaceFVar lhs rhs
return withReplaceFVarId lhs.fvarId! rhs do
withReplaceFVarId y.fvarId! arg do
go ys (args.push arg) (mask.push false) (i+1) typeNew
go (ys.push y) (args.push y) (mask.push true) (i+1) typeNew
else
let type Match.unfoldNamedPattern type
k ys args mask type
isNamedPatternProof (type : Expr) (h : Expr) : Bool :=
Option.isSome <| type.find? fun e =>
if let some e := Match.isNamedPattern? e then
e.appArg! == h
else
false
/--
Extension of `forallAltTelescope` that continues further:
Equality parameters associated with the `h : discr` notation are replaced with `rfl` proofs.
Recall that this kind of parameter always occurs after the parameters corresponding to pattern
variables.
The continuation `k` takes four arguments `ys args mask type`.
- `ys` are variables for the hypotheses that have not been eliminated.
- `eqs` are variables for equality hypotheses associated with discriminants annotated with `h : discr`.
- `args` are the arguments for the alternative `alt` that has type `altType`. `ys.size <= args.size`
- `mask[i]` is true if the hypotheses has not been eliminated. `mask.size == args.size`.
- `type` is the resulting type for `altType`.
We use the `mask` to build the splitter proof. See `mkSplitterProof`.
This can be used to use the alternative of a match expression in its splitter.
-/
partial def forallAltTelescope (altType : Expr) (altInfo : AltParamInfo) (numDiscrEqs : Nat)
(k : (ys : Array Expr) (eqs : Array Expr) (args : Array Expr) (mask : Array Bool) (type : Expr) MetaM α)
: MetaM α := do
forallAltVarsTelescope altType altInfo fun ys args mask altType => do
go ys #[] args mask 0 altType
where
go (ys : Array Expr) (eqs : Array Expr) (args : Array Expr) (mask : Array Bool) (i : Nat) (type : Expr) : MetaM α := do
let type whnfForall type
if i < numDiscrEqs then
let Expr.forallE n d b .. := type
| throwError "expecting {numDiscrEqs} equalities, but found type{indentExpr altType}"
let arg if let some (_, _, rhs) matchEq? d then
mkEqRefl rhs
else if let some (_, _, _, rhs) matchHEq? d then
mkHEqRefl rhs
else
throwError "unexpected match alternative type{indentExpr altType}"
withLocalDeclD n d fun eq => do
let typeNew := b.instantiate1 eq
go ys (eqs.push eq) (args.push arg) (mask.push false) (i+1) typeNew
else
let type unfoldNamedPattern type
k ys eqs args mask type
namespace Lean.Meta.Match
/--
Given an application of an matcher arm `alt` that is expecting the `numDiscrEqs`, and
@@ -262,220 +110,6 @@ where
(throwError "failed to generate equality theorems for `match` expression `{matchDeclName}`\n{MessageData.ofGoal mvarId}")
subgoals.forM (go · (depth+1))
/-- Construct new local declarations `xs` with types `altTypes`, and then execute `f xs` -/
private partial def withSplitterAlts (altTypes : Array Expr) (f : Array Expr MetaM α) : MetaM α := do
let rec go (i : Nat) (xs : Array Expr) : MetaM α := do
if h : i < altTypes.size then
let hName := (`h).appendIndexAfter (i+1)
withLocalDeclD hName altTypes[i] fun x =>
go (i+1) (xs.push x)
else
f xs
go 0 #[]
private abbrev ConvertM := ReaderT (FVarIdMap (Expr × AltParamInfo × Array Bool)) $ StateRefT (Array MVarId) MetaM
/--
Construct a proof for the splitter generated by `mkEquationsFor`.
The proof uses the definition of the `match`-declaration as a template (argument `template`).
- `alts` are free variables corresponding to alternatives of the `match` auxiliary declaration being processed.
- `altNews` are the new free variables which contains additional hypotheses that ensure they are only used
when the previous overlapping alternatives are not applicable.
- `altInfos` refers to the splitter -/
private partial def mkSplitterProof (matchDeclName : Name) (template : Expr) (alts altsNew : Array Expr)
(altInfos : Array AltParamInfo) (altArgMasks : Array (Array Bool)) : MetaM Expr := do
trace[Meta.Match.matchEqs] "proof template: {template}"
let map := mkMap
let (proof, mvarIds) convertTemplate template |>.run map |>.run #[]
trace[Meta.Match.matchEqs] "splitter proof: {proof}"
for mvarId in mvarIds do
let mvarId mvarId.tryClearMany (alts.map (·.fvarId!))
solveOverlap mvarId
instantiateMVars proof
where
mkMap : FVarIdMap (Expr × AltParamInfo × Array Bool) := Id.run do
let mut m := {}
for alt in alts, altNew in altsNew, altInfo in altInfos, argMask in altArgMasks do
m := m.insert alt.fvarId! (altNew, altInfo, argMask)
return m
trimFalseTrail (argMask : Array Bool) : Array Bool :=
if argMask.isEmpty then
argMask
else if !argMask.back! then
trimFalseTrail argMask.pop
else
argMask
/--
Auxiliary function used at `convertTemplate` to decide whether to use `convertCastEqRec`.
See `convertCastEqRec`. -/
isCastEqRec (e : Expr) : ConvertM Bool := do
-- TODO: we do not handle `Eq.rec` since we never found an example that needed it.
-- If we find one we must extend `convertCastEqRec`.
unless e.isAppOf ``Eq.ndrec do return false
unless e.getAppNumArgs > 6 do return false
for arg in e.getAppArgs[6...*] do
if arg.isFVar && ( read).contains arg.fvarId! then
return true
return true
/--
Auxiliary function used at `convertTemplate`. It is needed when the auxiliary `match` declaration had to refine the type of its
minor premises during dependent pattern match. For an example, consider
```
inductive Foo : Nat → Type _
| nil : Foo 0
| cons (t: Foo l): Foo l
def Foo.bar (t₁: Foo l₁): Foo l₂ → Bool
| cons s₁ => t₁.bar s₁
| _ => false
attribute [simp] Foo.bar
```
The auxiliary `Foo.bar.match_1` is of the form
```
def Foo.bar.match_1.{u_1} : {l₂ : Nat} →
(t₂ : Foo l₂) →
(motive : Foo l₂ → Sort u_1) →
(t₂ : Foo l₂) → ((s₁ : Foo l₂) → motive (Foo.cons s₁)) → ((x : Foo l₂) → motive x) → motive t₂ :=
fun {l₂} t₂ motive t₂_1 h_1 h_2 =>
(fun t₂_2 =>
Foo.casesOn (motive := fun a x => l₂ = a → t₂_1 ≍ x → motive t₂_1) t₂_2
(fun h =>
Eq.ndrec (motive := fun {l₂} =>
(t₂ t₂ : Foo l₂) →
(motive : Foo l₂ → Sort u_1) →
((s₁ : Foo l₂) → motive (Foo.cons s₁)) → ((x : Foo l₂) → motive x) → t₂ ≍ Foo.nil → motive t₂)
(fun t₂ t₂ motive h_1 h_2 h => Eq.symm (eq_of_heq h) ▸ h_2 Foo.nil) (Eq.symm h) t₂ t₂_1 motive h_1 h_2) --- HERE
fun {l} t h =>
Eq.ndrec (motive := fun {l} => (t : Foo l) → t₂_1 ≍ Foo.cons t → motive t₂_1)
(fun t h => Eq.symm (eq_of_heq h) ▸ h_1 t) h t)
t₂_1 (Eq.refl l₂) (HEq.refl t₂_1)
```
The `HERE` comment marks the place where the type of `Foo.bar.match_1` minor premises `h_1` and `h_2` is being "refined"
using `Eq.ndrec`.
This function will adjust the motive and minor premise of the `Eq.ndrec` to reflect the new minor premises used in the
corresponding splitter theorem.
We may have to extend this function to handle `Eq.rec` too.
This function was added to address issue #1179
-/
convertCastEqRec (e : Expr) : ConvertM Expr := do
assert! ( isCastEqRec e)
e.withApp fun f args => do
let mut argsNew := args
let mut isAlt := #[]
for i in 6...args.size do
let arg := argsNew[i]!
if arg.isFVar then
match ( read).get? arg.fvarId! with
| some (altNew, _, _) =>
argsNew := argsNew.set! i altNew
trace[Meta.Match.matchEqs] "arg: {arg} : {← inferType arg}, altNew: {altNew} : {← inferType altNew}"
isAlt := isAlt.push true
| none =>
argsNew := argsNew.set! i ( convertTemplate arg)
isAlt := isAlt.push false
else
argsNew := argsNew.set! i ( convertTemplate arg)
isAlt := isAlt.push false
assert! isAlt.size == args.size - 6
let rhs := args[4]!
let motive := args[2]!
-- Construct new motive using the splitter theorem minor premise types.
let motiveNew lambdaTelescope motive fun motiveArgs body => do
unless motiveArgs.size == 1 do
throwError "unexpected `Eq.ndrec` motive while creating splitter/eliminator theorem for `{matchDeclName}`, expected lambda with 1 binder{indentExpr motive}"
let x := motiveArgs[0]!
forallTelescopeReducing body fun motiveTypeArgs resultType => do
unless motiveTypeArgs.size >= isAlt.size do
throwError "unexpected `Eq.ndrec` motive while creating splitter/eliminator theorem for `{matchDeclName}`, expected arrow with at least #{isAlt.size} binders{indentExpr body}"
let rec go (i : Nat) (motiveTypeArgsNew : Array Expr) : ConvertM Expr := do
assert! motiveTypeArgsNew.size == i
if h : i < motiveTypeArgs.size then
let motiveTypeArg := motiveTypeArgs[i]
if i < isAlt.size && isAlt[i]! then
let altNew := argsNew[6+i]! -- Recall that `Eq.ndrec` has 6 arguments
let altTypeNew inferType altNew
trace[Meta.Match.matchEqs] "altNew: {altNew} : {altTypeNew}"
-- Replace `rhs` with `x` (the lambda binder in the motive)
let mut altTypeNewAbst := ( kabstract altTypeNew rhs).instantiate1 x
-- Replace args[6...(6+i)] with `motiveTypeArgsNew`
for j in *...i do
altTypeNewAbst := ( kabstract altTypeNewAbst argsNew[6+j]!).instantiate1 motiveTypeArgsNew[j]!
let localDecl motiveTypeArg.fvarId!.getDecl
withLocalDecl localDecl.userName localDecl.binderInfo altTypeNewAbst fun motiveTypeArgNew =>
go (i+1) (motiveTypeArgsNew.push motiveTypeArgNew)
else
go (i+1) (motiveTypeArgsNew.push motiveTypeArg)
else
mkLambdaFVars motiveArgs ( mkForallFVars motiveTypeArgsNew resultType)
go 0 #[]
trace[Meta.Match.matchEqs] "new motive: {motiveNew}"
unless ( isTypeCorrect motiveNew) do
throwError "failed to construct new type correct motive for `Eq.ndrec` while creating splitter/eliminator theorem for `{matchDeclName}`{indentExpr motiveNew}"
argsNew := argsNew.set! 2 motiveNew
-- Construct the new minor premise for the `Eq.ndrec` application.
-- First, we use `eqRecNewPrefix` to infer the new minor premise binders for `Eq.ndrec`
let eqRecNewPrefix := mkAppN f argsNew[*...3] -- `Eq.ndrec` minor premise is the fourth argument.
let .forallE _ minorTypeNew .. whnf ( inferType eqRecNewPrefix) | unreachable!
trace[Meta.Match.matchEqs] "new minor type: {minorTypeNew}"
let minor := args[3]!
let minorNew forallBoundedTelescope minorTypeNew isAlt.size fun minorArgsNew _ => do
let mut minorBodyNew := minor
-- We have to extend the mapping to make sure `convertTemplate` can "fix" occurrences of the refined minor premises
let mut m read
for h : i in *...isAlt.size do
if isAlt[i] then
-- `convertTemplate` will correct occurrences of the alternative
let alt := args[6+i]! -- Recall that `Eq.ndrec` has 6 arguments
let some (_, numParams, argMask) := m.get? alt.fvarId! | unreachable!
-- We add a new entry to `m` to make sure `convertTemplate` will correct the occurrences of the alternative
m := m.insert minorArgsNew[i]!.fvarId! (minorArgsNew[i]!, numParams, argMask)
unless minorBodyNew.isLambda do
throwError "unexpected `Eq.ndrec` minor premise while creating splitter/eliminator theorem for `{matchDeclName}`, expected lambda with at least #{isAlt.size} binders{indentExpr minor}"
minorBodyNew := minorBodyNew.bindingBody!
minorBodyNew := minorBodyNew.instantiateRev minorArgsNew
trace[Meta.Match.matchEqs] "minor premise new body before convertTemplate:{indentExpr minorBodyNew}"
minorBodyNew withReader (fun _ => m) <| convertTemplate minorBodyNew
trace[Meta.Match.matchEqs] "minor premise new body after convertTemplate:{indentExpr minorBodyNew}"
mkLambdaFVars minorArgsNew minorBodyNew
unless ( isTypeCorrect minorNew) do
throwError "failed to construct new type correct minor premise for `Eq.ndrec` while creating splitter/eliminator theorem for `{matchDeclName}`{indentExpr minorNew}"
argsNew := argsNew.set! 3 minorNew
-- trace[Meta.Match.matchEqs] "argsNew: {argsNew}"
trace[Meta.Match.matchEqs] "found cast target {e}"
return mkAppN f argsNew
convertTemplate (e : Expr) : ConvertM Expr :=
transform e fun e => do
if ( isCastEqRec e) then
return .done ( convertCastEqRec e)
else
let Expr.fvar fvarId .. := e.getAppFn | return .continue
let some (altNew, altParamInfo, argMask) := ( read).get? fvarId | return .continue
trace[Meta.Match.matchEqs] ">> argMask: {argMask}, altParamInfo: {repr altParamInfo}, e: {e}, alsNew: {altNew}, "
if altParamInfo.hasUnitThunk then
let eNew := mkApp altNew (mkConst ``Unit.unit)
return TransformStep.done eNew
let mut newArgs := #[]
let argMask := trimFalseTrail argMask
unless e.getAppNumArgs argMask.size do
throwError "unexpected occurrence of `match`-expression alternative (aka minor premise) while creating splitter/eliminator theorem for `{matchDeclName}`, minor premise is partially applied{indentExpr e}\npossible solution if you are matching on inductive families: add its indices as additional discriminants"
for arg in e.getAppArgs, includeArg in argMask do
if includeArg then
newArgs := newArgs.push arg
let eNew := mkAppN altNew newArgs
let (mvars, _, _) forallMetaBoundedTelescope ( inferType eNew) altParamInfo.numOverlaps (kind := MetavarKind.syntheticOpaque)
modify fun s => s ++ (mvars.map (·.mvarId!))
let eNew := mkAppN eNew mvars
return TransformStep.done eNew
/--
Create new alternatives (aka minor premises) by replacing `discrs` with `patterns` at `alts`.
Recall that `alts` depends on `discrs` when `numDiscrEqs > 0`, where `numDiscrEqs` is the number of discriminants
@@ -516,13 +150,15 @@ def getEquationsForImpl (matchDeclName : Name) : MetaM MatchEqns := do
-- `realizeConst` as well as for looking up the resultant environment extension state via
-- `getState`.
realizeConst matchDeclName splitterName (go baseName splitterName)
return matchEqnsExt.getState (asyncMode := .async .asyncEnv) (asyncDecl := splitterName) ( getEnv) |>.map.find! matchDeclName
match matchEqnsExt.getState (asyncMode := .async .asyncEnv) (asyncDecl := splitterName) ( getEnv) |>.map.find? matchDeclName with
| some eqns => return eqns
| none => throwError "failed to retrieve match equations for `{matchDeclName}` after realization"
where go baseName splitterName := withConfig (fun c => { c with etaStruct := .none }) do
let constInfo getConstInfo matchDeclName
let us := constInfo.levelParams.map mkLevelParam
let some matchInfo getMatcherInfo? matchDeclName | throwError "`{matchDeclName}` is not a matcher function"
let numDiscrEqs := getNumEqsFromDiscrInfos matchInfo.discrInfos
forallTelescopeReducing constInfo.type fun xs matchResultType => do
forallTelescopeReducing constInfo.type fun xs _matchResultType => do
let mut eqnNames := #[]
let params := xs[*...matchInfo.numParams]
let motive := xs[matchInfo.getMotivePos]!
@@ -531,16 +167,15 @@ where go baseName splitterName := withConfig (fun c => { c with etaStruct := .no
let discrs := xs[firstDiscrIdx...(firstDiscrIdx + matchInfo.numDiscrs)]
let mut notAlts := #[]
let mut idx := 1
let mut splitterAltTypes := #[]
let mut splitterAltInfos := #[]
let mut altArgMasks := #[] -- masks produced by `forallAltTelescope`
for i in *...alts.size do
let altInfo := matchInfo.altInfos[i]!
let thmName := Name.str baseName eqnThmSuffixBase |>.appendIndexAfter idx
eqnNames := eqnNames.push thmName
let (notAlt, splitterAltType, splitterAltInfo, argMask)
let (notAlt, splitterAltInfo, argMask)
forallAltTelescope ( inferType alts[i]!) altInfo numDiscrEqs
fun ys eqs rhsArgs argMask altResultType => do
fun ys _eqs rhsArgs argMask altResultType => do
let patterns := altResultType.getAppArgs
let mut hs := #[]
for overlappedBy in matchInfo.overlaps.overlapping i do
@@ -549,15 +184,7 @@ where go baseName splitterName := withConfig (fun c => { c with etaStruct := .no
if let some h simpH? h patterns.size then
hs := hs.push h
trace[Meta.Match.matchEqs] "hs: {hs}"
let splitterAltType mkForallFVars eqs altResultType
let splitterAltType mkArrowN hs splitterAltType
let splitterAltType mkForallFVars ys splitterAltType
let hasUnitThunk := splitterAltType == altResultType
let splitterAltType if hasUnitThunk then
mkArrow (mkConst ``Unit) splitterAltType
else
pure splitterAltType
let splitterAltType unfoldNamedPattern splitterAltType
let hasUnitThunk := ys.isEmpty && hs.isEmpty && numDiscrEqs = 0
let splitterAltInfo := { numFields := ys.size, numOverlaps := hs.size, hasUnitThunk }
-- Create a proposition for representing terms that do not match `patterns`
let mut notAlt := mkConst ``False
@@ -571,7 +198,7 @@ where go baseName splitterName := withConfig (fun c => { c with etaStruct := .no
let lhs := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ patterns ++ alts)
let rhs := mkAppN alt rhsArgs
let thmType mkEq lhs rhs
let thmType hs.foldrM (init := thmType) (mkArrow · ·)
let thmType mkArrowN hs thmType
let thmType mkForallFVars (params ++ #[motive] ++ ys ++ alts) thmType
let thmType unfoldNamedPattern thmType
let thmVal proveCondEqThm matchDeclName thmType
@@ -581,38 +208,38 @@ where go baseName splitterName := withConfig (fun c => { c with etaStruct := .no
type := thmType
value := thmVal
}
return (notAlt, splitterAltType, splitterAltInfo, argMask)
return (notAlt, splitterAltInfo, argMask)
notAlts := notAlts.push notAlt
splitterAltTypes := splitterAltTypes.push splitterAltType
splitterAltInfos := splitterAltInfos.push splitterAltInfo
altArgMasks := altArgMasks.push argMask
trace[Meta.Match.matchEqs] "splitterAltType: {splitterAltType}"
idx := idx + 1
-- Define splitter with conditional/refined alternatives
withSplitterAlts splitterAltTypes fun altsNew => do
let splitterParams := params.toArray ++ #[motive] ++ discrs.toArray ++ altsNew
let splitterType mkForallFVars splitterParams matchResultType
trace[Meta.Match.matchEqs] "splitterType: {splitterType}"
let splitterVal
if ( isDefEq splitterType constInfo.type) then
pure <| mkConst constInfo.name us
else
let template := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ discrs ++ alts)
let template deltaExpand template (· == constInfo.name)
let template := template.headBeta
mkLambdaFVars splitterParams ( mkSplitterProof matchDeclName template alts altsNew splitterAltInfos altArgMasks)
let splitterMatchInfo : MatcherInfo := { matchInfo with altInfos := splitterAltInfos }
let needsSplitter := !matchInfo.overlaps.isEmpty || (constInfo.type.find? (isNamedPattern )).isSome
if needsSplitter then
withMkMatcherInput matchDeclName (unfoldNamed := true) fun matcherInput => do
let matcherInput := { matcherInput with
matcherName := splitterName
isSplitter := some matchInfo.overlaps
}
let res Match.mkMatcher matcherInput
res.addMatcher -- TODO: Do not set matcherinfo for the splitter!
else
assert! matchInfo.altInfos == splitterAltInfos
-- This match statement does not need a splitter, we can use itself for that.
-- (We still have to generate a declaration to satisfy the realizable constant)
addAndCompile <| Declaration.defnDecl {
name := splitterName
levelParams := constInfo.levelParams
type := splitterType
value := splitterVal
type := constInfo.type
value := mkConst matchDeclName us
hints := .abbrev
safety := .safe
}
setInlineAttribute splitterName
let splitterMatchInfo := { matchInfo with altInfos := splitterAltInfos }
let result := { eqnNames, splitterName, splitterMatchInfo }
registerMatchEqns matchDeclName result
let result := { eqnNames, splitterName, splitterMatchInfo }
registerMatchEqns matchDeclName result
/- We generate the equations and splitter on demand, and do not save them on .olean files. -/
builtin_initialize matchCongrEqnsExt : EnvExtension (PHashMap Name (Array Name))
@@ -636,7 +263,8 @@ The code duplicates a fair bit of the logic above, and has to repeat the calcula
`notAlts`. One could avoid that and generate the generalized equations eagerly above, but they are
not always needed, so for now we live with the code duplication.
-/
def genMatchCongrEqns (matchDeclName : Name) : MetaM (Array Name) := do
@[export lean_get_congr_match_equations_for]
def genMatchCongrEqnsImpl (matchDeclName : Name) : MetaM (Array Name) := do
let baseName := mkPrivateName ( getEnv) matchDeclName
let firstEqnName := .str baseName congrEqn1ThmSuffix
realizeConst matchDeclName firstEqnName (go baseName)
@@ -684,7 +312,7 @@ where go baseName := withConfig (fun c => { c with etaStruct := .none }) do
notAlt mkForallFVars (discrs ++ altVars) notAlt
let lhs := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ discrs ++ alts)
let thmType mkHEq lhs rhs
let thmType hs.foldrM (init := thmType) (mkArrow · ·)
let thmType mkArrowN hs thmType
let thmType mkForallFVars (params ++ #[motive] ++ discrs ++ alts ++ altVars ++ heqs) thmType
let thmType Match.unfoldNamedPattern thmType
-- Here we prove the theorem from scratch. One could likely also use the (non-generalized)
@@ -718,7 +346,7 @@ builtin_initialize registerReservedNameAction fun name => do
let some (p, isGenEq) := isMatchEqName? ( getEnv) name |
return false
if isGenEq then
let _ MetaM.run' <| genMatchCongrEqns p
let _ MetaM.run' <| genMatchCongrEqnsImpl p
else
let _ MetaM.run' <| getEquationsFor p
return true

View File

@@ -8,6 +8,7 @@ module
prelude
public import Lean.Meta.Basic
public import Lean.Meta.Match.Basic
public import Lean.Meta.Match.MatcherInfo
import Lean.Meta.Eqns
public section
@@ -42,11 +43,19 @@ def registerMatchEqns (matchDeclName : Name) (matchEqns : MatchEqns) : CoreM Uni
}
/-
Forward definition. We want to use `getEquationsFor` in the simplifier,
`getEquationsFor` depends on `mkEquationsFor` which uses the simplifier. -/
Forward definition of `getEquationsForImpl`.
We want to use `getEquationsFor` in the simplifier,
getEquationsFor` depends on `mkEquationsFor` which uses the simplifier.
-/
@[extern "lean_get_match_equations_for"]
opaque getEquationsFor (matchDeclName : Name) : MetaM MatchEqns
/-
Forward definition of `genMatchCongrEqnsImpl`.
-/
@[extern "lean_get_congr_match_equations_for"]
opaque genMatchCongrEqns (matchDeclName : Name) : MetaM (Array Name)
/--
Returns `true` if `declName` is the name of a `match` equational theorem.
-/

View File

@@ -67,6 +67,7 @@ def matchMatcherApp? [Monad m] [MonadEnv m] [MonadError m] (e : Expr) (alsoCases
matcherName := declName
matcherLevels := declLevels.toArray
uElimPos?, discrInfos, params, motive, discrs, alts, remaining, altInfos
overlaps := {} -- CasesOn constructor have no overlaps
}
return none

View File

@@ -7,8 +7,12 @@ Authors: Leonardo de Moura, Joachim Breitner
module
prelude
public import Lean.Meta.Match
public import Lean.Meta.Tactic.Split
public import Lean.Meta.Match.MatcherApp.Basic
public import Lean.Meta.Match.MatchEqsExt
public import Lean.Meta.Match.AltTelescopes
public import Lean.Meta.AppBuilder
import Lean.Meta.Tactic.Split
import Lean.Meta.Tactic.Refl
public section

View File

@@ -23,6 +23,9 @@ structure Overlaps where
map : Std.HashMap Nat (Std.TreeSet Nat) := {}
deriving Inhabited, Repr
def Overlaps.isEmpty (o : Overlaps) : Bool :=
o.map.isEmpty
def Overlaps.insert (o : Overlaps) (overlapping overlapped : Nat) : Overlaps where
map := o.map.alter overlapped fun s? => some ((s?.getD {}).insert overlapping)
@@ -41,29 +44,32 @@ structure AltParamInfo where
numOverlaps : Nat
/-- Whether this alternatie has an artifcial `Unit` parameter -/
hasUnitThunk : Bool
deriving Inhabited, Repr
deriving Inhabited, Repr, BEq
/--
A "matcher" auxiliary declaration has the following structure:
- `numParams` parameters
- motive
- `numDiscrs` discriminators (aka major premises)
- `altInfos.size` alternatives (aka minor premises) with parameter structure information
- `uElimPos?` is `some pos` when the matcher can eliminate in different universe levels, and
`pos` is the position of the universe level parameter that specifies the elimination universe.
It is `none` if the matcher only eliminates into `Prop`.
- `overlaps` indicates which alternatives may overlap another
Information about the structure of a matcher declaration
-/
structure MatcherInfo where
/-- Number of parameters -/
numParams : Nat
/-- Number of discriminants -/
numDiscrs : Nat
/-- Parameter structure information for each alternative -/
altInfos : Array AltParamInfo
/--
`uElimPos?` is `some pos` when the matcher can eliminate in different universe levels, and
`pos` is the position of the universe level parameter that specifies the elimination universe.
It is `none` if the matcher only eliminates into `Prop`.
-/
uElimPos? : Option Nat
/--
`discrInfos[i] = { hName? := some h }` if the i-th discriminant was annotated with `h :`.
`discrInfos[i] = { hName? := some h }` if the i-th discriminant was annotated with `h :`.
-/
discrInfos : Array DiscrInfo
overlaps : Overlaps := {}
/--
(Conservative approximation of) which alternatives may overlap another.
-/
overlaps : Overlaps
deriving Inhabited, Repr
@[expose] def MatcherInfo.numAlts (info : MatcherInfo) : Nat :=

View File

@@ -0,0 +1,38 @@
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Lean.Meta.Basic
import Lean.Meta.AppBuilder
/-!
Helper functions around named patterns
-/
namespace Lean.Meta.Match
public def mkNamedPattern (x h p : Expr) : MetaM Expr :=
mkAppM ``namedPattern #[x, p, h]
public def isNamedPattern (e : Expr) : Bool :=
let e := e.consumeMData
e.getAppNumArgs == 4 && e.getAppFn.consumeMData.isConstOf ``namedPattern
public def isNamedPattern? (e : Expr) : Option Expr :=
let e := e.consumeMData
if e.getAppNumArgs == 4 && e.getAppFn.consumeMData.isConstOf ``namedPattern then
some e
else
none
public def unfoldNamedPattern (e : Expr) : MetaM Expr := do
let visit (e : Expr) : MetaM TransformStep := do
if let some e := isNamedPattern? e then
if let some eNew unfoldDefinition? e then
return TransformStep.visit eNew
return .continue
Meta.transform e (pre := visit)

View File

@@ -44,6 +44,18 @@ def matchEqHEq? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) := do
else
return none
/--
Return `some (α, lhs)` if `e` is of the form `@Eq α lhs rhs` or `@HEq α lhs β rhs`
-/
def matchEqHEqLHS? (e : Expr) : MetaM (Option (Expr × Expr)) := do
if let some (α, lhs, _rhs) matchEq? e then
return some (α, lhs)
else if let some (α, lhs, _β, _rhs) matchHEq? e then
return some (α, lhs)
else
return none
def matchFalse (e : Expr) : MetaM Bool := do
testHelper e fun e => return e.isFalse

View File

@@ -0,0 +1,56 @@
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Lean.Meta.Basic
import Lean.Meta.Tactic.SplitIf
namespace Lean.Meta
/-!
This module provides the `casesOnStuckLHS` tactic, used by
* match equation compilation
* equation compilation for recursive functions
-/
/--
Helper method for `proveCondEqThm`. Given a goal of the form `C.rec ... xMajor = rhs`,
apply `cases xMajor`. -/
public partial def casesOnStuckLHS (mvarId : MVarId) : MetaM (Array MVarId) := do
let target mvarId.getType
if let some (_, lhs) matchEqHEqLHS? target then
if let some fvarId findFVar? lhs then
return ( mvarId.cases fvarId).map fun s => s.mvarId
throwError "'casesOnStuckLHS' failed"
where
findFVar? (e : Expr) : MetaM (Option FVarId) := do
match e.getAppFn with
| Expr.proj _ _ e => findFVar? e
| f =>
if !f.isConst then
return none
else
let declName := f.constName!
let args := e.getAppArgs
match ( getProjectionFnInfo? declName) with
| some projInfo =>
if projInfo.numParams < args.size then
findFVar? args[projInfo.numParams]!
else
return none
| none =>
matchConstRec f (fun _ => return none) fun recVal _ => do
if recVal.getMajorIdx >= args.size then
return none
let major := args[recVal.getMajorIdx]!.consumeMData
if major.isFVar then
return some major.fvarId!
else
return none
public def casesOnStuckLHS? (mvarId : MVarId) : MetaM (Option (Array MVarId)) := do
try casesOnStuckLHS mvarId catch _ => return none

View File

@@ -72,7 +72,7 @@ where
- It occurs in the target type, or
- There is a relevant variable `y` that depends on `x`, or
- If `indirectProps` is true, the type of `x` is a proposition and it depends on a relevant variable `y`.
- If `indirectProps` is true, `x` is a local declartation and its value mentions a relevant variable `y`.
- If `indirectProps` is true, `x` is a local declaration and its value mentions a relevant variable `y`.
By default, `toPreserve := #[]` and `indirectProps := true`. These settings are used in the mathlib tactic `extract_goal`
to give the user more control over which variables to include.

View File

@@ -18,6 +18,8 @@ import Lean.Meta.Tactic.ElimInfo
import Lean.Meta.Tactic.FunIndInfo
import Lean.Data.Array
import Lean.Meta.Tactic.Simp.Rewrite
import Lean.Meta.Tactic.Refl
import Lean.Meta.Tactic.Replace
/-!
This module contains code to derive, from the definition of a recursive function (structural or
@@ -778,23 +780,10 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
-- Check for unreachable cases. We look for the kind of expressions that `by contradiction`
-- produces
match_expr e with
| False.elim _ h => do
return mkFalseElim goal h
| absurd _ _ h₁ h₂ => do
return mkAbsurd goal h₁ h₂
| _ => pure ()
if e.isApp && e.getAppFn.isConst && isNoConfusion ( getEnv) e.getAppFn.constName! then
let arity := ( inferType e.getAppFn).getNumHeadForalls -- crucially not reducing the noConfusionType in the type
let h := e.getArg! (arity - 1)
let hType inferType h
-- The following duplicates a bit of code from the contradiction tactic, maybe worth extracting
-- into a common helper at some point
if let some (_, lhs, rhs) matchEq? hType then
if let some lhsCtor matchConstructorApp? lhs then
if let some rhsCtor matchConstructorApp? rhs then
if lhsCtor.name != rhsCtor.name then
return ( mkNoConfusion goal h)
if e.isAppOf ``False.elim && 1 < e.getAppNumArgs then
return mkFalseElim goal e.getAppArgs[1]!
if e.isAppOf ``absurd && 3 < e.getAppNumArgs then
return mkAbsurd goal e.getAppArgs[2]! e.getAppArgs[3]!
-- we look in to `PProd.mk`, as it occurs in the mutual structural recursion construction
match_expr goal with
@@ -927,7 +916,7 @@ where doRealize (inductName : Name) := do
-- to make sure that `target` indeed the last parameter
let e := info.value
let e lambdaTelescope e fun params body => do
if body.isAppOfArity ``WellFounded.fix 5 then
if body.isAppOfArity ``WellFounded.fix 5 || body.isAppOfArity ``WellFounded.Nat.fix 4 then
forallBoundedTelescope ( inferType body) (some 1) fun xs _ => do
unless xs.size = 1 do
throwError "functional induction: Failed to eta-expand{indentExpr e}"
@@ -935,68 +924,76 @@ where doRealize (inductName : Name) := do
else
pure e
let (e', paramMask) lambdaTelescope e fun params funBody => MatcherApp.withUserNames params varNames do
match_expr funBody with
| fix@WellFounded.fix α _motive rel wf body target =>
unless params.back! == target do
throwError "functional induction: expected the target as last parameter{indentExpr e}"
let fixedParamPerms := params.pop
let motiveType
if unfolding then
withLocalDeclD `r ( instantiateForall info.type params) fun r =>
mkForallFVars #[target, r] (.sort 0)
else
mkForallFVars #[target] (.sort 0)
withLocalDeclD `motive motiveType fun motive => do
let fn := mkAppN ( mkConstWithLevelParams name) fixedParamPerms
let isRecCall : Expr Option Expr := fun e =>
e.withApp fun f xs =>
if f.isFVarOf motive.fvarId! && xs.size > 0 then
mkApp fn xs[0]!
else
none
let motiveArg
if unfolding then
let motiveArg := mkApp2 motive target (mkAppN ( mkConstWithLevelParams name) params)
mkLambdaFVars #[target] motiveArg
else
pure motive
let e' := .const ``WellFounded.fix [fix.constLevels![0]!, levelZero]
let e' := mkApp4 e' α motiveArg rel wf
check e'
let (body', mvars) M2.run do
forallTelescope ( inferType e').bindingDomain! fun xs goal => do
if xs.size 2 then
throwError "expected recursor argument to take 2 parameters, got {xs}" else
let targets : Array Expr := xs[*...1]
let genIH := xs[1]!
let extraParams := xs[2...*]
-- open body with the same arg
let body instantiateLambda body targets
lambdaTelescope1 body fun oldIH body => do
let body instantiateLambda body extraParams
let body' withRewrittenMotiveArg goal (rwFun #[name]) fun goal => do
buildInductionBody #[oldIH, genIH.fvarId!] #[] goal oldIH genIH.fvarId! isRecCall body
if body'.containsFVar oldIH then
throwError m!"Did not fully eliminate `{mkFVar oldIH}` from induction principle body:{indentExpr body}"
mkLambdaFVars (targets.push genIH) ( mkLambdaFVars extraParams body')
let e' := mkApp2 e' body' target
let e' mkLambdaFVars #[target] e'
let e' abstractIndependentMVars mvars ( motive.fvarId!.getDecl).index e'
let e' mkLambdaFVars #[motive] e'
-- We used to pass (usedOnly := false) below in the hope that the types of the
-- induction principle match the type of the function better.
-- But this leads to avoidable parameters that make functional induction strictly less
-- useful (e.g. when the unused parameter mentions bound variables in the users' goal)
let (paramMask, e') mkLambdaFVarsMasked fixedParamPerms e'
let e' instantiateMVars e'
return (e', paramMask)
| _ =>
if funBody.isAppOf ``WellFounded.fix then
throwError "Function `{name}` defined via `{.ofConstName ``WellFounded.fix}` with unexpected arity {funBody.getAppNumArgs}:{indentExpr funBody}"
unless funBody.isApp && funBody.appFn!.isApp do
throwError "functional induction: unexpected body {funBody}"
let body := funBody.appFn!.appArg!
let target := funBody.appArg!
unless params.back! == target do
throwError "functional induction: expected the target as last parameter{indentExpr e}"
let fixedParamPerms := params.pop
let motiveType
if unfolding then
withLocalDeclD `r ( instantiateForall info.type params) fun r =>
mkForallFVars #[target, r] (.sort 0)
else
throwError "Function `{name}` not defined via `{.ofConstName ``WellFounded.fix}`:{indentExpr funBody}"
mkForallFVars #[target] (.sort 0)
withLocalDeclD `motive motiveType fun motive => do
let fn := mkAppN ( mkConstWithLevelParams name) fixedParamPerms
let isRecCall : Expr Option Expr := fun e =>
e.withApp fun f xs =>
if f.isFVarOf motive.fvarId! && xs.size > 0 then
mkApp fn xs[0]!
else
none
let motiveArg
if unfolding then
let motiveArg := mkApp2 motive target (mkAppN ( mkConstWithLevelParams name) params)
mkLambdaFVars #[target] motiveArg
else
pure motive
let e' match_expr funBody with
| fix@WellFounded.fix α _motive rel wf _body _target =>
let e' := .const ``WellFounded.fix [fix.constLevels![0]!, levelZero]
pure <| mkApp4 e' α motiveArg rel wf
| fix@WellFounded.Nat.fix α _motive measure _body _target =>
let e' := .const `WellFounded.Nat.fix [fix.constLevels![0]!, levelZero]
pure <| mkApp3 e' α motiveArg measure
| _ =>
if funBody.isAppOf ``WellFounded.fix || funBody.isAppOf `WellFounded.Nat.Fix then
throwError "Function {name} defined via WellFounded.fix with unexpected arity {funBody.getAppNumArgs}:{indentExpr funBody}"
else
throwError "Function {name} not defined via WellFounded.fix:{indentExpr funBody}"
check e'
let (body', mvars) M2.run do
forallTelescope ( inferType e').bindingDomain! fun xs goal => do
if xs.size 2 then
throwError "expected recursor argument to take 2 parameters, got {xs}" else
let targets : Array Expr := xs[*...1]
let genIH := xs[1]!
let extraParams := xs[2...*]
-- open body with the same arg
let body instantiateLambda body targets
lambdaTelescope1 body fun oldIH body => do
let body instantiateLambda body extraParams
let body' withRewrittenMotiveArg goal (rwFun #[name]) fun goal => do
buildInductionBody #[oldIH, genIH.fvarId!] #[] goal oldIH genIH.fvarId! isRecCall body
if body'.containsFVar oldIH then
throwError m!"Did not fully eliminate `{mkFVar oldIH}` from induction principle body:{indentExpr body}"
mkLambdaFVars (targets.push genIH) ( mkLambdaFVars extraParams body')
let e' := mkApp2 e' body' target
let e' mkLambdaFVars #[target] e'
let e' abstractIndependentMVars mvars ( motive.fvarId!.getDecl).index e'
let e' mkLambdaFVars #[motive] e'
-- We used to pass (usedOnly := false) below in the hope that the types of the
-- induction principle match the type of the function better.
-- But this leads to avoidable parameters that make functional induction strictly less
-- useful (e.g. when the unused parameter mentions bound variables in the users' goal)
let (paramMask, e') mkLambdaFVarsMasked fixedParamPerms e'
let e' instantiateMVars e'
return (e', paramMask)
unless ( isTypeCorrect e') do
logError m!"failed to derive a type-correct induction principle:{indentExpr e'}"

View File

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
module
prelude
public import Lean.Meta.Tactic.Grind.Types
import Lean.Meta.Injective
import Lean.Meta.Tactic.Grind.Simp
public section
namespace Lean.Meta.Grind
@@ -33,20 +34,13 @@ private partial def propagateInjEqs (eqs : Expr) (proof : Expr) (generation : Na
reportIssue! "unexpected injectivity theorem result type{indentExpr eqs}"
return ()
/--
Given constructors `a` and `b`, propagate equalities if they are the same,
and close goal if they are different.
-/
def propagateCtor (a b : Expr) : GoalM Unit := do
let aType whnfD ( inferType a)
let bType whnfD ( inferType b)
unless ( isDefEqD aType bType) do
return ()
/-- Homogeneous case where constructor applications `a` and `b` have the same type `α`. -/
private def propagateCtorHomo (α : Expr) (a b : Expr) : GoalM Unit := do
let ctor₁ := a.getAppFn
let ctor₂ := b.getAppFn
if ctor₁ == ctor₂ then
let .const ctorName _ := a.getAppFn | return ()
let injDeclName := Name.mkStr ctorName "inj"
let .const ctorName _ := ctor₁ | return ()
let injDeclName := mkInjectiveTheoremNameFor ctorName
unless ( getEnv).contains injDeclName do return ()
let info getConstInfo injDeclName
let n := info.type.getForallArity
@@ -62,9 +56,57 @@ def propagateCtor (a b : Expr) : GoalM Unit := do
let gen := max ( getGeneration a) ( getGeneration b)
propagateInjEqs injLemmaType injLemma gen
else
let .const declName _ := aType.getAppFn | return ()
let .const declName _ := α.getAppFn | return ()
let noConfusionDeclName := Name.mkStr declName "noConfusion"
unless ( getEnv).contains noConfusionDeclName do return ()
closeGoal ( mkNoConfusion ( getFalseExpr) ( mkEqProof a b))
/-- Heterogeneous case where constructor applications `a` and `b` have different types `α` and `β`. -/
private def propagateCtorHetero (a b : Expr) : GoalM Unit := do
a.withApp fun ctor₁ args₁ =>
b.withApp fun ctor₂ args₂ => do
let .const ctorName₁ us₁ := ctor₁ | return ()
let .const ctorName₂ us₂ := ctor₂ | return ()
let .ctorInfo ctorVal₁ getConstInfo ctorName₁ | return ()
let .ctorInfo ctorVal₂ getConstInfo ctorName₂ | return ()
unless ctorVal₁.induct == ctorVal₂.induct do return ()
let params₁ := args₁[*...ctorVal₁.numParams]
let params₂ := args₂[*...ctorVal₂.numParams]
let fields₁ := args₁[ctorVal₁.numParams...*]
let fields₂ := args₂[ctorVal₂.numParams...*]
if h : params₁.size params₂.size then return () else
unless ( params₁.size.allM fun i h => isDefEq params₁[i] params₂[i]) do return ()
unless us₁.length == us₂.length do return ()
unless ( us₁.zip us₂ |>.allM fun (u₁, u₂) => isLevelDefEq u₁ u₂) do return ()
let gen := max ( getGeneration a) ( getGeneration b)
if ctorName₁ == ctorName₂ then
let hinjDeclName := mkHInjectiveTheoremNameFor ctorName₁
unless ( getEnv).containsOnBranch hinjDeclName do
let _ executeReservedNameAction hinjDeclName
let proof := mkAppN (mkConst hinjDeclName us₁) params₁
let proof := mkAppN (mkAppN proof fields₁) fields₂
addNewRawFact proof ( inferType proof) gen (.inj (.decl hinjDeclName))
else
let some indices₁ getCtorAppIndices? a | return ()
let some indices₂ getCtorAppIndices? b | return ()
let noConfusionName := ctorVal₁.induct.str "noConfusion"
let noConfusion := mkAppN (mkConst noConfusionName (0 :: us₁)) params₁
let noConfusion := mkApp noConfusion ( getFalseExpr)
let noConfusion := mkApp (mkAppN noConfusion indices₁) a
let noConfusion := mkApp (mkAppN noConfusion indices₂) b
let proof := noConfusion
addNewRawFact proof ( inferType proof) gen (.inj (.decl noConfusionName))
/--
Given constructors `a` and `b`, propagate equalities if they are the same,
and close goal if they are different.
-/
def propagateCtor (a b : Expr) : GoalM Unit := do
let aType whnfD ( inferType a)
let bType whnfD ( inferType b)
if ( isDefEqD aType bType) then
propagateCtorHomo aType a b
else
propagateCtorHetero a b
end Lean.Meta.Grind

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