The Coq mailing list

[Gyesik Lee <gslee AT ropas.snu.ac.kr>]

ah... thank you for the quick replies.

Gyesik

2010/5/31 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
>
>