LTS: τ-transitions

Stream: CSLib

[Pieter Cuijpers]

I'm working on a PR to include branching bisimulation and ran into the need to introduce a closure relation on tau steps that is more basic that the already defined LTS.STr. I propose to call it LTS.τTr and would look something like this:

/-- Saturated τ-transition. relation. -/
inductive LTS.τTr [HasTau Label] (lts : LTS State Label) : State → State → Prop where
| refl : lts.τTr s s
| tr : lts.τTr s1 s2 → lts.Tr s2 HasTau.τ s3 → lts.τTr s1 s3

But if we have this, it makes sense to also update the other definitions that are intended to support weak bisimulation. I think LTS.STr could look something like:

/-- Saturated transition relation. -/
inductive LTS.STr [HasTau Label] (lts : LTS State Label) : State → Label → State → Prop where
| refl : lts.τTr s  s
| tr : lts.τTr s1 s2 → lts.Tr s2 μ s3 → lts.τTr s3 s4 → lts.STr s1 μ s4

and a number of downstream 'induction helpers' would change into more τ-focused ones.

I'm willing to make the changes, but I would like to know if `everyone agrees' before embarking on such a refactoring. I hope there is not too much outside the LTS.basic file that needs updating as a result, but I don't know how to check this.

[Fabrizio Montesi]

The former sounds like 'tau transition', so it should probably be defined as lts.toRelation HasTau.tau; then we could define a tauSTr by applying the Refl/Trans Gen stuff in mathlib (which iirc comes with theorems/utilities) to it.
I haven't thought much about reformulating STr yet, but it sounds like it might make sense since it'd use simpler components (albeit multiple ones vs only one right now)?

[Pieter Cuijpers]

I've taken a stab at implementing my own definition and succeeded with minimal damage to the remainder of the library. But your suggestion to make it a lts.toRelation sounds interesting. Do you have a more precise definition for me? (I'm not familiar with that part of the mathlib library yet.)

And is there a way to share my progress on the refactoring without doing a PR? (I think I've made too many changes at once for a proper PR...)

[Pieter Cuijpers]

@Fabrizio Montesi I am tempted to first make a PR in which I split the basic file and the bisimulation file into smaller files. Have a "HasTau" file with basic definitions for the relation above, and a "WeakLTS" with the definition of the STr. How would you feel about that? I think it would give me a better overview of what it is that we are working on, and it would also allows a bit more precise explanation of what is going on in the doc-string.

[Fabrizio Montesi]

Pieter Cuijpers said:

I've taken a stab at implementing my own definition and succeeded with minimal damage to the remainder of the library. But your suggestion to make it a lts.toRelation sounds interesting. Do you have a more precise definition for me? (I'm not familiar with that part of the mathlib library yet.)

And is there a way to share my progress on the refactoring without doing a PR? (I think I've made too many changes at once for a proper PR...)

Sure. You can use this to define tauTr: https://cs-lean.github.io/Cslib/Foundations/Semantics/LTS/Basic.html#LTS.Tr.toRelation

And then this to define its reflexive and transitive closure: https://cs-lean.github.io/Mathlib/Logic/Relation.html#Relation.ReflTransGen

[Fabrizio Montesi]

Re sharing progress: create a branch in your fork and share a link to that here?

[Fabrizio Montesi]

As to restructuring: we probably should, files are getting a bit big. As a first step, I'd still keep all things about tau and saturated transitions in LTS Basic, but we should at least split the different kinds of bisimilations out.

[Fabrizio Montesi]

I'm planning to do some splits like this next week, so probably good to discuss them here first. This shouldn't block the work on tauTr & co.

[Pieter Cuijpers]

That looks useful indeed :-) I'll give it a shot.

[Pieter Cuijpers]

First attempt can be found here: https://github.com/PieterCuijpers/cslib/blob/tauTr/Cslib/Foundations/Semantics/LTS/Basic.lean

I've for the time being removed the definitions of STrN. I have a sense of why they would be useful if you are formalizing textbook proofs, but it's not really clear to me why we need them here already. I have not looked into whether "Relation" also has "RelationN" support in this way. If it has, fixing STrN is easy of course.

Not having STrN also breaks some things in SWBisimulation.

[Fabrizio Montesi]

STrN is used in proofs about weak/SW bisimulation iirc.

[Fabrizio Montesi]

that (fun s1 s2 => lts.Tr s1 HasTau.τ s2) can just be lts.Tr.toRelation HasTau.τ, as I pointed out before. (or have you tried and it didn't work?)

[Fabrizio Montesi]

and what you call τTr, I'd call τSTr, because it's reflexive and transitive (like STr).

[Fabrizio Montesi]

although that's not a great name either, I admit, just a bit better, because it might be confused with STr itself... :-\

[Pieter Cuijpers]

It didn't, but that was my bad, the following does work:

def LTS.τTr [HasTau Label] (lts : LTS State Label) : State → State → Prop :=   Relation.ReflTransGen (Tr.toRelation lts HasTau.τ)

[Pieter Cuijpers]

Not sure about naming either, I'm guessing both will be fine ultimately.

[Fabrizio Montesi]

sorry for the delay, been a bit swamped lately.
What I meant to say is that while I admit τSTr isn't a great name, it's at least acceptable for now.
τTr I'm too afraid it'll confuse concurrency theorists used to think of a 'tau-transition' as just a lts.Tr s1 HasTau.τ s2.

[Pieter Cuijpers]

Same swamp here ;-) Had a chance to update and look into it again a bit today.
I agree with your concern about the naming, so I've updated.
Also finished some of the small proofs.
In the meantime, I've lost the overview of what proofs are needed, but the ones that are in there now work.
Started a separate PR for this.

[Pieter Cuijpers]

I was wondering if the "labeling by number of tau steps" is - in the end - really helpful?
(I mean the STrN definition and proofs).
I appreciate that in literature people will like to think of the induction to go over the number of tau steps,
so if you want to mimick a proof from literature it may be helpful to have theorems like this.
But I imagine that there is always a "simpler" or "shorter" proof without in Lean, since the actual induction
takes place over the definition of STr anyway.

Why did you originally decide to include them?

[Fabrizio Montesi]

Pieter Cuijpers said:

I was wondering if the "labeling by number of tau steps" is - in the end - really helpful?
(I mean the STrN definition and proofs).
I appreciate that in literature people will like to think of the induction to go over the number of tau steps,
so if you want to mimick a proof from literature it may be helpful to have theorems like this.
But I imagine that there is always a "simpler" or "shorter" proof without in Lean, since the actual induction
takes place over the definition of STr anyway.

Why did you originally decide to include them?

I remember Lean giving me trouble with things about SWBisimulation, so at the time I just went for the 'standard' technique of counting tau-steps. Also because that enables comparing the 'efficiency' of saturated transitions in the future, which is sometimes used in asymmetric relations like expansion (IIRC) -- however, arguably even there we could just do with an inductive, I guess.. to be checked in the future.

[Fabrizio Montesi]

Thanks for cslib#220, @Pieter Cuijpers. I struggle a bit to get what's new and what's old, probably because you had to move some stuff around, there's some spacing change(s), and you reverted some 'scoped grind' to 'grind' (this is probably because you have to merge main).

Since the PR doesn't touch on many defs for now, would you be ok with this plan: (a) I move the Relation and Trans sections where you need them in the main branch; and then (b) you pull/merge from 'main' and modify things a bit more in place?

[Fabrizio Montesi]

Ah, and this is making me realise that the Relation- and Trans-related definitions should be spread out: each relation should define its own stuff. WIP...

[Fabrizio Montesi]

There, something like this: cslib#231