The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

Hi all

Le 12 octobre 2010 23:05, Stéphane Lescuyer
<stephane.lescuyer AT polytechnique.org>
 a écrit :
> Indeed, the less I mix proofs and programs, the more happy I
> am :)

I generally agree with this statement, except in the case of...
decidability function!
When you use a decidability function instead of a boolean function, it
comes at almost no cost. Indeed, the "if" construct works, and with
the nice coercion

Definition proj_sumbool (P Q: Prop) (a: {P} + {Q}) : bool :=
  if a then true else false.

Implicit Arguments proj_sumbool [P Q].

Coercion proj_sumbool: sumbool >-> bool.

(from the coqlib.v file of compcert,
http://compcert.inria.fr/doc/html/Coqlib.html), you can even write
things like

if (peq p q) || (peq r s) then....

And when you need to program the function, two main situations occurs:
either you want to extract it/compute with it, or you don't.
In the last case, the "decide equality" tactic is pretty convenient
(it is actually convenient in the first case too). But if you really
want to make sure the code is the right one, the Program extension is
pretty efficient. Imagine you want a fast equality check on unit

<<<<
Require Program.

Program Definition eq_dec_unit (u1 u2: unit):
  {u1 = u2} + {u1 <> u2}:=
  left _.
Next Obligation.
  destruct u1; destruct u2; reflexivity.
Qed.
>>>>

and if you don't want to prove it directly in your code, you still
have the option Stéphane pointed earlier in the discussion, namely to
split your definition in a boolean function and a lemma.


My 2c.

Alexandre Pilkiewicz