EQ_LENGTH_SNOC_INDUCT_TAC : tactic
STRUCTURE
SYNOPSIS
Performs tactical proof by structural induction on two equal length lists from the tail end.
DESCRIPTION
EQ_LENGTH_SNOC_INDUCT_TAC reduces a goal !x y . (LENGTH x = LENGTH y) ==> t[x,y], where x and y range over lists, to two subgoals corresponding to the base and step cases in a proof by induction on the length of x and y. The induction hypothesis appears among the assumptions of the subgoal for the step case. The specification of EQ_LENGTH_SNOC_INDUCT_TAC is:
     A ?- !x y . (LENGTH x = LENGTH y) ==> t[x,y]
   ================================================  EQ_LENGTH_SNOC_INDUCT_TAC
                            A ?- t[NIL/x][NIL/y]
    A u {{LENGTH x = LENGTH y, t[x'/x, y'/y]}} ?-
         !h h'. t[(SNOC h x)/x, (SNOC h' y)/y]
FAILURE
EQ_LENGTH_SNOC_INDUCT_TAC g fails unless the conclusion of the goal g has the form
   !x y . (LENGTH x = LENGTH y) ==> t[x,y]
where the variables x and y have types (xty)list and (yty)list for some types xty and yty. It also fails if either of the variables x or y appear free in the assumptions.
USES
Use this tactic to perform structural induction on two lists that have identical length.
SEEALSO
HOL  Trindemossen-1