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

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

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 resultant ← goal.getType
-    let motiveIndices := collectMotiveArguments forallBody
-    --IO.println s!"{motiveIndices.toList} from {← Meta.ppExpr forallBody}"
 
-    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 bvarIndex := info.nArgs - i - 1
-        let userName := if motiveIndices.contains (numArgs - i - 1) then `motive else .anonymous
+        let argGoal ← if bvarIndex = info.iMotive then
-        let argGoal ← Meta.mkFreshExprMVar argType .syntheticOpaque (userName := userName)
+            let surrogateMotiveType ← info.surrogateMotiveType resultant
-        IO.println s!"Creating [{i}] {← Meta.ppExpr argGoal}"
+            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
+      termination_by info.nArgs - i
-    let newMVars ← go 0 #[]
+    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

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

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.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
-      buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat",
+      buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat" (.some "major"),
-      buildNamedGoal "_uniq.72" [("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 ?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) :=

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