Matita HomeMatita HomeThe system shares a common look&feel with the Coq proof assistant and its graphical user interface. The two systems have the same logic, very close proof languages and similar sets of tactics. Moreover, Matita is compatible with the library of Coq. From the user point of view the main lacking features with respect to Coq are:
proof extraction;
an extensible language of tactics;
automatic implicit arguments;
several ad-hoc decision procedures;
several rarely used variants for most of the tactics;
sections and local variables. To maintain compatibility with the library of Coq, theorems defined inside sections are abstracted by name over the section variables; their instances are explicitly applied to actual arguments by means of explicit named substitutions.
Still from the user point of view, the main differences with respect to Coq are:
the language of tacticals that allows execution of partial tactical application;
the unification of the concept of metavariable and existential variable;
terms with subterms that cannot be inferred are always allowed as arguments of tactics or other commands;
ambiguous terms are disambiguated by direct interaction with the user;
theorems and definitions in the library are always accessible without needing to require/include them; right now, only notation needs to be included to become active, but we plan to remove this limitation.