Zulip Chat Archive

Stream: maths

Topic: constructive zerology


view this post on Zulip Patrick Massot (Jul 17 2018 at 14:59):

@Kenny Lau I have a question for you. Do you have a proof without decidable or classical of:

lemma closure_empty_iff {α : Type*} [topological_space α] [decidable_eq (set α)] (s : set α) :
closure s =   s =  :=
begin
  split ; intro h,
  { by_contradiction h',
    cases set.not_eq_empty_iff_exists.1 h' with _ H,
    simpa [h] using subset_closure H },
  { exact (eq.symm h)  closure_empty },
end

view this post on Zulip Reid Barton (Jul 17 2018 at 15:06):

Use set.eq_empty_iff_forall_not_mem instead I think

view this post on Zulip Kenny Lau (Jul 17 2018 at 15:11):

for this case, contradiction is intuitionistically valid

view this post on Zulip Patrick Massot (Jul 17 2018 at 15:12):

Thanks Reid!

view this post on Zulip Patrick Massot (Jul 17 2018 at 15:12):

lemma closure_empty_iff {α : Type*} [topological_space α] (s : set α) :
closure s =   s =  :=
begin
  split ; intro h,
  { rw set.eq_empty_iff_forall_not_mem,
    intros x H,
    simpa [h] using subset_closure H },
  { exact (eq.symm h)  closure_empty },
end

view this post on Zulip Patrick Massot (Jul 17 2018 at 15:14):

I'm very slowly working towards proving that the Hausdorff completion of a uniform space X is nonempty unless X is empty. This is no fun at all.

view this post on Zulip Patrick Massot (Jul 17 2018 at 15:24):

I can feel the dreaded spiral where I'm upset something is not obvious to Lean and I'm proving more and more stupid lemmas instead of cooling down and figure out what I exactly need

view this post on Zulip Patrick Massot (Jul 17 2018 at 15:32):

I need a break. If anyone here is bored and loves zerology, I think I may need proofs of:

lemma nonempty_iff_univ {α : Type*} : nonempty α  (univ : set α)   :=
sorry

lemma nonempty_of_nonempty_range {α : Type*} {β : Type*} {f : α  β} (H : ¬range f = ) : nonempty α :=
sorry

view this post on Zulip Kevin Buzzard (Jul 17 2018 at 15:42):

What am I allowed to use?

view this post on Zulip Kevin Buzzard (Jul 17 2018 at 15:43):

Excluded middle?

view this post on Zulip Kevin Buzzard (Jul 17 2018 at 15:43):

Or nothing like this?

view this post on Zulip Patrick Massot (Jul 17 2018 at 15:45):

Of course I don't care. Again, the goal is to prove the completion is empty only if the original space is empty. And this is only needed to implement Mario's trick allowing to totalize the function "lift to completion" so that any function from a uniform space to a complete Hausdorff space lifts, the lift being garbage is the function is not uniformly continuous.

view this post on Zulip Patrick Massot (Jul 17 2018 at 15:47):

But at some point we hope to put all this into mathlib, so it would be nicer to avoid unnecessary decidability assumption or classical logic

view this post on Zulip Kevin Buzzard (Jul 17 2018 at 15:49):

nonempty needs data for its constructor, and (univ : set α) ≠ ∅ is only a proposition

view this post on Zulip Patrick Massot (Jul 17 2018 at 15:49):

You can have a look at https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/completions/src/for_mathlib/completion.lean to see where I stand

view this post on Zulip Patrick Massot (Jul 17 2018 at 15:49):

Mario style lifting is defined at https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/completions/src/for_mathlib/completion.lean#L124

view this post on Zulip Kevin Buzzard (Jul 17 2018 at 15:50):

For the first one you need something like ¬ (∀ a : α, false) → ∃ a : α, true

view this post on Zulip Patrick Massot (Jul 17 2018 at 15:50):

Maybe I should use inhabited instead of nonempty

view this post on Zulip Chris Hughes (Jul 17 2018 at 15:51):

Assuming α is nonempty, the assumption decidable_eq (set α) implies decidability of all propositions

view this post on Zulip Patrick Massot (Jul 17 2018 at 15:51):

Or maybe this is too much trouble, given that I already have a working lift for uniformly continuous functions

view this post on Zulip Patrick Massot (Jul 17 2018 at 15:52):

I'm upset because none of this has any mathematical content

view this post on Zulip Kevin Buzzard (Jul 17 2018 at 15:58):

lemma nonempty_iff_univ {α : Type*} : nonempty α  (univ : set α)   :=
begin
  split,
  { intro H,
    cases H with a,
    intro H2,
    show ( : set α) a,
    rw H2,
    trivial
  },
  intro H,
  apply classical.by_contradiction,
  intro H2,
  apply H,
  funext,
  exfalso,
  apply H2,
  exact a
end

view this post on Zulip Mario Carneiro (Jul 17 2018 at 16:07):

I used many of these same theorems in the proof of dense_embedding.extend

view this post on Zulip Mario Carneiro (Jul 17 2018 at 16:08):

for the most part I just brute forced through all of it, using exists_mem_of_ne_empty to get elements out of nonempty sets

view this post on Zulip Mario Carneiro (Jul 17 2018 at 16:08):

and using mem_closure_iff to get a nonempty set from a closure

view this post on Zulip Kevin Buzzard (Jul 17 2018 at 16:21):

lemma nonempty_of_nonempty_range {α : Type*} {β : Type*} {f : α  β} (H : ¬range f = ) : nonempty α :=
begin
  apply classical.by_contradiction,
  intro H2,
  apply H,
  unfold range,
  funext,
  apply propext,
  show ( y : α, f y = x)  false,
  split,swap,exact false.elim,
  intro H3,cases H3 with a Ha,
  apply H2,
  exact a
end

view this post on Zulip Kevin Buzzard (Jul 17 2018 at 16:21):

What's the hurry :-)

view this post on Zulip Mario Carneiro (Jul 17 2018 at 16:22):

not so cleaned up:

lemma nonempty_completion_iff : nonempty (completion α) ↔ nonempty α :=
begin
  split,
  { rintro ⟨c⟩,
    have := eq_univ_iff_forall.1 (to_completion.dense α) c,
    have := mem_closure_iff.1 this _ is_open_univ trivial,
    rcases exists_mem_of_ne_empty this with ⟨_, ⟨_, a, _⟩⟩,
    exact ⟨a⟩ },
  { rintro ⟨a⟩,
    exact ⟨to_completion α a⟩ }
end

view this post on Zulip Patrick Massot (Jul 17 2018 at 16:22):

Many thanks to both of you!

view this post on Zulip Patrick Massot (Jul 17 2018 at 16:23):

In the mean time I saw Kevin's first lemma proof and then found some courage to write:

lemma nonempty_of_nonempty_range {α : Type*} {β : Type*} {f : α  β} (H : ¬range f = ) : nonempty α :=
begin
  cases exists_mem_of_ne_empty H with x h,
  cases mem_range.1 h with y _,
  exact y
end

view this post on Zulip Kevin Buzzard (Jul 17 2018 at 16:24):

I don't know any of these lemmas which people are using :-)

view this post on Zulip Patrick Massot (Jul 17 2018 at 16:24):

I find them using lots of suffering

view this post on Zulip Patrick Massot (Jul 17 2018 at 16:24):

But now I need to understand Mario's proof

view this post on Zulip Kevin Buzzard (Jul 17 2018 at 16:25):

I never quite know whether I should somehow attempt to learn exactly what is in mathlib and where it all is

view this post on Zulip Kevin Buzzard (Jul 17 2018 at 16:25):

I'm doing a lot of work with multisets at the minute for a student, and now I really know my way around multiset.lean

view this post on Zulip Kevin Buzzard (Jul 17 2018 at 16:26):

but I don't know my way around data.set.basic in that way

view this post on Zulip Mario Carneiro (Jul 17 2018 at 16:27):

It's worth a perusal (data.set.lattice is the other important one)

view this post on Zulip Mario Carneiro (Jul 17 2018 at 16:28):

but ideally you should be able to guess beforehand what is in there

view this post on Zulip Patrick Massot (Jul 17 2018 at 16:28):

rintro ⟨c⟩ is already a nice trick

view this post on Zulip Patrick Massot (Jul 17 2018 at 16:29):

But then I'm not sure this isn't too efficient. Don't you think closure_empty_iff should be in mathlib anyway?

view this post on Zulip Kevin Buzzard (Jul 17 2018 at 16:30):

I hope rintro isn't as slow as rsimp

view this post on Zulip Patrick Massot (Jul 17 2018 at 16:30):

Never noticed any slowness there

view this post on Zulip Patrick Massot (Jul 17 2018 at 16:32):

If you don't fear rcases then you don't fear rintro

view this post on Zulip Patrick Massot (Jul 17 2018 at 16:33):

and, together, they really make a difference in conciseness, without obfuscation (it's all about unpacking stuff that our mind would unpack unconsciously)

view this post on Zulip Patrick Massot (Jul 17 2018 at 16:41):

Mario, I tried to use your trick in https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/completions/src/for_mathlib/completion.lean#L124 but I needed to assume uniform continuity of f is decidable. Now I want to state lemmas assuming uniform continuity, but Lean asks me for an instance of decidable (uniform_continuous f). Did I do it wrong? What should I do?

view this post on Zulip Mario Carneiro (Jul 17 2018 at 16:42):

since that proof uses only structural tactics, I would normally compress it into a term proof

view this post on Zulip Patrick Massot (Jul 17 2018 at 16:43):

which proof?

view this post on Zulip Mario Carneiro (Jul 17 2018 at 16:44):

the one I gave

view this post on Zulip Mario Carneiro (Jul 17 2018 at 16:45):

you should have local instance prop_decidable

view this post on Zulip Patrick Massot (Jul 17 2018 at 16:46):

Oh I will happily add that if you don't tell me this will be an issue when trying to get all this into mathlib

view this post on Zulip Patrick Massot (Jul 17 2018 at 16:47):

My original version (with unique exists!) had no such assumption, but if course it makes no difference to me

view this post on Zulip Mario Carneiro (Jul 17 2018 at 16:48):

of course cases on uniform continuity is firmly classical, but we are not working in the constructive fragment here

view this post on Zulip Patrick Massot (Jul 17 2018 at 16:50):

Nice. I should be able to move on tonight. But right now I'm too hungry, I need diner.

view this post on Zulip Patrick Massot (Jul 17 2018 at 16:50):

Thanks!

view this post on Zulip Mario Carneiro (Jul 17 2018 at 16:57):

totalizing functions often requires classical axioms

view this post on Zulip Patrick Massot (Jul 17 2018 at 20:12):

I'm done totalizing. Now I'm back exactly where I was yesterday except that, in uniform_space.completion_lift f, f is now a function rather than a proof that a function is uniformly continuous. In particular fonctoriality now reads completion_lift (g ∘ f) = (completion_lift g) ∘ completion_lift f, as it should

view this post on Zulip Patrick Massot (Jul 17 2018 at 20:13):

All this for the cheap price of a few hours and a local attribute [instance] classical.prop_decidable

view this post on Zulip Patrick Massot (Jul 17 2018 at 20:14):

And I can see wisdom is coming to Kenny. He didn't write anything about that last classical detail.


Last updated: May 10 2021 at 06:13 UTC