The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

  (1) unrelated to actual question: from observing the list, is it correct that rich HTML is actually _encouraged_ for this list as long as it makes the code easier to read?

  (2) actual question:

I want to write a ltac that says: "apply this lemma, if and only if the newly introduced goals can be solved by omega"

For example, consider this minimal example:

Lemma silly:

  forall a,

    a < 10 -> a < 20.

Proof.

  intros. omega. Qed.

Ltac tst :=

match goal with

| |- ?a < 20 => apply silly

end.

Lemma silly2:

  5 < 20.

  tst. (* good *) Abort.

Lemma silly3:

  15 < 20.

  tst. (* bad *) Abort.

whenever we do "apply silly", it induces a new goal "a < 10"

I want to be able to say:

  when you see ?x < 20,

    do apply silly, _only if_ ?x < 10 can be solved by omega

So I want it to fire in case silly2, but to leave the goal un-changed in case silly3.

Can someone show me the idiomatic solution to this?

Thanks!