Hi Peter,
here is the difference:
(* The new hypotheses are added as conjuncts rather than as a *)
(* separate subgoal to reduce the user's burden of subgoal splits *)
(* when creating tactics to prove theorems. If a separate subgoal *)
(* is desired, simply use CONJ_TAC after the dependent rewriting to *)
(* split the goal into two, where the first contains the hypotheses *)
(* and the second contains the rewritten version of the original *)
(* goal. *)
In my tactic, the new hypotheses are added deeply, as close as possible to
the atom where the rewrite happens.
Consider the following examples:
- Consider the goal:
!x. x > 0 ==> x / x = y
Then my tactic will replace it by:
!x. x > 0 ==> x <> 0 /\ 1 = y
Whereas, from my tries, dep_rewrite could not apply because x is quantified.
- Without the quantification, you can consider the goal:
x > 0 ==> x / x = y
where dep_rewrite would yield
x <> 0 /\ (x > 0 ==> x / x = y)
which is not provable, whereas my tactic yields:
x > 0 ==> x <> 0 /\ x / x = y
This looks like a small difference but it changes a lot of things in
practice because calls to dep_rewrite need to be interleaved by calls to
GEN_TAC or DISCH_TAC (in these examples), whereas with my tactic one call
to IMP_REWRITE_TAC (with several theorems) is enough.
This change is not just a simple change but required the development of a
new notion of conversion, hence it seemed better to me to start it from
scratch rather than patching dep_rewrite.
V.
2013/7/11 Peter Vincent Homeier <palan...@trustworthytools.com>
> Vincent, how does this tactic compare to the dependent rewriting package
> in src/1/dep_rewrite.{sig,sml}? It appears at first glance to address the
> same problem you are working on. Here is part of the .sig header comment:
>
> (* ================================================================== *)
> (* ================================================================== *)
> (* DEPENDENT REWRITING TACTICS *)
> (* ================================================================== *)
> (* ================================================================== *)
> (* *)
> (* This file contains new tactics for dependent rewriting, *)
> (* a generalization of the rewriting tactics of standard HOL. *)
> (* *)
> (* The main tactics are named DEP_REWRITE_TAC[thm1,...], etc., with *)
> (* the standard variations (PURE,ONCE,ASM). In addition, tactics *)
> (* with LIST instead of ONCE are provided, making 12 tactics in all. *)
> (* *)
> (* The argument theorems thm1,... are typically implications. *)
> (* These tactics identify the consequents of the argument theorems, *)
> (* and attempt to match these against the current goal. If a match *)
> (* is found, the goal is rewritten according to the matched instance *)
> (* of the consequent, after which the corresponding hypotheses of *)
> (* the argument theorems are added to the goal as new conjuncts on *)
> (* the left. *)
> (* *)
> (* Care needs to be taken that the implications will match the goal *)
> (* properly, that is, instances where the hypotheses in fact can be *)
> (* proven. Also, even more commonly than with REWRITE_TAC, *)
> (* the rewriting process may diverge. *)
> (* *)
> (* Each implication theorem for rewriting may have a number of layers *)
> (* of universal quantification and implications. At the bottom of *)
> (* these layers is the base, which will either be an equality, a *)
> (* negation, or a general term. The pattern for matching will be *)
> (* the left-hand-side of an equality, the term negated of a negation, *)
> (* or the term itself in the third case. The search is top-to-bottom,*)
> (* left-to-right, depending on the quantifications of variables. *)
> (* *)
> (* To assist in focusing the matching to useful cases, the goal is *)
> (* searched for a subterm matching the pattern. The matching of the *)
> (* pattern to subterms is performed by higher-order matching, so for *)
> (* example, ``!x. P x`` will match the term ``!n. (n+m) < 4*n``. *)
> (* *)
> (* The argument theorems may each be either an implication or not. *)
> (* For those which are implications, the hypotheses of the instance *)
> (* of each theorem which matched the goal are added to the goal as *)
> (* conjuncts on the left side. For those argument theorems which *)
> (* are not implications, the goal is simply rewritten with them. *)
> (* This rewriting is also higher order. *)
> (* *)
> (* Deep inner universal quantifications of consequents are supported. *)
> (* Thus, an argument theorem like EQ_LIST: *)
> (* |- !h1 h2. (h1 = h2) ==> (!l1 l2. (l1 = l2) ==> *)
> (* (CONS h1 l1 = CONS h2 l2)) *)
> (* before it is used, is internally converted to appear as *)
> (* |- !h1 h2 l1 l2. (h1 = h2) /\ (l1 = l2) ==> *)
> (* (CONS h1 l1 = CONS h2 l2) *)
> (* *)
> (* As much as possible, the newly added hypotheses are analyzed to *)
> (* remove duplicates; thus, several theorems with the same *)
> (* hypothesis, or several uses of the same theorem, will generate *)
> (* a minimal additional proof burden. *)
> (* *)
> (* The new hypotheses are added as conjuncts rather than as a *)
> (* separate subgoal to reduce the user's burden of subgoal splits *)
> (* when creating tactics to prove theorems. If a separate subgoal *)
> (* is desired, simply use CONJ_TAC after the dependent rewriting to *)
> (* split the goal into two, where the first contains the hypotheses *)
> (* and the second contains the rewritten version of the original *)
> (* goal. *)
> (* *)
> (* The tactics including PURE in their name will only use the *)
> (* listed theorems for all rewriting; otherwise, the standard *)
> (* rewrites are used for normal rewriting, but they are not *)
> (* considered for dependent rewriting. *)
> (* *)
> (* The tactics including ONCE in their name attempt to use each *)
> (* theorem in the list, only once, in order, left to right. *)
> (* The hypotheses added in the process of dependent rewriting are *)
> (* not rewritten by the ONCE tactics. This gives a more restrained *)
> (* version of dependent rewriting. *)
> (* *)
> (* The tactics with LIST take a list of lists of theorems, and *)
> (* uses each list of theorems once in order, left-to-right. For *)
> (* each list of theorems, the goal is rewritten as much as possible, *)
> (* until no further changes can be achieved in the goal. Hypotheses *)
> (* are collected from all rewriting and added to the goal, but they *)
> (* are not themselves rewritten. *)
> (* *)
> (* The tactics without ONCE or LIST attempt to reuse all theorems *)
> (* repeatedly, continuing to rewrite until no changes can be *)
> (* achieved in the goal. Hypotheses are rewritten as well, and *)
> (* their hypotheses as well, ad infinitum. *)
> (* *)
> (* The tactics with ASM in their name add the assumption list to *)
> (* the list of theorems used for dependent rewriting. *)
> (* *)
> (* There are also three more general tactics provided, *)
> (* DEP_FIND_THEN, DEP_ONCE_FIND_THEN, and DEP_LIST_FIND_THEN, *)
> (* from which the others are constructed. *)
> (* *)
> (* The differences among these is that DEP_ONCE_FIND_THEN uses *)
> (* each of its theorems only once, in order left-to-right as given, *)
> (* whereas DEP_FIND_THEN continues to reuse its theorems repeatedly *)
> (* as long as forward progress and change is possible. In contrast *)
> (* to the others, DEP_LIST_FIND_THEN takes as its argument a list *)
> (* of lists of theorems, and processes these in order, left-to-right. *)
> (* For each list of theorems, the goal is rewritten as many times *)
> (* as they apply. The hypotheses for all these rewritings are *)
> (* collected into one set, added to the goal after all rewritings. *)
> (* *)
> (* DEP_ONCE_FIND_THEN and DEP_LIST_FIND_THEN will not attack the *)
> (* hypotheses generated as a byproduct of the dependent rewriting; *)
> (* in contrast, DEP_FIND_THEN will. DEP_ONCE_FIND_THEN and *)
> (* DEP_LIST_FIND_THEN might be fruitfully applied again to their *)
> (* results; DEP_FIND_THEN will complete any possible rewriting, *)
> (* and need not be reapplied. *)
> (* *)
> (* These take as argument a thm_tactic, a function which takes a *)
> (* theorem and yields a tactic. It is this which is used to apply *)
> (* the instantiated consequent of each successfully matched *)
> (* implication to the current goal. Usually this is something like *)
> (* (fn th => REWRITE_TAC[th]), but the user is free to supply any *)
> (* thm_tactic he wishes. *)
> (* *)
> (* One significant note: because of the strategy of adding new *)
> (* hypotheses as conjuncts to the current goal, it is not fruitful *)
> (* to add *any* new assumptions to the current goal, as one might *)
> (* think would happen from using, say, ASSUME_TAC. *)
> (* *)
> (* Rather, any such new assumptions introduced by thm_tactic are *)
> (* specifically removed. Instead, one might wish to try MP_TAC, *)
> (* which will have the effect of ASSUME_TAC and then undischarging *)
> (* that assumption to become an antecedent of the goal. Other *)
> (* thm_tactics may be used, and they may even convert the single *)
> (* current subgoal into multiple subgoals. If this happens, it is *)
> (* fine, but note that the control strategy of DEP_FIND_THEN will *)
> (* continue to attack only the first of the multiple subgoals. *)
> (* *)
> (* ================================================================== *)
> (* ================================================================== *)
>
> The dependent rewriting package has been part of HOL for many years.
> Perhaps if you desire some additional functionality, it could be folded
> into this package?
>
> Cheers,
> Peter
>
> On Thu, Jul 11, 2013 at 6:08 AM, Vincent Aravantinos <
> vincent.aravanti...@gmail.com> wrote:
>
>> Hi list,
>>
>> I developed a new tactic that takes a theorem of the form P ==> l = r and
>> replaces l by r in a goal adding whatever it needs to make it work properly
>> (typically conjunction with P; but can also be an implication or even
>> existentials).
>>
>> This is a follow-up of the discussion I started a few months ago (
>> http://sourceforge.net/mailarchive/message.php?msg_id=30133516), the
>> major difference being that it solves the problem raised by Michael Norrish
>> (i.e., it could not work under the scope of a quantifier) in a systematic
>> and (in my opinion) elegant way.
>>
>> This change entails that the tactic is much more modular and thus can be
>> chained very smoothly. Many preprocessing options also allows it to be a
>> (sometimes more powerful) replacement for REWRITE_TAC, SIMP_TAC and even
>> MATCH_MP_TAC. Please look at the (draft) manual for more info.
>>
>> The code is available at: https://github.com/aravantv/impconv (HOL Light
>> only for now)
>> To install, type:
>> # needs "target_rewrite.ml";;
>> The pdf manual is available in the directory "manual".
>>
>> The development of this tactic required quite some work that might be
>> useful in other context. This is undocumented for now but is described in a
>> paper which is currently under review.
>>
>> Regards,
>> --
>> Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University,
>> Hardware
>> Verification Group
>> http://users.encs.concordia.ca/~vincent/
>>
>>
>> ------------------------------------------------------------------------------
>> See everything from the browser to the database with AppDynamics
>> Get end-to-end visibility with application monitoring from AppDynamics
>> Isolate bottlenecks and diagnose root cause in seconds.
>> Start your free trial of AppDynamics Pro today!
>>
>> http://pubads.g.doubleclick.net/gampad/clk?id=48808831&iu=/4140/ostg.clktrk
>> _______________________________________________
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>>
>
>
> --
> "In Your majesty ride prosperously
> because of truth, humility, and righteousness;
> and Your right hand shall teach You awesome things." (Psalm 45:4)
>
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent/
------------------------------------------------------------------------------
See everything from the browser to the database with AppDynamics
Get end-to-end visibility with application monitoring from AppDynamics
Isolate bottlenecks and diagnose root cause in seconds.
Start your free trial of AppDynamics Pro today!
http://pubads.g.doubleclick.net/gampad/clk?id=48808831&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
