BINOP_TAC : tactic

SYNOPSIS
Breaks apart equation between binary operator applications into equality between their arguments.

DESCRIPTION
Given a goal whose conclusion is an equation between applications of the same curried binary function f, the tactic BINOP_TAC breaks it down to two subgoals expressing equality of the corresponding arguments:
       A ?- f x1 y1 = f x2 y2
   ================================  BINOP_TAC
      A ?- x1 = x2    A ?- y1 = y2

FAILURE CONDITIONS
Fails if the conclusion of the goal is not an equation between applications of the same curried binary operator.

EXAMPLE
We can set up the following goal which is an equation between applications of the binary operator +:
  # g `f(2 * x + 1) + w * z = f(SUC(x + 1) * 2 - 1) + z * w`;;
and it is simplest to prove if we split it up into two subgoals:
  # e BINOP_TAC;;
  val it : goalstack = 2 subgoals (2 total)

  `w * z = z * w`

  `f (2 * x + 1) = f (SUC (x + 1) * 2 - 1)`
the first of which can be solved by ARITH_TAC, and the second by AP_TERM_TAC THEN ARITH_TAC.

SEE ALSO
ABS_TAC, AP_TERM_TAC, AP_THM_TAC, MK_BINOP, MK_COMB_TAC.