coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?
- Date: Tue, 17 Jun 2014 11:41:53 -0400
Thank you, Arnaud. This is very
illuminating. I have some questions and comments (embedded
below)...
On 06/17/2014 08:09 AM, Arnaud Spiwack wrote: Let me try to give a more precise account of the situation in trunk. This is a long mail, but please read it if you are interested in this thread, because I value (need?) your input. A tactic can be seen as a function goal list -> goal list which updates a partial proof as a side-effect. Natively, a tactic manipulates a list of goal. A tactic could just reorder the goals, for instance (though I haven't written a syntax for that), or could count the goals. There is currently one tactic, in trunk, which strongly exploits this ability: shelve_unifiable (it hides all the goals whose proof appears (as an existential variable) in another goal). The semi-colon in Ltac is implemented as the functional composition of tactics. It is associative: t1;(t2;t3) is always exactly the same tactic as (t1;t2);t3. But confusion arises from the fact that t1;[t2|…|tn] is not of the form t1;t'. To be clear, when you say that t1;(t2;t3) is always the same as (t1;t2);t3, that's not the case when t3 is of the form [t3a|t3b|...], as shown by this: Goal forall (A B : Prop), A \/ B -> B. Note that the only difference between those two "destruct H" lines is their associativity. Thus, whether an alternative list like [idtac|fail..] is encapsulated in its own tactic (or parenthetical) vs. inlined matters. It behaves differently in the two cases, because it (naively) makes associativity matter, where before it didn't. I don't want to suggest that I think this is incorrect behavior. It has obviously worked out quite well, and hasn't been noticed much. I wouldn't have noticed it had I not wondered why Jason's attempt at a "at-most-one-goal-left" tactic didn't work. Although, when written out as in the above Goal, it seems quite counter-intuitive. It's just that there may be times (like with at-most-one-goal-left) where one would like to have the inlined-non-parenthetical behavior but also somehow contain this in its own tactic so that it doesn't need to be inlined everywhere. Tactics are only applied to a subset of the extant goals. The goals that the tactic currently "sees" are called the focused goals. The focused goals can be manipulated either by commands (Focus, braces, bullets) or, more dynamically, during the course of a tactic. There are several reasons to do so, the first one is that many tactics such as intro or refine, only really make sense in a given goal. For such tactic, the focus is restricted to a single goal, and the goal is given as a parameter to the tactic. This is the purpose of Proofview.Goal.enter in the OCaml code. In Ltac the choice is made dynamically during interpretation whether a tactic requires a goal or not. A second reason is the situation described above where we have several, presumably independent, goals which we may want to solve with different tactics [t1|t2…|tn]. A third case is for catching failure: take *try t* for instance a possible semantics is "do t, and if it fails do nothing"; but remember that t is applied to all the focused goals at the same time, so say "t" is intro, and one of the goals is not an implication then "try t" will do nothing at all, in any goal. So for such tactics, it is often the desired semantics that it is run focusing on one goal at a time. This is what tclINDEPENDENT does. A goal counting tactic would count the goals currently under focus. For example, in t ; [ let n := numgoals in … | ..], n will always be 1. That counting tactic would be useful. Also, by default, a tactic at toplevel is focused on the first goal. This default can be overriden by 2:t, 3:t to focus on the second goal or third. Neither "2:" nor "3:" can be used in tactics, they are just toplevel instruction. The new toplevel selector is all: (which, likewise, cannot be used inside a tactic): all:t applies t to every focused goal, not just the first one. The default can be changed (I would recommend doing so, actually) with Set Default Goal Selector "all" (try it: Goal True /\ True. split. exact I. Qed.). Then one can select a single toplevel goal to work with using the braces or the bullets. I have not yet tried Set Default Goal Selector "all". It seems like it would have the benefit of forcing scripts to clearly show where tactics apply to only one of several focused goals. Currently I use tclINDEPENDENT exactly at the places where it is required to be compatible with the former semantics: - fail (so that it succeed when there is 0 goal (anyway, fail uses the goal to understand its error message)) - t1||t2 (so that the choice of t1 or t2 can be different for each goal) - t1+t2 (to be compatible with t1||t2) - t;[t1|t2…|tn] (for the reason discussed earlier in the discussion. A very large amount of existing Ltac code depends on this semantics) - repeat t (so that the number of time t is used can be different for each goal) - progress t (so that it can fail in a goal where t does nothing even if t does something in another goal) What about match, first, and solve? They seem to act similarly, in that the don't need to do the same things in all focused goals. Also, I have not yet tried exactly_once, but it would seem to share this behavior, correct? There may be reasons to have global versions of these primitives. I just don't quite know, yet, how, syntax-wise, they should be introduced in Ltac. There is always the possibility of having names such as "global_fail", "global_orelse", "global_or", etc… It seems pretty clear that in the context of Ltac the global versions are not as useful than the local ones, so the nice syntax deserves to be attributed to the local versions. The one exception is t;[t1|…|tn] which clearly "steals" the syntax which should be attributed to a global tactic. Suggestions? Wishes? I don't seem to be able to come up with a case where || or + or progress, combined with associativity, produces a Goal as counter-intuitive as the one I gave above. Maybe it is only t;[t1|...|tn] that would benefit from an alternative? PS: @Jonathan, I am not aware of this "joining" feature in Prolog that you mentioned. Do you have pointers for me? I didn't mean to imply that I knew of any such Prolog feature - I meant the opposite, in a sense - that I could now see the usefulness of such a join feature in Ltac, even though I never considered one useful when using Prolog. -- Jonathan |
- Re: [Coq-Club] Tactic for detecting that there is a goal left?, (continued)
- Re: [Coq-Club] Tactic for detecting that there is a goal left?, Cedric Auger, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Arnaud Spiwack, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Jason Gross, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Jason Gross, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Arnaud Spiwack, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Jonathan, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Jonathan, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Arnaud Spiwack, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Jonathan, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Arnaud Spiwack, 06/17/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Jonathan, 06/17/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Arnaud Spiwack, 06/18/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Daniel Schepler, 06/18/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Arnaud Spiwack, 06/19/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Jonathan, 06/18/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Jonathan, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Jonathan, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Arnaud Spiwack, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Jason Gross, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Jason Gross, 06/13/2014
Archive powered by MHonArc 2.6.18.