[ringLib] RING_TAC|RULE ported from HOL-Light

[binghe]

Hi,

This PR ports the ring decision procedure (RING_TAC and RING_RULE) from HOL-Light (ringtheory.ml). The ring decision procedure, currently located at examples/algebra/ring/ringLib.sml, can be used to decide equations about ring arithmetics, e.g. (more cases can be found in examples/algebra/ring/selftest.ml):

> RING_RULE “ring_mul r y1 (ring_inv r y1) = ring_1 r /\
        ring_mul r y2 (ring_inv r y2) = ring_1 r /\
        ring_mul r x1 y2 = ring_mul r x2 y1
    ==> ring_mul r x1 (ring_inv r y1) = ring_mul r x2 (ring_inv r y2)”;
[...]
val it =
   |- x1 IN ring_carrier r /\ x2 IN ring_carrier r /\ y1 IN ring_carrier r /\
      y2 IN ring_carrier r /\ ring_inv r y1 IN ring_carrier r /\
      ring_inv r y2 IN ring_carrier r ==>
      ring_mul r y1 (ring_inv r y1) = ring_1 r /\ ring_mul r y2 (ring_inv r y2) = ring_1 r /\
      ring_mul r x1 y2 = ring_mul r x2 y1 ==>
      ring_mul r x1 (ring_inv r y1) = ring_mul r x2 (ring_inv r y2): thm

Notice that, the output theorems contain extra antecedents requiring all involved ring elements are in the carrier. Notice also that the ring decision procedure doesn't know anything of ring_inv (and ring_div, etc.), thus ring_inv r y1 is treated as an atom (that's why ring_inv r y1 IN ring_carrier r is put into the antecedents. The tactic version, RING_TAC, can automatically retrieve the needed antecedents from the assumptions.

This decision procedure can expand the ring expressions as multivariate polynomials (with a default ordering) and sometimes uses Grobner basis algorithm to solve common factors. It accepts input language described in examples/algebra/ring/ringLibScript.sml (ringLibTheory), which is a partial port of HOL-Light's ring theory. This ring theory port is based on HOL4's existing ring theory (now at src/algebra/construction/ringTheory) and theorems can be transported between the two ring theories.

Most number types or number-like objects (e.g. vector and matrix) in HOL4's core library can form a ring (actually mostly a field), and the present ring decision procedure can be later specialized to give a "default" decision procedure for all of them.

P.S. There is a dedicate GROUP_TAC (group decision procedure) in HOL-Light, which may be useful for cryptographic theories in HOL4. And there's also a FIELD_TAC (which understands divisions) in HOL-Light's ringtheory.ml that can be ported (but refined to use dedicated type) to HOL4, in the future.

--Chun

[mn200]

Thanks!