The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

Dear Robin,

Inversion generally produces complicated proof terms, so it is quite
often not such a good idea to unfold those and try to prove
properties. It is often better to first state the properties that your
function should satisfy and then create a function that satisfies
them. E.g., you need a function f: nat -> nat but would need lots of
complicated tactics to build it. It is often easier to characterize
the pairs (x, f(x)) using an inductive definition. So you make an
inductive definition def_f of type nat -> nat -> Prop and then you
create a definition realize_f of type forall n: nat, { m: nat | def_f
n m }. You can use tactics to build that. After that you can define f
using realize_f and prove properties of f using def_f. If the m that
satisfies def_f n m happens to be unique, the uniqueness property
def_f_unique of type forall n m1 m2: nat, f n m1 -> f n m2 -> m1 = m2
is quite often very useful as well.

Good luck,
Chris