aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity

feat: Elementarized tactics with motives, congruence, and absurdity #72

Merged
aniva merged 41 commits from goal/mapply into dev 2024-06-12 13:52:46 -07:00
Conversation 6 Commits 41 Files Changed 22 +3 -3
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit 63417ef179 - Show all commits

6
Pantograph/Tactic/MotivatedApply.lean
View File

@ -32,8 +32,8 @@ protected def getMotiveType (info: RecursorWithMotive): Expr :=
let a := info.args.get! level let a := info.args.get! level
a a
protected def surrogateMotiveType (info: RecursorWithMotive) (resultant: Expr): MetaM Expr := do protected def surrogateMotiveType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do
let motiveType := info.getMotiveType let motiveType := Expr.instantiateRev info.getMotiveType mvars
let resultantType ← Meta.inferType resultant let resultantType ← Meta.inferType resultant
return replaceForallBody motiveType resultantType return replaceForallBody motiveType resultantType
@ -83,7 +83,7 @@ def motivatedApply: Elab.Tactic.Tactic := λ stx => do
let argType := argType.instantiateRev prev let argType := argType.instantiateRev prev
let bvarIndex := info.nArgs - i - 1 let bvarIndex := info.nArgs - i - 1
let argGoal ← if bvarIndex = info.iMotive then let argGoal ← if bvarIndex = info.iMotive then
let surrogateMotiveType ← info.surrogateMotiveType resultant let surrogateMotiveType ← info.surrogateMotiveType prev resultant
Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive) Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive)
else else
Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous) Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous)