Stream: Coq users

Topic: Simulate #[refine] Definition


view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Apr 26 2021 at 09:49):

just normal proof mode

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Théo Winterhalter (Apr 26 2021 at 10:53):

How can you do it locally?

view this post on Zulip 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...

view this post on Zulip Yannick Forster (Apr 26 2021 at 10:59):

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

view this post on Zulip 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.

view this post on Zulip Kenji Maillard (Apr 26 2021 at 11:00):

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

view this post on Zulip 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

view this post on Zulip Yannick Forster (Apr 26 2021 at 11:01):

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

view this post on Zulip Théo Winterhalter (Apr 26 2021 at 11:38):

Right that's an option then, albeit unsatisfactory.

view this post on Zulip Théo Winterhalter (Apr 26 2021 at 11:39):

Thanks.

view this post on Zulip Matthieu Sozeau (Apr 26 2021 at 22:41):

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

view this post on Zulip Théo Winterhalter (Apr 27 2021 at 06:12):

So like Equations(notac)?

view this post on Zulip Théo Winterhalter (Apr 27 2021 at 06:12):

That would be cool.

view this post on Zulip 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

view this post on Zulip 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: Feb 06 2023 at 13:03 UTC