-
Notifications
You must be signed in to change notification settings - Fork 259
/
Simp.lean
242 lines (211 loc) · 9.75 KB
/
Simp.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
/-
Copyright (c) 2022 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison, Gabriel Ebner, Floris van Doorn
-/
import Lean
import Std.Tactic.OpenPrivate
/-!
# Helper functions for using the simplifier.
[TODO] Needs documentation, cleanup, and possibly reunification of `mkSimpContext'` with core.
-/
open Lean Elab.Tactic
def Lean.PHashSet.toList [BEq α] [Hashable α] (s : Lean.PHashSet α) : List α :=
s.1.toList.map (·.1)
namespace Lean
namespace Meta.DiscrTree
partial def Trie.getElements : Trie α s → Array α
| Trie.node vs children =>
vs ++ children.concatMap fun (_, child) ↦ child.getElements
def getElements (d : DiscrTree α s) : Array α :=
d.1.toList.toArray.concatMap fun (_, child) => child.getElements
end Meta.DiscrTree
namespace Meta.Simp
open Elab.Tactic
instance : ToFormat SimpTheorems where
format s :=
f!"pre:
{s.pre.getElements.toList}
post:
{s.post.getElements.toList}
lemmaNames:
{s.lemmaNames.toList.map (·.key)}
toUnfold: {s.toUnfold.toList}
erased: {s.erased.toList.map (·.key)}
toUnfoldThms: {s.toUnfoldThms.toList}"
def mkEqSymm (e : Expr) (r : Simp.Result) : MetaM Simp.Result :=
({ expr := e, proof? := · }) <$>
match r.proof? with
| none => pure none
| some p => some <$> Meta.mkEqSymm p
def mkCast (r : Simp.Result) (e : Expr) : MetaM Expr := do
mkAppM ``cast #[← r.getProof, e]
/-- Return all propositions in the local context. -/
def getPropHyps : MetaM (Array FVarId) := do
let mut result := #[]
for localDecl in (← getLCtx) do
unless localDecl.isAuxDecl do
if (← isProp localDecl.type) then
result := result.push localDecl.fvarId
return result
export private mkDischargeWrapper from Lean.Elab.Tactic.Simp
-- copied from core
/--
If `ctx == false`, the config argument is assumed to have type `Meta.Simp.Config`,
and `Meta.Simp.ConfigCtx` otherwise.
If `ctx == false`, the `discharge` option must be none
-/
def mkSimpContext' (simpTheorems : SimpTheorems) (stx : Syntax) (eraseLocal : Bool)
(kind := SimpKind.simp) (ctx := false) (ignoreStarArg : Bool := false) :
TacticM MkSimpContextResult := do
if ctx && !stx[2].isNone then
if kind == SimpKind.simpAll then
throwError "'simp_all' tactic does not support 'discharger' option"
if kind == SimpKind.dsimp then
throwError "'dsimp' tactic does not support 'discharger' option"
let dischargeWrapper ← mkDischargeWrapper stx[2]
let simpOnly := !stx[3].isNone
let simpTheorems ← if simpOnly then
simpOnlyBuiltins.foldlM (·.addConst ·) {}
else
pure simpTheorems
let congrTheorems ← Meta.getSimpCongrTheorems
let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) {
config := (← elabSimpConfig stx[1] (kind := kind))
simpTheorems := #[simpTheorems], congrTheorems
}
if !r.starArg || ignoreStarArg then
return { r with dischargeWrapper }
else
let mut simpTheorems := r.ctx.simpTheorems
let hs ← getPropHyps
for h in hs do
unless simpTheorems.isErased (.fvar h) do
simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr
return { ctx := { r.ctx with simpTheorems }, dischargeWrapper }
export private checkTypeIsProp shouldPreprocess preprocess mkSimpTheoremCore
from Lean.Meta.Tactic.Simp.SimpTheorems
/-- Similar to `mkSimpTheoremsFromConst` except that it also returns the names of the generated
lemmas.
Remark: either the length of the arrays is the same,
or the length of the first one is 0 and the length of the second one is 1. -/
def mkSimpTheoremsFromConst' (declName : Name) (post : Bool) (inv : Bool) (prio : Nat) :
MetaM (Array Name × Array SimpTheorem) := do
let cinfo ← getConstInfo declName
let val := mkConst declName (cinfo.levelParams.map mkLevelParam)
withReducible do
let type ← inferType val
checkTypeIsProp type
if inv || (← shouldPreprocess type) then
let mut r := #[]
let mut auxNames := #[]
for (val, type) in (← preprocess val type inv (isGlobal := true)) do
let auxName ← mkAuxLemma cinfo.levelParams type val
auxNames := auxNames.push auxName
r := r.push <| ← mkSimpTheoremCore (.decl declName)
(mkConst auxName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst auxName) post prio
return (auxNames, r)
else
return (#[], #[← mkSimpTheoremCore (.decl declName) (mkConst declName <|
cinfo.levelParams.map mkLevelParam) #[] (mkConst declName) post prio])
/-- Similar to `addSimpTheorem` except that it returns an array of all auto-generated
simp-theorems. -/
def addSimpTheorem' (ext : SimpExtension) (declName : Name) (post : Bool) (inv : Bool)
(attrKind : AttributeKind) (prio : Nat) : MetaM (Array Name) := do
let (auxNames, simpThms) ← mkSimpTheoremsFromConst' declName post inv prio
for simpThm in simpThms do
ext.add (SimpEntry.thm simpThm) attrKind
return auxNames
/-- Similar to `AttributeImpl.add` in `mkSimpAttr` except that it doesn't require syntax,
and returns an array of all auto-generated lemmas. -/
def addSimpAttr (declName : Name) (ext : SimpExtension) (attrKind : AttributeKind)
(post : Bool) (prio : Nat) :
MetaM (Array Name) := do
let info ← getConstInfo declName
if (← isProp info.type) then
addSimpTheorem' ext declName post (inv := false) attrKind prio
else if info.hasValue then
if let some eqns ← getEqnsFor? declName then
let mut auxNames := #[]
for eqn in eqns do
-- Is this list is always empty?
let newAuxNames ← addSimpTheorem' ext eqn post (inv := false) attrKind prio
auxNames := auxNames ++ newAuxNames
ext.add (SimpEntry.toUnfoldThms declName eqns) attrKind
if hasSmartUnfoldingDecl (← getEnv) declName then
ext.add (SimpEntry.toUnfold declName) attrKind
return auxNames
else
ext.add (SimpEntry.toUnfold declName) attrKind
return #[]
else
throwError "invalid 'simp', it is not a proposition nor a definition (to unfold)"
/-- Similar to `AttributeImpl.add` in `mkSimpAttr` except that it returns an array of all
auto-generated lemmas. -/
def addSimpAttrFromSyntax (declName : Name) (ext : SimpExtension) (attrKind : AttributeKind)
(stx : Syntax) : MetaM (Array Name) := do
let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
let prio ← getAttrParamOptPrio stx[2]
addSimpAttr declName ext attrKind post prio
end Simp
/-- Construct a `SimpTheorems` from a list of names. (i.e. as with `simp only`). -/
def simpTheoremsOfNames (lemmas : List Name) : MetaM SimpTheorems := do
lemmas.foldlM (·.addConst ·) (← simpOnlyBuiltins.foldlM (·.addConst ·) {})
/-- Simplify an expression using only a list of lemmas specified by name. -/
-- TODO We need to write a `mkSimpContext` in `MetaM`
-- that supports all the bells and whistles in `simp`.
-- It should generalize this, and another partial implementation in `Tactic.Simps.Basic`.
def simpOnlyNames (lemmas : List Name) (e : Expr) (config : Simp.Config := {}) :
MetaM Simp.Result := do
(·.1) <$> simp e
{ simpTheorems := #[← simpTheoremsOfNames lemmas], congrTheorems := ← getSimpCongrTheorems,
config := config }
/--
Given a simplifier `S : Expr → MetaM Simp.Result`,
and an expression `e : Expr`, run `S` on the type of `e`, and then
convert `e` into that simplified type, using a combination of type hints and `Eq.mp`.
-/
def simpType (S : Expr → MetaM Simp.Result) (e : Expr) : MetaM Expr := do
match (← S (← inferType e)) with
| ⟨ty', none, _⟩ => mkExpectedTypeHint e ty'
-- We use `mkExpectedTypeHint` in this branch as well, in order to preserve the binder types.
| ⟨ty', some prf, _⟩ => mkExpectedTypeHint (← mkEqMP prf e) ty'
/-- Independently simplify both the left-hand side and the right-hand side
of an equality. The equality is allowed to be under binders.
Returns the simplified equality and a proof of it. -/
def simpEq (S : Expr → MetaM Simp.Result) (type pf : Expr) : MetaM (Expr × Expr) := do
forallTelescope type fun fvars type => do
let .app (.app (.app (.const `Eq [u]) α) lhs) rhs := type | throwError "simpEq expecting Eq"
let ⟨lhs', lhspf?, _⟩ ← S lhs
let ⟨rhs', rhspf?, _⟩ ← S rhs
let mut pf' := mkAppN pf fvars
if let some lhspf := lhspf? then
pf' ← mkEqTrans (← mkEqSymm lhspf) pf'
if let some rhspf := rhspf? then
pf' ← mkEqTrans pf' rhspf
let type' := mkApp3 (mkConst ``Eq [u]) α lhs' rhs'
return (← mkForallFVars fvars type', ← mkLambdaFVars fvars pf')
/-- Checks whether `declName` is in `SimpTheorems` as either a lemma or definition to unfold. -/
def SimpTheorems.contains (d : SimpTheorems) (declName : Name) :=
d.isLemma (.decl declName) || d.isDeclToUnfold declName
/-- Tests whether `decl` has `simp`-attribute `simpAttr`. Returns `false` is `simpAttr` is not a
valid simp-attribute. -/
def isInSimpSet (simpAttr decl : Name) : CoreM Bool := do
let .some simpDecl ← getSimpExtension? simpAttr | return false
return (← simpDecl.getTheorems).contains decl
/-- Returns all declarations with the `simp`-attribute `simpAttr`.
Note: this also returns many auxiliary declarations. -/
def getAllSimpDecls (simpAttr : Name) : CoreM (List Name) := do
let .some simpDecl ← getSimpExtension? simpAttr | return []
let thms ← simpDecl.getTheorems
return thms.toUnfold.toList ++ thms.lemmaNames.toList.filterMap fun
| .decl decl => some decl
| _ => none
/-- Gets all simp-attributes given to declaration `decl`. -/
def getAllSimpAttrs (decl : Name) : CoreM (Array Name) := do
let mut simpAttrs := #[]
for (simpAttr, simpDecl) in (← simpExtensionMapRef.get).toList do
if (← simpDecl.getTheorems).contains decl then
simpAttrs := simpAttrs.push simpAttr
return simpAttrs
end Lean.Meta