This tactic works with coq-7.4
and is written using ocaml-3.06.
You can dowload the sources (tar.gz).
Gomega is a tactic that relies on Omega. Its aim is to partially clear the
proof context before running the Omega tactic.
It takes as input a list of identifiers. It generalizes them, and then
try to clear every hypothesis (starting from the lastest introduced).
Once the context has been purged, it calls Omega to solve the goal.
The main advantage of this tactic are that it reduces the time Omega
takes to decide whether the statement is provable or not.
Its drawback is that it forces the user to determine by him/herself which
hypotheses are relevant to prove the goal. However forcing the user to do so,
makes it easier to build dependency graphs from proof scripts.
It is useful when reprocessing proof scripts to prove slightly
different statements. It happens all the time when using
the Correctness command of Coq or the why tool
to generate some proof obligations.
Just write "Gomega" if enough information is available in the goal to
prove it. Otherwise you can use "Gomega with [hyps]" where hyps is
a list of hypotheses to be able to prove the current goal.
Here are some simple examples of proof scripts:
Require Export ZArith.
Lemma e1 : `0<1`.
Gomega.
Qed.
Lemma e2 : (n,m:Z)`n<m`->`0<n`->`n<n+n`.
Intros n m H1.
Gomega.
Qed.
Lemma e3 : (n,m:Z)`n<m`->`n<=m`.
Intros n m H.
Try Gomega. (* fails because Omega requires the hyp H to solve the goal *)
Gomega with H.
Qed.