Mtac2

Mtac2 is a plugin for the Coq proof assistant that introduces a typed tactic language for backward reasoning. It provides a monadic framework for writing and composing tactics with stronger type guarantees than Coq's native Ltac, improving reliability and expressiveness in proof automation.

Key Features

• Typed Tactics — Tactics are first-class citizens with types, enabling better error checking and composition.
• M Monad — A monadic interface for tactic execution, offering structured control flow and exception handling.
• Backward Reasoning — Supports goal-directed proof construction, similar to traditional Coq tactics but with enhanced typing.
• Tactic Combinators — Provides combinators for building complex tactics from simpler ones, facilitating modular proof automation.
• Intro Patterns — Includes support for intro patterns to manipulate hypotheses during proof steps.
• Constr Selector — Allows selection based on inductive type constructors, aiding in case analysis and pattern matching.

Philosophy

Mtac2 emphasizes type safety and composability in tactic design, aiming to make proof automation in Coq more robust and maintainable through a principled, monadic approach.