[Work and discussion in progress] Add `Unguarded` syntax for (co)fixpoints and `Assumed Positive` for (co)inductive types. by SimonBoulier · Pull Request #7651 · rocq-prover/rocq

SimonBoulier · 2018-05-31T12:33:46Z

Disable guard check for (co)fixpoints when defined with Ungarded keyword.
We can now write:

Unguarded Fixpoint f (n : nat) : False
  := f n.

Unguarded Fixpoint ackermann (m n : nat) {struct m} : nat.
  destruct m. exact (S n).
  destruct n. exact (ackermann m 1).
  exact (ackermann m (ackermann (S m) n)).
Defined.

Compute (ackermann 3 4).

Print Assumptions ackermann.
(* ackermann is assumed to be guarded *)

Unguarded CoFixpoint fer (s : Stream nat) : Stream nat.
Proof.
  exact (fer s).
Defined.

Kind: feature.

Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
Entry added in CHANGES.

I know that this PR is far from being perfect, any comment welcome.

ejgallego · 2018-05-31T13:22:33Z


-let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
+(* guarded: Some b -> set check_guarded to b, None -> does not change it *)
+let declare_fixpoint guarded local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =


As you are breaking the API here maybe we'd like to upgrade to named parameters?

I named guarded, but do you suggest I also name the other arguments?

Maybe that would be a good idea, what do other devs think?

Zimmi48

Since we can also do fixed points using Theorem, Lemma, etc, would it make sense to also add this new syntax for these commands?

Zimmi48 · 2018-05-31T13:56:05Z

  By default, they are disabled and produce an error. The deprecation
  warning which used to occur when using nested proofs has been removed.
+- Guard check can be temporary disabled to define non terminating fixpoints
+  or non productive cofixpoints with the commands `Unguarded Fixpoints`


typo: spurious s

Zimmi48 · 2018-05-31T13:56:45Z

   ind_body           : `ident` [`binders`] : `term` :=
                      : [[|] `ident` [`binders`] [:`term`] | … | `ident` [`binders`] [:`term`]]
-   fixpoint           : Fixpoint `fix_body` with … with `fix_body` .
+   fixpoint           : [Unguarded] Fixpoint `fix_body` with … with `fix_body` .


You should also add this on the CoFixpoint line below.

Zimmi48 · 2018-05-31T13:57:45Z

   end.

-The ``{struct`` :token:`ident```}`` annotation may be left implicit, in this case the
+The ``{struct`` :token:`ident` ``}`` annotation may be left implicit, in this case the


Note that this is already fixed in #7537 and the best fix goes further than this.

Zimmi48 · 2018-05-31T14:00:08Z

 starts with a constructor.

+The check of decreasing argument can be temporary disabled using ``Unguarded``.
+Warning: this can break the consistency of the system, use at your own risk.


This documentation is not done in the recommended style, the documentation must come after the variant grammar and must be indented. Since this chapter is heavily reindented by #7537 anyways, I suggest you rebase on top or wait for it to get merged. In any case, you will have so many conflicts in this file that the best way to solve them will be to copy / paste this part.

Ok thanks, I will do this after merge then.

Zimmi48 · 2018-06-01T08:21:19Z

Since we can also do fixed points using Theorem, Lemma, etc, would it make sense to also add this new syntax for these commands?

I withdraw this because I'm actually doubtful that doing fixed points using Theorem is a good idea anyways.

ppedrot · 2018-06-01T09:10:57Z

Please. Stop. Inflating. The. Definition. Modifier. Syntax. Again.

There have been a shitload of arguments against definition modifiers, and it all boils down that it doesn't scale. I am too tired to repeat them here and I think there are pointers in #79. I am fundamentally against this PR.

ppedrot

To expand on my above comment, I am even surprised that people that were (I think) at the heated Coq workgroup where we discussed the issue comment on that PR as if it was OK in principle, and that they did not try to deter @SimonBoulier from implementing it at the CIW... Is that the famous "History repeats twice, first as a tragedy, second as a farce" effect?

maximedenes · 2018-06-01T09:23:38Z

To expand on my above comment, I am even surprised that people that were (I think) at the heated Coq workgroup where we discussed the issue comment on that PR as if it was OK in principle, and that they did not try to deter @SimonBoulier from implementing it at the CIW... Is that the famous "History repeats twice, first as a tragedy, second as a farce" effect?

I don't remember hearing this project in the presentations of the first day, but I may have missed something.

maximedenes · 2018-06-01T09:25:09Z

Also, I guess what @ppedrot means is that he would like to see this implemented only once we have the attributes syntax.

Zimmi48 · 2018-06-01T09:32:25Z

@SimonBoulier The documentation PR has been merged so you might want to rebase now.

@ppedrot I completely disagree with your argument to reject this change. This argument has been stupidly used to delay #79 for three years now. The problem you are pointing at is a well known syntax problem and must be addressed independently without preventing people to work on new features in the meantime. Attributes are now on their way thanks to @vbgl and will probably be finished for 8.9 so it means that the current syntax will probably never make it into a released version as-is. But even if it wasn't the case, that wouldn't be a good reason to delay the availability of this feature.

ejgallego · 2018-06-01T09:55:35Z

I like this feature and its current syntax. We are taking attributes as a kind of "silver bullet" , but the more I think about them the less convinced I am they are going to bring significant benefits.

Attributes are hard to handle, and worse, they tend to override all kind of static checks due to their "generic" nature. So IMVHO we shouldn't delay this PR just for that.

maximedenes · 2018-06-01T09:57:18Z

So IMVHO we shouldn't delay this PR just for that.

I tend to agree with that part.

ppedrot · 2018-06-01T09:59:53Z

The problem you are pointing at is a well known syntax problem and must be addressed independently without preventing people to work on new features in the meantime.

Wrong. Syntax is non-local by nature, so this can affect people that are unrelated to this change. Plus in the current implementation it is a hell to get it right. There is no way to compute the syntax conflict because CAMLP5, but we would be surprised if this were possible. This is the kind of area where conservativity should be of utmost importance, because it will be hard to backtrack on that.

But like, I don't understand why it is taking THREE YEARS. Like I can implement a syntax that scales properly in literally half a day. Should I do that or what?

ppedrot · 2018-06-01T10:00:49Z

And also,

But even if it wasn't the case, that wouldn't be a good reason to delay the availability of this feature.

We've already discussed that, and the answer is: write a goddamn plugin.

Zimmi48 · 2018-06-01T10:05:51Z

But like, I don't understand why it is taking THREE YEARS. Like I can implement a syntax that scales properly in literally half a day. Should I do that or what?

Seriously? And you didn't do it?
Anyways, now your help on this is not needed anymore since it is well underway thanks to @vbgl.

ppedrot · 2018-06-01T10:13:56Z

Seriously? And you didn't do it?

This ended up in the sinkhole of workgroups and PR bikeshedding, as all syntactic considerations do. But yes, luckily @vbgl has started doing it with a wide approval, although I am still curious to see the moment where we start discussing on the actual syntax.

Disable guard check for (co)fixpoints when defined with `Ungarded` keyword.

…ptions.

[no ci]

ejgallego · 2018-06-01T09:58:58Z

  loc : Loc.t option;
  locality : bool option;
+  check_guard : bool option; (* None -> use global setting (true by default); Some -> override *)
  polymorphic : bool;


Why is guarded a global attribute? AFAICS it only applies to fixpoints, am I correct?

All attributes are global.

I mean this should not be an attribute, but an entry in the corresponding vernac_expr constructor.

ejgallego · 2018-06-01T10:00:46Z

  | VernacProgram
  | VernacPolymorphic of bool
  | VernacLocal of bool
+  | VernacGuarded of bool


There is an assymetry between the syntax and the interpreted here, which IMO signals that indeed the proper fixpoint AST should be extended.

ejgallego · 2018-06-01T11:48:14Z

IMO "Write a plugin" is hardly an answer to most problems, but rather a good way to add some maintenance burden and testing overhead. This seems to me like a well-delimited functionality that applies to two core vernaculars.

ejgallego

I am convinced now that this property is local to the vernaculars and thus doesn't belong in an attribute.

Zimmi48 · 2018-06-01T13:07:06Z

It seems Emilio that you have a diverging opinion of what should be an attribute than what was in the CEP and what is being implemented. IMO the great benefit of attributes is that they make the parsing phase more tractable by moving some of the complexity / error handling from the parsing file to the interpretation phase.

gares · 2018-06-01T20:16:03Z

Simon explained that this new feature doesn't go as far as he would have liked because the check disabling only occurs at definition time. So if the fixpoint ended up in a proof it would have to be typechecked again and this would fail.

Right! Much better this way ;-)

SimonBoulier · 2018-06-02T13:23:44Z

I don't have time to address your comments right now and I only pushed what I did in the train.
I understand this PR will need discussions before being merged.

ejgallego · 2018-06-02T16:16:47Z

@SimonBoulier personally I'd say that if you remove the VernacGuarded "attribute" and instead put this info in the Definition constructor itself that should be merged without too much problems.

Indeed it seems to me that quite a few design work on what "attributes" are and how are they gonna be implemented is needed, but IMHO that should be orthogonal to this PR.

Zimmi48 · 2018-06-02T22:15:17Z

Except that this is precisely what @ppedrot opposed to, isn't it?

ejgallego · 2018-06-02T22:29:56Z

The way I understand it is that @ppedrot complains about the syntax, I am referring to the AST itself.

At least to me it is clear that the AST needs a bit more of design work so I think that what I suggest is a reasonable compromise in order not to get this PR stuck.

About the syntax, I have no particular strong opinion.

ppedrot · 2018-06-03T10:06:09Z

To be clear, I'm just opposed to the syntax extension. How hackish the implementation is can be frowned upon from an engineering point of view, but this is one order of magnitude less problematic as it does not appear directly to the user.

Quizz: without looking at the code, which permutation(s) makes the syntax parsable in the current PR?

{Unguarded, Local, Polymorphic, Program} Fixpoint f (n : nat) := tt.

mattam82 · 2018-06-05T07:19:32Z

I think Unguarded/General fxpoint could have even a larger scope than Program, and apply to Lemma, Inductive as well, ie any command where an unguarded fixpoint might be typechecked. In the current codebase there’s no parsing support for attributes so I didn’t see a problem with the implementation. When they’re available we’ll use them. I suppose there will be a mechanism to check the support of an attribute by a given command, @vbgl @maximedenes ?

maximedenes · 2018-06-05T07:21:52Z

I suppose there will be a mechanism to check the support of an attribute by a given command, @vbgl @maximedenes ?

Yes, I believe that is the plan. @vbgl is very busy on other topics these days, but once he finds some time for Coq, I'm sure good progress will be made, and in particular the plans for attributes will be made clear.

Zimmi48 · 2018-06-05T13:48:58Z

I think Unguarded/General fxpoint could have even a larger scope than Program, and apply to Lemma, Inductive as well, ie any command where an unguarded fixpoint might be typechecked.

For Inductive, do you mean you mean that Unguarded should give access to the feature that was implemented in #79? In that case, I wonder if Unguarded is the right generic terminology.

For Lemma, Theorem, etc, yes, this is what I suggested in #7651 (review). However, I withdrew this in #7651 (comment) because I'm doubtful about the interest of using Theorem to define a (co-)fixpoint. I wonder if we shouldn't deprecate this feature instead. WDYT?

SkySkimmer · 2018-06-05T14:46:44Z

For Inductive, do you mean you mean that Unguarded should give access to the feature that was implemented in #79? In that case, I wonder if Unguarded is the right generic terminology.

No, it's that you could write Unguarded Inductive foo := bar : (fix f (x:unit) : empty := f x) -> foo.

nomeata · 2018-06-22T13:51:43Z

This might be very useful to me! But I often work with Definition and local fix, and from the description it is unclear to me whether there is a way to mark a local fix as Unguarded. Will that be supported?

Zimmi48 · 2018-06-22T14:03:53Z

It was discussed and this PR doesn't go as far because it doesn't change the AST of terms (we can't attach Unguarded to a term). However, I guess the options proposed in https://github.com/SimonBoulier/TypingFlags should do what you want. BTW @SimonBoulier what about first proposing to integrate these options to Coq. This was the approach recently followed by @jashug in #7703 to avoid the debates around attributes.

SimonBoulier · 2018-06-23T09:50:03Z

what about first proposing to integrate these options to Coq

That's my plan! I do this as soon as my thesis is written :-)

herbelin

OK to me as far as I'm concerned.

gares

wrt the classifier

maximedenes

This can now use attributes.

maximedenes · 2018-09-12T15:18:27Z

It seems to me that this PR could be rebased on top of attributes, now that we have them.

Zimmi48 · 2018-09-12T15:37:04Z

I think this is simply waiting on @SimonBoulier finishing writing their thesis first.

SimonBoulier · 2018-09-14T17:08:11Z

Sorry I am not very available those days but I will do it.
What is the deadline for the 8.9? October, the 1st?

Zimmi48 · 2018-09-17T16:55:42Z

October 1st is the date of the beta release so it will be too late for sure, but it is already quite late. If it is merged now, it goes in 8.10 by default unless developers convince the release manager how important it is to include this in 8.9.

SimonBoulier · 2018-09-18T19:26:41Z

Ok, it will be for 8.10 then.

SimonBoulier · 2018-11-15T11:43:27Z

Superseded by #9004.

SimonBoulier requested review from forestjulien, gares, mattam82 and maximedenes as code owners May 31, 2018 12:33

ejgallego reviewed May 31, 2018

View reviewed changes

SimonBoulier requested a review from herbelin as a code owner May 31, 2018 13:32

Zimmi48 reviewed May 31, 2018

View reviewed changes

SimonBoulier requested a review from silene as a code owner May 31, 2018 14:44

maximedenes self-assigned this Jun 1, 2018

ppedrot requested changes Jun 1, 2018

View reviewed changes

SimonBoulier added 5 commits June 1, 2018 12:34

Add Unguarded syntax for (co)fixpoints.

eca3733

Disable guard check for (co)fixpoints when defined with `Ungarded` keyword.

Rename safe to guarded in ppvernac.ml.

239756b

Change message for (co)fixpoints assumed to be guarded in Print Assum…

8a15241

…ptions.

Fix documentation.

39f727c

Use vernac flags and atts record.

1c80909

[no ci]

ejgallego reviewed Jun 1, 2018

View reviewed changes

ejgallego suggested changes Jun 1, 2018

View reviewed changes

Add syntax to assume positive inductive types + various fixes.

58029a5

SimonBoulier force-pushed the unsafe_fixpoints branch from 8817cfb to 58029a5 Compare June 2, 2018 13:18

SimonBoulier changed the title ~~Add Unguarded syntax for (co)fixpoints.~~ [Work and discussion in progress] Add Unguarded syntax for (co)fixpoints. Jun 2, 2018

SimonBoulier changed the title ~~[Work and discussion in progress] Add Unguarded syntax for (co)fixpoints.~~ [Work and discussion in progress] Add Unguarded syntax for (co)fixpoints and Assumed Positive for (co)inductive types. Jun 2, 2018

Zimmi48 mentioned this pull request Jun 2, 2018

RFC: generic attribute syntax rocq-prover/rfcs#31

Closed

Zimmi48 added the kind: feature New user-facing feature request or implementation. label Jun 5, 2018

herbelin reviewed Jun 23, 2018

View reviewed changes

gares approved these changes Jun 25, 2018

View reviewed changes

maximedenes suggested changes Jul 16, 2018

View reviewed changes

Zimmi48 mentioned this pull request Nov 7, 2018

Design of attributes needs to be refined #8027

Closed

SimonBoulier closed this Nov 15, 2018

Uh oh!

Conversation

SimonBoulier commented May 31, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Zimmi48 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Zimmi48 commented Jun 1, 2018

Uh oh!

ppedrot commented Jun 1, 2018

Uh oh!

ppedrot left a comment

Choose a reason for hiding this comment

Uh oh!

maximedenes commented Jun 1, 2018

Uh oh!

maximedenes commented Jun 1, 2018

Uh oh!

Zimmi48 commented Jun 1, 2018

Uh oh!

ejgallego commented Jun 1, 2018

Uh oh!

maximedenes commented Jun 1, 2018

Uh oh!

ppedrot commented Jun 1, 2018

Uh oh!

ppedrot commented Jun 1, 2018

Uh oh!

Zimmi48 commented Jun 1, 2018

Uh oh!

ppedrot commented Jun 1, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ejgallego commented Jun 1, 2018

Uh oh!

ejgallego left a comment

Choose a reason for hiding this comment

Uh oh!

Zimmi48 commented Jun 1, 2018

Uh oh!

gares commented Jun 1, 2018

Uh oh!

SimonBoulier commented Jun 2, 2018

Uh oh!

ejgallego commented Jun 2, 2018

Uh oh!

Zimmi48 commented Jun 2, 2018

Uh oh!

ejgallego commented Jun 2, 2018

Uh oh!

ppedrot commented Jun 3, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mattam82 commented Jun 5, 2018

Uh oh!

maximedenes commented Jun 5, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

SimonBoulier commented May 31, 2018 •

edited

Loading

ppedrot commented Jun 3, 2018 •

edited

Loading

maximedenes commented Jun 5, 2018 •

edited

Loading