## Stream: Coq users

### Topic: Ensembles

#### Quinn (Nov 06 2021 at 18:10):

I'm suspecting this isn't provable

``````Lemma Ensemble_Empty_Nonempty {A} (X : Ensemble A) : Same_set _ (Empty_set _) X \/ exists (x : A), X x.
``````

what's the story as to why?

Alternatively, what's the proof? I struggled with it enough and it's a subgoal of another project i'm doing

#### Paolo Giarrusso (Nov 06 2021 at 18:12):

You'd probably need to assume excluded middle, and use it to "test" whether `exists (x : A), X x.` holds or not.

#### Paolo Giarrusso (Nov 06 2021 at 18:15):

_without_ excluded middle or other axioms, you're in constructive logic, so to prove this you'd need a total algorithm that figures out which of the cases applies.

#### Paolo Giarrusso (Nov 06 2021 at 18:18):

With such an algorithm, you could compute whether `A` is empty (pick `X := Full_set`), which should let you decide the halting problem.

#### Quinn (Nov 07 2021 at 13:14):

I was thinking of doing basic list fp on ensembles, but it wasn't going well

#### Quinn (Nov 07 2021 at 13:14):

``````Inductive Map {A B} : (A -> B) -> Ensemble A -> Ensemble B -> Prop :=
| Map_Empty : forall f, Map f (Empty_set A) (Empty_set B)
| Map_Induc : forall f (X : Ensemble A) x, X x -> Map f X (fun y => y = f x).
``````

#### Quinn (Nov 07 2021 at 13:14):

``````Inductive SemigroupFold {A} : (A -> A -> A) -> A -> Ensemble A -> A -> Prop :=
| SGFold_Empty : forall f init, SemigroupFold f init (Empty_set A) init
| SGFold_Induc : forall f (X : Ensemble A) x init, X x -> SemigroupFold f init (Subtract _ X x) (f init x).
``````

#### Paolo Giarrusso (Nov 07 2021 at 13:51):

Ensemble is contravariant, so Haskell's contramap is likely easier to write, but you probably want a collection that lists elements instead of letting you test them, see alternative library suggestions.

#### Quinn (Nov 07 2021 at 14:05):

What do you mean "see alternative library suggestions"?

#### Quinn (Nov 07 2021 at 14:05):

oh you mean Karl's comment in the `Image` thread.

#### Quinn (Nov 07 2021 at 14:05):

great, thanks

Last updated: Jun 25 2024 at 18:02 UTC