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: Oct 13 2024 at 01:02 UTC