Stream: Coq users

Topic: Ensemble image

Quinn (Nov 07 2021 at 12:03):

Definition Image {A B} (X : Ensemble A) (f : A -> B) : Ensemble B
  :=
    fun y => exists x, X x /\ y = f x.

Theorem Image_sanity : Same_set _ (fun x => 10 <= x <= 20) (Image (fun x => 0 <= x <= 10) (fun x => x + 10)).
Proof.
  unfold Same_set, Included, In, Image.
  split; intros y Hy.
  - exists (y - 10).
    split; lia.
  - destruct Hy as [x Hy].
    lia.
Qed.

in constructive math can I find an image while under uncertainty about the inverse? I was a little surprised and annoyed that I needed to know the inverse in order to do this proof about my image implementation, and it implies that i'd be limited in working with images for unknown f

Gaëtan Gilbert (Nov 07 2021 at 12:19):

from that theorem you can derive forall y, 10 <= y <= 20 -> exists x, 0 <= x <= 10 /\ y = x + 10
so you need the inverse up to exists

Quinn (Nov 07 2021 at 12:28):

is there a particular reason Ensemble Image isn't in standard library?

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

the standard library is in general not very standard or complete. I'd recommend looking at alternative set libraries, such as those in Stdpp and finmap

Last updated: Oct 13 2024 at 01:02 UTC