The coq proofs are available below; is used either the excluded middle or a well-foundedness hypothesis over the reduction relation (instead of the non-divergence hypothesis).
Instructions: Download the sources. You can directly use the files in interactive mode or with coqide (no compilation is needed). The main result is in the file unique_sol_thm.v. Details are explained in the
comments, and in the README.
You can download the sources:
The files are split as follows, and in the following order:
- rels.v
A few lemmas and definitions regarding relations; the definitions of diagrams
is usefull to define bisimulations and bisimilarities
- LTS.v
Defines the notion of Labeled Transition System (with internal tau steps),
and the usual definitions of weak transitions in such a LTS.
- bsim.v
Definition and properties of weak bisimulations, and weak bisimilarity. Most
of the work is related to the transitivity of weak bisimilarity.
- operators.v
Definition of autonomous transitions, then of sets of operators; also includes
some properties of functions, extensional equality of functions, and composition
of functions.
- divergences.v
Definitions of the notions of reducts of an operator and divergence of the infinite
unfolding of an operator.
- unique_sol_prop.v
The first lemma: if an operator 'protects its solutions', then it has a unique
solution up to weak bisimilarity.
- termination.v
A few lemmas regarding termination, non divergence, well-foundedness.
- unique_solution_steps.v
The main part of the proof of the main theorem: we build a sequence of transitions
and operators, and use non divergence to show it must terminate; if it does, that
proves that the operator protects its solution.
- unique_solution_thm.v
Putting everything together: statement of the main theorem.
Some important definitions (particularly those used as hypothesis, if one wants to check) are in:
LTS, weak transitions (wtrans, wttrans, whtrans): LTS.v
(strong and weak) bisimulation and bisimilarity: bsim.v
extensional equality of functions, autonomous transitions, guardedness, set of operators, weak autonomous transitions (waut, wtaut, whaut): operators.v
reduct (comp_red) of an operator, divergence (comp_div and div) of an operator (of its infinite unfolding): divergences.v
unique solution, protects its solutions: unique_sol_prop.v
the tau reduction relation (red_tau and reduction_tau) are in termination.v (for red_tau) and in unique_solution_thm.v (for reduction_tau). they are based on subrevR in termination.v, itself using comp_red from divergences.v