test: Tactic failure on synthesizing placeholder

This commit is contained in:
Leni Aniva 2024-12-09 08:15:01 -08:00
parent d7457cd386
commit 7fc2bd0d0f
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 22 additions and 2 deletions

View File

@ -701,7 +701,7 @@ def test_nat_zero_add_alt: TestM Unit := do
}
])
def test_composite_tactic_failure: TestM Unit := do
def test_tactic_failure_unresolved_goals : TestM Unit := do
let state? ← startProof (.expr "∀ (p : Nat → Prop), ∃ (x : Nat), p (0 + x + 0)")
let state0 ← match state? with
| .some state => pure state
@ -720,6 +720,25 @@ def test_composite_tactic_failure: TestM Unit := do
let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail"
checkEq s!"{tactic} fails" messages #[s!"{← getFileName}:0:12: error: unsolved goals\np : Nat → Prop\n⊢ p 0\n"]
def test_tactic_failure_synthesize_placeholder : TestM Unit := do
let state? ← startProof (.expr "∀ (p q r : Prop) (h : p → q), q ∧ r")
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let tactic := "intro p q r h"
let state1 ← match ← state0.tacticOn 0 tactic with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
let tactic := "simpa [h] using And.imp_left h _"
let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail"
checkEq s!"{tactic} fails" messages #[s!"{← getFileName}:0:12: error: unsolved goals\np : Nat → Prop\n⊢ p 0\n"]
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
let tests := [
("identity", test_identity),
@ -732,7 +751,8 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
("calc", test_calc),
("Nat.zero_add", test_nat_zero_add),
("Nat.zero_add alt", test_nat_zero_add_alt),
("composite tactic failure", test_composite_tactic_failure),
("tactic failure with unresolved goals", test_tactic_failure_unresolved_goals),
("tactic failure with synthesize placeholder", test_tactic_failure_synthesize_placeholder),
]
tests.map (fun (name, test) => (name, proofRunner env test))