test: Tests for conv and calc

This commit is contained in:
Leni Aniva 2024-04-06 17:22:09 -07:00
parent 951c2cec19
commit 3db1207aa6
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 72 additions and 5 deletions

View File

@ -292,16 +292,14 @@ def test_or_comm: TestM Unit := do
{ userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible? := .some true } { userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible? := .some true }
] ]
} }
def test_have_tactic: TestM Unit := do
def test_have: TestM Unit := do
let state? ← startProof (.expr "∀ (p q: Prop), p → ((p q) (p q))") let state? ← startProof (.expr "∀ (p q: Prop), p → ((p q) (p q))")
let state0 ← match state? with let state0 ← match state? with
| .some state => pure state | .some state => pure state
| .none => do | .none => do
addTest $ assertUnreachable "Goal could not parse" addTest $ assertUnreachable "Goal could not parse"
return () return ()
addTest $ LSpec.check "(0 parent)" state0.parentExpr?.isNone
addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intro p q h") with let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intro p q h") with
| .success state => pure state | .success state => pure state
| other => do | other => do
@ -326,6 +324,71 @@ def test_have_tactic: TestM Unit := do
addTest $ LSpec.check "have" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = addTest $ LSpec.check "have" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
#[buildGoal [] ""]) #[buildGoal [] ""])
example : ∀ (a b c: Nat), (a + b) + c = (b + a) + c := by
intro a b c
conv =>
lhs
congr
rw [Nat.add_comm]
rfl
def test_conv: TestM Unit := do
let state? ← startProof (.expr "∀ (a b c: Nat), (a + b) + c = (b + a) + c")
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let tactic := "intro a b c"
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 [("a", "Nat"), ("b", "Nat"), ("c", "Nat")] "a + b + c = b + a + c"])
-- This solves the state in one-shot
let tactic := "conv => { lhs; congr; rw [Nat.add_comm]; rfl }"
let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
#[])
example : ∀ (a: Nat), 1 + a + 1 = a + 2 := by
intro a
calc 1 + a + 1 = a + 1 + 1 := by conv =>
rhs
rw [Nat.add_comm]
_ = a + 2 := by rw [Nat.add_assoc]
def test_calc: TestM Unit := do
let state? ← startProof (.expr "∀ (a: Nat), 1 + a + 1 = a + 2")
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let tactic := "intro a"
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 [("a", "Nat")] "1 + a + 1 = a + 2"])
let tactic := "calc"
let state2 ← match ← state1.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 [("a", "Nat")] "1 + a + 1 = a + 2"])
def suite (env: Environment): List (String × IO LSpec.TestSeq) := def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
let tests := [ let tests := [
("Nat.add_comm", test_nat_add_comm false), ("Nat.add_comm", test_nat_add_comm false),
@ -333,8 +396,12 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
("Nat.add_comm delta", test_delta_variable), ("Nat.add_comm delta", test_delta_variable),
("arithmetic", test_arith), ("arithmetic", test_arith),
("Or.comm", test_or_comm), ("Or.comm", test_or_comm),
("Have", test_have_tactic), ("have", test_have),
("conv", test_conv),
("calc", test_calc),
] ]
tests.map (fun (name, test) => (name, proofRunner env test)) tests.map (fun (name, test) => (name, proofRunner env test))
end Pantograph.Test.Proofs end Pantograph.Test.Proofs