Tutorial Equations: well-founded recursion #8

thomas-lamiaux · 2024-05-14T00:50:31Z

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 :

Write some text in the intro to well-founded recursion, section 1.1
Solve the issues with the ackerman function, section 1.2
Better text for definition using obligations
~~Find a good examples for subterm relation, section 2.1~~

…into tuto-equations-wf

thomas-lamiaux · 2024-05-18T00:55:01Z

The tutorial is now ready to be reviewed. It :

add a new tutorial
adds a paragraph to CONTRIBUTING about discussing what does not work
makes marginal modifications to Tutorial_Equations_basics and README

src/Tutorial_Equations_wf.v

MevenBertrand

I've found this tuto a bit more messy than the previous one. I feel my main issues were the following.

There is a lot of knowledge which is not specifically about well-founded induction, but rather about how to generally go about the obligation mechanism. They are scattered through the tutorial as things go, which makes them not so visible. Maybe having a self-contained presentation of this mechanism (Equation vs Equations?, printing and (locally) changing the obligation tactic, printing the obligations with Obligations, being careful that no obligations are left, etc.), either in this tutorial, in the one of Equations' basics, or a self-contained one.

I found the presentation of well-founded induction unclear: the first example, last, is a very specific limitation of the guard-checker of Coq, but it is really at the border, and thus not very enlightening. The examples of nubBy or gcd, which require non-trivial reasoning, are more to the point. Ackerman is nice to introduce lexical ordering, but I feel like this can come slightly later. I would rather start by using a measure with the well-founded order lt on nat (which btw Equation picks by default if you write only by wf (length l)), and introduce lexical order in a second time as a more advanced example. Also, I'm not sure a reader would be able to understand the current 1.1 if they do not already have heard about proofs of termination for functions, well-founded orders, etc.

I know it was a frustrating experience in the writing of the tutorial, and that it's good to give users ways to circumvent issues when they pop up rather than pretending everything is fine, but I feel a lot of cognitive load in 1.2 is spent of funelim and rewrite going wrong. This somehow deflects from the "main point" of the tutorial into subtle, more advanced issues.

Also, a few suggestions on more things that might be useful to have in this tutorial:

usage of map and friends which remember which list an element was in (something similar in spirit to the inspect pattern, see for instance here and here)
using the database [WellFounded], possibly in combination with Derive to obtain the subterm relation and an automatic proof that it is well-founded. Very useful for well-founded induction which is more or less structural but more complicated than what the guard detects (for instance, if one want to do the last example without resorting to length but directly by a well-founded order on lists)

It's a long review with a lot of comments, but I must say this tuto is still a nice step in the right direction of making Equations more accessible!

src/Tutorial_Equations_wf.v

thomas-lamiaux · 2024-05-28T17:15:56Z

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

Co-authored-by: Meven Lennon-Bertrand <[email protected]>

thomas-lamiaux · 2024-05-28T22:11:01Z

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 · 2024-05-29T08:50:07Z

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

-> Seperate section 1 in two sections "Intro to wf" and "wf and Equations" -> Remove the last example from the file, and ack from 1.2 -> Remove content that is now in tuto obligations

thomas-lamiaux · 2024-06-09T23:48:40Z

@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

MevenBertrand

I only looked at the obligations tutorial, lgtm up to some minor polishing. And I think it is much better to factor this out like it is done now.

MevenBertrand · 2024-06-10T14:15:27Z

src/Tutorial_Equations_Obligations.v

+
+    Therefore, we would much rather like to build our terms using the proof mode.
+    This is exactly what [Program] and obligations enables us to do.
+    At every point in a definition, it enables us:


Suggested change

At every point in a definition, it enables us:

At every point in a definition, it allows us to:

The structure of the list is a bit strange, the "allow to" really only applies to the first item. Maybe try to rephrase?

src/Tutorial_Equations_Obligations.v

Co-authored-by: Meven Lennon-Bertrand <[email protected]>

…into tuto-equations-wf

Lysxia · 2024-06-12T11:22:07Z

src/Tutorial_Equations_wf.v

+    In the following, we assume basic knowledge of obligations as discussed
+    in the (short) tutorial Equations: obligations.
+
+    ** 2.1 Using a size argument


Instead of framing the 2.1 and 2.2 examples as "size vs measure" I think it would be clearer to only talk about "measure", then 2.1 gives a simple example (where the measure depends on one argument), and 2.2 shows that the measure can depend on all of the arguments.

I was thinking about it and hesitating. I'll do that, thanks.

thomas-lamiaux · 2024-06-12T13:12:43Z

Ready to be reviewed again

MevenBertrand

Looks good to me! (Up to a big pass of clean-ups). Things are probably not perfect, but le mieux est l'ennemi du bien ;)

src/Tutorial_Equations_wf.v

MevenBertrand · 2024-06-18T15:33:34Z

src/Tutorial_Equations_wf.v

+    the obligation [sizeRT l < 1 + list_sum (map sizeRT lt0)] corresponding to
+    the case where [lt := l :: _].
+    This is obviously true, but we are stuck trying to prove it as we do not
+    remember that [l] in in [lt]:


Suggested change

remember that [l] in in [lt]:

remember that [l] is in [lt]:

MevenBertrand · 2024-06-18T15:33:41Z

src/Tutorial_Equations_wf.v

+Proof.
+    simp sizeRT.
+    (* What to do know ? We have forgotten that x is in l,
+      and hence that sizeRT l < 1 + list_sum (map sizeRT l0)  *)


Suggested change

and hence that sizeRT l < 1 + list_sum (map sizeRT l0) *)

and hence that sizeRT l < 1 + list_sum (map sizeRT lt) *)

src/Tutorial_Equations_wf.v

Co-authored-by: Meven Lennon-Bertrand <[email protected]>

thomas-lamiaux

Thanks for looking at it

thomas-lamiaux · 2024-06-19T12:10:34Z

src/Tutorial_Equations_Obligations.v

+    Hence, when there is no obligation proof mode is open for nothing, and
+    has to be closed by hand using [Qed] or [Defined] as it can be seen below.
+    As it is easy to forget, a warning is raised.
+*)


So I have asked and it does enable a better control, btw that is one of the advantage of Next obligation compared to Equation?, but I would rather not talk about it as it is really advanced.

src/Tutorial_Equations_wf.v

thomas-lamiaux · 2024-06-19T12:40:50Z

src/Tutorial_Equations_wf.v

+
+(** Knowing that the previous booleans have been [false] enables us to prove
+    that [R] is well-founded when combined with [h].
+    We omit the proof here because it is a bit long, and not very interesting


I am not what is the interrest here. To me it was showing of to declare and use a wf, not how to prove it is wf

thomas-lamiaux · 2024-06-20T20:53:57Z

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

MevenBertrand

🚀

src/Tutorial_Equations_wf.v

Co-authored-by: Meven Lennon-Bertrand <[email protected]>

draft tuto Equations wf

770b2cc

thomas-lamiaux marked this pull request as draft May 14, 2024 00:53

thomas-lamiaux and others added 9 commits May 14, 2024 21:52

some work

df65498

Merge branch 'tuto-equations-wf' of github.com:Zimmi48/platform-docs …

8eba324

…into tuto-equations-wf

implement new contribution guidelines

2a530ec

edit Contribting >> talk about issues

597b43c

edits contrib + readme

39fad41

Update README.md

2fca3ef

Update CONTRIBUTING.md

13ef8ab

fix ack

5ffb2f4

fix file

af42cec

thomas-lamiaux marked this pull request as ready for review May 18, 2024 00:51

thomas-lamiaux requested a review from Villetaneuse May 18, 2024 00:51

moved to_fill

dd94445

terencode reviewed May 21, 2024

View reviewed changes

src/Tutorial_Equations_wf.v Outdated Show resolved Hide resolved

src/Tutorial_Equations_wf.v Outdated Show resolved Hide resolved

thomas-lamiaux mentioned this pull request May 21, 2024

Whishlist for Equations #20

Closed

6 tasks

MevenBertrand reviewed May 28, 2024

View reviewed changes

Fix typos from code review

11965de

Co-authored-by: Meven Lennon-Bertrand <[email protected]>

thomas-lamiaux added 5 commits June 9, 2024 02:04

add file on obligations

162bf2f

typos

09640bc

edits obligations

f540689

Major refactoring of tuto wf:

f7df1fc

-> Seperate section 1 in two sections "Intro to wf" and "wf and Equations" -> Remove the last example from the file, and ack from 1.2 -> Remove content that is now in tuto obligations

work on 2.1 2.2 2.3

f63b2e4

MevenBertrand reviewed Jun 10, 2024

View reviewed changes

Apply suggestions from code review

c51538c

Co-authored-by: Meven Lennon-Bertrand <[email protected]>

thomas-lamiaux added 11 commits June 10, 2024 18:13

typos

5e87263

Merge branch 'tuto-equations-wf' of github.com:Zimmi48/platform-docs …

4f7377f

…into tuto-equations-wf

add example linear search

6c6b586

some work

6554b53

added comments printing obligations

c2dbc80

edits 2.2

7fa2b64

content section 2.2

01761ff

removed section 2.2 by lack of example

4fa0bcf

typos

c70a734

more typos

07b975f

work 1.2

1ef2a48

Lysxia reviewed Jun 12, 2024

View reviewed changes

thomas-lamiaux added 2 commits June 12, 2024 13:37

clean up

59f92a5

clean up

1d0bb32

thomas-lamiaux requested a review from MevenBertrand June 12, 2024 13:12

MevenBertrand reviewed Jun 18, 2024

View reviewed changes

thomas-lamiaux and others added 2 commits June 19, 2024 14:36

Apply suggestions from code review

3159008

Co-authored-by: Meven Lennon-Bertrand <[email protected]>

Update src/Tutorial_Equations_wf.v

f9ee8e2

Co-authored-by: Meven Lennon-Bertrand <[email protected]>

thomas-lamiaux commented Jun 19, 2024

View reviewed changes

thomas-lamiaux and others added 2 commits June 19, 2024 14:45

Merge branch 'main' into tuto-equations-wf

0f0c509

edits custom wf

169591a

MevenBertrand reviewed Jun 21, 2024

View reviewed changes

src/Tutorial_Equations_wf.v Outdated Show resolved Hide resolved

src/Tutorial_Equations_wf.v Outdated Show resolved Hide resolved

thomas-lamiaux and others added 2 commits June 21, 2024 14:04

Update Tutorial_Equations_wf.v

ca5047b

Co-authored-by: Meven Lennon-Bertrand <[email protected]>

Update Tutorial_Equations_wf.v

beac686

Co-authored-by: Meven Lennon-Bertrand <[email protected]>

thomas-lamiaux merged commit 0e881e9 into main Jun 21, 2024
2 checks passed

thomas-lamiaux deleted the tuto-equations-wf branch June 21, 2024 12:14

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Tutorial Equations: well-founded recursion #8

Tutorial Equations: well-founded recursion #8

thomas-lamiaux commented May 14, 2024 •

edited

Loading

thomas-lamiaux commented May 18, 2024

MevenBertrand left a comment

thomas-lamiaux commented May 28, 2024 •

edited

Loading

thomas-lamiaux commented May 28, 2024

MevenBertrand commented May 29, 2024

thomas-lamiaux commented Jun 9, 2024

MevenBertrand left a comment

MevenBertrand Jun 10, 2024

MevenBertrand Jun 10, 2024

Lysxia Jun 12, 2024

thomas-lamiaux Jun 12, 2024

thomas-lamiaux commented Jun 12, 2024

MevenBertrand left a comment

MevenBertrand Jun 18, 2024

MevenBertrand Jun 18, 2024

thomas-lamiaux left a comment

thomas-lamiaux Jun 19, 2024

thomas-lamiaux Jun 19, 2024

thomas-lamiaux commented Jun 20, 2024

MevenBertrand left a comment

	At every point in a definition, it enables us:
	At every point in a definition, it allows us to:

	and hence that sizeRT l < 1 + list_sum (map sizeRT l0) *)
	and hence that sizeRT l < 1 + list_sum (map sizeRT lt) *)

Tutorial Equations: well-founded recursion #8

Tutorial Equations: well-founded recursion #8

Conversation

thomas-lamiaux commented May 14, 2024 • edited Loading

thomas-lamiaux commented May 18, 2024

MevenBertrand left a comment

Choose a reason for hiding this comment

thomas-lamiaux commented May 28, 2024 • edited Loading

thomas-lamiaux commented May 28, 2024

MevenBertrand commented May 29, 2024

thomas-lamiaux commented Jun 9, 2024

MevenBertrand left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thomas-lamiaux commented Jun 12, 2024

MevenBertrand left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thomas-lamiaux left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thomas-lamiaux commented Jun 20, 2024

MevenBertrand left a comment

Choose a reason for hiding this comment

thomas-lamiaux commented May 14, 2024 •

edited

Loading

thomas-lamiaux commented May 28, 2024 •

edited

Loading