Compare commits

..

37 Commits

Author SHA1 Message Date
Leonardo de Moura
b23f4355c0 fix: replace_fn.cpp 2024-07-19 21:11:08 -07:00
Lean stage0 autoupdater
c2117d75a6 chore: update stage0 2024-07-20 03:58:16 +00:00
Leonardo de Moura
3477b0e7f6 fix: for_each_fn.cpp (#4797) 2024-07-20 03:22:56 +00:00
Lean stage0 autoupdater
696f70bb4e chore: update stage0 2024-07-20 02:35:13 +00:00
Leonardo de Moura
726e162527 perf: kernel replace with precise cache (#4796)
Changes:

- We avoid the thread local storage.
- We use a hash map to ensure that cached values are not lost.
- We remove `check_system`. If this becomes an issue in the future we
should precompute the remaining amount of stack space, and use a cheaper
check.
- We add a `Expr.replaceImpl`, and will use it to implement
`Expr.replace` after update-stage0
2024-07-20 02:00:29 +00:00
Leonardo de Moura
de5e07c4d2 perf: find? and findExt? (#4795)
use the kernel implementation.
2024-07-20 01:13:54 +00:00
Lean stage0 autoupdater
327986e6fb chore: update stage0 2024-07-20 00:51:23 +00:00
Leonardo de Moura
6c33b9c57f perf: for_each with precise cache (#4794)
This commit also adds support for `find?` and `findExt?` using kernel
`for_each`.
We need to perform `update-stage0`.
2024-07-20 00:18:55 +00:00
Henrik Böving
d907771fdd feat: theory from LeanSAT (#4742)
Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
2024-07-19 16:21:03 +00:00
Leonardo de Moura
5c3360200e fix: add term elaborator for Lean.Parser.Term.namedPattern (#4792)
closes #4662
2024-07-19 16:14:32 +00:00
Joachim Breitner
204d4839fa refactor: add numFixed to Structural.EqnInfo (#4788) 2024-07-19 10:21:43 +00:00
Joachim Breitner
e32f3e8140 refactor: IndGroupInst.brecOn (#4787)
this logic fits nicely within `IndGroupInst`.

Also makes `isAuxRecursorWithSuffix` recognize `brecOn_<n>`.
2024-07-19 10:20:50 +00:00
Sebastian Ullrich
7d2155943c doc: fix integer division example
Fixes #4785
2024-07-19 10:36:43 +02:00
Lean stage0 autoupdater
78c4d6daff chore: update stage0 2024-07-18 20:38:21 +00:00
Leonardo de Moura
5526ff6320 chore: Simp.Config.implicitDefEqProofs := true by default (#4784)
Motivation: unblock PR #4595
`Simp.Config.implicitDefEqProofs := false` is currently creating too
many issues in Mathlib.
2024-07-18 19:10:18 +00:00
Leonardo de Moura
bfca7ec72a fix: .eq_def theorem generation with messy universes (#4712)
closes #4673
2024-07-18 17:34:23 +00:00
Leonardo de Moura
9208b3585f chore: document replaceUnsafeM issue (#4783) 2024-07-18 16:26:20 +00:00
Leonardo de Moura
a94805ff71 perf: ensure Expr.replaceExpr preserve DAG structure in Exprs (#4779) 2024-07-18 02:24:15 +00:00
Lean stage0 autoupdater
4eb842560c chore: update stage0 2024-07-18 01:19:02 +00:00
Kyle Miller
490d16c80d fix: have elabAsElim check inferred motive for type correctness (#4722)
Declarations with `@[elab_as_elim]` could elaborate as type-incorrect
expressions. Reported by Jireh Loreaux [on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/bug.20in.20revert/near/450522157).

(In principle the elabAsElim routine could revert fvars appearing in the
expected type that depend on the discriminants (if the discriminants are
fvars) to increase the likelihood of type correctness, but that's at the
cost of some complexity to both the elaborator and to the user.)
2024-07-17 20:48:03 +00:00
Leonardo de Moura
f60721bfbd feat: add some low level helper APIs (#4778) 2024-07-17 20:12:05 +00:00
Kyle Miller
a5ecdd0a17 feat: improve @[ext] error message when ext_iff generation fails (#4762)
Now it suggests using `@[ext (iff := false)]` to disable generating the
`ext_iff` lemma.

This PR also adjusts error messages and attribute documentation.
Additionally, to simplify the code now the `x` and `y` arguments can't
come in reverse order (this feature was was added in the refactor
#4543).

Closes #4758
2024-07-17 18:26:12 +00:00
Leonardo de Moura
be717f03ef fix: missing assignment validation at closeMainGoal (#4777)
This primitive is used by the `exact` tactic. This issue allowed users
to create loops in the metavariable assignment.

closes #4773
2024-07-17 18:25:02 +00:00
Leonardo de Moura
41b4914836 perf: Replacement.apply (#4776)
Avoid potentially expensive `e.replace` if it is not applicable.
2024-07-17 16:17:47 +00:00
Leonardo de Moura
933445608c chore: simplify shareCommon' (#4775) 2024-07-17 15:32:35 +00:00
Markus Himmel
8e396068e4 doc: mention linearity in hash map docstring (#4771) 2024-07-17 09:26:38 +00:00
Markus Himmel
c1df7564ce fix: resolve instances for HashMap via unification (#4759) 2024-07-17 08:02:22 +00:00
Markus Himmel
ba3565f441 chore: fix BEq argument order in hash map lemmas (#4732)
The previous argument order was a conscious choice, but I had missed
#3056.
2024-07-17 04:25:21 +00:00
Kim Morrison
af03af5037 feat: simprocs for #[1,2,3,4,5][2] (#4765)
None of these were working previously:

```
#check_simp #[1,2,3,4,5][2]  ~> 3
#check_simp #[1,2,3,4,5][2]? ~> some 3
#check_simp #[1,2,3,4,5][7]? ~> none
#check_simp #[][0]? ~> none
#check_simp #[1,2,3,4,5][2]! ~> 3
#check_simp #[1,2,3,4,5][7]! ~> (default : Nat)
#check_simp (#[] : Array Nat)[0]! ~> (default : Nat)
```
2024-07-17 03:05:17 +00:00
Leonardo de Moura
f6666fe266 chore: add missing withTraceNode (#4769)
Motivation: improve `trace.profiler`
2024-07-17 02:32:32 +00:00
Leonardo de Moura
c580684c22 perf: add ShareCommon.shareCommon' (#4767)
A more restrictive but efficient max sharing primitive.

**Motivation:** Some software verification proofs may contain
significant redundancy that can be eliminated using hash-consing (also
known as `shareCommon`). For example, [theorem
`sha512_block_armv8_test_4_sym`](460fe5d74c/Proofs/SHA512/SHA512Sym.lean (L29))
took a few seconds at [`addPreDefinitions`
](1a12f63f74/src/Lean/Elab/PreDefinition/Main.lean (L155))
and one second at `fixLevelParams` on a MacBook Pro (with M1 Pro). The
proof term initially had over 16 million subterms, but the redundancy
was indirectly and inefficiently eliminated using `Core.transform` at
`addPreDefinitions`. I tried to use `shareCommon` method to fix the
performance issue, but it was too inefficient. This PR introduces a new
`shareCommon'` method that, although less flexible (e.g., it uses only a
local cache and hash-consing table), is much more efficient. The new
procedure minimizes the number of RC operations and optimizes the
caching strategy. It is 20 times faster than the old `shareCommon`
procedure for theorem `sha512_block_armv8_test_4_sym`.
2024-07-17 01:33:54 +00:00
Joachim Breitner
1a12f63f74 refactor: move Synax.hasIdent, shake dependencies (#4766)
I noticed that a change to `Lean.PrettyPrinter.Delaborator.Builtins`
rebuilt more modules than I expected, so I moved a definition and
reduced some dependcies.

More reduction would be possible to move const-delaboration out of the
big `Lean.PrettyPrinter`, and import from `Lean.PrettyPrinter`
selectively.
2024-07-16 21:19:26 +00:00
Joachim Breitner
95b8095fa6 feat: PProd syntax (part 3) (#4756)
reworks #4730 based on feedback from @kmill:

 * Uses `×'` for PProd
 * No syntax for MProd for now
 * Angle brackets (without nesting) for the values
2024-07-16 21:06:04 +00:00
Kyle Miller
94cc8eb863 chore: add comment for why anonymous constructor notation isn't flattened during pretty printing (#4764) 2024-07-16 19:04:51 +00:00
Kim Morrison
1cf47bce5a chore: rename TC to Relation.TransGen (#4760)
This is barely used in Lean, and this rename is both more readable, and
consistent with further developments downstream.

See
[zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Relation.2ETransGen.20vs.2E.20TC.20from.20Init.2ECore/near/448941824)
discussion.
2024-07-16 17:06:49 +00:00
Leonardo de Moura
b73fe04710 feat: add Lean.Expr.numObjs (#4754)
Add helper function for computing the number of allocated
sub-expressions in a given expression. Note: Use this function primarily
for diagnosing performance issues.
2024-07-16 15:52:33 +00:00
Leonardo de Moura
f986a2e9ef chore: missing profileitM (#4753)
This PR addresses the absence of the `profileitM` function in two
auxiliary functions. The added `profileitM` instances are particularly
useful for diagnosing performance issues in declarations that contain
many repeated sub-terms.
2024-07-16 15:43:23 +00:00
207 changed files with 1699 additions and 1018 deletions

View File

@@ -13,7 +13,7 @@ Recall that nonnegative numerals are considered to be a `Nat` if there are no ty
The operator `/` for `Int` implements integer division.
```lean
#eval -10 / 4 -- -2
#eval -10 / 4 -- -3
```
Similar to `Nat`, the internal representation of `Int` is optimized. Small integers are

View File

@@ -1089,15 +1089,18 @@ def InvImage {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β
fun a₁ a₂ => r (f a₁) (f a₂)
/--
The transitive closure `r` of a relation `r` is the smallest relation which is
transitive and contains `r`. `r a z` if and only if there exists a sequence
The transitive closure `TransGen r` of a relation `r` is the smallest relation which is
transitive and contains `r`. `TransGen r a z` if and only if there exists a sequence
`a r b r ... r z` of length at least 1 connecting `a` to `z`.
-/
inductive TC {α : Sort u} (r : α α Prop) : α α Prop where
/-- If `r a b` then `r a b`. This is the base case of the transitive closure. -/
| base : a b, r a b TC r a b
inductive Relation.TransGen {α : Sort u} (r : α α Prop) : α α Prop
/-- If `r a b` then `TransGen r a b`. This is the base case of the transitive closure. -/
| single {a b} : r a b TransGen r a b
/-- The transitive closure is transitive. -/
| trans : a b c, TC r a b TC r b c TC r a c
| tail {a b c} : TransGen r a b r b c TransGen r a c
/-- Deprecated synonym for `Relation.TransGen`. -/
@[deprecated Relation.TransGen (since := "2024-07-16")] abbrev TC := @Relation.TransGen
/-! # Subtype -/

View File

@@ -128,14 +128,6 @@ theorem length_pos {l : List α} : 0 < length l ↔ l ≠ [] :=
theorem length_eq_one {l : List α} : length l = 1 a, l = [a] :=
fun h => match l, h with | [_], _ => _, rfl, fun _, h => by simp [h]
/-! ### `isEmpty` -/
theorem isEmpty_iff {l : List α} : l.isEmpty l = [] := by
cases l <;> simp
theorem isEmpty_iff_length_eq_zero {l : List α} : l.isEmpty l.length = 0 := by
rw [isEmpty_iff, length_eq_zero]
/-! ## L[i] and L[i]? -/
/-! ### `get` and `get?`.
@@ -475,6 +467,18 @@ theorem forall_getElem (l : List α) (p : α → Prop) :
decide (y a :: l) = (y == a || decide (y l)) := by
cases h : y == a <;> simp_all
/-! ### `isEmpty` -/
theorem isEmpty_iff {l : List α} : l.isEmpty l = [] := by
cases l <;> simp
theorem isEmpty_false_iff_exists_mem (xs : List α) :
(List.isEmpty xs = false) x, x xs := by
cases xs <;> simp
theorem isEmpty_iff_length_eq_zero {l : List α} : l.isEmpty l.length = 0 := by
rw [isEmpty_iff, length_eq_zero]
/-! ### any / all -/
theorem any_eq {l : List α} : l.any p = decide ( x, x l p x) := by induction l <;> simp [*]
@@ -1141,6 +1145,18 @@ theorem head_filterMap_of_eq_some {f : α → Option β} {l : List α} (w : l
simp only [head_cons] at h
simp [filterMap_cons, h]
theorem forall_none_of_filterMap_eq_nil (h : List.filterMap f xs = []) : x xs, f x = none := by
intro x hx
induction xs with
| nil => contradiction
| cons y ys ih =>
simp only [filterMap_cons] at h
split at h
. cases hx with
| head => assumption
| tail _ hmem => exact ih h hmem
. contradiction
/-! ### append -/
theorem getElem?_append_right : {l₁ l₂ : List α} {n : Nat}, l₁.length n
@@ -3395,6 +3411,16 @@ theorem any_map (f : α → β) (l : List α) (p : β → Bool) : (l.map f).any
theorem all_map (f : α β) (l : List α) (p : β Bool) : (l.map f).all p = l.all (p f) := by
induction l with simp | cons _ _ ih => rw [ih]
@[simp] theorem any_append {x y : List α} : (x ++ y).any f = (x.any f || y.any f) := by
induction x with
| nil => rfl
| cons h t ih => simp_all [Bool.or_assoc]
@[simp] theorem all_append {x y : List α} : (x ++ y).all f = (x.all f && y.all f) := by
induction x with
| nil => rfl
| cons h t ih => simp_all [Bool.and_assoc]
/-! ## Zippers -/
/-! ### zip -/

View File

@@ -24,15 +24,16 @@ syntax extFlat := atomic("(" &"flat" " := " &"false" ")")
/--
Registers an extensionality theorem.
* When `@[ext]` is applied to a structure, it generates `.ext` and `.ext_iff` theorems and registers
them for the `ext` tactic.
* When `@[ext]` is applied to a theorem, the theorem is registered for the `ext` tactic, and it generates an `ext_iff` theorem.
* When `@[ext]` is applied to a theorem, the theorem is registered for the `ext` tactic, and it generates an "`ext_iff`" theorem.
The name of the theorem is from adding the suffix `_iff` to the theorem name.
* An optional natural number argument, e.g. `@[ext 9000]`, specifies a priority for the lemma. Higher-priority lemmas are chosen first, and the default is `1000`.
* When `@[ext]` is applied to a structure, it generates an `.ext` theorem and applies the `@[ext]` attribute to it.
The result is an `.ext` and an `.ext_iff` theorem with the `.ext` theorem registered for the `ext` tactic.
* The flag `@[ext (iff := false)]` prevents it from generating an `ext_iff` theorem.
* An optional natural number argument, e.g. `@[ext 9000]`, specifies a priority for the `ext` lemma.
Higher-priority lemmas are chosen first, and the default is `1000`.
* The flag `@[ext (iff := false)]` disables generating an `ext_iff` theorem.
* The flag `@[ext (flat := false)]` causes generated structure extensionality theorems to show inherited fields based on their representation,
rather than flattening the parents' fields into the lemma's equality hypotheses.

View File

@@ -219,13 +219,13 @@ structure Config where
-/
index : Bool := true
/--
When `true` (default: `false`), `simp` will **not** create a proof for a rewriting rule associated
When `true` (default: `true`), `simp` will **not** create a proof for a rewriting rule associated
with an `rfl`-theorem.
Rewriting rules are provided by users by annotating theorems with the attribute `@[simp]`.
If the proof of the theorem is just `rfl` (reflexivity), and `implicitDefEqProofs := true`, `simp`
will **not** create a proof term which is an application of the annotated theorem.
-/
implicitDefEqProofs : Bool := false
implicitDefEqProofs : Bool := true
deriving Inhabited, BEq
-- Configuration object for `simp_all`

View File

@@ -267,8 +267,7 @@ syntax (name := rawNatLit) "nat_lit " num : term
@[inherit_doc] infixr:90 "" => Function.comp
@[inherit_doc] infixr:35 " × " => Prod
@[inherit_doc] infixr:35 " × " => PProd
@[inherit_doc] infixr:35 " ×ₘ " => MProd
@[inherit_doc] infixr:35 " ×' " => PProd
@[inherit_doc] infix:50 " " => Dvd.dvd
@[inherit_doc] infixl:55 " ||| " => HOr.hOr

View File

@@ -163,16 +163,6 @@ end Lean
| `($(_) $x $y) => `(($x, $y))
| _ => throw ()
@[app_unexpander PProd.mk] def unexpandPProdMk : Lean.PrettyPrinter.Unexpander
| `($(_) $x ($y, $ys,*)) => `(($x, $y, $ys,*))
| `($(_) $x $y) => `(($x, $y))
| _ => throw ()
@[app_unexpander MProd.mk] def unexpandMProdMk : Lean.PrettyPrinter.Unexpander
| `($(_) $x ($y, $ys,*)) => `(($x, $y, $ys,*))
| `($(_) $x $y) => `(($x, $y))
| _ => throw ()
@[app_unexpander ite] def unexpandIte : Lean.PrettyPrinter.Unexpander
| `($(_) $c $t $e) => `(if $c then $t else $e)
| _ => throw ()

View File

@@ -488,9 +488,9 @@ attribute [unbox] Prod
/--
Similar to `Prod`, but `α` and `β` can be propositions.
You can use `α ×' β` as notation for `PProd α β`.
We use this type internally to automatically generate the `brecOn` recursor.
-/
@[pp_using_anonymous_constructor]
structure PProd (α : Sort u) (β : Sort v) where
/-- The first projection out of a pair. if `p : PProd α β` then `p.1 : α`. -/
fst : α

View File

@@ -309,6 +309,11 @@ theorem not_forall_of_exists_not {p : α → Prop} : (∃ x, ¬p x) → ¬∀ x,
@[simp] theorem exists_eq_right_right' : ( (a : α), p a q a a' = a) p a' q a' := by
simp [@eq_comm _ a']
@[simp] theorem exists_or_eq_left (y : α) (p : α Prop) : x : α, x = y p x := y, .inl rfl
@[simp] theorem exists_or_eq_right (y : α) (p : α Prop) : x : α, p x x = y := y, .inr rfl
@[simp] theorem exists_or_eq_left' (y : α) (p : α Prop) : x : α, y = x p x := y, .inl rfl
@[simp] theorem exists_or_eq_right' (y : α) (p : α Prop) : x : α, p x y = x := y, .inr rfl
@[simp] theorem exists_prop : ( _h : a, b) a b :=
fun hp, hq => hp, hq, fun hp, hq => hp, hq

View File

@@ -102,3 +102,11 @@ instance ShareCommonT.monadShareCommon [Monad m] : MonadShareCommon (ShareCommon
@[inline] def ShareCommonT.run [Monad m] (x : ShareCommonT σ m α) : m α := x.run' default
@[inline] def ShareCommonM.run (x : ShareCommonM σ α) : α := ShareCommonT.run x
/--
A more restrictive but efficient max sharing primitive.
Remark: it optimizes the number of RC operations, and the strategy for caching results.
-/
@[extern "lean_sharecommon_quick"]
def ShareCommon.shareCommon' (a : α) : α := a

View File

@@ -45,6 +45,13 @@ def dbgSleep {α : Type u} (ms : UInt32) (f : Unit → α) : α := f ()
@[extern "lean_ptr_addr"]
unsafe opaque ptrAddrUnsafe {α : Type u} (a : @& α) : USize
/--
Returns `true` if `a` is an exclusive object.
We say an object is exclusive if it is single-threaded and its reference counter is 1.
-/
@[extern "lean_is_exclusive_obj"]
unsafe opaque isExclusiveUnsafe {α : Type u} (a : @& α) : Bool
set_option linter.unusedVariables.funArgs false in
@[inline] unsafe def withPtrAddrUnsafe {α : Type u} {β : Type v} (a : α) (k : USize β) (h : u₁ u₂, k u₁ = k u₂) : β :=
k (ptrAddrUnsafe a)

View File

@@ -148,22 +148,26 @@ end InvImage
wf := InvImage.wf f h.wf
-- The transitive closure of a well-founded relation is well-founded
namespace TC
variable {α : Sort u} {r : α α Prop}
open Relation
theorem accessible {z : α} (ac : Acc r z) : Acc (TC r) z := by
induction ac with
| intro x acx ih =>
apply Acc.intro x
intro y rel
induction rel with
| base a b rab => exact ih a rab
| trans a b c rab _ _ ih₂ => apply Acc.inv (ih₂ acx ih) rab
theorem Acc.transGen (h : Acc r a) : Acc (TransGen r) a := by
induction h with
| intro x _ H =>
refine Acc.intro x fun y hy ?_
cases hy with
| single hyx =>
exact H y hyx
| tail hyz hzx =>
exact (H _ hzx).inv hyz
theorem wf (h : WellFounded r) : WellFounded (TC r) :=
fun a => accessible (apply h a)
end TC
theorem acc_transGen_iff : Acc (TransGen r) a Acc r a :=
Subrelation.accessible TransGen.single, Acc.transGen
theorem WellFounded.transGen (h : WellFounded r) : WellFounded (TransGen r) :=
fun a (h.apply a).transGen
@[deprecated Acc.transGen (since := "2024-07-16")] abbrev TC.accessible := @Acc.transGen
@[deprecated WellFounded.transGen (since := "2024-07-16")] abbrev TC.wf := @WellFounded.transGen
namespace Nat
-- less-than is well-founded

View File

@@ -37,7 +37,7 @@ def isAuxRecursor (env : Environment) (declName : Name) : Bool :=
def isAuxRecursorWithSuffix (env : Environment) (declName : Name) (suffix : String) : Bool :=
match declName with
| .str _ s => s == suffix && isAuxRecursor env declName
| .str _ s => (s == suffix || s.startsWith s!"{suffix}_") && isAuxRecursor env declName
| _ => false
def isCasesOnRecursor (env : Environment) (declName : Name) : Bool :=

View File

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
-/
prelude
import Lean.Compiler.Options
import Lean.Compiler.ExternAttr
import Lean.Compiler.LCNF.PassManager
import Lean.Compiler.LCNF.Passes
import Lean.Compiler.LCNF.PrettyPrinter

View File

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.PrettyPrinter
import Lean.PrettyPrinter.Delaborator.Options
import Lean.Compiler.LCNF.CompilerM
import Lean.Compiler.LCNF.Internalize

View File

@@ -80,6 +80,10 @@ protected def max : RBNode α β → Option (Sigma (fun k => β k))
def singleton (k : α) (v : β k) : RBNode α β :=
node red leaf k v leaf
def isSingleton : RBNode α β Bool
| node _ leaf _ _ leaf => true
| _ => false
-- the first half of Okasaki's `balance`, concerning red-red sequences in the left child
@[inline] def balance1 : RBNode α β (a : α) β a RBNode α β RBNode α β
| node red (node red a kx vx b) ky vy c, kz, vz, d
@@ -269,6 +273,9 @@ variable {α : Type u} {β : Type v} {σ : Type w} {cmp : αα → Ordering
def depth (f : Nat Nat Nat) (t : RBMap α β cmp) : Nat :=
t.val.depth f
def isSingleton (t : RBMap α β cmp) : Bool :=
t.val.isSingleton
@[inline] def fold (f : σ α β σ) : (init : σ) RBMap α β cmp σ
| b, t, _ => t.fold f b

View File

@@ -742,7 +742,10 @@ def mkMotive (discrs : Array Expr) (expectedType : Expr): MetaM Expr := do
let motiveBody kabstract motive discr
/- We use `transform (usedLetOnly := true)` to eliminate unnecessary let-expressions. -/
let discrType transform (usedLetOnly := true) ( instantiateMVars ( inferType discr))
return Lean.mkLambda ( mkFreshBinderName) BinderInfo.default discrType motiveBody
let motive := Lean.mkLambda ( mkFreshBinderName) BinderInfo.default discrType motiveBody
unless ( isTypeCorrect motive) do
throwError "failed to elaborate eliminator, motive is not type correct:{indentD motive}"
return motive
/-- If the eliminator is over-applied, we "revert" the extra arguments. -/
def revertArgs (args : List Arg) (f : Expr) (expectedType : Expr) : TermElabM (Expr × Expr) :=

View File

@@ -11,7 +11,6 @@ import Lean.Elab.Eval
import Lean.Elab.Command
import Lean.Elab.Open
import Lean.Elab.SetOption
import Lean.PrettyPrinter
namespace Lean.Elab.Command

View File

@@ -330,15 +330,6 @@ where
return ( expandCDot? pairs).getD pairs
| _ => Macro.throwUnsupported
@[builtin_macro Lean.Parser.Term.ptuple] def expandPTuple : Macro
| `(()) => ``(PUnit.unit)
| `(($e, $es,*)) => mkPPairs (#[e] ++ es)
| _ => Macro.throwUnsupported
@[builtin_macro Lean.Parser.Term.mtuple] def expandMTuple : Macro
| `(($e, $es,*)) => mkMPairs (#[e] ++ es)
| _ => Macro.throwUnsupported
@[builtin_macro Lean.Parser.Term.typeAscription] def expandTypeAscription : Macro
| `(($e : $(type)?)) => do
match ( expandCDot? e) with

View File

@@ -362,4 +362,7 @@ private opaque evalFilePath (stx : Syntax) : TermElabM System.FilePath
mkStrLit <$> IO.FS.readFile path
| _, _ => throwUnsupportedSyntax
@[builtin_term_elab Lean.Parser.Term.namedPattern] def elabNamedPatternErr : TermElab := fun stx _ =>
throwError "`<identifier>@<term>` is a named pattern and can only be used in pattern matching contexts{indentD stx}"
end Lean.Elab.Term

View File

@@ -728,12 +728,26 @@ def insertReplacementForLetRecs (r : Replacement) (letRecClosures : List LetRecC
letRecClosures.foldl (init := r) fun r c =>
r.insert c.toLift.fvarId c.closed
def isApplicable (r : Replacement) (e : Expr) : Bool :=
Option.isSome <| e.findExt? fun e =>
if e.hasFVar then
match e with
| .fvar fvarId => if r.contains fvarId then .found else .done
| _ => .visit
else
.done
def Replacement.apply (r : Replacement) (e : Expr) : Expr :=
e.replace fun e => match e with
| .fvar fvarId => match r.find? fvarId with
| some c => some c
| _ => none
| _ => none
-- Remark: if `r` is not a singlenton, then declaration is using `mutual` or `let rec`,
-- and there is a big chance `isApplicable r e` is true.
if r.isSingleton && !isApplicable r e then
e
else
e.replace fun e => match e with
| .fvar fvarId => match r.find? fvarId with
| some c => some c
| _ => none
| _ => none
def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mainVals : Array Expr)
: TermElabM (Array PreDefinition) :=
@@ -923,6 +937,7 @@ where
trace[Elab.definition] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
let preDefs withLevelNames allUserLevelNames <| levelMVarToParamPreDecls preDefs
let preDefs instantiateMVarsAtPreDecls preDefs
let preDefs shareCommonPreDefs preDefs
let preDefs fixLevelParams preDefs scopeLevelNames allUserLevelNames
for preDef in preDefs do
trace[Elab.definition] "after eraseAuxDiscr, {preDef.declName} : {preDef.type} :=\n{preDef.value}"

View File

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.ShareCommon
import Lean.Compiler.NoncomputableAttr
import Lean.Util.CollectLevelParams
import Lean.Meta.AbstractNestedProofs
@@ -52,20 +53,21 @@ private def getLevelParamsPreDecls (preDefs : Array PreDefinition) (scopeLevelNa
| Except.error msg => throwError msg
| Except.ok levelParams => pure levelParams
def fixLevelParams (preDefs : Array PreDefinition) (scopeLevelNames allUserLevelNames : List Name) : TermElabM (Array PreDefinition) :=
do profileitM Exception s!"fix level params" ( getOptions) do
-- We used to use `shareCommon` here, but is was a bottleneck
let levelParams getLevelParamsPreDecls preDefs scopeLevelNames allUserLevelNames
let us := levelParams.map mkLevelParam
let fixExpr (e : Expr) : Expr :=
e.replace fun c => match c with
| Expr.const declName _ => if preDefs.any fun preDef => preDef.declName == declName then some $ Lean.mkConst declName us else none
| _ => none
return preDefs.map fun preDef =>
{ preDef with
type := fixExpr preDef.type,
value := fixExpr preDef.value,
levelParams := levelParams }
def fixLevelParams (preDefs : Array PreDefinition) (scopeLevelNames allUserLevelNames : List Name) : TermElabM (Array PreDefinition) := do
profileitM Exception s!"fix level params" ( getOptions) do
withTraceNode `Elab.def.fixLevelParams (fun _ => return m!"fix level params") do
-- We used to use `shareCommon` here, but is was a bottleneck
let levelParams getLevelParamsPreDecls preDefs scopeLevelNames allUserLevelNames
let us := levelParams.map mkLevelParam
let fixExpr (e : Expr) : Expr :=
e.replace fun c => match c with
| Expr.const declName _ => if preDefs.any fun preDef => preDef.declName == declName then some $ Lean.mkConst declName us else none
| _ => none
return preDefs.map fun preDef =>
{ preDef with
type := fixExpr preDef.type,
value := fixExpr preDef.value,
levelParams := levelParams }
def applyAttributesOf (preDefs : Array PreDefinition) (applicationTime : AttributeApplicationTime) : TermElabM Unit := do
for preDef in preDefs do
@@ -211,4 +213,17 @@ def checkCodomainsLevel (preDefs : Array PreDefinition) : MetaM Unit := do
m!"for `{preDefs[0]!.declName}` is{indentExpr type₀} : {← inferType type₀}\n" ++
m!"and for `{preDefs[i]!.declName}` is{indentExpr typeᵢ} : {← inferType typeᵢ}"
def shareCommonPreDefs (preDefs : Array PreDefinition) : CoreM (Array PreDefinition) := do
profileitM Exception "share common exprs" ( getOptions) do
withTraceNode `Elab.def.maxSharing (fun _ => return m!"share common exprs") do
let mut es := #[]
for preDef in preDefs do
es := es.push preDef.type |>.push preDef.value
es := ShareCommon.shareCommon' es
let mut result := #[]
for h : i in [:preDefs.size] do
let preDef := preDefs[i]
result := result.push { preDef with type := es[2*i]!, value := es[2*i+1]! }
return result
end Lean.Elab

View File

@@ -333,7 +333,7 @@ def tryContradiction (mvarId : MVarId) : MetaM Bool := do
partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
let some eqs getEqnsFor? declName | throwError "failed to generate equations for '{declName}'"
let tryEqns (mvarId : MVarId) : MetaM Bool :=
eqs.anyM fun eq => commitWhen do
eqs.anyM fun eq => commitWhen do checkpointDefEq (mayPostpone := false) do
try
let subgoals mvarId.apply ( mkConstWithFreshMVarLevels eq)
subgoals.allM fun subgoal => do

View File

@@ -152,69 +152,71 @@ def shouldUseWF (preDefs : Array PreDefinition) : Bool :=
preDef.termination.decreasingBy?.isSome
def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLCtx {} {} do profileitM Exception "add pre-definitions" ( getOptions) do
for preDef in preDefs do
trace[Elab.definition.body] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
let preDefs preDefs.mapM ensureNoUnassignedMVarsAtPreDef
let preDefs betaReduceLetRecApps preDefs
let cliques := partitionPreDefs preDefs
for preDefs in cliques do
trace[Elab.definition.scc] "{preDefs.map (·.declName)}"
if preDefs.size == 1 && isNonRecursive preDefs[0]! then
/-
We must erase `recApp` annotations even when `preDef` is not recursive
because it may use another recursive declaration in the same mutual block.
See issue #2321
-/
let preDef eraseRecAppSyntax preDefs[0]!
ensureEqnReservedNamesAvailable preDef.declName
if preDef.modifiers.isNoncomputable then
addNonRec preDef
else
addAndCompileNonRec preDef
preDef.termination.ensureNone "not recursive"
else if preDefs.any (·.modifiers.isUnsafe) then
addAndCompileUnsafe preDefs
preDefs.forM (·.termination.ensureNone "unsafe")
else if preDefs.any (·.modifiers.isPartial) then
def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLCtx {} {} do
profileitM Exception "process pre-definitions" ( getOptions) do
withTraceNode `Elab.def.processPreDef (fun _ => return m!"process pre-definitions") do
for preDef in preDefs do
if preDef.modifiers.isPartial && !( whnfD preDef.type).isForall then
withRef preDef.ref <| throwError "invalid use of 'partial', '{preDef.declName}' is not a function{indentExpr preDef.type}"
addAndCompilePartial preDefs
preDefs.forM (·.termination.ensureNone "partial")
else
ensureFunIndReservedNamesAvailable preDefs
try
checkCodomainsLevel preDefs
checkTerminationByHints preDefs
let termArg?s elabTerminationByHints preDefs
if shouldUseStructural preDefs then
structuralRecursion preDefs termArg?s
else if shouldUseWF preDefs then
wfRecursion preDefs termArg?s
trace[Elab.definition.body] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
let preDefs preDefs.mapM ensureNoUnassignedMVarsAtPreDef
let preDefs betaReduceLetRecApps preDefs
let cliques := partitionPreDefs preDefs
for preDefs in cliques do
trace[Elab.definition.scc] "{preDefs.map (·.declName)}"
if preDefs.size == 1 && isNonRecursive preDefs[0]! then
/-
We must erase `recApp` annotations even when `preDef` is not recursive
because it may use another recursive declaration in the same mutual block.
See issue #2321
-/
let preDef eraseRecAppSyntax preDefs[0]!
ensureEqnReservedNamesAvailable preDef.declName
if preDef.modifiers.isNoncomputable then
addNonRec preDef
else
addAndCompileNonRec preDef
preDef.termination.ensureNone "not recursive"
else if preDefs.any (·.modifiers.isUnsafe) then
addAndCompileUnsafe preDefs
preDefs.forM (·.termination.ensureNone "unsafe")
else if preDefs.any (·.modifiers.isPartial) then
for preDef in preDefs do
if preDef.modifiers.isPartial && !( whnfD preDef.type).isForall then
withRef preDef.ref <| throwError "invalid use of 'partial', '{preDef.declName}' is not a function{indentExpr preDef.type}"
addAndCompilePartial preDefs
preDefs.forM (·.termination.ensureNone "partial")
else
withRef (preDefs[0]!.ref) <| mapError
(orelseMergeErrors
(structuralRecursion preDefs termArg?s)
(wfRecursion preDefs termArg?s))
(fun msg =>
let preDefMsgs := preDefs.toList.map (MessageData.ofExpr $ mkConst ·.declName)
m!"fail to show termination for{indentD (MessageData.joinSep preDefMsgs Format.line)}\nwith errors\n{msg}")
catch ex =>
logException ex
let s saveState
try
if preDefs.all fun preDef => preDef.kind == DefKind.def || preDefs.all fun preDef => preDef.kind == DefKind.abbrev then
-- try to add as partial definition
ensureFunIndReservedNamesAvailable preDefs
try
checkCodomainsLevel preDefs
checkTerminationByHints preDefs
let termArg?s elabTerminationByHints preDefs
if shouldUseStructural preDefs then
structuralRecursion preDefs termArg?s
else if shouldUseWF preDefs then
wfRecursion preDefs termArg?s
else
withRef (preDefs[0]!.ref) <| mapError
(orelseMergeErrors
(structuralRecursion preDefs termArg?s)
(wfRecursion preDefs termArg?s))
(fun msg =>
let preDefMsgs := preDefs.toList.map (MessageData.ofExpr $ mkConst ·.declName)
m!"fail to show termination for{indentD (MessageData.joinSep preDefMsgs Format.line)}\nwith errors\n{msg}")
catch ex =>
logException ex
let s saveState
try
addAndCompilePartial preDefs (useSorry := true)
catch _ =>
-- Compilation failed try again just as axiom
s.restore
addAsAxioms preDefs
else if preDefs.all fun preDef => preDef.kind == DefKind.theorem then
addAsAxioms preDefs
catch _ => s.restore
if preDefs.all fun preDef => preDef.kind == DefKind.def || preDefs.all fun preDef => preDef.kind == DefKind.abbrev then
-- try to add as partial definition
try
addAndCompilePartial preDefs (useSorry := true)
catch _ =>
-- Compilation failed try again just as axiom
s.restore
addAsAxioms preDefs
else if preDefs.all fun preDef => preDef.kind == DefKind.theorem then
addAsAxioms preDefs
catch _ => s.restore
builtin_initialize
registerTraceClass `Elab.definition.body

View File

@@ -245,18 +245,7 @@ def mkBRecOnConst (recArgInfos : Array RecArgInfo) (positions : Positions)
decLevel brecOnUniv
else
pure brecOnUniv
let brecOnCons := fun idx =>
let brecOn :=
if let .some n := indGroup.all[idx]? then
if useBInductionOn then .const (mkBInductionOnName n) indGroup.levels
else .const (mkBRecOnName n) (brecOnUniv :: indGroup.levels)
else
let n := indGroup.all[0]!
let j := idx - indGroup.all.size + 1
if useBInductionOn then .const (mkBInductionOnName n |>.appendIndexAfter j) indGroup.levels
else .const (mkBRecOnName n |>.appendIndexAfter j) (brecOnUniv :: indGroup.levels)
mkAppN brecOn indGroup.params
let brecOnCons := fun idx => indGroup.brecOn useBInductionOn brecOnUniv idx
-- Pick one as a prototype
let brecOnAux := brecOnCons 0
-- Infer the type of the packed motive arguments

View File

@@ -21,6 +21,7 @@ namespace Structural
structure EqnInfo extends EqnInfoCore where
recArgPos : Nat
declNames : Array Name
numFixed : Nat
deriving Inhabited
private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
@@ -81,9 +82,11 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo mkMapDeclarationExtension
def registerEqnsInfo (preDef : PreDefinition) (declNames : Array Name) (recArgPos : Nat) : CoreM Unit := do
def registerEqnsInfo (preDef : PreDefinition) (declNames : Array Name) (recArgPos : Nat)
(numFixed : Nat) : CoreM Unit := do
ensureEqnReservedNamesAvailable preDef.declName
modifyEnv fun env => eqnInfoExt.insert env preDef.declName { preDef with recArgPos, declNames }
modifyEnv fun env => eqnInfoExt.insert env preDef.declName
{ preDef with recArgPos, declNames, numFixed }
def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
if let some info := eqnInfoExt.find? ( getEnv) declName then

View File

@@ -62,6 +62,19 @@ def IndGroupInst.isDefEq (igi1 igi2 : IndGroupInst) : MetaM Bool := do
unless ( (igi1.params.zip igi2.params).allM (fun (e₁, e₂) => Meta.isDefEqGuarded e₁ e₂)) do return false
return true
/-- Instantiates the right `.brecOn` or `.bInductionOn` for the given type former index,
including universe parameters and fixed prefix. -/
def IndGroupInst.brecOn (group : IndGroupInst) (ind : Bool) (lvl : Level) (idx : Nat) : Expr :=
let e := if let .some n := group.all[idx]? then
if ind then .const (mkBInductionOnName n) group.levels
else .const (mkBRecOnName n) (lvl :: group.levels)
else
let n := group.all[0]!
let j := idx - group.all.size + 1
if ind then .const (mkBInductionOnName n |>.appendIndexAfter j) group.levels
else .const (mkBRecOnName n |>.appendIndexAfter j) (lvl :: group.levels)
mkAppN e group.params
/--
Figures out the nested type formers of an inductive group, with parameters instantiated
and indices still forall-abstracted.

View File

@@ -128,7 +128,7 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (xs : Array Expr
return (Array.zip preDefs valuesNew).map fun preDef, valueNew => { preDef with value := valueNew }
private def inferRecArgPos (preDefs : Array PreDefinition) (termArg?s : Array (Option TerminationArgument)) :
M (Array Nat × Array PreDefinition) := do
M (Array Nat × (Array PreDefinition) × Nat) := do
withoutModifyingEnv do
preDefs.forM (addAsAxiom ·)
let fnNames := preDefs.map (·.declName)
@@ -154,7 +154,7 @@ private def inferRecArgPos (preDefs : Array PreDefinition) (termArg?s : Array (O
withErasedFVars (xs.extract numFixed xs.size |>.map (·.fvarId!)) do
let xs := xs[:numFixed]
let preDefs' elimMutualRecursion preDefs xs recArgInfos
return (recArgPoss, preDefs')
return (recArgPoss, preDefs', numFixed)
def reportTermArg (preDef : PreDefinition) (recArgPos : Nat) : MetaM Unit := do
if let some ref := preDef.termination.terminationBy?? then
@@ -167,7 +167,7 @@ def reportTermArg (preDef : PreDefinition) (recArgPos : Nat) : MetaM Unit := do
def structuralRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option TerminationArgument)) : TermElabM Unit := do
let names := preDefs.map (·.declName)
let ((recArgPoss, preDefsNonRec), state) run <| inferRecArgPos preDefs termArg?s
let ((recArgPoss, preDefsNonRec, numFixed), state) run <| inferRecArgPos preDefs termArg?s
for recArgPos in recArgPoss, preDef in preDefs do
reportTermArg preDef recArgPos
state.addMatchers.forM liftM
@@ -190,7 +190,7 @@ def structuralRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Opti
for theorems and definitions that are propositions.
See issue #2327
-/
registerEqnsInfo preDef (preDefs.map (·.declName)) recArgPos
registerEqnsInfo preDef (preDefs.map (·.declName)) recArgPos numFixed
addSmartUnfoldingDef preDef recArgPos
markAsRecursive preDef.declName
applyAttributesOf preDefsNonRec AttributeApplicationTime.afterCompilation

View File

@@ -10,7 +10,7 @@ import Lean.Elab.Term
import Lean.Elab.Binders
import Lean.Elab.SyntheticMVars
import Lean.Elab.PreDefinition.TerminationHint
import Lean.PrettyPrinter.Delaborator
import Lean.PrettyPrinter.Delaborator.Basic
/-!
This module contains
@@ -115,7 +115,7 @@ def TerminationArgument.delab (arity : Nat) (extraParams : Nat) (termArg : Termi
-- any variable not mentioned syntatically (it may appear in the `Expr`, so do not just use
-- `e.bindingBody!.hasLooseBVar`) should be delaborated as a hole.
let vars : TSyntaxArray [`ident, `Lean.Parser.Term.hole] :=
Array.map (fun (i : Ident) => if hasIdent i.getId stxBody then i else hole) vars
Array.map (fun (i : Ident) => if stxBody.raw.hasIdent i.getId then i else hole) vars
-- drop trailing underscores
let mut vars := vars
while ! vars.isEmpty && vars.back.raw.isOfKind ``hole do vars := vars.pop

View File

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
prelude
import Lean.Meta.Tactic.Util
import Lean.Elab.Term
namespace Lean.Elab
@@ -398,12 +399,19 @@ def ensureHasNoMVars (e : Expr) : TacticM Unit := do
if e.hasExprMVar then
throwError "tactic failed, resulting expression contains metavariables{indentExpr e}"
/-- Close main goal using the given expression. If `checkUnassigned == true`, then `val` must not contain unassigned metavariables. -/
def closeMainGoal (val : Expr) (checkUnassigned := true): TacticM Unit := do
/--
Closes main goal using the given expression.
If `checkUnassigned == true`, then `val` must not contain unassigned metavariables.
Returns `true` if `val` was successfully used to close the goal.
-/
def closeMainGoal (tacName : Name) (val : Expr) (checkUnassigned := true): TacticM Unit := do
if checkUnassigned then
ensureHasNoMVars val
( getMainGoal).assign val
replaceMainGoal []
let mvarId getMainGoal
if ( mvarId.checkedAssign val) then
replaceMainGoal []
else
throwTacticEx tacName mvarId m!"attempting to close the goal using{indentExpr val}\nthis is often due occurs-check failure"
@[inline] def liftMetaMAtMain (x : MVarId MetaM α) : TacticM α := do
withMainContext do x ( getMainGoal)

View File

@@ -56,9 +56,9 @@ def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (mayPostpo
return e
/-- Try to close main goal using `x target`, where `target` is the type of the main goal. -/
def closeMainGoalUsing (x : Expr TacticM Expr) (checkUnassigned := true) : TacticM Unit :=
def closeMainGoalUsing (tacName : Name) (x : Expr TacticM Expr) (checkUnassigned := true) : TacticM Unit :=
withMainContext do
closeMainGoal (checkUnassigned := checkUnassigned) ( x ( getMainTarget))
closeMainGoal (tacName := tacName) (checkUnassigned := checkUnassigned) ( x ( getMainTarget))
def logUnassignedAndAbort (mvarIds : Array MVarId) : TacticM Unit := do
if ( Term.logUnassignedUsingErrorInfos mvarIds) then
@@ -68,13 +68,14 @@ def filterOldMVars (mvarIds : Array MVarId) (mvarCounterSaved : Nat) : MetaM (Ar
let mctx getMCtx
return mvarIds.filter fun mvarId => (mctx.getDecl mvarId |>.index) >= mvarCounterSaved
@[builtin_tactic «exact»] def evalExact : Tactic := fun stx =>
@[builtin_tactic «exact»] def evalExact : Tactic := fun stx => do
match stx with
| `(tactic| exact $e) => closeMainGoalUsing (checkUnassigned := false) fun type => do
let mvarCounterSaved := ( getMCtx).mvarCounter
let r elabTermEnsuringType e type
logUnassignedAndAbort ( filterOldMVars ( getMVars r) mvarCounterSaved)
return r
| `(tactic| exact $e) =>
closeMainGoalUsing `exact (checkUnassigned := false) fun type => do
let mvarCounterSaved := ( getMCtx).mvarCounter
let r elabTermEnsuringType e type
logUnassignedAndAbort ( filterOldMVars ( getMVars r) mvarCounterSaved)
return r
| _ => throwUnsupportedSyntax
def sortMVarIdArrayByIndex [MonadMCtx m] [Monad m] (mvarIds : Array MVarId) : m (Array MVarId) := do
@@ -393,7 +394,7 @@ private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := do
return inst
@[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun _ =>
closeMainGoalUsing fun expectedType => do
closeMainGoalUsing `decide fun expectedType => do
let expectedType preprocessPropToDecide expectedType
let d mkDecide expectedType
let d instantiateMVars d
@@ -472,7 +473,7 @@ private def mkNativeAuxDecl (baseName : Name) (type value : Expr) : TermElabM Na
pure auxName
@[builtin_tactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun _ =>
closeMainGoalUsing fun expectedType => do
closeMainGoalUsing `nativeDecide fun expectedType => do
let expectedType preprocessPropToDecide expectedType
let d mkDecide expectedType
let auxDeclName mkNativeAuxDecl `_nativeDecide (Lean.mkConst `Bool) d

View File

@@ -74,16 +74,16 @@ def mkExtIffType (extThmName : Name) : MetaM Expr := withLCtx {} {} do
let some (_, x, y) := ty.eq? | failNotEq
let some xIdx := args.findIdx? (· == x) | failNotEq
let some yIdx := args.findIdx? (· == y) | failNotEq
unless xIdx == yIdx + 1 || xIdx + 1 == yIdx do
unless xIdx + 1 == yIdx do
throwError "expecting {x} and {y} to be consecutive arguments"
let startIdx := max xIdx yIdx + 1
let startIdx := yIdx + 1
let toRevert := args[startIdx:].toArray
let fvars toRevert.foldlM (init := {}) (fun st e => return collectFVars st ( inferType e))
for fvar in toRevert do
unless Meta.isProof fvar do
throwError "argument {fvar} is not a proof, which is not supported"
throwError "argument {fvar} is not a proof, which is not supported for arguments after {x} and {y}"
if fvars.fvarSet.contains fvar.fvarId! then
throwError "argument {fvar} is depended upon, which is not supported"
throwError "argument {fvar} is depended upon, which is not supported for arguments after {x} and {y}"
let conj := mkAndN ( toRevert.mapM (inferType ·)).toList
-- Make everything implicit except for inst implicits
let mut newBis := #[]
@@ -104,27 +104,31 @@ def realizeExtTheorem (structName : Name) (flat : Bool) : Elab.Command.CommandEl
throwError "'{structName}' is not a structure"
let extName := structName.mkStr "ext"
unless ( getEnv).contains extName do
Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extName do
let type mkExtType structName flat
let pf withSynthesize do
let indVal getConstInfoInduct structName
let params := Array.mkArray indVal.numParams ( `(_))
Elab.Term.elabTermEnsuringType (expectedType? := type) (implicitLambda := false)
-- introduce the params, do cases on 'x' and 'y', and then substitute each equation
( `(by intro $params* {..} {..}; intros; subst_eqs; rfl))
let pf instantiateMVars pf
if pf.hasMVar then throwError "(internal error) synthesized ext proof contains metavariables{indentD pf}"
let info getConstInfo structName
addDecl <| Declaration.thmDecl {
name := extName
type
value := pf
levelParams := info.levelParams
}
modifyEnv fun env => addProtected env extName
Lean.addDeclarationRanges extName {
range := getDeclarationRange ( getRef)
selectionRange := getDeclarationRange ( getRef) }
try
Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extName do
let type mkExtType structName flat
let pf withSynthesize do
let indVal getConstInfoInduct structName
let params := Array.mkArray indVal.numParams ( `(_))
Elab.Term.elabTermEnsuringType (expectedType? := type) (implicitLambda := false)
-- introduce the params, do cases on 'x' and 'y', and then substitute each equation
( `(by intro $params* {..} {..}; intros; subst_eqs; rfl))
let pf instantiateMVars pf
if pf.hasMVar then throwError "(internal error) synthesized ext proof contains metavariables{indentD pf}"
let info getConstInfo structName
addDecl <| Declaration.thmDecl {
name := extName
type
value := pf
levelParams := info.levelParams
}
modifyEnv fun env => addProtected env extName
Lean.addDeclarationRanges extName {
range := getDeclarationRange ( getRef)
selectionRange := getDeclarationRange ( getRef) }
catch e =>
throwError m!"\
Failed to generate an 'ext' theorem for '{MessageData.ofConstName structName}': {e.toMessageData}"
return extName
/--
@@ -138,29 +142,35 @@ def realizeExtIffTheorem (extName : Name) : Elab.Command.CommandElabM Name := do
| .str n s => .str n (s ++ "_iff")
| _ => .str extName "ext_iff"
unless ( getEnv).contains extIffName do
let info getConstInfo extName
Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extIffName do
let type mkExtIffType extName
let pf withSynthesize do
Elab.Term.elabTermEnsuringType (expectedType? := type) <| `(by
intros
refine ?_, ?_
· intro h; cases h; and_intros <;> (intros; first | rfl | simp | fail "Failed to prove converse of ext theorem")
· intro; (repeat cases _ _); apply $(mkCIdent extName) <;> assumption)
let pf instantiateMVars pf
if pf.hasMVar then throwError "(internal error) synthesized ext_iff proof contains metavariables{indentD pf}"
addDecl <| Declaration.thmDecl {
name := extIffName
type
value := pf
levelParams := info.levelParams
}
-- Only declarations in a namespace can be protected:
unless extIffName.isAtomic do
modifyEnv fun env => addProtected env extIffName
Lean.addDeclarationRanges extIffName {
range := getDeclarationRange ( getRef)
selectionRange := getDeclarationRange ( getRef) }
try
let info getConstInfo extName
Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extIffName do
let type mkExtIffType extName
let pf withSynthesize do
Elab.Term.elabTermEnsuringType (expectedType? := type) <| `(by
intros
refine ?_, ?_
· intro h; cases h; and_intros <;> (intros; first | rfl | simp | fail "Failed to prove converse of ext theorem")
· intro; (repeat cases _ _); apply $(mkCIdent extName) <;> assumption)
let pf instantiateMVars pf
if pf.hasMVar then throwError "(internal error) synthesized ext_iff proof contains metavariables{indentD pf}"
addDecl <| Declaration.thmDecl {
name := extIffName
type
value := pf
levelParams := info.levelParams
}
-- Only declarations in a namespace can be protected:
unless extIffName.isAtomic do
modifyEnv fun env => addProtected env extIffName
Lean.addDeclarationRanges extIffName {
range := getDeclarationRange ( getRef)
selectionRange := getDeclarationRange ( getRef) }
catch e =>
throwError m!"\
Failed to generate an 'ext_iff' theorem from '{MessageData.ofConstName extName}': {e.toMessageData}\n\
\n\
Try '@[ext (iff := false)]' to prevent generating an 'ext_iff' theorem."
return extIffName

View File

@@ -504,6 +504,14 @@ def mkArrayLit (type : Expr) (xs : List Expr) : MetaM Expr := do
let listLit mkListLit type xs
return mkApp (mkApp (mkConst ``List.toArray [u]) type) listLit
def mkNone (type : Expr) : MetaM Expr := do
let u getDecLevel type
return mkApp (mkConst ``Option.none [u]) type
def mkSome (type value : Expr) : MetaM Expr := do
let u getDecLevel type
return mkApp2 (mkConst ``Option.some [u]) type value
def mkSorry (type : Expr) (synthetic : Bool) : MetaM Expr := do
let u getLevel type
return mkApp2 (mkConst ``sorryAx [u]) type (toExpr synthetic)

View File

@@ -1865,9 +1865,13 @@ abbrev isDefEqGuarded (t s : Expr) : MetaM Bool :=
def isDefEqNoConstantApprox (t s : Expr) : MetaM Bool :=
approxDefEq <| isDefEq t s
/-- Shorthand for `isDefEq (mkMVar mvarId) val` -/
def _root_.Lean.MVarId.checkedAssign (mvarId : MVarId) (val : Expr) : MetaM Bool :=
isDefEq (mkMVar mvarId) val
/--
Returns `true` if `mvarId := val` was successfully assigned.
This method uses the same assignment validation performed by `isDefEq`, but it does not check whether the types match.
-/
-- Remark: this method is implemented at `ExprDefEq`
@[extern "lean_checked_assign"]
opaque _root_.Lean.MVarId.checkedAssign (mvarId : MVarId) (val : Expr) : MetaM Bool
/--
Eta expand the given expression.

View File

@@ -1046,6 +1046,15 @@ def checkAssignment (mvarId : MVarId) (fvars : Array Expr) (v : Expr) : MetaM (O
return none
return some v
-- Implementation for `_root_.Lean.MVarId.checkedAssign`
@[export lean_checked_assign]
def checkedAssignImpl (mvarId : MVarId) (val : Expr) : MetaM Bool := do
if let some val checkAssignment mvarId #[] val then
mvarId.assign val
return true
else
return false
private def processAssignmentFOApproxAux (mvar : Expr) (args : Array Expr) (v : Expr) : MetaM Bool :=
match v with
| .mdata _ e => processAssignmentFOApproxAux mvar args e

View File

@@ -176,4 +176,48 @@ def litToCtor (e : Expr) : MetaM Expr := do
return mkApp3 (mkConst ``Fin.mk) n i h
return e
/--
Check if an expression is a list literal (i.e. a nested chain of `List.cons`, ending at a `List.nil`),
where each element is "recognised" by a given function `f : Expr → MetaM (Option α)`,
and return the array of recognised values.
-/
partial def getListLitOf? (e : Expr) (f : Expr MetaM (Option α)) : MetaM (Option (Array α)) := do
let mut e instantiateMVars e.consumeMData
let mut r := #[]
while true do
match_expr e with
| List.nil _ => break
| List.cons _ a as => do
let some a f a | return none
r := r.push a
e := as
| _ => return none
return some r
/--
Check if an expression is a list literal (i.e. a nested chain of `List.cons`, ending at a `List.nil`),
returning the array of `Expr` values.
-/
def getListLit? (e : Expr) : MetaM (Option (Array Expr)) := getListLitOf? e fun s => return some s
/--
Check if an expression is an array literal
(i.e. `List.toArray` applied to a nested chain of `List.cons`, ending at a `List.nil`),
where each element is "recognised" by a given function `f : Expr → MetaM (Option α)`,
and return the array of recognised values.
-/
def getArrayLitOf? (e : Expr) (f : Expr MetaM (Option α)) : MetaM (Option (Array α)) := do
let e instantiateMVars e.consumeMData
match_expr e with
| List.toArray _ as => getListLitOf? as f
| _ => return none
/--
Check if an expression is an array literal
(i.e. `List.toArray` applied to a nested chain of `List.cons`, ending at a `List.nil`),
returning the array of `Expr` values.
-/
def getArrayLit? (e : Expr) : MetaM (Option (Array Expr)) := getArrayLitOf? e fun s => return some s
end Lean.Meta

View File

@@ -13,3 +13,4 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
import Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
import Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List
import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Array

View File

@@ -0,0 +1,36 @@
/-
Copyright (c) 2024 Lean FRO. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison
-/
prelude
import Lean.Meta.LitValues
import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
namespace Array
open Lean Meta Simp
/-- Simplification procedure for `#[...][n]` for `n` a `Nat` literal. -/
builtin_dsimproc [simp, seval] reduceGetElem (@GetElem.getElem (Array _) Nat _ _ _ _ _ _) := fun e => do
let_expr GetElem.getElem _ _ _ _ _ xs n _ e | return .continue
let some n Nat.fromExpr? n | return .continue
let some xs getArrayLit? xs | return .continue
return .done <| xs[n]!
/-- Simplification procedure for `#[...][n]?` for `n` a `Nat` literal. -/
builtin_dsimproc [simp, seval] reduceGetElem? (@GetElem?.getElem? (Array _) Nat _ _ _ _ _) := fun e => do
let_expr GetElem?.getElem? _ _ α _ _ xs n e | return .continue
let some n Nat.fromExpr? n | return .continue
let some xs getArrayLit? xs | return .continue
let r if h : n < xs.size then mkSome α xs[n] else mkNone α
return .done r
/-- Simplification procedure for `#[...][n]!` for `n` a `Nat` literal. -/
builtin_dsimproc [simp, seval] reduceGetElem! (@GetElem?.getElem! (Array _) Nat _ _ _ _ _ _) := fun e => do
let_expr GetElem?.getElem! _ _ α _ _ I xs n e | return .continue
let some n Nat.fromExpr? n | return .continue
let some xs getArrayLit? xs | return .continue
let r if h : n < xs.size then pure xs[n] else mkDefault α
return .done r
end Array

View File

@@ -179,14 +179,6 @@ do not yield the right result.
@[builtin_term_parser] def tuple := leading_parser
"(" >> optional (withoutPosition (withoutForbidden (termParser >> ", " >> sepBy1 termParser ", " (allowTrailingSep := true)))) >> ")"
/-- Universe polymorphic tuple notation; `()ₚ` is short for `PUnit.unit`, `(a, b, c)ₚ` for `PProd.mk a (PProd.mk b c)`, etc. -/
@[builtin_term_parser] def ptuple := leading_parser
"(" >> optional (withoutPosition (withoutForbidden (termParser >> ", " >> sepBy1 termParser ", " (allowTrailingSep := true)))) >> ")ₚ"
/-- Universe monomorphic tuple notation; `(a, b, c)ₘ` for `MProd.mk a (MProd.mk b c)`, etc. -/
@[builtin_term_parser] def mtuple := leading_parser
"(" >> withoutPosition (withoutForbidden (termParser >> ", " >> sepBy1 termParser ", " (allowTrailingSep := true))) >> ")ₘ"
/--
Parentheses, used for grouping expressions (e.g., `a * (b + c)`).
Can also be used for creating simple functions when combined with `·`. Here are some examples:

View File

@@ -199,6 +199,10 @@ def unexpandStructureInstance (stx : Syntax) : Delab := whenPPOption getPPStruct
let mut fields := #[]
guard $ fieldNames.size == stx[1].getNumArgs
if hasPPUsingAnonymousConstructorAttribute env s.induct then
/- Note that we don't flatten anonymous constructor notation. Only a complete such notation receives TermInfo,
and flattening would cause the flattened-in notation to lose its TermInfo.
Potentially it would be justified to flatten anonymous constructor notation when the terms are
from the same type family (think `Sigma`), but for now users can write a custom delaborator in such instances. -/
return withTypeAscription (cond := ( withType <| getPPOption getPPStructureInstanceType)) do
`($[$(stx[1].getArgs)],*)
let args := e.getAppArgs
@@ -769,16 +773,6 @@ def delabMData : Delab := do
else
withMDataOptions delab
/--
Check for a `Syntax.ident` of the given name anywhere in the tree.
This is usually a bad idea since it does not check for shadowing bindings,
but in the delaborator we assume that bindings are never shadowed.
-/
partial def hasIdent (id : Name) : Syntax Bool
| Syntax.ident _ _ id' _ => id == id'
| Syntax.node _ _ args => args.any (hasIdent id)
| _ => false
/--
Return `true` iff current binder should be merged with the nested
binder, if any, into a single binder group:
@@ -824,7 +818,7 @@ def delabLam : Delab :=
let e getExpr
let stxT withBindingDomain delab
let ppTypes getPPOption getPPFunBinderTypes
let usedDownstream := curNames.any (fun n => hasIdent n.getId stxBody)
let usedDownstream := curNames.any (fun n => stxBody.hasIdent n.getId)
-- leave lambda implicit if possible
-- TODO: for now we just always block implicit lambdas when delaborating. We can revisit.
@@ -1135,6 +1129,24 @@ def delabSigma : Delab := delabSigmaCore (sigma := true)
@[builtin_delab app.PSigma]
def delabPSigma : Delab := delabSigmaCore (sigma := false)
-- PProd and MProd value delaborator
-- (like pp_using_anonymous_constructor but flattening nested tuples)
def delabPProdMkCore (mkName : Name) : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation do
guard <| ( getExpr).getAppNumArgs == 4
let a withAppFn <| withAppArg delab
let b withAppArg <| delab
if ( getExpr).appArg!.isAppOfArity mkName 4 then
if let `($xs,*) := b then
return `($a, $xs,*)
`($a, $b)
@[builtin_delab app.PProd.mk]
def delabPProdMk : Delab := delabPProdMkCore ``PProd.mk
@[builtin_delab app.MProd.mk]
def delabMProdMk : Delab := delabPProdMkCore ``MProd.mk
partial def delabDoElems : DelabM (List Syntax) := do
let e getExpr
if e.isAppOfArity ``Bind.bind 6 then

View File

@@ -164,6 +164,16 @@ def asNode : Syntax → SyntaxNode
def getIdAt (stx : Syntax) (i : Nat) : Name :=
(stx.getArg i).getId
/--
Check for a `Syntax.ident` of the given name anywhere in the tree.
This is usually a bad idea since it does not check for shadowing bindings,
but in the delaborator we assume that bindings are never shadowed.
-/
partial def hasIdent (id : Name) : Syntax Bool
| ident _ _ id' _ => id == id'
| node _ _ args => args.any (hasIdent id)
| _ => false
@[inline] def modifyArgs (stx : Syntax) (fn : Array Syntax Array Syntax) : Syntax :=
match stx with
| node i k args => node i k (fn args)

View File

@@ -31,3 +31,4 @@ import Lean.Util.FileSetupInfo
import Lean.Util.Heartbeats
import Lean.Util.SearchPath
import Lean.Util.SafeExponentiation
import Lean.Util.NumObjs

View File

@@ -9,48 +9,11 @@ import Lean.Util.PtrSet
namespace Lean
namespace Expr
namespace FindImpl
unsafe abbrev FindM := StateT (PtrSet Expr) Id
@[extern "lean_find_expr"]
opaque findImpl? (p : @& (Expr Bool)) (e : @& Expr) : Option Expr
@[inline] unsafe def checkVisited (e : Expr) : OptionT FindM Unit := do
if ( get).contains e then
failure
modify fun s => s.insert e
unsafe def findM? (p : Expr Bool) (e : Expr) : OptionT FindM Expr :=
let rec visit (e : Expr) := do
checkVisited e
if p e then
pure e
else match e with
| .forallE _ d b _ => visit d <|> visit b
| .lam _ d b _ => visit d <|> visit b
| .mdata _ b => visit b
| .letE _ t v b _ => visit t <|> visit v <|> visit b
| .app f a => visit f <|> visit a
| .proj _ _ b => visit b
| _ => failure
visit e
unsafe def findUnsafe? (p : Expr Bool) (e : Expr) : Option Expr :=
Id.run <| findM? p e |>.run' mkPtrSet
end FindImpl
@[implemented_by FindImpl.findUnsafe?]
def find? (p : Expr Bool) (e : Expr) : Option Expr :=
/- This is a reference implementation for the unsafe one above -/
if p e then
some e
else match e with
| .forallE _ d b _ => find? p d <|> find? p b
| .lam _ d b _ => find? p d <|> find? p b
| .mdata _ b => find? p b
| .letE _ t v b _ => find? p t <|> find? p v <|> find? p b
| .app f a => find? p f <|> find? p a
| .proj _ _ b => find? p b
| _ => none
@[inline] def find? (p : Expr Bool) (e : Expr) : Option Expr := findImpl? p e
/-- Return true if `e` occurs in `t` -/
def occurs (e : Expr) (t : Expr) : Bool :=
@@ -64,41 +27,13 @@ inductive FindStep where
/-- Search subterms -/ | visit
/-- Do not search subterms -/ | done
namespace FindExtImpl
unsafe def findM? (p : Expr FindStep) (e : Expr) : OptionT FindImpl.FindM Expr :=
visit e
where
visitApp (e : Expr) :=
match e with
| .app f a .. => visitApp f <|> visit a
| e => visit e
visit (e : Expr) := do
FindImpl.checkVisited e
match p e with
| .done => failure
| .found => pure e
| .visit =>
match e with
| .forallE _ d b _ => visit d <|> visit b
| .lam _ d b _ => visit d <|> visit b
| .mdata _ b => visit b
| .letE _ t v b _ => visit t <|> visit v <|> visit b
| .app .. => visitApp e
| .proj _ _ b => visit b
| _ => failure
unsafe def findUnsafe? (p : Expr FindStep) (e : Expr) : Option Expr :=
Id.run <| findM? p e |>.run' mkPtrSet
end FindExtImpl
@[extern "lean_find_ext_expr"]
opaque findExtImpl? (p : @& (Expr FindStep)) (e : @& Expr) : Option Expr
/--
Similar to `find?`, but `p` can return `FindStep.done` to interrupt the search on subterms.
Remark: Differently from `find?`, we do not invoke `p` for partial applications of an application. -/
@[implemented_by FindExtImpl.findUnsafe?]
opaque findExt? (p : Expr FindStep) (e : Expr) : Option Expr
@[inline] def findExt? (p : Expr FindStep) (e : Expr) : Option Expr := findExtImpl? p e
end Expr
end Lean

View File

@@ -0,0 +1,47 @@
/-
Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Expr
import Lean.Util.PtrSet
namespace Lean.Expr
namespace NumObjs
unsafe structure State where
visited : PtrSet Expr := mkPtrSet
counter : Nat := 0
unsafe abbrev M := StateM State
unsafe def visit (e : Expr) : M Unit :=
unless ( get).visited.contains e do
modify fun { visited, counter } => { visited := visited.insert e, counter := counter + 1 }
match e with
| .forallE _ d b _ => visit d; visit b
| .lam _ d b _ => visit d; visit b
| .mdata _ b => visit b
| .letE _ t v b _ => visit t; visit v; visit b
| .app f a => visit f; visit a
| .proj _ _ b => visit b
| _ => return ()
unsafe def main (e : Expr) : Nat :=
let (_, s) := NumObjs.visit e |>.run {}
s.counter
end NumObjs
/--
Returns the number of allocated `Expr` objects in the given expression `e`.
This operation is performed in `IO` because the result depends on the memory representation of the object.
Note: Use this function primarily for diagnosing performance issues.
-/
def numObjs (e : Expr) : IO Nat :=
return unsafe NumObjs.main e
end Lean.Expr

View File

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
prelude
import Init.Data.Hashable
import Lean.Data.HashSet
import Lean.Data.HashMap
namespace Lean
@@ -33,4 +34,22 @@ unsafe abbrev PtrSet.insert (s : PtrSet α) (a : α) : PtrSet α :=
unsafe abbrev PtrSet.contains (s : PtrSet α) (a : α) : Bool :=
HashSet.contains s { value := a }
/--
Map of pointers. It is a low-level auxiliary datastructure used for traversing DAGs.
-/
unsafe def PtrMap (α : Type) (β : Type) :=
HashMap (Ptr α) β
unsafe def mkPtrMap {α β : Type} (capacity : Nat := 64) : PtrMap α β :=
mkHashMap capacity
unsafe abbrev PtrMap.insert (s : PtrMap α β) (a : α) (b : β) : PtrMap α β :=
HashMap.insert s { value := a } b
unsafe abbrev PtrMap.contains (s : PtrMap α β) (a : α) : Bool :=
HashMap.contains s { value := a }
unsafe abbrev PtrMap.find? (s : PtrMap α β) (a : α) : Option β :=
HashMap.find? s { value := a }
end Lean

View File

@@ -5,74 +5,59 @@ Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich
-/
prelude
import Lean.Expr
import Lean.Util.PtrSet
namespace Lean
namespace Expr
namespace ReplaceImpl
structure Cache where
size : USize
-- First `size` elements are the keys.
-- Second `size` elements are the results.
keysResults : Array NonScalar -- Either Expr or Unit (disjoint memory representation)
unsafe abbrev ReplaceM := StateM (PtrMap Expr Expr)
unsafe def Cache.new (e : Expr) : Cache :=
-- scale size with approximate number of subterms up to 8k
-- make sure size is coprime with power of two for collision avoidance
let size := (1 <<< min (max e.approxDepth.toUSize 1) 13) - 1
{ size, keysResults := mkArray (2 * size).toNat (unsafeCast ()) }
@[inline]
unsafe def Cache.keyIdx (c : Cache) (key : Expr) : USize :=
ptrAddrUnsafe key % c.size
@[inline]
unsafe def Cache.resultIdx (c : Cache) (key : Expr) : USize :=
c.keyIdx key + c.size
@[inline]
unsafe def Cache.hasResultFor (c : Cache) (key : Expr) : Bool :=
have : (c.keyIdx key).toNat < c.keysResults.size := lcProof
ptrEq (unsafeCast key) c.keysResults[c.keyIdx key]
@[inline]
unsafe def Cache.getResultFor (c : Cache) (key : Expr) : Expr :=
have : (c.resultIdx key).toNat < c.keysResults.size := lcProof
unsafeCast c.keysResults[c.resultIdx key]
unsafe def Cache.store (c : Cache) (key result : Expr) : Cache :=
{ c with keysResults := c.keysResults
|>.uset (c.keyIdx key) (unsafeCast key) lcProof
|>.uset (c.resultIdx key) (unsafeCast result) lcProof }
abbrev ReplaceM := StateM Cache
@[inline]
unsafe def cache (key : Expr) (result : Expr) : ReplaceM Expr := do
modify (·.store key result)
unsafe def cache (key : Expr) (exclusive : Bool) (result : Expr) : ReplaceM Expr := do
unless exclusive do
modify (·.insert key result)
pure result
@[specialize]
unsafe def replaceUnsafeM (f? : Expr Option Expr) (e : Expr) : ReplaceM Expr := do
let rec @[specialize] visit (e : Expr) := do
if ( get).hasResultFor e then
return ( get).getResultFor e
else match f? e with
| some eNew => cache e eNew
/-
TODO: We need better control over RC operations to ensure
the following (unsafe) optimization is correctly applied.
Optimization goal: only cache results for shared objects.
The main problem is that the current code generator ignores borrow annotations
for code written in Lean. These annotations are only taken into account for extern functions.
Moveover, the borrow inference heuristic currently tags `e` as "owned" since it may be stored
in the cache and is used in "update" functions.
Thus, when visiting `e` sub-expressions the code generator increases their RC
because we are recursively invoking `visit` :(
Thus, to fix this issue, we must
1- Take borrow annotations into account for code written in Lean.
2- Mark `e` is borrowed (i.e., `(e : @& Expr)`)
-/
let excl := isExclusiveUnsafe e
unless excl do
if let some result := ( get).find? e then
return result
match f? e with
| some eNew => cache e excl eNew
| none => match e with
| Expr.forallE _ d b _ => cache e <| e.updateForallE! ( visit d) ( visit b)
| Expr.lam _ d b _ => cache e <| e.updateLambdaE! ( visit d) ( visit b)
| Expr.mdata _ b => cache e <| e.updateMData! ( visit b)
| Expr.letE _ t v b _ => cache e <| e.updateLet! ( visit t) ( visit v) ( visit b)
| Expr.app f a => cache e <| e.updateApp! ( visit f) ( visit a)
| Expr.proj _ _ b => cache e <| e.updateProj! ( visit b)
| e => pure e
| .forallE _ d b _ => cache e excl <| e.updateForallE! ( visit d) ( visit b)
| .lam _ d b _ => cache e excl <| e.updateLambdaE! ( visit d) ( visit b)
| .mdata _ b => cache e excl <| e.updateMData! ( visit b)
| .letE _ t v b _ => cache e excl <| e.updateLet! ( visit t) ( visit v) ( visit b)
| .app f a => cache e excl <| e.updateApp! ( visit f) ( visit a)
| .proj _ _ b => cache e excl <| e.updateProj! ( visit b)
| e => return e
visit e
@[inline]
unsafe def replaceUnsafe (f? : Expr Option Expr) (e : Expr) : Expr :=
(replaceUnsafeM f? e).run' (Cache.new e)
(replaceUnsafeM f? e).run' mkPtrMap
end ReplaceImpl
@@ -92,6 +77,10 @@ def replaceNoCache (f? : Expr → Option Expr) (e : Expr) : Expr :=
| .proj _ _ b => let b := replaceNoCache f? b; e.updateProj! b
| e => e
@[extern "lean_replace_expr"]
opaque replaceImpl (f? : @& (Expr Option Expr)) (e : @& Expr) : Expr
@[implemented_by ReplaceImpl.replaceUnsafe]
partial def replace (f? : Expr Option Expr) (e : Expr) : Expr :=
def replace (f? : Expr Option Expr) (e : Expr) : Expr :=
e.replaceNoCache f?

View File

@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Wojciech Nawrocki
-/
prelude
import Lean.PrettyPrinter
import Lean.Server.Rpc.Basic
import Lean.Server.InfoUtils
import Lean.Widget.TaggedText

View File

@@ -30,6 +30,8 @@ universe u v w
variable {α : Type u} {β : α Type v} {δ : Type w} {m : Type w Type w} [Monad m]
variable {_ : BEq α} {_ : Hashable α}
namespace Std
open DHashMap.Internal DHashMap.Internal.List
@@ -42,6 +44,9 @@ and an array of buckets, where each bucket is a linked list of key-value pais. T
is always a power of two. The hash map doubles its size upon inserting an element such that the
number of elements is more than 75% of the number of buckets.
The hash table is backed by an `Array`. Users should make sure that the hash map is used linearly to
avoid expensive copies.
The hash map uses `==` (provided by the `BEq` typeclass) to compare keys and `hash` (provided by
the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
@@ -66,34 +71,34 @@ instance [BEq α] [Hashable α] : EmptyCollection (DHashMap α β) where
instance [BEq α] [Hashable α] : Inhabited (DHashMap α β) where
default :=
@[inline, inherit_doc Raw.insert] def insert [BEq α] [Hashable α] (m : DHashMap α β) (a : α)
@[inline, inherit_doc Raw.insert] def insert (m : DHashMap α β) (a : α)
(b : β a) : DHashMap α β :=
Raw₀.insert m.1, m.2.size_buckets_pos a b, .insert₀ m.2
@[inline, inherit_doc Raw.insertIfNew] def insertIfNew [BEq α] [Hashable α] (m : DHashMap α β)
@[inline, inherit_doc Raw.insertIfNew] def insertIfNew (m : DHashMap α β)
(a : α) (b : β a) : DHashMap α β :=
Raw₀.insertIfNew m.1, m.2.size_buckets_pos a b, .insertIfNew₀ m.2
@[inline, inherit_doc Raw.containsThenInsert] def containsThenInsert [BEq α] [Hashable α]
@[inline, inherit_doc Raw.containsThenInsert] def containsThenInsert
(m : DHashMap α β) (a : α) (b : β a) : Bool × DHashMap α β :=
let m' := Raw₀.containsThenInsert m.1, m.2.size_buckets_pos a b
m'.1, m'.2.1, .containsThenInsert₀ m.2
@[inline, inherit_doc Raw.containsThenInsertIfNew] def containsThenInsertIfNew [BEq α] [Hashable α]
@[inline, inherit_doc Raw.containsThenInsertIfNew] def containsThenInsertIfNew
(m : DHashMap α β) (a : α) (b : β a) : Bool × DHashMap α β :=
let m' := Raw₀.containsThenInsertIfNew m.1, m.2.size_buckets_pos a b
m'.1, m'.2.1, .containsThenInsertIfNew₀ m.2
@[inline, inherit_doc Raw.getThenInsertIfNew?] def getThenInsertIfNew? [BEq α] [Hashable α]
@[inline, inherit_doc Raw.getThenInsertIfNew?] def getThenInsertIfNew?
[LawfulBEq α] (m : DHashMap α β) (a : α) (b : β a) : Option (β a) × DHashMap α β :=
let m' := Raw₀.getThenInsertIfNew? m.1, m.2.size_buckets_pos a b
m'.1, m'.2.1, .getThenInsertIfNew?₀ m.2
@[inline, inherit_doc Raw.get?] def get? [BEq α] [LawfulBEq α] [Hashable α] (m : DHashMap α β)
@[inline, inherit_doc Raw.get?] def get? [LawfulBEq α] (m : DHashMap α β)
(a : α) : Option (β a) :=
Raw₀.get? m.1, m.2.size_buckets_pos a
@[inline, inherit_doc Raw.contains] def contains [BEq α] [Hashable α] (m : DHashMap α β) (a : α) :
@[inline, inherit_doc Raw.contains] def contains (m : DHashMap α β) (a : α) :
Bool :=
Raw₀.contains m.1, m.2.size_buckets_pos a
@@ -103,19 +108,19 @@ instance [BEq α] [Hashable α] : Membership α (DHashMap α β) where
instance [BEq α] [Hashable α] {m : DHashMap α β} {a : α} : Decidable (a m) :=
show Decidable (m.contains a) from inferInstance
@[inline, inherit_doc Raw.get] def get [BEq α] [Hashable α] [LawfulBEq α] (m : DHashMap α β) (a : α)
@[inline, inherit_doc Raw.get] def get [LawfulBEq α] (m : DHashMap α β) (a : α)
(h : a m) : β a :=
Raw₀.get m.1, m.2.size_buckets_pos a h
@[inline, inherit_doc Raw.get!] def get! [BEq α] [Hashable α] [LawfulBEq α] (m : DHashMap α β)
@[inline, inherit_doc Raw.get!] def get! [LawfulBEq α] (m : DHashMap α β)
(a : α) [Inhabited (β a)] : β a :=
Raw₀.get! m.1, m.2.size_buckets_pos a
@[inline, inherit_doc Raw.getD] def getD [BEq α] [Hashable α] [LawfulBEq α] (m : DHashMap α β)
@[inline, inherit_doc Raw.getD] def getD [LawfulBEq α] (m : DHashMap α β)
(a : α) (fallback : β a) : β a :=
Raw₀.getD m.1, m.2.size_buckets_pos a fallback
@[inline, inherit_doc Raw.erase] def erase [BEq α] [Hashable α] (m : DHashMap α β) (a : α) :
@[inline, inherit_doc Raw.erase] def erase (m : DHashMap α β) (a : α) :
DHashMap α β :=
Raw₀.erase m.1, m.2.size_buckets_pos a, .erase₀ m.2
@@ -123,57 +128,57 @@ section
variable {β : Type v}
@[inline, inherit_doc Raw.Const.get?] def Const.get? [BEq α] [Hashable α]
@[inline, inherit_doc Raw.Const.get?] def Const.get?
(m : DHashMap α (fun _ => β)) (a : α) : Option β :=
Raw₀.Const.get? m.1, m.2.size_buckets_pos a
@[inline, inherit_doc Raw.Const.get] def Const.get [BEq α] [Hashable α]
@[inline, inherit_doc Raw.Const.get] def Const.get
(m : DHashMap α (fun _ => β)) (a : α) (h : a m) : β :=
Raw₀.Const.get m.1, m.2.size_buckets_pos a h
@[inline, inherit_doc Raw.Const.getD] def Const.getD [BEq α] [Hashable α]
@[inline, inherit_doc Raw.Const.getD] def Const.getD
(m : DHashMap α (fun _ => β)) (a : α) (fallback : β) : β :=
Raw₀.Const.getD m.1, m.2.size_buckets_pos a fallback
@[inline, inherit_doc Raw.Const.get!] def Const.get! [BEq α] [Hashable α] [Inhabited β]
@[inline, inherit_doc Raw.Const.get!] def Const.get! [Inhabited β]
(m : DHashMap α (fun _ => β)) (a : α) : β :=
Raw₀.Const.get! m.1, m.2.size_buckets_pos a
@[inline, inherit_doc Raw.Const.getThenInsertIfNew?] def Const.getThenInsertIfNew? [BEq α]
[Hashable α] (m : DHashMap α (fun _ => β)) (a : α) (b : β) :
@[inline, inherit_doc Raw.Const.getThenInsertIfNew?] def Const.getThenInsertIfNew?
(m : DHashMap α (fun _ => β)) (a : α) (b : β) :
Option β × DHashMap α (fun _ => β) :=
let m' := Raw₀.Const.getThenInsertIfNew? m.1, m.2.size_buckets_pos a b
m'.1, m'.2.1, .constGetThenInsertIfNew?₀ m.2
end
@[inline, inherit_doc Raw.size] def size [BEq α] [Hashable α] (m : DHashMap α β) : Nat :=
@[inline, inherit_doc Raw.size] def size (m : DHashMap α β) : Nat :=
m.1.size
@[inline, inherit_doc Raw.isEmpty] def isEmpty [BEq α] [Hashable α] (m : DHashMap α β) : Bool :=
@[inline, inherit_doc Raw.isEmpty] def isEmpty (m : DHashMap α β) : Bool :=
m.1.isEmpty
section Unverified
/-! We currently do not provide lemmas for the functions below. -/
@[inline, inherit_doc Raw.filter] def filter [BEq α] [Hashable α] (f : (a : α) β a Bool)
@[inline, inherit_doc Raw.filter] def filter (f : (a : α) β a Bool)
(m : DHashMap α β) : DHashMap α β :=
Raw₀.filter f m.1, m.2.size_buckets_pos, .filter₀ m.2
@[inline, inherit_doc Raw.foldM] def foldM [BEq α] [Hashable α] (f : δ (a : α) β a m δ)
@[inline, inherit_doc Raw.foldM] def foldM (f : δ (a : α) β a m δ)
(init : δ) (b : DHashMap α β) : m δ :=
b.1.foldM f init
@[inline, inherit_doc Raw.fold] def fold [BEq α] [Hashable α] (f : δ (a : α) β a δ)
@[inline, inherit_doc Raw.fold] def fold (f : δ (a : α) β a δ)
(init : δ) (b : DHashMap α β) : δ :=
b.1.fold f init
@[inline, inherit_doc Raw.forM] def forM [BEq α] [Hashable α] (f : (a : α) β a m PUnit)
@[inline, inherit_doc Raw.forM] def forM (f : (a : α) β a m PUnit)
(b : DHashMap α β) : m PUnit :=
b.1.forM f
@[inline, inherit_doc Raw.forIn] def forIn [BEq α] [Hashable α]
@[inline, inherit_doc Raw.forIn] def forIn
(f : (a : α) β a δ m (ForInStep δ)) (init : δ) (b : DHashMap α β) : m δ :=
b.1.forIn f init
@@ -183,49 +188,49 @@ instance [BEq α] [Hashable α] : ForM m (DHashMap α β) ((a : α) × β a) whe
instance [BEq α] [Hashable α] : ForIn m (DHashMap α β) ((a : α) × β a) where
forIn m init f := m.forIn (fun a b acc => f a, b acc) init
@[inline, inherit_doc Raw.toList] def toList [BEq α] [Hashable α] (m : DHashMap α β) :
@[inline, inherit_doc Raw.toList] def toList (m : DHashMap α β) :
List ((a : α) × β a) :=
m.1.toList
@[inline, inherit_doc Raw.toArray] def toArray [BEq α] [Hashable α] (m : DHashMap α β) :
@[inline, inherit_doc Raw.toArray] def toArray (m : DHashMap α β) :
Array ((a : α) × β a) :=
m.1.toArray
@[inline, inherit_doc Raw.Const.toList] def Const.toList {β : Type v} [BEq α] [Hashable α]
@[inline, inherit_doc Raw.Const.toList] def Const.toList {β : Type v}
(m : DHashMap α (fun _ => β)) : List (α × β) :=
Raw.Const.toList m.1
@[inline, inherit_doc Raw.Const.toArray] def Const.toArray {β : Type v} [BEq α] [Hashable α]
@[inline, inherit_doc Raw.Const.toArray] def Const.toArray {β : Type v}
(m : DHashMap α (fun _ => β)) : Array (α × β) :=
Raw.Const.toArray m.1
@[inline, inherit_doc Raw.keys] def keys [BEq α] [Hashable α] (m : DHashMap α β) : List α :=
@[inline, inherit_doc Raw.keys] def keys (m : DHashMap α β) : List α :=
m.1.keys
@[inline, inherit_doc Raw.keysArray] def keysArray [BEq α] [Hashable α] (m : DHashMap α β) :
@[inline, inherit_doc Raw.keysArray] def keysArray (m : DHashMap α β) :
Array α :=
m.1.keysArray
@[inline, inherit_doc Raw.values] def values {β : Type v} [BEq α] [Hashable α]
@[inline, inherit_doc Raw.values] def values {β : Type v}
(m : DHashMap α (fun _ => β)) : List β :=
m.1.values
@[inline, inherit_doc Raw.valuesArray] def valuesArray {β : Type v} [BEq α] [Hashable α]
@[inline, inherit_doc Raw.valuesArray] def valuesArray {β : Type v}
(m : DHashMap α (fun _ => β)) : Array β :=
m.1.valuesArray
@[inline, inherit_doc Raw.insertMany] def insertMany [BEq α] [Hashable α] {ρ : Type w}
@[inline, inherit_doc Raw.insertMany] def insertMany {ρ : Type w}
[ForIn Id ρ ((a : α) × β a)] (m : DHashMap α β) (l : ρ) : DHashMap α β :=
(Raw₀.insertMany m.1, m.2.size_buckets_pos l).1,
(Raw₀.insertMany m.1, m.2.size_buckets_pos l).2 _ Raw.WF.insert₀ m.2
@[inline, inherit_doc Raw.Const.insertMany] def Const.insertMany {β : Type v} [BEq α] [Hashable α]
@[inline, inherit_doc Raw.Const.insertMany] def Const.insertMany {β : Type v}
{ρ : Type w} [ForIn Id ρ (α × β)] (m : DHashMap α (fun _ => β)) (l : ρ) :
DHashMap α (fun _ => β) :=
(Raw₀.Const.insertMany m.1, m.2.size_buckets_pos l).1,
(Raw₀.Const.insertMany m.1, m.2.size_buckets_pos l).2 _ Raw.WF.insert₀ m.2
@[inline, inherit_doc Raw.Const.insertManyUnit] def Const.insertManyUnit [BEq α] [Hashable α]
@[inline, inherit_doc Raw.Const.insertManyUnit] def Const.insertManyUnit
{ρ : Type w} [ForIn Id ρ α] (m : DHashMap α (fun _ => Unit)) (l : ρ) :
DHashMap α (fun _ => Unit) :=
(Raw₀.Const.insertManyUnit m.1, m.2.size_buckets_pos l).1,
@@ -243,7 +248,7 @@ instance [BEq α] [Hashable α] : ForIn m (DHashMap α β) ((a : α) × β a) wh
DHashMap α (fun _ => Unit) :=
Const.insertManyUnit l
@[inherit_doc Raw.Internal.numBuckets] def Internal.numBuckets [BEq α] [Hashable α]
@[inherit_doc Raw.Internal.numBuckets] def Internal.numBuckets
(m : DHashMap α β) : Nat :=
Raw.Internal.numBuckets m.1

View File

@@ -77,61 +77,61 @@ variable {β : Type v}
/-- Internal implementation detail of the hash map -/
def get? [BEq α] (a : α) : AssocList α (fun _ => β) Option β
| nil => none
| cons k v es => bif a == k then some v else get? a es
| cons k v es => bif k == a then some v else get? a es
end
/-- Internal implementation detail of the hash map -/
def getCast? [BEq α] [LawfulBEq α] (a : α) : AssocList α β Option (β a)
| nil => none
| cons k v es => if h : a == k then some (cast (congrArg β (eq_of_beq h).symm) v)
| cons k v es => if h : k == a then some (cast (congrArg β (eq_of_beq h)) v)
else es.getCast? a
/-- Internal implementation detail of the hash map -/
def contains [BEq α] (a : α) : AssocList α β Bool
| nil => false
| cons k _ l => a == k || l.contains a
| cons k _ l => k == a || l.contains a
/-- Internal implementation detail of the hash map -/
def get {β : Type v} [BEq α] (a : α) : (l : AssocList α (fun _ => β)) l.contains a β
| cons k v es, h => if hka : a == k then v else get a es
| cons k v es, h => if hka : k == a then v else get a es
(by rw [ h, contains, Bool.of_not_eq_true hka, Bool.false_or])
/-- Internal implementation detail of the hash map -/
def getCast [BEq α] [LawfulBEq α] (a : α) : (l : AssocList α β) l.contains a β a
| cons k v es, h => if hka : a == k then cast (congrArg β (eq_of_beq hka).symm) v
| cons k v es, h => if hka : k == a then cast (congrArg β (eq_of_beq hka)) v
else es.getCast a (by rw [ h, contains, Bool.of_not_eq_true hka, Bool.false_or])
/-- Internal implementation detail of the hash map -/
def getCast! [BEq α] [LawfulBEq α] (a : α) [Inhabited (β a)] : AssocList α β β a
| nil => panic! "key is not present in hash table"
| cons k v es => if h : a == k then cast (congrArg β (eq_of_beq h).symm) v else es.getCast! a
| cons k v es => if h : k == a then cast (congrArg β (eq_of_beq h)) v else es.getCast! a
/-- Internal implementation detail of the hash map -/
def get! {β : Type v} [BEq α] [Inhabited β] (a : α) : AssocList α (fun _ => β) β
| nil => panic! "key is not present in hash table"
| cons k v es => bif a == k then v else es.get! a
| cons k v es => bif k == a then v else es.get! a
/-- Internal implementation detail of the hash map -/
def getCastD [BEq α] [LawfulBEq α] (a : α) (fallback : β a) : AssocList α β β a
| nil => fallback
| cons k v es => if h : a == k then cast (congrArg β (eq_of_beq h).symm) v
| cons k v es => if h : k == a then cast (congrArg β (eq_of_beq h)) v
else es.getCastD a fallback
/-- Internal implementation detail of the hash map -/
def getD {β : Type v} [BEq α] (a : α) (fallback : β) : AssocList α (fun _ => β) β
| nil => fallback
| cons k v es => bif a == k then v else es.getD a fallback
| cons k v es => bif k == a then v else es.getD a fallback
/-- Internal implementation detail of the hash map -/
def replace [BEq α] (a : α) (b : β a) : AssocList α β AssocList α β
| nil => nil
| cons k v l => bif a == k then cons a b l else cons k v (replace a b l)
| cons k v l => bif k == a then cons a b l else cons k v (replace a b l)
/-- Internal implementation detail of the hash map -/
def erase [BEq α] (a : α) : AssocList α β AssocList α β
| nil => nil
| cons k v l => bif a == k then l else cons k v (l.erase a)
| cons k v l => bif k == a then l else cons k v (l.erase a)
/-- Internal implementation detail of the hash map -/
@[inline] def filterMap (f : (a : α) β a Option (γ a)) :

View File

@@ -116,14 +116,14 @@ theorem toList_replace [BEq α] {l : AssocList α β} {a : α} {b : β a} :
(l.replace a b).toList = replaceEntry a b l.toList := by
induction l
· simp [replace]
· next k v t ih => cases h : a == k <;> simp_all [replace, List.replaceEntry_cons]
· next k v t ih => cases h : k == a <;> simp_all [replace, List.replaceEntry_cons]
@[simp]
theorem toList_erase [BEq α] {l : AssocList α β} {a : α} :
(l.erase a).toList = eraseKey a l.toList := by
induction l
· simp [erase]
· next k v t ih => cases h : a == k <;> simp_all [erase, List.eraseKey_cons]
· next k v t ih => cases h : k == a <;> simp_all [erase, List.eraseKey_cons]
theorem toList_filterMap {f : (a : α) β a Option (γ a)} {l : AssocList α β} :
Perm (l.filterMap f).toList (l.toList.filterMap fun p => (f p.1 p.2).map (p.1, ·)) := by

View File

@@ -35,19 +35,19 @@ theorem assoc_induction {motive : List ((a : α) × β a) → Prop} (nil : motiv
/-- Internal implementation detail of the hash map -/
def getEntry? [BEq α] (a : α) : List ((a : α) × β a) Option ((a : α) × β a)
| [] => none
| k, v :: l => bif a == k then some k, v else getEntry? a l
| k, v :: l => bif k == a then some k, v else getEntry? a l
@[simp] theorem getEntry?_nil [BEq α] {a : α} :
getEntry? a ([] : List ((a : α) × β a)) = none := rfl
theorem getEntry?_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
getEntry? a (k, v :: l) = bif a == k then some k, v else getEntry? a l := rfl
getEntry? a (k, v :: l) = bif k == a then some k, v else getEntry? a l := rfl
theorem getEntry?_cons_of_true [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : a == k) :
theorem getEntry?_cons_of_true [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : k == a) :
getEntry? a (k, v :: l) = some k, v := by
simp [getEntry?, h]
theorem getEntry?_cons_of_false [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
(h : (a == k) = false) : getEntry? a (k, v :: l) = getEntry? a l := by
(h : (k == a) = false) : getEntry? a (k, v :: l) = getEntry? a l := by
simp [getEntry?, h]
@[simp]
@@ -56,11 +56,11 @@ theorem getEntry?_cons_self [BEq α] [ReflBEq α] {l : List ((a : α) × β a)}
getEntry?_cons_of_true BEq.refl
theorem getEntry?_eq_some [BEq α] {l : List ((a : α) × β a)} {a : α} {p : (a : α) × β a}
(h : getEntry? a l = some p) : a == p.1 := by
(h : getEntry? a l = some p) : p.1 == a := by
induction l using assoc_induction
· simp at h
· next k' v' t ih =>
cases h' : a == k'
cases h' : k' == a
· rw [getEntry?_cons_of_false h'] at h
exact ih h
· rw [getEntry?_cons_of_true h', Option.some.injEq] at h
@@ -72,10 +72,10 @@ theorem getEntry?_congr [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β
induction l using assoc_induction
· simp
· next k v l ih =>
cases h' : b == k
· have h₂ : (a == k) = false := BEq.neq_of_beq_of_neq h h'
cases h' : k == a
· have h₂ : (k == b) = false := BEq.neq_of_neq_of_beq h' h
rw [getEntry?_cons_of_false h', getEntry?_cons_of_false h₂, ih]
· rw [getEntry?_cons_of_true h', getEntry?_cons_of_true (BEq.trans h h')]
· rw [getEntry?_cons_of_true h', getEntry?_cons_of_true (BEq.trans h' h)]
theorem isEmpty_eq_false_iff_exists_isSome_getEntry? [BEq α] [ReflBEq α] :
{l : List ((a : α) × β a)} l.isEmpty = false a, (getEntry? a l).isSome
@@ -89,18 +89,18 @@ variable {β : Type v}
/-- Internal implementation detail of the hash map -/
def getValue? [BEq α] (a : α) : List ((_ : α) × β) Option β
| [] => none
| k, v :: l => bif a == k then some v else getValue? a l
| k, v :: l => bif k == a then some v else getValue? a l
@[simp] theorem getValue?_nil [BEq α] {a : α} : getValue? a ([] : List ((_ : α) × β)) = none := rfl
theorem getValue?_cons [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} :
getValue? a (k, v :: l) = bif a == k then some v else getValue? a l := rfl
getValue? a (k, v :: l) = bif k == a then some v else getValue? a l := rfl
theorem getValue?_cons_of_true [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : a == k) :
theorem getValue?_cons_of_true [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : k == a) :
getValue? a (k, v :: l) = some v := by
simp [getValue?, h]
theorem getValue?_cons_of_false [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β}
(h : (a == k) = false) : getValue? a (k, v :: l) = getValue? a l := by
(h : (k == a) = false) : getValue? a (k, v :: l) = getValue? a l := by
simp [getValue?, h]
@[simp]
@@ -113,7 +113,7 @@ theorem getValue?_eq_getEntry? [BEq α] {l : List ((_ : α) × β)} {a : α} :
induction l using assoc_induction
· simp
· next k v l ih =>
cases h : a == k
cases h : k == a
· rw [getEntry?_cons_of_false h, getValue?_cons_of_false h, ih]
· rw [getEntry?_cons_of_true h, getValue?_cons_of_true h, Option.map_some']
@@ -130,22 +130,22 @@ end
/-- Internal implementation detail of the hash map -/
def getValueCast? [BEq α] [LawfulBEq α] (a : α) : List ((a : α) × β a) Option (β a)
| [] => none
| k, v :: l => if h : a == k then some (cast (congrArg β (eq_of_beq h).symm) v)
| k, v :: l => if h : k == a then some (cast (congrArg β (eq_of_beq h)) v)
else getValueCast? a l
@[simp] theorem getValueCast?_nil [BEq α] [LawfulBEq α] {a : α} :
getValueCast? a ([] : List ((a : α) × β a)) = none := rfl
theorem getValueCast?_cons [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
getValueCast? a (k, v :: l) = if h : a == k then some (cast (congrArg β (eq_of_beq h).symm) v)
getValueCast? a (k, v :: l) = if h : k == a then some (cast (congrArg β (eq_of_beq h)) v)
else getValueCast? a l := rfl
theorem getValueCast?_cons_of_true [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
{v : β k} (h : a == k) :
getValueCast? a (k, v :: l) = some (cast (congrArg β (eq_of_beq h).symm) v) := by
{v : β k} (h : k == a) :
getValueCast? a (k, v :: l) = some (cast (congrArg β (eq_of_beq h)) v) := by
simp [getValueCast?, h]
theorem getValueCast?_cons_of_false [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
{v : β k} (h : (a == k) = false) : getValueCast? a (k, v :: l) = getValueCast? a l := by
{v : β k} (h : (k == a) = false) : getValueCast? a (k, v :: l) = getValueCast? a l := by
simp [getValueCast?, h]
@[simp]
@@ -187,11 +187,11 @@ end
theorem getValueCast?_eq_getEntry? [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} :
getValueCast? a l = Option.dmap (getEntry? a l)
(fun p h => cast (congrArg β (eq_of_beq (getEntry?_eq_some h)).symm) p.2) := by
(fun p h => cast (congrArg β (eq_of_beq (getEntry?_eq_some h))) p.2) := by
induction l using assoc_induction
· simp
· next k v t ih =>
cases h : a == k
cases h : k == a
· rw [getValueCast?_cons_of_false h, ih, Option.dmap_congr (getEntry?_cons_of_false h)]
· rw [getValueCast?_cons_of_true h, Option.dmap_congr (getEntry?_cons_of_true h),
Option.dmap_some]
@@ -207,23 +207,23 @@ theorem isEmpty_eq_false_iff_exists_isSome_getValueCast? [BEq α] [LawfulBEq α]
/-- Internal implementation detail of the hash map -/
def containsKey [BEq α] (a : α) : List ((a : α) × β a) Bool
| [] => false
| k, _ :: l => a == k || containsKey a l
| k, _ :: l => k == a || containsKey a l
@[simp] theorem containsKey_nil [BEq α] {a : α} :
containsKey a ([] : List ((a : α) × β a)) = false := rfl
@[simp] theorem containsKey_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
containsKey a (k, v :: l) = (a == k || containsKey a l) := rfl
containsKey a (k, v :: l) = (k == a || containsKey a l) := rfl
theorem containsKey_cons_eq_false [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
(containsKey a (k, v :: l) = false) ((a == k) = false) (containsKey a l = false) := by
(containsKey a (k, v :: l) = false) ((k == a) = false) (containsKey a l = false) := by
simp [containsKey_cons, not_or]
theorem containsKey_cons_eq_true [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
(containsKey a (k, v :: l)) (a == k) (containsKey a l) := by
(containsKey a (k, v :: l)) (k == a) (containsKey a l) := by
simp [containsKey_cons]
theorem containsKey_cons_of_beq [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
(h : a == k) : containsKey a (k, v :: l) := containsKey_cons_eq_true.2 <| Or.inl h
(h : k == a) : containsKey a (k, v :: l) := containsKey_cons_eq_true.2 <| Or.inl h
@[simp]
theorem containsKey_cons_self [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
@@ -233,7 +233,7 @@ theorem containsKey_cons_of_containsKey [BEq α] {l : List ((a : α) × β a)} {
(h : containsKey a l) : containsKey a (k, v :: l) := containsKey_cons_eq_true.2 <| Or.inr h
theorem containsKey_of_containsKey_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
(h₁ : containsKey a (k, v :: l)) (h₂ : (a == k) = false) : containsKey a l := by
(h₁ : containsKey a (k, v :: l)) (h₂ : (k == a) = false) : containsKey a l := by
rcases (containsKey_cons_eq_true.1 h₁) with (h|h)
· exact False.elim (Bool.eq_false_iff.1 h₂ h)
· exact h
@@ -243,7 +243,7 @@ theorem containsKey_eq_isSome_getEntry? [BEq α] {l : List ((a : α) × β a)} {
induction l using assoc_induction
· simp
· next k v l ih =>
cases h : a == k
cases h : k == a
· simp [getEntry?_cons_of_false h, h, ih]
· simp [getEntry?_cons_of_true h, h]
@@ -297,7 +297,7 @@ theorem getEntry_eq_of_getEntry?_eq_some [BEq α] {l : List ((a : α) × β a)}
(h : getEntry? a l = some k, v) {h'} : getEntry a l h' = k, v := by
simp [getEntry, h]
theorem getEntry_cons_of_beq [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : a == k) :
theorem getEntry_cons_of_beq [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : k == a) :
getEntry a (k, v :: l) (containsKey_cons_of_beq (v := v) h) = k, v := by
simp [getEntry, getEntry?_cons_of_true h]
@@ -307,7 +307,7 @@ theorem getEntry_cons_self [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {
getEntry_cons_of_beq BEq.refl
theorem getEntry_cons_of_false [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
{h₁ : containsKey a (k, v :: l)} (h₂ : (a == k) = false) : getEntry a (k, v :: l) h₁ =
{h₁ : containsKey a (k, v :: l)} (h₂ : (k == a) = false) : getEntry a (k, v :: l) h₁ =
getEntry a l (containsKey_of_containsKey_cons (v := v) h₁ h₂) := by
simp [getEntry, getEntry?_cons_of_false h₂]
@@ -323,7 +323,7 @@ theorem getValue?_eq_some_getValue [BEq α] {l : List ((_ : α) × β)} {a : α}
getValue? a l = some (getValue a l h) := by
simp [getValue]
theorem getValue_cons_of_beq [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : a == k) :
theorem getValue_cons_of_beq [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : k == a) :
getValue a (k, v :: l) (containsKey_cons_of_beq (k := k) (v := v) h) = v := by
simp [getValue, getValue?_cons_of_true h]
@@ -333,12 +333,12 @@ theorem getValue_cons_self [BEq α] [ReflBEq α] {l : List ((_ : α) × β)} {k
getValue_cons_of_beq BEq.refl
theorem getValue_cons_of_false [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β}
{h₁ : containsKey a (k, v :: l)} (h₂ : (a == k) = false) : getValue a (k, v :: l) h₁ =
{h₁ : containsKey a (k, v :: l)} (h₂ : (k == a) = false) : getValue a (k, v :: l) h₁ =
getValue a l (containsKey_of_containsKey_cons (k := k) (v := v) h₁ h₂) := by
simp [getValue, getValue?_cons_of_false h₂]
theorem getValue_cons [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} {h} :
getValue a (k, v :: l) h = if h' : a == k then v
getValue a (k, v :: l) h = if h' : k == a then v
else getValue a l (containsKey_of_containsKey_cons (k := k) h (Bool.eq_false_iff.2 h')) := by
rw [ Option.some_inj, getValue?_eq_some_getValue, getValue?_cons, apply_dite Option.some,
cond_eq_if]
@@ -369,8 +369,8 @@ theorem Option.get_congr {o o' : Option α} {ho : o.isSome} (h : o = o') :
theorem getValueCast_cons [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
(h : containsKey a (k, v :: l)) :
getValueCast a (k, v :: l) h =
if h' : a == k then
cast (congrArg β (eq_of_beq h').symm) v
if h' : k == a then
cast (congrArg β (eq_of_beq h')) v
else
getValueCast a l (containsKey_of_containsKey_cons (k := k) h (Bool.eq_false_iff.2 h')) := by
rw [getValueCast, Option.get_congr getValueCast?_cons]
@@ -515,19 +515,19 @@ end
/-- Internal implementation detail of the hash map -/
def replaceEntry [BEq α] (k : α) (v : β k) : List ((a : α) × β a) List ((a : α) × β a)
| [] => []
| k', v' :: l => bif k == k' then k, v :: l else k', v' :: replaceEntry k v l
| k', v' :: l => bif k' == k then k, v :: l else k', v' :: replaceEntry k v l
@[simp] theorem replaceEntry_nil [BEq α] {k : α} {v : β k} : replaceEntry k v [] = [] := rfl
theorem replaceEntry_cons [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k} {v' : β k'} :
replaceEntry k v (k', v' :: l) =
bif k == k' then k, v :: l else k', v' :: replaceEntry k v l := rfl
bif k' == k then k, v :: l else k', v' :: replaceEntry k v l := rfl
theorem replaceEntry_cons_of_true [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k}
{v' : β k'} (h : k == k') : replaceEntry k v (k', v' :: l) = k, v :: l := by
{v' : β k'} (h : k' == k) : replaceEntry k v (k', v' :: l) = k, v :: l := by
simp [replaceEntry, h]
theorem replaceEntry_cons_of_false [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k}
{v' : β k'} (h : (k == k') = false) :
{v' : β k'} (h : (k' == k) = false) :
replaceEntry k v (k', v' :: l) = k', v' :: replaceEntry k v l := by
simp [replaceEntry, h]
@@ -553,37 +553,37 @@ theorem getEntry?_replaceEntry_of_containsKey_eq_false [BEq α] {l : List ((a :
rw [replaceEntry_of_containsKey_eq_false hl]
theorem getEntry?_replaceEntry_of_false [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
{a k : α} {v : β k} (h : (a == k) = false) :
{a k : α} {v : β k} (h : (k == a) = false) :
getEntry? a (replaceEntry k v l) = getEntry? a l := by
induction l using assoc_induction
· simp
· next k' v' l ih =>
cases h' : k == k'
cases h' : k' == k
· rw [replaceEntry_cons_of_false h', getEntry?_cons, getEntry?_cons, ih]
· rw [replaceEntry_cons_of_true h']
have hk : (a == k') = false := BEq.neq_of_neq_of_beq h h'
have hk : (k' == a) = false := BEq.neq_of_beq_of_neq h' h
simp [getEntry?_cons_of_false h, getEntry?_cons_of_false hk]
theorem getEntry?_replaceEntry_of_true [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
{a k : α} {v : β k} (hl : containsKey k l = true) (h : a == k) :
{a k : α} {v : β k} (hl : containsKey k l = true) (h : k == a) :
getEntry? a (replaceEntry k v l) = some k, v := by
induction l using assoc_induction
· simp at hl
· next k' v' l ih =>
cases hk'a : k == k'
cases hk'a : k' == k
· rw [replaceEntry_cons_of_false hk'a]
have hk'k : (a == k') = false := BEq.neq_of_beq_of_neq h hk'a
have hk'k : (k' == a) = false := BEq.neq_of_neq_of_beq hk'a h
rw [getEntry?_cons_of_false hk'k]
exact ih (containsKey_of_containsKey_cons hl hk'a)
· rw [replaceEntry_cons_of_true hk'a, getEntry?_cons_of_true h]
theorem getEntry?_replaceEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α}
{v : β k} :
getEntry? a (replaceEntry k v l) = bif containsKey k l && a == k then some k, v else
getEntry? a (replaceEntry k v l) = bif containsKey k l && k == a then some k, v else
getEntry? a l := by
cases hl : containsKey k l
· simp [getEntry?_replaceEntry_of_containsKey_eq_false hl]
· cases h : a == k
· cases h : k == a
· simp [getEntry?_replaceEntry_of_false h]
· simp [getEntry?_replaceEntry_of_true hl h]
@@ -601,12 +601,12 @@ theorem getValue?_replaceEntry_of_containsKey_eq_false [BEq α] {l : List ((_ :
simp [getValue?_eq_getEntry?, getEntry?_replaceEntry_of_containsKey_eq_false hl]
theorem getValue?_replaceEntry_of_false [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
{k a : α} {v : β} (h : (a == k) = false) :
{k a : α} {v : β} (h : (k == a) = false) :
getValue? a (replaceEntry k v l) = getValue? a l := by
simp [getValue?_eq_getEntry?, getEntry?_replaceEntry_of_false h]
theorem getValue?_replaceEntry_of_true [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
{k a : α} {v : β} (hl : containsKey k l = true) (h : a == k) :
{k a : α} {v : β} (hl : containsKey k l = true) (h : k == a) :
getValue? a (replaceEntry k v l) = some v := by
simp [getValue?_eq_getEntry?, getEntry?_replaceEntry_of_true hl h]
@@ -614,7 +614,7 @@ end
theorem getValueCast?_replaceEntry [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a k : α}
{v : β k} : getValueCast? a (replaceEntry k v l) =
if h : containsKey k l a == k then some (cast (congrArg β (eq_of_beq h.2).symm) v)
if h : containsKey k l k == a then some (cast (congrArg β (eq_of_beq h.2)) v)
else getValueCast? a l := by
rw [getValueCast?_eq_getEntry?]
split
@@ -632,25 +632,25 @@ theorem getValueCast?_replaceEntry [BEq α] [LawfulBEq α] {l : List ((a : α)
@[simp]
theorem containsKey_replaceEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α}
{v : β k} : containsKey a (replaceEntry k v l) = containsKey a l := by
cases h : containsKey k l && a == k
cases h : containsKey k l && k == a
· rw [containsKey_eq_isSome_getEntry?, getEntry?_replaceEntry, h, cond_false,
containsKey_eq_isSome_getEntry?]
· rw [containsKey_eq_isSome_getEntry?, getEntry?_replaceEntry, h, cond_true, Option.isSome_some,
Eq.comm]
rw [Bool.and_eq_true] at h
exact containsKey_of_beq h.1 (BEq.symm h.2)
exact containsKey_of_beq h.1 h.2
/-- Internal implementation detail of the hash map -/
def eraseKey [BEq α] (k : α) : List ((a : α) × β a) List ((a : α) × β a)
| [] => []
| k', v' :: l => bif k == k' then l else k', v' :: eraseKey k l
| k', v' :: l => bif k' == k then l else k', v' :: eraseKey k l
@[simp] theorem eraseKey_nil [BEq α] {k : α} : eraseKey k ([] : List ((a : α) × β a)) = [] := rfl
theorem eraseKey_cons [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v' : β k'} :
eraseKey k (k', v' :: l) = bif k == k' then l else k', v' :: eraseKey k l := rfl
eraseKey k (k', v' :: l) = bif k' == k then l else k', v' :: eraseKey k l := rfl
theorem eraseKey_cons_of_beq [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v' : β k'}
(h : k == k') : eraseKey k (k', v' :: l) = l :=
(h : k' == k) : eraseKey k (k', v' :: l) = l :=
by simp [eraseKey_cons, h]
@[simp]
@@ -659,7 +659,7 @@ theorem eraseKey_cons_self [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {
eraseKey_cons_of_beq BEq.refl
theorem eraseKey_cons_of_false [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v' : β k'}
(h : (k == k') = false) : eraseKey k (k', v' :: l) = k', v' :: eraseKey k l := by
(h : (k' == k) = false) : eraseKey k (k', v' :: l) = k', v' :: eraseKey k l := by
simp [eraseKey_cons, h]
theorem eraseKey_of_containsKey_eq_false [BEq α] {l : List ((a : α) × β a)} {k : α}
@@ -676,7 +676,7 @@ theorem sublist_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} :
· simp
· next k' v' t ih =>
rw [eraseKey_cons]
cases k == k'
cases k' == k
· simpa
· simpa using Sublist.cons_right Sublist.refl
@@ -686,7 +686,7 @@ theorem length_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} :
· simp
· next k' v' t ih =>
rw [eraseKey_cons, containsKey_cons]
cases k == k'
cases k' == k
· rw [cond_false, Bool.false_or, List.length_cons, ih]
cases h : containsKey k t
· simp
@@ -722,7 +722,7 @@ theorem containsKey_eq_keys_contains [BEq α] [PartialEquivBEq α] {l : List ((a
· next k _ l ih => simp [ih, BEq.comm]
theorem containsKey_eq_true_iff_exists_mem [BEq α] {l : List ((a : α) × β a)} {a : α} :
containsKey a l = true p l, a == p.1 := by
containsKey a l = true p l, p.1 == a := by
induction l using assoc_induction <;> simp_all
theorem containsKey_of_mem [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {p : (a : α) × β a}
@@ -798,11 +798,11 @@ theorem mem_iff_getEntry?_eq_some [BEq α] [EquivBEq α] {l : List ((a : α) ×
refine ?_, ?_
· rintro (rfl|hk)
· simp
· suffices (p.fst == k) = false by simp_all
· suffices (k == p.fst) = false by simp_all
refine Bool.eq_false_iff.2 fun hcon => Bool.false_ne_true ?_
rw [ h.containsKey_eq_false, containsKey_congr (BEq.symm hcon),
rw [ h.containsKey_eq_false, containsKey_congr hcon,
containsKey_eq_isSome_getEntry?, hk, Option.isSome_some]
· cases p.fst == k
· cases k == p.fst
· rw [cond_false]
exact Or.inr
· rw [cond_true, Option.some.injEq]
@@ -814,7 +814,7 @@ theorem DistinctKeys.replaceEntry [BEq α] [PartialEquivBEq α] {l : List ((a :
· simp
· next k' v' l ih =>
rw [distinctKeys_cons_iff] at h
cases hk'k : k == k'
cases hk'k : k' == k
· rw [replaceEntry_cons_of_false hk'k, distinctKeys_cons_iff]
refine ih h.1, ?_
simpa using h.2
@@ -870,7 +870,7 @@ section
variable {β : Type v}
theorem getValue?_insertEntry_of_beq [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α}
{v : β} (h : a == k) : getValue? a (insertEntry k v l) = some v := by
{v : β} (h : k == a) : getValue? a (insertEntry k v l) = some v := by
cases h' : containsKey k l
· rw [insertEntry_of_containsKey_eq_false h', getValue?_cons_of_true h]
· rw [insertEntry_of_containsKey h', getValue?_replaceEntry_of_true h' h]
@@ -880,14 +880,14 @@ theorem getValue?_insertEntry_of_self [BEq α] [EquivBEq α] {l : List ((_ : α)
getValue?_insertEntry_of_beq BEq.refl
theorem getValue?_insertEntry_of_false [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
{k a : α} {v : β} (h : (a == k) = false) : getValue? a (insertEntry k v l) = getValue? a l := by
{k a : α} {v : β} (h : (k == a) = false) : getValue? a (insertEntry k v l) = getValue? a l := by
cases h' : containsKey k l
· rw [insertEntry_of_containsKey_eq_false h', getValue?_cons_of_false h]
· rw [insertEntry_of_containsKey h', getValue?_replaceEntry_of_false h]
theorem getValue?_insertEntry [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α}
{v : β} : getValue? a (insertEntry k v l) = bif a == k then some v else getValue? a l := by
cases h : a == k
{v : β} : getValue? a (insertEntry k v l) = bif k == a then some v else getValue? a l := by
cases h : k == a
· simp [getValue?_insertEntry_of_false h, h]
· simp [getValue?_insertEntry_of_beq h, h]
@@ -899,14 +899,14 @@ end
theorem getEntry?_insertEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
{v : β k} :
getEntry? a (insertEntry k v l) = bif a == k then some k, v else getEntry? a l := by
getEntry? a (insertEntry k v l) = bif k == a then some k, v else getEntry? a l := by
cases hl : containsKey k l
· rw [insertEntry_of_containsKey_eq_false hl, getEntry?_cons]
· rw [insertEntry_of_containsKey hl, getEntry?_replaceEntry, hl, Bool.true_and, BEq.comm]
theorem getValueCast?_insertEntry [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
{v : β k} : getValueCast? a (insertEntry k v l) =
if h : a == k then some (cast (congrArg β (eq_of_beq h).symm) v) else getValueCast? a l := by
if h : k == a then some (cast (congrArg β (eq_of_beq h)) v) else getValueCast? a l := by
cases hl : containsKey k l
· rw [insertEntry_of_containsKey_eq_false hl, getValueCast?_cons]
· rw [insertEntry_of_containsKey hl, getValueCast?_replaceEntry, hl]
@@ -918,7 +918,7 @@ theorem getValueCast?_insertEntry_self [BEq α] [LawfulBEq α] {l : List ((a :
theorem getValueCast!_insertEntry [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
[Inhabited (β a)] {v : β k} : getValueCast! a (insertEntry k v l) =
if h : a == k then cast (congrArg β (eq_of_beq h).symm) v else getValueCast! a l := by
if h : k == a then cast (congrArg β (eq_of_beq h)) v else getValueCast! a l := by
simp [getValueCast!_eq_getValueCast?, getValueCast?_insertEntry, apply_dite Option.get!]
theorem getValueCast!_insertEntry_self [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α}
@@ -927,7 +927,7 @@ theorem getValueCast!_insertEntry_self [BEq α] [LawfulBEq α] {l : List ((a :
theorem getValueCastD_insertEntry [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
{fallback : β a} {v : β k} : getValueCastD a (insertEntry k v l) fallback =
if h : a == k then cast (congrArg β (eq_of_beq h).symm) v
if h : k == a then cast (congrArg β (eq_of_beq h)) v
else getValueCastD a l fallback := by
simp [getValueCastD_eq_getValueCast?, getValueCast?_insertEntry,
apply_dite (fun x => Option.getD x fallback)]
@@ -938,7 +938,7 @@ theorem getValueCastD_insertEntry_self [BEq α] [LawfulBEq α] {l : List ((a :
theorem getValue!_insertEntry {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β]
{l : List ((_ : α) × β)} {k a : α} {v : β} :
getValue! a (insertEntry k v l) = bif a == k then v else getValue! a l := by
getValue! a (insertEntry k v l) = bif k == a then v else getValue! a l := by
simp [getValue!_eq_getValue?, getValue?_insertEntry, Bool.apply_cond Option.get!]
theorem getValue!_insertEntry_self {β : Type v} [BEq α] [EquivBEq α] [Inhabited β]
@@ -947,7 +947,7 @@ theorem getValue!_insertEntry_self {β : Type v} [BEq α] [EquivBEq α] [Inhabit
theorem getValueD_insertEntry {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
{k a : α} {fallback v : β} : getValueD a (insertEntry k v l) fallback =
bif a == k then v else getValueD a l fallback := by
bif k == a then v else getValueD a l fallback := by
simp [getValueD_eq_getValue?, getValue?_insertEntry, Bool.apply_cond (fun x => Option.getD x fallback)]
theorem getValueD_insertEntry_self {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)}
@@ -956,12 +956,12 @@ theorem getValueD_insertEntry_self {β : Type v} [BEq α] [EquivBEq α] {l : Lis
@[simp]
theorem containsKey_insertEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
{v : β k} : containsKey a (insertEntry k v l) = ((a == k) || containsKey a l) := by
{v : β k} : containsKey a (insertEntry k v l) = ((k == a) || containsKey a l) := by
rw [containsKey_eq_isSome_getEntry?, containsKey_eq_isSome_getEntry?, getEntry?_insertEntry]
cases a == k <;> simp
cases k == a <;> simp
theorem containsKey_insertEntry_of_beq [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
{k a : α} {v : β k} (h : a == k) : containsKey a (insertEntry k v l) := by
{k a : α} {v : β k} (h : k == a) : containsKey a (insertEntry k v l) := by
simp [h]
@[simp]
@@ -971,12 +971,12 @@ theorem containsKey_insertEntry_self [BEq α] [EquivBEq α] {l : List ((a : α)
theorem containsKey_of_containsKey_insertEntry [BEq α] [PartialEquivBEq α]
{l : List ((a : α) × β a)} {k a : α} {v : β k} (h₁ : containsKey a (insertEntry k v l))
(h₂ : (a == k) = false) : containsKey a l := by
(h₂ : (k == a) = false) : containsKey a l := by
rwa [containsKey_insertEntry, h₂, Bool.false_or] at h₁
theorem getValueCast_insertEntry [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
{v : β k} {h} : getValueCast a (insertEntry k v l) h =
if h' : a == k then cast (congrArg β (eq_of_beq h').symm) v
if h' : k == a then cast (congrArg β (eq_of_beq h')) v
else getValueCast a l (containsKey_of_containsKey_insertEntry h (Bool.eq_false_iff.2 h')) := by
rw [ Option.some_inj, getValueCast?_eq_some_getValueCast, apply_dite Option.some,
getValueCast?_insertEntry]
@@ -988,7 +988,7 @@ theorem getValueCast_insertEntry_self [BEq α] [LawfulBEq α] {l : List ((a : α
theorem getValue_insertEntry {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
{k a : α} {v : β} {h} : getValue a (insertEntry k v l) h =
if h' : a == k then v
if h' : k == a then v
else getValue a l (containsKey_of_containsKey_insertEntry h (Bool.eq_false_iff.2 h')) := by
rw [ Option.some_inj, getValue?_eq_some_getValue, apply_dite Option.some,
getValue?_insertEntry, cond_eq_if, dite_eq_ite]
@@ -1020,14 +1020,14 @@ theorem isEmpty_insertEntryIfNew [BEq α] {l : List ((a : α) × β a)} {k : α}
theorem getEntry?_insertEntryIfNew [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
{v : β k} : getEntry? a (insertEntryIfNew k v l) =
bif a == k && !containsKey k l then some k, v else getEntry? a l := by
bif k == a && !containsKey k l then some k, v else getEntry? a l := by
cases h : containsKey k l
· simp [insertEntryIfNew_of_containsKey_eq_false h, getEntry?_cons]
· simp [insertEntryIfNew_of_containsKey h]
theorem getValueCast?_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
{v : β k} : getValueCast? a (insertEntryIfNew k v l) =
if h : a == k containsKey k l = false then some (cast (congrArg β (eq_of_beq h.1).symm) v)
if h : k == a containsKey k l = false then some (cast (congrArg β (eq_of_beq h.1)) v)
else getValueCast? a l := by
cases h : containsKey k l
· rw [insertEntryIfNew_of_containsKey_eq_false h, getValueCast?_cons]
@@ -1036,16 +1036,16 @@ theorem getValueCast?_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a :
theorem getValue?_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
{k a : α} {v : β} : getValue? a (insertEntryIfNew k v l) =
bif a == k && !containsKey k l then some v else getValue? a l := by
bif k == a && !containsKey k l then some v else getValue? a l := by
simp [getValue?_eq_getEntry?, getEntry?_insertEntryIfNew,
Bool.apply_cond (Option.map (fun (y : ((_ : α) × β)) => y.2))]
theorem containsKey_insertEntryIfNew [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
{k a : α} {v : β k} :
containsKey a (insertEntryIfNew k v l) = ((a == k) || containsKey a l) := by
containsKey a (insertEntryIfNew k v l) = ((k == a) || containsKey a l) := by
simp only [containsKey_eq_isSome_getEntry?, getEntry?_insertEntryIfNew, Bool.apply_cond Option.isSome,
Option.isSome_some, Bool.cond_true_left]
cases h : a == k
cases h : k == a
· simp
· rw [Bool.true_and, Bool.true_or, getEntry?_congr h, Bool.not_or_self]
@@ -1055,7 +1055,7 @@ theorem containsKey_insertEntryIfNew_self [BEq α] [EquivBEq α] {l : List ((a :
theorem containsKey_of_containsKey_insertEntryIfNew [BEq α] [PartialEquivBEq α]
{l : List ((a : α) × β a)} {k a : α} {v : β k} (h₁ : containsKey a (insertEntryIfNew k v l))
(h₂ : (a == k) = false) : containsKey a l := by
(h₂ : (k == a) = false) : containsKey a l := by
rwa [containsKey_insertEntryIfNew, h₂, Bool.false_or] at h₁
/--
@@ -1064,7 +1064,7 @@ obligation in the statement of `getValueCast_insertEntryIfNew`.
-/
theorem containsKey_of_containsKey_insertEntryIfNew' [BEq α] [PartialEquivBEq α]
{l : List ((a : α) × β a)} {k a : α} {v : β k} (h₁ : containsKey a (insertEntryIfNew k v l))
(h₂ : ¬((a == k) containsKey k l = false)) : containsKey a l := by
(h₂ : ¬((k == a) containsKey k l = false)) : containsKey a l := by
rw [Decidable.not_and_iff_or_not, Bool.not_eq_true, Bool.not_eq_false] at h₂
rcases h₂ with h₂|h₂
· rwa [containsKey_insertEntryIfNew, h₂, Bool.false_or] at h₁
@@ -1072,8 +1072,8 @@ theorem containsKey_of_containsKey_insertEntryIfNew' [BEq α] [PartialEquivBEq
theorem getValueCast_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
{v : β k} {h} : getValueCast a (insertEntryIfNew k v l) h =
if h' : a == k containsKey k l = false then
cast (congrArg β (eq_of_beq h'.1).symm) v
if h' : k == a containsKey k l = false then
cast (congrArg β (eq_of_beq h'.1)) v
else
getValueCast a l (containsKey_of_containsKey_insertEntryIfNew' h h') := by
rw [ Option.some_inj, getValueCast?_eq_some_getValueCast, apply_dite Option.some,
@@ -1082,7 +1082,7 @@ theorem getValueCast_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : α
theorem getValue_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
{k a : α} {v : β} {h} : getValue a (insertEntryIfNew k v l) h =
if h' : a == k containsKey k l = false then v
if h' : k == a containsKey k l = false then v
else getValue a l (containsKey_of_containsKey_insertEntryIfNew' h h') := by
rw [ Option.some_inj, getValue?_eq_some_getValue, apply_dite Option.some,
getValue?_insertEntryIfNew, cond_eq_if, dite_eq_ite]
@@ -1090,25 +1090,25 @@ theorem getValue_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] {l
theorem getValueCast!_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
{v : β k} [Inhabited (β a)] : getValueCast! a (insertEntryIfNew k v l) =
if h : a == k containsKey k l = false then cast (congrArg β (eq_of_beq h.1).symm) v
if h : k == a containsKey k l = false then cast (congrArg β (eq_of_beq h.1)) v
else getValueCast! a l := by
simp [getValueCast!_eq_getValueCast?, getValueCast?_insertEntryIfNew, apply_dite Option.get!]
theorem getValue!_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β]
{l : List ((_ : α) × β)} {k a : α} {v : β} : getValue! a (insertEntryIfNew k v l) =
bif a == k && !containsKey k l then v else getValue! a l := by
bif k == a && !containsKey k l then v else getValue! a l := by
simp [getValue!_eq_getValue?, getValue?_insertEntryIfNew, Bool.apply_cond Option.get!]
theorem getValueCastD_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
{v : β k} {fallback : β a} : getValueCastD a (insertEntryIfNew k v l) fallback =
if h : a == k containsKey k l = false then cast (congrArg β (eq_of_beq h.1).symm) v
if h : k == a containsKey k l = false then cast (congrArg β (eq_of_beq h.1)) v
else getValueCastD a l fallback := by
simp [getValueCastD_eq_getValueCast?, getValueCast?_insertEntryIfNew,
apply_dite (fun x => Option.getD x fallback)]
theorem getValueD_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
{k a : α} {fallback v : β} : getValueD a (insertEntryIfNew k v l) fallback =
bif a == k && !containsKey k l then v else getValueD a l fallback := by
bif k == a && !containsKey k l then v else getValueD a l fallback := by
simp [getValueD_eq_getValue?, getValue?_insertEntryIfNew,
Bool.apply_cond (fun x => Option.getD x fallback)]
@@ -1131,7 +1131,7 @@ theorem keys_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)
· next k' v' l ih =>
simp only [eraseKey_cons, keys_cons, List.erase_cons]
rw [BEq.comm]
cases k' == k <;> simp [ih]
cases k == k' <;> simp [ih]
theorem DistinctKeys.eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} :
DistinctKeys l DistinctKeys (eraseKey k l) := by
@@ -1142,35 +1142,35 @@ theorem getEntry?_eraseKey_self [BEq α] [PartialEquivBEq α] {l : List ((a : α
induction l using assoc_induction
· simp
· next k' v' t ih =>
cases h' : k == k'
cases h' : k' == k
· rw [eraseKey_cons_of_false h', getEntry?_cons_of_false h']
exact ih h.tail
· rw [eraseKey_cons_of_beq h', Option.not_isSome_iff_eq_none, Bool.not_eq_true,
containsKey_eq_isSome_getEntry?, containsKey_congr (BEq.symm h')]
containsKey_eq_isSome_getEntry?, containsKey_congr h']
exact h.containsKey_eq_false
theorem getEntry?_eraseKey_of_beq [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
(hl : DistinctKeys l) (hka : a == k) : getEntry? a (eraseKey k l) = none := by
rw [ getEntry?_congr (BEq.symm hka), getEntry?_eraseKey_self hl]
(hl : DistinctKeys l) (hka : k == a) : getEntry? a (eraseKey k l) = none := by
rw [ getEntry?_congr hka, getEntry?_eraseKey_self hl]
theorem getEntry?_eraseKey_of_false [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
{k a : α} (hka : (a == k) = false) : getEntry? a (eraseKey k l) = getEntry? a l := by
{k a : α} (hka : (k == a) = false) : getEntry? a (eraseKey k l) = getEntry? a l := by
induction l using assoc_induction
· simp
· next k' v' t ih =>
cases h' : k == k'
cases h' : k' == k
· rw [eraseKey_cons_of_false h']
cases h'' : a == k'
cases h'' : k' == a
· rw [getEntry?_cons_of_false h'', ih, getEntry?_cons_of_false h'']
· rw [getEntry?_cons_of_true h'', getEntry?_cons_of_true h'']
· rw [eraseKey_cons_of_beq h']
have hx : (a == k') = false := BEq.neq_of_neq_of_beq hka h'
have hx : (k' == a) = false := BEq.neq_of_beq_of_neq h' hka
rw [getEntry?_cons_of_false hx]
theorem getEntry?_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
(hl : DistinctKeys l) :
getEntry? a (eraseKey k l) = bif a == k then none else getEntry? a l := by
cases h : a == k
getEntry? a (eraseKey k l) = bif k == a then none else getEntry? a l := by
cases h : k == a
· simp [getEntry?_eraseKey_of_false h, h]
· simp [getEntry?_eraseKey_of_beq hl h, h]
@@ -1213,16 +1213,16 @@ theorem getValue?_eraseKey_self [BEq α] [PartialEquivBEq α] {l : List ((_ : α
simp [getValue?_eq_getEntry?, getEntry?_eraseKey_self h]
theorem getValue?_eraseKey_of_beq [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α}
(hl : DistinctKeys l) (hka : a == k) : getValue? a (eraseKey k l) = none := by
(hl : DistinctKeys l) (hka : k == a) : getValue? a (eraseKey k l) = none := by
simp [getValue?_eq_getEntry?, getEntry?_eraseKey_of_beq hl hka]
theorem getValue?_eraseKey_of_false [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α}
(hka : (a == k) = false) : getValue? a (eraseKey k l) = getValue? a l := by
(hka : (k == a) = false) : getValue? a (eraseKey k l) = getValue? a l := by
simp [getValue?_eq_getEntry?, getEntry?_eraseKey_of_false hka]
theorem getValue?_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α}
(hl : DistinctKeys l) :
getValue? a (eraseKey k l) = bif a == k then none else getValue? a l := by
getValue? a (eraseKey k l) = bif k == a then none else getValue? a l := by
simp [getValue?_eq_getEntry?, getEntry?_eraseKey hl, Bool.apply_cond (Option.map _)]
end
@@ -1236,18 +1236,18 @@ theorem containsKey_eraseKey_of_beq [BEq α] [PartialEquivBEq α] {l : List ((a
rw [containsKey_congr hka, containsKey_eraseKey_self hl]
theorem containsKey_eraseKey_of_false [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
{k a : α} (hka : (a == k) = false) : containsKey a (eraseKey k l) = containsKey a l := by
{k a : α} (hka : (k == a) = false) : containsKey a (eraseKey k l) = containsKey a l := by
simp [containsKey_eq_isSome_getEntry?, getEntry?_eraseKey_of_false hka]
theorem containsKey_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
(hl : DistinctKeys l) : containsKey a (eraseKey k l) = (!(a == k) && containsKey a l) := by
(hl : DistinctKeys l) : containsKey a (eraseKey k l) = (!(k == a) && containsKey a l) := by
simp [containsKey_eq_isSome_getEntry?, getEntry?_eraseKey hl, Bool.apply_cond]
theorem getValueCast?_eraseKey [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
(hl : DistinctKeys l) :
getValueCast? a (eraseKey k l) = bif a == k then none else getValueCast? a l := by
getValueCast? a (eraseKey k l) = bif k == a then none else getValueCast? a l := by
rw [getValueCast?_eq_getEntry?, Option.dmap_congr (getEntry?_eraseKey hl)]
rcases Bool.eq_false_or_eq_true (a == k) with h|h
rcases Bool.eq_false_or_eq_true (k == a) with h|h
· rw [Option.dmap_congr (Bool.cond_pos h), Option.dmap_none, Bool.cond_pos h]
· rw [Option.dmap_congr (Bool.cond_neg h), getValueCast?_eq_getEntry?]
exact (Bool.cond_neg h).symm
@@ -1258,7 +1258,7 @@ theorem getValueCast?_eraseKey_self [BEq α] [LawfulBEq α] {l : List ((a : α)
theorem getValueCast!_eraseKey [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
[Inhabited (β a)] (hl : DistinctKeys l) :
getValueCast! a (eraseKey k l) = bif a == k then default else getValueCast! a l := by
getValueCast! a (eraseKey k l) = bif k == a then default else getValueCast! a l := by
simp [getValueCast!_eq_getValueCast?, getValueCast?_eraseKey hl, Bool.apply_cond Option.get!]
theorem getValueCast!_eraseKey_self [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α}
@@ -1267,7 +1267,7 @@ theorem getValueCast!_eraseKey_self [BEq α] [LawfulBEq α] {l : List ((a : α)
theorem getValueCastD_eraseKey [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
{fallback : β a} (hl : DistinctKeys l) : getValueCastD a (eraseKey k l) fallback =
bif a == k then fallback else getValueCastD a l fallback := by
bif k == a then fallback else getValueCastD a l fallback := by
simp [getValueCastD_eq_getValueCast?, getValueCast?_eraseKey hl,
Bool.apply_cond (fun x => Option.getD x fallback)]
@@ -1278,7 +1278,7 @@ theorem getValueCastD_eraseKey_self [BEq α] [LawfulBEq α] {l : List ((a : α)
theorem getValue!_eraseKey {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β]
{l : List ((_ : α) × β)} {k a : α} (hl : DistinctKeys l) :
getValue! a (eraseKey k l) = bif a == k then default else getValue! a l := by
getValue! a (eraseKey k l) = bif k == a then default else getValue! a l := by
simp [getValue!_eq_getValue?, getValue?_eraseKey hl, Bool.apply_cond Option.get!]
theorem getValue!_eraseKey_self {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β]
@@ -1288,7 +1288,7 @@ theorem getValue!_eraseKey_self {β : Type v} [BEq α] [PartialEquivBEq α] [Inh
theorem getValueD_eraseKey {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
{k a : α} {fallback : β} (hl : DistinctKeys l) : getValueD a (eraseKey k l) fallback =
bif a == k then fallback else getValueD a l fallback := by
bif k == a then fallback else getValueD a l fallback := by
simp [getValueD_eq_getValue?, getValue?_eraseKey hl, Bool.apply_cond (fun x => Option.getD x fallback)]
theorem getValueD_eraseKey_self {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
@@ -1325,9 +1325,9 @@ theorem getEntry?_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α)
rcases p with k₁, v₁
rcases p' with k₂, v₂
simp only [getEntry?_cons]
cases h₂ : a == k₂ <;> cases h₁ : a == k₁ <;> try simp; done
cases h₂ : k₂ == a <;> cases h₁ : k₁ == a <;> try simp; done
simp only [distinctKeys_cons_iff, containsKey_cons, Bool.or_eq_false_iff] at hl
exact ((Bool.eq_false_iff.1 hl.2.1).elim (BEq.trans (BEq.symm h₁) h₂)).elim
exact ((Bool.eq_false_iff.1 hl.2.1).elim (BEq.trans h₂ (BEq.symm h₁))).elim
· next l₁ l₂ l₃ hl₁₂ _ ih₁ ih₂ => exact (ih₁ hl).trans (ih₂ (hl.perm (hl₁₂.symm)))
theorem containsKey_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {k : α}
@@ -1392,7 +1392,7 @@ theorem perm_cons_getEntry [BEq α] {l : List ((a : α) × β a)} {a : α} (h :
· simp at h
· next k' v' t ih =>
simp only [containsKey_cons, Bool.or_eq_true] at h
cases hk : a == k'
cases hk : k' == a
· obtain l', hl' := ih (h.resolve_left (Bool.not_eq_true _ hk))
rw [getEntry_cons_of_false hk]
exact k', v' :: l', (hl'.cons _).trans (Perm.swap _ _ (Perm.refl _))
@@ -1414,9 +1414,9 @@ theorem getEntry?_ext [BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)} (h
suffices Perm t l'' from (this.cons _).trans hl''.symm
apply ih hl.tail (hl'.perm hl''.symm).tail
intro k'
cases hk' : k' == k
cases hk' : k == k'
· simpa only [getEntry?_of_perm hl' hl'', getEntry?_cons_of_false hk'] using h k'
· rw [getEntry?_congr hk', getEntry?_congr hk', getEntry?_eq_none.2 hl.containsKey_eq_false,
· rw [ getEntry?_congr hk', getEntry?_congr hk', getEntry?_eq_none.2 hl.containsKey_eq_false,
getEntry?_eq_none.2 (hl'.perm hl''.symm).containsKey_eq_false]
theorem replaceEntry_of_perm [BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)} {k : α} {v : β k}
@@ -1439,7 +1439,7 @@ theorem getEntry?_append [BEq α] {l l' : List ((a : α) × β a)} {a : α} :
getEntry? a (l ++ l') = (getEntry? a l).or (getEntry? a l') := by
induction l using assoc_induction
· simp
· next k' v' t ih => cases h : a == k' <;> simp_all [getEntry?_cons]
· next k' v' t ih => cases h : k' == a <;> simp_all [getEntry?_cons]
theorem getEntry?_append_of_containsKey_eq_false [BEq α] {l l' : List ((a : α) × β a)} {a : α}
(h : containsKey a l' = false) : getEntry? a (l ++ l') = getEntry? a l := by
@@ -1501,7 +1501,7 @@ theorem replaceEntry_append_of_containsKey_left [BEq α] {l l' : List ((a : α)
· simp at h
· next k' v' t ih =>
simp only [containsKey_cons, Bool.or_eq_true] at h
cases h' : k == k'
cases h' : k' == k
· simpa [replaceEntry_cons, h'] using ih (h.resolve_left (Bool.not_eq_true _ h'))
· simp [replaceEntry_cons, h']
@@ -1535,7 +1535,7 @@ theorem eraseKey_append_of_containsKey_right_eq_false [BEq α] {l l' : List ((a
· simp [eraseKey_of_containsKey_eq_false h]
· next k' v' t ih =>
rw [List.cons_append, eraseKey_cons, eraseKey_cons]
cases k == k'
cases k' == k
· rw [cond_false, cond_false, ih, List.cons_append]
· rw [cond_true, cond_true]

View File

@@ -241,7 +241,7 @@ theorem updateAllBuckets [BEq α] [Hashable α] [LawfulHashable α] {m : Array (
simp only [Array.getElem_map, Array.size_map]
refine fun h p hp => ?_
rcases containsKey_eq_true_iff_exists_mem.1 (hf _ _ hp) with q, hq₁, hq₂
rw [hash_eq hq₂, (hm.hashes_to _ _).hash_self _ _ hq₁]
rw [ hash_eq hq₂, (hm.hashes_to _ _).hash_self _ _ hq₁]
end IsHashSelf

View File

@@ -127,11 +127,11 @@ theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashab
simp_to_model using List.isEmpty_eq_false_iff_exists_containsKey
theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
(m.insert k v).contains a = ((a == k) || m.contains a) := by
(m.insert k v).contains a = ((k == a) || m.contains a) := by
simp_to_model using List.containsKey_insertEntry
theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
(m.insert k v).contains a (a == k) = false m.contains a := by
(m.insert k v).contains a (k == a) = false m.contains a := by
simp_to_model using List.containsKey_of_containsKey_insertEntry
theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@@ -161,7 +161,7 @@ theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} :
simp_to_model using List.isEmpty_eraseKey
theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k).contains a = (!(a == k) && m.contains a) := by
(m.erase k).contains a = (!(k == a) && m.contains a) := by
simp_to_model using List.containsKey_eraseKey
theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
@@ -202,7 +202,7 @@ theorem get?_of_isEmpty [LawfulBEq α] {a : α} : m.1.isEmpty = true → m.get?
simp_to_model; empty
theorem get?_insert [LawfulBEq α] {a k : α} {v : β k} : (m.insert k v).get? a =
if h : a == k then some (cast (congrArg β (eq_of_beq h).symm) v) else m.get? a := by
if h : k == a then some (cast (congrArg β (eq_of_beq h)) v) else m.get? a := by
simp_to_model using List.getValueCast?_insertEntry
theorem get?_insert_self [LawfulBEq α] {k : α} {v : β k} : (m.insert k v).get? k = some v := by
@@ -215,7 +215,7 @@ theorem get?_eq_none [LawfulBEq α] {a : α} : m.contains a = false → m.get? a
simp_to_model using List.getValueCast?_eq_none
theorem get?_erase [LawfulBEq α] {k a : α} :
(m.erase k).get? a = bif a == k then none else m.get? a := by
(m.erase k).get? a = bif k == a then none else m.get? a := by
simp_to_model using List.getValueCast?_eraseKey
theorem get?_erase_self [LawfulBEq α] {k : α} : (m.erase k).get? k = none := by
@@ -234,7 +234,7 @@ theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
simp_to_model; empty
theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
get? (m.insert k v) a = bif a == k then some v else get? m a := by
get? (m.insert k v) a = bif k == a then some v else get? m a := by
simp_to_model using List.getValue?_insertEntry
theorem get?_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
@@ -250,7 +250,7 @@ theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} :
simp_to_model using List.getValue?_eq_none.2
theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
Const.get? (m.erase k) a = bif a == k then none else get? m a := by
Const.get? (m.erase k) a = bif k == a then none else get? m a := by
simp_to_model using List.getValue?_eraseKey
theorem get?_erase_self [EquivBEq α] [LawfulHashable α] {k : α} :
@@ -268,8 +268,8 @@ end Const
theorem get_insert [LawfulBEq α] {k a : α} {v : β k} {h₁} :
(m.insert k v).get a h₁ =
if h₂ : a == k then
cast (congrArg β (eq_of_beq h₂).symm) v
if h₂ : k == a then
cast (congrArg β (eq_of_beq h₂)) v
else
m.get a (contains_of_contains_insert _ h h₁ (Bool.eq_false_iff.2 h₂)) := by
simp_to_model using List.getValueCast_insertEntry
@@ -292,7 +292,7 @@ variable {β : Type v} (m : Raw₀ α (fun _ => β)) (h : m.1.WF)
theorem get_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
get (m.insert k v) a h₁ =
if h₂ : a == k then v
if h₂ : k == a then v
else get m a (contains_of_contains_insert _ h h₁ (Bool.eq_false_iff.2 h₂)) := by
simp_to_model using List.getValue_insertEntry
@@ -328,7 +328,7 @@ theorem get!_of_isEmpty [LawfulBEq α] {a : α} [Inhabited (β a)] :
theorem get!_insert [LawfulBEq α] {k a : α} [Inhabited (β a)] {v : β k} :
(m.insert k v).get! a =
if h : a == k then cast (congrArg β (eq_of_beq h).symm) v else m.get! a := by
if h : k == a then cast (congrArg β (eq_of_beq h)) v else m.get! a := by
simp_to_model using List.getValueCast!_insertEntry
theorem get!_insert_self [LawfulBEq α] {a : α} [Inhabited (β a)] {b : β a} :
@@ -340,7 +340,7 @@ theorem get!_eq_default [LawfulBEq α] {a : α} [Inhabited (β a)] :
simp_to_model using List.getValueCast!_eq_default
theorem get!_erase [LawfulBEq α] {k a : α} [Inhabited (β a)] :
(m.erase k).get! a = bif a == k then default else m.get! a := by
(m.erase k).get! a = bif k == a then default else m.get! a := by
simp_to_model using List.getValueCast!_eraseKey
theorem get!_erase_self [LawfulBEq α] {k : α} [Inhabited (β k)] :
@@ -372,7 +372,7 @@ theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
simp_to_model; empty
theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
get! (m.insert k v) a = bif a == k then v else get! m a := by
get! (m.insert k v) a = bif k == a then v else get! m a := by
simp_to_model using List.getValue!_insertEntry
theorem get!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} {v : β} :
@@ -384,7 +384,7 @@ theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
simp_to_model using List.getValue!_eq_default
theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
get! (m.erase k) a = bif a == k then default else get! m a := by
get! (m.erase k) a = bif k == a then default else get! m a := by
simp_to_model using List.getValue!_eraseKey
theorem get!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} :
@@ -423,7 +423,7 @@ theorem getD_of_isEmpty [LawfulBEq α] {a : α} {fallback : β a} :
theorem getD_insert [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} :
(m.insert k v).getD a fallback =
if h : a == k then cast (congrArg β (eq_of_beq h).symm) v else m.getD a fallback := by
if h : k == a then cast (congrArg β (eq_of_beq h)) v else m.getD a fallback := by
simp_to_model using List.getValueCastD_insertEntry
theorem getD_insert_self [LawfulBEq α] {a : α} {fallback b : β a} :
@@ -435,7 +435,7 @@ theorem getD_eq_fallback [LawfulBEq α] {a : α} {fallback : β a} :
simp_to_model using List.getValueCastD_eq_fallback
theorem getD_erase [LawfulBEq α] {k a : α} {fallback : β a} :
(m.erase k).getD a fallback = bif a == k then fallback else m.getD a fallback := by
(m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback := by
simp_to_model using List.getValueCastD_eraseKey
theorem getD_erase_self [LawfulBEq α] {k : α} {fallback : β k} :
@@ -471,7 +471,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
simp_to_model; empty
theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
getD (m.insert k v) a fallback = bif a == k then v else getD m a fallback := by
getD (m.insert k v) a fallback = bif k == a then v else getD m a fallback := by
simp_to_model using List.getValueD_insertEntry
theorem getD_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback v : β} :
@@ -483,7 +483,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
simp_to_model using List.getValueD_eq_fallback
theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
getD (m.erase k) a fallback = bif a == k then fallback else getD m a fallback := by
getD (m.erase k) a fallback = bif k == a then fallback else getD m a fallback := by
simp_to_model using List.getValueD_eraseKey
theorem getD_erase_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} :
@@ -521,7 +521,7 @@ theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k
simp_to_model using List.isEmpty_insertEntryIfNew
theorem contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
(m.insertIfNew k v).contains a = (a == k || m.contains a) := by
(m.insertIfNew k v).contains a = (k == a || m.contains a) := by
simp_to_model using List.containsKey_insertEntryIfNew
theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@@ -529,13 +529,13 @@ theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v
simp_to_model using List.containsKey_insertEntryIfNew_self
theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
(m.insertIfNew k v).contains a (a == k) = false m.contains a := by
(m.insertIfNew k v).contains a (k == a) = false m.contains a := by
simp_to_model using List.containsKey_of_containsKey_insertEntryIfNew
/-- This is a restatement of `contains_insertIfNew` that is written to exactly match the proof
obligation in the statement of `get_insertIfNew`. -/
theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
(m.insertIfNew k v).contains a ¬((a == k) m.contains k = false) m.contains a := by
(m.insertIfNew k v).contains a ¬((k == a) m.contains k = false) m.contains a := by
simp_to_model using List.containsKey_of_containsKey_insertEntryIfNew'
theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@@ -548,25 +548,25 @@ theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v :
theorem get?_insertIfNew [LawfulBEq α] {k a : α} {v : β k} :
(m.insertIfNew k v).get? a =
if h : a == k m.contains k = false then some (cast (congrArg β (eq_of_beq h.1).symm) v)
if h : k == a m.contains k = false then some (cast (congrArg β (eq_of_beq h.1)) v)
else m.get? a := by
simp_to_model using List.getValueCast?_insertEntryIfNew
theorem get_insertIfNew [LawfulBEq α] {k a : α} {v : β k} {h₁} :
(m.insertIfNew k v).get a h₁ =
if h₂ : a == k m.contains k = false then cast (congrArg β (eq_of_beq h₂.1).symm) v
if h₂ : k == a m.contains k = false then cast (congrArg β (eq_of_beq h₂.1)) v
else m.get a (contains_of_contains_insertIfNew' _ h h₁ h₂) := by
simp_to_model using List.getValueCast_insertEntryIfNew
theorem get!_insertIfNew [LawfulBEq α] {k a : α} [Inhabited (β a)] {v : β k} :
(m.insertIfNew k v).get! a =
if h : a == k m.contains k = false then cast (congrArg β (eq_of_beq h.1).symm) v
if h : k == a m.contains k = false then cast (congrArg β (eq_of_beq h.1)) v
else m.get! a := by
simp_to_model using List.getValueCast!_insertEntryIfNew
theorem getD_insertIfNew [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} :
(m.insertIfNew k v).getD a fallback =
if h : a == k m.contains k = false then cast (congrArg β (eq_of_beq h.1).symm) v
if h : k == a m.contains k = false then cast (congrArg β (eq_of_beq h.1)) v
else m.getD a fallback := by
simp_to_model using List.getValueCastD_insertEntryIfNew
@@ -575,22 +575,22 @@ namespace Const
variable {β : Type v} (m : Raw₀ α (fun _ => β)) (h : m.1.WF)
theorem get?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
get? (m.insertIfNew k v) a = bif a == k && !m.contains k then some v else get? m a := by
get? (m.insertIfNew k v) a = bif k == a && !m.contains k then some v else get? m a := by
simp_to_model using List.getValue?_insertEntryIfNew
theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
get (m.insertIfNew k v) a h₁ =
if h₂ : a == k m.contains k = false then v
if h₂ : k == a m.contains k = false then v
else get m a (contains_of_contains_insertIfNew' _ h h₁ h₂) := by
simp_to_model using List.getValue_insertEntryIfNew
theorem get!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
get! (m.insertIfNew k v) a = bif a == k && !m.contains k then v else get! m a := by
get! (m.insertIfNew k v) a = bif k == a && !m.contains k then v else get! m a := by
simp_to_model using List.getValue!_insertEntryIfNew
theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
getD (m.insertIfNew k v) a fallback =
bif a == k && !m.contains k then v else getD m a fallback := by
bif k == a && !m.contains k then v else getD m a fallback := by
simp_to_model using List.getValueD_insertEntryIfNew
end Const

View File

@@ -22,7 +22,7 @@ set_option autoImplicit false
universe u v
variable {α : Type u} {β : α Type v} [BEq α] [Hashable α]
variable {α : Type u} {β : α Type v} {_ : BEq α} {_ : Hashable α}
namespace Std.DHashMap
@@ -65,20 +65,20 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
@[simp]
theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
(m.insert k v).contains a = (a == k || m.contains a) :=
(m.insert k v).contains a = (k == a || m.contains a) :=
Raw₀.contains_insert m.1, _ m.2
@[simp]
theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
a m.insert k v a == k a m := by
a m.insert k v k == a a m := by
simp [mem_iff_contains, contains_insert]
theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
(m.insert k v).contains a (a == k) = false m.contains a :=
(m.insert k v).contains a (k == a) = false m.contains a :=
Raw₀.contains_of_contains_insert m.1, _ m.2
theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
a m.insert k v (a == k) = false a m := by
a m.insert k v (k == a) = false a m := by
simpa [mem_iff_contains, -contains_insert] using contains_of_contains_insert
@[simp]
@@ -124,12 +124,12 @@ theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} :
@[simp]
theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k).contains a = (!(a == k) && m.contains a) :=
(m.erase k).contains a = (!(k == a) && m.contains a) :=
Raw₀.contains_erase m.1, _ m.2
@[simp]
theorem mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
a m.erase k (a == k) = false a m := by
a m.erase k (k == a) = false a m := by
simp [mem_iff_contains, contains_erase]
theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
@@ -176,7 +176,7 @@ theorem get?_of_isEmpty [LawfulBEq α] {a : α} : m.isEmpty = true → m.get? a
Raw₀.get?_of_isEmpty m.1, _ m.2
theorem get?_insert [LawfulBEq α] {a k : α} {v : β k} : (m.insert k v).get? a =
if h : a == k then some (cast (congrArg β (eq_of_beq h).symm) v) else m.get? a :=
if h : k == a then some (cast (congrArg β (eq_of_beq h)) v) else m.get? a :=
Raw₀.get?_insert m.1, _ m.2
@[simp]
@@ -194,7 +194,7 @@ theorem get?_eq_none [LawfulBEq α] {a : α} : ¬a ∈ m → m.get? a = none :=
simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false
theorem get?_erase [LawfulBEq α] {k a : α} :
(m.erase k).get? a = bif a == k then none else m.get? a :=
(m.erase k).get? a = bif k == a then none else m.get? a :=
Raw₀.get?_erase m.1, _ m.2
@[simp]
@@ -218,7 +218,7 @@ theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
Raw₀.Const.get?_of_isEmpty m.1, _ m.2
theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
get? (m.insert k v) a = bif a == k then some v else get? m a :=
get? (m.insert k v) a = bif k == a then some v else get? m a :=
Raw₀.Const.get?_insert m.1, _ m.2
@[simp]
@@ -238,7 +238,7 @@ theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α } : ¬a ∈ m →
simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false
theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
Const.get? (m.erase k) a = bif a == k then none else get? m a :=
Const.get? (m.erase k) a = bif k == a then none else get? m a :=
Raw₀.Const.get?_erase m.1, _ m.2
@[simp]
@@ -255,8 +255,8 @@ end Const
theorem get_insert [LawfulBEq α] {k a : α} {v : β k} {h₁} :
(m.insert k v).get a h₁ =
if h₂ : a == k then
cast (congrArg β (eq_of_beq h₂).symm) v
if h₂ : k == a then
cast (congrArg β (eq_of_beq h₂)) v
else
m.get a (mem_of_mem_insert h₁ (Bool.eq_false_iff.2 h₂)) :=
Raw₀.get_insert m.1, _ m.2
@@ -280,7 +280,7 @@ variable {β : Type v} {m : DHashMap α (fun _ => β)}
theorem get_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
get (m.insert k v) a h₁ =
if h₂ : a == k then v else get m a (mem_of_mem_insert h₁ (Bool.eq_false_iff.2 h₂)) :=
if h₂ : k == a then v else get m a (mem_of_mem_insert h₁ (Bool.eq_false_iff.2 h₂)) :=
Raw₀.Const.get_insert m.1, _ m.2
@[simp]
@@ -322,7 +322,7 @@ theorem get!_of_isEmpty [LawfulBEq α] {a : α} [Inhabited (β a)] :
theorem get!_insert [LawfulBEq α] {k a : α} [Inhabited (β a)] {v : β k} :
(m.insert k v).get! a =
if h : a == k then cast (congrArg β (eq_of_beq h).symm) v else m.get! a :=
if h : k == a then cast (congrArg β (eq_of_beq h)) v else m.get! a :=
Raw₀.get!_insert m.1, _ m.2
@[simp]
@@ -339,7 +339,7 @@ theorem get!_eq_default [LawfulBEq α] {a : α} [Inhabited (β a)] :
simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false
theorem get!_erase [LawfulBEq α] {k a : α} [Inhabited (β a)] :
(m.erase k).get! a = bif a == k then default else m.get! a :=
(m.erase k).get! a = bif k == a then default else m.get! a :=
Raw₀.get!_erase m.1, _ m.2
@[simp]
@@ -381,7 +381,7 @@ theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
Raw₀.Const.get!_of_isEmpty m.1, _ m.2
theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
get! (m.insert k v) a = bif a == k then v else get! m a :=
get! (m.insert k v) a = bif k == a then v else get! m a :=
Raw₀.Const.get!_insert m.1, _ m.2
@[simp]
@@ -398,7 +398,7 @@ theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false
theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
get! (m.erase k) a = bif a == k then default else get! m a :=
get! (m.erase k) a = bif k == a then default else get! m a :=
Raw₀.Const.get!_erase m.1, _ m.2
@[simp]
@@ -448,7 +448,7 @@ theorem getD_of_isEmpty [LawfulBEq α] {a : α} {fallback : β a} :
theorem getD_insert [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} :
(m.insert k v).getD a fallback =
if h : a == k then cast (congrArg β (eq_of_beq h).symm) v else m.getD a fallback :=
if h : k == a then cast (congrArg β (eq_of_beq h)) v else m.getD a fallback :=
Raw₀.getD_insert m.1, _ m.2
@[simp]
@@ -465,7 +465,7 @@ theorem getD_eq_fallback [LawfulBEq α] {a : α} {fallback : β a} :
simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false
theorem getD_erase [LawfulBEq α] {k a : α} {fallback : β a} :
(m.erase k).getD a fallback = bif a == k then fallback else m.getD a fallback :=
(m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback :=
Raw₀.getD_erase m.1, _ m.2
@[simp]
@@ -512,7 +512,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
Raw₀.Const.getD_of_isEmpty m.1, _ m.2
theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
getD (m.insert k v) a fallback = bif a == k then v else getD m a fallback :=
getD (m.insert k v) a fallback = bif k == a then v else getD m a fallback :=
Raw₀.Const.getD_insert m.1, _ m.2
@[simp]
@@ -529,7 +529,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false
theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
getD (m.erase k) a fallback = bif a == k then fallback else getD m a fallback :=
getD (m.erase k) a fallback = bif k == a then fallback else getD m a fallback :=
Raw₀.Const.getD_erase m.1, _ m.2
@[simp]
@@ -574,12 +574,12 @@ theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k
@[simp]
theorem contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
(m.insertIfNew k v).contains a = (a == k || m.contains a) :=
(m.insertIfNew k v).contains a = (k == a || m.contains a) :=
Raw₀.contains_insertIfNew m.1, _ m.2
@[simp]
theorem mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
a m.insertIfNew k v a == k a m := by
a m.insertIfNew k v k == a a m := by
simp [mem_iff_contains, contains_insertIfNew]
theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@@ -591,23 +591,23 @@ theorem mem_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β
simpa [mem_iff_contains, -contains_insertIfNew] using contains_insertIfNew_self
theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
(m.insertIfNew k v).contains a (a == k) = false m.contains a :=
(m.insertIfNew k v).contains a (k == a) = false m.contains a :=
Raw₀.contains_of_contains_insertIfNew m.1, _ m.2
theorem mem_of_mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
a m.insertIfNew k v (a == k) = false a m := by
a m.insertIfNew k v (k == a) = false a m := by
simpa [mem_iff_contains, -contains_insertIfNew] using contains_of_contains_insertIfNew
/-- This is a restatement of `contains_insertIfNew` that is written to exactly match the proof
obligation in the statement of `get_insertIfNew`. -/
theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
(m.insertIfNew k v).contains a ¬((a == k) m.contains k = false) m.contains a :=
(m.insertIfNew k v).contains a ¬((k == a) m.contains k = false) m.contains a :=
Raw₀.contains_of_contains_insertIfNew' m.1, _ m.2
/-- This is a restatement of `mem_insertIfNew` that is written to exactly match the proof obligation
in the statement of `get_insertIfNew`. -/
theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
a m.insertIfNew k v ¬((a == k) ¬k m) a m := by
a m.insertIfNew k v ¬((k == a) ¬k m) a m := by
simpa [mem_iff_contains, -contains_insertIfNew] using contains_of_contains_insertIfNew'
theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@@ -619,25 +619,25 @@ theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v :
Raw₀.size_le_size_insertIfNew m.1, _ m.2
theorem get?_insertIfNew [LawfulBEq α] {k a : α} {v : β k} : (m.insertIfNew k v).get? a =
if h : a == k ¬k m then some (cast (congrArg β (eq_of_beq h.1).symm) v) else m.get? a := by
if h : k == a ¬k m then some (cast (congrArg β (eq_of_beq h.1)) v) else m.get? a := by
simp only [mem_iff_contains, Bool.not_eq_true]
exact Raw₀.get?_insertIfNew m.1, _ m.2
theorem get_insertIfNew [LawfulBEq α] {k a : α} {v : β k} {h₁} : (m.insertIfNew k v).get a h₁ =
if h₂ : a == k ¬k m then cast (congrArg β (eq_of_beq h₂.1).symm) v else m.get a
if h₂ : k == a ¬k m then cast (congrArg β (eq_of_beq h₂.1)) v else m.get a
(mem_of_mem_insertIfNew' h₁ h₂) := by
simp only [mem_iff_contains, Bool.not_eq_true]
exact Raw₀.get_insertIfNew m.1, _ m.2
theorem get!_insertIfNew [LawfulBEq α] {k a : α} [Inhabited (β a)] {v : β k} :
(m.insertIfNew k v).get! a =
if h : a == k ¬k m then cast (congrArg β (eq_of_beq h.1).symm) v else m.get! a := by
if h : k == a ¬k m then cast (congrArg β (eq_of_beq h.1)) v else m.get! a := by
simp only [mem_iff_contains, Bool.not_eq_true]
exact Raw₀.get!_insertIfNew m.1, _ m.2
theorem getD_insertIfNew [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} :
(m.insertIfNew k v).getD a fallback =
if h : a == k ¬k m then cast (congrArg β (eq_of_beq h.1).symm) v
if h : k == a ¬k m then cast (congrArg β (eq_of_beq h.1)) v
else m.getD a fallback := by
simp only [mem_iff_contains, Bool.not_eq_true]
exact Raw₀.getD_insertIfNew m.1, _ m.2
@@ -647,22 +647,22 @@ namespace Const
variable {β : Type v} {m : DHashMap α (fun _ => β)}
theorem get?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
get? (m.insertIfNew k v) a = bif a == k && !m.contains k then some v else get? m a :=
get? (m.insertIfNew k v) a = bif k == a && !m.contains k then some v else get? m a :=
Raw₀.Const.get?_insertIfNew m.1, _ m.2
theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
get (m.insertIfNew k v) a h₁ =
if h₂ : a == k ¬k m then v else get m a (mem_of_mem_insertIfNew' h₁ h₂) := by
if h₂ : k == a ¬k m then v else get m a (mem_of_mem_insertIfNew' h₁ h₂) := by
simp only [mem_iff_contains, Bool.not_eq_true]
exact Raw₀.Const.get_insertIfNew m.1, _ m.2
theorem get!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
get! (m.insertIfNew k v) a = bif a == k && !m.contains k then v else get! m a :=
get! (m.insertIfNew k v) a = bif k == a && !m.contains k then v else get! m a :=
Raw₀.Const.get!_insertIfNew m.1, _ m.2
theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
getD (m.insertIfNew k v) a fallback =
bif a == k && !m.contains k then v else getD m a fallback :=
bif k == a && !m.contains k then v else getD m a fallback :=
Raw₀.Const.getD_insertIfNew m.1, _ m.2
end Const

View File

@@ -26,16 +26,19 @@ inductive types. The well-formedness invariant is called `Raw.WF`. When in doubt
over `DHashMap.Raw`. Lemmas about the operations on `Std.Data.DHashMap.Raw` are available in the
module `Std.Data.DHashMap.RawLemmas`.
The hash map uses `==` (provided by the `BEq` typeclass) to compare keys and `hash` (provided by
the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
`EquivBEq` and `LawfulHashable` typeclasses). Both of these conditions are automatic if the BEq
instance is lawful, i.e., if `a == b` implies `a = b`.
The hash table is backed by an `Array`. Users should make sure that the hash map is used linearly to
avoid expensive copies.
This is a simple separate-chaining hash table. The data of the hash map consists of a cached size
and an array of buckets, where each bucket is a linked list of key-value pais. The number of buckets
is always a power of two. The hash map doubles its size upon inserting an element such that the
number of elements is more than 75% of the number of buckets.
The hash map uses `==` (provided by the `BEq` typeclass) to compare keys and `hash` (provided by
the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
`EquivBEq` and `LawfulHashable` typeclasses). Both of these conditions are automatic if the BEq
instance is lawful, i.e., if `a == b` implies `a = b`.
-/
structure Raw (α : Type u) (β : α Type v) where
/-- The number of mappings present in the hash map -/

View File

@@ -113,20 +113,20 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
@[simp]
theorem contains_insert [EquivBEq α] [LawfulHashable α] {a k : α} {v : β k} :
(m.insert k v).contains a = (a == k || m.contains a) := by
(m.insert k v).contains a = (k == a || m.contains a) := by
simp_to_raw using Raw₀.contains_insert
@[simp]
theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
a m.insert k v a == k a m := by
a m.insert k v k == a a m := by
simp [mem_iff_contains, contains_insert h]
theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] {a k : α} {v : β k} :
(m.insert k v).contains a (a == k) = false m.contains a := by
(m.insert k v).contains a (k == a) = false m.contains a := by
simp_to_raw using Raw₀.contains_of_contains_insert
theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
a m.insert k v (a == k) = false a m := by
a m.insert k v (k == a) = false a m := by
simpa [mem_iff_contains] using contains_of_contains_insert h
@[simp]
@@ -173,12 +173,12 @@ theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} :
@[simp]
theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k).contains a = (!(a == k) && m.contains a) := by
(m.erase k).contains a = (!(k == a) && m.contains a) := by
simp_to_raw using Raw₀.contains_erase
@[simp]
theorem mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
a m.erase k (a == k) = false a m := by
a m.erase k (k == a) = false a m := by
simp [mem_iff_contains, contains_erase h]
theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
@@ -225,7 +225,7 @@ theorem get?_of_isEmpty [LawfulBEq α] {a : α} : m.isEmpty = true → m.get? a
simp_to_raw using Raw₀.get?_of_isEmpty m, _
theorem get?_insert [LawfulBEq α] {a k : α} {v : β k} : (m.insert k v).get? a =
if h : a == k then some (cast (congrArg β (eq_of_beq h).symm) v) else m.get? a := by
if h : k == a then some (cast (congrArg β (eq_of_beq h)) v) else m.get? a := by
simp_to_raw using Raw₀.get?_insert
@[simp]
@@ -243,7 +243,7 @@ theorem get?_eq_none [LawfulBEq α] {a : α} : ¬a ∈ m → m.get? a = none :=
simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false h
theorem get?_erase [LawfulBEq α] {k a : α} :
(m.erase k).get? a = bif a == k then none else m.get? a := by
(m.erase k).get? a = bif k == a then none else m.get? a := by
simp_to_raw using Raw₀.get?_erase
@[simp]
@@ -267,7 +267,7 @@ theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
simp_to_raw using Raw₀.Const.get?_of_isEmpty m, _
theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
get? (m.insert k v) a = bif a == k then some v else get? m a := by
get? (m.insert k v) a = bif k == a then some v else get? m a := by
simp_to_raw using Raw₀.Const.get?_insert
@[simp]
@@ -287,7 +287,7 @@ theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m →
simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false h
theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
Const.get? (m.erase k) a = bif a == k then none else get? m a := by
Const.get? (m.erase k) a = bif k == a then none else get? m a := by
simp_to_raw using Raw₀.Const.get?_erase
@[simp]
@@ -305,8 +305,8 @@ end Const
theorem get_insert [LawfulBEq α] {k a : α} {v : β k} {h₁} :
(m.insert k v).get a h₁ =
if h₂ : a == k then
cast (congrArg β (eq_of_beq h₂).symm) v
if h₂ : k == a then
cast (congrArg β (eq_of_beq h₂)) v
else
m.get a (mem_of_mem_insert h h₁ (Bool.eq_false_iff.2 h₂)) := by
simp_to_raw using Raw₀.get_insert m, _
@@ -330,7 +330,7 @@ variable {β : Type v} {m : DHashMap.Raw α (fun _ => β)} (h : m.WF)
theorem get_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
get (m.insert k v) a h₁ =
if h₂ : a == k then v else get m a (mem_of_mem_insert h h₁ (Bool.eq_false_iff.2 h₂)) := by
if h₂ : k == a then v else get m a (mem_of_mem_insert h h₁ (Bool.eq_false_iff.2 h₂)) := by
simp_to_raw using Raw₀.Const.get_insert m, _
@[simp]
@@ -371,7 +371,7 @@ theorem get!_of_isEmpty [LawfulBEq α] {a : α} [Inhabited (β a)] :
simp_to_raw using Raw₀.get!_of_isEmpty m, _
theorem get!_insert [LawfulBEq α] {k a : α} [Inhabited (β a)] {v : β k} : (m.insert k v).get! a =
if h : a == k then cast (congrArg β (eq_of_beq h).symm) v else m.get! a := by
if h : k == a then cast (congrArg β (eq_of_beq h)) v else m.get! a := by
simp_to_raw using Raw₀.get!_insert
@[simp]
@@ -388,7 +388,7 @@ theorem get!_eq_default [LawfulBEq α] {a : α} [Inhabited (β a)] :
simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false h
theorem get!_erase [LawfulBEq α] {k a : α} [Inhabited (β a)] :
(m.erase k).get! a = bif a == k then default else m.get! a := by
(m.erase k).get! a = bif k == a then default else m.get! a := by
simp_to_raw using Raw₀.get!_erase
@[simp]
@@ -429,7 +429,7 @@ theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
simp_to_raw using Raw₀.Const.get!_of_isEmpty m, _
theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
get! (m.insert k v) a = bif a == k then v else get! m a := by
get! (m.insert k v) a = bif k == a then v else get! m a := by
simp_to_raw using Raw₀.Const.get!_insert
@[simp]
@@ -446,7 +446,7 @@ theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false h
theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
get! (m.erase k) a = bif a == k then default else get! m a := by
get! (m.erase k) a = bif k == a then default else get! m a := by
simp_to_raw using Raw₀.Const.get!_erase
@[simp]
@@ -496,7 +496,7 @@ theorem getD_of_isEmpty [LawfulBEq α] {a : α} {fallback : β a} :
theorem getD_insert [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} :
(m.insert k v).getD a fallback =
if h : a == k then cast (congrArg β (eq_of_beq h).symm) v else m.getD a fallback := by
if h : k == a then cast (congrArg β (eq_of_beq h)) v else m.getD a fallback := by
simp_to_raw using Raw₀.getD_insert
@[simp]
@@ -513,7 +513,7 @@ theorem getD_eq_fallback [LawfulBEq α] {a : α} {fallback : β a} :
simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false h
theorem getD_erase [LawfulBEq α] {k a : α} {fallback : β a} :
(m.erase k).getD a fallback = bif a == k then fallback else m.getD a fallback := by
(m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback := by
simp_to_raw using Raw₀.getD_erase
@[simp]
@@ -559,7 +559,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
simp_to_raw using Raw₀.Const.getD_of_isEmpty m, _
theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
getD (m.insert k v) a fallback = bif a == k then v else getD m a fallback := by
getD (m.insert k v) a fallback = bif k == a then v else getD m a fallback := by
simp_to_raw using Raw₀.Const.getD_insert
@[simp]
@@ -576,7 +576,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false h
theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
getD (m.erase k) a fallback = bif a == k then fallback else getD m a fallback := by
getD (m.erase k) a fallback = bif k == a then fallback else getD m a fallback := by
simp_to_raw using Raw₀.Const.getD_erase
@[simp]
@@ -621,12 +621,12 @@ theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k
@[simp]
theorem contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
(m.insertIfNew k v).contains a = (a == k || m.contains a) := by
(m.insertIfNew k v).contains a = (k == a || m.contains a) := by
simp_to_raw using Raw₀.contains_insertIfNew
@[simp]
theorem mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
a m.insertIfNew k v a == k a m := by
a m.insertIfNew k v k == a a m := by
simp [mem_iff_contains, contains_insertIfNew h]
theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@@ -638,23 +638,23 @@ theorem mem_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β
simpa [mem_iff_contains, -contains_insertIfNew] using contains_insertIfNew_self h
theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
(m.insertIfNew k v).contains a (a == k) = false m.contains a := by
(m.insertIfNew k v).contains a (k == a) = false m.contains a := by
simp_to_raw using Raw₀.contains_of_contains_insertIfNew
theorem mem_of_mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
a m.insertIfNew k v (a == k) = false a m := by
a m.insertIfNew k v (k == a) = false a m := by
simpa [mem_iff_contains, -contains_insertIfNew] using contains_of_contains_insertIfNew h
/-- This is a restatement of `contains_insertIfNew` that is written to exactly match the proof
obligation in the statement of `get_insertIfNew`. -/
theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
(m.insertIfNew k v).contains a ¬((a == k) m.contains k = false) m.contains a := by
(m.insertIfNew k v).contains a ¬((k == a) m.contains k = false) m.contains a := by
simp_to_raw using Raw₀.contains_of_contains_insertIfNew'
/-- This is a restatement of `mem_insertIfNew` that is written to exactly match the proof obligation
in the statement of `get_insertIfNew`. -/
theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
a m.insertIfNew k v ¬((a == k) ¬k m) a m := by
a m.insertIfNew k v ¬((k == a) ¬k m) a m := by
simpa [mem_iff_contains] using contains_of_contains_insertIfNew' h
theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@@ -667,27 +667,27 @@ theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v :
theorem get?_insertIfNew [LawfulBEq α] {k a : α} {v : β k} :
(m.insertIfNew k v).get? a =
if h : a == k ¬k m then some (cast (congrArg β (eq_of_beq h.1).symm) v)
if h : k == a ¬k m then some (cast (congrArg β (eq_of_beq h.1)) v)
else m.get? a := by
simp only [mem_iff_contains, Bool.not_eq_true]
simp_to_raw using Raw₀.get?_insertIfNew m, _
theorem get_insertIfNew [LawfulBEq α] {k a : α} {v : β k} {h₁} :
(m.insertIfNew k v).get a h₁ =
if h₂ : a == k ¬k m then cast (congrArg β (eq_of_beq h₂.1).symm) v
if h₂ : k == a ¬k m then cast (congrArg β (eq_of_beq h₂.1)) v
else m.get a (mem_of_mem_insertIfNew' h h₁ h₂) := by
simp only [mem_iff_contains, Bool.not_eq_true]
simp_to_raw using Raw₀.get_insertIfNew m, _
theorem get!_insertIfNew [LawfulBEq α] {k a : α} [Inhabited (β a)] {v : β k} :
(m.insertIfNew k v).get! a =
if h : a == k ¬k m then cast (congrArg β (eq_of_beq h.1).symm) v else m.get! a := by
if h : k == a ¬k m then cast (congrArg β (eq_of_beq h.1)) v else m.get! a := by
simp only [mem_iff_contains, Bool.not_eq_true]
simp_to_raw using Raw₀.get!_insertIfNew m, _
theorem getD_insertIfNew [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} :
(m.insertIfNew k v).getD a fallback =
if h : a == k ¬k m then cast (congrArg β (eq_of_beq h.1).symm) v
if h : k == a ¬k m then cast (congrArg β (eq_of_beq h.1)) v
else m.getD a fallback := by
simp only [mem_iff_contains, Bool.not_eq_true]
simp_to_raw using Raw₀.getD_insertIfNew
@@ -697,23 +697,23 @@ namespace Const
variable {β : Type v} {m : DHashMap.Raw α (fun _ => β)} (h : m.WF)
theorem get?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
get? (m.insertIfNew k v) a = bif a == k && !m.contains k then some v else get? m a := by
get? (m.insertIfNew k v) a = bif k == a && !m.contains k then some v else get? m a := by
simp_to_raw using Raw₀.Const.get?_insertIfNew
theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
get (m.insertIfNew k v) a h₁ =
if h₂ : a == k ¬k m then v
if h₂ : k == a ¬k m then v
else get m a (mem_of_mem_insertIfNew' h h₁ h₂) := by
simp only [mem_iff_contains, Bool.not_eq_true]
simp_to_raw using Raw₀.Const.get_insertIfNew m, _
theorem get!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
get! (m.insertIfNew k v) a = bif a == k && !m.contains k then v else get! m a := by
get! (m.insertIfNew k v) a = bif k == a && !m.contains k then v else get! m a := by
simp_to_raw using Raw₀.Const.get!_insertIfNew
theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
getD (m.insertIfNew k v) a fallback =
bif a == k && !m.contains k then v else getD m a fallback := by
bif k == a && !m.contains k then v else getD m a fallback := by
simp_to_raw using Raw₀.Const.getD_insertIfNew
end Const

View File

@@ -27,7 +27,7 @@ nested inductive types.
universe u v w
variable {α : Type u} {β : Type v}
variable {α : Type u} {β : Type v} {_ : BEq α} {_ : Hashable α}
namespace Std
@@ -39,6 +39,9 @@ and an array of buckets, where each bucket is a linked list of key-value pais. T
is always a power of two. The hash map doubles its size upon inserting an element such that the
number of elements is more than 75% of the number of buckets.
The hash table is backed by an `Array`. Users should make sure that the hash map is used linearly to
avoid expensive copies.
The hash map uses `==` (provided by the `BEq` typeclass) to compare keys and `hash` (provided by
the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
@@ -69,21 +72,21 @@ instance [BEq α] [Hashable α] : EmptyCollection (HashMap α β) where
instance [BEq α] [Hashable α] : Inhabited (HashMap α β) where
default :=
@[inline, inherit_doc DHashMap.insert] def insert [BEq α] [Hashable α] (m : HashMap α β) (a : α)
@[inline, inherit_doc DHashMap.insert] def insert (m : HashMap α β) (a : α)
(b : β) : HashMap α β :=
m.inner.insert a b
@[inline, inherit_doc DHashMap.insertIfNew] def insertIfNew [BEq α] [Hashable α] (m : HashMap α β)
@[inline, inherit_doc DHashMap.insertIfNew] def insertIfNew (m : HashMap α β)
(a : α) (b : β) : HashMap α β :=
m.inner.insertIfNew a b
@[inline, inherit_doc DHashMap.containsThenInsert] def containsThenInsert [BEq α] [Hashable α]
@[inline, inherit_doc DHashMap.containsThenInsert] def containsThenInsert
(m : HashMap α β) (a : α) (b : β) : Bool × HashMap α β :=
let replaced, r := m.inner.containsThenInsert a b
replaced, r
@[inline, inherit_doc DHashMap.containsThenInsertIfNew] def containsThenInsertIfNew [BEq α]
[Hashable α] (m : HashMap α β) (a : α) (b : β) : Bool × HashMap α β :=
@[inline, inherit_doc DHashMap.containsThenInsertIfNew] def containsThenInsertIfNew
(m : HashMap α β) (a : α) (b : β) : Bool × HashMap α β :=
let replaced, r := m.inner.containsThenInsertIfNew a b
replaced, r
@@ -96,7 +99,7 @@ returned map has a new value inserted.
Equivalent to (but potentially faster than) calling `get?` followed by `insertIfNew`.
-/
@[inline] def getThenInsertIfNew? [BEq α] [Hashable α] (m : HashMap α β) (a : α) (b : β) :
@[inline] def getThenInsertIfNew? (m : HashMap α β) (a : α) (b : β) :
Option β × HashMap α β :=
let previous, r := DHashMap.Const.getThenInsertIfNew? m.inner a b
previous, r
@@ -106,10 +109,10 @@ The notation `m[a]?` is preferred over calling this function directly.
Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.
-/
@[inline] def get? [BEq α] [Hashable α] (m : HashMap α β) (a : α) : Option β :=
@[inline] def get? (m : HashMap α β) (a : α) : Option β :=
DHashMap.Const.get? m.inner a
@[inline, inherit_doc DHashMap.contains] def contains [BEq α] [Hashable α] (m : HashMap α β)
@[inline, inherit_doc DHashMap.contains] def contains (m : HashMap α β)
(a : α) : Bool :=
m.inner.contains a
@@ -125,10 +128,10 @@ The notation `m[a]` or `m[a]'h` is preferred over calling this function directly
Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof of
`a ∈ m`.
-/
@[inline] def get [BEq α] [Hashable α] (m : HashMap α β) (a : α) (h : a m) : β :=
@[inline] def get (m : HashMap α β) (a : α) (h : a m) : β :=
DHashMap.Const.get m.inner a h
@[inline, inherit_doc DHashMap.Const.getD] def getD [BEq α] [Hashable α] (m : HashMap α β) (a : α)
@[inline, inherit_doc DHashMap.Const.getD] def getD (m : HashMap α β) (a : α)
(fallback : β) : β :=
DHashMap.Const.getD m.inner a fallback
@@ -137,7 +140,7 @@ The notation `m[a]!` is preferred over calling this function directly.
Tries to retrieve the mapping for the given key, panicking if no such mapping is present.
-/
@[inline] def get! [BEq α] [Hashable α] [Inhabited β] (m : HashMap α β) (a : α) : β :=
@[inline] def get! [Inhabited β] (m : HashMap α β) (a : α) : β :=
DHashMap.Const.get! m.inner a
instance [BEq α] [Hashable α] : GetElem? (HashMap α β) α β (fun m a => a m) where
@@ -145,37 +148,37 @@ instance [BEq α] [Hashable α] : GetElem? (HashMap α β) α β (fun m a => a
getElem? m a := m.get? a
getElem! m a := m.get! a
@[inline, inherit_doc DHashMap.erase] def erase [BEq α] [Hashable α] (m : HashMap α β) (a : α) :
@[inline, inherit_doc DHashMap.erase] def erase (m : HashMap α β) (a : α) :
HashMap α β :=
m.inner.erase a
@[inline, inherit_doc DHashMap.size] def size [BEq α] [Hashable α] (m : HashMap α β) : Nat :=
@[inline, inherit_doc DHashMap.size] def size (m : HashMap α β) : Nat :=
m.inner.size
@[inline, inherit_doc DHashMap.isEmpty] def isEmpty [BEq α] [Hashable α] (m : HashMap α β) : Bool :=
@[inline, inherit_doc DHashMap.isEmpty] def isEmpty (m : HashMap α β) : Bool :=
m.inner.isEmpty
section Unverified
/-! We currently do not provide lemmas for the functions below. -/
@[inline, inherit_doc DHashMap.filter] def filter [BEq α] [Hashable α] (f : α β Bool)
@[inline, inherit_doc DHashMap.filter] def filter (f : α β Bool)
(m : HashMap α β) : HashMap α β :=
m.inner.filter f
@[inline, inherit_doc DHashMap.foldM] def foldM [BEq α] [Hashable α] {m : Type w Type w}
@[inline, inherit_doc DHashMap.foldM] def foldM {m : Type w Type w}
[Monad m] {γ : Type w} (f : γ α β m γ) (init : γ) (b : HashMap α β) : m γ :=
b.inner.foldM f init
@[inline, inherit_doc DHashMap.fold] def fold [BEq α] [Hashable α] {γ : Type w}
@[inline, inherit_doc DHashMap.fold] def fold {γ : Type w}
(f : γ α β γ) (init : γ) (b : HashMap α β) : γ :=
b.inner.fold f init
@[inline, inherit_doc DHashMap.forM] def forM [BEq α] [Hashable α] {m : Type w Type w} [Monad m]
@[inline, inherit_doc DHashMap.forM] def forM {m : Type w Type w} [Monad m]
(f : (a : α) β m PUnit) (b : HashMap α β) : m PUnit :=
b.inner.forM f
@[inline, inherit_doc DHashMap.forIn] def forIn [BEq α] [Hashable α] {m : Type w Type w} [Monad m]
@[inline, inherit_doc DHashMap.forIn] def forIn {m : Type w Type w} [Monad m]
{γ : Type w} (f : (a : α) β γ m (ForInStep γ)) (init : γ) (b : HashMap α β) : m γ :=
b.inner.forIn f init
@@ -185,33 +188,33 @@ instance [BEq α] [Hashable α] {m : Type w → Type w} : ForM m (HashMap α β)
instance [BEq α] [Hashable α] {m : Type w Type w} : ForIn m (HashMap α β) (α × β) where
forIn m init f := m.forIn (fun a b acc => f (a, b) acc) init
@[inline, inherit_doc DHashMap.Const.toList] def toList [BEq α] [Hashable α] (m : HashMap α β) :
@[inline, inherit_doc DHashMap.Const.toList] def toList (m : HashMap α β) :
List (α × β) :=
DHashMap.Const.toList m.inner
@[inline, inherit_doc DHashMap.Const.toArray] def toArray [BEq α] [Hashable α] (m : HashMap α β) :
@[inline, inherit_doc DHashMap.Const.toArray] def toArray (m : HashMap α β) :
Array (α × β) :=
DHashMap.Const.toArray m.inner
@[inline, inherit_doc DHashMap.keys] def keys [BEq α] [Hashable α] (m : HashMap α β) : List α :=
@[inline, inherit_doc DHashMap.keys] def keys (m : HashMap α β) : List α :=
m.inner.keys
@[inline, inherit_doc DHashMap.keysArray] def keysArray [BEq α] [Hashable α] (m : HashMap α β) :
@[inline, inherit_doc DHashMap.keysArray] def keysArray (m : HashMap α β) :
Array α :=
m.inner.keysArray
@[inline, inherit_doc DHashMap.values] def values [BEq α] [Hashable α] (m : HashMap α β) : List β :=
@[inline, inherit_doc DHashMap.values] def values (m : HashMap α β) : List β :=
m.inner.values
@[inline, inherit_doc DHashMap.valuesArray] def valuesArray [BEq α] [Hashable α] (m : HashMap α β) :
@[inline, inherit_doc DHashMap.valuesArray] def valuesArray (m : HashMap α β) :
Array β :=
m.inner.valuesArray
@[inline, inherit_doc DHashMap.Const.insertMany] def insertMany [BEq α] [Hashable α] {ρ : Type w}
@[inline, inherit_doc DHashMap.Const.insertMany] def insertMany {ρ : Type w}
[ForIn Id ρ (α × β)] (m : HashMap α β) (l : ρ) : HashMap α β :=
DHashMap.Const.insertMany m.inner l
@[inline, inherit_doc DHashMap.Const.insertManyUnit] def insertManyUnit [BEq α] [Hashable α]
@[inline, inherit_doc DHashMap.Const.insertManyUnit] def insertManyUnit
{ρ : Type w} [ForIn Id ρ α] (m : HashMap α Unit) (l : ρ) : HashMap α Unit :=
DHashMap.Const.insertManyUnit m.inner l
@@ -223,7 +226,7 @@ instance [BEq α] [Hashable α] {m : Type w → Type w} : ForIn m (HashMap α β
HashMap α Unit :=
DHashMap.Const.unitOfList l
@[inline, inherit_doc DHashMap.Internal.numBuckets] def Internal.numBuckets [BEq α] [Hashable α]
@[inline, inherit_doc DHashMap.Internal.numBuckets] def Internal.numBuckets
(m : HashMap α β) : Nat :=
DHashMap.Internal.numBuckets m.inner

View File

@@ -20,7 +20,7 @@ set_option autoImplicit false
universe u v
variable {α : Type u} {β : Type v} [BEq α] [Hashable α]
variable {α : Type u} {β : Type v} {_ : BEq α} {_ : Hashable α}
namespace Std.HashMap
@@ -73,20 +73,20 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
@[simp]
theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insert k v).contains a = (a == k || m.contains a) :=
(m.insert k v).contains a = (k == a || m.contains a) :=
DHashMap.contains_insert
@[simp]
theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
a m.insert k v a == k a m :=
a m.insert k v k == a a m :=
DHashMap.mem_insert
theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insert k v).contains a (a == k) = false m.contains a :=
(m.insert k v).contains a (k == a) = false m.contains a :=
DHashMap.contains_of_contains_insert
theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
a m.insert k v (a == k) = false a m :=
a m.insert k v (k == a) = false a m :=
DHashMap.mem_of_mem_insert
@[simp]
@@ -132,12 +132,12 @@ theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} :
@[simp]
theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k).contains a = (!(a == k) && m.contains a) :=
(m.erase k).contains a = (!(k == a) && m.contains a) :=
DHashMap.contains_erase
@[simp]
theorem mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
a m.erase k (a == k) = false a m :=
a m.erase k (k == a) = false a m :=
DHashMap.mem_erase
theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
@@ -185,7 +185,7 @@ theorem getElem?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
DHashMap.Const.get?_of_isEmpty
theorem getElem?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insert k v)[a]? = bif a == k then some v else m[a]? :=
(m.insert k v)[a]? = bif k == a then some v else m[a]? :=
DHashMap.Const.get?_insert
@[simp]
@@ -205,7 +205,7 @@ theorem getElem?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m
DHashMap.Const.get?_eq_none
theorem getElem?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k)[a]? = bif a == k then none else m[a]? :=
(m.erase k)[a]? = bif k == a then none else m[a]? :=
DHashMap.Const.get?_erase
@[simp]
@@ -217,7 +217,7 @@ theorem getElem?_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a ==
theorem getElem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
(m.insert k v)[a]'h₁ =
if h₂ : a == k then v else m[a]'(mem_of_mem_insert h₁ (Bool.eq_false_iff.2 h₂)) :=
if h₂ : k == a then v else m[a]'(mem_of_mem_insert h₁ (Bool.eq_false_iff.2 h₂)) :=
DHashMap.Const.get_insert (h₁ := h₁)
@[simp]
@@ -251,7 +251,7 @@ theorem getElem!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a
DHashMap.Const.get!_of_isEmpty
theorem getElem!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
(m.insert k v)[a]! = bif a == k then v else m[a]! :=
(m.insert k v)[a]! = bif k == a then v else m[a]! :=
DHashMap.Const.get!_insert
@[simp]
@@ -268,7 +268,7 @@ theorem getElem!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a
DHashMap.Const.get!_eq_default
theorem getElem!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
(m.erase k)[a]! = bif a == k then default else m[a]! :=
(m.erase k)[a]! = bif k == a then default else m[a]! :=
DHashMap.Const.get!_erase
@[simp]
@@ -310,7 +310,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
DHashMap.Const.getD_of_isEmpty
theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
(m.insert k v).getD a fallback = bif a == k then v else m.getD a fallback :=
(m.insert k v).getD a fallback = bif k == a then v else m.getD a fallback :=
DHashMap.Const.getD_insert
@[simp]
@@ -327,7 +327,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
DHashMap.Const.getD_eq_fallback
theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
(m.erase k).getD a fallback = bif a == k then fallback else m.getD a fallback :=
(m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback :=
DHashMap.Const.getD_erase
@[simp]
@@ -366,12 +366,12 @@ theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β}
@[simp]
theorem contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insertIfNew k v).contains a = (a == k || m.contains a) :=
(m.insertIfNew k v).contains a = (k == a || m.contains a) :=
DHashMap.contains_insertIfNew
@[simp]
theorem mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
a m.insertIfNew k v a == k a m :=
a m.insertIfNew k v k == a a m :=
DHashMap.mem_insertIfNew
theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
@@ -383,23 +383,23 @@ theorem mem_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β}
DHashMap.mem_insertIfNew_self
theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insertIfNew k v).contains a (a == k) = false m.contains a :=
(m.insertIfNew k v).contains a (k == a) = false m.contains a :=
DHashMap.contains_of_contains_insertIfNew
theorem mem_of_mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
a m.insertIfNew k v (a == k) = false a m :=
a m.insertIfNew k v (k == a) = false a m :=
DHashMap.mem_of_mem_insertIfNew
/-- This is a restatement of `contains_insertIfNew` that is written to exactly match the proof
obligation in the statement of `getElem_insertIfNew`. -/
theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insertIfNew k v).contains a ¬((a == k) m.contains k = false) m.contains a :=
(m.insertIfNew k v).contains a ¬((k == a) m.contains k = false) m.contains a :=
DHashMap.contains_of_contains_insertIfNew'
/-- This is a restatement of `mem_insertIfNew` that is written to exactly match the proof obligation
in the statement of `getElem_insertIfNew`. -/
theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
a m.insertIfNew k v ¬((a == k) ¬k m) a m :=
a m.insertIfNew k v ¬((k == a) ¬k m) a m :=
DHashMap.mem_of_mem_insertIfNew'
theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
@@ -411,21 +411,21 @@ theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v :
DHashMap.size_le_size_insertIfNew
theorem getElem?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insertIfNew k v)[a]? = bif a == k && !m.contains k then some v else m[a]? :=
(m.insertIfNew k v)[a]? = bif k == a && !m.contains k then some v else m[a]? :=
DHashMap.Const.get?_insertIfNew
theorem getElem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
(m.insertIfNew k v)[a]'h₁ =
if h₂ : a == k ¬k m then v else m[a]'(mem_of_mem_insertIfNew' h₁ h₂) :=
if h₂ : k == a ¬k m then v else m[a]'(mem_of_mem_insertIfNew' h₁ h₂) :=
DHashMap.Const.get_insertIfNew (h₁ := h₁)
theorem getElem!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
(m.insertIfNew k v)[a]! = bif a == k && !m.contains k then v else m[a]! :=
(m.insertIfNew k v)[a]! = bif k == a && !m.contains k then v else m[a]! :=
DHashMap.Const.get!_insertIfNew
theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
(m.insertIfNew k v).getD a fallback =
bif a == k && !m.contains k then v else m.getD a fallback :=
bif k == a && !m.contains k then v else m.getD a fallback :=
DHashMap.Const.getD_insertIfNew
@[simp]

View File

@@ -37,17 +37,20 @@ inductive types. The well-formedness invariant is called `Raw.WF`. When in doubt
over `HashMap.Raw`. Lemmas about the operations on `Std.Data.HashMap.Raw` are available in the
module `Std.Data.HashMap.RawLemmas`.
This is a simple separate-chaining hash table. The data of the hash map consists of a cached size
and an array of buckets, where each bucket is a linked list of key-value pais. The number of buckets
is always a power of two. The hash map doubles its size upon inserting an element such that the
number of elements is more than 75% of the number of buckets.
The hash table is backed by an `Array`. Users should make sure that the hash map is used linearly to
avoid expensive copies.
The hash map uses `==` (provided by the `BEq` typeclass) to compare keys and `hash` (provided by
the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
`EquivBEq` and `LawfulHashable` typeclasses). Both of these conditions are automatic if the BEq
instance is lawful, i.e., if `a == b` implies `a = b`.
This is a simple separate-chaining hash table. The data of the hash map consists of a cached size
and an array of buckets, where each bucket is a linked list of key-value pais. The number of buckets
is always a power of two. The hash map doubles its size upon inserting an element such that the
number of elements is more than 75% of the number of buckets.
Dependent hash maps, in which keys may occur in their values' types, are available as
`Std.Data.Raw.DHashMap`.
-/

View File

@@ -72,20 +72,20 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
@[simp]
theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insert k v).contains a = (a == k || m.contains a) :=
(m.insert k v).contains a = (k == a || m.contains a) :=
DHashMap.Raw.contains_insert h.out
@[simp]
theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
a m.insert k v a == k a m :=
a m.insert k v k == a a m :=
DHashMap.Raw.mem_insert h.out
theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insert k v).contains a (a == k) = false m.contains a :=
(m.insert k v).contains a (k == a) = false m.contains a :=
DHashMap.Raw.contains_of_contains_insert h.out
theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
a m.insert k v (a == k) = false a m :=
a m.insert k v (k == a) = false a m :=
DHashMap.Raw.mem_of_mem_insert h.out
@[simp]
@@ -131,12 +131,12 @@ theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} :
@[simp]
theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k).contains a = (!(a == k) && m.contains a) :=
(m.erase k).contains a = (!(k == a) && m.contains a) :=
DHashMap.Raw.contains_erase h.out
@[simp]
theorem mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
a m.erase k (a == k) = false a m :=
a m.erase k (k == a) = false a m :=
DHashMap.Raw.mem_erase h.out
theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
@@ -184,7 +184,7 @@ theorem getElem?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
DHashMap.Raw.Const.get?_of_isEmpty h.out
theorem getElem?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insert k v)[a]? = bif a == k then some v else m[a]? :=
(m.insert k v)[a]? = bif k == a then some v else m[a]? :=
DHashMap.Raw.Const.get?_insert h.out
@[simp]
@@ -204,7 +204,7 @@ theorem getElem?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m
DHashMap.Raw.Const.get?_eq_none h.out
theorem getElem?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k)[a]? = bif a == k then none else m[a]? :=
(m.erase k)[a]? = bif k == a then none else m[a]? :=
DHashMap.Raw.Const.get?_erase h.out
@[simp]
@@ -216,7 +216,7 @@ theorem getElem?_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a ==
theorem getElem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
(m.insert k v)[a]'h₁ =
if h₂ : a == k then v else m[a]'(mem_of_mem_insert h h₁ (Bool.eq_false_iff.2 h₂)) :=
if h₂ : k == a then v else m[a]'(mem_of_mem_insert h h₁ (Bool.eq_false_iff.2 h₂)) :=
DHashMap.Raw.Const.get_insert (h₁ := h₁) h.out
@[simp]
@@ -250,7 +250,7 @@ theorem getElem!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a
DHashMap.Raw.Const.get!_of_isEmpty h.out
theorem getElem!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
(m.insert k v)[a]! = bif a == k then v else m[a]! :=
(m.insert k v)[a]! = bif k == a then v else m[a]! :=
DHashMap.Raw.Const.get!_insert h.out
@[simp]
@@ -267,7 +267,7 @@ theorem getElem!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a
DHashMap.Raw.Const.get!_eq_default h.out
theorem getElem!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
(m.erase k)[a]! = bif a == k then default else m[a]! :=
(m.erase k)[a]! = bif k == a then default else m[a]! :=
DHashMap.Raw.Const.get!_erase h.out
@[simp]
@@ -308,7 +308,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
DHashMap.Raw.Const.getD_of_isEmpty h.out
theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
(m.insert k v).getD a fallback = bif a == k then v else m.getD a fallback :=
(m.insert k v).getD a fallback = bif k == a then v else m.getD a fallback :=
DHashMap.Raw.Const.getD_insert h.out
@[simp]
@@ -325,7 +325,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
DHashMap.Raw.Const.getD_eq_fallback h.out
theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
(m.erase k).getD a fallback = bif a == k then fallback else m.getD a fallback :=
(m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback :=
DHashMap.Raw.Const.getD_erase h.out
@[simp]
@@ -364,12 +364,12 @@ theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β}
@[simp]
theorem contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insertIfNew k v).contains a = (a == k || m.contains a) :=
(m.insertIfNew k v).contains a = (k == a || m.contains a) :=
DHashMap.Raw.contains_insertIfNew h.out
@[simp]
theorem mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
a m.insertIfNew k v a == k a m :=
a m.insertIfNew k v k == a a m :=
DHashMap.Raw.mem_insertIfNew h.out
theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
@@ -381,23 +381,23 @@ theorem mem_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β}
DHashMap.Raw.mem_insertIfNew_self h.out
theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insertIfNew k v).contains a (a == k) = false m.contains a :=
(m.insertIfNew k v).contains a (k == a) = false m.contains a :=
DHashMap.Raw.contains_of_contains_insertIfNew h.out
theorem mem_of_mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
a m.insertIfNew k v (a == k) = false a m :=
a m.insertIfNew k v (k == a) = false a m :=
DHashMap.Raw.mem_of_mem_insertIfNew h.out
/-- This is a restatement of `contains_insertIfNew` that is written to exactly match the proof
obligation in the statement of `getElem_insertIfNew`. -/
theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insertIfNew k v).contains a ¬((a == k) m.contains k = false) m.contains a :=
(m.insertIfNew k v).contains a ¬((k == a) m.contains k = false) m.contains a :=
DHashMap.Raw.contains_of_contains_insertIfNew' h.out
/-- This is a restatement of `mem_insertIfNew` that is written to exactly match the proof obligation
in the statement of `getElem_insertIfNew`. -/
theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
a m.insertIfNew k v ¬((a == k) ¬k m) a m :=
a m.insertIfNew k v ¬((k == a) ¬k m) a m :=
DHashMap.Raw.mem_of_mem_insertIfNew' h.out
theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
@@ -409,21 +409,21 @@ theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v :
DHashMap.Raw.size_le_size_insertIfNew h.out
theorem getElem?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insertIfNew k v)[a]? = bif a == k && !m.contains k then some v else m[a]? :=
(m.insertIfNew k v)[a]? = bif k == a && !m.contains k then some v else m[a]? :=
DHashMap.Raw.Const.get?_insertIfNew h.out
theorem getElem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
(m.insertIfNew k v)[a]'h₁ =
if h₂ : a == k ¬k m then v else m[a]'(mem_of_mem_insertIfNew' h h₁ h₂) :=
if h₂ : k == a ¬k m then v else m[a]'(mem_of_mem_insertIfNew' h h₁ h₂) :=
DHashMap.Raw.Const.get_insertIfNew h.out (h₁ := h₁)
theorem getElem!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
(m.insertIfNew k v)[a]! = bif a == k && !m.contains k then v else m[a]! :=
(m.insertIfNew k v)[a]! = bif k == a && !m.contains k then v else m[a]! :=
DHashMap.Raw.Const.get!_insertIfNew h.out
theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
(m.insertIfNew k v).getD a fallback =
bif a == k && !m.contains k then v else m.getD a fallback :=
bif k == a && !m.contains k then v else m.getD a fallback :=
DHashMap.Raw.Const.getD_insertIfNew h.out
@[simp]

View File

@@ -23,7 +23,7 @@ set_option autoImplicit false
universe u v
variable {α : Type u}
variable {α : Type u} {_ : BEq α} {_ : Hashable α}
namespace Std
@@ -35,6 +35,9 @@ and an array of buckets, where each bucket is a linked list of keys. The number
is always a power of two. The hash set doubles its size upon inserting an element such that the
number of elements is more than 75% of the number of buckets.
The hash table is backed by an `Array`. Users should make sure that the hash set is used linearly to
avoid expensive copies.
The hash set uses `==` (provided by the `BEq` typeclass) to compare elements and `hash` (provided by
the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
@@ -71,7 +74,7 @@ instance [BEq α] [Hashable α] : Inhabited (HashSet α) where
Inserts the given element into the set. If the hash set already contains an element that is
equal (with regard to `==`) to the given element, then the hash set is returned unchanged.
-/
@[inline] def insert [BEq α] [Hashable α] (m : HashSet α) (a : α) : HashSet α :=
@[inline] def insert (m : HashSet α) (a : α) : HashSet α :=
m.inner.insertIfNew a ()
/--
@@ -81,7 +84,7 @@ element, then the hash set is returned unchanged.
Equivalent to (but potentially faster than) calling `contains` followed by `insert`.
-/
@[inline] def containsThenInsert [BEq α] [Hashable α] (m : HashSet α) (a : α) : Bool × HashSet α :=
@[inline] def containsThenInsert (m : HashSet α) (a : α) : Bool × HashSet α :=
let replaced, r := m.inner.containsThenInsertIfNew a ()
replaced, r
@@ -92,7 +95,7 @@ this: `a ∈ m` is equivalent to `m.contains a = true`.
Observe that this is different behavior than for lists: for lists, `∈` uses `=` and `contains` use
`==` for comparisons, while for hash sets, both use `==`.
-/
@[inline] def contains [BEq α] [Hashable α] (m : HashSet α) (a : α) : Bool :=
@[inline] def contains (m : HashSet α) (a : α) : Bool :=
m.inner.contains a
instance [BEq α] [Hashable α] : Membership α (HashSet α) where
@@ -102,11 +105,11 @@ instance [BEq α] [Hashable α] {m : HashSet α} {a : α} : Decidable (a ∈ m)
inferInstanceAs (Decidable (a m.inner))
/-- Removes the element if it exists. -/
@[inline] def erase [BEq α] [Hashable α] (m : HashSet α) (a : α) : HashSet α :=
@[inline] def erase (m : HashSet α) (a : α) : HashSet α :=
m.inner.erase a
/-- The number of elements present in the set -/
@[inline] def size [BEq α] [Hashable α] (m : HashSet α) : Nat :=
@[inline] def size (m : HashSet α) : Nat :=
m.inner.size
/--
@@ -116,7 +119,7 @@ Note that if your `BEq` instance is not reflexive or your `Hashable` instance is
lawful, then it is possible that this function returns `false` even though `m.contains a = false`
for all `a`.
-/
@[inline] def isEmpty [BEq α] [Hashable α] (m : HashSet α) : Bool :=
@[inline] def isEmpty (m : HashSet α) : Bool :=
m.inner.isEmpty
section Unverified
@@ -124,29 +127,29 @@ section Unverified
/-! We currently do not provide lemmas for the functions below. -/
/-- Removes all elements from the hash set for which the given function returns `false`. -/
@[inline] def filter [BEq α] [Hashable α] (f : α Bool) (m : HashSet α) : HashSet α :=
@[inline] def filter (f : α Bool) (m : HashSet α) : HashSet α :=
m.inner.filter fun a _ => f a
/--
Monadically computes a value by folding the given function over the elements in the hash set in some
order.
-/
@[inline] def foldM [BEq α] [Hashable α] {m : Type v Type v} [Monad m] {β : Type v}
@[inline] def foldM {m : Type v Type v} [Monad m] {β : Type v}
(f : β α m β) (init : β) (b : HashSet α) : m β :=
b.inner.foldM (fun b a _ => f b a) init
/-- Folds the given function over the elements of the hash set in some order. -/
@[inline] def fold [BEq α] [Hashable α] {β : Type v} (f : β α β) (init : β) (m : HashSet α) :
@[inline] def fold {β : Type v} (f : β α β) (init : β) (m : HashSet α) :
β :=
m.inner.fold (fun b a _ => f b a) init
/-- Carries out a monadic action on each element in the hash set in some order. -/
@[inline] def forM [BEq α] [Hashable α] {m : Type v Type v} [Monad m] (f : α m PUnit)
@[inline] def forM {m : Type v Type v} [Monad m] (f : α m PUnit)
(b : HashSet α) : m PUnit :=
b.inner.forM (fun a _ => f a)
/-- Support for the `for` loop construct in `do` blocks. -/
@[inline] def forIn [BEq α] [Hashable α] {m : Type v Type v} [Monad m] {β : Type v}
@[inline] def forIn {m : Type v Type v} [Monad m] {β : Type v}
(f : α β m (ForInStep β)) (init : β) (b : HashSet α) : m β :=
b.inner.forIn (fun a _ acc => f a acc) init
@@ -157,11 +160,11 @@ instance [BEq α] [Hashable α] {m : Type v → Type v} : ForIn m (HashSet α)
forIn m init f := m.forIn f init
/-- Transforms the hash set into a list of elements in some order. -/
@[inline] def toList [BEq α] [Hashable α] (m : HashSet α) : List α :=
@[inline] def toList (m : HashSet α) : List α :=
m.inner.keys
/-- Transforms the hash set into an array of elements in some order. -/
@[inline] def toArray [BEq α] [Hashable α] (m : HashSet α) : Array α :=
@[inline] def toArray (m : HashSet α) : Array α :=
m.inner.keysArray
/--
@@ -169,7 +172,7 @@ Inserts multiple elements into the hash set. Note that unlike repeatedly calling
collection contains multiple elements that are equal (with regard to `==`), then the last element
in the collection will be present in the returned hash set.
-/
@[inline] def insertMany [BEq α] [Hashable α] {ρ : Type v} [ForIn Id ρ α] (m : HashSet α) (l : ρ) :
@[inline] def insertMany {ρ : Type v} [ForIn Id ρ α] (m : HashSet α) (l : ρ) :
HashSet α :=
m.inner.insertManyUnit l
@@ -186,7 +189,7 @@ Returns the number of buckets in the internal representation of the hash set. Th
be useful for things like monitoring system health, but it should be considered an internal
implementation detail.
-/
def Internal.numBuckets [BEq α] [Hashable α] (m : HashSet α) : Nat :=
def Internal.numBuckets (m : HashSet α) : Nat :=
HashMap.Internal.numBuckets m.inner
instance [BEq α] [Hashable α] [Repr α] : Repr (HashSet α) where

View File

@@ -20,7 +20,7 @@ set_option autoImplicit false
universe u v
variable {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
variable {α : Type u} {_ : BEq α} {_ : Hashable α} [EquivBEq α] [LawfulHashable α]
namespace Std.HashSet
@@ -67,19 +67,19 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
@[simp]
theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.insert k).contains a = (a == k || m.contains a) :=
(m.insert k).contains a = (k == a || m.contains a) :=
HashMap.contains_insertIfNew
@[simp]
theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} : a m.insert k a == k a m :=
theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} : a m.insert k k == a a m :=
HashMap.mem_insertIfNew
theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.insert k).contains a (a == k) = false m.contains a :=
(m.insert k).contains a (k == a) = false m.contains a :=
HashMap.contains_of_contains_insertIfNew
theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
a m.insert k (a == k) = false a m :=
a m.insert k (k == a) = false a m :=
HashMap.mem_of_mem_insertIfNew
@[simp]
@@ -123,12 +123,12 @@ theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} :
@[simp]
theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k).contains a = (!(a == k) && m.contains a) :=
(m.erase k).contains a = (!(k == a) && m.contains a) :=
HashMap.contains_erase
@[simp]
theorem mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
a m.erase k (a == k) = false a m :=
a m.erase k (k == a) = false a m :=
HashMap.mem_erase
theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :

View File

@@ -37,16 +37,19 @@ inductive types. The well-formedness invariant is called `Raw.WF`. When in doubt
over `HashSet.Raw`. Lemmas about the operations on `Std.Data.HashSet.Raw` are available in the
module `Std.Data.HashSet.RawLemmas`.
This is a simple separate-chaining hash table. The data of the hash set consists of a cached size
and an array of buckets, where each bucket is a linked list of keys. The number of buckets
is always a power of two. The hash set doubles its size upon inserting an element such that the
number of elements is more than 75% of the number of buckets.
The hash table is backed by an `Array`. Users should make sure that the hash set is used linearly to
avoid expensive copies.
The hash set uses `==` (provided by the `BEq` typeclass) to compare elements and `hash` (provided by
the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
`EquivBEq` and `LawfulHashable` typeclasses). Both of these conditions are automatic if the BEq
instance is lawful, i.e., if `a == b` implies `a = b`.
This is a simple separate-chaining hash table. The data of the hash set consists of a cached size
and an array of buckets, where each bucket is a linked list of keys. The number of buckets
is always a power of two. The hash set doubles its size upon inserting an element such that the
number of elements is more than 75% of the number of buckets.
-/
structure Raw (α : Type u) where
/-- Internal implementation detail of the hash set. -/

View File

@@ -67,19 +67,19 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
@[simp]
theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.insert k).contains a = (a == k || m.contains a) :=
(m.insert k).contains a = (k == a || m.contains a) :=
HashMap.Raw.contains_insertIfNew h.out
@[simp]
theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} : a m.insert k a == k a m :=
theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} : a m.insert k k == a a m :=
HashMap.Raw.mem_insertIfNew h.out
theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.insert k).contains a (a == k) = false m.contains a :=
(m.insert k).contains a (k == a) = false m.contains a :=
HashMap.Raw.contains_of_contains_insertIfNew h.out
theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
a m.insert k (a == k) = false a m :=
a m.insert k (k == a) = false a m :=
HashMap.Raw.mem_of_mem_insertIfNew h.out
@[simp]
@@ -123,12 +123,12 @@ theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} :
@[simp]
theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k).contains a = (!(a == k) && m.contains a) :=
(m.erase k).contains a = (!(k == a) && m.contains a) :=
HashMap.Raw.contains_erase h.out
@[simp]
theorem mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
a m.erase k (a == k) = false a m :=
a m.erase k (k == a) = false a m :=
HashMap.Raw.mem_erase h.out
theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :

View File

@@ -448,9 +448,6 @@ static inline void lean_inc(lean_object * o) { if (!lean_is_scalar(o)) lean_inc_
static inline void lean_inc_n(lean_object * o, size_t n) { if (!lean_is_scalar(o)) lean_inc_ref_n(o, n); }
static inline void lean_dec(lean_object * o) { if (!lean_is_scalar(o)) lean_dec_ref(o); }
/* Just free memory */
LEAN_EXPORT void lean_dealloc(lean_object * o);
static inline bool lean_is_ctor(lean_object * o) { return lean_ptr_tag(o) <= LeanMaxCtorTag; }
static inline bool lean_is_closure(lean_object * o) { return lean_ptr_tag(o) == LeanClosure; }
static inline bool lean_is_array(lean_object * o) { return lean_ptr_tag(o) == LeanArray; }
@@ -484,6 +481,10 @@ static inline bool lean_is_exclusive(lean_object * o) {
}
}
static inline uint8_t lean_is_exclusive_obj(lean_object * o) {
return lean_is_exclusive(o);
}
static inline bool lean_is_shared(lean_object * o) {
if (LEAN_LIKELY(lean_is_st(o))) {
return o->m_rc > 1;
@@ -1136,6 +1137,17 @@ static inline void * lean_get_external_data(lean_object * o) {
return lean_to_external(o)->m_data;
}
static inline lean_object * lean_set_external_data(lean_object * o, void * data) {
if (lean_is_exclusive(o)) {
lean_to_external(o)->m_data = data;
return o;
} else {
lean_object * o_new = lean_alloc_external(lean_get_external_class(o), data);
lean_dec_ref(o);
return o_new;
}
}
/* Natural numbers */
#define LEAN_MAX_SMALL_NAT (SIZE_MAX >> 1)

View File

@@ -1,41 +0,0 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <vector>
#include <memory>
#include "runtime/debug.h"
/** \brief Macro for creating a stack of objects of type Cache in thread local storage.
The argument \c Arg is provided to every new instance of Cache.
The macro provides the helper class Cache_ref that "reuses" cache objects from the stack.
*/
#define MK_CACHE_STACK(Cache, Arg) \
struct Cache ## _stack { \
unsigned m_top; \
std::vector<std::unique_ptr<Cache>> m_cache_stack; \
Cache ## _stack():m_top(0) {} \
}; \
MK_THREAD_LOCAL_GET_DEF(Cache ## _stack, get_ ## Cache ## _stack); \
class Cache ## _ref { \
Cache * m_cache; \
public: \
Cache ## _ref() { \
Cache ## _stack & s = get_ ## Cache ## _stack(); \
lean_assert(s.m_top <= s.m_cache_stack.size()); \
if (s.m_top == s.m_cache_stack.size()) \
s.m_cache_stack.push_back(std::unique_ptr<Cache>(new Cache(Arg))); \
m_cache = s.m_cache_stack[s.m_top].get(); \
s.m_top++; \
} \
~Cache ## _ref() { \
Cache ## _stack & s = get_ ## Cache ## _stack(); \
lean_assert(s.m_top > 0); \
s.m_top--; \
m_cache->clear(); \
} \
Cache * operator->() const { return m_cache; } \
};

View File

@@ -161,7 +161,7 @@ bool declaration::is_unsafe() const {
bool use_unsafe(environment const & env, expr const & e) {
bool found = false;
for_each(e, [&](expr const & e, unsigned) {
for_each(e, [&](expr const & e) {
if (found) return false;
if (is_constant(e)) {
if (auto info = env.find(const_name(e))) {
@@ -181,7 +181,7 @@ declaration::declaration():declaration(*g_dummy) {}
static unsigned get_max_height(environment const & env, expr const & v) {
unsigned h = 0;
for_each(v, [&](expr const & e, unsigned) {
for_each(v, [&](expr const & e) {
if (is_constant(e)) {
auto d = env.find(const_name(e));
if (d && d->get_hints().get_height() > h)

View File

@@ -498,7 +498,7 @@ optional<expr> has_expr_metavar_strict(expr const & e) {
if (!has_expr_metavar(e))
return none_expr();
optional<expr> r;
for_each(e, [&](expr const & e, unsigned) {
for_each(e, [&](expr const & e) {
if (r || !has_expr_metavar(e)) return false;
if (is_metavar_app(e)) { r = e; return false; }
return true;

View File

@@ -5,119 +5,221 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <vector>
#include <unordered_map>
#include <utility>
#include "runtime/memory.h"
#include "runtime/interrupt.h"
#include "runtime/flet.h"
#include "kernel/for_each_fn.h"
#include "kernel/cache_stack.h"
#ifndef LEAN_DEFAULT_FOR_EACH_CACHE_CAPACITY
#define LEAN_DEFAULT_FOR_EACH_CACHE_CAPACITY 1024*8
#endif
namespace lean {
struct for_each_cache {
struct entry {
object const * m_cell;
unsigned m_offset;
entry():m_cell(nullptr) {}
};
unsigned m_capacity;
std::vector<entry> m_cache;
std::vector<unsigned> m_used;
for_each_cache(unsigned c):m_capacity(c), m_cache(c) {}
bool visited(expr const & e, unsigned offset) {
unsigned i = hash(hash(e), offset) % m_capacity;
if (m_cache[i].m_cell == e.raw() && m_cache[i].m_offset == offset) {
return true;
/*
If `partial_apps = true`, then given a term `g a b`, we also apply the function `m_f` to `g a`,
and not only to `g`, `a`, and `b`.
*/
template<bool partial_apps> class for_each_fn {
std::unordered_set<lean_object *> m_cache;
std::function<bool(expr const &)> m_f; // NOLINT
bool visited(expr const & e) {
if (!is_shared(e)) return false;
if (m_cache.find(e.raw()) != m_cache.end()) return true;
m_cache.insert(e.raw());
return false;
}
void apply_fn(expr const & e) {
if (is_app(e)) {
apply_fn(app_fn(e));
apply(app_arg(e));
} else {
if (m_cache[i].m_cell == nullptr)
m_used.push_back(i);
m_cache[i].m_cell = e.raw();
m_cache[i].m_offset = offset;
return false;
apply(e);
}
}
void clear() {
for (unsigned i : m_used)
m_cache[i].m_cell = nullptr;
m_used.clear();
}
};
void apply(expr const & e) {
switch (e.kind()) {
case expr_kind::Const: case expr_kind::BVar: case expr_kind::Sort:
m_f(e);
return;
default:
break;
}
/* CACHE_RESET: NO */
MK_CACHE_STACK(for_each_cache, LEAN_DEFAULT_FOR_EACH_CACHE_CAPACITY)
if (visited(e))
return;
class for_each_fn {
for_each_cache_ref m_cache;
std::function<bool(expr const &, unsigned)> m_f; // NOLINT
if (!m_f(e))
return;
void apply(expr const & e, unsigned offset) {
buffer<pair<expr const &, unsigned>> todo;
todo.emplace_back(e, offset);
while (true) {
begin_loop:
if (todo.empty())
break;
check_memory("expression traversal");
auto p = todo.back();
todo.pop_back();
expr const & e = p.first;
unsigned offset = p.second;
switch (e.kind()) {
case expr_kind::Const: case expr_kind::BVar:
case expr_kind::Sort:
m_f(e, offset);
goto begin_loop;
default:
break;
}
if (is_shared(e) && m_cache->visited(e, offset))
goto begin_loop;
if (!m_f(e, offset))
goto begin_loop;
switch (e.kind()) {
case expr_kind::Const: case expr_kind::BVar:
case expr_kind::Sort: case expr_kind::Lit:
case expr_kind::MVar: case expr_kind::FVar:
goto begin_loop;
case expr_kind::MData:
todo.emplace_back(mdata_expr(e), offset);
goto begin_loop;
case expr_kind::Proj:
todo.emplace_back(proj_expr(e), offset);
goto begin_loop;
case expr_kind::App:
todo.emplace_back(app_arg(e), offset);
todo.emplace_back(app_fn(e), offset);
goto begin_loop;
case expr_kind::Lambda: case expr_kind::Pi:
todo.emplace_back(binding_body(e), offset + 1);
todo.emplace_back(binding_domain(e), offset);
goto begin_loop;
case expr_kind::Let:
todo.emplace_back(let_body(e), offset + 1);
todo.emplace_back(let_value(e), offset);
todo.emplace_back(let_type(e), offset);
goto begin_loop;
}
switch (e.kind()) {
case expr_kind::Const: case expr_kind::BVar:
case expr_kind::Sort: case expr_kind::Lit:
case expr_kind::MVar: case expr_kind::FVar:
return;
case expr_kind::MData:
apply(mdata_expr(e));
return;
case expr_kind::Proj:
apply(proj_expr(e));
return;
case expr_kind::App:
if (partial_apps)
apply(app_fn(e));
else
apply_fn(app_fn(e));
apply(app_arg(e));
return;
case expr_kind::Lambda: case expr_kind::Pi:
apply(binding_domain(e));
apply(binding_body(e));
return;
case expr_kind::Let:
apply(let_type(e));
apply(let_value(e));
apply(let_body(e));
return;
}
}
public:
for_each_fn(std::function<bool(expr const &, unsigned)> && f):m_f(f) {} // NOLINT
for_each_fn(std::function<bool(expr const &, unsigned)> const & f):m_f(f) {} // NOLINT
for_each_fn(std::function<bool(expr const &)> && f):m_f(f) {} // NOLINT
for_each_fn(std::function<bool(expr const &)> const & f):m_f(f) {} // NOLINT
void operator()(expr const & e) { apply(e); }
};
class for_each_offset_fn {
struct key_hasher {
std::size_t operator()(std::pair<lean_object *, unsigned> const & p) const {
return hash((size_t)p.first, p.second);
}
};
std::unordered_set<std::pair<lean_object *, unsigned>, key_hasher> m_cache;
std::function<bool(expr const &, unsigned)> m_f; // NOLINT
bool visited(expr const & e, unsigned offset) {
if (!is_shared(e)) return false;
if (m_cache.find(std::make_pair(e.raw(), offset)) != m_cache.end()) return true;
m_cache.insert(std::make_pair(e.raw(), offset));
return false;
}
void apply(expr const & e, unsigned offset) {
switch (e.kind()) {
case expr_kind::Const: case expr_kind::BVar: case expr_kind::Sort:
m_f(e, offset);
return;
default:
break;
}
if (visited(e, offset))
return;
if (!m_f(e, offset))
return;
switch (e.kind()) {
case expr_kind::Const: case expr_kind::BVar:
case expr_kind::Sort: case expr_kind::Lit:
case expr_kind::MVar: case expr_kind::FVar:
return;
case expr_kind::MData:
apply(mdata_expr(e), offset);
return;
case expr_kind::Proj:
apply(proj_expr(e), offset);
return;
case expr_kind::App:
apply(app_fn(e), offset);
apply(app_arg(e), offset);
return;
case expr_kind::Lambda: case expr_kind::Pi:
apply(binding_domain(e), offset);
apply(binding_body(e), offset+1);
return;
case expr_kind::Let:
apply(let_type(e), offset);
apply(let_value(e), offset);
apply(let_body(e), offset+1);
return;
}
}
public:
for_each_offset_fn(std::function<bool(expr const &, unsigned)> && f):m_f(f) {} // NOLINT
for_each_offset_fn(std::function<bool(expr const &, unsigned)> const & f):m_f(f) {} // NOLINT
void operator()(expr const & e) { apply(e, 0); }
};
void for_each(expr const & e, std::function<bool(expr const &)> && f) { // NOLINT
return for_each_fn<true>(f)(e);
}
void for_each(expr const & e, std::function<bool(expr const &, unsigned)> && f) { // NOLINT
return for_each_fn(f)(e);
return for_each_offset_fn(f)(e);
}
extern "C" LEAN_EXPORT obj_res lean_find_expr(b_obj_arg p, b_obj_arg e_) {
lean_object * found = nullptr;
expr const & e = TO_REF(expr, e_);
for_each_fn<true>([&](expr const & e) {
if (found != nullptr) return false;
lean_inc(p);
lean_inc(e.raw());
if (lean_unbox(lean_apply_1(p, e.raw()))) {
found = e.raw();
return false;
}
return true;
})(e);
if (found) {
lean_inc(found);
lean_object * r = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(r, 0, found);
return r;
} else {
return lean_box(0);
}
}
/*
Similar to `lean_find_expr`, but `p` returns
```
inductive FindStep where
/-- Found desired subterm -/ | found
/-- Search subterms -/ | visit
/-- Do not search subterms -/ | done
```
*/
extern "C" LEAN_EXPORT obj_res lean_find_ext_expr(b_obj_arg p, b_obj_arg e_) {
lean_object * found = nullptr;
expr const & e = TO_REF(expr, e_);
// Recall that `findExt?` skips partial applications.
for_each_fn<false>([&](expr const & e) {
if (found != nullptr) return false;
lean_inc(p);
lean_inc(e.raw());
switch(lean_unbox(lean_apply_1(p, e.raw()))) {
case 0: // found
found = e.raw();
return false;
case 1: // visit
return true;
case 2: // done
return false;
default:
lean_unreachable();
}
})(e);
if (found) {
lean_inc(found);
lean_object * r = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(r, 0, found);
return r;
} else {
return lean_box(0);
}
}
}

View File

@@ -13,15 +13,18 @@ Author: Leonardo de Moura
#include "kernel/expr_sets.h"
namespace lean {
/** \brief Expression visitor.
/**
\brief Expression visitor.
The argument \c f must be a lambda (function object) containing the method
The argument \c f must be a lambda (function object) containing the method
<code>
bool operator()(expr const & e, unsigned offset)
</code>
<code>
bool operator()(expr const & e, unsigned offset)
</code>
The \c offset is the number of binders under which \c e occurs.
The \c offset is the number of binders under which \c e occurs.
*/
void for_each(expr const & e, std::function<bool(expr const &, unsigned)> && f); // NOLINT
void for_each(expr const & e, std::function<bool(expr const &)> && f); // NOLINT
}

View File

@@ -6,75 +6,35 @@ Author: Leonardo de Moura
*/
#include <vector>
#include <memory>
#include <unordered_map>
#include "kernel/replace_fn.h"
#include "kernel/cache_stack.h"
#ifndef LEAN_DEFAULT_REPLACE_CACHE_CAPACITY
#define LEAN_DEFAULT_REPLACE_CACHE_CAPACITY 1024*8
#endif
namespace lean {
struct replace_cache {
struct entry {
object * m_cell;
unsigned m_offset;
expr m_result;
entry():m_cell(nullptr) {}
};
unsigned m_capacity;
std::vector<entry> m_cache;
std::vector<unsigned> m_used;
replace_cache(unsigned c):m_capacity(c), m_cache(c) {}
expr * find(expr const & e, unsigned offset) {
unsigned i = hash(hash(e), offset) % m_capacity;
if (m_cache[i].m_cell == e.raw() && m_cache[i].m_offset == offset)
return &m_cache[i].m_result;
else
return nullptr;
}
void insert(expr const & e, unsigned offset, expr const & v) {
unsigned i = hash(hash(e), offset) % m_capacity;
if (m_cache[i].m_cell == nullptr)
m_used.push_back(i);
m_cache[i].m_cell = e.raw();
m_cache[i].m_offset = offset;
m_cache[i].m_result = v;
}
void clear() {
for (unsigned i : m_used) {
m_cache[i].m_cell = nullptr;
m_cache[i].m_result = expr();
}
m_used.clear();
}
};
/* CACHE_RESET: NO */
MK_CACHE_STACK(replace_cache, LEAN_DEFAULT_REPLACE_CACHE_CAPACITY)
class replace_rec_fn {
replace_cache_ref m_cache;
struct key_hasher {
std::size_t operator()(std::pair<lean_object *, unsigned> const & p) const {
return hash((size_t)p.first, p.second);
}
};
std::unordered_map<std::pair<lean_object *, unsigned>, expr, key_hasher> m_cache;
std::function<optional<expr>(expr const &, unsigned)> m_f;
bool m_use_cache;
expr save_result(expr const & e, unsigned offset, expr const & r, bool shared) {
if (shared)
m_cache->insert(e, offset, r);
m_cache.insert(mk_pair(mk_pair(e.raw(), offset), r));
return r;
}
expr apply(expr const & e, unsigned offset) {
bool shared = false;
if (m_use_cache && is_shared(e)) {
if (auto r = m_cache->find(e, offset))
return *r;
auto it = m_cache.find(mk_pair(e.raw(), offset));
if (it != m_cache.end())
return it->second;
shared = true;
}
check_system("replace");
if (optional<expr> r = m_f(e, offset)) {
return save_result(e, offset, *r, shared);
} else {
@@ -121,4 +81,73 @@ public:
expr replace(expr const & e, std::function<optional<expr>(expr const &, unsigned)> const & f, bool use_cache) {
return replace_rec_fn(f, use_cache)(e);
}
class replace_fn {
std::unordered_map<lean_object *, expr> m_cache;
lean_object * m_f;
expr save_result(expr const & e, expr const & r, bool shared) {
if (shared)
m_cache.insert(mk_pair(e.raw(), r));
return r;
}
expr apply(expr const & e) {
bool shared = false;
if (is_shared(e)) {
auto it = m_cache.find(e.raw());
if (it != m_cache.end())
return it->second;
shared = true;
}
lean_inc(e.raw());
lean_inc_ref(m_f);
lean_object * r = lean_apply_1(m_f, e.raw());
if (!lean_is_scalar(r)) {
expr e_new(lean_ctor_get(r, 0), true);
lean_dec_ref(r);
return save_result(e, e_new, shared);
}
switch (e.kind()) {
case expr_kind::Const: case expr_kind::Sort:
case expr_kind::BVar: case expr_kind::Lit:
case expr_kind::MVar: case expr_kind::FVar:
return save_result(e, e, shared);
case expr_kind::MData: {
expr new_e = apply(mdata_expr(e));
return save_result(e, update_mdata(e, new_e), shared);
}
case expr_kind::Proj: {
expr new_e = apply(proj_expr(e));
return save_result(e, update_proj(e, new_e), shared);
}
case expr_kind::App: {
expr new_f = apply(app_fn(e));
expr new_a = apply(app_arg(e));
return save_result(e, update_app(e, new_f, new_a), shared);
}
case expr_kind::Pi: case expr_kind::Lambda: {
expr new_d = apply(binding_domain(e));
expr new_b = apply(binding_body(e));
return save_result(e, update_binding(e, new_d, new_b), shared);
}
case expr_kind::Let: {
expr new_t = apply(let_type(e));
expr new_v = apply(let_value(e));
expr new_b = apply(let_body(e));
return save_result(e, update_let(e, new_t, new_v, new_b), shared);
}}
lean_unreachable();
}
public:
replace_fn(lean_object * f):m_f(f) {}
expr operator()(expr const & e) { return apply(e); }
};
extern "C" LEAN_EXPORT obj_res lean_replace_expr(b_obj_arg f, b_obj_arg e) {
expr r = replace_fn(f)(TO_REF(expr, e));
return r.steal();
}
}

View File

@@ -185,7 +185,7 @@ expr type_checker::infer_app(expr const & e, bool infer_only) {
static void mark_used(unsigned n, expr const * fvars, expr const & b, bool * used) {
if (!has_fvar(b)) return;
for_each(b, [&](expr const & x, unsigned) {
for_each(b, [&](expr const & x) {
if (!has_fvar(x)) return false;
if (is_fvar(x)) {
for (unsigned i = 0; i < n; i++) {

View File

@@ -6,6 +6,8 @@ Author: Leonardo de Moura
*/
#include <vector>
#include <cstring>
#include <unordered_map>
#include <unordered_set>
#include "runtime/object.h"
#include "runtime/hash.h"
@@ -268,4 +270,177 @@ public:
extern "C" LEAN_EXPORT obj_res lean_state_sharecommon(b_obj_arg tc, obj_arg s, obj_arg a) {
return sharecommon_fn(tc, s)(a);
}
/*
A faster version of `sharecommon_fn` which only uses a local state.
It optimizes the number of RC operations, the strategy for caching results,
and uses C++ hashmap.
*/
class sharecommon_quick_fn {
struct set_hash {
std::size_t operator()(lean_object * o) const { return lean_sharecommon_hash(o); }
};
struct set_eq {
std::size_t operator()(lean_object * o1, lean_object * o2) const { return lean_sharecommon_eq(o1, o2); }
};
/*
We use `m_cache` to ensure we do **not** traverse a DAG as a tree.
We use pointer equality for this collection.
*/
std::unordered_map<lean_object *, lean_object *> m_cache;
/* Set of maximally shared terms. AKA hash-consing table. */
std::unordered_set<lean_object *, set_hash, set_eq> m_set;
/*
We do not increment reference counters when inserting Lean objects at `m_cache` and `m_set`.
This is correct because
- The domain of `m_cache` contains only sub-objects of `lean_sharecommon_quick` parameter,
and we know the object referenced by this parameter will remain alive.
- The range of `m_cache` contains only new objects that have been maxed shared, and these
objects will be are sub-objects of the object returned by `lean_sharecommon_quick`.
- `m_set` is like the range of `m_cache`.
*/
lean_object * check_cache(lean_object * a) {
if (!lean_is_exclusive(a)) {
// We only check the cache if `a` is a shared object
auto it = m_cache.find(a);
if (it != m_cache.end()) {
// All objects stored in the range of `m_cache` are single threaded.
lean_assert(lean_is_st(it->second));
// We increment the reference counter because this object
// will be returned by `lean_sharecommon_quick` or stored into a new object.
it->second->m_rc++;
return it->second;
}
}
return nullptr;
}
/*
`new_a` is a new object that is equal to `a`, but its subobjects are maximally shared.
*/
lean_object * save(lean_object * a, lean_object * new_a) {
lean_assert(lean_is_st(new_a));
lean_assert(new_a->m_rc == 1);
auto it = m_set.find(new_a);
lean_object * result;
if (it == m_set.end()) {
// `new_a` is a new object
m_set.insert(new_a);
result = new_a;
} else {
// We already have a maximally shared object that is equal to `new_a`
result = *it;
DEBUG_CODE({
if (lean_is_ctor(new_a)) {
lean_assert(lean_is_ctor(result));
unsigned num_objs = lean_ctor_num_objs(new_a);
lean_assert(lean_ctor_num_objs(result) == num_objs);
for (unsigned i = 0; i < num_objs; i++) {
lean_assert(lean_ctor_get(result, i) == lean_ctor_get(new_a, i));
}
}
});
lean_dec_ref(new_a); // delete `new_a`
// All objects in `m_set` are single threaded.
lean_assert(lean_is_st(result));
result->m_rc++;
lean_assert(result->m_rc > 1);
}
if (!lean_is_exclusive(a)) {
// We only cache the result if `a` is a shared object.
m_cache.insert(std::make_pair(a, result));
}
lean_assert(result == new_a || result->m_rc > 1);
lean_assert(result != new_a || result->m_rc == 1);
return result;
}
// `sarray` and `string`
lean_object * visit_terminal(lean_object * a) {
auto it = m_set.find(a);
if (it == m_set.end()) {
m_set.insert(a);
} else {
a = *it;
}
lean_inc_ref(a);
return a;
}
lean_object * visit_array(lean_object * a) {
lean_object * r = check_cache(a);
if (r != nullptr) { lean_assert(r->m_rc > 1); return r; }
size_t sz = array_size(a);
lean_array_object * new_a = (lean_array_object*)lean_alloc_array(sz, sz);
for (size_t i = 0; i < sz; i++) {
lean_array_set_core((lean_object*)new_a, i, visit(lean_array_get_core(a, i)));
}
return save(a, (lean_object*)new_a);
}
lean_object * visit_ctor(lean_object * a) {
lean_object * r = check_cache(a);
if (r != nullptr) { lean_assert(r->m_rc > 1); return r; }
unsigned num_objs = lean_ctor_num_objs(a);
unsigned tag = lean_ptr_tag(a);
unsigned sz = lean_object_byte_size(a);
unsigned scalar_offset = sizeof(lean_object) + num_objs*sizeof(void*);
unsigned scalar_sz = sz - scalar_offset;
lean_object * new_a = lean_alloc_ctor(tag, num_objs, scalar_sz);
for (unsigned i = 0; i < num_objs; i++) {
lean_ctor_set(new_a, i, visit(lean_ctor_get(a, i)));
}
if (scalar_sz > 0) {
memcpy(reinterpret_cast<char*>(new_a) + scalar_offset, reinterpret_cast<char*>(a) + scalar_offset, scalar_sz);
}
return save(a, new_a);
}
public:
/*
**TODO:** We did not implement stack overflow detection.
We claim it is not needed in the current uses of `shareCommon'`.
If this becomes an issue, we can use the following approach to address the issue without
affecting the performance.
- Add an extra `depth` parameter.
- In `operator()`, estimate the maximum depth based on the remaining stack space. See `check_stack`.
- If the limit is reached, simply return `a`.
*/
lean_object * visit(lean_object * a) {
if (lean_is_scalar(a)) {
return a;
}
switch (lean_ptr_tag(a)) {
/*
Similarly to `sharecommon_fn`, we only maximally share arrays, scalar arrays, strings, and
constructor objects.
*/
case LeanMPZ: lean_inc_ref(a); return a;
case LeanClosure: lean_inc_ref(a); return a;
case LeanThunk: lean_inc_ref(a); return a;
case LeanTask: lean_inc_ref(a); return a;
case LeanRef: lean_inc_ref(a); return a;
case LeanExternal: lean_inc_ref(a); return a;
case LeanReserved: lean_inc_ref(a); return a;
case LeanScalarArray: return visit_terminal(a);
case LeanString: return visit_terminal(a);
case LeanArray: return visit_array(a);
default: return visit_ctor(a);
}
}
lean_object * operator()(lean_object * a) {
return visit(a);
}
};
// def ShareCommon.shareCommon' (a : A) : A := a
extern "C" LEAN_EXPORT obj_res lean_sharecommon_quick(obj_arg a) {
return sharecommon_quick_fn()(a);
}
};

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.

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