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 formwhere 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.
!x y . (LENGTH x = LENGTH y) ==> t[x,y]

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

HOL Kananaskis-14