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
5 changed files with 65 additions and 11 deletions
Showing only changes of commit c04b363de7 - Show all commits

View File

@ -98,7 +98,8 @@ Brings into scope a list of goals
-/
protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState :=
if ¬ (goals.all (λ goal => state.mvars.contains goal)) then
.error s!"Goals not in scope"
let invalid_goals := goals.filter (λ goal => ¬ state.mvars.contains goal) |>.map (·.name.toString)
.error s!"Goals {invalid_goals} are not in scope"
else
-- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
let unassigned := goals.filter (λ goal =>

View File

@ -32,7 +32,7 @@ def instantiatePartialDelayedMVars (e: Expr): MetaM Expr := do
def instantiateAll (e: Expr): MetaM Expr := do
let e ← instantiateMVars e
let e ← unfoldAuxLemmas e
let e ← instantiatePartialDelayedMVars e
--let e ← instantiatePartialDelayedMVars e
return e
--- Input Functions ---
@ -101,6 +101,7 @@ partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
| _, .zero => s!"{k}"
| _, _ => s!"(+ {u_str} {k})"
/--
Completely serializes an expression tree. Json not used due to compactness
@ -109,7 +110,37 @@ A `_` symbol in the AST indicates automatic deductions not present in the origin
partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do
self expr
where
self (e: Expr): MetaM String :=
delayedMVarToSexp (e: Expr): MetaM (Option String) := do
let .mvar mvarId := e.getAppFn | return .none
let .some decl ← getDelayedMVarAssignment? mvarId | return .none
let mvarIdPending := decl.mvarIdPending
-- Print the function application e. See Lean's `withOverApp`
let args := e.getAppArgs
-- Not enough arguments to instantiate this
if args.size < decl.fvars.size then
return .none
let callee ← self $ ← instantiateMVars $ .mvar mvarIdPending
let sites ←
decl.fvars.zip args |>.mapM (λ (fvar, arg) => do
let fvarName := Expr.fvarId! fvar |>.name
return s!"({toString fvarName} {← self arg})"
)
let tailArgs ← args.toList.drop decl.fvars.size |>.mapM self
let sites := " ".intercalate sites.toList
let result := if tailArgs.isEmpty then
s!"(:subst {callee} {sites})"
else
let tailArgs := " ".intercalate tailArgs
s!"((:subst {callee} {sites}) {tailArgs})"
return .some result
self (e: Expr): MetaM String := do
if let .some result ← delayedMVarToSexp e then
return result
match e with
| .bvar deBruijnIndex =>
-- This is very common so the index alone is shown. Literals are handled below.

View File

@ -88,11 +88,11 @@ def test_tactic : IO LSpec.TestSeq :=
vars := #[{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
}
let goal2: Protocol.Goal := {
name := "_uniq.17",
name := "_uniq.14",
target := { pp? := .some "x y → y x" },
vars := #[
{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
{ name := "_uniq.16", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
{ name := "_uniq.13", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
],
}
subroutine_runner [

View File

@ -263,7 +263,7 @@ def test_partial_continuation: TestM Unit := do
-- Continuation should fail if the state does not exist:
match state0.resume coupled_goals with
| .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals not in scope")
| .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals [_uniq.40, _uniq.41, _uniq.38, _uniq.47] are not in scope")
| .ok _ => addTest $ assertUnreachable "(continuation failure)"
-- Continuation should fail if some goals have not been solved
match state2.continue state1 with

View File

@ -243,9 +243,10 @@ def test_or_comm: TestM Unit := do
addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
let state2parent ← serializeExpressionSexp state2.parentExpr?.get! (sanitize := false)
-- This is due to delayed assignment
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) (_uniq.54 (:fv _uniq.16)) (_uniq.55 (:fv _uniq.50))) (_uniq.50 0))) (_uniq.47 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) (_uniq.67 (:fv _uniq.16)) (_uniq.68 (:fv _uniq.63))) (_uniq.63 0))) (_uniq.60 0))))"
let extra := "((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))"
addTest $ LSpec.test "(2 parent)" (state2parent ==
"((:mvd _uniq.43) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))")
s!"((:subst {substHead} (_uniq.41 (:fv _uniq.16))) {extra}")
let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with
| .success state => pure state
@ -769,13 +770,34 @@ def test_nat_zero_add_alt: TestM Unit := do
| other => do
addTest $ assertUnreachable $ other.toString
return ()
let state2b ← match state3m2.resume (state3m2.goals ++ state2.goals) with
addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = ["_uniq.85", "_uniq.86", "_uniq.84"]
let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict"
let state2b ← match state3m2.resume [conduit] with
| .ok state => pure state
| .error e => do
addTest $ assertUnreachable e
return ()
addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
#[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"])
let cNatAdd := "(:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat))"
let cNat0 := "((:c OfNat.ofNat) (:c Nat) (:lit 0) ((:c instOfNatNat) (:lit 0)))"
let fvN := "_uniq.63"
addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) =
#[
{
name := "_uniq.70",
userName? := .some "conduit",
target := {
pp? := .some "?m.79 ?m.68 = (n + 0 = n)",
sexp? := .some s!"((:c Eq) (:sort 0) (:subst ((:c Eq) (:mv _uniq.84) (:mv _uniq.85) (:mv _uniq.86)) (_uniq.77 (:mv _uniq.68))) ((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN})))",
},
vars := #[{
name := fvN,
userName := "n",
type? := .some { pp? := .some "Nat", sexp? := .some "(:c Nat)" },
isInaccessible? := .some false
}],
}
])
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
let tests := [