[Hol-info] Automatic subgoal to apply a conditional rewrite

[Vincent A. <vin...@gm...>]

Hi list,

I often face the following small but annoying problem:

* Situation:
   - I have a theorem (say, "Th") of the form "P ==> t = u"
     ex: REAL_DIV_REFL
     (|- !x. ~(x = &0) ==> x / x = &1 in HOL-Light, |- !x. x <> 0 ==> (x 
/ x = 1) in HOL4)

   - the conclusion of my goal is a (big) term containing a subterm 
(say, " t' ") matching t
     ex: a big expression with a subterm t / t somewhere deep inside the 
term

* My aim: rewrite t' into u' using Th

* Solution:
   - make a subgoal to prove P' (the instance of P corresponding to t')
     ex: t / t <> &0
     (assume t is a big expression to make it annoying to type in)

   - use this subgoal to rewrite the original goal

* Problem:
   What annoys me in this frequent use case is that I have to explicitly 
state the subgoal P' whereas it seems it can be automatized.
   So, questions:
   - Am I the only one to find this annoying? :-)
   - If not, I imagine there might already exist a tactic that solves 
this recurrent problem, but if so I did not find it ?

* Possible solution:
   If not, I developed my own tactic which a couple of students here at 
HVG have been using and found useful.
   Please find below the implementation in HOL4 and HOL Light, the 
tactic is called "MP_REWRITE_TAC".
   In order to use it, e.g., for the above situation, just use:

     e(MP_REWRITE_TAC REAL_DIV_REFL)

   then the tactic will:
   - search the goal for a subterm matching t (if several matches it 
takes the first one it finds),
   - introduce a subgoal for the corresponding P',
   - rewrite the original goal with Th, taking P' into account.
   - add P' to the set of assumptions of the original goal, so that it 
can be reused later if needed.

Regards,
V.


Code:

HOL-Light:

let MP_REWRITE_TAC th (_,c as g) =
   let sel = lhs o snd o strip_forall o snd o dest_imp in
   let PART_MATCH = PART_MATCH sel (SPEC_ALL th) in
   let th = ref TRUTH in
   ignore (find_term (fun t -> try th := PART_MATCH t; true with _ -> 
false) c);
   (SUBGOAL_THEN (lhand (concl !th)) (fun x ->
     REWRITE_TAC[MP !th x] THEN STRIP_ASSUME_TAC x)) g;;

HOL4:

fun MP_REWRITE_TAC th g =
   let
     val sel = lhs o snd o strip_forall o snd o dest_imp
     val PART_MATCH = PART_MATCH sel (SPEC_ALL th)
     val th = ref TRUTH
     val _ =
       find_term (fn t => (th := PART_MATCH t; true) handle _ => false) 
(snd g)
   in
    (SUBGOAL_THEN (lhand (concl (!th))) (fn x =>
      REWRITE_TAC[MP (!th) x] THEN STRIP_ASSUME_TAC x)) g
end;

-- 
Vincent Aravantinos
Postdoctoral Fellow, Concordia University, Hardware Verification Group
http://users.encs.concordia.ca/~vincent