Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
Date: Fri, 1 Nov 91 13:26:07 MST
From: graham@ca.ucalgary.cpsc (Graham Birtwistle)
Message-Id: <9111012026.AA08557@fsa.cpsc.ucalgary.ca>
To: info-hol@edu.uidaho.cs.ted

Let me make the initial point that I am not a HOL wizard.
I would like clean proof styles and "readable" proofs
that others can pick through and understand.

Here are some observations from that standpoint.

I think it good practice to write proofs that do
not depend in any way upon the order of assumptions,
i.e. will still hold good when  the next release of HOL
comes out.

 That means POP_ASSUM and FIRST_ASSUM are out. Period.
There are two tricks to learn:
  how to name and use just one assumption
  how to name and use just several assumptions


           ONE ASSUMPTION AT A TIME

Lift a copy out with ASSUME as below (in a rather boring lemma I
needed to prove an adder).

I prefer to use let and work bottom up
(it makes it easier to step through the proof afterwards,
should one wish to do so).
The let style has also encouraged me to lift what
I need off the assumption list and "keep it in hand".
whilst massaging it into shape.
I note that several HOL people pop assumptions,
massage them, and then push them back on the assumption
list. And then repeat several times. There is no
need to do that --- the ML host is very helpful here.

let case4 = prove
  (" ! x .
      (abc < (2 EXP (SUC(SUC n))))
      ==> ((~(abc < (2 EXP SUC n))))
      ==> ((((~x) /\ (val s n = abc - (2 EXP (SUC n)))))
           = (val s n + ((2 EXP (SUC n))*(bv x)) = abc - (2 EXP (SUC n))))",
    REPEAT GEN_TAC THEN REPEAT STRIP_TAC
    THEN BOOL_CASES_TAC "x:bool"
    THEN REWRITE_TAC [ bvals; MULT_CLAUSES; ADD_CLAUSES ]
    THEN
      let th1 = SPECL [ "val s n + (2 EXP (SUC n))";
                        "abc - (2 EXP (SUC n))";
                        "2 EXP (SUC n)"
                      ] (SYM_RULE EQ_MONO_ADD_EQ)

      in PURE_ONCE_REWRITE_TAC [ th1 ]
    THEN MAP_EVERY IMP_RES_TAC [ NOT_LESS; SUB_ADD ]
    THEN ASM_REWRITE_TAC
       (map SYM_RULE [ ADD_ASSOC; exp_doubles ])
    THEN
      let th2 = ASSUME "abc<2 EXP (SUC(SUC n))"        in       <<===== here we go
      let th3 = MATCH_MP lss_lss_add th2               in
      let th4 = PURE_ONCE_REWRITE_RULE [ ADD_SYM ] th3 in
      let th5 = SYM_RULE (MATCH_MP LESS_NOT_EQ th4)    in
        MATCH_ACCEPT_TAC th5
   );;


        MORE THAN ONE ASSUMPTION AT A TIME

We can pick them all up with ASSUM_LIST or just
a few with FILTER_ASM. Here is a little example
from an ALU proof that uses them both.

Given the goal

"(nEql s(nXor f g)n /\ (s(SUC n) = ~(f(SUC n) = g(SUC n)))) /\ ~c"
    [ "!f g s c.
        (?a b. (nEql a f n /\ nEql b g n) /\ nEql s(nXor a b)n /\ ~c) =
        nEql s(nXor f g)n /\ ~c" ]
    [ "nEql a f n" ]
    [ "a(SUC n) = f(SUC n)" ]
    [ "nEql b g n" ]
    [ "b(SUC n) = g(SUC n)" ]
    [ "nEql s(nXor a b)n" ]
    [ "s(SUC n) = ~(a(SUC n) = b(SUC n))" ]
    [ "~c" ]

() : void

rewriting with ASM_REWRITE_TAC is too powerful (try it).
We can filter out just the equalities (there are 3).

#e(FILTER_ASM_REWRITE_TAC is_eq []);;
OK..
"nEql s(nXor f g)n /\ ~c"
    [ "!f g s c.
        (?a b. (nEql a f n /\ nEql b g n) /\ nEql s(nXor a b)n /\ ~c) =
        nEql s(nXor f g)n /\ ~c" ]
    [ "nEql a f n" ]
    [ "a(SUC n) = f(SUC n)" ]
    [ "nEql b g n" ]
    [ "b(SUC n) = g(SUC n)" ]
    [ "nEql s(nXor a b)n" ]
    [ "s(SUC n) = ~(a(SUC n) = b(SUC n))" ]
    [ "~c" ]

() : void

Just to be different, we  now pick up the "longest" assumption,
turn it round  with ASSUM_LIST which is more basic than FILTER_ASM,
and more useful once you have mastered it.

#e(ASSUM_LIST ( PURE_ONCE_REWRITE_TAC
              o (map SYM_RULE)
              o (filter (is_forall o concl))     <<==== note we must use concl with ASSUM_LIST
              ));;
OK..
"?a b. (nEql a f n /\ nEql b g n) /\ nEql s(nXor a b)n /\ ~c"
    [ "!f g s c.
        (?a b. (nEql a f n /\ nEql b g n) /\ nEql s(nXor a b)n /\ ~c) =
        nEql s(nXor f g)n /\ ~c" ]
    [ "nEql a f n" ]
    [ "a(SUC n) = f(SUC n)" ]
    [ "nEql b g n" ]
    [ "b(SUC n) = g(SUC n)" ]
    [ "nEql s(nXor a b)n" ]
    [ "s(SUC n) = ~(a(SUC n) = b(SUC n))" ]
    [ "~c" ]

() : void

Here is how ASSUM_LIST  works in mini-stages:

e(ASSUM_LIST ( PURE_ONCE_REWRITE_TAC
              o (map SYM_RULE)
              o (filter (is_forall o concl))
              ));;
---> ASSUM_LIST ( PURE_ONCE_REWRITE_TAC
                o (map SYM_RULE)
                o (filter (is_forall o concl))
                ) (asm, C)                                                    <<=== e picks up the goal
---> PURE_ONCE_REWRITE_TAC
       (map SYM_RULE (filter (is_forall o concl)) (map ASSUME asm)) (asm, C)  <<=== effect of ASSUM_LIST
---> PURE_ONCE_REWRITE_TAC
       (map SYM_RULE [ |- ! f g s c . lhs = C ]) (asm, C)                     <<=== filtering done
---> PURE_ONCE_REWRITE_TAC [ |- ! f g s c . C = lhs ] (asm, C)                <<=== SYMed
---> (asm, lhs)

Note my inconsistency here.
I did not use let's in the application of ASSUM_LIST.
Oh, the perils of pedagogy.

Does this look better?

  ASSUM_LIST (\ g . let L1 = filter (is_forall o concl) g in
                    let L2 = map SYM_RULE  L1             in
                      PURE_ONCE_REWRITE_TAC L2);;


Take your pick.

In summary,
  if you want one assumption ASSUME it.
  if you want several, take the lot and filter them
                       via FILTER_ASM or via ASSUM_LIST

Do not use POP_ASSUM and do not use FIRST_ASSUM. Ever.

Yours,

    Graham Birtwistle
    Calgary