The Coq mailing list

[Stéphane Glondu <steph AT glondu.net>]

Le 18/07/2010 12:35, Tambet a écrit :
> 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?

I don't understand what you are trying to achieve here, but one way to
define a subset is to use the sig datatype (i.e. { z : Z | P z }, where
"P z" is a property about z). Note that you'll need a projection to use
something of this type as a Z. You can also define a record with a Z
field and/or a coercion to give an illusion of subtyping. Please refer
to the manual for more information (look for records and coercions).

> 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.

You can use assert: "assert (Hnew := Hold)" will duplicate the
hypothesis Hold and name it Hnew.

> 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.

Focus <n>.

> 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.

Show.

> 2) Automatic prover to generate Coq proofs - I could have a lot of help
> from automatic prover, which is able to prove simple things [...]

There are some kinds of goals that can be proved automatically... but
not all of them! Some of them are built-in in Coq, and documented in the
reference manual (look for "automat" in the table of contents).

> [...] 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.

Well... it depends on what you mean by "open it's result". You can
always have a look at the proof term of a completed proof with the
"Print" command. If you want to have a look at what a specific tactic
did, you can prefix it with "info" (it works very well with auto).

> 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.

You can define (using Ltac) a tactic that tries what usually works in
your case, and then use it. For example:

Ltac mytrivial := simpl; (trivial || tauto).

then use "mytrivial" in your scripts. And as usual, you can use "info
mytrivial" if you want to know what it actually did.

> The shell has some nasty behavior (I put "*" in end of important ones,
> but it would be nice to get feedback about others, too):

Note that the "shell" (or toplevel) is not really meant for direct
intensive use, especially by beginners (this remark applies to many of
your following comments). You should try to use coqide or proofgeneral
instead.

> 1*. It does not support up and down arrow for navigating history, which
> is trivially important feature for a beginner.

This feature doesn't belong to the toplevel. You can use rlwrap or ledit
for that.

> [...] 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.

I use SearchAbout a lot myself (it is documented in the reference manual).


Cheers,

-- 
Stéphane