From 4ee955c21fd7d51b0d5e2b9933a1c7854a5d1970 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 12 Apr 2024 21:16:00 -0700 Subject: [PATCH 1/3] test: Tests the `let` tactic --- Test/Proofs.lean | 72 ++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 70 insertions(+), 2 deletions(-) diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 1b1b9de..9837e04 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -542,14 +542,81 @@ def test_calc: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.test "(4m root)" state4m.rootExpr?.isSome - - where interiorGoal (free: List (String × String)) (target: String) (userName?: Option String := .none) := let free := [("a", "Nat"), ("b", "Nat"), ("c", "Nat"), ("d", "Nat"), ("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free buildGoal free target userName? +def test_let: TestM Unit := do + let state? ← startProof (.expr "∀ (a: Nat) (p: Prop), p → p ∨ ¬p") + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + let tactic := "intro a p h" + 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) = + #[interiorGoal [] "p ∨ ¬p"]) + + let expr := "let b: Nat := _; _" + let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check expr ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = + #[ + interiorGoal [] "Nat", + interiorGoal [] "let b := ?m.20;\np ∨ ¬p" + ]) + + let tactic := "exact a" + let state3 ← match ← state2.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) = #[]) + + let state3r ← match state3.continue state2 with + | .error msg => do + addTest $ assertUnreachable $ msg + return () + | .ok state => pure state + addTest $ LSpec.check "(continue)" ((← state3r.serializeGoals (options := ← read)).map (·.devolatilize) = + #[interiorGoal [] "let b := a;\np ∨ ¬p"]) + + let tactic := "exact h" + match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with + | .failure #[message] => + addTest $ LSpec.check tactic (message = "type mismatch\n h\nhas type\n p : Prop\nbut is expected to have type\n let b := a;\n p ∨ ¬p : Prop") + | other => do + addTest $ assertUnreachable $ other.toString + + let tactic := "intro b" + let state4 ← match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + let tactic := "exact Or.inl h" + let state5 ← match ← state4.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.test "(5 root)" state5.rootExpr?.isSome + where + interiorGoal (free: List (String × String)) (target: String) (userName?: Option String := .none) := + let free := [("a", "Nat"), ("p", "Prop"), ("h", "p")] ++ free + buildGoal free target userName? + def suite (env: Environment): List (String × IO LSpec.TestSeq) := let tests := [ ("Nat.add_comm", test_nat_add_comm false), @@ -560,6 +627,7 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) := ("have", test_have), ("conv", test_conv), ("calc", test_calc), + ("let", test_let), ] tests.map (fun (name, test) => (name, proofRunner env test)) -- 2.44.1 From 77907fd0609eb5db081b25dabca4fbf4a5f98e00 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 12 Apr 2024 21:30:56 -0700 Subject: [PATCH 2/3] feat: `goalLet` function --- Pantograph/Goal.lean | 46 +++++++++++++++++++++++++++++++++++++++++ Pantograph/Library.lean | 3 +++ Test/Proofs.lean | 10 ++++++--- 3 files changed, 56 insertions(+), 3 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index f1c2503..484ff51 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -177,6 +177,7 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr): }, newMVars, parentMVar? := .some goal, + calcPrevRhs? := .none } catch exception => return .failure #[← exception.toMessageData.toString] @@ -249,6 +250,49 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St }, newMVars := nextGoals.toSSet, parentMVar? := .some goal, + calcPrevRhs? := .none + } + catch exception => + return .failure #[← exception.toMessageData.toString] +protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): + Elab.TermElabM TacticResult := do + state.restoreElabM + let goal ← match state.savedState.tactic.goals.get? goalId with + | .some goal => pure goal + | .none => return .indexError goalId + let type ← match Parser.runParserCategory + (env := state.env) + (catName := `term) + (input := type) + (fileName := filename) with + | .ok syn => pure syn + | .error error => return .parseError error + let binderName := binderName.toName + try + -- Implemented similarly to the intro tactic + let nextGoals: List MVarId ← goal.withContext do + let type ← Elab.Term.elabType (stx := type) + let lctx ← MonadLCtx.getLCtx + + -- The branch goal inherits the same context, but with a different type + let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type + + let upstreamType := .letE binderName type mvarBranch (← goal.getType) false + let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) + upstreamType (kind := MetavarKind.synthetic) (userName := (← goal.getTag)) + + goal.assign mvarUpstream + + pure [mvarBranch.mvarId!, mvarUpstream.mvarId!] + return .success { + root := state.root, + savedState := { + term := ← MonadBacktrack.saveState, + tactic := { goals := nextGoals } + }, + newMVars := nextGoals.toSSet, + parentMVar? := .some goal, + calcPrevRhs? := .none } catch exception => return .failure #[← exception.toMessageData.toString] @@ -280,6 +324,7 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat): newMVars := newMVarSet prevMCtx nextMCtx, parentMVar? := .some goal, convMVar? := .some (convRhs, goal), + calcPrevRhs? := .none } catch exception => return .failure #[← exception.toMessageData.toString] @@ -318,6 +363,7 @@ protected def GoalState.convExit (state: GoalState): newMVars := newMVarSet prevMCtx nextMCtx, parentMVar? := .some convGoal, convMVar? := .none + calcPrevRhs? := .none } catch exception => return .failure #[← exception.toMessageData.toString] diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index ff365b2..17925cd 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -169,6 +169,9 @@ def goalAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM Tacti @[export pantograph_goal_have_m] def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult := runTermElabM <| state.tryHave goalId binderName type +@[export pantograph_goal_let_m] +def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult := + runTermElabM <| state.tryLet goalId binderName type @[export pantograph_goal_conv_m] def goalConv (state: GoalState) (goalId: Nat): Lean.CoreM TacticResult := diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 9837e04..4f81085 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -548,7 +548,7 @@ def test_calc: TestM Unit := do ("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free buildGoal free target userName? -def test_let: TestM Unit := do +def test_let (specialized: Bool): TestM Unit := do let state? ← startProof (.expr "∀ (a: Nat) (p: Prop), p → p ∨ ¬p") let state0 ← match state? with | .some state => pure state @@ -565,7 +565,10 @@ def test_let: TestM Unit := do #[interiorGoal [] "p ∨ ¬p"]) let expr := "let b: Nat := _; _" - let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with + let result2 ← match specialized with + | true => state1.tryLet (goalId := 0) (binderName := "b") (type := "Nat") + | false => state1.tryAssign (goalId := 0) (expr := expr) + let state2 ← match result2 with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -627,7 +630,8 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) := ("have", test_have), ("conv", test_conv), ("calc", test_calc), - ("let", test_let), + ("let via assign", test_let false), + ("let via tryLet", test_let true), ] tests.map (fun (name, test) => (name, proofRunner env test)) -- 2.44.1 From b45b90b810c845629788eca844a68873305bd1fd Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 12 Apr 2024 21:41:16 -0700 Subject: [PATCH 3/3] test: Metavariable name matches in let --- Test/Proofs.lean | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 4f81085..ad22e8d 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -564,20 +564,25 @@ def test_let (specialized: Bool): TestM Unit := do addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = #[interiorGoal [] "p ∨ ¬p"]) - let expr := "let b: Nat := _; _" + + let letType := "Nat" + let expr := s!"let b: {letType} := _; _" let result2 ← match specialized with - | true => state1.tryLet (goalId := 0) (binderName := "b") (type := "Nat") + | true => state1.tryLet (goalId := 0) (binderName := "b") (type := letType) | false => state1.tryAssign (goalId := 0) (expr := expr) let state2 ← match result2 with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check expr ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = + let serializedState2 ← state2.serializeGoals (options := ← read) + addTest $ LSpec.check expr (serializedState2.map (·.devolatilize) = #[ - interiorGoal [] "Nat", + interiorGoal [] letType, 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") let tactic := "exact a" let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with -- 2.44.1