36 lines
1.8 KiB
Python
36 lines
1.8 KiB
Python
"""Synthetic example: one isomorphism schema relates two groups and a map."""
|
|
from __future__ import annotations
|
|
|
|
import json
|
|
|
|
from leanbench.schema import KIND_FACT, KIND_GOAL, Role, Simplex, SimplexInstance
|
|
from leanbench.schema_registry import SchemaRegistry, slot_key
|
|
|
|
|
|
def example():
|
|
group = Role("group", type_text="group carrier", context="Reusable group role definition")
|
|
schema = Simplex("group_isomorphism", {
|
|
"left": group,
|
|
"right": group,
|
|
"map": Role("homomorphism", type_text="left →* right",
|
|
attrs={"references": ["left", "right"]}),
|
|
"bijective": Role("bijective", KIND_FACT, type_text="Bijective map",
|
|
attrs={"references": ["map"]}),
|
|
"goal": Role("isomorphic", KIND_GOAL, type_text="Nonempty (left ≃* right)",
|
|
attrs={"references": ["left", "right"]}),
|
|
}, context="A bijective homomorphism supplies a group isomorphism")
|
|
with SchemaRegistry() as registry:
|
|
registry.set_role(group, "role:group")
|
|
key = registry.set_simplex(schema, role_keys={"left": "role:group", "right": "role:group"})
|
|
instance = SimplexInstance(schema, facts={
|
|
"left": "group A", "right": "group B", "map": "f", "bijective": "supplied evidence"})
|
|
candidates = registry.find_solvable([slot_key(key, alias) for alias in instance.facts])
|
|
return {"schema": registry.get_simplex(key).as_dict(), "definition_keys": registry.slots(key),
|
|
"bindings": {alias: fact.value for alias, fact in instance.facts.items()},
|
|
"structural_candidates": candidates, "completed": instance.is_completed(),
|
|
"note": "Evidence is symbolic user input; this example does not run a Lean proof."}
|
|
|
|
|
|
if __name__ == "__main__":
|
|
print(json.dumps(example(), indent=2, ensure_ascii=False))
|