CSE773 Design Verification, Spring 2003

CSE773, Tactics and Interactive Help

You will use these tactics often, I have tried to arrange them in order of frequency of use, so in the first few weeks you will use only the those near the top. But a host of fine TACtics have been developed. If you find that you want to do something that makes sense to you, look for a TACtic to do it.
Prof. Morris has helpful notes on tactics including some he created. They are included in the course directory, /home/ecefac/cse773, in compiled form

GEN_TAC Example Operates on goal. Remove universal quantifiers of a goal
DISCH_TAC Example Move the antecedent of an implicative goal to the assumption list
CONJ_TAC Example Split a conjunctive goal into two separate goals
STRIP_TAC Example Combines CONJ_TAC, GEN_TAC and DISCH_TAC
UNDISCH_TAC: Example Move an assumption to the goal,as antecedent. Takes agrument which is a Term. For example: UNDISCH_TAC (Term `(n:num) < m`) ante_allTacs provides a useful shortcut, with_asm. You provide a list of variables, in order, to identify the assumption to be moved. with_asm "n m" (UNDISCH_TAC o concl)
RES_TAC Example Perform resolution on the assumption list, adding to the assumption list.
ASM_CASES_TAC Example Split the proof into two proofs, with CASE true, and CASE false.
ASM_REWRITE_TAC [] Example Rewrite the goal using the assumption list, and if you include some Theorems in the associated list, use these too.
LEMMA_TAC and LEMMA_MP_TAC Example Split the problem, allowing one to prove a useful lemma to be added to the assumption list, or to the goal as the antecedent of an implication. It is common that you want to prove some smaller fact that will help you in the main proof.
LEMMA_TAC with an argument that is the lemma you want will split the proof, with one goal being the lemma, and the other the original goal. But the second will now have the lemma added to the assumption list.
LEMMA_MP_TAC is the same except that the lemma is added to the goal as an antecedent of an implication with the original goal as conclusion.
REWRITE_TAC [...] The argument is a list of theorems. Example Use the theorems in the list to rewrite the goal.
Very common theorems are ADD_CLAUSES which simplifies things like 0 + x = x and MULT_CLAUSES that simplifies 1 * x = x and 0 * x = 0.
Another common use arises when you wish to rewrite the goal using a particular member of the assumption list.
MATCH_MP_TAC Example A nice one. Suppose you have a theorem that is in the form of an implication: A => B, and suppose your current goal is B. Then it is clear that it is sufficent to prove A. MATCH_MP_TAC does this for you, yielding a new goal, A, that must be proved.
TAUT_TAC Example If the goal is a propositional formula, bool variables and bool operators, TAUT_TAC should solve it, if tautology.
ARITH_TAC Example ARITH_TAC is very good at settling the final issues of an arithmetic proof. It examines the goal which can have equations, inequalities, implications and the like. It attempts to determine if the goal is true. If ARITH_TAC fails, and you think it should not, check whether all the necessary information is in the goal. Sometimes one leaves an important fact on the assumption list.
RW_TAC arith_ss [....] Example There is a 'simpset' built into HOL consisting of a set of simplifying rewrites. So if the goal seems 'easy' sometimes this tactic will solve it. But sometimes it does not solve it, and actually makes the proof more difficult or impossible. In the latter case issue the HOL command b(); to undo the tactic.
Induct is a tactic that transforms the proof into an induction proof requiring you to prove the goal for a base case and also for a step case in order to complete the proof. You will have many induction proofs, but it is worth a little effort to try to avoid them, or minimize the use of Induction by recognizing that previously proven theorems will suffice. The library "arithmetic" is chock full of theorems that were origiannly proven by induction, but we can use them to avoid doing induction. Example
IMP_RES_TAC Theorem, when Theorem is an implication, is equivalent to ASSUME_TAC Theorem THEN RES_TAC. In addition to being a good short cut, the Theorem is does not get added to the assumption list. Big assumption lists are annoying. Example
CR and CRE are similar but often superior to MATCH_MP_TAC since they try to rewrite portions of the goal as well. CR and CRE are included in the file ante_allTacs written by Prof. Morris. It is among the resources provided in the /home/ecefac/cse773 directory.
Use CRE if the goal is an equation, otherwise CR
CR,CRE take an argument that is a theorem, and the theorem is an implication such as A ==>B, and it is hoped that HOL will be able to unify B with the current goal. If it succeeds, then HOL notifies us that it will be sufficient to prove A.
COND_CASES_TAC is a good shortcut. If the goal contains a conditional, COND_CASES_TAC will find it and split the proof for you into the two cases.
EQ_TAC: If goal is A = B, replace by two goals A ==> B, B ==> A
CONV_TAC FORALL_AND_CONV If the goal is !x. A x /\ B x, move !x. inside
CUMUL_CONJ_TAC if goal is A /\ B and you want to use A to help with B
SUBGOAL_THEN Term Thm_Tactic, let us prove Term and then use Term as argument of Thm_Tactic. Keeps assumption list clean.
CONV_TAC CONTRAPOS_CONV. If goal is A ==> B and you prefer ~B ==> ~A
COND_CASES_TAC, if you have a conditional expression in your goal, will find it and figure out how to make two subgoals, without your having to quote a term. *)
BETA_TAC - makes applications of lambda expressions to argements in the goal go away; almost essential to know about if you are going to use lambda (i.e. \) expressions. prove (Term`!n. n Add O = n`, LEMMA_MP_TAC (Term`!n. (\m. m Add O = m) n`) THENL [MATCH_MP_TAC P5 THEN BETA_TAC THEN CONJ_TAC THENL [REWRITE_TAC [Add_def] ,REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [Add_def] ] ,BETA_TAC THEN AR ]);
UNASSUME_TAC Term, can be used to clean up the assumption list UNASSUME_TAC (Term `0LEMMA_TAC (Term`0 < SUC Init`) THENSGS ARITH_TAC THENSGS applies the tactic which follows to the top of the stack Often this solves the goal at the top, so no brackets and indentation is needed.
ARITH_TAC = CONV_TAC ARITH_CONV TRY ARITH_TAC is good when you have several goals, one or more could be solved by ARITH_TAC
To make a copy of an antecedent for example if you have A ==> b as goal you want [A], A ==> B, use DISCH_THEN (fn th=>(ASSUME_TAC th THEN MP_TAC th) (LI>IMP_RES_TAC thm

Other Useful Things:

Use DB.find to look for useful theorems. For example,
DB.find "ADD";
will yield a list of theorems with ADD in the name.
Use help to get assistance. For example,
help "STRIP_TAC";
will yield a list of documentary things about STRIP_TAC

Example of GEN_TAC

 GEN_TAC 
 Often used as the initial step of a proof 
 Remove the universal quantifier in the goal 
 Suppose the goal is to prove associativity of "/\"

         Initial goal:
         !x y z. x /\ y /\ z = (x /\ y) /\ z
Use GEN_TAC         
- e(GEN_TAC);
to obtain
1 subgoal:
> val it =
    !y z. x /\ y /\ z = (x /\ y) /\ z
    
     : goalstack
with universal quantifier x removed.
Use 
e(REPEAT GEN_TAC) to remove them all.
Use
e(GEN_TAC THEN GEN_TAC); to remove two universal quantifiers

Return to index
Return to tactics list

Example of DISCH_TAC

val it =
    (a x ==> b x) /\ ~b x ==> ~a x
    
     : goalstack
- e(DISCH_TAC);
OK..
1 subgoal:
> val it =
    ~a x
    ------------------------------------
      (a x ==> b x) /\ ~b x
     : goalstack

Return to index
Return to tactics list

Example of CONJ_TAC

Set a goal that is an implication and has a conjuctive conclusion
 g(`!(x:num). (a x==> b x) /\ ~b x ==> (~a x /\ ~~~b x)`); 
> val it =
    Proof manager status: 
         
    1. Incomplete:
         Initial goal:
         !x. (a x ==> b x) /\ ~b x ==> ~a x /\ ~~~b x
         
     : proofs
Now peel off universal quantifier and move antecedent to assumption list
- e(GEN_TAC THEN DISCH_TAC);
OK..
Now you have a conjunctive goal and can prove them separately
1 subgoal:
> val it =
    ~a x /\ ~~~b x
    ------------------------------------
      (a x ==> b x) /\ ~b x
     : goalstack
- e(CONJ_TAC);
OK..
2 subgoals:
> val it =
    ~~~b x
    ------------------------------------
      (a x ==> b x) /\ ~b x
    
    ~a x
    ------------------------------------
      (a x ==> b x) /\ ~b x
     : goalstack
This is an example where the "stack" property of the proof environment
can be seen. The original sequent that was on top of the stack
has been replaced by two sequents on the stack

Return to index
Return to tactics list

Example of STRIP_TAC

STRIP TAC is a combination of GEN_TAC, CONJ_TAC and DISCH_TAC

  1. Incomplete:
         Initial goal:
         !x. (a x ==> b x) /\ ~b x ==> ~a x /\ ~~~b x
         
         
     : proofs
- e(REPEAT STRIP_TAC);
OK..
2 subgoals:
> val it =
    F
    ------------------------------------
      0.  a x ==> b x
      1.  ~b x
      2.  ~~b x
    
    F
    ------------------------------------
      0.  a x ==> b x
      1.  ~b x
      2.  a x
     : goalstack

Return to index
Return to tactics list

Example of UNDISCH_TAC

Use UNDISCH_TAC to move an assumption from the assumption list to the goal, as the antecedent of an implication.

You must specify which assumption to move, so the "Term" function is used. It is frequent that you need to specify the types of the variables mentioned in the argument of Term.

val it =
    F
    ------------------------------------
      0.  a x ==> b x
      1.  ~b x
      2.  ~~b x
     : goalstack
- e(UNDISCH_TAC (Term `~~b (x:num)`));
OK..
1 subgoal:
> val it =
    ~~b x ==> F
    ------------------------------------
      0.  a x ==> b x
      1.  ~b x
     : goalstack

Return to index
Return to tactics list

Example of RES_TAC

Used to do resolution on the assumption list, adding results to the assumption list.

    
    F
    ------------------------------------
      0.  a x ==> b x
      1.  ~b x
      2.  a x
     : goalstack
- e(RES_TAC);
OK..
1 subgoal:
> val it =
    F
    ------------------------------------
      0.  a x ==> b x
      1.  ~b x
      2.  a x
      3.  b x
     : goalstack
Notice the assumption list now has both b x and ~ b x 
as elements. RES_TAC will detect this and since the assumption
list is contradictory, it will declare the sequent true.
False implies everything!!!
- e(RES_TAC);
OK..

Goal proved.
 [..] |- F

Goal proved.
 [...] |- F

Return to index
Return to tactics list

Example of ASM_CASES_TAC

Use in cases where you wish to split the proof in two, with some term true in one and false in the other.

val it =
    ~~b x ==> F
    ------------------------------------
      0.  a x ==> b x
      1.  ~b x
     : goalstack
We will split with b x in one part and ~b x in the other.
- e(ASM_CASES_TAC (Term `(b:num->bool) x`));
OK..
2 subgoals:
> val it =
    ~~b x ==> F
    ------------------------------------
      0.  a x ==> b x
      1.  ~b x
      2.  ~b x
    
    ~~b x ==> F
    ------------------------------------
      0.  a x ==> b x
      1.  ~b x
      2.  b x
     : goalstack

Return to index
Return to tactics list

Example of ASM_REWRITE_TAC

Rewrite the goal using equations in the assumption list.

Writing is left to right. If the left side of an equation from the assumption list appears in the goal, then the goal is rewritten with that occurence replaced by the right side of the equation. If you want right to left replacement, use GSYM conversion

ASM_REWRITE_TAC takes an argument that is a list of theorems. Often you don't have any theorems to include so an empty list is the argument.

ASM_REWRITE_TAC []

The above can be replaced by AR, which is less typing, if you have opened ante_allTacs.

val it =
    ~~b x ==> F
    ------------------------------------
      0.  a x ==> b x
      1.  ~b x
     : goalstack
- e(ASM_REWRITE_TAC []);
OK..

Goal proved.
 [.] |- ~~b x ==> F

Goal proved.
 [..] |- F
> val it =
    Initial goal proved.
    |- !x. (a x ==> b x) /\ ~b x ==> ~a x /\ ~~~b x : goalstack

Return to index
Return to tactics list

Example of LEMMA_TAC, LEMMA_MP_TAC
It is common that you want to prove some smaller fact that will help you in the main proof.
LEMMA_TAC with an argument that is the lemma you want will split the proof, with one goal being the lemma, and the other the original goal. But the second will now have the lemma added to the assumption list.
LEMMA_MP_TAC is the same except that the lemma is added to the goal as an antecedent of an implication with the original goal as conclusion.

e(LEMMA_TAC (Term `t0 < (SUC t) + t0`)
Presumably, the term is needed on the assumption list.
e(LEMMA_MP_TAC (Term `t0 < (SUC t) + t0`)
Presumably the term is needed as the antecedent of an implication with the original goal as conclusion. Return to index
Return to tactics list

Example of REWRITE_TAC
Used to rewrite the goal with a theorem. The theorem may be from a library, from the current environment, or from the assumption list.
REWRITE_TAC has an argument thet is a list of theorems. Our examples are from the file "parity.txt" which is part of the class notes.
First example uses a theorem from the local environment, where definitions are given.
Second example uses an assumption.
To select the right assumption use "with_asm" , a function that takes an argument that is a string of space-separated variable names to identify the assumption uniquely, then use another function "ulist" to put the selected assumption in a list, suitable for REWRITE_TAC.

1 subgoal:
> val it =
    PARITY_Design f out ==> PARITY_Spec f out
    
     : goalstack
- e(REWRITE_TAC [PARITY_Design_def, PARITY_Spec_def]);
OK..
1 subgoal:
> val it =
    (?next notgate.
       MULTIPLEXER f notgate out next /\ NOT_gate out notgate /\
       REG next out) ==>
    out 0 /\ !t. out (SUC t) = PARITY (SUC t) f
    
     : goalstack
;
So we see that the definitions of PARITY_Design_def and
PARITY_Spec_def have been used.

Later in the same proof we want to use an assumption for rewriting,
but we want the rewriting to be right to left. Use with_asm to
select the assumption. The "fn th" text captures the assumption
as "th". Then include th in the REWRITE_TAC using GSYM to reverse it.

It would have been a simpler tactic if we had not wanted the reversal.
e(with_asm "out t" (REWRITE_TAC o ulist));
would suffice for rewriting left to right.

> val it =
    (if f (SUC t) then ~PARITY (SUC t) f else PARITY (SUC t) f) =
    PARITY (SUC (SUC t)) f
    ------------------------------------
      0.  !t. next t = (if f t then notgate t else out t)
      1.  !t. notgate t = ~out t
      2.  out 0
      3.  !t. out (SUC t) = next t
      4.  out (SUC t) = PARITY (SUC t) f
     : goalstack
- e(with_asm "out t" (fn th => (REWRITE_TAC [(GSYM th)])));
OK..
1 subgoal:
> val it =
    (if f (SUC t) then ~out (SUC t) else out (SUC t)) =
    PARITY (SUC (SUC t)) f
    ------------------------------------
      0.  !t. next t = (if f t then notgate t else out t)
      1.  !t. notgate t = ~out t
      2.  out 0
      3.  !t. out (SUC t) = next t
      4.  out (SUC t) = PARITY (SUC t) f
     : goalstack

Return to index
Return to tactics list

Example of MATCH_MP_TAC
The theorem MOD_EQ_0 is used. MOD is the usual arithmetic MOD. Notice that MATCH_MP_TAC conveniently discovers the needed value for n.

       Initial goal:
         (x * 6) MOD 6 = 0
     : proofs
- MOD_EQ_0;
> val it = |- !n. 0 < n ==> !k. (k * n) MOD n = 0 : thm
- e(MATCH_MP_TAC MOD_EQ_0);
OK..
1 subgoal:
> val it =
    0 < 6

Return to index
Return to tactics list

Example of TAUT_TAC A good tautology checker.

       Initial goal:
         !a b c. (a \/ b) /\ (c \/ ~b) ==> a \/ c
         
         
     : proofs
- e(TAUT_TAC);
OK..
> val it =
    Initial goal proved.
    |- !a b c. (a \/ b) /\ (c \/ ~b) ==> a \/ c : goalstack

Return to index
Return to tactics list

Example of ARITH_TAC A good arithmetic expression checker.

1 subgoal:
> val it =
    (2 ** n - 1 + 1 = 2 ** n) ==> (2 * 2 ** n - 1 + 1 = 2 * 2 ** n)
    
     : goalstack
- e(ARITH_TAC);
OK..

Goal proved.
|- (2 ** n - 1 + 1 = 2 ** n) ==> (2 * 2 ** n - 1 + 1 = 2 * 2 ** n)

Return to index
Return to tactics list

Example of RW_TAC arith_ss []
Good at simplifying the goal, but not always!
In the example arith_ss detects that i<0 must be false, so it simplifies the goal.

  
    (!i. i < 0 ==> ~g i) = (0 = Val 0 g)
    
     : goalstack
- e(RW_TAC arith_ss []);
OK..
1 subgoal:
> val it =
    0 = Val 0 g
    
     : goalstack

Return to index
Return to tactics list

Induction Example The example is from the parity proof included in the class notes. We are seeking to prove that the PARITY_Design satisfies the PARITY_Spec for all n. So we use induction and prove it true for (n=0) and then prove it true for (SUC n) given that it is true for n.

> val it =
    !t. out (SUC t) = PARITY (SUC t) f
    ------------------------------------
      0.  !t. next t = (if f t then notgate t else out t)
      1.  !t. notgate t = ~out t
      2.  out 0
      3.  !t. out (SUC t) = next t
     : goalstack
- e(Induct);
OK..
2 subgoals:
> val it =
    out (SUC (SUC t)) = PARITY (SUC (SUC t)) f
    ------------------------------------
      0.  !t. next t = (if f t then notgate t else out t)
      1.  !t. notgate t = ~out t
      2.  out 0
      3.  !t. out (SUC t) = next t
      4.  out (SUC t) = PARITY (SUC t) f
    
    out (SUC 0) = PARITY (SUC 0) f
    ------------------------------------
      0.  !t. next t = (if f t then notgate t else out t)
      1.  !t. notgate t = ~out t
      2.  out 0
      3.  !t. out (SUC t) = next t
     : goalstack

Return to index
Return to tactics list

IMP_RES_TAC Example This is from our original example, design of a parity network

    !t. out (SUC t) = (if f t then ~out t else out t)
    ------------------------------------
      0.  PARITY_Design f out
      1.  out 0
     : goalstack
- PARITY_Design_Implies;
> val it =
    |- !f out.
         PARITY_Design f out ==>
         !t. out (SUC t) = (if f t then ~out t else out t) : thm
- e(IMP_RES_TAC PARITY_Design_Implies );
OK..

Goal proved.
 [.] |- !t. out (SUC t) = (if f t then ~out t else out t)