Changed title: `rw` doesn't create abbreviations as in `RW_TAC`

[binghe]

Hi,

From the implementation of rw in bossLib (and then BasicProvers) it looks that, roughly, rw = RW_TAC (srw_ss()) but in my practice I found rw doesn't do LET-elimination as RW_TAC can do.

If you go to the first theorem in examples/lambda/barendregt/boehmScript.sml:

Theorem BT_generator_of_hnf :
    !X M r. FINITE X /\ hnf M ==>
            BT_generator X (M,r) =
           (let
             n = LAMl_size M;
             vs = RNEWS r n X;
             M1 = principal_hnf (M @* MAP VAR vs);
             Ms = hnf_children M1;
             y = hnf_headvar M1;
             l = MAP (\e. (e,SUC r)) Ms
           in
             (SOME (vs,y),fromList l))
Proof
    ...
QED

At the beginning, the goal status is this:

   Proof manager status: 1 proof.
   1. Incomplete goalstack:
        Initial goal:
        !X M r.
          FINITE X /\ hnf M ==>
          BT_generator X (M,r) =
          (let
             n = LAMl_size M;
             vs = RNEWS r n X;
             M1 = principal_hnf (M @* MAP VAR vs);
             Ms = hnf_children M1;
             y = hnf_headvar M1;
             l = MAP (\e. (e,SUC r)) Ms
           in
             (SOME (vs,y),fromList l))
   : proofs

Below is the (desired) result of applying RW_TAC std_ss []:

    0.  FINITE X
    1.  hnf M
    2.  Abbrev (n = LAMl_size M)
    3.  Abbrev (vs = RNEWS r n X)
    4.  Abbrev (M1 = principal_hnf (M @* MAP VAR vs))
    5.  Abbrev (y = hnf_headvar M1)
    6.  Abbrev (Ms = hnf_children M1)
    7.  Abbrev (l = MAP (\e. (e,SUC r)) Ms)
   ------------------------------------
        BT_generator X (M,r) = (SOME (vs,y),fromList l)

As you can see, each LET-binding now becomes an abbreviation. And if I use RW_TAC (srw_ss()) [] instead, the result is the same (because no automatic simplification rule is triggered).

But if I use rw [] instead, I only get this (no more abbreviations!):

    0.  FINITE X
    1.  hnf M
   ------------------------------------
        BT_generator X (M,r) =
        (SOME
           (RNEWS r (LAMl_size M) X,
            hnf_headvar
              (principal_hnf (M @* MAP VAR (RNEWS r (LAMl_size M) X)))),
         fromList
           (MAP (\e. (e,SUC r))
              (hnf_children
                 (principal_hnf (M @* MAP VAR (RNEWS r (LAMl_size M) X))))))

Basically I never observed rw can do LET-elimination, and whenever I need it I always call RW_TAC in my proofs. Is there any explanation here?

--Chun

[binghe]

Hmmm, maybe I wrongly blamed LET_ELIM_TAC code. The result after rw [] looks like LET_ELIM has already been applied - all the LET-bindings are indeed eliminated. What's really unexpected is the missing of abbreviation creation.