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

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

holds or not.

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

With such an algorithm, you could compute whether `A`

is empty (pick `X := Full_set`

), which should let you decide the halting problem.

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

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

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

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.

isn't this similar to Haskell's contramap? https://github.com/jwiegley/coq-haskell/blob/master/src/Data/Functor/Contravariant.v

What do you mean "see alternative library suggestions"?

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

thread.

great, thanks

Last updated: Sep 23 2023 at 07:01 UTC