The Coq mailing list

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

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