diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 176e48e..0fdf2e1 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -547,7 +547,7 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu try -- Implemented similarly to the intro tactic let nextGoals: List MVarId ← goal.withContext do - let recursor ← Elab.Term.elabType (stx := recursor) + let recursor ← Elab.Term.elabTerm (stx := recursor) .none let recursorType ← Meta.inferType recursor let (forallArgs, forallBody) := getForallArgsBody recursorType @@ -555,14 +555,24 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu let numArgs ← Meta.getExpectedNumArgs recursorType - let rec go (i: Nat): MetaM (List MVarId × Expr) := do - let argType := forallArgs.get! i - sorry - let (newMVars, assign) ← go numArgs + let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do + if i ≥ numArgs then + return prev + else + let argType := forallArgs.get! i + -- If `argType` has motive references, its goal needs to be placed in it + let argType := argType.instantiateRev prev + -- Create the goal + let argGoal ← Meta.mkFreshExprMVar argType .natural .anonymous + let prev := prev ++ [argGoal] + go (i + 1) prev + termination_by numArgs - i + let newMVars ← go 0 #[] - goal.assign assign + -- Create the main goal for the return type of the recursor + goal.assign (mkAppN recursor newMVars) - pure newMVars + pure $ newMVars.toList.map (·.mvarId!) return .success { root := state.root, savedState := { diff --git a/Test/Common.lean b/Test/Common.lean index 8719ebd..8b8e977 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -10,11 +10,9 @@ namespace Pantograph -- Auxiliary functions namespace Protocol -/-- Set internal names to "" -/ -def Goal.devolatilize (goal: Goal): Goal := +def Goal.devolatilizeVars (goal: Goal): Goal := { goal with - name := "", vars := goal.vars.map removeInternalAux, } where removeInternalAux (v: Variable): Variable := @@ -22,6 +20,13 @@ def Goal.devolatilize (goal: Goal): Goal := v with name := "" } +/-- Set internal names to "" -/ +def Goal.devolatilize (goal: Goal): Goal := + { + goal.devolatilizeVars with + name := "", + } + deriving instance DecidableEq, Repr for Expression deriving instance DecidableEq, Repr for Variable deriving instance DecidableEq, Repr for Goal diff --git a/Test/Proofs.lean b/Test/Proofs.lean index e14ba4a..ae94054 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -49,6 +49,16 @@ def startProof (start: Start): TestM (Option GoalState) := do let goal ← GoalState.create (expr := expr) return Option.some goal +def buildNamedGoal (name: String) (nameType: List (String × String)) (target: String): Protocol.Goal := + { + name, + target := { pp? := .some target}, + vars := (nameType.map fun x => ({ + userName := x.fst, + type? := .some { pp? := .some x.snd }, + isInaccessible? := .some false + })).toArray + } def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): Protocol.Goal := { userName?, @@ -582,7 +592,7 @@ def test_let (specialized: Bool): TestM Unit := do interiorGoal [] "let b := ?m.20;\np ∨ ¬p" ]) -- Check that the goal mvar ids match up - addTest $ LSpec.check expr ((serializedState2.map (·.name) |>.get! 0) = "_uniq.20") + addTest $ LSpec.check "(mvarId)" ((serializedState2.map (·.name) |>.get! 0) = "_uniq.20") let tactic := "exact a" let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with @@ -625,6 +635,80 @@ def test_let (specialized: Bool): TestM Unit := do let free := [("a", "Nat"), ("p", "Prop"), ("h", "p")] ++ free buildGoal free target userName? +def test_nat_zero_add: TestM Unit := do + let state? ← startProof (.expr "∀ (n: Nat), n + 0 = n") + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + let tactic := "intro n" + let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = + #[buildGoal [("n", "Nat")] "n + 0 = n"]) + let recursor := "@Nat.brecOn" + let state2 ← match ← state1.tryMotivatedApply (goalId := 0) (recursor := recursor) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) = + #[ + buildNamedGoal "_uniq.70" [("n", "Nat")] "Nat → Sort ?u.66", + buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat", + buildNamedGoal "_uniq.72" [("n", "Nat")] "(t : Nat) → Nat.below t → ?m.70 t" + ]) + + let tactic := "exact n" + let state3b ← match ← state2.tryTactic (goalId := 1) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check tactic ((← state3b.serializeGoals (options := ← read)).map (·.devolatilize) = + #[]) + let state2b ← match state3b.continue state2 with + | .ok state => pure state + | .error e => do + addTest $ assertUnreachable e + return () + let tactic := "exact (λ x => x + 0 = x)" + let state3c ← match ← state2b.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check tactic ((← state3c.serializeGoals (options := ← read)).map (·.devolatilize) = + #[]) + let state2c ← match state3c.continue state2b with + | .ok state => pure state + | .error e => do + addTest $ assertUnreachable e + return () + let tactic := "intro t h" + let state3 ← match ← state2c.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check tactic ((← state3.serializeGoals (options := ← read)).map (·.devolatilize) = + #[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"]) + + let tactic := "simp" + let stateF ← match ← state3.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check tactic ((← stateF.serializeGoals (options := ← read)) = + #[]) + + addTest $ LSpec.check "(F root)" stateF.rootExpr?.isSome + def suite (env: Environment): List (String × IO LSpec.TestSeq) := let tests := [ ("Nat.add_comm", test_nat_add_comm false), @@ -637,6 +721,7 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) := ("calc", test_calc), ("let via assign", test_let false), ("let via tryLet", test_let true), + ("Nat.zero_add", test_nat_zero_add), ] tests.map (fun (name, test) => (name, proofRunner env test))