EQ_LENGTH_SNOC_INDUCT_TAC

listLib.EQ_LENGTH_SNOC_INDUCT_TAC : tactic

Performs tactical proof by structural induction on two equal length lists from the tail end.

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.

Use this tactic to perform structural induction on two lists that have identical length.

See also

listLib.EQ_LENGTH_INDUCT_TAC, listLib.LIST_INDUCT_TAC, listLib.SNOC_INDUCT_TAC