feat: tauSTr

[PieterCuijpers]

Separating the series of tau steps from the saturation relation to benefit the definition of branching bisimulation later.

Not sure if this counts as a feat: or refactor:, since it is a relatively small change and should not touch anything outside the scope of the file at the moment.

[PieterCuijpers]

I've updated the file to use #231
Still in doubt a bit on how to use @[grind] correctly.
When do you use "scoped" and which modifier (=, =, ->, .) should I use when?

Also, the naming of theorems is a bit confusing wrt the STr relation.
Do I name a theorem foo_sTr or foo_STr?
I'm personally inclided towards the latter, and tried to use it consistently, but since theorems generally prefer small letters I'm not sure if that is correct.

[chenson2018]

When do you use "scoped"

In CSLib we typically use scoped for almost all grind rules. Note that if this would put something in too deep of a namespace with a regular annotation, you can add it afterwards like attribute [grind] foo. (Soon there will be "grind sets" that make this easier)

which modifier (=, =, ->, .) should I use when?

See this page for a full description of patterns.

Also, the naming of theorems is a bit confusing wrt the STr relation. Do I name a theorem foo_sTr or foo_STr? I'm personally inclided towards the latter, and tried to use it consistently, but since theorems generally prefer small letters I'm not sure if that is correct.

We try to follow the Mathlib naming conventions but I will readily admit these don't come naturally to me for these oddly cased names. I think the relevant rule is:

5. When something named with UpperCamelCase is part of something named with snake_case, it is referenced in lowerCamelCase.

[PieterCuijpers]

See this page for a full description of patterns.

Hm... maybe it is better if I leave out @[grind] altogether for the time being?
I have some incling of the choices I should make, but I also realize that the wrong choice might mess things up thoroughly.

What is better for this PR, just leaving it out, or making an educated guess and hoping you will catch it if its wrong?

[fmontesi]

You can test what grind is doing by using the ? modifier, which will tell you the grind pattern being created. So you can try @[scoped grind? =>], @[scoped grind .], etc. and check what you prefer.

[fmontesi]

What's the status of this? I see some conflicts and I'm afraid of messing it up. :)

[PieterCuijpers]

I got into trouble making the changes, because it turned out I overlooked one of the bisimulation theorems when I thought the "metric" version was not being used anymore. And after that, I ran out of time and got swamped in teaching preparations. So it is indeed a bit of a mess now.

If you have ideas on how to clean it up and have time, please feel free to do so!

Next week Thursday, I hope to get four students who want to work with Lean4.
I have asked them to introduce themselves on Zulip and find a theorem they would like to work on.
I would like to see if we can get them to make useful contributions to the library.
So if you have suggestions for good (beginner) contributions, please suggest those to them.
(Since I'm also running my masters course in that same period, my own contributions will likely be limited to monitoring and reviewing the work of those students.)

[PieterCuijpers]

Fixed it! I hope... (Awaiting automatic checks to finish.)

I have now removed everything related to "induction over N tau-steps" and replaced this with a straightforward induction over tauSTr.

[PieterCuijpers]

It seems that I'm dependent on maintainers to run automatic workflows to check my code.
Is that on purpose, or is there something I can do to fix that?
If not, what can I do to verify commits on my own machine, apart from running "lake build"?

[chenson2018]

It seems that I'm dependent on maintainers to run automatic workflows to check my code. Is that on purpose, or is there something I can do to fix that?

This is a security measure that GitHub implements. Once your first PR is merged, this requirement is removed. I would do so now, but I'm not sure if/how this can be done ahead of time.

If not, what can I do to verify commits on my own machine, apart from running "lake build"?

CONTRIBUTING.md is where I have documented how to run the checks CI does locally.

The failure you are seeing is from lake test. Specifically these grind lints only slightly over the threshold I think can be registered as exceptions for the time being. (The annotations for LTS need some work in general)

[PieterCuijpers]

CONTRIBUTING.md is where I have documented how to run the checks CI does locally.

The failure you are seeing is from lake test. Specifically these grind lints only slightly over the threshold I think can be registered as exceptions for the time being. (The annotations for LTS need some work in general)

Thanks, that helps.
Except that I do not know how to register something as an exception... or where to find that?

[chenson2018]

Yes, I should document this... you add a #grind_lint skip ... line in CslibTests/GrindLint.lean.

[PieterCuijpers]

Thanks. For now, I managed to get all checks to pass by iterating on the test output.
I'm not sure if this is now already ready enough for the PR to go ahead, or whether I should add more @[grind] annotations.
Please let me know.

@fmontesi I have now removed all of the no-longer-needed theorems regarding STrN. I hope the changes are now a bit more readable for you.