The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Sun, Dec 23, 2012 at 5:28 PM, Victor Porton 
<porton AT narod.ru>
 wrote:
> I have the dream to formalize poset/lattice theory in Coq. (I am not very 
> qualified yet, but the dream exists.)
>
> My first attempt was based on using GAIA: 
> http://www-sop.inria.fr/marelle/gaia/ which is basically an ZFC 
> formalization in Coq.
>
> But I noticed that it is handy to treat [sub] as a partial order. This does 
> not work in ZFC because proper classes issues.
>
> So I have thought to replace a ZFC binary relation defined in GAIA with 
> just [Set*Set->Prop] (or more generally [T1*T2->Prop]).
>
> I doubt whether I can formulate order theory statements without using ZFC.
>
> For example, I was told that Coq's way is to use setoids.
>
> Can reasonable amount of set theory be expressed without resorting to ZFC, 
> instead using setoids and other Coq ways? I speak specifically about 
> formalization of order theory (partial order, meets, joins, maximum, 
> minimum, infimum, supremum, Galois connections, etc.)

I'd say that using Coq types as the base for the theory would almost
always be the way to go, unless somehow your theory is intricately
tied to ZFC concepts (which should be extremely rare outside model
theory).  The main advantage of ZFC is a small set of syntax and
axioms (mostly useful for model theory), while the big disadvantage is
that it's a fairly artificial model in which to do real mathematics.
Coq's type theory is a much closer match to how most mathematicians
think of things on a daily basis, but at the cost of a somewhat more
complex kernel and metatheory.

The question of whether to use setoids, or else whether to use some
axioms, is an orthogonal question.  The main issue with using axioms
is that it can make it more difficult or impossible to run
calculations within Coq, depending on the situation, which I think is
the usual reason why you'd want to use setoids.  But if you don't care
about running calculations, then you can just use whatever axioms you
need to be able to construct quotient types, and use regular equality
instead of going through the pain of specifying that every function in
your theory respects various equivalences.

If you'd like to see some examples of how things might look encoded in
Coq type theory as opposed to ZFC, you might take a look at my
SetTheory and Topology contribs, which develop classical point-set
topology in this way using axioms like excluded middle, axiom of
choice, definition by proving "there exists a unique ...", etc.  And a
short time ago I posted a file including some of the basic lattice
theory definitions, under a title which was something like "generating
product topology" -- though in that case, for technical reasons, I
chose to use an axiom-free setoid formulation.  Oh, and I guess I
hadn't included any lattice semantics yet, so if you'd like to see
that you can email me privately and I'll see if I can get an updated
version of the file to you.

(Oh, and by the way, you'll probably want to use Type in place of Set,
or you'll run into universe issues again with things like your sub
example.  Although Coq type theory doesn't really have a direct notion
of when one type is a "subtype" of another.)
-- 
Daniel Schepler