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.