The Coq mailing list

[Tambet <qtvali AT gmail.com>]

Hello!

I have installed Coq and played with it for a while and now I have a number of questions.

1. About the type system

Definition next_ (z:Z) :=
  match z with
    | Zpos  (xI  _)
    | Zpos  xH  => 1+1

    | Zpos  (xO  _) => 2+2
    | _ => 0
  end.

Inductive follows_ (n: Z): Z -> Prop :=
  | two:  (next_ n)
  | many: forall m:Z, follows_ n m -> follows_ n (next_ m).

The first case is: I tried to define "positive even integer" and "positive odd integer"  as types and ended up copying this from ZArith.Zeven. I did so, because I want it to be subset of Z. Is there a better way to define such subsets?

Second - this "follows" gives an error. "The term "next_ n" has type "Z" which should be Set, Prop or Type." I would like to create a simple ordered sequence, where from a>b and b>c it follows that a>c. Also, some manuals say that somehow using {...} inside it makes it better to unfold those things in proofs.

2. About few other things

I ask also about a few other things I have not found trivial, but will need soon.

Is there a tactic to duplicate working hypotheses (so that I can do transformations with only one instance) and to add working hypotheses from proven facts database (so that I could have it as reminder and use commands in the same way not depending, where those hypotheses come from)? I know that "cut" command is meant to add working hypotheses from scratch.

Is there a way to select active subgoal to be proven from list of subgoals? I mean, if I think that proving some of them gives me good evidence needed in proving another - that the order is not correct -, then it would be nice to choose another and start with that one.

3. General questions

Is there any command to redisplay current goal after some mess of queries? I have used just a name of some tactic, which does nothing in this situation, but it does not seem the best idea.

Are there two tools available:
1) Proof optimizer - I get quite long proofs and I know they could be made shorter. Is there any tool to remove unnecessary steps, simplify the logic and rewrite it into "intro; auto." form from "intro. auto."?

2) Automatic prover to generate Coq proofs - I could have a lot of help from automatic prover, which is able to prove simple things in such way that I can open it's result afterwards and read about how it did it (and check those commands out and try). It's also that this is somewhat annoying to prove trivial things like that positive number is not negative number.

3) Way to get hints - some possibilities seem trivial to me - 
that it could analyze the current state and say that "trivial" or 
"tauto" or "simple->tauto" path would have some effect over this one 
and "trivial" would prove it. Just a brute-force iteration over 
possibilities "try this" and "try that" up to x levels would be helpful 
(could I code it there?) Then I could maybe just write down steps I see 
more or less trivial and get proof logic for them, then think out about 
how to optimize such proof. If such thing has a customization about 
where to seek from, I would like to hear about that, too.

Is there any short and clear manual with each command described with a few lines? I have started to create such thing for myself, but it's not a good way to get the complete short reference. I mean, the reference spends several pages to give formal descriptions of syntax, which one could understand from first sight - and manuals make some selection of important basic things, but they are incomplete and long. I have started reading standard lib proofs, which is of help, but I would like to have such page as there are many for different languages - which is designed for two or three page and very fast-seekable.

4. About the shell

The shell has some nasty behavior (I put "*" in end of important ones, but it would be nice to get feedback about others, too):
1*. It does not support up and down arrow for navigating history, which is trivially important feature for a beginner.

2. It does not support tab-completition and suggestions (of available keywords etc.) Slightly related to this is question if in addition to "Check" and "Print All" is there some question about language built-ins? Because there is really a lot of them.

3. Last and least, when I clear terminal window, "Coq < " disappears until I hit return; when I paste multiline proof into terminal window, it will first paste it and then give Coq output instead of giving it correctly (error messages are not synchronized with lines).

I know that some environments have tools and plugins to fix exactly the same kind of annoyments. Does Coq have such things? I did also look those graphical IDEs (CoqIDE, which crashes and looks silly and into to pcoq, which needs me to click some "do it" button and does not give much additional power instead of clicking to type keywords I already know - the latter I will try anyway when they get it up). Command line interface is important anyway. I thought that it would be nice to hack Python's idle to support Coq.

Thanks,
    Tambet