## Stream: maths

### Topic: Turn a set { y : Y | exists x \in A, y = f x } into (f '' A)

#### Ryan Lahfa (Apr 03 2020 at 14:15):

I often dabble with sets which are images or preimages but I'm not sure how to switch between those two forms easily, I often do quick proofs of what I mentioned in the title, which I feel sub-efficient.

I read many times the docs of sets but never found something close to those facts, I just realized that maybe it could be hidden in set.range definition. But I'm not too much up-to-date with subtypes → sets relations.

MWE?

#### Johan Commelin (Apr 03 2020 at 14:17):

@Ryan Lahfa I think that you should almost always prefer the f '' A form, and use rw set.mem_image and friends when you have things like x \in f '' A

#### Ryan Lahfa (Apr 03 2020 at 14:18):

Let's take this small working example:

import tactic
import data.real.basic
import data.real.cau_seq
import data.set
import data.set.finite
import data.finset
import order.bounds
import order.complete_lattice

variable {X: Type}

local attribute [instance] classical.prop_decidable -- on active la décidabilité partout.

def suite_st_croissante [conditionally_complete_linear_order X] {S: set X}
(Hinf: set.infinite S)
(Hset: ∀ M ⊆ S, M.nonempty → (Inf M ∈ M)) : ℕ → X :=
well_founded.fix nat.lt_wf
(λ n suite_st_croissante,
Inf (S \ { x : X | ∃ k < n, x = suite_st_croissante k H}))

def suite_st_croissante_def [conditionally_complete_linear_order X] {S: set X}
(Hinf: set.infinite S)
(Hset: ∀ M ⊆ S, M.nonempty → (Inf M ∈ M)) (n: ℕ):
suite_st_croissante Hinf Hset n = Inf (S \ { x: X | ∃ k < n, x = suite_st_croissante Hinf Hset k })
:= well_founded.fix_eq _ _ _

def suite_st_croissante_nonempty [conditionally_complete_linear_order X] {S: set X}
(Hinf: set.infinite S) (Hset: ∀ M ⊆ S, M.nonempty → (Inf M ∈ M)) (n: ℕ):
(S \ { x: X | ∃ k < n, x = suite_st_croissante Hinf Hset k }).nonempty :=
begin
set L := {x : X | ∃ (k : ℕ) (H : k < n), x = suite_st_croissante Hinf Hset k},
by_contra,
apply Hinf,
have a := set.not_nonempty_iff_eq_empty.1 a,
have := set.diff_eq_empty.1 a,
apply set.finite_subset,
have HS_finite: ∀ y: ℕ, (({x : X | ∃ (k : ℕ) (H_1 : k < y), x = suite_st_croissante Hinf Hset k}).finite) :=
begin
{
intro y,
-- this proof looks complicated for nothing.
have:
{x : X | ∃ (k : ℕ) (H_1 : k < y), x = suite_st_croissante Hinf Hset k}
= (suite_st_croissante Hinf Hset) '' { i : ℕ | i < y} := begin
ext,
split,
repeat {
intro H1,
simp at H1,
simp,
obtain ⟨ x, ⟨ hxy, heq ⟩ ⟩ := H1,
use x,
split,
exact hxy,
symmetry,
exact heq,
},
end,
rw this,
apply set.finite_image,
apply set.finite_lt_nat,
}
end,
exact HS_finite n,
exact this,
end


#### Ryan Lahfa (Apr 03 2020 at 14:19):

Johan Commelin said:

Ryan Lahfa I think that you should almost always prefer the f '' A form, and use rw set.mem_image and friends when you have things like x \in f '' A

Okay, that was the answer I was converging by what I've seen, it is just that I feel like theorem statements look weird but I shouldn't think such things of statements… :D

#### Patrick Massot (Apr 03 2020 at 14:23):

Sorry, this is not minimal enough for me. It times out here.

#### Ryan Lahfa (Apr 03 2020 at 14:26):

I'll minimize it.

import data.real.basic
import data.set

variable {X: Type}

local attribute [instance] classical.prop_decidable

def suite_st_croissante [conditionally_complete_linear_order X] {S: set X}
(Hinf: set.infinite S)
(Hset: ∀ M ⊆ S, M.nonempty → (Inf M ∈ M)) : ℕ → X :=
well_founded.fix nat.lt_wf
(λ n suite_st_croissante,
Inf (S \ { x : X | ∃ k < n, x = suite_st_croissante k H}))

lemma suite_st_croissante_images [conditionally_complete_linear_order X] {S: set X}
(Hinf: set.infinite S) (Hset: ∀ M ⊆ S, M.nonempty → (Inf M ∈ M)) (n: ℕ):
{x : X | ∃ (k : ℕ) (H_1 : k < n), x = suite_st_croissante Hinf Hset k}
= (suite_st_croissante Hinf Hset) '' { i : ℕ | i < n} :=
-- this proof looks complicated for nothing.
begin
ext,
split,
repeat {
intro H1,
simp at H1,
simp,
obtain ⟨ x, ⟨ hxy, heq ⟩ ⟩ := H1,
use x,
split,
exact hxy,
symmetry,
exact heq,
},
end


@Patrick Massot Is it better?

#### Mario Carneiro (Apr 03 2020 at 14:27):

your theorem (which should not be a def) should be trivial by simp

#### Ryan Lahfa (Apr 03 2020 at 14:27):

Mario Carneiro said:

your theorem (which should not be a def) should be trivial by simp

Replacing the body by by simp ? I just tried it and it failed to simplify.

#### Mario Carneiro (Apr 03 2020 at 14:28):

maybe apply ext first

#### Ryan Lahfa (Apr 03 2020 at 14:29):

Same, it just rewrite the (x \in A <=> x \in B) by (exists … <=> exists …)

what?

#### Ryan Lahfa (Apr 03 2020 at 14:30):

It transforms the goal which is:

x ∈ {x : X | ∃ (k : ℕ) (H_1 : k < n), x = suite_st_croissante Hinf Hset k} ↔
x ∈ suite_st_croissante Hinf Hset '' {i : ℕ | i < n}


by

(∃ (k : ℕ), k < n ∧ x = suite_st_croissante Hinf Hset k) ↔
∃ (x_1 : ℕ), x_1 < n ∧ suite_st_croissante Hinf Hset x_1 = x


#### Ryan Lahfa (Apr 03 2020 at 14:31):

which sounds finishable by refl to me…

#### Mario Carneiro (Apr 03 2020 at 14:31):

note the equality is the wrong way around

#### Patrick Massot (Apr 03 2020 at 14:31):

ext , simp [eq_comm] does it

Ah! Right

#### Patrick Massot (Apr 03 2020 at 14:31):

Yes, eq_comm is the main ingredient here

#### Ryan Lahfa (Apr 03 2020 at 14:32):

@Patrick Massot Okay, so this happens because of this equality issue and eq_comm is not a simp-lemma, should it be a simp-lemma though?

no, this is fine

#### Mario Carneiro (Apr 03 2020 at 14:33):

by ext; simp [eq_comm] is a fine proof

#### Mario Carneiro (Apr 03 2020 at 14:33):

still "trivial" in my book

#### Patrick Massot (Apr 03 2020 at 14:33):

Even better: rewrite the statement with the "correct" equality

#### Ryan Lahfa (Apr 03 2020 at 14:33):

Yes, agreed, that helped me a lot!

#### Kevin Buzzard (Apr 03 2020 at 15:05):

Ryan Lahfa said:

eq_comm is not a simp-lemma, should it be a simp-lemma though?

It would loop, wouldn't it? I think the idea is to try and keep everything in the right order :-)

#### Mario Carneiro (Apr 03 2020 at 15:06):

No, it's specifically detected to be a symmetry lemma and does something with term orders to prevent it from looping. That's why simp [eq_comm]works

#### Mario Carneiro (Apr 03 2020 at 15:07):

similar things happen with simp [add_comm] or simp [add_comm, add_assoc]

#### Mario Carneiro (Apr 03 2020 at 15:08):

Probably if you had a more elaborate symmetry like lemma like foo a b c = foo b c a then it would loop

#### Kevin Buzzard (Apr 03 2020 at 15:09):

I thought that if it was a job for add_comm and add_assoc you used something like ac_refl. Are these really confluent enough for simp? This is some inbuilt hack or something, right?

#### Mario Carneiro (Apr 03 2020 at 15:10):

Yes, I think simp calls ac_refl or the thing that drives it behind the scenes

Last updated: May 09 2021 at 10:11 UTC