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

Stream: maths

[Ryan Lahfa]

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.

[Patrick Massot]

MWE?

[Johan Commelin]

@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]

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]

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]

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

[Ryan Lahfa]

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]

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

[Ryan Lahfa]

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]

maybe apply ext first

[Ryan Lahfa]

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

[Mario Carneiro]

what?

[Ryan Lahfa]

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]

which sounds finishable by refl to me…

[Mario Carneiro]

note the equality is the wrong way around

[Patrick Massot]

ext , simp [eq_comm] does it

[Ryan Lahfa]

Ah! Right

[Patrick Massot]

Yes, eq_comm is the main ingredient here

[Ryan Lahfa]

@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?

[Mario Carneiro]

no, this is fine

[Mario Carneiro]

by ext; simp [eq_comm] is a fine proof

[Mario Carneiro]

still "trivial" in my book

[Patrick Massot]

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

[Ryan Lahfa]

Yes, agreed, that helped me a lot!

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

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]

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]

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