The Formal Strong Completeness of Boolean BI

This archive contains version 2.0 of BBICoq, the formal proof of the Strong Completeness of Boolean BI based on the labeled Tableaux method, implemented in the system Coq.

It is distributed under the CeCILL v2 Free Software Licence Agreement. It includes no code borrowed from any other project but uses the Coq Standard Library, mainly: This code was developped under different versions of Coq and CoqIDE but this final version 2.0 should run without any problem under Coq version 8.3pl3 (January 2012).

Update: the 2.0 version of BBICoq is incompatible with Coq 8.4. The reason is change in the structure of the standard Coq library (Max in particular). Download version 2.1 of BBICoq if your Coq version is 8.4+. I checked the 2.1 version against Coq version 8.4pl1 (January 2013).

The Makefile was generated by the coq_makefile command. To compile the code, simply type make.

The informal proof on which this code is based is published in the Journal of Logic and Computation.
Here is a short description of the different modules

Utilities for reasonning
Utilities for lists
Utilities for predicates (viewed as sets) and maps
predicate.v sets, inclusion, (extensional) identity, [binary|indexed] unions & intersections, pred_solve tactic
maps.v maps, injectivivity, (infinite) surjectivity, boundedness, direct and inverse images
Utilities for finite sets
carrier.v lists as carriers of finite sets/predicates
finite.v properties of finite sets
Utilities for graphs of functions
graph.v graphs of functions
uniq_choice.v a unique choice recursive principle
Utilities for closure operators and systems of rules
closure.v properties of closure operators
system.v relations defined by systems of finitary derivation rules, proof objects
system_extensions.v extra properties of rule systems, compactness property
Utilities for natural numbers and indexations by the type nat
natpred.v sets of natural numbers
natseq.v sequences of natural numbers
maxf.v the maximum function on sequences of nat
cantorbernstein.v a constructive proof for indexing types by nat
enum.v (surjective) enumerations by nat
nat2.v a bijection nat <-> nat*nat
enumerations.v enumerations and recursive datatypes
nathole.v an injection nat -> nat avoiding a finite set of elements
Utilities for analytic tableaux
branch.v generic branch equivalence
tableaux.v generic tableaux proofs and properties of tableaux proofs
Main data structures for Partial Monoidal Equivalences (PME)
labels.v a particular nat indexed set of letters
words.v words (as list of letters), permutation equivalence, substitutions
constraints.v constraints (pairs of words), languages and alphabets
substitutions.v substitutions based on words of labels
pme.v partial monoidal equivalences, pme closure
Syntax and semantics of Boolean BI
formula.v the syntax of BBI
css.v the tableaux branches for BBI
kripke.v the PME semantics for BBI
Semantic Tableaux proofs for Boolean BI
bbi_expansion.v BBI tableaux expansion definition
bbi_exp_props.v properties of BBI tableaux expansion
bbi_closed_branch.v closure for branches in BBI tableaux
bbi_tableaux.v properties of BBI tableaux
The soundness of Tableaux proofs
bbi_realizability.v realizable branches have no closed tableaux
The strong completeness of Tableaux proofs
bbi_strategy.v infinite enumeration for BBI tableaux statements
bbi_oracle.v the counter-model building oracle
bbi_simple.v simple PMEs
bbi_basic.v basic PMEs
bbi_sequence.v the tool to build an increasing sequence of branches
bbi_limit.v the BBI tableaux extracted counter-model
bbi_hintikka.v Hintikka built counter-models
The Main Theorems

Dominique Larchey-Wendling
The TYPES team
CNRS, Bâtiment LORIA, BP 239
54506 Vandoeuvre-lès-Nancy

email :
Phone number: +33 (0) 3 54 95 85 14
Fax: +33 (0) 3 83 41 30 79

Last modification : 2014/06/03.