Skip to content

Conversation

sorgfresser
Copy link
Contributor

@sorgfresser sorgfresser commented May 7, 2025

Added a new command that retrieves the corresponding type for a definition.

Given that the approach of separate lemmas is becoming more popular, this might be interesting to have.
Consider the following:

lemma A := by <proof-of-a>

lemma B := by <proof-of-b>

theorem C := by
  have A := by <proof-of-a>

  have B := by <proof-of-b>

  <regular-proof>

which is the current approach, for example used in DeepSeekProver v2.
This is inherently redundant. Importantly, the proof of A, B is not necessary in C.

Instead, one can now write

theorem C (hx: type of A) (hy: type of B) := by <regular-proof>

and compose via

exact C A B

@sorgfresser sorgfresser changed the title Theorem type Command to get theorem type May 7, 2025
@augustepoiroux
Copy link
Contributor

augustepoiroux commented May 7, 2025

This is an interesting feature in my opinion. REPL has extraction capabilities centered around tactics, and I believe that adding some for declarations could be nice. #96 is related to this in that sense.
Regarding this PR, maybe it could be integrated directly into Command (i.e. "cmd" in JSON) as a parameter instead of having to do a separate query (similar to the allTactics parameter). What do you think?

@sorgfresser sorgfresser marked this pull request as draft May 23, 2025 12:39
@sorgfresser
Copy link
Contributor Author

@augustepoiroux thanks for the feedback! I moved this to a flag declTypes now. Let me know if that's a better interface :)

@sorgfresser sorgfresser marked this pull request as ready for review May 24, 2025 11:15
@sorgfresser sorgfresser marked this pull request as draft July 1, 2025 12:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants