Coq: How to add meaningful hints?

Question

I am new to Coq and might be doing completely the wrong way. It seems to me that I need to choose between writing axioms/theorems that are nicely human-readable and axioms/theorems that are useful as hints, since in the human-readable form they "hide" the syntax too much and the auto tactic fails to use them. I wish to know if there's some way to enjoy the best of both worlds.

I will give an example which is a little elaborate since otherwise I fear I won't be able to convey my meaning.

As a learning exercise I'm trying to do group theory. Here are my definitions:

Variable G: Set.
Variable op: G -> G -> G.
Variable inv: G -> G.
Variable e:G.
Infix "+" := op.
Notation "- x" := (inv x).

Definition identity x := forall a:G, a + x = a /\ x + a = a.

Definition associative_law := forall a b c:G, a + (b + c) = (a + b) + c.
Definition identity_law := identity e.
Definition inverse_law := forall a:G, a + (-a ) = e /\ -a + a = e.
Definition group_laws:= associative_law /\ identity_law /\ inverse_law.
Axiom group_laws_hold: group_laws.

I have attempted to make everything human-readable (to me, at least). So the axiom that says that e is identity is "hidden" behind two layers of abstraction: "group_laws" and "identity".

I can also write this axiom (well, one half of it I'll need) directly:

 Axiom identity_law_holds: forall a:G, a + e = a.

Now, let's take our group-axiom as hint:

Hint Resolve group_laws_hold.

Now I try to prove a simple statement on groups - identity is unique:

Theorem identity_is_unique: forall x:G, identity x -> x = e.
Proof.
intros.
transitivity (op x e).
symmetry.

So far, so good. Now my current goal is "x + e = x". If I do now

apply group_laws_hold.

This goal will be solved. However, doing "auto" does nothing, probably since Coq can't recognize that the "group_laws_hold" is relevant to "x + e = x" due to the fact that "group_laws_hold" is not of the same syntax as "x + e = x".

However, if I add the hint

Hint Resolve identity_law_holds.    

Then "auto" will work, of course. But if I slightly change "identity_law_holds" to something a little more general (and more correct)

 Axiom identity_law_holds: forall a:G, a + e = a /\ e + a = a.

Then "auto" will fail again.

So my question is: Is there a way to fix my code such that "auto" will work but with hints more general than mine "Axiom identity_law_holds: forall a:G, a + e = a"?

Answer 1

eauto is able to do some normalization. What eauto can't do is induction, because the conclusion of induction principles like and_ind is so general it would slow down eauto almost to a stop. At any rate, eauto uses intros before using eapply when often it's necessary to do induction before introducing anything.

You'll have to define your own less general projections.

Lemma l1 : group_laws -> identity_law.
Proof. intros [? [? ?]]. eauto. Qed.

Lemma l2 : identity_law -> identity e.
Proof. eauto. Qed.

Lemma l3 : forall x, identity x -> forall a, a + x = a.
Proof. intros. einduction H. eauto. Qed.

Lemma l4 : forall x, identity x -> forall a, x + a = a.
Proof. intros. einduction H. eauto. Qed.

Hint Resolve eq_sym eq_trans group_laws_hold l1 l2 l3 l4.

Theorem identity_is_unique: forall x, identity x -> x = e.
Proof. info_eauto 7. Qed.

But you can force eauto to use and_ind.

Hint Extern 1 => eapply and_ind.