The Coq mailing list

[richard dapoigny <richard.dapoigny AT univ-smb.fr>]

Hi,


Le 29/08/2019 à 20:00, Christian Doczkal a écrit :
> Hi
>
> > Merci Christian, mais notre objectif est de spécifier une théorie pour 
> > laquelle nous avons absolument besoin d'utiliser les fonctions 
> > caractéristiques des ensembles. Cette contrainte forte nous empêche 
> > d'envisager d'autres options.
> Wait, are you saying you want to combine:
>
> 1. No classical axioms other than (some instances of) XM
we import the classical logic (Classical_Prop, PropExtensionality and 
ClassicalEpsilon)
> 2. In particular, no boolean equality test on [object], i.e., only
>     [forall a b, a = b \/ a <> b]
> 3. Sets as characteristic functions [object -> bool]
characteristic functions in the classical framework become: object -> Prop
other definitions become classically:

Inductive N : Type := Caract : (object -> Prop) -> N.

Definition caract (s :N)(a:object) : Prop := let (f) := s in f a.
Definition In (s :N)(a:object) : Prop := caract s a = True.
Definition incl (s1 s2 :N) := forall a:object, In s1 a -> In s2 a.
Definition set_eq (s1 s2 :N) := forall a:object, In s1 a = In s2 a.

All the best,
Richard
> 4. A singleton operator.
>
> This is clearly impossible since assuming a singleton operator (together with 
> the inherent decidable membership) immediately gives you a boolean equality 
> on [object]. Am I missing something here?
>
> If you don't have a boolean equality on objects, I suppose using "characteristic 
> functions" of type [object -> Prop] (with Singleton a := eq a) looks more promising. This is 
> equivalent to the "Ensembles" in the standard library, whose use I would not recommend.
>
> Best,
> Christian
>
> PS. I don't know whether taking the discussion off coq-club was intentional 
> or not. In any event, replying from a French address does not make me French. 
> :)