How To Locate Premise Definitions

[yangky11]

Some constants in Lean are defined by attributes such as @[to_addictive] (see Mathematics in Lean) or @[reassoc]. For example, hom_inv_id_assoc in mathlib is defined as a result of this line. Such definitions are difficult to locate because their names cannot be anticipated.

Therefore, you shouldn't rely on names to locate the definition of a premise. Instead, you should use its path and position. For example, below is how we locate premises in ReProver:

ReProver/common.py

Lines 253 to 262 in b89e258

	def locate_premise(self, path: str, pos: Pos) -> Optional[Premise]:
	"""Return a premise at position ``pos`` in file ``path``.
	Return None if no such premise can be found.
	"""
	for p in self.get_premises(path):
	assert p.path == path
	if p.start <= pos <= p.end:
	return p
	return None

Even with this technique, there is still a small percentage (~%1) of premises whose definitions cannot be located. That's why you may see Cannot locate premise ... in the log when training the retriever.

Related issues: #44