Compare commits

..

3 Commits

Author SHA1 Message Date
Kim Morrison
d6fc6e6b45 perf: parallelize rw? tactic
Use `MetaM.parIterWithCancel` to try all candidate rewrites in parallel
while preserving deterministic result ordering. When an rfl-closeable
result is found (and `stopAtRfl` is true), or the maximum number of
results is reached, remaining tasks are cancelled.

This removes the old sequential `takeListAux` implementation along with
the heartbeat-based early termination and `RewriteResultConfig` structure.

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

Co-Authored-By: Claude <noreply@anthropic.com>
2025-12-02 18:39:38 +11:00
Kim Morrison
272f0f5db3 feat: add chunked variants of parIterWithCancel
Add `parIterWithCancelChunked` functions for CoreM, MetaM, TermElabM, and TacticM that support chunking jobs into groups to reduce task creation overhead.

The original `parIterWithCancel` functions remain unchanged for backward compatibility. The new chunked variants accept `maxTasks` and `minChunkSize` parameters to control parallelism.

This enables PRs that use `parIterWithCancel` (like parallel library search and rewrites) to benefit from chunking by switching to the new `parIterWithCancelChunked` function with `maxTasks := 128`.

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

Co-Authored-By: Claude <noreply@anthropic.com>
2025-12-02 18:35:46 +11:00
Kim Morrison
1d3fda4130 feat: add chunking support to par and par' in Lean.Elab.Parallel
This PR adds optional chunking support to the `par` and `par'` functions in
`Lean.Elab.Parallel` for CoreM, MetaM, TermElabM, and TacticM. This reduces
task creation overhead when there are many small jobs by grouping them into
chunks that run sequentially within each parallel task.

New optional parameters:
- `maxTasks : Nat := 0` - Maximum number of parallel tasks (0 = no limit)
- `minChunkSize : Nat := 1` - Minimum jobs per chunk

Example: With 1000 jobs and `maxTasks := 128, minChunkSize := 8`:
- Chunk size = max(8, ceil(1000/128)) = 8
- Creates ~125 parallel tasks instead of 1000

Default behavior (maxTasks = 0) is unchanged - one task per job.

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

Co-Authored-By: Claude <noreply@anthropic.com>
2025-12-02 18:22:40 +11:00
317 changed files with 1194 additions and 4134 deletions

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

@@ -59,8 +59,38 @@ as tasks complete, unlike `par`/`par'` which restore the initial state after col
Iterators do not have `Finite` instances, as we cannot prove termination from the available
information. For consumers that require `Finite` (like `.toList`), use `.allowNontermination.toList`.
## Chunking support
The `par`, `par'`, `parIter`, and `parIterWithCancel` functions support optional chunking to reduce
task creation overhead when there are many small jobs. Pass `maxTasks` to limit the number of parallel
tasks created; jobs will be grouped into chunks that run sequentially within each task.
- `maxTasks = 0` (default): No chunking, one task per job (original behavior)
- `maxTasks > 0`: Auto-compute chunk size to limit task count
- `minChunkSize`: Minimum jobs per chunk (default 1)
Example: With 1000 jobs and `maxTasks := 128, minChunkSize := 8`, chunk size = 8, creating ~125 tasks.
-/
/-- Split a list into chunks of at most `chunkSize` elements. -/
def toChunks {α : Type} (xs : List α) (chunkSize : Nat) : List (List α) :=
if h : chunkSize 1 then xs.map ([·])
else go xs [] (Nat.lt_of_not_le h)
where
go (remaining : List α) (acc : List (List α)) (hc : 1 < chunkSize) : List (List α) :=
if _h : remaining.length chunkSize then
(remaining :: acc).reverse
else
go (remaining.drop chunkSize) (remaining.take chunkSize :: acc) hc
termination_by remaining.length
decreasing_by simp_wf; omega
/-- Compute chunk size given job count, max tasks, and minimum chunk size. -/
def computeChunkSize (numJobs maxTasks minChunkSize : Nat) : Nat :=
if maxTasks = 0 then 1
else max minChunkSize ((numJobs + maxTasks - 1) / maxTasks)
public section
namespace Std.Iterators
@@ -125,6 +155,38 @@ namespace Lean.Core.CoreM
open Std.Iterators
/--
Internal state for an iterator over chunked tasks for CoreM.
Yields individual results while internally managing chunk boundaries.
-/
private structure ChunkedTaskIterator (α : Type) where
chunkTasks : List (Task (CoreM (List (Except Exception α))))
currentResults : List (Except Exception α)
private instance {α : Type} : Iterator (ChunkedTaskIterator α) CoreM (Except Exception α) where
IsPlausibleStep _
| .yield _ _ => True
| .skip _ => True -- Allow skip for empty chunks
| .done => True
step it := do
match it.internalState.currentResults with
| r :: rest =>
pure <| .deflate .yield (toIterM { it.internalState with currentResults := rest } CoreM (Except Exception α)) r, trivial
| [] =>
match it.internalState.chunkTasks with
| [] => pure <| .deflate .done, trivial
| task :: rest =>
try
let chunkResults task.get
match chunkResults with
| [] =>
-- Empty chunk, skip to try next
pure <| .deflate .skip (toIterM { chunkTasks := rest, currentResults := [] } CoreM (Except Exception α)), trivial
| r :: rs =>
pure <| .deflate .yield (toIterM { chunkTasks := rest, currentResults := rs } CoreM (Except Exception α)) r, trivial
catch e =>
pure <| .deflate .yield (toIterM { chunkTasks := rest, currentResults := [] } CoreM (Except Exception α)) (.error e), trivial
/--
Runs a list of CoreM computations in parallel and returns:
* a combined cancellation hook for all tasks, and
@@ -150,6 +212,29 @@ def parIterWithCancel {α : Type} (jobs : List (CoreM α)) := do
pure (Except.error e)
return (combinedCancel, iterWithErrors)
/--
Runs a list of CoreM computations in parallel with chunking and returns:
* a combined cancellation hook for all tasks, and
* an iterator that yields results in original order.
Unlike `parIterWithCancel`, this groups jobs into chunks to reduce task overhead.
Each chunk runs its jobs sequentially, but chunks run in parallel.
**Parameters:**
- `maxTasks`: Maximum number of parallel tasks (chunks). Default 0 means one task per job.
- `minChunkSize`: Minimum jobs per chunk. Default 1.
-/
def parIterWithCancelChunked {α : Type} (jobs : List (CoreM α))
(maxTasks : Nat := 0) (minChunkSize : Nat := 1) := do
let chunkSize := computeChunkSize jobs.length maxTasks minChunkSize
let chunks := toChunks jobs chunkSize
let chunkJobs : List (CoreM (List (Except Exception α))) :=
chunks.map fun (chunk : List (CoreM α)) => chunk.mapM (observing ·)
let (cancels, tasks) := ( chunkJobs.mapM asTask).unzip
let combinedCancel := cancels.forM id
let flatIter := toIterM (ChunkedTaskIterator.mk tasks []) CoreM (Except Exception α)
return (combinedCancel, flatIter)
/--
Runs a list of CoreM computations in parallel (without cancellation hook).
@@ -192,19 +277,9 @@ Returns an iterator that yields results in completion order, wrapped in `Except
def parIterGreedy {α : Type} (jobs : List (CoreM α)) :=
(·.2) <$> parIterGreedyWithCancel jobs
/--
Runs a list of CoreM computations in parallel and collects results in the original order,
including the saved state after each task completes.
Unlike `parIter`, this waits for all tasks to complete and returns results
in the same order as the input list, not in completion order.
Results are wrapped in `Except Exception (α × Core.SavedState)` so that errors in individual
tasks don't stop the collection - you can observe all results including which tasks failed.
The final CoreM state is restored to the initial state (before tasks ran).
-/
def par {α : Type} (jobs : List (CoreM α)) : CoreM (List (Except Exception (α × Core.SavedState))) := do
/-- Internal: run jobs in parallel without chunking, returning state. -/
private def parCore {α : Type} (jobs : List (CoreM α)) :
CoreM (List (Except Exception (α × Core.SavedState))) := do
let initialState get
let tasks jobs.mapM asTask'
let mut results := []
@@ -218,13 +293,47 @@ def par {α : Type} (jobs : List (CoreM α)) : CoreM (List (Except Exception (α
/--
Runs a list of CoreM computations in parallel and collects results in the original order,
discarding state information.
including the saved state after each task completes.
Unlike `par`, this doesn't return state information from tasks.
Unlike `parIter`, this waits for all tasks to complete and returns results
in the same order as the input list, not in completion order.
Results are wrapped in `Except Exception (α × Core.SavedState)` so that errors in individual
tasks don't stop the collection - you can observe all results including which tasks failed.
The final CoreM state is restored to the initial state (before tasks ran).
**Chunking:** Pass `maxTasks > 0` to limit parallel tasks by grouping jobs into chunks.
-/
def par' {α : Type} (jobs : List (CoreM α)) : CoreM (List (Except Exception α)) := do
def par {α : Type} (jobs : List (CoreM α))
(maxTasks : Nat := 0) (minChunkSize : Nat := 1) :
CoreM (List (Except Exception (α × Core.SavedState))) := do
let chunkSize := computeChunkSize jobs.length maxTasks minChunkSize
if chunkSize 1 then
parCore jobs
else
let initialState get
let chunks := toChunks jobs chunkSize
let chunkJobs := chunks.map fun chunk => do
let mut results := []
for job in chunk do
let r observing do
let a job
pure (a, saveState)
results := r :: results
pure results.reverse
let chunkResults parCore chunkJobs
set initialState
let mut allResults := []
for chunkResult in chunkResults do
match chunkResult with
| .ok (jobResults, _) => allResults := allResults ++ jobResults
| .error e => allResults := allResults ++ [.error e]
return allResults
/-- Internal: run jobs in parallel without chunking, discarding state. -/
private def parCore' {α : Type} (jobs : List (CoreM α)) :
CoreM (List (Except Exception α)) := do
let initialState get
let tasks jobs.mapM asTask'
let mut results := []
@@ -237,6 +346,40 @@ def par' {α : Type} (jobs : List (CoreM α)) : CoreM (List (Except Exception α
set initialState
return results.reverse
/--
Runs a list of CoreM computations in parallel and collects results in the original order,
discarding state information.
Unlike `par`, this doesn't return state information from tasks.
The final CoreM state is restored to the initial state (before tasks ran).
**Chunking:** Pass `maxTasks > 0` to limit parallel tasks by grouping jobs into chunks.
-/
def par' {α : Type} (jobs : List (CoreM α))
(maxTasks : Nat := 0) (minChunkSize : Nat := 1) :
CoreM (List (Except Exception α)) := do
let chunkSize := computeChunkSize jobs.length maxTasks minChunkSize
if chunkSize 1 then
parCore' jobs
else
let initialState get
let chunks := toChunks jobs chunkSize
let chunkJobs := chunks.map fun chunk => do
let mut results := []
for job in chunk do
let r observing job
results := r :: results
pure results.reverse
let chunkResults parCore' chunkJobs
set initialState
let mut allResults := []
for chunkResult in chunkResults do
match chunkResult with
| .ok jobResults => allResults := allResults ++ jobResults
| .error e => allResults := allResults ++ [.error e]
return allResults
/--
Runs a list of CoreM computations in parallel and returns the first successful result
(by completion order, not list order).
@@ -260,18 +403,43 @@ namespace Lean.Meta.MetaM
open Std.Iterators
/--
Runs a list of MetaM computations in parallel and collects results in the original order,
including the saved state after each task completes.
Unlike `parIter`, this waits for all tasks to complete and returns results
in the same order as the input list, not in completion order.
Results are wrapped in `Except Exception (α × Meta.SavedState)` so that errors in individual
tasks don't stop the collection - you can observe all results including which tasks failed.
The final MetaM state is restored to the initial state (before tasks ran).
Internal state for an iterator over chunked tasks for MetaM.
Yields individual results while internally managing chunk boundaries.
-/
def par {α : Type} (jobs : List (MetaM α)) : MetaM (List (Except Exception (α × Meta.SavedState))) := do
structure ChunkedTaskIterator (α : Type) where
chunkTasks : List (Task (MetaM (List (Except Exception α))))
currentResults : List (Except Exception α)
instance {α : Type} : Iterator (ChunkedTaskIterator α) MetaM (Except Exception α) where
IsPlausibleStep _
| .yield _ _ => True
| .skip _ => True
| .done => True
step it := do
match it.internalState.currentResults with
| r :: rest =>
pure <| .deflate .yield (toIterM { it.internalState with currentResults := rest } MetaM (Except Exception α)) r, trivial
| [] =>
match it.internalState.chunkTasks with
| [] => pure <| .deflate .done, trivial
| task :: rest =>
try
let chunkResults task.get
match chunkResults with
| [] =>
pure <| .deflate .skip (toIterM { chunkTasks := rest, currentResults := [] } MetaM (Except Exception α)), trivial
| r :: rs =>
pure <| .deflate .yield (toIterM { chunkTasks := rest, currentResults := rs } MetaM (Except Exception α)) r, trivial
catch e =>
pure <| .deflate .yield (toIterM { chunkTasks := rest, currentResults := [] } MetaM (Except Exception α)) (.error e), trivial
instance {α : Type} {n : Type Type u} [Monad n] [MonadLiftT MetaM n] :
IteratorLoopPartial (ChunkedTaskIterator α) MetaM n :=
.defaultImplementation
/-- Internal: run jobs in parallel without chunking, returning state. -/
private def parCore {α : Type} (jobs : List (MetaM α)) :
MetaM (List (Except Exception (α × Meta.SavedState))) := do
let initialState get
let tasks jobs.mapM asTask'
let mut results := []
@@ -283,15 +451,9 @@ def par {α : Type} (jobs : List (MetaM α)) : MetaM (List (Except Exception (α
set initialState
return results.reverse
/--
Runs a list of MetaM computations in parallel and collects results in the original order,
discarding state information.
Unlike `par`, this doesn't return state information from tasks.
The final MetaM state is restored to the initial state (before tasks ran).
-/
def par' {α : Type} (jobs : List (MetaM α)) : MetaM (List (Except Exception α)) := do
/-- Internal: run jobs in parallel without chunking, discarding state. -/
private def parCore' {α : Type} (jobs : List (MetaM α)) :
MetaM (List (Except Exception α)) := do
let initialState get
let tasks jobs.mapM asTask'
let mut results := []
@@ -304,6 +466,80 @@ def par' {α : Type} (jobs : List (MetaM α)) : MetaM (List (Except Exception α
set initialState
return results.reverse
/--
Runs a list of MetaM computations in parallel and collects results in the original order,
including the saved state after each task completes.
Unlike `parIter`, this waits for all tasks to complete and returns results
in the same order as the input list, not in completion order.
Results are wrapped in `Except Exception (α × Meta.SavedState)` so that errors in individual
tasks don't stop the collection - you can observe all results including which tasks failed.
The final MetaM state is restored to the initial state (before tasks ran).
**Chunking:** Pass `maxTasks > 0` to limit parallel tasks by grouping jobs into chunks.
-/
def par {α : Type} (jobs : List (MetaM α))
(maxTasks : Nat := 0) (minChunkSize : Nat := 1) :
MetaM (List (Except Exception (α × Meta.SavedState))) := do
let chunkSize := computeChunkSize jobs.length maxTasks minChunkSize
if chunkSize 1 then
parCore jobs
else
let initialState get
let chunks := toChunks jobs chunkSize
let chunkJobs := chunks.map fun chunk => do
let mut results := []
for job in chunk do
let r observing do
let a job
pure (a, saveState)
results := r :: results
pure results.reverse
let chunkResults parCore chunkJobs
set initialState
let mut allResults := []
for chunkResult in chunkResults do
match chunkResult with
| .ok (jobResults, _) => allResults := allResults ++ jobResults
| .error e => allResults := allResults ++ [.error e]
return allResults
/--
Runs a list of MetaM computations in parallel and collects results in the original order,
discarding state information.
Unlike `par`, this doesn't return state information from tasks.
The final MetaM state is restored to the initial state (before tasks ran).
**Chunking:** Pass `maxTasks > 0` to limit parallel tasks by grouping jobs into chunks.
-/
def par' {α : Type} (jobs : List (MetaM α))
(maxTasks : Nat := 0) (minChunkSize : Nat := 1) :
MetaM (List (Except Exception α)) := do
let chunkSize := computeChunkSize jobs.length maxTasks minChunkSize
if chunkSize 1 then
parCore' jobs
else
let initialState get
let chunks := toChunks jobs chunkSize
let chunkJobs := chunks.map fun chunk => do
let mut results := []
for job in chunk do
let r observing job
results := r :: results
pure results.reverse
let chunkResults parCore' chunkJobs
set initialState
let mut allResults := []
for chunkResult in chunkResults do
match chunkResult with
| .ok jobResults => allResults := allResults ++ jobResults
| .error e => allResults := allResults ++ [.error e]
return allResults
/--
Runs a list of MetaM computations in parallel and returns:
* a combined cancellation hook for all tasks, and
@@ -321,7 +557,6 @@ The iterator will terminate after all jobs complete (assuming they all do comple
def parIterWithCancel {α : Type} (jobs : List (MetaM α)) := do
let (cancels, tasks) := ( jobs.mapM asTask).unzip
let combinedCancel := cancels.forM id
-- Create iterator that processes tasks sequentially
let iterWithErrors := tasks.iter.mapM fun (task : Task (MetaM α)) => do
try
let result task.get
@@ -330,6 +565,29 @@ def parIterWithCancel {α : Type} (jobs : List (MetaM α)) := do
pure (Except.error e)
return (combinedCancel, iterWithErrors)
/--
Runs a list of MetaM computations in parallel with chunking and returns:
* a combined cancellation hook for all tasks, and
* an iterator that yields results in original order.
Unlike `parIterWithCancel`, this groups jobs into chunks to reduce task overhead.
Each chunk runs its jobs sequentially, but chunks run in parallel.
**Parameters:**
- `maxTasks`: Maximum number of parallel tasks (chunks). Default 0 means one task per job.
- `minChunkSize`: Minimum jobs per chunk. Default 1.
-/
def parIterWithCancelChunked {α : Type} (jobs : List (MetaM α))
(maxTasks : Nat := 0) (minChunkSize : Nat := 1) := do
let chunkSize := computeChunkSize jobs.length maxTasks minChunkSize
let chunks := toChunks jobs chunkSize
let chunkJobs : List (MetaM (List (Except Exception α))) :=
chunks.map fun (chunk : List (MetaM α)) => chunk.mapM (observing ·)
let (cancels, tasks) := ( chunkJobs.mapM asTask).unzip
let combinedCancel := cancels.forM id
let flatIter := toIterM (ChunkedTaskIterator.mk tasks []) MetaM (Except Exception α)
return (combinedCancel, flatIter)
/--
Runs a list of MetaM computations in parallel (without cancellation hook).
@@ -394,6 +652,37 @@ namespace Lean.Elab.Term.TermElabM
open Std.Iterators
/--
Internal state for an iterator over chunked tasks for TermElabM.
Yields individual results while internally managing chunk boundaries.
-/
private structure ChunkedTaskIterator (α : Type) where
chunkTasks : List (Task (TermElabM (List (Except Exception α))))
currentResults : List (Except Exception α)
private instance {α : Type} : Iterator (ChunkedTaskIterator α) TermElabM (Except Exception α) where
IsPlausibleStep _
| .yield _ _ => True
| .skip _ => True
| .done => True
step it := do
match it.internalState.currentResults with
| r :: rest =>
pure <| .deflate .yield (toIterM { it.internalState with currentResults := rest } TermElabM (Except Exception α)) r, trivial
| [] =>
match it.internalState.chunkTasks with
| [] => pure <| .deflate .done, trivial
| task :: rest =>
try
let chunkResults task.get
match chunkResults with
| [] =>
pure <| .deflate .skip (toIterM { chunkTasks := rest, currentResults := [] } TermElabM (Except Exception α)), trivial
| r :: rs =>
pure <| .deflate .yield (toIterM { chunkTasks := rest, currentResults := rs } TermElabM (Except Exception α)) r, trivial
catch e =>
pure <| .deflate .yield (toIterM { chunkTasks := rest, currentResults := [] } TermElabM (Except Exception α)) (.error e), trivial
/--
Runs a list of TermElabM computations in parallel and returns:
* a combined cancellation hook for all tasks, and
@@ -411,7 +700,6 @@ The iterator will terminate after all jobs complete (assuming they all do comple
def parIterWithCancel {α : Type} (jobs : List (TermElabM α)) := do
let (cancels, tasks) := ( jobs.mapM asTask).unzip
let combinedCancel := cancels.forM id
-- Create iterator that processes tasks sequentially
let iterWithErrors := tasks.iter.mapM fun (task : Task (TermElabM α)) => do
try
let result task.get
@@ -420,6 +708,34 @@ def parIterWithCancel {α : Type} (jobs : List (TermElabM α)) := do
pure (Except.error e)
return (combinedCancel, iterWithErrors)
/--
Runs a list of TermElabM computations in parallel with chunking and returns:
* a combined cancellation hook for all tasks, and
* an iterator that yields results in original order.
Unlike `parIterWithCancel`, this groups jobs into chunks to reduce task overhead.
Each chunk runs its jobs sequentially, but chunks run in parallel.
**Parameters:**
- `maxTasks`: Maximum number of parallel tasks (chunks). Default 0 means one task per job.
- `minChunkSize`: Minimum jobs per chunk. Default 1.
-/
def parIterWithCancelChunked {α : Type} (jobs : List (TermElabM α))
(maxTasks : Nat := 0) (minChunkSize : Nat := 1) := do
let chunkSize := computeChunkSize jobs.length maxTasks minChunkSize
let chunks := toChunks jobs chunkSize
let chunkJobs : List (TermElabM (List (Except Exception α))) :=
chunks.map fun (chunk : List (TermElabM α)) => chunk.mapM fun job => do
try
let a job
pure (.ok a)
catch e =>
pure (.error e)
let (cancels, tasks) := ( chunkJobs.mapM asTask).unzip
let combinedCancel := cancels.forM id
let flatIter := toIterM (ChunkedTaskIterator.mk tasks []) TermElabM (Except Exception α)
return (combinedCancel, flatIter)
/--
Runs a list of TermElabM computations in parallel (without cancellation hook).
@@ -462,19 +778,9 @@ Returns an iterator that yields results in completion order, wrapped in `Except
def parIterGreedy {α : Type} (jobs : List (TermElabM α)) :=
(·.2) <$> parIterGreedyWithCancel jobs
/--
Runs a list of TermElabM computations in parallel and collects results in the original order,
including the saved state after each task completes.
Unlike `parIter`, this waits for all tasks to complete and returns results
in the same order as the input list, not in completion order.
Results are wrapped in `Except Exception (α × Term.SavedState)` so that errors in individual
tasks don't stop the collection - you can observe all results including which tasks failed.
The final TermElabM state is restored to the initial state (before tasks ran).
-/
def par {α : Type} (jobs : List (TermElabM α)) : TermElabM (List (Except Exception (α × Term.SavedState))) := do
/-- Internal: run jobs in parallel without chunking, returning state. -/
private def parCore {α : Type} (jobs : List (TermElabM α)) :
TermElabM (List (Except Exception (α × Term.SavedState))) := do
let initialState get
let tasks jobs.mapM asTask'
let mut results := []
@@ -488,15 +794,9 @@ def par {α : Type} (jobs : List (TermElabM α)) : TermElabM (List (Except Excep
set initialState
return results.reverse
/--
Runs a list of TermElabM computations in parallel and collects results in the original order,
discarding state information.
Unlike `par`, this doesn't return state information from tasks.
The final TermElabM state is restored to the initial state (before tasks ran).
-/
def par' {α : Type} (jobs : List (TermElabM α)) : TermElabM (List (Except Exception α)) := do
/-- Internal: run jobs in parallel without chunking, discarding state. -/
private def parCore' {α : Type} (jobs : List (TermElabM α)) :
TermElabM (List (Except Exception α)) := do
let initialState get
let tasks jobs.mapM asTask'
let mut results := []
@@ -509,6 +809,86 @@ def par' {α : Type} (jobs : List (TermElabM α)) : TermElabM (List (Except Exce
set initialState
return results.reverse
/--
Runs a list of TermElabM computations in parallel and collects results in the original order,
including the saved state after each task completes.
Unlike `parIter`, this waits for all tasks to complete and returns results
in the same order as the input list, not in completion order.
Results are wrapped in `Except Exception (α × Term.SavedState)` so that errors in individual
tasks don't stop the collection - you can observe all results including which tasks failed.
The final TermElabM state is restored to the initial state (before tasks ran).
**Chunking:** Pass `maxTasks > 0` to limit parallel tasks by grouping jobs into chunks.
-/
def par {α : Type} (jobs : List (TermElabM α))
(maxTasks : Nat := 0) (minChunkSize : Nat := 1) :
TermElabM (List (Except Exception (α × Term.SavedState))) := do
let chunkSize := computeChunkSize jobs.length maxTasks minChunkSize
if chunkSize 1 then
parCore jobs
else
let initialState get
let chunks := toChunks jobs chunkSize
-- Each chunk processes its jobs sequentially, collecting Except results
let chunkJobs := chunks.map fun chunk => do
let mut results : List (Except Exception (α × Term.SavedState)) := []
for job in chunk do
try
let a job
let s saveState
results := .ok (a, s) :: results
catch e =>
results := .error e :: results
pure results.reverse
let chunkResults parCore' chunkJobs
set initialState
let mut allResults := []
for chunkResult in chunkResults do
match chunkResult with
| .ok jobResults => allResults := allResults ++ jobResults
| .error e => allResults := allResults ++ [.error e]
return allResults
/--
Runs a list of TermElabM computations in parallel and collects results in the original order,
discarding state information.
Unlike `par`, this doesn't return state information from tasks.
The final TermElabM state is restored to the initial state (before tasks ran).
**Chunking:** Pass `maxTasks > 0` to limit parallel tasks by grouping jobs into chunks.
-/
def par' {α : Type} (jobs : List (TermElabM α))
(maxTasks : Nat := 0) (minChunkSize : Nat := 1) :
TermElabM (List (Except Exception α)) := do
let chunkSize := computeChunkSize jobs.length maxTasks minChunkSize
if chunkSize 1 then
parCore' jobs
else
let initialState get
let chunks := toChunks jobs chunkSize
let chunkJobs := chunks.map fun chunk => do
let mut results : List (Except Exception α) := []
for job in chunk do
try
let a job
results := .ok a :: results
catch e =>
results := .error e :: results
pure results.reverse
let chunkResults parCore' chunkJobs
set initialState
let mut allResults := []
for chunkResult in chunkResults do
match chunkResult with
| .ok jobResults => allResults := allResults ++ jobResults
| .error e => allResults := allResults ++ [.error e]
return allResults
/--
Runs a list of TermElabM computations in parallel and returns the first successful result
(by completion order, not list order).
@@ -531,6 +911,37 @@ namespace Lean.Elab.Tactic.TacticM
open Std.Iterators
/--
Internal state for an iterator over chunked tasks for TacticM.
Yields individual results while internally managing chunk boundaries.
-/
private structure ChunkedTaskIterator (α : Type) where
chunkTasks : List (Task (TacticM (List (Except Exception α))))
currentResults : List (Except Exception α)
private instance {α : Type} : Iterator (ChunkedTaskIterator α) TacticM (Except Exception α) where
IsPlausibleStep _
| .yield _ _ => True
| .skip _ => True
| .done => True
step it := do
match it.internalState.currentResults with
| r :: rest =>
pure <| .deflate .yield (toIterM { it.internalState with currentResults := rest } TacticM (Except Exception α)) r, trivial
| [] =>
match it.internalState.chunkTasks with
| [] => pure <| .deflate .done, trivial
| task :: rest =>
try
let chunkResults task.get
match chunkResults with
| [] =>
pure <| .deflate .skip (toIterM { chunkTasks := rest, currentResults := [] } TacticM (Except Exception α)), trivial
| r :: rs =>
pure <| .deflate .yield (toIterM { chunkTasks := rest, currentResults := rs } TacticM (Except Exception α)) r, trivial
catch e =>
pure <| .deflate .yield (toIterM { chunkTasks := rest, currentResults := [] } TacticM (Except Exception α)) (.error e), trivial
/--
Runs a list of TacticM computations in parallel and returns:
* a combined cancellation hook for all tasks, and
@@ -548,7 +959,6 @@ The iterator will terminate after all jobs complete (assuming they all do comple
def parIterWithCancel {α : Type} (jobs : List (TacticM α)) := do
let (cancels, tasks) := ( jobs.mapM asTask).unzip
let combinedCancel := cancels.forM id
-- Create iterator that processes tasks sequentially
let iterWithErrors := tasks.iter.mapM fun (task : Task (TacticM α)) => do
try
let result task.get
@@ -557,6 +967,34 @@ def parIterWithCancel {α : Type} (jobs : List (TacticM α)) := do
pure (Except.error e)
return (combinedCancel, iterWithErrors)
/--
Runs a list of TacticM computations in parallel with chunking and returns:
* a combined cancellation hook for all tasks, and
* an iterator that yields results in original order.
Unlike `parIterWithCancel`, this groups jobs into chunks to reduce task overhead.
Each chunk runs its jobs sequentially, but chunks run in parallel.
**Parameters:**
- `maxTasks`: Maximum number of parallel tasks (chunks). Default 0 means one task per job.
- `minChunkSize`: Minimum jobs per chunk. Default 1.
-/
def parIterWithCancelChunked {α : Type} (jobs : List (TacticM α))
(maxTasks : Nat := 0) (minChunkSize : Nat := 1) := do
let chunkSize := computeChunkSize jobs.length maxTasks minChunkSize
let chunks := toChunks jobs chunkSize
let chunkJobs : List (TacticM (List (Except Exception α))) :=
chunks.map fun (chunk : List (TacticM α)) => chunk.mapM fun job => do
try
let a job
pure (.ok a)
catch e =>
pure (.error e)
let (cancels, tasks) := ( chunkJobs.mapM asTask).unzip
let combinedCancel := cancels.forM id
let flatIter := toIterM (ChunkedTaskIterator.mk tasks []) TacticM (Except Exception α)
return (combinedCancel, flatIter)
/--
Runs a list of TacticM computations in parallel (without cancellation hook).
@@ -599,19 +1037,9 @@ Returns an iterator that yields results in completion order, wrapped in `Except
def parIterGreedy {α : Type} (jobs : List (TacticM α)) :=
(·.2) <$> parIterGreedyWithCancel jobs
/--
Runs a list of TacticM computations in parallel and collects results in the original order,
including the saved state after each task completes.
Unlike `parIter`, this waits for all tasks to complete and returns results
in the same order as the input list, not in completion order.
Results are wrapped in `Except Exception (α × Tactic.SavedState)` so that errors in individual
tasks don't stop the collection - you can observe all results including which tasks failed.
The final TacticM state is restored to the initial state (before tasks ran).
-/
def par {α : Type} (jobs : List (TacticM α)) : TacticM (List (Except Exception (α × Tactic.SavedState))) := do
/-- Internal: run jobs in parallel without chunking, returning state. -/
private def parCore {α : Type} (jobs : List (TacticM α)) :
TacticM (List (Except Exception (α × Tactic.SavedState))) := do
let initialState get
let tasks jobs.mapM asTask'
let mut results := []
@@ -625,15 +1053,9 @@ def par {α : Type} (jobs : List (TacticM α)) : TacticM (List (Except Exception
set initialState
return results.reverse
/--
Runs a list of TacticM computations in parallel and collects results in the original order,
discarding state information.
Unlike `par`, this doesn't return state information from tasks.
The final TacticM state is restored to the initial state (before tasks ran).
-/
def par' {α : Type} (jobs : List (TacticM α)) : TacticM (List (Except Exception α)) := do
/-- Internal: run jobs in parallel without chunking, discarding state. -/
private def parCore' {α : Type} (jobs : List (TacticM α)) :
TacticM (List (Except Exception α)) := do
let initialState get
let tasks jobs.mapM asTask'
let mut results := []
@@ -646,6 +1068,86 @@ def par' {α : Type} (jobs : List (TacticM α)) : TacticM (List (Except Exceptio
set initialState
return results.reverse
/--
Runs a list of TacticM computations in parallel and collects results in the original order,
including the saved state after each task completes.
Unlike `parIter`, this waits for all tasks to complete and returns results
in the same order as the input list, not in completion order.
Results are wrapped in `Except Exception (α × Tactic.SavedState)` so that errors in individual
tasks don't stop the collection - you can observe all results including which tasks failed.
The final TacticM state is restored to the initial state (before tasks ran).
**Chunking:** Pass `maxTasks > 0` to limit parallel tasks by grouping jobs into chunks.
-/
def par {α : Type} (jobs : List (TacticM α))
(maxTasks : Nat := 0) (minChunkSize : Nat := 1) :
TacticM (List (Except Exception (α × Tactic.SavedState))) := do
let chunkSize := computeChunkSize jobs.length maxTasks minChunkSize
if chunkSize 1 then
parCore jobs
else
let initialState get
let chunks := toChunks jobs chunkSize
-- Each chunk processes its jobs sequentially, collecting Except results
let chunkJobs := chunks.map fun chunk => do
let mut results : List (Except Exception (α × Tactic.SavedState)) := []
for job in chunk do
try
let a job
let s Tactic.saveState
results := .ok (a, s) :: results
catch e =>
results := .error e :: results
pure results.reverse
let chunkResults parCore' chunkJobs
set initialState
let mut allResults := []
for chunkResult in chunkResults do
match chunkResult with
| .ok jobResults => allResults := allResults ++ jobResults
| .error e => allResults := allResults ++ [.error e]
return allResults
/--
Runs a list of TacticM computations in parallel and collects results in the original order,
discarding state information.
Unlike `par`, this doesn't return state information from tasks.
The final TacticM state is restored to the initial state (before tasks ran).
**Chunking:** Pass `maxTasks > 0` to limit parallel tasks by grouping jobs into chunks.
-/
def par' {α : Type} (jobs : List (TacticM α))
(maxTasks : Nat := 0) (minChunkSize : Nat := 1) :
TacticM (List (Except Exception α)) := do
let chunkSize := computeChunkSize jobs.length maxTasks minChunkSize
if chunkSize 1 then
parCore' jobs
else
let initialState get
let chunks := toChunks jobs chunkSize
let chunkJobs := chunks.map fun chunk => do
let mut results : List (Except Exception α) := []
for job in chunk do
try
let a job
results := .ok a :: results
catch e =>
results := .error e :: results
pure results.reverse
let chunkResults parCore' chunkJobs
set initialState
let mut allResults := []
for chunkResult in chunkResults do
match chunkResult with
| .ok jobResults => allResults := allResults ++ jobResults
| .error e => allResults := allResults ++ [.error e]
return allResults
/--
Runs a list of TacticM computations in parallel and returns the first successful result
(by completion order, not list order).

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

@@ -1119,27 +1119,10 @@ If the `trace.Meta.synthInstance` option is not already set, gives a hint explai
def useTraceSynthMsg : MessageData :=
MessageData.lazy fun ctx =>
if trace.Meta.synthInstance.get ctx.opts then
pure .nil
pure ""
else
pure <| .hint' s!"Type class instance resolution failures can be inspected with the `set_option {trace.Meta.synthInstance.name} true` command."
builtin_initialize derivableRef : IO.Ref NameSet IO.mkRef {}
/--
Registers a deriving handler for the purpose of error message delivery in `synthesizeInstMVarCore`.
This should only be called by `Lean.Elab.Term.registerDerivingHandler`.
-/
def registerDerivableClass (className : Name) : IO Unit := do
unless ( initializing) do
throw (IO.userError "failed to register derivable class, it can only be registered during initialization")
derivableRef.modify fun m => m.insert className
/--
Returns whether `className` has a `deriving` handler installed.
-/
def hasDerivingHandler (className : Name) : IO Bool := do
return ( derivableRef.get).contains className
/--
Try to synthesize metavariable using type class resolution.
This method assumes the local context and local instances of `instMVar` coincide
@@ -1198,16 +1181,7 @@ def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := n
if ( read).ignoreTCFailures then
return false
else
let msg match type with
| .app (.const cls _) (.const typ _) =>
-- This has the structure of a `deriving`-style type class, alter feedback accordingly
if hasDerivingHandler cls then
pure <| extraErrorMsg ++ .hint' m!"Adding the command `deriving instance {cls} for {typ}` may allow Lean to derive the missing instance."
else
pure <| extraErrorMsg ++ useTraceSynthMsg
| _ =>
pure <| extraErrorMsg ++ useTraceSynthMsg
throwNamedError lean.synthInstanceFailed "failed to synthesize instance of type class{indentExpr type}{msg}"
throwNamedError lean.synthInstanceFailed "failed to synthesize instance of type class{indentExpr type}{extraErrorMsg}{useTraceSynthMsg}"
def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgHeader? : Option String := none)
(mkErrorMsg? : Option (MVarId (expectedType e : Expr) MetaM MessageData) := none)

View File

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

View File

@@ -8,7 +8,6 @@ module
prelude
public import Lean.ErrorExplanations.CtorResultingTypeMismatch
public import Lean.ErrorExplanations.DependsOnNoncomputable
public import Lean.ErrorExplanations.InductionWithNoAlts
public import Lean.ErrorExplanations.InductiveParamMismatch
public import Lean.ErrorExplanations.InductiveParamMissing
public import Lean.ErrorExplanations.InferBinderTypeFailed

View File

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

View File

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

View File

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

View File

@@ -927,7 +927,7 @@ where doRealize (inductName : Name) := do
-- to make sure that `target` indeed the last parameter
let e := info.value
let e lambdaTelescope e fun params body => do
if body.isAppOfArity ``WellFounded.fix 5 || body.isAppOfArity ``WellFounded.Nat.fix 4 then
if body.isAppOfArity ``WellFounded.fix 5 then
forallBoundedTelescope ( inferType body) (some 1) fun xs _ => do
unless xs.size = 1 do
throwError "functional induction: Failed to eta-expand{indentExpr e}"
@@ -935,76 +935,68 @@ where doRealize (inductName : Name) := do
else
pure e
let (e', paramMask) lambdaTelescope e fun params funBody => MatcherApp.withUserNames params varNames do
unless funBody.isApp && funBody.appFn!.isApp do
throwError "functional induction: unexpected body {funBody}"
let body := funBody.appFn!.appArg!
let target := funBody.appArg!
unless params.back! == target do
throwError "functional induction: expected the target as last parameter{indentExpr e}"
let fixedParamPerms := params.pop
let motiveType
if unfolding then
withLocalDeclD `r ( instantiateForall info.type params) fun r =>
mkForallFVars #[target, r] (.sort 0)
else
mkForallFVars #[target] (.sort 0)
withLocalDeclD `motive motiveType fun motive => do
let fn := mkAppN ( mkConstWithLevelParams name) fixedParamPerms
let isRecCall : Expr Option Expr := fun e =>
e.withApp fun f xs =>
if f.isFVarOf motive.fvarId! && xs.size > 0 then
mkApp fn xs[0]!
else
none
let motiveArg
match_expr funBody with
| fix@WellFounded.fix α _motive rel wf body target =>
unless params.back! == target do
throwError "functional induction: expected the target as last parameter{indentExpr e}"
let fixedParamPerms := params.pop
let motiveType
if unfolding then
let motiveArg := mkApp2 motive target (mkAppN ( mkConstWithLevelParams name) params)
mkLambdaFVars #[target] motiveArg
withLocalDeclD `r ( instantiateForall info.type params) fun r =>
mkForallFVars #[target, r] (.sort 0)
else
pure motive
let e' match_expr funBody with
| fix@WellFounded.fix α _motive rel wf _body _target =>
let e' := .const ``WellFounded.fix [fix.constLevels![0]!, levelZero]
pure <| mkApp4 e' α motiveArg rel wf
| fix@WellFounded.Nat.fix α _motive measure _body _target =>
let e' := .const `WellFounded.Nat.fix [fix.constLevels![0]!, levelZero]
pure <| mkApp3 e' α motiveArg measure
| _ =>
if funBody.isAppOf ``WellFounded.fix || funBody.isAppOf `WellFounded.Nat.Fix then
throwError "Function {name} defined via WellFounded.fix with unexpected arity {funBody.getAppNumArgs}:{indentExpr funBody}"
mkForallFVars #[target] (.sort 0)
withLocalDeclD `motive motiveType fun motive => do
let fn := mkAppN ( mkConstWithLevelParams name) fixedParamPerms
let isRecCall : Expr Option Expr := fun e =>
e.withApp fun f xs =>
if f.isFVarOf motive.fvarId! && xs.size > 0 then
mkApp fn xs[0]!
else
throwError "Function {name} not defined via WellFounded.fix:{indentExpr funBody}"
check e'
let (body', mvars) M2.run do
forallTelescope ( inferType e').bindingDomain! fun xs goal => do
if xs.size 2 then
throwError "expected recursor argument to take 2 parameters, got {xs}" else
let targets : Array Expr := xs[*...1]
let genIH := xs[1]!
let extraParams := xs[2...*]
-- open body with the same arg
let body instantiateLambda body targets
lambdaTelescope1 body fun oldIH body => do
let body instantiateLambda body extraParams
let body' withRewrittenMotiveArg goal (rwFun #[name]) fun goal => do
buildInductionBody #[oldIH, genIH.fvarId!] #[] goal oldIH genIH.fvarId! isRecCall body
if body'.containsFVar oldIH then
throwError m!"Did not fully eliminate `{mkFVar oldIH}` from induction principle body:{indentExpr body}"
mkLambdaFVars (targets.push genIH) ( mkLambdaFVars extraParams body')
let e' := mkApp2 e' body' target
let e' mkLambdaFVars #[target] e'
let e' abstractIndependentMVars mvars ( motive.fvarId!.getDecl).index e'
let e' mkLambdaFVars #[motive] e'
none
-- We used to pass (usedOnly := false) below in the hope that the types of the
-- induction principle match the type of the function better.
-- But this leads to avoidable parameters that make functional induction strictly less
-- useful (e.g. when the unused parameter mentions bound variables in the users' goal)
let (paramMask, e') mkLambdaFVarsMasked fixedParamPerms e'
let e' instantiateMVars e'
return (e', paramMask)
let motiveArg
if unfolding then
let motiveArg := mkApp2 motive target (mkAppN ( mkConstWithLevelParams name) params)
mkLambdaFVars #[target] motiveArg
else
pure motive
let e' := .const ``WellFounded.fix [fix.constLevels![0]!, levelZero]
let e' := mkApp4 e' α motiveArg rel wf
check e'
let (body', mvars) M2.run do
forallTelescope ( inferType e').bindingDomain! fun xs goal => do
if xs.size 2 then
throwError "expected recursor argument to take 2 parameters, got {xs}" else
let targets : Array Expr := xs[*...1]
let genIH := xs[1]!
let extraParams := xs[2...*]
-- open body with the same arg
let body instantiateLambda body targets
lambdaTelescope1 body fun oldIH body => do
let body instantiateLambda body extraParams
let body' withRewrittenMotiveArg goal (rwFun #[name]) fun goal => do
buildInductionBody #[oldIH, genIH.fvarId!] #[] goal oldIH genIH.fvarId! isRecCall body
if body'.containsFVar oldIH then
throwError m!"Did not fully eliminate `{mkFVar oldIH}` from induction principle body:{indentExpr body}"
mkLambdaFVars (targets.push genIH) ( mkLambdaFVars extraParams body')
let e' := mkApp2 e' body' target
let e' mkLambdaFVars #[target] e'
let e' abstractIndependentMVars mvars ( motive.fvarId!.getDecl).index e'
let e' mkLambdaFVars #[motive] e'
-- We used to pass (usedOnly := false) below in the hope that the types of the
-- induction principle match the type of the function better.
-- But this leads to avoidable parameters that make functional induction strictly less
-- useful (e.g. when the unused parameter mentions bound variables in the users' goal)
let (paramMask, e') mkLambdaFVarsMasked fixedParamPerms e'
let e' instantiateMVars e'
return (e', paramMask)
| _ =>
if funBody.isAppOf ``WellFounded.fix then
throwError "Function `{name}` defined via `{.ofConstName ``WellFounded.fix}` with unexpected arity {funBody.getAppNumArgs}:{indentExpr funBody}"
else
throwError "Function `{name}` not defined via `{.ofConstName ``WellFounded.fix}`:{indentExpr funBody}"
unless ( isTypeCorrect e') do
logError m!"failed to derive a type-correct induction principle:{indentExpr e'}"

View File

@@ -8,11 +8,7 @@ module
prelude
public import Lean.Meta.LazyDiscrTree
public import Lean.Meta.Tactic.SolveByElim
public import Lean.Meta.Tactic.Grind.Main
public import Lean.Util.Heartbeats
import Init.Grind.Util
import Init.Try
import Lean.Elab.Tactic.Basic
public section
@@ -40,78 +36,16 @@ builtin_initialize registerTraceClass `Tactic.librarySearch.lemmas
open SolveByElim
/--
A discharger that tries `grind` on the goal.
The proof is wrapped in `Grind.Marker` so that suggestions display `(by grind)`
instead of the complex grind proof term.
Returns `some []` if grind succeeds, `none` otherwise (leaving the goal as a subgoal).
-/
def grindDischarger (mvarId : MVarId) : MetaM (Option (List MVarId)) := do
try
-- Apply the marker wrapper, creating a subgoal for grind to solve
let type mvarId.getType
let u getLevel type
let markerExpr := mkApp (.const ``Lean.Grind.Marker [u]) type
let [subgoal] mvarId.apply markerExpr
| return none
-- Solve the subgoal with grind
let params Grind.mkParams {}
let result Grind.main subgoal params
if result.hasFailed then
return none
else
return some []
catch _ =>
return none
/--
A discharger that tries `try?` on the goal.
The proof is wrapped in `Try.Marker` so that suggestions display `(by try?)`
instead of the complex proof term.
Returns `some []` if try? succeeds, `none` otherwise (leaving the goal as a subgoal).
-/
def tryDischarger (mvarId : MVarId) : MetaM (Option (List MVarId)) := do
try
-- Apply the marker wrapper, creating a subgoal for try? to solve
let type mvarId.getType
let u getLevel type
let markerExpr := mkApp (.const ``Lean.Try.Marker [u]) type
let [subgoal] mvarId.apply markerExpr
| return none
-- Run try? via TacticM to solve the subgoal
-- We suppress the "Try this" messages since we're using try? as a discharger
let tacStx `(tactic| try?)
let remainingGoals Elab.Term.TermElabM.run' <| Elab.Tactic.run subgoal do
-- Suppress info messages from try?
let initialLog Core.getMessageLog
Elab.Tactic.evalTactic tacStx
Core.setMessageLog initialLog
if remainingGoals.isEmpty then
return some []
else
return none
catch _ =>
return none
/--
Wrapper for calling `Lean.Meta.SolveByElim.solveByElim with
appropriate arguments for library search.
If `grind` is true, `grind` will be used as a fallback discharger for subgoals
that cannot be closed by other means.
If `try?` is true, `try?` will be used as a fallback discharger (via grind internally).
-/
def solveByElim (required : List Expr) (exfalso : Bool) (goals : List MVarId)
(maxDepth : Nat) (grind : Bool := false) (try? : Bool := false) := do
def solveByElim (required : List Expr) (exfalso : Bool) (goals : List MVarId) (maxDepth : Nat) := do
let cfg : SolveByElimConfig :=
{ maxDepth, exfalso := exfalso, symm := true, commitIndependentGoals := true,
transparency := getTransparency,
-- `constructor` has been observed to significantly slow down `exact?` in Mathlib.
constructor := false }
-- Add grind or try? as a fallback discharger (tried after intro/constructor fail)
let cfg := if try? then cfg.withDischarge tryDischarger
else if grind then cfg.withDischarge grindDischarger
else cfg
let lemmas, ctx SolveByElim.mkAssumptionSet false false [] [] #[]
let cfg := if !required.isEmpty then cfg.requireUsingAll required else cfg
SolveByElim.solveByElim cfg lemmas ctx goals
@@ -356,10 +290,12 @@ private def librarySearch' (goal : MVarId)
tryOnEach act candidates
/--
Tries to solve the goal by applying a library lemma
then calling `tactic` on the resulting goals.
Tries to solve the goal either by:
* calling `tactic true`
* or applying a library lemma then calling `tactic false` on the resulting goals.
Typically here `tactic` is `solveByElim`.
Typically here `tactic` is `solveByElim`,
with the `Bool` flag indicating whether it may retry with `exfalso`.
If it successfully closes the goal, returns `none`.
Otherwise, it returns `some a`, where `a : Array (List MVarId × MetavarContext)`,
@@ -373,12 +309,13 @@ unless the goal was completely solved.)
this is not currently tracked.)
-/
def librarySearch (goal : MVarId)
(tactic : List MVarId MetaM (List MVarId) :=
fun g => solveByElim [] (maxDepth := 6) (exfalso := false) g)
(tactic : Bool List MVarId MetaM (List MVarId) :=
fun initial g => solveByElim [] (maxDepth := 6) (exfalso := initial) g)
(allowFailure : MVarId MetaM Bool := fun _ => pure true)
(leavePercentHeartbeats : Nat := 10) :
MetaM (Option (Array (List MVarId × MetavarContext))) := do
librarySearch' goal tactic allowFailure leavePercentHeartbeats
(tactic true [goal] *> pure none) <|>
librarySearch' goal (tactic false) allowFailure leavePercentHeartbeats
end LibrarySearch

View File

@@ -13,6 +13,7 @@ public import Lean.Meta.Tactic.Refl
public import Lean.Meta.Tactic.SolveByElim
public import Lean.Meta.Tactic.TryThis
public import Lean.Util.Heartbeats
public import Lean.Elab.Parallel
public section
@@ -286,61 +287,44 @@ def RewriteResult.addSuggestion (ref : Syntax) (r : RewriteResult)
(type? := r.newGoal.toLOption) (origSpan? := getRef)
(checkState? := checkState?.getD ( saveState))
structure RewriteResultConfig where
stopAtRfl : Bool
max : Nat
minHeartbeats : Nat
goal : MVarId
target : Expr
side : SideConditions := .solveByElim
mctx : MetavarContext
/--
Find lemmas which can rewrite the goal.
def takeListAux (cfg : RewriteResultConfig) (seen : Std.HashMap String Unit) (acc : Array RewriteResult)
(xs : List ((Expr Name) × Bool × Nat)) : MetaM (Array RewriteResult) := do
let mut seen := seen
let mut acc := acc
for (lem, symm, weight) in xs do
if ( getRemainingHeartbeats) < cfg.minHeartbeats then
return acc
if acc.size cfg.max then
return acc
let res
withoutModifyingState <| withMCtx cfg.mctx do
rwLemma cfg.mctx cfg.goal cfg.target cfg.side lem symm weight
match res with
| none => continue
| some r =>
let s withoutModifyingState <| withMCtx r.mctx r.ppResult
if seen.contains s then
continue
let rfl? dischargableWithRfl? r.mctx r.result.eNew
if cfg.stopAtRfl then
if rfl? then
return #[r]
else
seen := seen.insert s ()
acc := acc.push r
else
seen := seen.insert s ()
acc := acc.push r
return acc
/-- Find lemmas which can rewrite the goal. -/
Runs all candidates in parallel, iterates through results in order.
Cancels remaining tasks and returns immediately if `stopAtRfl` is true and
an rfl-closeable result is found. Collects up to `max` unique results.
-/
def findRewrites (hyps : Array (Expr × Bool × Nat))
(moduleRef : LazyDiscrTree.ModuleDiscrTreeRef (Name × RwDirection))
(goal : MVarId) (target : Expr)
(forbidden : NameSet := ) (side : SideConditions := .solveByElim)
(stopAtRfl : Bool) (max : Nat := 20)
(leavePercentHeartbeats : Nat := 10) : MetaM (List RewriteResult) := do
(stopAtRfl : Bool) (max : Nat := 20) : MetaM (List RewriteResult) := do
let mctx getMCtx
let candidates rewriteCandidates hyps moduleRef target forbidden
let minHeartbeats : Nat
if ( getMaxHeartbeats) = 0 then
pure 0
else
pure <| leavePercentHeartbeats * ( getRemainingHeartbeats) / 100
let cfg : RewriteResultConfig :=
{ stopAtRfl, minHeartbeats, max, mctx, goal, target, side }
return ( takeListAux cfg {} (Array.mkEmpty max) candidates.toList).toList
-- Create parallel jobs for each candidate
let jobs := candidates.toList.map fun (lem, symm, weight) => do
withoutModifyingState <| withMCtx mctx do
let some r rwLemma mctx goal target side lem symm weight
| return none
let s withoutModifyingState <| withMCtx r.mctx r.ppResult
return some (r, s)
let (cancel, iter) MetaM.parIterWithCancelChunked jobs (maxTasks := 128)
let mut seen : Std.HashMap String Unit := {}
let mut acc : Array RewriteResult := Array.mkEmpty max
for result in iter.allowNontermination do
if acc.size max then
cancel
break
match result with
| .error _ => continue
| .ok none => continue
| .ok (some (r, s)) =>
if seen.contains s then continue
seen := seen.insert s ()
if stopAtRfl && r.rfl? then
cancel
return [r]
acc := acc.push r
return acc.toList
end Lean.Meta.Rewrites

View File

@@ -100,12 +100,6 @@ structure SolveByElimConfig extends ApplyRulesConfig where
intro : Bool := true
/-- Try calling `constructor` if no lemmas apply. -/
constructor : Bool := true
/--
If `suggestions` is `true`, `solve_by_elim` will invoke the currently configured library
suggestion engine on the current goal, and attempt to use the resulting suggestions as
additional lemmas.
-/
suggestions : Bool := false
namespace SolveByElimConfig

View File

@@ -151,18 +151,14 @@ section Elab
-- Placed here instead of Lean.Server.Utils because of an import loop
private def mkIleanInfoNotification (method : String) (m : DocumentMeta)
(trees : Array Elab.InfoTree) : BaseIO (JsonRpc.Notification Lsp.LeanIleanInfoParams) := do
let (references, decls) findModuleRefs m.text trees (localVars := true) |>.toLspModuleRefs
let param := { version := m.version, references, decls }
let references findModuleRefs m.text trees (localVars := true) |>.toLspModuleRefs
let param := { version := m.version, references }
return { method, param }
private def mkIleanHeaderInfoNotification (m : DocumentMeta)
private def mkInitialIleanInfoUpdateNotification (m : DocumentMeta)
(directImports : Array ImportInfo) : JsonRpc.Notification Lsp.LeanILeanHeaderInfoParams :=
{ method := "$/lean/ileanHeaderInfo", param := { version := m.version, directImports } }
private def mkIleanHeaderSetupInfoNotification (m : DocumentMeta)
(isSetupFailure : Bool) : JsonRpc.Notification Lsp.LeanILeanHeaderSetupInfoParams :=
{ method := "$/lean/ileanHeaderSetupInfo", param := { version := m.version, isSetupFailure } }
private def mkIleanInfoUpdateNotification : DocumentMeta Array Elab.InfoTree
BaseIO (JsonRpc.Notification Lsp.LeanIleanInfoParams) :=
mkIleanInfoNotification "$/lean/ileanInfoUpdate"
@@ -400,7 +396,7 @@ def setupImports
return .error { diagnostics := .empty, result? := none, metaSnap := default }
let header := stx.toModuleHeader
chanOut.sync.send <| .ofMsg <| mkIleanHeaderInfoNotification doc <| collectImports stx
chanOut.sync.send <| .ofMsg <| mkInitialIleanInfoUpdateNotification doc <| collectImports stx
let fileSetupResult setupFile doc header fun stderrLine => do
let progressDiagnostic := {
range := 0, 0, 1, 0
@@ -410,9 +406,6 @@ def setupImports
message := stderrLine
}
chanOut.sync.send <| .ofMsg <| mkPublishDiagnosticsNotification doc #[progressDiagnostic]
let isSetupError := fileSetupResult.kind matches .importsOutOfDate
|| fileSetupResult.kind matches .error ..
chanOut.sync.send <| .ofMsg <| mkIleanHeaderSetupInfoNotification doc isSetupError
-- clear progress notifications in the end
chanOut.sync.send <| .ofMsg <| mkPublishDiagnosticsNotification doc #[]
match fileSetupResult.kind with

View File

@@ -59,11 +59,11 @@ private def lines (s : String) : Array String := Id.run do
let c := iter.get h
iter := iter.next h
if c == '\n' then
result := result.push <| s.extract lineStart iter
result := result.push <| lineStart.extract iter
lineStart := iter
if iter != lineStart then
result := result.push <| s.extract lineStart iter
result := result.push <| lineStart.extract iter
return result
private inductive RWState where

View File

@@ -266,12 +266,12 @@ partial def handleDocumentHighlight (p : DocumentHighlightParams)
let highlightRefs? (snaps : Array Snapshot) : IO (Option (Array DocumentHighlight)) := do
let trees := snaps.map (·.infoTree)
let (refs, _) findModuleRefs text trees |>.toLspModuleRefs
let refs : Lsp.ModuleRefs findModuleRefs text trees |>.toLspModuleRefs
let mut ranges := #[]
for ident in refs.findAt p.position (includeStop := true) do
if let some info := refs.get? ident then
if let some loc := info.definition? then
ranges := ranges.push loc.range
if let some definitionRange, _ := info.definition? then
ranges := ranges.push definitionRange
ranges := ranges.append <| info.usages.map (·.range)
if ranges.isEmpty then
return none

View File

@@ -81,12 +81,11 @@ def addRef (i : RefInfo) (ref : Reference) : RefInfo :=
| { usages, .. }, { isBinder := false, .. } =>
{ i with usages := usages.push ref }
/-- Converts `i` to a JSON-serializable `Lsp.RefInfo` and collects its decls. -/
def toLspRefInfo (i : RefInfo) : StateT Decls BaseIO Lsp.RefInfo := do
let refToRefInfoLocation (ref : Reference) : StateT Decls BaseIO RefInfo.Location := do
/-- Converts `i` to a JSON-serializable `Lsp.RefInfo`. -/
def toLspRefInfo (i : RefInfo) : BaseIO Lsp.RefInfo := do
let refToRefInfoLocation (ref : Reference) : BaseIO RefInfo.Location := do
let parentDeclName? := ref.ci.parentDecl?
let parentDeclNameString? := parentDeclName?.map (·.toString)
let .ok parentDeclInfo? EIO.toBaseIO <| ref.ci.runCoreM do
let .ok parentDeclRanges? EIO.toBaseIO <| ref.ci.runCoreM do
let some parentDeclName := parentDeclName?
| return none
-- Use `local` as it avoids unnecessary blocking, which is especially important when called
@@ -94,15 +93,17 @@ def toLspRefInfo (i : RefInfo) : StateT Decls BaseIO Lsp.RefInfo := do
-- `parentDeclName` will not be available in the current environment and we would block only
-- to return `none` in the end anyway. At the end of elaboration, we rerun this function on
-- the full info tree with the main environment, so the access will succeed immediately.
let some parentDeclRanges := declRangeExt.find? (asyncMode := .local) ( getEnv) parentDeclName
| return none
return some <| .ofDeclarationRanges parentDeclRanges
return declRangeExt.find? (asyncMode := .local) ( getEnv) parentDeclName
-- we only use `CoreM` to get access to a `MonadEnv`, but these are currently all `IO`
| unreachable!
if let some parentDeclNameString := parentDeclNameString? then
if let some parentDeclInfo := parentDeclInfo? then
modify (·.insert parentDeclNameString parentDeclInfo)
return .mk ref.range (parentDeclName?.map (·.toString))
return {
range := ref.range
parentDecl? := do
let parentDeclName parentDeclName?
let parentDeclRange := ( parentDeclRanges?).range.toLspRange
let parentDeclSelectionRange := ( parentDeclRanges?).selectionRange.toLspRange
return parentDeclName.toString, parentDeclRange, parentDeclSelectionRange
}
let definition? i.definition.mapM refToRefInfoLocation
let usages i.usages.mapM refToRefInfoLocation
return {
@@ -122,8 +123,8 @@ def addRef (self : ModuleRefs) (ref : Reference) : ModuleRefs :=
let refInfo := self.getD ref.ident RefInfo.empty
self.insert ref.ident (refInfo.addRef ref)
/-- Converts `refs` to a JSON-serializable `Lsp.ModuleRefs` and collects all decls. -/
def toLspModuleRefs (refs : ModuleRefs) : BaseIO (Lsp.ModuleRefs × Decls) := StateT.run (s := ) do
/-- Converts `refs` to a JSON-serializable `Lsp.ModuleRefs`. -/
def toLspModuleRefs (refs : ModuleRefs) : BaseIO Lsp.ModuleRefs := do
let mut refs' :=
for (k, v) in refs do
refs' := refs'.insert k ( v.toLspRefInfo)
@@ -206,15 +207,13 @@ open Elab
/-- Content of individual `.ilean` files -/
structure Ilean where
/-- Version number of the ilean format. -/
version : Nat := 5
version : Nat := 4
/-- Name of the module that this ilean data has been collected for. -/
module : Name
/-- Direct imports of the module. -/
directImports : Array Lsp.ImportInfo
/-- All references of this module. -/
references : Lsp.ModuleRefs
/-- All declarations of this module. -/
decls : Lsp.Decls
deriving FromJson, ToJson
namespace Ilean
@@ -496,8 +495,6 @@ structure LoadedILean where
directImports : DirectImports
/-- Reference information from this ILean. -/
refs : Lsp.ModuleRefs
/-- Declarations in the module of the ILean. -/
decls : Lsp.Decls
/-- Paths and module references for every module name. Loaded from `.ilean` files. -/
abbrev ILeanMap := Std.TreeMap Name LoadedILean Name.quickCmp
@@ -509,24 +506,13 @@ built.
-/
structure TransientWorkerILean where
/-- URI of the module that the file worker is associated with. -/
moduleUri : DocumentUri
moduleUri : DocumentUri
/-- Document version for which these references have been collected. -/
version : Nat
version : Nat
/-- Direct imports of the module that the file worker is associated with. -/
directImports : DirectImports
/--
Whether `lake setup-file` has failed for this worker. `none` if no setup info has been received
for this version yet.
-/
isSetupFailure? : Option Bool
directImports : DirectImports
/-- References provided by the worker. -/
refs : Lsp.ModuleRefs
/-- Declarations provided by the worker. -/
decls : Lsp.Decls
/-- Determines whether this transient worker ILean includes actual references. -/
def TransientWorkerILean.hasRefs (i : TransientWorkerILean) : Bool :=
i.isSetupFailure?.any (fun isSetupFailure => ! isSetupFailure)
refs : Lsp.ModuleRefs
/--
Document versions and module references for every module name. Loaded from the current state
@@ -562,7 +548,6 @@ def addIlean
ileanPath := path
directImports
refs := ilean.references
decls := ilean.decls
}
}
@@ -585,41 +570,14 @@ def updateWorkerImports
: IO References := do
let directImports DirectImports.convertImportInfos directImports
let some workerRefs := self.workers[name]?
| return { self with workers := self.workers.insert name { moduleUri, version, directImports, isSetupFailure? := none, refs := , decls := } }
| return { self with workers := self.workers.insert name { moduleUri, version, directImports, refs := } }
match compare version workerRefs.version with
| .lt => return self
| .gt => return { self with workers := self.workers.insert name { moduleUri, version, directImports, isSetupFailure? := none, refs := , decls := } }
| .eq =>
let isSetupFailure? := workerRefs.isSetupFailure?
let refs := workerRefs.refs
let decls := workerRefs.decls
return { self with
workers := self.workers.insert name { moduleUri, version, directImports, isSetupFailure?, refs, decls }
}
/--
Replaces the direct imports of a worker for the module `name` in `self` with
a new set of direct imports.
-/
def updateWorkerSetupInfo
(self : References)
(name : Name)
(moduleUri : DocumentUri)
(version : Nat)
(isSetupFailure : Bool)
: IO References := do
let isSetupFailure? := some isSetupFailure
let some workerRefs := self.workers[name]?
| return { self with workers := self.workers.insert name { moduleUri, version, directImports := , isSetupFailure?, refs := , decls := } }
let directImports := workerRefs.directImports
match compare version workerRefs.version with
| .lt => return self
| .gt => return { self with workers := self.workers.insert name { moduleUri, version, directImports, isSetupFailure?, refs := , decls := } }
| .gt => return { self with workers := self.workers.insert name { moduleUri, version, directImports, refs := } }
| .eq =>
let refs := workerRefs.refs
let decls := workerRefs.decls
return { self with
workers := self.workers.insert name { moduleUri, version, directImports, isSetupFailure?, refs, decls }
workers := self.workers.insert name { moduleUri, version, directImports, refs }
}
/--
@@ -633,21 +591,18 @@ def updateWorkerRefs
(moduleUri : DocumentUri)
(version : Nat)
(refs : Lsp.ModuleRefs)
(decls : Lsp.Decls)
: IO References := do
let some workerRefs := self.workers[name]?
| return { self with workers := self.workers.insert name { moduleUri, version, directImports := , isSetupFailure? := none, refs, decls } }
| return { self with workers := self.workers.insert name { moduleUri, version, directImports := , refs } }
let directImports := workerRefs.directImports
let isSetupFailure? := workerRefs.isSetupFailure?
match compare version workerRefs.version with
| .lt => return self
| .gt => return { self with workers := self.workers.insert name { moduleUri, version, directImports, isSetupFailure?, refs, decls } }
| .gt => return { self with workers := self.workers.insert name { moduleUri, version, directImports, refs } }
| .eq =>
let mergedRefs := refs.foldl (init := workerRefs.refs) fun m ident info =>
m.getD ident Lsp.RefInfo.empty |>.merge info |> m.insert ident
let mergedDecls := workerRefs.decls.insertMany decls
return { self with
workers := self.workers.insert name { moduleUri, version, directImports, isSetupFailure?, refs := mergedRefs, decls := mergedDecls }
workers := self.workers.insert name { moduleUri, version, directImports, refs := mergedRefs }
}
/--
@@ -660,17 +615,15 @@ def finalizeWorkerRefs
(moduleUri : DocumentUri)
(version : Nat)
(refs : Lsp.ModuleRefs)
(decls : Lsp.Decls)
: IO References := do
let some workerRefs := self.workers[name]?
| return { self with workers := self.workers.insert name { moduleUri, version, directImports := , isSetupFailure? := none, refs, decls } }
| return { self with workers := self.workers.insert name { moduleUri, version, directImports := , refs } }
let directImports := workerRefs.directImports
let isSetupFailure? := workerRefs.isSetupFailure?
match compare version workerRefs.version with
| .lt => return self
| .gt => return { self with workers := self.workers.insert name { moduleUri, version, directImports, isSetupFailure?, refs, decls } }
| .gt => return { self with workers := self.workers.insert name { moduleUri, version, directImports, refs} }
| .eq =>
return { self with workers := self.workers.insert name { moduleUri, version, directImports, isSetupFailure?, refs, decls } }
return { self with workers := self.workers.insert name { moduleUri, version, directImports, refs } }
/-- Erases all worker references in `self` for the worker managing `name`. -/
def removeWorkerRefs (self : References) (name : Name) : References :=
@@ -680,16 +633,12 @@ def removeWorkerRefs (self : References) (name : Name) : References :=
Map from each module to all of its references.
The current references in a file worker take precedence over those in .ilean files.
-/
abbrev AllRefsMap := Std.TreeMap Name (DocumentUri × Lsp.ModuleRefs × Lsp.Decls) Name.quickCmp
abbrev AllRefsMap := Std.TreeMap Name (DocumentUri × Lsp.ModuleRefs) Name.quickCmp
/-- Yields a map from all modules to all of their references. -/
def allRefs (self : References) : AllRefsMap :=
let ileanRefs := self.ileans.foldl (init := ) fun m name { moduleUri, refs, decls, .. } => m.insert name (moduleUri, refs, decls)
self.workers.foldl (init := ileanRefs) fun m name i@{ moduleUri, refs, decls, ..} =>
if i.hasRefs then
m.insert name (moduleUri, refs, decls)
else
m
let ileanRefs := self.ileans.foldl (init := ) fun m name { moduleUri, refs, .. } => m.insert name (moduleUri, refs)
self.workers.foldl (init := ileanRefs) fun m name { moduleUri, refs, ..} => m.insert name (moduleUri, refs)
/--
Map from each module to all of its direct imports.
@@ -710,12 +659,11 @@ def allDirectImports (self : References) : AllDirectImportsMap := Id.run do
Gets the references for `mod`.
The current references in a file worker take precedence over those in .ilean files.
-/
def getModuleRefs? (self : References) (mod : Name) : Option (DocumentUri × Lsp.ModuleRefs × Lsp.Decls) := do
def getModuleRefs? (self : References) (mod : Name) : Option (DocumentUri × Lsp.ModuleRefs) := do
if let some worker := self.workers[mod]? then
if worker.hasRefs then
return (worker.moduleUri, worker.refs, worker.decls)
return (worker.moduleUri, worker.refs)
if let some ilean := self.ileans[mod]? then
return (ilean.moduleUri, ilean.refs, ilean.decls)
return (ilean.moduleUri, ilean.refs)
none
/--
@@ -729,15 +677,6 @@ def getDirectImports? (self : References) (mod : Name) : Option DirectImports :=
return ilean.directImports
none
/-- Gets the set of declarations of `mod`. -/
def getDecls? (self : References) (mod : Name) : Option Decls := do
if let some worker := self.workers[mod]? then
if worker.hasRefs then
return worker.decls
if let some ilean := self.ileans[mod]? then
return ilean.decls
none
/--
Yields all references in `self` for `ident`, as well as the `DocumentUri` that each
reference occurs in.
@@ -745,50 +684,32 @@ reference occurs in.
def allRefsFor
(self : References)
(ident : RefIdent)
: Array (DocumentUri × Name × Lsp.RefInfo × Decls) := Id.run do
: Array (DocumentUri × Name × Lsp.RefInfo) := Id.run do
let refsToCheck := match ident with
| RefIdent.const .. => self.allRefs.toArray
| RefIdent.fvar identModule .. =>
let identModuleName := identModule.toName
match self.getModuleRefs? identModuleName with
| none => #[]
| some (moduleUri, refs, decls) => #[(identModuleName, moduleUri, refs, decls)]
| some (moduleUri, refs) => #[(identModuleName, moduleUri, refs)]
let mut result := #[]
for (module, moduleUri, refs, decls) in refsToCheck do
for (module, moduleUri, refs) in refsToCheck do
let some info := refs.get? ident
| continue
result := result.push (moduleUri, module, info, decls)
result := result.push (moduleUri, module, info)
return result
/-- Yields all references in `module` at `pos`. -/
def findAt (self : References) (module : Name) (pos : Lsp.Position) (includeStop := false) : Array RefIdent := Id.run do
if let some (_, refs, _) := self.getModuleRefs? module then
if let some (_, refs) := self.getModuleRefs? module then
return refs.findAt pos includeStop
#[]
/-- Yields the first reference in `module` at `pos`. -/
def findRange? (self : References) (module : Name) (pos : Lsp.Position) (includeStop := false) : Option Range := do
let (_, refs, _) self.getModuleRefs? module
let (_, refs) self.getModuleRefs? module
refs.findRange? pos includeStop
/-- Parent declaration of an identifier. -/
structure ParentDecl where
/-- Name of the parent declaration. -/
name : String
/-- Range of the parent declaration. -/
range : Lsp.Range
/-- Selection range of the parent declaration. -/
selectionRange : Lsp.Range
/-- Yields a `ParentDecl` for the declaration `name`. -/
def ParentDecl.ofDecls? (ds : Decls) (name : String) : Option ParentDecl := do
let d ds.get? name
return {
name
range := d.range
selectionRange := d.selectionRange
}
/-- Location and parent declaration of a reference. -/
structure DocumentRefInfo where
/-- Location of the reference. -/
@@ -796,7 +717,7 @@ structure DocumentRefInfo where
/-- Module name of the reference. -/
module : Name
/-- Parent declaration of the reference. -/
parentInfo? : Option ParentDecl
parentInfo? : Option RefInfo.ParentDecl
/-- Yields locations and parent declaration for all references referring to `ident`. -/
def referringTo
@@ -805,16 +726,12 @@ def referringTo
(includeDefinition : Bool := true)
: Array DocumentRefInfo := Id.run do
let mut result := #[]
for (moduleUri, module, info, decls) in self.allRefsFor ident do
for (moduleUri, module, info) in self.allRefsFor ident do
if includeDefinition then
if let some loc := info.definition? then
let parentDecl? := do
ParentDecl.ofDecls? decls <| loc.parentDecl?
result := result.push moduleUri, loc.range, module, parentDecl?
for loc in info.usages do
let parentDecl? := do
ParentDecl.ofDecls? decls <| loc.parentDecl?
result := result.push moduleUri, loc.range, module, parentDecl?
if let some range, parentDeclInfo? := info.definition? then
result := result.push moduleUri, range, module, parentDeclInfo?
for range, parentDeclInfo? in info.usages do
result := result.push moduleUri, range, module, parentDeclInfo?
return result
/-- Yields the definition location of `ident`. -/
@@ -822,12 +739,10 @@ def definitionOf?
(self : References)
(ident : RefIdent)
: Option DocumentRefInfo := Id.run do
for (moduleUri, module, info, decls) in self.allRefsFor ident do
let some loc := info.definition?
for (moduleUri, module, info) in self.allRefsFor ident do
let some definitionRange, definitionParentDeclInfo? := info.definition?
| continue
let definitionParentDecl? := do
ParentDecl.ofDecls? decls <| loc.parentDecl?
return some moduleUri, loc.range, module, definitionParentDecl?
return some moduleUri, definitionRange, module, definitionParentDeclInfo?
return none
/-- A match in `References.definitionsMatching`. -/
@@ -848,16 +763,16 @@ def definitionsMatching
(cancelTk? : Option CancelToken := none)
: BaseIO (Array (MatchedDefinition α)) := do
let mut result := #[]
for (module, moduleUri, refs, _) in self.allRefs do
for (module, moduleUri, refs) in self.allRefs do
if let some cancelTk := cancelTk? then
if cancelTk.isSet then
return result
for (ident, info) in refs do
let (RefIdent.const _ nameString, some loc) := (ident, info.definition?)
let (RefIdent.const _ nameString, some definitionRange, _) := (ident, info.definition?)
| continue
let some v := filterMapIdent nameString.toName
| continue
result := result.push module, moduleUri, v, loc.range
result := result.push module, moduleUri, v, definitionRange
return result
/-- Yields all imports that import the given `requestedMod`. -/

View File

@@ -533,15 +533,10 @@ section ServerM
let uri := fw.doc.uri
modifyReferencesIO (·.updateWorkerImports module uri params.version params.directImports)
def handleILeanHeaderSetupInfo (fw : FileWorker) (params : LeanILeanHeaderSetupInfoParams) : ServerM Unit := do
let module := fw.doc.mod
let uri := fw.doc.uri
modifyReferencesIO (·.updateWorkerSetupInfo module uri params.version params.isSetupFailure)
def handleIleanInfoUpdate (fw : FileWorker) (params : LeanIleanInfoParams) : ServerM Unit := do
let module := fw.doc.mod
let uri := fw.doc.uri
modifyReferencesIO (·.updateWorkerRefs module uri params.version params.references params.decls)
modifyReferencesIO (·.updateWorkerRefs module uri params.version params.references)
def handleIleanInfoFinal (fw : FileWorker) (params : LeanIleanInfoParams) : ServerM Unit := do
let s read
@@ -549,7 +544,7 @@ section ServerM
let uri := fw.doc.uri
s.referenceData.atomically do
let rd get
let rd rd.modifyReferencesM (·.finalizeWorkerRefs module uri params.version params.references params.decls)
let rd rd.modifyReferencesM (·.finalizeWorkerRefs module uri params.version params.references)
let (pendingWaitForILeanRequests, rest) := rd.pendingWaitForILeanRequests.partition (·.uri == uri)
let rd := { rd with pendingWaitForILeanRequests := rest }
let rd := rd.modifyFinalizedWorkerILeanVersions (·.insert uri params.version)
@@ -857,9 +852,6 @@ section ServerM
| .notification "$/lean/ileanHeaderInfo" =>
if let .ok params := parseNotificationParams? LeanILeanHeaderInfoParams msg then
handleILeanHeaderInfo fw params
| .notification "$/lean/ileanHeaderSetupInfo" =>
if let .ok params := parseNotificationParams? LeanILeanHeaderSetupInfoParams msg then
handleILeanHeaderSetupInfo fw params
| .notification "$/lean/ileanInfoUpdate" =>
if let .ok params := parseNotificationParams? LeanIleanInfoParams msg then
handleIleanInfoUpdate fw params
@@ -1093,19 +1085,17 @@ def handleCallHierarchyIncomingCalls (p : CallHierarchyIncomingCallsParams)
let references := ( read).references
let identRefs := references.referringTo (.const itemData.module.toString itemData.name.toString) false
let incomingCalls identRefs.mapM fun location, refModule, parentDecl? => do
let incomingCalls identRefs.filterMapM fun location, refModule, parentDecl? => do
let parentDeclNameString, parentDeclRange, parentDeclSelectionRange :=
match parentDecl? with
| some parentDecl => parentDecl
| none => "[anonymous]", location.range, location.range
let some parentDeclNameString, parentDeclRange, parentDeclSelectionRange := parentDecl?
| return none
let parentDeclName := parentDeclNameString.toName
-- Remove private header from name
let label := Lean.privateToUserName? parentDeclName |>.getD parentDeclName
return {
return some {
«from» := {
name := label.toString
kind := SymbolKind.constant
@@ -1141,14 +1131,14 @@ def handleCallHierarchyOutgoingCalls (p : CallHierarchyOutgoingCallsParams)
let references := ( read).references
let some (_, refs, _) := references.getModuleRefs? itemData.module
let some (_, refs) := references.getModuleRefs? itemData.module
| return #[]
let items refs.toArray.filterMapM fun ident, info => do
let outgoingUsages := info.usages.filter fun usage => Id.run do
let some parentDecl := usage.parentDecl?
| return false
return itemData.name == parentDecl.toName
return itemData.name == parentDecl.name.toName
let outgoingUsages := outgoingUsages.map (·.range)
if outgoingUsages.isEmpty then
@@ -1435,13 +1425,7 @@ section MessageHandling
| "$/lean/waitForILeans" =>
let rd ctx.referenceData.atomically get
IO.wait rd.loadingTask.task
let some uri, some version parseParams WaitForILeansParams params
| writeMessage {
id
result :=
: Response WaitForILeans
}
return
let uri, version parseParams WaitForILeansParams params
if let none getFileWorker? uri then
writeMessage {
id

View File

@@ -1053,16 +1053,6 @@ def inter (t₁ t₂ : DTreeMap α β cmp) : DTreeMap α β cmp :=
letI : Ord α := cmp; t₁.inner.inter t₂.inner t₁.wf.balanced, @Impl.WF.inter _ _ _ _ t₂.inner t₁.wf.balanced t₁.wf
instance : Inter (DTreeMap α β cmp) := inter
/--
Computes the difference of the given tree maps.
This function always iterates through the smaller map.
-/
def diff (t₁ t₂ : DTreeMap α β cmp) : DTreeMap α β cmp :=
letI : Ord α := cmp; t₁.inner.diff t₂.inner t₁.wf.balanced, @Impl.WF.diff α β _ t₁.inner t₁.wf t₂.inner
instance : SDiff (DTreeMap α β cmp) := diff
/--
Erases multiple mappings from the tree map by iterating over the given collection and calling
`erase`.
@@ -1070,6 +1060,7 @@ Erases multiple mappings from the tree map by iterating over the given collectio
@[inline]
def eraseMany {ρ} [ForIn Id ρ α] (t : DTreeMap α β cmp) (l : ρ) : DTreeMap α β cmp :=
letI : Ord α := cmp; t.inner.eraseMany l t.wf.balanced, t.wf.eraseMany
namespace Const
variable {β : Type v}

View File

@@ -47,7 +47,7 @@ macro_rules
| apply WF.constInsertMany | apply WF.constInsertManyIfNewUnit
| apply WF.alter | apply WF.constAlter
| apply WF.modify | apply WF.constModify
| apply WF.filterMap | apply WF.filter | apply WF.map | apply WF.union | apply WF.inter | apply WF.diff) <;> wf_trivial)
| apply WF.filterMap | apply WF.filter | apply WF.map | apply WF.union | apply WF.inter) <;> wf_trivial)
/-- Internal implementation detail of the tree map -/
scoped macro "empty" : tactic => `(tactic| { intros; simp_all [List.isEmpty_iff] } )
@@ -68,7 +68,6 @@ private meta def modifyMap : Std.HashMap Name Name :=
`insertIfNew, ``toListModel_insertIfNew,
`union, ``toListModel_union_list,
`inter, ``toListModel_inter,
`diff, ``toListModel_diff,
`erase, ``toListModel_erase,
(`insertMany, ``toListModel_insertMany_list),
(`Const.insertMany, ``Const.toListModel_insertMany_list),
@@ -4851,731 +4850,6 @@ theorem get!_inter!_of_contains_eq_false_left [TransOrd α] [Inhabited β] (h₁
end Const
section Diff
variable {m₁ m₂ : Impl α β}
/- contains -/
theorem contains_diff [TransOrd α] (h₁ : m₁.WF)
(h₂ : m₂.WF) {k : α} :
(m₁.diff m₂ h₁.balanced).contains k = (m₁.contains k && !m₂.contains k) := by
simp_to_model [diff, contains]
using List.containsKey_filter_not_contains_map_fst
theorem contains_diff! [TransOrd α] (h₁ : m₁.WF)
(h₂ : m₂.WF) {k : α} :
(m₁.diff! m₂).contains k = (m₁.contains k && !m₂.contains k) := by
rw [ diff_eq_diff!]
apply contains_diff h₁ h₂
all_goals wf_trivial
theorem contains_diff_iff [TransOrd α] (h₁ : m₁.WF)
(h₂ : m₂.WF) {k : α} :
(m₁.diff m₂ h₁.balanced).contains k m₁.contains k ¬m₂.contains k := by
simp_to_model [diff, contains]
have := @List.containsKey_filter_not_contains_map_fst_iff α β _ _ m₁.toListModel m₂.toListModel h₁.ordered.distinctKeys k
simp only [Bool.not_eq_true] at this
exact this
theorem contains_diff!_iff [TransOrd α] (h₁ : m₁.WF)
(h₂ : m₂.WF) {k : α} :
(m₁.diff! m₂).contains k m₁.contains k ¬m₂.contains k := by
rw [ diff_eq_diff!]
apply contains_diff_iff h₁ h₂
all_goals wf_trivial
theorem contains_diff_eq_false_of_contains_eq_false_left [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) {k : α}
(h : m₁.contains k = false) :
(m₁.diff m₂ h₁.balanced).contains k = false := by
revert h
simp_to_model [diff, contains] using List.containsKey_filter_not_contains_map_fst_eq_false_left
theorem contains_diff!_eq_false_of_contains_eq_false_left [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) {k : α}
(h : m₁.contains k = false) :
(m₁.diff! m₂).contains k = false := by
rw [ diff_eq_diff!]
apply contains_diff_eq_false_of_contains_eq_false_left h₁ h₂
all_goals wf_trivial
theorem contains_diff_eq_false_of_contains_right [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) {k : α}
(h : m₂.contains k) :
(m₁.diff m₂ h₁.balanced).contains k = false := by
revert h
simp_to_model [diff, contains] using List.containsKey_filter_not_contains_map_fst_of_contains_map_fst_right
theorem contains_diff!_eq_false_of_contains_right [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) {k : α}
(h : m₂.contains k) :
(m₁.diff! m₂).contains k = false := by
rw [ diff_eq_diff!]
apply contains_diff_eq_false_of_contains_right h₁ h₂
all_goals wf_trivial
/- Equiv -/
theorem Equiv.diff_left {m₃ : Impl α β} [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (equiv : m₁.Equiv m₂) :
(m₁.diff m₃ h₁.balanced).Equiv (m₂.diff m₃ h₂.balanced) := by
revert equiv
simp_to_model [Equiv, diff]
intro equiv
apply List.Perm.filter
wf_trivial
theorem Equiv.diff!_left {m₃ : Impl α β} [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (equiv : m₁.Equiv m₂) :
(m₁.diff! m₃).Equiv (m₂.diff! m₃) := by
rw [ diff_eq_diff!, diff_eq_diff!]
apply Equiv.diff_left
all_goals wf_trivial
theorem Equiv.diff_right {m₃ : Impl α β} [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (equiv : m₂.Equiv m₃) :
(m₁.diff m₂ h₁.balanced).Equiv (m₁.diff m₃ h₁.balanced) := by
revert equiv
simp_to_model [Equiv, diff]
intro equiv
apply List.perm_filter_not_contains_map_fst_of_perm equiv
all_goals wf_trivial
theorem Equiv.diff!_right {m₃ : Impl α β} [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (equiv : m₂.Equiv m₃) :
(m₁.diff! m₂).Equiv (m₁.diff! m₃) := by
rw [ diff_eq_diff!, diff_eq_diff!]
apply Equiv.diff_right
all_goals wf_trivial
theorem Equiv.diff_congr {m₃ m₄ : Impl α β} [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF)
(equiv₁ : m₁.Equiv m₃) (equiv₂ : m₂.Equiv m₄) :
(m₁.diff m₂ h₁.balanced).Equiv (m₃.diff m₄ h₃.balanced) := by
revert equiv₁ equiv₂
simp_to_model [Equiv, diff]
intro equiv₁ equiv₂
apply List.congr_filter_not_contains_map_fst_of_perm
all_goals wf_trivial
theorem Equiv.diff!_congr {m₃ m₄ : Impl α β} [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF)
(equiv₁ : m₁.Equiv m₃) (equiv₂ : m₂.Equiv m₄) :
(m₁.diff! m₂).Equiv (m₃.diff! m₄) := by
rw [ diff_eq_diff!, diff_eq_diff!]
apply Equiv.diff_congr
all_goals wf_trivial
/- get? -/
theorem get?_diff [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
(m₁.diff m₂ h₁.balanced).get? k =
if m₂.contains k then none else m₁.get? k := by
simp_to_model [diff, get?, contains] using List.getValueCast?_filter_not_contains_map_fst
theorem get?_diff! [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
(m₁.diff! m₂).get? k =
if m₂.contains k then none else m₁.get? k := by
rw [ diff_eq_diff!]
apply get?_diff h₁ h₂
all_goals wf_trivial
theorem get?_diff_of_contains_eq_false_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : m₂.contains k = false) :
(m₁.diff m₂ h₁.balanced).get? k = m₁.get? k := by
revert h
simp_to_model [diff, contains, get?] using List.getValueCast?_filter_not_contains_map_fst_of_containsKey_eq_false_right
theorem get?_diff!_of_contains_eq_false_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : m₂.contains k = false) :
(m₁.diff! m₂).get? k = m₁.get? k := by
rw [ diff_eq_diff!]
apply get?_diff_of_contains_eq_false_right h₁ h₂
all_goals wf_trivial
theorem get?_diff_of_contains_eq_false_left [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : m₁.contains k = false) :
(m₁.diff m₂ h₁.balanced).get? k = none := by
revert h
simp_to_model [diff, contains, get?] using List.getValueCast?_filter_not_contains_map_fst_of_containsKey_eq_false_left
theorem get?_diff!_of_contains_eq_false_left [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : m₁.contains k = false) :
(m₁.diff! m₂).get? k = none := by
rw [ diff_eq_diff!]
apply get?_diff_of_contains_eq_false_left h₁ h₂
all_goals wf_trivial
theorem get?_diff_of_contains_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : m₂.contains k) :
(m₁.diff m₂ h₁.balanced).get? k = none := by
revert h
simp_to_model [diff, get?, contains] using List.getValueCast?_filter_not_contains_map_fst_of_containsKey_right
theorem get?_diff!_of_contains_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : m₂.contains k) :
(m₁.diff! m₂).get? k = none := by
rw [ diff_eq_diff!]
apply get?_diff_of_contains_right h₁ h₂
all_goals wf_trivial
/- get -/
theorem get_diff [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {h_contains : (m₁.diff m₂ h₁.balanced).contains k} :
(m₁.diff m₂ h₁.balanced).get k h_contains =
m₁.get k ((contains_diff_iff h₁ h₂).1 h_contains).1 := by
simp_to_model [diff, get, contains] using List.getValueCast_filter_not_contains_map_fst
theorem get_diff! [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {h_contains : (m₁.diff! m₂).contains k} :
(m₁.diff! m₂).get k h_contains =
m₁.get k ((contains_diff!_iff h₁ h₂).1 h_contains).1 := by
conv =>
lhs
arg 1
rw [ diff_eq_diff!]
. skip
. apply h₁
simp_to_model [diff, get, contains] using List.getValueCast_filter_not_contains_map_fst
/- getD -/
theorem getD_diff [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {fallback : β k} :
(m₁.diff m₂ h₁.balanced).getD k fallback =
if m₂.contains k then fallback else m₁.getD k fallback := by
simp_to_model [diff, getD, contains] using List.getValueCastD_filter_not_contains_map_fst
theorem getD_diff! [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {fallback : β k} :
(m₁.diff! m₂).getD k fallback =
if m₂.contains k then fallback else m₁.getD k fallback := by
rw [ diff_eq_diff!]
apply getD_diff h₁ h₂
all_goals wf_trivial
theorem getD_diff_of_contains_eq_false_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {fallback : β k} (h : m₂.contains k = false) :
(m₁.diff m₂ h₁.balanced).getD k fallback = m₁.getD k fallback := by
revert h
simp_to_model [diff, contains, getD] using List.getValueCastD_filter_not_contains_map_fst_of_containsKey_eq_false_right
theorem getD_diff!_of_contains_eq_false_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {fallback : β k} (h : m₂.contains k = false) :
(m₁.diff! m₂).getD k fallback = m₁.getD k fallback := by
rw [ diff_eq_diff!]
apply getD_diff_of_contains_eq_false_right h₁ h₂
all_goals wf_trivial
theorem getD_diff_of_contains_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {fallback : β k} (h : m₂.contains k) :
(m₁.diff m₂ h₁.balanced).getD k fallback = fallback := by
revert h
simp_to_model [diff, getD, contains] using List.getValueCastD_filter_not_contains_map_fst_of_contains_map_fst_right
theorem getD_diff!_of_contains_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {fallback : β k} (h : m₂.contains k) :
(m₁.diff! m₂).getD k fallback = fallback := by
rw [ diff_eq_diff!]
apply getD_diff_of_contains_right h₁ h₂
all_goals wf_trivial
theorem getD_diff_of_contains_eq_false_left [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {fallback : β k} (h : m₁.contains k = false) :
(m₁.diff m₂ h₁.balanced).getD k fallback = fallback := by
revert h
simp_to_model [diff, getD, contains] using List.getValueCastD_filter_not_contains_map_fst_of_containsKey_eq_false_left
theorem getD_diff!_of_contains_eq_false_left [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {fallback : β k} (h : m₁.contains k = false) :
(m₁.diff! m₂).getD k fallback = fallback := by
rw [ diff_eq_diff!]
apply getD_diff_of_contains_eq_false_left h₁ h₂
all_goals wf_trivial
/- get! -/
theorem get!_diff [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} [Inhabited (β k)] :
(m₁.diff m₂ h₁.balanced).get! k =
if m₂.contains k then default else m₁.get! k := by
simp_to_model [diff, get!, contains] using List.getValueCastD_filter_not_contains_map_fst
theorem get!_diff! [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} [Inhabited (β k)] :
(m₁.diff! m₂).get! k =
if m₂.contains k then default else m₁.get! k := by
rw [ diff_eq_diff!]
apply get!_diff h₁ h₂
all_goals wf_trivial
theorem get!_diff_of_contains_eq_false_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} [Inhabited (β k)] (h : m₂.contains k = false) :
(m₁.diff m₂ h₁.balanced).get! k = m₁.get! k := by
revert h
simp_to_model [diff, contains, get!] using List.getValueCastD_filter_not_contains_map_fst_of_containsKey_eq_false_right
theorem get!_diff!_of_contains_eq_false_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} [Inhabited (β k)] (h : m₂.contains k = false) :
(m₁.diff! m₂).get! k = m₁.get! k := by
rw [ diff_eq_diff!]
apply get!_diff_of_contains_eq_false_right h₁ h₂
all_goals wf_trivial
theorem get!_diff_of_contains_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} [Inhabited (β k)] (h : m₂.contains k) :
(m₁.diff m₂ h₁.balanced).get! k = default := by
revert h
simp_to_model [diff, get!, contains] using List.getValueCastD_filter_not_contains_map_fst_of_contains_map_fst_right
theorem get!_diff!_of_contains_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} [Inhabited (β k)] (h : m₂.contains k) :
(m₁.diff! m₂).get! k = default := by
rw [ diff_eq_diff!]
apply get!_diff_of_contains_right h₁ h₂
all_goals wf_trivial
theorem get!_diff_of_contains_eq_false_left [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} [Inhabited (β k)] (h : m₁.contains k = false) :
(m₁.diff m₂ h₁.balanced).get! k = default := by
revert h
simp_to_model [diff, get!, contains] using List.getValueCastD_filter_not_contains_map_fst_of_containsKey_eq_false_left
theorem get!_diff!_of_contains_eq_false_left [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} [Inhabited (β k)] (h : m₁.contains k = false) :
(m₁.diff! m₂).get! k = default := by
rw [ diff_eq_diff!]
apply get!_diff_of_contains_eq_false_left h₁ h₂
all_goals wf_trivial
/- getKey? -/
theorem getKey?_diff [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
(m₁.diff m₂ h₁.balanced).getKey? k =
if m₂.contains k then none else m₁.getKey? k := by
simp_to_model [diff, contains, getKey?] using List.getKey?_filter_not_contains_map_fst
theorem getKey?_diff! [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
(m₁.diff! m₂).getKey? k =
if m₂.contains k then none else m₁.getKey? k := by
rw [ diff_eq_diff!]
apply getKey?_diff h₁ h₂
all_goals wf_trivial
theorem getKey?_diff_of_contains_eq_false_right [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (h : m₂.contains k = false) :
(m₁.diff m₂ h₁.balanced).getKey? k = m₁.getKey? k := by
revert h
simp_to_model [contains, getKey?, diff] using List.getKey?_filter_not_contains_map_fst_of_containsKey_eq_false_right
theorem getKey?_diff!_of_contains_eq_false_right [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (h : m₂.contains k = false) :
(m₁.diff! m₂).getKey? k = m₁.getKey? k := by
rw [ diff_eq_diff!]
apply getKey?_diff_of_contains_eq_false_right h₁ h₂
all_goals wf_trivial
theorem getKey?_diff_of_contains_eq_false_left [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (h : m₁.contains k = false) :
(m₁.diff m₂ h₁.balanced).getKey? k = none := by
revert h
simp_to_model [contains, getKey?, diff] using List.getKey?_filter_not_contains_map_fst_of_containsKey_eq_false_left
theorem getKey?_diff!_of_contains_eq_false_left [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (h : m₁.contains k = false) :
(m₁.diff! m₂).getKey? k = none := by
rw [ diff_eq_diff!]
apply getKey?_diff_of_contains_eq_false_left h₁ h₂
all_goals wf_trivial
theorem getKey?_diff_of_contains_right [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (h : m₂.contains k) :
(m₁.diff m₂ h₁.balanced).getKey? k = none := by
revert h
simp_to_model [contains, getKey?, diff] using List.getKey?_filter_not_contains_map_fst_of_containsKey_right
theorem getKey?_diff!_of_contains_right [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (h : m₂.contains k) :
(m₁.diff! m₂).getKey? k = none := by
rw [ diff_eq_diff!]
apply getKey?_diff_of_contains_right h₁ h₂
all_goals wf_trivial
/- getKey -/
theorem getKey_diff [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {h_contains : (m₁.diff m₂ h₁.balanced).contains k} :
(m₁.diff m₂ h₁.balanced).getKey k h_contains =
m₁.getKey k ((contains_diff_iff h₁ h₂).1 h_contains).1 := by
simp_to_model [diff, contains, getKey] using List.getKey_filter_not_contains_map_fst
theorem getKey_diff! [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {h_contains : (m₁.diff! m₂).contains k} :
(m₁.diff! m₂).getKey k h_contains =
m₁.getKey k ((contains_diff!_iff h₁ h₂).1 h_contains).1 := by
conv =>
lhs
arg 1
rw [ diff_eq_diff!]
. skip
. apply h₁
simp_to_model [diff, contains, getKey] using List.getKey_filter_not_contains_map_fst
/- getKeyD -/
theorem getKeyD_diff [TransOrd α] (h₁ : m₁.WF)
(h₂ : m₂.WF) {k fallback : α} :
(m₁.diff m₂ h₁.balanced).getKeyD k fallback =
if m₂.contains k then fallback else m₁.getKeyD k fallback := by
simp_to_model [diff, getKeyD, contains] using List.getKeyD_filter_not_contains_map_fst
theorem getKeyD_diff! [TransOrd α] (h₁ : m₁.WF)
(h₂ : m₂.WF) {k fallback : α} :
(m₁.diff! m₂).getKeyD k fallback =
if m₂.contains k then fallback else m₁.getKeyD k fallback := by
rw [ diff_eq_diff!]
apply getKeyD_diff h₁ h₂
all_goals wf_trivial
theorem getKeyD_diff_of_contains_eq_false_right [TransOrd α] (h₁ : m₁.WF)
(h₂ : m₂.WF) {k fallback : α} (h : m₂.contains k = false) :
(m₁.diff m₂ h₁.balanced).getKeyD k fallback = m₁.getKeyD k fallback := by
revert h
simp_to_model [contains, diff, getKeyD] using List.getKeyD_filter_not_contains_map_fst_of_contains_eq_false_right
theorem getKeyD_diff!_of_contains_eq_false_right [TransOrd α] (h₁ : m₁.WF)
(h₂ : m₂.WF) {k fallback : α} (h : m₂.contains k = false) :
(m₁.diff! m₂).getKeyD k fallback = m₁.getKeyD k fallback := by
rw [ diff_eq_diff!]
apply getKeyD_diff_of_contains_eq_false_right h₁ h₂
all_goals wf_trivial
theorem getKeyD_diff_of_contains_right [TransOrd α] (h₁ : m₁.WF)
(h₂ : m₂.WF) {k fallback : α} (h : m₂.contains k) :
(m₁.diff m₂ h₁.balanced).getKeyD k fallback = fallback := by
revert h
simp_to_model [diff, getKeyD, contains] using List.getKeyD_filter_not_contains_map_fst_of_contains_right
theorem getKeyD_diff!_of_contains_right [TransOrd α] (h₁ : m₁.WF)
(h₂ : m₂.WF) {k fallback : α} (h : m₂.contains k) :
(m₁.diff! m₂).getKeyD k fallback = fallback := by
rw [ diff_eq_diff!]
apply getKeyD_diff_of_contains_right h₁ h₂
all_goals wf_trivial
theorem getKeyD_diff_of_contains_eq_false_left [TransOrd α] (h₁ : m₁.WF)
(h₂ : m₂.WF) {k fallback : α} (h : m₁.contains k = false) :
(m₁.diff m₂ h₁.balanced).getKeyD k fallback = fallback := by
revert h
simp_to_model [diff, getKeyD, contains] using getKeyD_filter_not_contains_map_fst_of_contains_eq_false_left
theorem getKeyD_diff!_of_contains_eq_false_left [TransOrd α] (h₁ : m₁.WF)
(h₂ : m₂.WF) {k fallback : α} (h : m₁.contains k = false) :
(m₁.diff! m₂).getKeyD k fallback = fallback := by
rw [ diff_eq_diff!]
apply getKeyD_diff_of_contains_eq_false_left h₁ h₂
all_goals wf_trivial
/- getKey! -/
theorem getKey!_diff [Inhabited α] [TransOrd α] (h₁ : m₁.WF)
(h₂ : m₂.WF) {k : α} :
(m₁.diff m₂ h₁.balanced).getKey! k =
if m₂.contains k then default else m₁.getKey! k := by
simp_to_model [diff, getKey!, contains] using List.getKeyD_filter_not_contains_map_fst
theorem getKey!_diff! [Inhabited α] [TransOrd α] (h₁ : m₁.WF)
(h₂ : m₂.WF) {k : α} :
(m₁.diff! m₂).getKey! k =
if m₂.contains k then default else m₁.getKey! k := by
rw [ diff_eq_diff!]
apply getKey!_diff h₁ h₂
all_goals wf_trivial
theorem getKey!_diff_of_contains_eq_false_right [Inhabited α] [TransOrd α] (h₁ : m₁.WF)
(h₂ : m₂.WF) {k : α} (h : m₂.contains k = false) :
(m₁.diff m₂ h₁.balanced).getKey! k = m₁.getKey! k := by
revert h
simp_to_model [diff, getKey!, contains] using List.getKeyD_filter_not_contains_map_fst_of_contains_eq_false_right
theorem getKey!_diff!_of_contains_eq_false_right [Inhabited α] [TransOrd α] (h₁ : m₁.WF)
(h₂ : m₂.WF) {k : α} (h : m₂.contains k = false) :
(m₁.diff! m₂).getKey! k = m₁.getKey! k := by
rw [ diff_eq_diff!]
apply getKey!_diff_of_contains_eq_false_right h₁ h₂
all_goals wf_trivial
theorem getKey!_diff_of_contains_right [Inhabited α] [TransOrd α] (h₁ : m₁.WF)
(h₂ : m₂.WF) {k : α} (h : m₂.contains k) :
(m₁.diff m₂ h₁.balanced).getKey! k = default := by
revert h
simp_to_model [diff, getKey!, contains] using List.getKeyD_filter_not_contains_map_fst_of_contains_right
theorem getKey!_diff!_of_contains_right [Inhabited α] [TransOrd α] (h₁ : m₁.WF)
(h₂ : m₂.WF) {k : α} (h : m₂.contains k) :
(m₁.diff! m₂).getKey! k = default := by
rw [ diff_eq_diff!]
apply getKey!_diff_of_contains_right h₁ h₂
all_goals wf_trivial
theorem getKey!_diff_of_contains_eq_false_left [Inhabited α] [TransOrd α] (h₁ : m₁.WF)
(h₂ : m₂.WF) {k : α} (h : m₁.contains k = false) :
(m₁.diff m₂ h₁.balanced).getKey! k = default := by
revert h
simp_to_model [diff, getKey!, contains] using List.getKeyD_filter_not_contains_map_fst_of_contains_eq_false_left
theorem getKey!_diff!_of_contains_eq_false_left [Inhabited α] [TransOrd α] (h₁ : m₁.WF)
(h₂ : m₂.WF) {k : α} (h : m₁.contains k = false) :
(m₁.diff! m₂).getKey! k = default := by
rw [ diff_eq_diff!]
apply getKey!_diff_of_contains_eq_false_left h₁ h₂
all_goals wf_trivial
/- size -/
theorem size_diff_le_size_left [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) :
(m₁.diff m₂ h₁.balanced).size m₁.size := by
simp_to_model [diff, size] using List.length_filter_le
theorem size_diff!_le_size_left [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) :
(m₁.diff! m₂).size m₁.size := by
rw [ diff_eq_diff!]
apply size_diff_le_size_left h₁ h₂
all_goals wf_trivial
theorem size_diff_eq_size_left [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF)
(h : (a : α), m₁.contains a m₂.contains a = false) :
(m₁.diff m₂ h₁.balanced).size = m₁.size := by
revert h
simp_to_model [diff, size, contains] using List.length_filter_not_contains_map_fst_eq_length_left
theorem size_diff!_eq_size_left [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF)
(h : (a : α), m₁.contains a m₂.contains a = false) :
(m₁.diff! m₂).size = m₁.size := by
rw [ diff_eq_diff!]
apply size_diff_eq_size_left h₁ h₂
all_goals wf_trivial
theorem size_diff_add_size_inter_eq_size_left [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) :
(m₁.diff m₂ h₁.balanced).size + (m₁.inter m₂ h₁.balanced).size = m₁.size := by
simp_to_model [diff, inter, size] using List.size_filter_not_contains_map_fst_add_size_inter_eq_size_left
theorem size_diff!_add_size_inter!_eq_size_left [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) :
(m₁.diff! m₂).size + (m₁.inter! m₂).size = m₁.size := by
rw [ diff_eq_diff!, inter_eq_inter!]
apply size_diff_add_size_inter_eq_size_left h₁ h₂
all_goals wf_trivial
/- isEmpty -/
@[simp]
theorem isEmpty_diff_left [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁.isEmpty) :
(m₁.diff m₂ h₁.balanced).isEmpty = true := by
revert h
simp_to_model [isEmpty, diff] using List.isEmpty_filter_not_contains_map_fst_left
@[simp]
theorem isEmpty_diff!_left [TransOrd α]
(h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁.isEmpty) :
(m₁.diff! m₂).isEmpty = true := by
rw [ diff_eq_diff!]
apply isEmpty_diff_left h₁ h₂
all_goals wf_trivial
theorem isEmpty_diff_iff [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) :
(m₁.diff m₂ h₁.balanced).isEmpty k, m₁.contains k m₂.contains k := by
simp_to_model [diff, contains, isEmpty] using List.isEmpty_filter_not_contains_map_fst_iff
theorem isEmpty_diff!_iff [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) :
(m₁.diff! m₂).isEmpty k, m₁.contains k m₂.contains k := by
rw [ diff_eq_diff!]
apply isEmpty_diff_iff h₁ h₂
all_goals wf_trivial
end Diff
namespace Const
variable {β : Type v} {m₁ m₂ : Impl α (fun _ => β)}
/- get? -/
theorem get?_diff [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
Const.get? (m₁.diff m₂ h₁.balanced) k =
if m₂.contains k then none else Const.get? m₁ k := by
simp_to_model [diff, Const.get?, contains] using List.getValue?_filter_not_contains_map_fst
theorem get?_diff! [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
Const.get? (m₁.diff! m₂) k =
if m₂.contains k then none else Const.get? m₁ k := by
rw [ diff_eq_diff!]
apply get?_diff h₁ h₂
all_goals wf_trivial
theorem get?_diff_of_contains_eq_false_right [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : m₂.contains k = false) :
Const.get? (m₁.diff m₂ h₁.balanced) k = Const.get? m₁ k := by
revert h
simp_to_model [diff, contains, Const.get?] using List.getValue?_filter_not_contains_map_fst_of_contains_eq_false_right
theorem get?_diff!_of_contains_eq_false_right [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : m₂.contains k = false) :
Const.get? (m₁.diff! m₂) k = Const.get? m₁ k := by
rw [ diff_eq_diff!]
apply get?_diff_of_contains_eq_false_right h₁ h₂
all_goals wf_trivial
theorem get?_diff_of_contains_eq_false_left [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : m₁.contains k = false) :
Const.get? (m₁.diff m₂ h₁.balanced) k = none := by
revert h
simp_to_model [diff, Const.get?, contains] using List.getValue?_filter_not_contains_map_fst_of_containsKey_eq_false_left
theorem get?_diff!_of_contains_eq_false_left [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : m₁.contains k = false) :
Const.get? (m₁.diff! m₂) k = none := by
rw [ diff_eq_diff!]
apply get?_diff_of_contains_eq_false_left h₁ h₂
all_goals wf_trivial
theorem get?_diff_of_contains_right [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : m₂.contains k) :
Const.get? (m₁.diff m₂ h₁.balanced) k = none := by
revert h
simp_to_model [diff, Const.get?, contains] using List.getValue?_filter_not_contains_map_fst_of_contains_right
theorem get?_diff!_of_contains_right [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : m₂.contains k) :
Const.get? (m₁.diff! m₂) k = none := by
rw [ diff_eq_diff!]
apply get?_diff_of_contains_right h₁ h₂
all_goals wf_trivial
/- get -/
theorem get_diff [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {h_contains : (m₁.diff m₂ h₁.balanced).contains k} :
Const.get (m₁.diff m₂ h₁.balanced) k h_contains =
Const.get m₁ k ((contains_diff_iff h₁ h₂).1 h_contains).1 := by
simp_to_model [diff, Const.get, contains] using List.getValue_filter_not_contains
theorem get_diff! [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {h_contains : (m₁.diff! m₂).contains k} :
Const.get (m₁.diff! m₂) k h_contains =
Const.get m₁ k ((contains_diff!_iff h₁ h₂).1 h_contains).1 := by
conv =>
lhs
arg 1
rw [ diff_eq_diff!]
. skip
. apply h₁
simp_to_model [diff, Const.get, contains] using List.getValue_filter_not_contains
/- getD -/
theorem getD_diff [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {fallback : β} :
Const.getD (m₁.diff m₂ h₁.balanced) k fallback =
if m₂.contains k then fallback else Const.getD m₁ k fallback := by
simp_to_model [diff, Const.getD, contains] using List.getValueD_filter_not_contains_map_fst
theorem getD_diff! [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {fallback : β} :
Const.getD (m₁.diff! m₂) k fallback =
if m₂.contains k then fallback else Const.getD m₁ k fallback := by
rw [ diff_eq_diff!]
apply getD_diff h₁ h₂
all_goals wf_trivial
theorem getD_diff_of_contains_eq_false_right [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {fallback : β} (h : m₂.contains k = false) :
Const.getD (m₁.diff m₂ h₁.balanced) k fallback = Const.getD m₁ k fallback := by
revert h
simp_to_model [diff, contains, Const.getD] using List.getValueD_filter_not_contains_map_fst_of_containsKey_eq_false_right
theorem getD_diff!_of_contains_eq_false_right [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {fallback : β} (h : m₂.contains k = false) :
Const.getD (m₁.diff! m₂) k fallback = Const.getD m₁ k fallback := by
rw [ diff_eq_diff!]
apply getD_diff_of_contains_eq_false_right h₁ h₂
all_goals wf_trivial
theorem getD_diff_of_contains_right [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {fallback : β} (h : m₂.contains k) :
Const.getD (m₁.diff m₂ h₁.balanced) k fallback = fallback := by
revert h
simp_to_model [diff, Const.getD, contains] using List.getValueD_filter_not_contains_map_fst_of_contains_map_fst_right
theorem getD_diff!_of_contains_right [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {fallback : β} (h : m₂.contains k) :
Const.getD (m₁.diff! m₂) k fallback = fallback := by
rw [ diff_eq_diff!]
apply getD_diff_of_contains_right h₁ h₂
all_goals wf_trivial
theorem getD_diff_of_contains_eq_false_left [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {fallback : β} (h : m₁.contains k = false) :
Const.getD (m₁.diff m₂ h₁.balanced) k fallback = fallback := by
revert h
simp_to_model [diff, Const.getD, contains] using List.getValueD_filter_not_contains_map_fst_of_containsKey_eq_false_left
theorem getD_diff!_of_contains_eq_false_left [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {fallback : β} (h : m₁.contains k = false) :
Const.getD (m₁.diff! m₂) k fallback = fallback := by
rw [ diff_eq_diff!]
apply getD_diff_of_contains_eq_false_left h₁ h₂
all_goals wf_trivial
/- get! -/
theorem get!_diff [TransOrd α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
Const.get! (m₁.diff m₂ h₁.balanced) k =
if m₂.contains k then default else Const.get! m₁ k := by
simp_to_model [diff, Const.get!, contains] using List.getValueD_filter_not_contains_map_fst
theorem get!_diff! [TransOrd α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
Const.get! (m₁.diff! m₂) k =
if m₂.contains k then default else Const.get! m₁ k := by
rw [ diff_eq_diff!]
apply get!_diff h₁ h₂
all_goals wf_trivial
theorem get!_diff_of_contains_eq_false_right [TransOrd α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : m₂.contains k = false) :
Const.get! (m₁.diff m₂ h₁.balanced) k = Const.get! m₁ k := by
revert h
simp_to_model [diff, contains, Const.get!] using List.getValueD_filter_not_contains_map_fst_of_containsKey_eq_false_right
theorem get!_diff!_of_contains_eq_false_right [TransOrd α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : m₂.contains k = false) :
Const.get! (m₁.diff! m₂) k = Const.get! m₁ k := by
rw [ diff_eq_diff!]
apply get!_diff_of_contains_eq_false_right h₁ h₂
all_goals wf_trivial
theorem get!_diff_of_contains_right [TransOrd α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : m₂.contains k) :
Const.get! (m₁.diff m₂ h₁.balanced) k = default := by
revert h
simp_to_model [diff, Const.get!, contains] using List.getValueD_filter_not_contains_map_fst_of_contains_map_fst_right
theorem get!_diff!_of_contains_right [TransOrd α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : m₂.contains k) :
Const.get! (m₁.diff! m₂) k = default := by
rw [ diff_eq_diff!]
apply get!_diff_of_contains_right h₁ h₂
all_goals wf_trivial
theorem get!_diff_of_contains_eq_false_left [TransOrd α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : m₁.contains k = false) :
Const.get! (m₁.diff m₂ h₁.balanced) k = default := by
revert h
simp_to_model [diff, Const.get!, contains] using List.getValueD_filter_not_contains_map_fst_of_containsKey_eq_false_left
theorem get!_diff!_of_contains_eq_false_left [TransOrd α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : m₁.contains k = false) :
Const.get! (m₁.diff! m₂) k = default := by
rw [ diff_eq_diff!]
apply get!_diff_of_contains_eq_false_left h₁ h₂
all_goals wf_trivial
end Const
section Alter
theorem isEmpty_alter_eq_isEmpty_erase [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α}

View File

@@ -481,36 +481,6 @@ def eraseMany! [Ord α] {ρ : Type w} [ForIn Id ρ α] (t : Impl α β) (l : ρ)
r := r.val.erase! a, fun h₀ h₁ => h₁ _ _ (r.2 h₀ h₁)
return r
/-- A tree map obtained by erasing elements from `t`, bundled with an inductive principle. -/
abbrev IteratedEntryErasureFrom [Ord α] (t) :=
{ t' // {P : Impl α β Prop}, P t ( t'' a h, P t'' P (t''.erase a h).impl) P t' }
/-- Iterate over `l` and erase all of its elements from `t`. -/
@[inline]
def eraseManyEntries [Ord α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] (t : Impl α β) (l : ρ) (h : t.Balanced) :
IteratedEntryErasureFrom t := Id.run do
let mut r := t, fun h _ => h
for a, _ in l do
let hr := r.2 h (fun t'' a h _ => (t''.erase a h).balanced_impl)
r := r.val.erase a hr |>.impl, fun h₀ h₁ => h₁ _ _ _ (r.2 h₀ h₁)
return r
/-- A tree map obtained by erasing elements from `t`, bundled with an inductive principle. -/
abbrev IteratedSlowEntryErasureFrom [Ord α] (t) :=
{ t' // {P : Impl α β Prop}, P t ( t'' a, P t'' P (t''.erase! a)) P t' }
/--
Slower version of `eraseManyEntries` which can be used in absence of balance information but still
assumes the preconditions of `eraseManyEntries`, otherwise might panic.
-/
@[inline]
def eraseManyEntries! [Ord α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] (t : Impl α β) (l : ρ) :
IteratedSlowErasureFrom t := Id.run do
let mut r := t, fun h _ => h
for a, _ in l do
r := r.val.erase! a, fun h₀ h₁ => h₁ _ _ (r.2 h₀ h₁)
return r
/-- A tree map obtained by inserting elements into `t`, bundled with an inductive principle. -/
abbrev IteratedInsertionInto [Ord α] (t) :=
{ t' // {P : Impl α β Prop}, P t ( t'' a b h, P t'' P (t''.insert a b h).impl) P t' }
@@ -822,20 +792,6 @@ information but still assumes the preconditions of `filter`, otherwise might pan
def inter! [Ord α] (m₁ m₂ : Impl α β): Impl α β :=
if m₁.size m₂.size then m₁.filter! (fun k _ => m₂.contains k) else interSmaller m₁ m₂
/--
Computes the difference of the given tree maps.
This function always iterates through the smaller map.
-/
def diff [Ord α] (t₁ t₂ : Impl α β) (h₁ : t₁.Balanced) : Impl α β :=
if t₁.size t₂.size then (t₁.filter (fun p _ => !t₂.contains p) h₁).impl else (t₁.eraseManyEntries t₂ h₁)
/--
Slower version of `diff` which can be used in the absence of balance
information but still assumes the preconditions of `diff`, otherwise might panic.
-/
def diff! [Ord α] (t₁ t₂ : Impl α β) : Impl α β :=
if t₁.size t₂.size then t₁.filter! (fun p _ => !t₂.contains p) else t₁.eraseManyEntries! t₂
/--
Changes the mapping of the key `k` by applying the function `f` to the current mapped value
(if any). This function can be used to insert a new mapping, modify an existing one or delete it.

View File

@@ -76,10 +76,6 @@ theorem WF.balanced [Ord α] {t : Impl α β} (h : WF t) : t.Balanced := by
case constModify ih => exact Const.balanced_modify ih
case inter ih => exact balanced_inter ih
theorem WF.eraseManyEntries [Ord α] {ρ} [ForIn Id ρ ((a : α) × β a)] {t : Impl α β} {l : ρ} {h} (hwf : WF t) :
WF (t.eraseManyEntries l h).val :=
(t.eraseManyEntries l h).2 hwf fun _ _ _ hwf' => hwf'.erase
theorem WF.eraseMany [Ord α] {ρ} [ForIn Id ρ α] {t : Impl α β} {l : ρ} {h} (hwf : WF t) :
WF (t.eraseMany l h).val :=
(t.eraseMany l h).2 hwf fun _ _ _ hwf' => hwf'.erase
@@ -114,13 +110,6 @@ theorem WF.union [Ord α] {t₁ : Impl α β} {h₁ : t₁.WF} {t₂ : Impl α
. apply WF.insertManyIfNew h₂
. apply WF.insertMany h₁
theorem WF.diff [Ord α] {t₁ : Impl α β} {h₁ : t₁.WF} {t₂ : Impl α β} :
(t₁.diff t₂ h₁.balanced).WF := by
simp [Impl.diff]
split
· apply WF.filter h₁
· apply WF.eraseManyEntries h₁
section Const
variable {β : Type v}

View File

@@ -1661,75 +1661,6 @@ theorem WF.eraseMany! {_ : Ord α} [TransOrd α] {ρ} [ForIn Id ρ α] {l : ρ}
{t : Impl α β} (h : t.WF) : (t.eraseMany! l).1.WF :=
(t.eraseMany! l).2 h (fun _ _ h' => h'.erase!)
/-!
### `eraseManyEntries`
-/
theorem eraseManyEntries!_eq_foldl {_ : Ord α} {l : List ((a : α) × β a)} {t : Impl α β} :
(t.eraseManyEntries! l).val = l.foldl (init := t) fun acc k, _ => acc.erase! k := by
simp [eraseManyEntries!, List.foldl_hom Subtype.val, List.forIn_pure_yield_eq_foldl]
theorem eraseManyEntries_eq_foldl {_ : Ord α} {l : List ((a : α) × β a)} {t : Impl α β} (h : t.Balanced) :
(t.eraseManyEntries l h).val = l.foldl (init := t) fun acc k, _ => acc.erase! k := by
simp [eraseManyEntries, erase_eq_erase!, List.foldl_hom Subtype.val, List.forIn_pure_yield_eq_foldl]
theorem eraseManyEntries_impl_eq_foldl {_ : Ord α} {t₁ : Impl α β} (h₁ : t₁.Balanced) {t₂ : Impl α β} :
(t₁.eraseManyEntries t₂ h₁).val = t₂.foldl (init := t₁) fun acc k _ => acc.erase! k := by
simp [foldl_eq_foldl]
rw [ eraseManyEntries_eq_foldl]
rotate_left
· exact h₁
· simp only [eraseManyEntries, pure, ForIn.forIn, Id.run_bind]
rw [forIn_eq_forIn_toListModel]
congr
theorem eraseManyEntries!_impl_eq_foldl {_ : Ord α} {t₁ : Impl α β} {t₂ : Impl α β} :
(t₁.eraseManyEntries! t₂).val = t₂.foldl (init := t₁) fun acc k _ => acc.erase! k := by
simp [foldl_eq_foldl]
rw [ eraseManyEntries!_eq_foldl]
simp only [eraseManyEntries!, pure, ForIn.forIn, Id.run_bind]
rw [forIn_eq_forIn_toListModel]
congr
theorem eraseManyEntries_impl_eq_eraseManyEntries! {_ : Ord α}
{t₁ t₂ : Impl α β} (h : t₁.Balanced) :
(t₁.eraseManyEntries t₂ h).val = (t₁.eraseManyEntries! t₂).val := by
simp only [eraseManyEntries_impl_eq_foldl, eraseManyEntries!_impl_eq_foldl]
theorem eraseManyEntries_impl_perm_eraseList {_ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α]
{t₁ : Impl α β} (h₁ : t₁.WF) {t₂ : Impl α β} :
List.Perm (t₁.eraseManyEntries t₂ h₁.balanced).val.toListModel (t₁.toListModel.eraseList (t₂.toListModel.map (·.1))) := by
rw [eraseManyEntries_impl_eq_foldl]
rw [foldl_eq_foldl]
induction t₂.toListModel generalizing t₁ with
| nil => rfl
| cons e es ih =>
simp only [List.foldl_cons]
apply List.Perm.trans (@ih (t₁.erase! e.1) (h₁.erase!))
apply eraseList_perm_of_perm_first
· apply toListModel_erase!
· exact h₁.balanced
· exact h₁.ordered
· apply h₁.erase!.ordered.distinctKeys
theorem toListModel_eraseManyEntries_impl {_ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α]
{t₁ : Impl α β} (h₁ : t₁.WF) {t₂ : Impl α β} :
List.Perm (t₁.eraseManyEntries t₂ h₁.balanced).val.toListModel (t₁.toListModel.filter (fun p => !List.contains (t₂.toListModel.map Sigma.fst) p.fst )) := by
apply List.Perm.trans
· apply eraseManyEntries_impl_perm_eraseList h₁
· apply eraseList_perm_filter_not_contains
· apply h₁.ordered.distinctKeys
theorem toListModel_eraseManyEntries!_impl {_ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α]
{t₁ : Impl α β} (h₁ : t₁.WF) {t₂ : Impl α β} :
List.Perm (t₁.eraseManyEntries! t₂).val.toListModel (t₁.toListModel.filter (fun p => !List.contains (t₂.toListModel.map Sigma.fst) p.fst)) := by
rw [ eraseManyEntries_impl_eq_eraseManyEntries! h₁.balanced]
apply toListModel_eraseManyEntries_impl h₁
theorem WF.eraseManyEntries! {_ : Ord α} [TransOrd α] {ρ} [ForIn Id ρ ((a : α) × β a)] {l : ρ}
{t : Impl α β} (h : t.WF) : (t.eraseManyEntries! l).1.WF :=
(t.eraseManyEntries! l).2 h (fun _ _ h' => h'.erase!)
/-!
### `insertMany`
-/
@@ -2117,40 +2048,6 @@ theorem toListModel_interSmallerFn {_ : Ord α} [TransOrd α] [BEq α] [LawfulBE
simp only [heq, hml]
exact h₁.ordered
/-!
### diff
-/
theorem toListModel_diff {_ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α]
{t₁ t₂ : Impl α β} (h₁ : t₁.WF) (h₂ : t₂.WF) :
List.Perm (t₁.diff t₂ h₁.balanced).toListModel (t₁.toListModel.filter (fun p => !List.contains (t₂.toListModel.map Sigma.fst) p.fst)) := by
rw [diff]
split
· simp only [toListModel_filter]
conv =>
lhs
lhs
ext e
congr
rw [contains_eq_containsKey h₂.ordered]
rw [containsKey_eq_contains_map_fst]
· apply toListModel_eraseManyEntries_impl h₁
theorem diff_eq_diff! [Ord α]
{t₁ t₂ : Impl α β} (h₁ : t₁.WF) :
(t₁.diff t₂ h₁.balanced) = t₁.diff! t₂ := by
simp only [diff, diff!]
split
· rw [filter_eq_filter!]
. rw [eraseManyEntries_impl_eq_eraseManyEntries! h₁.balanced]
theorem WF.diff! {_ : Ord α} [TransOrd α]
{t₁ : Impl α β} (h₁ : t₁.WF) {t₂ : Impl α β} : (t₁.diff! t₂).WF := by
simp only [Impl.diff!]
split
. exact WF.filter! h₁
. exact WF.eraseManyEntries! h₁
/-!
### interSmaller
-/

View File

@@ -2877,330 +2877,6 @@ theorem get!_inter_of_not_mem_left [TransCmp cmp] [Inhabited β]
end Const
section Diff
variable {t₁ t₂ : DTreeMap α β cmp}
@[simp]
theorem diff_eq : t₁.diff t₂ = t₁ \ t₂ := by
simp only [SDiff.sdiff]
/- contains -/
@[simp]
theorem contains_diff [TransCmp cmp] {k : α} :
(t₁ \ t₂).contains k = (t₁.contains k && !t₂.contains k) :=
Impl.contains_diff t₁.wf t₂.wf
/- mem -/
@[simp]
theorem mem_diff_iff [TransCmp cmp] {k : α} :
k t₁ \ t₂ k t₁ ¬k t₂ :=
Impl.contains_diff_iff t₁.wf t₂.wf
theorem not_mem_diff_of_not_mem_left [TransCmp cmp]
{k : α} (h : ¬k t₁) :
¬k t₁ \ t₂ := by
rw [ contains_eq_false_iff_not_mem] at h
exact Impl.contains_diff_eq_false_of_contains_eq_false_left t₁.wf t₂.wf h
theorem not_mem_diff_of_mem_right [TransCmp cmp]
{k : α} (h : k t₂) :
¬ k t₁ \ t₂ := by
rw [ contains_eq_false_iff_not_mem]
exact Impl.contains_diff_eq_false_of_contains_right t₁.wf t₂.wf h
/- Equiv -/
theorem Equiv.diff_left {t₃ : DTreeMap α β cmp} [TransCmp cmp]
(equiv : t₁ ~m t₂) :
(t₁ \ t₃).Equiv (t₂ \ t₃) :=
Impl.Equiv.diff_left t₁.wf t₂.wf t₃.wf equiv.1
theorem Equiv.diff_right {t₃ : DTreeMap α β cmp} [TransCmp cmp]
(equiv : t₂ ~m t₃) :
(t₁ \ t₂).Equiv (t₁ \ t₃) :=
Impl.Equiv.diff_right t₁.wf t₂.wf t₃.wf equiv.1
theorem Equiv.diff_congr {t₃ t₄ : DTreeMap α β cmp} [TransCmp cmp]
(equiv₁ : t₁ ~m t₃) (equiv₂ : t₂ ~m t₄) :
(t₁ \ t₂).Equiv (t₃ \ t₄) :=
Impl.Equiv.diff_congr t₁.wf t₂.wf t₃.wf t₄.wf equiv₁.1 equiv₂.1
/- get? -/
theorem get?_diff [TransCmp cmp] [LawfulEqCmp cmp] {k : α} :
(t₁ \ t₂).get? k =
if k t₂ then none else t₁.get? k :=
Impl.get?_diff t₁.wf t₂.wf
theorem get?_diff_of_not_mem_right [TransCmp cmp] [LawfulEqCmp cmp]
{k : α} (h : ¬k t₂) :
(t₁ \ t₂).get? k = t₁.get? k := by
rw [ contains_eq_false_iff_not_mem] at h
exact Impl.get?_diff_of_contains_eq_false_right t₁.wf t₂.wf h
theorem get?_diff_of_not_mem_left [TransCmp cmp] [LawfulEqCmp cmp]
{k : α} (h : ¬k t₁) :
(t₁ \ t₂).get? k = none := by
rw [ contains_eq_false_iff_not_mem] at h
exact Impl.get?_diff_of_contains_eq_false_left t₁.wf t₂.wf h
theorem get?_diff_of_mem_right [TransCmp cmp] [LawfulEqCmp cmp]
{k : α} (h : k t₂) :
(t₁ \ t₂).get? k = none := by
rw [mem_iff_contains] at h
exact Impl.get?_diff_of_contains_right t₁.wf t₂.wf h
/- get -/
theorem get_diff [TransCmp cmp] [LawfulEqCmp cmp]
{k : α} {h_mem : k t₁ \ t₂} :
(t₁ \ t₂).get k h_mem =
t₁.get k (mem_diff_iff.1 h_mem).1 :=
Impl.get_diff t₁.wf t₂.wf
/- getD -/
theorem getD_diff [TransCmp cmp] [LawfulEqCmp cmp]
{k : α} {fallback : β k} :
(t₁ \ t₂).getD k fallback =
if k t₂ then fallback else t₁.getD k fallback :=
Impl.getD_diff t₁.wf t₂.wf
theorem getD_diff_of_not_mem_right [TransCmp cmp] [LawfulEqCmp cmp]
{k : α} {fallback : β k} (h : ¬k t₂) :
(t₁ \ t₂).getD k fallback = t₁.getD k fallback := by
rw [ contains_eq_false_iff_not_mem] at h
exact Impl.getD_diff_of_contains_eq_false_right t₁.wf t₂.wf h
theorem getD_diff_of_mem_right [TransCmp cmp] [LawfulEqCmp cmp]
{k : α} {fallback : β k} (h : k t₂) :
(t₁ \ t₂).getD k fallback = fallback := by
rw [mem_iff_contains] at h
exact Impl.getD_diff_of_contains_right t₁.wf t₂.wf h
theorem getD_diff_of_not_mem_left [TransCmp cmp] [LawfulEqCmp cmp]
{k : α} {fallback : β k} (h : ¬k t₁) :
(t₁ \ t₂).getD k fallback = fallback := by
rw [ contains_eq_false_iff_not_mem] at h
exact Impl.getD_diff_of_contains_eq_false_left t₁.wf t₂.wf h
/- get! -/
theorem get!_diff [TransCmp cmp] [LawfulEqCmp cmp]
{k : α} [Inhabited (β k)] :
(t₁ \ t₂).get! k =
if k t₂ then default else t₁.get! k :=
Impl.get!_diff t₁.wf t₂.wf
theorem get!_diff_of_not_mem_right [TransCmp cmp] [LawfulEqCmp cmp]
{k : α} [Inhabited (β k)] (h : ¬k t₂) :
(t₁ \ t₂).get! k = t₁.get! k := by
rw [ contains_eq_false_iff_not_mem] at h
exact Impl.get!_diff_of_contains_eq_false_right t₁.wf t₂.wf h
theorem get!_diff_of_mem_right [TransCmp cmp] [LawfulEqCmp cmp]
{k : α} [Inhabited (β k)] (h : k t₂) :
(t₁ \ t₂).get! k = default := by
rw [mem_iff_contains] at h
exact Impl.get!_diff_of_contains_right t₁.wf t₂.wf h
theorem get!_diff_of_not_mem_left [TransCmp cmp] [LawfulEqCmp cmp]
{k : α} [Inhabited (β k)] (h : ¬k t₁) :
(t₁ \ t₂).get! k = default := by
rw [ contains_eq_false_iff_not_mem] at h
exact Impl.get!_diff_of_contains_eq_false_left t₁.wf t₂.wf h
/- getKey? -/
theorem getKey?_diff [TransCmp cmp]
{k : α} :
(t₁ \ t₂).getKey? k =
if k t₂ then none else t₁.getKey? k :=
Impl.getKey?_diff t₁.wf t₂.wf
theorem getKey?_diff_of_not_mem_right [TransCmp cmp]
{k : α} (h : ¬k t₂) :
(t₁ \ t₂).getKey? k = t₁.getKey? k := by
rw [ contains_eq_false_iff_not_mem] at h
exact Impl.getKey?_diff_of_contains_eq_false_right t₁.wf t₂.wf h
theorem getKey?_diff_of_not_mem_left [TransCmp cmp]
{k : α} (h : ¬k t₁) :
(t₁ \ t₂).getKey? k = none := by
rw [ contains_eq_false_iff_not_mem] at h
exact Impl.getKey?_diff_of_contains_eq_false_left t₁.wf t₂.wf h
theorem getKey?_diff_of_mem_right [TransCmp cmp]
{k : α} (h : k t₂) :
(t₁ \ t₂).getKey? k = none := by
rw [mem_iff_contains] at h
exact Impl.getKey?_diff_of_contains_right t₁.wf t₂.wf h
/- getKey -/
theorem getKey_diff [TransCmp cmp]
{k : α} {h_mem : k t₁ \ t₂} :
(t₁ \ t₂).getKey k h_mem =
t₁.getKey k (mem_diff_iff.1 h_mem).1 :=
Impl.getKey_diff t₁.wf t₂.wf
/- getKeyD -/
theorem getKeyD_diff [TransCmp cmp] {k fallback : α} :
(t₁ \ t₂).getKeyD k fallback =
if k t₂ then fallback else t₁.getKeyD k fallback :=
Impl.getKeyD_diff t₁.wf t₂.wf
theorem getKeyD_diff_of_not_mem_right [TransCmp cmp] {k fallback : α} (h : ¬k t₂) :
(t₁ \ t₂).getKeyD k fallback = t₁.getKeyD k fallback := by
rw [ contains_eq_false_iff_not_mem] at h
exact Impl.getKeyD_diff_of_contains_eq_false_right t₁.wf t₂.wf h
theorem getKeyD_diff_of_mem_right [TransCmp cmp] {k fallback : α} (h : k t₂) :
(t₁ \ t₂).getKeyD k fallback = fallback := by
rw [mem_iff_contains] at h
exact Impl.getKeyD_diff_of_contains_right t₁.wf t₂.wf h
theorem getKeyD_diff_of_not_mem_left [TransCmp cmp] {k fallback : α} (h : ¬k t₁) :
(t₁ \ t₂).getKeyD k fallback = fallback := by
rw [ contains_eq_false_iff_not_mem] at h
exact Impl.getKeyD_diff_of_contains_eq_false_left t₁.wf t₂.wf h
/- getKey! -/
theorem getKey!_diff [Inhabited α] [TransCmp cmp]
{k : α} :
(t₁ \ t₂).getKey! k =
if k t₂ then default else t₁.getKey! k :=
Impl.getKey!_diff t₁.wf t₂.wf
theorem getKey!_diff_of_not_mem_right [Inhabited α] [TransCmp cmp]
{k : α} (h : ¬k t₂) :
(t₁ \ t₂).getKey! k = t₁.getKey! k := by
rw [ contains_eq_false_iff_not_mem] at h
exact Impl.getKey!_diff_of_contains_eq_false_right t₁.wf t₂.wf h
theorem getKey!_diff_of_mem_right [Inhabited α] [TransCmp cmp]
{k : α} (h : k t₂) :
(t₁ \ t₂).getKey! k = default := by
rw [mem_iff_contains] at h
exact Impl.getKey!_diff_of_contains_right t₁.wf t₂.wf h
theorem getKey!_diff_of_not_mem_left [Inhabited α] [TransCmp cmp]
{k : α} (h : ¬k t₁) :
(t₁ \ t₂).getKey! k = default := by
rw [ contains_eq_false_iff_not_mem] at h
exact Impl.getKey!_diff_of_contains_eq_false_left t₁.wf t₂.wf h
/- size -/
theorem size_diff_le_size_left [TransCmp cmp] :
(t₁ \ t₂).size t₁.size :=
Impl.size_diff_le_size_left t₁.wf t₂.wf
theorem size_diff_eq_size_left [TransCmp cmp]
(h : (a : α), a t₁ ¬a t₂) :
(t₁ \ t₂).size = t₁.size := by
conv at h =>
ext a
rhs
rw [ contains_eq_false_iff_not_mem]
exact Impl.size_diff_eq_size_left t₁.wf t₂.wf h
theorem size_diff_add_size_inter_eq_size_left [TransCmp cmp] :
(t₁ \ t₂).size + (t₁ t₂).size = t₁.size :=
Impl.size_diff_add_size_inter_eq_size_left t₁.wf t₂.wf
/- isEmpty -/
@[simp]
theorem isEmpty_diff_left [TransCmp cmp] (h : t₁.isEmpty) :
(t₁ \ t₂).isEmpty = true :=
Impl.isEmpty_diff_left t₁.wf t₂.wf h
theorem isEmpty_diff_iff [TransCmp cmp] :
(t₁ \ t₂).isEmpty k, k t₁ k t₂ := by
exact Impl.isEmpty_diff_iff t₁.wf t₂.wf
end Diff
namespace Const
variable {β : Type v} {t₁ t₂ : DTreeMap α (fun _ => β) cmp}
/- get? -/
theorem get?_diff [TransCmp cmp] {k : α} :
Const.get? (t₁ \ t₂) k =
if k t₂ then none else Const.get? t₁ k :=
Impl.Const.get?_diff t₁.wf t₂.wf
theorem get?_diff_of_not_mem_right [TransCmp cmp]
{k : α} (h : ¬k t₂) :
Const.get? (t₁ \ t₂) k = Const.get? t₁ k := by
rw [ contains_eq_false_iff_not_mem] at h
exact Impl.Const.get?_diff_of_contains_eq_false_right t₁.wf t₂.wf h
theorem get?_diff_of_not_mem_left [TransCmp cmp]
{k : α} (h : ¬k t₁) :
Const.get? (t₁ \ t₂) k = none := by
rw [ contains_eq_false_iff_not_mem] at h
exact Impl.Const.get?_diff_of_contains_eq_false_left t₁.wf t₂.wf h
theorem get?_diff_of_mem_right [TransCmp cmp]
{k : α} (h : k t₂) :
Const.get? (t₁ \ t₂) k = none := by
rw [mem_iff_contains] at h
exact Impl.Const.get?_diff_of_contains_right t₁.wf t₂.wf h
/- get -/
theorem get_diff [TransCmp cmp]
{k : α} {h_mem : k t₁ \ t₂} :
Const.get (t₁ \ t₂) k h_mem =
Const.get t₁ k (mem_diff_iff.1 h_mem).1 :=
Impl.Const.get_diff t₁.wf t₂.wf
/- getD -/
theorem getD_diff [TransCmp cmp]
{k : α} {fallback : β} :
Const.getD (t₁ \ t₂) k fallback =
if k t₂ then fallback else Const.getD t₁ k fallback :=
Impl.Const.getD_diff t₁.wf t₂.wf
theorem getD_diff_of_not_mem_right [TransCmp cmp]
{k : α} {fallback : β} (h : ¬k t₂) :
Const.getD (t₁ \ t₂) k fallback = Const.getD t₁ k fallback := by
rw [ contains_eq_false_iff_not_mem] at h
exact Impl.Const.getD_diff_of_contains_eq_false_right t₁.wf t₂.wf h
theorem getD_diff_of_mem_right [TransCmp cmp]
{k : α} {fallback : β} (h : k t₂) :
Const.getD (t₁ \ t₂) k fallback = fallback := by
rw [mem_iff_contains] at h
exact Impl.Const.getD_diff_of_contains_right t₁.wf t₂.wf h
theorem getD_diff_of_not_mem_left [TransCmp cmp]
{k : α} {fallback : β} (h : ¬k t₁) :
Const.getD (t₁ \ t₂) k fallback = fallback := by
rw [ contains_eq_false_iff_not_mem] at h
exact Impl.Const.getD_diff_of_contains_eq_false_left t₁.wf t₂.wf h
/- get! -/
theorem get!_diff [TransCmp cmp] [Inhabited β]
{k : α} :
Const.get! (t₁ \ t₂) k =
if k t₂ then default else Const.get! t₁ k :=
Impl.Const.get!_diff t₁.wf t₂.wf
theorem get!_diff_of_not_mem_right [TransCmp cmp] [Inhabited β]
{k : α} (h : ¬k t₂) :
Const.get! (t₁ \ t₂) k = Const.get! t₁ k := by
rw [ contains_eq_false_iff_not_mem] at h
exact Impl.Const.get!_diff_of_contains_eq_false_right t₁.wf t₂.wf h
theorem get!_diff_of_mem_right [TransCmp cmp] [Inhabited β]
{k : α} (h : k t₂) :
Const.get! (t₁ \ t₂) k = default := by
rw [mem_iff_contains] at h
exact Impl.Const.get!_diff_of_contains_right t₁.wf t₂.wf h
theorem get!_diff_of_not_mem_left [TransCmp cmp] [Inhabited β]
{k : α} (h : ¬k t₁) :
Const.get! (t₁ \ t₂) k = default := by
rw [ contains_eq_false_iff_not_mem] at h
exact Impl.Const.get!_diff_of_contains_eq_false_left t₁.wf t₂.wf h
end Const
section Alter
theorem isEmpty_alter_eq_isEmpty_erase [TransCmp cmp] [LawfulEqCmp cmp] {k : α}

View File

@@ -732,15 +732,6 @@ def inter (t₁ t₂ : Raw α β cmp) : Raw α β cmp :=
instance : Inter (Raw α β cmp) := inter
/--
Computes the diffrence of the given tree maps.
This function always iteraters through the smaller map.
-/
def diff (t₁ t₂ : Raw α β cmp) : Raw α β cmp :=
letI : Ord α := cmp; t₁.inner.diff! t₂.inner
instance : SDiff (Raw α β cmp) := diff
@[inline, inherit_doc DTreeMap.eraseMany]
def eraseMany {ρ} [ForIn Id ρ α] (t : Raw α β cmp) (l : ρ) : Raw α β cmp :=
letI : Ord α := cmp; t.inner.eraseMany! l

View File

@@ -3042,374 +3042,6 @@ theorem get!_inter_of_not_mem_left [TransCmp cmp] [Inhabited β] (h₁ : m₁.WF
end Const
section Diff
variable {t₁ t₂ : Raw α β cmp}
@[simp]
theorem diff_eq : t₁.diff t₂ = t₁ \ t₂ := by
simp only [SDiff.sdiff]
/- contains -/
@[simp]
theorem contains_diff [TransCmp cmp] (h₁ : t₁.WF)
(h₂ : t₂.WF) {k : α} :
(t₁ \ t₂).contains k = (t₁.contains k && !t₂.contains k) := by
simp only [SDiff.sdiff]
exact Impl.contains_diff! h₁ h₂
/- mem -/
@[simp]
theorem mem_diff_iff [TransCmp cmp] (h₁ : t₁.WF)
(h₂ : t₂.WF) {k : α} :
k t₁ \ t₂ k t₁ ¬k t₂ := by
simp only [SDiff.sdiff, Membership.mem]
exact Impl.contains_diff!_iff h₁ h₂
theorem not_mem_diff_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} (h : ¬k t₁) :
¬k t₁ \ t₂ := by
rw [ contains_eq_false_iff_not_mem] at h
simp only [SDiff.sdiff]
exact Impl.contains_diff!_eq_false_of_contains_eq_false_left h₁ h₂ h
theorem not_mem_diff_of_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} (h : k t₂) :
¬k t₁ \ t₂ := by
rw [ contains_eq_false_iff_not_mem]
simp only [SDiff.sdiff]
exact Impl.contains_diff!_eq_false_of_contains_right h₁ h₂ h
theorem Equiv.diff_left [TransCmp cmp] {t₃ : Raw α β cmp}
(h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (equiv : t₁ ~m t₂) :
(t₁ \ t₃).Equiv (t₂ \ t₃) := by
simp only [SDiff.sdiff]
exact @Impl.Equiv.diff!_left _ _ cmp t₁.inner t₂.inner t₃.inner _ h₁.out h₂.out h₃.out equiv.1
theorem Equiv.diff_right [TransCmp cmp] {t₃ : Raw α β cmp}
(h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (equiv : t₂ ~m t₃) :
(t₁ \ t₂).Equiv (t₁ \ t₃) := by
simp only [SDiff.sdiff]
exact @Impl.Equiv.diff!_right _ _ cmp t₁.inner t₂.inner t₃.inner _ h₁.out h₂.out h₃.out equiv.1
theorem Equiv.diff_congr [TransCmp cmp] {t₃ t₄ : Raw α β cmp}
(h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (h₄ : t₄.WF)
(equiv₁ : t₁ ~m t₃) (equiv₂ : t₂ ~m t₄) :
(t₁ \ t₂).Equiv (t₃ \ t₄) := by
simp only [SDiff.sdiff]
exact @Impl.Equiv.diff!_congr _ _ cmp t₁.inner t₂.inner t₃.inner t₄.inner _ h₁.out h₂.out h₃.out h₄.out equiv₁.1 equiv₂.1
/- get? -/
theorem get?_diff [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} :
(t₁ \ t₂).get? k =
if t₂.contains k then none else t₁.get? k :=
Impl.get?_diff! h₁ h₂
theorem get?_diff_of_not_mem_right [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} (h : ¬k t₂) :
(t₁ \ t₂).get? k = t₁.get? k := by
rw [ contains_eq_false_iff_not_mem] at h
simp only [SDiff.sdiff]
exact Impl.get?_diff!_of_contains_eq_false_right h₁ h₂ h
theorem get?_diff_of_not_mem_left [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} (h : ¬k t₁) :
(t₁ \ t₂).get? k = none := by
rw [ contains_eq_false_iff_not_mem] at h
simp only [SDiff.sdiff]
exact Impl.get?_diff!_of_contains_eq_false_left h₁ h₂ h
theorem get?_diff_of_mem_right [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} (h : k t₂) :
(t₁ \ t₂).get? k = none :=
Impl.get?_diff!_of_contains_right h₁ h₂ h
/- get -/
theorem get_diff [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} {h_mem : k t₁ \ t₂} :
(t₁ \ t₂).get k h_mem =
t₁.get k ((mem_diff_iff h₁ h₂).1 h_mem).1 :=
Impl.get_diff! h₁ h₂
/- getD -/
theorem getD_diff [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} {fallback : β k} :
(t₁ \ t₂).getD k fallback =
if t₂.contains k then fallback else t₁.getD k fallback :=
Impl.getD_diff! h₁ h₂
theorem getD_diff_of_not_mem_right [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} {fallback : β k} (h : ¬k t₂) :
(t₁ \ t₂).getD k fallback = t₁.getD k fallback := by
rw [ contains_eq_false_iff_not_mem] at h
simp only [SDiff.sdiff]
exact Impl.getD_diff!_of_contains_eq_false_right h₁ h₂ h
theorem getD_diff_of_mem_right [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} {fallback : β k} (h : k t₂) :
(t₁ \ t₂).getD k fallback = fallback :=
Impl.getD_diff!_of_contains_right h₁ h₂ h
theorem getD_diff_of_not_mem_left [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} {fallback : β k} (h : ¬k t₁) :
(t₁ \ t₂).getD k fallback = fallback := by
rw [ contains_eq_false_iff_not_mem] at h
simp only [SDiff.sdiff]
exact Impl.getD_diff!_of_contains_eq_false_left h₁ h₂ h
/- get! -/
theorem get!_diff [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} [Inhabited (β k)] :
(t₁ \ t₂).get! k =
if t₂.contains k then default else t₁.get! k :=
Impl.get!_diff! h₁ h₂
theorem get!_diff_of_not_mem_right [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} [Inhabited (β k)] (h : ¬k t₂) :
(t₁ \ t₂).get! k = t₁.get! k := by
rw [ contains_eq_false_iff_not_mem] at h
simp only [SDiff.sdiff]
exact Impl.get!_diff!_of_contains_eq_false_right h₁ h₂ h
theorem get!_diff_of_mem_right [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} [Inhabited (β k)] (h : k t₂) :
(t₁ \ t₂).get! k = default :=
Impl.get!_diff!_of_contains_right h₁ h₂ h
theorem get!_diff_of_not_mem_left [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} [Inhabited (β k)] (h : ¬k t₁) :
(t₁ \ t₂).get! k = default := by
rw [ contains_eq_false_iff_not_mem] at h
simp only [SDiff.sdiff]
exact Impl.get!_diff!_of_contains_eq_false_left h₁ h₂ h
/- getKey? -/
theorem getKey?_diff [TransCmp cmp]
(h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} :
(t₁ \ t₂).getKey? k =
if t₂.contains k then none else t₁.getKey? k :=
Impl.getKey?_diff! h₁ h₂
theorem getKey?_diff_of_not_mem_right [TransCmp cmp]
(h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} (h : ¬k t₂) :
(t₁ \ t₂).getKey? k = t₁.getKey? k := by
rw [ contains_eq_false_iff_not_mem] at h
simp only [SDiff.sdiff]
exact Impl.getKey?_diff!_of_contains_eq_false_right h₁ h₂ h
theorem getKey?_diff_of_not_mem_left [TransCmp cmp]
(h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} (h : ¬k t₁) :
(t₁ \ t₂).getKey? k = none := by
rw [ contains_eq_false_iff_not_mem] at h
simp only [SDiff.sdiff]
exact Impl.getKey?_diff!_of_contains_eq_false_left h₁ h₂ h
theorem getKey?_diff_of_mem_right [TransCmp cmp]
(h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} (h : k t₂) :
(t₁ \ t₂).getKey? k = none :=
Impl.getKey?_diff!_of_contains_right h₁ h₂ h
/- getKey -/
theorem getKey_diff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} {h_mem : k t₁ \ t₂} :
(t₁ \ t₂).getKey k h_mem =
t₁.getKey k ((mem_diff_iff h₁ h₂).1 h_mem).1 :=
Impl.getKey_diff! h₁ h₂
/- getKeyD -/
theorem getKeyD_diff [TransCmp cmp] (h₁ : t₁.WF)
(h₂ : t₂.WF) {k fallback : α} :
(t₁ \ t₂).getKeyD k fallback =
if t₂.contains k then fallback else t₁.getKeyD k fallback :=
Impl.getKeyD_diff! h₁ h₂
theorem getKeyD_diff_of_not_mem_right [TransCmp cmp] (h₁ : t₁.WF)
(h₂ : t₂.WF) {k fallback : α} (h : ¬k t₂) :
(t₁ \ t₂).getKeyD k fallback = t₁.getKeyD k fallback := by
rw [ contains_eq_false_iff_not_mem] at h
simp only [SDiff.sdiff]
exact Impl.getKeyD_diff!_of_contains_eq_false_right h₁ h₂ h
theorem getKeyD_diff_of_mem_right [TransCmp cmp] (h₁ : t₁.WF)
(h₂ : t₂.WF) {k fallback : α} (h : k t₂) :
(t₁ \ t₂).getKeyD k fallback = fallback :=
Impl.getKeyD_diff!_of_contains_right h₁ h₂ h
theorem getKeyD_diff_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF)
(h₂ : t₂.WF) {k fallback : α} (h : ¬k t₁) :
(t₁ \ t₂).getKeyD k fallback = fallback := by
rw [ contains_eq_false_iff_not_mem] at h
simp only [SDiff.sdiff]
exact Impl.getKeyD_diff!_of_contains_eq_false_left h₁ h₂ h
/- getKey! -/
theorem getKey!_diff [TransCmp cmp] [Inhabited α]
(h₁ : t₁.WF)
(h₂ : t₂.WF) {k : α} :
(t₁ \ t₂).getKey! k =
if t₂.contains k then default else t₁.getKey! k :=
Impl.getKey!_diff! h₁ h₂
theorem getKey!_diff_of_not_mem_right [Inhabited α]
[TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α}
(h : ¬k t₂) :
(t₁ \ t₂).getKey! k = t₁.getKey! k := by
rw [ contains_eq_false_iff_not_mem] at h
simp only [SDiff.sdiff]
exact Impl.getKey!_diff!_of_contains_eq_false_right h₁ h₂ h
theorem getKey!_diff_of_mem_right [Inhabited α]
[TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α}
(h : k t₂) :
(t₁ \ t₂).getKey! k = default :=
Impl.getKey!_diff!_of_contains_right h₁ h₂ h
theorem getKey!_diff_of_not_mem_left [Inhabited α]
[TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α}
(h : ¬k t₁) :
(t₁ \ t₂).getKey! k = default := by
rw [ contains_eq_false_iff_not_mem] at h
simp only [SDiff.sdiff]
exact Impl.getKey!_diff!_of_contains_eq_false_left h₁ h₂ h
/- size -/
theorem size_diff_le_size_left [TransCmp cmp] (h₁ : t₁.WF)
(h₂ : t₂.WF) :
(t₁ \ t₂).size t₁.size :=
Impl.size_diff!_le_size_left h₁ h₂
theorem size_diff_eq_size_left [TransCmp cmp] (h₁ : t₁.WF)
(h₂ : t₂.WF)
(h : (a : α), a t₁ ¬a t₂) :
(t₁ \ t₂).size = t₁.size := by
conv at h =>
ext a
rhs
rw [ contains_eq_false_iff_not_mem]
exact Impl.size_diff!_eq_size_left h₁ h₂ h
theorem size_diff_add_size_inter_eq_size_left [TransCmp cmp]
(h₁ : t₁.WF) (h₂ : t₂.WF) :
(t₁ \ t₂).size + (t₁ t₂).size = t₁.size :=
Impl.size_diff!_add_size_inter!_eq_size_left h₁ h₂
/- isEmpty -/
@[simp]
theorem isEmpty_diff_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.isEmpty) :
(t₁ \ t₂).isEmpty = true :=
Impl.isEmpty_diff!_left h₁ h₂ h
theorem isEmpty_diff_iff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
(t₁ \ t₂).isEmpty k, k t₁ k t₂ := by
exact Impl.isEmpty_diff!_iff h₁ h₂
end Diff
namespace Const
variable {β : Type v} {m₁ m₂ : Raw α (fun _ => β) cmp}
/- get? -/
theorem get?_diff [TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
Const.get? (m₁ \ m₂) k =
if m₂.contains k then none else Const.get? m₁ k := by
simp only [SDiff.sdiff]
exact Impl.Const.get?_diff! h₁ h₂
theorem get?_diff_of_not_mem_right [TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : ¬k m₂) :
Const.get? (m₁ \ m₂) k = Const.get? m₁ k := by
rw [ contains_eq_false_iff_not_mem] at h
simp only [SDiff.sdiff]
exact Impl.Const.get?_diff!_of_contains_eq_false_right h₁ h₂ h
theorem get?_diff_of_not_mem_left [TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : ¬k m₁) :
Const.get? (m₁ \ m₂) k = none := by
rw [ contains_eq_false_iff_not_mem] at h
simp only [SDiff.sdiff]
exact Impl.Const.get?_diff!_of_contains_eq_false_left h₁ h₂ h
theorem get?_diff_of_mem_right [TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : k m₂) :
Const.get? (m₁ \ m₂) k = none := by
rw [mem_iff_contains] at h
simp only [SDiff.sdiff]
exact Impl.Const.get?_diff!_of_contains_right h₁ h₂ h
/- get -/
theorem get_diff [TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {h_mem : k m₁ \ m₂} :
Const.get (m₁ \ m₂) k h_mem =
Const.get m₁ k ((mem_diff_iff h₁ h₂).1 h_mem).1 := by
simp only [SDiff.sdiff]
exact Impl.Const.get_diff! h₁ h₂
/- getD -/
theorem getD_diff [TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {fallback : β} :
Const.getD (m₁ \ m₂) k fallback =
if m₂.contains k then fallback else Const.getD m₁ k fallback := by
simp only [SDiff.sdiff]
exact Impl.Const.getD_diff! h₁ h₂
theorem getD_diff_of_not_mem_right [TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {fallback : β} (h : ¬k m₂) :
Const.getD (m₁ \ m₂) k fallback = Const.getD m₁ k fallback := by
rw [ contains_eq_false_iff_not_mem] at h
simp only [SDiff.sdiff]
exact Impl.Const.getD_diff!_of_contains_eq_false_right h₁ h₂ h
theorem getD_diff_of_mem_right [TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {fallback : β} (h : k m₂) :
Const.getD (m₁ \ m₂) k fallback = fallback := by
rw [mem_iff_contains] at h
simp only [SDiff.sdiff]
exact Impl.Const.getD_diff!_of_contains_right h₁ h₂ h
theorem getD_diff_of_not_mem_left [TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} {fallback : β} (h : ¬k m₁) :
Const.getD (m₁ \ m₂) k fallback = fallback := by
rw [ contains_eq_false_iff_not_mem] at h
simp only [SDiff.sdiff]
exact Impl.Const.getD_diff!_of_contains_eq_false_left h₁ h₂ h
/- get! -/
theorem get!_diff [TransCmp cmp] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} :
Const.get! (m₁ \ m₂) k =
if m₂.contains k then default else Const.get! m₁ k := by
simp only [SDiff.sdiff]
exact Impl.Const.get!_diff! h₁ h₂
theorem get!_diff_of_not_mem_right [TransCmp cmp] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : ¬k m₂) :
Const.get! (m₁ \ m₂) k = Const.get! m₁ k := by
rw [ contains_eq_false_iff_not_mem] at h
simp only [SDiff.sdiff]
exact Impl.Const.get!_diff!_of_contains_eq_false_right h₁ h₂ h
theorem get!_diff_of_mem_right [TransCmp cmp] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : k m₂) :
Const.get! (m₁ \ m₂) k = default := by
rw [mem_iff_contains] at h
simp only [SDiff.sdiff]
exact Impl.Const.get!_diff!_of_contains_right h₁ h₂ h
theorem get!_diff_of_not_mem_left [TransCmp cmp] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
{k : α} (h : ¬k m₁) :
Const.get! (m₁ \ m₂) k = default := by
rw [ contains_eq_false_iff_not_mem] at h
simp only [SDiff.sdiff]
exact Impl.Const.get!_diff!_of_contains_eq_false_left h₁ h₂ h
end Const
section Alter
theorem isEmpty_alter_eq_isEmpty_erase [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α}

View File

@@ -165,8 +165,4 @@ theorem inter [TransCmp cmp] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) :
(t₁ t₂).WF :=
Impl.WF.inter! h₁.out
theorem diff [TransCmp cmp] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) :
(t₁ \ t₂).WF :=
Impl.WF.diff! h₁.out
end Std.DTreeMap.Raw.WF.Const

View File

@@ -501,12 +501,6 @@ def inter (t₁ t₂ : TreeMap α β cmp) : TreeMap α β cmp :=
instance : Inter (TreeMap α β cmp) := inter
@[inline, inherit_doc DTreeMap.diff]
def diff (t₁ t₂ : TreeMap α β cmp) : TreeMap α β cmp :=
letI : Ord α := cmp; DTreeMap.diff t₁.inner t₂.inner
instance : SDiff (TreeMap α β cmp) := diff
@[inline, inherit_doc DTreeMap.Const.insertManyIfNewUnit]
def insertManyIfNewUnit {ρ} [ForIn Id ρ α] (t : TreeMap α Unit cmp) (l : ρ) : TreeMap α Unit cmp :=
DTreeMap.Const.insertManyIfNewUnit t.inner l

View File

@@ -1961,221 +1961,6 @@ theorem isEmpty_inter_iff [TransCmp cmp] :
end Inter
section Diff
variable {t₁ t₂ : TreeMap α β cmp}
@[simp]
theorem diff_eq : t₁.diff t₂ = t₁ \ t₂ := by
simp only [SDiff.sdiff]
/- contains -/
@[simp]
theorem contains_diff [TransCmp cmp] {k : α} :
(t₁ \ t₂).contains k = (t₁.contains k && !t₂.contains k) :=
DTreeMap.contains_diff
/- mem -/
@[simp]
theorem mem_diff_iff [TransCmp cmp] {k : α} :
k t₁ \ t₂ k t₁ k t₂ :=
DTreeMap.mem_diff_iff
theorem not_mem_diff_of_not_mem_left [TransCmp cmp] {k : α}
(not_mem : k t₁) :
k t₁ \ t₂ :=
DTreeMap.not_mem_diff_of_not_mem_left not_mem
theorem not_mem_diff_of_mem_right [TransCmp cmp] {k : α}
(mem : k t₂) :
k t₁ \ t₂ :=
DTreeMap.not_mem_diff_of_mem_right mem
/- Equiv -/
theorem Equiv.diff_left {t₃ : TreeMap α β cmp} [TransCmp cmp]
(equiv : t₁ ~m t₂) :
(t₁ \ t₃).Equiv (t₂ \ t₃) := by
constructor
apply DTreeMap.Equiv.diff_left equiv.1
theorem Equiv.diff_right {t₃ : TreeMap α β cmp} [TransCmp cmp]
(equiv : t₂ ~m t₃) :
(t₁ \ t₂).Equiv (t₁ \ t₃) := by
constructor
apply DTreeMap.Equiv.diff_right equiv.1
theorem Equiv.diff_congr {t₃ t₄ : TreeMap α β cmp} [TransCmp cmp]
(equiv₁ : t₁ ~m t₃) (equiv₂ : t₂ ~m t₄) :
(t₁ \ t₂).Equiv (t₃ \ t₄) := by
constructor
apply DTreeMap.Equiv.diff_congr equiv₁.1 equiv₂.1
/- get? -/
theorem get?_diff [TransCmp cmp] {k : α} :
(t₁ \ t₂).get? k =
if k t₂ then none else t₁.get? k :=
DTreeMap.Const.get?_diff
theorem get?_diff_of_not_mem_right [TransCmp cmp]
{k : α} (not_mem : k t₂) :
(t₁ \ t₂).get? k = t₁.get? k :=
DTreeMap.Const.get?_diff_of_not_mem_right not_mem
theorem get?_diff_of_not_mem_left [TransCmp cmp]
{k : α} (not_mem : k t₁) :
(t₁ \ t₂).get? k = none :=
DTreeMap.Const.get?_diff_of_not_mem_left not_mem
theorem get?_diff_of_mem_right [TransCmp cmp]
{k : α} (mem : k t₂) :
(t₁ \ t₂).get? k = none :=
DTreeMap.Const.get?_diff_of_mem_right mem
/- get -/
theorem get_diff [TransCmp cmp]
{k : α} {h_mem : k t₁ \ t₂} :
(t₁ \ t₂).get k h_mem =
t₁.get k (mem_diff_iff.1 h_mem).1 :=
DTreeMap.Const.get_diff
/- getD -/
theorem getD_diff [TransCmp cmp] {k : α} {fallback : β} :
(t₁ \ t₂).getD k fallback =
if k t₂ then fallback else t₁.getD k fallback :=
DTreeMap.Const.getD_diff
theorem getD_diff_of_not_mem_right [TransCmp cmp]
{k : α} {fallback : β} (not_mem : k t₂) :
(t₁ \ t₂).getD k fallback = t₁.getD k fallback :=
DTreeMap.Const.getD_diff_of_not_mem_right not_mem
theorem getD_diff_of_mem_right [TransCmp cmp]
{k : α} {fallback : β} (mem : k t₂) :
(t₁ \ t₂).getD k fallback = fallback :=
DTreeMap.Const.getD_diff_of_mem_right mem
theorem getD_diff_of_not_mem_left [TransCmp cmp]
{k : α} {fallback : β} (not_mem : k t₁) :
(t₁ \ t₂).getD k fallback = fallback :=
DTreeMap.Const.getD_diff_of_not_mem_left not_mem
/- get! -/
theorem get!_diff [TransCmp cmp] {k : α} [Inhabited β] :
(t₁ \ t₂).get! k =
if k t₂ then default else t₁.get! k :=
DTreeMap.Const.get!_diff
theorem get!_diff_of_not_mem_right [TransCmp cmp]
{k : α} [Inhabited β] (not_mem : k t₂) :
(t₁ \ t₂).get! k = t₁.get! k :=
DTreeMap.Const.get!_diff_of_not_mem_right not_mem
theorem get!_diff_of_mem_right [TransCmp cmp]
{k : α} [Inhabited β] (mem : k t₂) :
(t₁ \ t₂).get! k = default :=
DTreeMap.Const.get!_diff_of_mem_right mem
theorem get!_diff_of_not_mem_left [TransCmp cmp]
{k : α} [Inhabited β] (not_mem : k t₁) :
(t₁ \ t₂).get! k = default :=
DTreeMap.Const.get!_diff_of_not_mem_left not_mem
/- getKey? -/
theorem getKey?_diff [TransCmp cmp] {k : α} :
(t₁ \ t₂).getKey? k =
if k t₂ then none else t₁.getKey? k :=
DTreeMap.getKey?_diff
theorem getKey?_diff_of_not_mem_right [TransCmp cmp]
{k : α} (not_mem : k t₂) :
(t₁ \ t₂).getKey? k = t₁.getKey? k :=
DTreeMap.getKey?_diff_of_not_mem_right not_mem
theorem getKey?_diff_of_not_mem_left [TransCmp cmp]
{k : α} (not_mem : k t₁) :
(t₁ \ t₂).getKey? k = none :=
DTreeMap.getKey?_diff_of_not_mem_left not_mem
theorem getKey?_diff_of_mem_right [TransCmp cmp]
{k : α} (mem : k t₂) :
(t₁ \ t₂).getKey? k = none :=
DTreeMap.getKey?_diff_of_mem_right mem
/- getKey -/
theorem getKey_diff [TransCmp cmp]
{k : α} {h_mem : k t₁ \ t₂} :
(t₁ \ t₂).getKey k h_mem =
t₁.getKey k (mem_diff_iff.1 h_mem).1 :=
DTreeMap.getKey_diff
/- getKeyD -/
theorem getKeyD_diff [TransCmp cmp] {k fallback : α} :
(t₁ \ t₂).getKeyD k fallback =
if k t₂ then fallback else t₁.getKeyD k fallback :=
DTreeMap.getKeyD_diff
theorem getKeyD_diff_of_not_mem_right [TransCmp cmp]
{k fallback : α} (not_mem : k t₂) :
(t₁ \ t₂).getKeyD k fallback = t₁.getKeyD k fallback :=
DTreeMap.getKeyD_diff_of_not_mem_right not_mem
theorem getKeyD_diff_of_mem_right [TransCmp cmp]
{k fallback : α} (mem : k t₂) :
(t₁ \ t₂).getKeyD k fallback = fallback :=
DTreeMap.getKeyD_diff_of_mem_right mem
theorem getKeyD_diff_of_not_mem_left [TransCmp cmp]
{k fallback : α} (not_mem : k t₁) :
(t₁ \ t₂).getKeyD k fallback = fallback :=
DTreeMap.getKeyD_diff_of_not_mem_left not_mem
/- getKey! -/
theorem getKey!_diff [TransCmp cmp] [Inhabited α] {k : α} :
(t₁ \ t₂).getKey! k =
if k t₂ then default else t₁.getKey! k :=
DTreeMap.getKey!_diff
theorem getKey!_diff_of_not_mem_right [TransCmp cmp] [Inhabited α]
{k : α} (not_mem : k t₂) :
(t₁ \ t₂).getKey! k = t₁.getKey! k :=
DTreeMap.getKey!_diff_of_not_mem_right not_mem
theorem getKey!_diff_of_mem_right [TransCmp cmp] [Inhabited α]
{k : α} (mem : k t₂) :
(t₁ \ t₂).getKey! k = default :=
DTreeMap.getKey!_diff_of_mem_right mem
theorem getKey!_diff_of_not_mem_left [TransCmp cmp] [Inhabited α]
{k : α} (not_mem : k t₁) :
(t₁ \ t₂).getKey! k = default :=
DTreeMap.getKey!_diff_of_not_mem_left not_mem
/- size -/
theorem size_diff_le_size_left [TransCmp cmp] :
(t₁ \ t₂).size t₁.size :=
DTreeMap.size_diff_le_size_left
theorem size_diff_eq_size_left [TransCmp cmp]
(h : (a : α), a t₁ a t₂) :
(t₁ \ t₂).size = t₁.size :=
DTreeMap.size_diff_eq_size_left h
theorem size_diff_add_size_inter_eq_size_left [TransCmp cmp] :
(t₁ \ t₂).size + (t₁ t₂).size = t₁.size :=
DTreeMap.size_diff_add_size_inter_eq_size_left
/- isEmpty -/
@[simp]
theorem isEmpty_diff_left [TransCmp cmp] (h : t₁.isEmpty) :
(t₁ \ t₂).isEmpty = true :=
DTreeMap.isEmpty_diff_left h
theorem isEmpty_diff_iff [TransCmp cmp] :
(t₁ \ t₂).isEmpty k, k t₁ k t₂ :=
DTreeMap.isEmpty_diff_iff
end Diff
section Alter
theorem isEmpty_alter_eq_isEmpty_erase [TransCmp cmp] {k : α}

View File

@@ -503,12 +503,6 @@ def inter (t₁ t₂ : Raw α β cmp) : Raw α β cmp :=
instance : Inter (Raw α β cmp) := inter
@[inline, inherit_doc DTreeMap.Raw.diff]
def diff (t₁ t₂ : Raw α β cmp) : Raw α β cmp :=
DTreeMap.Raw.diff t₁.inner t₂.inner
instance : SDiff (Raw α β cmp) := diff
@[inline, inherit_doc DTreeMap.Raw.Const.insertManyIfNewUnit]
def insertManyIfNewUnit {ρ} [ForIn Id ρ α] (t : Raw α Unit cmp) (l : ρ) : Raw α Unit cmp :=
DTreeMap.Raw.Const.insertManyIfNewUnit t.inner l

View File

@@ -2012,231 +2012,6 @@ theorem isEmpty_inter_iff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
end Inter
section Diff
variable {t₁ t₂ : Raw α β cmp}
@[simp]
theorem diff_eq : t₁.diff t₂ = t₁ \ t₂ := by
simp only [SDiff.sdiff]
/- contains -/
@[simp]
theorem contains_diff [TransCmp cmp] (h₁ : t₁.WF)
(h₂ : t₂.WF) {k : α} :
(t₁ \ t₂).contains k = (t₁.contains k && !t₂.contains k) :=
DTreeMap.Raw.contains_diff h₁ h₂
/- mem -/
@[simp]
theorem mem_diff_iff [TransCmp cmp] (h₁ : t₁.WF)
(h₂ : t₂.WF) {k : α} :
k t₁ \ t₂ k t₁ k t₂ :=
DTreeMap.Raw.mem_diff_iff h₁ h₂
theorem not_mem_diff_of_not_mem_left [TransCmp cmp]
(h₁ : t₁.WF) (h₂ : t₂.WF) {k : α}
(not_mem : k t₁) :
k t₁ \ t₂ :=
DTreeMap.Raw.not_mem_diff_of_not_mem_left h₁ h₂ not_mem
theorem not_mem_diff_of_mem_right [TransCmp cmp]
(h₁ : t₁.WF) (h₂ : t₂.WF) {k : α}
(mem : k t₂) :
k t₁ \ t₂ :=
DTreeMap.Raw.not_mem_diff_of_mem_right h₁ h₂ mem
/- Equiv -/
theorem Equiv.diff_left [TransCmp cmp] {t₃ : Raw α β cmp}
(h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (equiv : t₁ ~m t₂) :
(t₁ \ t₃).Equiv (t₂ \ t₃) :=
DTreeMap.Raw.Equiv.diff_left h₁ h₂ h₃ equiv.1
theorem Equiv.diff_right [TransCmp cmp] {t₃ : Raw α β cmp}
(h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (equiv : t₂ ~m t₃) :
(t₁ \ t₂).Equiv (t₁ \ t₃) :=
DTreeMap.Raw.Equiv.diff_right h₁ h₂ h₃ equiv.1
theorem Equiv.diff_congr [TransCmp cmp] {t₃ t₄ : Raw α β cmp}
(h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (h₄ : t₄.WF)
(equiv₁ : t₁ ~m t₃) (equiv₂ : t₂ ~m t₄) :
(t₁ \ t₂).Equiv (t₃ \ t₄) :=
DTreeMap.Raw.Equiv.diff_congr h₁ h₂ h₃ h₄ equiv₁.1 equiv₂.1
/- get? -/
theorem get?_diff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} :
(t₁ \ t₂).get? k =
if k t₂ then none else t₁.get? k :=
DTreeMap.Raw.Const.get?_diff h₁ h₂
theorem get?_diff_of_not_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} (not_mem : k t₂) :
(t₁ \ t₂).get? k = t₁.get? k :=
DTreeMap.Raw.Const.get?_diff_of_not_mem_right h₁ h₂ not_mem
theorem get?_diff_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} (not_mem : k t₁) :
(t₁ \ t₂).get? k = none :=
DTreeMap.Raw.Const.get?_diff_of_not_mem_left h₁ h₂ not_mem
theorem get?_diff_of_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} (mem : k t₂) :
(t₁ \ t₂).get? k = none :=
DTreeMap.Raw.Const.get?_diff_of_mem_right h₁ h₂ mem
/- get -/
theorem get_diff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} {h_mem : k t₁ \ t₂} :
(t₁ \ t₂).get k h_mem =
t₁.get k ((mem_diff_iff h₁ h₂).1 h_mem).1 :=
DTreeMap.Raw.Const.get_diff h₁ h₂
/- getD -/
theorem getD_diff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} {fallback : β} :
(t₁ \ t₂).getD k fallback =
if k t₂ then fallback else t₁.getD k fallback :=
DTreeMap.Raw.Const.getD_diff h₁ h₂
theorem getD_diff_of_not_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} {fallback : β} (not_mem : k t₂) :
(t₁ \ t₂).getD k fallback = t₁.getD k fallback :=
DTreeMap.Raw.Const.getD_diff_of_not_mem_right h₁ h₂ not_mem
theorem getD_diff_of_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} {fallback : β} (mem : k t₂) :
(t₁ \ t₂).getD k fallback = fallback :=
DTreeMap.Raw.Const.getD_diff_of_mem_right h₁ h₂ mem
theorem getD_diff_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} {fallback : β} (not_mem : k t₁) :
(t₁ \ t₂).getD k fallback = fallback :=
DTreeMap.Raw.Const.getD_diff_of_not_mem_left h₁ h₂ not_mem
/- get! -/
theorem get!_diff [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} :
(t₁ \ t₂).get! k =
if k t₂ then default else t₁.get! k :=
DTreeMap.Raw.Const.get!_diff h₁ h₂
theorem get!_diff_of_not_mem_right [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} (not_mem : k t₂) :
(t₁ \ t₂).get! k = t₁.get! k :=
DTreeMap.Raw.Const.get!_diff_of_not_mem_right h₁ h₂ not_mem
theorem get!_diff_of_mem_right [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} (mem : k t₂) :
(t₁ \ t₂).get! k = default :=
DTreeMap.Raw.Const.get!_diff_of_mem_right h₁ h₂ mem
theorem get!_diff_of_not_mem_left [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} (not_mem : k t₁) :
(t₁ \ t₂).get! k = default :=
DTreeMap.Raw.Const.get!_diff_of_not_mem_left h₁ h₂ not_mem
/- getKey? -/
theorem getKey?_diff [TransCmp cmp]
(h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} :
(t₁ \ t₂).getKey? k =
if k t₂ then none else t₁.getKey? k :=
DTreeMap.Raw.getKey?_diff h₁ h₂
theorem getKey?_diff_of_not_mem_right [TransCmp cmp]
(h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : k t₂) :
(t₁ \ t₂).getKey? k = t₁.getKey? k :=
DTreeMap.Raw.getKey?_diff_of_not_mem_right h₁ h₂ not_mem
theorem getKey?_diff_of_not_mem_left [TransCmp cmp]
(h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : k t₁) :
(t₁ \ t₂).getKey? k = none :=
DTreeMap.Raw.getKey?_diff_of_not_mem_left h₁ h₂ not_mem
theorem getKey?_diff_of_mem_right [TransCmp cmp]
(h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (mem : k t₂) :
(t₁ \ t₂).getKey? k = none :=
DTreeMap.Raw.getKey?_diff_of_mem_right h₁ h₂ mem
/- getKey -/
theorem getKey_diff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} {h_mem : k t₁ \ t₂} :
(t₁ \ t₂).getKey k h_mem =
t₁.getKey k ((mem_diff_iff h₁ h₂).1 h_mem).1 :=
DTreeMap.Raw.getKey_diff h₁ h₂
/- getKeyD -/
theorem getKeyD_diff [TransCmp cmp] (h₁ : t₁.WF)
(h₂ : t₂.WF) {k fallback : α} :
(t₁ \ t₂).getKeyD k fallback =
if k t₂ then fallback else t₁.getKeyD k fallback :=
DTreeMap.Raw.getKeyD_diff h₁ h₂
theorem getKeyD_diff_of_not_mem_right [TransCmp cmp] (h₁ : t₁.WF)
(h₂ : t₂.WF) {k fallback : α} (not_mem : k t₂) :
(t₁ \ t₂).getKeyD k fallback = t₁.getKeyD k fallback :=
DTreeMap.Raw.getKeyD_diff_of_not_mem_right h₁ h₂ not_mem
theorem getKeyD_diff_of_mem_right [TransCmp cmp] (h₁ : t₁.WF)
(h₂ : t₂.WF) {k fallback : α} (mem : k t₂) :
(t₁ \ t₂).getKeyD k fallback = fallback :=
DTreeMap.Raw.getKeyD_diff_of_mem_right h₁ h₂ mem
theorem getKeyD_diff_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF)
(h₂ : t₂.WF) {k fallback : α} (not_mem : k t₁) :
(t₁ \ t₂).getKeyD k fallback = fallback :=
DTreeMap.Raw.getKeyD_diff_of_not_mem_left h₁ h₂ not_mem
/- getKey! -/
theorem getKey!_diff [TransCmp cmp] [Inhabited α] (h₁ : t₁.WF)
(h₂ : t₂.WF) {k : α} :
(t₁ \ t₂).getKey! k =
if k t₂ then default else t₁.getKey! k :=
DTreeMap.Raw.getKey!_diff h₁ h₂
theorem getKey!_diff_of_not_mem_right [TransCmp cmp] [Inhabited α] (h₁ : t₁.WF)
(h₂ : t₂.WF) {k : α} (not_mem : k t₂) :
(t₁ \ t₂).getKey! k = t₁.getKey! k :=
DTreeMap.Raw.getKey!_diff_of_not_mem_right h₁ h₂ not_mem
theorem getKey!_diff_of_mem_right [TransCmp cmp] [Inhabited α] (h₁ : t₁.WF)
(h₂ : t₂.WF) {k : α} (mem : k t₂) :
(t₁ \ t₂).getKey! k = default :=
DTreeMap.Raw.getKey!_diff_of_mem_right h₁ h₂ mem
theorem getKey!_diff_of_not_mem_left [TransCmp cmp] [Inhabited α] (h₁ : t₁.WF)
(h₂ : t₂.WF) {k : α} (not_mem : k t₁) :
(t₁ \ t₂).getKey! k = default :=
DTreeMap.Raw.getKey!_diff_of_not_mem_left h₁ h₂ not_mem
/- size -/
theorem size_diff_le_size_left [TransCmp cmp]
(h₁ : t₁.WF) (h₂ : t₂.WF) :
(t₁ \ t₂).size t₁.size :=
DTreeMap.Raw.size_diff_le_size_left h₁ h₂
theorem size_diff_eq_size_left [TransCmp cmp]
(h₁ : t₁.WF) (h₂ : t₂.WF)
(h : (a : α), a t₁ a t₂) :
(t₁ \ t₂).size = t₁.size :=
DTreeMap.Raw.size_diff_eq_size_left h₁ h₂ h
theorem size_diff_add_size_inter_eq_size_left [TransCmp cmp]
(h₁ : t₁.WF) (h₂ : t₂.WF) :
(t₁ \ t₂).size + (t₁ t₂).size = t₁.size :=
DTreeMap.Raw.size_diff_add_size_inter_eq_size_left h₁ h₂
/- isEmpty -/
@[simp]
theorem isEmpty_diff_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.isEmpty) :
(t₁ \ t₂).isEmpty = true :=
DTreeMap.Raw.isEmpty_diff_left h₁ h₂ h
theorem isEmpty_diff_iff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
(t₁ \ t₂).isEmpty k, k t₁ k t₂ :=
DTreeMap.Raw.isEmpty_diff_iff h₁ h₂
end Diff
section Alter
theorem isEmpty_alter_eq_isEmpty_erase [TransCmp cmp] (h : t.WF) {k : α}

View File

@@ -123,8 +123,4 @@ theorem inter [TransCmp cmp] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) :
(t₁ t₂).WF :=
InnerWF.inter h₁
theorem diff [TransCmp cmp] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) :
(t₁ \ t₂).WF :=
InnerWF.diff h₁
end Std.TreeMap.Raw.WF

View File

@@ -503,16 +503,6 @@ def inter (t₁ t₂ : TreeSet α cmp) : TreeSet α cmp :=
instance : Inter (TreeSet α cmp) := inter
/--
Computes the difference of the given tree sets.
This function always iterates through the smaller set.
-/
def diff (t₁ t₂ : TreeSet α cmp) : TreeSet α cmp :=
TreeMap.diff t₁.inner t₂.inner
instance : SDiff (TreeSet α cmp) := diff
/--
Erases multiple items from the tree set by iterating over the given collection and calling erase.
-/

View File

@@ -772,151 +772,6 @@ theorem isEmpty_inter_iff [TransCmp cmp] :
end Inter
section Diff
variable {t₁ t₂ : TreeSet α cmp}
@[simp]
theorem diff_eq : t₁.diff t₂ = t₁ \ t₂ := by
simp only [SDiff.sdiff]
/- contains -/
@[simp]
theorem contains_diff [TransCmp cmp] {k : α} :
(t₁ \ t₂).contains k = (t₁.contains k && !t₂.contains k) :=
TreeMap.contains_diff
/- mem -/
@[simp]
theorem mem_diff_iff [TransCmp cmp] {k : α} :
k t₁ \ t₂ k t₁ k t₂ :=
TreeMap.mem_diff_iff
theorem not_mem_diff_of_not_mem_left [TransCmp cmp] {k : α}
(not_mem : k t₁) :
k t₁ \ t₂ :=
TreeMap.not_mem_diff_of_not_mem_left not_mem
theorem not_mem_diff_of_mem_right [TransCmp cmp] {k : α}
(mem : k t₂) :
k t₁ \ t₂ :=
TreeMap.not_mem_diff_of_mem_right mem
/- Equiv -/
theorem Equiv.diff_left {t₃ : TreeSet α cmp} [TransCmp cmp]
(equiv : t₁ ~m t₂) :
(t₁ \ t₃).Equiv (t₂ \ t₃) := by
constructor
apply TreeMap.Equiv.diff_left equiv.1
theorem Equiv.diff_right {t₃ : TreeSet α cmp} [TransCmp cmp]
(equiv : t₂ ~m t₃) :
(t₁ \ t₂).Equiv (t₁ \ t₃) := by
constructor
apply TreeMap.Equiv.diff_right equiv.1
theorem Equiv.diff_congr {t₃ t₄ : TreeSet α cmp} [TransCmp cmp]
(equiv₁ : t₁ ~m t₃) (equiv₂ : t₂ ~m t₄) :
(t₁ \ t₂).Equiv (t₃ \ t₄) := by
constructor
apply TreeMap.Equiv.diff_congr equiv₁.1 equiv₂.1
/- get? -/
theorem get?_diff [TransCmp cmp] {k : α} :
(t₁ \ t₂).get? k =
if k t₂ then none else t₁.get? k :=
TreeMap.getKey?_diff
theorem get?_diff_of_not_mem_right [TransCmp cmp]
{k : α} (not_mem : k t₂) :
(t₁ \ t₂).get? k = t₁.get? k :=
TreeMap.getKey?_diff_of_not_mem_right not_mem
theorem get?_diff_of_not_mem_left [TransCmp cmp]
{k : α} (not_mem : k t₁) :
(t₁ \ t₂).get? k = none :=
TreeMap.getKey?_diff_of_not_mem_left not_mem
theorem get?_diff_of_mem_right [TransCmp cmp]
{k : α} (mem : k t₂) :
(t₁ \ t₂).get? k = none :=
TreeMap.getKey?_diff_of_mem_right mem
/- get -/
theorem get_diff [TransCmp cmp]
{k : α} {h_mem : k t₁ \ t₂} :
(t₁ \ t₂).get k h_mem =
t₁.get k (mem_diff_iff.1 h_mem).1 :=
TreeMap.getKey_diff
/- getD -/
theorem getD_diff [TransCmp cmp] {k fallback : α} :
(t₁ \ t₂).getD k fallback =
if k t₂ then fallback else t₁.getD k fallback :=
TreeMap.getKeyD_diff
theorem getD_diff_of_not_mem_right [TransCmp cmp]
{k fallback : α} (not_mem : k t₂) :
(t₁ \ t₂).getD k fallback = t₁.getD k fallback :=
TreeMap.getKeyD_diff_of_not_mem_right not_mem
theorem getD_diff_of_mem_right [TransCmp cmp]
{k fallback : α} (mem : k t₂) :
(t₁ \ t₂).getD k fallback = fallback :=
TreeMap.getKeyD_diff_of_mem_right mem
theorem getD_diff_of_not_mem_left [TransCmp cmp]
{k fallback : α} (not_mem : k t₁) :
(t₁ \ t₂).getD k fallback = fallback :=
TreeMap.getKeyD_diff_of_not_mem_left not_mem
/- get! -/
theorem get!_diff [TransCmp cmp] [Inhabited α] {k : α} :
(t₁ \ t₂).get! k =
if k t₂ then default else t₁.get! k :=
TreeMap.getKey!_diff
theorem get!_diff_of_not_mem_right [TransCmp cmp] [Inhabited α]
{k : α} (not_mem : k t₂) :
(t₁ \ t₂).get! k = t₁.get! k :=
TreeMap.getKey!_diff_of_not_mem_right not_mem
theorem get!_diff_of_mem_right [TransCmp cmp] [Inhabited α]
{k : α} (mem : k t₂) :
(t₁ \ t₂).get! k = default :=
TreeMap.getKey!_diff_of_mem_right mem
theorem get!_diff_of_not_mem_left [TransCmp cmp] [Inhabited α]
{k : α} (not_mem : k t₁) :
(t₁ \ t₂).get! k = default :=
TreeMap.getKey!_diff_of_not_mem_left not_mem
/- size -/
theorem size_diff_le_size_left [TransCmp cmp] :
(t₁ \ t₂).size t₁.size :=
TreeMap.size_diff_le_size_left
theorem size_diff_eq_size_left [TransCmp cmp]
(h : (a : α), a t₁ a t₂) :
(t₁ \ t₂).size = t₁.size :=
TreeMap.size_diff_eq_size_left h
theorem size_diff_add_size_inter_eq_size_left [TransCmp cmp] :
(t₁ \ t₂).size + (t₁ t₂).size = t₁.size :=
TreeMap.size_diff_add_size_inter_eq_size_left
/- isEmpty -/
@[simp]
theorem isEmpty_diff_left [TransCmp cmp] (h : t₁.isEmpty) :
(t₁ \ t₂).isEmpty = true :=
TreeMap.isEmpty_diff_left h
theorem isEmpty_diff_iff [TransCmp cmp] :
(t₁ \ t₂).isEmpty k, k t₁ k t₂ :=
TreeMap.isEmpty_diff_iff
end Diff
section monadic
variable {δ : Type w} {m : Type w Type w'}

View File

@@ -353,16 +353,6 @@ def inter (t₁ t₂ : Raw α cmp) : Raw α cmp :=
instance : Inter (Raw α cmp) := inter
/--
Computes the difference of the given tree sets.
This function always iterates through the smaller set.
-/
def diff (t₁ t₂ : Raw α cmp) : Raw α cmp :=
letI : Ord α := cmp; TreeMap.Raw.diff t₁.inner t₂.inner
instance : SDiff (Raw α cmp) := diff
@[inline, inherit_doc TreeSet.empty]
def eraseMany {ρ} [ForIn Id ρ α] (t : Raw α cmp) (l : ρ) : Raw α cmp :=

View File

@@ -811,166 +811,6 @@ theorem isEmpty_inter_iff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
end Inter
section Diff
variable {t₁ t₂ : Raw α cmp}
@[simp]
theorem diff_eq : t₁.diff t₂ = t₁ \ t₂ := by
simp only [SDiff.sdiff]
/- contains -/
@[simp]
theorem contains_diff [TransCmp cmp] (h₁ : t₁.WF)
(h₂ : t₂.WF) {k : α} :
(t₁ \ t₂).contains k = (t₁.contains k && !t₂.contains k) :=
TreeMap.Raw.contains_diff h₁ h₂
/- mem -/
@[simp]
theorem mem_diff_iff [TransCmp cmp] (h₁ : t₁.WF)
(h₂ : t₂.WF) {k : α} :
k t₁ \ t₂ k t₁ k t₂ :=
TreeMap.Raw.mem_diff_iff h₁ h₂
theorem not_mem_diff_of_not_mem_left [TransCmp cmp]
(h₁ : t₁.WF) (h₂ : t₂.WF) {k : α}
(not_mem : k t₁) :
k t₁ \ t₂ :=
TreeMap.Raw.not_mem_diff_of_not_mem_left h₁ h₂ not_mem
theorem not_mem_diff_of_mem_right [TransCmp cmp]
(h₁ : t₁.WF) (h₂ : t₂.WF) {k : α}
(mem : k t₂) :
k t₁ \ t₂ :=
TreeMap.Raw.not_mem_diff_of_mem_right h₁ h₂ mem
theorem Equiv.diff_left [TransCmp cmp] {t₃ : Raw α cmp}
(h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (equiv : t₁ ~m t₂) :
(t₁ \ t₃).Equiv (t₂ \ t₃) :=
TreeMap.Raw.Equiv.diff_left h₁ h₂ h₃ equiv.1
theorem Equiv.diff_right [TransCmp cmp] {t₃ : Raw α cmp}
(h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (equiv : t₂ ~m t₃) :
(t₁ \ t₂).Equiv (t₁ \ t₃) :=
TreeMap.Raw.Equiv.diff_right h₁ h₂ h₃ equiv.1
theorem Equiv.diff_congr [TransCmp cmp] {t₃ t₄ : Raw α cmp}
(h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (h₄ : t₄.WF)
(equiv₁ : t₁ ~m t₃) (equiv₂ : t₂ ~m t₄) :
(t₁ \ t₂).Equiv (t₃ \ t₄) :=
TreeMap.Raw.Equiv.diff_congr h₁ h₂ h₃ h₄ equiv₁.1 equiv₂.1
/- get? -/
theorem get?_diff [TransCmp cmp]
(h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} :
(t₁ \ t₂).get? k =
if k t₂ then none else t₁.get? k :=
TreeMap.Raw.getKey?_diff h₁ h₂
theorem get?_diff_of_not_mem_right [TransCmp cmp]
(h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} (not_mem : k t₂) :
(t₁ \ t₂).get? k = t₁.get? k :=
TreeMap.Raw.getKey?_diff_of_not_mem_right h₁ h₂ not_mem
theorem get?_diff_of_not_mem_left [TransCmp cmp]
(h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} (not_mem : k t₁) :
(t₁ \ t₂).get? k = none :=
TreeMap.Raw.getKey?_diff_of_not_mem_left h₁ h₂ not_mem
theorem get?_diff_of_mem_right [TransCmp cmp]
(h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} (mem : k t₂) :
(t₁ \ t₂).get? k = none :=
TreeMap.Raw.getKey?_diff_of_mem_right h₁ h₂ mem
/- get -/
theorem get_diff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
{k : α} {h_mem : k t₁ \ t₂} :
(t₁ \ t₂).get k h_mem =
t₁.get k ((mem_diff_iff h₁ h₂).1 h_mem).1 :=
TreeMap.Raw.getKey_diff h₁ h₂
/- getD -/
theorem getD_diff [TransCmp cmp] (h₁ : t₁.WF)
(h₂ : t₂.WF) {k fallback : α} :
(t₁ \ t₂).getD k fallback =
if k t₂ then fallback else t₁.getD k fallback :=
TreeMap.Raw.getKeyD_diff h₁ h₂
theorem getD_diff_of_not_mem_right [TransCmp cmp] (h₁ : t₁.WF)
(h₂ : t₂.WF) {k fallback : α} (not_mem : k t₂) :
(t₁ \ t₂).getD k fallback = t₁.getD k fallback :=
TreeMap.Raw.getKeyD_diff_of_not_mem_right h₁ h₂ not_mem
theorem getD_diff_of_mem_right [TransCmp cmp] (h₁ : t₁.WF)
(h₂ : t₂.WF) {k fallback : α} (mem : k t₂) :
(t₁ \ t₂).getD k fallback = fallback :=
TreeMap.Raw.getKeyD_diff_of_mem_right h₁ h₂ mem
theorem getD_diff_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF)
(h₂ : t₂.WF) {k fallback : α} (not_mem : k t₁) :
(t₁ \ t₂).getD k fallback = fallback :=
TreeMap.Raw.getKeyD_diff_of_not_mem_left h₁ h₂ not_mem
/- get! -/
theorem get!_diff [TransCmp cmp] [Inhabited α]
(h₁ : t₁.WF)
(h₂ : t₂.WF) {k : α} :
(t₁ \ t₂).get! k =
if k t₂ then default else t₁.get! k :=
TreeMap.Raw.getKey!_diff h₁ h₂
theorem get!_diff_of_not_mem_right [Inhabited α]
[TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α}
(not_mem : k t₂) :
(t₁ \ t₂).get! k = t₁.get! k :=
TreeMap.Raw.getKey!_diff_of_not_mem_right h₁ h₂ not_mem
theorem get!_diff_of_mem_right [Inhabited α]
[TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α}
(mem : k t₂) :
(t₁ \ t₂).get! k = default :=
TreeMap.Raw.getKey!_diff_of_mem_right h₁ h₂ mem
theorem get!_diff_of_not_mem_left [Inhabited α]
[TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α}
(not_mem : k t₁) :
(t₁ \ t₂).get! k = default :=
TreeMap.Raw.getKey!_diff_of_not_mem_left h₁ h₂ not_mem
/- size -/
theorem size_diff_le_size_left [TransCmp cmp] (h₁ : t₁.WF)
(h₂ : t₂.WF) :
(t₁ \ t₂).size t₁.size :=
TreeMap.Raw.size_diff_le_size_left h₁ h₂
theorem size_diff_eq_size_left [TransCmp cmp] (h₁ : t₁.WF)
(h₂ : t₂.WF)
(h : (a : α), a t₁ a t₂) :
(t₁ \ t₂).size = t₁.size :=
TreeMap.Raw.size_diff_eq_size_left h₁ h₂ h
theorem size_diff_add_size_inter_eq_size_left [TransCmp cmp]
(h₁ : t₁.WF) (h₂ : t₂.WF) :
(t₁ \ t₂).size + (t₁ t₂).size = t₁.size :=
TreeMap.Raw.size_diff_add_size_inter_eq_size_left h₁ h₂
/- isEmpty -/
@[simp]
theorem isEmpty_diff_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.isEmpty) :
(t₁ \ t₂).isEmpty = true :=
TreeMap.Raw.isEmpty_diff_left h₁ h₂ h
theorem isEmpty_diff_iff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
(t₁ \ t₂).isEmpty k, k t₁ k t₂ :=
TreeMap.Raw.isEmpty_diff_iff h₁ h₂
end Diff
section monadic
variable {δ : Type w} {m : Type w Type w'}

View File

@@ -87,8 +87,4 @@ theorem inter [TransCmp cmp] {t₁ t₂ : Raw α cmp} (h₁ : t₁.WF) :
(t₁ t₂).WF :=
InnerWF.inter h₁
theorem diff [TransCmp cmp] {t₁ t₂ : Raw α cmp} (h₁ : t₁.WF) :
(t₁ \ t₂).WF :=
InnerWF.diff h₁
end Std.TreeSet.Raw.WF

View File

@@ -485,7 +485,6 @@ where
let lval := go lhs.gate decls assign (by omega) h2
let rval := go rhs.gate decls assign (by omega) h2
xor lval lhs.invert && xor rval rhs.invert
termination_by (x, 0) -- Don't allow reduction, we have large concrete gate entries
/--
Denotation of an `AIG` at a specific `Entrypoint`.

View File

@@ -196,7 +196,7 @@ def setConfigOpt (kvPair : String) : CliM PUnit :=
if h : pos.IsAtEnd then
(kvPair.toName, "")
else
(kvPair.extract kvPair.startPos pos |>.toName, kvPair.extract (pos.next h) kvPair.endPos)
(kvPair.startPos.extract pos |>.toName, (pos.next h).extract kvPair.endPos)
modifyThe LakeOptions fun opts =>
{opts with configOpts := opts.configOpts.insert key val}

View File

@@ -56,9 +56,9 @@ public def ofFilePath? (path : FilePath) : Except String ArtifactDescr := do
| throw "expected artifact file name to be a content hash"
return {hash, ext := ""}
else
let some hash := Hash.ofString? <| s.extract s.startPos pos
let some hash := Hash.ofString? <| s.startPos.extract pos
| throw "expected artifact file name to be a content hash"
let ext := s.extract (pos.next h) s.endPos
let ext := (pos.next h).extract s.endPos
return {hash, ext}
public protected def fromJson? (data : Json) : Except String ArtifactDescr := do

View File

@@ -102,8 +102,8 @@ variable [Monad m] [MonadStateOf ArgList m]
if h : pos = opt.endPos then
handle opt
else do
consArg <| opt.extract (pos.next h) opt.endPos
handle <| opt.extract opt.startPos pos
consArg <| (pos.next h).extract opt.endPos
handle <| opt.startPos.extract pos
/-- Splits a long option of the form `--long=arg` into `--long` and `arg`. -/
@[inline] public def longOptionOrEq (handle : String m α) (opt : String) : m α :=
@@ -111,8 +111,8 @@ variable [Monad m] [MonadStateOf ArgList m]
if h : pos = opt.endPos then
handle opt
else do
consArg <| opt.extract (pos.next h) opt.endPos
handle <| opt.extract opt.startPos pos
consArg <| (pos.next h).extract opt.endPos
handle <| opt.startPos.extract pos
/-- Process a long option of the form `--long`, `--long=arg`, `"--long arg"`. -/
@[inline] public def longOption (handle : String m α) : String m α :=

View File

@@ -88,7 +88,7 @@ def parseSpecialDescr? (s : String) : EStateM String s.Pos (Option String) := do
let p := p.next h
let p' := nextUntilWhitespace p
set p'
let specialDescr := s.extract p p'
let specialDescr := p.extract p'
return some specialDescr
else
return none
@@ -256,7 +256,7 @@ public def ofString (ver : String) : ToolchainVer := Id.run do
let (origin, tag) :=
if h : ¬colonPos.IsAtEnd then
let pos := colonPos.next h
(ver.extract ver.startPos colonPos, ver.extract pos ver.endPos)
(ver.startPos.extract colonPos, pos.extract ver.endPos)
else
("", ver)
let noOrigin := origin.isEmpty

View File

@@ -1,5 +1,6 @@
#include "util/options.h"
// stage0 update needed for grind_annotated command
namespace lean {
options get_default_options() {
options opts;

Binary file not shown.

View File

@@ -1,5 +1,6 @@
#include "util/options.h"
// stage0 update needed for grind_annotated command
namespace lean {
options get_default_options() {
options opts;

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

BIN
stage0/stdlib/Init/WF.c generated

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

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