## Stream: Coq users

### Topic: ✔ Coq.Sets.Ensembles inhabited

#### Jerome Hugues (Oct 03 2023 at 14:18):

Hi,

I am trying to make sense of this definition from https://coq.inria.fr/doc/V8.17.1/stdlib/Coq.Sets.Ensembles.html

``````Section Ensembles.
Variable U : Type.

Definition Ensemble := U -> Prop.

Inductive Inhabited (B:Ensemble) : Prop :=
Inhabited_intro : forall x:U, In B x -> Inhabited B.```
``````

Using a forall seems too strong, and is the definition of a full set, stated in `Full_set`.

I would have defined `Inhabited` as

``````  Inductive Inhabited (B:Ensemble) : Prop :=
Inhabited_intro : (exists x:U, In B x) -> Inhabited B.```
``````

i.e., it is sufficient to show there is at least one element for a set to be inhabited as recalled here: https://en.wikipedia.org/wiki/Inhabited_set

Am I missing something here?
Thanks

#### Karl Palmskog (Oct 03 2023 at 14:23):

I think the `forall` presentation is more standard? `exists` is not primitive.

``````  Inductive Inhabited (B:Ensemble) : Prop :=
Inhabited_intro : forall x:U, In B x -> Inhabited B.

Inductive Inhabited' (B:Ensemble) : Prop :=
Inhabited_intro' : (exists x:U, In B x) -> Inhabited' B.

Lemma Inabited_Inhabited' : forall (B:Ensemble),
Inhabited B <-> Inhabited' B.
Proof.
intros B; split; intros HB; destruct HB.
- constructor; exists x; auto.
- destruct H; exists x; auto.
Qed.
``````

#### Jerome Hugues (Oct 03 2023 at 14:31):

Hum, I get it. It is a (mental) parsing error of mine
Thanks for taking the time to build this proof. This clarified what I got wrong here.

#### Notification Bot (Oct 03 2023 at 14:31):

Jerome Hugues has marked this topic as resolved.

#### Pierre Courtieu (Oct 04 2023 at 19:11):

Indeed this is an extremely common mental parsing error: `forall x, P x -> Q x` is actually `forall x, (P x -> Q x)`, and it only takes one `x` s.t. `P x` to build a proof of `Q x`. Hence the equivalence with `(exists x, P x) -> (exists y, P y)`.

#### Ana de Almeida Borges (Oct 04 2023 at 21:12):

Note that the oposite convention is often used in math, ie, `forall x P -> Q` means `(forall x P) -> Q` in many contexts, unlike in Coq, where it means `forall x (P -> Q)`

Last updated: Jun 13 2024 at 21:01 UTC