Here, the inductive type expression has one constructor EValue and a bunch of other constructors which are not EValue. It feels silly to do this kind of case analysis because I know how most of the cases are going to go: just note that we’re looking at different constructors and discriminate. So
Is there a way to try to apply a particular tactic to all of the visible subgoals or to a subset of them? I’d like to write
intros. destruct e eqn:He. all:apply_intror. all:intros. all:discriminate.
but all requires that the tactic works on every goal. I’d like to shrug it off if some of them fail.
Is there a better way to perform this kind of case analysis when I’m working with match expressions? I find myself having to write a lot of lemmas for decidable disjunctions like the above so that, in later proofs, I can do something like destruct (expression_is_value_or_not my_expression) since that then gives me the two cases I care about. Is this canonical or is there a better way for me to express a case analysis of this form?
Thank you!
(edit: I had originally asked about all: and then discovered that, despite my previous misconceptions, all: does in fact exist.)
(Not very important here, but in general you should provide self-contained examples, I have had to concoct definitions for expression and value in order to play with your code.)
I won’t post any examples, just two general comments on the points you raise:
of course that code can be shortened, in fact in several different ways, with pros and cons each, but I would rather insist that you will learn (in a reasonable amount of time!) about at least the basic available features only if you go through at least some guides (I had mentioned the Software Foundation series). I would even advice the newcomer against diving directly into the reference documentation (the “refman”): Coq is the opposite of easy, and the opposite of small…
as for the “decidable disjunctions”, I am no expert but it seems to me you are proving things that are quite trivial and usually needn’t be proven explicitly at all… and then again, maybe going through at least some of the SF would give you a better sense of what needs stating and proving, certainly for various common problems.
First, you can make any tactic successful by prefixing it with try, so you could do all: try discriminate. Second, you can be a bit more precise than all:, e.g., 2-9: apply or_intror.
As for the more general question, no, there is no better way to do a case analysis. By design, the proof term needs to handle all the branches of the case analysis separately. (This might change in the future, but it would not help in your specific case.) So, you still need a separate proof for all the cases, though it can be a bit shorter, but not by much.
I agree with all the remarks from @jp-diegidio . I would just write an equivalent script with less redundancy:
...
destruct e eqn:He. (* Not sure the eqn is needed here, since e is a variable at start *)
1:{ apply or_introl. exists v. reflexivity. }
all:apply or_intro; intros; discriminate. }
Qed.
Note that there is no “try and error” strategy here. This script does exactly the same as yours. You may at some point want to use more complex tactic combinations like in now (try foo; repeat progress bar) (see Ltac — Coq 8.18.0 documentation) but as @jp-diegidio said this should not be your priority. Tactics are the tip of the iceberg of a formal proof. (Good) definitions and statements are of much greater importance. For instance your lemma statement is probably not the best you can prove about decidability of your type. One would prefer:
forall e:expression,
{exists v:value, e = EValue v} + {forall v:value, e <> EValue v}.
(edited the script, should have tried it first… But I was not as brave as @jp-diegidio to fill the holes in your examples)
This try is precisely the syntax I wanted. Thank you!
It makes sense that I should have to handle all the different cases of a given analysis. The lemma above is an example of a (probably quite hacky) way that I’ve been specifying the particular cases I case about:
destruct (expression_is_value_or_not my_expression).
- (* Deal with value case *)
- (* Deal with other cases *)
This sometimes allows me to have two cases instead of nine. But I suspect I won’t mind having nine cases so much equipped with the specific syntax you and @Matafou provided. Thanks again!
Thanks for the additional information! I didn’t know about the { ... } blocking syntax, probably because I’ve been skipping around in the material. Between this and try, I should be able to clean my toy proof up quite a bit.
I also just recently discovered the common practice of using {...}+{...} in equality decidability proofs. I bumped into it while learning how recursion schemes work and how to write my own (which I know I don’t need to do, but I always like to take a code generator like Scheme apart before I use it). I’ll put it on my list of things to examine. I appreciate the help!
Thanks again for your response! I’ll make sure to include more complete definitions in the future. I’ve prioritized brevity rather than completeness as I’m trying to minimize the amount of work these responses take. (As with any programming language, I figured that just about anyone familiar with it would see that syntax, wrinkle their nose, and say “you should just do X”.) But it’s clear that everyone here decided to experiment with what I posted, so minimal effort clearly involves giving all the definitions!
I’ve been using the Software Foundations material, but its examples are understandably short and so don’t always include instructions for how to handle engineering tasks. (For instance: grep 'all:' *.html *.v on the Logical Foundations directory yields no results. The same is true for grep 'eq_dec' *.html *.v.) I’ve found refman to be useful but, as you suggest, opaque. But I appreciate your emphasizing Software Foundations; it was some of the first material I used to get my footing last week and is quite helpful!
My reply to silene hopefully clarifies why I wanted the decidable disjunction for a particular constructor case. In general, I’m aware that I’m probably writing some very bad code. But, as with every other language I’ve learned, I’m starting with the approach of getting something to work and then incrementally understanding how to refactor to better practices and design. Right now, I’m pretty sure I’m at the “intro student who writes their own list element removal function” stage. But I’ll try to keep the noise on the forum down while I’m working through it.
Thank you! It does make things easier for anyone wanting to play with the code, it also makes things less ambiguous, especially where the questioner is not really sure about the substance and/or the boundaries of what s/he’s asking…
I can understand your pain there (I am primarily a programmer and an engineer), it was and still is a pain for me too: my humble opinion about that, after little more than a year that I have started using Coq, is that there is just very little available about that in general (which anyway is at least partly a reflection of “the sorry state of an entire industry”), so you’ll have to find out what works (I am myself still not at the point that I can share approaches in that sense, if not at a very general level), possibly up to building your own patterns, libraries and even tools… where the good news is that there is still a lot of work to do.
I didn’t know about the