[Hol-info] Improve EXISTS_TAC with by taking hints from the assumption list

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

Hi list,

here is another situation which I don't like and often meet (both in 
HOL-Light and HOL4), and a potential solution.
Please tell me if you also often meet the situation, if you agree that 
it is annoying, and if there is already a solution which I don't know of
(I'm pretty sure there is no solution in HOL-Light, but I'm not familiar 
with all its extensions over there).

SITUATION:

   goal of the form `?x. ... /\ P x /\ ...`
   + one of the assumptions is of the form `P t` (t is a big a term)
   + one wants to use t as the witness for x


USUAL MOVE:

   e (EXISTS_TAC `t`)
   (*Then rewrite with the assumptions in order to remove the now 
trivial P t:*)
   e(ASM_REWRITE_TAC[])


PROBLEM WITH THIS:

   Annoying to write explicitly the big term t.
   Plus the subsequent ASM_REWRITE_TAC is trivial and can thus be 
systematized.
   Not really annoying if it only appears from time to time, but I 
personally often face this situation.


SOLUTION:

   A tactic HINT_EXISTS_TAC which looks for an assumption matching one 
(or more) of the conjuncts in the conclusion and applies EXISTS_TAC with 
the corresponding term.


EXAMPLE IN HOL-LIGHT:

  (* Consider the following goal:*)

     0 [`P m`]
     1 [`!x. P x ==> x <= m`]

   `?x. P x`

   (* Usual move: *)
   # e (EXISTS_TAC `m:num`);;
   val it : goalstack = 1 subgoal (1 total)

     0 [`P m`]
     1 [`!x. P x ==> x <= m`]

   `P m`

   # e (ASM_REWRITE_TAC[]);;
   val it : goalstack = No subgoals

   (* New solution, which finds the witness automatically and removes 
the trivial conjunct : *)

   # b (); b (); e HINT_EXISTS_TAC;;
   val it : goalstack = No subgoals

   (* Notes:
    * - The use case gets more interesting when m is actually a big term.
    * - Though, in this example, the tactic allows to conclude the goal, 
it can also be used just to make progress in the proof without necessary 
concluding.
    *)

A HOL-Light implementation for HINT_EXISTS_TAC is provided below the 
signature.
One for HOL4 can easily be implemented if anyone expresses some interest 
for it.

Cheers,
V.

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


let HINT_EXISTS_TAC (hs,c as g) =
   let hs = map snd hs in
   let v,c' = dest_exists c in
   let vs,c' = strip_exists c' in
   let hyp_match c h =
     ignore (check (not o exists (C mem vs) o frees) c);
     term_match (subtract (frees c) [v]) c (concl h), h
   in
   let (_,subs,_),h = tryfind (C tryfind hs o hyp_match) (binops `/\` c') in
   let witness =
     match subs with
       |[] -> v
       |[t,u] when u = v -> t
       |_ -> failwith "HINT_EXISTS_TAC not applicable"
   in
   (EXISTS_TAC witness THEN REWRITE_TAC hs) g;;