Compare commits

...

46 Commits

Author SHA1 Message Date
Kim Morrison
ac7fc3ec45 dfold_add 2025-05-21 21:14:00 +10:00
Kim Morrison
1287043c7b dfoldRev theorems 2025-05-21 20:28:16 +10:00
Kim Morrison
c077c2d429 feat: Nat.dfold 2025-05-21 20:28:15 +10:00
Kim Morrison
3bf95e9b58 feat: add List/Array/Vector.ofFnM (#8389)
This PR adds the `List/Array/Vector.ofFnM`, the monadic analogues of
`ofFn`, along with basic theory.

At the same time we pave some potholes in nearby API.

---------

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
2025-05-20 05:28:29 +00:00
Kim Morrison
bc21b57396 chore: use HMul in Lean.Grind.Module (#8414) 2025-05-20 04:22:06 +00:00
Kim Morrison
6395d69140 feat: add HashMap.get*_filter* lemmas specialized for LawfulBEq (#8399)
This PR adds variants of `HashMap.getElem?_filter` that assume
`LawfulBEq` and have a simpler right-hand-side. `simp` can already
achieve these, via rewriting with `getKey_eq` under the lambda. However
`grind` can not, and these lemmas help `grind` work with `HashMap`
goals. There are variants for all variants of `HashMap`,
`getElem?/getElem/getElem!/getD`, and for `filter` and `filterMap`.
2025-05-20 03:04:32 +00:00
Leonardo de Moura
4ba72aeef7 feat: missing normalization rules in grind (#8413)
This PR implements normalization rules that pull universal quantifiers
across disjunctions. This is a common normalization step performed by
first-order theorem provers.
2025-05-20 02:38:29 +00:00
Leonardo de Moura
e984473886 fix: markNestedProofs preprocessor in grind (#8412)
This PR fixes the `markNestedProofs` preprocessor used in `grind`. There
was a missing case (e.g., `Expr.mdata`)
2025-05-20 01:46:23 +00:00
Leonardo de Moura
88f6439955 fix: case-splitting in grind (#8410)
This PR fixes a case-splitting heuristic in `grind` and simplifies the
proof for test `grind_palindrome2.lean`.
2025-05-20 00:51:47 +00:00
Cameron Zwarich
fc8f290347 feat: support native literals of size unsigned integer types (#8409)
This PR adds support to LCNF for native UInt8/UInt16/UInt32/UInt64
literals.
2025-05-20 00:38:38 +00:00
Cameron Zwarich
423b31755d chore: remove dependency of pretty-printing LCNF.LitValue on toExpr (#8408) 2025-05-19 22:55:21 +00:00
jrr6
d1ec806834 feat: improve error messages in invalid match alternatives (#8368)
This PR improves the error messages produced by invalid pattern-match
alternatives and improves parity in error placement between
pattern-matching tactics and elaborators.

Closes #7170
2025-05-19 17:40:41 +00:00
jrr6
b93231f97e feat: improve inductive type parameter error messages (#8338)
This PR improves the error messages displayed in `inductive`
declarations when type parameters are invalid or absent.

Closes #2195 by improving the relevant error message.
2025-05-19 17:03:49 +00:00
Kim Morrison
f40d72ea47 feat: typeclasses for grind to work with ordered modules (#8347)
This PR adds draft typeclasses for `grind` to process facts about
ordered modules. These interfaces will evolve as the implementation
develops.
2025-05-19 13:55:38 +00:00
Kim Morrison
10fdfc54cb chore: upstream HSMul notation typeclass (#8401)
Upstreaming the `HSMul` notation typeclass, to enable `grind` to process
goals using it.
2025-05-19 12:37:08 +00:00
David Thrane Christiansen
943a9c6a43 chore: revert mistaken deletion (#8404)
This PR reverts the deletion of files that should not have been removed
with the old documentation site.
2025-05-19 12:14:09 +00:00
Wojciech Rozowski
a8a6f71abb fix: add monotonicity lemmas for universal quantifiers (#8403)
This PR adds missing monotonicity lemmas for universal quantifiers, that
are used in defining (co)inductive predicates.
2025-05-19 11:27:46 +00:00
Markus Himmel
9ad4414642 feat: Option lemmas (#8379)
This PR adds missing `Option` lemmas.

Also:

- generalize `bindM` from `Monad` to `Pure`
- change the `simp` normal form of both `<|>` and `Option.orElse` to
`Option.or`
2025-05-19 08:59:31 +00:00
Kim Morrison
efe2ab4c04 chore: remove duplicate instances (#8397)
This PR cleans up many duplicate instances (or, in some cases,
needlessly duplicated `def X := ...; instance Y := X`).
2025-05-19 04:36:06 +00:00
Cameron Zwarich
831026bcf4 chore: remove redundant ToFormat/ToString debug printing instances (#8400) 2025-05-19 03:31:22 +00:00
Cameron Zwarich
fbac0d2ddb chore: use LitValue.toExpr instead of duplicating its definition (#8398) 2025-05-19 01:33:47 +00:00
Eric Wieser
e7b8df0c0e fix: change Array. lemma to be about Array (#8392)
This PR corrects some `Array` lemmas to be about `Array` not `List`.

Discovered [on
Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/duplicate.20declarations/near/518942094)
2025-05-19 00:29:35 +00:00
Kim Morrison
601ea24e31 chore: add failing grind tests for noncommutative/non-negation rings (#8396) 2025-05-19 00:26:16 +00:00
Cameron Zwarich
ca037ded0d chore: rename LitValue.natVal/strVal to .nat/str (#8394) 2025-05-18 22:10:58 +00:00
Cameron Zwarich
006d2925ba chore: rename LetValue.value to .lit (#8393) 2025-05-18 21:12:35 +00:00
Mac Malone
c8290bd942 fix: lake: import Lake w/ precompiled modules on MacOS (#8383)
This PR fixes the use of `import Lake` with precompiled modules, which
was previously broken on MacOS.

Closes #7388.
2025-05-16 21:24:13 +00:00
Henrik Böving
b7b95896aa fix: tests that suffer from renaming (#8386) 2025-05-16 17:18:52 +00:00
Lean stage0 autoupdater
e46daa8ee6 chore: update stage0 2025-05-16 16:17:48 +00:00
Kyle Miller
3854ba87b6 feat: pretty print letFun using have syntax (#8372)
This PR modifies the pretty printer to use `have` syntax instead of
`let_fun` syntax.
2025-05-16 15:10:01 +00:00
Sebastian Ullrich
4d58a3d124 feat: revamp aux decl name generation (#8363)
This PR unifies various ways of naming auxiliary declarations in a
conflict-free way and ensures the method is compatible with diverging
branches of elaboration such as parallelism or Aesop-like
backtracking+replaying search.
2025-05-16 14:57:18 +00:00
Joachim Breitner
6b7a803bf4 fix: mapError to store message data context (#8375)
This PR ensures that using `mapError` to expand an error message uses
`addMessageContext` to include the current context, so that expressions
are rendered correctly. Also adds a `preprendError` variant with a more
convenient argument order for the common cases of
prepending-and-indenting.
2025-05-16 14:46:23 +00:00
Joachim Breitner
0e96318c72 chore: update DTreeMap proofs with more unfolding induction (#8382)
This is a post-stage0 update following #8359.
2025-05-16 14:41:37 +00:00
Sebastian Ullrich
7994e55d80 chore: try refining some benchmark settings (#8377) 2025-05-16 11:24:11 +00:00
Lean stage0 autoupdater
d24aa91232 chore: update stage0 2025-05-16 10:08:06 +00:00
Joachim Breitner
e7b61232c9 feat: more parameters in .fun_cases theorem (#8359)
This PR improves the functional cases principles, by making a more
educated guess which function parameters should be targets and which
should remain parameters (or be dropped). This simplifies the
principles, and increases the chance that `fun_cases` can unfold the
function call.

Fixes #8296 (at least for the common cases, I hope.)
2025-05-16 09:06:21 +00:00
Sebastian Ullrich
af7eb01f29 chore: build leanc with Lake under USE_LAKE (#8336)
Removes the last use of stdlib.make.in in this configuration outside
stage 0.
2025-05-16 08:07:34 +00:00
Markus Himmel
ca9b3eb75f chore: variants of dite_eq_left_iff (#8357)
This PR adds variants of `dite_eq_left_iff` that will be useful in a
future PR.
2025-05-16 05:42:12 +00:00
Cameron Zwarich
a817067295 chore: adopt Option.getD (#8374) 2025-05-16 05:07:49 +00:00
Cameron Zwarich
fcb6bcee67 fix: revert #8023 now that it is redundant (#8371)
This PR reverts #8023 now that it has been made redundant by the more
general fix in #8367.
2025-05-16 00:53:30 +00:00
Kim Morrison
73509d03f3 chore: cleanup previously failing grind test (#8370)
This test is superseded by the `qsort_grind` branch.
2025-05-16 00:24:33 +00:00
Leonardo de Moura
6448547f41 fix: instantiateTheorem in grind (#8369)
This PR fixes a type error at `instantiateTheorem` function used in
`grind`. It was failing to instantiate theorems such as
```lean
theorem getElem_reverse {xs : Array α} {i : Nat} (hi : i < xs.reverse.size)
    : (xs.reverse)[i] = xs[xs.size - 1 - i]'(by simp at hi; omega)
```
in examples such as
```lean
example (xs : Array Nat) (w : xs.reverse = xs) (j : Nat) (hj : 0 ≤ j) (hj' : j < xs.size / 2)
    : xs[j] = xs[xs.size - 1 - j]
```
generating the issue
```lean
  [issue] type error constructing proof for Array.getElem_reverse
      when assigning metavariable ?hi with
        ‹j < xs.toList.length›
      has type
        j < xs.toList.length : Prop
      but is expected to have type
        j < xs.reverse.size : Prop
```
2025-05-15 23:06:32 +00:00
Cameron Zwarich
632b688cb7 feat: add an LCNF pass to convert structure projections to cases expressions (#8367)
This PR adds a new `structProjCases` pass to the new compiler, analogous
to the `struct_cases_on` pass in the old compiler, which converts all
projections from structs into `cases` expressions. When lowered to IR,
this causes all of the projections from a single structure to be grouped
together, which is an invariant relied upon by the IR RC passes (at
least for linearity, if not general correctness).
2025-05-15 21:54:25 +00:00
Cameron Zwarich
c5335b6f9a fix: give Ordering.then the expose attribute (#8366)
This PR adds the `expose` attribute to `Ordering.then`. This is required
for building with the new compiler, but works fine with the old compiler
because it silently ignores the missing definition.
2025-05-15 21:25:40 +00:00
Leonardo de Moura
a594f655da fix: use withReducibleAndIntances to match ground patterns (#8365)
This PR fixes the transparency mode for ground patterns. This is
important for implicit instances. Here is a mwe for an issue detected
while testing `grind` in Mathlib.
```lean
example (a : Nat) : max a a = a := by
  grind

instance : Max Nat where
  max := Nat.max

example (a : Nat) : max a a = a := by
  grind -- Should work
```
2025-05-15 19:50:46 +00:00
Leonardo de Moura
7a6bca5276 feat: basic support for eta reduction in grind (#7977)
This PR adds basic support for eta-reduction to `grind`.

---------

Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
2025-05-15 18:34:56 +00:00
Joachim Breitner
e5393cf6bc fix: cases tactic to handle non-atomic eliminator well (#8361)
This PR fixes a bug in the `cases` tacic introduced in #3188 that arises
when cases (not induction) is used with a non-atomic expression in using
and the argument indexing gets confused.

This fixes #8360.
2025-05-15 16:59:11 +00:00
717 changed files with 5229 additions and 1208 deletions

9
doc/std/README.md Normal file
View File

@@ -0,0 +1,9 @@
# The Lean standard library
This directory contains development information about the Lean standard library. The user-facing documentation of the standard library
is part of the [Lean Language Reference](https://lean-lang.org/doc/reference/latest/).
Here you will find
* the [standard library vision document](./vision.md), including the call for contributions,
* the [standard library style guide](./style.md), and
* the [standard library naming conventions](./naming.md).

3
doc/std/naming-tree.svg Normal file

File diff suppressed because one or more lines are too long

After

Width:  |  Height:  |  Size: 68 KiB

260
doc/std/naming.md Normal file
View File

@@ -0,0 +1,260 @@
# Standard library naming conventions
The easiest way to access a result in the standard library is to correctly guess the name of the declaration (possibly with the help of identifier autocompletion). This is faster and has lower friction than more sophisticated search tools, so easily guessable names (which are still reasonably short) make Lean users more productive.
The guide that follows contains very few hard rules, many heuristics and a selection of examples. It cannot and does not present a deterministic algorithm for choosing good names in all situations. It is intended as a living document that gets clarified and expanded as situations arise during code reviews for the standard library. If applying one of the suggestions in this guide leads to nonsensical results in a certain situation, it is
probably safe to ignore the suggestion (or even better, suggest a way to improve the suggestion).
## Prelude
Identifiers use a mix of `UpperCamelCase`, `lowerCamelCase` and `snake_case`, used for types, data, and theorems, respectively.
Structure fields should be named such that the projections have the correct names.
## Naming convention for types
When defining a type, i.e., a (possibly 0-ary) function whose codomain is Sort u for some u, it should be named in UpperCamelCase. Examples include `List`, and `List.IsPrefix`.
When defining a predicate, prefix the name by `Is`, like in `List.IsPrefix`. The `Is` prefix may be omitted if
* the resulting name would be ungrammatical, or
* the predicate depends on additional data in a way where the `Is` prefix would be confusing (like `List.Pairwise`), or
* the name is an adjective (like `Std.Time.Month.Ordinal.Valid`)
## Namespaces and generalized projection notation
Almost always, definitions and theorems relating to a type should be placed in a namespace with the same name as the type. For example, operations and theorems about lists should be placed in the `List` namespace, and operations and theorems about `Std.Time.PlainDate` should be placed in the `Std.Time.PlainDate` namespace.
Declarations in the root namespace will be relatively rare. The most common type of declaration in the root namespace are declarations about data and properties exported by notation type classes, as long as they are not about a specific type implementing that type class. For example, we have
```lean
theorem beq_iff_eq [BEq α] [LawfulBEq α] {a b : α} : a == b a = b := sorry
```
in the root namespace, but
```lean
theorem List.cons_beq_cons [BEq α] {a b : α} {l₁ l₂ : List α} :
(a :: l₁ == b :: l₂) = (a == b && l₁ == l₂) := rfl
```
belongs in the `List` namespace.
Subtleties arise when multiple namespaces are in play. Generally, place your theorem in the most specific namespace that appears in one of the hypotheses of the theorem. The following names are both correct according to this convention:
```lean
theorem List.Sublist.reverse : l₁ <+ l₂ l₁.reverse <+ l₂.reverse := sorry
theorem List.reverse_sublist : l₁.reverse <+ l₂.reverse l₁ <+ l₂ := sorry
```
Notice that the second theorem does not have a hypothesis of type `List.Sublist l` for some `l`, so the name `List.Sublist.reverse_iff` would be incorrect.
The advantage of placing results in a namespace like `List.Sublist` is that it enables generalized projection notation, i.e., given `h : l₁ <+ l₂`,
one can write `h.reverse` to obtain a proof of `l₁.reverse <+ l₂.reverse`. Thinking about which dot notations are convenient can act as a guideline
for deciding where to place a theorem, and is, on occasion, a good reason to duplicate a theorem into multiple namespaces.
### The `Std` namespace
New types that are added will usually be placed in the `Std` namespace and in the `Std/` source directory, unless there are good reasons to place
them elsewhere.
Inside the `Std` namespace, all internal declarations should be `private` or else have a name component that clearly marks them as internal, preferably
`Internal`.
## Naming convention for data
When defining data, i.e., a (possibly 0-ary) function whose codomain is not Sort u, but has type Type u for some u, it should be named in lowerCamelCase. Examples include `List.append` and `List.isPrefixOf`.
If your data is morally fully specified by its type, then use the naming procedure for theorems described below and convert the result to lower camel case.
If your function returns an `Option`, consider adding `?` as a suffix. If your function may panic, consider adding `!` as a suffix. In many cases, there will be multiple variants of a function; one returning an option, one that may panic and possibly one that takes a proof argument.
## Naming algorithm for theorems and some definitions
There is, in principle, a general algorithm for naming a theorem. The problem with this algorithm is that it produces very long and unwieldy names which need to be shortened. So choosing a name for a declaration can be thought of as consisting of a mechanical part and a creative part.
Usually the first part is to decide which namespace the result should live in, according to the guidelines described above.
Next, consider the type of your declaration as a tree. Inner nodes of this tree are function types or function applications. Leaves of the tree are 0-ary functions or bound variables.
As an example, consider the following result from the standard library:
```lean
example {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
[Inhabited β] {m : Std.HashMap α β} {a : α} {h' : a m} : m[a]? = some (m[a]'h') :=
sorry
```
The correct namespace is clearly `Std.HashMap`. The corresponding tree looks like this:
![](naming-tree.svg)
The preferred spelling of a notation can be looked up by hovering over the notation.
Now traverse the tree and build a name according to the following rules:
* When encountering a function type, first turn the result type into a name, then all of the argument types from left to right, and join the names using `_of_`.
* When encountering a function that is neither an infix notation nor a structure projection, first put the function name and then the arguments, joined by an underscore.
* When encountering an infix notation, join the arguments using the name of the notation, separated by underscores.
* When encountering a structure projection, proceed as for normal functions, but put the name of the projection last.
* When encountering a name, put it in lower camel case.
* Skip bound variables and proofs.
* Type class arguments are also generally skipped.
When encountering namespaces names, concatenate them in lower camel case.
Applying this algorithm to our example yields the name `Std.HashMap.getElem?_eq_optionSome_getElem_of_mem`.
From there, the name should be shortened, using the following heuristics:
* The namespace of functions can be omitted if it is clear from context or if the namespace is the current one. This is almost always the case.
* For infix operators, it is possible to leave out the RHS or the name of the notation and the RHS if they are clear from context.
* Hypotheses can be left out if it is clear that they are required or if they appear in the conclusion.
Based on this, here are some possible names for our example:
1. `Std.HashMap.getElem?_eq`
2. `Std.HashMap.getElem?_eq_of_mem`
3. `Std.HashMap.getElem?_eq_some`
4. `Std.HashMap.getElem?_eq_some_of_mem`
5. `Std.HashMap.getElem?_eq_some_getElem`
6. `Std.Hashmap.getElem?_eq_some_getElem_of_mem`
Choosing a good name among these then requires considering the context of the lemma. In this case it turns out that the first four options are underspecified as there is also a lemma relating `m[a]?` and `m[a]!` which could have the same name. This leaves the last two options, the first of which is shorter, and this is how the lemma is called in the Lean standard library.
Here are some additional examples:
```lean
example {x y : List α} (h : x <+: y) (hx : x []) :
x.head hx = y.head (h.ne_nil hx) := sorry
```
Since we have an `IsPrefix` parameter, this should live in the `List.IsPrefix` namespace, and the algorithm suggests `List.IsPrefix.head_eq_head_of_ne_nil`, which is shortened to `List.IsPrefix.head`. Note here the difference between the namespace name (`IsPrefix`) and the recommended spelling of the corresponding notation (`prefix`).
```lean
example : l₁ <+: l₂ reverse l₁ <:+ reverse l₂ := sorry
```
Again, this result should be in the `List.IsPrefix` namespace; the algorithm suggests `List.IsPrefix.reverse_prefix_reverse`, which becomes `List.IsPrefix.reverse`.
The following examples show how the traversal order often matters.
```lean
theorem Nat.mul_zero (n : Nat) : n * 0 = 0 := sorry
theorem Nat.zero_mul (n : Nat) : 0 * n = 0 := sorry
```
Here we see that one name may be a prefix of another name:
```lean
theorem Int.mul_ne_zero {a b : Int} (a0 : a 0) (b0 : b 0) : a * b 0 := sorry
theorem Int.mul_ne_zero_iff {a b : Int} : a * b 0 a 0 b 0 := sorry
```
It is usually a good idea to include the `iff` in a theorem name even if the name would still be unique without the name. For example,
```lean
theorem List.head?_eq_none_iff : l.head? = none l = [] := sorry
```
is a good name: if the lemma was simply called `List.head?_eq_none`, users might try to `apply` it when the goal is `l.head? = none`, leading
to confusion.
The more common you expect (or want) a theorem to be, the shorter you should try to make the name. For example, we have both
```lean
theorem Std.HashMap.getElem?_eq_none_of_contains_eq_false {a : α} : m.contains a = false m[a]? = none := sorry
theorem Std.HashMap.getElem?_eq_none {a : α} : ¬a m m[a]? = none := sorry
```
As users of the hash map are encouraged to use ∈ rather than contains, the second lemma gets the shorter name.
## Special cases
There are certain special “keywords” that may appear in identifiers.
| Keyword | Meaning | Example |
| :---- | :---- | :---- |
| `def` | Unfold a definition. Avoid this for public APIs. | `Nat.max_def` |
| `refl` | Theorems of the form `a R a`, where R is a reflexive relation and `a` is an explicit parameter | `Nat.le_refl` |
| `rfl` | Like `refl`, but with `a` implicit | `Nat.le_rfl` |
| `irrefl` | Theorems of the form `¬a R a`, where R is an irreflexive relation | `Nat.lt_irrefl` |
| `symm` | Theorems of the form `a R b → b R a`, where R is a symmetric relation (compare `comm` below) | `Eq.symm` |
| `trans` | Theorems of the form `a R b → b R c → a R c`, where R is a transitive relation (R may carry data) | `Eq.trans` |
| `antisymmm` | Theorems of the form `a R b → b R a → a = b`, where R is an antisymmetric relation | `Nat.le_antisymm` |
| `congr` | Theorems of the form `a R b → f a S f b`, where R and S are usually equivalence relations | `Std.HashMap.mem_congr` |
| `comm` | Theorems of the form `f a b = f b a` (compare `symm` above) | `Eq.comm`, `Nat.add_comm` |
| `assoc` | Theorems of the form `g (f a b) c = f a (g b c)` (note the order! In most cases, we have f = g) | `Nat.add_sub_assoc` |
| `distrib` | Theorems of the form `f (g a b) = g (f a) (f b)` | `Nat.add_left_distrib` |
| `self` | May be used if a variable appears multiple times in the conclusion | `List.mem_cons_self` |
| `inj` | Theorems of the form `f a = f b ↔ a = b`. | `Int.neg_inj`, `Nat.add_left_inj` |
| `cancel` | Theorems which have one of the forms `f a = f b → a = b` or `g (f a) = a`, where `f` and `g` usually involve a binary operator | `Nat.add_sub_cancel` |
| `cancel_iff` | Same as `inj`, but with different conventions for left and right (see below) | `Nat.add_right_cancel_iff` |
| `ext` | Theorems of the form `f a = f b → a = b`, where `f` usually involves some kind of projection | `List.ext_getElem`
| `mono` | Theorems of the form `a R b → f a R f b`, where `R` is a transitive relation | `List.countP_mono_left`
### Left and right
The keywords left and right are useful to disambiguate symmetric variants of theorems.
```lean
theorem imp_congr_left (h : a b) : (a c) (b c) := sorry
theorem imp_congr_right (h : a (b c)) : (a b) (a c) := sorry
```
It is not always obvious which version of a theorem should be “left” and which should be “right”.
Heuristically, the theorem should name the side which is “more variable”, but there are exceptions. For some of the special keywords discussed in this section, there are conventions which should be followed, as laid out in the following examples:
```lean
theorem Nat.left_distrib (n m k : Nat) : n * (m + k) = n * m + n * k := sorry
theorem Nat.right_distrib (n m k : Nat) : (n + m) * k = n * k + m * k := sorry
theorem Nat.add_left_cancel {n m k : Nat} : n + m = n + k m = k := sorry
theorem Nat.add_right_cancel {n m k : Nat} : n + m = k + m n = k := sorry
theorem Nat.add_left_cancel_iff {m k n : Nat} : n + m = n + k m = k := sorry
theorem Nat.add_right_cancel_iff {m k n : Nat} : m + n = k + n m = k := sorry
theorem Nat.add_left_inj {m k n : Nat} : m + n = k + n m = k := sorry
theorem Nat.add_right_inj {m k n : Nat} : n + m = n + k m = k := sorry
```
Note in particular that the convention is opposite for `cancel_iff` and `inj`.
```lean
theorem Nat.add_sub_self_left (a b : Nat) : (a + b) - a = b := sorry
theorem Nat.add_sub_self_right (a b : Nat) : (a + b) - b = a := sorry
theorem Nat.add_sub_cancel (n m : Nat) : (n + m) - m = n := sorry
```
## Primed names
Avoid disambiguating variants of a concept by appending the `'` character (e.g., introducing both `BitVec.sshiftRight` and `BitVec.sshiftRight'`), as it is impossible to tell the difference without looking at the type signature, the documentation or even the code, and even if you know what the two variants are there is no way to tell which is which. Prefer descriptive pairs `BitVec.sshiftRightNat`/`BitVec.sshiftRight`.
## Acronyms
For acronyms which are three letters or shorter, all letters should use the same case as dictated by the convention. For example, `IO` is a correct name for a type and the name `IO.Ref` may become `IORef` when used as part of a definition name and `ioRef` when used as part of a theorem name.
For acronyms which are at least four letters long, switch to lower case starting from the second letter. For example, `Json` is a correct name for a type, as is `JsonRPC`.
If an acronym is typically spelled using mixed case, this mixed spelling may be used in identifiers (for example `Std.Net.IPv4Addr`).
## Simp sets
Simp sets centered around a conversion function should be called `source_to_target`. For example, a simp set for the `BitVec.toNat` function, which goes from `BitVec` to
`Nat`, should be called `bitvec_to_nat`.
## Variable names
We make the following recommendations for variable names, but without insisting on them:
* Simple hypotheses should be named `h`, `h'`, or using a numerical sequence `h₁`, `h₂`, etc.
* Another common name for a simple hypothesis is `w` (for "witness").
* `List`s should be named `l`, `l'`, `l₁`, etc, or `as`, `bs`, etc.
(Use of `as`, `bs` is encouraged when the lists are of different types, e.g. `as : List α` and `bs : List β`.)
`xs`, `ys`, `zs` are allowed, but it is better if these are reserved for `Array` and `Vector`.
A list of lists may be named `L`.
* `Array`s should be named `xs`, `ys`, `zs`, although `as`, `bs` are encouraged when the arrays are of different types, e.g. `as : Array α` and `bs : Array β`.
An array of arrays may be named `xss`.
* `Vector`s should be named `xs`, `ys`, `zs`, although `as`, `bs` are encouraged when the vectors are of different types, e.g. `as : Vector α n` and `bs : Vector β n`.
A vector of vectors may be named `xss`.
* A common exception for `List` / `Array` / `Vector` is to use `acc` for an accumulator in a recursive function.
* `i`, `j`, `k` are preferred for numerical indices.
Descriptive names such as `start`, `stop`, `lo`, and `hi` are encouraged when they increase readability.
* `n`, `m` are preferred for sizes, e.g. in `Vector α n` or `xs.size = n`.
* `w` is preferred for the width of a `BitVec`.

522
doc/std/style.md Normal file
View File

@@ -0,0 +1,522 @@
# Standard library style
Please take some time to familiarize yourself with the stylistic conventions of
the project and the specific part of the library you are planning to contribute
to. While the Lean compiler may not enforce strict formatting rules,
consistently formatted code is much easier for others to read and maintain.
Attention to formatting is more than a cosmetic concern—it reflects the same
level of precision and care required to meet the deeper standards of the Lean 4
standard library.
Below we will give specific formatting prescriptions for various language constructs. Note that this style guide only applies to the Lean standard library, even though some examples in the guide are taken from other parts of the Lean code base.
## Basic whitespace rules
Syntactic elements (like `:`, `:=`, `|`, `::`) are surrounded by single spaces, with the exception of `,` and `;`, which are followed by a space but not preceded by one. Delimiters (like `()`, `{}`) do not have spaces on the inside, with the exceptions of subtype notation and structure instance notation.
Examples of correctly formatted function parameters:
* `{α : Type u}`
* `[BEq α]`
* `(cmp : αα → Ordering)`
* `(hab : a = b)`
* `{d : { l : List ((n : Nat) × Vector Nat n) // l.length % 2 = 0 }}`
Examples of correctly formatted terms:
* `1 :: [2, 3]`
* `letI : Ord α := ⟨cmp⟩; True`
* `(⟨2, 3⟩ : Nat × Nat)`
* `((2, 3) : Nat × Nat)`
* `{ x with fst := f (4 + f 0), snd := 4, .. }`
* `match 1 with | 0 => 0 | _ => 0`
* `fun ⟨a, b⟩ _ _ => by cases hab <;> apply id; rw [hbc]`
Configure your editor to remove trailing whitespace. If you have set up Visual Studio Code for Lean development in the recommended way then the correct setting is applied automatically.
## Splitting terms across multiple lines
When splitting a term across multiple lines, increase indentation by two spaces starting from the second line. When splitting a function application, try to split at argument boundaries. If an argument itself needs to be split, increase indentation further as appropriate.
When splitting at an infix operator, the operator goes at the end of the first line, not at the beginning of the second line. When splitting at an infix operator, you may or may not increase indentation depth, depending on what is more readable.
When splitting an `if`-`then`-`else` expression, the `then` keyword wants to stay with the condition and the `else` keyword wants to stay with the alternative term. Otherwise, indent as if the `if` and `else` keywords were arguments to the same function.
When splitting a comma-separated bracketed sequence (i.e., anonymous constructor application, list/array/vector literal, tuple) it is allowed to indent subsequent lines for alignment, but indenting by two spaces is also allowed.
Do not orphan parentheses.
Correct:
```lean
def MacroScopesView.isPrefixOf (v₁ v₂ : MacroScopesView) : Bool :=
v₁.name.isPrefixOf v₂.name &&
v₁.scopes == v₂.scopes &&
v₁.mainModule == v₂.mainModule &&
v₁.imported == v₂.imported
```
Correct:
```lean
theorem eraseP_eq_iff {p} {l : List α} :
l.eraseP p = l'
(( a l, ¬ p a) l = l')
a l₁ l₂, ( b l₁, ¬ p b) p a
l = l₁ ++ a :: l₂ l' = l₁ ++ l₂ :=
sorry
```
Correct:
```lean
example : Nat :=
functionWithAVeryLongNameSoThatSomeArgumentsWillNotFit firstArgument secondArgument
(firstArgumentWithAnEquallyLongNameAndThatFunctionDoesHaveMoreArguments firstArgument
secondArgument)
secondArgument
```
Correct:
```lean
theorem size_alter [LawfulBEq α] {k : α} {f : Option (β k) Option (β k)} (h : m.WF) :
(m.alter k f).size =
if m.contains k && (f (m.get? k)).isNone then
m.size - 1
else if !m.contains k && (f (m.get? k)).isSome then
m.size + 1
else
m.size := by
simp_to_raw using Raw₀.size_alter
```
Correct:
```lean
theorem get?_alter [LawfulBEq α] {k k' : α} {f : Option (β k) Option (β k)} (h : m.WF) :
(m.alter k f).get? k' =
if h : k == k' then
cast (congrArg (Option β) (eq_of_beq h)) (f (m.get? k))
else m.get? k' := by
simp_to_raw using Raw₀.get?_alter
```
Correct:
```lean
example : Nat × Nat :=
imagineThisWasALongTerm,
imagineThisWasAnotherLongTerm
```
Correct:
```lean
example : Nat × Nat :=
imagineThisWasALongTerm,
imagineThisWasAnotherLongTerm
```
Correct:
```lean
example : Vector Nat :=
#v[imagineThisWasALongTerm,
imagineThisWasAnotherLongTerm]
```
## Basic file structure
Every file should start with a copyright header, imports (in the standard library, this always includes a `prelude` declaration) and a module documentation string. There should not be a blank line between the copyright header and the imports. There should be a blank line between the imports and the module documentation string.
If you explicitly declare universe variables, do so at the top of the file, after the module documentation.
Correct:
```lean
/-
Copyright (c) 2014 Parikshit Khanna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro,
Yury Kudryashov
-/
prelude
import Init.Data.List.Pairwise
import Init.Data.List.Find
/-!
**# Lemmas about `List.eraseP` and `List.erase`.**
-/
universe u u'
```
Syntax that is not supposed to be user-facing must be scoped. New public syntax must always be discussed explicitly in an RFC.
## Top-level commands and declarations
All top-level commands are unindented. Sectioning commands like `section` and `namespace` do not increase the indentation level.
Attributes may be placed on the same line as the rest of the command or on a separate line.
Multi-line declaration headers are indented by four spaces starting from the second line. The colon that indicates the type of a declaration may not be placed at the start of a line or on its own line.
Declaration bodies are indented by two spaces. Short declaration bodies may be placed on the same line as the declaration type.
Correct:
```lean
theorem eraseP_eq_iff {p} {l : List α} :
l.eraseP p = l'
(( a l, ¬ p a) l = l')
a l₁ l₂, ( b l₁, ¬ p b) p a
l = l₁ ++ a :: l₂ l' = l₁ ++ l₂ :=
sorry
```
Correct:
```lean
@[simp] theorem eraseP_nil : [].eraseP p = [] := rfl
```
Correct:
```lean
@[simp]
theorem eraseP_nil : [].eraseP p = [] := rfl
```
### Documentation comments
Note to external contributors: this is a section where the Lean style and the mathlib style are different.
Declarations should be documented as required by the `docBlame` linter, which may be activated in a file using
`set_option linter.missingDocs true` (we allow these to stay in the file).
Single-line documentation comments should go on the same line as `/--`/`-/`, while multi-line documentation strings
should have these delimiters on their own line, with the documentation comment itself unindented.
Documentation comments must be written in the indicative mood. Use American orthography.
Correct:
```lean
/-- Carries out a monadic action on each mapping in the hash map in some order. -/
@[inline] def forM (f : (a : α) β a m PUnit) (b : Raw α β) : m PUnit :=
b.buckets.forM (AssocList.forM f)
```
Correct:
```lean
/--
Monadically computes a value by folding the given function over the mappings in the hash
map in some order.
-/
@[inline] def foldM (f : δ (a : α) β a m δ) (init : δ) (b : Raw α β) : m δ :=
b.buckets.foldlM (fun acc l => l.foldlM f acc) init
```
### Where clauses
The `where` keyword should be unindented, and all declarations bound by it should be indented with two spaces.
Blank lines before and after `where` and between declarations bound by `where` are optional and should be chosen
to maximize readability.
Correct:
```lean
@[simp] theorem partition_eq_filter_filter (p : α Bool) (l : List α) :
partition p l = (filter p l, filter (not p) l) := by
simp [partition, aux]
where
aux (l) {as bs} : partition.loop p l (as, bs) =
(as.reverse ++ filter p l, bs.reverse ++ filter (not p) l) :=
match l with
| [] => by simp [partition.loop, filter]
| a :: l => by cases pa : p a <;> simp [partition.loop, pa, aux, filter, append_assoc]
```
### Termination arguments
The `termination_by`, `decreasing_by`, `partial_fixpoint` keywords should be unindented. The associated terms should be indented like declaration bodies.
Correct:
```lean
@[inline] def multiShortOption (handle : Char m PUnit) (opt : String) : m PUnit := do
let rec loop (p : String.Pos) := do
if h : opt.atEnd p then
return
else
handle (opt.get' p h)
loop (opt.next' p h)
termination_by opt.utf8ByteSize - p.byteIdx
decreasing_by
simp [String.atEnd] at h
apply Nat.sub_lt_sub_left h
simp [String.lt_next opt p]
loop 1
```
Correct:
```lean
def substrEq (s1 : String) (off1 : String.Pos) (s2 : String) (off2 : String.Pos) (sz : Nat) : Bool :=
off1.byteIdx + sz s1.endPos.byteIdx && off2.byteIdx + sz s2.endPos.byteIdx && loop off1 off2 { byteIdx := off1.byteIdx + sz }
where
loop (off1 off2 stop1 : Pos) :=
if _h : off1.byteIdx < stop1.byteIdx then
let c₁ := s1.get off1
let c₂ := s2.get off2
c₁ == c₂ && loop (off1 + c₁) (off2 + c₂) stop1
else true
termination_by stop1.1 - off1.1
decreasing_by
have := Nat.sub_lt_sub_left _h (Nat.add_lt_add_left c₁.utf8Size_pos off1.1)
decreasing_tactic
```
Correct:
```lean
theorem div_add_mod (m n : Nat) : n * (m / n) + m % n = m := by
rw [div_eq, mod_eq]
have h : Decidable (0 < n n m) := inferInstance
cases h with
| isFalse h => simp [h]
| isTrue h =>
simp [h]
have ih := div_add_mod (m - n) n
rw [Nat.left_distrib, Nat.mul_one, Nat.add_assoc, Nat.add_left_comm, ih, Nat.add_comm, Nat.sub_add_cancel h.2]
decreasing_by apply div_rec_lemma; assumption
```
### Deriving
The `deriving` clause should be unindented.
Correct:
```lean
structure Iterator where
array : ByteArray
idx : Nat
deriving Inhabited
```
## Notation and Unicode
We generally prefer to use notation as available. We usually prefer the Unicode versions of notations over non-Unicode alternatives.
There are some rules and exceptions regarding specific notations which are listed below:
* Sigma types: use `(a : α) × β a` instead of `Σ a, β a` or `Sigma β`.
* Function arrows: use `fun a => f x` instead of `fun x ↦ f x` or `λ x => f x` or any other variant.
## Language constructs
### Pattern matching, induction etc.
Match arms are indented at the indentation level that the match statement would have if it was on its own line. If the match is implicit, then the arms should be indented as if the match was explicitly given. The content of match arms is indented two spaces, so that it appears on the same level as the match pattern.
Correct:
```lean
def alter [BEq α] {β : Type v} (a : α) (f : Option β Option β) :
AssocList α (fun _ => β) AssocList α (fun _ => β)
| nil => match f none with
| none => nil
| some b => AssocList.cons a b nil
| cons k v l =>
if k == a then
match f v with
| none => l
| some b => cons a b l
else
cons k v (alter a f l)
```
Correct:
```lean
theorem eq_append_cons_of_mem {a : α} {xs : List α} (h : a xs) :
as bs, xs = as ++ a :: bs a as := by
induction xs with
| nil => cases h
| cons x xs ih =>
simp at h
cases h with
| inl h => exact [], xs, by simp_all
| inr h =>
by_cases h' : a = x
· subst h'
exact [], xs, by simp
· obtain as, bs, rfl, h := ih h
exact x :: as, bs, rfl, by simp_all
```
Aligning match arms is allowed, but not required.
Correct:
```lean
def mkEqTrans? (h₁? h₂? : Option Expr) : MetaM (Option Expr) :=
match h₁?, h₂? with
| none, none => return none
| none, some h => return h
| some h, none => return h
| some h₁, some h₂ => mkEqTrans h₁ h₂
```
Correct:
```lean
def mkEqTrans? (h₁? h₂? : Option Expr) : MetaM (Option Expr) :=
match h₁?, h₂? with
| none, none => return none
| none, some h => return h
| some h, none => return h
| some h₁, some h₂ => mkEqTrans h₁ h₂
```
Correct:
```lean
def mkEqTrans? (h₁? h₂? : Option Expr) : MetaM (Option Expr) :=
match h₁?, h₂? with
| none, none => return none
| none, some h => return h
| some h, none => return h
| some h₁, some h₂ => mkEqTrans h₁ h₂
```
### Structures
Note to external contributors: this is a section where the Lean style and the mathlib style are different.
When using structure instance syntax over multiple lines, the opening brace should go on the preceding line, while the closing brace should go on its own line. The rest of the syntax should be indented by one level. During structure updates, the `with` clause goes on the same line as the opening brace. Aligning at the assignment symbol is allowed but not required.
Correct:
```lean
def addConstAsync (env : Environment) (constName : Name) (kind : ConstantKind) (reportExts := true) :
IO AddConstAsyncResult := do
let sigPromise IO.Promise.new
let infoPromise IO.Promise.new
let extensionsPromise IO.Promise.new
let checkedEnvPromise IO.Promise.new
let asyncConst := {
constInfo := {
name := constName
kind
sig := sigPromise.result
constInfo := infoPromise.result
}
exts? := guard reportExts *> some extensionsPromise.result
}
return {
constName, kind
mainEnv := { env with
asyncConsts := env.asyncConsts.add asyncConst
checked := checkedEnvPromise.result }
asyncEnv := { env with
asyncCtx? := some { declPrefix := privateToUserName constName.eraseMacroScopes }
}
sigPromise, infoPromise, extensionsPromise, checkedEnvPromise
}
```
Correct:
```lean
instance [Inhabited α] : Inhabited (Descr α β σ) where
default := {
name := default
mkInitial := default
ofOLeanEntry := default
toOLeanEntry := default
addEntry := fun s _ => s
}
```
### Declaring structures
When defining structure types, do not parenthesize structure fields.
When declaring a structure type with a custom constructor name, put the custom name on its own line, indented like the
structure fields, and add a documentation comment.
Correct:
```lean
/--
A bitvector of the specified width.
This is represented as the underlying `Nat` number in both the runtime
and the kernel, inheriting all the special support for `Nat`.
-/
structure BitVec (w : Nat) where
/--
Constructs a `BitVec w` from a number less than `2^w`.
O(1), because we use `Fin` as the internal representation of a bitvector.
-/
ofFin ::
/--
Interprets a bitvector as a number less than `2^w`.
O(1), because we use `Fin` as the internal representation of a bitvector.
-/
toFin : Fin (2 ^ w)
```
## Tactic proofs
Tactic proofs are the most common thing to break during any kind of upgrade, so it is important to write them in a way that minimizes the likelihood of proofs breaking and that makes it easy to debug breakages if they do occur.
If there are multiple goals, either use a tactic combinator (like `all_goals`) to operate on all of them or a clearly specified subset, or use focus dots to work on goals one at a time. Using structured proofs (e.g., `induction … with`) is encouraged but not mandatory.
Squeeze non-terminal `simp`s (i.e., calls to `simp` which do not close the goal). Squeezing terminal `simp`s is generally discouraged, although there are exceptions (for example if squeezing yields a noticeable performance improvement).
Do not over-golf proofs in ways that are likely to lead to hard-to-debug breakage. Examples of things to avoid include complex multi-goal manipulation using lots of tactic combinators, complex uses of the substitution operator (`▸`) and clever point-free expressions (possibly involving anonymous function notation for multiple arguments).
Do not under-golf proofs: for routine tasks, use the most powerful tactics available.
Do not use `erw`. Avoid using `rfl` after `simp` or `rw`, as this usually indicates a missing lemma that should be used instead of `rfl`.
Use `(d)simp` or `rw` instead of `delta` or `unfold`. Use `refine` instead of `refine`. Use `haveI` and `letI` only if they are actually required.
Prefer highly automated tactics (like `grind` and `omega`) over low-level proofs, unless the automated tactic requires unacceptable additional imports or has bad performance. If you decide against using a highly automated tactic, leave a comment explaining the decision.
## `do` notation
The `do` keyword goes on the same line as the corresponding `:=` (or `=>`, or similar). `Id.run do` should be treated as if it was a bare `do`.
Use early `return` statements to reduce nesting depth and make the non-exceptional control flow of a function easier to see.
Alternatives for `let` matches may be placed in the same line or in the next line, indented by two spaces. If the term that is
being matched on is itself more than one line and there is an alternative present, consider breaking immediately after `←` and indent
as far as necessary to ensure readability.
Correct:
```lean
def getFunDecl (fvarId : FVarId) : CompilerM FunDecl := do
let some decl findFunDecl? fvarId | throwError "unknown local function {fvarId.name}"
return decl
```
Correct:
```lean
def getFunDecl (fvarId : FVarId) : CompilerM FunDecl := do
let some decl
findFunDecl? fvarId
| throwError "unknown local function {fvarId.name}"
return decl
```
Correct:
```lean
def getFunDecl (fvarId : FVarId) : CompilerM FunDecl := do
let some decl findFunDecl?
fvarId
| throwError "unknown local function {fvarId.name}"
return decl
```
Correct:
```lean
def tagUntaggedGoals (parentTag : Name) (newSuffix : Name) (newGoals : List MVarId) : TacticM Unit := do
let mctx getMCtx
let mut numAnonymous := 0
for g in newGoals do
if mctx.isAnonymousMVar g then
numAnonymous := numAnonymous + 1
modifyMCtx fun mctx => Id.run do
let mut mctx := mctx
let mut idx := 1
for g in newGoals do
if mctx.isAnonymousMVar g then
if numAnonymous == 1 then
mctx := mctx.setMVarUserName g parentTag
else
mctx := mctx.setMVarUserName g (parentTag ++ newSuffix.appendIndexAfter idx)
idx := idx + 1
pure mctx
```

98
doc/std/vision.md Normal file
View File

@@ -0,0 +1,98 @@
# The Lean 4 standard library
Maintainer team (in alphabetical order): Henrik Böving, Markus Himmel
(community contact & external contribution coordinator), Kim Morrison, Paul
Reichert, Sofia Rodrigues.
The Lean 4 standard library is a core part of the Lean distribution, providing
essential building blocks for functional programming, verified software
development, and software verification. Unlike the standard libraries of most
other languages, many of its components are formally verified and can be used
as part of verified applications.
The standard library is a public API that contains the components listed in the
standard library outline below. Not all public APIs in the Lean distribution
are part of the standard library, and the standard library does not correspond
to a certain directory within the Lean source repository (like `Std`). For
example, the metaprogramming framework is not part of the standard library, but
basic types like `True` and `Nat` are.
The standard library is under active development. Our guiding principles are:
* Provide comprehensive, verified building blocks for real-world software.
* Build a public API of the highest quality with excellent internal consistency.
* Carefully optimize components that may be used in performance-critical software.
* Ensure smooth adoption and maintenance for users.
* Offer excellent documentation, example projects, and guides.
* Provide a reliable and extensible basis that libraries for software
development, software verification and mathematics can build on.
The standard library is principally developed by the Lean FRO. Community
contributions are welcome. If you would like to contribute, please refer to the
call for contributions below.
### Standard library outline
1. Core types and operations
1. Basic types
2. Numeric types, including floating point numbers
3. Containers
4. Strings and formatting
2. Language constructs
1. Ranges and iterators
2. Comparison, ordering, hashing and related type classes
3. Basic monad infrastructure
3. Libraries
1. Random numbers
2. Dates and times
4. Operating system abstractions
1. Concurrency and parallelism primitives
2. Asynchronous I/O
3. FFI helpers
4. Environment, file system, processes
5. Locales
The material covered in the first three sections (core types and operations,
language constructs and libraries) will be verified, with the exception of
floating point numbers and the parts of the libraries that interface with the
operating system (e.g., sources of operating system randomness or time zone
database access).
### Call for contributions
Thank you for taking interest in contributing to the Lean standard library\!
There are two main ways for community members to contribute to the Lean
standard library: by contributing experience reports or by contributing code
and lemmas.
**If you are using Lean for software verification or verified software
development:** hearing about your experiences using Lean and its standard
library for software verification is extremely valuable to us. We are committed
to building a standard library suitable for real-world applications and your
input will directly influence the continued evolution of the Lean standard
library. Please reach out to the standard library maintainer team via Zulip
(either in a public thread in the \#lean4 channel or via direct message). Even
just a link to your code helps. Thanks\!
**If you have code that you believe could enhance the Lean 4 standard
library:** we encourage you to initiate a discussion in the \#lean4 channel on
Zulip. This is the most effective way to receive preliminary feedback on your
contribution. The Lean standard library has a very precise scope and it has
very high quality standards, so at the moment we are mostly interested in
contributions that expand upon existing material rather than introducing novel
concepts.
**If you would like to contribute code to the standard library but dont know
what to work on:** we are always excited to meet motivated community members
who would like to contribute, and there is always impactful work that is
suitable for new contributors. Please reach out to Markus Himmel on Zulip to
discuss possible contributions.
As laid out in the [project-wide External Contribution
Guidelines](../../CONTRIBUTING.md),
PRs are much more likely to be merged if they are preceded by an RFC or if you
discussed your planned contribution with a member of the standard library
maintainer team. When in doubt, introducing yourself is always a good idea.
All code in the standard library is expected to strictly adhere to the
[standard library coding conventions](./style.md).

View File

@@ -689,7 +689,7 @@ add_custom_target(make_stdlib ALL
# The actual rule is in a separate makefile because we want to prefix it with '+' to use the Make job server
# for a parallelized nested build, but CMake doesn't let us do that.
# We use `lean` from the previous stage, but `leanc`, headers, etc. from the current stage
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init Std Lean
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init Std Lean Leanc
VERBATIM)
# if we have LLVM enabled, then build `lean.h.bc` which has the LLVM bitcode
@@ -768,7 +768,7 @@ if(${STAGE} GREATER 0 AND EXISTS ${LEAN_SOURCE_DIR}/Leanc.lean AND NOT ${CMAKE_S
add_custom_target(leanc ALL
WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/leanc
DEPENDS leanshared
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Leanc
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanc
VERBATIM)
endif()
@@ -823,7 +823,6 @@ endif()
# Escape for `make`. Yes, twice.
string(REPLACE "$" "\\\$$" CMAKE_EXE_LINKER_FLAGS_MAKE "${CMAKE_EXE_LINKER_FLAGS}")
string(REPLACE "$" "$$" CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE "${CMAKE_EXE_LINKER_FLAGS_MAKE}")
configure_file(${LEAN_SOURCE_DIR}/stdlib.make.in ${CMAKE_BINARY_DIR}/stdlib.make)
# hacky

View File

@@ -107,8 +107,8 @@ noncomputable def epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α
theorem epsilon_spec_aux {α : Sort u} (h : Nonempty α) (p : α Prop) : ( y, p y) p (@epsilon α h p) :=
(strongIndefiniteDescription p h).property
theorem epsilon_spec {α : Sort u} {p : α Prop} (hex : y, p y) : p (@epsilon α (nonempty_of_exists hex) p) :=
epsilon_spec_aux (nonempty_of_exists hex) p hex
theorem epsilon_spec {α : Sort u} {p : α Prop} (hex : y, p y) : p (@epsilon α hex.nonempty p) :=
epsilon_spec_aux hex.nonempty p hex
theorem epsilon_singleton {α : Sort u} (x : α) : @epsilon α x (fun y => y = x) = x :=
@epsilon_spec α (fun y => y = x) x, rfl

View File

@@ -1212,10 +1212,7 @@ abbrev noConfusionEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f :
instance : Inhabited Prop where
default := True
deriving instance Inhabited for NonScalar, PNonScalar, True, ForInStep
theorem nonempty_of_exists {α : Sort u} {p : α Prop} : Exists (fun x => p x) Nonempty α
| w, _ => w
deriving instance Inhabited for NonScalar, PNonScalar, True
/-! # Subsingleton -/
@@ -1389,16 +1386,7 @@ instance Sum.nonemptyLeft [h : Nonempty α] : Nonempty (Sum α β) :=
instance Sum.nonemptyRight [h : Nonempty β] : Nonempty (Sum α β) :=
Nonempty.elim h (fun b => Sum.inr b)
instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (Sum α β) := fun a b =>
match a, b with
| Sum.inl a, Sum.inl b =>
if h : a = b then isTrue (h rfl)
else isFalse fun h' => Sum.noConfusion h' fun h' => absurd h' h
| Sum.inr a, Sum.inr b =>
if h : a = b then isTrue (h rfl)
else isFalse fun h' => Sum.noConfusion h' fun h' => absurd h' h
| Sum.inr _, Sum.inl _ => isFalse fun h => Sum.noConfusion h
| Sum.inl _, Sum.inr _ => isFalse fun h => Sum.noConfusion h
deriving instance DecidableEq for Sum
end

View File

@@ -112,6 +112,10 @@ theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
rw [Array.mem_def, getElem_toList]
apply List.getElem_mem
@[simp] theorem emptyWithCapacity_eq {α n} : @emptyWithCapacity α n = #[] := rfl
@[simp] theorem mkEmpty_eq {α n} : @mkEmpty α n = #[] := rfl
end Array
namespace List
@@ -334,6 +338,8 @@ def ofFn {n} (f : Fin n → α) : Array α := go 0 (emptyWithCapacity n) where
if h : i < n then go (i+1) (acc.push (f i, h)) else acc
decreasing_by simp_wf; decreasing_trivial_pre_omega
-- See also `Array.ofFnM` defined in `Init.Data.Array.OfFn`.
/--
Constructs an array that contains all the numbers from `0` to `n`, exclusive.

View File

@@ -61,11 +61,6 @@ theorem toArray_eq : List.toArray as = xs ↔ as = xs.toList := by
@[grind] theorem size_empty : (#[] : Array α).size = 0 := rfl
@[simp] theorem emptyWithCapacity_eq {α n} : @emptyWithCapacity α n = #[] := rfl
@[deprecated emptyWithCapacity_eq (since := "2025-03-12")]
theorem mkEmpty_eq {α n} : @mkEmpty α n = #[] := rfl
/-! ### size -/
@[grind ] theorem eq_empty_of_size_eq_zero (h : xs.size = 0) : xs = #[] := by
@@ -247,6 +242,12 @@ theorem back?_pop {xs : Array α} :
/-! ### push -/
@[simp] theorem push_empty : #[].push x = #[x] := rfl
@[simp] theorem toList_push {xs : Array α} {x : α} : (xs.push x).toList = xs.toList ++ [x] := by
rcases xs with xs
simp
@[simp] theorem push_ne_empty {a : α} {xs : Array α} : xs.push a #[] := by
cases xs
simp
@@ -3266,6 +3267,22 @@ rather than `(arr.push a).size` as the argument.
(xs.push a).foldrM f init start = f a init >>= xs.foldrM f := by
simp [ foldrM_push, h]
@[simp, grind] theorem _root_.List.foldrM_push_eq_append [Monad m] [LawfulMonad m] {l : List α} {f : α m β} {xs : Array β} :
l.foldrM (fun x xs => xs.push <$> f x) xs = do return xs ++ ( l.reverse.mapM f).toArray := by
induction l with
| nil => simp
| cons a l ih =>
simp [ih]
congr 1
funext l'
congr 1
funext x
simp
@[simp, grind] theorem _root_.List.foldlM_push_eq_append [Monad m] [LawfulMonad m] {l : List α} {f : α m β} {xs : Array β} :
l.foldlM (fun xs x => xs.push <$> f x) xs = do return xs ++ ( l.mapM f).toArray := by
induction l generalizing xs <;> simp [*]
/-! ### foldl / foldr -/
@[grind] theorem foldl_empty {f : β α β} {init : β} : (#[].foldl f init) = init := rfl
@@ -3362,6 +3379,32 @@ rather than `(arr.push a).size` as the argument.
rcases as with as
simp
@[simp, grind] theorem _root_.List.foldr_push_eq_append {l : List α} {f : α β} {xs : Array β} :
l.foldr (fun x xs => xs.push (f x)) xs = xs ++ (l.reverse.map f).toArray := by
induction l <;> simp [*]
/-- Variant of `List.foldr_push_eq_append` specialized to `f = id`. -/
@[simp, grind] theorem _root_.List.foldr_push_eq_append' {l : List α} {xs : Array α} :
l.foldr (fun x xs => xs.push x) xs = xs ++ l.reverse.toArray := by
induction l <;> simp [*]
@[simp, grind] theorem _root_.List.foldl_push_eq_append {l : List α} {f : α β} {xs : Array β} :
l.foldl (fun xs x => xs.push (f x)) xs = xs ++ (l.map f).toArray := by
induction l generalizing xs <;> simp [*]
/-- Variant of `List.foldl_push_eq_append` specialized to `f = id`. -/
@[simp, grind] theorem _root_.List.foldl_push_eq_append' {l : List α} {xs : Array α} :
l.foldl (fun xs x => xs.push x) xs = xs ++ l.toArray := by
simpa using List.foldl_push_eq_append (f := id)
@[deprecated _root_.List.foldl_push_eq_append' (since := "2025-05-18")]
theorem _root_.List.foldl_push {l : List α} {as : Array α} : l.foldl Array.push as = as ++ l.toArray := by
induction l generalizing as <;> simp [*]
@[deprecated _root_.List.foldr_push_eq_append' (since := "2025-05-18")]
theorem _root_.List.foldr_push {l : List α} {as : Array α} : l.foldr (fun a bs => push bs a) as = as ++ l.reverse.toArray := by
rw [List.foldr_eq_foldl_reverse, List.foldl_push_eq_append']
@[simp, grind] theorem foldr_append_eq_append {xs : Array α} {f : α Array β} {ys : Array β} :
xs.foldr (f · ++ ·) ys = (xs.map f).flatten ++ ys := by
rcases xs with xs

View File

@@ -23,9 +23,9 @@ namespace Array
@[simp, grind =] theorem lt_toList [LT α] {xs ys : Array α} : xs.toList < ys.toList xs < ys := Iff.rfl
@[simp, grind =] theorem le_toList [LT α] {xs ys : Array α} : xs.toList ys.toList xs ys := Iff.rfl
protected theorem not_lt_iff_ge [LT α] {l₁ l₂ : List α} : ¬ l₁ < l₂ l₂ l₁ := Iff.rfl
protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} :
¬ l₁ l₂ l₂ < l₁ :=
protected theorem not_lt_iff_ge [LT α] {xs ys : Array α} : ¬ xs < ys ys xs := Iff.rfl
protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {xs ys : Array α} :
¬ xs ys ys < xs :=
Decidable.not_not
@[simp] theorem lex_empty [BEq α] {lt : α α Bool} {xs : Array α} : xs.lex #[] lt = false := by

View File

@@ -25,6 +25,11 @@ open Nat
/-! ## Monadic operations -/
@[simp] theorem map_toList_inj [Monad m] [LawfulMonad m]
{xs : m (Array α)} {ys : m (Array α)} :
toList <$> xs = toList <$> ys xs = ys :=
_root_.map_inj_right (by simp)
/-! ### mapM -/
@[simp] theorem mapM_pure [Monad m] [LawfulMonad m] {xs : Array α} {f : α β} :
@@ -34,6 +39,11 @@ open Nat
@[simp] theorem mapM_id {xs : Array α} {f : α Id β} : xs.mapM f = xs.map f :=
mapM_pure
@[simp] theorem mapM_map [Monad m] [LawfulMonad m] {f : α β} {g : β m γ} {xs : Array α} :
(xs.map f).mapM g = xs.mapM (g f) := by
rcases xs with xs
simp
@[simp] theorem mapM_append [Monad m] [LawfulMonad m] {f : α m β} {xs ys : Array α} :
(xs ++ ys).mapM f = (return ( xs.mapM f) ++ ( ys.mapM f)) := by
rcases xs with xs

View File

@@ -8,7 +8,9 @@ module
prelude
import all Init.Data.Array.Basic
import Init.Data.Array.Lemmas
import Init.Data.Array.Monadic
import Init.Data.List.OfFn
import Init.Data.List.FinRange
/-!
# Theorems about `Array.ofFn`
@@ -19,6 +21,8 @@ set_option linter.indexVariables true -- Enforce naming conventions for index va
namespace Array
/-! ### ofFn -/
@[simp] theorem ofFn_zero {f : Fin 0 α} : ofFn f = #[] := by
simp [ofFn, ofFn.go]
@@ -26,12 +30,17 @@ theorem ofFn_succ {f : Fin (n+1) → α} :
ofFn f = (ofFn (fun (i : Fin n) => f i.castSucc)).push (f n, by omega) := by
ext i h₁ h₂
· simp
· simp [getElem_push]
split <;> rename_i h₃
· rfl
· congr
simp at h₁ h₂
omega
· simp only [getElem_ofFn, getElem_push, size_ofFn, Fin.castSucc_mk, left_eq_dite_iff,
Nat.not_lt]
simp only [size_ofFn] at h₁
intro h₃
simp only [show i = n by omega]
theorem ofFn_add {n m} {f : Fin (n + m) α} :
ofFn f = (ofFn (fun i => f (i.castLE (Nat.le_add_right n m)))) ++ (ofFn (fun i => f (i.natAdd n))) := by
induction m with
| zero => simp
| succ m ih => simp [ofFn_succ, ih]
@[simp] theorem _root_.List.toArray_ofFn {f : Fin n α} : (List.ofFn f).toArray = Array.ofFn f := by
ext <;> simp
@@ -39,6 +48,11 @@ theorem ofFn_succ {f : Fin (n+1) → α} :
@[simp] theorem toList_ofFn {f : Fin n α} : (Array.ofFn f).toList = List.ofFn f := by
apply List.ext_getElem <;> simp
theorem ofFn_succ' {f : Fin (n+1) α} :
ofFn f = #[f 0] ++ ofFn (fun i => f i.succ) := by
apply Array.toList_inj.mp
simp [List.ofFn_succ]
@[simp]
theorem ofFn_eq_empty_iff {f : Fin n α} : ofFn f = #[] n = 0 := by
rw [ Array.toList_inj]
@@ -53,4 +67,71 @@ theorem mem_ofFn {n} {f : Fin n → α} {a : α} : a ∈ ofFn f ↔ ∃ i, f i =
· rintro i, rfl
apply mem_of_getElem (i := i) <;> simp
/-! ### ofFnM -/
/-- Construct (in a monadic context) an array by applying a monadic function to each index. -/
def ofFnM {n} [Monad m] (f : Fin n m α) : m (Array α) :=
Fin.foldlM n (fun xs i => xs.push <$> f i) (Array.emptyWithCapacity n)
@[simp]
theorem ofFnM_zero [Monad m] {f : Fin 0 m α} : ofFnM f = pure #[] := by
simp [ofFnM]
theorem ofFnM_succ' {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) m α} :
ofFnM f = (do
let a f 0
let as ofFnM fun i => f i.succ
pure (#[a] ++ as)) := by
simp [ofFnM, Fin.foldlM_eq_finRange_foldlM, List.foldlM_push_eq_append, List.finRange_succ, Function.comp_def]
theorem ofFnM_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) m α} :
ofFnM f = (do
let as ofFnM fun i => f i.castSucc
let a f (Fin.last n)
pure (as.push a)) := by
simp [ofFnM, Fin.foldlM_succ_last]
theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) m α} :
ofFnM f = (do
let as ofFnM fun i : Fin n => f (i.castLE (Nat.le_add_right n k))
let bs ofFnM fun i : Fin k => f (i.natAdd n)
pure (as ++ bs)) := by
induction k with
| zero => simp
| succ k ih =>
simp only [ofFnM_succ, Nat.add_eq, ih, Fin.castSucc_castLE, Fin.castSucc_natAdd, bind_pure_comp,
bind_assoc, bind_map_left, Fin.natAdd_last, map_bind, Functor.map_map]
congr 1
funext xs
congr 1
funext ys
congr 1
funext x
simp
@[simp] theorem toList_ofFnM [Monad m] [LawfulMonad m] {f : Fin n m α} :
toList <$> ofFnM f = List.ofFnM f := by
induction n with
| zero => simp
| succ n ih => simp [ofFnM_succ, List.ofFnM_succ_last, ih]
@[simp]
theorem ofFnM_pure_comp [Monad m] [LawfulMonad m] {n} {f : Fin n α} :
ofFnM (pure f) = (pure (ofFn f) : m (Array α)) := by
apply Array.map_toList_inj.mp
simp
-- Variant of `ofFnM_pure_comp` using a lambda.
-- This is not marked a `@[simp]` as it would match on every occurrence of `ofFnM`.
theorem ofFnM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n α} :
ofFnM (fun i => pure (f i)) = (pure (ofFn f) : m (Array α)) :=
ofFnM_pure_comp
@[simp, grind =] theorem idRun_ofFnM {f : Fin n Id α} :
Id.run (ofFnM f) = ofFn (fun i => Id.run (f i)) := by
unfold Id.run
induction n with
| zero => simp
| succ n ih => simp [ofFnM_succ', ofFn_succ', ih]
end Array

View File

@@ -2261,7 +2261,7 @@ theorem msb_sshiftRight {n : Nat} {x : BitVec w} :
theorem sshiftRight_add {x : BitVec w} {m n : Nat} :
x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n := by
ext i
simp [getElem_sshiftRight, getLsbD_sshiftRight, Nat.add_assoc]
simp only [getElem_sshiftRight, Nat.add_assoc, msb_sshiftRight, dite_eq_ite]
by_cases h₂ : n + i < w
· simp [h₂]
· simp only [h₂, reduceIte]

View File

@@ -100,6 +100,11 @@ Fin.foldrM n f xₙ = do
/-! ### foldlM -/
@[congr] theorem foldlM_congr [Monad m] {n k : Nat} (w : n = k) (f : α Fin n m α) :
foldlM n f = foldlM k (fun x i => f x (i.cast w.symm)) := by
subst w
rfl
theorem foldlM_loop_lt [Monad m] (f : α Fin n m α) (x) (h : i < n) :
foldlM.loop n f x i = f x i, h >>= (foldlM.loop n f . (i+1)) := by
rw [foldlM.loop, dif_pos h]
@@ -120,14 +125,49 @@ theorem foldlM_loop [Monad m] (f : α → Fin (n+1) → m α) (x) (h : i < n+1)
rw [foldlM_loop_eq, foldlM_loop_eq]
termination_by n - i
@[simp] theorem foldlM_zero [Monad m] (f : α Fin 0 m α) (x) : foldlM 0 f x = pure x :=
foldlM_loop_eq ..
@[simp] theorem foldlM_zero [Monad m] (f : α Fin 0 m α) : foldlM 0 f = pure := by
funext x
exact foldlM_loop_eq ..
theorem foldlM_succ [Monad m] (f : α Fin (n+1) m α) (x) :
foldlM (n+1) f x = f x 0 >>= foldlM n (fun x j => f x j.succ) := foldlM_loop ..
theorem foldlM_succ [Monad m] (f : α Fin (n+1) m α) :
foldlM (n+1) f = fun x => f x 0 >>= foldlM n (fun x j => f x j.succ) := by
funext x
exact foldlM_loop ..
/-- Variant of `foldlM_succ` that splits off `Fin.last n` rather than `0`. -/
theorem foldlM_succ_last [Monad m] [LawfulMonad m] (f : α Fin (n+1) m α) :
foldlM (n+1) f = fun x => foldlM n (fun x j => f x j.castSucc) x >>= (f · (Fin.last n)) := by
funext x
induction n generalizing x with
| zero =>
simp [foldlM_succ]
| succ n ih =>
rw [foldlM_succ]
conv => rhs; rw [foldlM_succ]
simp only [castSucc_zero, castSucc_succ, bind_assoc]
congr 1
funext x
rw [ih]
simp
theorem foldlM_add [Monad m] [LawfulMonad m] (f : α Fin (n + k) m α) :
foldlM (n + k) f =
fun x => foldlM n (fun x i => f x (i.castLE (Nat.le_add_right n k))) x >>= foldlM k (fun x i => f x (i.natAdd n)) := by
induction k with
| zero =>
funext x
simp
| succ k ih =>
funext x
simp [foldlM_succ_last, Nat.add_assoc, ih]
/-! ### foldrM -/
@[congr] theorem foldrM_congr [Monad m] {n k : Nat} (w : n = k) (f : Fin n α m α) :
foldrM n f = foldrM k (fun i => f (i.cast w.symm)) := by
subst w
rfl
theorem foldrM_loop_zero [Monad m] (f : Fin n α m α) (x) :
foldrM.loop n f 0, Nat.zero_le _ x = pure x := by
rw [foldrM.loop]
@@ -145,19 +185,47 @@ theorem foldrM_loop [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x
conv => rhs; rw [bind_pure (f 0 x)]
congr
funext
try simp only [foldrM.loop] -- the try makes this proof work with and without opaque wf rec
simp [foldrM_loop_zero]
| succ i ih =>
rw [foldrM_loop_succ, foldrM_loop_succ, bind_assoc]
congr; funext; exact ih ..
@[simp] theorem foldrM_zero [Monad m] (f : Fin 0 α m α) (x) : foldrM 0 f x = pure x :=
foldrM_loop_zero ..
@[simp] theorem foldrM_zero [Monad m] (f : Fin 0 α m α) : foldrM 0 f = pure := by
funext x
exact foldrM_loop_zero ..
theorem foldrM_succ [Monad m] [LawfulMonad m] (f : Fin (n+1) α m α) (x) :
foldrM (n+1) f x = foldrM n (fun i => f i.succ) x >>= f 0 := foldrM_loop ..
theorem foldrM_succ [Monad m] [LawfulMonad m] (f : Fin (n+1) α m α) :
foldrM (n+1) f = fun x => foldrM n (fun i => f i.succ) x >>= f 0 := by
funext x
exact foldrM_loop ..
theorem foldrM_succ_last [Monad m] [LawfulMonad m] (f : Fin (n+1) α m α) :
foldrM (n+1) f = fun x => f (Fin.last n) x >>= foldrM n (fun i => f i.castSucc) := by
funext x
induction n generalizing x with
| zero => simp [foldrM_succ]
| succ n ih =>
rw [foldrM_succ]
conv => rhs; rw [foldrM_succ]
simp [ih]
theorem foldrM_add [Monad m] [LawfulMonad m] (f : Fin (n + k) α m α) :
foldrM (n + k) f =
fun x => foldrM k (fun i => f (i.natAdd n)) x >>= foldrM n (fun i => f (i.castLE (Nat.le_add_right n k))) := by
induction k with
| zero =>
simp
| succ k ih =>
funext x
simp [foldrM_succ_last, Nat.add_assoc, ih]
/-! ### foldl -/
@[congr] theorem foldl_congr {n k : Nat} (w : n = k) (f : α Fin n α) :
foldl n f = foldl k (fun x i => f x (i.cast w.symm)) := by
subst w
rfl
theorem foldl_loop_lt (f : α Fin n α) (x) (h : i < n) :
foldl.loop n f x i = foldl.loop n f (f x i, h) (i+1) := by
rw [foldl.loop, dif_pos h]
@@ -187,14 +255,34 @@ theorem foldl_succ_last (f : α → Fin (n+1) → α) (x) :
rw [foldl_succ]
induction n generalizing x with
| zero => simp [foldl_succ, Fin.last]
| succ n ih => rw [foldl_succ, ih (f · ·.succ), foldl_succ]; simp [succ_castSucc]
| succ n ih => rw [foldl_succ, ih (f · ·.succ), foldl_succ]; simp
theorem foldl_add (f : α Fin (n + m) α) (x) :
foldl (n + m) f x =
foldl m (fun x i => f x (i.natAdd n))
(foldl n (fun x i => f x (i.castLE (Nat.le_add_right n m))) x):= by
induction m with
| zero => simp
| succ m ih => simp [foldl_succ_last, ih, Nat.add_assoc]
theorem foldl_eq_foldlM (f : α Fin n α) (x) :
foldl n f x = foldlM (m:=Id) n f x := by
induction n generalizing x <;> simp [foldl_succ, foldlM_succ, *]
-- This is not marked `@[simp]` as it would match on every occurrence of `foldlM`.
theorem foldlM_pure [Monad m] [LawfulMonad m] {n} {f : α Fin n α} :
foldlM n (fun x i => pure (f x i)) x = (pure (foldl n f x) : m α) := by
induction n generalizing x with
| zero => simp
| succ n ih => simp [foldlM_succ, foldl_succ, ih]
/-! ### foldr -/
@[congr] theorem foldr_congr {n k : Nat} (w : n = k) (f : Fin n α α) :
foldr n f = foldr k (fun i => f (i.cast w.symm)) := by
subst w
rfl
theorem foldr_loop_zero (f : Fin n α α) (x) :
foldr.loop n f 0 (Nat.zero_le _) x = x := by
rw [foldr.loop]
@@ -220,7 +308,15 @@ theorem foldr_succ_last (f : Fin (n+1) → αα) (x) :
foldr (n+1) f x = foldr n (f ·.castSucc) (f (last n) x) := by
induction n generalizing x with
| zero => simp [foldr_succ, Fin.last]
| succ n ih => rw [foldr_succ, ih (f ·.succ), foldr_succ]; simp [succ_castSucc]
| succ n ih => rw [foldr_succ, ih (f ·.succ), foldr_succ]; simp
theorem foldr_add (f : Fin (n + m) α α) (x) :
foldr (n + m) f x =
foldr n (fun i => f (i.castLE (Nat.le_add_right n m)))
(foldr m (fun i => f (i.natAdd n)) x) := by
induction m generalizing x with
| zero => simp
| succ m ih => simp [foldr_succ_last, ih, Nat.add_assoc]
theorem foldr_eq_foldrM (f : Fin n α α) (x) :
foldr n f x = foldrM (m:=Id) n f x := by
@@ -238,4 +334,11 @@ theorem foldr_rev (f : α → Fin n → α) (x) :
| zero => simp
| succ n ih => rw [foldl_succ_last, foldr_succ, ih]; simp [rev_succ]
-- This is not marked `@[simp]` as it would match on every occurrence of `foldrM`.
theorem foldrM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n α α} :
foldrM n (fun i x => pure (f i x)) x = (pure (foldr n f x) : m α) := by
induction n generalizing x with
| zero => simp
| succ n ih => simp [foldrM_succ, foldr_succ, ih]
end Fin

View File

@@ -646,6 +646,20 @@ theorem rev_castSucc (k : Fin n) : rev (castSucc k) = succ (rev k) := k.rev_cast
theorem rev_succ (k : Fin n) : rev (succ k) = castSucc (rev k) := k.rev_addNat 1
@[simp, grind _=_]
theorem castSucc_succ (i : Fin n) : i.succ.castSucc = i.castSucc.succ := rfl
@[simp, grind =]
theorem castLE_refl (h : n n) (i : Fin n) : i.castLE h = i := rfl
@[simp, grind =]
theorem castSucc_castLE (h : n m) (i : Fin n) :
(i.castLE h).castSucc = i.castLE (by omega) := rfl
@[simp, grind =]
theorem castSucc_natAdd (n : Nat) (i : Fin k) :
(i.natAdd n).castSucc = (i.castSucc).natAdd n := rfl
/-! ### pred -/
@[simp] theorem coe_pred (j : Fin (n + 1)) (h : j 0) : (j.pred h : Nat) = j - 1 := rfl

View File

@@ -161,8 +161,7 @@ This function does not reduce in the kernel. It is compiled to the C inequality
match a, b with
| a, b => floatSpec.decLe a b
instance floatDecLt (a b : Float) : Decidable (a < b) := Float.decLt a b
instance floatDecLe (a b : Float) : Decidable (a b) := Float.decLe a b
attribute [instance] Float.decLt Float.decLe
/--
Converts a floating-point number to a string.

View File

@@ -145,7 +145,7 @@ Compares two floating point numbers for strict inequality.
This function does not reduce in the kernel. It is compiled to the C inequality operator.
-/
@[extern "lean_float32_decLt"] opaque Float32.decLt (a b : Float32) : Decidable (a < b) :=
@[extern "lean_float32_decLt", instance] opaque Float32.decLt (a b : Float32) : Decidable (a < b) :=
match a, b with
| a, b => float32Spec.decLt a b
@@ -154,13 +154,10 @@ Compares two floating point numbers for non-strict inequality.
This function does not reduce in the kernel. It is compiled to the C inequality operator.
-/
@[extern "lean_float32_decLe"] opaque Float32.decLe (a b : Float32) : Decidable (a b) :=
@[extern "lean_float32_decLe", instance] opaque Float32.decLe (a b : Float32) : Decidable (a b) :=
match a, b with
| a, b => float32Spec.decLe a b
instance float32DecLt (a b : Float32) : Decidable (a < b) := Float32.decLt a b
instance float32DecLe (a b : Float32) : Decidable (a b) := Float32.decLe a b
/--
Converts a floating-point number to a string.

View File

@@ -57,9 +57,6 @@ instance : Hashable UInt64 where
instance : Hashable USize where
hash n := n.toUInt64
instance : Hashable ByteArray where
hash as := as.foldl (fun r a => mixHash r (hash a)) 7
instance : Hashable (Fin n) where
hash v := v.val.toUInt64

View File

@@ -121,7 +121,7 @@ theorem toNat_lt_toNat {n m : Int} (hn : 0 < m) : n.toNat < m.toNat ↔ n < m :=
/-! ### min and max -/
@[simp] protected theorem min_assoc : (a b c : Int), min (min a b) c = min a (min b c) := by omega
instance : Std.Associative (α := Nat) min := Nat.min_assoc
instance : Std.Associative (α := Int) min := Int.min_assoc
@[simp] protected theorem min_self_assoc {m n : Int} : min m (min m n) = min m n := by
rw [ Int.min_assoc, Int.min_self]
@@ -130,7 +130,7 @@ instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩
rw [Int.min_comm m n, Int.min_assoc, Int.min_self]
@[simp] protected theorem max_assoc (a b c : Int) : max (max a b) c = max a (max b c) := by omega
instance : Std.Associative (α := Nat) max := Nat.max_assoc
instance : Std.Associative (α := Int) max := Int.max_assoc
@[simp] protected theorem max_self_assoc {m n : Int} : max m (max m n) = max m n := by
rw [ Int.max_assoc, Int.max_self]

View File

@@ -6,7 +6,8 @@ Authors: François G. Dorais
module
prelude
import Init.Data.List.OfFn
import all Init.Data.List.OfFn
import Init.Data.List.Monadic
set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
set_option linter.indexVariables true -- Enforce naming conventions for index variables.
@@ -57,3 +58,50 @@ theorem finRange_reverse {n} : (finRange n).reverse = (finRange n).map Fin.rev :
simp [Fin.rev_succ]
end List
namespace Fin
theorem foldlM_eq_finRange_foldlM [Monad m] (f : α Fin n m α) (x : α) :
foldlM n f x = (List.finRange n).foldlM f x := by
induction n generalizing x with
| zero => simp
| succ n ih =>
simp [foldlM_succ, List.finRange_succ, List.foldlM_cons]
congr 1
funext y
simp [ih, List.foldlM_map]
theorem foldrM_eq_finRange_foldrM [Monad m] [LawfulMonad m] (f : Fin n α m α) (x : α) :
foldrM n f x = (List.finRange n).foldrM f x := by
induction n generalizing x with
| zero => simp
| succ n ih =>
simp [foldrM_succ, List.finRange_succ, ih, List.foldrM_map]
theorem foldl_eq_finRange_foldl (f : α Fin n α) (x : α) :
foldl n f x = (List.finRange n).foldl f x := by
induction n generalizing x with
| zero => simp
| succ n ih =>
simp [foldl_succ, List.finRange_succ, ih, List.foldl_map]
theorem foldr_eq_finRange_foldr (f : Fin n α α) (x : α) :
foldr n f x = (List.finRange n).foldr f x := by
induction n generalizing x with
| zero => simp
| succ n ih =>
simp [foldr_succ, List.finRange_succ, ih, List.foldr_map]
end Fin
namespace List
theorem ofFnM_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) m α} :
ofFnM f = (do
let a f 0
let as ofFnM fun i => f i.succ
pure (a :: as)) := by
simp [ofFnM, Fin.foldlM_eq_finRange_foldlM, List.finRange_succ, List.foldlM_cons_eq_append,
List.foldlM_map]
end List

View File

@@ -2576,6 +2576,11 @@ theorem foldr_eq_foldrM {f : α → β → β} {b : β} {l : List α} :
l.foldl (fun xs y => f y :: xs) l' = (l.map f).reverse ++ l' := by
induction l generalizing l' <;> simp [*]
/-- Variant of `foldl_flip_cons_eq_append` specalized to `f = id`. -/
@[simp, grind] theorem foldl_flip_cons_eq_append' {l l' : List α} :
l.foldl (fun xs y => y :: xs) l' = l.reverse ++ l' := by
induction l generalizing l' <;> simp [*]
@[simp, grind] theorem foldr_append_eq_append {l : List α} {f : α List β} {l' : List β} :
l.foldr (f · ++ ·) l' = (l.map f).flatten ++ l' := by
induction l <;> simp [*]

View File

@@ -8,6 +8,8 @@ module
prelude
import Init.Data.List.TakeDrop
import Init.Data.List.Attach
import Init.Data.List.OfFn
import Init.Data.Array.Bootstrap
import all Init.Data.List.Control
/-!
@@ -69,13 +71,17 @@ theorem mapM'_eq_mapM [Monad m] [LawfulMonad m] {f : α → m β} {l : List α}
@[simp] theorem mapM_id {l : List α} {f : α Id β} : l.mapM f = l.map f :=
mapM_pure
@[simp] theorem mapM_map [Monad m] [LawfulMonad m] {f : α β} {g : β m γ} {l : List α} :
(l.map f).mapM g = l.mapM (g f) := by
induction l <;> simp_all
@[simp] theorem mapM_append [Monad m] [LawfulMonad m] {f : α m β} {l₁ l₂ : List α} :
(l₁ ++ l₂).mapM f = (return ( l₁.mapM f) ++ ( l₂.mapM f)) := by induction l₁ <;> simp [*]
/-- Auxiliary lemma for `mapM_eq_reverse_foldlM_cons`. -/
theorem foldlM_cons_eq_append [Monad m] [LawfulMonad m] {f : α m β} {as : List α} {b : β} {bs : List β} :
(as.foldlM (init := b :: bs) fun acc a => return (( f a) :: acc)) =
(· ++ b :: bs) <$> as.foldlM (init := []) fun acc a => return (( f a) :: acc) := by
(as.foldlM (init := b :: bs) fun acc a => (· :: acc) <$> f a) =
(· ++ b :: bs) <$> as.foldlM (init := []) fun acc a => (· :: acc) <$> f a := by
induction as generalizing b bs with
| nil => simp
| cons a as ih =>
@@ -83,7 +89,7 @@ theorem foldlM_cons_eq_append [Monad m] [LawfulMonad m] {f : α → m β} {as :
simp [ih, _root_.map_bind, Functor.map_map, Function.comp_def]
theorem mapM_eq_reverse_foldlM_cons [Monad m] [LawfulMonad m] {f : α m β} {l : List α} :
mapM f l = reverse <$> (l.foldlM (fun acc a => return (( f a) :: acc)) []) := by
mapM f l = reverse <$> (l.foldlM (fun acc a => (· :: acc) <$> f a) []) := by
rw [ mapM'_eq_mapM]
induction l with
| nil => simp

View File

@@ -27,6 +27,13 @@ Examples:
-/
def ofFn {n} (f : Fin n α) : List α := Fin.foldr n (f · :: ·) []
/--
Creates a list wrapped in a monad by applying the monadic function `f : Fin n → m α`
to each potential index in order, starting at `0`.
-/
def ofFnM {n} [Monad m] (f : Fin n m α) : m (List α) :=
List.reverse <$> Fin.foldlM n (fun xs i => (· :: xs) <$> f i) []
@[simp]
theorem length_ofFn {f : Fin n α} : (ofFn f).length = n := by
simp only [ofFn]
@@ -49,7 +56,8 @@ protected theorem getElem_ofFn {f : Fin n → α} (h : i < (ofFn f).length) :
simp_all
@[simp]
protected theorem getElem?_ofFn {f : Fin n α} : (ofFn f)[i]? = if h : i < n then some (f i, h) else none :=
protected theorem getElem?_ofFn {f : Fin n α} :
(ofFn f)[i]? = if h : i < n then some (f i, h) else none :=
if h : i < (ofFn f).length
then by
rw [getElem?_eq_getElem h, List.getElem_ofFn]
@@ -60,16 +68,31 @@ protected theorem getElem?_ofFn {f : Fin n → α} : (ofFn f)[i]? = if h : i < n
/-- `ofFn` on an empty domain is the empty list. -/
@[simp]
theorem ofFn_zero {f : Fin 0 α} : ofFn f = [] :=
ext_get (by simp) (fun i hi₁ hi₂ => by contradiction)
theorem ofFn_zero {f : Fin 0 α} : ofFn f = [] := by
rw [ofFn, Fin.foldr_zero]
@[simp]
theorem ofFn_succ {n} {f : Fin (n + 1) α} : ofFn f = f 0 :: ofFn fun i => f i.succ :=
ext_get (by simp) (fun i hi₁ hi₂ => by
cases i
· simp
· simp)
theorem ofFn_succ_last {n} {f : Fin (n + 1) α} :
ofFn f = (ofFn fun i => f i.castSucc) ++ [f (Fin.last n)] := by
induction n with
| zero => simp [ofFn_succ]
| succ n ih =>
rw [ofFn_succ]
conv => rhs; rw [ofFn_succ]
rw [ih]
simp
theorem ofFn_add {n m} {f : Fin (n + m) α} :
ofFn f = (ofFn fun i => f (i.castLE (Nat.le_add_right n m))) ++ (ofFn fun i => f (i.natAdd n)) := by
induction m with
| zero => simp
| succ m ih => simp [ofFn_succ_last, ih]
@[simp]
theorem ofFn_eq_nil_iff {f : Fin n α} : ofFn f = [] n = 0 := by
cases n <;> simp only [ofFn_zero, ofFn_succ, eq_self_iff_true, Nat.succ_ne_zero, reduceCtorEq]
@@ -92,4 +115,66 @@ theorem getLast_ofFn {n} {f : Fin n → α} (h : ofFn f ≠ []) :
(ofFn f).getLast h = f n - 1, Nat.sub_one_lt (mt ofFn_eq_nil_iff.2 h) := by
simp [getLast_eq_getElem, length_ofFn, List.getElem_ofFn]
/-- `ofFnM` on an empty domain is the empty list. -/
@[simp]
theorem ofFnM_zero [Monad m] [LawfulMonad m] {f : Fin 0 m α} : ofFnM f = pure [] := by
simp [ofFnM]
/-! See `Init.Data.List.FinRange` for the `ofFnM_succ` variant. -/
theorem ofFnM_succ_last {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) m α} :
ofFnM f = (do
let as ofFnM fun i => f i.castSucc
let a f (Fin.last n)
pure (as ++ [a])) := by
simp [ofFnM, Fin.foldlM_succ_last]
theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) m α} :
ofFnM f = (do
let as ofFnM fun i : Fin n => f (i.castLE (Nat.le_add_right n k))
let bs ofFnM fun i : Fin k => f (i.natAdd n)
pure (as ++ bs)) := by
induction k with
| zero => simp
| succ k ih => simp [ofFnM_succ_last, ih]
end List
namespace Fin
theorem foldl_cons_eq_append {f : Fin n α} {xs : List α} :
Fin.foldl n (fun xs i => f i :: xs) xs = (List.ofFn f).reverse ++ xs := by
induction n generalizing xs with
| zero => simp
| succ n ih => simp [Fin.foldl_succ, List.ofFn_succ, ih]
theorem foldr_cons_eq_append {f : Fin n α} {xs : List α} :
Fin.foldr n (fun i xs => f i :: xs) xs = List.ofFn f ++ xs:= by
induction n generalizing xs with
| zero => simp
| succ n ih => simp [Fin.foldr_succ, List.ofFn_succ, ih]
end Fin
namespace List
@[simp]
theorem ofFnM_pure_comp [Monad m] [LawfulMonad m] {n} {f : Fin n α} :
ofFnM (pure f) = (pure (ofFn f) : m (List α)) := by
simp [ofFnM, Fin.foldlM_pure, Fin.foldl_cons_eq_append]
-- Variant of `ofFnM_pure_comp` using a lambda.
-- This is not marked a `@[simp]` as it would match on every occurrence of `ofFnM`.
theorem ofFnM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n α} :
ofFnM (fun i => pure (f i)) = (pure (ofFn f) : m (List α)) :=
ofFnM_pure_comp
@[simp, grind =] theorem idRun_ofFnM {f : Fin n Id α} :
Id.run (ofFnM f) = ofFn (fun i => Id.run (f i)) := by
unfold Id.run
induction n with
| zero => simp
| succ n ih => simp [ofFnM_succ_last, ofFn_succ_last, ih]
end List

View File

@@ -210,12 +210,6 @@ theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) :
cases as
simp
@[simp] theorem foldl_push {l : List α} {as : Array α} : l.foldl Array.push as = as ++ l.toArray := by
induction l generalizing as <;> simp [*]
@[simp] theorem foldr_push {l : List α} {as : Array α} : l.foldr (fun a bs => push bs a) as = as ++ l.reverse.toArray := by
rw [foldr_eq_foldl_reverse, foldl_push]
@[simp, grind =] theorem findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α m (Option β)) (l : List α) :
l.toArray.findSomeM? f = l.findSomeM? f := by
rw [Array.findSomeM?]

View File

@@ -197,6 +197,64 @@ theorem allTR_loop_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < n → Bo
omega
go n 0 f
/-! # `dfold` -/
private def dfoldCast {n : Nat} (α : (i : Nat) (h : i n := by omega) Type u)
{i j : Nat} {hi : i n} (w : i = j) (x : α i hi) : α j (by omega) := by
subst w
exact x
@[local simp] private theorem dfoldCast_rfl (h : i n) (w : i = i) (x : α i h) : dfoldCast α w x = x := by
simp [dfoldCast]
@[local simp] private theorem dfoldCast_trans (h : i n) (w₁ : i = j) (w₂ : j = k) (x : α i h) :
dfoldCast @α w₂ (dfoldCast @α w₁ x) = dfoldCast @α (w₁.trans w₂) x := by
cases w₁
cases w₂
simp [dfoldCast]
@[local simp] private theorem dfoldCast_eq_dfoldCast_iff {α : (i : Nat) (h : i n := by omega) Type u} {w₁ w₂ : i = j} {h : i n} {x : α i h} :
dfoldCast @α w₁ x = dfoldCast (n := n) (fun i h => α i) (hi := hi) w₂ x w₁ = w₂ := by
cases w₁
cases w₂
simp [dfoldCast]
private theorem apply_dfoldCast {α : (i : Nat) (h : i n := by omega) Type u}
(f : (i : Nat) (h : i < n) α i α (i + 1)) {i j : Nat} (h : i < n) {w : i = j} {x : α i (by omega)} :
f j (by omega) (dfoldCast @α w x) = dfoldCast (n := n) (fun i h => α i) (hi := by omega) (by omega) (f i h x) := by
subst w
simp
/--
`Nat.dfold` evaluates `f` on the numbers up to `n` exclusive, in increasing order:
* `Nat.dfold f 3 init = init |> f 0 |> f 1 |> f 2`
The input and output types of `f` are indexed by the current index, i.e. `f : (i : Nat) → (h : i < n) → α i → α (i + 1)`.
-/
@[specialize]
def dfold (n : Nat) {α : (i : Nat) (h : i n := by omega) Type u}
(f : (i : Nat) (h : i < n) α i α (i + 1)) (init : α 0) : α n :=
let rec @[specialize] loop : j, j n α (n - j) α n
| 0, h, a => a
| succ m, h, a =>
loop m (by omega) (dfoldCast @α (by omega) (f (n - succ m) (by omega) a))
loop n (by omega) (dfoldCast @α (by omega) init)
/--
`Nat.dfoldRev` evaluates `f` on the numbers up to `n` exclusive, in decreasing order:
* `Nat.dfoldRev f 3 init = f 0 <| f 1 <| f 2 <| init`
The input and output types of `f` are indexed by the current index, i.e. `f : (i : Nat) → (h : i < n) → α (i + 1) → α i`.
-/
@[specialize]
def dfoldRev (n : Nat) {α : (i : Nat) (h : i n := by omega) Type u}
(f : (i : Nat) (h : i < n) α (i + 1) α i) (init : α n) : α 0 :=
match n with
| 0 => init
| (n + 1) => dfoldRev n (α := fun i h => α i) (fun i h => f i (by omega)) (f n (by omega) init)
/-! # Theorems -/
/-! ### `fold` -/
@[simp] theorem fold_zero {α : Type u} (f : (i : Nat) i < 0 α α) (init : α) :
fold 0 f init = init := by simp [fold]
@@ -210,6 +268,8 @@ theorem fold_eq_finRange_foldl {α : Type u} (n : Nat) (f : (i : Nat) → i < n
| succ n ih =>
simp [ih, List.finRange_succ_last, List.foldl_map]
/-! ### `foldRev` -/
@[simp] theorem foldRev_zero {α : Type u} (f : (i : Nat) i < 0 α α) (init : α) :
foldRev 0 f init = init := by simp [foldRev]
@@ -223,10 +283,12 @@ theorem foldRev_eq_finRange_foldr {α : Type u} (n : Nat) (f : (i : Nat) → i <
| zero => simp
| succ n ih => simp [ih, List.finRange_succ_last, List.foldr_map]
/-! ### `any` -/
@[simp] theorem any_zero {f : (i : Nat) i < 0 Bool} : any 0 f = false := by simp [any]
@[simp] theorem any_succ {n : Nat} (f : (i : Nat) i < n + 1 Bool) :
any (n + 1) f = (any n (fun i h => f i (by omega)) || f n (by omega)) := by simp [any]
any (n + 1) f = (any n (fun i h => f i (by omega)) || f n (by omega)) := by simp [any]
theorem any_eq_finRange_any {n : Nat} (f : (i : Nat) i < n Bool) :
any n f = (List.finRange n).any (fun i, h => f i h) := by
@@ -234,10 +296,12 @@ theorem any_eq_finRange_any {n : Nat} (f : (i : Nat) → i < n → Bool) :
| zero => simp
| succ n ih => simp [ih, List.finRange_succ_last, List.any_map, Function.comp_def]
/-! ### `all` -/
@[simp] theorem all_zero {f : (i : Nat) i < 0 Bool} : all 0 f = true := by simp [all]
@[simp] theorem all_succ {n : Nat} (f : (i : Nat) i < n + 1 Bool) :
all (n + 1) f = (all n (fun i h => f i (by omega)) && f n (by omega)) := by simp [all]
all (n + 1) f = (all n (fun i h => f i (by omega)) && f n (by omega)) := by simp [all]
theorem all_eq_finRange_all {n : Nat} (f : (i : Nat) i < n Bool) :
all n f = (List.finRange n).all (fun i, h => f i h) := by
@@ -245,12 +309,108 @@ theorem all_eq_finRange_all {n : Nat} (f : (i : Nat) → i < n → Bool) :
| zero => simp
| succ n ih => simp [ih, List.finRange_succ_last, List.all_map, Function.comp_def]
/-! ### `dfold` -/
@[simp]
theorem dfold_zero
{α : (i : Nat) (h : i 0 := by omega) Type u}
(f : (i : Nat) (h : i < 0) α i α (i + 1)) (init : α 0) :
dfold 0 f init = init := by
simp [dfold, dfold.loop]
private theorem dfold_loop_succ
{α : (i : Nat) (h : i n + 1 := by omega) Type u}
(f : (i : Nat) (h : i < n + 1) α i α (i + 1))
(a : α (n + 1 - (j + 1))) (w : j n):
dfold.loop (n + 1) f (j + 1) (by omega) a =
f n (by omega)
(dfold.loop n (α := fun i h => α i) (fun i h => f i (by omega)) j w (dfoldCast @α (by omega) a)) := by
induction j with
| zero => simp [dfold.loop]
| succ j ih =>
rw [dfold.loop, ih _ (by omega)]
congr 2
simp only [succ_eq_add_one, dfoldCast_trans]
rw [apply_dfoldCast (h := by omega) f]
· erw [dfoldCast_trans (h := by omega)]
erw [dfoldCast_eq_dfoldCast_iff]
omega
@[simp]
theorem dfold_succ
{α : (i : Nat) (h : i n + 1 := by omega) Type u}
(f : (i : Nat) (h : i < n + 1) α i α (i + 1)) (init : α 0) :
dfold (n + 1) f init =
f n (by omega) (dfold n (α := fun i h => α i) (fun i h => f i (by omega)) init) := by
simp [dfold]
rw [dfold_loop_succ (w := Nat.le_refl _)]
congr 2
simp only [dfoldCast_trans]
erw [dfoldCast_eq_dfoldCast_iff]
exact le_add_left 0 (n + 1)
-- This isn't a proper `@[congr]` lemma, but it doesn't seem possible to state one.
theorem dfold_congr
{n m : Nat} (w : n = m)
{α : (i : Nat) (h : i n := by omega) Type u}
(f : (i : Nat) (h : i < n) α i α (i + 1)) (init : α 0) :
dfold n f init =
cast (by subst w; rfl)
(dfold m (α := fun i h => α i) (fun i h => f i (by omega)) init) := by
subst w
rfl
theorem dfold_add
{α : (i : Nat) (h : i n + m := by omega) Type u}
(f : (i : Nat) (h : i < n + m) α i α (i + 1)) (init : α 0) :
dfold (n + m) f init =
dfold m (α := fun i h => α (n + i)) (fun i h => f (n + i) (by omega))
(dfold n (α := fun i h => α i) (fun i h => f i (by omega)) init) := by
induction m with
| zero => simp; rfl
| succ m ih =>
simp [dfold_congr (Nat.add_assoc n m 1).symm, ih]
@[simp] theorem dfoldRev_zero
{α : (i : Nat) (h : i 0 := by omega) Type u}
(f : (i : Nat) (_ : i < 0) α (i + 1) α i) (init : α 0) :
dfoldRev 0 f init = init := by
simp [dfoldRev]
@[simp] theorem dfoldRev_succ
{α : (i : Nat) (h : i n + 1 := by omega) Type u}
(f : (i : Nat) (h : i < n + 1) α (i + 1) α i) (init : α (n + 1)) :
dfoldRev (n + 1) f init =
dfoldRev n (α := fun i h => α i) (fun i h => f i (by omega)) (f n (by omega) init) := by
simp [dfoldRev]
@[congr]
theorem dfoldRev_congr
{n m : Nat} (w : n = m)
{α : (i : Nat) (h : i n := by omega) Type u}
(f : (i : Nat) (h : i < n) α (i + 1) α i) (init : α n) :
dfoldRev n f init =
dfoldRev m (α := fun i h => α i) (fun i h => f i (by omega))
(cast (by subst w; rfl) init) := by
subst w
rfl
theorem dfoldRev_add
{α : (i : Nat) (h : i n + m := by omega) Type u}
(f : (i : Nat) (h : i < n + m) α (i + 1) α i) (init : α (n + m)) :
dfoldRev (n + m) f init =
dfoldRev n (α := fun i h => α i) (fun i h => f i (by omega))
(dfoldRev m (α := fun i h => α (n + i)) (fun i h => f (n + i) (by omega)) init) := by
induction m with
| zero => simp; rfl
| succ m ih => simp [ Nat.add_assoc, ih]
end Nat
namespace Prod
/--
Combines an initial value with each natural number from in a range, in increasing order.
Combines an initial value with each natural number from a range, in increasing order.
In particular, `(start, stop).foldI f init` applies `f`on all the numbers
from `start` (inclusive) to `stop` (exclusive) in increasing order:
@@ -260,7 +420,7 @@ Examples:
* `(5, 8).foldI (fun j _ _ xs => xs.push j) #[] = #[5, 6, 7]`
* `(5, 8).foldI (fun j _ _ xs => toString j :: xs) [] = ["7", "6", "5"]`
-/
@[inline] def foldI {α : Type u} (i : Nat × Nat) (f : (j : Nat) i.1 j j < i.2 α α) (init : α) : α :=
@[inline, simp] def foldI {α : Type u} (i : Nat × Nat) (f : (j : Nat) i.1 j j < i.2 α α) (init : α) : α :=
(i.2 - i.1).fold (fun j _ => f (i.1 + j) (by omega) (by omega)) init
/--
@@ -274,7 +434,7 @@ Examples:
* `(5, 8).anyI (fun j _ _ => j % 2 = 0) = true`
* `(6, 6).anyI (fun j _ _ => j % 2 = 0) = false`
-/
@[inline] def anyI (i : Nat × Nat) (f : (j : Nat) i.1 j j < i.2 Bool) : Bool :=
@[inline, simp] def anyI (i : Nat × Nat) (f : (j : Nat) i.1 j j < i.2 Bool) : Bool :=
(i.2 - i.1).any (fun j _ => f (i.1 + j) (by omega) (by omega))
/--
@@ -288,7 +448,7 @@ Examples:
* `(5, 8).allI (fun j _ _ => j % 2 = 0) = false`
* `(6, 7).allI (fun j _ _ => j % 2 = 0) = true`
-/
@[inline] def allI (i : Nat × Nat) (f : (j : Nat) i.1 j j < i.2 Bool) : Bool :=
@[inline, simp] def allI (i : Nat × Nat) (f : (j : Nat) i.1 j j < i.2 Bool) : Bool :=
(i.2 - i.1).all (fun j _ => f (i.1 + j) (by omega) (by omega))
end Prod

View File

@@ -8,9 +8,37 @@ module
prelude
import Init.Data.Array.Lemmas
import Init.Data.Option.List
import all Init.Data.Option.Instances
namespace Option
@[simp, grind] theorem mem_toArray {a : α} {o : Option α} : a o.toArray o = some a := by
cases o <;> simp [eq_comm]
@[simp, grind] theorem forIn'_toArray [Monad m] (o : Option α) (b : β) (f : (a : α) a o.toArray β m (ForInStep β)) :
forIn' o.toArray b f = forIn' o b fun a m b => f a (by simpa using m) b := by
cases o <;> simp <;> rfl
@[simp, grind] theorem forIn_toArray [Monad m] (o : Option α) (b : β) (f : α β m (ForInStep β)) :
forIn o.toArray b f = forIn o b f := by
cases o <;> simp <;> rfl
@[simp, grind] theorem foldlM_toArray [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : α β m α) :
o.toArray.foldlM f a = o.elim (pure a) (fun b => f a b) := by
cases o <;> simp
@[simp, grind] theorem foldrM_toArray [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : β α m α) :
o.toArray.foldrM f a = o.elim (pure a) (fun b => f b a) := by
cases o <;> simp
@[simp, grind] theorem foldl_toArray (o : Option β) (a : α) (f : α β α) :
o.toArray.foldl f a = o.elim a (fun b => f a b) := by
cases o <;> simp
@[simp, grind] theorem foldr_toArray (o : Option β) (a : α) (f : β α α) :
o.toArray.foldr f a = o.elim a (fun b => f b a) := by
cases o <;> simp
@[simp]
theorem toList_toArray {o : Option α} : o.toArray.toList = o.toList := by
cases o <;> simp
@@ -23,4 +51,47 @@ theorem toArray_filter {o : Option α} {p : α → Bool} :
(o.filter p).toArray = o.toArray.filter p := by
rw [ toArray_toList, toList_filter, List.filter_toArray, toArray_toList]
theorem toArray_bind {o : Option α} {f : α Option β} :
(o.bind f).toArray = o.toArray.flatMap (Option.toArray f) := by
cases o <;> simp
theorem toArray_join {o : Option (Option α)} : o.join.toArray = o.toArray.flatMap Option.toArray := by
simp [toArray_bind, bind_id_eq_join]
theorem toArray_map {o : Option α} {f : α β} : (o.map f).toArray = o.toArray.map f := by
cases o <;> simp
theorem toArray_min [Min α] {o o' : Option α} :
(min o o').toArray = o.toArray.zipWith min o'.toArray := by
cases o <;> cases o' <;> simp
@[simp]
theorem size_toArray_le {o : Option α} : o.toArray.size 1 := by
cases o <;> simp
theorem size_toArray_eq_ite {o : Option α} :
o.toArray.size = if o.isSome then 1 else 0 := by
cases o <;> simp
@[simp]
theorem toArray_eq_empty_iff {o : Option α} : o.toArray = #[] o = none := by
cases o <;> simp
@[simp]
theorem toArray_eq_singleton_iff {o : Option α} : o.toArray = #[a] o = some a := by
cases o <;> simp
@[simp]
theorem size_toArray_eq_zero_iff {o : Option α} :
o.toArray.size = 0 o = none := by
cases o <;> simp
@[simp]
theorem size_toArray_eq_one_iff {o : Option α} :
o.toArray.size = 1 o.isSome := by
cases o <;> simp
theorem size_toArray_choice_eq_one [Nonempty α] : (choice α).toArray.size = 1 := by
simp
end Option

View File

@@ -8,11 +8,16 @@ module
prelude
import Init.Data.Option.Basic
import Init.Data.Option.List
import Init.Data.Option.Array
import Init.Data.Array.Attach
import Init.Data.List.Attach
import Init.BinderPredicates
namespace Option
instance {o : Option α} : Subsingleton { x // o = some x } where
allEq a b := Subtype.ext (Option.some.inj (a.property.symm.trans b.property))
/--
Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
`Option {x // P x}` is the same as the input `Option α`.
@@ -86,7 +91,7 @@ theorem attachWith_map_subtype_val {p : α → Prop} (o : Option α) (H : ∀ a,
(o.attachWith p H).map Subtype.val = o :=
(attachWith_map_val _ _ _).trans (congrFun Option.map_id _)
theorem attach_eq_some : (o : Option a) (x : {x // o = some x}), o.attach = some x
theorem attach_eq_some : (o : Option α) (x : {x // o = some x}), o.attach = some x
| none, x, h => by simp at h
| some a, x, h => by simpa using h
@@ -123,20 +128,41 @@ theorem mem_attach : ∀ (o : Option α) (x : {x // o = some x}), x ∈ o.attach
cases o <;> cases x <;> simp
@[simp] theorem get_attach {o : Option α} (h : o.attach.isSome = true) :
o.attach.get h = o.get (by simpa using h), by simp := by
cases o
· simp at h
· simp [get_some]
o.attach.get h = o.get (by simpa using h), by simp :=
Subsingleton.elim _ _
@[simp] theorem getD_attach {o : Option α} {fallback} :
o.attach.getD fallback = fallback :=
Subsingleton.elim _ _
@[simp] theorem get!_attach {o : Option α} [Inhabited { x // o = some x }] :
o.attach.get! = default :=
Subsingleton.elim _ _
@[simp] theorem get_attachWith {p : α Prop} {o : Option α} (H : a, o = some a p a) (h : (o.attachWith p H).isSome) :
(o.attachWith p H).get h = o.get (by simpa using h), H _ (by simp) := by
cases o
· simp at h
· simp [get_some]
cases o <;> simp
@[simp] theorem getD_attachWith {p : α Prop} {o : Option α} {h} {fallback} :
(o.attachWith p h).getD fallback =
o.getD fallback.1, by cases o <;> (try exact fallback.2) <;> exact h _ (by simp) := by
cases o <;> simp
theorem toList_attach (o : Option α) :
o.attach.toList = o.toList.attach.map fun x, h => x, by simpa using h := by
cases o <;> simp [toList]
o.attach.toList = o.toList.attach.map fun x => x.1, by simpa using x.2 := by
cases o <;> simp
theorem toList_attachWith {p : α Prop} {o : Option α} {h} :
(o.attachWith p h).toList = o.toList.attach.map fun x => x.1, h _ (by simpa using x.2) := by
cases o <;> simp
theorem toArray_attach (o : Option α) :
o.attach.toArray = o.toArray.attach.map fun x => x.1, by simpa using x.2 := by
cases o <;> simp
theorem toArray_attachWith {p : α Prop} {o : Option α} {h} :
(o.attachWith p h).toArray = o.toArray.attach.map fun x => x.1, h _ (by simpa using x.2) := by
cases o <;> simp
@[simp, grind =] theorem attach_toList (o : Option α) :
o.toList.attach = (o.attach.map fun a, h => a, by simpa using h).toList := by
@@ -203,6 +229,11 @@ theorem attach_filter {o : Option α} {p : α → Bool} :
· rintro h, rfl
simp [h]
theorem filter_attachWith {P : α Prop} {o : Option α} {h : x, o = some x P x} {q : α Bool} :
(o.attachWith P h).filter q =
(o.filter q).attachWith P (fun _ h' => h _ (eq_some_of_filter_eq_some h')) := by
cases o <;> simp [filter_some] <;> split <;> simp
theorem filter_attach {o : Option α} {p : {x // o = some x} Bool} :
o.attach.filter p = o.pbind fun a h => if p a, h then some a, h else none := by
cases o <;> simp [filter_some]
@@ -211,6 +242,64 @@ theorem toList_pbind {o : Option α} {f : (a : α) → o = some a → Option β}
(o.pbind f).toList = o.attach.toList.flatMap (fun x, h => (f x h).toList) := by
cases o <;> simp
theorem toArray_pbind {o : Option α} {f : (a : α) o = some a Option β} :
(o.pbind f).toArray = o.attach.toArray.flatMap (fun x, h => (f x h).toArray) := by
cases o <;> simp
theorem toList_pfilter {o : Option α} {p : (a : α) o = some a Bool} :
(o.pfilter p).toList = (o.toList.attach.filter (fun x => p x.1 (by simpa using x.2))).unattach := by
cases o with
| none => simp
| some a =>
simp only [pfilter_some, toList_some, List.attach_cons, List.attach_nil, List.map_nil]
split <;> rename_i h
· rw [List.filter_cons_of_pos h]; simp
· rw [List.filter_cons_of_neg h]; simp
theorem toArray_pfilter {o : Option α} {p : (a : α) o = some a Bool} :
(o.pfilter p).toArray = (o.toArray.attach.filter (fun x => p x.1 (by simpa using x.2))).unattach := by
cases o with
| none => simp
| some a =>
simp only [pfilter_some, toArray_some, List.attach_toArray, List.attachWith_mem_toArray,
List.attach_cons, List.attach_nil, List.map_nil, List.map_cons, List.size_toArray,
List.length_cons, List.length_nil, Nat.zero_add, List.filter_toArray', List.unattach_toArray]
split <;> rename_i h
· rw [List.filter_cons_of_pos h]; simp
· rw [List.filter_cons_of_neg h]; simp
theorem toList_pmap {p : α Prop} {o : Option α} {f : (a : α) p a β}
(h : a, o = some a p a) :
(o.pmap f h).toList = o.attach.toList.map (fun x => f x.1 (h _ x.2)) := by
cases o <;> simp
theorem toArray_pmap {p : α Prop} {o : Option α} {f : (a : α) p a β}
(h : a, o = some a p a) :
(o.pmap f h).toArray = o.attach.toArray.map (fun x => f x.1 (h _ x.2)) := by
cases o <;> simp
theorem attach_pfilter {o : Option α} {p : (a : α) o = some a Bool} :
(o.pfilter p).attach =
o.attach.pbind fun x h => if h' : p x (by simp_all) then
some x.1, by simpa [pfilter_eq_some_iff] using _, h' else none := by
cases o with
| none => simp
| some a =>
simp only [attach_some, eq_mp_eq_cast, id_eq, pbind_some]
rw [attach_congr pfilter_some]
split <;> simp [*]
theorem attach_guard {p : α Bool} {x : α} :
(guard p x).attach = if h : p x then some x, by simp_all else none := by
simp only [guard_eq_ite]
split <;> simp [*]
theorem attachWith_guard {q : α Bool} {x : α} {P : α Prop}
{h : a, guard q x = some a P a} :
(guard q x).attachWith P h = if h' : q x then some x, h _ (by simp_all) else none := by
simp only [guard_eq_ite]
split <;> simp [*]
/-! ## unattach
`Option.unattach` is the (one-sided) inverse of `Option.attach`. It is a synonym for `Option.map Subtype.val`.
@@ -255,6 +344,29 @@ def unattach {α : Type _} {p : α → Prop} (o : Option { x // p x }) := o.map
(o.attachWith p H).unattach = o := by
cases o <;> simp
theorem unattach_eq_some_iff {p : α Prop} {o : Option { x // p x }} {x : α} :
o.unattach = some x h, o = some x, h :=
match o with
| none => by simp
| some y, h => by simpa using fun h' => h' h
@[simp]
theorem unattach_eq_none_iff {p : α Prop} {o : Option { x // p x }} :
o.unattach = none o = none := by
cases o <;> simp
theorem get_unattach {p : α Prop} {o : Option { x // p x }} {h} :
o.unattach.get h = (o.get (by simpa using h)).1 := by
cases o <;> simp
theorem toList_unattach {p : α Prop} {o : Option { x // p x }} :
o.unattach.toList = o.toList.unattach := by
cases o <;> simp
theorem toArray_unattach {p : α Prop} {o : Option { x // p x }} :
o.unattach.toArray = o.toArray.unattach := by
cases o <;> simp
/-! ### Recognizing higher order functions on subtypes using a function that only depends on the value. -/
/--
@@ -279,4 +391,51 @@ and simplifies these to the function directly taking the value.
· simp only [filter_some, hf, unattach_some]
split <;> simp
@[simp] theorem unattach_guard {p : α Prop} {q : { x // p x } Bool} {r : α Bool}
(hq : x h, q x, h = r x) {x : { x // p x }} :
(guard q x).unattach = guard r x.1 := by
simp only [guard]
split <;> simp_all
@[simp] theorem unattach_pfilter {p : α Prop} {o : Option { x // p x }}
{f : (a : { x // p x }) o = some a Bool}
{g : (a : α) o.unattach = some a Bool} (hf : x h h', f x, h h' = g x (by simp_all)) :
(o.pfilter f).unattach = o.unattach.pfilter g := by
cases o with
| none => simp
| some a =>
simp only [hf, pfilter_some, unattach_some]
split <;> simp
@[simp] theorem unattach_merge {p : α Prop} {f : { x // p x } { x // p x } { x // p x }}
{g : α α α} (hf : x h y h', (f x, h y, h').1 = g x y) {o o' : Option { x // p x }} :
(o.merge f o').unattach = o.unattach.merge g o'.unattach := by
cases o <;> cases o' <;> simp [*]
theorem any_attach {p : α Bool} {o : Option α} {q : { x // o = some x } Bool}
(h : x h, q x, h = p x) : o.attach.any q = o.any p := by
cases o <;> simp [*]
theorem any_attachWith {p : α Bool} {o : Option α} {r : α Prop} (hr : x, o = some x r x)
{q : { x // r x } Bool}
(h : x h, q x, h = p x) : (o.attachWith r hr).any q = o.any p := by
cases o <;> simp [*]
theorem any_unattach {p : α Prop} {o : Option { x // p x }} {q : α Bool} :
o.unattach.any q = o.any (q Subtype.val) := by
cases o <;> simp
theorem all_attach {p : α Bool} {o : Option α} {q : { x // o = some x } Bool}
(h : x h, q x, h = p x) : o.attach.all q = o.all p := by
cases o <;> simp [*]
theorem all_attachWith {p : α Bool} {o : Option α} {r : α Prop} (hr : x, o = some x r x)
{q : { x // r x } Bool}
(h : x h, q x, h = p x) : (o.attachWith r hr).all q = o.all p := by
cases o <;> simp [*]
theorem all_unattach {p : α Prop} {o : Option { x // p x }} {q : α Bool} :
o.unattach.all q = o.all (q Subtype.val) := by
cases o <;> simp
end Option

View File

@@ -102,11 +102,9 @@ From the perspective of `Option` as a collection with at most one element, the m
is applied to the element if present, and the final result is empty if either the initial or the
resulting collections are empty.
-/
@[inline] protected def bindM [Monad m] (f : α m (Option β)) (o : Option α) : m (Option β) := do
if let some a := o then
return ( f a)
else
return none
@[inline] protected def bindM [Pure m] (f : α m (Option β)) : Option α m (Option β)
| none => pure none
| some a => f a
/--
Applies a function in some applicative functor to an optional value, returning `none` with no

View File

@@ -14,6 +14,8 @@ import Init.Ext
namespace Option
theorem default_eq_none : (default : Option α) = none := rfl
@[deprecated mem_def (since := "2025-04-07")]
theorem mem_iff {a : α} {b : Option α} : a b b = some a := .rfl
@@ -149,6 +151,22 @@ theorem not_isSome_iff_eq_none : ¬o.isSome ↔ o = none := by
theorem ne_none_iff_isSome : o none o.isSome := by cases o <;> simp
@[simp]
theorem any_true {o : Option α} : o.any (fun _ => true) = o.isSome := by
cases o <;> simp
@[simp]
theorem any_false {o : Option α} : o.any (fun _ => false) = false := by
cases o <;> simp
@[simp]
theorem all_true {o : Option α} : o.all (fun _ => true) = true := by
cases o <;> simp
@[simp]
theorem all_false {o : Option α} : o.all (fun _ => false) = o.isNone := by
cases o <;> simp
theorem ne_none_iff_exists : o none x, some x = o := by cases o <;> simp
theorem ne_none_iff_exists' : o none x, o = some x :=
@@ -176,8 +194,6 @@ abbrev ball_ne_none := @forall_ne_none
@[simp, grind] theorem bind_eq_bind : bind = @Option.bind α β := rfl
@[simp, grind] theorem orElse_eq_orElse : HOrElse.hOrElse = @Option.orElse α := rfl
@[simp, grind] theorem bind_fun_some (x : Option α) : x.bind some = x := by cases x <;> rfl
@[simp] theorem bind_fun_none (x : Option α) : x.bind (fun _ => none (α := β)) = none := by
@@ -238,10 +254,18 @@ theorem isSome_apply_of_isSome_bind {α β : Type _} {x : Option α} {f : α
(isSome_apply_of_isSome_bind h) := by
cases x <;> trivial
theorem join_eq_bind_id {x : Option (Option α)} : x.join = x.bind id := rfl
theorem any_bind {p : β Bool} {f : α Option β} {o : Option α} :
(o.bind f).any p = o.any (Option.any p f) := by
cases o <;> simp
theorem all_bind {p : β Bool} {f : α Option β} {o : Option α} :
(o.bind f).all p = o.all (Option.all p f) := by
cases o <;> simp
@[grind] theorem bind_id_eq_join {x : Option (Option α)} : x.bind id = x.join := rfl
theorem join_eq_some_iff : x.join = some a x = some (some a) := by
simp [join_eq_bind_id, bind_eq_some_iff]
simp [ bind_id_eq_join, bind_eq_some_iff]
@[deprecated join_eq_some_iff (since := "2025-04-10")]
abbrev join_eq_some := @join_eq_some_iff
@@ -253,12 +277,14 @@ theorem join_ne_none' : ¬x.join = none ↔ ∃ z, x = some (some z) :=
join_ne_none
theorem join_eq_none_iff : o.join = none o = none o = some none :=
match o with | none | some none | some (some _) => by simp [join_eq_bind_id]
match o with | none | some none | some (some _) => by simp [bind_id_eq_join]
@[deprecated join_eq_none_iff (since := "2025-04-10")]
abbrev join_eq_none := @join_eq_none_iff
@[grind] theorem bind_id_eq_join {x : Option (Option α)} : x.bind id = x.join := rfl
theorem bind_join {f : α Option β} {o : Option (Option α)} :
o.join.bind f = o.bind (·.bind f) := by
cases o <;> simp
@[simp, grind] theorem map_eq_map : Functor.map f = Option.map f := rfl
@@ -395,10 +421,16 @@ theorem mem_filter_iff {p : α → Bool} {a : α} {o : Option α} :
a o.filter p a o p a := by
simp
theorem filter_eq_bind (x : Option α) (p : α Bool) :
x.filter p = x.bind (Option.guard p) := by
@[grind]
theorem bind_guard (x : Option α) (p : α Bool) :
x.bind (Option.guard p) = x.filter p := by
cases x <;> rfl
@[deprecated bind_guard (since := "2025-05-15")]
theorem filter_eq_bind (x : Option α) (p : α Bool) :
x.filter p = x.bind (Option.guard p) :=
(bind_guard x p).symm
@[simp] theorem any_filter : (o : Option α)
(Option.filter p o).any q = Option.any (fun a => p a && q a) o
| none => rfl
@@ -499,6 +531,10 @@ theorem any_eq_false_iff_get (p : α → Bool) (x : Option α) :
theorem isSome_of_any {x : Option α} {p : α Bool} (h : x.any p) : x.isSome := by
cases x <;> trivial
theorem get_of_any_eq_true (p : α Bool) (x : Option α) (h : x.any p = true) :
p (x.get (isSome_of_any h)) :=
any_eq_true_iff_get p x |>.1 h |>.2
@[grind]
theorem any_map {α β : Type _} {x : Option α} {f : α β} {p : β Bool} :
(x.map f).any p = x.any (fun a => p (f a)) := by
@@ -527,29 +563,39 @@ theorem bind_map_comm {α β} {x : Option (Option α)} {f : α → β} :
theorem mem_of_mem_join {a : α} {x : Option (Option α)} (h : a x.join) : some a x :=
h.symm join_eq_some_iff.1 h
@[deprecated orElse_some (since := "2025-05-03")]
theorem some_orElse (a : α) (f) : (some a).orElse f = some a := rfl
@[deprecated orElse_none (since := "2025-05-03")]
theorem none_orElse (f : Unit Option α) : none.orElse f = f () := rfl
@[simp] theorem orElse_fun_none (x : Option α) : x.orElse (fun _ => none) = x := by cases x <;> rfl
@[simp] theorem orElse_fun_some (x : Option α) (a : α) :
x.orElse (fun _ => some a) = some (x.getD a) := by
theorem any_join {p : α Bool} {x : Option (Option α)} :
x.join.any p = x.any (Option.any p) := by
cases x <;> simp
theorem orElse_eq_some_iff (o : Option α) (f) (x : α) :
(o.orElse f) = some x o = some x o = none f () = some x := by
cases o <;> simp
theorem orElse_eq_none_iff (o : Option α) (f) : (o.orElse f) = none o = none f () = none := by
cases o <;> simp
@[grind] theorem map_orElse {x : Option α} {y} :
(x.orElse y).map f = (x.map f).orElse (fun _ => (y ()).map f) := by
theorem all_join {p : α Bool} {x : Option (Option α)} :
x.join.all p = x.all (Option.all p) := by
cases x <;> simp
theorem isNone_join {x : Option (Option α)} : x.join.isNone = x.all Option.isNone := by
cases x <;> simp
theorem isSome_join {x : Option (Option α)} : x.join.isSome = x.any Option.isSome := by
cases x <;> simp
theorem get_join {x : Option (Option α)} {h} : x.join.get h =
(x.get (Option.isSome_of_any (Option.isSome_join h))).get (get_of_any_eq_true _ _ (Option.isSome_join h)) := by
cases x with
| none => simp at h
| some _ => simp
theorem join_eq_get {x : Option (Option α)} {h} : x.join = x.get h := by
cases x with
| none => simp at h
| some _ => simp
theorem getD_join {x : Option (Option α)} {default : α} :
x.join.getD default = (x.getD (some default)).getD default := by
cases x <;> simp
theorem get!_join [Inhabited α] {x : Option (Option α)} :
x.join.get! = x.get!.get! := by
cases x <;> simp [default_eq_none]
@[simp] theorem guard_eq_some_iff : guard p a = some b a = b p a :=
if h : p a then by simp [Option.guard, h] else by simp [Option.guard, h]
@@ -562,6 +608,9 @@ abbrev guard_eq_some := @guard_eq_some_iff
@[deprecated isSome_guard (since := "2025-03-18")]
abbrev guard_isSome := @isSome_guard
@[simp] theorem isNone_guard : (Option.guard p a).isNone = !p a := by
rw [ not_isSome, isSome_guard]
@[simp] theorem guard_eq_none_iff : Option.guard p a = none p a = false :=
if h : p a then by simp [Option.guard, h] else by simp [Option.guard, h]
@@ -587,19 +636,27 @@ theorem guard_comp {p : α → Bool} {f : β → α} :
ext1 b
simp [guard]
@[grind] theorem bind_guard (x : Option α) (p : α Bool) :
x.bind (Option.guard p) = x.filter p := by
simp only [Option.filter_eq_bind, decide_eq_true_eq]
theorem get_none (a : α) {h} : none.get h = a := by
simp at h
theorem guard_eq_map (p : α Bool) :
Option.guard p = fun x => Option.map (fun _ => x) (if p x then some x else none) := by
funext x
simp [Option.guard]
@[simp]
theorem get_none_eq_iff_true {h} : (none : Option α).get h = a True := by
simp at h
theorem get_guard : (guard p a).get h = a := by
simp only [guard]
split <;> simp
@[grind]
theorem guard_def (p : α Bool) :
Option.guard p = fun x => if p x then some x else none := rfl
@[deprecated guard_def (since := "2025-05-15")]
theorem guard_eq_map (p : α Bool) :
Option.guard p = fun x => Option.map (fun _ => x) (if p x then some x else none) := by
funext x
simp [Option.guard]
theorem guard_eq_ite {p : α Bool} {x : α} :
Option.guard p x = if p x then some x else none := rfl
@@ -611,6 +668,10 @@ theorem guard_eq_filter {p : α → Bool} {x : α} :
rw [guard_eq_ite]
split <;> simp_all [filter_some, guard_eq_ite]
theorem map_guard {p : α Bool} {f : α β} {x : α} :
(Option.guard p x).map f = if p x then some (f x) else none := by
simp [guard_eq_ite]
theorem join_filter {p : Option α Bool} : {o : Option (Option α)}
(o.filter p).join = o.join.filter (fun a => p (some a))
| none => by simp
@@ -680,6 +741,44 @@ instance lawfulIdentity_merge (f : ααα) : Std.LawfulIdentity (merge
left_id a := by cases a <;> simp [merge]
right_id a := by cases a <;> simp [merge]
theorem merge_join {o o' : Option (Option α)} {f : α α α} :
o.join.merge f o'.join = (o.merge (Option.merge f) o').join := by
cases o <;> cases o' <;> simp
theorem merge_eq_some_iff {o o' : Option α} {f : α α α} {a : α} :
o.merge f o' = some a (o = some a o' = none) (o = none o' = some a)
( b c, o = some b o' = some c f b c = a) := by
cases o <;> cases o' <;> simp
@[simp]
theorem merge_eq_none_iff {o o' : Option α} : o.merge f o' = none o = none o' = none := by
cases o <;> cases o' <;> simp
@[simp]
theorem any_merge {p : α Bool} {f : α α α} (hpf : a b, p (f a b) = (p a || p b))
{o o' : Option α} : (o.merge f o').any p = (o.any p || o'.any p) := by
cases o <;> cases o' <;> simp [*]
@[simp]
theorem all_merge {p : α Bool} {f : α α α} (hpf : a b, p (f a b) = (p a && p b))
{o o' : Option α} : (o.merge f o').all p = (o.all p && o'.all p) := by
cases o <;> cases o' <;> simp [*]
@[simp]
theorem isSome_merge {o o' : Option α} {f : α α α} :
(o.merge f o').isSome = (o.isSome || o'.isSome) := by
simp [ any_true]
@[simp]
theorem isNone_merge {o o' : Option α} {f : α α α} :
(o.merge f o').isNone = (o.isNone && o'.isNone) := by
simp [ all_false]
@[simp]
theorem get_merge {o o' : Option α} {f : α α α} {i : α} [Std.LawfulIdentity f i] {h} :
(o.merge f o').get h = f (o.getD i) (o'.getD i) := by
cases o <;> cases o' <;> simp [Std.LawfulLeftIdentity.left_id, Std.LawfulRightIdentity.right_id]
@[simp, grind] theorem elim_none (x : β) (f : α β) : none.elim x f = x := rfl
@[simp, grind] theorem elim_some (x : β) (f : α β) (a : α) : (some a).elim x f = f a := rfl
@@ -693,6 +792,13 @@ theorem elim_filter {o : Option α} {b : β} :
| false => by simp [filter_some_neg h, h]
| true => by simp [filter_some_pos, h]
theorem elim_join {o : Option (Option α)} {b : β} {f : α β} :
o.join.elim b f = o.elim b (·.elim b f) := by
cases o <;> simp
theorem elim_guard : (guard p a).elim b f = if p a then f a else b := by
cases h : p a <;> simp [*, guard]
@[simp, grind] theorem getD_map (f : α β) (x : α) (o : Option α) :
(o.map f).getD (f x) = f (getD o x) := by cases o <;> rfl
@@ -727,12 +833,29 @@ theorem choice_eq_none_iff_not_nonempty : choice α = none ↔ ¬Nonempty α :=
theorem isSome_choice_iff_nonempty : (choice α).isSome Nonempty α :=
fun h => (choice α).get h, fun h => by simp only [choice, dif_pos h, isSome_some]
@[simp]
theorem isSome_choice [Nonempty α] : (choice α).isSome :=
isSome_choice_iff_nonempty.2 inferInstance
@[deprecated isSome_choice_iff_nonempty (since := "2025-03-18")]
abbrev choice_isSome_iff_nonempty := @isSome_choice_iff_nonempty
theorem isNone_choice_iff_not_nonempty : (choice α).isNone ¬Nonempty α := by
rw [isNone_iff_eq_none, choice_eq_none_iff_not_nonempty]
@[simp]
theorem isNone_choice_eq_false [Nonempty α] : (choice α).isNone = false := by
simp [ not_isSome]
@[simp]
theorem getD_choice {a} :
(choice α).getD a = (choice α).get (isSome_choice_iff_nonempty.2 a) := by
rw [get_eq_getD]
@[simp]
theorem get!_choice [Inhabited α] : (choice α).get! = (choice α).get isSome_choice := by
rw [get_eq_get!]
end choice
@[simp, grind] theorem toList_some (a : α) : (some a).toList = [a] := rfl
@@ -796,9 +919,6 @@ theorem or_self : or o o = o := by
cases o <;> rfl
instance : Std.IdempotentOp (or (α := α)) := @or_self _
theorem or_eq_orElse : or o o' = o.orElse (fun _ => o') := by
cases o <;> rfl
@[grind _=_] theorem map_or : (or o o').map f = (o.map f).or (o'.map f) := by
cases o <;> rfl
@@ -818,10 +938,54 @@ theorem getD_or {o o' : Option α} {fallback : α} :
(o.or o').getD fallback = o.getD (o'.getD fallback) := by
cases o <;> simp
@[simp]
theorem get!_or {o o' : Option α} [Inhabited α] : (o.or o').get! = o.getD o'.get! := by
cases o <;> simp
@[simp] theorem filter_or_filter {o o' : Option α} {f : α Bool} :
(o.or (o'.filter f)).filter f = (o.or o').filter f := by
cases o <;> cases o' <;> simp
theorem guard_or_guard : (guard p a).or (guard q a) = guard (fun x => p x || q x) a := by
simp only [guard]
split <;> simp_all
/-! ### `orElse` -/
/-- The `simp` normal form of `o <|> o'` is `o.or o'` via `orElse_eq_orElse` and `orElse_eq_or`. -/
@[simp, grind] theorem orElse_eq_orElse : HOrElse.hOrElse = @Option.orElse α := rfl
theorem or_eq_orElse : or o o' = o.orElse (fun _ => o') := by
cases o <;> rfl
/-- The `simp` normal form of `o.orElse f` is o.or (f ())`. -/
@[simp, grind] theorem orElse_eq_or {o : Option α} {f} : o.orElse f = o.or (f ()) := by
simp [or_eq_orElse]
@[deprecated or_some (since := "2025-05-03")]
theorem some_orElse (a : α) (f) : (some a).orElse f = some a := rfl
@[deprecated or_none (since := "2025-05-03")]
theorem none_orElse (f : Unit Option α) : none.orElse f = f () := rfl
@[deprecated or_none (since := "2025-05-13")]
theorem orElse_fun_none (x : Option α) : x.orElse (fun _ => none) = x := by simp
@[deprecated or_some (since := "2025-05-13")]
theorem orElse_fun_some (x : Option α) (a : α) :
x.orElse (fun _ => some a) = some (x.getD a) := by simp
@[deprecated or_eq_some_iff (since := "2025-05-13")]
theorem orElse_eq_some_iff (o : Option α) (f) (x : α) :
(o.orElse f) = some x o = some x o = none f () = some x := by simp
@[deprecated or_eq_none_iff (since := "2025-05-13")]
theorem orElse_eq_none_iff (o : Option α) (f) : (o.orElse f) = none o = none f () = none := by simp
@[deprecated map_or (since := "2025-05-13")]
theorem map_orElse {x : Option α} {y} :
(x.orElse y).map f = (x.map f).orElse (fun _ => (y ()).map f) := by simp [map_or]
/-! ### beq -/
section beq
@@ -860,6 +1024,42 @@ variable [BEq α]
· intro h
infer_instance
@[simp] theorem beq_none {o : Option α} : (o == none) = o.isNone := by cases o <;> simp
@[simp]
theorem filter_beq_self [ReflBEq α] {p : α Bool} {o : Option α} : (o.filter p == o) = (o.all p) := by
cases o with
| none => simp
| some _ =>
simp only [filter_some]
split <;> simp [*]
@[simp]
theorem self_beq_filter [ReflBEq α] {p : α Bool} {o : Option α} : (o == o.filter p) = (o.all p) := by
cases o with
| none => simp
| some _ =>
simp only [filter_some]
split <;> simp [*]
theorem join_beq_some {o : Option (Option α)} {a : α} : (o.join == some a) = (o == some (some a)) := by
cases o <;> simp
theorem join_beq_none {o : Option (Option α)} : (o.join == none) = (o == none || o == some none) := by
cases o <;> simp
@[simp]
theorem guard_beq_some [ReflBEq α] {x : α} {p : α Bool} : (guard p x == some x) = p x := by
simp only [guard_eq_ite]
split <;> simp [*]
theorem guard_beq_none {x : α} {p : α Bool} : (guard p x == none) = !p x := by
simp
theorem merge_beq_none {o o' : Option α} {f : α α α} :
(o.merge f o' == none) = (o == none && o' == none) := by
simp [beq_none]
end beq
/-! ### ite -/
@@ -897,6 +1097,9 @@ section ite
some a = (if p then b else none) p some a = b := by
split <;> simp_all
theorem ite_some_none_eq_some {p : Prop} {_ : Decidable p} {a b : α} :
(if p then some a else none) = some b p a = b := by simp
theorem mem_dite_none_left {x : α} {_ : Decidable p} {l : ¬ p Option α} :
(x if h : p then none else l h) h : ¬ p, x l h := by
simp
@@ -988,6 +1191,10 @@ theorem isSome_pbind_iff {o : Option α} {f : (a : α) → o = some a → Option
(o.pbind f).isSome a h, (f a h).isSome := by
cases o <;> simp
theorem isNone_pbind_iff {o : Option α} {f : (a : α) o = some a Option β} :
(o.pbind f).isNone o = none a h, f a h = none := by
cases o <;> simp
@[deprecated "isSome_pbind_iff" (since := "2025-04-01")]
theorem pbind_isSome {o : Option α} {f : (a : α) o = some a Option β} :
(o.pbind f).isSome = a h, (f a h).isSome := by
@@ -997,6 +1204,25 @@ theorem pbind_eq_some_iff {o : Option α} {f : (a : α) → o = some a → Optio
o.pbind f = some b a h, f a h = some b := by
cases o <;> simp
theorem pbind_join {o : Option (Option α)} {f : (a : α) o.join = some a Option β} :
o.join.pbind f = o.pbind (fun o' ho' => o'.pbind (fun a ha => f a (by simp_all))) := by
cases o <;> simp <;> congr
theorem isSome_of_isSome_pbind {o : Option α} {f : (a : α) o = some a Option β} :
(o.pbind f).isSome o.isSome := by
cases o <;> simp
theorem isSome_get_of_isSome_pbind {o : Option α} {f : (a : α) o = some a Option β}
(h : (o.pbind f).isSome) : (f (o.get (isSome_of_isSome_pbind h)) (by simp)).isSome := by
cases o with
| none => simp at h
| some a => simp [ h]
@[simp]
theorem get_pbind {o : Option α} {f : (a : α) o = some a Option β} {h} :
(o.pbind f).get h = (f (o.get (isSome_of_isSome_pbind h)) (by simp)).get (isSome_get_of_isSome_pbind h) := by
cases o <;> simp
/-! ### pmap -/
@[simp, grind] theorem pmap_none {p : α Prop} {f : (a : α), p a β} {h} :
@@ -1073,6 +1299,18 @@ theorem pmap_congr {α : Type u} {β : Type v}
· dsimp
rw [hf]
theorem pmap_guard {q : α Bool} {p : α Prop} (f : (x : α) p x β) {x : α}
(h : (a : α), guard q x = some a p a) :
(guard q x).pmap f h = if h' : q x then some (f x (h _ (by simp_all))) else none := by
simp only [guard_eq_ite]
split <;> simp_all
@[simp]
theorem get_pmap {p : α Bool} {f : (x : α) p x β} {o : Option α}
{h : a, o = some a p a} {h'} :
(o.pmap f h).get h' = f (o.get (by simpa using h')) (h _ (by simp)) := by
cases o <;> simp
/-! ### pelim -/
@[simp, grind] theorem pelim_none : pelim none b f = b := rfl
@@ -1101,6 +1339,22 @@ theorem pelim_filter {o : Option α} {b : β} {f : (a : α) → a ∈ o.filter p
| false => by simp [pelim_congr_left (filter_some_neg h), h]
| true => by simp [pelim_congr_left (filter_some_pos h), h]
theorem pelim_join {o : Option (Option α)} {b : β} {f : (a : α) a o.join β} :
o.join.pelim b f = o.pelim b (fun o' ho' => o'.pelim b (fun a ha => f a (by simp_all))) := by
cases o <;> simp <;> congr
@[congr]
theorem pelim_congr {o o' : Option α} {b b' : β}
{f : (a : α) o = some a β} {g : (a : α) o' = some a β}
(ho : o = o') (hb : b = b') (hf : a ha, f a (ho.trans ha) = g a ha) :
o.pelim b f = o'.pelim b' g := by
cases ho; cases hb; cases o <;> apply_assumption
theorem pelim_guard {a : α} {f : (a' : α) guard p a = some a' β} :
(guard p a).pelim b f = if h : p a then f a (by simpa) else b := by
simp only [guard]
split <;> simp
/-! ### pfilter -/
@[congr]
@@ -1132,6 +1386,15 @@ theorem isSome_of_isSome_pfilter {α : Type _} {o : Option α} {p : (a : α) →
(h : (o.pfilter p).isSome) : o.isSome :=
(isSome_pfilter_iff_get.mp h).1
theorem isNone_pfilter_iff {o : Option α} {p : (a : α) o = some a Bool} :
(o.pfilter p).isNone (a : α) (ha : o = some a), p a ha = false := by
cases o with
| none => simp
| some a =>
simp only [pfilter_some, isNone_iff_eq_none, ite_eq_right_iff, reduceCtorEq, imp_false,
Bool.not_eq_true, some.injEq]
exact fun h _ h' => h' h, fun h => h _ rfl
@[simp, grind] theorem get_pfilter {α : Type _} {o : Option α} {p : (a : α) o = some a Bool}
(h : (o.pfilter p).isSome) :
(o.pfilter p).get h = o.get (isSome_of_isSome_pfilter h) := by
@@ -1205,6 +1468,53 @@ theorem pfilter_eq_pbind_ite {α : Type _} {o : Option α}
· rfl
· simp only [Option.pfilter, Bool.cond_eq_ite, Option.pbind_some]
theorem filter_pmap {p : α Prop} {f : (a : α) p a β} {h : (a : α), o = some a p a}
{q : β Bool} : (o.pmap f h).filter q = (o.pfilter (fun a h' => q (f a (h _ h')))).pmap f
(fun _ h' => h _ (eq_some_of_pfilter_eq_some h')) := by
cases o with
| none => simp
| some a =>
simp only [pmap_some, filter_some, pfilter_some]
split <;> simp
theorem pfilter_join {o : Option (Option α)} {p : (a : α) o.join = some a Bool} :
o.join.pfilter p = (o.pfilter (fun o' h => o'.pelim false (fun a ha => p a (by simp_all)))).join := by
cases o with
| none => simp
| some o' =>
cases o' with
| none => simp
| some a =>
simp only [join_some, pfilter_some, pelim_some]
split <;> simp
theorem join_pfilter {o : Option (Option α)} {p : (o' : Option α) o = some o' Bool} :
(o.pfilter p).join = o.pbind (fun o' ho' => if p o' ho' then o' else none) := by
cases o <;> simp <;> split <;> simp
theorem elim_pfilter {o : Option α} {b : β} {f : α β} {p : (a : α) o = some a Bool} :
(o.pfilter p).elim b f = o.pelim b (fun a ha => if p a ha then f a else b) := by
cases o with
| none => simp
| some a =>
simp only [pfilter_some, pelim_some]
split <;> simp
theorem pelim_pfilter {o : Option α} {b : β} {p : (a : α) o = some a Bool}
{f : (a : α) o.pfilter p = some a β} :
(o.pfilter p).pelim b f = o.pelim b
(fun a ha => if hp : p a ha then f a (pfilter_eq_some_iff.2 _, hp) else b) := by
cases o with
| none => simp
| some a =>
simp only [pfilter_some, pelim_some]
split <;> simp
theorem pfilter_guard {a : α} {p : α Bool} {q : (a' : α) guard p a = some a' Bool} :
(guard p a).pfilter q = if (h : p a), q a (by simp [h]) then some a else none := by
simp only [guard]
split <;> simp_all
/-! ### LT and LE -/
@[simp, grind] theorem not_lt_none [LT α] {a : Option α} : ¬ a < none := by cases a <;> simp [LT.lt, Option.lt]
@@ -1217,6 +1527,112 @@ theorem pfilter_eq_pbind_ite {α : Type _} {o : Option α}
@[simp] theorem le_none [LE α] {a : Option α} : a none a = none := by cases a <;> simp
@[simp, grind] theorem some_le_some [LE α] {a b : α} : some a some b a b := by simp [LE.le, Option.le]
@[simp]
theorem filter_le [LE α] (le_refl : x : α, x x) {o : Option α} {p : α Bool} : o.filter p o := by
cases o with
| none => simp
| some _ =>
simp only [filter_some]
split <;> simp [le_refl]
@[simp]
theorem filter_lt [LT α] (lt_irrefl : x : α, ¬x < x) {o : Option α} {p : α Bool} : o.filter p < o o.any (fun a => !p a) := by
cases o with
| none => simp
| some _ =>
simp only [filter_some]
split <;> simp [*]
@[simp]
theorem le_filter [LE α] (le_refl : x : α, x x) {o : Option α} {p : α Bool} : o o.filter p o.all p := by
cases o with
| none => simp
| some _ =>
simp only [filter_some]
split <;> simp [*]
@[simp]
theorem not_lt_filter [LT α] (lt_irrefl : x : α, ¬x < x) {o : Option α} {p : α Bool} : ¬o < o.filter p := by
cases o with
| none => simp
| some _ =>
simp only [filter_some]
split <;> simp [lt_irrefl]
@[simp]
theorem pfilter_le [LE α] (le_refl : x : α, x x) {o : Option α} {p : (a : α) o = some a Bool} :
o.pfilter p o := by
cases o with
| none => simp
| some _ =>
simp only [pfilter_some]
split <;> simp [*]
@[simp]
theorem not_lt_pfilter [LT α] (lt_irrefl : x : α, ¬x < x) {o : Option α}
{p : (a : α) o = some a Bool} : ¬o < o.pfilter p := by
cases o with
| none => simp
| some _ =>
simp only [pfilter_some]
split <;> simp [lt_irrefl]
theorem join_le [LE α] {o : Option (Option α)} {o' : Option α} : o.join o' o some o' := by
cases o <;> simp
@[simp]
theorem guard_le_some [LE α] (le_refl : x : α, x x) {x : α} {p : α Bool} : guard p x some x := by
simp only [guard_eq_ite]
split <;> simp [le_refl]
@[simp]
theorem guard_lt_some [LT α] (lt_irrefl : x : α, ¬x < x) {x : α} {p : α Bool} :
guard p x < some x p x = false := by
simp only [guard_eq_ite]
split <;> simp [*]
theorem left_le_of_merge_le [LE α] {f : α α α} (hf : a b c, f a b c a c)
{o₁ o₂ o₃ : Option α} : o₁.merge f o₂ o₃ o₁ o₃ := by
cases o₁ <;> cases o₂ <;> cases o₃ <;> try (simp; done)
simpa using hf _ _ _
theorem right_le_of_merge_le [LE α] {f : α α α} (hf : a b c, f a b c b c)
{o₁ o₂ o₃ : Option α} : o₁.merge f o₂ o₃ o₂ o₃ := by
cases o₁ <;> cases o₂ <;> cases o₃ <;> try (simp; done)
simpa using hf _ _ _
theorem merge_le [LE α] {f : α α α} {o₁ o₂ o₃ : Option α}
(hf : a b c, a c b c f a b c) : o₁ o₃ o₂ o₃ o₁.merge f o₂ o₃ := by
cases o₁ <;> cases o₂ <;> cases o₃ <;> try (simp; done)
simpa using hf _ _ _
@[simp]
theorem merge_le_iff [LE α] {f : α α α} {o₁ o₂ o₃ : Option α}
(hf : a b c, f a b c a c b c) :
o₁.merge f o₂ o₃ o₁ o₃ o₂ o₃ := by
cases o₁ <;> cases o₂ <;> cases o₃ <;> simp [*]
theorem left_lt_of_merge_lt [LT α] {f : α α α} (hf : a b c, f a b < c a < c)
{o₁ o₂ o₃ : Option α} : o₁.merge f o₂ < o₃ o₁ < o₃ := by
cases o₁ <;> cases o₂ <;> cases o₃ <;> try (simp; done)
simpa using hf _ _ _
theorem right_lt_of_merge_lt [LT α] {f : α α α} (hf : a b c, f a b < c b < c)
{o₁ o₂ o₃ : Option α} : o₁.merge f o₂ < o₃ o₂ < o₃ := by
cases o₁ <;> cases o₂ <;> cases o₃ <;> try (simp; done)
simpa using hf _ _ _
theorem merge_lt [LT α] {f : α α α} {o₁ o₂ o₃ : Option α}
(hf : a b c, a < c b < c f a b < c) : o₁ < o₃ o₂ < o₃ o₁.merge f o₂ < o₃ := by
cases o₁ <;> cases o₂ <;> cases o₃ <;> try (simp; done)
simpa using hf _ _ _
@[simp]
theorem merge_lt_iff [LT α] {f : α α α} {o₁ o₂ o₃ : Option α}
(hf : a b c, f a b < c a < c b < c) :
o₁.merge f o₂ < o₃ o₁ < o₃ o₂ < o₃ := by
cases o₁ <;> cases o₂ <;> cases o₃ <;> simp [*]
/-! ### Rel -/
@[simp] theorem rel_some_some {r : α β Prop} : Rel r (some a) (some b) r a b :=
@@ -1298,4 +1714,192 @@ theorem merge_max [Max α] : merge (α := α) max = max := by
instance [Max α] : Std.LawfulIdentity (α := Option α) max none := by
rw [ merge_max]; infer_instance
instance [Max α] [Std.IdempotentOp (α := α) max] : Std.IdempotentOp (α := Option α) max where
idempotent o := by cases o <;> simp [Std.IdempotentOp.idempotent]
@[simp]
theorem max_filter_left [Max α] [Std.IdempotentOp (α := α) max] {p : α Bool} {o : Option α} :
max (o.filter p) o = o := by
cases o with
| none => simp
| some _ =>
simp only [filter_some]
split <;> simp [Std.IdempotentOp.idempotent]
@[simp]
theorem max_filter_right [Max α] [Std.IdempotentOp (α := α) max] {p : α Bool} {o : Option α} :
max o (o.filter p) = o := by
cases o with
| none => simp
| some _ =>
simp only [filter_some]
split <;> simp [Std.IdempotentOp.idempotent]
@[simp]
theorem min_filter_left [Min α] [Std.IdempotentOp (α := α) min] {p : α Bool} {o : Option α} :
min (o.filter p) o = o.filter p := by
cases o with
| none => simp
| some _ =>
simp only [filter_some]
split <;> simp [Std.IdempotentOp.idempotent]
@[simp]
theorem min_filter_right [Min α] [Std.IdempotentOp (α := α) min] {p : α Bool} {o : Option α} :
min o (o.filter p) = o.filter p := by
cases o with
| none => simp
| some _ =>
simp only [filter_some]
split <;> simp [Std.IdempotentOp.idempotent]
@[simp]
theorem max_pfilter_left [Max α] [Std.IdempotentOp (α := α) max] {o : Option α} {p : (a : α) o = some a Bool} :
max (o.pfilter p) o = o := by
cases o with
| none => simp
| some _ =>
simp only [pfilter_some]
split <;> simp [Std.IdempotentOp.idempotent]
@[simp]
theorem max_pfilter_right [Max α] [Std.IdempotentOp (α := α) max] {o : Option α} {p : (a : α) o = some a Bool} :
max o (o.pfilter p) = o := by
cases o with
| none => simp
| some _ =>
simp only [pfilter_some]
split <;> simp [Std.IdempotentOp.idempotent]
@[simp]
theorem min_pfilter_left [Min α] [Std.IdempotentOp (α := α) min] {o : Option α} {p : (a : α) o = some a Bool} :
min (o.pfilter p) o = o.pfilter p := by
cases o with
| none => simp
| some _ =>
simp only [pfilter_some]
split <;> simp [Std.IdempotentOp.idempotent]
@[simp]
theorem min_pfilter_right [Min α] [Std.IdempotentOp (α := α) min] {o : Option α} {p : (a : α) o = some a Bool} :
min o (o.pfilter p) = o.pfilter p := by
cases o with
| none => simp
| some _ =>
simp only [pfilter_some]
split <;> simp [Std.IdempotentOp.idempotent]
@[simp]
theorem isSome_max [Max α] {o o' : Option α} : (max o o').isSome = (o.isSome || o'.isSome) := by
cases o <;> cases o' <;> simp
@[simp]
theorem isNone_max [Max α] {o o' : Option α} : (max o o').isNone = (o.isNone && o'.isNone) := by
cases o <;> cases o' <;> simp
@[simp]
theorem isSome_min [Min α] {o o' : Option α} : (min o o').isSome = (o.isSome && o'.isSome) := by
cases o <;> cases o' <;> simp
@[simp]
theorem isNone_min [Min α] {o o' : Option α} : (min o o').isNone = (o.isNone || o'.isNone) := by
cases o <;> cases o' <;> simp
theorem max_join_left [Max α] {o : Option (Option α)} {o' : Option α} :
max o.join o' = (max o (some o')).get (by simp) := by
cases o <;> simp
theorem max_join_right [Max α] {o : Option α} {o' : Option (Option α)} :
max o o'.join = (max (some o) o').get (by simp) := by
cases o' <;> simp
theorem join_max [Max α] {o o' : Option (Option α)} :
(max o o').join = max o.join o'.join := by
cases o <;> cases o' <;> simp
theorem min_join_left [Min α] {o : Option (Option α)} {o' : Option α} :
min o.join o' = (min o (some o')).join := by
cases o <;> simp
theorem min_join_right [Min α] {o : Option α} {o' : Option (Option α)} :
min o o'.join = (min (some o) o').join := by
cases o' <;> simp
theorem join_min [Min α] {o o' : Option (Option α)} :
(min o o').join = min o.join o'.join := by
cases o <;> cases o' <;> simp
@[simp]
theorem min_guard_some [Min α] [Std.IdempotentOp (α := α) min] {x : α} {p : α Bool} :
min (guard p x) (some x) = guard p x := by
simp only [guard_eq_ite]
split <;> simp [Std.IdempotentOp.idempotent]
@[simp]
theorem min_some_guard [Min α] [Std.IdempotentOp (α := α) min] {x : α} {p : α Bool} :
min (some x) (guard p x) = guard p x := by
simp only [guard_eq_ite]
split <;> simp [Std.IdempotentOp.idempotent]
@[simp]
theorem max_guard_some [Max α] [Std.IdempotentOp (α := α) max] {x : α} {p : α Bool} :
max (guard p x) (some x) = some x := by
simp only [guard_eq_ite]
split <;> simp [Std.IdempotentOp.idempotent]
@[simp]
theorem max_some_guard [Max α] [Std.IdempotentOp (α := α) max] {x : α} {p : α Bool} :
max (some x) (guard p x) = some x := by
simp only [guard_eq_ite]
split <;> simp [Std.IdempotentOp.idempotent]
theorem max_eq_some_iff [Max α] {o o' : Option α} {a : α} :
max o o' = some a (o = some a o' = none) (o = none o' = some a)
( b c, o = some b o' = some c max b c = a) := by
cases o <;> cases o' <;> simp
@[simp]
theorem max_eq_none_iff [Max α] {o o' : Option α} :
max o o' = none o = none o' = none := by
cases o <;> cases o' <;> simp
@[simp]
theorem min_eq_some_iff [Min α] {o o' : Option α} {a : α} :
min o o' = some a b c, o = some b o' = some c min b c = a := by
cases o <;> cases o' <;> simp
@[simp]
theorem min_eq_none_iff [Min α] {o o' : Option α} :
min o o' = none o = none o' = none := by
cases o <;> cases o' <;> simp
@[simp]
theorem any_max [Max α] {o o' : Option α} {p : α Bool} (hp : a b, p (max a b) = (p a || p b)) :
(max o o').any p = (o.any p || o'.any p) := by
cases o <;> cases o' <;> simp [hp]
@[simp]
theorem all_min [Min α] {o o' : Option α} {p : α Bool} (hp : a b, p (min a b) = (p a || p b)) :
(min o o').all p = (o.all p || o'.all p) := by
cases o <;> cases o' <;> simp [hp]
theorem isSome_left_of_isSome_min [Min α] {o o' : Option α} : (min o o').isSome o.isSome := by
cases o <;> simp
theorem isSome_right_of_isSome_min [Min α] {o o' : Option α} : (min o o').isSome o'.isSome := by
cases o' <;> simp
@[simp]
theorem get_min [Min α] {o o' : Option α} {h} :
(min o o').get h = min (o.get (isSome_left_of_isSome_min h)) (o'.get (isSome_right_of_isSome_min h)) := by
cases o <;> cases o' <;> simp
theorem map_max [Max α] [Max β] {o o' : Option α} {f : α β} (hf : x y, f (max x y) = max (f x) (f y)) :
(max o o').map f = max (o.map f) (o'.map f) := by
cases o <;> cases o' <;> simp [*]
theorem map_min [Min α] [Min β] {o o' : Option α} {f : α β} (hf : x y, f (min x y) = min (f x) (f y)) :
(min o o').map f = min (o.map f) (o'.map f) := by
cases o <;> cases o' <;> simp [*]
end Option

View File

@@ -60,6 +60,42 @@ theorem toList_bind {o : Option α} {f : α → Option β} :
cases o <;> simp
theorem toList_join {o : Option (Option α)} : o.join.toList = o.toList.flatMap Option.toList := by
simp [toList_bind, join_eq_bind_id]
simp [toList_bind, bind_id_eq_join]
theorem toList_map {o : Option α} {f : α β} : (o.map f).toList = o.toList.map f := by
cases o <;> simp
theorem toList_min [Min α] {o o' : Option α} :
(min o o').toList = o.toList.zipWith min o'.toList := by
cases o <;> cases o' <;> simp
@[simp]
theorem length_toList_le {o : Option α} : o.toList.length 1 := by
cases o <;> simp
theorem length_toList_eq_ite {o : Option α} :
o.toList.length = if o.isSome then 1 else 0 := by
cases o <;> simp
@[simp]
theorem toList_eq_nil_iff {o : Option α} : o.toList = [] o = none := by
cases o <;> simp
@[simp]
theorem toList_eq_singleton_iff {o : Option α} : o.toList = [a] o = some a := by
cases o <;> simp
@[simp]
theorem length_toList_eq_zero_iff {o : Option α} :
o.toList.length = 0 o = none := by
cases o <;> simp
@[simp]
theorem length_toList_eq_one_iff {o : Option α} :
o.toList.length = 1 o.isSome := by
cases o <;> simp
theorem length_toList_choice_eq_one [Nonempty α] : (choice α).toList.length = 1 := by
simp
end Option

View File

@@ -13,8 +13,8 @@ import Init.Control.Lawful.Basic
namespace Option
@[simp, grind] theorem bindM_none [Monad m] (f : α m (Option β)) : none.bindM f = pure none := rfl
@[simp, grind] theorem bindM_some [Monad m] [LawfulMonad m] (a) (f : α m (Option β)) : (some a).bindM f = f a := by
@[simp, grind] theorem bindM_none [Pure m] (f : α m (Option β)) : none.bindM f = pure none := rfl
@[simp, grind] theorem bindM_some [Pure m] (a) (f : α m (Option β)) : (some a).bindM f = f a := by
simp [Option.bindM]
-- We simplify `Option.forM` to `forM`.
@@ -30,6 +30,10 @@ namespace Option
forM (o.map g) f = forM o (fun a => f (g a)) := by
cases o <;> simp
theorem forM_join [Monad m] [LawfulMonad m] (o : Option (Option α)) (f : α m PUnit) :
forM o.join f = forM o (forM · f) := by
cases o <;> simp
@[simp, grind] theorem forIn'_none [Monad m] (b : β) (f : (a : α) a none β m (ForInStep β)) :
forIn' none b f = pure b := by
rfl
@@ -97,6 +101,13 @@ theorem forIn'_eq_pelim [Monad m] [LawfulMonad m]
forIn' (o.map g) init f = forIn' o init fun a h y => f (g a) (mem_map_of_mem g h) y := by
cases o <;> simp
theorem forIn'_join [Monad m] [LawfulMonad m] (b : β) (o : Option (Option α))
(f : (a : α) a o.join β m (ForInStep β)) :
forIn' o.join b f = forIn' o b (fun o' ho' b => ForInStep.yield <$> forIn' o' b (fun a ha b' => f a (by simp_all [join_eq_some_iff]) b')) := by
cases o with
| none => simp
| some a => simpa using forIn'_congr rfl rfl (by simp)
theorem forIn_eq_elim [Monad m] [LawfulMonad m]
(o : Option α) (f : (a : α) β m (ForInStep β)) (b : β) :
forIn o b f =
@@ -126,6 +137,11 @@ theorem forIn_eq_elim [Monad m] [LawfulMonad m]
forIn (o.map g) init f = forIn o init fun a y => f (g a) y := by
cases o <;> simp
theorem forIn_join [Monad m] [LawfulMonad m]
(o : Option (Option α)) (f : α β m (ForInStep β)) :
forIn o.join init f = forIn o init (fun o' b => ForInStep.yield <$> forIn o' b f) := by
cases o <;> simp
@[simp] theorem elimM_pure [Monad m] [LawfulMonad m] (x : Option α) (y : m β) (z : α m β) :
Option.elimM (pure x : m (Option α)) y z = x.elim y z := by
simp [Option.elimM]
@@ -138,11 +154,8 @@ theorem forIn_eq_elim [Monad m] [LawfulMonad m]
(y : m γ) (z : β m γ) : Option.elimM (f <$> x) y z = (do Option.elim (f ( x)) y z) := by
simp [Option.elimM]
@[simp] theorem tryCatch_none (alternative : Unit Option α) :
(tryCatch none alternative) = alternative () := rfl
@[simp] theorem tryCatch_some (a : α) (alternative : Unit Option α) :
(tryCatch (some a) alternative) = some a := rfl
@[simp] theorem tryCatch_eq_or (o : Option α) (alternative : Unit Option α) :
tryCatch o alternative = o.or (alternative ()) := by cases o <;> rfl
@[simp] theorem throw_eq_none : throw () = (none : Option α) := rfl
@@ -151,4 +164,21 @@ theorem forIn_eq_elim [Monad m] [LawfulMonad m]
theorem filterM_some [Applicative m] (p : α m Bool) (a : α) :
(some a).filterM p = (fun b => if b then some a else none) <$> p a := rfl
theorem sequence_join [Applicative m] [LawfulApplicative m] {o : Option (Option (m α))} :
o.join.sequence = join <$> sequence (o.map sequence) := by
cases o <;> simp
theorem bindM_join [Pure m] {f : α m (Option β)} {o : Option (Option α)} :
o.join.bindM f = o.bindM (·.bindM f) := by
cases o <;> simp
theorem mapM_join [Applicative m] [LawfulApplicative m] {f : α m β} {o : Option (Option α)} :
o.join.mapM f = join <$> o.mapM (Option.mapM f) := by
cases o <;> simp
theorem mapM_guard [Applicative m] {x : α} {p : α Bool} {f : α m β} :
(guard p x).mapM f = if p x then some <$> f x else pure none := by
simp only [guard_eq_ite]
split <;> simp
end Option

View File

@@ -88,7 +88,7 @@ Ordering.gt
Ordering.lt
```
-/
@[macro_inline] def «then» (a b : Ordering) : Ordering :=
@[macro_inline, expose] def «then» (a b : Ordering) : Ordering :=
match a with
| .eq => b
| a => a
@@ -849,13 +849,4 @@ comparisons.
protected def lex' (ord₁ ord₂ : Ord α) : Ord α where
compare := compareLex ord₁.compare ord₂.compare
/--
Constructs an order which compares elements of an `Array` in lexicographic order.
-/
protected def arrayOrd [a : Ord α] : Ord (Array α) where
compare x y :=
let _ : LT α := a.toLT
let _ : BEq α := a.toBEq
if List.lex x.toList y.toList then .lt else if x == y then .eq else .gt
end Ord

View File

@@ -429,8 +429,8 @@ Examples:
def Int8.decLe (a b : Int8) : Decidable (a b) :=
inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
instance (a b : Int8) : Decidable (a < b) := Int8.decLt a b
instance (a b : Int8) : Decidable (a b) := Int8.decLe a b
attribute [instance] Int8.decLt Int8.decLe
instance : Max Int8 := maxOfLe
instance : Min Int8 := minOfLe
@@ -800,8 +800,8 @@ Examples:
def Int16.decLe (a b : Int16) : Decidable (a b) :=
inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
instance (a b : Int16) : Decidable (a < b) := Int16.decLt a b
instance (a b : Int16) : Decidable (a b) := Int16.decLe a b
attribute [instance] Int16.decLt Int16.decLe
instance : Max Int16 := maxOfLe
instance : Min Int16 := minOfLe
@@ -1187,8 +1187,8 @@ Examples:
def Int32.decLe (a b : Int32) : Decidable (a b) :=
inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
instance (a b : Int32) : Decidable (a < b) := Int32.decLt a b
instance (a b : Int32) : Decidable (a b) := Int32.decLe a b
attribute [instance] Int32.decLt Int32.decLe
instance : Max Int32 := maxOfLe
instance : Min Int32 := minOfLe
@@ -1593,8 +1593,8 @@ Examples:
def Int64.decLe (a b : Int64) : Decidable (a b) :=
inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
instance (a b : Int64) : Decidable (a < b) := Int64.decLt a b
instance (a b : Int64) : Decidable (a b) := Int64.decLe a b
attribute [instance] Int64.decLt Int64.decLe
instance : Max Int64 := maxOfLe
instance : Min Int64 := minOfLe
@@ -1986,7 +1986,7 @@ Examples:
def ISize.decLe (a b : ISize) : Decidable (a b) :=
inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
instance (a b : ISize) : Decidable (a < b) := ISize.decLt a b
instance (a b : ISize) : Decidable (a b) := ISize.decLe a b
attribute [instance] ISize.decLt ISize.decLe
instance : Max ISize := maxOfLe
instance : Min ISize := minOfLe

View File

@@ -32,22 +32,4 @@ protected theorem ne_of_lt {a b : String} (h : a < b) : a ≠ b := by
have := String.lt_irrefl a
intro h; subst h; contradiction
instance ltIrrefl : Std.Irrefl (· < · : Char Char Prop) where
irrefl := Char.lt_irrefl
instance leRefl : Std.Refl (· · : Char Char Prop) where
refl := Char.le_refl
instance leTrans : Trans (· · : Char Char Prop) (· ·) (· ·) where
trans := Char.le_trans
instance leAntisymm : Std.Antisymm (· · : Char Char Prop) where
antisymm _ _ := Char.le_antisymm
instance ltAsymm : Std.Asymm (· < · : Char Char Prop) where
asymm _ _ := Char.lt_asymm
instance leTotal : Std.Total (· · : Char Char Prop) where
total := Char.le_total
end String

View File

@@ -44,7 +44,6 @@ universe signature in consequence. The `Prop` version is `Or`.
namespace Sum
deriving instance DecidableEq for Sum
deriving instance BEq for Sum
section get

View File

@@ -222,8 +222,8 @@ Examples:
def UInt8.decLe (a b : UInt8) : Decidable (a b) :=
inferInstanceAs (Decidable (a.toBitVec b.toBitVec))
instance (a b : UInt8) : Decidable (a < b) := UInt8.decLt a b
instance (a b : UInt8) : Decidable (a b) := UInt8.decLe a b
attribute [instance] UInt8.decLt UInt8.decLe
instance : Max UInt8 := maxOfLe
instance : Min UInt8 := minOfLe
@@ -438,8 +438,8 @@ Examples:
def UInt16.decLe (a b : UInt16) : Decidable (a b) :=
inferInstanceAs (Decidable (a.toBitVec b.toBitVec))
instance (a b : UInt16) : Decidable (a < b) := UInt16.decLt a b
instance (a b : UInt16) : Decidable (a b) := UInt16.decLe a b
attribute [instance] UInt16.decLt UInt16.decLe
instance : Max UInt16 := maxOfLe
instance : Min UInt16 := minOfLe
@@ -586,8 +586,7 @@ set_option linter.deprecated false in
instance : HMod UInt32 Nat UInt32 := UInt32.modn
instance : Div UInt32 := UInt32.div
instance : LT UInt32 := UInt32.lt
instance : LE UInt32 := UInt32.le
-- `LT` and `LE` are already defined in `Init.Prelude`
/--
Bitwise complement, also known as bitwise negation, for 32-bit unsigned integers. Usually accessed
@@ -832,8 +831,8 @@ Examples:
def UInt64.decLe (a b : UInt64) : Decidable (a b) :=
inferInstanceAs (Decidable (a.toBitVec b.toBitVec))
instance (a b : UInt64) : Decidable (a < b) := UInt64.decLt a b
instance (a b : UInt64) : Decidable (a b) := UInt64.decLe a b
attribute [instance] UInt64.decLt UInt64.decLe
instance : Max UInt64 := maxOfLe
instance : Min UInt64 := minOfLe

View File

@@ -437,5 +437,4 @@ Examples:
def USize.decLe (a b : USize) : Decidable (a b) :=
inferInstanceAs (Decidable (a.toBitVec b.toBitVec))
instance (a b : USize) : Decidable (a < b) := USize.decLt a b
instance (a b : USize) : Decidable (a b) := USize.decLe a b
attribute [instance] USize.decLt USize.decLe

View File

@@ -307,6 +307,8 @@ abbrev zipWithIndex := @zipIdx
@[inline] def ofFn (f : Fin n α) : Vector α n :=
Array.ofFn f, by simp
/-! See also `Vector.ofFnM` defined in `Init.Data.Vector.OfFn`. -/
/--
Swap two elements of a vector using `Fin` indices.

View File

@@ -44,12 +44,6 @@ theorem isEqv_self [DecidableEq α] (xs : Vector α n) : Vector.isEqv xs xs (·
rcases xs with xs, rfl
simp [Array.isEqv_self]
instance [DecidableEq α] : DecidableEq (Vector α n) :=
fun xs ys =>
match h:isEqv xs ys (fun x y => x = y) with
| true => isTrue (eq_of_isEqv xs ys h)
| false => isFalse fun h' => by subst h'; rw [isEqv_self] at h; contradiction
theorem beq_eq_decide [BEq α] (xs ys : Vector α n) :
(xs == ys) = decide ( (i : Nat) (h' : i < n), xs[i] == ys[i]) := by
simp [BEq.beq, isEqv_eq_decide]

View File

@@ -53,9 +53,9 @@ theorem toArray_mk {xs : Array α} (h : xs.size = n) : (Vector.mk xs h).toArray
(Vector.mk xs size).contains a = xs.contains a := by
simp [contains]
@[simp] theorem push_mk {xs : Array α} {size : xs.size = n} {x : α} :
(Vector.mk xs size).push x =
Vector.mk (xs.push x) (by simp [size, Nat.succ_eq_add_one]) := rfl
@[simp] theorem push_mk {xs : Array α} {size : xs.size = n} :
(Vector.mk xs size).push =
fun x => Vector.mk (xs.push x) (by simp [size, Nat.succ_eq_add_one]) := rfl
@[simp] theorem pop_mk {xs : Array α} {size : xs.size = n} :
(Vector.mk xs size).pop = Vector.mk xs.pop (by simp [size]) := rfl
@@ -1660,12 +1660,12 @@ theorem forall_mem_append {p : α → Prop} {xs : Vector α n} {ys : Vector α m
( (x) (_ : x xs ++ ys), p x) ( (x) (_ : x xs), p x) ( (x) (_ : x ys), p x) := by
simp only [mem_append, or_imp, forall_and]
@[grind]
@[simp, grind]
theorem empty_append {xs : Vector α n} : (#v[] : Vector α 0) ++ xs = xs.cast (by omega) := by
rcases xs with as, rfl
simp
@[grind]
@[simp, grind]
theorem append_empty {xs : Vector α n} : xs ++ (#v[] : Vector α 0) = xs := by
rw [ toArray_inj, toArray_append, Array.append_empty]

View File

@@ -38,6 +38,11 @@ theorem mapM_pure [Monad m] [LawfulMonad m] {xs : Vector α n} (f : α → β) :
apply map_toArray_inj.mp
simp
@[simp] theorem mapM_map [Monad m] [LawfulMonad m] {f : α β} {g : β m γ} {xs : Vector α n} :
(xs.map f).mapM g = xs.mapM (g f) := by
apply map_toArray_inj.mp
simp
@[congr] theorem mapM_congr [Monad m] {xs ys : Vector α n} (w : xs = ys)
{f : α m β} :
xs.mapM f = ys.mapM f := by

View File

@@ -8,6 +8,7 @@ module
prelude
import all Init.Data.Vector.Basic
import Init.Data.Vector.Lemmas
import Init.Data.Vector.Monadic
import Init.Data.Array.OfFn
/-!
@@ -40,4 +41,122 @@ theorem back_ofFn {n} [NeZero n] {f : Fin n → α} :
(ofFn f).back = f n - 1, by have := NeZero.ne n; omega := by
simp [back]
theorem ofFn_succ {f : Fin (n+1) α} :
ofFn f = (ofFn (fun (i : Fin n) => f i.castSucc)).push (f n, by omega) := by
ext i h
· simp only [getElem_ofFn, getElem_push, Fin.castSucc_mk, left_eq_dite_iff]
intro h'
have : i = n := by omega
simp_all
theorem ofFn_add {n m} {f : Fin (n + m) α} :
ofFn f = (ofFn (fun i => f (i.castLE (Nat.le_add_right n m)))) ++ (ofFn (fun i => f (i.natAdd n))) := by
apply Vector.toArray_inj.mp
simp [Array.ofFn_add]
theorem ofFn_succ' {f : Fin (n+1) α} :
ofFn f = (#v[f 0] ++ ofFn (fun i => f i.succ)).cast (by omega) := by
apply Vector.toArray_inj.mp
simp [Array.ofFn_succ']
/-! ### ofFnM -/
/-- Construct (in a monadic context) a vector by applying a monadic function to each index. -/
def ofFnM {n} [Monad m] (f : Fin n m α) : m (Vector α n) :=
go 0 (by omega) (Array.emptyWithCapacity n) rfl where
/-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #v[f i, ..., f(n - 1)]` -/
go (i : Nat) (h' : i n) (acc : Array α) (w : acc.size = i) : m (Vector α n) := do
if h : i < n then
go (i+1) (by omega) (acc.push ( f i, h)) (by simp [w])
else
pure acc, by omega
@[simp]
theorem ofFnM_zero [Monad m] {f : Fin 0 m α} : Vector.ofFnM f = pure #v[] := by
simp [ofFnM, ofFnM.go]
private theorem ofFnM_go_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) m α}
(hi : i n := by omega) {h : xs.size = i} :
ofFnM.go f i (by omega) xs h = (do
let as ofFnM.go (fun i => f i.castSucc) i hi xs h
let a f (Fin.last n)
pure (as.push a)) := by
fun_induction ofFnM.go f i (by omega) xs h
case case1 acc h' h ih =>
if h : acc.size = n then
unfold ofFnM.go
rw [dif_neg (by omega)]
have h : ¬ acc.size + 1 < n + 1 := by omega
have : Fin.last n = acc.size, by omega := by ext; simp; omega
simp [*]
else
have : acc.size + 1 n := by omega
simp only [ih, this]
conv => rhs; unfold ofFnM.go
rw [dif_pos (by omega)]
simp
case case2 =>
omega
theorem ofFnM_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) m α} :
ofFnM f = (do
let as ofFnM fun i => f i.castSucc
let a f (Fin.last n)
pure (as.push a)) := by
simp [ofFnM, ofFnM_go_succ]
theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) m α} :
ofFnM f = (do
let as ofFnM (fun i => f (i.castLE (Nat.le_add_right n k)))
let bs ofFnM (fun i => f (i.natAdd n))
pure (as ++ bs)) := by
induction k with
| zero => simp
| succ k ih => simp [ofFnM_succ, ih, push_append]
@[simp, grind] theorem toArray_ofFnM [Monad m] [LawfulMonad m] {f : Fin n m α} :
toArray <$> ofFnM f = Array.ofFnM f := by
induction n with
| zero => simp
| succ n ih => simp [ofFnM_succ, Array.ofFnM_succ, ih]
@[simp, grind] theorem toList_ofFnM [Monad m] [LawfulMonad m] {f : Fin n m α} :
toList <$> Vector.ofFnM f = List.ofFnM f := by
unfold toList
suffices Array.toList <$> (toArray <$> ofFnM f) = List.ofFnM f by
simpa [-toArray_ofFnM]
simp
theorem ofFnM_succ' {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) m α} :
ofFnM f = (do
let a f 0
let as ofFnM fun i => f i.succ
pure ((#v[a] ++ as).cast (by omega))) := by
apply Vector.map_toArray_inj.mp
simp only [toArray_ofFnM, Array.ofFnM_succ', bind_pure_comp, map_bind, Functor.map_map,
toArray_cast, toArray_append]
congr 1
funext x
have : (fun xs : Vector α n => #[x] ++ xs.toArray) = (#[x] ++ ·) toArray := by funext xs; simp
simp [this, comp_map]
@[simp]
theorem ofFnM_pure_comp [Monad m] [LawfulMonad m] {n} {f : Fin n α} :
ofFnM (pure f) = (pure (ofFn f) : m (Vector α n)) := by
apply Vector.map_toArray_inj.mp
simp
-- Variant of `ofFnM_pure_comp` using a lambda.
-- This is not marked a `@[simp]` as it would match on every occurrence of `ofFnM`.
theorem ofFnM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n α} :
ofFnM (fun i => pure (f i)) = (pure (ofFn f) : m (Vector α n)) :=
ofFnM_pure_comp
@[simp, grind =] theorem idRun_ofFnM {f : Fin n Id α} :
Id.run (ofFnM f) = ofFn (fun i => Id.run (f i)) := by
unfold Id.run
induction n with
| zero => simp
| succ n ih => simp [ofFnM_succ', ofFn_succ', ih]
end Vector

View File

@@ -15,4 +15,5 @@ import Init.Grind.Util
import Init.Grind.Offset
import Init.Grind.PP
import Init.Grind.CommRing
import Init.Grind.Module
import Init.Grind.Ext

View File

@@ -189,7 +189,7 @@ def Mon.grevlex (m₁ m₂ : Mon) : Ordering :=
inductive Poly where
| num (k : Int)
| add (k : Int) (v : Mon) (p : Poly)
deriving BEq, Inhabited, Hashable
deriving BEq, Repr, Inhabited, Hashable
instance : LawfulBEq Poly where
eq_of_beq {a} := by

View File

@@ -0,0 +1,10 @@
/-
Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison
-/
module
prelude
import Init.Grind.Module.Basic
import Init.Grind.Module.Int

View File

@@ -0,0 +1,76 @@
/-
Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison
-/
module
prelude
import Init.Data.Int.Order
namespace Lean.Grind
class NatModule (M : Type u) extends Zero M, Add M, HMul Nat M M where
add_zero : a : M, a + 0 = a
zero_add : a : M, 0 + a = a
add_comm : a b : M, a + b = b + a
add_assoc : a b c : M, a + b + c = a + (b + c)
zero_hmul : a : M, 0 * a = 0
one_hmul : a : M, 1 * a = a
add_hmul : n m : Nat, a : M, (n + m) * a = n * a + m * a
hmul_zero : n : Nat, n * (0 : M) = 0
hmul_add : n : Nat, a b : M, n * (a + b) = n * a + n * b
mul_hmul : n m : Nat, a : M, (n * m) * a = n * (m * a)
attribute [instance 100] NatModule.toZero NatModule.toAdd NatModule.toHMul
class IntModule (M : Type u) extends Zero M, Add M, Neg M, Sub M, HMul Int M M where
add_zero : a : M, a + 0 = a
zero_add : a : M, 0 + a = a
add_comm : a b : M, a + b = b + a
add_assoc : a b c : M, a + b + c = a + (b + c)
zero_hmul : a : M, (0 : Int) * a = 0
one_hmul : a : M, (1 : Int) * a = a
add_hmul : n m : Int, a : M, (n + m) * a = n * a + m * a
neg_hmul : n : Int, a : M, (-n) * a = - (n * a)
hmul_zero : n : Int, n * (0 : M) = 0
hmul_add : n : Int, a b : M, n * (a + b) = n * a + n * b
mul_hmul : n m : Int, a : M, (n * m) * a = n * (m * a)
neg_add_cancel : a : M, -a + a = 0
sub_eq_add_neg : a b : M, a - b = a + -b
attribute [instance 100] IntModule.toZero IntModule.toAdd IntModule.toNeg IntModule.toSub IntModule.toHMul
instance IntModule.toNatModule (M : Type u) [i : IntModule M] : NatModule M :=
{ i with
hMul a x := (a : Int) * x
hmul_zero := by simp [IntModule.hmul_zero]
add_hmul := by simp [IntModule.add_hmul]
hmul_add := by simp [IntModule.hmul_add]
mul_hmul := by simp [IntModule.mul_hmul] }
/--
We keep track of rational linear combinations as integer linear combinations,
but with the assurance that we can cancel the GCD of the coefficients.
-/
class RatModule (M : Type u) extends IntModule M where
no_int_zero_divisors : (k : Int) (a : M), k 0 k * a = 0 a = 0
/-- A preorder is a reflexive, transitive relation `≤` with `a < b` defined in the obvious way. -/
class Preorder (α : Type u) extends LE α, LT α where
le_refl : a : α, a a
le_trans : a b c : α, a b b c a c
lt := fun a b => a b ¬b a
lt_iff_le_not_le : a b : α, a < b a b ¬b a := by intros; rfl
class IntModule.IsOrdered (M : Type u) [Preorder M] [IntModule M] where
neg_le_iff : a b : M, -a b -b a
neg_lt_iff : a b : M, -a < b -b < a
add_lt_left : a b c : M, a < b a + c < b + c
add_lt_right : a b c : M, a < b c + a < c + b
hmul_pos : (k : Int) (a : M), 0 < a (0 < k 0 < k * a)
hmul_neg : (k : Int) (a : M), a < 0 (0 < k k * a < 0)
hmul_nonneg : (k : Int) (a : M), 0 a 0 k 0 k * a
hmul_nonpos : (k : Int) (a : M), a 0 0 k k * a 0
end Lean.Grind

View File

@@ -0,0 +1,48 @@
/-
Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison
-/
module
prelude
import Init.Grind.Module.Basic
import Init.Omega
/-!
# `grind` instances for `Int` as an ordered module.
-/
namespace Lean.Grind
instance : IntModule Int where
add_zero := Int.add_zero
zero_add := Int.zero_add
add_comm := Int.add_comm
add_assoc := Int.add_assoc
zero_hmul := Int.zero_mul
one_hmul := Int.one_mul
add_hmul := Int.add_mul
neg_hmul := Int.neg_mul
hmul_zero := Int.mul_zero
hmul_add := Int.mul_add
mul_hmul := Int.mul_assoc
neg_add_cancel := Int.add_left_neg
sub_eq_add_neg _ _ := Int.sub_eq_add_neg
instance : Preorder Int where
le_refl := Int.le_refl
le_trans _ _ _ := Int.le_trans
lt_iff_le_not_le := by omega
instance : IntModule.IsOrdered Int where
neg_le_iff := by omega
neg_lt_iff := by omega
add_lt_left := by omega
add_lt_right := by omega
hmul_pos k a ha := fun hk => Int.mul_pos hk ha, fun h => Int.pos_of_mul_pos_left h ha
hmul_neg k a ha := fun hk => Int.mul_neg_of_pos_of_neg hk ha, fun h => Int.pos_of_mul_neg_left h ha
hmul_nonpos k a ha hk := Int.mul_nonpos_of_nonneg_of_nonpos hk ha
hmul_nonneg k a ha hk := Int.mul_nonneg hk ha
end Lean.Grind

View File

@@ -104,6 +104,26 @@ theorem flip_bool_eq (a b : Bool) : (a = b) = (b = a) := by
theorem bool_eq_to_prop (a b : Bool) : (a = b) = ((a = true) = (b = true)) := by
simp
theorem forall_or_forall {α : Sort u} {β : α Sort v} (p : α Prop) (q : (a : α) β a Prop)
: ( a : α, p a b : β a, q a b) =
( (a : α) (b : β a), p a q a b) := by
apply propext; constructor
· intro h a b; cases h a <;> simp [*]
· intro h a
apply Classical.byContradiction
intro h'; simp at h'; have h₁, b, h₂ := h'
replace h := h a b; simp [h₁, h₂] at h
theorem forall_forall_or {α : Sort u} {β : α Sort v} (p : α Prop) (q : (a : α) β a Prop)
: ( a : α, ( b : β a, q a b) p a) =
( (a : α) (b : β a), q a b p a) := by
apply propext; constructor
· intro h a b; cases h a <;> simp [*]
· intro h a
apply Classical.byContradiction
intro h'; simp at h'; have b, h₁, h₂ := h'
replace h := h a b; simp [h₁, h₂] at h
init_grind_norm
/- Pre theorems -/
not_and not_or not_ite not_forall not_exists
@@ -113,6 +133,7 @@ init_grind_norm
/- Post theorems -/
Classical.not_not
ne_eq iff_eq eq_self heq_eq_eq
forall_or_forall forall_forall_or
-- Prop equality
eq_true_eq eq_false_eq not_eq_prop
-- True

View File

@@ -877,6 +877,12 @@ instance ImplicationOrder.instCompleteLattice : CompleteLattice ImplicationOrder
@monotone _ _ _ ImplicationOrder.instOrder (fun x => (Exists (f x))) :=
fun x y hxy w, hw => w, monotone_apply w f h x y hxy hw
@[partial_fixpoint_monotone] theorem implication_order_monotone_forall
{α} [PartialOrder α] {β} (f : α β ImplicationOrder)
(h : monotone f) :
@monotone _ _ _ ImplicationOrder.instOrder (fun x => y, f x y) :=
fun x y hxy h₂ y₁ => monotone_apply y₁ f h x y hxy (h₂ y₁)
@[partial_fixpoint_monotone] theorem implication_order_monotone_and
{α} [PartialOrder α] (f₁ : α ImplicationOrder) (f₂ : α ImplicationOrder)
(h₁ : @monotone _ _ _ ImplicationOrder.instOrder f₁)
@@ -931,6 +937,12 @@ def ReverseImplicationOrder.instCompleteLattice : CompleteLattice ReverseImplica
@monotone _ _ _ ReverseImplicationOrder.instOrder (fun x => Exists (f x)) :=
fun x y hxy w, hw => w, monotone_apply w f h x y hxy hw
@[partial_fixpoint_monotone] theorem coind_monotone_forall
{α} [PartialOrder α] {β} (f : α β ReverseImplicationOrder)
(h : monotone f) :
@monotone _ _ _ ReverseImplicationOrder.instOrder (fun x => y, f x y) :=
fun x y hxy h₂ y₁ => monotone_apply y₁ f h x y hxy (h₂ y₁)
@[partial_fixpoint_monotone] theorem coind_monotone_and
{α} [PartialOrder α] (f₁ : α Prop) (f₂ : α Prop)
(h₁ : @monotone _ _ _ ReverseImplicationOrder.instOrder f₁)

View File

@@ -82,16 +82,13 @@ theorem SeqRight.monotone_seqRight [LawfulMonad m] (f : γ → m α) (g : γ
namespace Option
omit [MonoBind m] in
@[partial_fixpoint_monotone]
theorem monotone_bindM (f : γ α m (Option β)) (xs : Option α) (hmono : monotone f) :
monotone (fun x => xs.bindM (f x)) := by
cases xs with
| none => apply monotone_const
| some x =>
apply monotone_bind
· apply monotone_apply
apply hmono
· apply monotone_const
| some x => apply monotone_apply _ _ hmono
@[partial_fixpoint_monotone]
theorem monotone_mapM [LawfulMonad m] (f : γ α m β) (xs : Option α) (hmono : monotone f) :

View File

@@ -295,6 +295,7 @@ recommended_spelling "PProd" for "×'" in [PProd, «term_×'_»]
@[inherit_doc] prefix:75 "-" => Neg.neg
@[inherit_doc] prefix:100 "~~~" => Complement.complement
@[inherit_doc] postfix:max "⁻¹" => Inv.inv
@[inherit_doc] infixr:73 "" => HSMul.hSMul
/-!
Remark: the infix commands above ensure a delaborator is generated for each relations.
@@ -312,6 +313,40 @@ macro_rules | `($x % $y) => `(binop% HMod.hMod $x $y)
macro_rules | `($x ^ $y) => `(rightact% HPow.hPow $x $y)
macro_rules | `($x ++ $y) => `(binop% HAppend.hAppend $x $y)
macro_rules | `(- $x) => `(unop% Neg.neg $x)
/-!
We have a macro to make `x • y` notation participate in the expression tree elaborator,
like other arithmetic expressions such as `+`, `*`, `/`, `^`, `=`, inequalities, etc.
The macro is using the `leftact%` elaborator introduced in
[this RFC](https://github.com/leanprover/lean4/issues/2854).
As a concrete example of the effect of this macro, consider
```lean
variable [Ring R] [AddCommMonoid M] [Module R M] (r : R) (N : Submodule R M) (m : M) (n : N)
#check m + r • n
```
Without the macro, the expression would elaborate as `m + ↑(r • n : ↑N) : M`.
With the macro, the expression elaborates as `m + r • (↑n : M) : M`.
To get the first interpretation, one can write `m + (r • n :)`.
Here is a quick review of the expression tree elaborator:
1. It builds up an expression tree of all the immediately accessible operations
that are marked with `binop%`, `unop%`, `leftact%`, `rightact%`, `binrel%`, etc.
2. It elaborates every leaf term of this tree
(without an expected type, so as if it were temporarily wrapped in `(... :)`).
3. Using the types of each elaborated leaf, it computes a supremum type they can all be
coerced to, if such a supremum exists.
4. It inserts coercions around leaf terms wherever needed.
The hypothesis is that individual expression trees tend to be calculations with respect
to a single algebraic structure.
Note(kmill): If we were to remove `HSMul` and switch to using `SMul` directly,
then the expression tree elaborator would not be able to insert coercions within the right operand;
they would likely appear as `↑(x • y)` rather than `x • ↑y`, unlike other arithmetic operations.
-/
@[inherit_doc HSMul.hSMul]
macro_rules | `($x $y) => `(leftact% HSMul.hSMul $x $y)
recommended_spelling "or" for "|||" in [HOr.hOr, «term_|||_»]
recommended_spelling "xor" for "^^^" in [HXor.hXor, «term_^^^_»]
@@ -323,6 +358,7 @@ recommended_spelling "mul" for "*" in [HMul.hMul, «term_*_»]
recommended_spelling "div" for "/" in [HDiv.hDiv, «term_/_»]
recommended_spelling "mod" for "%" in [HMod.hMod, «term_%_»]
recommended_spelling "pow" for "^" in [HPow.hPow, «term_^_»]
recommended_spelling "smul" for "" in [HSMul.hSMul, «term__»]
recommended_spelling "append" for "++" in [HAppend.hAppend, «term_++_»]
/-- when used as a unary operator -/
recommended_spelling "neg" for "-" in [Neg.neg, «term-_»]

View File

@@ -1348,6 +1348,23 @@ class HPow (α : Type u) (β : Type v) (γ : outParam (Type w)) where
The meaning of this notation is type-dependent. -/
hPow : α β γ
/--
The notation typeclass for heterogeneous scalar multiplication.
This enables the notation `a • b : γ` where `a : α`, `b : β`.
It is assumed to represent a left action in some sense.
The notation `a • b` is augmented with a macro (below) to have it elaborate as a left action.
Only the `b` argument participates in the elaboration algorithm: the algorithm uses the type of `b`
when calculating the type of the surrounding arithmetic expression
and it tries to insert coercions into `b` to get some `b'`
such that `a • b'` has the same type as `b'`.
See the module documentation near the macro for more details.
-/
class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
/-- `a • b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent, but it is intended to be used for left actions. -/
hSMul : α β γ
/--
The notation typeclass for heterogeneous append.
This enables the notation `a ++ b : γ` where `a : α`, `b : β`.
@@ -1510,6 +1527,12 @@ class HomogeneousPow (α : Type u) where
/-- `a ^ b` computes `a` to the power of `b` where `a` and `b` both have the same type. -/
protected pow : α α α
/-- Typeclass for types with a scalar multiplication operation, denoted `•` (`\bu`) -/
class SMul (M : Type u) (α : Type v) where
/-- `a • b` computes the product of `a` and `b`. The meaning of this notation is type-dependent,
but it is intended to be used for left actions. -/
smul : M α α
/-- The homogeneous version of `HAppend`: `a ++ b : α` where `a b : α`. -/
class Append (α : Type u) where
/-- `a ++ b` is the result of concatenation of `a` and `b`. See `HAppend`. -/
@@ -1601,6 +1624,13 @@ instance instPowNat [NatPow α] : Pow α Nat where
instance [HomogeneousPow α] : Pow α α where
pow a b := HomogeneousPow.pow a b
@[default_instance]
instance instHSMul {α β} [SMul α β] : HSMul α β β where
hSMul := SMul.smul
instance (priority := 910) {α : Type u} [Mul α] : SMul α α where
smul x y := Mul.mul x y
@[default_instance]
instance [Append α] : HAppend α α α where
hAppend a b := Append.append a b
@@ -2303,8 +2333,8 @@ Examples:
def UInt32.decLe (a b : UInt32) : Decidable (LE.le a b) :=
inferInstanceAs (Decidable (LE.le a.toBitVec b.toBitVec))
instance (a b : UInt32) : Decidable (LT.lt a b) := UInt32.decLt a b
instance (a b : UInt32) : Decidable (LE.le a b) := UInt32.decLe a b
attribute [instance] UInt32.decLt UInt32.decLe
instance : Max UInt32 := maxOfLe
instance : Min UInt32 := minOfLe

View File

@@ -309,6 +309,10 @@ theorem exists_or : (∃ x, p x q x) ↔ (∃ x, p x) ∃ x, q x :=
theorem Exists.nonempty : ( x, p x) Nonempty α | x, _ => x
@[deprecated Exists.nonempty (since := "2025-05-19")]
theorem nonempty_of_exists {α : Sort u} {p : α Prop} : Exists (fun x => p x) Nonempty α
| w, _ => w
theorem not_forall_of_exists_not {p : α Prop} : ( x, ¬p x) ¬ x, p x
| x, hn, h => hn (h x)
@@ -692,24 +696,48 @@ attribute [local simp] Decidable.imp_iff_left_iff
@[simp] theorem dite_eq_right_iff {p : Prop} [Decidable p] {x : p α} {y : α} : (if h : p then x h else y) = y h : p, x h = y := by
split <;> simp_all
@[simp] theorem left_eq_dite_iff {p : Prop} [Decidable p] {x : α} {y : ¬ p α} : x = (if h : p then x else y h) h : ¬ p, x = y h := by
split <;> simp_all
@[simp] theorem right_eq_dite_iff {p : Prop} [Decidable p] {x : p α} {y : α} : y = (if h : p then x h else y) h : p, y = x h := by
split <;> simp_all
@[simp] theorem dite_iff_left_iff {p : Prop} [Decidable p] {x : Prop} {y : ¬ p Prop} : ((if h : p then x else y h) x) h : ¬ p, y h x := by
split <;> simp_all
@[simp] theorem dite_iff_right_iff {p : Prop} [Decidable p] {x : p Prop} {y : Prop} : ((if h : p then x h else y) y) h : p, x h y := by
split <;> simp_all
@[simp] theorem left_iff_dite_iff {p : Prop} [Decidable p] {x : Prop} {y : ¬ p Prop} : (x (if h : p then x else y h)) h : ¬ p, x y h := by
split <;> simp_all
@[simp] theorem right_iff_dite_iff {p : Prop} [Decidable p] {x : p Prop} {y : Prop} : (y (if h : p then x h else y)) h : p, y x h := by
split <;> simp_all
@[simp] theorem ite_eq_left_iff {p : Prop} [Decidable p] {x y : α} : (if p then x else y) = x ¬ p y = x := by
split <;> simp_all
@[simp] theorem ite_eq_right_iff {p : Prop} [Decidable p] {x y : α} : (if p then x else y) = y p x = y := by
split <;> simp_all
@[simp] theorem left_eq_ite_iff {p : Prop} [Decidable p] {x y : α} : x = (if p then x else y) ¬ p x = y := by
split <;> simp_all
@[simp] theorem right_eq_ite_iff {p : Prop} [Decidable p] {x y : α} : y = (if p then x else y) p y = x := by
split <;> simp_all
@[simp] theorem ite_iff_left_iff {p : Prop} [Decidable p] {x y : Prop} : ((if p then x else y) x) ¬ p y = x := by
split <;> simp_all
@[simp] theorem ite_iff_right_iff {p : Prop} [Decidable p] {x y : Prop} : ((if p then x else y) y) p x = y := by
split <;> simp_all
@[simp] theorem left_iff_ite_iff {p : Prop} [Decidable p] {x y : Prop} : (x (if p then x else y)) ¬ p x = y := by
split <;> simp_all
@[simp] theorem right_iff_ite_iff {p : Prop} [Decidable p] {x y : Prop} : (y (if p then x else y)) p y = x := by
split <;> simp_all
@[simp] theorem dite_then_false {p : Prop} [Decidable p] {x : ¬ p Prop} : (if h : p then False else x h) h : ¬ p, x h := by
split <;> simp_all

View File

@@ -255,8 +255,7 @@ abbrev measure {α : Sort u} (f : α → Nat) : WellFoundedRelation α :=
abbrev sizeOfWFRel {α : Sort u} [SizeOf α] : WellFoundedRelation α :=
measure sizeOf
instance (priority := low) [SizeOf α] : WellFoundedRelation α :=
sizeOfWFRel
attribute [instance low] sizeOfWFRel
namespace Prod
open WellFounded

View File

@@ -69,15 +69,6 @@ partial def merge (v₁ v₂ : Value) : Value :=
| choice vs, v => choice <| addChoice merge vs v
| v, choice vs => choice <| addChoice merge vs v
protected partial def format : Value Format
| top => "top"
| bot => "bot"
| choice vs => format "@" ++ @List.format _ Value.format vs
| ctor i vs => format "#" ++ if vs.isEmpty then format i.name else Format.paren (format i.name ++ @formatArray _ Value.format vs)
instance : ToFormat Value := Value.format
instance : ToString Value := Format.pretty Value.format
/--
In `truncate`, we approximate a value as `top` if depth > `truncateMaxDepth`.
TODO: add option to control this parameter.

View File

@@ -495,7 +495,10 @@ def emitNumLit (t : IRType) (v : Nat) : M Unit := do
else
emit "lean_cstr_to_nat(\""; emit v; emit "\")"
else
emit v
if v < UInt32.size then
emit v
else
emit v; emit "ULL"
def emitLit (z : VarId) (t : IRType) (v : LitVal) : M Unit := do
emitLhs z;

View File

@@ -49,23 +49,11 @@ partial def consumed (x : VarId) : FnBody → Bool
| e => !e.isTerminal && consumed x e.body
abbrev Mask := Array (Option VarId)
abbrev ProjCounts := Std.HashMap (VarId × Nat) Nat
partial def computeProjCounts (bs : Array FnBody) : ProjCounts :=
let incrementCountIfProj r b :=
if let .vdecl _ _ (.proj i v) _ := b then
r.alter (v, i) fun
| some n => some (n + 1)
| none => some 1
else
r
bs.foldl incrementCountIfProj Std.HashMap.emptyWithCapacity
/-- Auxiliary function for eraseProjIncFor -/
partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (projCounts : ProjCounts)
(mask : Mask) (keep : Array FnBody) : Array FnBody × Mask :=
partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (keep : Array FnBody) : Array FnBody × Mask :=
let done (_ : Unit) := (bs ++ keep.reverse, mask)
let keepInstr (b : FnBody) := eraseProjIncForAux y bs.pop projCounts mask (keep.push b)
let keepInstr (b : FnBody) := eraseProjIncForAux y bs.pop mask (keep.push b)
if h : bs.size < 2 then done ()
else
let b := bs.back!
@@ -77,10 +65,7 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (projCounts : Pro
let b' := bs[bs.size - 2]
match b' with
| .vdecl w _ (.proj i x) _ =>
-- We disable the inc optimization if there are multiple projections with the same base
-- and index, because the downstream transformations are incapable of correctly handling
-- the aliasing.
if w == z && y == x && projCounts[(x, i)]! == 1 then
if w == z && y == x then
/- Found
```
let z := proj[i] y
@@ -92,7 +77,7 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (projCounts : Pro
let mask := mask.set! i (some z)
let keep := keep.push b'
let keep := if n == 1 then keep else keep.push (FnBody.inc z (n-1) c p FnBody.nil)
eraseProjIncForAux y bs projCounts mask keep
eraseProjIncForAux y bs mask keep
else done ()
| _ => done ()
| _ => done ()
@@ -100,7 +85,7 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (projCounts : Pro
/-- Try to erase `inc` instructions on projections of `y` occurring in the tail of `bs`.
Return the updated `bs` and a bit mask specifying which `inc`s have been removed. -/
def eraseProjIncFor (n : Nat) (y : VarId) (bs : Array FnBody) : Array FnBody × Mask :=
eraseProjIncForAux y bs (computeProjCounts bs) (.replicate n none) #[]
eraseProjIncForAux y bs (.replicate n none) #[]
/-- Replace `reuse x ctor ...` with `ctor ...`, and remove `dec x` -/
partial def reuseToCtor (x : VarId) : FnBody FnBody

View File

@@ -65,8 +65,12 @@ def addDecl (d : Decl) : M Unit :=
def lowerLitValue (v : LCNF.LitValue) : LitVal :=
match v with
| .natVal n => .num n
| .strVal s => .str s
| .nat n => .num n
| .str s => .str s
| .uint8 v => .num (UInt8.toNat v)
| .uint16 v => .num (UInt16.toNat v)
| .uint32 v => .num (UInt32.toNat v)
| .uint64 v => .num (UInt64.toNat v)
-- TODO: This should be cached.
def lowerEnumToScalarType (name : Name) : M (Option IRType) := do
@@ -224,7 +228,7 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
return none
match decl.value with
| .value litValue =>
| .lit litValue =>
mkExpr (.lit (lowerLitValue litValue))
| .proj typeName i fvarId =>
match ( get).fvars[fvarId]? with

View File

@@ -140,7 +140,7 @@ def setBuiltinInitAttr (env : Environment) (declName : Name) (initFnName : Name
builtinInitAttr.setParam env declName initFnName
def declareBuiltin (forDecl : Name) (value : Expr) : CoreM Unit := do
let name mkAuxName (`_regBuiltin ++ forDecl) 1
let name mkAuxDeclName (kind := `_regBuiltin ++ forDecl)
let type := mkApp (mkConst `IO) (mkConst `Unit)
let decl := Declaration.defnDecl { name, levelParams := [], type, value, hints := ReducibilityHints.opaque,
safety := DefinitionSafety.safe }

View File

@@ -54,7 +54,7 @@ def eqvArgs (as₁ as₂ : Array Arg) : EqvM Bool := do
def eqvLetValue (e₁ e₂ : LetValue) : EqvM Bool := do
match e₁, e₂ with
| .value v₁, .value v₂ => return v₁ == v₂
| .lit v₁, .lit v₂ => return v₁ == v₂
| .erased, .erased => return true
| .proj s₁ i₁ x₁, .proj s₂ i₂ x₂ => pure (s₁ == s₂ && i₁ == i₂) <&&> eqvFVar x₁ x₂
| .const n₁ us₁ as₁, .const n₂ us₂ as₂ => pure (n₁ == n₂ && us₁ == us₂) <&&> eqvArgs as₁ as₂

View File

@@ -34,14 +34,22 @@ def Param.toExpr (p : Param) : Expr :=
.fvar p.fvarId
inductive LitValue where
| natVal (val : Nat)
| strVal (val : String)
-- TODO: add constructors for `Int`, `Float`, `UInt` ...
| nat (val : Nat)
| str (val : String)
| uint8 (val : UInt8)
| uint16 (val : UInt16)
| uint32 (val : UInt32)
| uint64 (val : UInt64)
-- TODO: add constructors for `Int`, `Float`, `USize` ...
deriving Inhabited, BEq, Hashable
def LitValue.toExpr : LitValue Expr
| .natVal v => .lit (.natVal v)
| .strVal v => .lit (.strVal v)
| .nat v => .lit (.natVal v)
| .str v => .lit (.strVal v)
| .uint8 v => .app (.const ``UInt8.ofNat []) (.lit (.natVal (UInt8.toNat v)))
| .uint16 v => .app (.const ``UInt16.ofNat []) (.lit (.natVal (UInt16.toNat v)))
| .uint32 v => .app (.const ``UInt32.ofNat []) (.lit (.natVal (UInt32.toNat v)))
| .uint64 v => .app (.const ``UInt64.ofNat []) (.lit (.natVal (UInt64.toNat v)))
inductive Arg where
| erased
@@ -73,7 +81,7 @@ private unsafe def Arg.updateFVarImp (arg : Arg) (fvarId' : FVarId) : Arg :=
@[implemented_by Arg.updateFVarImp] opaque Arg.updateFVar! (arg : Arg) (fvarId' : FVarId) : Arg
inductive LetValue where
| value (value : LitValue)
| lit (value : LitValue)
| erased
| proj (typeName : Name) (idx : Nat) (struct : FVarId)
| const (declName : Name) (us : List Level) (args : Array Arg)
@@ -117,8 +125,7 @@ private unsafe def LetValue.updateArgsImp (e : LetValue) (args' : Array Arg) : L
def LetValue.toExpr (e : LetValue) : Expr :=
match e with
| .value (.natVal val) => .lit (.natVal val)
| .value (.strVal val) => .lit (.strVal val)
| .lit v => v.toExpr
| .erased => erasedExpr
| .proj n i s => .proj n i (.fvar s)
| .const n us as => mkAppN (.const n us) (as.map Arg.toExpr)
@@ -457,7 +464,7 @@ where
match e with
| .const declName vs args => e.updateConst! declName (vs.mapMono instLevel) (args.mapMono instArg)
| .fvar fvarId args => e.updateFVar! fvarId (args.mapMono instArg)
| .proj .. | .value .. | .erased => e
| .proj .. | .lit .. | .erased => e
instLetDecl (decl : LetDecl) :=
decl.updateCore (instExpr decl.type) (instLetValue decl.value)
@@ -673,7 +680,7 @@ private def collectLetValue (e : LetValue) (s : FVarIdSet) : FVarIdSet :=
| .fvar fvarId args => collectArgs args <| s.insert fvarId
| .const _ _ args => collectArgs args s
| .proj _ _ fvarId => s.insert fvarId
| .value .. | .erased => s
| .lit .. | .erased => s
private partial def collectParams (ps : Array Param) (s : FVarIdSet) : FVarIdSet :=
ps.foldl (init := s) fun s p => collectType p.type s

View File

@@ -140,7 +140,7 @@ def checkAppArgs (f : Expr) (args : Array Arg) : CheckM Unit := do
def checkLetValue (e : LetValue) : CheckM Unit := do
match e with
| .value .. | .erased => pure ()
| .lit .. | .erased => pure ()
| .const declName us args => checkAppArgs (mkConst declName us) args
| .fvar fvarId args => checkFVar fvarId; checkAppArgs (.fvar fvarId) args
| .proj _ _ fvarId => checkFVar fvarId

View File

@@ -86,7 +86,7 @@ mutual
partial def collectLetValue (e : LetValue) : ClosureM Unit := do
match e with
| .erased | .value .. => return ()
| .erased | .lit .. => return ()
| .proj _ _ fvarId => collectFVar fvarId
| .const _ _ args => args.forM collectArg
| .fvar fvarId args => collectFVar fvarId; args.forM collectArg

View File

@@ -264,7 +264,7 @@ See `normExprImp`
-/
private partial def normLetValueImp (s : FVarSubst) (e : LetValue) (translator : Bool) : LetValue :=
match e with
| .erased | .value .. => e
| .erased | .lit .. => e
| .proj _ _ fvarId => match normFVarImp s fvarId translator with
| .fvar fvarId' => e.updateProj! fvarId'
| .erased => .erased

View File

@@ -25,7 +25,7 @@ private def argDepOn (a : Arg) : M Bool := do
private def letValueDepOn (e : LetValue) : M Bool :=
match e with
| .erased | .value .. => return false
| .erased | .lit .. => return false
| .proj _ _ fvarId => fvarDepOn fvarId
| .fvar fvarId args => fvarDepOn fvarId <||> args.anyM argDepOn
| .const _ _ args => args.anyM argDepOn

View File

@@ -37,7 +37,7 @@ def collectLocalDeclsArgs (s : UsedLocalDecls) (args : Array Arg) : UsedLocalDec
def collectLocalDeclsLetValue (s : UsedLocalDecls) (e : LetValue) : UsedLocalDecls :=
match e with
| .erased | .value .. => s
| .erased | .lit .. => s
| .proj _ _ fvarId => s.insert fvarId
| .const _ _ args => collectLocalDeclsArgs s args
| .fvar fvarId args => collectLocalDeclsArgs (s.insert fvarId) args

View File

@@ -171,9 +171,13 @@ where
| n + 1 => .ctor ``Nat.succ #[goSmall n]
def ofLCNFLit : LCNF.LitValue Value
| .natVal n => ofNat n
| .nat n => ofNat n
-- TODO: We could make this much more precise but the payoff is questionable
| .strVal .. => .top
| .str .. => .top
| .uint8 v => ofNat (UInt8.toNat v)
| .uint16 v => ofNat (UInt16.toNat v)
| .uint32 v => ofNat (UInt32.toNat v)
| .uint64 v => ofNat (UInt64.toNat v)
partial def proj : Value Nat Value
| .ctor _ vs , i => vs.getD i bot
@@ -206,11 +210,11 @@ partial def getLiteral (v : Value) : CompilerM (Option ((Array CodeDecl) × FVar
where
go : Value CompilerM ((Array CodeDecl) × FVarId)
| .ctor `Nat.zero #[] .. => do
let decl mkAuxLetDecl <| .value <| .natVal <| 0
let decl mkAuxLetDecl <| .lit <| .nat <| 0
return (#[.let decl], decl.fvarId)
| .ctor `Nat.succ #[val] .. => do
let val := getNatConstant val + 1
let decl mkAuxLetDecl <| .value <| .natVal <| val
let decl mkAuxLetDecl <| .lit <| .nat <| val
return (#[.let decl], decl.fvarId)
| .ctor i vs => do
let args vs.mapM go
@@ -456,7 +460,7 @@ where
-/
interpLetValue (letVal : LetValue) : InterpM Value := do
match letVal with
| .value val => return .ofLCNFLit val
| .lit val => return .ofLCNFLit val
| .proj _ idx struct => return ( findVarValue struct).proj idx
| .const declName _ args =>
let env getEnv

View File

@@ -64,14 +64,14 @@ instance : TraverseFVar Arg where
def LetValue.mapFVarM [MonadLiftT CompilerM m] [Monad m] (f : FVarId m FVarId) (e : LetValue) : m LetValue := do
match e with
| .value .. | .erased => return e
| .lit .. | .erased => return e
| .proj _ _ fvarId => return e.updateProj! ( f fvarId)
| .const _ _ args => return e.updateArgs! ( args.mapM (TraverseFVar.mapFVarM f))
| .fvar fvarId args => return e.updateFVar! ( f fvarId) ( args.mapM (TraverseFVar.mapFVarM f))
def LetValue.forFVarM [Monad m] (f : FVarId m Unit) (e : LetValue) : m Unit := do
match e with
| .value .. | .erased => return ()
| .lit .. | .erased => return ()
| .proj _ _ fvarId => f fvarId
| .const _ _ args => args.forM (TraverseFVar.forFVarM f)
| .fvar fvarId args => f fvarId; args.forM (TraverseFVar.forFVarM f)

View File

@@ -103,8 +103,12 @@ def inferConstType (declName : Name) (us : List Level) : CompilerM Expr := do
def inferLitValueType (value : LitValue) : Expr :=
match value with
| .natVal .. => mkConst ``Nat
| .strVal .. => mkConst ``String
| .nat .. => mkConst ``Nat
| .str .. => mkConst ``String
| .uint8 .. => mkConst ``UInt8
| .uint16 .. => mkConst ``UInt16
| .uint32 .. => mkConst ``UInt32
| .uint64 .. => mkConst ``UInt64
mutual
partial def inferArgType (arg : Arg) : InferTypeM Expr :=
@@ -126,7 +130,7 @@ mutual
partial def inferLetValueType (e : LetValue) : InferTypeM Expr := do
match e with
| .erased => return erasedExpr
| .value v => return inferLitValueType v
| .lit v => return inferLitValueType v
| .proj structName idx fvarId => inferProjType structName idx fvarId
| .const declName us args => inferAppTypeCore ( inferConstType declName us) args
| .fvar fvarId args => inferAppTypeCore ( getType fvarId) args

View File

@@ -111,7 +111,7 @@ def visitArgs (args : Array Arg) : Visitor :=
def visitLetValue (e : LetValue) : Visitor :=
match e with
| .erased | .value .. | .proj .. => id
| .erased | .lit .. | .proj .. => id
| .const _ us args => visitLevels us visitArgs args
| .fvar _ args => visitArgs args

View File

@@ -18,6 +18,7 @@ import Lean.Compiler.LCNF.LambdaLifting
import Lean.Compiler.LCNF.FloatLetIn
import Lean.Compiler.LCNF.ReduceArity
import Lean.Compiler.LCNF.ElimDeadBranches
import Lean.Compiler.LCNF.StructProjCases
namespace Lean.Compiler.LCNF
@@ -76,6 +77,7 @@ def builtinPassManager : PassManager := {
lambdaLifting,
extendJoinPointContext (phase := .mono) (occurrence := 1),
simp (occurrence := 5) (phase := .mono),
structProjCases,
cse (occurrence := 2) (phase := .mono),
saveMono -- End of mono phase
]

View File

@@ -56,10 +56,15 @@ def ppArg (e : Arg) : M Format := do
def ppArgs (args : Array Arg) : M Format := do
prefixJoin " " args ppArg
def ppLitValue (lit : LitValue) : M Format := do
match lit with
| .nat v | .uint8 v | .uint16 v | .uint32 v | .uint64 v => return format v
| .str v => return format (repr v)
def ppLetValue (e : LetValue) : M Format := do
match e with
| .erased => return ""
| .value v => ppExpr v.toExpr
| .lit v => ppLitValue v
| .proj _ i fvarId => return f!"{← ppFVar fvarId} # {i}"
| .fvar fvarId args => return f!"{← ppFVar fvarId}{← ppArgs args}"
| .const declName us args => return f!"{← ppExpr (.const declName us)}{← ppArgs args}"

View File

@@ -70,7 +70,7 @@ def visitArg (arg : Arg) : FindUsedM Unit := do
def visitLetValue (e : LetValue) : FindUsedM Unit := do
match e with
| .erased | .value .. => return ()
| .erased | .lit .. => return ()
| .proj _ _ fvarId => visitFVar fvarId
| .fvar fvarId args => visitFVar fvarId; args.forM visitArg
| .const declName _ args =>

View File

@@ -64,22 +64,22 @@ def mkAuxLit [Literal α] (x : α) (prefixName := `_x) : FolderM FVarId := do
mkAuxLetDecl lit prefixName
partial def getNatLit (fvarId : FVarId) : CompilerM (Option Nat) := do
let some (.value (.natVal n)) findLetValue? fvarId | return none
let some (.lit (.nat n)) findLetValue? fvarId | return none
return n
def mkNatLit (n : Nat) : FolderM LetValue :=
return .value (.natVal n)
return .lit (.nat n)
instance : Literal Nat where
getLit := getNatLit
mkLit := mkNatLit
def getStringLit (fvarId : FVarId) : CompilerM (Option String) := do
let some (.value (.strVal s)) findLetValue? fvarId | return none
let some (.lit (.str s)) findLetValue? fvarId | return none
return s
def mkStringLit (n : String) : FolderM LetValue :=
return .value (.strVal n)
return .lit (.str n)
instance : Literal String where
getLit := getStringLit
@@ -308,6 +308,14 @@ def higherOrderLiteralFolders : List (Name × Folder) := [
def Folder.mulShift [Literal α] [BEq α] (shiftLeft : Name) (pow2 : α α) (log2 : α α) : Folder :=
Folder.first #[Folder.mulLhsShift shiftLeft pow2 log2, Folder.mulRhsShift shiftLeft pow2 log2]
/--
Folder for ofNat operations on fixed-sized integer types.
-/
def Folder.ofNat (f : Nat LitValue) (args : Array Arg): FolderM (Option LetValue) := do
let #[.fvar fvarId] := args | return none
let some value getNatLit fvarId | return none
return some (.lit (f value))
/--
All arithmetic folders.
-/
@@ -355,6 +363,13 @@ def relationFolders : List (Name × Folder) := [
(``Bool.decEq, Folder.mkBinaryDecisionProcedure String.decEq)
]
def conversionFolders : List (Name × Folder) := [
(``UInt8.ofNat, Folder.ofNat (fun v => .uint8 (UInt8.ofNat v))),
(``UInt16.ofNat, Folder.ofNat (fun v => .uint16 (UInt16.ofNat v))),
(``UInt32.ofNat, Folder.ofNat (fun v => .uint32 (UInt32.ofNat v))),
(``UInt64.ofNat, Folder.ofNat (fun v => .uint64 (UInt64.ofNat v))),
]
/--
All string folders.
-/
@@ -387,7 +402,7 @@ private def getFolder (declName : Name) : CoreM Folder := do
ofExcept <| getFolderCore ( getEnv) ( getOptions) declName
def builtinFolders : SMap Name Folder :=
(arithmeticFolders ++ relationFolders ++ higherOrderLiteralFolders ++ stringFolders).foldl (init := {}) fun s (declName, folder) =>
(arithmeticFolders ++ relationFolders ++ conversionFolders ++ higherOrderLiteralFolders ++ stringFolders).foldl (init := {}) fun s (declName, folder) =>
s.insert declName folder
structure FolderOleanEntry where

View File

@@ -54,7 +54,7 @@ Remark: We use this method when simplifying projections and cases-constructor.
-/
def findCtor? (fvarId : FVarId) : DiscrM (Option CtorInfo) := do
match ( findLetDecl? fvarId) with
| some { value := .value (.natVal n), .. } =>
| some { value := .lit (.nat n), .. } =>
return some <| .natVal n
| some { value := .const declName _ args, .. } =>
let some (.ctorInfo val) := ( getEnv).find? declName | return none

View File

@@ -103,7 +103,7 @@ where
addLetValueOccs (e : LetValue) : StateRefT FunDeclInfoMap CompilerM Unit := do
match e with
| .erased | .value .. | .proj .. => return ()
| .erased | .lit .. | .proj .. => return ()
| .const _ _ args => args.forM addArgOcc
| .fvar fvarId args =>
let some funDecl findFunDecl'? fvarId | return ()

View File

@@ -52,7 +52,7 @@ where
let some letDecl findLetDecl? fvarId | failure
match letDecl.value with
| .proj _ i s => visit s (i :: projs)
| .fvar .. | .value .. | .erased => failure
| .fvar .. | .lit .. | .erased => failure
| .const declName us args =>
if let some (.ctorInfo ctorVal) := ( getEnv).find? declName then
let i :: projs := projs | unreachable!

View File

@@ -290,7 +290,7 @@ where
let argsNew := mkJmpNewArgs args info.paramIdx #[] jpAlt.dependsOnDiscr
return some <| .jmp jpAlt.decl.fvarId argsNew
| .natVal (n+1) =>
let auxDecl mkAuxLetDecl (.value (.natVal n))
let auxDecl mkAuxLetDecl (.lit (.nat n))
let argsNew := mkJmpNewArgs args info.paramIdx #[.fvar auxDecl.fvarId] jpAlt.dependsOnDiscr
return some <| .let auxDecl (.jmp jpAlt.decl.fvarId argsNew)

View File

@@ -207,7 +207,7 @@ partial def simpCasesOnCtor? (cases : Cases) : SimpM (Option Code) := do
return k
| .natVal 0 => simp k
| .natVal (n+1) =>
let auxDecl mkAuxLetDecl (.value (.natVal n))
let auxDecl mkAuxLetDecl (.lit (.nat n))
addFVarSubst params[0]!.fvarId auxDecl.fvarId
let k simp k
eraseParams params

View File

@@ -37,7 +37,7 @@ def simpAppApp? (e : LetValue) : OptionT SimpM LetValue := do
return .fvar f (args' ++ args)
| .const declName us args' => return .const declName us (args' ++ args)
| .erased => return .erased
| .proj .. | .value .. => failure
| .proj .. | .lit .. => failure
def simpCtorDiscr? (e : LetValue) : OptionT SimpM LetValue := do
let .const declName _ _ := e | failure

View File

@@ -37,7 +37,7 @@ Mark all free variables occurring in `e` as used.
-/
def markUsedLetValue (e : LetValue) : SimpM Unit := do
match e with
| .value .. | .erased => return ()
| .lit .. | .erased => return ()
| .proj _ _ fvarId => markUsedFVar fvarId
| .const _ _ args => args.forM markUsedArg
| .fvar fvarId args => markUsedFVar fvarId; args.forM markUsedArg

View File

@@ -0,0 +1,131 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Cameron Zwarich
-/
prelude
import Lean.Compiler.LCNF.Basic
import Lean.Compiler.LCNF.InferType
import Lean.Compiler.LCNF.MonoTypes
import Lean.Compiler.LCNF.PassManager
import Lean.Compiler.LCNF.PrettyPrinter
namespace Lean.Compiler.LCNF
namespace StructProjCases
def findStructCtorInfo? (typeName : Name) : CoreM (Option ConstructorVal) := do
let .inductInfo info getConstInfo typeName | return none
let [ctorName] := info.ctors | return none
let some (.ctorInfo ctorInfo) := ( getEnv).find? ctorName | return none
return ctorInfo
def mkFieldParamsForCtorType (e : Expr) (numParams : Nat): CompilerM (Array Param) := do
let rec loop (params : Array Param) (e : Expr) (numParams : Nat): CompilerM (Array Param) := do
match e with
| .forallE name type body _ =>
if numParams == 0 then
let param mkParam name ( toMonoType type) false
loop (params.push param) body numParams
else
loop params body (numParams - 1)
| _ => return params
loop #[] e numParams
structure StructProjState where
projMap : Std.HashMap FVarId (Array FVarId) := {}
fvarMap : Std.HashMap FVarId FVarId := {}
abbrev M := StateRefT StructProjState CompilerM
def M.run (x : M α) : CompilerM α := do
x.run' {}
def remapFVar (fvarId : FVarId) : M FVarId := do
return ( get).fvarMap[fvarId]?.getD fvarId
mutual
partial def visitCode (code : Code) : M Code := do
match code with
| .let decl k =>
match decl.value with
| .proj typeName i base =>
eraseLetDecl decl
let base remapFVar base
if let some projVars := ( get).projMap[base]? then
modify fun s => { s with fvarMap := s.fvarMap.insert decl.fvarId projVars[i]! }
visitCode k
else
let some ctorInfo findStructCtorInfo? typeName | panic! "expected struct constructor"
let params mkFieldParamsForCtorType ctorInfo.type ctorInfo.numParams
assert! params.size == ctorInfo.numFields
let fvars := params.map (·.fvarId)
modify fun s => { s with projMap := s.projMap.insert base fvars,
fvarMap := s.fvarMap.insert decl.fvarId fvars[i]! }
let k visitCode k
modify fun s => { s with projMap := s.projMap.erase base }
let resultType toMonoType ( k.inferType)
let alts := #[.alt ctorInfo.name params k]
return .cases { typeName, resultType, discr := base, alts }
| _ => return code.updateLet! ( decl.updateValue ( visitLetValue decl.value)) ( visitCode k)
| .fun decl k =>
let decl decl.updateValue ( visitCode decl.value)
return code.updateFun! decl ( visitCode k)
| .jp decl k =>
let decl decl.updateValue ( visitCode decl.value)
return code.updateFun! decl ( visitCode k)
| .jmp fvarId args =>
return code.updateJmp! ( remapFVar fvarId) ( args.mapM visitArg)
| .cases cases =>
let discr remapFVar cases.discr
if let #[.alt ctorName params k] := cases.alts then
if let some projVars := ( get).projMap[discr]? then
assert! projVars.size == params.size
for param in params, projVar in projVars do
modify fun s => { s with fvarMap := s.fvarMap.insert param.fvarId projVar }
eraseParam param
visitCode k
else
let fvars := params.map (·.fvarId)
modify fun s => { s with projMap := s.projMap.insert discr fvars }
let k visitCode k
modify fun s => { s with projMap := s.projMap.erase discr }
-- TODO: This should preserve the .alt allocation, but binding it to
-- a variable above while also destructuring an array doesn't work.
return code.updateCases! cases.resultType discr #[.alt ctorName params k]
else
let alts cases.alts.mapM (visitAlt ·)
return code.updateCases! cases.resultType discr alts
| .return fvarId => return code.updateReturn! ( remapFVar fvarId)
| .unreach .. => return code
partial def visitLetValue (v : LetValue) : M LetValue := do
match v with
| .const _ _ args =>
return v.updateArgs! ( args.mapM visitArg)
| .fvar fvarId args =>
return v.updateFVar! ( remapFVar fvarId) ( args.mapM visitArg)
| .lit _ | .erased => return v
-- Projections should be handled directly by `visitCode`.
| .proj .. => unreachable!
partial def visitAlt (alt : Alt) : M Alt := do
return alt.updateCode ( visitCode alt.getCode)
partial def visitArg (arg : Arg) : M Arg :=
match arg with
| .fvar fvarId => return arg.updateFVar! ( remapFVar fvarId)
| .type _ | .erased => return arg
end
def visitDecl (decl : Decl) : M Decl := do
let value decl.value.mapCodeM (visitCode ·)
return { decl with value }
end StructProjCases
def structProjCases : Pass :=
.mkPerDeclaration `structProjCases (StructProjCases.visitDecl · |>.run) .mono
end Lean.Compiler.LCNF

View File

@@ -27,7 +27,7 @@ where
| _ => false
goLetValue (l : LetValue) : Bool :=
match l with
| .value .. | .erased | .proj .. | .fvar .. => false
| .lit .. | .erased | .proj .. | .fvar .. => false
| .const name .. => name == constName
namespace Testing

View File

@@ -407,8 +407,8 @@ partial def etaReduceImplicit (e : Expr) : Expr :=
def litToValue (lit : Literal) : LitValue :=
match lit with
| .natVal val => .natVal val
| .strVal val => .strVal val
| .natVal val => .nat val
| .strVal val => .str val
/--
Put the given expression in `LCNF`.
@@ -453,7 +453,7 @@ where
visitCore e
visitLit (lit : Literal) : M Arg :=
letValueToArg (.value (litToValue lit))
letValueToArg (.lit (litToValue lit))
visitAppArg (e : Expr) : M Arg := do
if isLCProof e then

View File

@@ -44,7 +44,7 @@ def ctorAppToMono (ctorInfo : ConstructorVal) (args : Array Arg) : ToMonoM LetVa
partial def LetValue.toMono (e : LetValue) : ToMonoM LetValue := do
match e with
| .erased | .value .. => return e
| .erased | .lit .. => return e
| .const declName _ args =>
if declName == ``Decidable.isTrue then
return .const ``Bool.true [] #[]
@@ -105,7 +105,7 @@ partial def decToMono (c : Cases) (_ : c.typeName == ``Decidable) : ToMonoM Code
partial def casesNatToMono (c: Cases) (_ : c.typeName == ``Nat) : ToMonoM Code := do
let resultType toMonoType c.resultType
let natType := mkConst ``Nat
let zeroDecl mkLetDecl `zero natType (.value (.natVal 0))
let zeroDecl mkLetDecl `zero natType (.lit (.nat 0))
let isZeroDecl mkLetDecl `isZero (mkConst ``Bool) (.const ``Nat.decEq [] #[.fvar c.discr, .fvar zeroDecl.fvarId])
let alts c.alts.mapM fun alt => do
match alt with
@@ -114,7 +114,7 @@ partial def casesNatToMono (c: Cases) (_ : c.typeName == ``Nat) : ToMonoM Code :
eraseParams ps
if ctorName == ``Nat.succ then
let p := ps[0]!
let oneDecl mkLetDecl `one natType (.value (.natVal 1))
let oneDecl mkLetDecl `one natType (.lit (.nat 1))
let subOneDecl := { fvarId := p.fvarId, binderName := p.binderName, type := natType, value := .const ``Nat.sub [] #[.fvar c.discr, .fvar oneDecl.fvarId] }
modifyLCtx fun lctx => lctx.addLetDecl subOneDecl
return .alt ``Bool.false #[] (.let oneDecl (.let subOneDecl ( k.toMono)))
@@ -126,7 +126,7 @@ partial def casesNatToMono (c: Cases) (_ : c.typeName == ``Nat) : ToMonoM Code :
partial def casesIntToMono (c: Cases) (_ : c.typeName == ``Int) : ToMonoM Code := do
let resultType toMonoType c.resultType
let natType := mkConst ``Nat
let zeroNatDecl mkLetDecl `natZero natType (.value (.natVal 0))
let zeroNatDecl mkLetDecl `natZero natType (.lit (.nat 0))
let zeroIntDecl mkLetDecl `intZero (mkConst ``Int) (.const ``Int.ofNat [] #[.fvar zeroNatDecl.fvarId])
let isNegDecl mkLetDecl `isNeg (mkConst ``Bool) (.const ``Int.decLt [] #[.fvar c.discr, .fvar zeroIntDecl.fvarId])
let alts c.alts.mapM fun alt => do
@@ -137,7 +137,7 @@ partial def casesIntToMono (c: Cases) (_ : c.typeName == ``Int) : ToMonoM Code :
let p := ps[0]!
if ctorName == ``Int.negSucc then
let absDecl mkLetDecl `abs natType (.const ``Int.natAbs [] #[.fvar c.discr])
let oneDecl mkLetDecl `one natType (.value (.natVal 1))
let oneDecl mkLetDecl `one natType (.lit (.nat 1))
let subOneDecl := { fvarId := p.fvarId, binderName := p.binderName, type := natType, value := .const ``Nat.sub [] #[.fvar absDecl.fvarId, .fvar oneDecl.fvarId] }
modifyLCtx fun lctx => lctx.addLetDecl subOneDecl
return .alt ``Bool.true #[] (.let absDecl (.let oneDecl (.let subOneDecl ( k.toMono))))

View File

@@ -70,6 +70,91 @@ def useDiagnosticMsg : MessageData :=
else
pure s!"\n\nAdditional diagnostic information may be available using the `set_option {diagnostics.name} true` command."
/-- Name generator that creates user-accessible names. -/
structure DeclNameGenerator where
namePrefix : Name := .anonymous
-- We use a non-nil list instead of changing `namePrefix` as we want to distinguish between
-- numeric components in the original name (e.g. from macro scopes) and ones added by `mkChild`.
private idx : Nat := 1
private parentIdxs : List Nat := .nil
deriving Inhabited
namespace DeclNameGenerator
private def idxs (g : DeclNameGenerator) : List Nat :=
g.idx :: g.parentIdxs
def next (g : DeclNameGenerator) : DeclNameGenerator :=
{ g with idx := g.idx + 1 }
/--
Creates a user-accessible unique name of the following structure:
```
<name prefix>.<infix>_<numeric components>_...
```
Uniqueness is guaranteed for the current branch of elaboration. When entering parallelism and other
branching elaboration steps, `mkChild` must be used (automatically done in `wrapAsync*`).
-/
partial def mkUniqueName (env : Environment) (g : DeclNameGenerator) («infix» : Name) :
(Name × DeclNameGenerator) := Id.run do
-- `Name.append` does not allow macro scopes on both operands; as the result of this function is
-- unlikely to be referenced in a macro; the choice doesn't really matter.
let «infix» := if g.namePrefix.hasMacroScopes && infix.hasMacroScopes then infix.eraseMacroScopes else «infix»
let base := g.namePrefix ++ «infix»
let mut g := g
-- NOTE: We only check the current branch and rely on the documented invariant instead because we
-- do not want to block here and because it would not solve the issue for completely separated
-- threads of elaboration such as in Aesop's backtracking search.
while env.containsOnBranch (curr g base) do
g := g.next
return (curr g base, g)
where curr (g : DeclNameGenerator) (base : Name) : Name :=
g.idxs.foldr (fun i n => n.appendIndexAfter i) base
def mkChild (g : DeclNameGenerator) : DeclNameGenerator × DeclNameGenerator :=
({ g with parentIdxs := g.idx :: g.parentIdxs, idx := 1 },
{ g with idx := g.idx + 1 })
end DeclNameGenerator
class MonadDeclNameGenerator (m : Type Type) where
getDeclNGen : m DeclNameGenerator
setDeclNGen : DeclNameGenerator m Unit
export MonadDeclNameGenerator (getDeclNGen setDeclNGen)
instance [MonadLift m n] [MonadDeclNameGenerator m] : MonadDeclNameGenerator n where
getDeclNGen := liftM (getDeclNGen : m _)
setDeclNGen := fun ngen => liftM (setDeclNGen ngen : m _)
/--
Creates a new name for use as an auxiliary declaration that can be assumed to be globally unique.
Uniqueness is guaranteed for the current branch of elaboration. When entering parallelism and other
branching elaboration steps, `mkChild` must be used (automatically done in `wrapAsync*`).
-/
def mkAuxDeclName [Monad m] [MonadEnv m] [MonadDeclNameGenerator m] (kind : Name := `_aux) : m Name := do
let ngen getDeclNGen
let (n, ngen) := ngen.mkUniqueName ( getEnv) («infix» := kind)
setDeclNGen ngen
return n
/--
Adjusts the `namePrefix` of `getDeclNGen` to the given name and resets the nested counter.
-/
def withDeclNameForAuxNaming [Monad m] [MonadFinally m] [MonadDeclNameGenerator m]
(name : Name) (x : m α) : m α := do
let ngen getDeclNGen
-- do not reset index if prefix unchanged
if ngen.namePrefix != name then
try
setDeclNGen { namePrefix := name }
x
finally
setDeclNGen ngen
else
x
namespace Core
builtin_initialize registerTraceClass `Kernel
@@ -93,6 +178,11 @@ structure State where
nextMacroScope : MacroScope := firstFrontendMacroScope + 1
/-- Name generator for producing unique `FVarId`s, `MVarId`s, and `LMVarId`s -/
ngen : NameGenerator := {}
/--
Name generator for creating persistent auxiliary declarations. Separate from `ngen` to keep
numbers smaller and create user-accessible names.
-/
auxDeclNGen : DeclNameGenerator := {}
/-- Trace messages -/
traceState : TraceState := {}
/-- Cache for instantiating universe polymorphic declarations. -/
@@ -197,6 +287,10 @@ instance : MonadNameGenerator CoreM where
getNGen := return ( get).ngen
setNGen ngen := modify fun s => { s with ngen := ngen }
instance : MonadDeclNameGenerator CoreM where
getDeclNGen := return ( get).auxDeclNGen
setDeclNGen ngen := modify fun s => { s with auxDeclNGen := ngen }
instance : MonadRecDepth CoreM where
withRecDepth d x := withReader (fun ctx => { ctx with currRecDepth := d }) x
getRecDepth := return ( read).currRecDepth
@@ -220,8 +314,8 @@ instance : Elab.MonadInfoTree CoreM where
modifyInfoState f := modify fun s => { s with infoState := f s.infoState }
@[inline] def modifyCache (f : Cache Cache) : CoreM Unit :=
modify fun env, next, ngen, trace, cache, messages, infoState, snaps =>
env, next, ngen, trace, f cache, messages, infoState, snaps
modify fun env, next, ngen, auxDeclNGen, trace, cache, messages, infoState, snaps =>
env, next, ngen, auxDeclNGen, trace, f cache, messages, infoState, snaps
@[inline] def modifyInstLevelTypeCache (f : InstantiateLevelCache InstantiateLevelCache) : CoreM Unit :=
modifyCache fun c₁, c₂ => f c₁, c₂
@@ -435,7 +529,10 @@ def logSnapshotTask (task : Language.SnapshotTask Language.SnapshotTree) : CoreM
/-- Wraps the given action for use in `EIO.asTask` etc., discarding its final monadic state. -/
def wrapAsync {α : Type} (act : α CoreM β) (cancelTk? : Option IO.CancelToken) :
CoreM (α EIO Exception β) := do
let (childNGen, parentNGen) := ( getDeclNGen).mkChild
setDeclNGen parentNGen
let st get
let st := { st with auxDeclNGen := childNGen }
let ctx read
let ctx := { ctx with cancelTk? }
let heartbeats := ( IO.getNumHeartbeats) - ctx.initHeartbeats

View File

@@ -77,12 +77,9 @@ def lt (a b : JsonNumber) : Bool :=
else if ae > be then false
else am < bm
def ltProp : LT JsonNumber :=
instance ltProp : LT JsonNumber :=
fun a b => lt a b = true
instance : LT JsonNumber :=
ltProp
instance (a b : JsonNumber) : Decidable (a < b) :=
inferInstanceAs (Decidable (lt a b = true))

View File

@@ -137,9 +137,9 @@ def isInternalDetail : Name → Bool
| .num _ _ => true
| p => p.isInternalOrNum
where
/-- Check that a string begins with the given prefix, and then is only digit characters. -/
/-- Check that a string begins with the given prefix, and then is only digits/'_'. -/
matchPrefix (s : String) (pre : String) :=
s.startsWith pre && (s |>.drop pre.length |>.all Char.isDigit)
s.startsWith pre && (s |>.drop pre.length |>.all fun c => c.isDigit || c == '_')
/--
Checks whether the name is an implementation-detail hypothesis name.

View File

@@ -24,8 +24,10 @@ def elabAuxDef : CommandElab
let id := `_aux ++ ( getMainModule) ++ `_ ++ id
let id := String.intercalate "_" <| id.components.map (·.toString (escape := false))
let ns getCurrNamespace
-- make sure we only add a single component so that scoped works
let id mkAuxName (ns.mkStr id) 1
-- We use a new generator here because we want more control over the name; the default would
-- create a private name that then breaks the macro below. We assume that `aux_def` is not used
-- with the same arguments in parallel contexts.
let (id, _) := { namePrefix := ns : DeclNameGenerator }.mkUniqueName ( getEnv) («infix» := Name.mkSimple id)
let id := id.replacePrefix ns Name.anonymous -- TODO: replace with def _root_.id
elabCommand <|
`($[$doc?:docComment]? $[$attrs?:attributes]?

View File

@@ -9,6 +9,7 @@ import Lean.Elab.Term
import Lean.Elab.BindersUtil
import Lean.Elab.SyntheticMVars
import Lean.Elab.PreDefinition.TerminationHint
import Lean.Elab.Match
namespace Lean.Elab.Term
open Meta
@@ -553,6 +554,43 @@ def expandMatchAltsIntoMatch (ref : Syntax) (matchAlts : Syntax) (useExplicit :=
def expandMatchAltsIntoMatchTactic (ref : Syntax) (matchAlts : Syntax) : MacroM Syntax :=
withRef ref <| expandMatchAltsIntoMatchAux matchAlts (isTactic := true) (useExplicit := false) (getMatchAltsNumPatterns matchAlts) #[] #[]
/--
Sanity-checks the number of patterns in each alternative of a definition by pattern matching.
Specifically, verifies that all alternatives have the same number of patterns and that the number
of patterns is upper-bounded by the number of (dependent) arrows in the expected type.
Note: This function assumes that the number of patterns in the first alternative will be equal to
`numDiscrs` (since we use the first alternative to infer the arity of the generated matcher in
`getMatchAltsNumPatterns`).
-/
private def checkMatchAltPatternCounts (matchAlts : Syntax) (numDiscrs : Nat) (expectedType : Expr)
: MetaM Unit := do
let sepPats (pats : List Syntax) := MessageData.joinSep (pats.map toMessageData) ", "
let maxDiscrs? forallTelescopeReducing expectedType fun xs e =>
if e.getAppFn.isMVar then pure none else pure (some xs.size)
let matchAltViews := matchAlts[0].getArgs.filterMap getMatchAlt
let numPatternsStr (n : Nat) := s!"{n} {if n == 1 then "pattern" else "patterns"}"
if h : matchAltViews.size > 0 then
if let some maxDiscrs := maxDiscrs? then
if numDiscrs > maxDiscrs then
if maxDiscrs == 0 then
throwErrorAt matchAltViews[0].lhs m!"Cannot define a value of type{indentExpr expectedType}\n\
by pattern matching because it is not a function type"
else
throwErrorAt matchAltViews[0].lhs m!"Too many patterns in match alternative: \
At most {numPatternsStr maxDiscrs} expected in a definition of type {indentExpr expectedType}\n\
but found {numDiscrs}:{indentD <| sepPats matchAltViews[0].patterns.toList}"
-- Catch inconsistencies between pattern counts here so that we can report them as "inconsistent"
-- rather than as "too many" or "too few" (as the `match` elaborator does)
for view in matchAltViews do
let numPats := view.patterns.size
if numPats != numDiscrs then
let origPats := sepPats matchAltViews[0].patterns.toList
let pats := sepPats view.patterns.toList
throwErrorAt view.lhs m!"Inconsistent number of patterns in match alternatives: This \
alternative contains {numPatternsStr numPats}:{indentD pats}\n\
but a preceding alternative contains {numDiscrs}:{indentD origPats}"
/--
Similar to `expandMatchAltsIntoMatch`, but supports an optional `where` clause.
@@ -581,19 +619,21 @@ def expandMatchAltsIntoMatchTactic (ref : Syntax) (matchAlts : Syntax) : MacroM
| i, _ => ... f i + g i ...
```
-/
def expandMatchAltsWhereDecls (matchAltsWhereDecls : Syntax) : MacroM Syntax :=
def expandMatchAltsWhereDecls (matchAltsWhereDecls : Syntax) (expectedType : Expr) : TermElabM Syntax :=
let matchAlts := matchAltsWhereDecls[0]
-- matchAltsWhereDecls[1] is the termination hints, collected elsewhere
let whereDeclsOpt := matchAltsWhereDecls[2]
let rec loop (i : Nat) (discrs : Array Syntax) : MacroM Syntax :=
let rec loop (i : Nat) (discrs : Array Syntax) : TermElabM Syntax :=
match i with
| 0 => do
checkMatchAltPatternCounts matchAlts discrs.size expectedType
let matchStx `(match $[@$discrs:term],* with $matchAlts:matchAlts)
let matchStx clearInMatch matchStx discrs
if whereDeclsOpt.isNone then
return matchStx
else
expandWhereDeclsOpt whereDeclsOpt matchStx
liftMacroM do
let matchStx clearInMatch matchStx discrs
if whereDeclsOpt.isNone then
return matchStx
else
expandWhereDeclsOpt whereDeclsOpt matchStx
| n+1 => withFreshMacroScope do
let body loop n (discrs.push ( `(x)))
`(@fun x => $body)

View File

@@ -88,6 +88,7 @@ structure State where
nextMacroScope : Nat := firstFrontendMacroScope + 1
maxRecDepth : Nat
ngen : NameGenerator := {}
auxDeclNGen : DeclNameGenerator := {}
infoState : InfoState := {}
traceState : TraceState := {}
snapshotTasks : Array (Language.SnapshotTask Language.SnapshotTree) := #[]
@@ -158,6 +159,8 @@ def mkState (env : Environment) (messages : MessageLog := {}) (opts : Options :=
messages := messages
scopes := [{ header := "", opts := opts }]
maxRecDepth := maxRecDepth.get opts
-- Outside of declarations, fall back to a module-specific prefix
auxDeclNGen := { namePrefix := mkPrivateName env .anonymous }
}
/- Linters should be loadable as plugins, so store in a global IO ref instead of an attribute managed by the
@@ -203,6 +206,10 @@ instance : AddErrorMessageContext CommandElabM where
let msg addMacroStack msg ctx.macroStack
return (ref, msg)
instance : MonadDeclNameGenerator CommandElabM where
getDeclNGen := return ( get).auxDeclNGen
setDeclNGen ngen := modify fun s => { s with auxDeclNGen := ngen }
private def runCore (x : CoreM α) : CommandElabM α := do
let s get
let ctx read
@@ -225,6 +232,7 @@ private def runCore (x : CoreM α) : CommandElabM α := do
let x : EIO _ _ := x.run coreCtx {
env
ngen := s.ngen
auxDeclNGen := s.auxDeclNGen
nextMacroScope := s.nextMacroScope
infoState.enabled := s.infoState.enabled
traceState := s.traceState
@@ -235,6 +243,7 @@ private def runCore (x : CoreM α) : CommandElabM α := do
env := coreS.env
nextMacroScope := coreS.nextMacroScope
ngen := coreS.ngen
auxDeclNGen := coreS.auxDeclNGen
infoState.trees := s.infoState.trees.append coreS.infoState.trees
-- we assume substitution of `assignment` has already happened, but for lazy assignments we only
-- do it at the very end
@@ -312,7 +321,10 @@ def wrapAsync {α β : Type} (act : α → CommandElabM β) (cancelTk? : Option
CommandElabM (α EIO Exception β) := do
let ctx read
let ctx := { ctx with cancelTk? }
let (childNGen, parentNGen) := ( getDeclNGen).mkChild
setDeclNGen parentNGen
let st get
let st := { st with auxDeclNGen := childNGen }
return (act · |>.run ctx |>.run' st)
open Language in
@@ -811,6 +823,7 @@ private def liftCommandElabMCore (cmd : CommandElabM α) (throwOnError : Bool) :
nextMacroScope := s.nextMacroScope
maxRecDepth := ctx.maxRecDepth
ngen := s.ngen
auxDeclNGen := s.auxDeclNGen
scopes := [{ header := "", opts := ctx.options }]
infoState.enabled := s.infoState.enabled
}
@@ -818,6 +831,7 @@ private def liftCommandElabMCore (cmd : CommandElabM α) (throwOnError : Bool) :
env := commandState.env
nextMacroScope := commandState.nextMacroScope
ngen := commandState.ngen
auxDeclNGen := commandState.auxDeclNGen
traceState.traces := coreState.traceState.traces ++ commandState.traceState.traces
}
if throwOnError then

View File

@@ -138,7 +138,7 @@ private def reorderCtorArgs (ctorType : Expr) : MetaM Expr := do
else
let r mkForallFVars (bsPrefix ++ as) type
/- `r` already contains the resulting type.
To be able to produce more better error messages, we copy the first `bsPrefix.size` binder names from `C` to `r`.
To be able to produce better error messages, we copy the first `bsPrefix.size` binder names from `C` to `r`.
This is important when some of constructor parameters were inferred using the auto-bound implicit feature.
For example, in the following declaration.
```
@@ -178,7 +178,8 @@ private def elabCtors (indFVars : Array Expr) (params : Array Expr) (r : ElabHea
match ctorView.type? with
| none =>
if indFamily then
throwError "constructor resulting type must be specified in inductive family declaration"
throwError "Missing resulting type for constructor '{ctorView.declName}': \
Its resulting type must be specified because it is part of an inductive family declaration"
return mkAppN indFVar params
| some ctorType =>
let type Term.elabType ctorType
@@ -188,9 +189,9 @@ private def elabCtors (indFVars : Array Expr) (params : Array Expr) (r : ElabHea
let type checkParamOccs type
forallTelescopeReducing type fun _ resultingType => do
unless resultingType.getAppFn == indFVar do
throwError "unexpected constructor resulting type{indentExpr resultingType}"
throwUnexpectedResultingTypeMismatch resultingType indFVar ctorView.declName ctorType
unless ( isType resultingType) do
throwError "unexpected constructor resulting type, type expected{indentExpr resultingType}"
throwUnexpectedResultingTypeNotType resultingType ctorView.declName ctorType
return type
let type elabCtorType
Term.synthesizeSyntheticMVarsNoPostponing
@@ -229,23 +230,62 @@ private def elabCtors (indFVars : Array Expr) (params : Array Expr) (r : ElabHea
trace[Elab.inductive] "{ctorView.declName} : {type}"
return { name := ctorView.declName, type }
where
/--
Ensures that the arguments to recursive occurrences of the type family being defined match the
parameters from the inductive definition.
-/
checkParamOccs (ctorType : Expr) : MetaM Expr :=
let visit (e : Expr) : MetaM TransformStep := do
let visit (e : Expr) : StateT (List Expr) MetaM TransformStep := do
let f := e.getAppFn
if indFVars.contains f then
let mut args := e.getAppArgs
unless args.size params.size do
throwError "unexpected inductive type occurrence{indentExpr e}"
for h : i in [:params.size] do
let param := params[i]
-- Prefer throwing an "argument mismatch" error rather than a "missing parameter" one
for i in [:min args.size params.size] do
let param := params[i]!
let arg := args[i]!
unless ( isDefEq param arg) do
throwError "inductive datatype parameter mismatch{indentExpr arg}\nexpected{indentExpr param}"
let (arg, param) addPPExplicitToExposeDiff arg param
let msg := m!"Mismatched inductive type parameter in{indentExpr e}\nThe provided argument\
{indentExpr arg}\nis not definitionally equal to the expected parameter{indentExpr param}"
let noteMsg := m!"The value of parameter '{param}' must be fixed throughout the inductive \
declaration. Consider making this parameter an index if it must vary."
throwError msg ++ .note noteMsg
args := args.set! i param
unless args.size params.size do
let expected := mkAppN f params
let containingExprMsg := ( get).head?.map toMessageData |>.getD m!"<missing>"
let msg :=
m!"Missing parameter(s) in occurrence of inductive type: In the expression{indentD containingExprMsg}\n\
found{indentExpr e}\nbut expected all parameters to be specified:{indentExpr expected}"
let noteMsg :=
m!"All occurrences of an inductive type in the types of its constructors must specify its \
fixed parameters. Only indices can be omitted in a partial application of the type constructor."
throwError msg ++ .note noteMsg
return TransformStep.done (mkAppN f args)
else
modify fun es => e :: es
return .continue
transform ctorType (pre := visit)
let popContainingExpr (e : Expr) : StateT (List Expr) MetaM TransformStep := do
modify fun es => es.drop 1
return .done e
transform ctorType (pre := visit) (post := popContainingExpr) |>.run' [ctorType]
throwUnexpectedResultingTypeMismatch (resultingType indFVar : Expr) (declName : Name) (ctorType : Syntax) := do
let lazyAppMsg := MessageData.ofLazyM do
if let some fvarId := indFVar.fvarId? then
if let some decl := ( getLCtx).find? fvarId then
if ( whnfD decl.type).isForall then
return m!" an application of"
return m!""
throwErrorAt ctorType "Unexpected resulting type for constructor '{declName}': \
Expected{lazyAppMsg}{indentExpr indFVar}\nbut found{indentExpr resultingType}"
throwUnexpectedResultingTypeNotType (resultingType : Expr) (declName : Name) (ctorType : Syntax) := do
let lazyMsg := MessageData.ofLazyM do
let resultingTypeType inferType resultingType
return indentExpr resultingTypeType
throwErrorAt ctorType "Unexpected resulting type for constructor '{declName}': \
Expected a type, but found{indentExpr resultingType}\nof type{lazyMsg}"
@[builtin_inductive_elab Lean.Parser.Command.inductive, builtin_inductive_elab Lean.Parser.Command.classInductive]
def elabInductiveCommand : InductiveElabDescr where

View File

@@ -104,7 +104,7 @@ where
matchType := b.instantiate1 discr
discrs := discrs.push { expr := discr }
| _ =>
throwError "invalid motive provided to match-expression, function type with arity #{discrStxs.size} expected"
throwError "Invalid motive provided to match-expression: Function type with arity {discrStxs.size} expected"
return (discrs, isDep)
markIsDep (r : ElabMatchTypeAndDiscrsResult) :=
@@ -156,16 +156,20 @@ private def getMatchGeneralizing? : Syntax → Option Bool
| `(match (generalizing := false) $[$motive]? $_discrs,* with $_alts:matchAlt*) => some false
| _ => none
/-- Given `stx` a match-expression, return its alternatives. -/
private def getMatchAlts : Syntax Array MatchAltView
| `(match $[$gen]? $[$motive]? $_discrs,* with $alts:matchAlt*) =>
alts.filterMap fun alt => match alt with
| `(matchAltExpr| | $patterns,* => $rhs) => some {
/-- Given the `stx` of a single match alternative, return a corresponding `MatchAltView`. -/
def getMatchAlt : Syntax Option MatchAltView
| alt@`(matchAltExpr| | $patterns,* => $rhs) => some {
ref := alt,
patterns := patterns,
lhs := alt[1],
rhs := rhs
}
| _ => none
| _ => none
/-- Given `stx` a match-expression, return its alternatives. -/
def getMatchAlts : Syntax Array MatchAltView
| `(match $[$gen]? $[$motive]? $_discrs,* with $alts:matchAlt*) =>
alts.filterMap getMatchAlt
| _ => #[]
@[builtin_term_elab inaccessible] def elabInaccessible : TermElab := fun stx expectedType? => do
@@ -333,16 +337,31 @@ private partial def eraseIndices (type : Expr) : MetaM Expr := do
let params args[:info.numParams].toArray.mapM eraseIndices
let result := mkAppN type'.getAppFn params
let resultType inferType result
let (newIndices, _, _) forallMetaTelescopeReducing resultType (some (args.size - info.numParams))
let (newIndices, _, _) forallMetaTelescopeReducing resultType (some (args.size - info.numParams))
return mkAppN result newIndices
private def withPatternElabConfig (x : TermElabM α) : TermElabM α :=
withoutErrToSorry <| withReader (fun ctx => { ctx with inPattern := true }) <| x
private def elabPatterns (patternStxs : Array Syntax) (matchType : Expr) : ExceptT PatternElabException TermElabM (Array Expr × Expr) :=
open Meta.Match (throwIncorrectNumberOfPatternsAt logIncorrectNumberOfPatternsAt)
private def elabPatterns (patternStxs : Array Syntax) (numDiscrs : Nat) (matchType : Expr) : ExceptT PatternElabException TermElabM (Array Expr × Expr) :=
withReader (fun ctx => { ctx with implicitLambda := false }) do
let origMatchType := matchType
let mut patterns := #[]
let mut matchType := matchType
let mut patternStxs := patternStxs
if patternStxs.size < numDiscrs then
-- If there are too few patterns, log the error but continue elaborating with holes for the missing patterns
logIncorrectNumberOfPatternsAt ( getRef) "Not enough" numDiscrs patternStxs.size patternStxs.toList
let numHoles := numDiscrs - patternStxs.size
let mut extraStxs := Array.emptyWithCapacity numHoles
for _ in [:numHoles] do
extraStxs := extraStxs.push ( `(_))
patternStxs := patternStxs ++ extraStxs
else if patternStxs.size > numDiscrs then
throwIncorrectNumberOfPatternsAt ( getRef) "Too many" numDiscrs patternStxs.size patternStxs.toList
for h : idx in [:patternStxs.size] do
let patternStx := patternStxs[idx]
matchType whnf matchType
@@ -365,7 +384,7 @@ private def elabPatterns (patternStxs : Array Syntax) (matchType : Expr) : Excep
| none => throw ex
matchType := b.instantiate1 pattern
patterns := patterns.push pattern
| _ => throwError "unexpected match type"
| _ => throwError "Failed to elaborate match expression: Inferred {idx} discriminants, but more were found"
return (patterns, matchType)
open Meta.Match (Pattern Pattern.var Pattern.inaccessible Pattern.ctor Pattern.as Pattern.val Pattern.arrayLit AltLHS MatcherResult)
@@ -373,7 +392,7 @@ open Meta.Match (Pattern Pattern.var Pattern.inaccessible Pattern.ctor Pattern.a
namespace ToDepElimPattern
private def throwInvalidPattern (e : Expr) : MetaM α :=
throwError "invalid pattern {indentExpr e}"
throwError "Invalid pattern{indentExpr e}"
structure State where
patternVars : Array Expr := #[]
@@ -482,7 +501,7 @@ partial def normalize (e : Expr) : M Expr := do
let p := e.getArg! 2
let h := e.getArg! 3
unless x.consumeMData.isFVar && h.consumeMData.isFVar do
throwError "unexpected occurrence of auxiliary declaration 'namedPattern'"
throwError "Unexpected occurrence of auxiliary declaration 'namedPattern'"
addVar x
let p normalize p
addVar h
@@ -584,7 +603,7 @@ private partial def toPattern (e : Expr) : MetaM Pattern := do
let p toPattern <| e.getArg! 2
match e.getArg! 1, e.getArg! 3 with
| Expr.fvar x, Expr.fvar h => return Pattern.as x p h
| _, _ => throwError "unexpected occurrence of auxiliary declaration 'namedPattern'"
| _, _ => throwError "Unexpected occurrence of auxiliary declaration 'namedPattern'"
else if ( isMatchValue e) then
return Pattern.val ( normLitValue e)
else if e.isFVar then
@@ -682,7 +701,7 @@ partial def main (patternVarDecls : Array PatternVarDecl) (ps : Array Expr) (mat
for explicit in explicitPatternVars do
unless patternVars.any (· == mkFVar explicit) do
withInPattern do
throwError "invalid patterns, `{mkFVar explicit}` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching{indentD (MessageData.joinSep (ps.toList.map (MessageData.ofExpr .)) m!"\n\n")}"
throwError "Invalid pattern(s): `{mkFVar explicit}` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching:{indentD (MessageData.joinSep (ps.toList.map (MessageData.ofExpr .)) m!"\n\n")}"
let packed pack patternVars ps matchType
trace[Elab.match] "packed: {packed}"
withErasedFVars explicitPatternVars do
@@ -734,9 +753,9 @@ end ToDepElimPattern
def withDepElimPatterns (patternVarDecls : Array PatternVarDecl) (ps : Array Expr) (matchType : Expr) (k : Array LocalDecl Array Pattern Expr TermElabM α) : TermElabM α := do
ToDepElimPattern.main patternVarDecls ps matchType k
private def withElaboratedLHS {α} (ref : Syntax) (patternVarDecls : Array PatternVarDecl) (patternStxs : Array Syntax) (matchType : Expr)
private def withElaboratedLHS {α} (ref : Syntax) (patternVarDecls : Array PatternVarDecl) (patternStxs : Array Syntax) (lhsStx : Syntax) (numDiscrs : Nat) (matchType : Expr)
(k : AltLHS Expr TermElabM α) : ExceptT PatternElabException TermElabM α := do
let (patterns, matchType) withSynthesize <| elabPatterns patternStxs matchType
let (patterns, matchType) withSynthesize <| withRef lhsStx <| elabPatterns patternStxs numDiscrs matchType
id (α := TermElabM α) do
trace[Elab.match] "patterns: {patterns}"
withDepElimPatterns patternVarDecls patterns matchType fun localDecls patterns matchType => do
@@ -792,7 +811,7 @@ private def elabMatchAltView (discrs : Array Discr) (alt : MatchAltView) (matchT
let (patternVars, alt) collectPatternVars alt
trace[Elab.match] "patternVars: {patternVars}"
withPatternVars patternVars fun patternVarDecls => do
withElaboratedLHS alt.ref patternVarDecls alt.patterns matchType fun altLHS matchType =>
withElaboratedLHS alt.ref patternVarDecls alt.patterns alt.lhs discrs.size matchType fun altLHS matchType =>
withEqs discrs altLHS.patterns fun eqs =>
withLocalInstances altLHS.fvarDecls do
trace[Elab.match] "elabMatchAltView: {matchType}"
@@ -808,7 +827,7 @@ private def elabMatchAltView (discrs : Array Discr) (alt : MatchAltView) (matchT
let rhs elabTermEnsuringType alt.rhs matchType'
-- We use all approximations to ensure the auxiliary type is defeq to the original one.
unless ( fullApproxDefEq <| isDefEq matchType' matchType) do
throwError "type mismatch, alternative {← mkHasTypeButIsExpectedMsg matchType' matchType}"
throwError "Type mismatch: Alternative {← mkHasTypeButIsExpectedMsg matchType' matchType}"
let xs := altLHS.fvarDecls.toArray.map LocalDecl.toExpr ++ eqs
let rhs if xs.isEmpty then pure <| mkSimpleThunk rhs else mkLambdaFVars xs rhs
trace[Elab.match] "rhs: {rhs}"
@@ -1000,16 +1019,29 @@ register_builtin_option match.ignoreUnusedAlts : Bool := {
descr := "if true, do not generate error if an alternative is not used"
}
/--
Constructs a "redundant alternative" error message.
Optionally accepts the name of the constructor (e.g., for use in the `induction` tactic) and/or the
message-data representation of the alternative in question.
-/
def mkRedundantAlternativeMsg (altName? : Option Name) (altMsg? : Option MessageData) : MessageData :=
let altName := altName?.map (m!" '{toMessageData ·}'") |>.getD ""
let altMsg := altMsg?.map (indentD · ++ m!"\n") |>.getD " this pattern "
m!"Redundant alternative{altName}: Any expression matching{altMsg}will match one of the preceding alternatives"
def reportMatcherResultErrors (altLHSS : List AltLHS) (result : MatcherResult) : TermElabM Unit := do
unless result.counterExamples.isEmpty do
withHeadRefOnly <| logError m!"missing cases:\n{Meta.Match.counterExamplesToMessageData result.counterExamples}"
withHeadRefOnly <| logError m!"Missing cases:\n{Meta.Match.counterExamplesToMessageData result.counterExamples}"
return ()
unless match.ignoreUnusedAlts.get ( getOptions) || result.unusedAltIdxs.isEmpty do
let mut i := 0
for alt in altLHSS do
if result.unusedAltIdxs.contains i then
withRef alt.ref do
logError "redundant alternative"
withRef alt.ref do withInPattern do withExistingLocalDecls alt.fvarDecls do
let pats alt.patterns.mapM fun p => return toMessageData ( Pattern.toExpr p)
let pats := MessageData.joinSep pats ", "
logError (mkRedundantAlternativeMsg none pats)
i := i + 1
/--
@@ -1031,7 +1063,7 @@ private def elabMatchAux (generalizing? : Option Bool) (discrStxs : Array Syntax
let mut generalizing? := generalizing?
if !matchOptMotive.isNone then
if generalizing? == some true then
throwError "the '(generalizing := true)' parameter is not supported when the 'match' motive is explicitly provided"
throwError "The '(generalizing := true)' parameter is not supported when the 'match' motive is explicitly provided"
generalizing? := some false
let (discrs, matchType, altLHSS, isDep, rhss) commitIfDidNotPostpone do
let discrs, matchType, isDep, altViews elabMatchTypeAndDiscrs discrStxs matchOptMotive altViews expectedType
@@ -1086,12 +1118,12 @@ private def elabMatchAux (generalizing? : Option Bool) (discrStxs : Array Syntax
withExistingLocalDecls altLHS.fvarDecls do
runPendingTacticsAt d.type
if ( instantiateMVars d.type).hasExprMVar then
throwMVarError m!"invalid match-expression, type of pattern variable '{d.toExpr}' contains metavariables{indentExpr d.type}"
throwMVarError m!"Invalid match expression: The type of pattern variable '{d.toExpr}' contains metavariables:{indentExpr d.type}"
for p in altLHS.patterns do
if ( Match.instantiatePatternMVars p).hasExprMVar then
tryPostpone
withExistingLocalDecls altLHS.fvarDecls do
throwMVarError m!"invalid match-expression, pattern contains metavariables{indentExpr (← p.toExpr)}"
throwMVarError m!"Invalid match expression: This pattern contains metavariables:{indentExpr (← p.toExpr)}"
pure altLHS
return (discrs, matchType, altLHSS, isDep, rhss)
if let some r if isDep then pure none else isMatchUnit? altLHSS rhss then

View File

@@ -20,6 +20,7 @@ def «match» := leading_parser:leadPrec "match " >> sepBy1 matchDiscr ", " >> o
structure MatchAltView where
ref : Syntax
patterns : Array Syntax
lhs : Syntax
rhs : Syntax
deriving Inhabited

View File

@@ -353,17 +353,17 @@ def declVal := declValSimple <|> declValEqns <|> Term.whereDecls
The `Termination.suffix` is ignored here, and extracted in `declValToTerminationHint`.
-/
private def declValToTerm (declVal : Syntax) : MacroM Syntax := withRef declVal do
private def declValToTerm (declVal : Syntax) (expectedType : Expr) : TermElabM Syntax := withRef declVal do
if declVal.isOfKind ``Parser.Command.declValSimple then
expandWhereDeclsOpt declVal[3] declVal[1]
liftMacroM <| expandWhereDeclsOpt declVal[3] declVal[1]
else if declVal.isOfKind ``Parser.Command.declValEqns then
expandMatchAltsWhereDecls declVal[0]
expandMatchAltsWhereDecls declVal[0] expectedType
else if declVal.isOfKind ``Parser.Command.whereStructInst then
expandWhereStructInst declVal
liftMacroM <| expandWhereStructInst declVal
else if declVal.isMissing then
Macro.throwErrorAt declVal "declaration body is missing"
throwErrorAt declVal "declaration body is missing"
else
Macro.throwErrorAt declVal "unexpected declaration body"
throwErrorAt declVal "unexpected declaration body"
/-- Elaborates the termination hints in a `declVal` syntax. -/
private def declValToTerminationHint (declVal : Syntax) : TermElabM TerminationHints :=
@@ -464,7 +464,7 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
withReuseContext header.value do
withTraceNode `Elab.definition.value (fun _ => pure header.declName) do
withDeclName header.declName <| withLevelNames header.levelNames do
let valStx liftMacroM <| declValToTerm header.value
let valStx declValToTerm header.value header.type
(if header.kind.isTheorem && !deprecated.oldSectionVars.get ( getOptions) then withHeaderSecVars vars sc #[header] else fun x => x #[]) fun vars => do
forallBoundedTelescope header.type header.numParams fun xs type => do
-- Add new info nodes for new fvars. The server will detect all fvars of a binder by the binder's source location.
@@ -1129,7 +1129,11 @@ where
-- now start new thread for body elaboration, then nested thread for kernel checking
let cancelTk IO.CancelToken.new
let act wrapAsyncAsSnapshot (desc := s!"elaborating proof of {declId.declName}")
let act
-- NOTE: We must set the decl name before going async to ensure that the `auxDeclNGen` is
-- forked correctly.
withDeclName header.declName do
wrapAsyncAsSnapshot (desc := s!"elaborating proof of {declId.declName}")
(cancelTk? := cancelTk) fun _ => do profileitM Exception "elaboration" ( getOptions) do
setEnv async.asyncEnv
try

View File

@@ -219,7 +219,7 @@ private def checkUnsafe (rs : Array PreElabHeaderResult) : TermElabM Unit := do
let isUnsafe := rs[0]!.view.modifiers.isUnsafe
for r in rs do
unless r.view.modifiers.isUnsafe == isUnsafe do
throwErrorAt r.view.ref "invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes"
throwErrorAt r.view.ref "invalid inductive type, cannot mix unsafe and safe declarations in mutually inductive datatypes"
private def checkClass (rs : Array PreElabHeaderResult) : TermElabM Unit := do
if rs.size > 1 then

View File

@@ -16,7 +16,7 @@ abbrev PatternVar := Syntax -- TODO: should be `Ident`
/-!
Patterns define new local variables.
This module collect them and preprocess `_` occurring in patterns.
This module collects them and preprocesses `_` occurring in patterns.
Recall that an `_` may represent anonymous variables or inaccessible terms
that are implied by typing constraints. Thus, we represent them with fresh named holes `?x`.
After we elaborate the pattern, if the metavariable remains unassigned, we transform it into
@@ -49,7 +49,7 @@ abbrev M := StateRefT State TermElabM
private def throwCtorExpected {α} (ident : Option Syntax) : M α := do
let message : MessageData :=
"invalid pattern, constructor or constant marked with '[match_pattern]' expected"
"Invalid pattern: Expected a constructor or constant marked with `[match_pattern]`"
let some idStx := ident | throwError message
let name := idStx.getId
if let .anonymous := name then throwError message
@@ -64,7 +64,7 @@ private def throwCtorExpected {α} (ident : Option Syntax) : M α := do
if candidates.size = 0 then
throwError message
else if h : candidates.size = 1 then
throwError message ++ m!"\n\nSuggestion: '{candidates[0]}' is similar"
throwError message ++ .hint' m!"'{candidates[0]}' is similar"
else
let sorted := candidates.qsort (·.toString < ·.toString)
let diff :=
@@ -73,28 +73,28 @@ private def throwCtorExpected {α} (ident : Option Syntax) : M α := do
let suggestions : MessageData := .group <|
.joinSep ((sorted.extract 0 10 |>.toList |>.map (showName env)) ++ diff)
("," ++ Format.line)
throwError message ++ .group ("\n\nSuggestions:" ++ .nestD (Format.line ++ suggestions))
throwError message ++ .group (.hint' ("These are similar:" ++ .nestD (Format.line ++ suggestions)))
where
-- Create some `MessageData` for a name that shows it without an `@`, but with the metadata that
-- makes infoview hovers and the like work. This technique only works because the names are known
-- to be global constants, so we don't need the local context.
showName (env : Environment) (n : Name) : MessageData :=
let params :=
env.constants.find?' n |>.map (·.levelParams.map Level.param) |>.getD []
.ofFormatWithInfos {
fmt := "'" ++ .tag 0 (format n) ++ "'",
infos :=
.fromList [(0, .ofTermInfo {
lctx := .empty,
expr := .const n params,
stx := .ident .none (toString n).toSubstring n [.decl n []],
elaborator := `Delab,
expectedType? := none
})] _
}
let params :=
env.constants.find?' n |>.map (·.levelParams.map Level.param) |>.getD []
.ofFormatWithInfos {
fmt := "'" ++ .tag 0 (format n) ++ "'",
infos :=
.fromList [(0, .ofTermInfo {
lctx := .empty,
expr := .const n params,
stx := .ident .none (toString n).toSubstring n [.decl n []],
elaborator := `Delab,
expectedType? := none
})] _
}
private def throwInvalidPattern {α} : M α :=
throwError "invalid pattern"
throwError "Invalid pattern"
/-!
An application in a pattern can be
@@ -118,6 +118,26 @@ structure Context where
newArgs : Array Term := #[]
deriving Inhabited
private def throwInvalidNamedArgs [Monad m] [MonadError m]
(namedArgs : Array NamedArg) (funId : Term) : m α :=
let names := (namedArgs.map fun narg => m!"'{narg.name}'").toList
let nameStr := if names.length == 1 then "name" else "names"
throwError m!"Invalid argument {nameStr} {.andList names} for function '{funId}'"
private def throwWrongArgCount (ctx : Context) (tooMany : Bool) : M α := do
if !ctx.namedArgs.isEmpty then
throwInvalidNamedArgs ctx.namedArgs ctx.funId
let numExpectedArgs :=
(if ctx.explicit then ctx.paramDecls else ctx.paramDecls.filter (·.2.isExplicit)).size
let argKind := if ctx.explicit then "" else "explicit "
let argWord := if numExpectedArgs == 1 then "argument" else "arguments"
let discrepancyKind := if tooMany then "Too many" else "Not enough"
let mut msg := m!"Invalid pattern: {discrepancyKind} arguments to '{ctx.funId}'; \
expected {numExpectedArgs} {argKind}{argWord}"
if !tooMany then
msg := msg ++ .hint' "To ignore all remaining arguments, use the ellipsis notation `..`"
throwError msg
private def isDone (ctx : Context) : Bool :=
ctx.paramDeclIdx ctx.paramDecls.size
@@ -125,8 +145,10 @@ private def finalize (ctx : Context) : M Syntax := do
if ctx.namedArgs.isEmpty && ctx.args.isEmpty then
let fStx `(@$(ctx.funId):ident)
return Syntax.mkApp fStx ctx.newArgs
else if ctx.args.isEmpty then
throwInvalidNamedArgs ctx.namedArgs ctx.funId
else
throwError "too many arguments"
throwWrongArgCount ctx true
private def isNextArgAccessible (ctx : Context) : Bool :=
let i := ctx.paramDeclIdx
@@ -147,12 +169,12 @@ private def getNextParam (ctx : Context) : (Name × BinderInfo) × Context :=
private def processVar (idStx : Syntax) : M Syntax := do
unless idStx.isIdent do
throwErrorAt idStx "identifier expected"
throwErrorAt idStx "Invalid pattern variable: Identifier expected, but found{indentD idStx}"
let id := idStx.getId
unless id.eraseMacroScopes.isAtomic do
throwError "invalid pattern variable, must be atomic"
throwError "Invalid pattern variable: Variable name must be atomic, but '{id}' has multiple components"
if ( get).found.contains id then
throwError "invalid pattern, variable '{id}' occurred more than once"
throwError "Invalid pattern variable: Variable name '{id}' was already used"
modify fun s => { s with vars := s.vars.push idStx, found := s.found.insert id }
return idStx
@@ -175,6 +197,7 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
let elems stx[1].getArgs.mapSepElemsM collect
return stx.setArg 1 <| mkNullNode elems
else if k == ``Lean.Parser.Term.dotIdent then
-- TODO: validate that `stx` corresponds to a valid constructor or match pattern
return stx
else if k == ``Lean.Parser.Term.hole then
`(.( $stx ))
@@ -187,6 +210,8 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
return stx.setArg 1 t
else if k == ``Lean.Parser.Term.explicitUniv then
processCtor stx[0]
else if k == ``Lean.Parser.Term.explicit then
processCtor stx
else if k == ``Lean.Parser.Term.namedPattern then
/- Recall that
```
@@ -254,13 +279,13 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
set stateSaved
argsNew := argsNew.push ( collect arg)
unless samePatternsVariables stateSaved.vars.size stateNew ( get) do
throwError "invalid pattern, overloaded notation is only allowed when all alternative have the same set of pattern variables"
throwError "Invalid pattern: Overloaded notation is only allowed when all alternatives have the same set of pattern variables"
set stateNew
return mkNode choiceKind argsNew
else match stx with
| `({ $[$srcs?,* with]? $fields,* $[..%$ell?]? $[: $ty?]? }) =>
if let some srcs := srcs? then
throwErrorAt (mkNullNode srcs) "invalid struct instance pattern, 'with' is not allowed in patterns"
throwErrorAt (mkNullNode srcs) "Invalid struct instance pattern: `with` is not allowed in patterns"
let fields fields.getElems.mapM fun
| `(Parser.Term.structInstField| $lval:structInstLVal := $val) => do
let newVal collect val
@@ -316,7 +341,7 @@ where
if ctx.ellipsis then
pushNewArg accessible ctx (Arg.stx ( `(_)))
else
throwError "explicit parameter is missing, unused named arguments {ctx.namedArgs.map fun narg => narg.name}"
throwWrongArgCount ctx false
| arg::args =>
pushNewArg accessible { ctx with args := args } arg
@@ -351,7 +376,8 @@ where
let (fId, explicit) match f with
| `($fId:ident) => pure (fId, false)
| `(@$fId:ident) => pure (fId, true)
| _ => throwError "identifier expected"
| _ =>
throwError "Invalid pattern: Expected an identifier in function position, but found{indentD f}"
let some (Expr.const fName _) resolveId? fId "pattern" (withInfo := true) | throwCtorExpected (some fId)
let fInfo getConstInfo fName
let paramDecls forallTelescopeReducing fInfo.type fun xs _ => xs.mapM fun x => do

View File

@@ -91,7 +91,9 @@ def abstractNestedProofs (preDef : PreDefinition) (cache := true) : MetaM PreDef
if preDef.kind.isTheorem || preDef.kind.isExample then
pure preDef
else do
let value Meta.abstractNestedProofs (cache := cache) preDef.declName preDef.value
let value
withDeclNameForAuxNaming preDef.declName do
Meta.abstractNestedProofs (cache := cache) preDef.value
pure { preDef with value := value }
/-- Auxiliary method for (temporarily) adding pre definition as an axiom -/

View File

@@ -172,20 +172,19 @@ end FixedParams
open Lean Meta FixedParams
def getParamRevDeps (preDefs : Array PreDefinition) : MetaM (Array (Array (Array Nat))) := do
preDefs.mapM fun preDef =>
lambdaTelescope preDef.value (cleanupAnnotations := true) fun xs _ => do
let mut revDeps := #[]
for h : i in [:xs.size] do
let mut deps := #[]
for h : j in [i+1:xs.size] do
if ( dependsOn ( inferType xs[j]) xs[i].fvarId!) then
deps := deps.push j
revDeps := revDeps.push deps
pure revDeps
def getParamRevDeps (value : Expr) : MetaM (Array (Array Nat)) := do
lambdaTelescope value (cleanupAnnotations := true) fun xs _ => do
let mut revDeps := #[]
for h : i in [:xs.size] do
let mut deps := #[]
for h : j in [i+1:xs.size] do
if ( dependsOn ( inferType xs[j]) xs[i].fvarId!) then
deps := deps.push j
revDeps := revDeps.push deps
pure revDeps
def getFixedParamsInfo (preDefs : Array PreDefinition) : MetaM FixedParams.Info := do
let revDeps getParamRevDeps preDefs
let revDeps preDefs.mapM (getParamRevDeps ·.value)
let arities := revDeps.map (·.size)
let ref IO.mkRef (Info.init revDeps)

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