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 sequent goal is the term
`true`. - The sequent contains
`false`as a hypothesis. - The sequent can be proved by
`nthHypT`.

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

typeauto_prectypeauto_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_resourceresource(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:

valcreate_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.

valauto_wrap : tactic -> auto_tacvalauto_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 }BYbackThruHypT 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.