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.

Karl Palmskog (Nov 07 2021 at 13:55):

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

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