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

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.
```

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.

Jerome Hugues has marked this topic as resolved.

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)`

.

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