The Coq mailing list

[Hendrik Tews <tews AT os.inf.tu-dresden.de>]

Michiel Helvensteijn 
<mhelvens AT gmail.com>
 writes:

   Definition do_stuff (a: Op) : T + { a = remove }.
     ... Defined.

   Definition do_stuff' (a: Op) : (a <> remove) -> T.
     ... Defined.

   Definition do_stuff'' (a: {o: Op | o <> remove}) : T.
     ... Defined.

   I'm trying to decide which to go ahead with. In your experience, what
   are the advantages and disadvantages of each of these choices in
   practice? Which do you prefer?


In general there is another alternative: returning a default
value when the arguments are inappropriate:

   Definition do_stuff (a : Op) (default : T) : T


In my experience there is no general answer about what is the
best solution. It depends on how you use you function and about
the proof obligations that you have to prove about it. 

The solution with a default value makes the least problems in
proofs, but can of course only be used if there exists a natural
default value (which is rarely ever the case).

For the comparison of sumor vs. precondition, I would say that in
proofs, sumor does _always_ cause a little bit of trouble, while
the precondition may cause big trouble sometimes.

With someor you have to make a case distinction (destruct) for
every use of your function in every proof obligation. However,
this is usually easy and the proof obligation for the error case
is usually easy to solve.

The precondition works nicely if you usually have proof terms for
(a <> remove) available and if you don't have to rewrite the 
(a : Op) argument. If you don't have a proof for (a <> remove)
then you usually have to make a case distinction beforehand
(assert (a <> remove)). This can involve a lot of typing/copying
and the proof needs manual adjustment for even the smallest
change in "a".

With the precondition, you cannot simply rewrite the "a" or use
destruct on it. The problem is that you have to change "a" and 
"a <> remove" simultaneously, because otherwise your terms do not
type check. One usually has to first (generalize (a <> remove))
before rewriting. In case you want to rewrite in the assumptions,
you have to revert before generalize.

Another disadvantage with the precondition is that eapply does
not work nicely: With the precondition, eapply introduces
existentials for "a" _and_ "a <> remove". While you usually
instantiate the existential for "a", it often happens that parts
of "a <> remove" remain uninstantiated. In these cases you have
to "Grab Existential Variables" or add "with" clauses.

With the precondition, you often have the problem, that apply,
trivial or reflexivity do not work, because the terms for 
"a <> remove" are not convertible. For these cases you need a
proof irrelevance theorem, stating 

    forall(a : OP)(a_ok1 a_ok2 : a <> remove), 
      do_staff a a_ok1 = do_staff a a_ok2.

The proof for this is obvious but relatively long, because you
usually need a full induction on a.

The precondition has also a small presentation problem: Theorems
usually read "forall(a : op)(a_ok : a <> remove), ... " and you
have to explain why a precondition appears as a bound variable to
all those reviewers that are not familiar with dependent typing.
;-)


In summary, I would say, that the precondition often leads to
"cleaner" specifications but also to noticeably more complex
proofs.

Bye,

Hendrik