The Coq mailing list

["Andrew Kent" <andmkent AT indiana.edu>]

Hello all!

So I’ve been working on a project and finally proved a particular relation is
decidable:
Theorem MyRel_dec : forall (a:A) (b:B),
{MyRel a b} + {~MyRel a b}.
Proof.
...
Defined.

The proof is ~220 lines and hinges primarily on well_founded_induction on the
weight of the arguments.

I had thought I would be able to use this theorem to automatically solve MyRel
proof obligations as they come up with no problems using something like this:

Ltac solve_it :=
  match goal with
    | |- MyRel ?a ?b =>
      let provability := constr:(MyRel_dec a b) in
      let proof := eval compute in provability in
      match proof with
        | left ?prf => exact prf
        | right _ => idtac
      end
  end.

However, this takes an inordinate amount of time on all but the most trivial
of examples. (I let one example I thought was simple enough spin for an hour
before aborting)

It seems that although I have proven that MyRel is decidable, I built quite
possibly the absolute worst function for producing witnesses of the MyRel-
validity of potential arguments.

My question is, was it silly of me to think that a big proof of decidability
would be useful in helping prove particular instances? Is there some other
"obviously better" approach I should have taken? Or an obviously better way to
now prove instances of MyRel? Is this the kind of problem where one must
utilize the refine tactic to get correct *and* efficient code? Or is it
possible that I just wrote a particularly bad proof?

Thanks,
Andrew