What is the current best way to do
I sometimes do
#[program] Definition instead, but I would like not to have to override the obligation tactic globally to do that.
Also Program will modify pattern matching to keep info about equalities, and I don't want that.
just normal proof mode
Program changing equalities, you might want to use
Unset Program Cases. (doc), no ? I have also used Equations for that purposes sometimes (in particular
Equations? to land into a standard proof mode instead of the
Anyway, a simple bare metal
#[refine] Definition would be much appreciated.
Normal proof mode wouldn't work in all cases, if the type also has holes typically. But yeah, since it's for a library, I'd rather not change global options, so local changes would be nicer.
I was also wondering how
Equations? fared for this, but it will also call the obligation tactic automatically to "simplify" the goals right?
same as Program yes, but you can also locally set the program obligation tactic to what you need
How can you do it locally?
I just meant saving the obligation tactic, setting it to what you want and reset the change at the end of your definition/section/file. Would be great to be able to do it automatically in a well-scoped fashion though...
Changes to the Obligation tactic are local to sections, no?
At least when I do
Obligation Tactic := idtac. Section test. Obligation Tactic := exact 5. #[program] Definition five : nat := _. End test. #[program] Definition six : nat := _. Next Obligation. exact 6. Defined.
actually I am not sure how you could save the current obligation...
You don't have to save it I think, you can simply open a section, redefine the tactic, do what you want, close the section and the tactic is back to what it was before opening the section
At least that's what I infer from the above ad hoc example
Right that's an option then, albeit unsatisfactory.
It'd be easy to deactivate the call to equations_simpl_tactic or whatever
That would be cool.
You can also do
Local Obligation Tactic := idtac at the top of each of your files, I think
Ok, I was a bit wary of those because importing a module with a submodule changing the obligation tactic seemed to change it even if the submodule was not itself imported.
But anyway, I see that the new release of Equations introduces what I want, thanks. :smile:
Last updated: Oct 01 2023 at 19:01 UTC