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
3 changed files with 106 additions and 28 deletions
Showing only changes of commit 6ad24b72d4 - Show all commits

View File

@ -10,35 +10,94 @@ def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _
def unfoldAuxLemmas (e : Expr) : CoreM Expr := do def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
Lean.Meta.deltaExpand e Lean.Name.isAuxLemma Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
def instantiatePartialDelayedMVars (e: Expr): MetaM Expr := do /--
Meta.transform e Force the instantiation of delayed metavariables even if they cannot be fully
instantiated. This is used during resumption.
Since Lean 4 does not have an `Expr` constructor corresponding to delayed
metavariables, any delayed metavariables must be recursively handled by this
function to ensure that nested delayed metavariables can be properly processed.
The caveat is this recursive call will lead to infinite recursion if a loop
between metavariable assignment exists.
This function ensures any metavariable in the result is either
1. Delayed assigned with its pending mvar not assigned in any form
2. Not assigned (delay or not)
-/
partial def instantiateDelayedMVars (eOrig: Expr): MetaM Expr := do
--let padding := String.join $ List.replicate level " "
--IO.println s!"{padding}Starting {toString eOrig}"
let result ← Meta.transform (← instantiateMVars eOrig)
(pre := fun e => e.withApp fun f args => do (pre := fun e => e.withApp fun f args => do
--IO.println s!"{padding} V {toString e}"
if let .mvar mvarId := f then if let .mvar mvarId := f then
if ← mvarId.isAssigned then if ← mvarId.isAssigned then
return .visit <| (← instantiateMVars e) --IO.println s!"{padding} A ?{mvarId.name}"
if let some decl ← getDelayedMVarAssignment? mvarId then return .continue <| .some (← self e)
if args.size ≥ decl.fvars.size then if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
-- Do not use instantiateMVars here. Only one step of instantiation should happen. -- No progress can be made on this
let pending ← instantiateMVars (.mvar decl.mvarIdPending) if !(← mvarIdPending.isAssigned) then
if !pending.isMVar then --IO.println s!"{padding} D/T1: {toString e}"
let pending := pending.abstract decl.fvars let args ← args.mapM self
let pending := pending.instantiateRevRange 0 decl.fvars.size args let result := mkAppN f args
let pending := mkAppRange pending decl.fvars.size args.size args return .done result
return .visit <| pending
return .continue)
--IO.println s!"{padding} D ?{mvarId.name} := [{fvars.size}] ?{mvarIdPending.name}"
-- This asstion fails when a tactic or elaboration function is
-- implemented incorrectly. See `instantiateExprMVars`
if args.size < fvars.size then
--IO.println s!"{padding} Illegal callsite: {args.size} < {fvars.size}"
throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}"
assert! !(← mvarIdPending.isDelayedAssigned)
let pending ← self (.mvar mvarIdPending)
if pending == .mvar mvarIdPending then
-- No progress could be made on this case
--IO.println s!"{padding}D/N {toString e}"
assert! !(← mvarIdPending.isAssigned)
assert! !(← mvarIdPending.isDelayedAssigned)
--else if pending.isMVar then
-- assert! !(← pending.mvarId!.isAssigned)
-- assert! !(← pending.mvarId!.isDelayedAssigned)
-- -- Progress made, but this is now another delayed assigned mvar
-- let nextMVarId ← mkFreshMVarId
-- assignDelayedMVar nextMVarId fvars pending.mvarId!
-- let args ← args.mapM self
-- let result := mkAppN (.mvar nextMVarId) args
-- return .done result
else
-- Progress has been made on this mvar
let pending := pending.abstract fvars
let args ← args.mapM self
-- Craete the function call structure
let subst := pending.instantiateRevRange 0 fvars.size args
let result := mkAppRange subst fvars.size args.size args
--IO.println s!"{padding}D/T2 {toString result}"
return .done result
return .continue)
--IO.println s!"{padding}Result {toString result}"
return result
where
self e := instantiateDelayedMVars e
/--
Convert an expression to an equiavlent form with
1. No nested delayed assigned mvars
2. No aux lemmas
3. No assigned mvars
-/
@[export pantograph_instantiate_all_meta_m] @[export pantograph_instantiate_all_meta_m]
def instantiateAll (e: Expr): MetaM Expr := do def instantiateAll (e: Expr): MetaM Expr := do
let e ← instantiateMVars e let e ← instantiateDelayedMVars e
let e ← instantiatePartialDelayedMVars e
let e ← unfoldAuxLemmas e let e ← unfoldAuxLemmas e
return e return e
structure DelayedMVarInvocation where structure DelayedMVarInvocation where
mvarIdPending: MVarId mvarIdPending: MVarId
args: Array (FVarId × (Option Expr)) args: Array (FVarId × (Option Expr))
-- Extra arguments applied to the result of this substitution
tail: Array Expr tail: Array Expr
-- The pending mvar of any delayed assigned mvar must not be assigned in any way.
@[export pantograph_to_delayed_mvar_invocation_meta_m] @[export pantograph_to_delayed_mvar_invocation_meta_m]
def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do
let .mvar mvarId := e.getAppFn | return .none let .mvar mvarId := e.getAppFn | return .none
@ -48,7 +107,9 @@ def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := d
-- Print the function application e. See Lean's `withOverApp` -- Print the function application e. See Lean's `withOverApp`
let args := e.getAppArgs let args := e.getAppArgs
assert! args.size >= decl.fvars.size assert! args.size ≥ decl.fvars.size
assert! !(← mvarIdPending.isAssigned)
assert! !(← mvarIdPending.isDelayedAssigned)
let fvarArgMap: HashMap FVarId Expr := HashMap.ofList $ (decl.fvars.map (·.fvarId!) |>.zip args).toList let fvarArgMap: HashMap FVarId Expr := HashMap.ofList $ (decl.fvars.map (·.fvarId!) |>.zip args).toList
let subst ← mvarDecl.lctx.foldlM (init := []) λ acc localDecl => do let subst ← mvarDecl.lctx.foldlM (init := []) λ acc localDecl => do
let fvarId := localDecl.fvarId let fvarId := localDecl.fvarId

View File

@ -91,7 +91,7 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
where where
delayedMVarToSexp (e: Expr): MetaM (Option String) := do delayedMVarToSexp (e: Expr): MetaM (Option String) := do
let .some invocation ← toDelayedMVarInvocation e | return .none let .some invocation ← toDelayedMVarInvocation e | return .none
let callee ← self $ ← instantiateMVars $ .mvar invocation.mvarIdPending let callee ← self $ .mvar invocation.mvarIdPending
let sites ← invocation.args.mapM (λ (fvarId, arg) => do let sites ← invocation.args.mapM (λ (fvarId, arg) => do
let arg := match arg with let arg := match arg with
| .some arg => arg | .some arg => arg
@ -264,7 +264,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
name := ofName goal.name, name := ofName goal.name,
userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName), userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
isConversion := isLHSGoal? mvarDecl.type |>.isSome, isConversion := isLHSGoal? mvarDecl.type |>.isSome,
target := (← serializeExpression options (← instantiateAll mvarDecl.type)), target := (← serializeExpression options (← instantiate mvarDecl.type)),
vars := vars.reverse.toArray vars := vars.reverse.toArray
} }
where where

View File

@ -226,11 +226,25 @@ def test_or_comm: TestM Unit := do
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = let fvP := "_uniq.10"
#[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p q")] "q p"]) let fvQ := "_uniq.13"
let fvH := "_uniq.16"
let state1g0 := "_uniq.17"
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)) =
#[{
name := state1g0,
target := { pp? := .some "q p" },
vars := #[
{ name := fvP, userName := "p", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false },
{ name := fvQ, userName := "q", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false },
{ name := fvH, userName := "h", type? := .some { pp? := .some "p q" }, isInaccessible? := .some false }
]
}])
addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome
addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone
let state1parent ← serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false)
addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda h ((:c Or) 1 0) (:subst (:mv {state1g0}) (:fv {fvP}) (:fv {fvQ}) 0))))")
let tactic := "cases h" let tactic := "cases h"
let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
@ -239,22 +253,25 @@ def test_or_comm: TestM Unit := do
return () return ()
addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
#[branchGoal "inl" "p", branchGoal "inr" "q"]) #[branchGoal "inl" "p", branchGoal "inr" "q"])
let (caseL, caseR) := ("_uniq.62", "_uniq.75")
addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) =
#[caseL, caseR])
addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome
addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
let state2parent ← serializeExpressionSexp state2.parentExpr?.get! (sanitize := false) let state2parent ← serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) (sanitize := false)
let substHead := "((:c Or.casesOn) (:fv _uniq.10) (:fv _uniq.13) (:lambda t._@._hyg.26 ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:forall h ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) 0) ((:c Or) (:fv _uniq.13) (:fv _uniq.10)))) (:fv _uniq.16) (:lambda h._@._hyg.27 (:fv _uniq.10) (:subst (:lambda h._@._hyg.28 ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) ((:c Or.inl) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.47))) (:subst (:subst (:mv _uniq.59) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.47) (:fv _uniq.16) (:fv _uniq.50)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) (:fv _uniq.47) 0)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) 0)) (:lambda h._@._hyg.29 (:fv _uniq.13) (:subst (:lambda h._@._hyg.30 ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) ((:c Or.inr) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.60))) (:subst (:subst (:mv _uniq.72) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.60) (:fv _uniq.16) (:fv _uniq.63)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) (:fv _uniq.60) 0)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) 0)))" let orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))"
let extra := "((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16))" let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))"
addTest $ LSpec.test "(2 parent)" (state2parent == addTest $ LSpec.test "(2 parent)" (state2parent ==
s!"((:subst {substHead} (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) (:fv _uniq.16)) {extra})") s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) (:lambda t._@._hyg.26 {orPQ} (:forall h ((:c Eq) {orPQ} (:fv {fvH}) 0) {orQP})) (:fv {fvH}) (:lambda h._@._hyg.27 (:fv {fvP}) (:lambda h._@._hyg.28 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:mv {caseL}))) (:lambda h._@._hyg.29 (:fv {fvQ}) (:lambda h._@._hyg.30 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:mv {caseR}))) ((:c Eq.refl) {orPQ} (:fv {fvH})))")
let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
let state3_1parent ← serializeExpressionSexp state3_1.parentExpr?.get! (sanitize := false) let state3_1parent ← serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!) (sanitize := false)
addTest $ LSpec.test "(3_1 parent)" (state3_1parent == "((:c Or.inr) (:fv _uniq.13) (:fv _uniq.10) (:mv _uniq.78))") addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv _uniq.87))")
addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1) addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
let state4_1 ← match ← state3_1.tryTactic (goalId := 0) (tactic := "assumption") with let state4_1 ← match ← state3_1.tryTactic (goalId := 0) (tactic := "assumption") with
| .success state => pure state | .success state => pure state
@ -262,8 +279,8 @@ def test_or_comm: TestM Unit := do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
addTest $ LSpec.check " assumption" state4_1.goals.isEmpty addTest $ LSpec.check " assumption" state4_1.goals.isEmpty
let state4_1parent ← serializeExpressionSexp state4_1.parentExpr?.get! (sanitize := false) let state4_1parent ← instantiateAll state4_1.parentExpr?.get!
addTest $ LSpec.test "(4_1 parent)" (state4_1parent == "(:fv _uniq.47)") addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar
addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone
let state3_2 ← match ← state2.tryTactic (goalId := 1) (tactic := "apply Or.inl") with let state3_2 ← match ← state2.tryTactic (goalId := 1) (tactic := "apply Or.inl") with
| .success state => pure state | .success state => pure state