The Coq mailing list

["Lucian M. Patcas" <lucian.patcas AT gmail.com>]

Hi Cedric,

OK, I shouldn't have used the word "evaluate". My question is what's the strategy to prove this lemma

forall t : nat, t >=2 -> t <= 1000 -> f t

in Coq, assuming f t holds over that interval. (Noted that using nat for big numbers is not a good idea).

Thanks,
Lucian

On Wed, Jun 22, 2011 at 09:18, AUGER Cedric <Cedric.Auger AT lri.fr> wrote:

Le Wed, 22 Jun 2011 09:41:35 -0400,
"Lucian M. Patcas" <lucian.patcas AT gmail.com> a écrit :

> Hi all,
>
> Thank you for your answers. It was late in the night and I guess my
> questions weren't as clear as I wanted them to be. Even so, your
> answers were very helpful.
>
> To clarify, these were my questions:
>
> 1. How to prove such theorems using minimum automation? I am all for
> automation, however, to understand how Coq works, it's better to use
> less sometimes.
>
> 2. How to find lemmas that could be useful? Jacques' hint on the info
> tactic is very useful indeed. Meanwhile, I have found that
> SearchPattern is a useful tool as well.
>
> Now, I have another question. Say I wanted to prove a theorem like
> this
>
> forall t : nat, t >=2 -> t <= 1000 -> f t
>
> assuming f is a function defined in the context and that the theorem
> has a proof indeed. How can I make Coq evaluate this function on that
> restricted domain?
>
> Thanks,
> Lucian

Can you precise your question? Are you using some coercion?

If not, all coq functions are total, so you don't have to assume that
you perform function application on restricted domain.

Eval compute (f 256).

should work.

If you want to evaluate your lemma, then you should do:

Eval compute
 (my_lemma 256
   (le_S (le_S ...(le_n 2)...))
   (le_S (le_S ...(le_n 256)...))).

Or probably beter: prove that "H: 256 >= 2" (for instance with the
tactic "repeat constructor.") and "H': 256 <= 1000" and then

Eval compute (my_lemma 256 H H').

Beware that if you make your proofs opaque (by ending them with Qed.
instead of Defined.), then if your lemma needs to know the structure of
your arguments, then the reduction may halt where computation is
required.

Note also, that I don't advise you to use "nat" with big numbers such
as "1000", use rather "positive", "Nat", or "Z", since the structure of
the reunion of the proofs of "H" and "H'" will be a 998 application of
the constructor "le_S".