Matita HomeMatita Home- The 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.