-
Notifications
You must be signed in to change notification settings - Fork 259
/
Propose.lean
145 lines (123 loc) · 5.74 KB
/
Propose.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
/-
Copyright (c) 2023 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison
-/
import Lean.Meta.Tactic.TryThis
import Lean.Meta.Tactic.SolveByElim
import Mathlib.Lean.Expr.Basic
import Mathlib.Lean.Meta
import Mathlib.Lean.Meta.Basic
import Std.Util.Cache
import Mathlib.Tactic.Core
/-!
# Propose
This file defines a tactic `have? using a, b, c`
that tries to find a lemma which makes use of each of the local hypotheses `a, b, c`.
The variant `have? : t using a, b, c` restricts to lemmas with type `t` (which may contain `_`).
Note that in either variant `have?` does not look at the current goal at all.
It is a relative of `apply?` but for *forward reasoning* (i.e. looking at the hypotheses)
rather than backward reasoning.
```
import Std.Data.List.Basic
import Mathlib.Tactic.Propose
example (K L M : List α) (w : L.Disjoint M) (m : K ⊆ L) : True := by
have? using w, m -- Try this: `List.disjoint_of_subset_left m w`
trivial
```
-/
set_option autoImplicit true
namespace Mathlib.Tactic.Propose
open Lean Meta Std.Tactic Tactic.TryThis
initialize registerTraceClass `Tactic.propose
/-- Configuration for `DiscrTree`. -/
def discrTreeConfig : WhnfCoreConfig := {}
initialize proposeLemmas : DeclCache (DiscrTree Name) ←
DeclCache.mk "have?: init cache" failure {} fun name constInfo lemmas => do
if constInfo.isUnsafe then return lemmas
if ← name.isBlackListed then return lemmas
withNewMCtxDepth do withReducible do
let (mvars, _, _) ← forallMetaTelescope constInfo.type
let mut lemmas := lemmas
for m in mvars do
lemmas ← lemmas.insertIfSpecific (← inferType m) name discrTreeConfig
pure lemmas
open Lean.Meta.SolveByElim in
/-- Shortcut for calling `solveByElim`. -/
def solveByElim (orig : MVarId) (goals : Array MVarId) (use : Array Expr) (required : Array Expr)
(depth) := do
let cfg : SolveByElimConfig := { maxDepth := depth, exfalso := true, symm := true }
let cfg := if !required.isEmpty then
cfg.testSolutions (fun _ => do
let r ← instantiateMVars (.mvar orig)
pure <| required.all fun e => e.occurs r)
else
cfg
let cfg := cfg.synthInstance
_ ← SolveByElim.solveByElim cfg (use.toList.map pure) (pure (← getLocalHyps).toList) goals.toList
/--
Attempts to find lemmas which use all of the `required` expressions as arguments, and
can be unified with the given `type` (which may contain metavariables, which we avoid assigning).
We look up candidate lemmas from a discrimination tree using the first such expression.
Returns an array of pairs, containing the names of found lemmas and the resulting application.
-/
def propose (lemmas : DiscrTree Name) (type : Expr) (required : Array Expr)
(solveByElimDepth := 15) : MetaM (Array (Name × Expr)) := do
guard !required.isEmpty
let ty ← whnfR (← instantiateMVars (← inferType required[0]!))
let candidates ← lemmas.getMatch ty discrTreeConfig
candidates.filterMapM fun lem : Name =>
try
trace[Tactic.propose] "considering {lem}"
let Expr.mvar g ← mkFreshExprMVar type | failure
let e ← mkConstWithFreshMVarLevels lem
let (args, _, _) ← forallMetaTelescope (← inferType e)
let .true ← preservingMCtx <| withAssignableSyntheticOpaque <|
isDefEq type (← inferType (mkAppN e args)) | failure
g.assign (mkAppN e args)
let use := required.filterMap fun e => match e with | .fvar _ => none | _ => some e
solveByElim g (args.map fun a => a.mvarId!) use required solveByElimDepth
trace[Tactic.propose] "successfully filled in arguments for {lem}"
pure <| some (lem, ← instantiateMVars (.mvar g))
catch _ => pure none
open Lean.Parser.Tactic
/--
* `have? using a, b, c` tries to find a lemma
which makes use of each of the local hypotheses `a, b, c`,
and reports any results via trace messages.
* `have? : h using a, b, c` only returns lemmas whose type matches `h` (which may contain `_`).
* `have?! using a, b, c` will also call `have` to add results to the local goal state.
Note that `have?` (unlike `apply?`) does not inspect the goal at all,
only the types of the lemmas in the `using` clause.
`have?` should not be left in proofs; it is a search tool, like `apply?`.
Suggestions are printed as `have := f a b c`.
-/
syntax (name := propose') "have?" "!"? (ident)? (" : " term)? " using " (colGt term),+ : tactic
open Elab.Tactic Elab Tactic in
elab_rules : tactic
| `(tactic| have?%$tk $[!%$lucky]? $[$h:ident]? $[ : $type:term]? using $[$terms:term],*) => do
let stx ← getRef
let goal ← getMainGoal
goal.withContext do
let required ← terms.mapM (elabTerm · none)
let type ← match type with
| some stx => elabTermWithHoles stx none (← getMainTag) true <&> (·.1)
| none => mkFreshTypeMVar
let proposals ← propose (← proposeLemmas.get) type required
if proposals.isEmpty then
throwError "propose could not find any lemmas using the given hypotheses"
-- TODO we should have `proposals` return a lazy list, to avoid unnecessary computation here.
for p in proposals.toList.take 10 do
addHaveSuggestion tk (h.map (·.getId)) (← inferType p.2) p.2 stx
if lucky.isSome then
let mut g := goal
for p in proposals.toList.take 10 do
(_, g) ← g.let p.1 p.2
replaceMainGoal [g]
@[inherit_doc propose'] syntax "have?!" (" : " term)? " using " (colGt term),+ : tactic
@[inherit_doc propose'] syntax "have!?" (" : " term)? " using " (colGt term),+ : tactic
macro_rules
| `(tactic| have?!%$tk $[: $type]? using $terms,*) =>
`(tactic| have?%$tk ! $[: $type]? using $terms,*)
| `(tactic| have!?%$tk $[: $type]? using $terms,*) =>
`(tactic| have?%$tk ! $[: $type]? using $terms,*)