The Formal Strong Completeness of partial monoidal BI


This archive contains the final version 2.0 of the formal proof of the Strong Completeness of partial monoidal 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).

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

This code is direct adaptation of the formal proof of strong completeness of partial monoidal Boolean BI, available elsewhere on this site: you can find an informal proof there as well.
Here is a short description of the different modules

Utilities for reasonning
replace.v
classical_help.v
Utilities for (dependent) lists and parametric terms
list_fall_exst.v
list_in_t.v
list_fall_exst_t.v
dlist.v length dependent lists
term.v terms based on a signature
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 Orders (PMO)
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 orders, pmo closure
Syntax and semantics of BI
formula.v the syntax of BI
css.v the tableaux branches for BI
kripke.v the PMO semantics for BI
Semantic Tableaux proofs for BI
bi_expansion.v BI tableaux expansion definition
bi_exp_props.v properties of BI tableaux expansion
bi_closed_branch.v closure for branches in BI tableaux
bi_tableaux.v properties of BI tableaux
The soundness of Tableaux proofs
bi_realizability.v realizable branches have no closed tableaux
The strong completeness of Tableaux proofs
bi_strategy.v infinite enumeration for BI tableaux statements
bi_oracle.v the counter-model building oracle
bi_simple.v simple PMOs
bi_basic.v basic PMOs
bi_sequence.v the tool to build an increasing sequence of branches
bi_limit.v the BOI tableaux extracted counter-model
bi_hintikka.v Hintikka built counter-models
The Main Theorems
bi_sound_and_complete.v

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

email : larchey@loria.fr
Phone number: +33 (0) 3 54 95 85 14
Fax: +33 (0) 3 83 41 30 79

Last modification : 2012/10/24.