search

coq / platform-docs

A project of short tutorials and how-to guides for Coq features and Coq Platform packages.
https://coq.inria.fr/platform-docs/
Other
19 stars 10 forks source link

Tutorial Equations: well-founded recursion #8

Closed thomas-lamiaux closed 4 months ago

thomas-lamiaux commented 5 months ago

A tutorial explaining how to use Equations to define functions by well-founded recursion, and how to reason about such functions.

There is left to :

thomas-lamiaux commented 5 months ago

The tutorial is now ready to be reviewed. It :

  1. add a new tutorial
  2. adds a paragraph to CONTRIBUTING about discussing what does not work
  3. makes marginal modifications to Tutorial_Equations_basics and README
thomas-lamiaux commented 5 months ago

The comment's are good and I'll look into them. An issue I have is that I lack simple examples. Would you have some to share @MevenBertrand ? In particular, would you have a good example for

using the database [WellFounded], possibly in combination with Derive to obtain the subterm relation

thomas-lamiaux commented 5 months ago

Also the issue with ack in 1.2 is that it is supposed to be basic and yet it doesn't work as you would expect. Though to make it clearer I can move it to a section 3.

MevenBertrand commented 5 months ago

For your first question: maybe you can show how to do last a second time, but using subterm as the order rather lt + length? Otherwise, I don't have an example on the top of my head, but I will think about one.

Re: ack, I understand your issue, and I'm annoyingly not sure how to make it more readable (apart from having fixes merged upstream in Equations, it seems Matthieu is on it?). Maybe the solution would be again to have an alternative example which Equations does not choke on? (Again, I don't have one right now, but I can think about it.)

thomas-lamiaux commented 5 months ago

@MevenBertrand could you review the file tutorial about obligations and tell me if it is looks good to you ? Btw, I could also use help for the 2.2 part

thomas-lamiaux commented 4 months ago

Ready to be reviewed again

thomas-lamiaux commented 4 months ago

@MevenBertrand could you review the last commit. If all is good for you I'll merge. Btw if you hadn't noticed there is now automatic type checking and deployment.