The Coq mailing list

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

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

On Wed, Jun 22, 2011 at 01:58, Bruno Woltzenlogel Paleo <bruno.wp AT gmail.com> wrote:

Hi Lucian,

Although I probably cannot help you, since my knowledge of Coq is quite basic, I found your question interesting. Do you mind if I ask you a question for my own clarification?

> How can I prove this theorem without using "auto with arith"?
>
> Lemma silly : forall t : nat, t >=2 -> t <= 2 -> t = 2.
>
> When proved using "auto with arith", the proof term is
>
> silly =
> fun (t : nat) (H1 : t >= 2) (H2 : t <= 2) => le_antisym t 2 H2 H1
>      : forall t : nat, t >= 2 -> t <= 2 -> t = 2
>
> I didn't even know le_antisym existed, not to mention how ugly this term looks:

Are you interested in proving this lemma without "auto with arith", but still using "le_antisym"? Or are you (also) interested in proving it without using the pre-existing "le_antisym"?

Best regards,

Bruno

--
Bruno Woltzenlogel Paleo
http://www.logic.at/people/bruno/