claude-bot
ca98703538
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FYqwNMyPUHeTbFWg83GQq6
95 lines
3.5 KiB
Python
95 lines
3.5 KiB
Python
from leanbench.project import classify, project
|
||
from leanbench.schema import KIND_FACT, KIND_GOAL, KIND_OBJECT, KIND_OWN
|
||
|
||
|
||
def roles(code):
|
||
return {r.name: r for r in project(code).roles}
|
||
|
||
|
||
def test_objects_instances_and_goal():
|
||
p = project(
|
||
"theorem t (G : Type*) [Group G] [Fintype G] (g : G) : g ^ Fintype.card G = 1 := by sorry"
|
||
)
|
||
got = {r.name: r for r in p.roles}
|
||
assert list(got) == ["G", "g", "goal"]
|
||
assert got["G"].kind == KIND_OBJECT
|
||
assert got["G"].attrs["instances"] == ["Group G", "Fintype G"]
|
||
assert got["goal"].kind == KIND_GOAL
|
||
assert not p.degenerate
|
||
assert p.simplex is not None and len(p.simplex.roles) == 3
|
||
|
||
|
||
def test_hypothesis_binders_become_facts():
|
||
got = roles("theorem t (n : ℕ) (a : ℤ) (h : Nat.Coprime a n) : a ≡ 1 [ZMOD n] := by sorry")
|
||
assert got["h"].kind == KIND_FACT
|
||
assert got["h"].attrs["classified_by"] == "predicate"
|
||
assert got["n"].kind == KIND_OBJECT
|
||
|
||
|
||
def test_relation_symbols_mark_a_fact():
|
||
got = roles("theorem t (a b : ℤ) (hab : a ∣ b) (hpos : 0 < a) : a ≤ b := by sorry")
|
||
assert got["hab"].kind == KIND_FACT and got["hpos"].kind == KIND_FACT
|
||
assert got["a"].kind == KIND_OBJECT
|
||
|
||
|
||
def test_function_type_is_data_not_a_fact():
|
||
kind, how = classify("ℕ → ℕ", ["f"], set())
|
||
assert kind == KIND_OBJECT and how == "default"
|
||
assert classify("Type*", ["G"], set()) == (KIND_OBJECT, "sort")
|
||
|
||
|
||
def test_leading_forall_is_lifted_so_both_spellings_agree():
|
||
a = project("theorem t (n : ℕ) : n = n := by rfl")
|
||
b = project("theorem t : ∀ n : ℕ, n = n := by rfl")
|
||
assert [(r.name, r.kind) for r in a.roles] == [(r.name, r.kind) for r in b.roles]
|
||
assert {r.attrs.get("origin") for r in b.roles if r.name == "n"} == {"forall_in_goal"}
|
||
|
||
|
||
def test_goal_implication_splits_into_premises():
|
||
got = roles("theorem t : ∀ n m : ℕ, n < m → m < 10 → n < 10 := by omega")
|
||
assert [n for n in got if n.startswith("premise")] == ["premise1", "premise2"]
|
||
assert got["goal"].type_text == "n < 10"
|
||
|
||
|
||
def test_bounded_forall_adds_an_object_and_a_fact():
|
||
got = roles("theorem t : ∀ x ∈ S, f x = 0 := by sorry")
|
||
assert got["x"].kind == KIND_OBJECT and got["h_x"].kind == KIND_FACT
|
||
|
||
|
||
def test_definition_has_an_own_role():
|
||
p = project("def divides (a b : Int) : Prop := ∃ k, b = a * k")
|
||
assert p.by_kind(KIND_OWN)[0].type_text == "Prop"
|
||
assert [r.name for r in p.roles] == ["a", "b", "own"]
|
||
|
||
|
||
def test_structure_stops_at_where_and_ignores_extends():
|
||
p = project("structure Ring (R : Type*) extends AddCommGroup R, Mul R where\n x : R")
|
||
assert [r.name for r in p.roles] == ["R", "own"]
|
||
|
||
|
||
def test_bare_statement_is_degenerate_not_an_error():
|
||
p = project("theorem t : 2 + 2 = 4 := by norm_num")
|
||
assert p.degenerate and p.simplex is None
|
||
assert [r.name for r in p.roles] == ["goal"]
|
||
|
||
|
||
def test_no_declaration():
|
||
p = project("-- just a comment")
|
||
assert p.degenerate and p.notes == ["no declaration found"]
|
||
|
||
|
||
def test_instance_without_target_is_noted():
|
||
p = project("theorem t (n : ℕ) [Fact (1 < 2)] : n = n := by rfl")
|
||
assert any("constrains no named object" in n for n in p.notes)
|
||
|
||
|
||
def test_duplicate_names_are_aliased():
|
||
p = project("theorem t (h : 0 < 1) (h : 1 < 2) : True := by trivial")
|
||
assert p.simplex is not None
|
||
assert "h" in p.simplex.roles and "h_2" in p.simplex.roles
|
||
|
||
|
||
def test_comments_and_proof_body_are_ignored():
|
||
code = "/- doc -/\ntheorem t (n : ℕ) : n = n := by\n -- (x : T) here is noise\n rfl"
|
||
assert [r.name for r in project(code).roles] == ["n", "goal"]
|