-
Notifications
You must be signed in to change notification settings - Fork 259
/
LibrarySearch.lean
302 lines (265 loc) · 11.8 KB
/
LibrarySearch.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
/-
Copyright (c) 2021 Gabriel Ebner. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gabriel Ebner, Scott Morrison
-/
import Std.Util.Pickle
import Mathlib.Tactic.Cache
import Mathlib.Tactic.SolveByElim
import Std.Data.MLList.Heartbeats
/-!
# Library search
This file defines tactics `exact?` and `apply?`,
(formerly known as `library_search`)
and a term elaborator `exact?%`
that tries to find a lemma
solving the current goal
(subgoals are solved using `solveByElim`).
```
example : x < x + 1 := exact?%
example : Nat := by exact?
```
-/
namespace Mathlib.Tactic.LibrarySearch
open Lean Meta Std.Tactic.TryThis
initialize registerTraceClass `Tactic.librarySearch
initialize registerTraceClass `Tactic.librarySearch.lemmas
/--
A "modifier" for a declaration.
* `none` indicates the original declaration,
* `mp` indicates that (possibly after binders) the declaration is an `↔`,
and we want to consider the forward direction,
* `mpr` similarly, but for the backward direction.
-/
inductive DeclMod
| none | mp | mpr
deriving DecidableEq, Ord
instance : ToString DeclMod where
toString m := match m with | .none => "" | .mp => "mp" | .mpr => "mpr"
/-- Prepare the discrimination tree entries for a lemma. -/
def processLemma (name : Name) (constInfo : ConstantInfo) :
MetaM (Array (Array (DiscrTree.Key true) × (Name × DeclMod))) := do
if constInfo.isUnsafe then return #[]
if ← name.isBlackListed then return #[]
withNewMCtxDepth do withReducible do
let (_, _, type) ← forallMetaTelescope constInfo.type
let keys ← DiscrTree.mkPath type
let mut r := #[(keys, (name, .none))]
match type.getAppFnArgs with
| (``Iff, #[lhs, rhs]) => do
return r.push (← DiscrTree.mkPath rhs, (name, .mp))
|>.push (← DiscrTree.mkPath lhs, (name, .mpr))
| _ => return r
/-- Insert a lemma into the discrimination tree. -/
-- Recall that `apply?` caches the discrimination tree on disk.
-- If you are modifying this file, you will probably want to delete
-- `build/lib/MathlibExtras/LibrarySearch.extra`
-- so that the cache is rebuilt.
def addLemma (name : Name) (constInfo : ConstantInfo)
(lemmas : DiscrTree (Name × DeclMod) true) : MetaM (DiscrTree (Name × DeclMod) true) := do
let mut lemmas := lemmas
for (key, value) in ← processLemma name constInfo do
lemmas := lemmas.insertIfSpecific key value
return lemmas
/-- Construct the discrimination tree of all lemmas. -/
def buildDiscrTree : IO (DiscrTreeCache (Name × DeclMod)) :=
DiscrTreeCache.mk "apply?: init cache" processLemma
-- Sort so lemmas with longest names come first.
-- This is counter-intuitive, but the way that `DiscrTree.getMatch` returns results
-- means that the results come in "batches", with more specific matches *later*.
-- Thus we're going to call reverse on the result of `DiscrTree.getMatch`,
-- so if we want to try lemmas with shorter names first,
-- we need to put them into the `DiscrTree` backwards.
(post? := some fun A =>
A.map (fun (n, m) => (n.toString.length, n, m)) |>.qsort (fun p q => p.1 > q.1) |>.map (·.2))
open System (FilePath)
def cachePath : IO FilePath :=
try
return (← findOLean `MathlibExtras.LibrarySearch).withExtension "extra"
catch _ =>
return "build" / "lib" / "MathlibExtras" / "LibrarySearch.extra"
/--
Retrieve the current current of lemmas.
-/
initialize librarySearchLemmas : DiscrTreeCache (Name × DeclMod) ← unsafe do
let path ← cachePath
if (← path.pathExists) then
let (d, _r) ← unpickle (DiscrTree (Name × DeclMod) true) path
-- We can drop the `CompactedRegion` value; we do not plan to free it
DiscrTreeCache.mk "apply?: using cache" processLemma (init := some d)
else
buildDiscrTree
/-- Shortcut for calling `solveByElim`. -/
def solveByElim (goals : List MVarId) (required : List Expr) (exfalso := false) (depth) := do
-- There is only a marginal decrease in performance for using the `symm` option for `solveByElim`.
-- (measured via `lake build && time lake env lean test/librarySearch.lean`).
let cfg : SolveByElim.Config :=
{ maxDepth := depth, exfalso := exfalso, symm := true, commitIndependentGoals := true }
let cfg := if !required.isEmpty then cfg.requireUsingAll required else cfg
SolveByElim.solveByElim.processSyntax cfg false false [] [] #[] goals
/--
Try applying the given lemma (with symmetry modifier) to the goal,
then try to close subsequent goals using `solveByElim`.
If `solveByElim` succeeds, we return `[]` as the list of new subgoals,
otherwise the full list of subgoals.
-/
def librarySearchLemma (lem : Name) (mod : DeclMod) (required : List Expr) (solveByElimDepth := 6)
(goal : MVarId) : MetaM (List MVarId) :=
withTraceNode `Tactic.librarySearch (return m!"{·.emoji} trying {lem}") do
let lem ← mkConstWithFreshMVarLevels lem
let lem ← match mod with
| .none => pure lem
| .mp => mapForallTelescope (fun e => mkAppM ``Iff.mp #[e]) lem
| .mpr => mapForallTelescope (fun e => mkAppM ``Iff.mpr #[e]) lem
let newGoals ← goal.apply lem { allowSynthFailures := true }
try
let subgoals ← solveByElim newGoals required (exfalso := false) (depth := solveByElimDepth)
pure subgoals
catch _ =>
if required.isEmpty then
pure newGoals
else
failure
/--
Returns a lazy list of the results of applying a library lemma,
then calling `solveByElim` on the resulting goals.
-/
def librarySearchCore (goal : MVarId)
(required : List Expr) (solveByElimDepth := 6) : Nondet MetaM (List MVarId) :=
.squash fun _ => do
let ty ← goal.getType
let lemmas := (← librarySearchLemmas.getMatch ty).toList
trace[Tactic.librarySearch.lemmas] m!"Candidate library_search lemmas:\n{lemmas}"
return (Nondet.ofList lemmas).filterMapM fun (lem, mod) =>
observing? <| librarySearchLemma lem mod required solveByElimDepth goal
/--
Run `librarySearchCore` on both the goal and `symm` applied to the goal.
-/
def librarySearchSymm (goal : MVarId)
(required : List Expr) (solveByElimDepth := 6) :
Nondet MetaM (List MVarId) :=
(librarySearchCore goal required solveByElimDepth) <|>
.squash fun _ => do
if let some symm ← observing? goal.applySymm then
return librarySearchCore symm required solveByElimDepth
else
return .nil
/-- A type synonym for our subgoal ranking algorithm. -/
def subgoalRankType : Type := Bool × Nat × Int
deriving ToString
instance : Ord subgoalRankType :=
have : Ord (Nat × Int) := lexOrd
lexOrd
/-- Returns a tuple:
* are there no remaining goals?
* how many local hypotheses were used?
* how many goals remain, negated?
Larger values (i.e. no remaining goals, more local hypotheses, fewer remaining goals)
are better.
-/
def subgoalRanking (goal : MVarId) (subgoals : List MVarId) : MetaM subgoalRankType := do
return (subgoals.isEmpty, ← countLocalHypsUsed (.mvar goal), - subgoals.length)
/-- Sort the incomplete results from `librarySearchCore` according to
* the number of local hypotheses used (the more the better) and
* the number of remaining subgoals (the fewer the better).
-/
def sortResults (goal : MVarId) (R : Array (List MVarId × MetavarContext)) :
MetaM (Array (List MVarId × MetavarContext)) := do
let R' ← R.mapM fun (gs, ctx) => do
return (← withMCtx ctx (subgoalRanking goal gs), gs, ctx)
let R'' := R'.qsort fun a b => compare a.1 b.1 = Ordering.gt
return R''.map (·.2)
/--
Try to solve the goal either by:
* calling `solveByElim`
* or applying a library lemma then calling `solveByElim` on the resulting goals.
If it successfully closes the goal, returns `none`.
Otherwise, it returns `some a`, where `a : Array (MetavarContext × List MVarId)`,
with an entry for each library lemma which was successfully applied,
containing the metavariable context after the application, and a list of the subsidiary goals.
(Always succeeds, and the metavariable context stored in the monad is reverted,
unless the goal was completely solved.)
(Note that if `solveByElim` solves some but not all subsidiary goals,
this is not currently tracked.)
-/
def librarySearch (goal : MVarId) (required : List Expr)
(solveByElimDepth := 6) (leavePercentHeartbeats : Nat := 10) :
MetaM (Option (Array (List MVarId × MetavarContext))) := do
let librarySearchEmoji := fun
| .error _ => bombEmoji
| .ok (some _) => crossEmoji
| .ok none => checkEmoji
withTraceNode `Tactic.librarySearch (return m!"{librarySearchEmoji ·} {← goal.getType}") do
profileitM Exception "librarySearch" (← getOptions) do
(do
_ ← solveByElim [goal] required (exfalso := true) (depth := solveByElimDepth)
return none) <|>
(do
let results ← librarySearchSymm goal required solveByElimDepth
|>.mapM (fun x => do pure (x, ← getMCtx))
|>.toMLList'
-- Don't use too many heartbeats.
|>.whileAtLeastHeartbeatsPercent leavePercentHeartbeats
-- Stop if we find something that closes the goal
|>.takeUpToFirst (·.1.isEmpty)
|>.asArray
match results.find? (·.1.isEmpty) with
| none => return (← sortResults goal results)
| some (_, ctx) => do
setMCtx ctx
return none)
open Lean.Parser.Tactic
-- TODO: implement the additional options for `library_search` from Lean 3,
-- in particular including additional lemmas
-- with `exact? [X, Y, Z]` or `exact? with attr`.
syntax (name := exact?') "exact?" (config)? (simpArgs)?
(" using " (colGt term),+)? : tactic
syntax (name := exact?!) "exact?!" (config)? (simpArgs)?
(" using " (colGt term),+)? : tactic
syntax (name := exact!?) "exact!?" (config)? (simpArgs)?
(" using " (colGt term),+)? : tactic
syntax (name := apply?') "apply?" (config)? (simpArgs)?
(" using " (colGt term),+)? : tactic
-- For now we only implement the basic functionality.
-- The full syntax is recognized, but will produce a "Tactic has not been implemented" error.
open Elab.Tactic Elab Tactic
def exact? (tk : Syntax) (required : Option (Array (TSyntax `term))) (requireClose : Bool) :
TacticM Unit := do
let mvar ← getMainGoal
let (_, goal) ← (← getMainGoal).intros
goal.withContext do
let required := (← (required.getD #[]).mapM getFVarId).toList.map .fvar
if let some suggestions ← librarySearch goal required then
if requireClose then
throwError "`exact?` could not close the goal. Try `apply?` to see partial suggestions."
reportOutOfHeartbeats `library_search tk
for suggestion in suggestions do
withMCtx suggestion.2 do
addExactSuggestion tk (← instantiateMVars (mkMVar mvar)).headBeta (addSubgoalsMsg := true)
if suggestions.isEmpty then logError "apply? didn't find any relevant lemmas"
admitGoal goal
else
addExactSuggestion tk (← instantiateMVars (mkMVar mvar)).headBeta
elab_rules : tactic | `(tactic| exact? $[using $[$required],*]?) => do
exact? (← getRef) required true
elab_rules : tactic | `(tactic| apply? $[using $[$required],*]?) => do
exact? (← getRef) required false
elab tk:"library_search" : tactic => do
logWarning ("`library_search` has been renamed to `apply?`" ++
" (or `exact?` if you only want solutions closing the goal)")
exact? tk none false
open Elab Term in
elab tk:"exact?%" : term <= expectedType => do
let goal ← mkFreshExprMVar expectedType
let (_, introdGoal) ← goal.mvarId!.intros
introdGoal.withContext do
if let some suggestions ← librarySearch introdGoal [] then
reportOutOfHeartbeats `library_search tk
for suggestion in suggestions do
withMCtx suggestion.2 do
addTermSuggestion tk (← instantiateMVars goal).headBeta
if suggestions.isEmpty then logError "exact? didn't find any relevant lemmas"
mkSorry expectedType (synthetic := true)
else
addTermSuggestion tk (← instantiateMVars goal).headBeta
instantiateMVars goal