Stream: Beginner Questions

Topic: Method to instantiate schematic variables in a goal

Qiyuan Xu (Apr 04 2023 at 09:44):

Hello dear friends,

I'm looking for some method or tactic (instead of some Isar statements) that can instantiate schematic variables in a goal. Is anyone ever heard that?

Thank you!

Manuel Eberl (Apr 04 2023 at 13:02):

I think the usual approach is to either instantiate them indirectly with e.g. resolution (rule etc.) or to make sure that you don't even get schematic variables in the first place. I don't know of a tactic.

Manuel Eberl (Apr 04 2023 at 13:03):

I did once make one for existentials. One could probably do something similar for schematic variables without too much effort…

Wolfgang Jeltsch (Apr 04 2023 at 15:30):

Depends on whether you want to instantiate the schematic variables with particular terms or with some freshly created variables. I don’t know proof methods for these things, but there are attributes: of and where for the former, no_vars for the latter.

Qiyuan Xu (Apr 05 2023 at 05:12):

Yeah, i made the method version of the of and where by myself, by copying and modifying the implementation in Eisbach. Actually I just modified the final declaration of the attributes and added the declaration of methods. The attributes originally apply on theorems and now as methods they apply on the state sequent of the proof. That is all, in only 10 lines of change. So I think, maybe it would be interesting to add the of and where method in Eisbach, adding 10 lines and giving good features?

Wolfgang Jeltsch (Apr 05 2023 at 10:25):

Not sure. I have to say that I never missed such methods. Maybe you’re using a heavily tactics-based style, while my style is focused on Isar. With Isar, you often have to write things more explicitly, but that’s a feature: it makes the proofs more intelligible for the human reader.

Last updated: Apr 27 2024 at 20:14 UTC