The Coq mailing list

[Victor Porton <porton AT narod.ru>]

But what if I want to write "supremum S == supremum T"? (to add more 
complexity, the first and the second supremum may be taken on different sets.)

How to write it in terms of "supremum S x" and "has_supremum"?

04.11.2011, 01:12, "Andrej Bauer" 
<andrej.bauer AT andrej.com>:
>> šI will restate my problem again.
>>
>> šI want syntax similar to the following:
>>
>> š"supremum S == a".
>
> You can define a relation "is_supremum S a" and then define a special
> Notation so that you can write "supremum S == a" if you really want
> to. But I would advise against it. Not every informal syntax invented
> by mathematicians makes sense.
>
>> šI want the following to come true:
>>
>> š"a in X /\ S is a subset of X /\ supremum S = a -> S has a supremum"
>
> This is a triviality because you would write it as (continuing from
> the file I sent):
>
> ššššDefinition has_supremum {X : Poset} (S : X -> Prop) := exists x :
> X, supremum S x.
>
> ššššTheorem victor_or_daniel (X : Poset) (a : X) (S : X -> prop) :
> supremum S a -> has_supremum S.
> šššš(* proof left as exercise *)
>
>> šHow to do it with type theory? I ZF I can define "y" in such a way that 
>> "y not in S" and use "supremum S == y" to denote that S has no supremum. I 
>> see no alternative for this in type theory except to formalize some 
>> universe of sets (for example ZF) and work inside this universe. So to 
>> have this syntax convenience ZF is essentially unavoidable (at least so it 
>> seems to me).
>
> The alternative is to say simply
>
> Definition has_no_supremum {X : Poset} (S : X -> Prop) := not exists x
> : X, supremum S x.
>
> Why do you want that y? Just so that you can use your informal
> notation "supremum S == y" for two purposes, one of which makes little
> sense? Just stop using the broken informal notation and life will be
> easier.

-- 
Victor Porton - http://portonvictor.org