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
1 changed files with 66 additions and 0 deletions
Showing only changes of commit 75b4648ba9 - Show all commits

View File

@ -252,6 +252,7 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String
let goal ← match state.savedState.tactic.goals.get? goalId with let goal ← match state.savedState.tactic.goals.get? goalId with
| .some goal => pure goal | .some goal => pure goal
| .none => return .indexError goalId | .none => return .indexError goalId
goal.checkNotAssigned `GoalState.tryAssign
let expr ← match Parser.runParserCategory let expr ← match Parser.runParserCategory
(env := state.env) (env := state.env)
(catName := `term) (catName := `term)
@ -275,6 +276,7 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St
let goal ← match state.savedState.tactic.goals.get? goalId with let goal ← match state.savedState.tactic.goals.get? goalId with
| .some goal => pure goal | .some goal => pure goal
| .none => return .indexError goalId | .none => return .indexError goalId
goal.checkNotAssigned `GoalState.tryHave
let type ← match Parser.runParserCategory let type ← match Parser.runParserCategory
(env := state.env) (env := state.env)
(catName := `term) (catName := `term)
@ -324,6 +326,7 @@ protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: Str
let goal ← match state.savedState.tactic.goals.get? goalId with let goal ← match state.savedState.tactic.goals.get? goalId with
| .some goal => pure goal | .some goal => pure goal
| .none => return .indexError goalId | .none => return .indexError goalId
goal.checkNotAssigned `GoalState.tryLet
let type ← match Parser.runParserCategory let type ← match Parser.runParserCategory
(env := state.env) (env := state.env)
(catName := `term) (catName := `term)
@ -369,6 +372,7 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat):
let goal ← match state.savedState.tactic.goals.get? goalId with let goal ← match state.savedState.tactic.goals.get? goalId with
| .some goal => pure goal | .some goal => pure goal
| .none => return .indexError goalId | .none => return .indexError goalId
goal.checkNotAssigned `GoalState.conv
let tacticM : Elab.Tactic.TacticM (Elab.Tactic.SavedState × MVarId) := do let tacticM : Elab.Tactic.TacticM (Elab.Tactic.SavedState × MVarId) := do
state.restoreTacticM goal state.restoreTacticM goal
@ -452,6 +456,7 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
(fileName := filename) with (fileName := filename) with
| .ok syn => pure syn | .ok syn => pure syn
| .error error => return .parseError error | .error error => return .parseError error
goal.checkNotAssigned `GoalState.tryCalc
let calcPrevRhs? := state.calcPrevRhsOf? goalId let calcPrevRhs? := state.calcPrevRhsOf? goalId
let target ← instantiateMVars (← goal.getDecl).type let target ← instantiateMVars (← goal.getDecl).type
let tag := (← goal.getDecl).userName let tag := (← goal.getDecl).userName
@ -510,4 +515,65 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
catch exception => catch exception =>
return .failure #[← exception.toMessageData.toString] return .failure #[← exception.toMessageData.toString]
def getForallArgsBody: Expr → List Expr × Expr
| .forallE _ d b _ =>
let (innerArgs, innerBody) := getForallArgsBody b
(d :: innerArgs, innerBody)
| e => ([], e)
def collectMotiveArguments (forallBody: Expr): SSet Nat :=
-- Get all de Bruijn indices
Id.run $ do
Expr.foldlM (λ acc subexpr => do
match subexpr with
| .app (.bvar i) _ => return acc.insert i
| _ => return acc
) SSet.empty forallBody
protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String):
Elab.TermElabM TacticResult := do
state.restoreElabM
let goal ← match state.savedState.tactic.goals.get? goalId with
| .some goal => pure goal
| .none => return .indexError goalId
goal.checkNotAssigned `GoalState.tryMotivatedApply
let recursor ← match Parser.runParserCategory
(env := state.env)
(catName := `term)
(input := recursor)
(fileName := filename) with
| .ok syn => pure syn
| .error error => return .parseError error
try
-- Implemented similarly to the intro tactic
let nextGoals: List MVarId ← goal.withContext do
let recursor ← Elab.Term.elabType (stx := recursor)
let recursorType ← Meta.inferType recursor
let (forallArgs, forallBody) := getForallArgsBody recursorType
let motiveIndices := collectMotiveArguments forallBody
let numArgs ← Meta.getExpectedNumArgs recursorType
let rec go (i: Nat): MetaM (List MVarId × Expr) := do
let argType := forallArgs.get! i
sorry
let (newMVars, assign) ← go numArgs
goal.assign assign
pure newMVars
return .success {
root := state.root,
savedState := {
term := ← MonadBacktrack.saveState,
tactic := { goals := nextGoals }
},
newMVars := nextGoals.toSSet,
parentMVar? := .some goal,
calcPrevRhs? := .none
}
catch exception =>
return .failure #[← exception.toMessageData.toString]
end Pantograph end Pantograph