Compare commits

..

24 Commits

Author SHA1 Message Date
Kim Morrison
2e9f62cc98 feat: List.replicate lemmas 2024-09-16 09:37:47 +10:00
Joachim Breitner
4c439c73a7 test: tracing and test case for #5347 (#5348)
not a fix, unfortunately, just recording the test.
2024-09-15 15:45:39 +00:00
thorimur
5eea8355ba fix: set check level correctly during workflow (#5344)
Fixes a workflow bug where the `check-level` was not always set
correctly. Arguments to a `gh` call used to determine the `check_level`
were accidentally outside of the relevant command substitution (`$(gh
...)`).

-----

This can be observed in [these
logs](https://github.com/leanprover/lean4/actions/runs/10859763037/job/30139540920),
where the check level (shown first under "configure build matrix") is
`2`, but the PR does not have the `release-ci` tag. As a "test", run the
script for "set check level" printed in those logs (with some lines
omitted):
```
check_level=0

labels="$(gh api repos/leanprover/lean4/pulls/5343) --jq '.labels'"
if echo "$labels" | grep -q "release-ci"; then
  check_level=2
elif echo "$labels" | grep -q "merge-ci"; then
  check_level=1
fi

echo "check_level=$check_level"
```
Note that this prints `check_level=2`, but changing `labels` to
`labels="$(gh api repos/leanprover/lean4/pulls/5343 --jq '.labels')"`
prints `check_level=0`.
2024-09-14 08:14:08 +00:00
thorimur
60bb451d45 feat: allow addition of release-ci label via comment (#5343)
Updates the PR labeling workflow to allow an external contributor to add
the `release-ci` label to their own PR via comment. This is allows users
on Windows and Intel-based macs to generate toolchains for local
testing. The pull request template is also updated to reflect this.

-----

See Zulip discussion
[here](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/No.20binary.20for.20lean.20PR.20testing.20locally).
2024-09-14 08:13:48 +00:00
Marc Huisinga
f989520d2b fix: invalid namespace completions (#5322)
This PR fixes an issue reported a while ago at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60Monad.2Emap.60.20is.20a.20namespace.3F/near/425662846
where `Monad.map` was incorrectly reported by the autocompletion as a
namespace.

The underlying issue is that `Monad.map` contains an internal
declaration `_default`. This PR ensures that no namespaces are
registered that only contain internal declarations.

This also means that `open`ing namespaces that only contain internal
declarations will now fail.

The Mathlib adaption for this is a minor change where a declaration
(i.e. a namespace that only contains internal declarations) was `open`ed
by accident.
2024-09-13 12:23:03 +00:00
Jeremy Tan Jie Rui
626dda9358 refactor: tag Iff.refl with @[refl] (#5329)
and remove `exact Off.rfl` from the `rfl` macro.


This upstreams a property found in
[`Mathlib.Init.Logic`](4e40837aec/Mathlib/Init/Logic.lean (L63)).
2024-09-13 11:55:36 +00:00
Sebastian Ullrich
5f789e63fa chore: remove confusing test 2024-09-13 13:04:57 +02:00
Sebastian Ullrich
438061a924 fix: inaccessible pattern vars reported as binders (#5337)
Fixes an unused variable false positive on some wildcard patterns

Fixes #1633, fixes #2830
2024-09-13 09:53:58 +00:00
Mario Carneiro
ec98c92ba6 feat: @[builtin_doc] attribute (part 2) (#3918)
This solves the issue where certain subexpressions are lacking syntax
hovers because the hover text is not "builtin" - it only shows up if the
`Parser` constant is imported in the environment. For top level syntaxes
this is not a problem because `builtin_term_parser` will automatically
add this doc information, but nested syntaxes don't get the same
treatment.

We could walk the expression and add builtin docs recursively, but this
is somewhat expensive and unnecessary given that it's a fixed list of
declarations in lean core. Moreover, there are reasons to want to
control which syntax nodes actually get hovers, and while a better
system for that is forthcoming, for now it can be achieved by
strategically not applying the `@[builtin_doc]` attribute.

Fixes #3842
2024-09-13 08:05:10 +00:00
Henrik Böving
2080fc0221 feat: (DHashMap|HashMap|HashSet).(getKey?|getKey|getKey!|getKeyD) (#5244) 2024-09-13 05:40:10 +00:00
Marc Huisinga
b34379554d feat: completion fallback (#5299)
When the elaborator doesn't provide us with any `CompletionInfo`, we
currently provide no completions whatsoever. But in many cases, we can
still provide some helpful identifier completions without elaborator
information. This PR adds a fallback mode for this situation.

There is more potential here, but this should be a good start.

In principle, this issue alleviates #5172 (since we now provide
completions in these contexts). I'll leave it up to an elaboration
maintainer whether we also want to ensure that the completion infos are
provided correctly in these cases.
2024-09-12 16:09:20 +00:00
Siddharth
273b7540b2 feat: toNat_sub_of_le (#5314)
This adds a simplification lemma for `(x - y).toNat` when the
subtraction is known to not overflow (i.e., `y ≤ x`).

We make a new section for this for two reasons:
1. Definitions of subtraction occur before the definition of
`BitVec.le_def`, so we cannot directly place this lemma at `sub`.
2. There are other theorems of this kind, for addition and
multiplication, which can morally live in the same section.
2024-09-12 13:19:39 +00:00
Lars - he/him
b875627198 feat: add ediv_nonneg_of_nonpos_of_nonpos to DivModLemmas (#5320)
The theorem 

```lean
namespace Int

theorem ediv_nonneg_of_nonpos_of_nonpos {a b : Int} (Ha : a ≤ 0) (Hb : b ≤ 0) : 0 ≤ a / b := by
  match a, b with
  | ofNat a, b =>
    match Int.le_antisymm Ha (ofNat_zero_le a) with
    | h1 =>
    rw [h1, zero_ediv,]
    exact Int.le_refl 0
  | a, ofNat b =>
    match Int.le_antisymm Hb (ofNat_zero_le  b) with
    | h1 =>
    rw [h1, Int.ediv_zero]
    exact Int.le_refl 0
  | negSucc a, negSucc b =>
    rw [Int.div_def, ediv]
    have le_succ {a: Int} : a ≤ a+1 := (le_add_one (Int.le_refl a))
    have h2: 0 ≤ ((↑b:Int) + 1) := Int.le_trans (ofNat_zero_le b) le_succ
    have h3: (0:Int) ≤ ↑a / (↑b + 1) := (ediv_nonneg (ofNat_zero_le a) h2)
    exact Int.le_trans h3 le_succ
```
is nontrivial to prove from existing theorems and would be nice to add
as standard theorem in DivModLemmas.

See the zullip conversation
[here](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Adding.20theorem.20theorem.20ediv_nonneg'.20for.20negative.20a.20and.20b)

---------

Co-authored-by: Kim Morrison <kim@tqft.net>
2024-09-12 11:26:20 +00:00
Kim Morrison
adfd6c090e chore: add Nat.self_sub_mod lemma (#5306) 2024-09-12 03:36:50 +00:00
Kim Morrison
da0d309d65 feat: provide mergeSort comparator autoParam (#5302)
Write `mergeSort xs ys cmp` to provide an explicit comparator, or
otherwise `mergeSort xs ys` falls back to `LE` and `DecidablePred` via
an autoparam.
2024-09-12 01:50:01 +00:00
Kim Morrison
87fdd7809f feat: List.tail lemma (#5316) 2024-09-12 01:09:57 +00:00
Henrik Böving
8fd6e46a9c feat: more basic BitVec ordering theory for UInt (#5313) 2024-09-11 18:16:21 +00:00
Sebastian Ullrich
0602b805c8 fix: changing whitespace after module header may break subsequent commands (#5312)
`with` considered harmful when merging old and new state, let's always
be explicit in these cases
2024-09-11 13:00:42 +00:00
Kim Morrison
0b7debe376 chore: fix List.countP lemmas (#5311) 2024-09-11 10:09:37 +00:00
Kim Morrison
f5146c6edb chore: fix List.all/any lemmas (#5310) 2024-09-11 10:02:47 +00:00
Kim Morrison
461283ecf4 chore: restoring Option simp confluence (#5307) 2024-09-11 06:52:31 +00:00
Kim Morrison
27bf7367ca chore: rename Nat bitwise lemmas (#5305) 2024-09-11 06:29:00 +00:00
Kim Morrison
d4cc934149 chore: rename Int.div/mod to tdiv/tmod (#5301)
From the new doc-string:
```quote
In early versions of Lean, the typeclasses provided by `/` and `%`
were defined in terms of `tdiv` and `tmod`, and these were named simply as `div` and `mod`.

However we decided it was better to use `ediv` and `emod`,
as they are consistent with the conventions used in SMTLib, Mathlib,
and often mathematical reasoning is easier with these conventions.

At that time, we did not rename `div` and `mod` to `tdiv` and `tmod` (along with all their lemma).
In September 2024, we decided to do this rename (with deprecations in place),
and later we intend to rename `ediv` and `emod` to `div` and `mod`, as nearly all users will only
ever need to use these functions and their associated lemmas.
```
2024-09-11 06:15:44 +00:00
Kim Morrison
b88cdf6a3e chore: Array.not_mem_empty (#5304) 2024-09-11 06:13:24 +00:00
65 changed files with 2728 additions and 375 deletions

View File

@@ -5,6 +5,7 @@
* Include the link to your `RFC` or `bug` issue in the description.
* If the issue does not already have approval from a developer, submit the PR as draft.
* The PR title/description will become the commit message. Keep it up-to-date as the PR evolves.
* A toolchain of the form `leanprover/lean4-pr-releases:pr-release-NNNN` for Linux and M-series Macs will be generated upon build. To generate binaries for Windows and Intel-based Macs as well, write a comment containing `release-ci` on its own line.
* If you rebase your PR onto `nightly-with-mathlib` then CI will test Mathlib against your PR.
* You can manage the `awaiting-review`, `awaiting-author`, and `WIP` labels yourself, by writing a comment containing one of these labels on its own line.
* Remove this section, up to and including the `---` before submitting.

View File

@@ -114,7 +114,7 @@ jobs:
elif [[ "${{ github.event_name }}" != "pull_request" ]]; then
check_level=1
else
labels="$(gh api repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/${{ github.event.pull_request.number }}) --jq '.labels'"
labels="$(gh api repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/${{ github.event.pull_request.number }} --jq '.labels')"
if echo "$labels" | grep -q "release-ci"; then
check_level=2
elif echo "$labels" | grep -q "merge-ci"; then

View File

@@ -1,6 +1,7 @@
# This workflow allows any user to add one of the `awaiting-review`, `awaiting-author`, or `WIP` labels,
# by commenting on the PR or issue.
# Other labels from this set are removed automatically at the same time.
# This workflow allows any user to add one of the `awaiting-review`, `awaiting-author`, `WIP`,
# or `release-ci` labels by commenting on the PR or issue.
# If any labels from the set {`awaiting-review`, `awaiting-author`, `WIP`} are added, other labels
# from that set are removed automatically at the same time.
name: Label PR based on Comment
@@ -10,7 +11,7 @@ on:
jobs:
update-label:
if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP'))
if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP') || contains(github.event.comment.body, 'release-ci'))
runs-on: ubuntu-latest
steps:
@@ -25,6 +26,7 @@ jobs:
const awaitingReview = commentLines.includes('awaiting-review');
const awaitingAuthor = commentLines.includes('awaiting-author');
const wip = commentLines.includes('WIP');
const releaseCI = commentLines.includes('release-ci');
if (awaitingReview || awaitingAuthor || wip) {
await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'awaiting-review' }).catch(() => {});
@@ -41,3 +43,7 @@ jobs:
if (wip) {
await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['WIP'] });
}
if (releaseCI) {
await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['release-ci'] });
}

View File

@@ -817,14 +817,12 @@ variable {a b c d : Prop}
theorem iff_iff_implies_and_implies {a b : Prop} : (a b) (a b) (b a) :=
Iff.intro (fun h => And.intro h.mp h.mpr) (fun h => Iff.intro h.left h.right)
theorem Iff.refl (a : Prop) : a a :=
@[refl] theorem Iff.refl (a : Prop) : a a :=
Iff.intro (fun h => h) (fun h => h)
protected theorem Iff.rfl {a : Prop} : a a :=
Iff.refl a
macro_rules | `(tactic| rfl) => `(tactic| exact Iff.rfl)
theorem Iff.of_eq (h : a = b) : a b := h Iff.rfl
theorem Iff.trans (h₁ : a b) (h₂ : b c) : a c :=

View File

@@ -1667,6 +1667,14 @@ protected theorem lt_of_le_ne {x y : BitVec n} : x ≤ y → ¬ x = y → x < y
simp only [lt_def, le_def, BitVec.toNat_eq]
apply Nat.lt_of_le_of_ne
protected theorem ne_of_lt {x y : BitVec n} : x < y x y := by
simp only [lt_def, ne_eq, toNat_eq]
apply Nat.ne_of_lt
protected theorem umod_lt (x : BitVec n) {y : BitVec n} : 0 < y x.umod y < y := by
simp only [ofNat_eq_ofNat, lt_def, toNat_ofNat, Nat.zero_mod, umod, toNat_ofNatLt]
apply Nat.mod_lt
/-! ### ofBoolList -/
@[simp] theorem getMsbD_ofBoolListBE : (ofBoolListBE bs).getMsbD i = bs.getD i false := by
@@ -2038,4 +2046,20 @@ theorem getLsbD_intMax (w : Nat) : (intMax w).getLsbD i = decide (i + 1 < w) :=
· simp [h]
· rw [Nat.sub_add_cancel (Nat.two_pow_pos (w - 1)), Nat.two_pow_pred_mod_two_pow (by omega)]
/-! ### Non-overflow theorems -/
/--
If `y ≤ x`, then the subtraction `(x - y)` does not overflow.
Thus, `(x - y).toNat = x.toNat - y.toNat`
-/
theorem toNat_sub_of_le {x y : BitVec n} (h : y x) :
(x - y).toNat = x.toNat - y.toNat := by
simp only [toNat_sub]
rw [BitVec.le_def] at h
by_cases h' : x.toNat = y.toNat
· rw [h', Nat.sub_self, Nat.sub_add_cancel (by omega), Nat.mod_self]
· have : 2 ^ n - y.toNat + x.toNat = 2 ^ n + (x.toNat - y.toNat) := by omega
rw [this, Nat.add_mod_left, Nat.mod_eq_of_lt (by omega)]
end BitVec

View File

@@ -16,83 +16,99 @@ There are three main conventions for integer division,
referred here as the E, F, T rounding conventions.
All three pairs satisfy the identity `x % y + (x / y) * y = x` unconditionally,
and satisfy `x / 0 = 0` and `x % 0 = x`.
### Historical notes
In early versions of Lean, the typeclasses provided by `/` and `%`
were defined in terms of `tdiv` and `tmod`, and these were named simply as `div` and `mod`.
However we decided it was better to use `ediv` and `emod`,
as they are consistent with the conventions used in SMTLib, and Mathlib,
and often mathematical reasoning is easier with these conventions.
At that time, we did not rename `div` and `mod` to `tdiv` and `tmod` (along with all their lemma).
In September 2024, we decided to do this rename (with deprecations in place),
and later we intend to rename `ediv` and `emod` to `div` and `mod`, as nearly all users will only
ever need to use these functions and their associated lemmas.
-/
/-! ### T-rounding division -/
/--
`div` uses the [*"T-rounding"*][t-rounding]
`tdiv` uses the [*"T-rounding"*][t-rounding]
(**T**runcation-rounding) convention, meaning that it rounds toward
zero. Also note that division by zero is defined to equal zero.
The relation between integer division and modulo is found in
`Int.mod_add_div` which states that
`a % b + b * (a / b) = a`, unconditionally.
`Int.tmod_add_tdiv` which states that
`tmod a b + b * (tdiv a b) = a`, unconditionally.
[t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862 [theo
mod_add_div]:
https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.mod_add_div#doc
[t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862
[theo tmod_add_tdiv]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.tmod_add_tdiv#doc
Examples:
```
#eval (7 : Int).div (0 : Int) -- 0
#eval (0 : Int).div (7 : Int) -- 0
#eval (7 : Int).tdiv (0 : Int) -- 0
#eval (0 : Int).tdiv (7 : Int) -- 0
#eval (12 : Int).div (6 : Int) -- 2
#eval (12 : Int).div (-6 : Int) -- -2
#eval (-12 : Int).div (6 : Int) -- -2
#eval (-12 : Int).div (-6 : Int) -- 2
#eval (12 : Int).tdiv (6 : Int) -- 2
#eval (12 : Int).tdiv (-6 : Int) -- -2
#eval (-12 : Int).tdiv (6 : Int) -- -2
#eval (-12 : Int).tdiv (-6 : Int) -- 2
#eval (12 : Int).div (7 : Int) -- 1
#eval (12 : Int).div (-7 : Int) -- -1
#eval (-12 : Int).div (7 : Int) -- -1
#eval (-12 : Int).div (-7 : Int) -- 1
#eval (12 : Int).tdiv (7 : Int) -- 1
#eval (12 : Int).tdiv (-7 : Int) -- -1
#eval (-12 : Int).tdiv (7 : Int) -- -1
#eval (-12 : Int).tdiv (-7 : Int) -- 1
```
Implemented by efficient native code.
-/
@[extern "lean_int_div"]
def div : (@& Int) (@& Int) Int
def tdiv : (@& Int) (@& Int) Int
| ofNat m, ofNat n => ofNat (m / n)
| ofNat m, -[n +1] => -ofNat (m / succ n)
| -[m +1], ofNat n => -ofNat (succ m / n)
| -[m +1], -[n +1] => ofNat (succ m / succ n)
@[deprecated tdiv (since := "2024-09-11")] abbrev div := tdiv
/-- Integer modulo. This function uses the
[*"T-rounding"*][t-rounding] (**T**runcation-rounding) convention
to pair with `Int.div`, meaning that `a % b + b * (a / b) = a`
unconditionally (see [`Int.mod_add_div`][theo mod_add_div]). In
to pair with `Int.tdiv`, meaning that `tmod a b + b * (tdiv a b) = a`
unconditionally (see [`Int.tmod_add_tdiv`][theo tmod_add_tdiv]). In
particular, `a % 0 = a`.
[t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862
[theo mod_add_div]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.mod_add_div#doc
[theo tmod_add_tdiv]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.tmod_add_tdiv#doc
Examples:
```
#eval (7 : Int).mod (0 : Int) -- 7
#eval (0 : Int).mod (7 : Int) -- 0
#eval (7 : Int).tmod (0 : Int) -- 7
#eval (0 : Int).tmod (7 : Int) -- 0
#eval (12 : Int).mod (6 : Int) -- 0
#eval (12 : Int).mod (-6 : Int) -- 0
#eval (-12 : Int).mod (6 : Int) -- 0
#eval (-12 : Int).mod (-6 : Int) -- 0
#eval (12 : Int).tmod (6 : Int) -- 0
#eval (12 : Int).tmod (-6 : Int) -- 0
#eval (-12 : Int).tmod (6 : Int) -- 0
#eval (-12 : Int).tmod (-6 : Int) -- 0
#eval (12 : Int).mod (7 : Int) -- 5
#eval (12 : Int).mod (-7 : Int) -- 5
#eval (-12 : Int).mod (7 : Int) -- -5
#eval (-12 : Int).mod (-7 : Int) -- -5
#eval (12 : Int).tmod (7 : Int) -- 5
#eval (12 : Int).tmod (-7 : Int) -- 5
#eval (-12 : Int).tmod (7 : Int) -- -5
#eval (-12 : Int).tmod (-7 : Int) -- -5
```
Implemented by efficient native code. -/
@[extern "lean_int_mod"]
def mod : (@& Int) (@& Int) Int
def tmod : (@& Int) (@& Int) Int
| ofNat m, ofNat n => ofNat (m % n)
| ofNat m, -[n +1] => ofNat (m % succ n)
| -[m +1], ofNat n => -ofNat (succ m % n)
| -[m +1], -[n +1] => -ofNat (succ m % succ n)
@[deprecated tmod (since := "2024-09-11")] abbrev mod := tmod
/-! ### F-rounding division
This pair satisfies `fdiv x y = floor (x / y)`.
-/
@@ -233,7 +249,9 @@ instance : Mod Int where
@[simp, norm_cast] theorem ofNat_ediv (m n : Nat) : ((m / n) : Int) = m / n := rfl
theorem ofNat_div (m n : Nat) : (m / n) = div m n := rfl
theorem ofNat_tdiv (m n : Nat) : (m / n) = tdiv m n := rfl
@[deprecated ofNat_tdiv (since := "2024-09-11")] abbrev ofNat_div := ofNat_tdiv
theorem ofNat_fdiv : m n : Nat, (m / n) = fdiv m n
| 0, _ => by simp [fdiv]

View File

@@ -137,12 +137,12 @@ theorem eq_one_of_mul_eq_one_left {a b : Int} (H : 0 ≤ b) (H' : a * b = 1) : b
| ofNat _ => show ofNat _ = _ by simp
| -[_+1] => rfl
@[simp] protected theorem zero_div : b : Int, div 0 b = 0
@[simp] protected theorem zero_tdiv : b : Int, tdiv 0 b = 0
| ofNat _ => show ofNat _ = _ by simp
| -[_+1] => show -ofNat _ = _ by simp
unseal Nat.div in
@[simp] protected theorem div_zero : a : Int, div a 0 = 0
@[simp] protected theorem tdiv_zero : a : Int, tdiv a 0 = 0
| ofNat _ => show ofNat _ = _ by simp
| -[_+1] => rfl
@@ -156,16 +156,17 @@ unseal Nat.div in
/-! ### div equivalences -/
theorem div_eq_ediv : {a b : Int}, 0 a 0 b a.div b = a / b
theorem tdiv_eq_ediv : {a b : Int}, 0 a 0 b a.tdiv b = a / b
| 0, _, _, _ | _, 0, _, _ => by simp
| succ _, succ _, _, _ => rfl
theorem fdiv_eq_ediv : (a : Int) {b : Int}, 0 b fdiv a b = a / b
| 0, _, _ | -[_+1], 0, _ => by simp
| succ _, ofNat _, _ | -[_+1], succ _, _ => rfl
theorem fdiv_eq_div {a b : Int} (Ha : 0 a) (Hb : 0 b) : fdiv a b = div a b :=
div_eq_ediv Ha Hb fdiv_eq_ediv _ Hb
theorem fdiv_eq_tdiv {a b : Int} (Ha : 0 a) (Hb : 0 b) : fdiv a b = tdiv a b :=
tdiv_eq_ediv Ha Hb fdiv_eq_ediv _ Hb
/-! ### mod zero -/
@@ -175,9 +176,9 @@ theorem fdiv_eq_div {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fdiv a b = div a
| ofNat _ => congrArg ofNat <| Nat.mod_zero _
| -[_+1] => congrArg negSucc <| Nat.mod_zero _
@[simp] theorem zero_mod (b : Int) : mod 0 b = 0 := by cases b <;> simp [mod]
@[simp] theorem zero_tmod (b : Int) : tmod 0 b = 0 := by cases b <;> simp [tmod]
@[simp] theorem mod_zero : a : Int, mod a 0 = a
@[simp] theorem tmod_zero : a : Int, tmod a 0 = a
| ofNat _ => congrArg ofNat <| Nat.mod_zero _
| -[_+1] => congrArg (fun n => -ofNat n) <| Nat.mod_zero _
@@ -221,7 +222,7 @@ theorem ediv_add_emod' (a b : Int) : a / b * b + a % b = a := by
theorem emod_def (a b : Int) : a % b = a - b * (a / b) := by
rw [ Int.add_sub_cancel (a % b), emod_add_ediv]
theorem mod_add_div : a b : Int, mod a b + b * (a.div b) = a
theorem tmod_add_tdiv : a b : Int, tmod a b + b * (a.tdiv b) = a
| ofNat _, ofNat _ => congrArg ofNat (Nat.mod_add_div ..)
| ofNat m, -[n+1] => by
show (m % succ n + -(succ n) * -(m / succ n) : Int) = m
@@ -238,17 +239,17 @@ theorem mod_add_div : ∀ a b : Int, mod a b + b * (a.div b) = a
rw [Int.neg_mul, Int.neg_add]
exact congrArg (-ofNat ·) (Nat.mod_add_div ..)
theorem div_add_mod (a b : Int) : b * a.div b + mod a b = a := by
rw [Int.add_comm]; apply mod_add_div ..
theorem tdiv_add_tmod (a b : Int) : b * a.tdiv b + tmod a b = a := by
rw [Int.add_comm]; apply tmod_add_tdiv ..
theorem mod_add_div' (m k : Int) : mod m k + m.div k * k = m := by
rw [Int.mul_comm]; apply mod_add_div
theorem tmod_add_tdiv' (m k : Int) : tmod m k + m.tdiv k * k = m := by
rw [Int.mul_comm]; apply tmod_add_tdiv
theorem div_add_mod' (m k : Int) : m.div k * k + mod m k = m := by
rw [Int.mul_comm]; apply div_add_mod
theorem tdiv_add_tmod' (m k : Int) : m.tdiv k * k + tmod m k = m := by
rw [Int.mul_comm]; apply tdiv_add_tmod
theorem mod_def (a b : Int) : mod a b = a - b * a.div b := by
rw [ Int.add_sub_cancel (mod a b), mod_add_div]
theorem tmod_def (a b : Int) : tmod a b = a - b * a.tdiv b := by
rw [ Int.add_sub_cancel (tmod a b), tmod_add_tdiv]
theorem fmod_add_fdiv : a b : Int, a.fmod b + b * a.fdiv b = a
| 0, ofNat _ | 0, -[_+1] => congrArg ofNat <| by simp
@@ -278,11 +279,11 @@ theorem fmod_def (a b : Int) : a.fmod b = a - b * a.fdiv b := by
theorem fmod_eq_emod (a : Int) {b : Int} (hb : 0 b) : fmod a b = a % b := by
simp [fmod_def, emod_def, fdiv_eq_ediv _ hb]
theorem mod_eq_emod {a b : Int} (ha : 0 a) (hb : 0 b) : mod a b = a % b := by
simp [emod_def, mod_def, div_eq_ediv ha hb]
theorem tmod_eq_emod {a b : Int} (ha : 0 a) (hb : 0 b) : tmod a b = a % b := by
simp [emod_def, tmod_def, tdiv_eq_ediv ha hb]
theorem fmod_eq_mod {a b : Int} (Ha : 0 a) (Hb : 0 b) : fmod a b = mod a b :=
mod_eq_emod Ha Hb fmod_eq_emod _ Hb
theorem fmod_eq_tmod {a b : Int} (Ha : 0 a) (Hb : 0 b) : fmod a b = tmod a b :=
tmod_eq_emod Ha Hb fmod_eq_emod _ Hb
/-! ### `/` ediv -/
@@ -297,7 +298,7 @@ theorem ediv_neg' {a b : Int} (Ha : a < 0) (Hb : 0 < b) : a / b < 0 :=
protected theorem div_def (a b : Int) : a / b = Int.ediv a b := rfl
theorem negSucc_ediv (m : Nat) {b : Int} (H : 0 < b) : -[m+1] / b = -(div m b + 1) :=
theorem negSucc_ediv (m : Nat) {b : Int} (H : 0 < b) : -[m+1] / b = -(ediv m b + 1) :=
match b, eq_succ_of_zero_lt H with
| _, _, rfl => rfl
@@ -305,6 +306,22 @@ theorem ediv_nonneg {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a / b :=
match a, b, eq_ofNat_of_zero_le Ha, eq_ofNat_of_zero_le Hb with
| _, _, _, rfl, _, rfl => ofNat_zero_le _
theorem ediv_nonneg_of_nonpos_of_nonpos {a b : Int} (Ha : a 0) (Hb : b 0) : 0 a / b := by
match a, b with
| ofNat a, b =>
match Int.le_antisymm Ha (ofNat_zero_le a) with
| h1 =>
rw [h1, zero_ediv]
exact Int.le_refl 0
| a, ofNat b =>
match Int.le_antisymm Hb (ofNat_zero_le b) with
| h1 =>
rw [h1, Int.ediv_zero]
exact Int.le_refl 0
| negSucc a, negSucc b =>
rw [Int.div_def, ediv]
exact le_add_one (ediv_nonneg (ofNat_zero_le a) (Int.le_trans (ofNat_zero_le b) (le.intro 1 rfl)))
theorem ediv_nonpos {a b : Int} (Ha : 0 a) (Hb : b 0) : a / b 0 :=
Int.nonpos_of_neg_nonneg <| Int.ediv_neg .. Int.ediv_nonneg Ha (Int.neg_nonneg_of_nonpos Hb)
@@ -796,191 +813,191 @@ theorem ediv_eq_ediv_of_mul_eq_mul {a b c d : Int}
Int.ediv_eq_of_eq_mul_right H3 <| by
rw [ Int.mul_ediv_assoc _ H2]; exact (Int.ediv_eq_of_eq_mul_left H4 H5.symm).symm
/-! ### div -/
/-! ### tdiv -/
@[simp] protected theorem div_one : a : Int, a.div 1 = a
@[simp] protected theorem tdiv_one : a : Int, a.tdiv 1 = a
| (n:Nat) => congrArg ofNat (Nat.div_one _)
| -[n+1] => by simp [Int.div, neg_ofNat_succ]; rfl
| -[n+1] => by simp [Int.tdiv, neg_ofNat_succ]; rfl
unseal Nat.div in
@[simp] protected theorem div_neg : a b : Int, a.div (-b) = -(a.div b)
@[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
unseal Nat.div in
@[simp] protected theorem neg_div : a b : Int, (-a).div b = -(a.div b)
@[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
protected theorem neg_div_neg (a b : Int) : (-a).div (-b) = a.div b := by
simp [Int.div_neg, Int.neg_div, Int.neg_neg]
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]
protected theorem div_nonneg {a b : Int} (Ha : 0 a) (Hb : 0 b) : 0 a.div b :=
protected theorem tdiv_nonneg {a b : Int} (Ha : 0 a) (Hb : 0 b) : 0 a.tdiv b :=
match a, b, eq_ofNat_of_zero_le Ha, eq_ofNat_of_zero_le Hb with
| _, _, _, rfl, _, rfl => ofNat_zero_le _
protected theorem div_nonpos {a b : Int} (Ha : 0 a) (Hb : b 0) : a.div b 0 :=
Int.nonpos_of_neg_nonneg <| Int.div_neg .. Int.div_nonneg Ha (Int.neg_nonneg_of_nonpos Hb)
protected theorem tdiv_nonpos {a b : Int} (Ha : 0 a) (Hb : b 0) : a.tdiv b 0 :=
Int.nonpos_of_neg_nonneg <| Int.tdiv_neg .. Int.tdiv_nonneg Ha (Int.neg_nonneg_of_nonpos Hb)
theorem div_eq_zero_of_lt {a b : Int} (H1 : 0 a) (H2 : a < b) : a.div b = 0 :=
theorem tdiv_eq_zero_of_lt {a b : Int} (H1 : 0 a) (H2 : a < b) : a.tdiv b = 0 :=
match a, b, eq_ofNat_of_zero_le H1, eq_succ_of_zero_lt (Int.lt_of_le_of_lt H1 H2) with
| _, _, _, rfl, _, rfl => congrArg Nat.cast <| Nat.div_eq_of_lt <| ofNat_lt.1 H2
@[simp] protected theorem mul_div_cancel (a : Int) {b : Int} (H : b 0) : (a * b).div b = a :=
have : {a b : Nat}, (b : Int) 0 (div (a * b) b : Int) = a := fun H => by
rw [ ofNat_mul, ofNat_div,
@[simp] protected theorem mul_tdiv_cancel (a : Int) {b : Int} (H : b 0) : (a * b).tdiv b = a :=
have : {a b : Nat}, (b : Int) 0 (tdiv (a * b) b : Int) = a := fun H => by
rw [ ofNat_mul, ofNat_tdiv,
Nat.mul_div_cancel _ <| Nat.pos_of_ne_zero <| Int.ofNat_ne_zero.1 H]
match a, b, a.eq_nat_or_neg, b.eq_nat_or_neg with
| _, _, a, .inl rfl, b, .inl rfl => this H
| _, _, a, .inl rfl, b, .inr rfl => by
rw [Int.mul_neg, Int.neg_div, Int.div_neg, Int.neg_neg,
rw [Int.mul_neg, Int.neg_tdiv, Int.tdiv_neg, Int.neg_neg,
this (Int.neg_ne_zero.1 H)]
| _, _, a, .inr rfl, b, .inl rfl => by rw [Int.neg_mul, Int.neg_div, this H]
| _, _, a, .inr rfl, b, .inl rfl => by rw [Int.neg_mul, Int.neg_tdiv, this H]
| _, _, a, .inr rfl, b, .inr rfl => by
rw [Int.neg_mul_neg, Int.div_neg, this (Int.neg_ne_zero.1 H)]
rw [Int.neg_mul_neg, Int.tdiv_neg, this (Int.neg_ne_zero.1 H)]
@[simp] protected theorem mul_div_cancel_left (b : Int) (H : a 0) : (a * b).div a = b :=
Int.mul_comm .. Int.mul_div_cancel _ H
@[simp] protected theorem mul_tdiv_cancel_left (b : Int) (H : a 0) : (a * b).tdiv a = b :=
Int.mul_comm .. Int.mul_tdiv_cancel _ H
@[simp] protected theorem div_self {a : Int} (H : a 0) : a.div a = 1 := by
have := Int.mul_div_cancel 1 H; rwa [Int.one_mul] at this
@[simp] protected theorem tdiv_self {a : Int} (H : a 0) : a.tdiv a = 1 := by
have := Int.mul_tdiv_cancel 1 H; rwa [Int.one_mul] at this
theorem mul_div_cancel_of_mod_eq_zero {a b : Int} (H : a.mod b = 0) : b * (a.div b) = a := by
have := mod_add_div a b; rwa [H, Int.zero_add] at this
theorem mul_tdiv_cancel_of_tmod_eq_zero {a b : Int} (H : a.tmod b = 0) : b * (a.tdiv b) = a := by
have := tmod_add_tdiv a b; rwa [H, Int.zero_add] at this
theorem div_mul_cancel_of_mod_eq_zero {a b : Int} (H : a.mod b = 0) : a.div b * b = a := by
rw [Int.mul_comm, mul_div_cancel_of_mod_eq_zero H]
theorem tdiv_mul_cancel_of_tmod_eq_zero {a b : Int} (H : a.tmod b = 0) : a.tdiv b * b = a := by
rw [Int.mul_comm, mul_tdiv_cancel_of_tmod_eq_zero H]
theorem dvd_of_mod_eq_zero {a b : Int} (H : mod b a = 0) : a b :=
b.div a, (mul_div_cancel_of_mod_eq_zero H).symm
theorem dvd_of_tmod_eq_zero {a b : Int} (H : tmod b a = 0) : a b :=
b.tdiv a, (mul_tdiv_cancel_of_tmod_eq_zero H).symm
protected theorem mul_div_assoc (a : Int) : {b c : Int}, c b (a * b).div c = a * (b.div c)
protected theorem mul_tdiv_assoc (a : Int) : {b c : Int}, c b (a * b).tdiv c = a * (b.tdiv c)
| _, c, d, rfl =>
if cz : c = 0 then by simp [cz, Int.mul_zero] else by
rw [Int.mul_left_comm, Int.mul_div_cancel_left _ cz, Int.mul_div_cancel_left _ cz]
rw [Int.mul_left_comm, Int.mul_tdiv_cancel_left _ cz, Int.mul_tdiv_cancel_left _ cz]
protected theorem mul_div_assoc' (b : Int) {a c : Int} (h : c a) :
(a * b).div c = a.div c * b := by
rw [Int.mul_comm, Int.mul_div_assoc _ h, Int.mul_comm]
protected theorem mul_tdiv_assoc' (b : Int) {a c : Int} (h : c a) :
(a * b).tdiv c = a.tdiv c * b := by
rw [Int.mul_comm, Int.mul_tdiv_assoc _ h, Int.mul_comm]
theorem div_dvd_div : {a b c : Int}, a b b c b.div a c.div a
theorem tdiv_dvd_tdiv : {a b c : Int}, a b b c b.tdiv a c.tdiv a
| a, _, _, b, rfl, c, rfl => by
by_cases az : a = 0
· simp [az]
· rw [Int.mul_div_cancel_left _ az, Int.mul_assoc, Int.mul_div_cancel_left _ az]
· rw [Int.mul_tdiv_cancel_left _ az, Int.mul_assoc, Int.mul_tdiv_cancel_left _ az]
apply Int.dvd_mul_right
@[simp] theorem natAbs_div (a b : Int) : natAbs (a.div b) = (natAbs a).div (natAbs b) :=
@[simp] theorem natAbs_tdiv (a b : Int) : natAbs (a.tdiv b) = (natAbs a).div (natAbs b) :=
match a, b, eq_nat_or_neg a, eq_nat_or_neg b with
| _, _, _, .inl rfl, _, .inl rfl => rfl
| _, _, _, .inl rfl, _, .inr rfl => by rw [Int.div_neg, natAbs_neg, natAbs_neg]; rfl
| _, _, _, .inr rfl, _, .inl rfl => by rw [Int.neg_div, natAbs_neg, natAbs_neg]; rfl
| _, _, _, .inr rfl, _, .inr rfl => by rw [Int.neg_div_neg, natAbs_neg, natAbs_neg]; rfl
| _, _, _, .inl rfl, _, .inr rfl => by rw [Int.tdiv_neg, natAbs_neg, natAbs_neg]; rfl
| _, _, _, .inr rfl, _, .inl rfl => by rw [Int.neg_tdiv, natAbs_neg, natAbs_neg]; rfl
| _, _, _, .inr rfl, _, .inr rfl => by rw [Int.neg_tdiv_neg, natAbs_neg, natAbs_neg]; rfl
protected theorem div_eq_of_eq_mul_right {a b c : Int}
(H1 : b 0) (H2 : a = b * c) : a.div b = c := by rw [H2, Int.mul_div_cancel_left _ H1]
protected theorem tdiv_eq_of_eq_mul_right {a b c : Int}
(H1 : b 0) (H2 : a = b * c) : a.tdiv b = c := by rw [H2, Int.mul_tdiv_cancel_left _ H1]
protected theorem eq_div_of_mul_eq_right {a b c : Int}
(H1 : a 0) (H2 : a * b = c) : b = c.div a :=
(Int.div_eq_of_eq_mul_right H1 H2.symm).symm
protected theorem eq_tdiv_of_mul_eq_right {a b c : Int}
(H1 : a 0) (H2 : a * b = c) : b = c.tdiv a :=
(Int.tdiv_eq_of_eq_mul_right H1 H2.symm).symm
/-! ### (t-)mod -/
theorem ofNat_mod (m n : Nat) : ((m % n) : Int) = mod m n := rfl
theorem ofNat_tmod (m n : Nat) : ((m % n) : Int) = tmod m n := rfl
@[simp] theorem mod_one (a : Int) : mod a 1 = 0 := by
simp [mod_def, Int.div_one, Int.one_mul, Int.sub_self]
@[simp] theorem tmod_one (a : Int) : tmod a 1 = 0 := by
simp [tmod_def, Int.tdiv_one, Int.one_mul, Int.sub_self]
theorem mod_eq_of_lt {a b : Int} (H1 : 0 a) (H2 : a < b) : mod a b = a := by
rw [mod_eq_emod H1 (Int.le_trans H1 (Int.le_of_lt H2)), emod_eq_of_lt H1 H2]
theorem tmod_eq_of_lt {a b : Int} (H1 : 0 a) (H2 : a < b) : tmod a b = a := by
rw [tmod_eq_emod H1 (Int.le_trans H1 (Int.le_of_lt H2)), emod_eq_of_lt H1 H2]
theorem mod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : mod a b < b :=
theorem tmod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : tmod a b < b :=
match a, b, eq_succ_of_zero_lt H with
| ofNat _, _, n, rfl => ofNat_lt.2 <| Nat.mod_lt _ n.succ_pos
| -[_+1], _, n, rfl => Int.lt_of_le_of_lt
(Int.neg_nonpos_of_nonneg <| Int.ofNat_nonneg _) (ofNat_pos.2 n.succ_pos)
theorem mod_nonneg : {a : Int} (b : Int), 0 a 0 mod a b
theorem tmod_nonneg : {a : Int} (b : Int), 0 a 0 tmod a b
| ofNat _, -[_+1], _ | ofNat _, ofNat _, _ => ofNat_nonneg _
@[simp] theorem mod_neg (a b : Int) : mod a (-b) = mod a b := by
rw [mod_def, mod_def, Int.div_neg, Int.neg_mul_neg]
@[simp] theorem tmod_neg (a b : Int) : tmod a (-b) = tmod a b := by
rw [tmod_def, tmod_def, Int.tdiv_neg, Int.neg_mul_neg]
@[simp] theorem mul_mod_left (a b : Int) : (a * b).mod b = 0 :=
@[simp] theorem mul_tmod_left (a b : Int) : (a * b).tmod b = 0 :=
if h : b = 0 then by simp [h, Int.mul_zero] else by
rw [Int.mod_def, Int.mul_div_cancel _ h, Int.mul_comm, Int.sub_self]
rw [Int.tmod_def, Int.mul_tdiv_cancel _ h, Int.mul_comm, Int.sub_self]
@[simp] theorem mul_mod_right (a b : Int) : (a * b).mod a = 0 := by
rw [Int.mul_comm, mul_mod_left]
@[simp] theorem mul_tmod_right (a b : Int) : (a * b).tmod a = 0 := by
rw [Int.mul_comm, mul_tmod_left]
theorem mod_eq_zero_of_dvd : {a b : Int}, a b mod b a = 0
| _, _, _, rfl => mul_mod_right ..
theorem tmod_eq_zero_of_dvd : {a b : Int}, a b tmod b a = 0
| _, _, _, rfl => mul_tmod_right ..
theorem dvd_iff_mod_eq_zero {a b : Int} : a b mod b a = 0 :=
mod_eq_zero_of_dvd, dvd_of_mod_eq_zero
theorem dvd_iff_tmod_eq_zero {a b : Int} : a b tmod b a = 0 :=
tmod_eq_zero_of_dvd, dvd_of_tmod_eq_zero
@[simp] theorem neg_mul_mod_right (a b : Int) : (-(a * b)).mod a = 0 := by
rw [ dvd_iff_mod_eq_zero, Int.dvd_neg]
@[simp] theorem neg_mul_tmod_right (a b : Int) : (-(a * b)).tmod a = 0 := by
rw [ dvd_iff_tmod_eq_zero, Int.dvd_neg]
exact Int.dvd_mul_right a b
@[simp] theorem neg_mul_mod_left (a b : Int) : (-(a * b)).mod b = 0 := by
rw [ dvd_iff_mod_eq_zero, Int.dvd_neg]
@[simp] theorem neg_mul_tmod_left (a b : Int) : (-(a * b)).tmod b = 0 := by
rw [ dvd_iff_tmod_eq_zero, Int.dvd_neg]
exact Int.dvd_mul_left a b
protected theorem div_mul_cancel {a b : Int} (H : b a) : a.div b * b = a :=
div_mul_cancel_of_mod_eq_zero (mod_eq_zero_of_dvd H)
protected theorem tdiv_mul_cancel {a b : Int} (H : b a) : a.tdiv b * b = a :=
tdiv_mul_cancel_of_tmod_eq_zero (tmod_eq_zero_of_dvd H)
protected theorem mul_div_cancel' {a b : Int} (H : a b) : a * b.div a = b := by
rw [Int.mul_comm, Int.div_mul_cancel H]
protected theorem mul_tdiv_cancel' {a b : Int} (H : a b) : a * b.tdiv a = b := by
rw [Int.mul_comm, Int.tdiv_mul_cancel H]
protected theorem eq_mul_of_div_eq_right {a b c : Int}
(H1 : b a) (H2 : a.div b = c) : a = b * c := by rw [ H2, Int.mul_div_cancel' H1]
protected theorem eq_mul_of_tdiv_eq_right {a b c : Int}
(H1 : b a) (H2 : a.tdiv b = c) : a = b * c := by rw [ H2, Int.mul_tdiv_cancel' H1]
@[simp] theorem mod_self {a : Int} : a.mod a = 0 := by
have := mul_mod_left 1 a; rwa [Int.one_mul] at this
@[simp] theorem tmod_self {a : Int} : a.tmod a = 0 := by
have := mul_tmod_left 1 a; rwa [Int.one_mul] at this
@[simp] theorem neg_mod_self (a : Int) : (-a).mod a = 0 := by
rw [ dvd_iff_mod_eq_zero, Int.dvd_neg]
@[simp] theorem neg_tmod_self (a : Int) : (-a).tmod a = 0 := by
rw [ dvd_iff_tmod_eq_zero, Int.dvd_neg]
exact Int.dvd_refl a
theorem lt_div_add_one_mul_self (a : Int) {b : Int} (H : 0 < b) : a < (a.div b + 1) * b := by
theorem lt_tdiv_add_one_mul_self (a : Int) {b : Int} (H : 0 < b) : a < (a.tdiv b + 1) * b := by
rw [Int.add_mul, Int.one_mul, Int.mul_comm]
exact Int.lt_add_of_sub_left_lt <| Int.mod_def .. mod_lt_of_pos _ H
exact Int.lt_add_of_sub_left_lt <| Int.tmod_def .. tmod_lt_of_pos _ H
protected theorem div_eq_iff_eq_mul_right {a b c : Int}
(H : b 0) (H' : b a) : a.div b = c a = b * c :=
Int.eq_mul_of_div_eq_right H', Int.div_eq_of_eq_mul_right H
protected theorem tdiv_eq_iff_eq_mul_right {a b c : Int}
(H : b 0) (H' : b a) : a.tdiv b = c a = b * c :=
Int.eq_mul_of_tdiv_eq_right H', Int.tdiv_eq_of_eq_mul_right H
protected theorem div_eq_iff_eq_mul_left {a b c : Int}
(H : b 0) (H' : b a) : a.div b = c a = c * b := by
rw [Int.mul_comm]; exact Int.div_eq_iff_eq_mul_right H H'
protected theorem tdiv_eq_iff_eq_mul_left {a b c : Int}
(H : b 0) (H' : b a) : a.tdiv b = c a = c * b := by
rw [Int.mul_comm]; exact Int.tdiv_eq_iff_eq_mul_right H H'
protected theorem eq_mul_of_div_eq_left {a b c : Int}
(H1 : b a) (H2 : a.div b = c) : a = c * b := by
rw [Int.mul_comm, Int.eq_mul_of_div_eq_right H1 H2]
protected theorem eq_mul_of_tdiv_eq_left {a b c : Int}
(H1 : b a) (H2 : a.tdiv b = c) : a = c * b := by
rw [Int.mul_comm, Int.eq_mul_of_tdiv_eq_right H1 H2]
protected theorem div_eq_of_eq_mul_left {a b c : Int}
(H1 : b 0) (H2 : a = c * b) : a.div b = c :=
Int.div_eq_of_eq_mul_right H1 (by rw [Int.mul_comm, H2])
protected theorem tdiv_eq_of_eq_mul_left {a b c : Int}
(H1 : b 0) (H2 : a = c * b) : a.tdiv b = c :=
Int.tdiv_eq_of_eq_mul_right H1 (by rw [Int.mul_comm, H2])
protected theorem eq_zero_of_div_eq_zero {d n : Int} (h : d n) (H : n.div d = 0) : n = 0 := by
rw [ Int.mul_div_cancel' h, H, Int.mul_zero]
protected theorem eq_zero_of_tdiv_eq_zero {d n : Int} (h : d n) (H : n.tdiv d = 0) : n = 0 := by
rw [ Int.mul_tdiv_cancel' h, H, Int.mul_zero]
@[simp] protected theorem div_left_inj {a b d : Int}
(hda : d a) (hdb : d b) : a.div d = b.div d a = b := by
refine fun h => ?_, congrArg (div · d)
rw [ Int.mul_div_cancel' hda, Int.mul_div_cancel' hdb, h]
@[simp] protected theorem tdiv_left_inj {a b d : Int}
(hda : d a) (hdb : d b) : a.tdiv d = b.tdiv d a = b := by
refine fun h => ?_, congrArg (tdiv · d)
rw [ Int.mul_tdiv_cancel' hda, Int.mul_tdiv_cancel' hdb, h]
theorem div_sign : a b, a.div (sign b) = a * sign b
theorem tdiv_sign : a b, a.tdiv (sign b) = a * sign b
| _, succ _ => by simp [sign, Int.mul_one]
| _, 0 => by simp [sign, Int.mul_zero]
| _, -[_+1] => by simp [sign, Int.mul_neg, Int.mul_one]
protected theorem sign_eq_div_abs (a : Int) : sign a = a.div (natAbs a) :=
protected theorem sign_eq_tdiv_abs (a : Int) : sign a = a.tdiv (natAbs a) :=
if az : a = 0 then by simp [az] else
(Int.div_eq_of_eq_mul_left (ofNat_ne_zero.2 <| natAbs_ne_zero.2 az)
(Int.tdiv_eq_of_eq_mul_left (ofNat_ne_zero.2 <| natAbs_ne_zero.2 az)
(sign_mul_natAbs _).symm).symm
/-! ### fdiv -/
@@ -1033,7 +1050,7 @@ theorem fmod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a.fmod b = a :=
rw [fmod_eq_emod _ (Int.le_trans H1 (Int.le_of_lt H2)), emod_eq_of_lt H1 H2]
theorem fmod_nonneg {a b : Int} (ha : 0 a) (hb : 0 b) : 0 a.fmod b :=
fmod_eq_mod ha hb mod_nonneg _ ha
fmod_eq_tmod ha hb tmod_nonneg _ ha
theorem fmod_nonneg' (a : Int) {b : Int} (hb : 0 < b) : 0 a.fmod b :=
fmod_eq_emod _ (Int.le_of_lt hb) emod_nonneg _ (Int.ne_of_lt hb).symm
@@ -1053,10 +1070,10 @@ theorem fmod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a.fmod b < b :=
/-! ### Theorems crossing div/mod versions -/
theorem div_eq_ediv_of_dvd {a b : Int} (h : b a) : a.div b = a / b := by
theorem tdiv_eq_ediv_of_dvd {a b : Int} (h : b a) : a.tdiv b = a / b := by
by_cases b0 : b = 0
· simp [b0]
· rw [Int.div_eq_iff_eq_mul_left b0 h, Int.ediv_eq_iff_eq_mul_left b0 h]
· rw [Int.tdiv_eq_iff_eq_mul_left b0 h, Int.ediv_eq_iff_eq_mul_left b0 h]
theorem fdiv_eq_ediv_of_dvd : {a b : Int}, b a a.fdiv b = a / b
| _, b, c, rfl => by
@@ -1268,3 +1285,65 @@ theorem bmod_natAbs_plus_one (x : Int) (w : 1 < x.natAbs) : bmod x (x.natAbs + 1
all_goals decide
· exact ofNat_nonneg x
· exact succ_ofNat_pos (x + 1)
/-! ### Deprecations -/
@[deprecated Int.zero_tdiv (since := "2024-09-11")] protected abbrev zero_div := @Int.zero_tdiv
@[deprecated Int.tdiv_zero (since := "2024-09-11")] protected abbrev div_zero := @Int.tdiv_zero
@[deprecated tdiv_eq_ediv (since := "2024-09-11")] abbrev div_eq_ediv := @tdiv_eq_ediv
@[deprecated fdiv_eq_tdiv (since := "2024-09-11")] abbrev fdiv_eq_div := @fdiv_eq_tdiv
@[deprecated zero_tmod (since := "2024-09-11")] abbrev zero_mod := @zero_tmod
@[deprecated tmod_zero (since := "2024-09-11")] abbrev mod_zero := @tmod_zero
@[deprecated tmod_add_tdiv (since := "2024-09-11")] abbrev mod_add_div := @tmod_add_tdiv
@[deprecated tdiv_add_tmod (since := "2024-09-11")] abbrev div_add_mod := @tdiv_add_tmod
@[deprecated tmod_add_tdiv' (since := "2024-09-11")] abbrev mod_add_div' := @tmod_add_tdiv'
@[deprecated tdiv_add_tmod' (since := "2024-09-11")] abbrev div_add_mod' := @tdiv_add_tmod'
@[deprecated tmod_def (since := "2024-09-11")] abbrev mod_def := @tmod_def
@[deprecated tmod_eq_emod (since := "2024-09-11")] abbrev mod_eq_emod := @tmod_eq_emod
@[deprecated fmod_eq_tmod (since := "2024-09-11")] abbrev fmod_eq_mod := @fmod_eq_tmod
@[deprecated Int.tdiv_one (since := "2024-09-11")] protected abbrev div_one := @Int.tdiv_one
@[deprecated Int.tdiv_neg (since := "2024-09-11")] protected abbrev div_neg := @Int.tdiv_neg
@[deprecated Int.neg_tdiv (since := "2024-09-11")] protected abbrev neg_div := @Int.neg_tdiv
@[deprecated Int.neg_tdiv_neg (since := "2024-09-11")] protected abbrev neg_div_neg := @Int.neg_tdiv_neg
@[deprecated Int.tdiv_nonneg (since := "2024-09-11")] protected abbrev div_nonneg := @Int.tdiv_nonneg
@[deprecated Int.tdiv_nonpos (since := "2024-09-11")] protected abbrev div_nonpos := @Int.tdiv_nonpos
@[deprecated Int.tdiv_eq_zero_of_lt (since := "2024-09-11")] abbrev div_eq_zero_of_lt := @Int.tdiv_eq_zero_of_lt
@[deprecated Int.mul_tdiv_cancel (since := "2024-09-11")] protected abbrev mul_div_cancel := @Int.mul_tdiv_cancel
@[deprecated Int.mul_tdiv_cancel_left (since := "2024-09-11")] protected abbrev mul_div_cancel_left := @Int.mul_tdiv_cancel_left
@[deprecated Int.tdiv_self (since := "2024-09-11")] protected abbrev div_self := @Int.tdiv_self
@[deprecated Int.mul_tdiv_cancel_of_tmod_eq_zero (since := "2024-09-11")] abbrev mul_div_cancel_of_mod_eq_zero := @Int.mul_tdiv_cancel_of_tmod_eq_zero
@[deprecated Int.tdiv_mul_cancel_of_tmod_eq_zero (since := "2024-09-11")] abbrev div_mul_cancel_of_mod_eq_zero := @Int.tdiv_mul_cancel_of_tmod_eq_zero
@[deprecated Int.dvd_of_tmod_eq_zero (since := "2024-09-11")] abbrev dvd_of_mod_eq_zero := @Int.dvd_of_tmod_eq_zero
@[deprecated Int.mul_tdiv_assoc (since := "2024-09-11")] protected abbrev mul_div_assoc := @Int.mul_tdiv_assoc
@[deprecated Int.mul_tdiv_assoc' (since := "2024-09-11")] protected abbrev mul_div_assoc' := @Int.mul_tdiv_assoc'
@[deprecated Int.tdiv_dvd_tdiv (since := "2024-09-11")] abbrev div_dvd_div := @Int.tdiv_dvd_tdiv
@[deprecated Int.natAbs_tdiv (since := "2024-09-11")] abbrev natAbs_div := @Int.natAbs_tdiv
@[deprecated Int.tdiv_eq_of_eq_mul_right (since := "2024-09-11")] protected abbrev div_eq_of_eq_mul_right := @Int.tdiv_eq_of_eq_mul_right
@[deprecated Int.eq_tdiv_of_mul_eq_right (since := "2024-09-11")] protected abbrev eq_div_of_mul_eq_right := @Int.eq_tdiv_of_mul_eq_right
@[deprecated Int.ofNat_tmod (since := "2024-09-11")] abbrev ofNat_mod := @Int.ofNat_tmod
@[deprecated Int.tmod_one (since := "2024-09-11")] abbrev mod_one := @Int.tmod_one
@[deprecated Int.tmod_eq_of_lt (since := "2024-09-11")] abbrev mod_eq_of_lt := @Int.tmod_eq_of_lt
@[deprecated Int.tmod_lt_of_pos (since := "2024-09-11")] abbrev mod_lt_of_pos := @Int.tmod_lt_of_pos
@[deprecated Int.tmod_nonneg (since := "2024-09-11")] abbrev mod_nonneg := @Int.tmod_nonneg
@[deprecated Int.tmod_neg (since := "2024-09-11")] abbrev mod_neg := @Int.tmod_neg
@[deprecated Int.mul_tmod_left (since := "2024-09-11")] abbrev mul_mod_left := @Int.mul_tmod_left
@[deprecated Int.mul_tmod_right (since := "2024-09-11")] abbrev mul_mod_right := @Int.mul_tmod_right
@[deprecated Int.tmod_eq_zero_of_dvd (since := "2024-09-11")] abbrev mod_eq_zero_of_dvd := @Int.tmod_eq_zero_of_dvd
@[deprecated Int.dvd_iff_tmod_eq_zero (since := "2024-09-11")] abbrev dvd_iff_mod_eq_zero := @Int.dvd_iff_tmod_eq_zero
@[deprecated Int.neg_mul_tmod_right (since := "2024-09-11")] abbrev neg_mul_mod_right := @Int.neg_mul_tmod_right
@[deprecated Int.neg_mul_tmod_left (since := "2024-09-11")] abbrev neg_mul_mod_left := @Int.neg_mul_tmod_left
@[deprecated Int.tdiv_mul_cancel (since := "2024-09-11")] protected abbrev div_mul_cancel := @Int.tdiv_mul_cancel
@[deprecated Int.mul_tdiv_cancel' (since := "2024-09-11")] protected abbrev mul_div_cancel' := @Int.mul_tdiv_cancel'
@[deprecated Int.eq_mul_of_tdiv_eq_right (since := "2024-09-11")] protected abbrev eq_mul_of_div_eq_right := @Int.eq_mul_of_tdiv_eq_right
@[deprecated Int.tmod_self (since := "2024-09-11")] abbrev mod_self := @Int.tmod_self
@[deprecated Int.neg_tmod_self (since := "2024-09-11")] abbrev neg_mod_self := @Int.neg_tmod_self
@[deprecated Int.lt_tdiv_add_one_mul_self (since := "2024-09-11")] abbrev lt_div_add_one_mul_self := @Int.lt_tdiv_add_one_mul_self
@[deprecated Int.tdiv_eq_iff_eq_mul_right (since := "2024-09-11")] protected abbrev div_eq_iff_eq_mul_right := @Int.tdiv_eq_iff_eq_mul_right
@[deprecated Int.tdiv_eq_iff_eq_mul_left (since := "2024-09-11")] protected abbrev div_eq_iff_eq_mul_left := @Int.tdiv_eq_iff_eq_mul_left
@[deprecated Int.eq_mul_of_tdiv_eq_left (since := "2024-09-11")] protected abbrev eq_mul_of_div_eq_left := @Int.eq_mul_of_tdiv_eq_left
@[deprecated Int.tdiv_eq_of_eq_mul_left (since := "2024-09-11")] protected abbrev div_eq_of_eq_mul_left := @Int.tdiv_eq_of_eq_mul_left
@[deprecated Int.eq_zero_of_tdiv_eq_zero (since := "2024-09-11")] protected abbrev eq_zero_of_div_eq_zero := @Int.eq_zero_of_tdiv_eq_zero
@[deprecated Int.tdiv_left_inj (since := "2024-09-11")] protected abbrev div_left_inj := @Int.tdiv_left_inj
@[deprecated Int.tdiv_sign (since := "2024-09-11")] abbrev div_sign := @Int.tdiv_sign
@[deprecated Int.sign_eq_tdiv_abs (since := "2024-09-11")] protected abbrev sign_eq_div_abs := @Int.sign_eq_tdiv_abs
@[deprecated Int.tdiv_eq_ediv_of_dvd (since := "2024-09-11")] abbrev div_eq_ediv_of_dvd := @Int.tdiv_eq_ediv_of_dvd

View File

@@ -119,12 +119,12 @@ theorem countP_filter (l : List α) :
countP p (filter q l) = countP (fun a => p a && q a) l := by
simp only [countP_eq_length_filter, filter_filter]
@[simp] theorem countP_true {l : List α} : (l.countP fun _ => true) = l.length := by
rw [countP_eq_length]
@[simp] theorem countP_true : (countP fun (_ : α) => true) = length := by
funext l
simp
@[simp] theorem countP_false {l : List α} : (l.countP fun _ => false) = 0 := by
rw [countP_eq_zero]
@[simp] theorem countP_false : (countP fun (_ : α) => false) = Function.const _ 0 := by
funext l
simp
@[simp] theorem countP_map (p : β Bool) (f : α β) :

View File

@@ -572,17 +572,25 @@ theorem any_eq {l : List α} : l.any p = decide (∃ x, x ∈ l ∧ p x) := by i
theorem all_eq {l : List α} : l.all p = decide ( x, x l p x) := by induction l <;> simp [*]
@[simp] theorem any_decide {l : List α} {p : α Prop} [DecidablePred p] :
l.any p = decide ( x, x l p x) := by
theorem decide_exists_mem {l : List α} {p : α Prop} [DecidablePred p] :
decide ( x, x l p x) = l.any p := by
simp [any_eq]
@[simp] theorem all_decide {l : List α} {p : α Prop} [DecidablePred p] :
l.all p = decide ( x, x l p x) := by
theorem decide_forall_mem {l : List α} {p : α Prop} [DecidablePred p] :
decide ( x, x l p x) = l.all p := by
simp [all_eq]
@[simp] theorem any_eq_true {l : List α} : l.any p = true x, x l p x := by simp [any_eq]
@[simp] theorem any_eq_true {l : List α} : l.any p = true x, x l p x := by
simp only [any_eq, decide_eq_true_eq]
@[simp] theorem all_eq_true {l : List α} : l.all p = true x, x l p x := by simp [all_eq]
@[simp] theorem all_eq_true {l : List α} : l.all p = true x, x l p x := by
simp only [all_eq, decide_eq_true_eq]
@[simp] theorem any_eq_false {l : List α} : l.any p = false x, x l ¬p x := by
simp [any_eq]
@[simp] theorem all_eq_false {l : List α} : l.all p = false x, x l ¬p x := by
simp [all_eq]
/-! ### set -/
@@ -1044,6 +1052,9 @@ theorem tail_eq_tailD (l) : @tail α l = tailD l [] := by cases l <;> rfl
theorem tail_eq_tail? (l) : @tail α l = (tail? l).getD [] := by simp [tail_eq_tailD]
theorem mem_of_mem_tail {a : α} {l : List α} (h : a tail l) : a l := by
induction l <;> simp_all
/-! ## Basic operations -/
/-! ### map -/
@@ -2312,6 +2323,47 @@ theorem bind_replicate {β} (f : α → List β) : (replicate n a).bind f = (rep
@[simp] theorem isEmpty_replicate : (replicate n a).isEmpty = decide (n = 0) := by
cases n <;> simp [replicate_succ]
/-- Every list is either empty, a non-empty `replicate`, or begins with a non-empty `replicate`
followed by a different element. -/
theorem eq_replicate_or_eq_replicate_append_cons {α : Type _} (l : List α) :
(l = []) ( n a, l = replicate n a 0 < n)
( n a b l', l = replicate n a ++ b :: l' 0 < n a b) := by
induction l with
| nil => simp
| cons x l ih =>
right
rcases ih with rfl | n, a, rfl, h | n, a, b, l', rfl, h
· left
exact 1, x, rfl, by decide
· by_cases h' : x = a
· subst h'
left
exact n + 1, x, rfl, by simp
· right
refine 1, x, a, replicate (n - 1) a, ?_, by decide, h'
match n with | n + 1 => simp [replicate_succ]
· right
by_cases h' : x = a
· subst h'
refine n + 1, x, b, l', by simp [replicate_succ], by simp, h.2
· refine 1, x, a, replicate (n - 1) a ++ b :: l', ?_, by decide, h'
match n with | n + 1 => simp [replicate_succ]
/-- An induction principle for lists based on contiguous runs of identical elements. -/
-- A `Sort _` valued version would require a different design. (And associated `@[simp]` lemmas.)
theorem replicateRecOn {α : Type _} {p : List α Prop} (m : List α)
(h0 : p []) (hr : a n, 0 < n p (replicate n a))
(hi : a b n l, a b 0 < n p (b :: l) p (replicate n a ++ b :: l)) : p m := by
rcases eq_replicate_or_eq_replicate_append_cons m with
rfl | n, a, rfl, hn | n, a, b, l', w, hn, h
· exact h0
· exact hr _ _ hn
· have : (b :: l').length < m.length := by
simpa [w] using Nat.lt_add_of_pos_left hn
subst w
exact hi _ _ _ _ h hn (replicateRecOn (b :: l') h0 hr hi)
termination_by m.length
/-! ### reverse -/
@[simp] theorem length_reverse (as : List α) : (as.reverse).length = as.length := by

View File

@@ -22,17 +22,18 @@ namespace List
This version is not tail-recursive,
but it is replaced at runtime by `mergeTR` using a `@[csimp]` lemma.
-/
def merge (le : α α Bool) : List α List α List α
def merge (xs ys : List α) (le : α α Bool := by exact fun a b => a b) : List α :=
match xs, ys with
| [], ys => ys
| xs, [] => xs
| x :: xs, y :: ys =>
if le x y then
x :: merge le xs (y :: ys)
x :: merge xs (y :: ys) le
else
y :: merge le (x :: xs) ys
y :: merge (x :: xs) ys le
@[simp] theorem nil_merge (ys : List α) : merge le [] ys = ys := by simp [merge]
@[simp] theorem merge_right (xs : List α) : merge le xs [] = xs := by
@[simp] theorem nil_merge (ys : List α) : merge [] ys le = ys := by simp [merge]
@[simp] theorem merge_right (xs : List α) : merge xs [] le = xs := by
induction xs with
| nil => simp [merge]
| cons x xs ih => simp [merge, ih]
@@ -45,6 +46,7 @@ def splitInTwo (l : { l : List α // l.length = n }) :
let r := splitAt ((n+1)/2) l.1
(r.1, by simp [r, splitAt_eq, l.2]; omega, r.2, by simp [r, splitAt_eq, l.2]; omega)
set_option linter.unusedVariables false in
/--
Simplified implementation of stable merge sort.
@@ -56,16 +58,15 @@ It is replaced at runtime in the compiler by `mergeSortTR₂` using a `@[csimp]`
Because we want the sort to be stable,
it is essential that we split the list in two contiguous sublists.
-/
def mergeSort (le : α α Bool) : List α List α
| [] => []
| [a] => [a]
| a :: b :: xs =>
def mergeSort : (xs : List α) (le : α α Bool := by exact fun a b => a b), List α
| [], _ => []
| [a], _ => [a]
| a :: b :: xs, le =>
let lr := splitInTwo a :: b :: xs, rfl
have := by simpa using lr.2.2
have := by simpa using lr.1.2
merge le (mergeSort le lr.1) (mergeSort le lr.2)
termination_by l => l.length
merge (mergeSort lr.1 le) (mergeSort lr.2 le) le
termination_by xs => xs.length
/--
Given an ordering relation `le : αα → Bool`,

View File

@@ -38,7 +38,7 @@ namespace List.MergeSort.Internal
/--
`O(min |l| |r|)`. Merge two lists using `le` as a switch.
-/
def mergeTR (le : α α Bool) (l l₂ : List α) : List α :=
def mergeTR (l l₂ : List α) (le : α α Bool) : List α :=
go l₁ l₂ []
where go : List α List α List α List α
| [], l₂, acc => reverseAux acc l₂
@@ -49,7 +49,7 @@ where go : List α → List α → List α → List α
else
go (x :: xs) ys (y :: acc)
theorem mergeTR_go_eq : mergeTR.go le l₁ l₂ acc = acc.reverse ++ merge le l₁ l₂ := by
theorem mergeTR_go_eq : mergeTR.go le l₁ l₂ acc = acc.reverse ++ merge l₁ l₂ le := by
induction l₁ generalizing l₂ acc with
| nil => simp [mergeTR.go, merge, reverseAux_eq]
| cons x l₁ ih₁ =>
@@ -97,14 +97,14 @@ This version uses the tail-recurive `mergeTR` function as a subroutine.
This is not the final version we use at runtime, as `mergeSortTR₂` is faster.
This definition is useful as an intermediate step in proving the `@[csimp]` lemma for `mergeSortTR₂`.
-/
def mergeSortTR (le : α α Bool) (l : List α) : List α :=
def mergeSortTR (l : List α) (le : α α Bool := by exact fun a b => a b) : List α :=
run l, rfl
where run : {n : Nat} { l : List α // l.length = n } List α
| 0, [], _ => []
| 1, [a], _ => [a]
| n+2, xs =>
let (l, r) := splitInTwo xs
mergeTR le (run l) (run r)
mergeTR (run l) (run r) le
/--
Split a list in two equal parts, reversing the first part.
@@ -130,7 +130,7 @@ Faster version of `mergeSortTR`, which avoids unnecessary list reversals.
-- Per the benchmark in `tests/bench/mergeSort/`
-- (which averages over 4 use cases: already sorted lists, reverse sorted lists, almost sorted lists, and random lists),
-- for lists of length 10^6, `mergeSortTR₂` is about 20% faster than `mergeSortTR`.
def mergeSortTR₂ (le : α α Bool) (l : List α) : List α :=
def mergeSortTR₂ (l : List α) (le : α α Bool := by exact fun a b => a b) : List α :=
run l, rfl
where
run : {n : Nat} { l : List α // l.length = n } List α
@@ -138,13 +138,13 @@ where
| 1, [a], _ => [a]
| n+2, xs =>
let (l, r) := splitRevInTwo xs
mergeTR le (run' l) (run r)
mergeTR (run' l) (run r) le
run' : {n : Nat} { l : List α // l.length = n } List α
| 0, [], _ => []
| 1, [a], _ => [a]
| n+2, xs =>
let (l, r) := splitRevInTwo' xs
mergeTR le (run' r) (run l)
mergeTR (run' r) (run l) le
theorem splitRevInTwo'_fst (l : { l : List α // l.length = n }) :
(splitRevInTwo' l).1 = (splitInTwo l.1.reverse, by simpa using l.2).2.1, by have := l.2; simp; omega := by
@@ -166,7 +166,7 @@ theorem splitRevInTwo_snd (l : { l : List α // l.length = n }) :
(splitRevInTwo l).2 = (splitInTwo l).2.1, by have := l.2; simp; omega := by
simp only [splitRevInTwo, splitRevAt_eq, reverse_take, splitInTwo_snd]
theorem mergeSortTR_run_eq_mergeSort : {n : Nat} (l : { l : List α // l.length = n }) mergeSortTR.run le l = mergeSort le l.1
theorem mergeSortTR_run_eq_mergeSort : {n : Nat} (l : { l : List α // l.length = n }) mergeSortTR.run le l = mergeSort l.1 le
| 0, [], _
| 1, [a], _ => by simp [mergeSortTR.run, mergeSort]
| n+2, a :: b :: l, h => by
@@ -183,7 +183,7 @@ theorem mergeSort_eq_mergeSortTR : @mergeSort = @mergeSortTR := by
-- This mutual block is unfortunately quite slow to elaborate.
set_option maxHeartbeats 400000 in
mutual
theorem mergeSortTR₂_run_eq_mergeSort : {n : Nat} (l : { l : List α // l.length = n }) mergeSortTR₂.run le l = mergeSort le l.1
theorem mergeSortTR₂_run_eq_mergeSort : {n : Nat} (l : { l : List α // l.length = n }) mergeSortTR₂.run le l = mergeSort l.1 le
| 0, [], _
| 1, [a], _ => by simp [mergeSortTR₂.run, mergeSort]
| n+2, a :: b :: l, h => by
@@ -195,7 +195,7 @@ theorem mergeSortTR₂_run_eq_mergeSort : {n : Nat} → (l : { l : List α // l.
rw [reverse_reverse]
termination_by n => n
theorem mergeSortTR₂_run'_eq_mergeSort : {n : Nat} (l : { l : List α // l.length = n }) (w : l' = l.1.reverse) mergeSortTR₂.run' le l = mergeSort le l'
theorem mergeSortTR₂_run'_eq_mergeSort : {n : Nat} (l : { l : List α // l.length = n }) (w : l' = l.1.reverse) mergeSortTR₂.run' le l = mergeSort l' le
| 0, [], _, w
| 1, [a], _, w => by simp_all [mergeSortTR₂.run', mergeSort]
| n+2, a :: b :: l, h, w => by

View File

@@ -23,11 +23,6 @@ import Init.Data.Bool
namespace List
-- We enable this instance locally so we can write `Pairwise le` instead of `Pairwise (le · ·)` everywhere.
attribute [local instance] boolRelToRel
variable {le : α α Bool}
/-! ### splitInTwo -/
@[simp] theorem splitInTwo_fst (l : { l : List α // l.length = n }) :
@@ -89,6 +84,8 @@ theorem splitInTwo_fst_le_splitInTwo_snd {l : { l : List α // l.length = n }} (
/-! ### enumLE -/
variable {le : α α Bool}
theorem enumLE_trans (trans : a b c, le a b le b c le a c)
(a b c : Nat × α) : enumLE le a b enumLE le b c enumLE le a c := by
simp only [enumLE]
@@ -129,7 +126,7 @@ theorem enumLE_total (total : ∀ a b, !le a b → le b a)
/-! ### merge -/
theorem merge_stable : (xs ys) (_ : x y, x xs y ys x.1 y.1),
(merge (enumLE le) xs ys).map (·.2) = merge le (xs.map (·.2)) (ys.map (·.2))
(merge xs ys (enumLE le)).map (·.2) = merge (xs.map (·.2)) (ys.map (·.2)) le
| [], ys, _ => by simp [merge]
| xs, [], _ => by simp [merge]
| (i, x) :: xs, (j, y) :: ys, h => by
@@ -147,7 +144,7 @@ theorem merge_stable : ∀ (xs ys) (_ : ∀ x y, x ∈ xs → y ∈ ys → x.1
The elements of `merge le xs ys` are exactly the elements of `xs` and `ys`.
-/
-- We subsequently prove that `mergeSort_perm : merge le xs ys ~ xs ++ ys`.
theorem mem_merge {a : α} {xs ys : List α} : a merge le xs ys a xs a ys := by
theorem mem_merge {a : α} {xs ys : List α} : a merge xs ys le a xs a ys := by
induction xs generalizing ys with
| nil => simp [merge]
| cons x xs ih =>
@@ -161,6 +158,9 @@ theorem mem_merge {a : α} {xs ys : List α} : a ∈ merge le xs ys ↔ a ∈ xs
apply or_congr_left
simp only [or_comm (a := a = y), or_assoc]
-- We enable this instance locally so we can write `Pairwise le` instead of `Pairwise (le · ·)` everywhere.
attribute [local instance] boolRelToRel
/--
If the ordering relation `le` is transitive and total (i.e. `le a b le b a` for all `a, b`)
then the `merge` of two sorted lists is sorted.
@@ -168,7 +168,7 @@ then the `merge` of two sorted lists is sorted.
theorem sorted_merge
(trans : (a b c : α), le a b le b c le a c)
(total : (a b : α), !le a b le b a)
(l₁ l₂ : List α) (h₁ : l₁.Pairwise le) (h₂ : l₂.Pairwise le) : (merge le l₁ l₂).Pairwise le := by
(l₁ l₂ : List α) (h₁ : l₁.Pairwise le) (h₂ : l₂.Pairwise le) : (merge l₁ l₂ le).Pairwise le := by
induction l₁ generalizing l₂ with
| nil => simpa only [merge]
| cons x l₁ ih₁ =>
@@ -195,7 +195,7 @@ theorem sorted_merge
· exact ih₂ h₂.tail
theorem merge_of_le : {xs ys : List α} (_ : a b, a xs b ys le a b),
merge le xs ys = xs ++ ys
merge xs ys le = xs ++ ys
| [], ys, _
| xs, [], _ => by simp [merge]
| x :: xs, y :: ys, h => by
@@ -206,7 +206,7 @@ theorem merge_of_le : ∀ {xs ys : List α} (_ : ∀ a b, a ∈ xs → b ∈ ys
· exact h x y (mem_cons_self _ _) (mem_cons_self _ _)
variable (le) in
theorem merge_perm_append : {xs ys : List α}, merge le xs ys ~ xs ++ ys
theorem merge_perm_append : {xs ys : List α}, merge xs ys le ~ xs ++ ys
| [], ys => by simp [merge]
| xs, [] => by simp [merge]
| x :: xs, y :: ys => by
@@ -222,24 +222,23 @@ theorem merge_perm_append : ∀ {xs ys : List α}, merge le xs ys ~ xs ++ ys
@[simp] theorem mergeSort_singleton (a : α) : [a].mergeSort r = [a] := by rw [List.mergeSort]
variable (le) in
theorem mergeSort_perm : (l : List α), mergeSort le l ~ l
| [] => by simp [mergeSort]
| [a] => by simp [mergeSort]
| a :: b :: xs => by
theorem mergeSort_perm : (l : List α) (le), mergeSort l le ~ l
| [], _ => by simp [mergeSort]
| [a], _ => by simp [mergeSort]
| a :: b :: xs, le => by
simp only [mergeSort]
have : (splitInTwo a :: b :: xs, rfl).1.1.length < xs.length + 1 + 1 := by simp [splitInTwo_fst]; omega
have : (splitInTwo a :: b :: xs, rfl).2.1.length < xs.length + 1 + 1 := by simp [splitInTwo_snd]; omega
exact (merge_perm_append le).trans
(((mergeSort_perm _).append (mergeSort_perm _)).trans
(((mergeSort_perm _ _).append (mergeSort_perm _ _)).trans
(Perm.of_eq (splitInTwo_fst_append_splitInTwo_snd _)))
termination_by l => l.length
@[simp] theorem mergeSort_length (l : List α) : (mergeSort le l).length = l.length :=
(mergeSort_perm le l).length_eq
@[simp] theorem mergeSort_length (l : List α) : (mergeSort l le).length = l.length :=
(mergeSort_perm l le).length_eq
@[simp] theorem mem_mergeSort {a : α} {l : List α} : a mergeSort le l a l :=
(mergeSort_perm le l).mem_iff
@[simp] theorem mem_mergeSort {a : α} {l : List α} : a mergeSort l le a l :=
(mergeSort_perm l le).mem_iff
/--
The result of `mergeSort` is sorted,
@@ -251,7 +250,7 @@ The comparison function need not be irreflexive, i.e. `le a b` and `le b a` is a
theorem sorted_mergeSort
(trans : (a b c : α), le a b le b c le a c)
(total : (a b : α), !le a b le b a) :
(l : List α) (mergeSort le l).Pairwise le
(l : List α) (mergeSort l le).Pairwise le
| [] => by simp [mergeSort]
| [a] => by simp [mergeSort]
| a :: b :: xs => by
@@ -268,7 +267,7 @@ termination_by l => l.length
/--
If the input list is already sorted, then `mergeSort` does not change the list.
-/
theorem mergeSort_of_sorted : {l : List α} (_ : Pairwise le l), mergeSort le l = l
theorem mergeSort_of_sorted : {l : List α} (_ : Pairwise le l), mergeSort l le = l
| [], _ => by simp [mergeSort]
| [a], _ => by simp [mergeSort]
| a :: b :: xs, h => by
@@ -294,10 +293,10 @@ See also:
* `pair_sublist_mergeSort`: if `[a, b] <+ l` and `le a b`, then `[a, b] <+ mergeSort le l`)
-/
theorem mergeSort_enum {l : List α} :
(mergeSort (enumLE le) (l.enum)).map (·.2) = mergeSort le l :=
(mergeSort (l.enum) (enumLE le)).map (·.2) = mergeSort l le :=
go 0 l
where go : (i : Nat) (l : List α),
(mergeSort (enumLE le) (l.enumFrom i)).map (·.2) = mergeSort le l
(mergeSort (l.enumFrom i) (enumLE le)).map (·.2) = mergeSort l le
| _, []
| _, [a] => by simp [mergeSort]
| _, a :: b :: xs => by
@@ -320,24 +319,24 @@ theorem mergeSort_cons {le : αα → Bool}
(trans : (a b c : α), le a b le b c le a c)
(total : (a b : α), !le a b le b a)
(a : α) (l : List α) :
l₁ l₂, mergeSort le (a :: l) = l₁ ++ a :: l₂ mergeSort le l = l₁ ++ l₂
l₁ l₂, mergeSort (a :: l) le = l₁ ++ a :: l₂ mergeSort l le = l₁ ++ l₂
b, b l₁ !le a b := by
rw [ mergeSort_enum]
rw [enum_cons]
have nd : Nodup ((a :: l).enum.map (·.1)) := by rw [enum_map_fst]; exact nodup_range _
have m₁ : (0, a) mergeSort (enumLE le) ((a :: l).enum) :=
have m₁ : (0, a) mergeSort ((a :: l).enum) (enumLE le) :=
mem_mergeSort.mpr (mem_cons_self _ _)
obtain l₁, l₂, h := append_of_mem m₁
have s := sorted_mergeSort (enumLE_trans trans) (enumLE_total total) ((a :: l).enum)
rw [h] at s
have p := mergeSort_perm (enumLE le) ((a :: l).enum)
have p := mergeSort_perm ((a :: l).enum) (enumLE le)
rw [h] at p
refine l₁.map (·.2), l₂.map (·.2), ?_, ?_, ?_
· simpa using congrArg (·.map (·.2)) h
· rw [ mergeSort_enum.go 1, map_append]
congr 1
have q : mergeSort (enumLE le) (enumFrom 1 l) ~ l₁ ++ l₂ :=
(mergeSort_perm (enumLE le) (enumFrom 1 l)).trans
have q : mergeSort (enumFrom 1 l) (enumLE le) ~ l₁ ++ l₂ :=
(mergeSort_perm (enumFrom 1 l) (enumLE le)).trans
(p.symm.trans perm_middle).cons_inv
apply Perm.eq_of_sorted (le := enumLE le)
· rintro i, a j, b ha hb
@@ -379,7 +378,7 @@ theorem sublist_mergeSort
(trans : (a b c : α), le a b le b c le a c)
(total : (a b : α), !le a b le b a) :
{c : List α} (_ : c.Pairwise le) (_ : c <+ l),
c <+ mergeSort le l
c <+ mergeSort l le
| _, _, .slnil => nil_sublist _
| c, hc, @Sublist.cons _ _ l a h => by
obtain l₁, l₂, h₁, h₂, - := mergeSort_cons trans total a l
@@ -409,7 +408,7 @@ then `[a, b]` is still a sublist of `mergeSort le l`.
theorem pair_sublist_mergeSort
(trans : (a b c : α), le a b le b c le a c)
(total : (a b : α), !le a b le b a)
(hab : le a b) (h : [a, b] <+ l) : [a, b] <+ mergeSort le l :=
(hab : le a b) (h : [a, b] <+ l) : [a, b] <+ mergeSort l le :=
sublist_mergeSort trans total (pairwise_pair.mpr hab) h
@[deprecated (since := "2024-09-02")] abbrev mergeSort_stable_pair := @pair_sublist_mergeSort

View File

@@ -514,6 +514,10 @@ protected theorem add_lt_add_left {n m : Nat} (h : n < m) (k : Nat) : k + n < k
protected theorem add_lt_add_right {n m : Nat} (h : n < m) (k : Nat) : n + k < m + k :=
Nat.add_comm k m Nat.add_comm k n Nat.add_lt_add_left h k
protected theorem lt_add_of_pos_left (h : 0 < k) : n < k + n := by
rw [Nat.add_comm]
exact Nat.add_lt_add_left h n
protected theorem lt_add_of_pos_right (h : 0 < k) : n < n + k :=
Nat.add_lt_add_left h n

View File

@@ -476,16 +476,20 @@ theorem and_lt_two_pow (x : Nat) {y n : Nat} (right : y < 2^n) : (x &&& y) < 2^n
exact pow_le_pow_of_le_right Nat.zero_lt_two i_ge_n
simp [testBit_and, yf]
@[simp] theorem and_pow_two_is_mod (x n : Nat) : x &&& (2^n-1) = x % 2^n := by
@[simp] theorem and_pow_two_sub_one_eq_mod (x n : Nat) : x &&& 2^n - 1 = x % 2^n := by
apply eq_of_testBit_eq
intro i
simp only [testBit_and, testBit_mod_two_pow]
cases testBit x i <;> simp
theorem and_pow_two_identity {x : Nat} (lt : x < 2^n) : x &&& 2^n-1 = x := by
rw [and_pow_two_is_mod]
@[deprecated and_pow_two_sub_one_eq_mod (since := "2024-09-11")] abbrev and_pow_two_is_mod := @and_pow_two_sub_one_eq_mod
theorem and_pow_two_sub_one_of_lt_two_pow {x : Nat} (lt : x < 2^n) : x &&& 2^n - 1 = x := by
rw [and_pow_two_sub_one_eq_mod]
apply Nat.mod_eq_of_lt lt
@[deprecated and_pow_two_sub_one_of_lt_two_pow (since := "2024-09-11")] abbrev and_two_pow_identity := @and_pow_two_sub_one_of_lt_two_pow
@[simp] theorem and_mod_two_eq_one : (a &&& b) % 2 = 1 a % 2 = 1 b % 2 = 1 := by
simp only [mod_two_eq_one_iff_testBit_zero]
rw [testBit_and]

View File

@@ -84,9 +84,6 @@ protected theorem add_lt_add_of_lt_of_le {a b c d : Nat} (hlt : a < b) (hle : c
a + c < b + d :=
Nat.lt_of_le_of_lt (Nat.add_le_add_left hle _) (Nat.add_lt_add_right hlt _)
protected theorem lt_add_of_pos_left : 0 < k n < k + n := by
rw [Nat.add_comm]; exact Nat.lt_add_of_pos_right
protected theorem pos_of_lt_add_right (h : n < n + k) : 0 < k :=
Nat.lt_of_add_lt_add_left h
@@ -577,6 +574,15 @@ theorem mul_mod (a b n : Nat) : a * b % n = (a % n) * (b % n) % n := by
theorem add_mod (a b n : Nat) : (a + b) % n = ((a % n) + (b % n)) % n := by
rw [add_mod_mod, mod_add_mod]
@[simp] theorem self_sub_mod (n k : Nat) [NeZero k] : (n - k) % n = n - k := by
cases n with
| zero => simp
| succ n =>
rw [mod_eq_of_lt]
cases k with
| zero => simp_all
| succ k => omega
/-! ### pow -/
theorem pow_succ' {m n : Nat} : m ^ n.succ = m * m ^ n := by

View File

@@ -13,7 +13,7 @@ namespace Option
theorem mem_iff {a : α} {b : Option α} : a b b = some a := .rfl
@[simp] theorem mem_some {a b : α} : a some b a = b := by simp [mem_iff, eq_comm]
@[simp] theorem mem_some {a b : α} : a some b b = a := by simp [mem_iff]
theorem mem_some_self (a : α) : a some a := mem_some.2 rfl
@@ -432,6 +432,38 @@ section ite
(x if p then l else none) p x l := by
split <;> simp_all
@[simp] theorem dite_none_left_eq_some {p : Prop} [Decidable p] {b : ¬p Option β} :
(if h : p then none else b h) = some a h, b h = some a := by
split <;> simp_all
@[simp] theorem dite_none_right_eq_some {p : Prop} [Decidable p] {b : p Option α} :
(if h : p then b h else none) = some a h, b h = some a := by
split <;> simp_all
@[simp] theorem some_eq_dite_none_left {p : Prop} [Decidable p] {b : ¬p Option β} :
some a = (if h : p then none else b h) h, some a = b h := by
split <;> simp_all
@[simp] theorem some_eq_dite_none_right {p : Prop} [Decidable p] {b : p Option α} :
some a = (if h : p then b h else none) h, some a = b h := by
split <;> simp_all
@[simp] theorem ite_none_left_eq_some {p : Prop} [Decidable p] {b : Option β} :
(if p then none else b) = some a ¬ p b = some a := by
split <;> simp_all
@[simp] theorem ite_none_right_eq_some {p : Prop} [Decidable p] {b : Option α} :
(if p then b else none) = some a p b = some a := by
split <;> simp_all
@[simp] theorem some_eq_ite_none_left {p : Prop} [Decidable p] {b : Option β} :
some a = (if p then none else b) ¬ p some a = b := by
split <;> simp_all
@[simp] theorem some_eq_ite_none_right {p : Prop} [Decidable p] {b : Option α} :
some a = (if p then b else none) p some a = b := by
split <;> simp_all
@[simp] theorem isSome_dite {p : Prop} [Decidable p] {b : p β} :
(if h : p then some (b h) else none).isSome = true p := by
split <;> simpa

View File

@@ -29,7 +29,7 @@ instance : Repr Rat where
@[inline] def Rat.normalize (a : Rat) : Rat :=
let n := Nat.gcd a.num.natAbs a.den
if n == 1 then a else { num := a.num.div n, den := a.den / n }
if n == 1 then a else { num := a.num.tdiv n, den := a.den / n }
def mkRat (num : Int) (den : Nat) : Rat :=
if den == 0 then { num := 0 } else Rat.normalize { num, den }
@@ -53,7 +53,7 @@ protected def lt (a b : Rat) : Bool :=
protected def mul (a b : Rat) : Rat :=
let g1 := Nat.gcd a.den b.num.natAbs
let g2 := Nat.gcd a.num.natAbs b.den
{ num := (a.num.div g2)*(b.num.div g1)
{ num := (a.num.tdiv g2)*(b.num.tdiv g1)
den := (b.den / g2)*(a.den / g1) }
protected def inv (a : Rat) : Rat :=
@@ -78,7 +78,7 @@ protected def add (a b : Rat) : Rat :=
if g1 == 1 then
{ num, den }
else
{ num := num.div g1, den := den / g1 }
{ num := num.tdiv g1, den := den / g1 }
protected def sub (a b : Rat) : Rat :=
let g := Nat.gcd a.den b.den
@@ -91,7 +91,7 @@ protected def sub (a b : Rat) : Rat :=
if g1 == 1 then
{ num, den }
else
{ num := num.div g1, den := den / g1 }
{ num := num.tdiv g1, den := den / g1 }
protected def neg (a : Rat) : Rat :=
{ a with num := - a.num }
@@ -100,14 +100,14 @@ protected def floor (a : Rat) : Int :=
if a.den == 1 then
a.num
else
let r := a.num.mod a.den
let r := a.num.tmod a.den
if a.num < 0 then r - 1 else r
protected def ceil (a : Rat) : Int :=
if a.den == 1 then
a.num
else
let r := a.num.mod a.den
let r := a.num.tmod a.den
if a.num > 0 then r + 1 else r
instance : LT Rat where

View File

@@ -21,7 +21,7 @@ builtin_initialize
let some id := id?
| throwError "invalid `[inherit_doc]` attribute, could not infer doc source"
let declName Elab.realizeGlobalConstNoOverloadWithInfo id
if ( findSimpleDocString? ( getEnv) decl).isSome then
if ( findSimpleDocString? ( getEnv) decl (includeBuiltin := false)).isSome then
logWarning m!"{← mkConstWithLevelParams decl} already has a doc string"
let some doc findSimpleDocString? ( getEnv) declName
| logWarningAt id m!"{← mkConstWithLevelParams declName} does not have a doc string"

View File

@@ -643,7 +643,7 @@ where
| .proj _ _ b => return p.updateProj! ( go b)
| .mdata k b =>
if inaccessible? p |>.isSome then
return mkMData k ( withReader (fun _ => false) (go b))
return mkMData k ( withReader (fun _ => true) (go b))
else if let some (stx, p) := patternWithRef? p then
Elab.withInfoContext' (go p) fun p => do
/- If `p` is a free variable and we are not inside of an "inaccessible" pattern, this `p` is a binder. -/

View File

@@ -1016,7 +1016,15 @@ private def registerNamePrefixes : Environment → Name → Environment
@[export lean_environment_add]
private def add (env : Environment) (cinfo : ConstantInfo) : Environment :=
let env := registerNamePrefixes env cinfo.name
let name := cinfo.name
let env := match name with
| .str _ s =>
if s.get 0 == '_' then
-- Do not register namespaces that only contain internal declarations.
env
else
registerNamePrefixes env name
| _ => env
env.addAux cinfo
@[export lean_display_stats]

View File

@@ -322,7 +322,8 @@ where
stx := newStx
diagnostics := old.diagnostics
cancelTk? := ctx.newCancelTk
result? := some { oldSuccess with
result? := some {
parserState := newParserState
processedSnap := ( oldSuccess.processedSnap.bindIO (sync := true) fun oldProcessed => do
if let some oldProcSuccess := oldProcessed.result? then
-- also wait on old command parse snapshot as parsing is cheap and may allow for
@@ -330,8 +331,11 @@ where
oldProcSuccess.firstCmdSnap.bindIO (sync := true) fun oldCmd => do
let prom IO.Promise.new
let _ IO.asTask (parseCmd oldCmd newParserState oldProcSuccess.cmdState prom ctx)
return .pure { oldProcessed with result? := some { oldProcSuccess with
firstCmdSnap := { range? := none, task := prom.result } } }
return .pure {
diagnostics := oldProcessed.diagnostics
result? := some {
cmdState := oldProcSuccess.cmdState
firstCmdSnap := { range? := none, task := prom.result } } }
else
return .pure oldProcessed) } }
else return old

View File

@@ -438,9 +438,11 @@ def buildInductionCase (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr)
let mvar mkFreshExprSyntheticOpaqueMVar goal (tag := `hyp)
let mut mvarId := mvar.mvarId!
mvarId assertIHs IHs mvarId
trace[Meta.FunInd] "Goal before cleanup:{mvarId}"
for fvarId in toClear do
mvarId mvarId.clear fvarId
mvarId mvarId.cleanup (toPreserve := toPreserve)
trace[Meta.FunInd] "Goal after cleanup (toClear := {toClear.map mkFVar}) (toPreserve := {toPreserve.map mkFVar}):{mvarId}"
modify (·.push mvarId)
let mvar instantiateMVars mvar
pure mvar

View File

@@ -71,8 +71,8 @@ builtin_dsimproc [simp, seval] reduceMul ((_ * _ : Int)) := reduceBin ``HMul.hMu
builtin_dsimproc [simp, seval] reduceSub ((_ - _ : Int)) := reduceBin ``HSub.hSub 6 (· - ·)
builtin_dsimproc [simp, seval] reduceDiv ((_ / _ : Int)) := reduceBin ``HDiv.hDiv 6 (· / ·)
builtin_dsimproc [simp, seval] reduceMod ((_ % _ : Int)) := reduceBin ``HMod.hMod 6 (· % ·)
builtin_dsimproc [simp, seval] reduceTDiv (div _ _) := reduceBin ``Int.div 2 Int.div
builtin_dsimproc [simp, seval] reduceTMod (mod _ _) := reduceBin ``Int.mod 2 Int.mod
builtin_dsimproc [simp, seval] reduceTDiv (tdiv _ _) := reduceBin ``Int.div 2 Int.tdiv
builtin_dsimproc [simp, seval] reduceTMod (tmod _ _) := reduceBin ``Int.mod 2 Int.tmod
builtin_dsimproc [simp, seval] reduceFDiv (fdiv _ _) := reduceBin ``Int.fdiv 2 Int.fdiv
builtin_dsimproc [simp, seval] reduceFMod (fmod _ _) := reduceBin ``Int.fmod 2 Int.fmod
builtin_dsimproc [simp, seval] reduceBdiv (bdiv _ _) := reduceBinIntNatOp ``bdiv bdiv

View File

@@ -145,7 +145,7 @@ def errorAtSavedPosFn (msg : String) (delta : Bool) : ParserFn := fun c s =>
/-- Generate an error at the position saved with the `withPosition` combinator.
If `delta == true`, then it reports at saved position+1.
This useful to make sure a parser consumed at least one character. -/
def errorAtSavedPos (msg : String) (delta : Bool) : Parser := {
@[builtin_doc] def errorAtSavedPos (msg : String) (delta : Bool) : Parser := {
fn := errorAtSavedPosFn msg delta
}
@@ -271,7 +271,7 @@ def orelseFn (p q : ParserFn) : ParserFn :=
NOTE: In order for the pretty printer to retrace an `orelse`, `p` must be a call to `node` or some other parser
producing a single node kind. Nested `orelse` calls are flattened for this, i.e. `(node k1 p1 <|> node k2 p2) <|> ...`
is fine as well. -/
def orelse (p q : Parser) : Parser where
@[builtin_doc] def orelse (p q : Parser) : Parser where
info := orelseInfo p.info q.info
fn := orelseFn p.fn q.fn
@@ -295,7 +295,7 @@ This is important for the `p <|> q` combinator, because it is not backtracking,
`p` fails after consuming some tokens. To get backtracking behavior, use `atomic(p) <|> q` instead.
This parser has the same arity as `p` - it produces the same result as `p`. -/
def atomic : Parser Parser := withFn atomicFn
@[builtin_doc] def atomic : Parser Parser := withFn atomicFn
/-- Information about the state of the parse prior to the failing parser's execution -/
structure RecoveryContext where
@@ -335,7 +335,7 @@ state immediately after the failure.
The interactions between <|> and `recover'` are subtle, especially for syntactic
categories that admit user extension. Consider avoiding it in these cases. -/
def recover' (parser : Parser) (handler : RecoveryContext Parser) : Parser where
@[builtin_doc] def recover' (parser : Parser) (handler : RecoveryContext Parser) : Parser where
info := parser.info
fn := recoverFn parser.fn fun s => handler s |>.fn
@@ -347,7 +347,7 @@ If `handler` fails itself, then no recovery is performed.
The interactions between <|> and `recover` are subtle, especially for syntactic
categories that admit user extension. Consider avoiding it in these cases. -/
def recover (parser handler : Parser) : Parser := recover' parser fun _ => handler
@[builtin_doc] def recover (parser handler : Parser) : Parser := recover' parser fun _ => handler
def optionalFn (p : ParserFn) : ParserFn := fun c s =>
let iniSz := s.stackSize
@@ -378,7 +378,7 @@ position to the original state on success. So for example `lookahead("=>")` will
next token is `"=>"`, without actually consuming this token.
This parser has arity 0 - it does not capture anything. -/
def lookahead : Parser Parser := withFn lookaheadFn
@[builtin_doc] def lookahead : Parser Parser := withFn lookaheadFn
def notFollowedByFn (p : ParserFn) (msg : String) : ParserFn := fun c s =>
let iniSz := s.stackSize
@@ -394,7 +394,7 @@ def notFollowedByFn (p : ParserFn) (msg : String) : ParserFn := fun c s =>
if `p` succeeds then it fails with the message `"unexpected foo"`.
This parser has arity 0 - it does not capture anything. -/
def notFollowedBy (p : Parser) (msg : String) : Parser where
@[builtin_doc] def notFollowedBy (p : Parser) (msg : String) : Parser where
fn := notFollowedByFn p.fn msg
partial def manyAux (p : ParserFn) : ParserFn := fun c s => Id.run do
@@ -1143,7 +1143,7 @@ def checkWsBeforeFn (errorMsg : String) : ParserFn := fun _ s =>
For example, the parser `"foo" ws "+"` parses `foo +` or `foo/- -/+` but not `foo+`.
This parser has arity 0 - it does not capture anything. -/
def checkWsBefore (errorMsg : String := "space before") : Parser where
@[builtin_doc] def checkWsBefore (errorMsg : String := "space before") : Parser where
info := epsilonInfo
fn := checkWsBeforeFn errorMsg
@@ -1160,7 +1160,7 @@ def checkLinebreakBeforeFn (errorMsg : String) : ParserFn := fun _ s =>
(The line break may be inside a comment.)
This parser has arity 0 - it does not capture anything. -/
def checkLinebreakBefore (errorMsg : String := "line break") : Parser where
@[builtin_doc] def checkLinebreakBefore (errorMsg : String := "line break") : Parser where
info := epsilonInfo
fn := checkLinebreakBeforeFn errorMsg
@@ -1180,7 +1180,7 @@ This is almost the same as `"foo+"`, but using this parser will make `foo+` a to
problems for the use of `"foo"` and `"+"` as separate tokens in other parsers.
This parser has arity 0 - it does not capture anything. -/
def checkNoWsBefore (errorMsg : String := "no space before") : Parser := {
@[builtin_doc] def checkNoWsBefore (errorMsg : String := "no space before") : Parser := {
info := epsilonInfo
fn := checkNoWsBeforeFn errorMsg
}
@@ -1430,7 +1430,7 @@ position (see `withPosition`). This can be used to do whitespace sensitive synta
a `by` block or `do` block, where all the lines have to line up.
This parser has arity 0 - it does not capture anything. -/
def checkColEq (errorMsg : String := "checkColEq") : Parser where
@[builtin_doc] def checkColEq (errorMsg : String := "checkColEq") : Parser where
fn := checkColEqFn errorMsg
def checkColGeFn (errorMsg : String) : ParserFn := fun c s =>
@@ -1449,7 +1449,7 @@ certain indentation scope. For example it is used in the lean grammar for `else
that the `else` is not less indented than the `if` it matches with.
This parser has arity 0 - it does not capture anything. -/
def checkColGe (errorMsg : String := "checkColGe") : Parser where
@[builtin_doc] def checkColGe (errorMsg : String := "checkColGe") : Parser where
fn := checkColGeFn errorMsg
def checkColGtFn (errorMsg : String) : ParserFn := fun c s =>
@@ -1473,7 +1473,7 @@ Here, the `revert` tactic is followed by a list of `colGt ident`, because otherw
interpret `exact` as an identifier and try to revert a variable named `exact`.
This parser has arity 0 - it does not capture anything. -/
def checkColGt (errorMsg : String := "checkColGt") : Parser where
@[builtin_doc] def checkColGt (errorMsg : String := "checkColGt") : Parser where
fn := checkColGtFn errorMsg
def checkLineEqFn (errorMsg : String) : ParserFn := fun c s =>
@@ -1491,7 +1491,7 @@ different lines. For example, `else if` is parsed using `lineEq` to ensure that
are on the same line.
This parser has arity 0 - it does not capture anything. -/
def checkLineEq (errorMsg : String := "checkLineEq") : Parser where
@[builtin_doc] def checkLineEq (errorMsg : String := "checkLineEq") : Parser where
fn := checkLineEqFn errorMsg
/-- `withPosition(p)` runs `p` while setting the "saved position" to the current position.
@@ -1507,7 +1507,7 @@ The saved position is only available in the read-only state, which is why this i
after the `withPosition(..)` block the saved position will be restored to its original value.
This parser has the same arity as `p` - it just forwards the results of `p`. -/
def withPosition : Parser → Parser := withFn fun f c s =>
@[builtin_doc] def withPosition : Parser → Parser := withFn fun f c s =>
adaptCacheableContextFn ({ · with savedPos? := s.pos }) f c s
def withPositionAfterLinebreak : Parser → Parser := withFn fun f c s =>
@@ -1519,7 +1519,7 @@ parsers like `colGt` will have no effect. This is usually used by bracketing con
`(...)` so that the user can locally override whitespace sensitivity.
This parser has the same arity as `p` - it just forwards the results of `p`. -/
def withoutPosition (p : Parser) : Parser :=
@[builtin_doc] def withoutPosition (p : Parser) : Parser :=
adaptCacheableContext ({ · with savedPos? := none }) p
/-- `withForbidden tk p` runs `p` with `tk` as a "forbidden token". This means that if the token
@@ -1529,7 +1529,7 @@ stop there, making `tk` effectively a lowest-precedence operator. This is used f
would be treated as an application.
This parser has the same arity as `p` - it just forwards the results of `p`. -/
def withForbidden (tk : Token) (p : Parser) : Parser :=
@[builtin_doc] def withForbidden (tk : Token) (p : Parser) : Parser :=
adaptCacheableContext ({ · with forbiddenTk? := tk }) p
/-- `withoutForbidden(p)` runs `p` disabling the "forbidden token" (see `withForbidden`), if any.
@@ -1537,7 +1537,7 @@ This is usually used by bracketing constructs like `(...)` because there is no p
inside these nested constructs.
This parser has the same arity as `p` - it just forwards the results of `p`. -/
def withoutForbidden (p : Parser) : Parser :=
@[builtin_doc] def withoutForbidden (p : Parser) : Parser :=
adaptCacheableContext ({ · with forbiddenTk? := none }) p
def eoiFn : ParserFn := fun c s =>
@@ -1692,7 +1692,7 @@ def termParser (prec : Nat := 0) : Parser :=
-- ==================
/-- Fail if previous token is immediately followed by ':'. -/
def checkNoImmediateColon : Parser := {
@[builtin_doc] def checkNoImmediateColon : Parser := {
fn := fun c s =>
let prev := s.stxStack.back
if checkTailNoWs prev then
@@ -1756,7 +1756,7 @@ def unicodeSymbol (sym asciiSym : String) : Parser :=
Define parser for `$e` (if `anonymous == true`) and `$e:name`.
`kind` is embedded in the antiquotation's kind, and checked at syntax `match` unless `isPseudoKind` is true.
Antiquotations can be escaped as in `$$e`, which produces the syntax tree for `$e`. -/
def mkAntiquot (name : String) (kind : SyntaxNodeKind) (anonymous := true) (isPseudoKind := false) : Parser :=
@[builtin_doc] def mkAntiquot (name : String) (kind : SyntaxNodeKind) (anonymous := true) (isPseudoKind := false) : Parser :=
let kind := kind ++ (if isPseudoKind then `pseudo else .anonymous) ++ `antiquot
let nameP := node `antiquotName <| checkNoWsBefore ("no space before ':" ++ name ++ "'") >> symbol ":" >> nonReservedSymbol name
-- if parsing the kind fails and `anonymous` is true, check that we're not ignoring a different
@@ -1781,7 +1781,7 @@ def withAntiquotFn (antiquotP p : ParserFn) (isCatAntiquot := false) : ParserFn
p c s
/-- Optimized version of `mkAntiquot ... <|> p`. -/
def withAntiquot (antiquotP p : Parser) : Parser := {
@[builtin_doc] def withAntiquot (antiquotP p : Parser) : Parser := {
fn := withAntiquotFn antiquotP.fn p.fn
info := orelseInfo antiquotP.info p.info
}
@@ -1791,7 +1791,7 @@ def withoutInfo (p : Parser) : Parser := {
}
/-- Parse `$[p]suffix`, e.g. `$[p],*`. -/
def mkAntiquotSplice (kind : SyntaxNodeKind) (p suffix : Parser) : Parser :=
@[builtin_doc] def mkAntiquotSplice (kind : SyntaxNodeKind) (p suffix : Parser) : Parser :=
let kind := kind ++ `antiquot_scope
leadingNode kind maxPrec <| atomic <|
setExpected [] "$" >>
@@ -1808,7 +1808,7 @@ private def withAntiquotSuffixSpliceFn (kind : SyntaxNodeKind) (suffix : ParserF
s.mkNode (kind ++ `antiquot_suffix_splice) (s.stxStack.size - 2)
/-- Parse `suffix` after an antiquotation, e.g. `$x,*`, and put both into a new node. -/
def withAntiquotSuffixSplice (kind : SyntaxNodeKind) (p suffix : Parser) : Parser where
@[builtin_doc] def withAntiquotSuffixSplice (kind : SyntaxNodeKind) (p suffix : Parser) : Parser where
info := andthenInfo p.info suffix.info
fn c s :=
let s := p.fn c s

View File

@@ -78,7 +78,7 @@ All modifiers are optional, and have to come in the listed order.
`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. -/
def declModifiers (inline : Bool) := leading_parser
@[builtin_doc] def declModifiers (inline : Bool) := leading_parser
optional docComment >>
optional (Term.«attributes» >> if inline then skip else ppDedent ppLine) >>
optional visibility >>
@@ -86,13 +86,16 @@ def declModifiers (inline : Bool) := leading_parser
optional «unsafe» >>
optional («partial» <|> «nonrec»)
/-- `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names -/
def declId := leading_parser
-- @[builtin_doc] -- FIXME: suppress the hover
def declId := leading_parser
ident >> optional (".{" >> sepBy1 (recover ident (skipUntil (fun c => c.isWhitespace || c [',', '}']))) ", " >> "}")
/-- `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` -/
def declSig := leading_parser
-- @[builtin_doc] -- FIXME: suppress the hover
def declSig := leading_parser
many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> Term.typeSpec
/-- `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` -/
def optDeclSig := leading_parser
-- @[builtin_doc] -- FIXME: suppress the hover
def optDeclSig := leading_parser
many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> Term.optType
/-- Right-hand side of a `:=` in a declaration, a term. -/
def declBody : Parser :=
@@ -141,11 +144,11 @@ def whereStructInst := leading_parser
* a sequence of `| pat => expr` (a declaration by equations), shorthand for a `match`
* `where` and then a sequence of `field := value` initializers, shorthand for a structure constructor
-/
def declVal :=
@[builtin_doc] def declVal :=
-- Remark: we should not use `Term.whereDecls` at `declVal`
-- because `Term.whereDecls` is defined using `Term.letRecDecl` which may contain attributes.
-- Issue #753 shows an example that fails to be parsed when we used `Term.whereDecls`.
withAntiquot (mkAntiquot "declVal" `Lean.Parser.Command.declVal (isPseudoKind := true)) <|
withAntiquot (mkAntiquot "declVal" decl_name% (isPseudoKind := true)) <|
declValSimple <|> declValEqns <|> whereStructInst
def «abbrev» := leading_parser
"abbrev " >> declId >> ppIndent optDeclSig >> declVal
@@ -193,9 +196,10 @@ inductive List (α : Type u) where
```
A list of elements of type `α` is either the empty list, `nil`,
or an element `head : α` followed by a list `tail : List α`.
For more information about [inductive types](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html).
See [Inductive types](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html)
for more information.
-/
def «inductive» := leading_parser
@[builtin_doc] def «inductive» := leading_parser
"inductive " >> recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >> optional (symbol " :=" <|> " where") >>
many ctor >> optional (ppDedent ppLine >> computedFields) >> optDeriving
def classInductive := leading_parser
@@ -544,7 +548,7 @@ def openSimple := leading_parser
def openScoped := leading_parser
" scoped" >> many1 (ppSpace >> checkColGt >> ident)
/-- `openDecl` is the body of an `open` declaration (see `open`) -/
def openDecl :=
@[builtin_doc] def openDecl :=
withAntiquot (mkAntiquot "openDecl" `Lean.Parser.Command.openDecl (isPseudoKind := true)) <|
openHiding <|> openRenaming <|> openOnly <|> openSimple <|> openScoped
/-- Makes names from other namespaces visible without writing the namespace prefix.

View File

@@ -30,7 +30,7 @@ def doSeqBracketed := leading_parser
do elements that take blocks. It can either have the form `"{" (doElem ";"?)* "}"` or
`many1Indent (doElem ";"?)`, where `many1Indent` ensures that all the items are at
the same or higher indentation level as the first line. -/
def doSeq :=
@[builtin_doc] def doSeq :=
withAntiquot (mkAntiquot "doSeq" decl_name% (isPseudoKind := true)) <|
doSeqBracketed <|> doSeqIndent
/-- `termBeforeDo` is defined as `withForbidden("do", term)`, which will parse a term but

View File

@@ -31,7 +31,7 @@ it to parse correctly. `ident?` will not work; one must write `(ident)?` instead
This parser has arity 1: it produces a `nullKind` node containing either zero arguments
(for the `none` case) or the list of arguments produced by `p`.
(In particular, if `p` has arity 0 then the two cases are not differentiated!) -/
@[run_builtin_parser_attribute_hooks] def optional (p : Parser) : Parser :=
@[run_builtin_parser_attribute_hooks, builtin_doc] def optional (p : Parser) : Parser :=
optionalNoAntiquot (withAntiquotSpliceAndSuffix `optional p (symbol "?"))
/-- The parser `many(p)`, or `p*`, repeats `p` until it fails, and returns the list of results.
@@ -41,7 +41,7 @@ automatically replaced by `group(p)` to ensure that it produces exactly 1 value.
This parser has arity 1: it produces a `nullKind` node containing one argument for each
invocation of `p` (or `group(p)`). -/
@[run_builtin_parser_attribute_hooks] def many (p : Parser) : Parser :=
@[run_builtin_parser_attribute_hooks, builtin_doc] def many (p : Parser) : Parser :=
manyNoAntiquot (withAntiquotSpliceAndSuffix `many p (symbol "*"))
/-- The parser `many1(p)`, or `p+`, repeats `p` until it fails, and returns the list of results.
@@ -56,7 +56,7 @@ automatically replaced by `group(p)` to ensure that it produces exactly 1 value.
This parser has arity 1: it produces a `nullKind` node containing one argument for each
invocation of `p` (or `group(p)`). -/
@[run_builtin_parser_attribute_hooks] def many1 (p : Parser) : Parser :=
@[run_builtin_parser_attribute_hooks, builtin_doc] def many1 (p : Parser) : Parser :=
many1NoAntiquot (withAntiquotSpliceAndSuffix `many p (symbol "*"))
/-- The parser `ident` parses a single identifier, possibly with namespaces, such as `foo` or
@@ -70,18 +70,18 @@ using disallowed characters in identifiers such as `«foo.bar».baz` or `«hello
This parser has arity 1: it produces a `Syntax.ident` node containing the parsed identifier.
You can use `TSyntax.getId` to extract the name from the resulting syntax object. -/
@[run_builtin_parser_attribute_hooks] def ident : Parser :=
@[run_builtin_parser_attribute_hooks, builtin_doc] def ident : Parser :=
withAntiquot (mkAntiquot "ident" identKind) identNoAntiquot
-- `optional (checkNoWsBefore >> "." >> checkNoWsBefore >> ident)`
-- can never fully succeed but ensures that the identifier
-- produces a partial syntax that contains the dot.
-- The partial syntax is sometimes useful for dot-auto-completion.
@[run_builtin_parser_attribute_hooks] def identWithPartialTrailingDot :=
@[run_builtin_parser_attribute_hooks, builtin_doc] def identWithPartialTrailingDot :=
ident >> optional (checkNoWsBefore >> "." >> checkNoWsBefore >> ident)
-- `ident` and `rawIdent` produce the same syntax tree, so we reuse the antiquotation kind name
@[run_builtin_parser_attribute_hooks] def rawIdent : Parser :=
@[run_builtin_parser_attribute_hooks, builtin_doc] def rawIdent : Parser :=
withAntiquot (mkAntiquot "ident" identKind) rawIdentNoAntiquot
/-- The parser `hygieneInfo` parses no text, but captures the current macro scope information
@@ -96,7 +96,7 @@ for more information about macro hygiene.
This parser has arity 1: it produces a `Syntax.ident` node containing the parsed identifier.
You can use `TSyntax.getHygieneInfo` to extract the name from the resulting syntax object. -/
@[run_builtin_parser_attribute_hooks] def hygieneInfo : Parser :=
@[run_builtin_parser_attribute_hooks, builtin_doc] def hygieneInfo : Parser :=
withAntiquot (mkAntiquot "hygieneInfo" hygieneInfoKind (anonymous := false)) hygieneInfoNoAntiquot
/-- The parser `num` parses a numeric literal in several bases:
@@ -109,7 +109,7 @@ You can use `TSyntax.getHygieneInfo` to extract the name from the resulting synt
This parser has arity 1: it produces a `numLitKind` node containing an atom with the text of the
literal.
You can use `TSyntax.getNat` to extract the number from the resulting syntax object. -/
@[run_builtin_parser_attribute_hooks] def numLit : Parser :=
@[run_builtin_parser_attribute_hooks, builtin_doc] def numLit : Parser :=
withAntiquot (mkAntiquot "num" numLitKind) numLitNoAntiquot
/-- The parser `scientific` parses a scientific-notation literal, such as `1.3e-24`.
@@ -117,7 +117,7 @@ You can use `TSyntax.getNat` to extract the number from the resulting syntax obj
This parser has arity 1: it produces a `scientificLitKind` node containing an atom with the text
of the literal.
You can use `TSyntax.getScientific` to extract the parts from the resulting syntax object. -/
@[run_builtin_parser_attribute_hooks] def scientificLit : Parser :=
@[run_builtin_parser_attribute_hooks, builtin_doc] def scientificLit : Parser :=
withAntiquot (mkAntiquot "scientific" scientificLitKind) scientificLitNoAntiquot
/-- The parser `str` parses a string literal, such as `"foo"` or `"\r\n"`. Strings can contain
@@ -127,7 +127,7 @@ Newlines in a string are interpreted literally.
This parser has arity 1: it produces a `strLitKind` node containing an atom with the raw
literal (including the quote marks and without interpreting the escapes).
You can use `TSyntax.getString` to decode the string from the resulting syntax object. -/
@[run_builtin_parser_attribute_hooks] def strLit : Parser :=
@[run_builtin_parser_attribute_hooks, builtin_doc] def strLit : Parser :=
withAntiquot (mkAntiquot "str" strLitKind) strLitNoAntiquot
/-- The parser `char` parses a character literal, such as `'a'` or `'\n'`. Character literals can
@@ -138,7 +138,7 @@ like `∈`, but must evaluate to a single unicode codepoint, so `'♥'` is allow
This parser has arity 1: it produces a `charLitKind` node containing an atom with the raw
literal (including the quote marks and without interpreting the escapes).
You can use `TSyntax.getChar` to decode the string from the resulting syntax object. -/
@[run_builtin_parser_attribute_hooks] def charLit : Parser :=
@[run_builtin_parser_attribute_hooks, builtin_doc] def charLit : Parser :=
withAntiquot (mkAntiquot "char" charLitKind) charLitNoAntiquot
/-- The parser `name` parses a name literal like `` `foo``. The syntax is the same as for identifiers
@@ -147,7 +147,7 @@ You can use `TSyntax.getChar` to decode the string from the resulting syntax obj
This parser has arity 1: it produces a `nameLitKind` node containing the raw literal
(including the backquote).
You can use `TSyntax.getName` to extract the name from the resulting syntax object. -/
@[run_builtin_parser_attribute_hooks] def nameLit : Parser :=
@[run_builtin_parser_attribute_hooks, builtin_doc] def nameLit : Parser :=
withAntiquot (mkAntiquot "name" nameLitKind) nameLitNoAntiquot
/-- The parser `group(p)` parses the same thing as `p`, but it wraps the results in a `groupKind`
@@ -156,7 +156,7 @@ node.
This parser always has arity 1, even if `p` does not. Parsers like `p*` are automatically
rewritten to `group(p)*` if `p` does not have arity 1, so that the results from separate invocations
of `p` can be differentiated. -/
@[run_builtin_parser_attribute_hooks, inline] def group (p : Parser) : Parser :=
@[run_builtin_parser_attribute_hooks, builtin_doc, inline] def group (p : Parser) : Parser :=
node groupKind p
/-- The parser `many1Indent(p)` is equivalent to `withPosition((colGe p)+)`. This has the effect of
@@ -165,7 +165,7 @@ the same or more than the first parse.
This parser has arity 1, and returns a list of the results from `p`.
`p` is "auto-grouped" if it is not arity 1. -/
@[run_builtin_parser_attribute_hooks, inline] def many1Indent (p : Parser) : Parser :=
@[run_builtin_parser_attribute_hooks, builtin_doc, inline] def many1Indent (p : Parser) : Parser :=
withPosition $ many1 (checkColGe "irrelevant" >> p)
/-- The parser `manyIndent(p)` is equivalent to `withPosition((colGe p)*)`. This has the effect of
@@ -174,14 +174,14 @@ the same or more than the first parse.
This parser has arity 1, and returns a list of the results from `p`.
`p` is "auto-grouped" if it is not arity 1. -/
@[run_builtin_parser_attribute_hooks, inline] def manyIndent (p : Parser) : Parser :=
@[run_builtin_parser_attribute_hooks, builtin_doc, inline] def manyIndent (p : Parser) : Parser :=
withPosition $ many (checkColGe "irrelevant" >> p)
@[inline] def sepByIndent (p : Parser) (sep : String) (psep : Parser := symbol sep) (allowTrailingSep : Bool := false) : Parser :=
@[builtin_doc, inline] def sepByIndent (p : Parser) (sep : String) (psep : Parser := symbol sep) (allowTrailingSep : Bool := false) : Parser :=
let p := withAntiquotSpliceAndSuffix `sepBy p (symbol "*")
withPosition $ sepBy (checkColGe "irrelevant" >> p) sep (psep <|> checkColEq "irrelevant" >> checkLinebreakBefore >> pushNone) allowTrailingSep
@[inline] def sepBy1Indent (p : Parser) (sep : String) (psep : Parser := symbol sep) (allowTrailingSep : Bool := false) : Parser :=
@[builtin_doc, inline] def sepBy1Indent (p : Parser) (sep : String) (psep : Parser := symbol sep) (allowTrailingSep : Bool := false) : Parser :=
let p := withAntiquotSpliceAndSuffix `sepBy p (symbol "*")
withPosition $ sepBy1 (checkColGe "irrelevant" >> p) sep (psep <|> checkColEq "irrelevant" >> checkLinebreakBefore >> pushNone) allowTrailingSep
@@ -205,32 +205,33 @@ def sepByIndent.formatter (p : Formatter) (_sep : String) (pSep : Formatter) : F
attribute [run_builtin_parser_attribute_hooks] sepByIndent sepBy1Indent
@[run_builtin_parser_attribute_hooks] abbrev notSymbol (s : String) : Parser :=
@[run_builtin_parser_attribute_hooks, builtin_doc] abbrev notSymbol (s : String) : Parser :=
notFollowedBy (symbol s) s
/-- No-op parser combinator that annotates subtrees to be ignored in syntax patterns. -/
@[inline, run_builtin_parser_attribute_hooks] def patternIgnore : Parser Parser := node `patternIgnore
@[run_builtin_parser_attribute_hooks, builtin_doc, inline]
def patternIgnore : Parser Parser := node `patternIgnore
/-- No-op parser that advises the pretty printer to emit a non-breaking space. -/
@[inline] def ppHardSpace : Parser := skip
@[builtin_doc, inline] def ppHardSpace : Parser := skip
/-- No-op parser that advises the pretty printer to emit a space/soft line break. -/
@[inline] def ppSpace : Parser := skip
@[builtin_doc, inline] def ppSpace : Parser := skip
/-- No-op parser that advises the pretty printer to emit a hard line break. -/
@[inline] def ppLine : Parser := skip
@[builtin_doc, inline] def ppLine : Parser := skip
/-- No-op parser combinator that advises the pretty printer to emit a `Format.fill` node. -/
@[inline] def ppRealFill : Parser Parser := id
@[builtin_doc, inline] def ppRealFill : Parser Parser := id
/-- No-op parser combinator that advises the pretty printer to emit a `Format.group` node. -/
@[inline] def ppRealGroup : Parser Parser := id
@[builtin_doc, inline] def ppRealGroup : Parser Parser := id
/-- No-op parser combinator that advises the pretty printer to indent the given syntax without grouping it. -/
@[inline] def ppIndent : Parser Parser := id
@[builtin_doc, inline] def ppIndent : Parser Parser := id
/--
No-op parser combinator that advises the pretty printer to group and indent the given syntax.
By default, only syntax categories are grouped. -/
@[inline] def ppGroup (p : Parser) : Parser := ppRealFill (ppIndent p)
@[builtin_doc, inline] def ppGroup (p : Parser) : Parser := ppRealFill (ppIndent p)
/--
No-op parser combinator that advises the pretty printer to dedent the given syntax.
Dedenting can in particular be used to counteract automatic indentation. -/
@[inline] def ppDedent : Parser Parser := id
@[builtin_doc, inline] def ppDedent : Parser Parser := id
/--
No-op parser combinator that allows the pretty printer to omit the group and
@@ -242,19 +243,19 @@ attribute [run_builtin_parser_attribute_hooks] sepByIndent sepBy1Indent
trivial
```
-/
@[inline] def ppAllowUngrouped : Parser := skip
@[builtin_doc, inline] def ppAllowUngrouped : Parser := skip
/--
No-op parser combinator that advises the pretty printer to dedent the given syntax,
if it was grouped by the category parser.
Dedenting can in particular be used to counteract automatic indentation. -/
@[inline] def ppDedentIfGrouped : Parser Parser := id
@[builtin_doc, inline] def ppDedentIfGrouped : Parser Parser := id
/--
No-op parser combinator that prints a line break.
The line break is soft if the combinator is followed
by an ungrouped parser (see ppAllowUngrouped), otherwise hard. -/
@[inline] def ppHardLineUnlessUngrouped : Parser := skip
@[builtin_doc, inline] def ppHardLineUnlessUngrouped : Parser := skip
end Parser

View File

@@ -68,7 +68,7 @@ This parser has arity 1, and returns a `interpolatedStrKind` with an odd number
alternating between chunks of literal text and results from `p`. The literal chunks contain
uninterpreted substrings of the input. For example, `"foo\n{2 + 2}"` would have three arguments:
an atom `"foo\n{`, the parsed `2 + 2` term, and then the atom `}"`. -/
def interpolatedStr (p : Parser) : Parser :=
@[builtin_doc] def interpolatedStr (p : Parser) : Parser :=
withAntiquot (mkAntiquot "interpolatedStr" interpolatedStrKind) $ interpolatedStrNoAntiquot p
end Lean.Parser

View File

@@ -24,6 +24,7 @@ a regular comment (that is, as whitespace); it is parsed and forms part of the s
A `docComment` node contains a `/--` atom and then the remainder of the comment, `foo -/` in this
example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node. -/
-- @[builtin_doc] -- FIXME: suppress the hover
def docComment := leading_parser
ppDedent $ "/--" >> ppSpace >> commentBody >> ppLine
end Command
@@ -49,7 +50,7 @@ example := by
skip
```
is legal, but `by skip skip` is not - it must be written as `by skip; skip`. -/
@[run_builtin_parser_attribute_hooks]
@[run_builtin_parser_attribute_hooks, builtin_doc]
def sepByIndentSemicolon (p : Parser) : Parser :=
sepByIndent p "; " (allowTrailingSep := true)
@@ -62,7 +63,7 @@ example := by
skip
```
is legal, but `by skip skip` is not - it must be written as `by skip; skip`. -/
@[run_builtin_parser_attribute_hooks]
@[run_builtin_parser_attribute_hooks, builtin_doc]
def sepBy1IndentSemicolon (p : Parser) : Parser :=
sepBy1Indent p "; " (allowTrailingSep := true)
@@ -70,22 +71,22 @@ builtin_initialize
register_parser_alias sepByIndentSemicolon
register_parser_alias sepBy1IndentSemicolon
def tacticSeq1Indented : Parser := leading_parser
@[builtin_doc] def tacticSeq1Indented : Parser := leading_parser
sepBy1IndentSemicolon tacticParser
/-- The syntax `{ tacs }` is an alternative syntax for `· tacs`.
It runs the tactics in sequence, and fails if the goal is not solved. -/
def tacticSeqBracketed : Parser := leading_parser
@[builtin_doc] def tacticSeqBracketed : Parser := leading_parser
"{" >> sepByIndentSemicolon tacticParser >> ppDedent (ppLine >> "}")
/-- A sequence of tactics in brackets, or a delimiter-free indented sequence of tactics.
Delimiter-free indentation is determined by the *first* tactic of the sequence. -/
def tacticSeq := leading_parser
@[builtin_doc] def tacticSeq := leading_parser
tacticSeqBracketed <|> tacticSeq1Indented
/-- Same as [`tacticSeq`] but requires delimiter-free tactic sequence to have strict indentation.
The strict indentation requirement only apply to *nested* `by`s, as top-level `by`s do not have a
position set. -/
def tacticSeqIndentGt := withAntiquot (mkAntiquot "tacticSeq" ``tacticSeq) <| node ``tacticSeq <|
@[builtin_doc] def tacticSeqIndentGt := withAntiquot (mkAntiquot "tacticSeq" ``tacticSeq) <| node ``tacticSeq <|
tacticSeqBracketed <|> (checkColGt "indented tactic sequence" >> tacticSeq1Indented)
/- Raw sequence for quotation and grouping -/
@@ -206,7 +207,7 @@ def fromTerm := leading_parser
def showRhs := fromTerm <|> byTactic'
/-- A `sufficesDecl` represents everything that comes after the `suffices` keyword:
an optional `x :`, then a term `ty`, then `from val` or `by tac`. -/
def sufficesDecl := leading_parser
@[builtin_doc] def sufficesDecl := leading_parser
(atomic (group (binderIdent >> " : ")) <|> hygieneInfo) >> termParser >> ppSpace >> showRhs
@[builtin_term_parser] def «suffices» := leading_parser:leadPrec
withPosition ("suffices " >> sufficesDecl) >> optSemicolon termParser
@@ -272,7 +273,7 @@ open Lean.PrettyPrinter Parenthesizer Syntax.MonadTraverser in
Explicit binder, like `(x y : A)` or `(x y)`.
Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.
-/
def explicitBinder (requireType := false) := leading_parser ppGroup <|
@[builtin_doc] def explicitBinder (requireType := false) := leading_parser ppGroup <|
"(" >> withoutPosition (many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault)) >> ")"
/--
Implicit binder, like `{x y : A}` or `{x y}`.
@@ -283,7 +284,7 @@ by unification.
In `@` explicit mode, implicit binders behave like explicit binders.
-/
def implicitBinder (requireType := false) := leading_parser ppGroup <|
@[builtin_doc] def implicitBinder (requireType := false) := leading_parser ppGroup <|
"{" >> withoutPosition (many1 binderIdent >> binderType requireType) >> "}"
def strictImplicitLeftBracket := atomic (group (symbol "{" >> "{")) <|> ""
def strictImplicitRightBracket := atomic (group (symbol "}" >> "}")) <|> ""
@@ -300,7 +301,7 @@ and `h hs` has type `p y`.
In contrast, if `h' : ∀ {x : A}, x ∈ s → p x`, then `h` by itself elaborates to have type `?m ∈ s → p ?m`
with `?m` a fresh metavariable.
-/
def strictImplicitBinder (requireType := false) := leading_parser ppGroup <|
@[builtin_doc] def strictImplicitBinder (requireType := false) := leading_parser ppGroup <|
strictImplicitLeftBracket >> many1 binderIdent >>
binderType requireType >> strictImplicitRightBracket
/--
@@ -310,7 +311,7 @@ and solved for by typeclass inference for the specified class `C`.
In `@` explicit mode, if `_` is used for an an instance-implicit parameter, then it is still solved for by typeclass inference;
use `(_)` to inhibit this and have it be solved for by unification instead, like an implicit argument.
-/
def instBinder := leading_parser ppGroup <|
@[builtin_doc] def instBinder := leading_parser ppGroup <|
"[" >> withoutPosition (optIdent >> termParser) >> "]"
/-- A `bracketedBinder` matches any kind of binder group that uses some kind of brackets:
* An explicit binder like `(x y : A)`
@@ -318,7 +319,7 @@ def instBinder := leading_parser ppGroup <|
* A strict implicit binder, `⦃y z : A⦄` or its ASCII alternative `{{y z : A}}`
* An instance binder `[A]` or `[x : A]` (multiple variables are not allowed here)
-/
def bracketedBinder (requireType := false) :=
@[builtin_doc] def bracketedBinder (requireType := false) :=
withAntiquot (mkAntiquot "bracketedBinder" decl_name% (isPseudoKind := true)) <|
explicitBinder requireType <|> strictImplicitBinder requireType <|>
implicitBinder requireType <|> instBinder
@@ -366,7 +367,7 @@ def matchAlts (rhsParser : Parser := termParser) : Parser :=
/-- `matchDiscr` matches a "match discriminant", either `h : tm` or `tm`, used in `match` as
`match h1 : e1, e2, h3 : e3 with ...`. -/
def matchDiscr := leading_parser
@[builtin_doc] def matchDiscr := leading_parser
optional (atomic (ident >> " : ")) >> termParser
def trueVal := leading_parser nonReservedSymbol "true"
@@ -497,7 +498,7 @@ def letEqnsDecl := leading_parser (withAnonymousAntiquot := false)
`let pat := e` (where `pat` is an arbitrary term) or `let f | pat1 => e1 | pat2 => e2 ...`
(a pattern matching declaration), except for the `let` keyword itself.
`let rec` declarations are not handled here. -/
def letDecl := leading_parser (withAnonymousAntiquot := false)
@[builtin_doc] def letDecl := leading_parser (withAnonymousAntiquot := false)
-- Remark: we disable anonymous antiquotations here to make sure
-- anonymous antiquotations (e.g., `$x`) are not `letDecl`
notFollowedBy (nonReservedSymbol "rec") "rec" >>
@@ -556,7 +557,7 @@ def haveEqnsDecl := leading_parser (withAnonymousAntiquot := false)
/-- `haveDecl` matches the body of a have declaration: `have := e`, `have f x1 x2 := e`,
`have pat := e` (where `pat` is an arbitrary term) or `have f | pat1 => e1 | pat2 => e2 ...`
(a pattern matching declaration), except for the `have` keyword itself. -/
def haveDecl := leading_parser (withAnonymousAntiquot := false)
@[builtin_doc] def haveDecl := leading_parser (withAnonymousAntiquot := false)
haveIdDecl <|> (ppSpace >> letPatDecl) <|> haveEqnsDecl
@[builtin_term_parser] def «have» := leading_parser:leadPrec
withPosition ("have" >> haveDecl) >> optSemicolon termParser
@@ -570,7 +571,7 @@ def haveDecl := leading_parser (withAnonymousAntiquot := false)
def «scoped» := leading_parser "scoped "
def «local» := leading_parser "local "
/-- `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. -/
def attrKind := leading_parser optional («scoped» <|> «local»)
@[builtin_doc] def attrKind := leading_parser optional («scoped» <|> «local»)
def attrInstance := ppGroup $ leading_parser attrKind >> attrParser
def attributes := leading_parser
@@ -607,13 +608,13 @@ If omitted, a termination argument will be inferred. If written as `termination_
the inferrred termination argument will be suggested.
-/
def terminationBy := leading_parser
@[builtin_doc] def terminationBy := leading_parser
"termination_by " >>
optional (nonReservedSymbol "structural ") >>
optional (atomic (many (ppSpace >> Term.binderIdent) >> " => ")) >>
termParser
@[inherit_doc terminationBy]
@[inherit_doc terminationBy, builtin_doc]
def terminationBy? := leading_parser
"termination_by?"
@@ -626,13 +627,13 @@ By default, the tactic `decreasing_tactic` is used.
Forces the use of well-founded recursion and is hence incompatible with
`termination_by structural`.
-/
def decreasingBy := leading_parser
@[builtin_doc] def decreasingBy := leading_parser
ppDedent ppLine >> "decreasing_by " >> Tactic.tacticSeqIndentGt
/--
Termination hints are `termination_by` and `decreasing_by`, in that order.
-/
def suffix := leading_parser
@[builtin_doc] def suffix := leading_parser
optional (ppDedent ppLine >> (terminationBy? <|> terminationBy)) >> optional decreasingBy
end Termination
@@ -640,9 +641,10 @@ namespace Term
/-- `letRecDecl` matches the body of a let-rec declaration: a doc comment, attributes, and then
a let declaration without the `let` keyword, such as `/-- foo -/ @[simp] bar := 1`. -/
def letRecDecl := leading_parser
@[builtin_doc] def letRecDecl := leading_parser
optional Command.docComment >> optional «attributes» >> letDecl >> Termination.suffix
/-- `letRecDecls` matches `letRecDecl,+`, a comma-separated list of let-rec declarations (see `letRecDecl`). -/
-- @[builtin_doc] -- FIXME: suppress the hover
def letRecDecls := leading_parser
sepBy1 letRecDecl ", "
@[builtin_term_parser]

View File

@@ -7,6 +7,7 @@ prelude
import Lean.Data.Trie
import Lean.Syntax
import Lean.Message
import Lean.DocString.Extension
namespace Lean.Parser
@@ -428,7 +429,7 @@ def withCacheFn (parserName : Name) (p : ParserFn) : ParserFn := fun c s => Id.r
panic! s!"withCacheFn: unexpected stack growth {s.stxStack.raw}"
{ s with cache.parserCache := s.cache.parserCache.insert key s.stxStack.back, s.lhsPrec, s.pos, s.errorMsg }
@[inherit_doc withCacheFn]
@[inherit_doc withCacheFn, builtin_doc]
def withCache (parserName : Name) : Parser Parser := withFn (withCacheFn parserName)
def ParserFn.run (p : ParserFn) (ictx : InputContext) (pmctx : ParserModuleContext) (tokens : TokenTable) (s : ParserState) : ParserState :=

View File

@@ -666,6 +666,50 @@ private def tacticCompletion (params : CompletionParams) (ctx : ContextInfo) : I
}, 1)
return some { items := sortCompletionItems items, isIncomplete := true }
/--
If there are `Info`s that contain `hoverPos` and have a nonempty `LocalContext`,
yields the closest one of those `Info`s.
Otherwise, yields the closest `Info` that contains `hoverPos` and has an empty `LocalContext`.
-/
private def findClosestInfoWithLocalContextAt?
(hoverPos : String.Pos)
(infoTree : InfoTree)
: Option (ContextInfo × Info) :=
infoTree.visitM (m := Id) (postNode := choose) |>.join
where
choose
(ctx : ContextInfo)
(info : Info)
(_ : PersistentArray InfoTree)
(childValues : List (Option (Option (ContextInfo × Info))))
: Option (ContextInfo × Info) :=
let bestChildValue := childValues.map (·.join) |>.foldl (init := none) fun v best =>
if isBetter v best then
v
else
best
if info.occursInOrOnBoundary hoverPos && isBetter (ctx, info) bestChildValue then
(ctx, info)
else
bestChildValue
isBetter (a b : Option (ContextInfo × Info)) : Bool :=
match a, b with
| none, none => false
| some _, none => true
| none, some _ => false
| some (_, ia), some (_, ib) =>
if !ia.lctx.isEmpty && ib.lctx.isEmpty then
true
else if ia.lctx.isEmpty && !ib.lctx.isEmpty then
false
else if ia.isSmaller ib then
true
else if ib.isSmaller ia then
false
else
false
private def findCompletionInfoAt?
(fileMap : FileMap)
(hoverPos : String.Pos)
@@ -675,9 +719,32 @@ private def findCompletionInfoAt?
match infoTree.foldInfo (init := none) (choose hoverLine) with
| some (hoverInfo, ctx, Info.ofCompletionInfo info) =>
some (hoverInfo, ctx, info)
| _ =>
-- TODO try to extract id from `fileMap` and some `ContextInfo` from `InfoTree`
none
| _ => do
-- No completion info => Attempt providing identifier completions
let some (ctx, info) := findClosestInfoWithLocalContextAt? hoverPos infoTree
| none
let some stack := info.stx.findStack? (·.getRange?.any (·.contains hoverPos (includeStop := true)))
| none
let stack := stack.dropWhile fun (stx, _) => !(stx matches `($_:ident) || stx matches `($_:ident.))
let some (stx, _) := stack.head?
| none
let isDotIdCompletion := stack.any fun (stx, _) => stx matches `(.$_:ident)
if isDotIdCompletion then
-- An identifier completion is never useful in a dotId completion context.
none
let some (id, danglingDot) :=
match stx with
| `($id:ident) => some (id.getId, false)
| `($id:ident.) => some (id.getId, true)
| _ => none
| none
let tailPos := stx.getTailPos?.get!
let hoverInfo :=
if hoverPos < tailPos then
HoverInfo.inside (tailPos - hoverPos).byteIdx
else
HoverInfo.after
some (hoverInfo, ctx, .id stx id danglingDot info.lctx none)
where
choose
(hoverLine : Nat)

View File

@@ -141,10 +141,12 @@ def Info.stx : Info → Syntax
| ofOmissionInfo i => i.stx
def Info.lctx : Info LocalContext
| Info.ofTermInfo i => i.lctx
| Info.ofFieldInfo i => i.lctx
| Info.ofOmissionInfo i => i.lctx
| _ => LocalContext.empty
| .ofTermInfo i => i.lctx
| .ofFieldInfo i => i.lctx
| .ofOmissionInfo i => i.lctx
| .ofMacroExpansionInfo i => i.lctx
| .ofCompletionInfo i => i.lctx
| _ => LocalContext.empty
def Info.pos? (i : Info) : Option String.Pos :=
i.stx.getPos? (canonicalOnly := true)

View File

@@ -152,6 +152,18 @@ variable {β : Type v}
end
@[inline, inherit_doc Raw.getKey?] def getKey? (m : DHashMap α β) (a : α) : Option α :=
Raw₀.getKey? m.1, m.2.size_buckets_pos a
@[inline, inherit_doc Raw.getKey] def getKey (m : DHashMap α β) (a : α) (h : a m) : α :=
Raw₀.getKey m.1, m.2.size_buckets_pos a h
@[inline, inherit_doc Raw.getKey!] def getKey! [Inhabited α] (m : DHashMap α β) (a : α) : α :=
Raw₀.getKey! m.1, m.2.size_buckets_pos a
@[inline, inherit_doc Raw.getKeyD] def getKeyD (m : DHashMap α β) (a : α) (fallback : α) : α :=
Raw₀.getKeyD m.1, m.2.size_buckets_pos a fallback
@[inline, inherit_doc Raw.size] def size (m : DHashMap α β) : Nat :=
m.1.size

View File

@@ -102,16 +102,31 @@ def getCast [BEq α] [LawfulBEq α] (a : α) : (l : AssocList α β) → l.conta
| cons k v es, h => if hka : k == a then cast (congrArg β (eq_of_beq hka)) v
else es.getCast a (by rw [ h, contains, Bool.of_not_eq_true hka, Bool.false_or])
/-- Internal implementation detail of the hash map -/
def getKey [BEq α] (a : α) : (l : AssocList α β) l.contains a α
| cons k _ es, h => if hka : k == a then k
else es.getKey a (by rw [ h, contains, Bool.of_not_eq_true hka, Bool.false_or])
/-- Internal implementation detail of the hash map -/
def getCast! [BEq α] [LawfulBEq α] (a : α) [Inhabited (β a)] : AssocList α β β a
| nil => panic! "key is not present in hash table"
| cons k v es => if h : k == a then cast (congrArg β (eq_of_beq h)) v else es.getCast! a
/-- Internal implementation detail of the hash map -/
def getKey? [BEq α] (a : α) : AssocList α β Option α
| nil => none
| cons k _ es => if k == a then some k else es.getKey? a
/-- Internal implementation detail of the hash map -/
def get! {β : Type v} [BEq α] [Inhabited β] (a : α) : AssocList α (fun _ => β) β
| nil => panic! "key is not present in hash table"
| cons k v es => bif k == a then v else es.get! a
/-- Internal implementation detail of the hash map -/
def getKey! [BEq α] [Inhabited α] (a : α) : AssocList α β α
| nil => panic! "key is not present in hash table"
| cons k _ es => if k == a then k else es.getKey! a
/-- Internal implementation detail of the hash map -/
def getCastD [BEq α] [LawfulBEq α] (a : α) (fallback : β a) : AssocList α β β a
| nil => fallback
@@ -123,6 +138,11 @@ def getD {β : Type v} [BEq α] (a : α) (fallback : β) : AssocList α (fun _ =
| nil => fallback
| cons k v es => bif k == a then v else es.getD a fallback
/-- Internal implementation detail of the hash map -/
def getKeyD [BEq α] (a : α) (fallback : α) : AssocList α β α
| nil => fallback
| cons k _ es => if k == a then k else es.getKeyD a fallback
/-- Internal implementation detail of the hash map -/
def replace [BEq α] (a : α) (b : β a) : AssocList α β AssocList α β
| nil => nil

View File

@@ -112,6 +112,32 @@ theorem get!_eq {β : Type v} [BEq α] [Inhabited β] {l : AssocList α (fun _ =
· simp_all [get!, List.getValue!, List.getValue!, List.getValue?_cons,
Bool.apply_cond Option.get!]
@[simp]
theorem getKey?_eq [BEq α] {l : AssocList α β} {a : α} :
l.getKey? a = List.getKey? a l.toList := by
induction l <;> simp_all [getKey?]
@[simp]
theorem getKey_eq [BEq α] {l : AssocList α β} {a : α} {h} :
l.getKey a h = List.getKey a l.toList (contains_eq.symm.trans h) := by
induction l
· simp [contains] at h
· next k v t ih => simp only [getKey, toList_cons, List.getKey_cons, ih]
@[simp]
theorem getKeyD_eq [BEq α] {l : AssocList α β} {a fallback : α} :
l.getKeyD a fallback = List.getKeyD a l.toList fallback := by
induction l
· simp [getKeyD, List.getKeyD]
· simp_all [getKeyD, List.getKeyD, Bool.apply_cond (fun x => Option.getD x fallback)]
@[simp]
theorem getKey!_eq [BEq α] [Inhabited α] {l : AssocList α β} {a : α} :
l.getKey! a = List.getKey! a l.toList := by
induction l
· simp [getKey!, List.getKey!]
· simp_all [getKey!, List.getKey!, Bool.apply_cond Option.get!]
@[simp]
theorem toList_replace [BEq α] {l : AssocList α β} {a : α} {b : β a} :
(l.replace a b).toList = replaceEntry a b l.toList := by

View File

@@ -100,9 +100,9 @@ Here is a summary of the steps required to add and verify a new operation:
* Connect the implementation on lists and associative lists in `Internal.AssocList.Lemmas` via a
lemma `AssocList.operation_eq`.
3. Write the model implementation
* Write the model implementation `Raw₀.operationₘ` in `Internal.List.Model`
* Write the model implementation `Raw₀.operationₘ` in `Internal.Model`
* Prove that the model implementation is equal to the actual implementation in
`Internal.List.Model` via a lemma `operation_eq_operationₘ`.
`Internal.Model` via a lemma `operation_eq_operationₘ`.
4. Verify the model implementation
* In `Internal.WF`, prove `operationₘ_eq_List.operation` (for access operations) or
`wfImp_operationₘ` and `toListModel_operationₘ`
@@ -121,18 +121,18 @@ Here is a summary of the steps required to add and verify a new operation:
might also have to prove that your list operation is invariant under permutation and add that to
the tactic.
7. State and prove the user-facing lemmas
* Restate all of your lemmas for `DHashMap.Raw` in `DHashMap.Lemmas` and prove them using the
* Restate all of your lemmas for `DHashMap.Raw` in `DHashMap.RawLemmas` and prove them using the
provided tactic after hooking in your `operation_eq` and `operation_val` from step 5.
* Restate all of your lemmas for `DHashMap` in `DHashMap.Lemmas` and prove them by reducing to
`Raw₀`.
* Restate all of your lemmas for `HashMap.Raw` in `HashMap.Lemmas` and prove them by reducing to
* Restate all of your lemmas for `HashMap.Raw` in `HashMap.RawLemmas` and prove them by reducing to
`DHashMap.Raw`.
* Restate all of your lemmas for `HashMap` in `HashMap.Lemmas` and prove them by reducing to
`DHashMap`.
* Restate all of your lemmas for `HashSet.Raw` in `HashSet.Lemmas` and prove them by reducing to
`DHashSet.Raw`.
* Restate all of your lemmas for `HashSet.Raw` in `HashSet.RawLemmas` and prove them by reducing to
`HashMap.Raw`.
* Restate all of your lemmas for `HashSet` in `HashSet.Lemmas` and prove them by reducing to
`DHashSet`.
`HashMap`.
This sounds like a lot of work (and it is if you have to add a lot of user-facing lemmas), but the
framework is set up in such a way that each step is really easy and the proofs are all really short
@@ -420,6 +420,30 @@ variable {β : Type v}
end
/-- Internal implementation detail of the hash map -/
@[inline] def getKey? [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) : Option α :=
let _, buckets, h := m
let i, h := mkIdx buckets.size h (hash a)
buckets[i].getKey? a
/-- Internal implementation detail of the hash map -/
@[inline] def getKey [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (hma : m.contains a) : α :=
let _, buckets, h := m
let idx := mkIdx buckets.size h (hash a)
buckets[idx.1].getKey a hma
/-- Internal implementation detail of the hash map -/
@[inline] def getKeyD [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (fallback : α) : α :=
let _, buckets, h := m
let idx := mkIdx buckets.size h (hash a)
buckets[idx.1].getKeyD a fallback
/-- Internal implementation detail of the hash map -/
@[inline] def getKey! [BEq α] [Hashable α] [Inhabited α] (m : Raw₀ α β) (a : α) : α :=
let _, buckets, h := m
let idx := mkIdx buckets.size h (hash a)
buckets[idx.1].getKey! a
end Raw₀
/-- Internal implementation detail of the hash map -/

View File

@@ -526,6 +526,111 @@ theorem getValue!_eq_getValueD_default [BEq α] [Inhabited β] {l : List ((_ :
end
/-- Internal implementation detail of the hash map -/
def getKey? [BEq α] (a : α) : List ((a : α) × β a) Option α
| [] => none
| k, _ :: l => bif k == a then some k else getKey? a l
@[simp] theorem getKey?_nil [BEq α] {a : α} :
getKey? a ([] : List ((a : α) × β a)) = none := rfl
@[simp] theorem getKey?_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
getKey? a (k, v :: l) = bif k == a then some k else getKey? a l := rfl
theorem getKey?_cons_of_true [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : k == a) :
getKey? a (k, v :: l) = some k := by
simp [h]
theorem getKey?_cons_of_false [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
(h : (k == a) = false) : getKey? a (k, v :: l) = getKey? a l := by
simp [h]
theorem getKey?_eq_getEntry? [BEq α] {l : List ((a : α) × β a)} {a : α} :
getKey? a l = (getEntry? a l).map (·.1) := by
induction l using assoc_induction
· simp
· next k v l ih =>
cases h : k == a
· rw [getEntry?_cons_of_false h, getKey?_cons_of_false h, ih]
· rw [getEntry?_cons_of_true h, getKey?_cons_of_true h, Option.map_some']
theorem containsKey_eq_isSome_getKey? [BEq α] {l : List ((a : α) × β a)} {a : α} :
containsKey a l = (getKey? a l).isSome := by
simp [containsKey_eq_isSome_getEntry?, getKey?_eq_getEntry?]
/-- Internal implementation detail of the hash map -/
def getKey [BEq α] (a : α) (l : List ((a : α) × β a)) (h : containsKey a l) : α :=
(getKey? a l).get <| containsKey_eq_isSome_getKey?.symm.trans h
theorem getKey?_eq_some_getKey [BEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l) :
getKey? a l = some (getKey a l h) := by
simp [getKey]
theorem getKey_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} {h} :
getKey a (k, v :: l) h = if h' : k == a then k
else getKey a l (containsKey_of_containsKey_cons (k := k) h (Bool.eq_false_iff.2 h')) := by
rw [ Option.some_inj, getKey?_eq_some_getKey, getKey?_cons, apply_dite Option.some,
cond_eq_if]
split
· rfl
· exact getKey?_eq_some_getKey _
/-- Internal implementation detail of the hash map -/
def getKeyD [BEq α] (a : α) (l : List ((a : α) × β a)) (fallback : α) : α :=
(getKey? a l).getD fallback
@[simp]
theorem getKeyD_nil [BEq α] {a fallback : α} :
getKeyD a ([] : List ((a : α) × β a)) fallback = fallback := rfl
theorem getKeyD_eq_getKey? [BEq α] {l : List ((a : α) × β a)} {a fallback : α} :
getKeyD a l fallback = (getKey? a l).getD fallback := rfl
theorem getKeyD_eq_fallback [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a fallback : α}
(h : containsKey a l = false) : getKeyD a l fallback = fallback := by
rw [containsKey_eq_isSome_getKey?, Bool.eq_false_iff, ne_eq,
Option.not_isSome_iff_eq_none] at h
rw [getKeyD_eq_getKey?, h, Option.getD_none]
theorem getKey_eq_getKeyD [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a fallback : α}
(h : containsKey a l = true) :
getKey a l h = getKeyD a l fallback := by
rw [getKeyD_eq_getKey?, getKey, Option.get_eq_getD]
theorem getKey?_eq_some_getKeyD [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a fallback : α}
(h : containsKey a l = true) :
getKey? a l = some (getKeyD a l fallback) := by
rw [getKey?_eq_some_getKey h, getKey_eq_getKeyD]
/-- Internal implementation detail of the hash map -/
def getKey! [BEq α] [Inhabited α] (a : α) (l : List ((a : α) × β a)) : α :=
(getKey? a l).get!
@[simp]
theorem getKey!_nil [BEq α] [Inhabited α] {a : α} :
getKey! a ([] : List ((a : α) × β a)) = default := rfl
theorem getKey!_eq_getKey? [BEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α} :
getKey! a l = (getKey? a l).get! := rfl
theorem getKey!_eq_default [BEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α}
(h : containsKey a l = false) : getKey! a l = default := by
rw [containsKey_eq_isSome_getKey?, Bool.eq_false_iff, ne_eq,
Option.not_isSome_iff_eq_none] at h
rw [getKey!_eq_getKey?, h, Option.get!_none]
theorem getKey_eq_getKey! [BEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α}
(h : containsKey a l = true) : getKey a l h = getKey! a l := by
rw [getKey!_eq_getKey?, getKey, Option.get_eq_get!]
theorem getKey?_eq_some_getKey! [BEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α}
(h : containsKey a l = true) :
getKey? a l = some (getKey! a l) := by
rw [getKey?_eq_some_getKey h, getKey_eq_getKey!]
theorem getKey!_eq_getKeyD_default [BEq α] [EquivBEq α] [Inhabited α] {l : List ((a : α) × β a)}
{a : α} : getKey! a l = getKeyD a l default := rfl
/-- Internal implementation detail of the hash map -/
def replaceEntry [BEq α] (k : α) (v : β k) : List ((a : α) × β a) List ((a : α) × β a)
| [] => []
@@ -643,6 +748,18 @@ theorem getValueCast?_replaceEntry [BEq α] [LawfulBEq α] {l : List ((a : α)
· rw [Option.dmap_congr (getEntry?_replaceEntry_of_false (Bool.eq_false_iff.2 h)),
getValueCast?_eq_getEntry?]
theorem getKey?_replaceEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α}
{v : β k} : getKey? a (replaceEntry k v l) =
if containsKey k l k == a then some k else getKey? a l := by
rw [getKey?_eq_getEntry?]
split
· next h => simp [getEntry?_replaceEntry_of_true h.1 h.2]
· next h =>
simp only [Decidable.not_and_iff_or_not_not] at h
rcases h with h|h
· rw [getEntry?_replaceEntry_of_containsKey_eq_false (Bool.eq_false_iff.2 h), getKey?_eq_getEntry?]
· rw [getEntry?_replaceEntry_of_false (Bool.eq_false_iff.2 h), getKey?_eq_getEntry?]
@[simp]
theorem containsKey_replaceEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α}
{v : β k} : containsKey a (replaceEntry k v l) = containsKey a l := by
@@ -974,6 +1091,39 @@ theorem getValueD_insertEntry_self {β : Type v} [BEq α] [EquivBEq α] {l : Lis
{k : α} {fallback v : β} : getValueD k (insertEntry k v l) fallback = v := by
simp [getValueD_insertEntry, BEq.refl]
theorem getKey?_insertEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
{v : β k} : getKey? a (insertEntry k v l) = if k == a then some k else getKey? a l := by
cases hl : containsKey k l
· simp [insertEntry_of_containsKey_eq_false hl]
· rw [insertEntry_of_containsKey hl, getKey?_replaceEntry, hl]
split <;> simp_all
theorem getKey?_insertEntry_self [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α}
{v : β k} : getKey? k (insertEntry k v l) = some k := by
simp [getKey?_insertEntry]
theorem getKey?_eq_none [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α}
(h : containsKey a l = false) : getKey? a l = none := by
rwa [ Option.not_isSome_iff_eq_none, containsKey_eq_isSome_getKey?, Bool.not_eq_true]
theorem getKey!_insertEntry [BEq α] [EquivBEq α] [Inhabited α] {l : List ((a : α) × β a)}
{k a : α} {v : β k} : getKey! a (insertEntry k v l) =
if k == a then k else getKey! a l := by
simp [getKey!_eq_getKey?, getKey?_insertEntry, apply_ite Option.get!]
theorem getKey!_insertEntry_self [BEq α] [EquivBEq α] [Inhabited α] {l : List ((a : α) × β a)}
{k : α} {v : β k} : getKey! k (insertEntry k v l) = k := by
rw [getKey!_insertEntry, if_pos BEq.refl]
theorem getKeyD_insertEntry [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k a fallback : α}
{v : β k} : getKeyD a (insertEntry k v l) fallback =
if k == a then k else getKeyD a l fallback := by
simp [getKeyD_eq_getKey?, getKey?_insertEntry, apply_ite (fun x => Option.getD x fallback)]
theorem getKeyD_insertEntry_self [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k fallback : α}
{v : β k} : getKeyD k (insertEntry k v l) fallback = k := by
rw [getKeyD_insertEntry, if_pos BEq.refl]
@[local simp]
theorem containsKey_insertEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
{v : β k} : containsKey a (insertEntry k v l) = ((k == a) || containsKey a l) := by
@@ -1017,6 +1167,17 @@ theorem getValue_insertEntry_self {β : Type v} [BEq α] [EquivBEq α] {l : List
{v : β} : getValue k (insertEntry k v l) containsKey_insertEntry_self = v := by
simp [getValue_insertEntry]
theorem getKey_insertEntry [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k a : α}
{v : β k} {h} : getKey a (insertEntry k v l) h =
if h' : k == a then k
else getKey a l (containsKey_of_containsKey_insertEntry h (Bool.eq_false_iff.2 h')) := by
rw [ Option.some_inj, getKey?_eq_some_getKey, apply_dite Option.some, getKey?_insertEntry]
simp only [ getKey?_eq_some_getKey, dite_eq_ite]
theorem getKey_insertEntry_self [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α}
{v : β k} : getKey k (insertEntry k v l) containsKey_insertEntry_self = k := by
simp [getKey_insertEntry]
/-- Internal implementation detail of the hash map -/
def insertEntryIfNew [BEq α] (k : α) (v : β k) (l : List ((a : α) × β a)) : List ((a : α) × β a) :=
bif containsKey k l then l else k, v :: l
@@ -1135,6 +1296,32 @@ theorem getValueD_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] {
simp [getValueD_eq_getValue?, getValue?_insertEntryIfNew,
apply_ite (fun x => Option.getD x fallback)]
theorem getKey?_insertEntryIfNew [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
{v : β k} : getKey? a (insertEntryIfNew k v l) =
if k == a containsKey k l = false then some k else getKey? a l := by
cases h : containsKey k l
· rw [insertEntryIfNew_of_containsKey_eq_false h]
split <;> simp_all
· simp [insertEntryIfNew_of_containsKey h]
theorem getKey_insertEntryIfNew [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
{k a : α} {v : β k} {h} : getKey a (insertEntryIfNew k v l) h =
if h' : k == a containsKey k l = false then k
else getKey a l (containsKey_of_containsKey_insertEntryIfNew' h h') := by
rw [ Option.some_inj, getKey?_eq_some_getKey, apply_dite Option.some,
getKey?_insertEntryIfNew, dite_eq_ite]
simp [ getKey?_eq_some_getKey]
theorem getKey!_insertEntryIfNew [BEq α] [PartialEquivBEq α] [Inhabited α]
{l : List ((a : α) × β a)} {k a : α} {v : β k} : getKey! a (insertEntryIfNew k v l) =
if k == a containsKey k l = false then k else getKey! a l := by
simp [getKey!_eq_getKey?, getKey?_insertEntryIfNew, apply_ite Option.get!]
theorem getKeyD_insertEntryIfNew [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
{k a fallback : α} {v : β k} : getKeyD a (insertEntryIfNew k v l) fallback =
if k == a containsKey k l = false then k else getKeyD a l fallback := by
simp [getKeyD_eq_getKey?, getKey?_insertEntryIfNew, apply_ite (fun x => Option.getD x fallback)]
theorem length_insertEntryIfNew [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
(insertEntryIfNew k v l).length = if containsKey k l then l.length else l.length + 1 := by
simp [insertEntryIfNew, Bool.apply_cond List.length]
@@ -1253,6 +1440,36 @@ theorem getValue?_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((_ : α) ×
end
theorem getKey?_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
(hl : DistinctKeys l) :
getKey? a (eraseKey k l) = if k == a then none else getKey? a l := by
rw [getKey?_eq_getEntry?, getEntry?_eraseKey hl]
by_cases h : k == a
. simp [h]
. simp [h, getKey?_eq_getEntry?]
theorem getKey?_eraseKey_self [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α}
(hl : DistinctKeys l) : getKey? k (eraseKey k l) = none := by
simp [getKey?_eq_getEntry?, getEntry?_eraseKey_self hl]
theorem getKey!_eraseKey [BEq α] [PartialEquivBEq α] [Inhabited α] {l : List ((a : α) × β a)}
{k a : α} (hl : DistinctKeys l) :
getKey! a (eraseKey k l) = if k == a then default else getKey! a l := by
simp [getKey!_eq_getKey?, getKey?_eraseKey hl, apply_ite Option.get!]
theorem getKey!_eraseKey_self [BEq α] [PartialEquivBEq α] [Inhabited α] {l : List ((a : α) × β a)}
{k : α} (hl : DistinctKeys l) : getKey! k (eraseKey k l) = default := by
simp [getKey!_eq_getKey?, getKey?_eraseKey_self hl]
theorem getKeyD_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a fallback : α}
(hl : DistinctKeys l) :
getKeyD a (eraseKey k l) fallback = if k == a then fallback else getKeyD a l fallback := by
simp [getKeyD_eq_getKey?, getKey?_eraseKey hl, apply_ite (fun x => Option.getD x fallback)]
theorem getKeyD_eraseKey_self [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
{k fallback : α} (hl : DistinctKeys l) : getKeyD k (eraseKey k l) fallback = fallback := by
simp [getKeyD_eq_getKey?, getKey?_eraseKey_self hl]
theorem containsKey_eraseKey_self [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α}
(h : DistinctKeys l) : containsKey k (eraseKey k l) = false := by
simp [containsKey_eq_isSome_getEntry?, getEntry?_eraseKey_self h]
@@ -1340,6 +1557,13 @@ theorem getValue_eraseKey {β : Type v} [BEq α] [PartialEquivBEq α] {l : List
rw [ Option.some_inj, getValue?_eq_some_getValue, getValue?_eraseKey hl, h.1]
simp [ getValue?_eq_some_getValue]
theorem getKey_eraseKey [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k a : α} {h}
(hl : DistinctKeys l) : getKey a (eraseKey k l) h =
getKey a l (containsKey_of_containsKey_eraseKey hl h) := by
rw [containsKey_eraseKey hl, Bool.and_eq_true, Bool.not_eq_true'] at h
rw [ Option.some_inj, getKey?_eq_some_getKey, getKey?_eraseKey hl, h.1]
simp [ getKey?_eq_some_getKey]
theorem getEntry?_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α}
(hl : DistinctKeys l) (h : Perm l l') : getEntry? a l = getEntry? a l' := by
induction h
@@ -1412,6 +1636,26 @@ theorem getValueD_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((_ : α)
end
theorem getKey?_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α}
(hl : DistinctKeys l) (h : Perm l l') : getKey? a l = getKey? a l' := by
rw [getKey?_eq_getEntry?, getKey?_eq_getEntry?, getEntry?_of_perm hl h]
theorem getKey_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α} {h'}
(hl : DistinctKeys l) (h : Perm l l') :
getKey a l h' = getKey a l' ((containsKey_of_perm h).symm.trans h') := by
rw [ Option.some_inj, getKey?_eq_some_getKey, getKey?_eq_some_getKey,
getKey?_of_perm hl h]
theorem getKey!_of_perm [BEq α] [PartialEquivBEq α] [Inhabited α] {l l' : List ((a : α) × β a)}
{a : α} (hl : DistinctKeys l) (h : Perm l l') :
getKey! a l = getKey! a l' := by
simp only [getKey!_eq_getKey?, getKey?_of_perm hl h]
theorem getKeyD_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a fallback : α}
(hl : DistinctKeys l) (h : Perm l l') :
getKeyD a l fallback = getKeyD a l' fallback := by
simp only [getKeyD_eq_getKey?, getKey?_of_perm hl h]
theorem perm_cons_getEntry [BEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l) :
l', Perm l (getEntry a l h :: l') := by
induction l using assoc_induction
@@ -1521,6 +1765,18 @@ theorem getValueCast_append_of_containsKey_eq_false [BEq α] [LawfulBEq α]
rw [ Option.some_inj, getValueCast?_eq_some_getValueCast, getValueCast?_eq_some_getValueCast,
getValueCast?_append_of_containsKey_eq_false hl']
theorem getKey?_append_of_containsKey_eq_false [BEq α] [PartialEquivBEq α]
{l l' : List ((a : α) × β a)} {a : α} (hl' : containsKey a l' = false) :
getKey? a (l ++ l') = getKey? a l := by
simp [getKey?_eq_getEntry?, getEntry?_eq_none.2 hl']
theorem getKey_append_of_containsKey_eq_false [BEq α] [PartialEquivBEq α]
{l l' : List ((a : α) × β a)} {a : α} {h} (hl' : containsKey a l' = false) :
getKey a (l ++ l') h =
getKey a l ((containsKey_append_of_not_contains_right hl').symm.trans h) := by
rw [ Option.some_inj, getKey?_eq_some_getKey, getKey?_eq_some_getKey,
getKey?_append_of_containsKey_eq_false hl']
theorem replaceEntry_append_of_containsKey_left [BEq α] {l l' : List ((a : α) × β a)} {k : α}
{v : β k} (h : containsKey k l) : replaceEntry k v (l ++ l') = replaceEntry k v l ++ l' := by
induction l using assoc_induction

View File

@@ -262,6 +262,10 @@ def consₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (b : β a) : Raw
def get?ₘ [BEq α] [LawfulBEq α] [Hashable α] (m : Raw₀ α β) (a : α) : Option (β a) :=
(bucket m.1.buckets m.2 a).getCast? a
/-- Internal implementation detail of the hash map -/
def getKey?ₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) : Option α :=
(bucket m.1.buckets m.2 a).getKey? a
/-- Internal implementation detail of the hash map -/
def containsₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) : Bool :=
(bucket m.1.buckets m.2 a).contains a
@@ -278,6 +282,18 @@ def getDₘ [BEq α] [LawfulBEq α] [Hashable α] (m : Raw₀ α β) (a : α) (f
def get!ₘ [BEq α] [LawfulBEq α] [Hashable α] (m : Raw₀ α β) (a : α) [Inhabited (β a)] : β a :=
(m.get?ₘ a).get!
/-- Internal implementation detail of the hash map -/
def getKeyₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (h : m.containsₘ a) : α :=
(bucket m.1.buckets m.2 a).getKey a h
/-- Internal implementation detail of the hash map -/
def getKeyDₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (fallback : α) : α :=
(m.getKey?ₘ a).getD fallback
/-- Internal implementation detail of the hash map -/
def getKey!ₘ [BEq α] [Hashable α] [Inhabited α] (m : Raw₀ α β) (a : α) : α :=
(m.getKey?ₘ a).get!
/-- Internal implementation detail of the hash map -/
def insertₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (b : β a) : Raw₀ α β :=
if m.containsₘ a then m.replaceₘ a b else Raw₀.expandIfNecessary (m.consₘ a b)
@@ -348,6 +364,20 @@ theorem get!_eq_get!ₘ [BEq α] [LawfulBEq α] [Hashable α] (m : Raw₀ α β)
get! m a = get!ₘ m a := by
simp [get!, get!ₘ, get?ₘ, List.getValueCast!_eq_getValueCast?, bucket]
theorem getKey?_eq_getKey?ₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) :
getKey? m a = getKey?ₘ m a := rfl
theorem getKey_eq_getKeyₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (h : m.contains a) :
getKey m a h = getKeyₘ m a h := rfl
theorem getKeyD_eq_getKeyDₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a fallback : α) :
getKeyD m a fallback = getKeyDₘ m a fallback := by
simp [getKeyD, getKeyDₘ, getKey?ₘ, List.getKeyD_eq_getKey?, bucket]
theorem getKey!_eq_getKey!ₘ [BEq α] [Hashable α] [Inhabited α] (m : Raw₀ α β) (a : α) :
getKey! m a = getKey!ₘ m a := by
simp [getKey!, getKey!ₘ, getKey?ₘ, List.getKey!_eq_getKey?, bucket]
theorem contains_eq_containsₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) :
m.contains a = m.containsₘ a := rfl

View File

@@ -135,6 +135,37 @@ theorem get!_val [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} {a :
m.val.get! a = m.get! a := by
simp [Raw.get!, m.2]
theorem getKey?_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} :
m.getKey? a = Raw₀.getKey? m, h.size_buckets_pos a := by
simp [Raw.getKey?, h.size_buckets_pos]
theorem getKey?_val [BEq α] [Hashable α] {m : Raw₀ α β} {a : α} :
m.val.getKey? a = m.getKey? a := by
simp [Raw.getKey?, m.2]
theorem getKey_eq [BEq α] [Hashable α] {m : Raw α β} {a : α} {h : a m} :
m.getKey a h = Raw₀.getKey m, by change dite .. = true at h; split at h <;> simp_all a
(by change dite .. = true at h; split at h <;> simp_all) := rfl
theorem getKey_val [BEq α] [Hashable α] {m : Raw₀ α β} {a : α} {h : a m.val} :
m.val.getKey a h = m.getKey a (contains_val (m := m) h) := rfl
theorem getKeyD_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a fallback : α} :
m.getKeyD a fallback = Raw₀.getKeyD m, h.size_buckets_pos a fallback := by
simp [Raw.getKeyD, h.size_buckets_pos]
theorem getKeyD_val [BEq α] [Hashable α] {m : Raw₀ α β} {a fallback : α} :
m.val.getKeyD a fallback = m.getKeyD a fallback := by
simp [Raw.getKeyD, m.2]
theorem getKey!_eq [BEq α] [Hashable α] [Inhabited α] {m : Raw α β} (h : m.WF) {a : α} :
m.getKey! a = Raw₀.getKey! m, h.size_buckets_pos a := by
simp [Raw.getKey!, h.size_buckets_pos]
theorem getKey!_val [BEq α] [Hashable α] [Inhabited α] {m : Raw₀ α β} {a : α} :
m.val.getKey! a = m.getKey! a := by
simp [Raw.getKey!, m.2]
theorem erase_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} :
m.erase a = Raw₀.erase m, h.size_buckets_pos a := by
simp [Raw.erase, h.size_buckets_pos]

View File

@@ -83,7 +83,8 @@ private def queryNames : Array Name :=
#[``contains_eq_containsKey, ``Raw.isEmpty_eq_isEmpty, ``Raw.size_eq_length,
``get?_eq_getValueCast?, ``Const.get?_eq_getValue?, ``get_eq_getValueCast,
``Const.get_eq_getValue, ``get!_eq_getValueCast!, ``getD_eq_getValueCastD,
``Const.get!_eq_getValue!, ``Const.getD_eq_getValueD]
``Const.get!_eq_getValue!, ``Const.getD_eq_getValueD, ``getKey?_eq_getKey?,
``getKey_eq_getKey, ``getKeyD_eq_getKeyD, ``getKey!_eq_getKey!]
private def modifyNames : Array Name :=
#[``toListModel_insert, ``toListModel_erase, ``toListModel_insertIfNew]
@@ -93,7 +94,8 @@ private def congrNames : MacroM (Array (TSyntax `term)) := do
`(_root_.List.Perm.length_eq), `(getValueCast?_of_perm _),
`(getValue?_of_perm _), `(getValue_of_perm _), `(getValueCast_of_perm _),
`(getValueCast!_of_perm _), `(getValueCastD_of_perm _), `(getValue!_of_perm _),
`(getValueD_of_perm _) ]
`(getValueD_of_perm _), `(getKey?_of_perm _), `(getKey_of_perm _), `(getKeyD_of_perm _),
`(getKey!_of_perm _)]
/-- Internal implementation detail of the hash map -/
scoped syntax "simp_to_model" ("using" term)? : tactic
@@ -535,6 +537,147 @@ theorem getD_congr [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a b : α} {fa
end Const
@[simp]
theorem getKey?_empty {a : α} {c} : (empty c : Raw₀ α β).getKey? a = none := by
simp [getKey?]
theorem getKey?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} :
m.1.isEmpty = true m.getKey? a = none := by
simp_to_model; empty
theorem getKey?_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a k : α} {v : β k} :
(m.insert k v).getKey? a = if k == a then some k else m.getKey? a := by
simp_to_model using List.getKey?_insertEntry
theorem getKey?_insert_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
(m.insert k v).getKey? k = some k := by
simp_to_model using List.getKey?_insertEntry_self
theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} :
m.contains a = (m.getKey? a).isSome := by
simp_to_model using List.containsKey_eq_isSome_getKey?
theorem getKey?_eq_none [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} :
m.contains a = false m.getKey? a = none := by
simp_to_model using List.getKey?_eq_none
theorem getKey?_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} :
(m.erase k).getKey? a = if k == a then none else m.getKey? a := by
simp_to_model using List.getKey?_eraseKey
theorem getKey?_erase_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
(m.erase k).getKey? k = none := by
simp_to_model using List.getKey?_eraseKey_self
theorem getKey_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {v : β k} {h₁} :
(m.insert k v).getKey a h₁ =
if h₂ : k == a then
k
else
m.getKey a (contains_of_contains_insert _ h h₁ (Bool.eq_false_iff.2 h₂)) := by
simp_to_model using List.getKey_insertEntry
theorem getKey_insert_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
(m.insert k v).getKey k (contains_insert_self _ h) = k := by
simp_to_model using List.getKey_insertEntry_self
@[simp]
theorem getKey_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {h'} :
(m.erase k).getKey a h' = m.getKey a (contains_of_contains_erase _ h h') := by
simp_to_model using List.getKey_eraseKey
theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} {h} :
m.getKey? a = some (m.getKey a h) := by
simp_to_model using List.getKey?_eq_some_getKey
theorem getKey!_empty {a : α} [Inhabited α] {c} :
(empty c : Raw₀ α β).getKey! a = default := by
simp [getKey!, empty]
theorem getKey!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {a : α} :
m.1.isEmpty = true m.getKey! a = default := by
simp_to_model; empty;
theorem getKey!_insert [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {k a : α}
{v : β k} :
(m.insert k v).getKey! a = if k == a then k else m.getKey! a := by
simp_to_model using List.getKey!_insertEntry
theorem getKey!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {a : α}
{b : β a} : (m.insert a b).getKey! a = a := by
simp_to_model using List.getKey!_insertEntry_self
theorem getKey!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {a : α} :
m.contains a = false m.getKey! a = default := by
simp_to_model using List.getKey!_eq_default
theorem getKey!_erase [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {k a : α} :
(m.erase k).getKey! a = if k == a then default else m.getKey! a := by
simp_to_model using List.getKey!_eraseKey
theorem getKey!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {k : α} :
(m.erase k).getKey! k = default := by
simp_to_model using List.getKey!_eraseKey_self
theorem getKey?_eq_some_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {a : α} :
m.contains a = true m.getKey? a = some (m.getKey! a) := by
simp_to_model using List.getKey?_eq_some_getKey!
theorem getKey!_eq_get!_getKey? [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {a : α} :
m.getKey! a = (m.getKey? a).get! := by
simp_to_model using List.getKey!_eq_getKey?
theorem getKey_eq_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {a : α} {h} :
m.getKey a h = m.getKey! a := by
simp_to_model using List.getKey_eq_getKey!
theorem getKeyD_empty {a : α} {fallback : α} {c} :
(empty c : Raw₀ α β).getKeyD a fallback = fallback := by
simp [getKeyD, empty]
theorem getKeyD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a fallback : α} :
m.1.isEmpty = true m.getKeyD a fallback = fallback := by
simp_to_model; empty
theorem getKeyD_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a fallback : α} {v : β k} :
(m.insert k v).getKeyD a fallback =
if k == a then k else m.getKeyD a fallback := by
simp_to_model using List.getKeyD_insertEntry
theorem getKeyD_insert_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a fallback : α}
{b : β a} :
(m.insert a b).getKeyD a fallback = a := by
simp_to_model using List.getKeyD_insertEntry_self
theorem getKeyD_eq_fallback [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a fallback : α} :
m.contains a = false m.getKeyD a fallback = fallback := by
simp_to_model using List.getKeyD_eq_fallback
theorem getKeyD_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a fallback : α} :
(m.erase k).getKeyD a fallback = if k == a then fallback else m.getKeyD a fallback := by
simp_to_model using List.getKeyD_eraseKey
theorem getKeyD_erase_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k fallback : α} :
(m.erase k).getKeyD k fallback = fallback := by
simp_to_model using List.getKeyD_eraseKey_self
theorem getKey?_eq_some_getKeyD [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a fallback : α} :
m.contains a = true m.getKey? a = some (m.getKeyD a fallback) := by
simp_to_model using List.getKey?_eq_some_getKeyD
theorem getKeyD_eq_getD_getKey? [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a fallback : α} :
m.getKeyD a fallback = (m.getKey? a).getD fallback := by
simp_to_model using List.getKeyD_eq_getKey?
theorem getKey_eq_getKeyD [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a fallback : α} {h} :
m.getKey a h = m.getKeyD a fallback := by
simp_to_model using List.getKey_eq_getKeyD
theorem getKey!_eq_getKeyD_default [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF)
{a : α} :
m.getKey! a = m.getKeyD a default := by
simp_to_model using List.getKey!_eq_getKeyD_default
theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
(m.insertIfNew k v).1.isEmpty = false := by
simp_to_model using List.isEmpty_insertEntryIfNew
@@ -620,6 +763,29 @@ theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a :
end Const
theorem getKey?_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {v : β k} :
(m.insertIfNew k v).getKey? a =
if k == a m.contains k = false then some k else m.getKey? a := by
simp_to_model using List.getKey?_insertEntryIfNew
theorem getKey_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {v : β k} {h₁} :
(m.insertIfNew k v).getKey a h₁ =
if h₂ : k == a m.contains k = false then k
else m.getKey a (contains_of_contains_insertIfNew' _ h h₁ h₂) := by
simp_to_model using List.getKey_insertEntryIfNew
theorem getKey!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {k a : α}
{v : β k} :
(m.insertIfNew k v).getKey! a =
if k == a m.contains k = false then k else m.getKey! a := by
simp_to_model using List.getKey!_insertEntryIfNew
theorem getKeyD_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a fallback : α}
{v : β k} :
(m.insertIfNew k v).getKeyD a fallback =
if k == a m.contains k = false then k else m.getKeyD a fallback := by
simp_to_model using List.getKeyD_insertEntryIfNew
@[simp]
theorem getThenInsertIfNew?_fst [LawfulBEq α] {k : α} {v : β k} :
(m.getThenInsertIfNew? k v).1 = m.get? k := by

View File

@@ -233,6 +233,47 @@ theorem getD_eq_getValueCastD [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀
m.getD a fallback = getValueCastD a (toListModel m.1.buckets) fallback := by
rw [getD_eq_getDₘ, getDₘ_eq_getValueCastD hm]
theorem getKey?ₘ_eq_getKey? [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
(hm : Raw.WFImp m.1) {a : α} :
m.getKey?ₘ a = List.getKey? a (toListModel m.1.buckets) :=
apply_bucket hm AssocList.getKey?_eq List.getKey?_of_perm List.getKey?_append_of_containsKey_eq_false
theorem getKey?_eq_getKey? [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
(hm : Raw.WFImp m.1) {a : α} :
m.getKey? a = List.getKey? a (toListModel m.1.buckets) := by
rw [getKey?_eq_getKey?ₘ, getKey?ₘ_eq_getKey? hm]
theorem getKeyₘ_eq_getKey [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
(hm : Raw.WFImp m.1) {a : α} {h : m.contains a} :
m.getKeyₘ a h = List.getKey a (toListModel m.1.buckets) (contains_eq_containsKey hm h) :=
apply_bucket_with_proof hm a AssocList.getKey List.getKey AssocList.getKey_eq
List.getKey_of_perm List.getKey_append_of_containsKey_eq_false
theorem getKey_eq_getKey [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
(hm : Raw.WFImp m.1) {a : α} {h : m.contains a} :
m.getKey a h = List.getKey a (toListModel m.1.buckets) (contains_eq_containsKey hm h) := by
rw [getKey_eq_getKeyₘ, getKeyₘ_eq_getKey hm]
theorem getKey!ₘ_eq_getKey! [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α]
{m : Raw₀ α β} (hm : Raw.WFImp m.1) {a : α} :
m.getKey!ₘ a = List.getKey! a (toListModel m.1.buckets) := by
rw [getKey!ₘ, getKey?ₘ_eq_getKey? hm, List.getKey!_eq_getKey?]
theorem getKey!_eq_getKey! [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α]
{m : Raw₀ α β} (hm : Raw.WFImp m.1) {a : α} :
m.getKey! a = List.getKey! a (toListModel m.1.buckets) := by
rw [getKey!_eq_getKey!ₘ, getKey!ₘ_eq_getKey! hm]
theorem getKeyDₘ_eq_getKeyD [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
(hm : Raw.WFImp m.1) {a fallback : α} :
m.getKeyDₘ a fallback = List.getKeyD a (toListModel m.1.buckets) fallback := by
rw [getKeyDₘ, getKey?ₘ_eq_getKey? hm, List.getKeyD_eq_getKey?]
theorem getKeyD_eq_getKeyD [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
(hm : Raw.WFImp m.1) {a fallback : α} :
m.getKeyD a fallback = List.getKeyD a (toListModel m.1.buckets) fallback := by
rw [getKeyD_eq_getKeyDₘ, getKeyDₘ_eq_getKeyD hm]
section
variable {β : Type v}

View File

@@ -599,6 +599,189 @@ theorem getD_congr [EquivBEq α] [LawfulHashable α] {a b : α} {fallback : β}
end Const
@[simp]
theorem getKey?_empty {a : α} {c} : (empty c : DHashMap α β).getKey? a = none :=
Raw₀.getKey?_empty
@[simp]
theorem getKey?_emptyc {a : α} : ( : DHashMap α β).getKey? a = none :=
Raw₀.getKey?_empty
theorem getKey?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
m.isEmpty = true m.getKey? a = none :=
Raw₀.getKey?_of_isEmpty m.1, _ m.2
theorem getKey?_insert [EquivBEq α] [LawfulHashable α] {a k : α} {v : β k} :
(m.insert k v).getKey? a = if k == a then some k else m.getKey? a :=
Raw₀.getKey?_insert m.1, _ m.2
@[simp]
theorem getKey?_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
(m.insert k v).getKey? k = some k :=
Raw₀.getKey?_insert_self m.1, _ m.2
theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = (m.getKey? a).isSome :=
Raw₀.contains_eq_isSome_getKey? m.1, _ m.2
theorem getKey?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = false m.getKey? a = none :=
Raw₀.getKey?_eq_none m.1, _ m.2
theorem getKey?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a m m.getKey? a = none := by
simpa [mem_iff_contains] using getKey?_eq_none_of_contains_eq_false
theorem getKey?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k).getKey? a = if k == a then none else m.getKey? a :=
Raw₀.getKey?_erase m.1, _ m.2
@[simp]
theorem getKey?_erase_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).getKey? k = none :=
Raw₀.getKey?_erase_self m.1, _ m.2
theorem getKey_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} {h₁} :
(m.insert k v).getKey a h₁ =
if h₂ : k == a then
k
else
m.getKey a (mem_of_mem_insert h₁ (Bool.eq_false_iff.2 h₂)) :=
Raw₀.getKey_insert m.1, _ m.2
@[simp]
theorem getKey_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
(m.insert k v).getKey k mem_insert_self = k :=
Raw₀.getKey_insert_self m.1, _ m.2
@[simp]
theorem getKey_erase [EquivBEq α] [LawfulHashable α] {k a : α} {h'} :
(m.erase k).getKey a h' = m.getKey a (mem_of_mem_erase h') :=
Raw₀.getKey_erase m.1, _ m.2
theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] {a : α}
{h} :
m.getKey? a = some (m.getKey a h) :=
Raw₀.getKey?_eq_some_getKey m.1, _ m.2
@[simp]
theorem getKey!_empty [Inhabited α] {a : α} {c} :
(empty c : DHashMap α β).getKey! a = default :=
Raw₀.getKey!_empty
@[simp]
theorem getKey!_emptyc [Inhabited α] {a : α} :
( : DHashMap α β).getKey! a = default :=
getKey!_empty
theorem getKey!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
m.isEmpty = true m.getKey! a = default :=
Raw₀.getKey!_of_isEmpty m.1, _ m.2
theorem getKey!_insert [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} {v : β k} :
(m.insert k v).getKey! a =
if k == a then k else m.getKey! a :=
Raw₀.getKey!_insert m.1, _ m.2
@[simp]
theorem getKey!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} {b : β a} :
(m.insert a b).getKey! a = a :=
Raw₀.getKey!_insert_self m.1, _ m.2
theorem getKey!_eq_default_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α]
{a : α} :
m.contains a = false m.getKey! a = default :=
Raw₀.getKey!_eq_default m.1, _ m.2
theorem getKey!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
¬a m m.getKey! a = default := by
simpa [mem_iff_contains] using getKey!_eq_default_of_contains_eq_false
theorem getKey!_erase [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} :
(m.erase k).getKey! a = if k == a then default else m.getKey! a :=
Raw₀.getKey!_erase m.1, _ m.2
@[simp]
theorem getKey!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} :
(m.erase k).getKey! k = default :=
Raw₀.getKey!_erase_self m.1, _ m.2
theorem getKey?_eq_some_getKey!_of_contains [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
m.contains a = true m.getKey? a = some (m.getKey! a) :=
Raw₀.getKey?_eq_some_getKey! m.1, _ m.2
theorem getKey?_eq_some_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
a m m.getKey? a = some (m.getKey! a) := by
simpa [mem_iff_contains] using getKey?_eq_some_getKey!_of_contains
theorem getKey!_eq_get!_getKey? [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
m.getKey! a = (m.getKey? a).get! :=
Raw₀.getKey!_eq_get!_getKey? m.1, _ m.2
theorem getKey_eq_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} {h} :
m.getKey a h = m.getKey! a :=
Raw₀.getKey_eq_getKey! m.1, _ m.2
@[simp]
theorem getKeyD_empty {a fallback : α} {c} :
(empty c : DHashMap α β).getKeyD a fallback = fallback :=
Raw₀.getKeyD_empty
@[simp]
theorem getKeyD_emptyc {a fallback : α} :
( : DHashMap α β).getKeyD a fallback = fallback :=
getKeyD_empty
theorem getKeyD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a fallback : α} :
m.isEmpty = true m.getKeyD a fallback = fallback :=
Raw₀.getKeyD_of_isEmpty m.1, _ m.2
theorem getKeyD_insert [EquivBEq α] [LawfulHashable α] {k a fallback : α} {v : β k} :
(m.insert k v).getKeyD a fallback =
if k == a then k else m.getKeyD a fallback :=
Raw₀.getKeyD_insert m.1, _ m.2
@[simp]
theorem getKeyD_insert_self [EquivBEq α] [LawfulHashable α] {k fallback : α} {v : β k} :
(m.insert k v).getKeyD k fallback = k :=
Raw₀.getKeyD_insert_self m.1, _ m.2
theorem getKeyD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α}
{fallback : α} :
m.contains a = false m.getKeyD a fallback = fallback :=
Raw₀.getKeyD_eq_fallback m.1, _ m.2
theorem getKeyD_eq_fallback [EquivBEq α] [LawfulHashable α] {a fallback : α} :
¬a m m.getKeyD a fallback = fallback := by
simpa [mem_iff_contains] using getKeyD_eq_fallback_of_contains_eq_false
theorem getKeyD_erase [EquivBEq α] [LawfulHashable α] {k a fallback : α} :
(m.erase k).getKeyD a fallback = if k == a then fallback else m.getKeyD a fallback :=
Raw₀.getKeyD_erase m.1, _ m.2
@[simp]
theorem getKeyD_erase_self [EquivBEq α] [LawfulHashable α] {k fallback : α} :
(m.erase k).getKeyD k fallback = fallback :=
Raw₀.getKeyD_erase_self m.1, _ m.2
theorem getKey?_eq_some_getKeyD_of_contains [EquivBEq α] [LawfulHashable α] {a fallback : α} :
m.contains a = true m.getKey? a = some (m.getKeyD a fallback) :=
Raw₀.getKey?_eq_some_getKeyD m.1, _ m.2
theorem getKey?_eq_some_getKeyD [EquivBEq α] [LawfulHashable α] {a fallback : α} :
a m m.getKey? a = some (m.getKeyD a fallback) := by
simpa [mem_iff_contains] using getKey?_eq_some_getKeyD_of_contains
theorem getKeyD_eq_getD_getKey? [EquivBEq α] [LawfulHashable α] {a fallback : α} :
m.getKeyD a fallback = (m.getKey? a).getD fallback :=
Raw₀.getKeyD_eq_getD_getKey? m.1, _ m.2
theorem getKey_eq_getKeyD [EquivBEq α] [LawfulHashable α] {a fallback : α} {h} :
m.getKey a h = m.getKeyD a fallback :=
Raw₀.getKey_eq_getKeyD m.1, _ m.2
theorem getKey!_eq_getKeyD_default [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
m.getKey! a = m.getKeyD a default :=
Raw₀.getKey!_eq_getKeyD_default m.1, _ m.2
@[simp]
theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
(m.insertIfNew k v).isEmpty = false :=
@@ -706,6 +889,29 @@ theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback
end Const
theorem getKey?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
getKey? (m.insertIfNew k v) a = if k == a ¬k m then some k else getKey? m a := by
simp [mem_iff_contains, contains_insertIfNew]
exact Raw₀.getKey?_insertIfNew m.1, _ m.2
theorem getKey_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} {h₁} :
getKey (m.insertIfNew k v) a h₁ =
if h₂ : k == a ¬k m then k else getKey m a (mem_of_mem_insertIfNew' h₁ h₂) := by
simp [mem_iff_contains, contains_insertIfNew]
exact Raw₀.getKey_insertIfNew m.1, _ m.2
theorem getKey!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} {v : β k} :
getKey! (m.insertIfNew k v) a = if k == a ¬k m then k else getKey! m a := by
simp [mem_iff_contains, contains_insertIfNew]
exact Raw₀.getKey!_insertIfNew m.1, _ m.2
theorem getKeyD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a fallback : α} {v : β k} :
getKeyD (m.insertIfNew k v) a fallback =
if k == a ¬k m then k else getKeyD m a fallback := by
simp [mem_iff_contains, contains_insertIfNew]
exact Raw₀.getKeyD_insertIfNew m.1, _ m.2
@[simp]
theorem getThenInsertIfNew?_fst [LawfulBEq α] {k : α} {v : β k} :
(m.getThenInsertIfNew? k v).1 = m.get? k :=

View File

@@ -237,6 +237,41 @@ returned map has a new value inserted.
end
/--
Checks if a mapping for the given key exists and returns the key if it does, otherwise `none`.
The result in the `some` case is guaranteed to be pointer equal to the key in the map.
-/
@[inline] def getKey? [BEq α] [Hashable α] (m : Raw α β) (a : α) : Option α :=
if h : 0 < m.buckets.size then
Raw₀.getKey? m, h a
else none -- will never happen for well-formed inputs
/--
Retrieves the key from the mapping that matches `a`. Ensures that such a mapping exists by
requiring a proof of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the map.
-/
@[inline] def getKey [BEq α] [Hashable α] (m : Raw α β) (a : α) (h : a m) : α :=
Raw₀.getKey m, by change dite .. = true at h; split at h <;> simp_all a
(by change dite .. = true at h; split at h <;> simp_all)
/--
Checks if a mapping for the given key exists and returns the key if it does, otherwise `fallback`.
If a mapping exists the result is guaranteed to be pointer equal to the key in the map.
-/
@[inline] def getKeyD [BEq α] [Hashable α] (m : Raw α β) (a : α) (fallback : α) : α :=
if h : 0 < m.buckets.size then
Raw₀.getKeyD m, h a fallback
else fallback -- will never happen for well-formed inputs
/--
Checks if a mapping for the given key exists and returns the key if it does, otherwise panics.
If no panic occurs the result is guaranteed to be pointer equal to the key in the map.
-/
@[inline] def getKey! [BEq α] [Hashable α] [Inhabited α] (m : Raw α β) (a : α) : α :=
if h : 0 < m.buckets.size then
Raw₀.getKey! m, h a
else default -- will never happen for well-formed inputs
/--
Returns `true` if the hash map contains no mappings.

View File

@@ -54,7 +54,11 @@ private def baseNames : Array Name :=
``contains_eq, ``contains_val,
``get_eq, ``get_val,
``getD_eq, ``getD_val,
``get!_eq, ``get!_val]
``get!_eq, ``get!_val,
``getKey?_eq, ``getKey?_val,
``getKey_eq, ``getKey_val,
``getKey!_eq, ``getKey!_val,
``getKeyD_eq, ``getKeyD_val]
/-- Internal implementation detail of the hash map -/
scoped syntax "simp_to_raw" ("using" term)? : tactic
@@ -661,6 +665,194 @@ theorem getD_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} {fall
end Const
@[simp]
theorem getKey?_empty {a : α} {c} :
(empty c : Raw α β).getKey? a = none := by
simp_to_raw using Raw₀.getKey?_empty
@[simp]
theorem getKey?_emptyc {a : α} : ( : Raw α β).getKey? a = none :=
getKey?_empty
theorem getKey?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
m.isEmpty = true m.getKey? a = none := by
simp_to_raw using Raw₀.getKey?_of_isEmpty m, _
theorem getKey?_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {a k : α} {v : β k} :
(m.insert k v).getKey? a = if k == a then some k else m.getKey? a := by
simp_to_raw using Raw₀.getKey?_insert
@[simp]
theorem getKey?_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
(m.insert k v).getKey? k = some k := by
simp_to_raw using Raw₀.getKey?_insert_self
theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
m.contains a = (m.getKey? a).isSome := by
simp_to_raw using Raw₀.contains_eq_isSome_getKey?
theorem getKey?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
m.contains a = false m.getKey? a = none := by
simp_to_raw using Raw₀.getKey?_eq_none
theorem getKey?_eq_none [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
¬a m m.getKey? a = none := by
simpa [mem_iff_contains] using getKey?_eq_none_of_contains_eq_false h
theorem getKey?_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
(m.erase k).getKey? a = if k == a then none else m.getKey? a := by
simp_to_raw using Raw₀.getKey?_erase
@[simp]
theorem getKey?_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
(m.erase k).getKey? k = none := by
simp_to_raw using Raw₀.getKey?_erase_self
theorem getKey_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} {h₁} :
(m.insert k v).getKey a h₁ =
if h₂ : k == a then
k
else
m.getKey a (mem_of_mem_insert h h₁ (Bool.eq_false_iff.2 h₂)) := by
simp_to_raw using Raw₀.getKey_insert m, _
@[simp]
theorem getKey_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
(m.insert k v).getKey k (mem_insert_self h) = k := by
simp_to_raw using Raw₀.getKey_insert_self m, _
@[simp]
theorem getKey_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {h'} :
(m.erase a).getKey k h' = m.getKey k (mem_of_mem_erase h h') := by
simp_to_raw using Raw₀.getKey_erase m, _
theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {h} :
m.getKey? a = some (m.getKey a h) := by
simp_to_raw using Raw₀.getKey?_eq_some_getKey
@[simp]
theorem getKey!_empty [Inhabited α] {a : α} {c} :
(empty c : Raw α β).getKey! a = default := by
simp_to_raw using Raw₀.getKey!_empty
@[simp]
theorem getKey!_emptyc [Inhabited α] {a : α} :
( : Raw α β).getKey! a = default :=
getKey!_empty
theorem getKey!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
m.isEmpty = true m.getKey! a = default := by
simp_to_raw using Raw₀.getKey!_of_isEmpty m, _
theorem getKey!_insert [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k a : α} {v : β k} :
(m.insert k v).getKey! a = if k == a then k else m.getKey! a := by
simp_to_raw using Raw₀.getKey!_insert
@[simp]
theorem getKey!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k : α}
{v : β k} :
(m.insert k v).getKey! k = k := by
simp_to_raw using Raw₀.getKey!_insert_self
theorem getKey!_eq_default_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α]
(h : m.WF) {a : α} :
m.contains a = false m.getKey! a = default := by
simp_to_raw using Raw₀.getKey!_eq_default
theorem getKey!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α}:
¬a m m.getKey! a = default := by
simpa [mem_iff_contains] using getKey!_eq_default_of_contains_eq_false h
theorem getKey!_erase [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k a : α} :
(m.erase k).getKey! a = if k == a then default else m.getKey! a := by
simp_to_raw using Raw₀.getKey!_erase
@[simp]
theorem getKey!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k : α} :
(m.erase k).getKey! k = default := by
simp_to_raw using Raw₀.getKey!_erase_self
theorem getKey?_eq_some_getKey!_of_contains [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF)
{a : α} :
m.contains a = true m.getKey? a = some (m.getKey! a) := by
simp_to_raw using Raw₀.getKey?_eq_some_getKey!
theorem getKey?_eq_some_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
a m m.getKey? a = some (m.getKey! a) := by
simpa [mem_iff_contains] using getKey?_eq_some_getKey!_of_contains h
theorem getKey!_eq_get!_getKey? [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
m.getKey! a = (m.getKey? a).get! := by
simp_to_raw using Raw₀.getKey!_eq_get!_getKey?
theorem getKey_eq_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} {h} :
m.getKey a h = m.getKey! a := by
simp_to_raw using Raw₀.getKey_eq_getKey!
@[simp]
theorem getKeyD_empty {a fallback : α} {c} :
(empty c : Raw α β).getKeyD a fallback = fallback := by
simp_to_raw using Raw₀.getKeyD_empty
@[simp]
theorem getKeyD_emptyc {a fallback : α} :
( : Raw α β).getKeyD a fallback = fallback :=
getKeyD_empty
theorem getKeyD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
m.isEmpty = true m.getKeyD a fallback = fallback := by
simp_to_raw using Raw₀.getKeyD_of_isEmpty m, _
theorem getKeyD_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α} {v : β k} :
(m.insert k v).getKeyD a fallback =
if k == a then k else m.getKeyD a fallback := by
simp_to_raw using Raw₀.getKeyD_insert
@[simp]
theorem getKeyD_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} {b : β a} :
(m.insert a b).getKeyD a fallback = a := by
simp_to_raw using Raw₀.getKeyD_insert_self
theorem getKeyD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF)
{a fallback : α} :
m.contains a = false m.getKeyD a fallback = fallback := by
simp_to_raw using Raw₀.getKeyD_eq_fallback
theorem getKeyD_eq_fallback [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
¬a m m.getKeyD a fallback = fallback := by
simpa [mem_iff_contains] using getKeyD_eq_fallback_of_contains_eq_false h
theorem getKeyD_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α} :
(m.erase k).getKeyD a fallback = if k == a then fallback else m.getKeyD a fallback := by
simp_to_raw using Raw₀.getKeyD_erase
@[simp]
theorem getKeyD_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k fallback : α} :
(m.erase k).getKeyD k fallback = fallback := by
simp_to_raw using Raw₀.getKeyD_erase_self
theorem getKey?_eq_some_getKeyD_of_contains [EquivBEq α] [LawfulHashable α] (h : m.WF)
{a fallback : α} :
m.contains a = true m.getKey? a = some (m.getKeyD a fallback) := by
simp_to_raw using Raw₀.getKey?_eq_some_getKeyD
theorem getKey?_eq_some_getKeyD [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
a m m.getKey? a = some (m.getKeyD a fallback) := by
simpa [mem_iff_contains] using getKey?_eq_some_getKeyD_of_contains h
theorem getKeyD_eq_getD_getKey? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
m.getKeyD a fallback = (m.getKey? a).getD fallback := by
simp_to_raw using Raw₀.getKeyD_eq_getD_getKey?
theorem getKey_eq_getKeyD [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} {h} :
m.getKey a h = m.getKeyD a fallback := by
simp_to_raw using Raw₀.getKey_eq_getKeyD
theorem getKey!_eq_getKeyD_default [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF)
{a : α} :
m.getKey! a = m.getKeyD a default := by
simp_to_raw using Raw₀.getKey!_eq_getKeyD_default
@[simp]
theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
(m.insertIfNew k v).isEmpty = false := by
@@ -774,6 +966,30 @@ theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α}
end Const
theorem getKey?_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
getKey? (m.insertIfNew k v) a = if k == a ¬k m then some k else getKey? m a := by
simp only [mem_iff_contains, Bool.not_eq_true]
simp_to_raw using Raw₀.getKey?_insertIfNew
theorem getKey_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} {h₁} :
getKey (m.insertIfNew k v) a h₁ =
if h₂ : k == a ¬k m then k else getKey m a (mem_of_mem_insertIfNew' h h₁ h₂) := by
simp only [mem_iff_contains, Bool.not_eq_true]
simp_to_raw using Raw₀.getKey_insertIfNew m, _
theorem getKey!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k a : α}
{v : β k} :
getKey! (m.insertIfNew k v) a = if k == a ¬k m then k else getKey! m a := by
simp only [mem_iff_contains, Bool.not_eq_true]
simp_to_raw using Raw₀.getKey!_insertIfNew
theorem getKeyD_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α}
{v : β k} :
getKeyD (m.insertIfNew k v) a fallback =
if k == a ¬k m then k else getKeyD m a fallback := by
simp only [mem_iff_contains, Bool.not_eq_true]
simp_to_raw using Raw₀.getKeyD_insertIfNew
@[simp]
theorem getThenInsertIfNew?_fst [LawfulBEq α] (h : m.WF) {k : α} {v : β k} :
(m.getThenInsertIfNew? k v).1 = m.get? k := by

View File

@@ -160,6 +160,18 @@ instance [BEq α] [Hashable α] : GetElem? (HashMap α β) α β (fun m a => a
getElem? m a := m.get? a
getElem! m a := m.get! a
@[inline, inherit_doc DHashMap.getKey?] def getKey? (m : HashMap α β) (a : α) : Option α :=
DHashMap.getKey? m.inner a
@[inline, inherit_doc DHashMap.getKey] def getKey (m : HashMap α β) (a : α) (h : a m) : α :=
DHashMap.getKey m.inner a h
@[inline, inherit_doc DHashMap.getKeyD] def getKeyD (m : HashMap α β) (a : α) (fallback : α) : α :=
DHashMap.getKeyD m.inner a fallback
@[inline, inherit_doc DHashMap.getKey!] def getKey! [Inhabited α] (m : HashMap α β) (a : α) : α :=
DHashMap.getKey! m.inner a
@[inline, inherit_doc DHashMap.erase] def erase (m : HashMap α β) (a : α) :
HashMap α β :=
m.inner.erase a

View File

@@ -391,6 +391,178 @@ theorem getD_congr [EquivBEq α] [LawfulHashable α] {a b : α} {fallback : β}
m.getD a fallback = m.getD b fallback :=
DHashMap.Const.getD_congr hab
@[simp]
theorem getKey?_empty {a : α} {c} : (empty c : HashMap α β).getKey? a = none :=
DHashMap.getKey?_empty
@[simp]
theorem getKey?_emptyc {a : α} : ( : HashMap α β).getKey? a = none :=
DHashMap.getKey?_emptyc
theorem getKey?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
m.isEmpty = true m.getKey? a = none :=
DHashMap.getKey?_of_isEmpty
theorem getKey?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insert k v).getKey? a = if k == a then some k else m.getKey? a :=
DHashMap.getKey?_insert
@[simp]
theorem getKey?_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v).getKey? k = some k :=
DHashMap.getKey?_insert_self
theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = (m.getKey? a).isSome :=
DHashMap.contains_eq_isSome_getKey?
theorem getKey?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = false m.getKey? a = none :=
DHashMap.getKey?_eq_none_of_contains_eq_false
theorem getKey?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a m m.getKey? a = none :=
DHashMap.getKey?_eq_none
theorem getKey?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k).getKey? a = if k == a then none else m.getKey? a :=
DHashMap.getKey?_erase
@[simp]
theorem getKey?_erase_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).getKey? k = none :=
DHashMap.getKey?_erase_self
theorem getKey_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
(m.insert k v)[a]'h₁ =
if h₂ : k == a then v else m[a]'(mem_of_mem_insert h₁ (Bool.eq_false_iff.2 h₂)) :=
DHashMap.Const.get_insert (h₁ := h₁)
@[simp]
theorem getKey_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v).getKey k mem_insert_self = k :=
DHashMap.getKey_insert_self
@[simp]
theorem getKey_erase [EquivBEq α] [LawfulHashable α] {k a : α} {h'} :
(m.erase k).getKey a h' = m.getKey a (mem_of_mem_erase h') :=
DHashMap.getKey_erase (h' := h')
theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] {a : α} {h' : a m} :
m.getKey? a = some (m.getKey a h') :=
@DHashMap.getKey?_eq_some_getKey _ _ _ _ _ _ _ _ h'
@[simp]
theorem getKey!_empty [Inhabited α] {a : α} {c} : (empty c : HashMap α β).getKey! a = default :=
DHashMap.getKey!_empty
@[simp]
theorem getKey!_emptyc [Inhabited α] {a : α} : ( : HashMap α β).getKey! a = default :=
DHashMap.getKey!_emptyc
theorem getKey!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
m.isEmpty = true m.getKey! a = default :=
DHashMap.getKey!_of_isEmpty
theorem getKey!_insert [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} {v : β} :
(m.insert k v).getKey! a = if k == a then k else m.getKey! a :=
DHashMap.getKey!_insert
@[simp]
theorem getKey!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {v : β} :
(m.insert k v).getKey! k = k :=
DHashMap.getKey!_insert_self
theorem getKey!_eq_default_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α]
{a : α} : m.contains a = false m.getKey! a = default :=
DHashMap.getKey!_eq_default_of_contains_eq_false
theorem getKey!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
¬a m m.getKey! a = default :=
DHashMap.getKey!_eq_default
theorem getKey!_erase [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} :
(m.erase k).getKey! a = if k == a then default else m.getKey! a :=
DHashMap.getKey!_erase
@[simp]
theorem getKey!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} :
(m.erase k).getKey! k = default :=
DHashMap.getKey!_erase_self
theorem getKey?_eq_some_getKey!_of_contains [EquivBEq α] [LawfulHashable α] [Inhabited α]
{a : α} : m.contains a = true m.getKey? a = some (m.getKey! a) :=
DHashMap.getKey?_eq_some_getKey!_of_contains
theorem getKey?_eq_some_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
a m m.getKey? a = some (m.getKey! a) :=
DHashMap.getKey?_eq_some_getKey!
theorem getKey!_eq_get!_getKey? [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
m.getKey! a = (m.getKey? a).get! :=
DHashMap.getKey!_eq_get!_getKey?
theorem getKey_eq_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} {h'} :
m.getKey a h' = m.getKey! a :=
@DHashMap.getKey_eq_getKey! _ _ _ _ _ _ _ _ _ h'
@[simp]
theorem getKeyD_empty {a : α} {fallback : α} {c} :
(empty c : HashMap α β).getKeyD a fallback = fallback :=
DHashMap.getKeyD_empty
@[simp]
theorem getKeyD_emptyc {a : α} {fallback : α} : ( : HashMap α β).getKeyD a fallback = fallback :=
DHashMap.getKeyD_empty
theorem getKeyD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : α} :
m.isEmpty = true m.getKeyD a fallback = fallback :=
DHashMap.getKeyD_of_isEmpty
theorem getKeyD_insert [EquivBEq α] [LawfulHashable α] {k a fallback : α} {v : β} :
(m.insert k v).getKeyD a fallback = if k == a then k else m.getKeyD a fallback :=
DHashMap.getKeyD_insert
@[simp]
theorem getKeyD_insert_self [EquivBEq α] [LawfulHashable α] {k fallback : α} {v : β} :
(m.insert k v).getKeyD k fallback = k :=
DHashMap.getKeyD_insert_self
theorem getKeyD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α}
{fallback : α} : m.contains a = false m.getKeyD a fallback = fallback :=
DHashMap.getKeyD_eq_fallback_of_contains_eq_false
theorem getKeyD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback : α} :
¬a m m.getKeyD a fallback = fallback :=
DHashMap.getKeyD_eq_fallback
theorem getKeyD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : α} :
(m.erase k).getKeyD a fallback = if k == a then fallback else m.getKeyD a fallback :=
DHashMap.getKeyD_erase
@[simp]
theorem getKeyD_erase_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : α} :
(m.erase k).getKeyD k fallback = fallback :=
DHashMap.getKeyD_erase_self
theorem getKey?_eq_some_getKeyD_of_contains [EquivBEq α] [LawfulHashable α] {a : α} {fallback : α} :
m.contains a = true m.getKey? a = some (m.getKeyD a fallback) :=
DHashMap.getKey?_eq_some_getKeyD_of_contains
theorem getKey?_eq_some_getKeyD [EquivBEq α] [LawfulHashable α] {a : α} {fallback : α} :
a m m.getKey? a = some (m.getKeyD a fallback) :=
DHashMap.getKey?_eq_some_getKeyD
theorem getKeyD_eq_getD_getKey? [EquivBEq α] [LawfulHashable α] {a : α} {fallback : α} :
m.getKeyD a fallback = (m.getKey? a).getD fallback :=
DHashMap.getKeyD_eq_getD_getKey?
theorem getKey_eq_getKeyD [EquivBEq α] [LawfulHashable α] {a : α} {fallback : α} {h'} :
m.getKey a h' = m.getKeyD a fallback :=
@DHashMap.getKey_eq_getKeyD _ _ _ _ _ _ _ _ _ h'
theorem getKey!_eq_getKeyD_default [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
m.getKey! a = m.getKeyD a default :=
DHashMap.getKey!_eq_getKeyD_default
@[simp]
theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insertIfNew k v).isEmpty = false :=
@@ -464,6 +636,23 @@ theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback
if k == a ¬k m then v else m.getD a fallback :=
DHashMap.Const.getD_insertIfNew
theorem getKey?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
getKey? (m.insertIfNew k v) a = if k == a ¬k m then some k else getKey? m a :=
DHashMap.getKey?_insertIfNew
theorem getKey_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
getKey (m.insertIfNew k v) a h₁ =
if h₂ : k == a ¬k m then k else getKey m a (mem_of_mem_insertIfNew' h₁ h₂) :=
DHashMap.getKey_insertIfNew
theorem getKey!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} {v : β} :
getKey! (m.insertIfNew k v) a = if k == a ¬k m then k else getKey! m a :=
DHashMap.getKey!_insertIfNew
theorem getKeyD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a fallback : α} {v : β} :
getKeyD (m.insertIfNew k v) a fallback = if k == a ¬k m then k else getKeyD m a fallback :=
DHashMap.getKeyD_insertIfNew
@[simp]
theorem getThenInsertIfNew?_fst {k : α} {v : β} : (getThenInsertIfNew? m k v).1 = get? m k :=
DHashMap.Const.getThenInsertIfNew?_fst

View File

@@ -138,6 +138,22 @@ instance [BEq α] [Hashable α] : GetElem? (Raw α β) α β (fun m a => a ∈ m
getElem? m a := m.get? a
getElem! m a := m.get! a
@[inline, inherit_doc DHashMap.Raw.getKey?] def getKey? [BEq α] [Hashable α] (m : Raw α β) (a : α) :
Option α :=
DHashMap.Raw.getKey? m.inner a
@[inline, inherit_doc DHashMap.Raw.getKey] def getKey [BEq α] [Hashable α] (m : Raw α β) (a : α)
(h : a m) : α :=
DHashMap.Raw.getKey m.inner a h
@[inline, inherit_doc DHashMap.Raw.getKeyD] def getKeyD [BEq α] [Hashable α] (m : Raw α β) (a : α)
(fallback : α) : α :=
DHashMap.Raw.getKeyD m.inner a fallback
@[inline, inherit_doc DHashMap.Raw.getKey!] def getKey! [BEq α] [Hashable α] [Inhabited α]
(m : Raw α β) (a : α) : α :=
DHashMap.Raw.getKey! m.inner a
@[inline, inherit_doc DHashMap.Raw.erase] def erase [BEq α] [Hashable α] (m : Raw α β)
(a : α) : Raw α β :=
m.inner.erase a

View File

@@ -400,6 +400,181 @@ theorem getD_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} {fall
(hab : a == b) : m.getD a fallback = m.getD b fallback :=
DHashMap.Raw.Const.getD_congr h.out hab
@[simp]
theorem getKey?_empty {a : α} {c} : (empty c : Raw α β).getKey? a = none :=
DHashMap.Raw.getKey?_empty
@[simp]
theorem getKey?_emptyc {a : α} : ( : Raw α β).getKey? a = none :=
DHashMap.Raw.getKey?_emptyc
theorem getKey?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
m.isEmpty = true m.getKey? a = none :=
DHashMap.Raw.getKey?_of_isEmpty h.out
theorem getKey?_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} :
(m.insert k v).getKey? a = if k == a then some k else m.getKey? a :=
DHashMap.Raw.getKey?_insert h.out
@[simp]
theorem getKey?_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
(m.insert k v).getKey? k = some k :=
DHashMap.Raw.getKey?_insert_self h.out
theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
m.contains a = (m.getKey? a).isSome :=
DHashMap.Raw.contains_eq_isSome_getKey? h.out
theorem getKey?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
m.contains a = false m.getKey? a = none :=
DHashMap.Raw.getKey?_eq_none_of_contains_eq_false h.out
theorem getKey?_eq_none [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
¬a m m.getKey? a = none :=
DHashMap.Raw.getKey?_eq_none h.out
theorem getKey?_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
(m.erase k).getKey? a = if k == a then none else m.getKey? a :=
DHashMap.Raw.getKey?_erase h.out
@[simp]
theorem getKey?_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
(m.erase k).getKey? k = none :=
DHashMap.Raw.getKey?_erase_self h.out
theorem getKey_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} {h₁} :
(m.insert k v).getKey a h₁ =
if h₂ : k == a then k else m.getKey a (mem_of_mem_insert h h₁ (Bool.eq_false_iff.2 h₂)) :=
DHashMap.Raw.getKey_insert (h₁ := h₁) h.out
@[simp]
theorem getKey_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
(m.insert k v).getKey k (mem_insert_self h) = k :=
DHashMap.Raw.getKey_insert_self h.out
@[simp]
theorem getKey_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {h'} :
(m.erase k).getKey a h' = m.getKey a (mem_of_mem_erase h h') :=
DHashMap.Raw.getKey_erase (h' := h') h.out
theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {h' : a m} :
m.getKey? a = some (m.getKey a h') :=
@DHashMap.Raw.getKey?_eq_some_getKey _ _ _ _ _ _ _ h.out _ h'
@[simp]
theorem getKey!_empty [Inhabited α] {a : α} {c} : (empty c : Raw α β).getKey! a = default :=
DHashMap.Raw.getKey!_empty
@[simp]
theorem getKey!_emptyc [Inhabited α] {a : α} : ( : Raw α β).getKey! a = default :=
DHashMap.Raw.getKey!_emptyc
theorem getKey!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
m.isEmpty = true m.getKey! a = default :=
DHashMap.Raw.getKey!_of_isEmpty h.out
theorem getKey!_insert [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k a : α} {v : β} :
(m.insert k v).getKey! a = if k == a then k else m.getKey! a :=
DHashMap.Raw.getKey!_insert h.out
@[simp]
theorem getKey!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k : α}
{v : β} : (m.insert k v).getKey! k = k :=
DHashMap.Raw.getKey!_insert_self h.out
theorem getKey!_eq_default_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α]
(h : m.WF) {a : α} : m.contains a = false m.getKey! a = default :=
DHashMap.Raw.getKey!_eq_default_of_contains_eq_false h.out
theorem getKey!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
¬a m m.getKey! a = default :=
DHashMap.Raw.getKey!_eq_default h.out
theorem getKey!_erase [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k a : α} :
(m.erase k).getKey! a = if k == a then default else m.getKey! a :=
DHashMap.Raw.getKey!_erase h.out
@[simp]
theorem getKey!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k : α} :
(m.erase k).getKey! k = default :=
DHashMap.Raw.getKey!_erase_self h.out
theorem getKey?_eq_some_getKey!_of_contains [EquivBEq α] [LawfulHashable α] [Inhabited α]
(h : m.WF) {a : α} : m.contains a = true m.getKey? a = some (m.getKey! a) :=
DHashMap.Raw.getKey?_eq_some_getKey!_of_contains h.out
theorem getKey?_eq_some_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
a m m.getKey? a = some (m.getKey! a) :=
DHashMap.Raw.getKey?_eq_some_getKey! h.out
theorem getKey!_eq_get!_getKey? [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
m.getKey! a = (m.getKey? a).get! :=
DHashMap.Raw.getKey!_eq_get!_getKey? h.out
theorem getKey_eq_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} {h'} :
m.getKey a h' = m.getKey! a :=
DHashMap.Raw.getKey_eq_getKey! h.out
@[simp]
theorem getKeyD_empty {a fallback : α} {c} :
(empty c : Raw α β).getKeyD a fallback = fallback :=
DHashMap.Raw.getKeyD_empty
@[simp]
theorem getKeyD_emptyc {a fallback : α} : ( : Raw α β).getKeyD a fallback = fallback :=
DHashMap.Raw.getKeyD_empty
theorem getKeyD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
m.isEmpty = true m.getKeyD a fallback = fallback :=
DHashMap.Raw.getKeyD_of_isEmpty h.out
theorem getKeyD_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α} {v : β} :
(m.insert k v).getKeyD a fallback = if k == a then k else m.getKeyD a fallback :=
DHashMap.Raw.getKeyD_insert h.out
@[simp]
theorem getKeyD_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k fallback : α} {v : β} :
(m.insert k v).getKeyD k fallback = k :=
DHashMap.Raw.getKeyD_insert_self h.out
theorem getKeyD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF)
{a fallback : α} : m.contains a = false m.getKeyD a fallback = fallback :=
DHashMap.Raw.getKeyD_eq_fallback_of_contains_eq_false h.out
theorem getKeyD_eq_fallback [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
¬a m m.getKeyD a fallback = fallback :=
DHashMap.Raw.getKeyD_eq_fallback h.out
theorem getKeyD_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α} :
(m.erase k).getKeyD a fallback = if k == a then fallback else m.getKeyD a fallback :=
DHashMap.Raw.getKeyD_erase h.out
@[simp]
theorem getKeyD_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k fallback : α} :
(m.erase k).getKeyD k fallback = fallback :=
DHashMap.Raw.getKeyD_erase_self h.out
theorem getKey?_eq_some_getKeyD_of_contains [EquivBEq α] [LawfulHashable α] (h : m.WF)
{a fallback : α} : m.contains a = true m.getKey? a = some (m.getKeyD a fallback) :=
DHashMap.Raw.getKey?_eq_some_getKeyD_of_contains h.out
theorem getKey?_eq_some_getKeyD [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
a m m.getKey? a = some (m.getKeyD a fallback) :=
DHashMap.Raw.getKey?_eq_some_getKeyD h.out
theorem getKeyD_eq_getD_getKey? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
m.getKeyD a fallback = (m.getKey? a).getD fallback :=
DHashMap.Raw.getKeyD_eq_getD_getKey? h.out
theorem getKey_eq_getKeyD [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} {h'} :
m.getKey a h' = m.getKeyD a fallback :=
@DHashMap.Raw.getKey_eq_getKeyD _ _ _ _ _ _ _ h.out _ _ h'
theorem getKey!_eq_getKeyD_default [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF)
{a : α} :
m.getKey! a = m.getKeyD a default :=
DHashMap.Raw.getKey!_eq_getKeyD_default h.out
@[simp]
theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
(m.insertIfNew k v).isEmpty = false :=
@@ -473,6 +648,24 @@ theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α}
if k == a ¬k m then v else m.getD a fallback :=
DHashMap.Raw.Const.getD_insertIfNew h.out
theorem getKey?_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} :
(m.insertIfNew k v).getKey? a = if k == a ¬k m then some k else m.getKey? a :=
DHashMap.Raw.getKey?_insertIfNew h.out
theorem getKey_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} {h₁} :
(m.insertIfNew k v).getKey a h₁ =
if h₂ : k == a ¬k m then k else m.getKey a (mem_of_mem_insertIfNew' h h₁ h₂) :=
DHashMap.Raw.getKey_insertIfNew h.out
theorem getKey!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k a : α} {v : β} :
(m.insertIfNew k v).getKey! a = if k == a ¬k m then k else m.getKey! a :=
DHashMap.Raw.getKey!_insertIfNew h.out
theorem getKeyD_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α} {v : β} :
(m.insertIfNew k v).getKeyD a fallback = if k == a ¬k m then k else m.getKeyD a fallback :=
DHashMap.Raw.getKeyD_insertIfNew h.out
@[simp]
theorem getThenInsertIfNew?_fst (h : m.WF) {k : α} {v : β} :
(getThenInsertIfNew? m k v).1 = get? m k :=

View File

@@ -112,6 +112,34 @@ instance [BEq α] [Hashable α] {m : HashSet α} {a : α} : Decidable (a ∈ m)
@[inline] def size (m : HashSet α) : Nat :=
m.inner.size
/--
Checks if given key is contained and returns the key if it is, otherwise `none`.
The result in the `some` case is guaranteed to be pointer equal to the key in the set.
-/
@[inline] def get? (m : HashSet α) (a : α) : Option α :=
m.inner.getKey? a
/--
Retrieves the key from the set that matches `a`. Ensures that such a key exists by requiring a proof
of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the set.
-/
@[inline] def get [BEq α] [Hashable α] (m : HashSet α) (a : α) (h : a m) : α :=
m.inner.getKey a h
/--
Checks if given key is contained and returns the key if it is, otherwise `fallback`.
If they key is contained the result is guaranteed to be pointer equal to the key in the set.
-/
@[inline] def getD [BEq α] [Hashable α] (m : HashSet α) (a : α) (fallback : α) : α :=
m.inner.getKeyD a fallback
/--
Checks if given key is contained and returns the key if it is, otherwise panics.
If no panic occurs the result is guaranteed to be pointer equal to the key in the set.
-/
@[inline] def get! [BEq α] [Hashable α] [Inhabited α] (m : HashSet α) (a : α) : α :=
m.inner.getKey! a
/--
Returns `true` if the hash set contains no elements.

View File

@@ -106,6 +106,18 @@ theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
a m.insert k (k == a) = false a m :=
HashMap.mem_of_mem_insertIfNew
/-- This is a restatement of `contains_insert` that is written to exactly match the proof
obligation in the statement of `get_insert`. -/
theorem contains_of_contains_insert' [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.insert k).contains a ¬((k == a) m.contains k = false) m.contains a :=
HashMap.contains_of_contains_insertIfNew'
/-- This is a restatement of `mem_insert` that is written to exactly match the proof obligation
in the statement of `get_insert`. -/
theorem mem_of_mem_insert' [EquivBEq α] [LawfulHashable α] {k a : α} :
a m.insert k ¬((k == a) ¬k m) a m :=
DHashMap.mem_of_mem_insertIfNew'
@[simp]
theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.insert k).contains k :=
HashMap.contains_insertIfNew_self
@@ -177,6 +189,158 @@ theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
m.size (m.erase k).size + 1 :=
HashMap.size_le_size_erase
@[simp]
theorem get?_empty {a : α} {c} : (empty c : HashSet α).get? a = none :=
HashMap.getKey?_empty
@[simp]
theorem get?_emptyc {a : α} : ( : HashSet α).get? a = none :=
HashMap.getKey?_emptyc
theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
m.isEmpty = true m.get? a = none :=
HashMap.getKey?_of_isEmpty
theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.insert k).get? a = if k == a ¬k m then some k else m.get? a :=
HashMap.getKey?_insertIfNew
theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = (m.get? a).isSome :=
HashMap.contains_eq_isSome_getKey?
theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = false m.get? a = none :=
HashMap.getKey?_eq_none_of_contains_eq_false
theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a m m.get? a = none :=
HashMap.getKey?_eq_none
theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k).get? a = if k == a then none else m.get? a :=
HashMap.getKey?_erase
@[simp]
theorem get?_erase_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).get? k = none :=
HashMap.getKey?_erase_self
theorem get_insert [EquivBEq α] [LawfulHashable α] {k a : α} {h₁} :
(m.insert k).get a h₁ =
if h₂ : k == a ¬k m then k else m.get a (mem_of_mem_insert' h₁ h₂) :=
HashMap.getKey_insertIfNew (h₁ := h₁)
@[simp]
theorem get_erase [EquivBEq α] [LawfulHashable α] {k a : α} {h'} :
(m.erase k).get a h' = m.get a (mem_of_mem_erase h') :=
HashMap.getKey_erase (h' := h')
theorem get?_eq_some_get [EquivBEq α] [LawfulHashable α] {a : α} {h' : a m} :
m.get? a = some (m.get a h') :=
@HashMap.getKey?_eq_some_getKey _ _ _ _ _ _ _ _ h'
@[simp]
theorem get!_empty [Inhabited α] {a : α} {c} : (empty c : HashSet α).get! a = default :=
HashMap.getKey!_empty
@[simp]
theorem get!_emptyc [Inhabited α] {a : α} : ( : HashSet α).get! a = default :=
HashMap.getKey!_emptyc
theorem get!_of_isEmpty [Inhabited α] [EquivBEq α] [LawfulHashable α] {a : α} :
m.isEmpty = true m.get! a = default :=
HashMap.getKey!_of_isEmpty
theorem get!_insert [Inhabited α] [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.insert k).get! a = if k == a ¬k m then k else m.get! a :=
HashMap.getKey!_insertIfNew
theorem get!_eq_default_of_contains_eq_false [Inhabited α] [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = false m.get! a = default :=
HashMap.getKey!_eq_default_of_contains_eq_false
theorem get!_eq_default [Inhabited α] [EquivBEq α] [LawfulHashable α] {a : α} :
¬a m m.get! a = default :=
HashMap.getKey!_eq_default
theorem get!_erase [Inhabited α] [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k).get! a = if k == a then default else m.get! a :=
HashMap.getKey!_erase
@[simp]
theorem get!_erase_self [Inhabited α] [EquivBEq α] [LawfulHashable α] {k : α} :
(m.erase k).get! k = default :=
HashMap.getKey!_erase_self
theorem get?_eq_some_get!_of_contains [EquivBEq α] [LawfulHashable α] [Inhabited α]
{a : α} : m.contains a = true m.get? a = some (m.get! a) :=
HashMap.getKey?_eq_some_getKey!_of_contains
theorem get?_eq_some_get! [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
a m m.get? a = some (m.get! a) :=
HashMap.getKey?_eq_some_getKey!
theorem get!_eq_get!_get? [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
m.get! a = (m.get? a).get! :=
HashMap.getKey!_eq_get!_getKey?
theorem get_eq_get! [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} {h'} :
m.get a h' = m.get! a :=
HashMap.getKey_eq_getKey!
@[simp]
theorem getD_empty {a fallback : α} {c} : (empty c : HashSet α).getD a fallback = fallback :=
HashMap.getKeyD_empty
@[simp]
theorem getD_emptyc {a fallback : α} : ( : HashSet α).getD a fallback = fallback :=
HashMap.getKeyD_emptyc
theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a fallback : α} :
m.isEmpty = true m.getD a fallback = fallback :=
HashMap.getKeyD_of_isEmpty
theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a fallback : α} :
(m.insert k).getD a fallback = if k == a ¬k m then k else m.getD a fallback :=
HashMap.getKeyD_insertIfNew
theorem getD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
{a fallback : α} :
m.contains a = false m.getD a fallback = fallback :=
HashMap.getKeyD_eq_fallback_of_contains_eq_false
theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a fallback : α} :
¬a m m.getD a fallback = fallback :=
HashMap.getKeyD_eq_fallback
theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a fallback : α} :
(m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback :=
HashMap.getKeyD_erase
@[simp]
theorem getD_erase_self [EquivBEq α] [LawfulHashable α] {k fallback : α} :
(m.erase k).getD k fallback = fallback :=
HashMap.getKeyD_erase_self
theorem get?_eq_some_getD_of_contains [EquivBEq α] [LawfulHashable α] {a fallback : α} :
m.contains a = true m.get? a = some (m.getD a fallback) :=
HashMap.getKey?_eq_some_getKeyD_of_contains
theorem get?_eq_some_getD [EquivBEq α] [LawfulHashable α] {a fallback : α} :
a m m.get? a = some (m.getD a fallback) :=
HashMap.getKey?_eq_some_getKeyD
theorem getD_eq_getD_get? [EquivBEq α] [LawfulHashable α] {a fallback : α} :
m.getD a fallback = (m.get? a).getD fallback :=
HashMap.getKeyD_eq_getD_getKey?
theorem get_eq_getD [EquivBEq α] [LawfulHashable α] {a fallback : α} {h'} :
m.get a h' = m.getD a fallback :=
@HashMap.getKey_eq_getKeyD _ _ _ _ _ _ _ _ _ h'
theorem get!_eq_getD_default [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
m.get! a = m.getD a default :=
HashMap.getKey!_eq_getKeyD_default
@[simp]
theorem containsThenInsert_fst {k : α} : (m.containsThenInsert k).1 = m.contains k :=
HashMap.containsThenInsertIfNew_fst

View File

@@ -14,7 +14,7 @@ set with unbundled well-formedness invariant.
This version is safe to use in nested inductive types. The well-formedness predicate is
available as `Std.Data.HashSet.Raw.WF` and we prove in this file that all operations preserve
well-formedness. When in doubt, prefer `HashSet` over `DHashSet.Raw`.
well-formedness. When in doubt, prefer `HashSet` over `HashSet.Raw`.
Lemmas about the operations on `Std.Data.HashSet.Raw` are available in the module
`Std.Data.HashSet.RawLemmas`.
@@ -113,6 +113,34 @@ instance [BEq α] [Hashable α] {m : Raw α} {a : α} : Decidable (a ∈ m) :=
@[inline] def size (m : Raw α) : Nat :=
m.inner.size
/--
Checks if given key is contained and returns the key if it is, otherwise `none`.
The result in the `some` case is guaranteed to be pointer equal to the key in the map.
-/
@[inline] def get? [BEq α] [Hashable α] (m : Raw α) (a : α) : Option α :=
m.inner.getKey? a
/--
Retrieves the key from the set that matches `a`. Ensures that such a key exists by requiring a proof
of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the set.
-/
@[inline] def get [BEq α] [Hashable α] (m : Raw α) (a : α) (h : a m) : α :=
m.inner.getKey a h
/--
Checks if given key is contained and returns the key if it is, otherwise `fallback`.
If they key is contained the result is guaranteed to be pointer equal to the key in the set.
-/
@[inline] def getD [BEq α] [Hashable α] (m : Raw α) (a : α) (fallback : α) : α :=
m.inner.getKeyD a fallback
/--
Checks if given key is contained and returns the key if it is, otherwise panics.
If no panic occurs the result is guaranteed to be pointer equal to the key in the set.
-/
@[inline] def get! [BEq α] [Hashable α] [Inhabited α] (m : Raw α) (a : α) : α :=
m.inner.getKey! a
/--
Returns `true` if the hash set contains no elements.

View File

@@ -122,6 +122,18 @@ theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α
a m.insert k (k == a) = false a m :=
HashMap.Raw.mem_of_mem_insertIfNew h.out
/-- This is a restatement of `contains_insert` that is written to exactly match the proof
obligation in the statement of `get_insert`. -/
theorem contains_of_contains_insert' [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
(m.insert k).contains a ¬((k == a) m.contains k = false) m.contains a :=
HashMap.Raw.contains_of_contains_insertIfNew' h.out
/-- This is a restatement of `mem_insert` that is written to exactly match the proof obligation
in the statement of `get_insertIfNew`. -/
theorem mem_of_mem_insert' [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
a m.insert k ¬((k == a) ¬k m) a m :=
HashMap.Raw.mem_of_mem_insertIfNew' h.out
@[simp]
theorem contains_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
(m.insert k).contains k :=
@@ -186,6 +198,162 @@ theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α}
m.size (m.erase k).size + 1 :=
HashMap.Raw.size_le_size_erase h.out
@[simp]
theorem get?_empty {a : α} {c} : (empty c : Raw α).get? a = none :=
HashMap.Raw.getKey?_empty
@[simp]
theorem get?_emptyc {a : α} : ( : Raw α).get? a = none :=
HashMap.Raw.getKey?_emptyc
theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
m.isEmpty = true m.get? a = none :=
HashMap.Raw.getKey?_of_isEmpty h.out
theorem get?_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
(m.insert k).get? a = if k == a ¬k m then some k else m.get? a :=
HashMap.Raw.getKey?_insertIfNew h.out
theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
m.contains a = (m.get? a).isSome :=
HashMap.Raw.contains_eq_isSome_getKey? h.out
theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
m.contains a = false m.get? a = none :=
HashMap.Raw.getKey?_eq_none_of_contains_eq_false h.out
theorem get?_eq_none [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
¬a m m.get? a = none :=
HashMap.Raw.getKey?_eq_none h.out
theorem get?_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
(m.erase k).get? a = if k == a then none else m.get? a :=
HashMap.Raw.getKey?_erase h.out
theorem get_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {h₁} :
(m.insert k).get a h₁ =
if h₂ : k == a ¬k m then k else m.get a (mem_of_mem_insert' h h₁ h₂) :=
HashMap.Raw.getKey_insertIfNew (h₁ := h₁) h.out
@[simp]
theorem get_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {h'} :
(m.erase k).get a h' = m.get a (mem_of_mem_erase h h') :=
HashMap.Raw.getKey_erase (h' := h') h.out
theorem get?_eq_some_get [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {h' : a m} :
m.get? a = some (m.get a h') :=
@HashMap.Raw.getKey?_eq_some_getKey _ _ _ _ _ _ _ h.out _ h'
@[simp]
theorem get?_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
(m.erase k).get? k = none :=
HashMap.Raw.getKey?_erase_self h.out
@[simp]
theorem get!_empty [Inhabited α] {a : α} {c} : (empty c : Raw α).get! a = default :=
HashMap.Raw.getKey!_empty
@[simp]
theorem get!_emptyc [Inhabited α] {a : α} : ( : Raw α).get! a = default :=
HashMap.Raw.getKey!_emptyc
theorem get!_of_isEmpty [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
m.isEmpty = true m.get! a = default :=
HashMap.Raw.getKey!_of_isEmpty h.out
theorem get!_insert [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
(m.insert k).get! a = if k == a ¬k m then k else m.get! a :=
HashMap.Raw.getKey!_insertIfNew h.out
theorem get!_eq_default_of_contains_eq_false [Inhabited α] [EquivBEq α] [LawfulHashable α]
(h : m.WF) {a : α} :
m.contains a = false m.get! a = default :=
HashMap.Raw.getKey!_eq_default_of_contains_eq_false h.out
theorem get!_eq_default [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
¬a m m.get! a = default :=
HashMap.Raw.getKey!_eq_default h.out
theorem get!_erase [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
(m.erase k).get! a = if k == a then default else m.get! a :=
HashMap.Raw.getKey!_erase h.out
@[simp]
theorem get!_erase_self [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
(m.erase k).get! k = default :=
HashMap.Raw.getKey!_erase_self h.out
theorem get?_eq_some_get!_of_contains [EquivBEq α] [LawfulHashable α] [Inhabited α]
(h : m.WF) {a : α} : m.contains a = true m.get? a = some (m.get! a) :=
HashMap.Raw.getKey?_eq_some_getKey!_of_contains h.out
theorem get?_eq_some_get! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
a m m.get? a = some (m.get! a) :=
HashMap.Raw.getKey?_eq_some_getKey! h.out
theorem get!_eq_get!_get? [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
m.get! a = (m.get? a).get! :=
HashMap.Raw.getKey!_eq_get!_getKey? h.out
theorem get_eq_get! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} {h'} :
m.get a h' = m.get! a :=
HashMap.Raw.getKey_eq_getKey! h.out
@[simp]
theorem getD_empty {a fallback : α} {c} : (empty c : Raw α).getD a fallback = fallback :=
HashMap.Raw.getKeyD_empty
@[simp]
theorem getD_emptyc {a fallback : α} : ( : Raw α).getD a fallback = fallback :=
HashMap.Raw.getKeyD_emptyc
theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
m.isEmpty = true m.getD a fallback = fallback :=
HashMap.Raw.getKeyD_of_isEmpty h.out
theorem getD_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α} :
(m.insert k).getD a fallback = if k == a ¬k m then k else m.getD a fallback :=
HashMap.Raw.getKeyD_insertIfNew h.out
theorem getD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF)
{a fallback : α} :
m.contains a = false m.getD a fallback = fallback :=
HashMap.Raw.getKeyD_eq_fallback_of_contains_eq_false h.out
theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
¬a m m.getD a fallback = fallback :=
HashMap.Raw.getKeyD_eq_fallback h.out
theorem getD_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α} :
(m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback :=
HashMap.Raw.getKeyD_erase h.out
@[simp]
theorem getD_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k fallback : α} :
(m.erase k).getD k fallback = fallback :=
HashMap.Raw.getKeyD_erase_self h.out
theorem get?_eq_some_getD_of_contains [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α}
{fallback : α} : m.contains a = true m.get? a = some (m.getD a fallback) :=
HashMap.Raw.getKey?_eq_some_getKeyD_of_contains h.out
theorem get?_eq_some_getD [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : α} :
a m m.get? a = some (m.getD a fallback) :=
HashMap.Raw.getKey?_eq_some_getKeyD h.out
theorem getD_eq_getD_get? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : α} :
m.getD a fallback = (m.get? a).getD fallback :=
HashMap.Raw.getKeyD_eq_getD_getKey? h.out
theorem get_eq_getD [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : α} {h'} :
m.get a h' = m.getD a fallback :=
@HashMap.Raw.getKey_eq_getKeyD _ _ _ _ _ _ _ h.out _ _ h'
theorem get!_eq_getD_default [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF)
{a : α} :
m.get! a = m.getD a default :=
HashMap.Raw.getKey!_eq_getKeyD_default h.out
@[simp]
theorem containsThenInsert_fst (h : m.WF) {k : α} : (m.containsThenInsert k).1 = m.contains k :=
HashMap.Raw.containsThenInsertIfNew_fst h.out

View File

@@ -0,0 +1,31 @@
-- When the elaborator doesn't provide `CompletionInfo`, try to provide identifier completions.
-- As of when this test case was written, the elaborator did not provide `CompletionInfo` in these cases.
-- https://github.com/leanprover/lean4/issues/5172
inductive Direction where
| up
| right
| down
| left
deriving Repr
def angle (d: Direction) :=
match d with
| Direction. => 90
--^ textDocument/completion
| Direction.right => 0
| Direction.down => 270
| Direction.left => 180
-- Ensure that test is stable when changes to the `And` namespace are made.
structure CustomAnd (a b : Prop) : Prop where
ha : a
hb : b
example : p (q r) CustomAnd (p q) (p r) := by
intro h
cases h with
| inl hp => apply CustomAnd. (Or.intro_left q hp) (Or.intro_left r hp)
--^ textDocument/completion
| inr hqr => apply CustomAnd.mk (Or.intro_right p hqr.left) (Or.intro_right p hqr.right)

View File

@@ -0,0 +1,80 @@
{"textDocument": {"uri": "file:///completionFallback.lean"},
"position": {"line": 14, "character": 14}}
{"items":
[{"sortText": "0",
"label": "down",
"kind": 4,
"data":
{"params":
{"textDocument": {"uri": "file:///completionFallback.lean"},
"position": {"line": 14, "character": 14}},
"id": {"const": {"declName": "Direction.down"}}}},
{"sortText": "1",
"label": "left",
"kind": 4,
"data":
{"params":
{"textDocument": {"uri": "file:///completionFallback.lean"},
"position": {"line": 14, "character": 14}},
"id": {"const": {"declName": "Direction.left"}}}},
{"sortText": "2",
"label": "noConfusionType",
"kind": 3,
"data":
{"params":
{"textDocument": {"uri": "file:///completionFallback.lean"},
"position": {"line": 14, "character": 14}},
"id": {"const": {"declName": "Direction.noConfusionType"}}}},
{"sortText": "3",
"label": "right",
"kind": 4,
"data":
{"params":
{"textDocument": {"uri": "file:///completionFallback.lean"},
"position": {"line": 14, "character": 14}},
"id": {"const": {"declName": "Direction.right"}}}},
{"sortText": "4",
"label": "toCtorIdx",
"kind": 3,
"data":
{"params":
{"textDocument": {"uri": "file:///completionFallback.lean"},
"position": {"line": 14, "character": 14}},
"id": {"const": {"declName": "Direction.toCtorIdx"}}}},
{"sortText": "5",
"label": "up",
"kind": 4,
"data":
{"params":
{"textDocument": {"uri": "file:///completionFallback.lean"},
"position": {"line": 14, "character": 14}},
"id": {"const": {"declName": "Direction.up"}}}}],
"isIncomplete": true}
{"textDocument": {"uri": "file:///completionFallback.lean"},
"position": {"line": 28, "character": 30}}
{"items":
[{"sortText": "0",
"label": "ha",
"kind": 5,
"data":
{"params":
{"textDocument": {"uri": "file:///completionFallback.lean"},
"position": {"line": 28, "character": 30}},
"id": {"const": {"declName": "CustomAnd.ha"}}}},
{"sortText": "1",
"label": "hb",
"kind": 5,
"data":
{"params":
{"textDocument": {"uri": "file:///completionFallback.lean"},
"position": {"line": 28, "character": 30}},
"id": {"const": {"declName": "CustomAnd.hb"}}}},
{"sortText": "2",
"label": "mk",
"kind": 4,
"data":
{"params":
{"textDocument": {"uri": "file:///completionFallback.lean"},
"position": {"line": 28, "character": 30}},
"id": {"const": {"declName": "CustomAnd.mk"}}}}],
"isIncomplete": true}

View File

@@ -1,8 +0,0 @@
import Lean
open Lean Elab
def f (s : DefView) : DefView := {
m
--^ textDocument/completion
}

View File

@@ -1,3 +0,0 @@
{"textDocument": {"uri": "file:///fieldCompletion.lean"},
"position": {"line": 5, "character": 3}}
{"items": [], "isIncomplete": true}

View File

@@ -1,3 +1,8 @@
{"textDocument": {"uri": "file:///hoverException.lean"},
"position": {"line": 2, "character": 14}}
null
{"range":
{"start": {"line": 2, "character": 7}, "end": {"line": 2, "character": 18}},
"contents":
{"value":
"Explicit binder, like `(x y : A)` or `(x y)`.\nDefault values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.\n",
"kind": "markdown"}}

View File

@@ -81,3 +81,16 @@ where
--^ sync
--^ insert: " "
--^ collectDiagnostics
/-!
A reuse bug led to deletions after the header skipping a prefix of the next command on further edits
-/
-- RESET
--asdf
--^ delete: "a"
--^ sync
def f := 1 -- used to raise "unexpected identifier" after edit below because we would start parsing
-- on "ef"
def g := 2
--^ insert: "g"
--^ collectDiagnostics

View File

@@ -33,3 +33,4 @@ w
"message": "tactic 'assumption' failed\n⊢ False",
"fullRange":
{"start": {"line": 2, "character": 2}, "end": {"line": 2, "character": 9}}}]}
{"version": 3, "uri": "file:///incrementalCommand.lean", "diagnostics": []}

View File

@@ -250,8 +250,9 @@ example [ord : Ord β] (f : α → β) (x y : α) : Ordering := compare (f x) (f
example {α β} [ord : Ord β] (f : α β) (x y : α) : Ordering := compare (f x) (f y)
example {h : Decidable True} (t e : α) : ite True t e = t := if_pos trivial
@[unused_variables_ignore_fn]
def ignoreEverything : Lean.Linter.IgnoreFunction :=
fun _ _ _ => true
def ignored (x : Nat) := 0
/-!
The wildcard pattern introduces a copy of `x` that should not be linted as it is in an
inaccessible annotation.
-/
example : (x = y) y = x
| .refl _ => .refl _

View File

@@ -0,0 +1,19 @@
def f (x: Nat): Option Nat :=
if x > 10 then some 0 else none
def test (x: Nat): Nat :=
match f x, x with
| some k, _ => k
| none, 0 => 0
| none, n + 1 => test n
-- set_option trace.Meta.FunInd true
-- At the time of writing, the induction princpile misses the `f x = some k` assumptions:
/--
info: test.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), motive x) (case2 : motive 0)
(case3 : ∀ (n : Nat), motive n → motive n.succ) (x : Nat) : motive x
-/
#guard_msgs in
#check test.induct

View File

@@ -1,25 +1,62 @@
open List MergeSort Internal
-- If we omit the comparator, it is filled by the autoparam `fun a b => a ≤ b`
unseal mergeSort merge in
example : mergeSort (· ·) [3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5] = [1, 1, 2, 3, 3, 4, 5, 5, 5, 6, 9] :=
example : mergeSort [3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5] = [1, 1, 2, 3, 3, 4, 5, 5, 5, 6, 9] :=
rfl
unseal mergeSort merge in
example : mergeSort (fun x y => x/10 y/10) [3, 100 + 1, 4, 100 + 1, 5, 100 + 9, 2, 10 + 6, 5, 10 + 3, 5] = [3, 4, 5, 2, 5, 5, 16, 13, 101, 101, 109] :=
example : mergeSort [3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5] (· ·) = [1, 1, 2, 3, 3, 4, 5, 5, 5, 6, 9] :=
rfl
unseal mergeSort merge in
example : mergeSort [3, 100 + 1, 4, 100 + 1, 5, 100 + 9, 2, 10 + 6, 5, 10 + 3, 5] (fun x y => x/10 y/10) = [3, 4, 5, 2, 5, 5, 16, 13, 101, 101, 109] :=
rfl
unseal mergeSortTR.run mergeTR.go in
example : mergeSortTR (· ·) [3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5] = [1, 1, 2, 3, 3, 4, 5, 5, 5, 6, 9] :=
example : mergeSortTR [3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5] = [1, 1, 2, 3, 3, 4, 5, 5, 5, 6, 9] :=
rfl
unseal mergeSortTR.run mergeTR.go in
example : mergeSortTR (fun x y => x/10 y/10) [3, 100 + 1, 4, 100 + 1, 5, 100 + 9, 2, 10 + 6, 5, 10 + 3, 5] = [3, 4, 5, 2, 5, 5, 16, 13, 101, 101, 109] :=
example : mergeSortTR [3, 100 + 1, 4, 100 + 1, 5, 100 + 9, 2, 10 + 6, 5, 10 + 3, 5] (fun x y => x/10 y/10) = [3, 4, 5, 2, 5, 5, 16, 13, 101, 101, 109] :=
rfl
unseal mergeSortTR₂.run mergeTR.go in
example : mergeSortTR₂ (· ·) [3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5] = [1, 1, 2, 3, 3, 4, 5, 5, 5, 6, 9] :=
example : mergeSortTR₂ [3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5] = [1, 1, 2, 3, 3, 4, 5, 5, 5, 6, 9] :=
rfl
unseal mergeSortTR₂.run mergeTR.go in
example : mergeSortTR₂ (fun x y => x/10 y/10) [3, 100 + 1, 4, 100 + 1, 5, 100 + 9, 2, 10 + 6, 5, 10 + 3, 5] = [3, 4, 5, 2, 5, 5, 16, 13, 101, 101, 109] :=
example : mergeSortTR₂ [3, 100 + 1, 4, 100 + 1, 5, 100 + 9, 2, 10 + 6, 5, 10 + 3, 5] (fun x y => x/10 y/10) = [3, 4, 5, 2, 5, 5, 16, 13, 101, 101, 109] :=
rfl
/-!
# Behaviour of mergeSort when the comparator is not provided, but typeclasses are missing.
-/
inductive NoLE
| mk : NoLE
/--
error: failed to synthesize
LE NoLE
Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#guard_msgs in
example : mergeSort [NoLE.mk] = [NoLE.mk] := sorry
inductive UndecidableLE
| mk : UndecidableLE
instance : LE UndecidableLE where
le := fun _ _ => true
/--
error: type mismatch
a ≤ b
has type
Prop : Type
but is expected to have type
Bool : Type
-/
#guard_msgs in
example : mergeSort [UndecidableLE.mk] = [UndecidableLE.mk] := sorry

View File

@@ -6,7 +6,7 @@ def List.insert' (p : αα → Bool) (a : α) (bs : List α) : List α :=
def List.merge' (p : α α Bool) (as bs : List α) : List α :=
match as with
| [] => bs
| a :: as' => insert' p a (merge p as' bs)
| a :: as' => insert' p a (merge' p as' bs)
def List.split (as : List α) : List α × List α :=
match as with

View File

@@ -138,6 +138,7 @@ variable [ToString α] in
omit [ToString α] in
theorem t13 (a : α) : toString a = toString a := rfl
set_option pp.mvars false in
/--
error: application type mismatch
ToString True
@@ -146,7 +147,7 @@ argument
has type
Prop : Type
but is expected to have type
Type ?u.1758 : Type (?u.1758 + 1)
Type _ : Type (_ + 1)
-/
#guard_msgs in
omit [ToString True]

View File

@@ -10,7 +10,7 @@ out.putStrLn "print stdout"
let err IO.getStderr;
(err.putStr "print stderr" : IO Unit)
open usingIO IO
open IO
def test : IO Unit := do
FS.withFile "stdout1.txt" IO.FS.Mode.write $ fun h₁ => do