RFC: Introduce the guard/unguard attributes for Fixpoint

[lthms]

I occasionally run into situation where I am okay with relying on the Unset Guard Checking recent feature of Coq (for utility functions, mostly), but I found the current way of using it cumbersome.

This patch adds new attributes to more easily control the feature.

It is a work in progress, in particular I believe the code can be refactor to be made more idiomatic wrt. the rest of the code base.

Overall, this is a RFC. Do you think we can move forward, from this draft to a complete PR?

And, finally, the obligatory snippet to demonstrate the feature.

(* Success *)
#[unguard]
Fixpoint tada (x : nat) : nat := tada (S x).

(* Fail *)
Unset Guard Checking.
#[guard]
Fixpoint tada (x : nat) : nat := tada (S x).
Set Guard Checking.

[Zimmi48]

I'm in favor of this PR (and generally in favor of adding attributes every time it is convenient to locally enable an option). Of course, the usual nitpicking regarding the name of the attribute applies. I'd personally prefer if there was a generic way of specifying boolean attributes such as guard(on) / guard(off) or guard(enable) / guard(disable) rather than having to invent two names each time.

[Zimmi48]

On a technical note, there is no reason why the attribute should be defined in a central place. Please put the definition in the file where you use it.

[lthms]

Thanks for your feedback, @Zimmi48.

I'd personally prefer if there was a generic way of specifying boolean attributes such as guard(on) / guard(off) or guard(enable) / guard(disable) rather than having to invent two names each time.

Your comment suggests this approach does not yet exist, at least not in the form you’d like it to exist. Do you think this PR is a good occasion to introduce it? Another possibility is for me to implement your naming proposition, but in a more ad-hoc way.

Please put the definition in the file where you use it.

Will do. Thanks!

[Zimmi48]

Your comment suggests this approach does not yet exist, at least not in the form you’d like it to exist. Do you think this PR is a good occasion to introduce it?

Yes, that would make sense. One possible API would be for bool_attribute to have this behavior when ~on and ~off are not provided.

[lthms]

I was wondering: maybe set/unset (e.g., guard(set) etc.) is a good approach, since it mimics the Set/Unset commands.

What do you think?

[Zimmi48]

Sure, that sounds reasonable. But if we want to mimic the flags as much as possible, it could be guard_checking(set) / guard_checking(unset).

[lthms]

You’re right. My focus was the set/unset as a general approach to deal with missing ~on: and ~off: parameter, but indeed for the particular case of guard checking, we can have more verbose (but explicit) guard_checking.

Will try to implement this this afternoon. Do you think it can find its way to a 8.12 beta, or it will be postponed to 8.13? (it would make a lot of sense if so)

[Zimmi48]

This is definitely 8.13 material. (The beta has already been tagged BTW.)

[Zimmi48]

for the particular case of guard checking, we can have more verbose (but explicit) guard_checking

Even for the general case, we could consider having a function that declares at the same time, a flag and the corresponding attribute, following standard conventions regarding casing and the replacement of spaces by underscores.

[Zimmi48]

Another remark is that your current implementation that sets the flag locally through side-effects is too naive as witnessed by this failing example:

#[ unguard ] Fixpoint tada (x : nat) : nat.
exact (tada (S x)).
Defined.
(*
Error:
Recursive definition of tada is ill-formed.
In environment
tada : nat -> nat
x : nat
Recursive call to tada has principal argument equal to 
"S x" instead of a subterm of "x".
Recursive definition is: "fun x : nat => tada (S x)".
*)

Instead, you should probably have the attribute passed to the functions constructing the fixpoints, and end up with setting the right typing flags in the environment. But as witnessed by the initial attempt of @SimonBoulier in #9004, it is far from trivial.

[ejgallego]

it is far from trivial.

I think it is not very hard, we have the infrastructure for it in Declare now, and will be make uniform among interactive / non-interactive forms in #12372 ; ping me if you need help with this.

[lthms]

Should I wait until #12372 is merged, then?

[ejgallego]

Should I wait until #12372 is merged, then?

I think it is not necessary, tho we may get some small conflicts, but the main strategy can be carried out. So it seems that vernac_fixpoint should itself take the parameter into account, up to declare_fixpoint_interactive_generic, which should then update start_with_initialization [here you would find a small conflict, but nothing to worry about.

More generally [@Zimmi48 you did follow the discussion more closely] , what kind of parameters should start_with_initialization take?

[ejgallego]

More generally [@Zimmi48 you did follow the discussion more closely] , what kind of parameters should start_with_initialization take?

In fact all the ones in #9004 can be added, but indeed it would be more easy to base this PR on top of #12372 , adding a typing_flags field to CInfo.t ; I need to do a bit more work on that PR as the information structure there is not yet canonical [in the sense that for example opaque cannot be part of CInfo.t as for interactive proofs is a qed-set attribute.

[lthms]

Since this change would be part of 8.13 rather than 8.12, I think I will subscribe to #12372, wait until it is merged, then start working on this again. Thanks for the feedback, @Zimmi48 and @ejgallego.

[ejgallego]

Sounds good @lthms , if you wait for that PR most of the changes that will be needed will be in the parsing front, I'm going to add a typing_flags field to the record.

[lthms]

It looks like the awaited PR has been merged. (: Congrats @ejgallego!

I will take the time to study it and understand how to use the API it introduces/refactors. Do you have any good example of how to do that in mind that I could read?

[ejgallego]

Hi @lthms :) , I suggest you have a look to #12586 , which you should also depend on.

Basically you want to update the calls to Info.make with the proper flags, for example in Vernacentries.interp_lemma

[ejgallego]

Superseded by #12586