Zulip Chat Archive

Stream: maths

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


view this post on Zulip 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.

view this post on Zulip Patrick Massot (Apr 03 2020 at 14:16):

MWE?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 03 2020 at 14:23):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Apr 03 2020 at 14:27):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 03 2020 at 14:28):

maybe apply ext first

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 14:29):

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

view this post on Zulip Mario Carneiro (Apr 03 2020 at 14:30):

what?

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 14:31):

which sounds finishable by refl to me…

view this post on Zulip Mario Carneiro (Apr 03 2020 at 14:31):

note the equality is the wrong way around

view this post on Zulip Patrick Massot (Apr 03 2020 at 14:31):

ext , simp [eq_comm] does it

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 14:31):

Ah! Right

view this post on Zulip Patrick Massot (Apr 03 2020 at 14:31):

Yes, eq_comm is the main ingredient here

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Apr 03 2020 at 14:32):

no, this is fine

view this post on Zulip Mario Carneiro (Apr 03 2020 at 14:33):

by ext; simp [eq_comm] is a fine proof

view this post on Zulip Mario Carneiro (Apr 03 2020 at 14:33):

still "trivial" in my book

view this post on Zulip Patrick Massot (Apr 03 2020 at 14:33):

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

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 14:33):

Yes, agreed, that helped me a lot!

view this post on Zulip 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 :-)

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 03 2020 at 15:07):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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