Hi Alexey, That looks great, I already had a quick look at your extension but didn't notice that particular feature of "rewrite". Unfortunately I don't have access to a checkpoint version of HOL-Light so I can't use it. And I had the feeling while browsing the manual that I was forced to use the provided IDE, which I don't really like. But if I can manage to install a checkpoint software on my machine, It looks really worth trying it!
Cheers, V. Le 22/11/2012 16:30, Alexey Solovyev a écrit : > 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; >> > -- Vincent Aravantinos Postdoctoral Fellow, Concordia University, Hardware Verification Group http://users.encs.concordia.ca/~vincent ------------------------------------------------------------------------------ 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
