Stream: Coq users

Topic: Simulate #[refine] Definition

Théo Winterhalter (Apr 26 2021 at 09:32):

What is the current best way to do #[refine] Definition?
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.

Thanks.

Gaëtan Gilbert (Apr 26 2021 at 09:49):

just normal proof mode

Kenji Maillard (Apr 26 2021 at 10:05):

About 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 Obligations mechanism).
Anyway, a simple bare metal #[refine] Definition would be much appreciated.

Théo Winterhalter (Apr 26 2021 at 10:18):

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?

Kenji Maillard (Apr 26 2021 at 10:38):

same as Program yes, but you can also locally set the program obligation tactic to what you need

Théo Winterhalter (Apr 26 2021 at 10:53):

How can you do it locally?

Kenji Maillard (Apr 26 2021 at 10:57):

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...

Yannick Forster (Apr 26 2021 at 10:59):

Changes to the Obligation tactic are local to sections, no?

Yannick Forster (Apr 26 2021 at 11:00):

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.

Kenji Maillard (Apr 26 2021 at 11:00):

actually I am not sure how you could save the current obligation...

Yannick Forster (Apr 26 2021 at 11:01):

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

Yannick Forster (Apr 26 2021 at 11:01):

At least that's what I infer from the above ad hoc example

Théo Winterhalter (Apr 26 2021 at 11:38):

Right that's an option then, albeit unsatisfactory.

Théo Winterhalter (Apr 26 2021 at 11:39):

Thanks.

Matthieu Sozeau (Apr 26 2021 at 22:41):

It'd be easy to deactivate the call to equations_simpl_tactic or whatever

Théo Winterhalter (Apr 27 2021 at 06:12):

So like Equations(notac)?

Théo Winterhalter (Apr 27 2021 at 06:12):

That would be cool.

Jason Gross (May 07 2021 at 14:20):

You can also do Local Obligation Tactic := idtac at the top of each of your files, I think

Théo Winterhalter (May 07 2021 at 14:22):

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: Apr 19 2024 at 15:02 UTC