Zulip Chat Archive

Stream: general

Topic: Infinity Hotel


view this post on Zulip Reid Barton (Sep 19 2019 at 15:46):

This Proof Ground problem is actually almost exactly a lemma I want. Would somebody (@Floris van Doorn?) like to PR a solution to mathlib?
Maybe as a mathlib lemma, it is more natural to use equiv in place of bijective, and replace the target nat by denumerable

view this post on Zulip Mario Carneiro (Sep 19 2019 at 15:58):

I discussed this with floris after the competition. I think it generalizes to embedding B < A when A is an infinite cardinal

view this post on Zulip Kevin Buzzard (Sep 19 2019 at 16:17):

Assuming AC, a+b=max(a,b) so A-B bijects with A-f(B)

view this post on Zulip Floris van Doorn (Sep 19 2019 at 18:19):

Yes, I'm going to PR this to mathlib. The current statement I am proving is

theorem extend_function_of_lt {α β : Type*} {s : set α} (f : s  β) (hs : #s < #α)
  (h : nonempty (α  β)) :  (g : α  β),  x : s, g x = f x

view this post on Zulip Floris van Doorn (Sep 19 2019 at 18:20):

Here # means cardinal.mk

view this post on Zulip Floris van Doorn (Sep 19 2019 at 18:26):

I have already proved this in the case where is infinite.

Now that I think of this, when α is infinite, I should probably replace the assumption #s < #α with the weaker condition #(-s : set α) = #α (I already proved the lemma that the former implies the latter).
EDIT: Oh wait, then it's false.

view this post on Zulip Mario Carneiro (Sep 20 2019 at 04:20):

@Kevin Buzzard Could you elaborate on that proof? a+b=a does not imply a-b=a for cardinals

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 07:21):

I was imagining the generalisation being this: if B<A is a subset, and |B|<|A|, then any injection f:B -> A can be extended to a bijection A -> A. The proof is: write C=A\B and D=A\f(B) and observe that |C|=|A|=|D|. Did I slip up?

view this post on Zulip Mario Carneiro (Sep 20 2019 at 07:39):

Those facts are all true but I'm not sure how you are arguing them

view this post on Zulip Mario Carneiro (Sep 20 2019 at 07:40):

actually you forgot to assume A is infinite, else |C|=|A| fails

view this post on Zulip Chris Hughes (Sep 20 2019 at 07:41):

I proved something similar as part of algebraic closure.

import set_theory.schroeder_bernstein

open set function
universes u v w
noncomputable theory
local attribute [instance] classical.dec

lemma thing_aux {X : Type u} {Y : Type v} {Z : Type w} (fxy : X  Y) (fxz : X  Z)
  (hYZ : (Z  Y)  false) : -range fxy.1  -range fxz.1 :=
classical.choice $ or.resolve_left embedding.total $
  λ f, hYZ $
    calc Z  range fxz  -range fxz :
      (equiv.set.sum_compl _).symm.to_embedding
    ...  range fxy  -range fxy :
      embedding.sum_congr
        (((equiv.set.range _ fxz.2).symm.to_embedding).trans
          (equiv.set.range _ fxy.2).to_embedding)
        f
    ...  Y : (equiv.set.sum_compl _).to_embedding

def thing {X : Type u} {Y : Type v} {Z : Type w} (fxy : X  Y) (fxz : X  Z)
  (hYZ : (Z  Y)  false) : Y  Z :=
calc Y  range fxy  -range fxy : (equiv.set.sum_compl _).symm.to_embedding
...  range fxz  -range fxz : embedding.sum_congr
  ((equiv.set.range _ fxy.2).symm.to_embedding.trans
    (equiv.set.range _ fxz.2).to_embedding)
  (thing_aux fxy fxz hYZ)
...  Z : (equiv.set.sum_compl _).to_embedding

lemma thing_commutes {X : Type u} {Y : Type v} {Z : Type w}  (fxy : X  Y) (fxz : X  Z)
  (hYZ : (Z  Y)  false) (x : X) : thing fxy fxz hYZ (fxy x) = fxz x :=
have (fxy x, mem_range_self _⟩ : range fxy) = equiv.set.range _ fxy.2 x, from rfl,
begin
  dsimp only [thing, embedding.trans_apply, equiv.trans_apply, function.comp,
    equiv.to_embedding_coe_fn],
  simp only [equiv.set.sum_compl_symm_apply_of_mem (mem_range_self _),
    embedding.sum_congr_apply_inl, equiv.set.sum_compl_apply_inl,
    embedding.trans_apply, equiv.to_embedding_coe_fn, this, equiv.symm_apply_apply],
  refl
end

view this post on Zulip Chris Hughes (Sep 20 2019 at 07:43):

Somehow the assumption (Z ↪ Y) → false should be turned into (Z ↪ X) → false

view this post on Zulip Mario Carneiro (Sep 20 2019 at 07:43):

isn't that just transitivity?

view this post on Zulip Mario Carneiro (Sep 20 2019 at 07:46):

@Kevin Buzzard I think your proof sketch is basically what floris did in the competition

view this post on Zulip Mario Carneiro (Sep 20 2019 at 07:47):

it would be nice to reduce it to a one liner of mathlib lemmas though

view this post on Zulip Mario Carneiro (Sep 20 2019 at 07:50):

Unfortunately I don't see how to apply chris's lemma directly here

view this post on Zulip Mario Carneiro (Sep 20 2019 at 07:51):

it only seems to construct an injection from Y to Z where |Y|<|Z|, and the only obvious candidates are Y=B and Z=A, or Y=f(B) and Z=A, and neither is particularly helpful

view this post on Zulip Mario Carneiro (Sep 20 2019 at 07:54):

In this situation, we want Y=Z=A, but then (Z ↪ Y) → false fails

view this post on Zulip Chris Hughes (Sep 20 2019 at 07:56):

But in the infinite case can we weaken the assumption to (Z ↪ X) → false?

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 07:57):

@Mario Carneiro I don't understand why you're calling it a sketch ;-)

view this post on Zulip Mario Carneiro (Sep 20 2019 at 07:57):

you have to reference actual theorems, and also prove the side conditions

view this post on Zulip Mario Carneiro (Sep 20 2019 at 07:58):

ideally the formal proof should actually be that short, but the side conditions are messy here

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 07:58):

The argument would convince any mathematician. That's the level where we operate. What we really need is an interface where I can just say what I said to you and then let tactics do the rest.

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 07:59):

we can try cases, refl on the side conditions or whatever. It's all noise.

view this post on Zulip Mario Carneiro (Sep 20 2019 at 07:59):

you also didn't prove what you claimed to... there are lots of issues with treating that literally as a proof

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 08:00):

Can you give me specific examples of issues? I'd be happy to talk about this but I have to run

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 08:00):

I think my proof is "math-complete"

view this post on Zulip Mario Carneiro (Sep 20 2019 at 08:00):

it's absolutely a sketch, but it's enough hints for a competent mathematician to fill in the rest of the proof

view this post on Zulip Mario Carneiro (Sep 20 2019 at 08:00):

but you should never confuse "enough to communicate the main ideas" with "proof"

view this post on Zulip Johan Commelin (Sep 20 2019 at 08:01):

Isn't that the definition of proof?

view this post on Zulip Mario Carneiro (Sep 20 2019 at 08:02):

for one thing, communication depends on the target audience; computers should be treated as a particularly dumb student

view this post on Zulip Mario Carneiro (Sep 20 2019 at 08:04):

it is not really possible to give an actual definition of "proof" if you take that position seriously... in the limit, anything that is logically derivable can be considered "proof by trivial"

view this post on Zulip Mario Carneiro (Sep 20 2019 at 08:06):

This is trending philosophical, but one property I want the word "proof" to have is that it's objective or at least societally defined, whereas "communication" is context dependent

view this post on Zulip Mario Carneiro (Sep 20 2019 at 08:09):

Really, I prefer to just sidestep the whole matter and only talk about formal proof, which has a proper definition, but it makes it difficult for me to interpret Kevin when he wants a raised eyebrow to constitute a valid proof

view this post on Zulip Patrick Massot (Sep 20 2019 at 08:21):

It depends whose eyebrow it is.

view this post on Zulip Mario Carneiro (Sep 20 2019 at 08:53):

Here's the closest I got to Kevin's sketch, modulo the cardinality fact:

import set_theory.cardinal

local prefix `#` := cardinal.mk
theorem mk_eq_mk {α β} (h : α  β) : #α = #β := quotient.sound h
theorem foo {α} {S : set α} (h : #S < #α) : #(-S : set α) = #α := sorry

example {X Y Z} (f : X  Y) (g : X  Z) (h₁ : #X < #Y) (h₂ : #Y = #Z) :
   e : Y  Z,  x, e (f x) = g x :=
begin
  have e1 : #(-set.range f : set _) = #Y := foo (by rwa [ mk_eq_mk (equiv.set.range f f.2)]),
  have e2 : #(-set.range g : set _) = #Z := foo (by rwa [ h₂,  mk_eq_mk (equiv.set.range g g.2)]),
  rw [h₂,  e2] at e1,
  cases quotient.exact e1 with e1,
  classical,
  refine (equiv.set.sum_compl _).symm.trans ((equiv.sum_congr _ e1).trans (equiv.set.sum_compl _)), λ x, _⟩,
  { exact (equiv.set.range f f.2).symm.trans (equiv.set.range g g.2) },
  { simp [equiv.set.sum_compl_symm_apply_of_mem, set.mem_range_self],
    rw (equiv.symm_apply_eq _).2, simp }
end

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 09:18):

the cardinal fact is proved like this: If b<a then a=b+(a-b)=max(b,a-b), hence a-b=a.

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 09:19):

Maybe some automatic theorem prover can find that fact about cardinals given what is in mathlib?

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 09:22):

I'm taking a look at your proof. It's annoying that hovering over equiv.set.sum_compl doesn't show me its type -- I think this is because we're in tactic mode.

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:30):

Note that the cardinal fact as I've stated it is false, so if you think you have proved it you should not trust your proof

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:31):

it would be pretty difficult to get nitpick or whatever counterexample generator to find why the statement is false too

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:32):

actually scratch that - the problem is with finite sets so they can probably handle it

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:34):

In chris's proof he uses calc blocks instead to build the equivs, which looks a bit nicer

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 09:34):

I thought we were talking about the infinite case now. All this a+b=max(a,b) is only true in the infinite case, I've been assuming infinite.

Your proof is extraordinary.

⊢ ⇑(equiv.trans (equiv.symm (equiv.set.sum_compl (set.range ⇑f)))
         (equiv.trans (equiv.sum_congr (equiv.trans (equiv.symm (equiv.set.range ⇑f _)) (equiv.set.range ⇑g _)) e1)
            (equiv.set.sum_compl (set.range ⇑g))))
      (⇑f x) =
    ⇑g x

We prove this by saying "...and the diagram obviously commutes". What is going on? This is trivial stuff.

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:35):

there are side conditions

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 09:35):

I can prove this whole thing by drawing one picture.

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:35):

no, you can state the problem by drawing a picture

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 09:36):

There aren't any side conditions. Assuming foo, we can prove the existence theorem. This is a really great example of a proof which can be done by a simple picture.

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:36):

The only thing I wrote in the proof are side conditions

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:36):

everything else is indeed being handled by simp

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 09:36):

wow

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:37):

The proof sketch you gave me essentially covers the first two lines of the proof

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:37):

you never said what the bijection is or how to build it

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:38):

that's all "type tetris"

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:38):

with side conditions in the middle of it all

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:40):

I think side conditions are the bane of any theorem prover, because there is no good way to write them, which makes it easy to ignore them for expositional purposes in math

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 09:42):

IMG_20190920_104043021.jpg

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 09:44):

Where is equiv.set.sum_compl_symm_apply_of_mem in my picture? What is going on?

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:44):

Where's the bijection? I'm not even sure where f is in the picture

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 09:44):

Two down arrows are f and g.

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 09:45):

The bijection is because I identified the two sets Y and Z, the top halves are the same, and the bottom halves biject by a trivial lemma which I proved elsewhere on the board.

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:45):

equiv.set.sum_compl_symm_apply_of_mem says that if you are on the top half of the picture then you can go from y to the top half of y

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 09:45):

I am working in the category of sets equipped with a map from X, so somehow the commutativity of the diagrams just all gets swallowed up by the machine.

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 09:46):

Maybe I am using some better structure than you.

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:46):

in lean there are two additional points in the picture, Y and Z

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:47):

and maps from Y to the parts of Y

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 09:47):

Aah, this is one of these instances where a mathematician thinks "set-theoretically" and all these issues melt away.

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:47):

sure I'd love to do that, but DTT

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 09:47):

(all the maps become the identity map in some sense)

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:48):

actually it doesn't really solve anything, it just removes the function equiv.set.sum_compl_symm_apply_of_mem and leaves the side condition

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 09:48):

Are we missing a tactic which does arguments like this?

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:48):

meh

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:48):

"like this" is never enough

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:49):

I generalize from >1 example

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 09:49):

given that Y \ f(X) bijects with Z \ g(X), figure out the rest yourself. Is that too much for an AI?

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:49):

Probably not

view this post on Zulip Mario Carneiro (Sep 20 2019 at 09:50):

I can imagine an SMT prover can get this, but when it's all embedded in lean some things get obscured


Last updated: May 14 2021 at 07:19 UTC