Stream: Coq users

Topic: ✔ Coq.Sets.Ensembles inhabited


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Notification Bot (Oct 03 2023 at 14:31):

Jerome Hugues has marked this topic as resolved.

view this post on Zulip 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).

view this post on Zulip 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: Oct 13 2024 at 01:02 UTC