Extract mathlib proofs

Stream: new members

[Auguste Poiroux]

Hello!

Is there a tool to extract the whole structure of a Lean file? The goal is to extract all the tactics from each proof (for proof in tactic mode) and to transform a term proof into a tactic proof.
Also t o transform a term proof into a tactic proof, I have found that adding "begin exact(" - ") end" around the term proofs works quite well. However, there are cases where it does not work (mathlib/src/data/analysis/topology.lean is an example where it doesn't work). Is there a general way to do this?

Thank you in advance!

Auguste

[Kenny Lau]

bad link

[Kenny Lau]

why would you want to convert term mode to tactic mode?

[Auguste Poiroux]

I'm trying to get the combination of proof state + applied tactic. Tactic proof mode gives the proof state. Term mode proofs do not allow to obtain this state (I did not find how anyway), so I try to transform them into tactic mode.
About the link, this is not a link to the original file, but a link to a modified version of this file where all the term mode proofs have been transformed into tactic mode proofs (and there are two errors).

[Kevin Buzzard]

You can inspect a term mode proof in VS Code with a recent version of lean -- move your cursor through the proof and you should be able to see output

[Auguste Poiroux]

Thank you! However, since I'm doing the extraction from a program, how do I know where to place my cursor to get the same output as if it was the first state of the proof in tactic mode? Can I always get this state in a term mode proof?
For example, in the next proof, I have to place my cursor just before the ̀$`:

theorem ext [T : topological_space α] {σ : Type*} {F : ctop α σ}
  (H₁ : ∀ a, is_open (F a))
  (H₂ : ∀ a s, s ∈ 𝓝 a → ∃ b, a ∈ F b ∧ F b ⊆ s) :
  F.to_topsp = T :=
ext' $ λ a s, ⟨H₂ a s, λ ⟨b, h₁, h₂⟩, mem_nhds_sets_iff.2 ⟨_, h₂, H₁ _, h₁⟩⟩

And in this proof, I have to put it just before .trans:

theorem tendsto_nhds_iff {m : β → α} {f : filter β} (F : f.realizer) (R : realizer α) {a : α} :
  tendsto m f (𝓝 a) ↔ ∀ t, a ∈ R.F t → ∃ s, ∀ x ∈ F.F s, m x ∈ R.F t :=
(F.tendsto_iff _ (R.nhds a)).trans subtype.forall

[Auguste Poiroux]

Since there are variables that are declared before, I cannot get this state directly from the declaration of the theorem in a term mode proof. The tactic mode facilitates this since Lean takes care of it. But if there is a Lean file parser, it wouldn't be too hard to do I guess.

[Chris B]

You might be able to get more exact/machine-oriented info from the olean files? There's a parser https://github.com/digama0/olean-rs but it might be out of date.

[Auguste Poiroux]

Thank you! I'll look into it.

[Kenny Lau]

there's also the #explode command, and you still haven't fixed your bad link

[Auguste Poiroux]

Thank you for the command! I can't find it in the Lean reference manual, but if I understand it correctly, it returns the basic steps of a proof, right?
About the link, I don't understand what's wrong. It's a link to an uploaded file (which is a modified version of the original file), and I can re-download it. What's wrong with it?

[Chris B]

I think it's been said that olean files are version dependent and that repo hasn't been updated in a while, so I just meant it might not parse new olean files correctly.
There's some info on explode in the mathlib docs : https://leanprover-community.github.io/mathlib_docs/commands.html##explode

[Auguste Poiroux]

Thanks for the link to the doc!
About the olean parser, I am trying to use the Lean version. But I still have the same "failed to open file" error. I tried absolute and relative paths but nothing works. Do you know if there is a particular way to use it? Or is it also the error that the program returns when there is a problem during parsing?

[Chris B]

It looks like the header (and probably other stuff) has changed for the olean format since the last updates on that parser. I was able to get it to work by setting the leanpkg.toml to use an older version lean_version = "leanprover-community/lean:3.5.0", then building the project with leanpkg build.
The format to get the parser working was olean-rs/target/debug/olean-rs -D /home/user/my_lean_project/src/main.olean > output.txt

[Auguste Poiroux]

Thank you very much! I'm going to try that.

[Chris B]

However, there are cases where it does not work (mathlib/src/data/analysis/topology.lean is an example where it doesn't work). Is there a general way to do this?

If you end up going back to this, you should print them with set_option pp.all true to get the best odds. You'll still need to bring the universes into scope manually I think, and even with pp.all there are instances where the pretty printer won't round-trip.

[Mario Carneiro]

I will look into adding a --lean-version flag to olean-rs to support newer versions of lean