CCS behavioural theory

Stream: computer science

[Thomas Waring]

I’ve been looking at some of the proof_wanteds in CCS.BehaviouralTheory as grind practice — bisimilarity_choice_nil went through nicely but I think bisimilarity_par_assoc is not true in the current formalisation. The problem is transitions like: image_6348A634-D21B-4C39-B8CA-98CA3DA5C836_1757690603.heic
which is allowed because we have define tau.co = tau. That doesn’t seem to be the case in the original presentation, see Theorem 5.5 where the above problematic case doesn’t appear. I’m new to the maths of this though so let me know if I’ve missed something! (ping @Fabrizio Montesi)

[Fabrizio Montesi]

Good I put that proof_wanted, because you're right. :-)

[Fabrizio Montesi]

Duality should be only on names.

[Fabrizio Montesi]

One solution I'm playing is to define Act.co only on a subtype of Act.

[Thomas Waring]

the one that came to mind was to have a predicate is_dual on actions and take two names as arguments to Tr.com, which must be name / coname or vice versa

[Fabrizio Montesi]

We can go down that road, too. I was thinking of the subtype because that matches exactly what people typically call 'visible actions' (all actions but \tau). You can see how it looks here:

https://github.com/leanprover/cslib/blob/8554d17fc62f7bd823301e5838f755ff72bbf0c5/Cslib/Languages/CCS/Basic.lean#L47

[Fabrizio Montesi]

My newfound addiction to grind made it easier than I expected..

[Thomas Waring]

this seems reasonable, but i'm having some trouble using it to rule out the problematic case — instead of seeing that the transition in question can't be Tr.com, I get an error along the lines of (VisibleAct.co Name μ).1 = τ, I think because lean is pattern matching on the coercion not the VisibleAct itself. do you know how to get around this?

[Fabrizio Montesi]

Good point... I've been battling it for 2 hrs already and haven't figured out a solution. :-\ Mmmh..

[Fabrizio Montesi]

I got to the point where it's almost good. I wrote a custom casesOn that makes the \tau-case unreachable, but it's not picked up by the dependent elimination for Tr. So I gotta do cases on the transition label before doing cases on the transition derivation: https://github.com/leanprover/cslib/blob/2f5aa093f3facb49d51dbac76087f781d1f89406/Cslib/Languages/CCS/BehaviouralTheory.lean#L140

Very annoying. :\

[Fabrizio Montesi]

This is most certainly a recurring problem: we have an inductive type and we'd like to define a subtype that only has some of its cases. We could go down other routes, but it'd be very nice to know whether this is really a hornet's nest or if it's just us being naive.

[Thomas Waring]

it seems to me also that there should be a way of making it work — in the meantime i implemented this IsDual version which goes through pretty easily, at the cost of DecidableEq Name assumptions

you can see how it looks on my scratch branch if you like — happy to turn it into a PR given that the proof_wanted's are filled in now

[Fabrizio Montesi]

Thanks, Thomas! Let's see if we can get some help understanding this in the general thread I started, since I'm interested in distilling the pattern. Otherwise I'm happy with your solution (btw why a Def and not an inductive?).

[Fabrizio Montesi]

I'm giving up on Subtype for now, I tried hard enough to be satisfied. :-)
Dependent case elimination has trouble with that kind of stuff, and I couldn't figure out how to make it work (yet..?).

[Fabrizio Montesi]

I've tried an approach based on Prop as you suggested, but ended up with a slightly different formulation. I've also cleaned up the previous stuff. What do you think? It's in branch ccs-fix.

I have fixed existing proofs but not completed the proof_wanteds, I'd like to merge those from you. :-)
But first let me know if you like my definitions and names, they can of course be changed. Adapting your proofs should be straightforward.

[Thomas Waring]

this all looks neat to me :-)

[Fabrizio Montesi]

Cool! I'm gonna merge it into main then. Feel free to prep a PR to fill in the proof_wanted you've completed, once you've adapted your code.

Edit: done!

[Thomas Waring]

The PR is up :) not only was adapting the proofs easy literally all that was required was changing the name Act.IsDual to Act.Co (the joy of good definitions)