(* file: tactic_n2.txt; author: L. Morris 10/25/01, revised 1/8/03, 1/14/03
   for CSE 773 Spring 2003 *)

  (* More notes on tactics and related ML functions provided by HOL. *)

loadPath := "/home/ecefac/cse773" :: !loadPath; (* get at ante_allTacs *)
load "bossLib"; open bossLib;
load "ante_allTacs"; open ante_allTacs;
load "numLib"; open arithmeticTheory prim_recTheory numTheory numLib;
load "listTheory"; open listTheory;
load "tautLib"; open tautLib;

(* This note is intended to mention a few more tactics and other functions
 which were omitted from my first note (the file tactic_n1.txt) on the
 subject, and which Prof. Stabler or I think should be particularly called
 to your attention. More realistic examples of use should be added;
 contributions will be gratefully received. *)

(* impOfEqn, impByOfEqn: These two oddly-named thm->thm functions were put
 into ante_allTacs because MATCH_MP_TAC, CRE, and CR are so useful that one
 often would like to turn an equivalence (i.e., an equation of type bool,
 possibly with hypotheses and/or universal quantifiers) into an implication
 just so as to be able to use one of those thm_tactics. impOfEqn, short for
 "implication of (boolean) equation" will pick out the forward direction
 of implication from a (conditional) equivalence, putting back all the
 hypotheses and quantifiers just as it found them; conversely impByOfEqn
 ("is-implied-by of equation") picks out the right-to-left implication.

 IMP_RES_TAC, if you give it a (conditional) equivalence, uses both
 directions of implication, which is often the cause of generating
 a lot of unwanted assumptions; IMP_RES_TAC (impOfEqn some_theorem)
 is a useful idiom to remember to avoid some of the garbage. *)

 (* There is also symOfEqn, which reverses precisely the main-connective
  = at the bottom of a nest of universal quantifiers and implicative
  hypotheses; almost always GSYM will do what you want, but if there
  are ever other equations, say in the hypotheses of a theorem, that
  you don't want to reverse, you might want to use symOfEqn *)

EQ_SYM_EQ;  (* val it = |- !x y. (x = y) = (y = x) : thm *)

(GSYM EQ_SYM_EQ, symOfEqn EQ_SYM_EQ,
 GSYM (impOfEqn EQ_SYM_EQ), symOfEqn (impOfEqn EQ_SYM_EQ));

(*  (|- !x y. (y = x) = (x = y), |- !x y. (y = x) = (x = y),
     |- !x y. (y = x) ==> (x = y), |- !x y. (x = y) ==> (x = y))
    : thm * thm * thm * thm  *)  (* not useful examples *)

(* Throwing away unwanted assumptions. *)

(* If you can identify an assumption uniquely by the string consisting
 of its occurrences of vaiable names from left to right, you can get rid
 of it with drop_asm "<sequence of enough variable names>" . Actual
 example from tactic_n1.txt:  *)

g`(m + 1 = n) ==> (f (m + n) = f (2 * m + 1))`;
e(DISCH_TAC THEN IMP_RES_TAC EQ_SYM_EQ);
(*1 subgoal:

    f (m + n) = f (2 * m + 1)
    ------------------------------------
      0.  m + 1 = n
      1.  n = m + 1   *)

e(drop_asm "m");  (* or e(drop_asm "m n"); would do the same *)

(*1 subgoal:

    f (m + n) = f (2 * m + 1)
    ------------------------------------
      n = m + 1  *)

(*  You do need to be able to distinguish constants from variables.

 That example was done in the notes so that e(AR); would not loop forever;
 there are many other good reasons to throw assumptions away, but drop_asm
 is mentioned here mainly as an easy introduction to the assumption-
 identification-by-a-string-of-variables technique. The same method will
 do a lot more for you used with

 with_asm "<string to identify an assumption>" (some thm_tactic). *)

b();  (*  f (m + n) = f (2 * m + 1)
      ------------------------------------
      0.  m + 1 = n
      1.  n = m + 1  *)

(* Cleverer would be to do just what we do want to do with the assumption
 we like: *)

e(with_asm "n" SUBST1_TAC);

(*    f (m + (m + 1)) = f (2 * m + 1)
    ------------------------------------
      0.  m + 1 = n
      1.  n = m + 1  *)

(* SUBST1_TAC works when the selected assumption is a bare equation, and
 you just want to replace occurrences of its left side by its right side.
 More general, because it can use a quantified assumption, and look for
 instances of its left-hand side, is (equivalent in this example): *)

b();
e(with_asm "n" (REWRITE_TAC o ulist));  (* same result as before *)

(* In this example, we only have two assumptions because of having used
 IMP_RES_TAC unwisely. Let's start over: *)

restart();  (*    Initial goal: *)
    
(*    (m + 1 = n) ==> (f (m + n) = f (2 * m + 1))  *)

e(DISCH_TAC THEN with_asm "" (SUBST1_TAC o SYM));

(*    f (m + (m + 1)) = f (2 * m + 1)
    ------------------------------------
      m + 1 = n  *)

(* and then you may observe, as in the previous notes, that

restart();
e(DISCH_THEN (SUBST1_TAC o SYM));

is the really slick way to do this example; however, my purpose here is to
advertise with_asm. *)

(* Cases: bossLib offers, for every kind of type it understands - notably
 including num and <anything> list - not only Induct, which will set you
 up to do proof by induction over the outermost universally quantified
 variable of your goal, but also Cases, which in case you don't want to
 start another induction, but just want to make a case split, as for
 an inductive proof, over the outermost universally quantified variable,
 will do exactly what you want. What could be a realistic example: Suppose
 we know about the definitions of MAP and LENGTH: *)

drop();

MAP;

(* |- (!f. MAP f [] = []) /\ !f h t. MAP f (h::t) = f h::MAP f t : thm *)

LENGTH;

(* |- (LENGTH [] = 0) /\ !h t. LENGTH (h::t) = SUC (LENGTH t) : thm *)

(* and we might want to prove that MAP is LENGTH-preserving, in the form:*)

g`!(l1:'a list) (l2:'b list) f. (MAP f l1 = l2) ==>
                                                 (LENGTH l1 = LENGTH l2)`;
e(Induct THEN REWRITE_TAC [LENGTH, MAP]);

(*2 subgoals:

    !h l2 f. (f h::MAP f l1 = l2) ==> (SUC (LENGTH l1) = LENGTH l2)
    ------------------------------------
      !l2 f. (MAP f l1 = l2) ==> (LENGTH l1 = LENGTH l2)
    
    !l2. ([] = l2) ==> (0 = LENGTH l2)  *)

(* There are lots of ways to solve the base case, but the point here is
 to demonstrate Cases: *)

e(Cases);

(* 2 subgoals:  (of the base case)

    ([] = h::t) ==> (0 = LENGTH (h::t))
    
    
    ([] = []) ==> (0 = LENGTH [])  *)

b(); (* so easy we'll knock it off at one blow: *)
e(Cases THEN REWRITE_TAC [LENGTH, NOT_NIL_CONS]);

(* (NOT_NIL_CONS is  |- !a1 a0. ~([] = a0::a1) : thm.)
Goal proved.
|- !l2. ([] = l2) ==> (0 = LENGTH l2)

Remaining subgoals:

    !h l2 f. (f h::MAP f l1 = l2) ==> (SUC (LENGTH l1) = LENGTH l2)
    ------------------------------------
      !l2 f. (MAP f l1 = l2) ==> (LENGTH l1 = LENGTH l2)  *)

(* Note that in the case of l1 being non-null, Cases has invented new
 names h and l1 (not the original l1, which has disappeared) of which
 the original l1 was the CONS. *)

(* h and f are not interesting for this proof; l2 is: *)

e(GEN_TAC THEN Cases THEN GEN_TAC THEN REWRITE_TAC [LENGTH]);

(*2 subgoals:

    (f h::MAP f l1 = h'::t) ==> (SUC (LENGTH l1) = SUC (LENGTH t))
    ------------------------------------
      !l2 f. (MAP f l1 = l2) ==> (LENGTH l1 = LENGTH l2)
    
    (f h::MAP f l1 = []) ==> (SUC (LENGTH l1) = 0)
    ------------------------------------
      !l2 f. (MAP f l1 = l2) ==> (LENGTH l1 = LENGTH l2)  *)

(* The first subgoal is very easy, once we realize that because
 NOT_NIL_CONS is the negation of an equation, we need to match the
 whole equation, not just one side: *)

e(REWRITE_TAC [GSYM NOT_NIL_CONS]);

(* Goal proved. |- (f h::MAP f l1 = []) ==> (SUC (LENGTH l1) = 0)

Remaining subgoals:

    (f h::MAP f l1 = h'::t) ==> (SUC (LENGTH l1) = SUC (LENGTH t))
    ------------------------------------
      !l2 f. (MAP f l1 = l2) ==> (LENGTH l1 = LENGTH l2)  *)

(* Here is the one serious subgoal; it is helpful to hunt up the theorem
 list_11 (meaning that the constructor CONS (i.e., ::) is one-to-one): *)

list_11;

(* val it = |- !a0 a1 a0' a1'.
                (a0::a1 = a0'::a1') = (a0 = a0') /\ (a1 = a1')  *)

(* This makes a typical opportunity to use DISCH_THEN with a thm_tactic: *)

e(DISCH_THEN (STRIP_ASSUME_TAC o REWRITE_RULE [list_11]));

(* 1 subgoal:

    SUC (LENGTH l1) = SUC (LENGTH t)
    ------------------------------------
      0.  !l2 f. (MAP f l1 = l2) ==> (LENGTH l1 = LENGTH l2)
      1.  f h = h'
      2.  MAP f l1 = t  *)

(* Now it's obvious what to do: *)

e(RES_TAC THEN AR);

(*    Initial goal proved.
    |- !l1 l2 f. (MAP f l1 = l2) ==> (LENGTH l1 = LENGTH l2) *)

(* Sometimes the expression we want to make cases over is not a
 universally quantified variable; so it is good to know how to get
 similar results "by hand" to what Cases gives us.  Cases's justification
 comes (I am fairly sure) from the "_CASES" theorem which is automatically
 proved for every recursively defined data type; the following are two
 everyone should be well acquainted with: *)

num_CASES;

(* val it = |- !m. (m = 0) \/ ?n. m = SUC n : thm *)

list_CASES;

(* val it = |- !l. (l = []) \/ ?t h. l = h::t : thm *)

(* Note that, under their universal quantifications, these theorems are
 disjunctions; they provide a wonderful opportunity to use a HOL function
 called DISJ_CASES_THEN2 which may seem slightly exotic at first, as its
 type is thm_tactic -> thm_tactic -> thm_tactic. (And recall thm_tactic
 is the function type thm -> tactic.)

 DISJ_CASES_THEN2 embodies the principle: "If A \/ B is a theorem, and
 if you could prove your goal supposing A were true, and on the other
 hand you could prove your goal supposing B were true, then you
 can prove your goal."

 Let's demonstrate on the inductive step of the example we just proved: *)

restart();

(*  Initial goal:
    
    !l1 l2 f. (MAP f l1 = l2) ==> (LENGTH l1 = LENGTH l2) *)

e(Induct THEN REWRITE_TAC [LENGTH, MAP]);
e(Cases THEN REWRITE_TAC [LENGTH, NOT_NIL_CONS]);

(* Remaining subgoals:

    !h l2 f. (f h::MAP f l1 = l2) ==> (SUC (LENGTH l1) = LENGTH l2)
    ------------------------------------
      !l2 f. (MAP f l1 = l2) ==> (LENGTH l1 = LENGTH l2)  *)

(* Let's say, out of habit, we strip all the variables off next: *)

e(REPEAT GEN_TAC);

(* 1 subgoal:

    (f h::MAP f l1 = l2) ==> (SUC (LENGTH l1) = LENGTH l2)
    ------------------------------------
      !l2 f. (MAP f l1 = l2) ==> (LENGTH l1 = LENGTH l2)  *)

(* Now we decide we want to argue by cases on whether l2 is [] or not: *)

(* And here I offer a general suggestion that helps me a lot: whenever
 I am puzzling out how to use some fancy piece of machinery that wants
 a thm-tactic as an argument or arguments, I try it out first with
 MP_TAC as the supplied thm_tactic; whatever theorem MP_TAC turns out to
 be given will show up as a new hypothesis of the goal, so I will know what
 it was, and if it would work for what I really wanted to do with it. *)

(* Remember we have to specialize list_CASES, and because the goal as I
 stated it had type variables in the types, we need ISPEC, not SPEC. *)

e(DISJ_CASES_THEN2 MP_TAC MP_TAC (ISPEC (Term`l2:'b list`) list_CASES));

(* 2 subgoals:

    (?t h. l2 = h::t) ==>
    (f h::MAP f l1 = l2) ==>
    (SUC (LENGTH l1) = LENGTH l2)
    ------------------------------------
      !l2 f. (MAP f l1 = l2) ==> (LENGTH l1 = LENGTH l2)
    
    (l2 = []) ==> (f h::MAP f l1 = l2) ==> (SUC (LENGTH l1) = LENGTH l2)
    ------------------------------------
      !l2 f. (MAP f l1 = l2) ==> (LENGTH l1 = LENGTH l2) *)

(* "l2 = []" certainly makes sense as one case; and note that the other
 case gives us two existentially quantified variables that we could
 use STRIP_ASSUME_TAC to turn into constants - I suspect that is just
 what Cases does.

 It looks as if plausible thm_tactics to use are SUBST1_TAC with the
 first subgoal and STRIP_ASSUME_TAC with the second; let's try: *)

b(); (* undo DISJ_CASES_THEN2 MP_TAC MP_TAC ... *)
e(DISJ_CASES_THEN2
   SUBST1_TAC
   STRIP_ASSUME_TAC
   (ISPEC (Term`l2:'b list`) list_CASES));

(* As before, use NOT_NIL_CONS on the easy case. *)

e(REWRITE_TAC [GSYM NOT_NIL_CONS]);  (* Goal proved. *)

(* and, for the other subgoal, rewriting with our stripped assumption about
 l2 should get us almost back to where we were with the Cases proof: *)

e(AR THEN DISCH_THEN (STRIP_ASSUME_TAC o REWRITE_RULE [list_11]));

(* 1 subgoal:

    SUC (LENGTH l1) = LENGTH (h'::t)
    ------------------------------------
      0.  !l2 f. (MAP f l1 = l2) ==> (LENGTH l1 = LENGTH l2)
      1.  l2 = h'::t
      2.  f h = h'
      3.  MAP f l1 = t  *)

e(RES_TAC THEN ASM_REWRITE_TAC [LENGTH]);

(*  Initial goal proved.
    |- !l1 l2 f. (MAP f l1 = l2) ==> (LENGTH l1 = LENGTH l2) *)

(* For practice with lambda-expressions, here we put the whole end
 of the proof into the DISJ_CASES_THEN2 arguemnts: *)

restart();
e(Induct THEN REWRITE_TAC [LENGTH, MAP]);
e(Cases THEN REWRITE_TAC [LENGTH, NOT_NIL_CONS]);
e(REPEAT GEN_TAC);

(* 1 subgoal:

    (f h::MAP f l1 = l2) ==> (SUC (LENGTH l1) = LENGTH l2)
    ------------------------------------
      !l2 f. (MAP f l1 = l2) ==> (LENGTH l1 = LENGTH l2)  *)

e(DISJ_CASES_THEN2
   (fn th => REWRITE_TAC [th, GSYM NOT_NIL_CONS])
   (fn th' => STRIP_ASSUME_TAC th' THEN AR
         THEN DISCH_THEN (STRIP_ASSUME_TAC o REWRITE_RULE [list_11])
         THEN RES_TAC THEN ASM_REWRITE_TAC [LENGTH])
   (ISPEC (Term`l2:'b list`) list_CASES));  (*  Initial goal proved.  *)

(* Off-the-subject exercise for anyone who likes it: look up the theorem
  LENGTH_MAP, and use it to give a proof our little theorem that doesn't
  even use induction. *)

drop();