`LIST_INDUCT_TAC : tactic`

SYNOPSIS
Performs tactical proof by structural induction on lists.

DESCRIPTION
LIST_INDUCT_TAC reduces a goal A ?- !l. P[l], where l ranges over lists, to two subgoals corresponding to the base and step cases in a proof by structural induction on l. The induction hypothesis appears among the assumptions of the subgoal for the step case. The specification of LIST_INDUCT_TAC is:
```                     A ?- !l. P
=====================================================  LIST_INDUCT_TAC
A |- P[[]/l]   A u {P[t/l]} ?- P[CONS h t/l]
```

FAILURE CONDITIONS
LIST_INDUCT_TAC g fails unless the conclusion of the goal g has the form `!l. t`, where the variable l has type (ty)list for some type ty.

EXAMPLE
Many simple list theorems can be proved simply by list induction then just first-order reasoning (or even rewriting) with definitions of the operations involved. For example if we want to prove that mapping a composition of functions over a list is the same as successive mapping of the two functions:
```  # g `!l f:A->B g:B->C. MAP (g o f) l = MAP g (MAP f l)`;;
```
we can start by list induction:
```  # e LIST_INDUCT_TAC;;
val it : goalstack = 2 subgoals (2 total)

0 [`!f g. MAP (g o f) t = MAP g (MAP f t)`]

`!f g. MAP (g o f) (CONS h t) = MAP g (MAP f (CONS h t))`

`!f g. MAP (g o f) [] = MAP g (MAP f [])`
```
and each resulting subgoal is just solved at once by:
```  # e(ASM_REWRITE_TAC[MAP; o_THM]);;
```

Essentially the same effect can be had by MATCH_MP_TAC list_INDUCT. This does not subsequently break down the goal in such a convenient way, but gives more control over choice of variable. For example, starting with the same goal:
```  # g `!l f:A->B g:B->C. MAP (g o f) l = MAP g (MAP f l)`;;
```
we get:
```  # e(MATCH_MP_TAC list_INDUCT);;
val it : goalstack = 1 subgoal (1 total)

`(!f g. MAP (g o f) [] = MAP g (MAP f [])) /\
(!a0 a1.
(!f g. MAP (g o f) a1 = MAP g (MAP f a1))
==> (!f g. MAP (g o f) (CONS a0 a1) = MAP g (MAP f (CONS a0 a1))))`
```
and after getting rid of some trivia:
```  # e(REWRITE_TAC[MAP]);;
val it : goalstack = 1 subgoal (1 total)

`!a0 a1.
(!f g. MAP (g o f) a1 = MAP g (MAP f a1))
==> (!f g.
CONS ((g o f) a0) (MAP (g o f) a1) =
CONS (g (f a0)) (MAP g (MAP f a1)))`
```
we can carefully choose the variable names:
```  # e(MAP_EVERY X_GEN_TAC [`k:A`; `l:A list`]);;
val it : goalstack = 1 subgoal (1 total)

`(!f g. MAP (g o f) l = MAP g (MAP f l))
==> (!f g.
CONS ((g o f) k) (MAP (g o f) l) =
CONS (g (f k)) (MAP g (MAP f l)))`
```
This kind of control can be useful when the sub-proof is more challenging. Here of course the same simple pattern as before works:
```  # e(SIMP_TAC[o_THM]);;
val it : goalstack = No subgoals
```