MEBI: Mechanised Bisimilarities

This repository contains a Coq plugin for automating bisimilarity proofs (which are currently taken from the methods detailed in "Advanced Topics in Bisimulation and Coinduction", Section 3.2.2).

Work in progress

---

Building the Project

Using coq 8.20.0, below is the "fool-poof" method:

make .merlin clean; dune build; coq_makefile -f _CoqProject -o CoqMakeFile; make -f CoqMakeFile

Running tests

Compiling using the above will also generate a tests.exe which can be run:

_build/default/test/tests.exe

Altogether

make .merlin clean; dune build; coq_makefile -f _CoqProject -o CoqMakeFile; make -f CoqMakeFile; _build/default/test/tests.exe

Using VSCode

Use the vscoq extension and build as shown above. Afterwards, you have to reload vscode. (This extension is helpful for this.)

Issues with vscoqtop

Try adding this to your workspace settings .json file, under the "settings" field:

"vscoq.path": "/home/user/.opam/mebi/bin/vscoqtop"

E.g.:

{ "settings": {
    "vscoq.path": "/home/user/.opam/mebi/bin/vscoqtop"
} }

Access this file by pressing ctrl+, and then clicking the file icon button in the top right corner, which will open the settings as a json file.

Scratchpad

Command that declares a relation as a "LTS-generating relation":

MeBi LTS <ident>.

• <ident> should be the identifier of a relation with type Term -> Action -> Term -> Prop.

TODO

So far, this is essentially coq/doc/plugins_tutorial/tuto1 but renamed. Here is the current TODO list.

• Reading step relation with type Step : Term -> Label -> Term -> Prop' that captures state transitions in a LTS semantics.

• Reading terms t : Term.

• Building a state machine using Step for term t

• Implementing one of the algoriths for deciding bisimilarity in Sangiorgi's book.

Questions:

• We need to build a proof in Coq that two terms are bisimilar. We need the statement in terms of Step, and turn the result of our algorithm into sequences of Coq tactics.
• Tau transitions/weak bisimilarity?
• Open terms/use of existing lemmas?

Other Resources

Templates

• (Community) Coq Plugin Template
• (Community) Coq Program Verification Template

Tutorials

• (Official) Coq Plugin Tutorial
• (tlringer) Coq Plugin Tutorial (see also)

Other

• Coq Makefiles

• Writing Coq Plugins

• Dune Init

• Dune Coq Plugin Project

• Ltac

• Ltac2

• evar-map helper functions in coq-plugin-lib (recommended by tlringer)

Papers

• Popescu, A., Gunter, E.L. (2010). Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization
• Rodrigues, N., Sebe, M.O., Chen, X., Roşu, G. (2024). A Logical Treatment of Finite Automata.
• Stefanescu, A., Ciobaca, S., Moore, B., Serbanuta, T.F., Rosu, G. (2013). Reachability Logic in K

Books

• Sangiorgi, D. (2011). Introduction to Bisimulation and Coinduction
• Sangiorgi, D., Rutten, J. (2011). Advanced Topics in Bisimulation and Coinduction