Tac is a framework for implementing interactive theorem provers with good support for both interactive proof development and automated proof search. While our main research focus is on automated reasoning, it is useful to be able to interactively play with the logic when developing automated tactics; moreover, an interactive system is often useful to manually fill the gaps between automatically discovered proofs. Currently, the main development within Tac is the logic μLJ and its automated focused inductive theorem proving tactic. Tac provides several tools:
The logic μLJ is a simple but powerful extension of first-order logic with equality, least and greatest fixed points and minimal generic quantification. It enjoys a focusing proof system on which our implementation relies, for both automatic and interactive proof developments.
Learn more about μLJ in Focused Inductive Theorem Proving by Baelde, Miller & Snow (submitted paper).
The distributed system comes with several example theorems. They include proofs of properties of Peano arithmetic, standard list predicates, the pi-calculus, Buchi automata, and lambda calculus variants (e.g., PCF, F≤).
Tac can be used to interactively write proofs. For example,
in the domain of operational semantics, we have developed proofs
of subject reduction, determinacy of typing, transitivity of
subtyping for a variety of systems.
To help in this tedious task, Tac offers a powerful automated
prove, which can prove several theorems
or proof obligations.
Here is a list of such theorems:
pi x\ pi y\ nat x => nat y => sigma z\ ack x y z, nat z.
pi x\ nat x => sigma h\ half x h.
pi x\ pi r\ reverse x r => reverse r x.
As said above, Tac produces proofs. Here are a couple examples. Most proofs are outlined: the asynchronous phase (invertible rules) is collapsed into one rule, leaving only the more relevant information in the proof. Even using this technique, we can only show here some of the simplest proofs automatically discovered. Larger proofs would be not only be unreadable, but in fact are not even manageable for LaTeX. Also, several of the Postcript files below are known to not work in Ghostview.
half) is total, with a hand-crafted invariant and only one induction (PS) or proved automatically using nested inductions (PS).
sim.muLJ.tac: simulation is reflexive (PS) and transitive (PS).
copy.muLJ.tac: inductive equality on λ-terms implies term equality, PS, PNG (large files, use a powerful viewer).
lambda/lemmas.muLJ.tac: keys and variables found in a context that does not use a generic variable cannot use it either (PS).
Download: We released Tac 0.9.2 in January 2010. Get the source code, or the latest Windows installer.
Open source repository: Active development versions are available from the Slimmer SVN repository hosted by INRIA's Gforge. You can browse the repository, in particular ourexamples.
Tac is an open source project. The first major version was released on 18 June 2008. We welcome contributions from others of both theorems and new features. The developers behind the current distribution are:
Much of the effort for this work is supported within the context of the Slimmer project, which is supported by funds from INRIA and NSF. Support has also been provided by the NSF Grants OISE-0553462 (IRES-REUSSI) and CCF-0917140. Of course, the opinions, findings, and conclusions or recommendations expressed in this material are those of the project participants and do not necessarily reflect the views of INRIA or the National Science Foundation.