[Hol-info] Procedure for equations with addition and multiplication

[Michael N. <Mic...@ni...>]

Alexey Gotsman writes:
 
> Does anyone know if there is a procedure in HOL for proving simple
> statements about equations with addition and multiplication like the
> following one?
 
> (e*bv_c+e*(2*bv_cout+wb_sum)+wbs_sum=bv_cin+e*(bv_c+wb_a+wb_b)+wbs_a+wbs_b) 
> ==>        (2*e*bv_cout+e*wb_sum+wbs_sum=bv_cin+e*wb_a+e*wb_b+wbs_a+wbs_b)
 
> Unfortunately, PROVE_TAC and RW_TAC arith_ss [] don't do the job.
 
You don't say what the type of your variables is, but if they are
either integers or nats, then rewriting with distributivity (that is,
either arithmeticTheory.LEFT_ADD_DISTRIB, or
integerTheory.INT_LDISTRIB), and then using intLib.ARITH_CONV solves
this goal.

val t = (* 2n below forces terms to be natural numbers *)
 ``(e*bv_c+e*(2*bv_cout+wb_sum)+wbs_sum=bv_cin+e*(bv_c+wb_a+wb_b)+wbs_a+wbs_b) 
    ==> (2n*e*bv_cout+e*wb_sum+wbs_sum=bv_cin+e*wb_a+e*wb_b+wbs_a+wbs_b)``;
> val t =
    ``(e * bv_c + e * (2 * bv_cout + wb_sum) + wbs_sum =
       bv_cin + e * (bv_c + wb_a + wb_b) + wbs_a + wbs_b) ==>
      (2 * e * bv_cout + e * wb_sum + wbs_sum =
       bv_cin + e * wb_a + e * wb_b + wbs_a + wbs_b)`` : term

- (REWRITE_CONV [arithmeticTheory.LEFT_ADD_DISTRIB] THENC intLib.ARITH_CONV) t;
> val it =
    |- (e * bv_c + e * (2 * bv_cout + wb_sum) + wbs_sum =
        bv_cin + e * (bv_c + wb_a + wb_b) + wbs_a + wbs_b) ==>
       (2 * e * bv_cout + e * wb_sum + wbs_sum =
        bv_cin + e * wb_a + e * wb_b + wbs_a + wbs_b) =
       T : thm

I'm not sure why ARITH_CONV in intLib does not apply distributivity
itself (my initial reaction says this is a bug, and that
intLib.ARITH_CONV (intLib.ARITH_TAC when applied to a goal) should
suffice).

The reason intLib gets this, and numLib.ARITH_CONV does not is that
intLib normalises products before then generalising them as
variables.  numLib probably should do the same.

Michael.