The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT ens-lyon.fr>]

Hi,

I'm working on generating part of proof scripts automatically. On the
whole, it works quite well. But sometimes Coq is unable to check the
generated proof script: it gets stuck on the "apply" tactic. Here is a
small testcase (only the last two lines are important, the others are
given to provide a self-contained script):

  Variable A : Set.
  Variable f : A -> A -> A.
  Variable P : A -> Prop.
  Variable T : forall x y : A, P (f x y) -> P (f y x).
  Variables a b : A.
  Definition d := (f a b).
  Definition e := (f b a).
  Axiom K : P d.
  Lemma L : P e.
  apply T with (1 := K).

So we are trying to prove "(P e)", and a trivial proof is "(T a b K)".
As much as possible I would like to avoid generating this proof term
directly. I would prefer using the "apply" tactic. But Coq replies:

  Error: The term "K" has type "P d" while it is expected to have type "P (f 
?7 ?8)"

Coq has been unable to notice that "d" is "(f a b)" when trying to apply
the theorem. So we have to unfold "d", but since it is not visible in
the goal or in an hypothesis, we have first to load it. The same problem
will then appear with "e". So here is a proof script, it ends by a
similar "apply" and Coq is able to check it:

  generalize K.
  intro H.
  unfold d in H.
  unfold e.
  apply T with (1 := H).

There are obviously smaller proof scripts. This is not a challenge for
the one who will find the smallest proof script. I already have one,
it's "Let L : P e := T a b K." But as I explained, I would like to avoid
just generating a proof term, it would defeat the idea of using a Coq
script in the first place.

So my questions are:
- Why does Coq not notice that "d" is "f a b" when trying to match "P d"
and "P (f ?7 ?8)"?
- Is there a way to convince Coq to work a bit harder when applying a
theorem?
- Is there another tactic I could use instead of "apply"?

Best regards,

Guillaume