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
2 changed files with 31 additions and 20 deletions
Showing only changes of commit f813d4a8dd - Show all commits

View File

@ -101,6 +101,26 @@ partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
| _, .zero => s!"{k}" | _, .zero => s!"{k}"
| _, _ => s!"(+ {u_str} {k})" | _, _ => s!"(+ {u_str} {k})"
structure DelayedMVarInvocation where
mvarIdPending: MVarId
args: Array (FVarId × Expr)
tail: Array Expr
def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := 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
assert! args.size >= decl.fvars.size
return .some {
mvarIdPending,
args := decl.fvars.map (·.fvarId!) |>.zip args,
tail := args.toList.drop decl.fvars.size |>.toArray,
}
/-- /--
Completely serializes an expression tree. Json not used due to compactness Completely serializes an expression tree. Json not used due to compactness
@ -111,30 +131,19 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
self expr self expr
where where
delayedMVarToSexp (e: Expr): MetaM (Option String) := do delayedMVarToSexp (e: Expr): MetaM (Option String) := do
let .mvar mvarId := e.getAppFn | return .none let .some invocation ← toDelayedMVarInvocation e | return .none
let .some decl ← getDelayedMVarAssignment? mvarId | return .none let callee ← self $ ← instantiateMVars $ .mvar invocation.mvarIdPending
let mvarIdPending := decl.mvarIdPending let sites ← invocation.args.mapM (λ (fvar, arg) => do
-- Print the function application e. See Lean's `withOverApp` pure s!"({toString fvar.name} {← self arg})"
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 tailArgs ← invocation.tail.mapM self
let sites := " ".intercalate sites.toList let sites := " ".intercalate sites.toList
let result := if tailArgs.isEmpty then let result := if tailArgs.isEmpty then
s!"(:subst {callee} {sites})" s!"(:subst {callee} {sites})"
else else
let tailArgs := " ".intercalate tailArgs let tailArgs := " ".intercalate tailArgs.toList
s!"((:subst {callee} {sites}) {tailArgs})" s!"((:subst {callee} {sites}) {tailArgs})"
return .some result return .some result

View File

@ -748,10 +748,11 @@ def test_nat_zero_add_alt: TestM Unit := do
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
let major := "_uniq.68"
addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) = addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
#[ #[
buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"), buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat", buildNamedGoal major [("n", "Nat")] "Nat",
buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t", buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit") buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
]) ])
@ -770,7 +771,8 @@ def test_nat_zero_add_alt: TestM Unit := do
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = ["_uniq.85", "_uniq.86", "_uniq.84"] let (eqL, eqR, eqT) := ("_uniq.85", "_uniq.86", "_uniq.84")
addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = [eqL, eqR, eqT]
let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict" let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict"
let state2b ← match state3m2.resume [conduit] with let state2b ← match state3m2.resume [conduit] with
| .ok state => pure state | .ok state => pure state
@ -788,7 +790,7 @@ def test_nat_zero_add_alt: TestM Unit := do
userName? := .some "conduit", userName? := .some "conduit",
target := { target := {
pp? := .some "?m.79 ?m.68 = (n + 0 = n)", 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})))", sexp? := .some s!"((:c Eq) (:sort 0) (:subst ((:c Eq) (:mv {eqT}) (:mv {eqL}) (:mv {eqR})) (_uniq.77 (:mv {major}))) ((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN})))",
}, },
vars := #[{ vars := #[{
name := fvN, name := fvN,