MetaPRL trivialT and autoT tactics

The trivialT and autoT tactics are tactics for automated reasoning. The trivialT tactic performs "trivial" reasoning: in the ITT type theory, it solves sequent goals that meet one of the following requirements:

The autoT tactic performs all the reasoning of trivialT, and it adds recursive application. The trivialT and autoT tactics have the following resource definitions.

type auto_prec
type auto_tac =
   AutoTac of (tactic_arg -> (tactic * auto_tac) list)

type 'a auto_info =
   { auto_name : string;
     auto_prec : auto_prec;
     auto_tac : 'a
   }

resource (tactic auto_info, tactic, tactic auto_data) trivial_resource
resource (auto_tac auto_info, tactic, auto_tac auto_data) auto_resource

The resources are augmented with values of type auto_info. The auto_name is a string describing the component of the tactic. Tactics are given precedences: all tactics with lower precedences are tried first. Finally, the auto_tac field provides the function the implements part of the resource. For the trivialT tactic, this is just a tactic, but for the autoT tactic, a function is provided to compute a tactic and a continuation based on the tactic argument, allowing the parts of the autoT tactic to "remember" how they have been applied.

Precedences are created with the function:

val create_auto_prec : auto_prec list -> auto_prec list -> auto_prec

The first argument is a list of precedences that the new precedence should be larger than, and the second list is the precedences that the new value should be smaller than.

There are several wrappers that make the construction of autoT components easier.

val auto_wrap : tactic -> auto_tac
val auto_progress : tactic -> auto_tac

The auto_wrap function produces an auto_tac component from a normal tactic. The auto_progress wrapper computes an auto_tac component that remembers the goals that the components has been applied to, and fails if a goal ever repeats. This is used to add the backThruHypT and backThruAssumT tactics in the Itt_logic module.

There are several tactics that are defined as part of the autoT tactic.

The backThruHypT tactic performs "backward-chaining" through a hypothesis. The hypothesis should be a chain of universal quantifications and implications, and the sequent goal should match the remainder of the hypothesis. For example, the following proof fragment uses backward-chaining.

Goal: sequent { 'H; x: all x, y: x > y => int. x - y > 0 ... >- 2 - 1 > 0 }
BY backThruHypT 2
Subgoal 1: sequent { 'H; ... >- 2 > 1 }
Subgoal 2: sequent { 'H; ... >- int type }

There is a similar tactic for backward chaining through an assumption, called backThruAssumT.

Another part of the autoT tactic is a dT tactic which is described in the next section.