Pantograph/Tactic/MotivatedApply.lean

@@ -22,6 +22,7 @@ structure RecursorWithMotive where
 
   -- .bvar index for the motive and major from the body
   iMotive: Nat
+  iMajor: Nat
 
 namespace RecursorWithMotive
 
@@ -37,23 +38,23 @@ protected def surrogateMotiveType (info: RecursorWithMotive) (resultant: Expr):
   let resultantType ← Meta.inferType resultant
   return replaceForallBody motiveType resultantType
 
-protected def conduitType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do
-  let motiveCall := Expr.instantiateRev info.body mvars
-  Meta.mkEq motiveCall resultant
+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
-  if ¬ body.isApp then
-    .none
-  let iMotive ← match body.getAppFn with
-    | .bvar iMotive => pure iMotive
+  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 :=
@@ -85,6 +86,8 @@ def motivatedApply: Elab.Tactic.Tactic := λ stx => do
         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]
@@ -92,11 +95,11 @@ def motivatedApply: Elab.Tactic.Tactic := λ stx => do
       termination_by info.nArgs - i
     let mut newMVars ← go 0 #[]
 
-    -- Create the conduit type which proves the result of the motive is equal to the goal
-    let conduitType ← info.conduitType newMVars resultant
-    let goalConduit ← Meta.mkFreshExprMVar conduitType .syntheticOpaque (userName := `conduit)
-    goal.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars)
-    newMVars := newMVars ++ [goalConduit]
+    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

Test/Proofs.lean

@@ -662,9 +662,9 @@ def test_nat_zero_add: TestM Unit := do
   addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
     #[
       buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
-      buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat",
+      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 ?m.68 = (n + 0 = n)" (.some "conduit")
+      buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?major = (n + 0 = n)" (.some "phantom")
     ])
 
   let tactic := "exact n"
@@ -703,18 +703,7 @@ def test_nat_zero_add: TestM Unit := do
     #[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"])
 
   let tactic := "simp"
-  let state3d ← match ← state3.tryTactic (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  let state2d ← match state3d.continue state2c with
-    | .ok state => pure state
-    | .error e => do
-      addTest $ assertUnreachable e
-      return ()
-  let tactic := "rfl"
-  let stateF ← match ← state2d.tryTactic (goalId := 0) (tactic := tactic) with
+  let stateF ← match ← state3.tryTactic (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString

Test/Tactic/MotivatedApply.lean

@@ -31,6 +31,7 @@ def test_type_extract (env: Environment): IO LSpec.TestSeq :=
       | .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))
@@ -59,7 +60,7 @@ def test_execute (env: Environment): IO LSpec.TestSeq :=
             "Nat → Prop",
             "Nat",
             "∀ (t : Nat), Nat.below t → ?motive t",
-            "?motive ?m.69 = (n + 0 = n)",
+            "?motive ?major = (n + 0 = n)",
           ])
       tests := tests ++ test
       return tests