The Coq mailing list

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

Thank you, Stephane. That's exactly what I wanted to know. Also, many thanks to Adam and the other guys for their help.

Best,
Lucian

2011/6/22 Stéphane Lescuyer <stephane.lescuyer AT polytechnique.org>

Well, Adam's proof is the one you should write for that particular
lemma, but I have the feeling what you really want to know is how to
mechanically prove that some predicate holds on some finite integer
domain by evaluating the predicate.

In that case, you could write something like this:

Goal forall t : nat, 1 < t -> t < 100 -> f t.
Proof.
 intros H H0.
 rewrite nat_compare_lt in H, H0.
 repeat (destruct t; try discriminate; try (exact I)).
Qed.

The rewrites are just there to rewrite the logical hypotheses to
computational hypotheses (you can skip this step and, instead, write a
tactic which automatically proves or disproves ground instances of 'n
<= m', but this is much more efficient to do it this way).

Then there is a tactic 'loop' which repeatedly destructs the integer,
trying 0, 1, 2, ... in order, trying each time to disprove the
hypotheses (using discriminate) or to prove the goal ('exact I' will
succeed if and only if the current goal evaluates to True). You can
unroll the loop and manually go through it step by step and you should
get the idea.

And if you re curious, print the proof term you obtain with this
proof... and you will understand why I changed 2000 to 100, and why
Cedric advised you not to used large "nat"s :)

Hope this helps,

Stéphane L.

On Wed, Jun 22, 2011 at 5:11 PM, Lucian M. Patcas
<lucian.patcas AT gmail.com> wrote:
> Point taken, but why not "P = NP"? :)
>
> Say f is
>
> f (t : nat) := if t>1 and t<2000 then True else False
>
> How can I prove this
>
> forall t : nat, t >=2 -> t <= 1000 -> f t
>
> Pardon my ignorance.
>
> On Wed, Jun 22, 2011 at 10:52, Adam Chlipala <adam AT chlipala.net> wrote:
>>
>> Lucian M. Patcas wrote:
>>>
>>> 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.
>>
>> I wouldn't say there is a well-defined strategy for all lemmas of that
>> form.  For instance, consider [f] that ignores its argument and always
>> returns "P <> NP".
>
>

--
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06