package coq-trakt

Trakt is a Coq plugin that provides a new Coq tactic, trakt, for preprocessing goals before handing them to a proof automation tactic, as well as Coq commands to fill a knowledge database before calling the tactic.

Drawing inspiration from the zify tactic in the Coq standard library, it acts like a type-level funnel by casting all the possible values in the goal into a given target type. It can also express logic in Prop or bool according to the user's choice.

The translation is implemented in Coq-Elpi. It is certifying (it leaves no proof obligation), generic (the translation does not focus on a precise theory, it is determined by the parameters and user knowledge), and efficient (it tries to make sparse use of Coq conversion).