The Coq mailing list

[Andrew McCreight <continuation AT gmail.com>]

Use Defined instead of Qed.  When you use Qed, Coq makes the definition opaque, and it won't reduce it during evaluation.  Even that may not work, depending on what proof "decide equality" happens to generate.

On Sun, May 30, 2010 at 8:39 PM, Gyesik Lee <gslee AT ropas.snu.ac.kr> wrote:

Hi,

I am wondering about how to get a simple answer when I perform "Eval
compute in ...".
Here is a simple example.

===========================

 Inductive toto_titi := toto | titi.

 Lemma toto_titi_dec : forall x y : toto_titi, {x = y} + {x <> y}.
 Proof.
   decide equality.
 Qed.

 Definition decision (t:toto_titi) : bool :=
   if toto_titi_dec t toto then true else false.

 Eval compute in (decision toto).

(* Coq's reply:
 if toto_titi_dec toto toto then true else false
    : bool
*)

=============================

Of course, Coq need to make a decision, but is there a way to get a
simplified answer "true" in the above case?

Gyesik