golfing challenge

Stream: general

[Adam Topaz]

Is there a one line proof of this?

import data.fin

example {α : Type*} (f g : α → fin 2) : f ⁻¹' ({0} : set (fin 2)) = g ⁻¹' {0} → f = g := sorry

[Johan Commelin]

This is just over the 100 character limit:

import tactic
import data.fin

local attribute [simp] set.ext_iff

example {α : Type*} (f g : α → fin 2) : f ⁻¹' ({0} : set (fin 2)) = g ⁻¹' {0} → f = g :=
λ H, by simp at H; ext; have := H x; set y := f x; set z := g x; fin_cases y; fin_cases z; simp * at *
--λ H, by simp at H; ext; specialize H x; set y := f x; set z := g x; fin_cases y; fin_cases z; simp * at *

[Johan Commelin]

I wish we had sets [y,z] [f x, g x]. Also fin_cases * doesn't work as I expected.

[Johan Commelin]

Golfed specialize down to have :=

[Johan Commelin]

Is it ok to move the hypothesis to the left of the colon?

[Johan Commelin]

import tactic
import data.fin

local attribute [simp] set.ext_iff

example {α : Type*} (f g : α → fin 2) (H : f ⁻¹' ({0} : set (fin 2)) = g ⁻¹' {0}) : f = g :=
by simp at H; ext; have := H x; set y := f x; set z := g x; fin_cases y; fin_cases z; simp * at *

[Johan Commelin]

That's now < 100 chars

[Adam Topaz]

Nice!

[Johan Commelin]

I wish fin_cases [f x, g x] would work. That would avoid the sets.

[Adam Topaz]

yeah that would be nice.

[Johan Commelin]

Moving the have after the two sets breaks the proof :head_bandage:

[Johan Commelin]

Turning have into set or let doesn't work either.

[Alex J. Best]

Johan Commelin said:

I wish we had sets [y,z] [f x, g x]. Also fin_cases * doesn't work as I expected.

In term mode let x := 1, y := 2 works, but in tactic mode the comma is seen as next tactic, maybe a bracketed version of this would be good though set [x := 1, y := 2]?

[Adam Topaz]

A variant of @Johan Commelin 's proof is now part of #7954

[Yakov Pechersky]

Might be easier to do this for bool (can just use cases on the bool val), and use the fin 2 to bool iso

[Johan Commelin]

From LTE. I can't believe this proof is optimal, but I don't see a better proof either.

import data.real.basic

lemma real.Sup_mul (r : ℝ) (s : set ℝ) (hr : 0 < r) :
  Sup ({x | ∃ y ∈ s, r * y = x}) = r * Sup s :=
begin
  let P₁ : Prop := (∃ (x : ℝ), x ∈ {x : ℝ | ∃ (y : ℝ) (H : y ∈ s), r * y = x}) ∧
    ∃ (x : ℝ), ∀ (y : ℝ), y ∈ {x : ℝ | ∃ (y : ℝ) (H : y ∈ s), r * y = x} → y ≤ x,
  let P₂ : Prop := (∃ (x : ℝ), x ∈ s) ∧ ∃ (x : ℝ), ∀ (y : ℝ), y ∈ s → y ≤ x,
  have H : P₁ ↔ P₂ := _,
  { by_cases h : P₁,
    { apply le_antisymm,
      { rw real.Sup_le _ h.1 h.2,
        rintro _ ⟨x, hx, rfl⟩,
        apply mul_le_mul_of_nonneg_left _ hr.le,
        rw H at h,
        exact real.le_Sup _ h.2 hx },
      { rw H at h,
        rw [← le_div_iff' hr, real.Sup_le _ h.1 h.2],
        intros x hx,
        rw le_div_iff' hr,
        rw ← H at h,
        exact real.le_Sup _ h.2 ⟨_, hx, rfl⟩ } },
    { simp only [real.Sup_def],
      classical,
      rw [dif_neg, dif_neg, mul_zero],
      { rw H at h, exact h }, { exact h } } },
  { apply and_congr,
    { simp only [exists_prop, set.mem_set_of_eq],
      rw exists_comm,
      simp only [and_comm, exists_eq_left'] },
    { simp only [exists_prop, set.mem_set_of_eq, and_comm],
      simp only [exists_eq_left', mul_comm r, ← div_eq_iff_mul_eq hr.ne.symm],
      split; rintro ⟨x, hx⟩,
      { refine ⟨x / r, λ y hy, _⟩,
        rw ← mul_div_cancel y hr.ne.symm at hy,
        rw le_div_iff hr,
        exact hx _ hy },
      { refine ⟨r * x, λ y hy, _⟩,
        rw ← div_le_iff' hr,
        exact hx _ hy } } },
end

[Kevin Buzzard]

This is a bit shorter and a bit less gnarly but it's still pretty long:

import data.real.basic

lemma foo {a b c : ℝ} (ha : 0 < a) : b ≤ a⁻¹ * c ↔ a * b ≤ c :=
begin
  rw [mul_comm a, mul_comm, ←le_div_iff ha],
  refl,
end

lemma real.Sup_mul (r : ℝ) (s : set ℝ) (hr : 0 < r) :
  Sup ({x | ∃ y ∈ s, r * y = x}) = r * Sup s :=
begin
  by_cases hb : bdd_above s,
  swap, { -- unbounded case
    rw [real.Sup_of_not_bdd_above hb, mul_zero, real.Sup_of_not_bdd_above],
    rintro ⟨B, hB⟩,
    refine hb ⟨r⁻¹ * B, λ t ht, _⟩,
    rw foo hr,
    exact hB ⟨t, ht, rfl⟩ },
  have hrb : bdd_above {x : ℝ | ∃ (y : ℝ) (H : y ∈ s), r * y = x},
  { rcases hb with ⟨B, hB⟩,
    refine ⟨r * B, _⟩,
    rintro _ ⟨y, hys, rfl⟩,
    rw mul_le_mul_left hr,
    exact hB hys },
  by_cases hs : s.nonempty,
  swap, { -- empty case
    rw set.not_nonempty_iff_eq_empty at hs,
    simp [hs, real.Sup_empty] },
  apply le_antisymm,
  { cases hs with t ht,
    rw cSup_le_iff hrb ⟨r * t, t, ht, rfl⟩,
    rintros b ⟨y, hys, rfl⟩,
    rw mul_le_mul_left hr,
    exact le_cSup hb hys },
  { rw ← foo hr,
    apply cSup_le hs,
    rintros b hbs,
    rw foo hr,
    exact le_cSup hrb ⟨b, hbs, rfl⟩ },
end

[Kevin Buzzard]

The problem (for those idly watching on) is that basically the definition of "Sup S" is "if S is empty or unbounded it's zero, else it's what a mathematician would call Sup S" so I had to break into three cases.

[Eric Wieser]

It feels like we're missing a cSup_image lemma:

import data.real.basic

lemma real.Sup_mul (r : ℝ) (s : set ℝ) (hr : 0 < r) :
  Sup ({x | ∃ y ∈ s, r * y = x}) = r * Sup s :=
begin
  simp_rw exists_prop,
  change Sup (((*) r) '' s) = r * Sup s,
  have : monotone ((*) r) := λ a b h, (mul_le_mul_left hr).mpr h,
  set f := ((*) r),
  sorry,
  /-
  this: monotone f
  ⊢ Sup (f '' s) = f (Sup s)
  -/
end

[Patrick Massot]

Eric, you haven't read Kevin's message carefully enough

[Patrick Massot]

The lemma you have in mind is wrong. Counter-example: f maps x to x+1 and s = univ.

[Patrick Massot]

You need to add the assumption that f preserves zero and something like f '' s is bounded iff s is bounded. Yes, it's a pain, that's the point.

[Eric Wieser]

Here's the version I'm thinking of:

lemma cSup_image {α β}
  [conditionally_complete_linear_order α] [conditionally_complete_lattice β]
  (s : set α) (hs : bdd_above s) (hs' : s.nonempty)
  (f : α → β) (hf : monotone f) : Sup (f '' s) = f (Sup s) :=
begin
  have := hf.map_bdd_above hs,
  apply le_antisymm,
  { apply hf.cSup_image_le hs',
    rw mem_upper_bounds,
    intros x hx,
    apply le_cSup hs hx, },
  apply hf.le_cSup_image _ hs,
  sorry -- `Sup s ∈ s` - is this true, given we have a linear order?
end

lemma foo {a b c : ℝ} (ha : 0 < a) : b ≤ a⁻¹ * c ↔ a * b ≤ c :=
begin
  rw [mul_comm a, mul_comm, ←le_div_iff ha],
  refl,
end

lemma real.Sup_mul' (r : ℝ) (s : set ℝ) (hr : 0 < r) :
  Sup ({x | ∃ y ∈ s, r * y = x}) = r * Sup s :=
begin
  by_cases hb : bdd_above s,
  swap, { -- unbounded case
    rw [real.Sup_of_not_bdd_above hb, mul_zero, real.Sup_of_not_bdd_above],
    rintro ⟨B, hB⟩,
    refine hb ⟨r⁻¹ * B, λ t ht, _⟩,
    rw foo hr,
    exact hB ⟨t, ht, rfl⟩ },
  by_cases hs : s.nonempty,
  swap, { -- empty case
    rw set.not_nonempty_iff_eq_empty at hs,
    simp [hs, real.Sup_empty] },
  simp_rw exists_prop,
  have : monotone ((*) r) := λ a b h, (mul_le_mul_left hr).mpr h,
  apply cSup_image s hb hs _ this,
end

I don't know whether that sorry is true

[Johan Commelin]

sorry looks false to me: bounded subsets of reals don't need to contain their Sup

[Johan Commelin]

Take (0, x). The Sup is x, but not contained in the open interval

[Yaël Dillies]

Yeah otherwise everything would have a maximal element.

[Eric Wieser]

Does cSup_image look true, even if my proof went in a bad direction?

[Patrick Massot]

No, it doesn't

[Eric Wieser]

Alright, in that case I back down my cSup_image suggestion, and just offer a golfed version of Kevin's proof (keeping his foo):

lemma real.Sup_mul'' (r : ℝ) (s : set ℝ) (hr : 0 < r) :
  Sup ({x | ∃ y ∈ s, r * y = x}) = r * Sup s :=
begin
  simp_rw exists_prop,
  change Sup (((*) r) '' s) = r * Sup s,
  by_cases hb : bdd_above s,
  swap, { -- unbounded case
    rw [real.Sup_of_not_bdd_above hb, mul_zero, real.Sup_of_not_bdd_above],
    rintro ⟨B, hB⟩,
    refine hb ⟨r⁻¹ * B, λ t ht, _⟩,
    rw foo hr,
    exact hB ⟨t, ht, rfl⟩ },
  have hm : monotone ((*) r) := λ a b h, (mul_le_mul_left hr).mpr h,
  have hrb := hm.map_bdd_above hb,
  by_cases hs : s.nonempty,
  swap, { -- empty case
    rw set.not_nonempty_iff_eq_empty at hs,
    simp [hs, real.Sup_empty] },
  apply le_antisymm,
  { apply hm.cSup_image_le hs,
    intros x,
    apply le_cSup hb, },
  { rw ← foo hr,
    apply cSup_le hs,
    rintros b hbs,
    rw foo hr,
    exact le_cSup hrb ⟨b, hbs, rfl⟩ },
end

[Patrick Massot]

This is soo painful. This kind of proof is a really cruel example of how far we are from having a usable tool. Where is AI when we need it?

[Eric Wieser]

Is this an example of cSup / docs#conditionally_complete_linear_order being too weird a definition to have a generalizable API?

[Eric Wieser]

Eg the fact that we don't have a typeclass that says Sup s = 0 if s is not bounded / empty. Maybe the only instance where that's true is the reals though anyway, I think the other instances all have a bot.

[Ruben Van de Velde]

This generalizes out the multiplication, at least (slightly cleaned up):

import data.real.basic

lemma real.Sup_image (s : set ℝ) (f : ℝ ≃o ℝ) (hf' : f 0 = 0):
  Sup (f '' s) = f (Sup s) :=
begin
  by_cases hb : bdd_above (f '' s),
  swap, { -- unbounded case
    rw [real.Sup_of_not_bdd_above hb, real.Sup_of_not_bdd_above, hf'],
    contrapose! hb,
    apply f.monotone.map_bdd_above hb },

  have hrb : bdd_above s,
  { convert monotone.map_bdd_above f.symm.monotone hb,
    ext,
    simp },

  by_cases hs : s.nonempty,
  swap, { -- empty case
    rw set.not_nonempty_iff_eq_empty at hs,
    simp [hs, real.Sup_empty, hf'], },

  apply le_antisymm,
  { cases hs with t ht,
    rw cSup_le_iff hb ⟨f t, t, ht, rfl⟩,
    rintros b ⟨y, hys, rfl⟩,
    exact f.monotone (le_cSup hrb hys) },
  { rw ←f.apply_symm_apply (Sup (f '' s)),
    apply f.monotone,
    apply cSup_le hs,
    intros b hb,
    convert f.symm.monotone (f.monotone.le_cSup_image hb hrb),
    simp },
end

lemma real.Sup_mul (r : ℝ) (s : set ℝ) (hr : 0 < r) :
  Sup ({x | ∃ y ∈ s, r * y = x}) = r * Sup s :=
begin
  set S := ((*) r) '' s with hS,
  have : S = {x | ∃ y ∈ s, r * y = x},
  { ext, simp, },
  rw [←this, hS],
  let ff : ℝ ≃o ℝ := {
    to_fun := ((*) r),
    inv_fun := ((*) r⁻¹),
    left_inv := _,
    right_inv := _,
    map_rel_iff' := _
  },
  refine real.Sup_image s ff _,
  { simp },
  { intros x, simp [hr.ne'] },
  { intros x, simp [hr.ne'] },
  { intros a b, simp [mul_le_mul_left hr] }
end

[Kevin Buzzard]

Patrick Massot said:

This is soo painful. This kind of proof is a really cruel example of how far we are from having a usable tool. Where is AI when we need it?

I claim that the reason it's painful is that we spend a lot of time dealing with the junk case where Sup(S) is meaningless and it coincidentally happens to be the case that the lemma is true anyway -- this is precisely what hurts Eric's approach, where a more conceptual lemma is not true because it fails in the junk cases. However Johan is a mathematician so presumably only cares about this lemma in the case where Sup(S) is not junk, in which case the proof is just those last 8 lines of Eric's proof and looks far more reasonable. So whilst I agree with you that in some sense this is a problem with the tool, the problem is that we mathematicians now have taken on board this whole "garbage in garbage out" approach with our definitions and are trying to prove lemmas which are easier for people to use, and harder to prove.

I think the real question is: take Eric's abstraction about monotone functions and sups, and now add in the hypotheses that the set is nonempty and bounded. Then the abstraction becomes true, the proof will be short, and it looks useful to me. Is this good enough for Johan's application? I bet it is.

[Kevin Buzzard]

Argument from CS people: "the great thing about garbage-in garbage-out defs is that sometimes stuff is true without side conditions! For example a/b + c/b = (a+c)/b is true without assuming b=0! This is a big win!". Mathematician: "...but I have hb : b != 0 in my local context anyway"

[Johan Commelin]

Is this good enough for Johan's application? I bet it is.

Yes it is. But it shifts the burden, as you say yourself:

prove lemmas which are easier for people to use, and harder to prove.

[Kevin Buzzard]

We all agree that it's cute that / can be extended to all of the reals, however it extends to a junk function which mathematicians have no use for most of the time apart from super-low-level stuff, so will not show up at all after some point (in the sense that hb : b != 0 will always be there)

[Johan Commelin]

Because it means that I have to do the painful checking that my input is not garbage at the place where I want to apply the lemma. And at that point I really don't want to be bothered by those "silly" side conditions.

[Kevin Buzzard]

So you're saying that you _don't_ have the handy hypotheses that S is nonempty and bounded above in your local context, even though they're going to be there in the mathematical source you're formalising?

[Johan Commelin]

Let me check exactly what I have

[Kevin Buzzard]

If this is a serious problem for you then probably one should push ahead with Eric's abstraction

[Johan Commelin]

The norm of a locally constant function is the Sup norm. But if the range is empty or unbounded...

[Kevin Buzzard]

There should perhaps be a "one size fits all" lemma of the form "to prove some theorem about Sups, it suffices to prove it when all the sets are nonempty and bounded above, and also that it works for 0" (except I am currnetly unclear how one manages the situation we have here, where there are two sets and it's a cute lemma that one is empty/unbounded iff the other one is), and then use the mono lemma for the sensible case...oh crap the mono lemma isn't even true in the unbounded case of course, it needs continuity as well

[Johan Commelin]

So, we are on a compact space, so it cannot be unbounded. But it can still be empty.

[Kevin Buzzard]

Mathematically, the sup of an empty collection of norms is the sup of the empty set in nnreal so it really is 0

[Johan Commelin]

Maybe we should embrace nnreal a bit more.

[Kevin Buzzard]

The analysts seem to have thought hard about where to use it (e.g. they don't want to use it for metric spaces but do want to use it for some measure theory)

[Johan Commelin]

See https://github.com/leanprover-community/lean-liquid/blob/master/src/prop_92/concrete.lean#L58L127 for a bit more pain

[Patrick Massot]

Kevin, the issue is not only that S can be unbounded, it's also that S can be bounded and f(S) unbounded.

[Eric Wieser]

If f is a A ≃o A as in @Ruben Van de Velde's version then docs#monotone.map_bdd_above means that f(S) and S are both bounded, right?

[Kevin Buzzard]

Aah interesting -- Patrick and I are thinking of maps like y=tan(x) which send the bounded region (-pi/2,pi/2) to an unbounded region, but tan is not defined on all of the reals.

[Floris van Doorn]

Another issue with the latest proposed cSup_image lemma is that f can be discontinuous at Sup x: s = {x : ℝ | x < 0} and f = real.sign.

[Eric Wieser]

Here's a generalized version of @Ruben Van de Velde's:

import data.real.basic

lemma order_iso.cSup_image
  {α β} [conditionally_complete_lattice α] [conditionally_complete_lattice β]
  (f : α ≃o β) (s : set α) (hs : bdd_above s) (hs' : s.nonempty):
  Sup (f '' s) = f (Sup s) :=
begin
  apply le_antisymm,
  { apply f.monotone.cSup_image_le hs',
    intro x,
    apply le_cSup hs },
  { rw ←f.apply_symm_apply (Sup (f '' s)),
    apply f.monotone,
    apply cSup_le hs',
    intros b hb,
    convert f.symm.monotone (f.monotone.le_cSup_image hb hs),
    rw f.symm_apply_apply, },
end

lemma real.Sup_image (s : set ℝ) (f : ℝ ≃o ℝ) (hf' : f 0 = 0):
  Sup (f '' s) = f (Sup s) :=
begin
  by_cases hb : bdd_above (f '' s),
  swap, { -- unbounded case
    rw [real.Sup_of_not_bdd_above hb, real.Sup_of_not_bdd_above, hf'],
    contrapose! hb,
    apply f.monotone.map_bdd_above hb },

  have hrb : bdd_above s,
  { convert monotone.map_bdd_above f.symm.monotone hb,
    ext,
    simp },

  by_cases hs : s.nonempty,
  swap, { -- empty case
    rw set.not_nonempty_iff_eq_empty at hs,
    simp [hs, real.Sup_empty, hf'], },

  exact f.cSup_image s hrb hs,
end

/-- `equiv.mul_left'` as an order_iso. TODO: add this for all the other equivs too. -/
@[simps {simp_rhs := tt}]
def order_iso.mul_left' {K} [linear_ordered_field K] (k : K) (hk : 0 < k) : K ≃o K :=
{ map_rel_iff' := λ a b, mul_le_mul_left hk,
  ..equiv.mul_left' k hk.ne' }

lemma real.Sup_mul (r : ℝ) (s : set ℝ) (hr : 0 < r) :
  Sup ({x | ∃ y ∈ s, r * y = x}) = r * Sup s :=
begin
  simp_rw exists_prop,
  refine real.Sup_image s (order_iso.mul_left' r hr) (mul_zero _),
end

[Eric Wieser]

My guess would be that mul_left_iso already exists somewhere. Yep: docs#equiv.mul_left'

[Floris van Doorn]

@Johan Commelin the first lemma is docs#set.nonempty.cSup_mem

[Eric Wieser]

#8150 adds order_iso.mul_left' and similar defintions