Forgot: in the examples below, both tactics are used with the theorem |-
!x. x <> 0 ==> x / x = 1
2013/7/11 Vincent Aravantinos <vincent.aravanti...@gmail.com>
> 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/
>
--
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
