Hi Vincent, I had exactly the same problem when I was doing long proofs in HOL Light for the Flyspeck project. Later, I learned SSReflect extension in Coq where the described rewriting issue was solved by "rewrite" tactic. Some time ago, I implemented my version of a subset of SSReflect language in HOL Light. This implementation and a reference manual are available at http://code.google.com/p/flyspeck/downloads/list If you are interested, read the description of the "rewrite" tactic in the SSReflect/HOL Light manual.
Best, Alexey On 11/22/2012 3:31 PM, Vincent Aravantinos wrote: > 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; > ------------------------------------------------------------------------------ Monitor your physical, virtual and cloud infrastructure from a single web console. Get in-depth insight into apps, servers, databases, vmware, SAP, cloud infrastructure, etc. Download 30-day Free Trial. Pricing starts from $795 for 25 servers or applications! http://p.sf.net/sfu/zoho_dev2dev_nov _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
