[BasicProvers] avoid CONJ_TAC in LET_ELIM_TAC

[binghe]

Hi,

Per our (offline) discussion, this PR makes LET_ELIM_TAC (part of RW_TAC, no documentation) more useful by not breaking the current conjuncted goal. The behavior of RW_TAC, which contains LET_ELIM_TAC, is not changed, because RW_TAC will do STRIP_TAC (which contains CONJ_TAC) after calling LET_ELIM_TAC.

For example, suppose I have the following theorem in the middle of its proof:

        (let
           M0 = principle_hnf M;
           N0 = principle_hnf N;
           n = LAMl_size M0;
           n' = LAMl_size N0;
           vs = FRESH_list (MAX n n') (FV M UNION FV N);
           vsM = TAKE n vs;
           vsN = TAKE n' vs;
           M1 = principle_hnf (M0 @* MAP VAR vsM);
           N1 = principle_hnf (N0 @* MAP VAR vsN);
           y = hnf_head M1;
           y' = hnf_head N1;
           m = LENGTH (hnf_children M1);
           m' = LENGTH (hnf_children N1)
         in
           y = y' /\ n + m' = n' + m) /\
        !P Q. ?pi. Boehm_transform pi /\ apply pi M == P /\ apply pi N == Q
   ------------------------------------
    0.  solvable M
    1.  solvable N
    2.  LAMl_size (principle_hnf M) <= LAMl_size (principle_hnf N)

I want to have all LET variables converted to abbreviations, while still keeping the single conjuncted goal not broken into subgoals (because there are still shared tactics to execute). But either RW_TAC or LET_ELIM_TAC cannot do this job, as they both do STRIP_TAC internally.

Now the new LET_ELIM_TAC produces what I needed:

> e LET_ELIM_TAC;
OK..
1 subgoal:
val it =

        (y = y' /\ n + m' = n' + m) /\
        !P Q. ?pi. Boehm_transform pi /\ apply pi M == P /\ apply pi N == Q
   ------------------------------------
    0.  solvable M
    1.  solvable N
    2.  n <= n'
    3.  Abbrev (M0 = principle_hnf M)
    4.  Abbrev (N0 = principle_hnf N)
    5.  Abbrev (n' = LAMl_size N0)
    6.  Abbrev (n = LAMl_size M0)
    7.  Abbrev (vs = FRESH_list (MAX n n') (FV M UNION FV N))
    8.  Abbrev (vsN = TAKE n' vs)
    9.  Abbrev (vsM = TAKE n vs)
   10.  Abbrev (N1 = principle_hnf (N0 @* MAP VAR vsN))
   11.  Abbrev (M1 = principle_hnf (M0 @* MAP VAR vsM))
   12.  Abbrev (m' = LENGTH (hnf_children N1))
   13.  Abbrev (m = LENGTH (hnf_children M1))
   14.  Abbrev (y' = hnf_head N1)
   15.  Abbrev (y = hnf_head M1)

The core library can still be built. Let's see how the docker CI build goes.

--Chun

[binghe]

By the way, it's confirmed that even the new LET_ELIM_TAC cannot deal with LETs hidden inside existential quantifiers, which can be handled by UNBETA_TAC.

[binghe]

Some examples are broken, I will fix them.

[binghe]

In examples/algebra/lib/helperScript.sml, I meet the following proof goal:

val it =
   Proof manager status: 1 proof.
   1. Incomplete goalstack:
        Initial goal:
        !s. FINITE s ==>
            !P. (let
                   u = {x | x IN s /\ P x};
                   v = {x | x IN s /\ ~P x}
                 in
                   FINITE u /\ FINITE v /\ s =|= u # v)
   : proofs
> val it = (): unit

And after rw_tac std_ss[], the conjunctions FINITE u /\ FINITE v /\ s =|= u # v inside let is not stripped:

1 subgoal:
val it =

        FINITE u /\ FINITE v /\ s =|= u # v
   ------------------------------------
    0.  FINITE s
    1.  Abbrev (u = {x | x IN s /\ P x})
    2.  Abbrev (v = {x | x IN s /\ ~P x})

   : proof

It seems that the other STRIP_TAC inside RW_TAC does not touch conjunctions inside let, and the CONJ_TAC I removed, has caused the present issue.

I'm going to close this PR. (My other proofs do not rely on the changed LET_ELIM_TAC)