coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] decision procedure during "Eval compute"

From: Gyesik Lee <gslee AT ropas.snu.ac.kr>
To: coq-club AT inria.fr
Subject: [Coq-Club] decision procedure during "Eval compute"
Date: Mon, 31 May 2010 12:39:43 +0900
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:date:x-google-sender-auth:message-id:subject :from:to:content-type; b=q+IbbpKNUA9sjq/vsOljIxFl6t4gDD4A2q5gFBxKbYrI3f6N3VhtoLwT+MXIV7yyPj liqWV88Ltqr52fQ3jFOcUOx2k1IlXnbryxdhMJOIBrnLiU5KAVrbv76pB0Ftoi9hIIG6 +chXXsn1Cl2VmUORjoDTzEV3KyRrfTIppMPeU=

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

[Coq-Club] decision procedure during "Eval compute", Gyesik Lee
- Re: [Coq-Club] decision procedure during "Eval compute", Andrew McCreight
  - Re: [Coq-Club] decision procedure during "Eval compute", Gyesik Lee
- Re: [Coq-Club] decision procedure during "Eval compute", Gregory Malecha