The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

Hi Gyesik,

The problem is that Qed makes the implementation of toto_titi_dec opaque, i.e. the evaluator doesn't look inside of it. If you want to be able to simplify it using compute, then you need to make it transparent using Defined instead.

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

Then compute will simplify it down to true for you.

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

--
gregory malecha