From 3812aa56ecb871a9531d3cabec61a51eab7acbde Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 22 Apr 2024 00:11:41 -0700 Subject: [PATCH] feat: Phantom var in mapply --- Makefile | 4 +- Pantograph/Goal.lean | 2 +- Pantograph/Tactic/MotivatedApply.lean | 88 +++++++++++++++++++++------ Test/Common.lean | 6 ++ Test/Proofs.lean | 9 ++- Test/Tactic/MotivatedApply.lean | 65 +++++++++++++++++++- 6 files changed, 147 insertions(+), 27 deletions(-) diff --git a/Makefile b/Makefile index 5d4ad6b..86f9e5b 100644 --- a/Makefile +++ b/Makefile @@ -1,9 +1,9 @@ LIB := ./.lake/build/lib/Pantograph.olean EXE := ./.lake/build/bin/pantograph -SOURCE := $(wildcard Pantograph/*.lean) $(wildcard *.lean) lean-toolchain +SOURCE := $(wildcard *.lean Pantograph/*.lean Pantograph/**/*.lean) lean-toolchain TEST_EXE := ./.lake/build/bin/test -TEST_SOURCE := $(wildcard Test/*.lean) +TEST_SOURCE := $(wildcard Test/*.lean Test/**/*.lean) $(LIB) $(EXE): $(SOURCE) lake build pantograph diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 0b7e306..17d94c0 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -126,7 +126,7 @@ protected def GoalState.continue (target: GoalState) (branch: GoalState): Except protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do let expr ← goalState.mctx.eAssignment.find? goalState.root let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) - if expr.hasMVar then + if expr.hasExprMVar then -- Must not assert that the goal state is empty here. We could be in a branch goal. --assert! ¬goalState.goals.isEmpty .none diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean index 817942d..9826e3d 100644 --- a/Pantograph/Tactic/MotivatedApply.lean +++ b/Pantograph/Tactic/MotivatedApply.lean @@ -9,6 +9,54 @@ def getForallArgsBody: Expr → List Expr × Expr let (innerArgs, innerBody) := getForallArgsBody b (d :: innerArgs, innerBody) | e => ([], e) + +def replaceForallBody: Expr → Expr → Expr + | .forallE param domain body binderInfo, target => + let body := replaceForallBody body target + .forallE param domain body binderInfo + | _, target => target + +structure RecursorWithMotive where + args: List Expr + body: Expr + + -- .bvar index for the motive and major from the body + iMotive: Nat + iMajor: Nat + +namespace RecursorWithMotive + +protected def nArgs (info: RecursorWithMotive): Nat := info.args.length + +protected def getMotiveType (info: RecursorWithMotive): Expr := + let level := info.nArgs - info.iMotive - 1 + let a := info.args.get! level + a + +protected def surrogateMotiveType (info: RecursorWithMotive) (resultant: Expr): MetaM Expr := do + let motiveType := info.getMotiveType + let resultantType ← Meta.inferType resultant + return replaceForallBody motiveType resultantType + +protected def phantomType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do + let goalMotive := mvars.get! (info.nArgs - info.iMotive - 1) + let goalMajor := mvars.get! (info.nArgs - info.iMajor - 1) + Meta.mkEq (.app goalMotive goalMajor) resultant + +end RecursorWithMotive + +def getRecursorInformation (recursorType: Expr): Option RecursorWithMotive := do + let (args, body) := getForallArgsBody recursorType + let (iMotive, iMajor) ← match body with + | .app (.bvar iMotive) (.bvar iMajor) => pure (iMotive, iMajor) + | _ => .none + return { + args, + body, + iMotive, + iMajor, + } + def collectMotiveArguments (forallBody: Expr): SSet Nat := match forallBody with | .app (.bvar i) _ => SSet.empty.insert i @@ -21,38 +69,38 @@ def motivatedApply: Elab.Tactic.Tactic := λ stx => do let recursor ← Elab.Term.elabTerm (stx := stx) .none let recursorType ← Meta.inferType recursor - let (forallArgs, forallBody) := getForallArgsBody recursorType - let motiveIndices := collectMotiveArguments forallBody - --IO.println s!"{motiveIndices.toList} from {← Meta.ppExpr forallBody}" + let resultant ← goal.getType - let numArgs ← Meta.getExpectedNumArgs recursorType + let info ← match getRecursorInformation recursorType with + | .some info => pure info + | .none => throwError "Recursor return type does not correspond with the invocation of a motive: {← Meta.ppExpr recursorType}" let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do - if i ≥ numArgs then + if i ≥ info.nArgs then return prev else - let argType := forallArgs.get! i + let argType := info.args.get! i -- If `argType` has motive references, its goal needs to be placed in it let argType := argType.instantiateRev prev - -- Create the goal - let userName := if motiveIndices.contains (numArgs - i - 1) then `motive else .anonymous - let argGoal ← Meta.mkFreshExprMVar argType .syntheticOpaque (userName := userName) - IO.println s!"Creating [{i}] {← Meta.ppExpr argGoal}" + let bvarIndex := info.nArgs - i - 1 + let argGoal ← if bvarIndex = info.iMotive then + let surrogateMotiveType ← info.surrogateMotiveType resultant + Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive) + else if bvarIndex = info.iMajor then + Meta.mkFreshExprMVar argType .syntheticOpaque (userName := `major) + else + Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous) let prev := prev ++ [argGoal] go (i + 1) prev - termination_by numArgs - i - let newMVars ← go 0 #[] + termination_by info.nArgs - i + let mut newMVars ← go 0 #[] - -- FIXME: Add an `Eq` target and swap out the motive type - - --let sourceType := forallBody.instantiateRev newMVars - --unless ← withTheReader Meta.Context (λ ctx => { ctx with config := { ctx.config with } }) $ - -- Meta.isDefEq sourceType (← goal.getType) do - -- throwError "invalid mapply: The resultant type {← Meta.ppExpr sourceType} cannot be unified with {← Meta.ppExpr $ ← goal.getType}" - - -- Create the main goal for the return type of the recursor goal.assign (mkAppN recursor newMVars) + let phantomType ← info.phantomType newMVars resultant + let goalPhantom ← Meta.mkFreshExprMVar phantomType .syntheticOpaque (userName := `phantom) + newMVars := newMVars ++ [goalPhantom] + let nextGoals ← newMVars.toList.map (·.mvarId!) |>.filterM (not <$> ·.isAssigned) pure nextGoals Elab.Tactic.setGoals nextGoals diff --git a/Test/Common.lean b/Test/Common.lean index 8b8e977..6ea4fb2 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -63,6 +63,12 @@ def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSe def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α := termElabM.run' (ctx := Pantograph.defaultTermElabMContext) +def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e + +def runTacticOnMVar (tacticM: Elab.Tactic.TacticM Unit) (goal: MVarId): Elab.TermElabM (List MVarId) := do + let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] } + return newGoals.goals + end Test end Pantograph diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 1adc9d4..43c346b 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -661,9 +661,10 @@ def test_nat_zero_add: TestM Unit := do return () addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) = #[ - buildNamedGoal "_uniq.70" [("n", "Nat")] "Nat → Sort ?u.66" (.some "motive"), - buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat", - buildNamedGoal "_uniq.72" [("n", "Nat")] "(t : Nat) → Nat.below t → ?motive t" + buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"), + buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat" (.some "major"), + buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t", + buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?major = (n + 0 = n)" (.some "phantom") ]) let tactic := "exact n" @@ -710,6 +711,8 @@ def test_nat_zero_add: TestM Unit := do addTest $ LSpec.check tactic ((← stateF.serializeGoals (options := ← read)) = #[]) + let expr := stateF.mctx.eAssignment.find! stateF.root + let (expr, _) := instantiateMVarsCore (mctx := stateF.mctx) (e := expr) addTest $ LSpec.check "(F root)" stateF.rootExpr?.isSome def suite (env: Environment): List (String × IO LSpec.TestSeq) := diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean index 04d7825..60ed7be 100644 --- a/Test/Tactic/MotivatedApply.lean +++ b/Test/Tactic/MotivatedApply.lean @@ -1,11 +1,74 @@ import LSpec import Lean +import Test.Common open Lean +open Pantograph namespace Pantograph.Test.Tactic.MotivatedApply +def valueAndType (recursor: String): MetaM (Expr × Expr) := do + let recursor ← match Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := recursor) + (fileName := filename) with + | .ok syn => pure syn + | .error error => throwError "Failed to parse: {error}" + runTermElabMInMeta do + let recursor ← Elab.Term.elabTerm (stx := recursor) .none + let recursorType ← Meta.inferType recursor + return (recursor, recursorType) + + +def test_type_extract (env: Environment): IO LSpec.TestSeq := + runMetaMSeq env do + let mut tests := LSpec.TestSeq.done + let (recursor, recursorType) ← valueAndType "@Nat.brecOn" + tests := tests ++ LSpec.check "recursorType" ("{motive : Nat → Sort ?u.1} → (t : Nat) → ((t : Nat) → Nat.below t → motive t) → motive t" = + (← exprToStr recursorType)) + let info ← match Tactic.getRecursorInformation recursorType with + | .some info => pure info + | .none => throwError "Failed to extract recursor info" + tests := tests ++ LSpec.check "iMotive" (info.iMotive = 2) + tests := tests ++ LSpec.check "iMajor" (info.iMajor = 1) + let motiveType := info.getMotiveType + tests := tests ++ LSpec.check "motiveType" ("Nat → Sort ?u.1" = + (← exprToStr motiveType)) + return tests + +def test_execute (env: Environment): IO LSpec.TestSeq := + let expr := "λ (n t: Nat) => n + 0 = n" + runMetaMSeq env do + let (expr, exprType) ← valueAndType expr + Meta.lambdaTelescope expr $ λ _ body => do + let recursor ← match Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := "@Nat.brecOn") + (fileName := filename) with + | .ok syn => pure syn + | .error error => throwError "Failed to parse: {error}" + let mut tests := LSpec.TestSeq.done + -- Apply the tactic + let target ← Meta.mkFreshExprSyntheticOpaqueMVar body + let tactic := Tactic.motivatedApply recursor + let test ← runTermElabMInMeta do + let newGoals ← runTacticOnMVar tactic target.mvarId! + pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = + [ + "Nat → Prop", + "Nat", + "∀ (t : Nat), Nat.below t → ?motive t", + "?motive ?major = (n + 0 = n)", + ]) + tests := tests ++ test + return tests + def suite (env: Environment): List (String × IO LSpec.TestSeq) := - [] + [ + ("type_extract", test_type_extract env), + ("execute", test_execute env), + ] end Pantograph.Test.Tactic.MotivatedApply