Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] (newbie) How to encode a set algebra

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] (newbie) How to encode a set algebra


chronological Thread 
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: Marco Servetto <marco.servetto AT gmail.com>
  • Cc: Stijn Timbermont <stijn.timbermont AT gmail.com>, coq-club AT inria.fr
  • Subject: Re: [Coq-Club] (newbie) How to encode a set algebra
  • Date: Mon, 15 Aug 2011 10:50:40 -0400

Marco Servetto wrote:
To run to the solution of your problem you have two possibility
(for what my limited experience tell)
To define a normalize representation for your sets, so that two equals
set "really are syntactically equals"
and use operation that preserve such representation (that is does not
define sets as inductive trees of operations)
or use your first naive inductive definition but create your own
equals definition not using the "=" concept.

Actually, I'd recommend using ensembles. The details of how that should be done will depend on Stijn's answer to my clarification question.

Adding a layer of explicit syntax (e.g., a grammar of set expressions) is a decision always to be treated with the appropriate gravity. Let's hope it's not needed here. ;)



Archive powered by MhonArc 2.6.16.

Top of Page