-
Notifications
You must be signed in to change notification settings - Fork 7
/
By.lean
92 lines (82 loc) · 3.44 KB
/
By.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
import Verbose.Infrastructure.Extension
import Verbose.Tactics.Common
open Lean Elab Tactic Meta
open Std Tactic RCases
def destructTac (fact : Term) (news : Array MaybeTypedIdent) : TacticM Unit := do
let orig_goal ← getMainGoal
orig_goal.withContext do
for new in news do
checkName new.1
let news := Array.toList news
match news with
| [(name, stuff)] => do
let applied_fact_expr : Expr ← elabTerm fact none
let type ← instantiateMVars (← inferType applied_fact_expr)
let newTypeExpr ← match stuff with
| some new => elabTermEnsuringValue new type
| none => pure type
let intermediate_goal ← orig_goal.assert name newTypeExpr applied_fact_expr
let (_, new_goal) ← intermediate_goal.intro1P
replaceMainGoal [new_goal]
| news =>
let news_patt := news.map RCasesPattOfMaybeTypedIdent
let new_goals ← rcases #[(none, fact)] (RCasesPatt.tuple Syntax.missing news_patt) (← getMainGoal)
replaceMainGoal new_goals
withMainContext do
let mut goal ← getMainGoal
for new in news do
let decl ← getLocalDeclFromUserName new.1
if let some type := new.2 then
let actualType ← instantiateMVars (← elabTermEnsuringValue type decl.type)
goal ← goal.changeLocalDecl decl.fvarId actualType
replaceMainGoal (goal::new_goals)
register_endpoint cannotGet : CoreM String
def anonymousLemmaTac (fact : Term) (news : Array MaybeTypedIdent) : TacticM Unit := do
let lemmas := (← verboseConfigurationExt.get).anonymousFactSplittingLemmas
for lem in lemmas do
let appStx : Term ← `($(mkIdent lem) $fact)
try
destructTac appStx news
return
catch _ => pure ()
throwError ← cannotGet
register_endpoint theName : CoreM String
def obtainTac (fact : Term) (news : Array MaybeTypedIdent) : TacticM Unit := do
try
destructTac fact news
catch
| e@(.error _ msg) =>
if (← msg.toString).startsWith (← theName) then
throw e
else
anonymousLemmaTac fact news
| internal => throw internal
register_endpoint needName : CoreM String
open Mathlib.Tactic.Choose in
def chooseTac (fact : Term) (news : Array MaybeTypedIdent) : TacticM Unit := do
(← getMainGoal).withContext do
for new in news do
checkName new.1
let applied_fact_expr : Expr ← elabTerm fact none
if news.isEmpty then throwError ← needName
let new_names := (← news.mapM fun p ↦ (mkBinderIdent p.1)).toList
let newGoal : MVarId ← elabChoose true (some applied_fact_expr) new_names (.failure []) (← getMainGoal)
newGoal.withContext do
let mut newerGoal : MVarId := newGoal
for new in news[1:] do
if let (n, some t) := new then
let decl ← getLocalDeclFromUserName n
newerGoal := ← newGoal.changeLocalDecl decl.fvarId (← elabTerm t none)
replaceMainGoal [newerGoal]
register_endpoint wrongNbGoals (actual announced : ℕ) : CoreM String
def bySufficesTac (fact : Term) (goals : Array Term) : TacticM Unit := do
let mainGoal ← getMainGoal
mainGoal.withContext do
let newGoals ← mainGoal.apply (← elabTermForApply fact)
if newGoals.length != goals.size then
throwError ← wrongNbGoals newGoals.length goals.size
let mut newerGoals : Array MVarId := #[]
for (goal, announced) in newGoals.zip goals.toList do
let announcedExpr ← elabTermEnsuringValue announced (← goal.getType)
newerGoals := newerGoals.push (← goal.replaceTargetDefEq announcedExpr)
replaceMainGoal newerGoals.toList