mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-18 10:54:09 +00:00
Compare commits
37 Commits
array_30
...
unattach_a
| Author | SHA1 | Date | |
|---|---|---|---|
|
e095aa340b | ||
|
|
721617d734 | ||
|
|
532c782e20 | ||
|
|
683fa8a794 | ||
|
|
9322d8d639 | ||
|
|
9dcd2ad2a3 | ||
|
|
e3811fd838 | ||
|
|
867e67b9f3 | ||
|
|
6cd80c28b7 | ||
|
|
f202469c8a | ||
|
|
e417a2331c | ||
|
|
5eb6c67a78 | ||
|
|
499c58796b | ||
|
|
863e9c073b | ||
|
|
60096e7d15 | ||
|
|
e90c3cf15a | ||
|
|
d4195c2605 | ||
|
|
4932dbc65d | ||
|
|
d0ee9d0127 | ||
|
|
3e2bca7309 | ||
|
|
ddec5336e5 | ||
|
|
37baa89d9b | ||
|
|
949feb25a4 | ||
|
|
bfb73c4a5e | ||
|
|
b22dee8816 | ||
|
|
4771741fa2 | ||
|
|
ffb4c5becf | ||
|
|
d3f7ed434b | ||
|
|
6bd0d9d73b | ||
|
|
db79d9e5ce | ||
|
|
5e8718dff9 | ||
|
|
4f2c4c7bd1 | ||
|
|
56ba39d68a | ||
|
|
1fca66b8c9 | ||
|
|
36c29bee31 | ||
|
|
cf14178929 | ||
|
|
a4dfa83af5 |
314
RELEASES.md
314
RELEASES.md
@@ -10,7 +10,317 @@ of each version.
|
||||
|
||||
v4.12.0
|
||||
----------
|
||||
Development in progress.
|
||||
|
||||
### Language features, tactics, and metaprograms
|
||||
|
||||
* `bv_decide` tactic. This release introduces a new tactic for proving goals involving `BitVec` and `Bool`. It reduces the goal to a SAT instance that is refuted by an external solver, and the resulting LRAT proof is checked in Lean. This is used to synthesize a proof of the goal by reflection. As this process uses verified algorithms, proofs generated by this tactic use `Lean.ofReduceBool`, so this tactic includes the Lean compiler as part of the trusted code base. The external solver CaDiCaL is included with Lean and does not need to be installed separately to make use of `bv_decide`.
|
||||
|
||||
For example, we can use `bv_decide` to verify that a bit twiddling formula leaves at most one bit set:
|
||||
```lean
|
||||
def popcount (x : BitVec 64) : BitVec 64 :=
|
||||
let rec go (x pop : BitVec 64) : Nat → BitVec 64
|
||||
| 0 => pop
|
||||
| n + 1 => go (x >>> 2) (pop + (x &&& 1)) n
|
||||
go x 0 64
|
||||
|
||||
example (x : BitVec 64) : popcount ((x &&& (x - 1)) ^^^ x) ≤ 1 := by
|
||||
simp only [popcount, popcount.go]
|
||||
bv_decide
|
||||
```
|
||||
When the external solver fails to refute the SAT instance generated by `bv_decide`, it can report a counterexample:
|
||||
```lean
|
||||
/--
|
||||
error: The prover found a counterexample, consider the following assignment:
|
||||
x = 0xffffffffffffffff#64
|
||||
-/
|
||||
#guard_msgs in
|
||||
example (x : BitVec 64) : x < x + 1 := by
|
||||
bv_decide
|
||||
```
|
||||
|
||||
See `Lean.Elab.Tactic.BVDecide` for a more detailed overview, and look in `tests/lean/run/bv_*` for examples.
|
||||
|
||||
[#5013](https://github.com/leanprover/lean4/pull/5013), [#5074](https://github.com/leanprover/lean4/pull/5074), [#5100](https://github.com/leanprover/lean4/pull/5100), [#5113](https://github.com/leanprover/lean4/pull/5113), [#5137](https://github.com/leanprover/lean4/pull/5137), [#5203](https://github.com/leanprover/lean4/pull/5203), [#5212](https://github.com/leanprover/lean4/pull/5212), [#5220](https://github.com/leanprover/lean4/pull/5220).
|
||||
|
||||
* `simp` tactic
|
||||
* [#4988](https://github.com/leanprover/lean4/pull/4988) fixes a panic in the `reducePow` simproc.
|
||||
* [#5071](https://github.com/leanprover/lean4/pull/5071) exposes the `index` option to the `dsimp` tactic, introduced to `simp` in [#4202](https://github.com/leanprover/lean4/pull/4202).
|
||||
* [#5159](https://github.com/leanprover/lean4/pull/5159) fixes a panic at `Fin.isValue` simproc.
|
||||
* [#5167](https://github.com/leanprover/lean4/pull/5167) and [#5175](https://github.com/leanprover/lean4/pull/5175) rename the `simpCtorEq` simproc to `reduceCtorEq` and makes it optional. (See breaking changes.)
|
||||
* [#5187](https://github.com/leanprover/lean4/pull/5187) ensures `reduceCtorEq` is enabled in the `norm_cast` tactic.
|
||||
* [#5073](https://github.com/leanprover/lean4/pull/5073) modifies the simp debug trace messages to tag with "dpre" and "dpost" instead of "pre" and "post" when in definitional rewrite mode. [#5054](https://github.com/leanprover/lean4/pull/5054) explains the `reduce` steps for `trace.Debug.Meta.Tactic.simp` trace messages.
|
||||
* `ext` tactic
|
||||
* [#4996](https://github.com/leanprover/lean4/pull/4996) reduces default maximum iteration depth from 1000000 to 100.
|
||||
* `induction` tactic
|
||||
* [#5117](https://github.com/leanprover/lean4/pull/5117) fixes a bug where `let` bindings in minor premises wouldn't be counted correctly.
|
||||
|
||||
* `omega` tactic
|
||||
* [#5157](https://github.com/leanprover/lean4/pull/5157) fixes a panic.
|
||||
|
||||
* `conv` tactic
|
||||
* [#5149](https://github.com/leanprover/lean4/pull/5149) improves `arg n` to handle subsingleton instance arguments.
|
||||
|
||||
* [#5044](https://github.com/leanprover/lean4/pull/5044) upstreams the `#time` command.
|
||||
* [#5079](https://github.com/leanprover/lean4/pull/5079) makes `#check` and `#reduce` typecheck the elaborated terms.
|
||||
|
||||
* **Incrementality**
|
||||
* [#4974](https://github.com/leanprover/lean4/pull/4974) fixes regression where we would not interrupt elaboration of previous document versions.
|
||||
* [#5004](https://github.com/leanprover/lean4/pull/5004) fixes a performance regression.
|
||||
* [#5001](https://github.com/leanprover/lean4/pull/5001) disables incremental body elaboration in presence of `where` clauses in declarations.
|
||||
* [#5018](https://github.com/leanprover/lean4/pull/5018) enables infotrees on the command line for ilean generation.
|
||||
* [#5040](https://github.com/leanprover/lean4/pull/5040) and [#5056](https://github.com/leanprover/lean4/pull/5056) improve performance of info trees.
|
||||
* [#5090](https://github.com/leanprover/lean4/pull/5090) disables incrementality in the `case .. | ..` tactic.
|
||||
* [#5312](https://github.com/leanprover/lean4/pull/5312) fixes a bug where changing whitespace after the module header could break subsequent commands.
|
||||
|
||||
* **Definitions**
|
||||
* [#5016](https://github.com/leanprover/lean4/pull/5016) and [#5066](https://github.com/leanprover/lean4/pull/5066) add `clean_wf` tactic to clean up tactic state in `decreasing_by`. This can be disabled with `set_option debug.rawDecreasingByGoal false`.
|
||||
* [#5055](https://github.com/leanprover/lean4/pull/5055) unifies equational theorems between structural and well-founded recursion.
|
||||
* [#5041](https://github.com/leanprover/lean4/pull/5041) allows mutually recursive functions to use different parameter names among the “fixed parameter prefix”
|
||||
* [#4154](https://github.com/leanprover/lean4/pull/4154) and [#5109](https://github.com/leanprover/lean4/pull/5109) add fine-grained equational lemmas for non-recursive functions. See breaking changes.
|
||||
* [#5129](https://github.com/leanprover/lean4/pull/5129) unifies equation lemmas for recursive and non-recursive definitions. The `backward.eqns.deepRecursiveSplit` option can be set to `false` to get the old behavior. See breaking changes.
|
||||
* [#5141](https://github.com/leanprover/lean4/pull/5141) adds `f.eq_unfold` lemmas. Now Lean produces the following zoo of rewrite rules:
|
||||
```
|
||||
Option.map.eq_1 : Option.map f none = none
|
||||
Option.map.eq_2 : Option.map f (some x) = some (f x)
|
||||
Option.map.eq_def : Option.map f p = match o with | none => none | (some x) => some (f x)
|
||||
Option.map.eq_unfold : Option.map = fun f p => match o with | none => none | (some x) => some (f x)
|
||||
```
|
||||
The `f.eq_unfold` variant is especially useful to rewrite with `rw` under binders.
|
||||
* [#5136](https://github.com/leanprover/lean4/pull/5136) fixes bugs in recursion over predicates.
|
||||
|
||||
* **Variable inclusion**
|
||||
* [#5206](https://github.com/leanprover/lean4/pull/5206) documents that `include` currently only applies to theorems.
|
||||
|
||||
* **Elaboration**
|
||||
* [#4926](https://github.com/leanprover/lean4/pull/4926) fixes a bug where autoparam errors were associated to an incorrect source position.
|
||||
* [#4833](https://github.com/leanprover/lean4/pull/4833) fixes an issue where cdot anonymous functions (e.g. `(· + ·)`) would not handle ambiguous notation correctly. Numbers the parameters, making this example expand as `fun x1 x2 => x1 + x2` rather than `fun x x_1 => x + x_1`.
|
||||
* [#5037](https://github.com/leanprover/lean4/pull/5037) improves strength of the tactic that proves array indexing is in bounds.
|
||||
* [#5119](https://github.com/leanprover/lean4/pull/5119) fixes a bug in the tactic that proves indexing is in bounds where it could loop in the presence of mvars.
|
||||
* [#5072](https://github.com/leanprover/lean4/pull/5072) makes the structure type clickable in "not a field of structure" errors for structure instance notation.
|
||||
* [#4717](https://github.com/leanprover/lean4/pull/4717) fixes a bug where mutual `inductive` commands could create terms that the kernel rejects.
|
||||
* [#5142](https://github.com/leanprover/lean4/pull/5142) fixes a bug where `variable` could fail when mixing binder updates and declarations.
|
||||
|
||||
* **Other fixes or improvements**
|
||||
* [#5118](https://github.com/leanprover/lean4/pull/5118) changes the definition of the `syntheticHole` parser so that hovering over `_` in `?_` gives the docstring for synthetic holes.
|
||||
* [#5173](https://github.com/leanprover/lean4/pull/5173) uses the emoji variant selector for ✅️,❌️,💥️ in messages, improving fonts selection.
|
||||
* [#5183](https://github.com/leanprover/lean4/pull/5183) fixes a bug in `rename_i` where implementation detail hypotheses could be renamed.
|
||||
|
||||
### Language server, widgets, and IDE extensions
|
||||
|
||||
* [#4821](https://github.com/leanprover/lean4/pull/4821) resolves two language server bugs that especially affect Windows users. (1) Editing the header could result in the watchdog not correctly restarting the file worker, which would lead to the file seemingly being processed forever. (2) On an especially slow Windows machine, we found that starting the language server would sometimes not succeed at all. This PR also resolves an issue where we would not correctly emit messages that we received while the file worker is being restarted to the corresponding file worker after the restart.
|
||||
* [#5006](https://github.com/leanprover/lean4/pull/5006) updates the user widget manual.
|
||||
* [#5193](https://github.com/leanprover/lean4/pull/5193) updates the quickstart guide with the new display name for the Lean 4 extension ("Lean 4").
|
||||
* [#5185](https://github.com/leanprover/lean4/pull/5185) fixes a bug where over time "import out of date" messages would accumulate.
|
||||
* [#4900](https://github.com/leanprover/lean4/pull/4900) improves ilean loading performance by about a factor of two. Optimizes the JSON parser and the conversion from JSON to Lean data structures; see PR description for details.
|
||||
* **Other fixes or improvements**
|
||||
* [#5031](https://github.com/leanprover/lean4/pull/5031) localizes an instance in `Lsp.Diagnostics`.
|
||||
|
||||
### Pretty printing
|
||||
|
||||
* [#4976](https://github.com/leanprover/lean4/pull/4976) introduces `@[app_delab]`, a macro for creating delaborators for particular constants. The `@[app_delab ident]` syntax resolves `ident` to its constant name `name` and then expands to `@[delab app.name]`.
|
||||
* [#4982](https://github.com/leanprover/lean4/pull/4982) fixes a bug where the pretty printer assumed structure projections were type correct (such terms can appear in type mismatch errors). Improves hoverability of `#print` output for structures.
|
||||
* [#5218](https://github.com/leanprover/lean4/pull/5218) and [#5239](https://github.com/leanprover/lean4/pull/5239) add `pp.exprSizes` debugging option. When true, each pretty printed expression is prefixed with `[size a/b/c]`, where `a` is the size without sharing, `b` is the actual size, and `c` is the size with the maximum possible sharing.
|
||||
|
||||
### Library
|
||||
|
||||
* [#5020](https://github.com/leanprover/lean4/pull/5020) swaps the parameters to `Membership.mem`. A purpose of this change is to make set-like `CoeSort` coercions to refer to the eta-expanded function `fun x => Membership.mem s x`, which can reduce in many computations. Another is that having the `s` argument first leads to better discrimination tree keys. (See breaking changes.)
|
||||
* `Array`
|
||||
* [#4970](https://github.com/leanprover/lean4/pull/4970) adds `@[ext]` attribute to `Array.ext`.
|
||||
* [#4957](https://github.com/leanprover/lean4/pull/4957) deprecates `Array.get_modify`.
|
||||
* `List`
|
||||
* [#4995](https://github.com/leanprover/lean4/pull/4995) upstreams `List.findIdx` lemmas.
|
||||
* [#5029](https://github.com/leanprover/lean4/pull/5029), [#5048](https://github.com/leanprover/lean4/pull/5048) and [#5132](https://github.com/leanprover/lean4/pull/5132) add `List.Sublist` lemmas, some upstreamed. [#5077](https://github.com/leanprover/lean4/pull/5077) fixes implicitness in refl/rfl lemma binders. add `List.Sublist` theorems.
|
||||
* [#5047](https://github.com/leanprover/lean4/pull/5047) upstreams `List.Pairwise` lemmas.
|
||||
* [#5053](https://github.com/leanprover/lean4/pull/5053), [#5124](https://github.com/leanprover/lean4/pull/5124), and [#5161](https://github.com/leanprover/lean4/pull/5161) add `List.find?/findSome?/findIdx?` theorems.
|
||||
* [#5039](https://github.com/leanprover/lean4/pull/5039) adds `List.foldlRecOn` and `List.foldrRecOn` recursion principles to prove things about `List.foldl` and `List.foldr`.
|
||||
* [#5069](https://github.com/leanprover/lean4/pull/5069) upstreams `List.Perm`.
|
||||
* [#5092](https://github.com/leanprover/lean4/pull/5092) and [#5107](https://github.com/leanprover/lean4/pull/5107) add `List.mergeSort` and a fast `@[csimp]` implementation.
|
||||
* [#5103](https://github.com/leanprover/lean4/pull/5103) makes the simp lemmas for `List.subset` more aggressive.
|
||||
* [#5106](https://github.com/leanprover/lean4/pull/5106) changes the statement of `List.getLast?_cons`.
|
||||
* [#5123](https://github.com/leanprover/lean4/pull/5123) and [#5158](https://github.com/leanprover/lean4/pull/5158) add `List.range` and `List.iota` lemmas.
|
||||
* [#5130](https://github.com/leanprover/lean4/pull/5130) adds `List.join` lemmas.
|
||||
* [#5131](https://github.com/leanprover/lean4/pull/5131) adds `List.append` lemmas.
|
||||
* [#5152](https://github.com/leanprover/lean4/pull/5152) adds `List.erase(|P|Idx)` lemmas.
|
||||
* [#5127](https://github.com/leanprover/lean4/pull/5127) makes miscellaneous lemma updates.
|
||||
* [#5153](https://github.com/leanprover/lean4/pull/5153) and [#5160](https://github.com/leanprover/lean4/pull/5160) add lemmas about `List.attach` and `List.pmap`.
|
||||
* [#5164](https://github.com/leanprover/lean4/pull/5164), [#5177](https://github.com/leanprover/lean4/pull/5177), and [#5215](https://github.com/leanprover/lean4/pull/5215) add `List.find?` and `List.range'/range/iota` lemmas.
|
||||
* [#5196](https://github.com/leanprover/lean4/pull/5196) adds `List.Pairwise_erase` and related lemmas.
|
||||
* [#5151](https://github.com/leanprover/lean4/pull/5151) and [#5163](https://github.com/leanprover/lean4/pull/5163) improve confluence of `List` simp lemmas. [#5105](https://github.com/leanprover/lean4/pull/5105) and [#5102](https://github.com/leanprover/lean4/pull/5102) adjust `List` simp lemmas.
|
||||
* [#5178](https://github.com/leanprover/lean4/pull/5178) removes `List.getLast_eq_iff_getLast_eq_some` as a simp lemma.
|
||||
* [#5210](https://github.com/leanprover/lean4/pull/5210) reverses the meaning of `List.getElem_drop` and `List.getElem_drop'`.
|
||||
* [#5214](https://github.com/leanprover/lean4/pull/5214) moves `@[csimp]` lemmas earlier where possible.
|
||||
* `Nat` and `Int`
|
||||
* [#5104](https://github.com/leanprover/lean4/pull/5104) adds `Nat.add_left_eq_self` and relatives.
|
||||
* [#5146](https://github.com/leanprover/lean4/pull/5146) adds missing `Nat.and_xor_distrib_(left|right)`.
|
||||
* [#5148](https://github.com/leanprover/lean4/pull/5148) and [#5190](https://github.com/leanprover/lean4/pull/5190) improve `Nat` and `Int` simp lemma confluence.
|
||||
* [#5165](https://github.com/leanprover/lean4/pull/5165) adjusts `Int` simp lemmas.
|
||||
* [#5166](https://github.com/leanprover/lean4/pull/5166) adds `Int` lemmas relating `neg` and `emod`/`mod`.
|
||||
* [#5208](https://github.com/leanprover/lean4/pull/5208) reverses the direction of the `Int.toNat_sub` simp lemma.
|
||||
* [#5209](https://github.com/leanprover/lean4/pull/5209) adds `Nat.bitwise` lemmas.
|
||||
* [#5230](https://github.com/leanprover/lean4/pull/5230) corrects the docstrings for integer division and modulus.
|
||||
* `Option`
|
||||
* [#5128](https://github.com/leanprover/lean4/pull/5128) and [#5154](https://github.com/leanprover/lean4/pull/5154) add `Option` lemmas.
|
||||
* `BitVec`
|
||||
* [#4889](https://github.com/leanprover/lean4/pull/4889) adds `sshiftRight` bitblasting.
|
||||
* [#4981](https://github.com/leanprover/lean4/pull/4981) adds `Std.Associative` and `Std.Commutative` instances for `BitVec.[and|or|xor]`.
|
||||
* [#4913](https://github.com/leanprover/lean4/pull/4913) enables `missingDocs` error for `BitVec` modules.
|
||||
* [#4930](https://github.com/leanprover/lean4/pull/4930) makes parameter names for `BitVec` more consistent.
|
||||
* [#5098](https://github.com/leanprover/lean4/pull/5098) adds `BitVec.intMin`. Introduces `boolToPropSimps` simp set for converting from boolean to propositional expressions.
|
||||
* [#5200](https://github.com/leanprover/lean4/pull/5200) and [#5217](https://github.com/leanprover/lean4/pull/5217) rename `BitVec.getLsb` to `BitVec.getLsbD`, etc., to bring naming in line with `List`/`Array`/etc.
|
||||
* **Theorems:** [#4977](https://github.com/leanprover/lean4/pull/4977), [#4951](https://github.com/leanprover/lean4/pull/4951), [#4667](https://github.com/leanprover/lean4/pull/4667), [#5007](https://github.com/leanprover/lean4/pull/5007), [#4997](https://github.com/leanprover/lean4/pull/4997), [#5083](https://github.com/leanprover/lean4/pull/5083), [#5081](https://github.com/leanprover/lean4/pull/5081), [#4392](https://github.com/leanprover/lean4/pull/4392)
|
||||
* `UInt`
|
||||
* [#4514](https://github.com/leanprover/lean4/pull/4514) fixes naming convention for `UInt` lemmas.
|
||||
* `Std.HashMap` and `Std.HashSet`
|
||||
* [#4943](https://github.com/leanprover/lean4/pull/4943) deprecates variants of hash map query methods. (See breaking changes.)
|
||||
* [#4917](https://github.com/leanprover/lean4/pull/4917) switches the library and Lean to `Std.HashMap` and `Std.HashSet` almost everywhere.
|
||||
* [#4954](https://github.com/leanprover/lean4/pull/4954) deprecates `Lean.HashMap` and `Lean.HashSet`.
|
||||
* [#5023](https://github.com/leanprover/lean4/pull/5023) cleans up lemma parameters.
|
||||
|
||||
* `Std.Sat` (for `bv_decide`)
|
||||
* [#4933](https://github.com/leanprover/lean4/pull/4933) adds definitions of SAT and CNF.
|
||||
* [#4953](https://github.com/leanprover/lean4/pull/4953) defines "and-inverter graphs" (AIGs) as described in section 3 of [Davis-Swords 2013](https://arxiv.org/pdf/1304.7861.pdf).
|
||||
|
||||
* **Parsec**
|
||||
* [#4774](https://github.com/leanprover/lean4/pull/4774) generalizes the `Parsec` library, allowing parsing of iterable data beyong `String` such as `ByteArray`. (See breaking changes.)
|
||||
* [#5115](https://github.com/leanprover/lean4/pull/5115) moves `Lean.Data.Parsec` to `Std.Internal.Parsec` for bootstrappng reasons.
|
||||
|
||||
* `Thunk`
|
||||
* [#4969](https://github.com/leanprover/lean4/pull/4969) upstreams `Thunk.ext`.
|
||||
|
||||
* **IO**
|
||||
* [#4973](https://github.com/leanprover/lean4/pull/4973) modifies `IO.FS.lines` to handle `\r\n` on all operating systems instead of just on Windows.
|
||||
* [#5125](https://github.com/leanprover/lean4/pull/5125) adds `createTempFile` and `withTempFile` for creating temporary files that can only be read and written by the current user.
|
||||
|
||||
* **Other fixes or improvements**
|
||||
* [#4945](https://github.com/leanprover/lean4/pull/4945) adds `Array`, `Bool` and `Prod` utilities from LeanSAT.
|
||||
* [#4960](https://github.com/leanprover/lean4/pull/4960) adds `Relation.TransGen.trans`.
|
||||
* [#5012](https://github.com/leanprover/lean4/pull/5012) states `WellFoundedRelation Nat` using `<`, not `Nat.lt`.
|
||||
* [#5011](https://github.com/leanprover/lean4/pull/5011) uses `≠` instead of `Not (Eq ...)` in `Fin.ne_of_val_ne`.
|
||||
* [#5197](https://github.com/leanprover/lean4/pull/5197) upstreams `Fin.le_antisymm`.
|
||||
* [#5042](https://github.com/leanprover/lean4/pull/5042) reduces usage of `refine'`.
|
||||
* [#5101](https://github.com/leanprover/lean4/pull/5101) adds about `if-then-else` and `Option`.
|
||||
* [#5112](https://github.com/leanprover/lean4/pull/5112) adds basic instances for `ULift` and `PLift`.
|
||||
* [#5133](https://github.com/leanprover/lean4/pull/5133) and [#5168](https://github.com/leanprover/lean4/pull/5168) make fixes from running the simpNF linter over Lean.
|
||||
* [#5156](https://github.com/leanprover/lean4/pull/5156) removes a bad simp lemma in `omega` theory.
|
||||
* [#5155](https://github.com/leanprover/lean4/pull/5155) improves confluence of `Bool` simp lemmas.
|
||||
* [#5162](https://github.com/leanprover/lean4/pull/5162) improves confluence of `Function.comp` simp lemmas.
|
||||
* [#5191](https://github.com/leanprover/lean4/pull/5191) improves confluence of `if-then-else` simp lemmas.
|
||||
* [#5147](https://github.com/leanprover/lean4/pull/5147) adds `@[elab_as_elim]` to `Quot.rec`, `Nat.strongInductionOn` and `Nat.casesStrongInductionOn`, and also renames the latter two to `Nat.strongRecOn` and `Nat.casesStrongRecOn` (deprecated in [#5179](https://github.com/leanprover/lean4/pull/5179)).
|
||||
* [#5180](https://github.com/leanprover/lean4/pull/5180) disables some simp lemmas with bad discrimination tree keys.
|
||||
* [#5189](https://github.com/leanprover/lean4/pull/5189) cleans up internal simp lemmas that had leaked.
|
||||
* [#5198](https://github.com/leanprover/lean4/pull/5198) cleans up `allowUnsafeReducibility`.
|
||||
* [#5229](https://github.com/leanprover/lean4/pull/5229) removes unused lemmas from some `simp` tactics.
|
||||
* [#5199](https://github.com/leanprover/lean4/pull/5199) removes >6 month deprecations.
|
||||
|
||||
### Lean internals
|
||||
|
||||
* **Performance**
|
||||
* Some core algorithms have been rewritten in C++ for performance.
|
||||
* [#4910](https://github.com/leanprover/lean4/pull/4910) and [#4912](https://github.com/leanprover/lean4/pull/4912) reimplement `instantiateLevelMVars`.
|
||||
* [#4915](https://github.com/leanprover/lean4/pull/4915), [#4922](https://github.com/leanprover/lean4/pull/4922), and [#4931](https://github.com/leanprover/lean4/pull/4931) reimplement `instantiateExprMVars`, 30% faster on a benchmark.
|
||||
* [#4934](https://github.com/leanprover/lean4/pull/4934) has optimizations for the kernel's `Expr` equality test.
|
||||
* [#4990](https://github.com/leanprover/lean4/pull/4990) fixes bug in hashing for the kernel's `Expr` equality test.
|
||||
* [#4935](https://github.com/leanprover/lean4/pull/4935) and [#4936](https://github.com/leanprover/lean4/pull/4936) skip some `PreDefinition` transformations if they are not needed.
|
||||
* [#5225](https://github.com/leanprover/lean4/pull/5225) adds caching for visited exprs at `CheckAssignmentQuick` in `ExprDefEq`.
|
||||
* [#5226](https://github.com/leanprover/lean4/pull/5226) maximizes term sharing at `instantiateMVarDeclMVars`, used by `runTactic`.
|
||||
* **Diagnostics and profiling**
|
||||
* [#4923](https://github.com/leanprover/lean4/pull/4923) adds profiling for `instantiateMVars` in `Lean.Elab.MutualDef`, which can be a bottleneck there.
|
||||
* [#4924](https://github.com/leanprover/lean4/pull/4924) adds diagnostics for large theorems, controlled by the `diagnostics.threshold.proofSize` option.
|
||||
* [#4897](https://github.com/leanprover/lean4/pull/4897) improves display of diagnostic results.
|
||||
* **Other fixes or improvements**
|
||||
* [#4921](https://github.com/leanprover/lean4/pull/4921) cleans up `Expr.betaRev`.
|
||||
* [#4940](https://github.com/leanprover/lean4/pull/4940) fixes tests by not writing directly to stdout, which is unreliable now that elaboration and reporting are executed in separate threads.
|
||||
* [#4955](https://github.com/leanprover/lean4/pull/4955) documents that `stderrAsMessages` is now the default on the command line as well.
|
||||
* [#4647](https://github.com/leanprover/lean4/pull/4647) adjusts documentation for building on macOS.
|
||||
* [#4987](https://github.com/leanprover/lean4/pull/4987) makes regular mvar assignments take precedence over delayed ones in `instantiateMVars`. Normally delayed assignment metavariables are never directly assigned, but on errors Lean assigns `sorry` to unassigned metavariables.
|
||||
* [#4967](https://github.com/leanprover/lean4/pull/4967) adds linter name to errors when a linter crashes.
|
||||
* [#5043](https://github.com/leanprover/lean4/pull/5043) cleans up command line snapshots logic.
|
||||
* [#5067](https://github.com/leanprover/lean4/pull/5067) minimizes some imports.
|
||||
* [#5068](https://github.com/leanprover/lean4/pull/5068) generalizes the monad for `addMatcherInfo`.
|
||||
* [f71a1f](https://github.com/leanprover/lean4/commit/f71a1fb4ae958fccb3ad4d48786a8f47ced05c15) adds missing test for [#5126](https://github.com/leanprover/lean4/issues/5126).
|
||||
* [#5201](https://github.com/leanprover/lean4/pull/5201) restores a test.
|
||||
* [#3698](https://github.com/leanprover/lean4/pull/3698) fixes a bug where label attributes did not pass on the attribute kind.
|
||||
* Typos: [#5080](https://github.com/leanprover/lean4/pull/5080), [#5150](https://github.com/leanprover/lean4/pull/5150), [#5202](https://github.com/leanprover/lean4/pull/5202)
|
||||
|
||||
### Compiler, runtime, and FFI
|
||||
|
||||
* [#3106](https://github.com/leanprover/lean4/pull/3106) moves frontend to new snapshot architecture. Note that `Frontend.processCommand` and `FrontendM` are no longer used by Lean core, but they will be preserved.
|
||||
* [#4919](https://github.com/leanprover/lean4/pull/4919) adds missing include in runtime for `AUTO_THREAD_FINALIZATION` feature on Windows.
|
||||
* [#4941](https://github.com/leanprover/lean4/pull/4941) adds more `LEAN_EXPORT`s for Windows.
|
||||
* [#4911](https://github.com/leanprover/lean4/pull/4911) improves formatting of CLI help text for the frontend.
|
||||
* [#4950](https://github.com/leanprover/lean4/pull/4950) improves file reading and writing.
|
||||
* `readBinFile` and `readFile` now only require two system calls (`stat` + `read`) instead of one `read` per 1024 byte chunk.
|
||||
* `Handle.getLine` and `Handle.putStr` no longer get tripped up by NUL characters.
|
||||
* [#4971](https://github.com/leanprover/lean4/pull/4971) handles the SIGBUS signal when detecting stack overflows.
|
||||
* [#5062](https://github.com/leanprover/lean4/pull/5062) avoids overwriting existing signal handlers, like in [rust-lang/rust#69685](https://github.com/rust-lang/rust/pull/69685).
|
||||
* [#4860](https://github.com/leanprover/lean4/pull/4860) improves workarounds for building on Windows. Splits `libleanshared` on Windows to avoid symbol limit, removes the `LEAN_EXPORT` denylist workaround, adds missing `LEAN_EXPORT`s.
|
||||
* [#4952](https://github.com/leanprover/lean4/pull/4952) output panics into Lean's redirected stderr, ensuring panics ARE visible as regular messages in the language server and properly ordered in relation to other messages on the command line.
|
||||
* [#4963](https://github.com/leanprover/lean4/pull/4963) links LibUV.
|
||||
|
||||
### Lake
|
||||
|
||||
* [#5030](https://github.com/leanprover/lean4/pull/5030) removes dead code.
|
||||
* [#4770](https://github.com/leanprover/lean4/pull/4770) adds additional fields to the package configuration which will be used by Reservoir. See the PR description for details.
|
||||
|
||||
|
||||
### DevOps/CI
|
||||
* [#4914](https://github.com/leanprover/lean4/pull/4914) and [#4937](https://github.com/leanprover/lean4/pull/4937) improve the release checklist.
|
||||
* [#4925](https://github.com/leanprover/lean4/pull/4925) ignores stale leanpkg tests.
|
||||
* [#5003](https://github.com/leanprover/lean4/pull/5003) upgrades `actions/cache` in CI.
|
||||
* [#5010](https://github.com/leanprover/lean4/pull/5010) sets `save-always` in cache actions in CI.
|
||||
* [#5008](https://github.com/leanprover/lean4/pull/5008) adds more libuv search patterns for the speedcenter.
|
||||
* [#5009](https://github.com/leanprover/lean4/pull/5009) reduce number of runs in the speedcenter for "fast" benchmarks from 10 to 3.
|
||||
* [#5014](https://github.com/leanprover/lean4/pull/5014) adjusts lakefile editing to use new `git` syntax in `pr-release` workflow.
|
||||
* [#5025](https://github.com/leanprover/lean4/pull/5025) has `pr-release` workflow pass `--retry` to `curl`.
|
||||
* [#5022](https://github.com/leanprover/lean4/pull/5022) builds MacOS Aarch64 release for PRs by default.
|
||||
* [#5045](https://github.com/leanprover/lean4/pull/5045) adds libuv to the required packages heading in macos docs.
|
||||
* [#5034](https://github.com/leanprover/lean4/pull/5034) fixes the install name of `libleanshared_1` on macOS.
|
||||
* [#5051](https://github.com/leanprover/lean4/pull/5051) fixes Windows stage 0.
|
||||
* [#5052](https://github.com/leanprover/lean4/pull/5052) fixes 32bit stage 0 builds in CI.
|
||||
* [#5057](https://github.com/leanprover/lean4/pull/5057) avoids rebuilding `leanmanifest` in each build.
|
||||
* [#5099](https://github.com/leanprover/lean4/pull/5099) makes `restart-on-label` workflow also filter by commit SHA.
|
||||
* [#4325](https://github.com/leanprover/lean4/pull/4325) adds CaDiCaL.
|
||||
|
||||
### Breaking changes
|
||||
|
||||
* [LibUV](https://libuv.org/) is now required to build Lean. This change only affects developers who compile Lean themselves instead of obtaining toolchains via `elan`. We have updated the official build instructions with information on how to obtain LibUV on our supported platforms. ([#4963](https://github.com/leanprover/lean4/pull/4963))
|
||||
|
||||
* Recursive definitions with a `decreasing_by` clause that begins with `simp_wf` may break. Try removing `simp_wf` or replacing it with `simp`. ([#5016](https://github.com/leanprover/lean4/pull/5016))
|
||||
|
||||
* The behavior of `rw [f]` where `f` is a non-recursive function defined by pattern matching changed.
|
||||
|
||||
For example, preciously, `rw [Option.map]` would rewrite `Option.map f o` to `match o with … `. Now this rewrite fails because it will use the equational lemmas, and these require constructors – just like for `List.map`.
|
||||
|
||||
Remedies:
|
||||
* Split on `o` before rewriting.
|
||||
* Use `rw [Option.map.eq_def]`, which rewrites any (saturated) application of `Option.map`.
|
||||
* Use `set_option backward.eqns.nonrecursive false` when *defining* the function in question.
|
||||
([#4154](https://github.com/leanprover/lean4/pull/4154))
|
||||
|
||||
* The unified handling of equation lemmas for recursive and non-recursive functions can break existing code, as there now can be extra equational lemmas:
|
||||
|
||||
* Explicit uses of `f.eq_2` might have to be adjusted if the numbering changed.
|
||||
|
||||
* Uses of `rw [f]` or `simp [f]` may no longer apply if they previously matched (and introduced a `match` statement), when the equational lemmas got more fine-grained.
|
||||
|
||||
In this case either case analysis on the parameters before rewriting helps, or setting the option `backward.eqns.deepRecursiveSplit false` while *defining* the function.
|
||||
|
||||
([#5129](https://github.com/leanprover/lean4/pull/5129), [#5207](https://github.com/leanprover/lean4/pull/5207))
|
||||
|
||||
* The `reduceCtorEq` simproc is now optional, and it might need to be included in lists of simp lemmas, like `simp only [reduceCtorEq]`. This simproc is responsible for reducing equalities of constructors. ([#5167](https://github.com/leanprover/lean4/pull/5167))
|
||||
|
||||
* `Nat.strongInductionOn` is now `Nat.strongRecOn` and `Nat.caseStrongInductionOn` to `Nat.caseStrongRecOn`. ([#5147](https://github.com/leanprover/lean4/pull/5147))
|
||||
|
||||
* The parameters to `Membership.mem` have been swapped, which affects all `Membership` instances. ([#5020](https://github.com/leanprover/lean4/pull/5020))
|
||||
|
||||
* The meanings of `List.getElem_drop` and `List.getElem_drop'` have been reversed and the first is now a simp lemma. ([#5210](https://github.com/leanprover/lean4/pull/5210))
|
||||
|
||||
* The `Parsec` library has moved from `Lean.Data.Parsec` to `Std.Internal.Parsec`. The `Parsec` type is now more general with a parameter for an iterable. Users parsing strings can migrate to `Parser` in the `Std.Internal.Parsec.String` namespace, which also includes string-focused parsing combinators. ([#4774](https://github.com/leanprover/lean4/pull/4774))
|
||||
|
||||
* The `Lean` module has switched from `Lean.HashMap` and `Lean.HashSet` to `Std.HashMap` and `Std.HashSet` ([#4943](https://github.com/leanprover/lean4/pull/4943)). `Lean.HashMap` and `Lean.HashSet` are now deprecated ([#4954](https://github.com/leanprover/lean4/pull/4954)) and will be removed in a future release. Users of `Lean` APIs that interact with hash maps, for example `Lean.Environment.const2ModIdx`, might encounter minor breakage due to the following changes from `Lean.HashMap` to `Std.HashMap`:
|
||||
* query functions use the term `get` instead of `find`, ([#4943](https://github.com/leanprover/lean4/pull/4943))
|
||||
* the notation `map[key]` no longer returns an optional value but instead expects a proof that the key is present in the map. The previous behavior is available via the `map[key]?` notation.
|
||||
|
||||
|
||||
v4.11.0
|
||||
----------
|
||||
@@ -21,7 +331,7 @@ v4.11.0
|
||||
|
||||
See breaking changes below.
|
||||
|
||||
PRs: [#4883](https://github.com/leanprover/lean4/pull/4883), [1242ff](https://github.com/leanprover/lean4/commit/1242ffbfb5a79296041683682268e770fc3cf820), [#5000](https://github.com/leanprover/lean4/pull/5000), [#5036](https://github.com/leanprover/lean4/pull/5036), [#5138](https://github.com/leanprover/lean4/pull/5138), [0edf1b](https://github.com/leanprover/lean4/commit/0edf1bac392f7e2fe0266b28b51c498306363a84).
|
||||
PRs: [#4883](https://github.com/leanprover/lean4/pull/4883), [#4814](https://github.com/leanprover/lean4/pull/4814), [#5000](https://github.com/leanprover/lean4/pull/5000), [#5036](https://github.com/leanprover/lean4/pull/5036), [#5138](https://github.com/leanprover/lean4/pull/5138), [0edf1b](https://github.com/leanprover/lean4/commit/0edf1bac392f7e2fe0266b28b51c498306363a84).
|
||||
|
||||
* **Recursive definitions**
|
||||
* Structural recursion can now be explicitly requested using
|
||||
|
||||
@@ -1,3 +0,0 @@
|
||||
* The `Lean` module has switched from `Lean.HashMap` and `Lean.HashSet` to `Std.HashMap` and `Std.HashSet`. `Lean.HashMap` and `Lean.HashSet` are now deprecated and will be removed in a future release. Users of `Lean` APIs that interact with hash maps, for example `Lean.Environment.const2ModIdx`, might encounter minor breakage due to the following breaking changes from `Lean.HashMap` to `Std.HashMap`:
|
||||
* query functions use the term `get` instead of `find`,
|
||||
* the notation `map[key]` no longer returns an optional value but expects a proof that the key is present in the map instead. The previous behavior is available via the `map[key]?` notation.
|
||||
@@ -1 +0,0 @@
|
||||
* #4963 [LibUV](https://libuv.org/) is now required to build Lean. This change only affects developers who compile Lean themselves instead of obtaining toolchains via `elan`. We have updated the official build instructions with information on how to obtain LibUV on our supported platforms.
|
||||
@@ -80,6 +80,8 @@ noncomputable scoped instance (priority := low) propDecidable (a : Prop) : Decid
|
||||
noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) where
|
||||
default := inferInstance
|
||||
|
||||
instance (a : Prop) : Nonempty (Decidable a) := ⟨propDecidable a⟩
|
||||
|
||||
noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α :=
|
||||
fun _ _ => inferInstance
|
||||
|
||||
|
||||
@@ -133,6 +133,9 @@ theorem seqLeft_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x <* y
|
||||
rw [← bind_pure_comp]
|
||||
simp only [bind_assoc, pure_bind]
|
||||
|
||||
@[simp] theorem Functor.map_unit [Monad m] [LawfulMonad m] {a : m PUnit} : (fun _ => PUnit.unit) <$> a = a := by
|
||||
simp [map]
|
||||
|
||||
/--
|
||||
An alternative constructor for `LawfulMonad` which has more
|
||||
defaultable fields in the common case.
|
||||
@@ -180,9 +183,9 @@ end Id
|
||||
|
||||
instance : LawfulMonad Option := LawfulMonad.mk'
|
||||
(id_map := fun x => by cases x <;> rfl)
|
||||
(pure_bind := fun x f => rfl)
|
||||
(bind_assoc := fun x f g => by cases x <;> rfl)
|
||||
(bind_pure_comp := fun f x => by cases x <;> rfl)
|
||||
(pure_bind := fun _ _ => rfl)
|
||||
(bind_assoc := fun x _ _ => by cases x <;> rfl)
|
||||
(bind_pure_comp := fun _ x => by cases x <;> rfl)
|
||||
|
||||
instance : LawfulApplicative Option := inferInstance
|
||||
instance : LawfulFunctor Option := inferInstance
|
||||
|
||||
@@ -84,14 +84,19 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m) where
|
||||
pure_bind := by intros; apply ext; simp [run_bind]
|
||||
bind_assoc := by intros; apply ext; simp [run_bind]; apply bind_congr; intro a; cases a <;> simp
|
||||
|
||||
@[simp] theorem map_throw [Monad m] [LawfulMonad m] {α β : Type _} (f : α → β) (e : ε) :
|
||||
f <$> (throw e : ExceptT ε m α) = (throw e : ExceptT ε m β) := by
|
||||
simp only [ExceptT.instMonad, ExceptT.map, ExceptT.mk, throw, throwThe, MonadExceptOf.throw,
|
||||
pure_bind]
|
||||
|
||||
end ExceptT
|
||||
|
||||
/-! # Except -/
|
||||
|
||||
instance : LawfulMonad (Except ε) := LawfulMonad.mk'
|
||||
(id_map := fun x => by cases x <;> rfl)
|
||||
(pure_bind := fun a f => rfl)
|
||||
(bind_assoc := fun a f g => by cases a <;> rfl)
|
||||
(pure_bind := fun _ _ => rfl)
|
||||
(bind_assoc := fun a _ _ => by cases a <;> rfl)
|
||||
|
||||
instance : LawfulApplicative (Except ε) := inferInstance
|
||||
instance : LawfulFunctor (Except ε) := inferInstance
|
||||
|
||||
@@ -5,6 +5,7 @@ Authors: Joachim Breitner, Mario Carneiro
|
||||
-/
|
||||
prelude
|
||||
import Init.Data.Array.Mem
|
||||
import Init.Data.Array.Lemmas
|
||||
import Init.Data.List.Attach
|
||||
|
||||
namespace Array
|
||||
@@ -26,4 +27,154 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
|
||||
with the same elements but in the type `{x // x ∈ xs}`. -/
|
||||
@[inline] def attach (xs : Array α) : Array {x // x ∈ xs} := xs.attachWith _ fun _ => id
|
||||
|
||||
@[simp] theorem _root_.List.attachWith_toArray {l : List α} {P : α → Prop} {H : ∀ x ∈ l.toArray, P x} :
|
||||
l.toArray.attachWith P H = (l.attachWith P (by simpa using H)).toArray := by
|
||||
simp [attachWith]
|
||||
|
||||
@[simp] theorem _root_.List.attach_toArray {l : List α} :
|
||||
l.toArray.attach = (l.attachWith (· ∈ l.toArray) (by simp)).toArray := by
|
||||
simp [attach]
|
||||
|
||||
@[simp] theorem toList_attachWith {l : Array α} {P : α → Prop} {H : ∀ x ∈ l, P x} :
|
||||
(l.attachWith P H).toList = l.toList.attachWith P (by simpa [mem_toList] using H) := by
|
||||
simp [attachWith]
|
||||
|
||||
@[simp] theorem toList_attach {α : Type _} {l : Array α} :
|
||||
l.attach.toList = l.toList.attachWith (· ∈ l) (by simp [mem_toList]) := by
|
||||
simp [attach]
|
||||
|
||||
/-! ## unattach
|
||||
|
||||
`Array.unattach` is the (one-sided) inverse of `Array.attach`. It is a synonym for `Array.map Subtype.val`.
|
||||
|
||||
We use it by providing a simp lemma `l.attach.unattach = l`, and simp lemmas which recognize higher order
|
||||
functions applied to `l : Array { x // p x }` which only depend on the value, not the predicate, and rewrite these
|
||||
in terms of a simpler function applied to `l.unattach`.
|
||||
|
||||
Further, we provide simp lemmas that push `unattach` inwards.
|
||||
-/
|
||||
|
||||
/--
|
||||
A synonym for `l.map (·.val)`. Mostly this should not be needed by users.
|
||||
It is introduced as in intermediate step by lemmas such as `map_subtype`,
|
||||
and is ideally subsequently simplified away by `unattach_attach`.
|
||||
|
||||
If not, usually the right approach is `simp [Array.unattach, -Array.map_subtype]` to unfold.
|
||||
-/
|
||||
def unattach {α : Type _} {p : α → Prop} (l : Array { x // p x }) := l.map (·.val)
|
||||
|
||||
@[simp] theorem unattach_nil {α : Type _} {p : α → Prop} : (#[] : Array { x // p x }).unattach = #[] := rfl
|
||||
@[simp] theorem unattach_push {α : Type _} {p : α → Prop} {a : { x // p x }} {l : Array { x // p x }} :
|
||||
(l.push a).unattach = l.unattach.push a.1 := by
|
||||
simp [unattach]
|
||||
|
||||
@[simp] theorem size_unattach {α : Type _} {p : α → Prop} {l : Array { x // p x }} :
|
||||
l.unattach.size = l.size := by
|
||||
unfold unattach
|
||||
simp
|
||||
|
||||
@[simp] theorem _root_.List.unattach_toArray {α : Type _} {p : α → Prop} {l : List { x // p x }} :
|
||||
l.toArray.unattach = l.unattach.toArray := by
|
||||
simp [unattach, List.unattach]
|
||||
|
||||
@[simp] theorem toList_unattach {α : Type _} {p : α → Prop} {l : Array { x // p x }} :
|
||||
l.unattach.toList = l.toList.unattach := by
|
||||
simp [unattach, List.unattach]
|
||||
|
||||
@[simp] theorem unattach_attach {α : Type _} (l : Array α) : l.attach.unattach = l := by
|
||||
cases l
|
||||
simp
|
||||
|
||||
@[simp] theorem unattach_attachWith {α : Type _} {p : α → Prop} {l : Array α}
|
||||
{H : ∀ a ∈ l, p a} :
|
||||
(l.attachWith p H).unattach = l := by
|
||||
cases l
|
||||
simp
|
||||
|
||||
/-! ### Recognizing higher order functions using a function that only depends on the value. -/
|
||||
|
||||
/--
|
||||
This lemma identifies folds over arrays of subtypes, where the function only depends on the value, not the proposition,
|
||||
and simplifies these to the function directly taking the value.
|
||||
-/
|
||||
theorem foldl_subtype {p : α → Prop} {l : Array { x // p x }}
|
||||
{f : β → { x // p x } → β} {g : β → α → β} {x : β}
|
||||
{hf : ∀ b x h, f b ⟨x, h⟩ = g b x} :
|
||||
l.foldl f x = l.unattach.foldl g x := by
|
||||
cases l
|
||||
simp only [List.foldl_toArray', List.unattach_toArray]
|
||||
rw [List.foldl_subtype] -- Why can't simp do this?
|
||||
simp [hf]
|
||||
|
||||
/-- Variant of `foldl_subtype` with side condition to check `stop = l.size`. -/
|
||||
@[simp] theorem foldl_subtype' {p : α → Prop} {l : Array { x // p x }}
|
||||
{f : β → { x // p x } → β} {g : β → α → β} {x : β}
|
||||
{hf : ∀ b x h, f b ⟨x, h⟩ = g b x} (h : stop = l.size) :
|
||||
l.foldl f x 0 stop = l.unattach.foldl g x := by
|
||||
subst h
|
||||
rwa [foldl_subtype]
|
||||
|
||||
/--
|
||||
This lemma identifies folds over arrays of subtypes, where the function only depends on the value, not the proposition,
|
||||
and simplifies these to the function directly taking the value.
|
||||
-/
|
||||
theorem foldr_subtype {p : α → Prop} {l : Array { x // p x }}
|
||||
{f : { x // p x } → β → β} {g : α → β → β} {x : β}
|
||||
{hf : ∀ x h b, f ⟨x, h⟩ b = g x b} :
|
||||
l.foldr f x = l.unattach.foldr g x := by
|
||||
cases l
|
||||
simp only [List.foldr_toArray', List.unattach_toArray]
|
||||
rw [List.foldr_subtype]
|
||||
simp [hf]
|
||||
|
||||
/-- Variant of `foldr_subtype` with side condition to check `stop = l.size`. -/
|
||||
@[simp] theorem foldr_subtype' {p : α → Prop} {l : Array { x // p x }}
|
||||
{f : { x // p x } → β → β} {g : α → β → β} {x : β}
|
||||
{hf : ∀ x h b, f ⟨x, h⟩ b = g x b} (h : start = l.size) :
|
||||
l.foldr f x start 0 = l.unattach.foldr g x := by
|
||||
subst h
|
||||
rwa [foldr_subtype]
|
||||
|
||||
/--
|
||||
This lemma identifies maps over arrays of subtypes, where the function only depends on the value, not the proposition,
|
||||
and simplifies these to the function directly taking the value.
|
||||
-/
|
||||
@[simp] theorem map_subtype {p : α → Prop} {l : Array { x // p x }}
|
||||
{f : { x // p x } → β} {g : α → β} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
|
||||
l.map f = l.unattach.map g := by
|
||||
cases l
|
||||
simp only [List.map_toArray, List.unattach_toArray]
|
||||
rw [List.map_subtype]
|
||||
simp [hf]
|
||||
|
||||
@[simp] theorem filterMap_subtype {p : α → Prop} {l : Array { x // p x }}
|
||||
{f : { x // p x } → Option β} {g : α → Option β} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
|
||||
l.filterMap f = l.unattach.filterMap g := by
|
||||
cases l
|
||||
simp only [size_toArray, List.filterMap_toArray', List.unattach_toArray, List.length_unattach,
|
||||
mk.injEq]
|
||||
rw [List.filterMap_subtype]
|
||||
simp [hf]
|
||||
|
||||
@[simp] theorem unattach_filter {p : α → Prop} {l : Array { x // p x }}
|
||||
{f : { x // p x } → Bool} {g : α → Bool} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
|
||||
(l.filter f).unattach = l.unattach.filter g := by
|
||||
cases l
|
||||
simp [hf]
|
||||
rw [List.unattach_filter]
|
||||
simp [hf]
|
||||
|
||||
/-! ### Simp lemmas pushing `unattach` inwards. -/
|
||||
|
||||
@[simp] theorem unattach_reverse {p : α → Prop} {l : Array { x // p x }} :
|
||||
l.reverse.unattach = l.unattach.reverse := by
|
||||
cases l
|
||||
simp
|
||||
|
||||
@[simp] theorem unattach_append {p : α → Prop} {l₁ l₂ : Array { x // p x }} :
|
||||
(l₁ ++ l₂).unattach = l₁.unattach ++ l₂.unattach := by
|
||||
cases l₁
|
||||
cases l₂
|
||||
simp
|
||||
|
||||
end Array
|
||||
|
||||
@@ -617,7 +617,7 @@ def concatMap (f : α → Array β) (as : Array α) : Array β :=
|
||||
|
||||
`flatten #[#[a₁, a₂, ⋯], #[b₁, b₂, ⋯], ⋯]` = `#[a₁, a₂, ⋯, b₁, b₂, ⋯]`
|
||||
-/
|
||||
def flatten (as : Array (Array α)) : Array α :=
|
||||
@[inline] def flatten (as : Array (Array α)) : Array α :=
|
||||
as.foldl (init := empty) fun r a => r ++ a
|
||||
|
||||
@[inline]
|
||||
@@ -720,7 +720,7 @@ termination_by a.size - i.val
|
||||
decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ i.isLt
|
||||
|
||||
-- This is required in `Lean.Data.PersistentHashMap`.
|
||||
theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
|
||||
@[simp] theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
|
||||
induction a, i using Array.feraseIdx.induct with
|
||||
| @case1 a i h a' _ ih =>
|
||||
unfold feraseIdx
|
||||
|
||||
@@ -73,7 +73,7 @@ theorem foldr_eq_foldr_toList (f : α → β → β) (init : β) (arr : Array α
|
||||
|
||||
@[simp] theorem append_eq_append (arr arr' : Array α) : arr.append arr' = arr ++ arr' := rfl
|
||||
|
||||
@[simp] theorem append_toList (arr arr' : Array α) :
|
||||
@[simp] theorem toList_append (arr arr' : Array α) :
|
||||
(arr ++ arr').toList = arr.toList ++ arr'.toList := by
|
||||
rw [← append_eq_append]; unfold Array.append
|
||||
rw [foldl_eq_foldl_toList]
|
||||
@@ -111,8 +111,8 @@ abbrev toList_eq := @toListImpl_eq
|
||||
@[deprecated pop_toList (since := "2024-09-09")]
|
||||
abbrev pop_data := @pop_toList
|
||||
|
||||
@[deprecated append_toList (since := "2024-09-09")]
|
||||
abbrev append_data := @append_toList
|
||||
@[deprecated toList_append (since := "2024-09-09")]
|
||||
abbrev append_data := @toList_append
|
||||
|
||||
@[deprecated appendList_toList (since := "2024-09-09")]
|
||||
abbrev appendList_data := @appendList_toList
|
||||
|
||||
@@ -91,6 +91,8 @@ abbrev toArray_data := @toArray_toList
|
||||
@[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
|
||||
a.toArray[i] = a[i]'(by simpa using h) := rfl
|
||||
|
||||
@[simp] theorem getElem?_toArray {a : List α} {i : Nat} : a.toArray[i]? = a[i]? := rfl
|
||||
|
||||
@[deprecated "Use the reverse direction of `List.push_toArray`." (since := "2024-09-27")]
|
||||
theorem toArray_concat {as : List α} {x : α} :
|
||||
(as ++ [x]).toArray = as.toArray.push x := by
|
||||
@@ -98,7 +100,7 @@ theorem toArray_concat {as : List α} {x : α} :
|
||||
simp
|
||||
|
||||
@[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
|
||||
apply Array.ext'
|
||||
apply ext'
|
||||
simp
|
||||
|
||||
/-- Unapplied variant of `push_toArray`, useful for monadic reasoning. -/
|
||||
@@ -106,23 +108,57 @@ theorem toArray_concat {as : List α} {x : α} :
|
||||
funext a
|
||||
simp
|
||||
|
||||
@[simp] theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) :
|
||||
theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) :
|
||||
l.toArray.foldrM f init = l.foldrM f init := by
|
||||
rw [foldrM_eq_reverse_foldlM_toList]
|
||||
simp
|
||||
|
||||
@[simp] theorem foldlM_toArray [Monad m] (f : β → α → m β) (init : β) (l : List α) :
|
||||
theorem foldlM_toArray [Monad m] (f : β → α → m β) (init : β) (l : List α) :
|
||||
l.toArray.foldlM f init = l.foldlM f init := by
|
||||
rw [foldlM_eq_foldlM_toList]
|
||||
|
||||
@[simp] theorem foldr_toArray (f : α → β → β) (init : β) (l : List α) :
|
||||
theorem foldr_toArray (f : α → β → β) (init : β) (l : List α) :
|
||||
l.toArray.foldr f init = l.foldr f init := by
|
||||
rw [foldr_eq_foldr_toList]
|
||||
|
||||
@[simp] theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
|
||||
theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
|
||||
l.toArray.foldl f init = l.foldl f init := by
|
||||
rw [foldl_eq_foldl_toList]
|
||||
|
||||
/-- Variant of `foldrM_toArray` with a side condition for the `start` argument. -/
|
||||
@[simp] theorem foldrM_toArray' [Monad m] (f : α → β → m β) (init : β) (l : List α)
|
||||
(h : start = l.toArray.size) :
|
||||
l.toArray.foldrM f init start 0 = l.foldrM f init := by
|
||||
subst h
|
||||
rw [foldrM_eq_reverse_foldlM_toList]
|
||||
simp
|
||||
|
||||
/-- Variant of `foldlM_toArray` with a side condition for the `stop` argument. -/
|
||||
@[simp] theorem foldlM_toArray' [Monad m] (f : β → α → m β) (init : β) (l : List α)
|
||||
(h : stop = l.toArray.size) :
|
||||
l.toArray.foldlM f init 0 stop = l.foldlM f init := by
|
||||
subst h
|
||||
rw [foldlM_eq_foldlM_toList]
|
||||
|
||||
/-- Variant of `foldr_toArray` with a side condition for the `start` argument. -/
|
||||
@[simp] theorem foldr_toArray' (f : α → β → β) (init : β) (l : List α)
|
||||
(h : start = l.toArray.size) :
|
||||
l.toArray.foldr f init start 0 = l.foldr f init := by
|
||||
subst h
|
||||
rw [foldr_eq_foldr_toList]
|
||||
|
||||
/-- Variant of `foldl_toArray` with a side condition for the `stop` argument. -/
|
||||
@[simp] theorem foldl_toArray' (f : β → α → β) (init : β) (l : List α)
|
||||
(h : stop = l.toArray.size) :
|
||||
l.toArray.foldl f init 0 stop = l.foldl f init := by
|
||||
subst h
|
||||
rw [foldl_eq_foldl_toList]
|
||||
|
||||
@[simp] theorem append_toArray (l₁ l₂ : List α) :
|
||||
l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
|
||||
apply ext'
|
||||
simp
|
||||
|
||||
end List
|
||||
|
||||
namespace Array
|
||||
@@ -136,10 +172,10 @@ attribute [simp] uset
|
||||
@[deprecated toArray_toList (since := "2024-09-09")]
|
||||
abbrev toArray_data := @toArray_toList
|
||||
|
||||
@[simp] theorem toList_length {l : Array α} : l.toList.length = l.size := rfl
|
||||
@[simp] theorem length_toList {l : Array α} : l.toList.length = l.size := rfl
|
||||
|
||||
@[deprecated toList_length (since := "2024-09-09")]
|
||||
abbrev data_length := @toList_length
|
||||
@[deprecated length_toList (since := "2024-09-09")]
|
||||
abbrev data_length := @length_toList
|
||||
|
||||
@[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
|
||||
|
||||
@@ -175,25 +211,25 @@ where
|
||||
mapM.map f arr i r = (arr.toList.drop i).foldlM (fun bs a => bs.push <$> f a) r := by
|
||||
unfold mapM.map; split
|
||||
· rw [← List.get_drop_eq_drop _ i ‹_›]
|
||||
simp only [aux (i + 1), map_eq_pure_bind, toList_length, List.foldlM_cons, bind_assoc,
|
||||
simp only [aux (i + 1), map_eq_pure_bind, length_toList, List.foldlM_cons, bind_assoc,
|
||||
pure_bind]
|
||||
rfl
|
||||
· rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
|
||||
termination_by arr.size - i
|
||||
decreasing_by decreasing_trivial_pre_omega
|
||||
|
||||
@[simp] theorem map_toList (f : α → β) (arr : Array α) : (arr.map f).toList = arr.toList.map f := by
|
||||
@[simp] theorem toList_map (f : α → β) (arr : Array α) : (arr.map f).toList = arr.toList.map f := by
|
||||
rw [map, mapM_eq_foldlM]
|
||||
apply congrArg toList (foldl_eq_foldl_toList (fun bs a => push bs (f a)) #[] arr) |>.trans
|
||||
have H (l arr) : List.foldl (fun bs a => push bs (f a)) arr l = ⟨arr.toList ++ l.map f⟩ := by
|
||||
induction l generalizing arr <;> simp [*]
|
||||
simp [H]
|
||||
|
||||
@[deprecated map_toList (since := "2024-09-09")]
|
||||
abbrev map_data := @map_toList
|
||||
@[deprecated toList_map (since := "2024-09-09")]
|
||||
abbrev map_data := @toList_map
|
||||
|
||||
@[simp] theorem size_map (f : α → β) (arr : Array α) : (arr.map f).size = arr.size := by
|
||||
simp only [← toList_length]
|
||||
simp only [← length_toList]
|
||||
simp
|
||||
|
||||
@[simp] theorem appendList_nil (arr : Array α) : arr ++ ([] : List α) = arr := Array.ext' (by simp)
|
||||
@@ -201,6 +237,11 @@ abbrev map_data := @map_toList
|
||||
@[simp] theorem appendList_cons (arr : Array α) (a : α) (l : List α) :
|
||||
arr ++ (a :: l) = arr.push a ++ l := Array.ext' (by simp)
|
||||
|
||||
@[simp] theorem toList_appendList (arr : Array α) (l : List α) :
|
||||
(arr ++ l).toList = arr.toList ++ l := by
|
||||
cases arr
|
||||
simp
|
||||
|
||||
theorem foldl_toList_eq_bind (l : List α) (acc : Array β)
|
||||
(F : Array β → α → Array β) (G : α → List β)
|
||||
(H : ∀ acc a, (F acc a).toList = acc.toList ++ G a) :
|
||||
@@ -292,14 +333,14 @@ theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
|
||||
@[simp] theorem set!_is_setD : @set! = @setD := rfl
|
||||
|
||||
@[simp] theorem size_setD (a : Array α) (index : Nat) (val : α) :
|
||||
(Array.setD a index val).size = a.size := by
|
||||
(Array.setD a index val).size = a.size := by
|
||||
if h : index < a.size then
|
||||
simp [setD, h]
|
||||
else
|
||||
simp [setD, h]
|
||||
|
||||
@[simp] theorem getElem_setD_eq (a : Array α) {i : Nat} (v : α) (h : _) :
|
||||
(setD a i v)[i]'h = v := by
|
||||
(setD a i v)[i]'h = v := by
|
||||
simp at h
|
||||
simp only [setD, h, dite_true, getElem_set, ite_true]
|
||||
|
||||
@@ -309,7 +350,7 @@ theorem getElem?_setD_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) : (a
|
||||
|
||||
/-- Simplifies a normal form from `get!` -/
|
||||
@[simp] theorem getD_get?_setD (a : Array α) (i : Nat) (v d : α) :
|
||||
Option.getD (setD a i v)[i]? d = if i < a.size then v else d := by
|
||||
Option.getD (setD a i v)[i]? d = if i < a.size then v else d := by
|
||||
by_cases h : i < a.size <;>
|
||||
simp [setD, Nat.not_lt_of_le, h, getD_get?]
|
||||
|
||||
@@ -445,6 +486,10 @@ abbrev get?_eq_data_get? := @get?_eq_toList_get?
|
||||
theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
|
||||
simp [get!_eq_getD]
|
||||
|
||||
theorem getElem?_eq_some_iff {as : Array α} : as[n]? = some a ↔ ∃ h : n < as.size, as[n] = a := by
|
||||
cases as
|
||||
simp [List.getElem?_eq_some_iff]
|
||||
|
||||
@[simp] theorem back_eq_back? [Inhabited α] (a : Array α) : a.back = a.back?.getD default := by
|
||||
simp [back, back?]
|
||||
|
||||
@@ -507,7 +552,7 @@ theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v :
|
||||
simp only [set, getElem_eq_getElem_toList, List.getElem_set_ne h]
|
||||
|
||||
theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
|
||||
(setD a i v)[i] = v := by
|
||||
(setD a i v)[i] = v := by
|
||||
simp at h
|
||||
simp only [setD, h, dite_true, get_set, ite_true]
|
||||
|
||||
@@ -608,7 +653,8 @@ abbrev data_range := @toList_range
|
||||
theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Array.range n)[x] = x := by
|
||||
simp [getElem_eq_getElem_toList]
|
||||
|
||||
@[simp] theorem reverse_toList (a : Array α) : a.reverse.toList = a.toList.reverse := by
|
||||
set_option linter.deprecated false in
|
||||
@[simp] theorem toList_reverse (a : Array α) : a.reverse.toList = a.toList.reverse := by
|
||||
let rec go (as : Array α) (i j hj)
|
||||
(h : i + j + 1 = a.size) (h₂ : as.size = a.size)
|
||||
(H : ∀ k, as.toList[k]? = if i ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?)
|
||||
@@ -649,6 +695,9 @@ theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Arra
|
||||
true_and, Nat.not_lt] at h
|
||||
rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (a.toList.length_reverse ▸ ‹_›)]
|
||||
|
||||
@[deprecated toList_reverse (since := "2024-09-30")]
|
||||
abbrev reverse_toList := @toList_reverse
|
||||
|
||||
/-! ### foldl / foldr -/
|
||||
|
||||
@[simp] theorem foldlM_loop_empty [Monad m] (f : β → α → m β) (init : β) (i j : Nat) :
|
||||
@@ -710,19 +759,35 @@ theorem foldr_induction
|
||||
simp [foldr, foldrM]; split; {exact go _ h0}
|
||||
· next h => exact (Nat.eq_zero_of_not_pos h ▸ h0)
|
||||
|
||||
@[congr]
|
||||
theorem foldl_congr {as bs : Array α} (h₀ : as = bs) {f g : β → α → β} (h₁ : f = g)
|
||||
{a b : β} (h₂ : a = b) {start start' stop stop' : Nat} (h₃ : start = start') (h₄ : stop = stop') :
|
||||
as.foldl f a start stop = bs.foldl g b start' stop' := by
|
||||
congr
|
||||
|
||||
@[congr]
|
||||
theorem foldr_congr {as bs : Array α} (h₀ : as = bs) {f g : α → β → β} (h₁ : f = g)
|
||||
{a b : β} (h₂ : a = b) {start start' stop stop' : Nat} (h₃ : start = start') (h₄ : stop = stop') :
|
||||
as.foldr f a start stop = bs.foldr g b start' stop' := by
|
||||
congr
|
||||
|
||||
/-! ### map -/
|
||||
|
||||
@[simp] theorem mem_map {f : α → β} {l : Array α} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b := by
|
||||
simp only [mem_def, map_toList, List.mem_map]
|
||||
simp only [mem_def, toList_map, List.mem_map]
|
||||
|
||||
theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
|
||||
arr.mapM f = return mk (← arr.toList.mapM f) := by
|
||||
arr.mapM f = List.toArray <$> (arr.toList.mapM f) := by
|
||||
rw [mapM_eq_foldlM, foldlM_eq_foldlM_toList, ← List.foldrM_reverse]
|
||||
conv => rhs; rw [← List.reverse_reverse arr.toList]
|
||||
induction arr.toList.reverse with
|
||||
| nil => simp
|
||||
| cons a l ih => simp [ih]
|
||||
|
||||
@[simp] theorem toList_mapM [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
|
||||
toList <$> arr.mapM f = arr.toList.mapM f := by
|
||||
simp [mapM_eq_mapM_toList]
|
||||
|
||||
@[deprecated mapM_eq_mapM_toList (since := "2024-09-09")]
|
||||
abbrev mapM_eq_mapM_data := @mapM_eq_mapM_toList
|
||||
|
||||
@@ -779,16 +844,27 @@ theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Pro
|
||||
simpa using map_induction as f (fun _ => True) trivial p (by simp_all)
|
||||
|
||||
@[simp] theorem getElem_map (f : α → β) (as : Array α) (i : Nat) (h) :
|
||||
((as.map f)[i]) = f (as[i]'(size_map .. ▸ h)) := by
|
||||
(as.map f)[i] = f (as[i]'(size_map .. ▸ h)) := by
|
||||
have := map_spec as f (fun i b => b = f (as[i]))
|
||||
simp only [implies_true, true_implies] at this
|
||||
obtain ⟨eq, w⟩ := this
|
||||
apply w
|
||||
simp_all
|
||||
|
||||
@[simp] theorem getElem?_map (f : α → β) (as : Array α) (i : Nat) :
|
||||
(as.map f)[i]? = as[i]?.map f := by
|
||||
simp [getElem?_def]
|
||||
|
||||
@[simp] theorem map_push {f : α → β} {as : Array α} {x : α} :
|
||||
(as.push x).map f = (as.map f).push (f x) := by
|
||||
ext
|
||||
· simp
|
||||
· simp only [getElem_map, get_push, size_map]
|
||||
split <;> rfl
|
||||
|
||||
/-! ### mapIdx -/
|
||||
|
||||
-- This could also be prove from `SatisfiesM_mapIdxM`.
|
||||
-- This could also be proved from `SatisfiesM_mapIdxM` in Batteries.
|
||||
theorem mapIdx_induction (as : Array α) (f : Fin as.size → α → β)
|
||||
(motive : Nat → Prop) (h0 : motive 0)
|
||||
(p : Fin as.size → β → Prop)
|
||||
@@ -828,36 +904,41 @@ theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β)
|
||||
|
||||
@[simp] theorem getElem_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat)
|
||||
(h : i < (mapIdx a f).size) :
|
||||
haveI : i < a.size := by simp_all
|
||||
(a.mapIdx f)[i] = f ⟨i, this⟩ a[i] :=
|
||||
(a.mapIdx f)[i] = f ⟨i, by simp_all⟩ (a[i]'(by simp_all)) :=
|
||||
(mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
|
||||
|
||||
@[simp] theorem getElem?_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat) :
|
||||
(a.mapIdx f)[i]? =
|
||||
a[i]?.pbind fun b h => f ⟨i, (getElem?_eq_some_iff.1 h).1⟩ b := by
|
||||
simp only [getElem?_def, size_mapIdx, getElem_mapIdx]
|
||||
split <;> simp_all
|
||||
|
||||
/-! ### modify -/
|
||||
|
||||
@[simp] theorem size_modify (a : Array α) (i : Nat) (f : α → α) : (a.modify i f).size = a.size := by
|
||||
unfold modify modifyM Id.run
|
||||
split <;> simp
|
||||
|
||||
theorem getElem_modify {as : Array α} {x i} (h : i < as.size) :
|
||||
(as.modify x f)[i]'(by simp [h]) = if x = i then f as[i] else as[i] := by
|
||||
theorem getElem_modify {as : Array α} {x i} (h : i < (as.modify x f).size) :
|
||||
(as.modify x f)[i] = if x = i then f (as[i]'(by simpa using h)) else as[i]'(by simpa using h) := by
|
||||
simp only [modify, modifyM, get_eq_getElem, Id.run, Id.pure_eq]
|
||||
split
|
||||
· simp only [Id.bind_eq, get_set _ _ _ h]; split <;> simp [*]
|
||||
· rw [if_neg (mt (by rintro rfl; exact h) ‹_›)]
|
||||
· simp only [Id.bind_eq, get_set _ _ _ (by simpa using h)]; split <;> simp [*]
|
||||
· rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
|
||||
|
||||
theorem getElem_modify_self {as : Array α} {i : Nat} (h : i < as.size) (f : α → α) :
|
||||
(as.modify i f)[i]'(by simp [h]) = f as[i] := by
|
||||
theorem getElem_modify_self {as : Array α} {i : Nat} (f : α → α) (h : i < (as.modify i f).size) :
|
||||
(as.modify i f)[i] = f (as[i]'(by simpa using h)) := by
|
||||
simp [getElem_modify h]
|
||||
|
||||
theorem getElem_modify_of_ne {as : Array α} {i : Nat} (hj : j < as.size)
|
||||
(f : α → α) (h : i ≠ j) :
|
||||
(as.modify i f)[j]'(by rwa [size_modify]) = as[j] := by
|
||||
theorem getElem_modify_of_ne {as : Array α} {i : Nat} (h : i ≠ j)
|
||||
(f : α → α) (hj : j < (as.modify i f).size) :
|
||||
(as.modify i f)[j] = as[j]'(by simpa using hj) := by
|
||||
simp [getElem_modify hj, h]
|
||||
|
||||
@[deprecated getElem_modify (since := "2024-08-08")]
|
||||
theorem get_modify {arr : Array α} {x i} (h : i < arr.size) :
|
||||
(arr.modify x f).get ⟨i, by simp [h]⟩ =
|
||||
if x = i then f (arr.get ⟨i, h⟩) else arr.get ⟨i, h⟩ := by
|
||||
theorem get_modify {arr : Array α} {x i} (h : i < (arr.modify x f).size) :
|
||||
(arr.modify x f).get ⟨i, h⟩ =
|
||||
if x = i then f (arr.get ⟨i, by simpa using h⟩) else arr.get ⟨i, by simpa using h⟩ := by
|
||||
simp [getElem_modify h]
|
||||
|
||||
/-! ### filter -/
|
||||
@@ -887,6 +968,13 @@ abbrev filter_data := @toList_filter
|
||||
theorem mem_of_mem_filter {a : α} {l} (h : a ∈ filter p l) : a ∈ l :=
|
||||
(mem_filter.mp h).1
|
||||
|
||||
@[congr]
|
||||
theorem filter_congr {as bs : Array α} (h : as = bs)
|
||||
{f : α → Bool} {g : α → Bool} (h' : f = g) {start stop start' stop' : Nat}
|
||||
(h₁ : start = start') (h₂ : stop = stop') :
|
||||
filter f as start stop = filter g bs start' stop' := by
|
||||
congr
|
||||
|
||||
/-! ### filterMap -/
|
||||
|
||||
@[simp] theorem toList_filterMap (f : α → Option β) (l : Array α) :
|
||||
@@ -909,6 +997,13 @@ abbrev filterMap_data := @toList_filterMap
|
||||
b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b := by
|
||||
simp only [mem_def, toList_filterMap, List.mem_filterMap]
|
||||
|
||||
@[congr]
|
||||
theorem filterMap_congr {as bs : Array α} (h : as = bs)
|
||||
{f : α → Option β} {g : α → Option β} (h' : f = g) {start stop start' stop' : Nat}
|
||||
(h₁ : start = start') (h₂ : stop = stop') :
|
||||
filterMap f as start stop = filterMap g bs start' stop' := by
|
||||
congr
|
||||
|
||||
/-! ### empty -/
|
||||
|
||||
theorem size_empty : (#[] : Array α).size = 0 := rfl
|
||||
@@ -923,34 +1018,66 @@ abbrev empty_data := @toList_empty
|
||||
theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] := rfl
|
||||
|
||||
@[simp] theorem mem_append {a : α} {s t : Array α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
|
||||
simp only [mem_def, append_toList, List.mem_append]
|
||||
simp only [mem_def, toList_append, List.mem_append]
|
||||
|
||||
theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
|
||||
simp only [size, append_toList, List.length_append]
|
||||
@[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
|
||||
simp only [size, toList_append, List.length_append]
|
||||
|
||||
theorem get_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
|
||||
theorem getElem_append {as bs : Array α} (h : i < (as ++ bs).size) :
|
||||
(as ++ bs)[i] = if h' : i < as.size then as[i] else bs[i - as.size]'(by simp at h; omega) := by
|
||||
cases as; cases bs
|
||||
simp [List.getElem_append]
|
||||
|
||||
theorem getElem_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
|
||||
(as ++ bs)[i] = as[i] := by
|
||||
simp only [getElem_eq_getElem_toList]
|
||||
have h' : i < (as.toList ++ bs.toList).length := by rwa [← toList_length, append_toList] at h
|
||||
have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, toList_append] at h
|
||||
conv => rhs; rw [← List.getElem_append_left (bs := bs.toList) (h' := h')]
|
||||
apply List.get_of_eq; rw [append_toList]
|
||||
apply List.get_of_eq; rw [toList_append]
|
||||
|
||||
theorem get_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i)
|
||||
@[deprecated getElem_append_left (since := "2024-09-30")]
|
||||
abbrev get_append_left := @getElem_append_left
|
||||
|
||||
theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i)
|
||||
(hlt : i - as.size < bs.size := Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) :
|
||||
(as ++ bs)[i] = bs[i - as.size] := by
|
||||
simp only [getElem_eq_getElem_toList]
|
||||
have h' : i < (as.toList ++ bs.toList).length := by rwa [← toList_length, append_toList] at h
|
||||
have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, toList_append] at h
|
||||
conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
|
||||
apply List.get_of_eq; rw [append_toList]
|
||||
apply List.get_of_eq; rw [toList_append]
|
||||
|
||||
@[deprecated getElem_append_right (since := "2024-09-30")]
|
||||
abbrev get_append_right := @getElem_append_right
|
||||
|
||||
@[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by
|
||||
apply ext'; simp only [append_toList, toList_empty, List.append_nil]
|
||||
apply ext'; simp only [toList_append, toList_empty, List.append_nil]
|
||||
|
||||
@[simp] theorem nil_append (as : Array α) : #[] ++ as = as := by
|
||||
apply ext'; simp only [append_toList, toList_empty, List.nil_append]
|
||||
apply ext'; simp only [toList_append, toList_empty, List.nil_append]
|
||||
|
||||
theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) := by
|
||||
apply ext'; simp only [append_toList, List.append_assoc]
|
||||
apply ext'; simp only [toList_append, List.append_assoc]
|
||||
|
||||
/-! ### flatten -/
|
||||
|
||||
@[simp] theorem toList_flatten {l : Array (Array α)} : l.flatten.toList = (l.toList.map toList).join := by
|
||||
dsimp [flatten]
|
||||
simp only [foldl_eq_foldl_toList]
|
||||
generalize l.toList = l
|
||||
have : ∀ a : Array α, (List.foldl ?_ a l).toList = a.toList ++ ?_ := ?_
|
||||
exact this #[]
|
||||
induction l with
|
||||
| nil => simp
|
||||
| cons h => induction h.toList <;> simp [*]
|
||||
|
||||
theorem mem_flatten : ∀ {L : Array (Array α)}, a ∈ L.flatten ↔ ∃ l, l ∈ L ∧ a ∈ l := by
|
||||
simp only [mem_def, toList_flatten, List.mem_join, List.mem_map]
|
||||
intro l
|
||||
constructor
|
||||
· rintro ⟨_, ⟨s, m, rfl⟩, h⟩
|
||||
exact ⟨s, m, h⟩
|
||||
· rintro ⟨s, h₁, h₂⟩
|
||||
refine ⟨s.toList, ⟨⟨s, h₁, rfl⟩, h₂⟩⟩
|
||||
|
||||
/-! ### extract -/
|
||||
|
||||
@@ -1000,20 +1127,20 @@ theorem size_extract_loop (as bs : Array α) (size start : Nat) :
|
||||
simp [extract]; rw [size_extract_loop, size_empty, Nat.zero_add, Nat.sub_min_sub_right,
|
||||
Nat.min_assoc, Nat.min_self]
|
||||
|
||||
theorem get_extract_loop_lt_aux (as bs : Array α) (size start : Nat) (hlt : i < bs.size) :
|
||||
theorem getElem_extract_loop_lt_aux (as bs : Array α) (size start : Nat) (hlt : i < bs.size) :
|
||||
i < (extract.loop as size start bs).size := by
|
||||
rw [size_extract_loop]
|
||||
apply Nat.lt_of_lt_of_le hlt
|
||||
exact Nat.le_add_right ..
|
||||
|
||||
theorem get_extract_loop_lt (as bs : Array α) (size start : Nat) (hlt : i < bs.size)
|
||||
(h := get_extract_loop_lt_aux as bs size start hlt) :
|
||||
theorem getElem_extract_loop_lt (as bs : Array α) (size start : Nat) (hlt : i < bs.size)
|
||||
(h := getElem_extract_loop_lt_aux as bs size start hlt) :
|
||||
(extract.loop as size start bs)[i] = bs[i] := by
|
||||
apply Eq.trans _ (get_append_left (bs:=extract.loop as size start #[]) hlt)
|
||||
apply Eq.trans _ (getElem_append_left (bs:=extract.loop as size start #[]) hlt)
|
||||
· rw [size_append]; exact Nat.lt_of_lt_of_le hlt (Nat.le_add_right ..)
|
||||
· congr; rw [extract_loop_eq_aux]
|
||||
|
||||
theorem get_extract_loop_ge_aux (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
|
||||
theorem getElem_extract_loop_ge_aux (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
|
||||
(h : i < (extract.loop as size start bs).size) : start + i - bs.size < as.size := by
|
||||
have h : i < bs.size + (as.size - start) := by
|
||||
apply Nat.lt_of_lt_of_le h
|
||||
@@ -1024,9 +1151,9 @@ theorem get_extract_loop_ge_aux (as bs : Array α) (size start : Nat) (hge : i
|
||||
apply Nat.add_lt_of_lt_sub'
|
||||
exact Nat.sub_lt_left_of_lt_add hge h
|
||||
|
||||
theorem get_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
|
||||
theorem getElem_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
|
||||
(h : i < (extract.loop as size start bs).size)
|
||||
(h' := get_extract_loop_ge_aux as bs size start hge h) :
|
||||
(h' := getElem_extract_loop_ge_aux as bs size start hge h) :
|
||||
(extract.loop as size start bs)[i] = as[start + i - bs.size] := by
|
||||
induction size using Nat.recAux generalizing start bs with
|
||||
| zero =>
|
||||
@@ -1048,28 +1175,37 @@ theorem get_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i ≥ b
|
||||
have h₂ : bs.size < (extract.loop as size (start+1) (bs.push as[start])).size := by
|
||||
rw [size_extract_loop]; apply Nat.lt_of_lt_of_le h₁; exact Nat.le_add_right ..
|
||||
have h : (extract.loop as size (start + 1) (push bs as[start]))[bs.size] = as[start] := by
|
||||
rw [get_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, get_push_eq]
|
||||
rw [getElem_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, get_push_eq]
|
||||
rw [h]; congr; rw [Nat.add_sub_cancel]
|
||||
else
|
||||
have hge : bs.size + 1 ≤ i := Nat.lt_of_le_of_ne hge hi
|
||||
rw [ih (bs.push as[start]) (start+1) ((size_push ..).symm ▸ hge)]
|
||||
congr 1; rw [size_push, Nat.add_right_comm, Nat.add_sub_add_right]
|
||||
|
||||
theorem get_extract_aux {as : Array α} {start stop : Nat} (h : i < (as.extract start stop).size) :
|
||||
theorem getElem_extract_aux {as : Array α} {start stop : Nat} (h : i < (as.extract start stop).size) :
|
||||
start + i < as.size := by
|
||||
rw [size_extract] at h; apply Nat.add_lt_of_lt_sub'; apply Nat.lt_of_lt_of_le h
|
||||
apply Nat.sub_le_sub_right; apply Nat.min_le_right
|
||||
|
||||
@[simp] theorem get_extract {as : Array α} {start stop : Nat}
|
||||
@[simp] theorem getElem_extract {as : Array α} {start stop : Nat}
|
||||
(h : i < (as.extract start stop).size) :
|
||||
(as.extract start stop)[i] = as[start + i]'(get_extract_aux h) :=
|
||||
(as.extract start stop)[i] = as[start + i]'(getElem_extract_aux h) :=
|
||||
show (extract.loop as (min stop as.size - start) start #[])[i]
|
||||
= as[start + i]'(get_extract_aux h) by rw [get_extract_loop_ge]; rfl; exact Nat.zero_le _
|
||||
= as[start + i]'(getElem_extract_aux h) by rw [getElem_extract_loop_ge]; rfl; exact Nat.zero_le _
|
||||
|
||||
theorem getElem?_extract {as : Array α} {start stop : Nat} :
|
||||
(as.extract start stop)[i]? = if i < min stop as.size - start then as[start + i]? else none := by
|
||||
simp only [getElem?_def, size_extract, getElem_extract]
|
||||
split
|
||||
· split
|
||||
· rfl
|
||||
· omega
|
||||
· rfl
|
||||
|
||||
@[simp] theorem extract_all (as : Array α) : as.extract 0 as.size = as := by
|
||||
apply ext
|
||||
· rw [size_extract, Nat.min_self, Nat.sub_zero]
|
||||
· intros; rw [get_extract]; congr; rw [Nat.zero_add]
|
||||
· intros; rw [getElem_extract]; congr; rw [Nat.zero_add]
|
||||
|
||||
theorem extract_empty_of_stop_le_start (as : Array α) {start stop : Nat} (h : stop ≤ start) :
|
||||
as.extract start stop = #[] := by
|
||||
@@ -1151,9 +1287,12 @@ theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
|
||||
theorem any_eq_true {p : α → Bool} {as : Array α} :
|
||||
any as p ↔ ∃ i : Fin as.size, p as[i] := by simp [any_iff_exists, Fin.isLt]
|
||||
|
||||
theorem any_def {p : α → Bool} (as : Array α) : as.any p = as.toList.any p := by
|
||||
theorem any_toList {p : α → Bool} (as : Array α) : as.toList.any p = as.any p := by
|
||||
rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]; simp only [List.mem_iff_get]
|
||||
exact ⟨fun ⟨i, h⟩ => ⟨_, ⟨i, rfl⟩, h⟩, fun ⟨_, ⟨i, rfl⟩, h⟩ => ⟨i, h⟩⟩
|
||||
exact ⟨fun ⟨_, ⟨i, rfl⟩, h⟩ => ⟨i, h⟩, fun ⟨i, h⟩ => ⟨_, ⟨i, rfl⟩, h⟩⟩
|
||||
|
||||
@[deprecated "Use the reverse direction of `Array.any_toList`" (since := "2024-09-30")]
|
||||
abbrev any_def := @any_toList
|
||||
|
||||
/-! ### all -/
|
||||
|
||||
@@ -1185,22 +1324,25 @@ theorem all_iff_forall {p : α → Bool} {as : Array α} {start stop} :
|
||||
theorem all_eq_true {p : α → Bool} {as : Array α} : all as p ↔ ∀ i : Fin as.size, p as[i] := by
|
||||
simp [all_iff_forall, Fin.isLt]
|
||||
|
||||
theorem all_def {p : α → Bool} (as : Array α) : as.all p = as.toList.all p := by
|
||||
theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all p := by
|
||||
rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]; simp only [List.mem_iff_getElem]
|
||||
constructor
|
||||
· intro w i
|
||||
exact w as[i] ⟨i, i.2, (getElem_eq_getElem_toList i.2).symm⟩
|
||||
· rintro w x ⟨r, h, rfl⟩
|
||||
rw [← getElem_eq_getElem_toList]
|
||||
exact w ⟨r, h⟩
|
||||
· intro w i
|
||||
exact w as[i] ⟨i, i.2, (getElem_eq_getElem_toList i.2).symm⟩
|
||||
|
||||
@[deprecated "Use the reverse direction of `Array.all_toList`" (since := "2024-09-30")]
|
||||
abbrev all_def := @all_toList
|
||||
|
||||
theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by
|
||||
simp only [all_def, List.all_eq_true, mem_def]
|
||||
simp only [← all_toList, List.all_eq_true, mem_def]
|
||||
|
||||
/-! ### contains -/
|
||||
|
||||
theorem contains_def [DecidableEq α] {a : α} {as : Array α} : as.contains a ↔ a ∈ as := by
|
||||
rw [mem_def, contains, any_def, List.any_eq_true]; simp [and_comm]
|
||||
rw [mem_def, contains, ← any_toList, List.any_eq_true]; simp [and_comm]
|
||||
|
||||
instance [DecidableEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
|
||||
decidable_of_iff _ contains_def
|
||||
@@ -1209,12 +1351,12 @@ instance [DecidableEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
|
||||
|
||||
open Fin
|
||||
|
||||
@[simp] theorem get_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.val] = a[i] :=
|
||||
@[simp] theorem getElem_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.val] = a[i] :=
|
||||
by simp only [swap, fin_cast_val, get_eq_getElem, getElem_set_eq, getElem_fin]
|
||||
|
||||
@[simp] theorem get_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.val] = a[j] :=
|
||||
@[simp] theorem getElem_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.val] = a[j] :=
|
||||
if he : ((Array.size_set _ _ _).symm ▸ j).val = i.val then by
|
||||
simp only [←he, fin_cast_val, get_swap_right, getElem_fin]
|
||||
simp only [←he, fin_cast_val, getElem_swap_right, getElem_fin]
|
||||
else by
|
||||
apply Eq.trans
|
||||
· apply Array.get_set_ne
|
||||
@@ -1222,7 +1364,7 @@ open Fin
|
||||
· assumption
|
||||
· simp [get_set_ne]
|
||||
|
||||
@[simp] theorem get_swap_of_ne (a : Array α) {i j : Fin a.size} (hp : p < a.size)
|
||||
@[simp] theorem getElem_swap_of_ne (a : Array α) {i j : Fin a.size} (hp : p < a.size)
|
||||
(hi : p ≠ i) (hj : p ≠ j) : (a.swap i j)[p]'(a.size_swap .. |>.symm ▸ hp) = a[p] := by
|
||||
apply Eq.trans
|
||||
· have : ((a.size_set i (a.get j)).symm ▸ j).val = j.val := by simp only [fin_cast_val]
|
||||
@@ -1234,22 +1376,22 @@ open Fin
|
||||
· apply Ne.symm
|
||||
· assumption
|
||||
|
||||
theorem get_swap (a : Array α) (i j : Fin a.size) (k : Nat) (hk: k < a.size) :
|
||||
theorem getElem_swap' (a : Array α) (i j : Fin a.size) (k : Nat) (hk : k < a.size) :
|
||||
(a.swap i j)[k]'(by simp_all) = if k = i then a[j] else if k = j then a[i] else a[k] := by
|
||||
split
|
||||
· simp_all only [get_swap_left]
|
||||
· simp_all only [getElem_swap_left]
|
||||
· split <;> simp_all
|
||||
|
||||
theorem get_swap' (a : Array α) (i j : Fin a.size) (k : Nat) (hk' : k < (a.swap i j).size) :
|
||||
theorem getElem_swap (a : Array α) (i j : Fin a.size) (k : Nat) (hk : k < (a.swap i j).size) :
|
||||
(a.swap i j)[k] = if k = i then a[j] else if k = j then a[i] else a[k]'(by simp_all) := by
|
||||
apply get_swap
|
||||
apply getElem_swap'
|
||||
|
||||
@[simp] theorem swap_swap (a : Array α) {i j : Fin a.size} :
|
||||
(a.swap i j).swap ⟨i.1, (a.size_swap ..).symm ▸i.2⟩ ⟨j.1, (a.size_swap ..).symm ▸j.2⟩ = a := by
|
||||
apply ext
|
||||
· simp only [size_swap]
|
||||
· intros
|
||||
simp only [get_swap']
|
||||
simp only [getElem_swap]
|
||||
split
|
||||
· simp_all
|
||||
· split <;> simp_all
|
||||
@@ -1258,11 +1400,35 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
|
||||
apply ext
|
||||
· simp only [size_swap]
|
||||
· intros
|
||||
simp only [get_swap']
|
||||
simp only [getElem_swap]
|
||||
split
|
||||
· split <;> simp_all
|
||||
· split <;> simp_all
|
||||
|
||||
@[deprecated getElem_extract_loop_lt_aux (since := "2024-09-30")]
|
||||
abbrev get_extract_loop_lt_aux := @getElem_extract_loop_lt_aux
|
||||
@[deprecated getElem_extract_loop_lt (since := "2024-09-30")]
|
||||
abbrev get_extract_loop_lt := @getElem_extract_loop_lt
|
||||
@[deprecated getElem_extract_loop_ge_aux (since := "2024-09-30")]
|
||||
abbrev get_extract_loop_ge_aux := @getElem_extract_loop_ge_aux
|
||||
@[deprecated getElem_extract_loop_ge (since := "2024-09-30")]
|
||||
abbrev get_extract_loop_ge := @getElem_extract_loop_ge
|
||||
@[deprecated getElem_extract_aux (since := "2024-09-30")]
|
||||
abbrev get_extract_aux := @getElem_extract_aux
|
||||
@[deprecated getElem_extract (since := "2024-09-30")]
|
||||
abbrev get_extract := @getElem_extract
|
||||
|
||||
@[deprecated getElem_swap_right (since := "2024-09-30")]
|
||||
abbrev get_swap_right := @getElem_swap_right
|
||||
@[deprecated getElem_swap_left (since := "2024-09-30")]
|
||||
abbrev get_swap_left := @getElem_swap_left
|
||||
@[deprecated getElem_swap_of_ne (since := "2024-09-30")]
|
||||
abbrev get_swap_of_ne := @getElem_swap_of_ne
|
||||
@[deprecated getElem_swap (since := "2024-09-30")]
|
||||
abbrev get_swap := @getElem_swap
|
||||
@[deprecated getElem_swap' (since := "2024-09-30")]
|
||||
abbrev get_swap' := @getElem_swap'
|
||||
|
||||
end Array
|
||||
|
||||
|
||||
@@ -1279,9 +1445,6 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
|
||||
@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
|
||||
simp [mem_def]
|
||||
|
||||
@[simp] theorem getElem?_toArray (l : List α) (i : Nat) : l.toArray[i]? = l[i]? := by
|
||||
simp [getElem?_eq_getElem?_toList]
|
||||
|
||||
@[simp] theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse := by
|
||||
simp
|
||||
|
||||
@@ -1331,19 +1494,45 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
|
||||
· simp
|
||||
· simp_all [List.set_eq_of_length_le]
|
||||
|
||||
@[simp] theorem anyM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
|
||||
theorem anyM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
|
||||
l.toArray.anyM p = l.anyM p := by
|
||||
rw [← anyM_toList]
|
||||
|
||||
@[simp] theorem any_toArray (p : α → Bool) (l : List α) : l.toArray.any p = l.any p := by
|
||||
rw [Array.any_def]
|
||||
theorem any_toArray (p : α → Bool) (l : List α) : l.toArray.any p = l.any p := by
|
||||
rw [any_toList]
|
||||
|
||||
@[simp] theorem allM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
|
||||
theorem allM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
|
||||
l.toArray.allM p = l.allM p := by
|
||||
rw [← allM_toList]
|
||||
|
||||
@[simp] theorem all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p := by
|
||||
rw [Array.all_def]
|
||||
theorem all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p := by
|
||||
rw [all_toList]
|
||||
|
||||
/-- Variant of `anyM_toArray` with a side condition on `stop`. -/
|
||||
@[simp] theorem anyM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
|
||||
(h : stop = l.toArray.size) :
|
||||
l.toArray.anyM p 0 stop = l.anyM p := by
|
||||
subst h
|
||||
rw [← anyM_toList]
|
||||
|
||||
/-- Variant of `any_toArray` with a side condition on `stop`. -/
|
||||
@[simp] theorem any_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
|
||||
l.toArray.any p 0 stop = l.any p := by
|
||||
subst h
|
||||
rw [any_toList]
|
||||
|
||||
/-- Variant of `allM_toArray` with a side condition on `stop`. -/
|
||||
@[simp] theorem allM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
|
||||
(h : stop = l.toArray.size) :
|
||||
l.toArray.allM p 0 stop = l.allM p := by
|
||||
subst h
|
||||
rw [← allM_toList]
|
||||
|
||||
/-- Variant of `all_toArray` with a side condition on `stop`. -/
|
||||
@[simp] theorem all_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
|
||||
l.toArray.all p 0 stop = l.all p := by
|
||||
subst h
|
||||
rw [all_toList]
|
||||
|
||||
@[simp] theorem swap_toArray (l : List α) (i j : Fin l.toArray.size) :
|
||||
l.toArray.swap i j = ((l.set i l[j]).set j l[i]).toArray := by
|
||||
@@ -1358,21 +1547,30 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
|
||||
apply ext'
|
||||
simp
|
||||
|
||||
@[simp] theorem filter_toArray (p : α → Bool) (l : List α) :
|
||||
@[simp] theorem filter_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
|
||||
l.toArray.filter p 0 stop = (l.filter p).toArray := by
|
||||
subst h
|
||||
apply ext'
|
||||
rw [toList_filter]
|
||||
|
||||
@[simp] theorem filterMap_toArray' (f : α → Option β) (l : List α) (h : stop = l.toArray.size) :
|
||||
l.toArray.filterMap f 0 stop = (l.filterMap f).toArray := by
|
||||
subst h
|
||||
apply ext'
|
||||
rw [toList_filterMap]
|
||||
|
||||
theorem filter_toArray (p : α → Bool) (l : List α) :
|
||||
l.toArray.filter p = (l.filter p).toArray := by
|
||||
apply ext'
|
||||
erw [toList_filter] -- `erw` required to unify `l.length` with `l.toArray.size`.
|
||||
|
||||
@[simp] theorem filterMap_toArray (f : α → Option β) (l : List α) :
|
||||
l.toArray.filterMap f = (l.filterMap f).toArray := by
|
||||
apply ext'
|
||||
erw [toList_filterMap] -- `erw` required to unify `l.length` with `l.toArray.size`.
|
||||
|
||||
@[simp] theorem append_toArray (l₁ l₂ : List α) :
|
||||
l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
|
||||
apply ext'
|
||||
simp
|
||||
|
||||
theorem filterMap_toArray (f : α → Option β) (l : List α) :
|
||||
l.toArray.filterMap f = (l.filterMap f).toArray := by
|
||||
simp
|
||||
|
||||
@[simp] theorem flatten_toArray (l : List (List α)) : (l.toArray.map List.toArray).flatten = l.join.toArray := by
|
||||
apply ext'
|
||||
simp [Function.comp_def]
|
||||
|
||||
@[simp] theorem toArray_range (n : Nat) : (range n).toArray = Array.range n := by
|
||||
apply ext'
|
||||
simp
|
||||
|
||||
@@ -164,6 +164,17 @@ theorem getLsbD_add {i : Nat} (i_lt : i < w) (x y : BitVec w) :
|
||||
(getLsbD x i ^^ (getLsbD y i ^^ carry i x y false)) := by
|
||||
simpa using getLsbD_add_add_bool i_lt x y false
|
||||
|
||||
theorem getElem_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool) :
|
||||
(x + y + setWidth w (ofBool c))[i] =
|
||||
(x[i] ^^ (y[i] ^^ carry i x y c)) := by
|
||||
simp only [← getLsbD_eq_getElem]
|
||||
rw [getLsbD_add_add_bool]
|
||||
omega
|
||||
|
||||
theorem getElem_add {i : Nat} (i_lt : i < w) (x y : BitVec w) :
|
||||
(x + y)[i] = (x[i] ^^ (y[i] ^^ carry i x y false)) := by
|
||||
simpa using getElem_add_add_bool i_lt x y false
|
||||
|
||||
theorem adc_spec (x y : BitVec w) (c : Bool) :
|
||||
adc x y c = (carry w x y c, x + y + setWidth w (ofBool c)) := by
|
||||
simp only [adc]
|
||||
@@ -368,6 +379,10 @@ theorem getLsbD_mul (x y : BitVec w) (i : Nat) :
|
||||
· simp
|
||||
· omega
|
||||
|
||||
theorem getElem_mul {x y : BitVec w} {i : Nat} (h : i < w) :
|
||||
(x * y)[i] = (mulRec x y w)[i] := by
|
||||
simp [mulRec_eq_mul_signExtend_setWidth]
|
||||
|
||||
/-! ## shiftLeft recurrence for bitblasting -/
|
||||
|
||||
/--
|
||||
|
||||
@@ -463,6 +463,16 @@ theorem toInt_pos_iff {w : Nat} {x : BitVec w} :
|
||||
0 ≤ BitVec.toInt x ↔ 2 * x.toNat < 2 ^ w := by
|
||||
simp [toInt_eq_toNat_cond]; omega
|
||||
|
||||
theorem eq_zero_or_eq_one (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by
|
||||
obtain ⟨a, ha⟩ := a
|
||||
simp only [Nat.reducePow]
|
||||
have acases : a = 0 ∨ a = 1 := by omega
|
||||
rcases acases with ⟨rfl | rfl⟩
|
||||
· simp
|
||||
· case inr h =>
|
||||
subst h
|
||||
simp
|
||||
|
||||
/-! ### setWidth, zeroExtend and truncate -/
|
||||
|
||||
@[simp]
|
||||
@@ -525,6 +535,7 @@ theorem getElem_setWidth' (x : BitVec w) (i : Nat) (h : w ≤ v) (hi : i < v) :
|
||||
(setWidth' h x)[i] = x.getLsbD i := by
|
||||
rw [getElem_eq_testBit_toNat, toNat_setWidth', getLsbD]
|
||||
|
||||
@[simp]
|
||||
theorem getElem_setWidth (m : Nat) (x : BitVec n) (i : Nat) (h : i < m) :
|
||||
(setWidth m x)[i] = x.getLsbD i := by
|
||||
rw [setWidth]
|
||||
@@ -1909,6 +1920,11 @@ theorem shiftLeft_add_distrib {x y : BitVec w} {n : Nat} :
|
||||
case succ n ih =>
|
||||
simp [ih, toNat_eq, Nat.shiftLeft_eq, ← Nat.add_mul]
|
||||
|
||||
theorem add_eq_xor {a b : BitVec 1} : a + b = a ^^^ b := by
|
||||
have ha : a = 0 ∨ a = 1 := eq_zero_or_eq_one _
|
||||
have hb : b = 0 ∨ b = 1 := eq_zero_or_eq_one _
|
||||
rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp [h, h']))
|
||||
|
||||
/-! ### sub/neg -/
|
||||
|
||||
theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toNat) := by rfl
|
||||
@@ -2018,6 +2034,11 @@ theorem neg_ne_iff_ne_neg {x y : BitVec w} : -x ≠ y ↔ x ≠ -y := by
|
||||
subst h'
|
||||
simp at h
|
||||
|
||||
theorem sub_eq_xor {a b : BitVec 1} : a - b = a ^^^ b := by
|
||||
have ha : a = 0 ∨ a = 1 := eq_zero_or_eq_one _
|
||||
have hb : b = 0 ∨ b = 1 := eq_zero_or_eq_one _
|
||||
rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp [h, h']))
|
||||
|
||||
/-! ### abs -/
|
||||
|
||||
@[simp, bv_toNat]
|
||||
@@ -2085,6 +2106,11 @@ theorem ofInt_mul {n} (x y : Int) : BitVec.ofInt n (x * y) =
|
||||
apply eq_of_toInt_eq
|
||||
simp
|
||||
|
||||
theorem mul_eq_and {a b : BitVec 1} : a * b = a &&& b := by
|
||||
have ha : a = 0 ∨ a = 1 := eq_zero_or_eq_one _
|
||||
have hb : b = 0 ∨ b = 1 := eq_zero_or_eq_one _
|
||||
rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp [h, h']))
|
||||
|
||||
/-! ### le and lt -/
|
||||
|
||||
@[bv_toNat] theorem le_def {x y : BitVec n} :
|
||||
@@ -2260,6 +2286,12 @@ theorem getLsbD_rotateLeft {x : BitVec w} {r i : Nat} :
|
||||
· simp
|
||||
· rw [← rotateLeft_mod_eq_rotateLeft, getLsbD_rotateLeft_of_le (Nat.mod_lt _ (by omega))]
|
||||
|
||||
@[simp]
|
||||
theorem getElem_rotateLeft {x : BitVec w} {r i : Nat} (h : i < w) :
|
||||
(x.rotateLeft r)[i] =
|
||||
if h' : i < r % w then x[(w - (r % w) + i)] else x[i - (r % w)] := by
|
||||
simp [← BitVec.getLsbD_eq_getElem, h]
|
||||
|
||||
/-! ## Rotate Right -/
|
||||
|
||||
/--
|
||||
@@ -2341,6 +2373,12 @@ theorem getLsbD_rotateRight {x : BitVec w} {r i : Nat} :
|
||||
· simp
|
||||
· rw [← rotateRight_mod_eq_rotateRight, getLsbD_rotateRight_of_le (Nat.mod_lt _ (by omega))]
|
||||
|
||||
@[simp]
|
||||
theorem getElem_rotateRight {x : BitVec w} {r i : Nat} (h : i < w) :
|
||||
(x.rotateRight r)[i] = if h' : i < w - (r % w) then x[(r % w) + i] else x[(i - (w - (r % w)))] := by
|
||||
simp only [← BitVec.getLsbD_eq_getElem]
|
||||
simp [getLsbD_rotateRight, h]
|
||||
|
||||
/- ## twoPow -/
|
||||
|
||||
@[simp, bv_toNat]
|
||||
@@ -2369,6 +2407,12 @@ theorem getLsbD_twoPow (i j : Nat) : (twoPow w i).getLsbD j = ((i < w) && (i = j
|
||||
simp at hi
|
||||
simp_all
|
||||
|
||||
@[simp]
|
||||
theorem getElem_twoPow {i j : Nat} (h : j < w) : (twoPow w i)[j] = decide (j = i) := by
|
||||
rw [←getLsbD_eq_getElem, getLsbD_twoPow]
|
||||
simp [eq_comm]
|
||||
omega
|
||||
|
||||
theorem and_twoPow (x : BitVec w) (i : Nat) :
|
||||
x &&& (twoPow w i) = if x.getLsbD i then twoPow w i else 0#w := by
|
||||
ext j
|
||||
@@ -2400,6 +2444,10 @@ theorem twoPow_zero {w : Nat} : twoPow w 0 = 1#w := by
|
||||
theorem getLsbD_one {w i : Nat} : (1#w).getLsbD i = (decide (0 < w) && decide (0 = i)) := by
|
||||
rw [← twoPow_zero, getLsbD_twoPow]
|
||||
|
||||
@[simp]
|
||||
theorem getElem_one {w i : Nat} (h : i < w) : (1#w)[i] = decide (i = 0) := by
|
||||
rw [← twoPow_zero, getElem_twoPow]
|
||||
|
||||
theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
|
||||
x <<< n = x * (BitVec.twoPow w n) := by
|
||||
ext i
|
||||
@@ -2504,6 +2552,12 @@ theorem getLsbD_replicate {n w : Nat} (x : BitVec w) :
|
||||
simp only [show ¬i < w * n by omega, decide_False, cond_false, hi, Bool.false_and]
|
||||
apply BitVec.getLsbD_ge (x := x) (i := i - w * n) (ge := by omega)
|
||||
|
||||
@[simp]
|
||||
theorem getElem_replicate {n w : Nat} (x : BitVec w) (h : i < w * n) :
|
||||
(x.replicate n)[i] = if h' : w = 0 then false else x[i % w]'(@Nat.mod_lt i w (by omega)) := by
|
||||
simp only [← getLsbD_eq_getElem, getLsbD_replicate]
|
||||
by_cases h' : w = 0 <;> simp [h'] <;> omega
|
||||
|
||||
/-! ### intMin -/
|
||||
|
||||
/-- The bitvector of width `w` that has the smallest value when interpreted as an integer. -/
|
||||
|
||||
@@ -245,7 +245,7 @@ On an invalid position, returns `(default : UInt8)`. -/
|
||||
@[inline]
|
||||
def curr : Iterator → UInt8
|
||||
| ⟨arr, i⟩ =>
|
||||
if h:i < arr.size then
|
||||
if h : i < arr.size then
|
||||
arr[i]'h
|
||||
else
|
||||
default
|
||||
|
||||
@@ -582,8 +582,8 @@ theorem rev_succ (k : Fin n) : rev (succ k) = castSucc (rev k) := k.rev_addNat 1
|
||||
@[simp] theorem coe_pred (j : Fin (n + 1)) (h : j ≠ 0) : (j.pred h : Nat) = j - 1 := rfl
|
||||
|
||||
@[simp] theorem succ_pred : ∀ (i : Fin (n + 1)) (h : i ≠ 0), (i.pred h).succ = i
|
||||
| ⟨0, h⟩, hi => by simp only [mk_zero, ne_eq, not_true] at hi
|
||||
| ⟨n + 1, h⟩, hi => rfl
|
||||
| ⟨0, _⟩, hi => by simp only [mk_zero, ne_eq, not_true] at hi
|
||||
| ⟨_ + 1, _⟩, _ => rfl
|
||||
|
||||
@[simp]
|
||||
theorem pred_succ (i : Fin n) {h : i.succ ≠ 0} : i.succ.pred h = i := by
|
||||
|
||||
@@ -73,33 +73,33 @@ instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b
|
||||
|
||||
@[extern "lean_float_to_string"] opaque Float.toString : Float → String
|
||||
/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
|
||||
If negative or NaN, returns 0.
|
||||
If larger than the maximum value for UInt8 (including Inf), returns maximum value of UInt8
|
||||
(i.e. UInt8.size - 1).
|
||||
If negative or NaN, returns `0`.
|
||||
If larger than the maximum value for `UInt8` (including Inf), returns the maximum value of `UInt8`
|
||||
(i.e. `UInt8.size - 1`).
|
||||
-/
|
||||
@[extern "lean_float_to_uint8"] opaque Float.toUInt8 : Float → UInt8
|
||||
/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
|
||||
If negative or NaN, returns 0.
|
||||
If larger than the maximum value for UInt16 (including Inf), returns maximum value of UInt16
|
||||
(i.e. UInt16.size - 1).
|
||||
If negative or NaN, returns `0`.
|
||||
If larger than the maximum value for `UInt16` (including Inf), returns the maximum value of `UInt16`
|
||||
(i.e. `UInt16.size - 1`).
|
||||
-/
|
||||
@[extern "lean_float_to_uint16"] opaque Float.toUInt16 : Float → UInt16
|
||||
/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
|
||||
If negative or NaN, returns 0.
|
||||
If larger than the maximum value for UInt32 (including Inf), returns maximum value of UInt32
|
||||
(i.e. UInt32.size - 1).
|
||||
If negative or NaN, returns `0`.
|
||||
If larger than the maximum value for `UInt32` (including Inf), returns the maximum value of `UInt32`
|
||||
(i.e. `UInt32.size - 1`).
|
||||
-/
|
||||
@[extern "lean_float_to_uint32"] opaque Float.toUInt32 : Float → UInt32
|
||||
/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
|
||||
If negative or NaN, returns 0.
|
||||
If larger than the maximum value for UInt64 (including Inf), returns maximum value of UInt64
|
||||
(i.e. UInt64.size - 1).
|
||||
If negative or NaN, returns `0`.
|
||||
If larger than the maximum value for `UInt64` (including Inf), returns the maximum value of `UInt64`
|
||||
(i.e. `UInt64.size - 1`).
|
||||
-/
|
||||
@[extern "lean_float_to_uint64"] opaque Float.toUInt64 : Float → UInt64
|
||||
/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
|
||||
If negative or NaN, returns 0.
|
||||
If larger than the maximum value for USize (including Inf), returns maximum value of USize
|
||||
(i.e. USize.size - 1; Note that this value is platform dependent).
|
||||
If negative or NaN, returns `0`.
|
||||
If larger than the maximum value for `USize` (including Inf), returns the maximum value of `USize`
|
||||
(i.e. `USize.size - 1`). This value is platform dependent).
|
||||
-/
|
||||
@[extern "lean_float_to_usize"] opaque Float.toUSize : Float → USize
|
||||
|
||||
|
||||
@@ -253,7 +253,7 @@ theorem tmod_def (a b : Int) : tmod a b = a - b * a.tdiv b := by
|
||||
|
||||
theorem fmod_add_fdiv : ∀ a b : Int, a.fmod b + b * a.fdiv b = a
|
||||
| 0, ofNat _ | 0, -[_+1] => congrArg ofNat <| by simp
|
||||
| succ m, ofNat n => congrArg ofNat <| Nat.mod_add_div ..
|
||||
| succ _, ofNat _ => congrArg ofNat <| Nat.mod_add_div ..
|
||||
| succ m, -[n+1] => by
|
||||
show subNatNat (m % succ n) n + (↑(succ n * (m / succ n)) + n + 1) = (m + 1)
|
||||
rw [Int.add_comm _ n, ← Int.add_assoc, ← Int.add_assoc,
|
||||
@@ -289,8 +289,8 @@ theorem fmod_eq_tmod {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fmod a b = tmod
|
||||
|
||||
@[simp] protected theorem ediv_neg : ∀ a b : Int, a / (-b) = -(a / b)
|
||||
| ofNat m, 0 => show ofNat (m / 0) = -↑(m / 0) by rw [Nat.div_zero]; rfl
|
||||
| ofNat m, -[n+1] => (Int.neg_neg _).symm
|
||||
| ofNat m, succ n | -[m+1], 0 | -[m+1], succ n | -[m+1], -[n+1] => rfl
|
||||
| ofNat _, -[_+1] => (Int.neg_neg _).symm
|
||||
| ofNat _, succ _ | -[_+1], 0 | -[_+1], succ _ | -[_+1], -[_+1] => rfl
|
||||
|
||||
theorem ediv_neg' {a b : Int} (Ha : a < 0) (Hb : 0 < b) : a / b < 0 :=
|
||||
match a, b, eq_negSucc_of_lt_zero Ha, eq_succ_of_zero_lt Hb with
|
||||
@@ -339,7 +339,7 @@ theorem add_mul_ediv_right (a b : Int) {c : Int} (H : c ≠ 0) : (a + b * c) / c
|
||||
| _, ⟨k, rfl⟩, -[n+1] => show (a - n.succ * k.succ).ediv k.succ = a.ediv k.succ - n.succ by
|
||||
rw [← Int.add_sub_cancel (ediv ..), ← this, Int.sub_add_cancel]
|
||||
fun {k n} => @fun
|
||||
| ofNat m => congrArg ofNat <| Nat.add_mul_div_right _ _ k.succ_pos
|
||||
| ofNat _ => congrArg ofNat <| Nat.add_mul_div_right _ _ k.succ_pos
|
||||
| -[m+1] => by
|
||||
show ((n * k.succ : Nat) - m.succ : Int).ediv k.succ = n - (m / k.succ + 1 : Nat)
|
||||
by_cases h : m < n * k.succ
|
||||
@@ -396,7 +396,7 @@ theorem add_mul_ediv_left (a : Int) {b : Int}
|
||||
rw [Int.mul_neg, Int.ediv_neg, Int.ediv_neg]; apply congrArg Neg.neg; apply this
|
||||
fun m k b =>
|
||||
match b, k with
|
||||
| ofNat n, k => congrArg ofNat (Nat.mul_div_mul_left _ _ m.succ_pos)
|
||||
| ofNat _, _ => congrArg ofNat (Nat.mul_div_mul_left _ _ m.succ_pos)
|
||||
| -[n+1], 0 => by
|
||||
rw [Int.ofNat_zero, Int.mul_zero, Int.ediv_zero, Int.ediv_zero]
|
||||
| -[n+1], succ k => congrArg negSucc <|
|
||||
@@ -822,14 +822,14 @@ theorem ediv_eq_ediv_of_mul_eq_mul {a b c d : Int}
|
||||
unseal Nat.div in
|
||||
@[simp] protected theorem tdiv_neg : ∀ a b : Int, a.tdiv (-b) = -(a.tdiv b)
|
||||
| ofNat m, 0 => show ofNat (m / 0) = -↑(m / 0) by rw [Nat.div_zero]; rfl
|
||||
| ofNat m, -[n+1] | -[m+1], succ n => (Int.neg_neg _).symm
|
||||
| ofNat m, succ n | -[m+1], 0 | -[m+1], -[n+1] => rfl
|
||||
| ofNat _, -[_+1] | -[_+1], succ _ => (Int.neg_neg _).symm
|
||||
| ofNat _, succ _ | -[_+1], 0 | -[_+1], -[_+1] => rfl
|
||||
|
||||
unseal Nat.div in
|
||||
@[simp] protected theorem neg_tdiv : ∀ a b : Int, (-a).tdiv b = -(a.tdiv b)
|
||||
| 0, n => by simp [Int.neg_zero]
|
||||
| succ m, (n:Nat) | -[m+1], 0 | -[m+1], -[n+1] => rfl
|
||||
| succ m, -[n+1] | -[m+1], succ n => (Int.neg_neg _).symm
|
||||
| succ _, (n:Nat) | -[_+1], 0 | -[_+1], -[_+1] => rfl
|
||||
| succ _, -[_+1] | -[_+1], succ _ => (Int.neg_neg _).symm
|
||||
|
||||
protected theorem neg_tdiv_neg (a b : Int) : (-a).tdiv (-b) = a.tdiv b := by
|
||||
simp [Int.tdiv_neg, Int.neg_tdiv, Int.neg_neg]
|
||||
|
||||
@@ -181,12 +181,12 @@ theorem subNatNat_add_negSucc (m n k : Nat) :
|
||||
Nat.add_comm]
|
||||
|
||||
protected theorem add_assoc : ∀ a b c : Int, a + b + c = a + (b + c)
|
||||
| (m:Nat), (n:Nat), c => aux1 ..
|
||||
| (m:Nat), (n:Nat), _ => aux1 ..
|
||||
| Nat.cast m, b, Nat.cast k => by
|
||||
rw [Int.add_comm, ← aux1, Int.add_comm k, aux1, Int.add_comm b]
|
||||
| a, (n:Nat), (k:Nat) => by
|
||||
rw [Int.add_comm, Int.add_comm a, ← aux1, Int.add_comm a, Int.add_comm k]
|
||||
| -[m+1], -[n+1], (k:Nat) => aux2 ..
|
||||
| -[_+1], -[_+1], (k:Nat) => aux2 ..
|
||||
| -[m+1], (n:Nat), -[k+1] => by
|
||||
rw [Int.add_comm, ← aux2, Int.add_comm n, ← aux2, Int.add_comm -[m+1]]
|
||||
| (m:Nat), -[n+1], -[k+1] => by
|
||||
|
||||
@@ -512,8 +512,8 @@ theorem toNat_add_nat {a : Int} (ha : 0 ≤ a) (n : Nat) : (a + n).toNat = a.toN
|
||||
|
||||
@[simp] theorem pred_toNat : ∀ i : Int, (i - 1).toNat = i.toNat - 1
|
||||
| 0 => rfl
|
||||
| (n+1:Nat) => by simp [ofNat_add]
|
||||
| -[n+1] => rfl
|
||||
| (_+1:Nat) => by simp [ofNat_add]
|
||||
| -[_+1] => rfl
|
||||
|
||||
theorem toNat_sub_toNat_neg : ∀ n : Int, ↑n.toNat - ↑(-n).toNat = n
|
||||
| 0 => rfl
|
||||
|
||||
@@ -73,7 +73,7 @@ theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (l H)
|
||||
· simp only [*, pmap, map]
|
||||
|
||||
theorem pmap_map {p : β → Prop} (g : ∀ b, p b → γ) (f : α → β) (l H) :
|
||||
pmap g (map f l) H = pmap (fun a h => g (f a) h) l fun a h => H _ (mem_map_of_mem _ h) := by
|
||||
pmap g (map f l) H = pmap (fun a h => g (f a) h) l fun _ h => H _ (mem_map_of_mem _ h) := by
|
||||
induction l
|
||||
· rfl
|
||||
· simp only [*, pmap, map]
|
||||
@@ -84,7 +84,7 @@ theorem attach_congr {l₁ l₂ : List α} (h : l₁ = l₂) :
|
||||
simp
|
||||
|
||||
theorem attachWith_congr {l₁ l₂ : List α} (w : l₁ = l₂) {P : α → Prop} {H : ∀ x ∈ l₁, P x} :
|
||||
l₁.attachWith P H = l₂.attachWith P fun x h => H _ (w ▸ h) := by
|
||||
l₁.attachWith P H = l₂.attachWith P fun _ h => H _ (w ▸ h) := by
|
||||
subst w
|
||||
simp
|
||||
|
||||
@@ -353,7 +353,7 @@ theorem attach_map {l : List α} (f : α → β) :
|
||||
induction l <;> simp [*]
|
||||
|
||||
theorem attachWith_map {l : List α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), b ∈ l.map f → P b} :
|
||||
(l.map f).attachWith P H = (l.attachWith (P ∘ f) (fun a h => H _ (mem_map_of_mem f h))).map
|
||||
(l.map f).attachWith P H = (l.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem f h))).map
|
||||
fun ⟨x, h⟩ => ⟨f x, h⟩ := by
|
||||
induction l <;> simp [*]
|
||||
|
||||
@@ -548,4 +548,131 @@ theorem count_attachWith [DecidableEq α] {p : α → Prop} (l : List α) (H :
|
||||
(l.attachWith p H).count a = l.count ↑a :=
|
||||
Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attachWith _ _ _
|
||||
|
||||
/-! ## unattach
|
||||
|
||||
`List.unattach` is the (one-sided) inverse of `List.attach`. It is a synonym for `List.map Subtype.val`.
|
||||
|
||||
We use it by providing a simp lemma `l.attach.unattach = l`, and simp lemmas which recognize higher order
|
||||
functions applied to `l : List { x // p x }` which only depend on the value, not the predicate, and rewrite these
|
||||
in terms of a simpler function applied to `l.unattach`.
|
||||
|
||||
Further, we provide simp lemmas that push `unattach` inwards.
|
||||
-/
|
||||
|
||||
/--
|
||||
A synonym for `l.map (·.val)`. Mostly this should not be needed by users.
|
||||
It is introduced as an intermediate step by lemmas such as `map_subtype`,
|
||||
and is ideally subsequently simplified away by `unattach_attach`.
|
||||
|
||||
If not, usually the right approach is `simp [List.unattach, -List.map_subtype]` to unfold.
|
||||
-/
|
||||
def unattach {α : Type _} {p : α → Prop} (l : List { x // p x }) := l.map (·.val)
|
||||
|
||||
@[simp] theorem unattach_nil {α : Type _} {p : α → Prop} : ([] : List { x // p x }).unattach = [] := rfl
|
||||
@[simp] theorem unattach_cons {α : Type _} {p : α → Prop} {a : { x // p x }} {l : List { x // p x }} :
|
||||
(a :: l).unattach = a.val :: l.unattach := rfl
|
||||
|
||||
@[simp] theorem length_unattach {α : Type _} {p : α → Prop} {l : List { x // p x }} :
|
||||
l.unattach.length = l.length := by
|
||||
unfold unattach
|
||||
simp
|
||||
|
||||
@[simp] theorem unattach_attach {α : Type _} (l : List α) : l.attach.unattach = l := by
|
||||
unfold unattach
|
||||
induction l with
|
||||
| nil => simp
|
||||
| cons a l ih => simp [ih, Function.comp_def]
|
||||
|
||||
@[simp] theorem unattach_attachWith {α : Type _} {p : α → Prop} {l : List α}
|
||||
{H : ∀ a ∈ l, p a} :
|
||||
(l.attachWith p H).unattach = l := by
|
||||
unfold unattach
|
||||
induction l with
|
||||
| nil => simp
|
||||
| cons a l ih => simp [ih, Function.comp_def]
|
||||
|
||||
/-! ### Recognizing higher order functions on subtypes using a function that only depends on the value. -/
|
||||
|
||||
/--
|
||||
This lemma identifies folds over lists of subtypes, where the function only depends on the value, not the proposition,
|
||||
and simplifies these to the function directly taking the value.
|
||||
-/
|
||||
@[simp] theorem foldl_subtype {p : α → Prop} {l : List { x // p x }}
|
||||
{f : β → { x // p x } → β} {g : β → α → β} {x : β}
|
||||
{hf : ∀ b x h, f b ⟨x, h⟩ = g b x} :
|
||||
l.foldl f x = l.unattach.foldl g x := by
|
||||
unfold unattach
|
||||
induction l generalizing x with
|
||||
| nil => simp
|
||||
| cons a l ih => simp [ih, hf]
|
||||
|
||||
/--
|
||||
This lemma identifies folds over lists of subtypes, where the function only depends on the value, not the proposition,
|
||||
and simplifies these to the function directly taking the value.
|
||||
-/
|
||||
@[simp] theorem foldr_subtype {p : α → Prop} {l : List { x // p x }}
|
||||
{f : { x // p x } → β → β} {g : α → β → β} {x : β}
|
||||
{hf : ∀ x h b, f ⟨x, h⟩ b = g x b} :
|
||||
l.foldr f x = l.unattach.foldr g x := by
|
||||
unfold unattach
|
||||
induction l generalizing x with
|
||||
| nil => simp
|
||||
| cons a l ih => simp [ih, hf]
|
||||
|
||||
/--
|
||||
This lemma identifies maps over lists of subtypes, where the function only depends on the value, not the proposition,
|
||||
and simplifies these to the function directly taking the value.
|
||||
-/
|
||||
@[simp] theorem map_subtype {p : α → Prop} {l : List { x // p x }}
|
||||
{f : { x // p x } → β} {g : α → β} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
|
||||
l.map f = l.unattach.map g := by
|
||||
unfold unattach
|
||||
induction l with
|
||||
| nil => simp
|
||||
| cons a l ih => simp [ih, hf]
|
||||
|
||||
@[simp] theorem filterMap_subtype {p : α → Prop} {l : List { x // p x }}
|
||||
{f : { x // p x } → Option β} {g : α → Option β} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
|
||||
l.filterMap f = l.unattach.filterMap g := by
|
||||
unfold unattach
|
||||
induction l with
|
||||
| nil => simp
|
||||
| cons a l ih => simp [ih, hf, filterMap_cons]
|
||||
|
||||
@[simp] theorem bind_subtype {p : α → Prop} {l : List { x // p x }}
|
||||
{f : { x // p x } → List β} {g : α → List β} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
|
||||
(l.bind f) = l.unattach.bind g := by
|
||||
unfold unattach
|
||||
induction l with
|
||||
| nil => simp
|
||||
| cons a l ih => simp [ih, hf]
|
||||
|
||||
@[simp] theorem unattach_filter {p : α → Prop} {l : List { x // p x }}
|
||||
{f : { x // p x } → Bool} {g : α → Bool} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
|
||||
(l.filter f).unattach = l.unattach.filter g := by
|
||||
induction l with
|
||||
| nil => simp
|
||||
| cons a l ih =>
|
||||
simp only [filter_cons, hf, unattach_cons]
|
||||
split <;> simp [ih]
|
||||
|
||||
/-! ### Simp lemmas pushing `unattach` inwards. -/
|
||||
|
||||
@[simp] theorem unattach_reverse {p : α → Prop} {l : List { x // p x }} :
|
||||
l.reverse.unattach = l.unattach.reverse := by
|
||||
simp [unattach, -map_subtype]
|
||||
|
||||
@[simp] theorem unattach_append {p : α → Prop} {l₁ l₂ : List { x // p x }} :
|
||||
(l₁ ++ l₂).unattach = l₁.unattach ++ l₂.unattach := by
|
||||
simp [unattach, -map_subtype]
|
||||
|
||||
@[simp] theorem unattach_join {p : α → Prop} {l : List (List { x // p x })} :
|
||||
l.join.unattach = (l.map unattach).join := by
|
||||
unfold unattach
|
||||
induction l <;> simp_all
|
||||
|
||||
@[simp] theorem unattach_replicate {p : α → Prop} {n : Nat} {x : { x // p x }} :
|
||||
(List.replicate n x).unattach = List.replicate n x.1 := by
|
||||
simp [unattach, -map_subtype]
|
||||
|
||||
end List
|
||||
|
||||
@@ -218,8 +218,8 @@ def get? : (as : List α) → (i : Nat) → Option α
|
||||
|
||||
theorem ext_get? : ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n) → l₁ = l₂
|
||||
| [], [], _ => rfl
|
||||
| a :: l₁, [], h => nomatch h 0
|
||||
| [], a' :: l₂, h => nomatch h 0
|
||||
| _ :: _, [], h => nomatch h 0
|
||||
| [], _ :: _, h => nomatch h 0
|
||||
| a :: l₁, a' :: l₂, h => by
|
||||
have h0 : some a = some a' := h 0
|
||||
injection h0 with aa; simp only [aa, ext_get? fun n => h (n+1)]
|
||||
|
||||
@@ -235,8 +235,8 @@ theorem sizeOf_get [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.g
|
||||
theorem le_antisymm [LT α] [s : Antisymm (¬ · < · : α → α → Prop)] {as bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) : as = bs :=
|
||||
match as, bs with
|
||||
| [], [] => rfl
|
||||
| [], b::bs => False.elim <| h₂ (List.lt.nil ..)
|
||||
| a::as, [] => False.elim <| h₁ (List.lt.nil ..)
|
||||
| [], _::_ => False.elim <| h₂ (List.lt.nil ..)
|
||||
| _::_, [] => False.elim <| h₁ (List.lt.nil ..)
|
||||
| a::as, b::bs => by
|
||||
by_cases hab : a < b
|
||||
· exact False.elim <| h₂ (List.lt.head _ _ hab)
|
||||
|
||||
@@ -52,9 +52,9 @@ theorem eraseP_of_forall_not {l : List α} (h : ∀ a, a ∈ l → ¬p a) : l.er
|
||||
theorem eraseP_ne_nil {xs : List α} {p : α → Bool} : xs.eraseP p ≠ [] ↔ xs ≠ [] ∧ ∀ x, p x → xs ≠ [x] := by
|
||||
simp
|
||||
|
||||
theorem exists_of_eraseP : ∀ {l : List α} {a} (al : a ∈ l) (pa : p a),
|
||||
theorem exists_of_eraseP : ∀ {l : List α} {a} (_ : a ∈ l) (_ : p a),
|
||||
∃ a l₁ l₂, (∀ b ∈ l₁, ¬p b) ∧ p a ∧ l = l₁ ++ a :: l₂ ∧ l.eraseP p = l₁ ++ l₂
|
||||
| b :: l, a, al, pa =>
|
||||
| b :: l, _, al, pa =>
|
||||
if pb : p b then
|
||||
⟨b, [], l, forall_mem_nil _, pb, by simp [pb]⟩
|
||||
else
|
||||
@@ -168,8 +168,8 @@ theorem eraseP_append_left {a : α} (pa : p a) :
|
||||
|
||||
theorem eraseP_append_right :
|
||||
∀ {l₁ : List α} l₂, (∀ b ∈ l₁, ¬p b) → eraseP p (l₁++l₂) = l₁ ++ l₂.eraseP p
|
||||
| [], l₂, _ => rfl
|
||||
| x :: xs, l₂, h => by
|
||||
| [], _, _ => rfl
|
||||
| _ :: _, _, h => by
|
||||
simp [(forall_mem_cons.1 h).1, eraseP_append_right _ (forall_mem_cons.1 h).2]
|
||||
|
||||
theorem eraseP_append (l₁ l₂ : List α) :
|
||||
|
||||
@@ -191,7 +191,7 @@ theorem get?_eq_some : l.get? n = some a ↔ ∃ h, get l ⟨n, h⟩ = a :=
|
||||
⟨fun e =>
|
||||
have : n < length l := Nat.gt_of_not_le fun hn => by cases get?_len_le hn ▸ e
|
||||
⟨this, by rwa [get?_eq_get this, Option.some.injEq] at e⟩,
|
||||
fun ⟨h, e⟩ => e ▸ get?_eq_get _⟩
|
||||
fun ⟨_, e⟩ => e ▸ get?_eq_get _⟩
|
||||
|
||||
theorem get?_eq_none : l.get? n = none ↔ length l ≤ n :=
|
||||
⟨fun e => Nat.ge_of_not_lt (fun h' => by cases e ▸ get?_eq_some.2 ⟨h', rfl⟩), get?_len_le⟩
|
||||
@@ -718,9 +718,9 @@ theorem set_eq_of_length_le {l : List α} {n : Nat} (h : l.length ≤ n) {a : α
|
||||
theorem set_comm (a b : α) : ∀ {n m : Nat} (l : List α), n ≠ m →
|
||||
(l.set n a).set m b = (l.set m b).set n a
|
||||
| _, _, [], _ => by simp
|
||||
| n+1, 0, _ :: _, _ => by simp [set]
|
||||
| 0, m+1, _ :: _, _ => by simp [set]
|
||||
| n+1, m+1, x :: t, h =>
|
||||
| _+1, 0, _ :: _, _ => by simp [set]
|
||||
| 0, _+1, _ :: _, _ => by simp [set]
|
||||
| _+1, _+1, _ :: t, h =>
|
||||
congrArg _ <| set_comm a b t fun h' => h <| Nat.succ_inj'.mpr h'
|
||||
|
||||
@[simp]
|
||||
@@ -994,8 +994,8 @@ theorem getLast_eq_getElem : ∀ (l : List α) (h : l ≠ []),
|
||||
match l with
|
||||
| [] => contradiction
|
||||
| a :: l => exact Nat.le_refl _)
|
||||
| [a], h => rfl
|
||||
| a :: b :: l, h => by
|
||||
| [_], _ => rfl
|
||||
| _ :: _ :: _, _ => by
|
||||
simp [getLast, get, Nat.succ_sub_succ, getLast_eq_getElem]
|
||||
|
||||
@[deprecated getLast_eq_getElem (since := "2024-07-15")]
|
||||
@@ -1028,7 +1028,7 @@ theorem getLast!_cons [Inhabited α] : @getLast! α _ (a::l) = getLastD l a := b
|
||||
|
||||
theorem getLast_mem_getLast? : ∀ {l : List α} (h : l ≠ []), getLast l h ∈ getLast? l
|
||||
| [], h => by contradiction
|
||||
| a :: l, _ => rfl
|
||||
| _ :: _, _ => rfl
|
||||
|
||||
theorem getLastD_mem_cons : ∀ (l : List α) (a : α), getLastD l a ∈ a::l
|
||||
| [], _ => .head ..
|
||||
@@ -1134,7 +1134,7 @@ theorem mem_of_mem_head? : ∀ {l : List α} {a : α}, a ∈ l.head? → a ∈ l
|
||||
|
||||
theorem head_mem_head? : ∀ {l : List α} (h : l ≠ []), head l h ∈ head? l
|
||||
| [], h => by contradiction
|
||||
| a :: l, _ => rfl
|
||||
| _ :: _, _ => rfl
|
||||
|
||||
theorem head?_concat {a : α} : (l ++ [a]).head? = l.head?.getD a := by
|
||||
cases l <;> simp
|
||||
@@ -1466,7 +1466,7 @@ theorem map_filter_eq_foldr (f : α → β) (p : α → Bool) (as : List α) :
|
||||
|
||||
@[simp] theorem filter_append {p : α → Bool} :
|
||||
∀ (l₁ l₂ : List α), filter p (l₁ ++ l₂) = filter p l₁ ++ filter p l₂
|
||||
| [], l₂ => rfl
|
||||
| [], _ => rfl
|
||||
| a :: l₁, l₂ => by simp [filter]; split <;> simp [filter_append l₁]
|
||||
|
||||
theorem filter_eq_cons_iff {l} {a} {as} :
|
||||
@@ -1690,7 +1690,7 @@ theorem getElem?_append_left {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.leng
|
||||
|
||||
theorem getElem?_append_right : ∀ {l₁ l₂ : List α} {n : Nat}, l₁.length ≤ n →
|
||||
(l₁ ++ l₂)[n]? = l₂[n - l₁.length]?
|
||||
| [], _, n, _ => rfl
|
||||
| [], _, _, _ => rfl
|
||||
| a :: l, _, n+1, h₁ => by
|
||||
rw [cons_append]
|
||||
simp [Nat.succ_sub_succ_eq_sub, getElem?_append_right (Nat.lt_succ.1 h₁)]
|
||||
@@ -1755,8 +1755,8 @@ theorem append_of_mem {a : α} {l : List α} : a ∈ l → ∃ s t : List α, l
|
||||
|
||||
theorem append_inj :
|
||||
∀ {s₁ s₂ t₁ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → length s₁ = length s₂ → s₁ = s₂ ∧ t₁ = t₂
|
||||
| [], [], t₁, t₂, h, _ => ⟨rfl, h⟩
|
||||
| a :: s₁, b :: s₂, t₁, t₂, h, hl => by
|
||||
| [], [], _, _, h, _ => ⟨rfl, h⟩
|
||||
| _ :: _, _ :: _, _, _, h, hl => by
|
||||
simp [append_inj (cons.inj h).2 (Nat.succ.inj hl)] at h ⊢; exact h
|
||||
|
||||
theorem append_inj_right (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : length s₁ = length s₂) : t₁ = t₂ :=
|
||||
@@ -2707,7 +2707,7 @@ theorem bind_reverse {β} (l : List α) (f : α → List β) : (l.reverse.bind f
|
||||
@[simp] theorem reverse_replicate (n) (a : α) : reverse (replicate n a) = replicate n a :=
|
||||
eq_replicate_iff.2
|
||||
⟨by rw [length_reverse, length_replicate],
|
||||
fun b h => eq_of_mem_replicate (mem_reverse.1 h)⟩
|
||||
fun _ h => eq_of_mem_replicate (mem_reverse.1 h)⟩
|
||||
|
||||
/-! #### Further results about `getLast` and `getLast?` -/
|
||||
|
||||
@@ -2912,7 +2912,7 @@ theorem head?_dropLast (xs : List α) : xs.dropLast.head? = if 1 < xs.length the
|
||||
|
||||
theorem getLast_dropLast {xs : List α} (h) :
|
||||
xs.dropLast.getLast h =
|
||||
xs[xs.length - 2]'(match xs, h with | (a :: b :: xs), _ => Nat.lt_trans (Nat.lt_add_one _) (Nat.lt_add_one _)) := by
|
||||
xs[xs.length - 2]'(match xs, h with | (_ :: _ :: _), _ => Nat.lt_trans (Nat.lt_add_one _) (Nat.lt_add_one _)) := by
|
||||
rw [getLast_eq_getElem, getElem_dropLast]
|
||||
congr 1
|
||||
simp; rfl
|
||||
@@ -2936,8 +2936,8 @@ theorem dropLast_cons_of_ne_nil {α : Type u} {x : α}
|
||||
|
||||
theorem dropLast_concat_getLast : ∀ {l : List α} (h : l ≠ []), dropLast l ++ [getLast l h] = l
|
||||
| [], h => absurd rfl h
|
||||
| [a], h => rfl
|
||||
| a :: b :: l, h => by
|
||||
| [_], _ => rfl
|
||||
| _ :: b :: l, _ => by
|
||||
rw [dropLast_cons₂, cons_append, getLast_cons (cons_ne_nil _ _)]
|
||||
congr
|
||||
exact dropLast_concat_getLast (cons_ne_nil b l)
|
||||
|
||||
@@ -10,7 +10,7 @@ import Init.Data.List.Erase
|
||||
namespace List
|
||||
|
||||
theorem getElem?_eraseIdx (l : List α) (i : Nat) (j : Nat) :
|
||||
(l.eraseIdx i)[j]? = if h : j < i then l[j]? else l[j + 1]? := by
|
||||
(l.eraseIdx i)[j]? = if j < i then l[j]? else l[j + 1]? := by
|
||||
rw [eraseIdx_eq_take_drop_succ, getElem?_append]
|
||||
split <;> rename_i h
|
||||
· rw [getElem?_take]
|
||||
|
||||
@@ -154,7 +154,7 @@ theorem erase_range' :
|
||||
/-! ### range -/
|
||||
|
||||
theorem reverse_range' : ∀ s n : Nat, reverse (range' s n) = map (s + n - 1 - ·) (range n)
|
||||
| s, 0 => rfl
|
||||
| _, 0 => rfl
|
||||
| s, n + 1 => by
|
||||
rw [range'_1_concat, reverse_append, range_succ_eq_map,
|
||||
show s + (n + 1) - 1 = s + n from rfl, map, map_map]
|
||||
|
||||
@@ -98,8 +98,8 @@ theorem Perm.append_cons (a : α) {h₁ h₂ t₁ t₂ : List α} (p₁ : h₁ ~
|
||||
perm_middle.trans <| by rw [append_nil]
|
||||
|
||||
theorem perm_append_comm : ∀ {l₁ l₂ : List α}, l₁ ++ l₂ ~ l₂ ++ l₁
|
||||
| [], l₂ => by simp
|
||||
| a :: t, l₂ => (perm_append_comm.cons _).trans perm_middle.symm
|
||||
| [], _ => by simp
|
||||
| _ :: _, _ => (perm_append_comm.cons _).trans perm_middle.symm
|
||||
|
||||
theorem perm_append_comm_assoc (l₁ l₂ l₃ : List α) :
|
||||
Perm (l₁ ++ (l₂ ++ l₃)) (l₂ ++ (l₁ ++ l₃)) := by
|
||||
|
||||
@@ -92,7 +92,7 @@ theorem map_add_range' (a) : ∀ s n step, map (a + ·) (range' s n step) = rang
|
||||
|
||||
theorem range'_append : ∀ s m n step : Nat,
|
||||
range' s m step ++ range' (s + step * m) n step = range' s (n + m) step
|
||||
| s, 0, n, step => rfl
|
||||
| _, 0, _, _ => rfl
|
||||
| s, m + 1, n, step => by
|
||||
simpa [range', Nat.mul_succ, Nat.add_assoc, Nat.add_comm]
|
||||
using range'_append (s + step) m n step
|
||||
@@ -131,7 +131,7 @@ theorem range'_eq_cons_iff : range' s n = a :: xs ↔ s = a ∧ 0 < n ∧ xs = r
|
||||
/-! ### range -/
|
||||
|
||||
theorem range_loop_range' : ∀ s n : Nat, range.loop s (range' s n) = range' 0 (n + s)
|
||||
| 0, n => rfl
|
||||
| 0, _ => rfl
|
||||
| s + 1, n => by rw [← Nat.add_assoc, Nat.add_right_comm n s 1]; exact range_loop_range' s (n + 1)
|
||||
|
||||
theorem range_eq_range' (n : Nat) : range n = range' 0 n :=
|
||||
@@ -214,9 +214,9 @@ theorem enumFrom_eq_nil {n : Nat} {l : List α} : List.enumFrom n l = [] ↔ l =
|
||||
@[simp]
|
||||
theorem getElem?_enumFrom :
|
||||
∀ n (l : List α) m, (enumFrom n l)[m]? = l[m]?.map fun a => (n + m, a)
|
||||
| n, [], m => rfl
|
||||
| n, a :: l, 0 => by simp
|
||||
| n, a :: l, m + 1 => by
|
||||
| _, [], _ => rfl
|
||||
| _, _ :: _, 0 => by simp
|
||||
| n, _ :: l, m + 1 => by
|
||||
simp only [enumFrom_cons, getElem?_cons_succ]
|
||||
exact (getElem?_enumFrom (n + 1) l m).trans <| by rw [Nat.add_right_comm]; rfl
|
||||
|
||||
|
||||
@@ -102,7 +102,7 @@ def mergeSortTR (l : List α) (le : α → α → Bool := by exact fun a b => a
|
||||
where run : {n : Nat} → { l : List α // l.length = n } → List α
|
||||
| 0, ⟨[], _⟩ => []
|
||||
| 1, ⟨[a], _⟩ => [a]
|
||||
| n+2, xs =>
|
||||
| _+2, xs =>
|
||||
let (l, r) := splitInTwo xs
|
||||
mergeTR (run l) (run r) le
|
||||
|
||||
@@ -136,13 +136,13 @@ where
|
||||
run : {n : Nat} → { l : List α // l.length = n } → List α
|
||||
| 0, ⟨[], _⟩ => []
|
||||
| 1, ⟨[a], _⟩ => [a]
|
||||
| n+2, xs =>
|
||||
| _+2, xs =>
|
||||
let (l, r) := splitRevInTwo xs
|
||||
mergeTR (run' l) (run r) le
|
||||
run' : {n : Nat} → { l : List α // l.length = n } → List α
|
||||
| 0, ⟨[], _⟩ => []
|
||||
| 1, ⟨[a], _⟩ => [a]
|
||||
| n+2, xs =>
|
||||
| _+2, xs =>
|
||||
let (l, r) := splitRevInTwo' xs
|
||||
mergeTR (run' r) (run l) le
|
||||
|
||||
|
||||
@@ -742,8 +742,8 @@ theorem IsSuffix.eq_of_length_le (h : l₁ <:+ l₂) : l₂.length ≤ l₁.leng
|
||||
|
||||
theorem prefix_of_prefix_length_le :
|
||||
∀ {l₁ l₂ l₃ : List α}, l₁ <+: l₃ → l₂ <+: l₃ → length l₁ ≤ length l₂ → l₁ <+: l₂
|
||||
| [], l₂, _, _, _, _ => nil_prefix
|
||||
| a :: l₁, b :: l₂, _, ⟨r₁, rfl⟩, ⟨r₂, e⟩, ll => by
|
||||
| [], _, _, _, _, _ => nil_prefix
|
||||
| _ :: _, b :: _, _, ⟨_, rfl⟩, ⟨_, e⟩, ll => by
|
||||
injection e with _ e'; subst b
|
||||
rcases prefix_of_prefix_length_le ⟨_, rfl⟩ ⟨_, e'⟩ (le_of_succ_le_succ ll) with ⟨r₃, rfl⟩
|
||||
exact ⟨r₃, rfl⟩
|
||||
|
||||
@@ -247,9 +247,9 @@ theorem zip_eq_zipWith : ∀ (l₁ : List α) (l₂ : List β), zip l₁ l₂ =
|
||||
|
||||
theorem zip_map (f : α → γ) (g : β → δ) :
|
||||
∀ (l₁ : List α) (l₂ : List β), zip (l₁.map f) (l₂.map g) = (zip l₁ l₂).map (Prod.map f g)
|
||||
| [], l₂ => rfl
|
||||
| l₁, [] => by simp only [map, zip_nil_right]
|
||||
| a :: l₁, b :: l₂ => by
|
||||
| [], _ => rfl
|
||||
| _, [] => by simp only [map, zip_nil_right]
|
||||
| _ :: _, _ :: _ => by
|
||||
simp only [map, zip_cons_cons, zip_map, Prod.map]; constructor
|
||||
|
||||
theorem zip_map_left (f : α → γ) (l₁ : List α) (l₂ : List β) :
|
||||
@@ -287,12 +287,12 @@ theorem of_mem_zip {a b} : ∀ {l₁ : List α} {l₂ : List β}, (a, b) ∈ zip
|
||||
|
||||
theorem map_fst_zip :
|
||||
∀ (l₁ : List α) (l₂ : List β), l₁.length ≤ l₂.length → map Prod.fst (zip l₁ l₂) = l₁
|
||||
| [], bs, _ => rfl
|
||||
| [], _, _ => rfl
|
||||
| _ :: as, _ :: bs, h => by
|
||||
simp [Nat.succ_le_succ_iff] at h
|
||||
show _ :: map Prod.fst (zip as bs) = _ :: as
|
||||
rw [map_fst_zip as bs h]
|
||||
| a :: as, [], h => by simp at h
|
||||
| _ :: _, [], h => by simp at h
|
||||
|
||||
theorem map_snd_zip :
|
||||
∀ (l₁ : List α) (l₂ : List β), l₂.length ≤ l₁.length → map Prod.snd (zip l₁ l₂) = l₂
|
||||
@@ -430,9 +430,9 @@ theorem zip_unzip : ∀ l : List (α × β), zip (unzip l).1 (unzip l).2 = l
|
||||
|
||||
theorem unzip_zip_left :
|
||||
∀ {l₁ : List α} {l₂ : List β}, length l₁ ≤ length l₂ → (unzip (zip l₁ l₂)).1 = l₁
|
||||
| [], l₂, _ => rfl
|
||||
| l₁, [], h => by rw [eq_nil_of_length_eq_zero (Nat.eq_zero_of_le_zero h)]; rfl
|
||||
| a :: l₁, b :: l₂, h => by
|
||||
| [], _, _ => rfl
|
||||
| _, [], h => by rw [eq_nil_of_length_eq_zero (Nat.eq_zero_of_le_zero h)]; rfl
|
||||
| _ :: _, _ :: _, h => by
|
||||
simp only [zip_cons_cons, unzip_cons, unzip_zip_left (le_of_succ_le_succ h)]
|
||||
|
||||
theorem unzip_zip_right :
|
||||
|
||||
@@ -248,7 +248,7 @@ protected theorem add_mul (n m k : Nat) : (n + m) * k = n * k + m * k :=
|
||||
Nat.right_distrib n m k
|
||||
|
||||
protected theorem mul_assoc : ∀ (n m k : Nat), (n * m) * k = n * (m * k)
|
||||
| n, m, 0 => rfl
|
||||
| _, _, 0 => rfl
|
||||
| n, m, succ k => by simp [mul_succ, Nat.mul_assoc n m k, Nat.left_distrib]
|
||||
instance : Std.Associative (α := Nat) (· * ·) := ⟨Nat.mul_assoc⟩
|
||||
|
||||
|
||||
@@ -269,7 +269,7 @@ protected theorem div_div_eq_div_mul (m n k : Nat) : m / n / k = m / (n * k) :=
|
||||
|
||||
theorem div_mul_le_self : ∀ (m n : Nat), m / n * n ≤ m
|
||||
| m, 0 => by simp
|
||||
| m, n+1 => (le_div_iff_mul_le (Nat.succ_pos _)).1 (Nat.le_refl _)
|
||||
| _, _+1 => (le_div_iff_mul_le (Nat.succ_pos _)).1 (Nat.le_refl _)
|
||||
|
||||
theorem div_lt_iff_lt_mul (Hk : 0 < k) : x / k < y ↔ x < y * k := by
|
||||
rw [← Nat.not_le, ← Nat.not_le]; exact not_congr (le_div_iff_mul_le Hk)
|
||||
|
||||
@@ -874,15 +874,15 @@ theorem shiftLeft_succ_inside (m n : Nat) : m <<< (n+1) = (2*m) <<< n := rfl
|
||||
|
||||
/-- Shiftleft on successor with multiple moved to outside. -/
|
||||
theorem shiftLeft_succ : ∀(m n), m <<< (n + 1) = 2 * (m <<< n)
|
||||
| m, 0 => rfl
|
||||
| m, k + 1 => by
|
||||
| _, 0 => rfl
|
||||
| _, k + 1 => by
|
||||
rw [shiftLeft_succ_inside _ (k+1)]
|
||||
rw [shiftLeft_succ _ k, shiftLeft_succ_inside]
|
||||
|
||||
/-- Shiftright on successor with division moved inside. -/
|
||||
theorem shiftRight_succ_inside : ∀m n, m >>> (n+1) = (m/2) >>> n
|
||||
| m, 0 => rfl
|
||||
| m, k + 1 => by
|
||||
| _, 0 => rfl
|
||||
| _, k + 1 => by
|
||||
rw [shiftRight_succ _ (k+1)]
|
||||
rw [shiftRight_succ_inside _ k, shiftRight_succ]
|
||||
|
||||
|
||||
@@ -8,3 +8,5 @@ import Init.Data.Option.Basic
|
||||
import Init.Data.Option.BasicAux
|
||||
import Init.Data.Option.Instances
|
||||
import Init.Data.Option.Lemmas
|
||||
import Init.Data.Option.Attach
|
||||
import Init.Data.Option.List
|
||||
|
||||
178
src/Init/Data/Option/Attach.lean
Normal file
178
src/Init/Data/Option/Attach.lean
Normal file
@@ -0,0 +1,178 @@
|
||||
/-
|
||||
Copyright (c) 2024 Lean FRO. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Kim Morrison
|
||||
-/
|
||||
prelude
|
||||
import Init.Data.Option.Basic
|
||||
import Init.Data.Option.List
|
||||
import Init.Data.List.Attach
|
||||
import Init.BinderPredicates
|
||||
|
||||
namespace Option
|
||||
|
||||
/--
|
||||
Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
|
||||
`Option {x // P x}` is the same as the input `Option α`.
|
||||
-/
|
||||
@[inline] private unsafe def attachWithImpl
|
||||
(o : Option α) (P : α → Prop) (_ : ∀ x ∈ o, P x) : Option {x // P x} := unsafeCast o
|
||||
|
||||
/-- "Attach" a proof `P x` that holds for the element of `o`, if present,
|
||||
to produce a new option with the same element but in the type `{x // P x}`. -/
|
||||
@[implemented_by attachWithImpl] def attachWith
|
||||
(xs : Option α) (P : α → Prop) (H : ∀ x ∈ xs, P x) : Option {x // P x} :=
|
||||
match xs with
|
||||
| none => none
|
||||
| some x => some ⟨x, H x (mem_some_self x)⟩
|
||||
|
||||
/-- "Attach" the proof that the element of `xs`, if present, is in `xs`
|
||||
to produce a new option with the same elements but in the type `{x // x ∈ xs}`. -/
|
||||
@[inline] def attach (xs : Option α) : Option {x // x ∈ xs} := xs.attachWith _ fun _ => id
|
||||
|
||||
@[simp] theorem attach_none : (none : Option α).attach = none := rfl
|
||||
@[simp] theorem attachWith_none : (none : Option α).attachWith P H = none := rfl
|
||||
|
||||
@[simp] theorem attach_some {x : α} :
|
||||
(some x).attach = some ⟨x, rfl⟩ := rfl
|
||||
@[simp] theorem attachWith_some {x : α} {P : α → Prop} (h : ∀ (b : α), b ∈ some x → P b) :
|
||||
(some x).attachWith P h = some ⟨x, by simpa using h⟩ := rfl
|
||||
|
||||
theorem attach_congr {o₁ o₂ : Option α} (h : o₁ = o₂) :
|
||||
o₁.attach = o₂.attach.map (fun x => ⟨x.1, h ▸ x.2⟩) := by
|
||||
subst h
|
||||
simp
|
||||
|
||||
theorem attachWith_congr {o₁ o₂ : Option α} (w : o₁ = o₂) {P : α → Prop} {H : ∀ x ∈ o₁, P x} :
|
||||
o₁.attachWith P H = o₂.attachWith P fun x h => H _ (w ▸ h) := by
|
||||
subst w
|
||||
simp
|
||||
|
||||
theorem attach_map_coe (o : Option α) (f : α → β) :
|
||||
(o.attach.map fun (i : {i // i ∈ o}) => f i) = o.map f := by
|
||||
cases o <;> simp
|
||||
|
||||
theorem attach_map_val (o : Option α) (f : α → β) :
|
||||
(o.attach.map fun i => f i.val) = o.map f :=
|
||||
attach_map_coe _ _
|
||||
|
||||
@[simp]
|
||||
theorem attach_map_subtype_val (o : Option α) :
|
||||
o.attach.map Subtype.val = o :=
|
||||
(attach_map_coe _ _).trans (congrFun Option.map_id _)
|
||||
|
||||
theorem attachWith_map_coe {p : α → Prop} (f : α → β) (o : Option α) (H : ∀ a ∈ o, p a) :
|
||||
((o.attachWith p H).map fun (i : { i // p i}) => f i.val) = o.map f := by
|
||||
cases o <;> simp [H]
|
||||
|
||||
theorem attachWith_map_val {p : α → Prop} (f : α → β) (o : Option α) (H : ∀ a ∈ o, p a) :
|
||||
((o.attachWith p H).map fun i => f i.val) = o.map f :=
|
||||
attachWith_map_coe _ _ _
|
||||
|
||||
@[simp]
|
||||
theorem attachWith_map_subtype_val {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
|
||||
(o.attachWith p H).map Subtype.val = o :=
|
||||
(attachWith_map_coe _ _ _).trans (congrFun Option.map_id _)
|
||||
|
||||
@[simp] theorem mem_attach : ∀ (o : Option α) (x : {x // x ∈ o}), x ∈ o.attach
|
||||
| none, ⟨x, h⟩ => by simp at h
|
||||
| some a, ⟨x, h⟩ => by simpa using h
|
||||
|
||||
@[simp] theorem isNone_attach (o : Option α) : o.attach.isNone = o.isNone := by
|
||||
cases o <;> simp
|
||||
|
||||
@[simp] theorem isNone_attachWith {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
|
||||
(o.attachWith p H).isNone = o.isNone := by
|
||||
cases o <;> simp
|
||||
|
||||
@[simp] theorem isSome_attach (o : Option α) : o.attach.isSome = o.isSome := by
|
||||
cases o <;> simp
|
||||
|
||||
@[simp] theorem isSome_attachWith {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
|
||||
(o.attachWith p H).isSome = o.isSome := by
|
||||
cases o <;> simp
|
||||
|
||||
@[simp] theorem attach_eq_none_iff (o : Option α) : o.attach = none ↔ o = none := by
|
||||
cases o <;> simp
|
||||
|
||||
@[simp] theorem attach_eq_some_iff {o : Option α} {x : {x // x ∈ o}} :
|
||||
o.attach = some x ↔ o = some x.val := by
|
||||
cases o <;> cases x <;> simp
|
||||
|
||||
@[simp] theorem attachWith_eq_none_iff {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
|
||||
o.attachWith p H = none ↔ o = none := by
|
||||
cases o <;> simp
|
||||
|
||||
@[simp] theorem attachWith_eq_some_iff {p : α → Prop} {o : Option α} (H : ∀ a ∈ o, p a) {x : {x // p x}} :
|
||||
o.attachWith p H = some x ↔ o = some x.val := by
|
||||
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]
|
||||
|
||||
@[simp] theorem get_attachWith {p : α → Prop} {o : Option α} (H : ∀ a ∈ o, 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]
|
||||
|
||||
@[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
|
||||
|
||||
theorem attach_map {o : Option α} (f : α → β) :
|
||||
(o.map f).attach = o.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem f h⟩) := by
|
||||
cases o <;> simp
|
||||
|
||||
theorem attachWith_map {o : Option α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), b ∈ o.map f → P b} :
|
||||
(o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun a h => H _ (mem_map_of_mem f h))).map
|
||||
fun ⟨x, h⟩ => ⟨f x, h⟩ := by
|
||||
cases o <;> simp
|
||||
|
||||
theorem map_attach {o : Option α} (f : { x // x ∈ o } → β) :
|
||||
o.attach.map f = o.pmap (fun a (h : a ∈ o) => f ⟨a, h⟩) (fun a h => h) := by
|
||||
cases o <;> simp
|
||||
|
||||
theorem map_attachWith {o : Option α} {P : α → Prop} {H : ∀ (a : α), a ∈ o → P a}
|
||||
(f : { x // P x } → β) :
|
||||
(o.attachWith P H).map f =
|
||||
o.pmap (fun a (h : a ∈ o ∧ P a) => f ⟨a, h.2⟩) (fun a h => ⟨h, H a h⟩) := by
|
||||
cases o <;> simp
|
||||
|
||||
theorem attach_bind {o : Option α} {f : α → Option β} :
|
||||
(o.bind f).attach =
|
||||
o.attach.bind fun ⟨x, h⟩ => (f x).attach.map fun ⟨y, h'⟩ => ⟨y, mem_bind_iff.mpr ⟨x, h, h'⟩⟩ := by
|
||||
cases o <;> simp
|
||||
|
||||
theorem bind_attach {o : Option α} {f : {x // x ∈ o} → Option β} :
|
||||
o.attach.bind f = o.pbind fun a h => f ⟨a, h⟩ := by
|
||||
cases o <;> simp
|
||||
|
||||
theorem pbind_eq_bind_attach {o : Option α} {f : (a : α) → a ∈ o → Option β} :
|
||||
o.pbind f = o.attach.bind fun ⟨x, h⟩ => f x h := by
|
||||
cases o <;> simp
|
||||
|
||||
theorem attach_filter {o : Option α} {p : α → Bool} :
|
||||
(o.filter p).attach =
|
||||
o.attach.bind fun ⟨x, h⟩ => if h' : p x then some ⟨x, by simp_all⟩ else none := by
|
||||
cases o with
|
||||
| none => simp
|
||||
| some a =>
|
||||
simp only [filter_some, attach_some]
|
||||
ext
|
||||
simp only [mem_def, attach_eq_some_iff, ite_none_right_eq_some, some.injEq, some_bind,
|
||||
dite_none_right_eq_some]
|
||||
constructor
|
||||
· rintro ⟨h, w⟩
|
||||
refine ⟨h, by ext; simpa using w⟩
|
||||
· rintro ⟨h, rfl⟩
|
||||
simp [h]
|
||||
|
||||
theorem filter_attach {o : Option α} {p : {x // x ∈ o} → 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]
|
||||
|
||||
end Option
|
||||
@@ -202,7 +202,7 @@ result.
|
||||
instance (α) [BEq α] [LawfulBEq α] : LawfulBEq (Option α) where
|
||||
rfl {x} :=
|
||||
match x with
|
||||
| some x => LawfulBEq.rfl (α := α)
|
||||
| some _ => LawfulBEq.rfl (α := α)
|
||||
| none => rfl
|
||||
eq_of_beq {x y h} := by
|
||||
match x, y with
|
||||
|
||||
@@ -138,6 +138,10 @@ theorem bind_eq_none' {o : Option α} {f : α → Option β} :
|
||||
o.bind f = none ↔ ∀ b a, a ∈ o → b ∉ f a := by
|
||||
simp only [eq_none_iff_forall_not_mem, not_exists, not_and, mem_def, bind_eq_some]
|
||||
|
||||
theorem mem_bind_iff {o : Option α} {f : α → Option β} :
|
||||
b ∈ o.bind f ↔ ∃ a, a ∈ o ∧ b ∈ f a := by
|
||||
cases o <;> simp
|
||||
|
||||
theorem bind_comm {f : α → β → Option γ} (a : Option α) (b : Option β) :
|
||||
(a.bind fun x => b.bind (f x)) = b.bind fun y => a.bind fun x => f x y := by
|
||||
cases a <;> cases b <;> rfl
|
||||
@@ -232,9 +236,27 @@ theorem isSome_filter_of_isSome (p : α → Bool) (o : Option α) (h : (o.filter
|
||||
cases o <;> simp at h ⊢
|
||||
|
||||
@[simp] theorem filter_eq_none {p : α → Bool} :
|
||||
Option.filter p o = none ↔ o = none ∨ ∀ a, a ∈ o → ¬ p a := by
|
||||
o.filter p = none ↔ o = none ∨ ∀ a, a ∈ o → ¬ p a := by
|
||||
cases o <;> simp [filter_some]
|
||||
|
||||
@[simp] theorem filter_eq_some {o : Option α} {p : α → Bool} :
|
||||
o.filter p = some a ↔ a ∈ o ∧ p a := by
|
||||
cases o with
|
||||
| none => simp
|
||||
| some a =>
|
||||
simp [filter_some]
|
||||
split <;> rename_i h
|
||||
· simp only [some.injEq, iff_self_and]
|
||||
rintro rfl
|
||||
exact h
|
||||
· simp only [reduceCtorEq, false_iff, not_and, Bool.not_eq_true]
|
||||
rintro rfl
|
||||
simpa using h
|
||||
|
||||
theorem mem_filter_iff {p : α → Bool} {a : α} {o : Option α} :
|
||||
a ∈ o.filter p ↔ a ∈ o ∧ p a := by
|
||||
simp
|
||||
|
||||
@[simp] theorem all_guard (p : α → Prop) [DecidablePred p] (a : α) :
|
||||
Option.all q (guard p a) = (!p a || q a) := by
|
||||
simp only [guard]
|
||||
@@ -308,8 +330,8 @@ theorem guard_comp {p : α → Prop} [DecidablePred p] {f : β → α} :
|
||||
theorem liftOrGet_eq_or_eq {f : α → α → α} (h : ∀ a b, f a b = a ∨ f a b = b) :
|
||||
∀ o₁ o₂, liftOrGet f o₁ o₂ = o₁ ∨ liftOrGet f o₁ o₂ = o₂
|
||||
| none, none => .inl rfl
|
||||
| some a, none => .inl rfl
|
||||
| none, some b => .inr rfl
|
||||
| some _, none => .inl rfl
|
||||
| none, some _ => .inr rfl
|
||||
| some a, some b => by have := h a b; simp [liftOrGet] at this ⊢; exact this
|
||||
|
||||
@[simp] theorem liftOrGet_none_left {f} {b : Option α} : liftOrGet f none b = b := by
|
||||
@@ -350,6 +372,8 @@ end choice
|
||||
|
||||
@[simp] theorem toList_none (α : Type _) : (none : Option α).toList = [] := rfl
|
||||
|
||||
-- See `Init.Data.Option.List` for lemmas about `toList`.
|
||||
|
||||
@[simp] theorem or_some : (some a).or o = some a := rfl
|
||||
@[simp] theorem none_or : none.or o = o := rfl
|
||||
|
||||
|
||||
14
src/Init/Data/Option/List.lean
Normal file
14
src/Init/Data/Option/List.lean
Normal file
@@ -0,0 +1,14 @@
|
||||
/-
|
||||
Copyright (c) 2024 Lean FRO. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Kim Morrison
|
||||
-/
|
||||
prelude
|
||||
import Init.Data.List.Lemmas
|
||||
|
||||
namespace Option
|
||||
|
||||
@[simp] theorem mem_toList {a : α} {o : Option α} : a ∈ o.toList ↔ a ∈ o := by
|
||||
cases o <;> simp [eq_comm]
|
||||
|
||||
end Option
|
||||
@@ -322,7 +322,7 @@ theorem lt_next (s : String) (i : Pos) : i.1 < (s.next i).1 :=
|
||||
|
||||
theorem utf8PrevAux_lt_of_pos : ∀ (cs : List Char) (i p : Pos), p ≠ 0 →
|
||||
(utf8PrevAux cs i p).1 < p.1
|
||||
| [], i, p, h =>
|
||||
| [], _, _, h =>
|
||||
Nat.lt_of_le_of_lt (Nat.zero_le _)
|
||||
(Nat.zero_lt_of_ne_zero (mt (congrArg Pos.mk) h))
|
||||
| c::cs, i, p, h => by
|
||||
|
||||
@@ -352,10 +352,10 @@ theorem not_forall_of_exists_not {p : α → Prop} : (∃ x, ¬p x) → ¬∀ x,
|
||||
@[simp] theorem exists_or_eq_left' (y : α) (p : α → Prop) : ∃ x : α, y = x ∨ p x := ⟨y, .inl rfl⟩
|
||||
@[simp] theorem exists_or_eq_right' (y : α) (p : α → Prop) : ∃ x : α, p x ∨ y = x := ⟨y, .inr rfl⟩
|
||||
|
||||
@[simp] theorem exists_prop' {p : Prop} : (∃ _ : α, p) ↔ Nonempty α ∧ p :=
|
||||
theorem exists_prop' {p : Prop} : (∃ _ : α, p) ↔ Nonempty α ∧ p :=
|
||||
⟨fun ⟨a, h⟩ => ⟨⟨a⟩, h⟩, fun ⟨⟨a⟩, h⟩ => ⟨a, h⟩⟩
|
||||
|
||||
theorem exists_prop : (∃ _h : a, b) ↔ a ∧ b :=
|
||||
@[simp] theorem exists_prop : (∃ _h : a, b) ↔ a ∧ b :=
|
||||
⟨fun ⟨hp, hq⟩ => ⟨hp, hq⟩, fun ⟨hp, hq⟩ => ⟨hp, hq⟩⟩
|
||||
|
||||
@[simp] theorem exists_apply_eq_apply (f : α → β) (a' : α) : ∃ a, f a = f a' := ⟨a', rfl⟩
|
||||
@@ -458,7 +458,7 @@ theorem Decidable.imp_iff_not_or [Decidable a] : (a → b) ↔ (¬a ∨ b) :=
|
||||
theorem Decidable.imp_iff_or_not [Decidable b] : b → a ↔ a ∨ ¬b :=
|
||||
Decidable.imp_iff_not_or.trans or_comm
|
||||
|
||||
theorem Decidable.imp_or [h : Decidable a] : (a → b ∨ c) ↔ (a → b) ∨ (a → c) :=
|
||||
theorem Decidable.imp_or [Decidable a] : (a → b ∨ c) ↔ (a → b) ∨ (a → c) :=
|
||||
if h : a then by
|
||||
rw [imp_iff_right h, imp_iff_right h, imp_iff_right h]
|
||||
else by
|
||||
|
||||
@@ -399,6 +399,19 @@ example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by ac_rfl
|
||||
-/
|
||||
syntax (name := acRfl) "ac_rfl" : tactic
|
||||
|
||||
/--
|
||||
`ac_nf` normalizes equalities up to application of an associative and commutative operator.
|
||||
```
|
||||
instance : Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩
|
||||
instance : Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩
|
||||
|
||||
example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by
|
||||
ac_nf
|
||||
-- goal: a + (b + (c + d)) = a + (b + (c + d))
|
||||
```
|
||||
-/
|
||||
syntax (name := acNf) "ac_nf" : tactic
|
||||
|
||||
/--
|
||||
The `sorry` tactic closes the goal using `sorryAx`. This is intended for stubbing out incomplete
|
||||
parts of a proof while still having a syntactically correct proof skeleton. Lean will give
|
||||
|
||||
@@ -249,8 +249,8 @@ theorem lex_def {r : α → α → Prop} {s : β → β → Prop} {p q : α ×
|
||||
Prod.Lex r s p q ↔ r p.1 q.1 ∨ p.1 = q.1 ∧ s p.2 q.2 :=
|
||||
⟨fun h => by cases h <;> simp [*], fun h =>
|
||||
match p, q, h with
|
||||
| (a, b), (c, d), Or.inl h => Lex.left _ _ h
|
||||
| (a, b), (c, d), Or.inr ⟨e, h⟩ => by subst e; exact Lex.right _ h⟩
|
||||
| _, _, Or.inl h => Lex.left _ _ h
|
||||
| (_, _), (_, _), Or.inr ⟨e, h⟩ => by subst e; exact Lex.right _ h⟩
|
||||
|
||||
namespace Lex
|
||||
|
||||
|
||||
@@ -305,15 +305,16 @@ def registerAttributeImplBuilder (builderId : Name) (builder : AttributeImplBuil
|
||||
if table.contains builderId then throw (IO.userError ("attribute implementation builder '" ++ toString builderId ++ "' has already been declared"))
|
||||
attributeImplBuilderTableRef.modify fun table => table.insert builderId builder
|
||||
|
||||
def mkAttributeImplOfBuilder (builderId ref : Name) (args : List DataValue) : IO AttributeImpl := do
|
||||
let table ← attributeImplBuilderTableRef.get
|
||||
match table[builderId]? with
|
||||
| none => throw (IO.userError ("unknown attribute implementation builder '" ++ toString builderId ++ "'"))
|
||||
| some builder => IO.ofExcept <| builder ref args
|
||||
structure AttributeExtensionOLeanEntry where
|
||||
builderId : Name
|
||||
ref : Name
|
||||
args : List DataValue
|
||||
|
||||
inductive AttributeExtensionOLeanEntry where
|
||||
| decl (declName : Name) -- `declName` has type `AttributeImpl`
|
||||
| builder (builderId ref : Name) (args : List DataValue)
|
||||
def mkAttributeImplOfEntry (e : AttributeExtensionOLeanEntry) : IO AttributeImpl := do
|
||||
let table ← attributeImplBuilderTableRef.get
|
||||
match table[e.builderId]? with
|
||||
| none => throw (IO.userError ("unknown attribute implementation builder '" ++ toString e.builderId ++ "'"))
|
||||
| some builder => IO.ofExcept <| builder e.ref e.args
|
||||
|
||||
structure AttributeExtensionState where
|
||||
newEntries : List AttributeExtensionOLeanEntry := []
|
||||
@@ -337,19 +338,13 @@ unsafe def mkAttributeImplOfConstantUnsafe (env : Environment) (opts : Options)
|
||||
@[implemented_by mkAttributeImplOfConstantUnsafe]
|
||||
opaque mkAttributeImplOfConstant (env : Environment) (opts : Options) (declName : Name) : Except String AttributeImpl
|
||||
|
||||
def mkAttributeImplOfEntry (env : Environment) (opts : Options) (e : AttributeExtensionOLeanEntry) : IO AttributeImpl :=
|
||||
match e with
|
||||
| .decl declName => IO.ofExcept <| mkAttributeImplOfConstant env opts declName
|
||||
| .builder builderId ref args => mkAttributeImplOfBuilder builderId ref args
|
||||
|
||||
private def AttributeExtension.addImported (es : Array (Array AttributeExtensionOLeanEntry)) : ImportM AttributeExtensionState := do
|
||||
let ctx ← read
|
||||
let map ← attributeMapRef.get
|
||||
let map ← es.foldlM
|
||||
(fun map entries =>
|
||||
entries.foldlM
|
||||
(fun (map : Std.HashMap Name AttributeImpl) entry => do
|
||||
let attrImpl ← mkAttributeImplOfEntry ctx.env ctx.opts entry
|
||||
let attrImpl ← mkAttributeImplOfEntry entry
|
||||
return map.insert attrImpl.name attrImpl)
|
||||
map)
|
||||
map
|
||||
@@ -400,19 +395,13 @@ def getAttributeImpl (env : Environment) (attrName : Name) : Except String Attri
|
||||
| some attr => pure attr
|
||||
| none => throw ("unknown attribute '" ++ toString attrName ++ "'")
|
||||
|
||||
def registerAttributeOfDecl (env : Environment) (opts : Options) (attrDeclName : Name) : Except String Environment := do
|
||||
let attrImpl ← mkAttributeImplOfConstant env opts attrDeclName
|
||||
if isAttribute env attrImpl.name then
|
||||
throw ("invalid builtin attribute declaration, '" ++ toString attrImpl.name ++ "' has already been used")
|
||||
else
|
||||
return attributeExtension.addEntry env (.decl attrDeclName, attrImpl)
|
||||
|
||||
def registerAttributeOfBuilder (env : Environment) (builderId ref : Name) (args : List DataValue) : IO Environment := do
|
||||
let attrImpl ← mkAttributeImplOfBuilder builderId ref args
|
||||
let entry := {builderId, ref, args}
|
||||
let attrImpl ← mkAttributeImplOfEntry entry
|
||||
if isAttribute env attrImpl.name then
|
||||
throw (IO.userError ("invalid builtin attribute declaration, '" ++ toString attrImpl.name ++ "' has already been used"))
|
||||
else
|
||||
return attributeExtension.addEntry env (.builder builderId ref args, attrImpl)
|
||||
return attributeExtension.addEntry env (entry, attrImpl)
|
||||
|
||||
def Attribute.add (declName : Name) (attrName : Name) (stx : Syntax) (kind := AttributeKind.global) : AttrM Unit := do
|
||||
let attr ← ofExcept <| getAttributeImpl (← getEnv) attrName
|
||||
|
||||
@@ -20,18 +20,18 @@ def ensureHasDefault (alts : Array Alt) : Array Alt :=
|
||||
private def getOccsOf (alts : Array Alt) (i : Nat) : Nat := Id.run do
|
||||
let aBody := (alts.get! i).body
|
||||
let mut n := 1
|
||||
for j in [i+1:alts.size] do
|
||||
if alts[j]!.body == aBody then
|
||||
for h : j in [i+1:alts.size] do
|
||||
if alts[j].body == aBody then
|
||||
n := n+1
|
||||
return n
|
||||
|
||||
private def maxOccs (alts : Array Alt) : Alt × Nat := Id.run do
|
||||
let mut maxAlt := alts[0]!
|
||||
let mut max := getOccsOf alts 0
|
||||
for i in [1:alts.size] do
|
||||
for h : i in [1:alts.size] do
|
||||
let curr := getOccsOf alts i
|
||||
if curr > max then
|
||||
maxAlt := alts[i]!
|
||||
maxAlt := alts[i]
|
||||
max := curr
|
||||
return (maxAlt, max)
|
||||
|
||||
|
||||
@@ -110,8 +110,8 @@ def isCtorParam (f : Expr) (i : Nat) : CoreM Bool := do
|
||||
def checkAppArgs (f : Expr) (args : Array Arg) : CheckM Unit := do
|
||||
let mut fType ← inferType f
|
||||
let mut j := 0
|
||||
for i in [:args.size] do
|
||||
let arg := args[i]!
|
||||
for h : i in [:args.size] do
|
||||
let arg := args[i]
|
||||
if fType.isErased then
|
||||
return ()
|
||||
fType := fType.headBeta
|
||||
|
||||
@@ -505,8 +505,8 @@ ones. Return whether any `Value` got updated in the process.
|
||||
-/
|
||||
def inferStep : InterpM Bool := do
|
||||
let ctx ← read
|
||||
for idx in [0:ctx.decls.size] do
|
||||
let decl := ctx.decls[idx]!
|
||||
for h : idx in [0:ctx.decls.size] do
|
||||
let decl := ctx.decls[idx]
|
||||
if !decl.safe then
|
||||
continue
|
||||
|
||||
|
||||
@@ -48,8 +48,8 @@ def hasTrivialStructure? (declName : Name) : CoreM (Option TrivialStructureInfo)
|
||||
let [ctorName] := info.ctors | return none
|
||||
let mask ← getRelevantCtorFields ctorName
|
||||
let mut result := none
|
||||
for i in [:mask.size] do
|
||||
if mask[i]! then
|
||||
for h : i in [:mask.size] do
|
||||
if mask[i] then
|
||||
if result.isSome then return none
|
||||
result := some { ctorName, fieldIdx := i, numParams := info.numParams }
|
||||
return result
|
||||
@@ -129,4 +129,4 @@ def getOtherDeclMonoType (declName : Name) : CoreM Expr := do
|
||||
modifyEnv fun env => monoTypeExt.modifyState env fun s => { s with mono := s.mono.insert declName type }
|
||||
return type
|
||||
|
||||
end Lean.Compiler.LCNF
|
||||
end Lean.Compiler.LCNF
|
||||
|
||||
@@ -96,9 +96,9 @@ where
|
||||
unless (← visited i) do
|
||||
modify fun (k, visited) => (k, visited.set! i true)
|
||||
let pi := ps[i]!
|
||||
for j in [:ps.size] do
|
||||
for h : j in [:ps.size] do
|
||||
unless (← visited j) do
|
||||
let pj := ps[j]!
|
||||
let pj := ps[j]
|
||||
if pj.used.contains pi.decl.fvarId then
|
||||
visit j
|
||||
modify fun (k, visited) => (pi.attach k, visited)
|
||||
|
||||
@@ -18,10 +18,10 @@ or not.
|
||||
private def getMaxOccs (alts : Array Alt) : Alt × Nat := Id.run do
|
||||
let mut maxAlt := alts[0]!
|
||||
let mut max := getNumOccsOf alts 0
|
||||
for i in [1:alts.size] do
|
||||
for h : i in [1:alts.size] do
|
||||
let curr := getNumOccsOf alts i
|
||||
if curr > max then
|
||||
maxAlt := alts[i]!
|
||||
maxAlt := alts[i]
|
||||
max := curr
|
||||
return (maxAlt, max)
|
||||
where
|
||||
@@ -34,8 +34,8 @@ where
|
||||
getNumOccsOf (alts : Array Alt) (i : Nat) : Nat := Id.run do
|
||||
let code := alts[i]!.getCode
|
||||
let mut n := 1
|
||||
for j in [i+1:alts.size] do
|
||||
if Code.alphaEqv alts[j]!.getCode code then
|
||||
for h : j in [i+1:alts.size] do
|
||||
if Code.alphaEqv alts[j].getCode code then
|
||||
n := n+1
|
||||
return n
|
||||
|
||||
|
||||
@@ -121,8 +121,8 @@ where
|
||||
let mut paramsNew := #[]
|
||||
let singleton : FVarIdSet := ({} : FVarIdSet).insert params[targetParamIdx]!.fvarId
|
||||
let dependsOnDiscr := k.dependsOn singleton || decls.any (·.dependsOn singleton)
|
||||
for i in [:params.size] do
|
||||
let param := params[i]!
|
||||
for h : i in [:params.size] do
|
||||
let param := params[i]
|
||||
if targetParamIdx == i then
|
||||
if dependsOnDiscr then
|
||||
paramsNew := paramsNew.push (← internalizeParam param)
|
||||
@@ -300,4 +300,3 @@ builtin_initialize
|
||||
registerTraceClass `Compiler.simp.jpCases
|
||||
|
||||
end Lean.Compiler.LCNF
|
||||
|
||||
|
||||
@@ -129,9 +129,9 @@ See comment at `.fixedNeutral`.
|
||||
-/
|
||||
private def hasFwdDeps (decl : Decl) (paramsInfo : Array SpecParamInfo) (j : Nat) : Bool := Id.run do
|
||||
let param := decl.params[j]!
|
||||
for k in [j+1 : decl.params.size] do
|
||||
for h : k in [j+1 : decl.params.size] do
|
||||
if paramsInfo[k]! matches .user | .fixedHO | .fixedInst then
|
||||
let param' := decl.params[k]!
|
||||
let param' := decl.params[k]
|
||||
if param'.type.containsFVar param.fvarId then
|
||||
return true
|
||||
return false
|
||||
@@ -214,4 +214,3 @@ builtin_initialize
|
||||
registerTraceClass `Compiler.specialize.info
|
||||
|
||||
end Lean.Compiler.LCNF
|
||||
|
||||
|
||||
@@ -50,9 +50,9 @@ partial def inlineMatchers (e : Expr) : CoreM Expr :=
|
||||
let numAlts := info.numAlts
|
||||
let altNumParams := info.altNumParams
|
||||
let rec inlineMatcher (i : Nat) (args : Array Expr) (letFVars : Array Expr) : MetaM Expr := do
|
||||
if i < numAlts then
|
||||
if h : i < numAlts then
|
||||
let altIdx := i + info.getFirstAltPos
|
||||
let numParams := altNumParams[i]!
|
||||
let numParams := altNumParams[i]
|
||||
let alt ← normalizeAlt args[altIdx]! numParams
|
||||
Meta.withLetDecl (← mkFreshUserName `_alt) (← Meta.inferType alt) alt fun altFVar =>
|
||||
inlineMatcher (i+1) (args.set! altIdx altFVar) (letFVars.push altFVar)
|
||||
|
||||
@@ -421,8 +421,8 @@ private def findNamedArgDependsOnCurrent? : M (Option NamedArg) := do
|
||||
else
|
||||
forallTelescopeReducing s.fType fun xs _ => do
|
||||
let curr := xs[0]!
|
||||
for i in [1:xs.size] do
|
||||
let xDecl ← xs[i]!.fvarId!.getDecl
|
||||
for h : i in [1:xs.size] do
|
||||
let xDecl ← xs[i].fvarId!.getDecl
|
||||
if let some arg := s.namedArgs.find? fun arg => arg.name == xDecl.userName then
|
||||
/- Remark: a default value at `optParam` does not count as a dependency -/
|
||||
if (← exprDependsOn xDecl.type.cleanupAnnotations curr.fvarId!) then
|
||||
@@ -800,8 +800,8 @@ def getElabElimExprInfo (elimExpr : Expr) : MetaM ElabElimInfo := do
|
||||
return s
|
||||
/- Collect the major parameter positions -/
|
||||
let mut majorsPos := #[]
|
||||
for i in [:xs.size] do
|
||||
let x := xs[i]!
|
||||
for h : i in [:xs.size] do
|
||||
let x := xs[i]
|
||||
unless motivePos == i do
|
||||
let xType ← x.fvarId!.getType
|
||||
/-
|
||||
@@ -1301,8 +1301,8 @@ private def addLValArg (baseName : Name) (fullName : Name) (e : Expr) (args : Ar
|
||||
forallTelescopeReducing fType fun xs _ => do
|
||||
let mut argIdx := 0 -- position of the next explicit argument
|
||||
let mut remainingNamedArgs := namedArgs
|
||||
for i in [:xs.size] do
|
||||
let x := xs[i]!
|
||||
for h : i in [:xs.size] do
|
||||
let x := xs[i]
|
||||
let xDecl ← x.fvarId!.getDecl
|
||||
/- If there is named argument with name `xDecl.userName`, then we skip it. -/
|
||||
match remainingNamedArgs.findIdx? (fun namedArg => namedArg.name == xDecl.userName) with
|
||||
|
||||
@@ -55,8 +55,8 @@ open Meta
|
||||
let cinfo ← getConstInfoCtor ctor
|
||||
let numExplicitFields ← forallTelescopeReducing cinfo.type fun xs _ => do
|
||||
let mut n := 0
|
||||
for i in [cinfo.numParams:xs.size] do
|
||||
if (← getFVarLocalDecl xs[i]!).binderInfo.isExplicit then
|
||||
for h : i in [cinfo.numParams:xs.size] do
|
||||
if (← getFVarLocalDecl xs[i]).binderInfo.isExplicit then
|
||||
n := n + 1
|
||||
return n
|
||||
let args := args.getElems
|
||||
|
||||
@@ -64,13 +64,13 @@ private partial def winnowExpr (e : Expr) : MetaM Expr := do
|
||||
let mut fty ← inferType f
|
||||
let mut j := 0
|
||||
let mut e' ← visit f
|
||||
for i in [0:args.size] do
|
||||
for h : i in [0:args.size] do
|
||||
unless fty.isForall do
|
||||
fty ← withTransparency .all <| whnf <| fty.instantiateRevRange j i args
|
||||
j := i
|
||||
let .forallE _ _ fty' bi := fty | failure
|
||||
fty := fty'
|
||||
let arg := args[i]!
|
||||
let arg := args[i]
|
||||
if ← pure bi.isExplicit <||> (pure !arg.isSort <&&> isTypeFormer arg) then
|
||||
unless (← isProof arg) do
|
||||
e' := .app e' (← visit arg)
|
||||
@@ -206,8 +206,11 @@ Uses heuristics to generate an informative but terse base name for a term of the
|
||||
Makes use of the current namespace.
|
||||
It tries to make these names relatively unique ecosystem-wide,
|
||||
and it adds suffixes using the current module if the resulting name doesn't refer to anything defined in this module.
|
||||
|
||||
If any constant in `type` has a name with macro scopes, then the result will be a name with fresh macro scopes.
|
||||
While in this case we could skip the naming heuristics, we still want informative names for debugging purposes.
|
||||
-/
|
||||
def mkBaseNameWithSuffix (pre : String) (type : Expr) : MetaM String := do
|
||||
def mkBaseNameWithSuffix (pre : String) (type : Expr) : MetaM Name := do
|
||||
let (name, st) ← mkBaseName type |>.run {}
|
||||
let name := pre ++ name
|
||||
let project := (← getMainModule).getRoot
|
||||
@@ -217,8 +220,13 @@ def mkBaseNameWithSuffix (pre : String) (type : Expr) : MetaM String := do
|
||||
let isModuleLocal := modules.any Option.isNone
|
||||
-- We can also avoid adding the full module suffix if the instance refers to "project"-local names.
|
||||
let isProjectLocal := isModuleLocal || modules.any fun mod? => mod?.map (·.getRoot) == project
|
||||
if !isProjectLocal then
|
||||
return s!"{name}{moduleToSuffix project}"
|
||||
let name := Name.mkSimple <|
|
||||
if !isProjectLocal then
|
||||
s!"{name}{moduleToSuffix project}"
|
||||
else
|
||||
name
|
||||
if Option.isSome <| type.find? (fun e => if let .const n _ := e then n.hasMacroScopes else false) then
|
||||
mkFreshUserName name
|
||||
else
|
||||
return name
|
||||
|
||||
@@ -233,8 +241,8 @@ def mkBaseNameWithSuffix' (pre : String) (binders : Array Syntax) (type : Syntax
|
||||
let ty ← mkForallFVars binds (← Term.elabType type)
|
||||
mkBaseNameWithSuffix pre ty
|
||||
catch _ =>
|
||||
pure pre
|
||||
liftMacroM <| mkUnusedBaseName <| Name.mkSimple name
|
||||
mkFreshUserName <| Name.mkSimple pre
|
||||
liftMacroM <| mkUnusedBaseName name
|
||||
|
||||
end NameGen
|
||||
|
||||
|
||||
@@ -86,8 +86,8 @@ where
|
||||
addLocalInstancesForParams xs[:ctorVal.numParams] fun localInst2Index => do
|
||||
let mut usedInstIdxs := {}
|
||||
let mut ok := true
|
||||
for i in [ctorVal.numParams:xs.size] do
|
||||
let x := xs[i]!
|
||||
for h : i in [ctorVal.numParams:xs.size] do
|
||||
let x := xs[i]
|
||||
let instType ← mkAppM `Inhabited #[(← inferType x)]
|
||||
trace[Elab.Deriving.inhabited] "checking {instType} for '{ctorName}'"
|
||||
match (← trySynthInstance instType) with
|
||||
|
||||
@@ -29,8 +29,8 @@ def mkBodyForStruct (header : Header) (indVal : InductiveVal) : TermElabM Term :
|
||||
let mut fields ← `(Format.nil)
|
||||
if xs.size != numParams + fieldNames.size then
|
||||
throwError "'deriving Repr' failed, unexpected number of fields in structure"
|
||||
for i in [:fieldNames.size] do
|
||||
let fieldName := fieldNames[i]!
|
||||
for h : i in [:fieldNames.size] do
|
||||
let fieldName := fieldNames[i]
|
||||
let fieldNameLit := Syntax.mkStrLit (toString fieldName)
|
||||
let x := xs[numParams + i]!
|
||||
if i != 0 then
|
||||
@@ -59,10 +59,10 @@ where
|
||||
let mut ctorArgs := #[]
|
||||
let mut rhs : Term := Syntax.mkStrLit (toString ctorInfo.name)
|
||||
rhs ← `(Format.text $rhs)
|
||||
for i in [:xs.size] do
|
||||
for h : i in [:xs.size] do
|
||||
-- Note: some inductive parameters are explicit if they were promoted from indices,
|
||||
-- so we process all constructor arguments in the same loop.
|
||||
let x := xs[i]!
|
||||
let x := xs[i]
|
||||
let a ← mkIdent <$> if i < indVal.numParams then pure header.argNames[i]! else mkFreshUserName `a
|
||||
if i < indVal.numParams then
|
||||
-- add `_` for inductive parameters, they are inaccessible
|
||||
|
||||
@@ -513,7 +513,7 @@ partial def extendUpdatedVarsAux (c : Code) (ws : VarSet) : TermElabM Code :=
|
||||
| .ite ref none o c t e => return .ite ref none o c (← update t) (← update e)
|
||||
| .ite ref (some h) o cond t e =>
|
||||
if ws.contains h.getId then
|
||||
-- if the `h` at `if h:c then t else e` shadows a variable in `ws`, we `pullExitPoints`
|
||||
-- if the `h` at `if h : c then t else e` shadows a variable in `ws`, we `pullExitPoints`
|
||||
pullExitPoints c
|
||||
else
|
||||
return Code.ite ref (some h) o cond (← update t) (← update e)
|
||||
|
||||
@@ -168,8 +168,8 @@ private def checkHeader (r : ElabHeaderResult) (numParams : Nat) (firstType? : O
|
||||
|
||||
-- Auxiliary function for checking whether the types in mutually inductive declaration are compatible.
|
||||
private partial def checkHeaders (rs : Array ElabHeaderResult) (numParams : Nat) (i : Nat) (firstType? : Option Expr) : TermElabM Unit := do
|
||||
if i < rs.size then
|
||||
let type ← checkHeader rs[i]! numParams firstType?
|
||||
if h : i < rs.size then
|
||||
let type ← checkHeader rs[i] numParams firstType?
|
||||
checkHeaders rs numParams (i+1) type
|
||||
|
||||
private def elabHeader (views : Array InductiveView) : TermElabM (Array ElabHeaderResult) := do
|
||||
@@ -222,11 +222,11 @@ private def replaceArrowBinderNames (type : Expr) (newNames : Array Name) : Expr
|
||||
go type 0
|
||||
where
|
||||
go (type : Expr) (i : Nat) : Expr :=
|
||||
if i < newNames.size then
|
||||
if h : i < newNames.size then
|
||||
match type with
|
||||
| .forallE n d b bi =>
|
||||
if n.hasMacroScopes then
|
||||
mkForall newNames[i]! bi d (go b (i+1))
|
||||
mkForall newNames[i] bi d (go b (i+1))
|
||||
else
|
||||
mkForall n bi d (go b (i+1))
|
||||
| _ => type
|
||||
|
||||
@@ -330,8 +330,8 @@ private def elabPatterns (patternStxs : Array Syntax) (matchType : Expr) : Excep
|
||||
withReader (fun ctx => { ctx with implicitLambda := false }) do
|
||||
let mut patterns := #[]
|
||||
let mut matchType := matchType
|
||||
for idx in [:patternStxs.size] do
|
||||
let patternStx := patternStxs[idx]!
|
||||
for h : idx in [:patternStxs.size] do
|
||||
let patternStx := patternStxs[idx]
|
||||
matchType ← whnf matchType
|
||||
match matchType with
|
||||
| Expr.forallE _ d b _ =>
|
||||
|
||||
@@ -406,9 +406,9 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
|
||||
(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.
|
||||
for i in [0:header.binderIds.size] do
|
||||
for h : i in [0:header.binderIds.size] do
|
||||
-- skip auto-bound prefix in `xs`
|
||||
addLocalVarInfo header.binderIds[i]! xs[header.numParams - header.binderIds.size + i]!
|
||||
addLocalVarInfo header.binderIds[i] xs[header.numParams - header.binderIds.size + i]!
|
||||
let val ← withReader ({ · with tacSnap? := header.tacSnap? }) do
|
||||
-- synthesize mvars here to force the top-level tactic block (if any) to run
|
||||
elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
|
||||
|
||||
@@ -77,9 +77,9 @@ def mkEqns (declName : Name) (info : DefinitionVal) : MetaM (Array Name) :=
|
||||
withReducible do
|
||||
mkEqnTypes #[] goal.mvarId!
|
||||
let mut thmNames := #[]
|
||||
for i in [: eqnTypes.size] do
|
||||
let type := eqnTypes[i]!
|
||||
trace[Elab.definition.eqns] "eqnType[{i}]: {eqnTypes[i]!}"
|
||||
for h : i in [: eqnTypes.size] do
|
||||
let type := eqnTypes[i]
|
||||
trace[Elab.definition.eqns] "eqnType[{i}]: {eqnTypes[i]}"
|
||||
let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1)
|
||||
thmNames := thmNames.push name
|
||||
let value ← mkProof declName type
|
||||
|
||||
@@ -67,8 +67,8 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
|
||||
mkEqnTypes info.declNames goal.mvarId!
|
||||
let baseName := info.declName
|
||||
let mut thmNames := #[]
|
||||
for i in [: eqnTypes.size] do
|
||||
let type := eqnTypes[i]!
|
||||
for h : i in [: eqnTypes.size] do
|
||||
let type := eqnTypes[i]
|
||||
trace[Elab.definition.structural.eqns] "eqnType {i}: {type}"
|
||||
let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1)
|
||||
thmNames := thmNames.push name
|
||||
|
||||
@@ -83,9 +83,9 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
|
||||
withReducible do
|
||||
mkEqnTypes info.declNames goal.mvarId!
|
||||
let mut thmNames := #[]
|
||||
for i in [: eqnTypes.size] do
|
||||
let type := eqnTypes[i]!
|
||||
trace[Elab.definition.wf.eqns] "{eqnTypes[i]!}"
|
||||
for h : i in [: eqnTypes.size] do
|
||||
let type := eqnTypes[i]
|
||||
trace[Elab.definition.wf.eqns] "{eqnTypes[i]}"
|
||||
let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1)
|
||||
thmNames := thmNames.push name
|
||||
let value ← mkProof declName type
|
||||
|
||||
@@ -655,9 +655,9 @@ The parameter `alts` provides position information for alternatives.
|
||||
-/
|
||||
private def checkUnusedAlts (stx : Syntax) (alts : Array Syntax) (altIdxMap : NameMap Nat) (ignoreIfUnused : IdxSet) : TermElabM Syntax := do
|
||||
let (stx, used) ← findUsedAlts stx altIdxMap
|
||||
for i in [:alts.size] do
|
||||
for h : i in [:alts.size] do
|
||||
unless used.contains i || ignoreIfUnused.contains i do
|
||||
logErrorAt alts[i]! s!"redundant alternative #{i+1}"
|
||||
logErrorAt alts[i] s!"redundant alternative #{i+1}"
|
||||
return stx
|
||||
|
||||
def match_syntax.expand (stx : Syntax) : TermElabM Syntax := do
|
||||
|
||||
@@ -733,7 +733,8 @@ private def addDefaults (lctx : LocalContext) (defaultAuxDecls : Array (Name ×
|
||||
throwError "invalid default value for field, it contains metavariables{indentExpr value}"
|
||||
/- The identity function is used as "marker". -/
|
||||
let value ← mkId value
|
||||
discard <| mkAuxDefinition declName type value (zetaDelta := true)
|
||||
-- No need to compile the definition, since it is only used during elaboration.
|
||||
discard <| mkAuxDefinition declName type value (zetaDelta := true) (compile := false)
|
||||
setReducibleAttribute declName
|
||||
|
||||
/--
|
||||
|
||||
@@ -257,8 +257,8 @@ private def throwStuckAtUniverseCnstr : TermElabM Unit := do
|
||||
unless found.contains (lhs, rhs) do
|
||||
found := found.insert (lhs, rhs)
|
||||
uniqueEntries := uniqueEntries.push entry
|
||||
for i in [1:uniqueEntries.size] do
|
||||
logErrorAt uniqueEntries[i]!.ref (← mkLevelStuckErrorMessage uniqueEntries[i]!)
|
||||
for h : i in [1:uniqueEntries.size] do
|
||||
logErrorAt uniqueEntries[i].ref (← mkLevelStuckErrorMessage uniqueEntries[i]!)
|
||||
throwErrorAt uniqueEntries[0]!.ref (← mkLevelStuckErrorMessage uniqueEntries[0]!)
|
||||
|
||||
/--
|
||||
|
||||
@@ -55,9 +55,9 @@ def evalBvCheck : Tactic := fun
|
||||
| `(tactic| bv_check%$tk $path:str) => do
|
||||
let cfg ← BVDecide.Frontend.BVCheck.mkContext path.getString
|
||||
liftMetaFinishingTactic fun g => do
|
||||
let res ← Normalize.bvNormalize g
|
||||
match res.goal with
|
||||
| some g => bvCheck g cfg
|
||||
let g'? ← Normalize.bvNormalize g
|
||||
match g'? with
|
||||
| some g' => bvCheck g' cfg
|
||||
| none =>
|
||||
let bvNormalizeStx ← `(tactic| bv_normalize)
|
||||
TryThis.addSuggestion tk bvNormalizeStx (origSpan? := ← getRef)
|
||||
|
||||
@@ -265,10 +265,6 @@ def bvUnsat (g : MVarId) (cfg : TacticContext) : MetaM (Except CounterExample Lr
|
||||
The result of calling `bv_decide`.
|
||||
-/
|
||||
structure Result where
|
||||
/--
|
||||
Trace of the `simp` used in `bv_decide`'s normalization procedure.
|
||||
-/
|
||||
simpTrace : Simp.Stats
|
||||
/--
|
||||
If the normalization step was not enough to solve the goal this contains the LRAT proof
|
||||
certificate.
|
||||
@@ -280,10 +276,10 @@ Try to close `g` using a bitblaster. Return either a `CounterExample` if one is
|
||||
if `g` is proven.
|
||||
-/
|
||||
def bvDecide' (g : MVarId) (cfg : TacticContext) : MetaM (Except CounterExample Result) := do
|
||||
let ⟨g?, simpTrace⟩ ← Normalize.bvNormalize g
|
||||
let some g := g? | return .ok ⟨simpTrace, none⟩
|
||||
let g? ← Normalize.bvNormalize g
|
||||
let some g := g? | return .ok ⟨none⟩
|
||||
match ← bvUnsat g cfg with
|
||||
| .ok lratCert => return .ok ⟨simpTrace, some lratCert⟩
|
||||
| .ok lratCert => return .ok ⟨some lratCert⟩
|
||||
| .error counterExample => return .error counterExample
|
||||
|
||||
/--
|
||||
|
||||
@@ -89,7 +89,7 @@ where
|
||||
M (Option ReifiedBVPred) := do
|
||||
let some lhs ← ReifiedBVExpr.of lhsExpr | return none
|
||||
let some rhs ← ReifiedBVExpr.of rhsExpr | return none
|
||||
if h:lhs.width = rhs.width then
|
||||
if h : lhs.width = rhs.width then
|
||||
let bvExpr : BVPred := .bin (w := lhs.width) lhs.bvExpr pred (h ▸ rhs.bvExpr)
|
||||
let expr :=
|
||||
mkApp4
|
||||
|
||||
@@ -37,40 +37,102 @@ builtin_simproc [bv_normalize] eqToBEq (((_ : Bool) = (_ : Bool))) := fun e => d
|
||||
let proof := mkApp2 (mkConst ``Bool.eq_to_beq) lhs rhs
|
||||
return .done { expr := new, proof? := some proof }
|
||||
|
||||
structure Result where
|
||||
goal : Option MVarId := none
|
||||
stats : Simp.Stats := {}
|
||||
builtin_simproc [bv_normalize] andOnes ((_ : BitVec _) &&& (_ : BitVec _)) := fun e => do
|
||||
let_expr HAnd.hAnd _ _ _ _ lhs rhs := e | return .continue
|
||||
let some ⟨w, rhsValue⟩ ← getBitVecValue? rhs | return .continue
|
||||
if rhsValue == -1#w then
|
||||
let proof := mkApp2 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.and_ones) (toExpr w) lhs
|
||||
return .visit { expr := lhs, proof? := some proof }
|
||||
else
|
||||
return .continue
|
||||
|
||||
def bvNormalize (g : MVarId) : MetaM Result := do
|
||||
builtin_simproc [bv_normalize] onesAnd ((_ : BitVec _) &&& (_ : BitVec _)) := fun e => do
|
||||
let_expr HAnd.hAnd _ _ _ _ lhs rhs := e | return .continue
|
||||
let some ⟨w, lhsValue⟩ ← getBitVecValue? lhs | return .continue
|
||||
if lhsValue == -1#w then
|
||||
let proof := mkApp2 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.ones_and) (toExpr w) rhs
|
||||
return .visit { expr := rhs, proof? := some proof }
|
||||
else
|
||||
return .continue
|
||||
|
||||
builtin_simproc [bv_normalize] maxUlt (BitVec.ult (_ : BitVec _) (_ : BitVec _)) := fun e => do
|
||||
let_expr BitVec.ult _ lhs rhs := e | return .continue
|
||||
let some ⟨w, lhsValue⟩ ← getBitVecValue? lhs | return .continue
|
||||
if lhsValue == -1#w then
|
||||
let proof := mkApp2 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.max_ult') (toExpr w) rhs
|
||||
return .visit { expr := toExpr Bool.false, proof? := some proof }
|
||||
else
|
||||
return .continue
|
||||
|
||||
/--
|
||||
A pass in the normalization pipeline. Takes the current goal and produces a refined one or closes
|
||||
the goal fully, indicated by returning `none`.
|
||||
-/
|
||||
abbrev Pass := MVarId → MetaM (Option MVarId)
|
||||
|
||||
namespace Pass
|
||||
|
||||
/--
|
||||
Repeatedly run a list of `Pass` until they either close the goal or an iteration doesn't change
|
||||
the goal anymore.
|
||||
-/
|
||||
partial def fixpointPipeline (passes : List Pass) (goal : MVarId) : MetaM (Option MVarId) := do
|
||||
let runPass (goal? : Option MVarId) (pass : Pass) : MetaM (Option MVarId) := do
|
||||
let some goal := goal? | return none
|
||||
pass goal
|
||||
|
||||
let some newGoal := ← passes.foldlM (init := some goal) runPass | return none
|
||||
if goal != newGoal then
|
||||
trace[Meta.Tactic.bv] m!"Rerunning pipeline on:\n{newGoal}"
|
||||
fixpointPipeline passes newGoal
|
||||
else
|
||||
trace[Meta.Tactic.bv] "Pipeline reached a fixpoint"
|
||||
return newGoal
|
||||
|
||||
/--
|
||||
Responsible for applying the Bitwuzla style rewrite rules.
|
||||
-/
|
||||
def rewriteRulesPass : Pass := fun goal => do
|
||||
let bvThms ← bvNormalizeExt.getTheorems
|
||||
let bvSimprocs ← bvNormalizeSimprocExt.getSimprocs
|
||||
let sevalThms ← getSEvalTheorems
|
||||
let sevalSimprocs ← Simp.getSEvalSimprocs
|
||||
|
||||
let simpCtx : Simp.Context := {
|
||||
config := { failIfUnchanged := false, zetaDelta := true }
|
||||
simpTheorems := #[bvThms, sevalThms]
|
||||
congrTheorems := (← getSimpCongrTheorems)
|
||||
}
|
||||
|
||||
let hyps ← goal.getNondepPropHyps
|
||||
let ⟨result?, _⟩ ← simpGoal goal
|
||||
(ctx := simpCtx)
|
||||
(simprocs := #[bvSimprocs, sevalSimprocs])
|
||||
(fvarIdsToSimp := hyps)
|
||||
let some (_, newGoal) := result? | return none
|
||||
return newGoal
|
||||
|
||||
/--
|
||||
The normalization passes used by `bv_normalize` and thus `bv_decide`.
|
||||
-/
|
||||
def defaultPipeline : List Pass := [rewriteRulesPass]
|
||||
|
||||
end Pass
|
||||
|
||||
def bvNormalize (g : MVarId) : MetaM (Option MVarId) := do
|
||||
withTraceNode `bv (fun _ => return "Normalizing goal") do
|
||||
-- Contradiction proof
|
||||
let some g ← g.falseOrByContra | return {}
|
||||
|
||||
-- Normalization by simp
|
||||
let bvThms ← bvNormalizeExt.getTheorems
|
||||
let bvSimprocs ← bvNormalizeSimprocExt.getSimprocs
|
||||
let sevalThms ← getSEvalTheorems
|
||||
let sevalSimprocs ← Simp.getSEvalSimprocs
|
||||
|
||||
let simpCtx : Simp.Context := {
|
||||
config := { failIfUnchanged := false, zetaDelta := true }
|
||||
simpTheorems := #[bvThms, sevalThms]
|
||||
congrTheorems := (← getSimpCongrTheorems)
|
||||
}
|
||||
|
||||
let hyps ← g.getNondepPropHyps
|
||||
let ⟨result?, stats⟩ ← simpGoal g
|
||||
(ctx := simpCtx)
|
||||
(simprocs := #[bvSimprocs, sevalSimprocs])
|
||||
(fvarIdsToSimp := hyps)
|
||||
let some (_, g) := result? | return ⟨none, stats⟩
|
||||
return ⟨some g, stats⟩
|
||||
let some g ← g.falseOrByContra | return none
|
||||
trace[Meta.Tactic.bv] m!"Running preprocessing pipeline on:\n{g}"
|
||||
Pass.fixpointPipeline Pass.defaultPipeline g
|
||||
|
||||
@[builtin_tactic Lean.Parser.Tactic.bvNormalize]
|
||||
def evalBVNormalize : Tactic := fun
|
||||
| `(tactic| bv_normalize) => do
|
||||
liftMetaFinishingTactic fun g => do
|
||||
discard <| bvNormalize g
|
||||
let g ← getMainGoal
|
||||
match ← bvNormalize g with
|
||||
| some newGoal => setGoals [newGoal]
|
||||
| none => setGoals []
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
end Frontend.Normalize
|
||||
|
||||
@@ -205,8 +205,8 @@ private def isWildcard (altStx : Syntax) : Bool :=
|
||||
getAltName altStx == `_
|
||||
|
||||
private def checkAltNames (alts : Array Alt) (altsSyntax : Array Syntax) : TacticM Unit :=
|
||||
for i in [:altsSyntax.size] do
|
||||
let altStx := altsSyntax[i]!
|
||||
for h : i in [:altsSyntax.size] do
|
||||
let altStx := altsSyntax[i]
|
||||
if getAltName altStx == `_ && i != altsSyntax.size - 1 then
|
||||
withRef altStx <| throwError "invalid occurrence of wildcard alternative, it must be the last alternative"
|
||||
let altName := getAltName altStx
|
||||
@@ -236,8 +236,8 @@ private def saveAltVarsInfo (altMVarId : MVarId) (altStx : Syntax) (fvarIds : Ar
|
||||
let altVars := getAltVars altStx
|
||||
for fvarId in fvarIds do
|
||||
if !useNamesForExplicitOnly || (← fvarId.getDecl).binderInfo.isExplicit then
|
||||
if i < altVars.size then
|
||||
Term.addLocalVarInfo altVars[i]! (mkFVar fvarId)
|
||||
if h : i < altVars.size then
|
||||
Term.addLocalVarInfo altVars[i] (mkFVar fvarId)
|
||||
i := i + 1
|
||||
|
||||
open Language in
|
||||
@@ -320,8 +320,8 @@ where
|
||||
2- The errors are produced in the same order the appear in the code above. This is not super
|
||||
important when using IDEs.
|
||||
-/
|
||||
for altStxIdx in [0:altStxs.size] do
|
||||
let altStx := altStxs[altStxIdx]!
|
||||
for h : altStxIdx in [0:altStxs.size] do
|
||||
let altStx := altStxs[altStxIdx]
|
||||
let altName := getAltName altStx
|
||||
if let some i := alts.findIdx? (·.1 == altName) then
|
||||
-- cover named alternative
|
||||
|
||||
@@ -513,13 +513,13 @@ def fourierMotzkinSelect (data : Array FourierMotzkinData) : MetaM FourierMotzki
|
||||
if bestSize = 0 then
|
||||
trace[omega] "Selected variable {data[0]!.var}."
|
||||
return data[0]!
|
||||
for i in [1:data.size] do
|
||||
let exact := data[i]!.exact
|
||||
let size := data[i]!.size
|
||||
for h : i in [1:data.size] do
|
||||
let exact := data[i].exact
|
||||
let size := data[i].size
|
||||
if size = 0 || !bestExact && exact || (bestExact == exact) && size < bestSize then
|
||||
if size = 0 then
|
||||
trace[omega] "Selected variable {data[i]!.var}"
|
||||
return data[i]!
|
||||
trace[omega] "Selected variable {data[i].var}"
|
||||
return data[i]
|
||||
bestIdx := i
|
||||
bestExact := exact
|
||||
bestSize := size
|
||||
|
||||
@@ -765,8 +765,8 @@ where
|
||||
loop (i : Nat) (env : Environment) : IO Environment := do
|
||||
-- Recall that the size of the array stored `persistentEnvExtensionRef` may increase when we import user-defined environment extensions.
|
||||
let pExtDescrs ← persistentEnvExtensionsRef.get
|
||||
if i < pExtDescrs.size then
|
||||
let extDescr := pExtDescrs[i]!
|
||||
if h : i < pExtDescrs.size then
|
||||
let extDescr := pExtDescrs[i]
|
||||
let s := extDescr.toEnvExtension.getState env
|
||||
let prevSize := (← persistentEnvExtensionsRef.get).size
|
||||
let prevAttrSize ← getNumBuiltinAttributes
|
||||
@@ -858,7 +858,7 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
|
||||
numConsts + mod.constants.size + mod.extraConstNames.size
|
||||
let mut const2ModIdx : Std.HashMap Name ModuleIdx := Std.HashMap.empty (capacity := numConsts)
|
||||
let mut constantMap : Std.HashMap Name ConstantInfo := Std.HashMap.empty (capacity := numConsts)
|
||||
for h:modIdx in [0:s.moduleData.size] do
|
||||
for h : modIdx in [0:s.moduleData.size] do
|
||||
let mod := s.moduleData[modIdx]'h.upper
|
||||
for cname in mod.constNames, cinfo in mod.constants do
|
||||
match constantMap.getThenInsertIfNew? cname cinfo with
|
||||
@@ -1096,6 +1096,13 @@ def isDefEqGuarded (env : Environment) (lctx : LocalContext) (a b : Expr) : Bool
|
||||
@[extern "lean_kernel_whnf"]
|
||||
opaque whnf (env : Environment) (lctx : LocalContext) (a : Expr) : Except KernelException Expr
|
||||
|
||||
/--
|
||||
Kernel typecheck function. We use it mainly for debugging purposes.
|
||||
Recall that the Kernel type checker does not support metavariables.
|
||||
When implementing automation, consider using the `MetaM` methods. -/
|
||||
@[extern "lean_kernel_check"]
|
||||
opaque check (env : Environment) (lctx : LocalContext) (a : Expr) : Except KernelException Expr
|
||||
|
||||
end Kernel
|
||||
|
||||
class MonadEnv (m : Type → Type) where
|
||||
|
||||
@@ -385,14 +385,14 @@ def size (lctx : LocalContext) : Nat :=
|
||||
Id.run <| lctx.findDeclRevM? f
|
||||
|
||||
partial def isSubPrefixOfAux (a₁ a₂ : PArray (Option LocalDecl)) (exceptFVars : Array Expr) (i j : Nat) : Bool :=
|
||||
if i < a₁.size then
|
||||
match a₁[i]! with
|
||||
if h : i < a₁.size then
|
||||
match a₁[i] with
|
||||
| none => isSubPrefixOfAux a₁ a₂ exceptFVars (i+1) j
|
||||
| some decl₁ =>
|
||||
if exceptFVars.any fun fvar => fvar.fvarId! == decl₁.fvarId then
|
||||
isSubPrefixOfAux a₁ a₂ exceptFVars (i+1) j
|
||||
else if j < a₂.size then
|
||||
match a₂[j]! with
|
||||
else if h2 : j < a₂.size then
|
||||
match a₂[j] with
|
||||
| none => isSubPrefixOfAux a₁ a₂ exceptFVars i (j+1)
|
||||
| some decl₂ => if decl₁.fvarId == decl₂.fvarId then isSubPrefixOfAux a₁ a₂ exceptFVars (i+1) (j+1) else isSubPrefixOfAux a₁ a₂ exceptFVars i (j+1)
|
||||
else false
|
||||
|
||||
@@ -155,8 +155,8 @@ where
|
||||
if !infos[i]!.isInstImplicit then
|
||||
if !(← lt args[i]! b) then
|
||||
return false
|
||||
for i in [infos.size:args.size] do
|
||||
if !(← lt args[i]! b) then
|
||||
for h : i in [infos.size:args.size] do
|
||||
if !(← lt args[i] b) then
|
||||
return false
|
||||
return true
|
||||
| .lam _ d e .. => lt d b <&&> lt e b
|
||||
|
||||
@@ -277,7 +277,7 @@ private def mkAppMFinal (methodName : Name) (f : Expr) (args : Array Expr) (inst
|
||||
|
||||
private partial def mkAppMArgs (f : Expr) (fType : Expr) (xs : Array Expr) : MetaM Expr :=
|
||||
let rec loop (type : Expr) (i : Nat) (j : Nat) (args : Array Expr) (instMVars : Array MVarId) : MetaM Expr := do
|
||||
if i >= xs.size then
|
||||
if h : i >= xs.size then
|
||||
mkAppMFinal `mkAppM f args instMVars
|
||||
else match type with
|
||||
| Expr.forallE n d b bi =>
|
||||
@@ -293,7 +293,7 @@ private partial def mkAppMArgs (f : Expr) (fType : Expr) (xs : Array Expr) : Met
|
||||
let mvar ← mkFreshExprMVar d MetavarKind.synthetic n
|
||||
loop b i j (args.push mvar) (instMVars.push mvar.mvarId!)
|
||||
| _ =>
|
||||
let x := xs[i]!
|
||||
let x := xs[i]
|
||||
let xType ← inferType x
|
||||
if (← isDefEq d xType) then
|
||||
loop b (i+1) j (args.push x) instMVars
|
||||
|
||||
@@ -69,8 +69,8 @@ The `type` should be the expected type of the packed argument, as created with `
|
||||
partial def pack (type : Expr) (args : Array Expr) : Expr := go 0 type
|
||||
where
|
||||
go (i : Nat) (type : Expr) : Expr :=
|
||||
if i < args.size - 1 then
|
||||
let arg := args[i]!
|
||||
if h : i < args.size - 1 then
|
||||
let arg := args[i]
|
||||
assert! type.isAppOfArity ``PSigma 2
|
||||
let us := type.getAppFn.constLevels!
|
||||
let α := type.appFn!.appArg!
|
||||
|
||||
@@ -77,7 +77,7 @@ partial def mkHCongrWithArity (f : Expr) (numArgs : Nat) : MetaM CongrTheorem :=
|
||||
where
|
||||
withNewEqs {α} (xs ys : Array Expr) (k : Array Expr → Array CongrArgKind → MetaM α) : MetaM α :=
|
||||
let rec loop (i : Nat) (eqs : Array Expr) (kinds : Array CongrArgKind) := do
|
||||
if i < xs.size then
|
||||
if i < xs.size then
|
||||
let x := xs[i]!
|
||||
let y := ys[i]!
|
||||
let xType := (← inferType x).cleanupAnnotations
|
||||
@@ -185,11 +185,11 @@ private def getClassSubobjectMask? (f : Expr) : MetaM (Option (Array Bool)) := d
|
||||
forallTelescopeReducing val.type (cleanupAnnotations := true) fun xs _ => do
|
||||
let env ← getEnv
|
||||
let mut mask := #[]
|
||||
for i in [:xs.size] do
|
||||
for h : i in [:xs.size] do
|
||||
if i < val.numParams then
|
||||
mask := mask.push false
|
||||
else
|
||||
let localDecl ← xs[i]!.fvarId!.getDecl
|
||||
let localDecl ← xs[i].fvarId!.getDecl
|
||||
mask := mask.push (isSubobjectField? env val.induct localDecl.userName).isSome
|
||||
return some mask
|
||||
|
||||
@@ -211,14 +211,14 @@ def getCongrSimpKinds (f : Expr) (info : FunInfo) : MetaM (Array CongrArgKind) :
|
||||
-/
|
||||
let mut result := #[]
|
||||
let mask? ← getClassSubobjectMask? f
|
||||
for i in [:info.paramInfo.size] do
|
||||
for h : i in [:info.paramInfo.size] do
|
||||
if info.resultDeps.contains i then
|
||||
result := result.push .fixed
|
||||
else if info.paramInfo[i]!.isProp then
|
||||
else if info.paramInfo[i].isProp then
|
||||
result := result.push .cast
|
||||
else if info.paramInfo[i]!.isInstImplicit then
|
||||
else if info.paramInfo[i].isInstImplicit then
|
||||
if let some mask := mask? then
|
||||
if h : i < mask.size then
|
||||
if h2 : i < mask.size then
|
||||
if mask[i] then
|
||||
-- Parameter is a subobect field of a class constructor. See comment above.
|
||||
result := result.push .eq
|
||||
|
||||
@@ -80,19 +80,19 @@ where
|
||||
checkpointDefEq do
|
||||
let args := b.getAppArgs
|
||||
let params := args[:ctorVal.numParams].toArray
|
||||
for i in [ctorVal.numParams : args.size] do
|
||||
for h : i in [ctorVal.numParams : args.size] do
|
||||
let j := i - ctorVal.numParams
|
||||
let proj ← mkProjFn ctorVal us params j a
|
||||
if ← isProof proj then
|
||||
unless ← isAbstractedUnassignedMVar args[i]! do
|
||||
unless ← isAbstractedUnassignedMVar args[i] do
|
||||
-- Skip expensive unification problem that is likely solved
|
||||
-- using proof irrelevance. We already know that `proj` and
|
||||
-- `args[i]!` have the same type, so they're defeq in any case.
|
||||
-- `args[i]` have the same type, so they're defeq in any case.
|
||||
-- See comment at `isAbstractedUnassignedMVar`.
|
||||
continue
|
||||
trace[Meta.isDefEq.eta.struct] "{a} =?= {b} @ [{j}], {proj} =?= {args[i]!}"
|
||||
unless (← isDefEq proj args[i]!) do
|
||||
trace[Meta.isDefEq.eta.struct] "failed, unexpected arg #{i}, projection{indentExpr proj}\nis not defeq to{indentExpr args[i]!}"
|
||||
trace[Meta.isDefEq.eta.struct] "{a} =?= {b} @ [{j}], {proj} =?= {args[i]}"
|
||||
unless (← isDefEq proj args[i]) do
|
||||
trace[Meta.isDefEq.eta.struct] "failed, unexpected arg #{i}, projection{indentExpr proj}\nis not defeq to{indentExpr args[i]}"
|
||||
return false
|
||||
return true
|
||||
else
|
||||
|
||||
@@ -59,8 +59,8 @@ private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo :=
|
||||
forallBoundedTelescope fnType maxArgs? fun fvars type => do
|
||||
let mut paramInfo := #[]
|
||||
let mut higherOrderOutParams : FVarIdSet := {}
|
||||
for i in [:fvars.size] do
|
||||
let fvar := fvars[i]!
|
||||
for h : i in [:fvars.size] do
|
||||
let fvar := fvars[i]
|
||||
let decl ← getFVarLocalDecl fvar
|
||||
let backDeps := collectDeps fvars decl.type
|
||||
let dependsOnHigherOrderOutParam :=
|
||||
@@ -79,9 +79,9 @@ private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo :=
|
||||
if let some outParamPositions := getOutParamPositions? (← getEnv) className then
|
||||
unless outParamPositions.isEmpty do
|
||||
let args := decl.type.getAppArgs
|
||||
for i in [:args.size] do
|
||||
for h2 : i in [:args.size] do
|
||||
if outParamPositions.contains i then
|
||||
let arg := args[i]!
|
||||
let arg := args[i]
|
||||
if let some idx := fvars.indexOf? arg then
|
||||
if (← whnf (← inferType arg)).isForall then
|
||||
paramInfo := paramInfo.modify idx fun info => { info with higherOrderOutParam := true }
|
||||
|
||||
@@ -119,8 +119,8 @@ where
|
||||
modifyBinders { vars with target := vars.target ++ xs, motives := xs } 0
|
||||
|
||||
modifyBinders (vars : Variables) (i : Nat) := do
|
||||
if i < vars.args.size then
|
||||
let binder := vars.args[i]!
|
||||
if h : i < vars.args.size then
|
||||
let binder := vars.args[i]
|
||||
let binderType ← inferType binder
|
||||
if (← checkCount binderType) then
|
||||
mkBelowBinder vars binder binderType fun indValIdx x =>
|
||||
@@ -372,8 +372,8 @@ where
|
||||
(rest : Expr)
|
||||
(belowIndices : Array Nat)
|
||||
(xIdx yIdx : Nat) : MetaM $ Array Nat := do
|
||||
if xIdx ≥ xs.size then return belowIndices else
|
||||
let x := xs[xIdx]!
|
||||
if h : xIdx ≥ xs.size then return belowIndices else
|
||||
let x := xs[xIdx]
|
||||
let xTy ← inferType x
|
||||
let yTy := rest.bindingDomain!
|
||||
if (← isDefEq xTy yTy) then
|
||||
|
||||
@@ -95,10 +95,10 @@ private def inferConstType (c : Name) (us : List Level) : MetaM Expr := do
|
||||
throwIncorrectNumberOfLevels c us
|
||||
|
||||
private def inferProjType (structName : Name) (idx : Nat) (e : Expr) : MetaM Expr := do
|
||||
let failed {α} : Unit → MetaM α := fun _ =>
|
||||
throwError "invalid projection{indentExpr (mkProj structName idx e)}"
|
||||
let structType ← inferType e
|
||||
let structType ← whnf structType
|
||||
let failed {α} : Unit → MetaM α := fun _ =>
|
||||
throwError "invalid projection{indentExpr (mkProj structName idx e)} from type {structType}"
|
||||
matchConstStruct structType.getAppFn failed fun structVal structLvls ctorVal =>
|
||||
let n := structVal.numParams
|
||||
let structParams := structType.getAppArgs
|
||||
|
||||
@@ -115,8 +115,8 @@ It returns a dummy motive `(xs : ) → PUnit` or `(xs : … ) → True` if no ex
|
||||
|
||||
-/
|
||||
def packLambdas (type : Expr) (es : Array Expr) : MetaM Expr := do
|
||||
if es.size = 1 then
|
||||
return es[0]!
|
||||
if h : es.size = 1 then
|
||||
return es[0]
|
||||
forallTelescope type fun xs sort => do
|
||||
assert! sort.isSort
|
||||
-- NB: Use beta, not instantiateLambda; when constructing the belowDict below
|
||||
@@ -131,8 +131,8 @@ The value analogue to `PProdN.packLambdas`.
|
||||
It is the identity if `es.size = 1`.
|
||||
-/
|
||||
def mkLambdas (type : Expr) (es : Array Expr) : MetaM Expr := do
|
||||
if es.size = 1 then
|
||||
return es[0]!
|
||||
if h : es.size = 1 then
|
||||
return es[0]
|
||||
forallTelescope type fun xs body => do
|
||||
let lvl ← getLevel body
|
||||
let es' := es.map (·.beta xs)
|
||||
|
||||
@@ -182,13 +182,13 @@ private def getUnivLevelPos (declName : Name) (lparams : List Name) (motiveLvl :
|
||||
private def getProduceMotiveAndRecursive (xs : Array Expr) (numParams numIndices majorPos : Nat) (motive : Expr) : MetaM (List Bool × Bool) := do
|
||||
let mut produceMotive := #[]
|
||||
let mut recursor := false
|
||||
for i in [:xs.size] do
|
||||
for h : i in [:xs.size] do
|
||||
if i < numParams + 1 then
|
||||
continue --skip parameters and motive
|
||||
if majorPos - numIndices ≤ i && i ≤ majorPos then
|
||||
continue -- skip indices and major premise
|
||||
-- process minor premise
|
||||
let x := xs[i]!
|
||||
let x := xs[i]
|
||||
let xType ← inferType x
|
||||
(produceMotive, recursor) ← forallTelescopeReducing xType fun minorArgs minorResultType => minorResultType.withApp fun res _ => do
|
||||
let produceMotive := produceMotive.push (res == motive)
|
||||
|
||||
@@ -26,8 +26,8 @@ partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : Meta
|
||||
let finfo ← getFunInfoNArgs f nargs
|
||||
let mut args := e.getAppArgs
|
||||
for i in [:args.size] do
|
||||
if i < finfo.paramInfo.size then
|
||||
let info := finfo.paramInfo[i]!
|
||||
if h : i < finfo.paramInfo.size then
|
||||
let info := finfo.paramInfo[i]
|
||||
if !explicitOnly || info.isExplicit then
|
||||
args ← args.modifyM i visit
|
||||
else
|
||||
|
||||
@@ -16,8 +16,8 @@ private partial def mkLocalInstances (params : Array Expr) (k : Array Expr → M
|
||||
loop 0 #[]
|
||||
where
|
||||
loop (i : Nat) (insts : Array Expr) : MetaM α := do
|
||||
if i < params.size then
|
||||
let param := params[i]!
|
||||
if h : i < params.size then
|
||||
let param := params[i]
|
||||
let paramType ← inferType param
|
||||
let instType? ← forallTelescopeReducing paramType fun xs _ => do
|
||||
let type := mkAppN param xs
|
||||
@@ -67,8 +67,8 @@ private partial def mkSizeOfMotives (motiveFVars : Array Expr) (k : Array Expr
|
||||
loop 0 #[]
|
||||
where
|
||||
loop (i : Nat) (motives : Array Expr) : MetaM α := do
|
||||
if i < motiveFVars.size then
|
||||
let type ← inferType motiveFVars[i]!
|
||||
if h : i < motiveFVars.size then
|
||||
let type ← inferType motiveFVars[i]
|
||||
let motive ← forallTelescopeReducing type fun xs _ => do
|
||||
mkLambdaFVars xs <| mkConst ``Nat
|
||||
trace[Meta.sizeOf] "motive: {motive}"
|
||||
|
||||
@@ -140,7 +140,7 @@ where
|
||||
| .op l r => mkApp2 preContext.op (convertTarget vars l) (convertTarget vars r)
|
||||
| .var x => vars[x]!
|
||||
|
||||
def rewriteUnnormalized (mvarId : MVarId) : MetaM Unit := do
|
||||
def rewriteUnnormalized (mvarId : MVarId) : MetaM MVarId := do
|
||||
let simpCtx :=
|
||||
{
|
||||
simpTheorems := {}
|
||||
@@ -149,8 +149,7 @@ def rewriteUnnormalized (mvarId : MVarId) : MetaM Unit := do
|
||||
}
|
||||
let tgt ← instantiateMVars (← mvarId.getType)
|
||||
let (res, _) ← Simp.main tgt simpCtx (methods := { post })
|
||||
let newGoal ← applySimpResultToTarget mvarId tgt res
|
||||
newGoal.refl
|
||||
applySimpResultToTarget mvarId tgt res
|
||||
where
|
||||
post (e : Expr) : SimpM Simp.Step := do
|
||||
let ctx ← Simp.getContext
|
||||
@@ -171,9 +170,21 @@ where
|
||||
| none => return Simp.Step.done { expr := e }
|
||||
| e, _ => return Simp.Step.done { expr := e }
|
||||
|
||||
def rewriteUnnormalizedRefl (goal : MVarId) : MetaM Unit := do
|
||||
let newGoal ← rewriteUnnormalized goal
|
||||
newGoal.refl
|
||||
|
||||
def rewriteUnnormalizedNormalForm (goal : MVarId) : TacticM Unit := do
|
||||
let newGoal ← rewriteUnnormalized goal
|
||||
replaceMainGoal [newGoal]
|
||||
|
||||
@[builtin_tactic acRfl] def acRflTactic : Lean.Elab.Tactic.Tactic := fun _ => do
|
||||
let goal ← getMainGoal
|
||||
goal.withContext <| rewriteUnnormalized goal
|
||||
goal.withContext <| rewriteUnnormalizedRefl goal
|
||||
|
||||
@[builtin_tactic acNf] def acNfTactic : Lean.Elab.Tactic.Tactic := fun _ => do
|
||||
let goal ← getMainGoal
|
||||
goal.withContext <| rewriteUnnormalizedNormalForm goal
|
||||
|
||||
builtin_initialize
|
||||
registerTraceClass `Meta.AC
|
||||
|
||||
@@ -68,8 +68,8 @@ def getElimExprInfo (elimExpr : Expr) (baseDeclName? : Option Name := none) : Me
|
||||
| some targetPos => pure targetPos.val
|
||||
let mut altsInfo := #[]
|
||||
let env ← getEnv
|
||||
for i in [:xs.size] do
|
||||
let x := xs[i]!
|
||||
for h : i in [:xs.size] do
|
||||
let x := xs[i]
|
||||
if x != motive && !targets.contains x then
|
||||
let xDecl ← x.fvarId!.getDecl
|
||||
if xDecl.binderInfo.isExplicit then
|
||||
|
||||
@@ -27,7 +27,7 @@ builtin_dsimproc [simp, seval] reduceGetElem? (@GetElem?.getElem? (Array _) Nat
|
||||
|
||||
/-- Simplification procedure for `#[...][n]!` for `n` a `Nat` literal. -/
|
||||
builtin_dsimproc [simp, seval] reduceGetElem! (@GetElem?.getElem! (Array _) Nat _ _ _ _ _ _) := fun e => do
|
||||
let_expr GetElem?.getElem! _ _ α _ _ I xs n ← e | return .continue
|
||||
let_expr GetElem?.getElem! _ _ α _ _ _ xs n ← e | return .continue
|
||||
let some n ← Nat.fromExpr? n | return .continue
|
||||
let some xs ← getArrayLit? xs | return .continue
|
||||
let r ← if h : n < xs.size then pure xs[n] else mkDefault α
|
||||
|
||||
@@ -320,8 +320,8 @@ def simpMatchDiscrs? (info : MatcherInfo) (e : Expr) : SimpM (Option Result) :=
|
||||
r ← mkCongrFun r argNew
|
||||
unless modified do
|
||||
return none
|
||||
for i in [info.numDiscrs : args.size] do
|
||||
let arg := args[i]!
|
||||
for h : i in [info.numDiscrs : args.size] do
|
||||
let arg := args[i]
|
||||
r ← mkCongrFun r arg
|
||||
return some r
|
||||
|
||||
|
||||
@@ -207,8 +207,8 @@ def unexpandStructureInstance (stx : Syntax) : Delab := whenPPOption getPPStruct
|
||||
`(⟨$[$(stx[1].getArgs)],*⟩)
|
||||
let args := e.getAppArgs
|
||||
let fieldVals := args.extract s.numParams args.size
|
||||
for idx in [:fieldNames.size] do
|
||||
let fieldName := fieldNames[idx]!
|
||||
for h : idx in [:fieldNames.size] do
|
||||
let fieldName := fieldNames[idx]
|
||||
if (← getPPOption getPPStructureInstancesFlatten) && (Lean.isSubobjectField? env s.induct fieldName).isSome then
|
||||
match stx[1][idx] with
|
||||
| `({ $fields',* $[: $_]?}) =>
|
||||
@@ -397,9 +397,9 @@ def delabAppImplicitCore (unexpand : Bool) (numArgs : Nat) (delabHead : Delab) (
|
||||
|
||||
-- Field notation
|
||||
if let some (fieldIdx, field) := field? then
|
||||
if fieldIdx < args.size then
|
||||
if h : fieldIdx < args.size then
|
||||
let obj? : Option Term ← do
|
||||
let arg := args[fieldIdx]!
|
||||
let arg := args[fieldIdx]
|
||||
if let .regular s := arg then
|
||||
withNaryArg fieldIdx <| some <$> stripParentProjections s
|
||||
else
|
||||
@@ -491,8 +491,8 @@ def useAppExplicit (numArgs : Nat) (paramKinds : Array ParamKind) : DelabM Bool
|
||||
-- If there was an error collecting ParamKinds, fall back to explicit mode.
|
||||
if paramKinds.size < numArgs then return true
|
||||
|
||||
if numArgs < paramKinds.size then
|
||||
let nextParam := paramKinds[numArgs]!
|
||||
if h : numArgs < paramKinds.size then
|
||||
let nextParam := paramKinds[numArgs]
|
||||
|
||||
-- If the next parameter is implicit or inst implicit, fall back to explicit mode.
|
||||
-- This is necessary for `@Eq` for example.
|
||||
@@ -741,8 +741,8 @@ where
|
||||
m acc
|
||||
|
||||
usingNames {α} (varNames : Array Name) (x : DelabM α) (i : Nat := 0) : DelabM α :=
|
||||
if i < varNames.size then
|
||||
withBindingBody varNames[i]! <| usingNames varNames x (i+1)
|
||||
if h : i < varNames.size then
|
||||
withBindingBody varNames[i] <| usingNames varNames x (i+1)
|
||||
else
|
||||
x
|
||||
|
||||
|
||||
@@ -28,7 +28,7 @@ partial def runLakeSetupFile
|
||||
: IO LakeSetupFileOutput := do
|
||||
let mut args := #["setup-file", filePath.toString] ++ imports.map (toString ·.module)
|
||||
if m.dependencyBuildMode matches .never then
|
||||
args := args.push "--no-build"
|
||||
args := args.push "--no-build" |>.push "--no-cache"
|
||||
let spawnArgs : Process.SpawnArgs := {
|
||||
stdin := Process.Stdio.null
|
||||
stdout := Process.Stdio.piped
|
||||
|
||||
@@ -312,8 +312,8 @@ where
|
||||
|
||||
findCanonicalRepresentative (idMap : Std.HashMap RefIdent RefIdent) (id : RefIdent) : RefIdent := Id.run do
|
||||
let mut canonicalRepresentative := id
|
||||
while idMap.contains canonicalRepresentative do
|
||||
canonicalRepresentative := idMap[canonicalRepresentative]!
|
||||
while h : idMap.contains canonicalRepresentative do
|
||||
canonicalRepresentative := idMap[canonicalRepresentative]
|
||||
return canonicalRepresentative
|
||||
|
||||
buildIdMap posMap := Id.run <| StateT.run' (s := Std.HashMap.empty) do
|
||||
|
||||
@@ -41,10 +41,7 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr
|
||||
decInits := decInits.push (← `(structInstField| $fid:ident := ← rpcDecode a.$fid))
|
||||
|
||||
let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName
|
||||
let indName := mkIdent indVal.name
|
||||
`(-- Workaround for https://github.com/leanprover/lean4/issues/2044
|
||||
namespace $indName
|
||||
structure RpcEncodablePacket where
|
||||
`(structure RpcEncodablePacket where
|
||||
$[($fieldIds : $fieldTys)]*
|
||||
deriving FromJson, ToJson
|
||||
|
||||
@@ -57,7 +54,6 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr
|
||||
dec j := do
|
||||
let a : RpcEncodablePacket ← fromJson? j
|
||||
return { $decInits:structInstField,* }
|
||||
end $indName
|
||||
)
|
||||
|
||||
private def matchAltTerm := Lean.Parser.Term.matchAlt (rhsParser := Lean.Parser.termParser)
|
||||
@@ -95,10 +91,7 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
|
||||
let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName
|
||||
let typeId ← `(@$(mkIdent indVal.name) $paramIds*)
|
||||
|
||||
let indName := mkIdent indVal.name
|
||||
`(-- Workaround for https://github.com/leanprover/lean4/issues/2044
|
||||
namespace $indName
|
||||
inductive RpcEncodablePacket where
|
||||
`(inductive RpcEncodablePacket where
|
||||
$[$ctors:ctor]*
|
||||
deriving FromJson, ToJson
|
||||
|
||||
@@ -113,7 +106,6 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
|
||||
have inst : RpcEncodable $typeId := { rpcEncode := enc, rpcDecode := dec }
|
||||
let pkt : RpcEncodablePacket ← fromJson? j
|
||||
id <| match pkt with $[$decodes:matchAlt]*
|
||||
end $indName
|
||||
)
|
||||
|
||||
/-- Creates an `RpcEncodablePacket` for `typeName`. For structures, the packet is a structure
|
||||
|
||||
@@ -186,7 +186,7 @@ theorem toListModel_updateAllBuckets {m : Raw₀ α β} {f : AssocList α β →
|
||||
have := (hg (l := []) (l' := [])).length_eq
|
||||
rw [List.length_append, List.append_nil] at this
|
||||
omega
|
||||
rw [updateAllBuckets, toListModel, Array.map_toList, List.bind_eq_foldl, List.foldl_map,
|
||||
rw [updateAllBuckets, toListModel, Array.toList_map, List.bind_eq_foldl, List.foldl_map,
|
||||
toListModel, List.bind_eq_foldl]
|
||||
suffices ∀ (l : List (AssocList α β)) (l' : List ((a: α) × δ a)) (l'' : List ((a : α) × β a)),
|
||||
Perm (g l'') l' →
|
||||
|
||||
@@ -598,9 +598,9 @@ where
|
||||
else
|
||||
let decl := aig.decls[upper]
|
||||
match heq : decl with
|
||||
| .const b => state.addConst upper h heq
|
||||
| .atom a => state.addAtom upper h heq
|
||||
| .gate lhs rhs linv rinv =>
|
||||
| .const _ => state.addConst upper h heq
|
||||
| .atom _ => state.addAtom upper h heq
|
||||
| .gate lhs rhs _ _ =>
|
||||
have := aig.invariant h heq
|
||||
let ⟨lstate, hlstate⟩ := go aig lhs (by omega) state
|
||||
let ⟨rstate, hrstate⟩ := go aig rhs (by omega) lstate
|
||||
|
||||
@@ -104,10 +104,10 @@ def append (lhs : RefVec aig lw) (rhs : RefVec aig rw) : RefVec aig (lw + rw) :=
|
||||
by
|
||||
intro i h
|
||||
by_cases hsplit : i < lrefs.size
|
||||
· rw [Array.get_append_left]
|
||||
· rw [Array.getElem_append_left]
|
||||
apply hl2
|
||||
omega
|
||||
· rw [Array.get_append_right]
|
||||
· rw [Array.getElem_append_right]
|
||||
· apply hr2
|
||||
omega
|
||||
· omega
|
||||
@@ -124,9 +124,9 @@ theorem get_append (lhs : RefVec aig lw) (rhs : RefVec aig rw) (idx : Nat)
|
||||
simp only [get, append]
|
||||
split
|
||||
· simp [Ref.mk.injEq]
|
||||
rw [Array.get_append_left]
|
||||
rw [Array.getElem_append_left]
|
||||
· simp only [Ref.mk.injEq]
|
||||
rw [Array.get_append_right]
|
||||
rw [Array.getElem_append_right]
|
||||
· simp [lhs.hlen]
|
||||
· rw [lhs.hlen]
|
||||
omega
|
||||
|
||||
@@ -85,7 +85,7 @@ where
|
||||
@[specialize]
|
||||
go (aig : AIG α) (idx : Nat) (s : RefVec aig idx) (hidx : idx ≤ len)
|
||||
(lhs rhs : RefVec aig len) (f : (aig : AIG α) → BinaryInput aig → Entrypoint α)
|
||||
[LawfulOperator α BinaryInput f] [chainable : LawfulZipOperator α f] :
|
||||
[LawfulOperator α BinaryInput f] [LawfulZipOperator α f] :
|
||||
RefVecEntry α len :=
|
||||
if hidx : idx < len then
|
||||
let res := f aig ⟨lhs.get idx hidx, rhs.get idx hidx⟩
|
||||
|
||||
@@ -29,9 +29,9 @@ structure OverflowInput (aig : AIG α) where
|
||||
|
||||
def mkOverflowBit (aig : AIG α) (input : OverflowInput aig) : AIG.Entrypoint α :=
|
||||
let ⟨_, ⟨lhs, rhs⟩, cin⟩ := input
|
||||
go aig lhs rhs 0 (by omega) cin
|
||||
go aig lhs rhs 0 cin
|
||||
where
|
||||
go {w : Nat} (aig : AIG α) (lhs rhs : AIG.RefVec aig w) (curr : Nat) (hcurr : curr ≤ w)
|
||||
go {w : Nat} (aig : AIG α) (lhs rhs : AIG.RefVec aig w) (curr : Nat)
|
||||
(cin : AIG.Ref aig) :
|
||||
AIG.Entrypoint α :=
|
||||
if hidx : curr < w then
|
||||
@@ -43,7 +43,7 @@ where
|
||||
let carryRef := res.ref
|
||||
let lhs := lhs.cast this
|
||||
let rhs := rhs.cast this
|
||||
go aig lhs rhs (curr + 1) (by omega) carryRef
|
||||
go aig lhs rhs (curr + 1) carryRef
|
||||
else
|
||||
⟨aig, cin⟩
|
||||
termination_by w - curr
|
||||
@@ -51,7 +51,7 @@ where
|
||||
namespace mkOverflowBit
|
||||
|
||||
theorem go_le_size {aig : AIG α} {cin} {lhs rhs : AIG.RefVec aig w} :
|
||||
aig.decls.size ≤ (go aig lhs rhs curr hcurr cin).aig.decls.size := by
|
||||
aig.decls.size ≤ (go aig lhs rhs curr cin).aig.decls.size := by
|
||||
unfold go
|
||||
dsimp only
|
||||
split
|
||||
@@ -63,8 +63,8 @@ termination_by w - curr
|
||||
|
||||
theorem go_decl_eq {aig : AIG α} {cin} {lhs rhs : AIG.RefVec aig w} :
|
||||
∀ (idx : Nat) (h1) (h2),
|
||||
(go aig lhs rhs curr hcurr cin).aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
|
||||
generalize hgo : go aig lhs rhs curr hcurr cin = res
|
||||
(go aig lhs rhs curr cin).aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
|
||||
generalize hgo : go aig lhs rhs curr cin = res
|
||||
unfold go at hgo
|
||||
dsimp only at hgo
|
||||
split at hgo
|
||||
|
||||
Some files were not shown because too many files have changed in this diff Show More
Reference in New Issue
Block a user