Why are the premises from the same file not listed as such?

[josojo]

Hey

I was wondering why the premises that are in the same file as a parsed theorem not listed as premises? Is there intention behind it? I think this could improve the training data quite a bit.

Yes, during the testing of the reprover with a unseen mathlib4 file, one would have to add the new theorems to the retriever on the fly, but this should not be a real challenge, right?

Eg.

tactic.get_annotated_tactic()

returns

("· rintro ⟨y, h₁, h₂⟩\n    rw [<a>SetLike.le_def</a>]\n    intro z hz\n    simp only [mem_ker, <a>SetLike.mem_coe</a>] at hz\n    rw [← <a>SetLike.mem_coe</a>, range_coe, <a>Set.mem_range</a>] at h₁\n    obtain ⟨x, hx⟩ := h₁\n    have hx' : x ∈ p := h₂ hx\n    have hxz : z + x ∈ p := by\n      apply h₂\n      simp [hx, hz]\n    suffices z + x - x ∈ p by simpa only [this, <a>add_sub_cancel</a>]\n    exact p.sub_mem hxz hx'",
 [{'full_name': 'SetLike.le_def',
   'def_path': 'Mathlib/Data/SetLike/Basic.lean',
   'def_pos': [191, 9],
   'def_end_pos': [191, 15]},
  {'full_name': 'SetLike.mem_coe',
   'def_path': 'Mathlib/Data/SetLike/Basic.lean',
   'def_pos': [163, 9],
   'def_end_pos': [163, 16]},
  {'full_name': 'SetLike.mem_coe',
   'def_path': 'Mathlib/Data/SetLike/Basic.lean',
   'def_pos': [163, 9],
   'def_end_pos': [163, 16]},
  {'full_name': 'Set.mem_range',
   'def_path': 'Mathlib/Data/Set/Image.lean',
   'def_pos': [673, 9],
   'def_end_pos': [673, 18]},
  {'full_name': 'add_sub_cancel',
   'def_path': 'Mathlib/Algebra/Group/Basic.lean',
   'def_pos': [739, 30],
   'def_end_pos': [739, 44]}])

and mem_ker is not annoated, nor defined as a premise, but it is defined in the file mathlib4/Mathlib/LinearAlgebra/Basic.lean, the same that was traced in the example above.
( I ran that code from the demo.ipynb)

[yangky11]

Looks like a bug. I'll investigate more and let you know.

[yangky11]

It is indeed a bug in ExtractData.lean. I have fixed it and will update the main branch after running unit tests. I'll also update the pre-extracted datasets on Zenodo. @josojo Thanks a lot for catching it!

[josojo]

nIce! thanks for fixing it so quickly.