discrete_topology

Stream: new members

[Damiano Testa]

Dear All,

while playing around with #4301, following the thread, I decided to learn some topology in Lean. Below is my attempt to prove that the roots of a polynomial with real coefficients are a discrete topological space.

I am somewhat puzzled that I was not asked by Lean to assume that the polynomial is non-zero, though. Therefore, I learned that 0.roots is defined to be ∅. Should this have been univ instead?

Anyway, any suggestions on how to streamline the proofs below would be more than welcome! I particularly struggled with discrete_of_finite. I suspect that the largest issue is that I do not understand well all the coercions and I had the impression that I had forced myself in a co[e]rner...

import analysis.calculus.mean_value

open_locale classical

open polynomial set

lemma discrete_of_forall_open {X : Type*} [topological_space X] :
  (∀ s : set X, is_open s) ↔ discrete_topology X :=
⟨λ sep, ⟨topological_space_eq (funext (λ x, eq_iff_iff.mpr ⟨λ _, ⟨⟩, λ _, sep x⟩))⟩, λ d s,
  @is_open_discrete X _ d s⟩

lemma discrete_of_singletons_open {X : Type*} [topological_space X] :
  (∀ a : X, @is_open X _ (singleton a)) → discrete_topology X :=
λ s, discrete_of_forall_open.mp (λ t,
begin
  rw ← bUnion_of_singleton t,
  refine is_open_Union (λ (i : X), is_open_Union (λ j, s i)),
end)

lemma open_of_open_inter {X : Type*} [topological_space X] {U S : set X} :
  @is_open X _ U → @is_open S _ {s : S | ↑s ∈ U} :=
λ oU, ⟨U, oU, rfl⟩

lemma discrete_subspace_of_open_int_singletons {X : Type*} [topological_space X] {S : set X}
  (sep : ∀ s ∈ S, ∃ U : set X, is_open U ∧ U ∩ S = singleton s) : discrete_topology S :=
begin
  refine discrete_of_singletons_open _,
  rintro ⟨t, ht⟩,
  obtain ⟨U, oU, j⟩ := (sep t ht),
  refine ⟨U, oU, ext (λ x, _)⟩,
  cases x with x hx,
  refine ⟨λ a, _, λ a, _⟩,
  { obtain F := (mem_inter_iff x U S).mpr ⟨a, hx⟩,
    rw [j, mem_singleton_iff] at F,
    exact (id (subtype.mk.inj_eq x hx t ht)).mpr F },
  { rw [mem_singleton_iff, subtype.mk.inj_eq] at a,
    change x ∈ U,
    apply mem_of_subset_of_mem _ (mem_singleton x),
    rw ← a at j,
    rw ← j,
    exact inter_subset_left U S },
end

lemma discrete_of_lt_dist {X : Type*} [metric_space X] {s : set X}
  (sep : ∀ a ∈ s, ∃ e : ℝ, 0 < e ∧ (∀ b ∈ s, dist a b < e → a = b)) : discrete_topology s :=
begin
  apply discrete_subspace_of_open_int_singletons,
  intros x xs,
  rcases (sep x xs) with ⟨e, e0, disj⟩,
  refine ⟨metric.ball x e, metric.is_open_ball, ext (λ y, ⟨λ h, mem_singleton_iff.mpr _, λ h, _⟩)⟩,
  { exact eq.symm (disj y h.2 (metric.mem_ball'.mp h.1)) },
  { induction h,
    exact ⟨metric.mem_ball_self e0, xs⟩ },
end

lemma discrete_of_lt_dist_uniform {X : Type*} [metric_space X] {s : set X} :
  (∃ e : ℝ, 0 < e ∧ (∀ a b ∈ s, dist a b < e → a = b)) → discrete_topology s :=
begin
  rintros ⟨e, e0, F⟩,
  apply discrete_of_lt_dist (λ x xs, ⟨e, e0, λ b bs, F x b xs bs⟩),
end

lemma min'_image_le {S T : Type*} [linear_order T] {s : finset S} (hs : s.nonempty)
  (a : S) (ha : a ∈ s) (f : S → T) :
  finset.min' (finset.image f s) (finset.nonempty.image hs f) ≤ f a :=
finset.min'_le _ _ $ finset.mem_image.mpr ⟨_, ‹_›, rfl⟩

lemma lt_min' {S : Type*} [linear_order S] {s : finset S} (hs : s.nonempty) (a : S) :
  a < finset.min' s hs → a ∉ s :=
λ al as, imp_false.mpr (not_lt.mpr (finset.min'_le s a as)) al

lemma lt_min'_image {S T : Type*} [linear_order T] {s : finset S} (hs : s.nonempty)
  (a : S) (f : S → T) :
  f a < finset.min' (finset.image f s) (finset.nonempty.image hs f) → a ∉ s :=
λ al as, not_le.mpr al (min'_image_le hs a as f)

lemma discrete_of_finite {X : Type*} [metric_space X] {s : finset X} :
  discrete_topology {a : X // a ∈ s} :=
begin
  apply discrete_of_lt_dist,
  intros a am,
  by_cases d0 : (finset.erase s a).nonempty,
  { obtain ⟨a0, ha0, da0⟩ :=
      finset.mem_image.mp (finset.min'_mem ((finset.erase s a).image (λ x, dist x a))
      (finset.nonempty.image d0 (λ (x : X), dist x a))),
    refine ⟨finset.min' ((finset.erase s a).image (λ x, dist x a))
      (finset.nonempty.image d0 (λ (x : X), dist x a)), _, λ b hb dab, _⟩,
    { apply lt_of_le_of_ne (finset.le_min' _ _ _ (λ y hy, _)) _,
      { rcases finset.mem_image.mp hy with ⟨aa, bb, rfl⟩,
        exact dist_nonneg },
      { intros ma,
        rw [← ma, dist_eq_zero] at da0,
        rw da0 at ha0,
        exact finset.not_mem_erase a s ha0 } },
    { rw dist_comm a b at dab,
      have : (λ x, dist x a) b < (@finset.image X ℝ (λ (a b : ℝ), classical.prop_decidable (a = b))
        (λ x, dist x a) (s.erase a)).min' _,
      { convert dab,
        convert finset.nonempty.image d0 (λ x, dist x a) },
    obtain F := lt_min'_image d0 b (λ x, dist x a) this,
    symmetry,
    apply finset.eq_of_mem_of_not_mem_erase hb F, } },
  { refine ⟨1, zero_lt_one, λ b hb dab, _⟩,
    rw ← finset.sdiff_singleton_eq_erase a at d0,
    apply finset.mem_singleton.mp,
    convert am,
    obtain sa : s = singleton a := le_antisymm _ (finset.singleton_subset_iff.mpr am),
    { subst sa,
      cases hb,
      rw hb,
      cases hb },
    { by_contradiction h,
      exact d0 (finset.nonempty_of_ne_empty (λ e, h (finset.sdiff_eq_empty_iff_subset.mp e))) } },
end

lemma roots_discrete (f : polynomial ℝ) : discrete_topology {a : ℝ // a ∈ f.roots.to_finset} :=
discrete_of_finite

[Kenny Lau]

Damiano Testa said:

I am somewhat puzzled that I was not asked by Lean to assume that the polynomial is non-zero, though. Therefore, I learned that 0.roots is defined to be ∅. Should this have been univ instead?

Unfortunately, univ is not a finset.

[Damiano Testa]

Ok, I guess this is one of the things that I will constantly have in the back of my mind, like the fact that 1-2=0!

[Damiano Testa]

It might make sense to add the hypothesis f ≠ 0 to the final lemma (roots_discrete), even though the lemma is correct also in its more general form, right?

[Kenny Lau]

Yes.

[Alex J. Best]

Damiano Testa said:

It might make sense to add the hypothesis f ≠ 0 to the final lemma (roots_discrete), even though the lemma is correct also in its more general form, right?

Why? It just means people will have to prove their polynomials are zero every time they want to use your lemma?

[Kenny Lau]

Yeah, if it's true in general, then state it in general.

[Damiano Testa]

@Alex J. Best @Kenny Lau I am not so comfortable with the idea that the zero set of the polynomial 0 should be considered as a discrete topological space. I realize that the definitions in Lean allow this, since the zero set of the zero polynomial is empty. However, this might lead to the (human) conclusion that the topology on ℝ is discrete.

Am I the only one who thinks this?

[Kenny Lau]

I understand that a person coming from a mathematical background might not be very comfortable with this idea of stating a junk theorem in general, but that's just how we do it in Lean, so that other people can use it more easily.

[Alex J. Best]

In that case I might write a big warning message in the docstring before the theorem so that nobody reading the theorem makes a mistake.

[Damiano Testa]

Ok, I removed the hypothesis. I do like the idea of flagging this in a comment somewhere, though!

[Alex J. Best]

If you use the

/-- comment here -/
theorem blah

syntax it will show up prominently in the docs and if people hover their mouse over the theorem

[Damiano Testa]

Alex J. Best said:

If you use the

/-- comment here -/
theorem blah

syntax it will show up prominently in the docs and if people hover their mouse over the theorem

Comment added! Thanks for the suggestion!

[Damiano Testa]

If you think that this might be a useful addition to mathlib, let me know and I might ask a couple of specific questions, to clean up the parts of the proofs that feel clunky!

As usual, thank you all for making this chat so helpful and supportive!
:pray:

[Kevin Buzzard]

@Damiano Testa here's a parable. When I was formalising my first year course example sheets in 2017, mathlib had the reals as a complete ordered field but didn't have a square root function. In my course I proved that sqrt(x) could be defined to be the sup of the real numbers whose square was <= x, if x was nonnegative. So I defined a square root function myself for x nonnegative as this sup and posted on the chat (this was back in the gitter days so it's lost in time). Mario laughed at the definition because he said he said it was a function which asked for an input (a proof that x>=0) and then never used it. I was surprised it didn't use it but what was happening was that real.sup didn't ask for a proof that the set was nonempty and bounded either, it just returned 37 if the set didn't actually have a sup and then there was a lemma saying that the value of real.sup was a least upper bound if the set was nonempty and bounded. From a computer science point of view I could understand that it was ridiculous to ask for an input to my function which was never used when calculating the output but from a mathematical point of view I was deeply concerned about the square root of every negative real being 37 so I left the assumption in there anyway and went on to formalise the example sheet.

And it was a nightmare. Because the first question on is was "prove $\sqrt2+\sqrt3<\sqrt{10}$" (and this was before the days that proving $0\leq2$ was easy) and in every single line of the proof I had to keep inserting these stupid proofs that everything was nonnegative, even if I was just doing something like squaring both sides which mathematically would work fine if the square root of every negative number was 37, and this was all in the knowledge that the system was asking me for a proof which I was finding annoying to construct and then simply ignoring it. I soon learnt that the idea of "garbage in, garbage out" was a convenient one in dependent type theory.

In this situation one could imagine two polynomial roots functions, one returning a set which functioned correctly, and one which returned a finset which returned junk at zero. In fact we'll have a similar situation with DVRs soon. I defined the additive valuation on a DVR but it's nat-valued and sends 0 to 37 instead of +infinity, for the simple reason that this function is much easier to work with in practice than the function taking values in with_top nat. The advantage of with_top nat is that things like v(a+b)>=min(v(a),v(b)) are true unconditionally, but when you look at the proofs of these things they always treat 0 as a special case anyway, we claim it's a unified approach but actually this is an illusion. There's an art to all this but basically the best definitions in dependent type theory are the ones most convenient to work with in dependent type theory and if this differs from mathematical conventions then maybe that's the fault of dependent type theory but we're doing dependent type theory and goodness knows we have enough other problems, we may as well use the definition style best suited to the theory.

[Patrick Massot]

Damiano, I think you're making this a lot more complicated that it needs to be, because you are too focused on the intended application.

[Patrick Massot]

@Damiano Testa your issue is that you're too focused on sets inside metric spaces. In Lean this is costly. You need to think as much as possible about abstract spaces and then apply things to sets endowed with the induced topology. I claim your file should begin with:

open_locale classical

open polynomial set

lemma forall_open_iff_discrete {X : Type*} [topological_space X] :
  (∀ s : set X, is_open s) ↔ discrete_topology X :=
⟨λ h, ⟨by { ext U ; show is_open U ↔ true, by simp [h U] }⟩,
 by introsI ; exact is_open_discrete _⟩


lemma singletons_open_iff_discrete {X : Type*} [topological_space X] :
  (∀ a : X, is_open ({a} : set X)) ↔ discrete_topology X :=
⟨λ h, ⟨eq_bot_of_singletons_open h⟩, by introsI ; exact is_open_discrete _⟩


lemma subset_singleton_iff {α : Type*} {s : set α} {x : α} : s ⊆ {x} ↔ ∀ y ∈ s, y = x :=
⟨λ h y hy, mem_singleton_iff.mp (h hy),
 λ h y hy, mem_singleton_iff.mpr (h y hy)⟩

open metric

lemma metric.is_open_singleton_iff {X : Type*} [metric_space X] {x : X} :
  is_open ({x} : set X) ↔ ∃ ε > 0, ∀ y, dist y x < ε → y = x :=
by simp [is_open_iff, subset_singleton_iff, mem_ball]

lemma metric.discrete_of_finite {X : Type*} [metric_space X] [fintype X] : discrete_topology X :=
begin
  rw ← singletons_open_iff_discrete,
  intros x,
  rw metric.is_open_singleton_iff,
  sorry
end

lemma discrete_of_finite {X : Type*} [metric_space X] {s : finset X} :
  discrete_topology {a : X // a ∈ s} :=
metric.discrete_of_finite

And the sorry should be filled using some version of your finset.min' stuff (that I didn't look at closely), but my point is this is a completely separate issue from the induced topology stuff.

[Reid Barton]

For the final statement roots_discrete I think a more natural formulation is discrete_topology {a : ℝ // f.eval a = 0}, which now does need the nonzero hypothesis you expected.

[Patrick Massot]

My shower says this has nothing to do with metric spaces, some kind of separation condition should be enough and get us rid of finset.min. Hold on.

[Patrick Massot]

import topology.metric_space.basic

open set

lemma forall_open_iff_discrete {X : Type*} [topological_space X] :
  (∀ s : set X, is_open s) ↔ discrete_topology X :=
⟨λ h, ⟨by { ext U ; show is_open U ↔ true, by simp [h U] }⟩,
 by introsI ; exact is_open_discrete _⟩


lemma singletons_open_iff_discrete {X : Type*} [topological_space X] :
  (∀ a : X, is_open ({a} : set X)) ↔ discrete_topology X :=
⟨λ h, ⟨eq_bot_of_singletons_open h⟩, by introsI ; exact is_open_discrete _⟩

lemma subset_singleton_iff {α : Type*} {s : set α} {x : α} : s ⊆ {x} ↔ ∀ y ∈ s, y = x :=
⟨λ h y hy, mem_singleton_iff.mp (h hy),
 λ h y hy, mem_singleton_iff.mpr (h y hy)⟩

open metric

lemma metric.is_open_singleton_iff {X : Type*} [metric_space X] {x : X} :
  is_open ({x} : set X) ↔ ∃ ε > 0, ∀ y, dist y x < ε → y = x :=
by simp [is_open_iff, subset_singleton_iff, mem_ball]

lemma compl_singleton_eq_bUnion_singleton {α : Type*} (x : α) :
  ({x} : set α)ᶜ = ⋃ (y : α) (hy : y ≠ x), {y} :=
begin
  rw compl_singleton_eq,
  ext y,
  simp
end

lemma discrete_of_t1_of_finite {X : Type*} [topological_space X] [t1_space X] [fintype X] :
  discrete_topology X :=
begin
  rw ← singletons_open_iff_discrete,
  intros x,
  rw [← is_closed_compl_iff, compl_singleton_eq_bUnion_singleton x],
  exact is_closed_bUnion (finite.of_fintype _) (λ y _, is_closed_singleton)
end

lemma metric.discrete_of_finite {X : Type*} [metric_space X] [fintype X] : discrete_topology X :=
discrete_of_t1_of_finite

lemma discrete_of_finite {X : Type*} [metric_space X] {s : finset X} :
  discrete_topology {a : X // a ∈ s} :=
metric.discrete_of_finite

[Patrick Massot]

No cheating involved, I started searching wikipedia for separation axioms after I posted the preceding message.

[Patrick Massot]

Notice how the last two lemmas aren't doing anything, only specializing discrete_of_t1_of_finite using type class instances magic.

[Patrick Massot]

I claim this is formalization. If you're suffering then you need to get clearer, more abstract, ideas.

[Kevin Buzzard]

I remember when I was at Damiano's stage, and this idea which Patrick refers to as "suffering", presumably referring to Damiano's original 34 line proof of discrete_of_finite, is something which I always thought of as "fun" (as I was beginning to realise that I had found a computer program which thought about mathematics in the same way that I did). However, whatever your take on writing 34 line proofs, Patrick certainly has a point that it's better to find the right generality in which to prove a theorem. The introduction of t1 and the abstraction of using topological spaces instead of metric spaces turns a 34 line proof that a finite subset of a metric space is discrete (using fiddly mins of sets of distances) into a 4 line proof that a finite subset of a T1 space is discrete, and this is an important lesson, regardless of how much fun we're having.

[Damiano Testa]

Dear All,

thank you so much for your suggestions! I had no idea that the T_i axioms were in Lean! I will now look at how you managed to avoid all the coercion suffering that I was going through!

@Kevin Buzzard I understand your parable and I had read your post about division by zero. However, I am still trying to get my head around stuff in Lean. My (I realize incorrect) reasoning is. If you are trying to talk about 1/0, then you already did something wrong, so getting garbage results is ok. If you are asking Lean to compute the roots of a polynomial, though, it is reasonable that you argument also applies to the zero polynomial. In this case, the Lean theorem makes me think that the topology on ℝ is discrete, not that the vanishing set of the zero polynomial is empty! I can see that Lean is working consistently, but I since I am familiar with the mathematical conventions and not the Lean ones, I still need adjusting!

Anyway, I will now dive into learning the "correct" proof of these results. Sadly, once the proof is done, it becomes irrelevant, right?
:smile:

[Kevin Buzzard]

the issue is the type of the function. If you're looking for the roots of a polynomial, the roots of 0 will be everything. But if the question is to find the finite set of roots of a polynomial, which apparently it is if it's returning a finset, then because it's a definition and not a theorem, it's best to have this "garbage in, garbage out" principle. I think that the most extreme example of it is real.sup, which takes any set of reals, bounded or unbounded, and produces a real number anyway. All the correct hypotheses are there but they're in the theorems, not the definitions. Definitions are special and different.

[Damiano Testa]

Ok, I can agree with this. But then, the result roots_discrete should contain the hypothesis, no? Or am I still misunderstanding something? This is a result, not a definition, or at least this is how I view it!

[Riccardo Brasca]

@Damiano Testa If you want to have infinitely many roots for the zero polynomial you can use directly is_root instead of p.roots.

[Riccardo Brasca]

I think that the current state of things is really the optimal one, I have used this stuff a little bit in the last weeks and it's quite natural to work with them.

[Damiano Testa]

@Patrick Massot Thank you very much for taking the time to generalize and consequently cleaning up my clunky proofs! I feel that I have learned a lot!

To be honest, even if I had known about the existence of T_i spaces, first, I might have used T_2, just to be safe, and second, I would have probably had long proofs anyway!

[Damiano Testa]

Riccardo Brasca said:

Damiano Testa If you want to have infinitely many roots for the zero polynomial you can use directly is_root instead of p.roots.

Ok, I learned about the rootscommand from the Liouville PR, but I will keep an eye out for is_root: thanks for the pointer!

[Kevin Buzzard]

The most extreme example I've seen of long proofs going to short proofs is trying to prove any theorem about basic topology using open sets the way it was taught to us as undergraduates. You prove e.g. compact subspace of Hausdorff space is closed by chasing open sets around, and then you look at the mathlib proof and it's usually about 4 lines with filters. This is especially true for Tychonoff.

[Riccardo Brasca]

Moreover p.roots is a multiset (and we happy to have multiplicity of the roots!), I don't see any reasonable convention for the multiplicity of the roots of 0...

[Damiano Testa]

Just to spell out something that is likely clear to everyone else, but I feel that I should air out. I will take this example at hand: in mathematics, I would say that the roots of a polynomials are a finite set, except in the case of the zero polynomial. Thus, in my mind, I construct a "function" with inputs polynomials and targets "finite sets" or "everything", depending on the input. This appeared to me to work well with dependent type theory: the type of the image of the function depends on the input. The fault in this is that the Type of the target is allowed to depend only on the Type of the source, not on the given term. Is this correct?

Now that I am writing this, I realize that it should be a tautology, but I had not internalized this until now...

[Mario Carneiro]

The paradox here is that writing dependent types in dependent type theory is inadvisable

[Damiano Testa]

Reid Barton said:

For the final statement roots_discrete I think a more natural formulation is discrete_topology {a : ℝ // f.eval a = 0}, which now does need the nonzero hypothesis you expected.

Thank you for this comment! It makes me feel better about omitting the hypothesis in the initial formulation. I am thinking that it might be useful to have both statements...

[Mario Carneiro]

DTT makes it possible but it makes every use harder so it should be used sparingly and well encapsulated

[Riccardo Brasca]

I don't know the answer to your question, but my feeling is that in any case the real difference is that in normal mathematics nobody proves that X ^ 2 - 3 is different from 0, so we can speak about the finite set of its roots without any trouble. In lean you would be forced to prove this over and over, essentially anytime you want to speak about p.roots. I realized this working with p.degree and p.nat_degree: there is really no alternative to have the two definitions, but sometimes it's really annoying.

[Damiano Testa]

Ah, ok! While my skills had not made working with dependent types especially accessible, I had not realized that it was actually hard. And coming from you, @Mario Carneiro , adds an unfathomable weight to the assertion!

[Damiano Testa]

Riccardo Brasca said:

I don't know the answer to your question, but my feeling is that in any case the real difference is that in normal mathematics nobody proves that X ^ 2 - 3 is different from 0, so we can speak about the finite set of its roots without any trouble. In lean you would be forced to prove this over and over, essentially anytime you want to speak about p.roots. I realized this working with p.degree and p.nat_degree: there is really no alternative to have the two definitions, but sometimes it's really annoying.

I had a similar experience with nat_degree and degree, however, I think that the min' always requiring the assumption nonempty is what really annoys me most. Why is there such an assumption all the time in this case?

[Mario Carneiro]

I'm not sure exactly which min' you mean but I would guess that the codomain is not necessarily inhabited, so it's impossible to avoid the assumption in that case

[Damiano Testa]

I am thinking of finset.min'.

[Mario Carneiro]

there are actually several variations on min and max for finsets depending on your constraints

[Damiano Testa]

I see, I have likely only used min' for subsets of nat and (today) of \R!

[Mario Carneiro]

you can have it return an option A, or if A is a inf-top semilattice you can return an A using finset.sup, or if it's known to be nonempty but A isn't then you can use finset.min'

[Mario Carneiro]

I guess we don't have a version that assumes [nonempty A] instead of s.nonempty

[Damiano Testa]

I have bad memories of getting stuck on options, so I am wary of choosing this "option". Especially in the context of degrees of polynomials, I found that I would have liked it to be defined as the min' insert f.support 0...

[Mario Carneiro]

that's nat_degree, right?

[Kevin Buzzard]

@Damiano Testa I had to choose between v : R -> nat and v : R -> with_top nat for the valuation on a DVR and I went for nat and gave v(0) a junk value, and this was simply because I know from experience that nat is much easier to deal with than with_top nat. Probably I will make v' : R -> with_top nat at some point, but I know that I can make the norm n : R -> real easily from v so now I am not even sure why I need v' at all. To get n from v I just say "(1/p)^v(x) if x isn't 0, and 0 if x=0". To get n from v' you might think it's easier but I still need to split into cases because (1/p)^n isn't defined if n is in with_top nat. I think it's swings and roundabouts.

[Damiano Testa]

I think that nat_degree is defined using option.get_or_else. Due to my limitations, I did not understand how to use option...

[Damiano Testa]

Kevin Buzzard said:

Damiano Testa I had to choose between v : R -> nat and v : R -> with_top nat for the valuation on a DVR and I went for nat and gave v(0) a junk value, and this was simply because I know from experience that nat is much easier to deal with than with_top nat. Probably I will make v' : R -> with_top nat at some point, but I know that I can make the norm n : R -> real easily from v so now I am not even sure why I need v' at all. To get n from v I just say "(1/p)^v(x) if x isn't 0, and 0 if x=0". To get n from v' you might think it's easier but I still need to split into cases because (1/p)^n isn't defined if n is in with_top nat. I think it's swings and roundabouts.

I am becoming more familiar with Lean, so I start to "feel inside" what you mean by this! I still need to go through a bit of the learning process, though, to fully automate it and stop worrying about it!

[Mario Carneiro]

Damiano Testa said:

I think that nat_degree is defined using option.get_or_else. Due to my limitations, I did not understand how to use option...

It shouldn't matter what the definition is, as long as it is extensionally equal to whatever you want it to be

[Mario Carneiro]

because you can simply prove a theorem that gives the desired unfolding

[Damiano Testa]

Mario Carneiro said:

because you can simply prove a theorem that gives the desired unfolding

True, although you was not me in this specific case: Johan proved what I had tried and failed to achieve!

[Damiano Testa]

Once I had a lemma showing that nat_degree equals min' (exponents with 0 added), I would start all my proofs with first applying this lemma, and then proceeding from there!

[Mario Carneiro]

In the case of nat_degree, I would expect the api theorem to say that nat_degree 0 = 0 and nat_degree p = <degree of p>

[Mario Carneiro]

so you don't have to worry about any options here

[Damiano Testa]

(I know that this is due to my inability to use Lean propertly: if I looked back at these issues now, I may not feel so strongly about it...)

[Kevin Buzzard]

Right. If you're having to translate to min' them it might mean that you either don't know the API for nat_degree or it wasn't made.

[Damiano Testa]

I think that the API might even have been there, except that I was trying to introduce trailing_degrees and wanted to mimick the lemmas for degree and found out that I failed a fairly high proportion of the times

[Damiano Testa]

In the specific case of converting a nat_degree to a min' I am not sure that that was available, though a lot was available!

[Riccardo Brasca]

Thank's to this discussion I just realized that with_bot ℕ is by definition option ℕ! This is weird because in my mind option ℕ is used to produce partial functions, and, still in my mind, degree is not partial, 0.degree is something like $-\infty$, where $-\infty$ is an element of with_bot ℕ (like in $\bar \mathbf{N} = \mathbf{N} \cup \{-\infty\}$). I find this approach very clever :smile:

[Riccardo Brasca]

And this also explains why in the definition of nat_degree there is no proof that the degree of a nonzero polynomial is the coercion of a natural number.

[Mario Carneiro]

You should think of option as the + 1 operator on types

[Mario Carneiro]

it's useful whenever you want to add a single new element disjoint from everything else

[Mario Carneiro]

It can also be used to represent fallible operations, but this is used less in mathlib than in other programming languages, because we also have a couple other alternative representations. I usually use the term "partial function" to refer to a function with a propositional argument, like min'

[Damiano Testa]

I kind of got the hang of what option does, but I felt that the API was too much oriented to be parsed by a computer scientist, than by a mathematician. This is why I realize that it was my fault for "not getting it"...

[Mario Carneiro]

A -> option B means that the function is fallible but it can also tell you when it failed

[Mario Carneiro]

A -> roption B means that the function is fallible but it can't determine the success condition

[Mario Carneiro]

\all x : A, p x -> B means that the function always returns a proper result but it has a precondition p x so it is partial in the mathematical sense

[Damiano Testa]

(I have been reading a book suggested by Kevin, Learn you a Haskell, which clarified a lot of basic Lean for me. I understood the idea behind option it just always felt like a dead-end when I had that some hypothesis was an option.get_or_else ..., since I knew none of the API to convert it to something else.

[Mario Carneiro]

it is a pretty programmer friendly side of things, but it's definitely useful for pure maths as well

[Damiano Testa]

Mario Carneiro said:

A -> roption B means that the function is fallible but it can't determine the success condition

I don't think that I ever encountered a roption, or, if I did, I skimmed it so quickly, that I pretended it was an option!

[Mario Carneiro]

enat is defined in terms of roption

[Kevin Buzzard]

...and that's exactly the reason we didn't have valuations on a DVR for several months :-)

[Mario Carneiro]

It is classically equivalent to option

[Mario Carneiro]

you probably want to prefer option for most things

[Damiano Testa]

Mario Carneiro said:

it is a pretty programmer friendly side of things, but it's definitely useful for pure maths as well

Undoubtedly! For instance, the notion of monoid_with_zero is something that is probably lurking in the back of every mathematician, but I had never really formalized it in my head and seeing it written down really added depth to my understanding of mathematics!

[Kevin Buzzard]

Yeah, monoid_with_zero makes me really happy. Stuff like units of a ring and UFDs and IDs are all defined using only * and not +, but because we only use them for rings we don't ever really think about the *-only side of the story.

[Damiano Testa]

Mario Carneiro said:

It is classically equivalent to option

Ok, this makes sense! To be honest, even though I consider myself as a mathematician, I am not so much against constructive mathematics as other mathematicians are..

[Kevin Buzzard]

you wait until you start trying to use roption.

[Kevin Buzzard]

Although Mario's comment above just taught me a useful way of thinking about it!

[Mario Carneiro]

The idea is that it represents "unending computations", for example the return value of a turing machine or other enumerable search procedure

[Damiano Testa]

Mario Carneiro said:

\all x : A, p x -> B means that the function always returns a proper result but it has a precondition p x so it is partial in the mathematical sense

This simple observation actually clears up some of the confusion in my mind!!

[Kevin Buzzard]

Because I'm so used to just saying "if it terminates then x, else y" and not really caring about whether there's an algorithm, this is why I've had option and roption conflated in my head forever.

[Damiano Testa]

Kevin Buzzard said:

...and that's exactly the reason we didn't have valuations on a DVR for several months :-)

I feel your pain! And probably, I feel it much less than you did!

[Mario Carneiro]

computationally, you can't shoehorn this into option even though logically it is, because an option would require you to determine if the value is some or none, which is basically the halting problem

[Kevin Buzzard]

Right, but for someone who opens their files with open_locale classical and then says "if this happens then do that, else do something else", you quickly lose track of what is easy to decide in practice.

[Mario Carneiro]

Also, roption has an interesting topology different from option

[Kevin Buzzard]

yeah that's pretty insane

[Mario Carneiro]

option adds the point discretely separate from everything else, while roption is the one point compactification

[Kevin Buzzard]

and the continuous map is the constructive one, right?

[Mario Carneiro]

right

[Damiano Testa]

Mario Carneiro said:

The idea is that it represents "unending computations", for example the return value of a turing machine or other enumerable search procedure

In a module that I taught, I presented part of Hilbert's 10th problem and developed a soft spot for the circle of ideas around termination of algorithms. Also, since I started doing mathematics as an algebraic geometer over an algebraically closed field, it was difficult to come across natural concepts that do not have a decidable first order theory. Seeing number theory really opened to door for the possibility of knowing something, but not being able to compute it!

[Damiano Testa]

Mario Carneiro said:

Also, roption has an interesting topology different from option

I am only beginning to see glimpses of this "topological side" to type theory right now, but this observation (and the one about the disjoint point or the one point compactification) are really helpful! Thanks for these insights!

[Kevin Buzzard]

There are two interpretations of "every constructible function $\mathbb{R}\to\mathbb{R}$ is continuous" -- one is "hey that's a really cool property of constructibility" and the other is "constructive maths is crazy". I veer from one to the other!

[Damiano Testa]

Wait, really every constructible function is continuous? What about the characteristic function of 0? Is this not constructible? Is it continuous at 0?

[Mario Carneiro]

You can't determine if a real number is zero computably

[Kevin Buzzard]

Let $E$ be an explicit elliptic curve over $\mathbb{Q}$ with rank 4. Is $L''(E,1)=0$?

[Kevin Buzzard]

There is no elliptic curve of rank 4 for which the value of $L''(E,1)$ is known!

[Mario Carneiro]

or the sum of $1/i^2$ over all odd perfect numbers $i$

[Damiano Testa]

With these comments, I am tempted to strengthen the above statement to "every constructible function \mathbb{R}\to\mathbb{R}R→R is constant", or even "there are no constructible functions \mathbb{R}\to\mathbb{R}"!

[Mario Carneiro]

the identity function is computable

[Damiano Testa]

... but maybe it is constructibly constant... hahaha

[Damiano Testa]

(In case this was not clear, I am joking! :smile: )

[Mario Carneiro]

more generally, most explicitly given continuous functions are computable, like $\sin x$ or $\sqrt x$ (with $x\ge 0$ as precondition)

[Mario Carneiro]

here computable just means that you can calculate the value out to n decimal places in finite time

[Damiano Testa]

I see, so the issue with continuity is that, for instance, at a point of a jump discontinuity you would not know on which of the two branches you would be with enough precision to know which value to choose?

[Mario Carneiro]

right

[Mario Carneiro]

there will be some finite $\epsilon$ where no amount of precision $\delta$ on the input is good enough to resolve the answer

[Damiano Testa]

Thanks for the explanation!

[Damiano Testa]

I really like the new version: thank you again @Patrick Massot !

In the process of cleaning up, I decided to add the lemma the Reid Barton suggested as well and something strange happened: I end up with having to prove the same goal twice, after applying convert. Why is that? Below I repeat all the code above, but the question is really about the last proof.

import topology.metric_space.basic
import data.polynomial.ring_division

open set

namespace topological_space

lemma forall_open_iff_discrete {X : Type*} [topological_space X] :
  (∀ s : set X, is_open s) ↔ discrete_topology X :=
⟨λ h, ⟨by { ext U ; show is_open U ↔ true, by simp [h U] }⟩,
 by introsI ; exact is_open_discrete _⟩


lemma singletons_open_iff_discrete {X : Type*} [topological_space X] :
  (∀ a : X, is_open ({a} : set X)) ↔ discrete_topology X :=
⟨λ h, ⟨eq_bot_of_singletons_open h⟩, by introsI ; exact is_open_discrete _⟩

lemma subset_singleton_iff {α : Type*} {s : set α} {x : α} : s ⊆ {x} ↔ ∀ y ∈ s, y = x :=
⟨λ h y hy, mem_singleton_iff.mp (h hy),
 λ h y hy, mem_singleton_iff.mpr (h y hy)⟩

open metric

lemma metric.is_open_singleton_iff {X : Type*} [metric_space X] {x : X} :
  is_open ({x} : set X) ↔ ∃ ε > 0, ∀ y, dist y x < ε → y = x :=
by simp [is_open_iff, subset_singleton_iff, mem_ball]

lemma compl_singleton_eq_bUnion_singleton {α : Type*} (x : α) :
  ({x} : set α)ᶜ = ⋃ (y : α) (hy : y ≠ x), {y} :=
by { ext y,  simp }

lemma discrete_of_t1_of_finite {X : Type*} [topological_space X] [t1_space X] [fintype X] :
  discrete_topology X :=
begin
  rw ← singletons_open_iff_discrete,
  intros x,
  rw [← is_closed_compl_iff, compl_singleton_eq_bUnion_singleton x],
  exact is_closed_bUnion (finite.of_fintype _) (λ y _, is_closed_singleton)
end

lemma metric.discrete_of_finite {X : Type*} [metric_space X] [fintype X] : discrete_topology X :=
discrete_of_t1_of_finite

lemma discrete_of_finite {X : Type*} [metric_space X] {s : finset X} :
  discrete_topology {a : X // a ∈ s} :=
discrete_of_t1_of_finite

end topological_space

lemma roots_discrete (f : polynomial ℝ) : discrete_topology {a : ℝ // a ∈ f.roots.to_finset} :=
topological_space.discrete_of_t1_of_finite

lemma polynomial_eval_zero_discrete (f : polynomial ℝ) (hf : f ≠ 0) :
  discrete_topology {a : ℝ // f.eval a = 0} :=
begin
  convert roots_discrete f;  --creates two identical goals, each of which is solved by the commands below
  { ext x,
  rw [multiset.mem_to_finset, (polynomial.mem_roots hf), polynomial.is_root.def] },
end

[Patrick Massot]

I'm happy that you like it. It's good to remember that formalizating is not only playing a computer game where you fight a weird programming language. There is actual mathematical content that can be very satisfying.

[Patrick Massot]

Your new question is definitely more on the weird computer game side. In the type of roots_discrete f, the set (or finset) that is not quite the announced one appear twice: one appearance is clear, the second one is hidden in the topological space structure that discrete_topology needs. So convert bumps into both and is somehow not smart enough to clean up afterwards. This is definitely a technological issue, there should be a better version of convert.

[Damiano Testa]

Ok, thanks for the explanation! I agree that the double appearance of an identical goal is not too important. Still, I am happy with the explanation!

Should I make a pull request with your arguments? :). Or is it too trivial for mathlib?

[Mario Carneiro]

I don't think this is likely to change, as congr is the responsible party and it has no maintainer atm

[Damiano Testa]

Ok, although I meant to have the stuff about discrete topological spaces PR'ed

[Patrick Massot]

There are two interleaved discussion here. Mario, I think convert (and congr') could do a post-processing pass getting rid of duplicate goals, probably testing only for syntactic equality of goals to keep performance under control. Obviously this isn't very high priority. Damiano, please PR all that, it clearly deserves to get in.

[Mario Carneiro]

Actually, that should probably be a tactic on its own

[Mario Carneiro]

which perhaps is used as a post processing step in convert

[Patrick Massot]

We could even run it only if convert is given some flag, this would keep performance in existing cases.

[Damiano Testa]

Ok, I will do the PR, either tomorrow or on Monday!

Regardless of the issue with the duplicate goal, I might introduce the conversion of the "finset" as a separate lemma, and then rw instead of convert.

[Patrick Massot]

Yes, I also wanted to write this and then I forgot.

[Damiano Testa]

Hopefully, this is one of the last details in this thread. I tried to find a good home for the lemmas and below is what I came up with. I am missing a good fit for the last two results. Any suggestions?

Thanks!

import topology.metric_space.basic
import data.polynomial.ring_division

open set

/-- to data.set.basic -/
lemma subset_singleton_iff {α : Type*} {s : set α} {x : α} : s ⊆ {x} ↔ ∀ y ∈ s, y = x :=
⟨λ h y hy, mem_singleton_iff.mp (h hy),
 λ h y hy, mem_singleton_iff.mpr (h y hy)⟩

/-- to data.set.basic -/
lemma compl_singleton_eq_bUnion_singleton {α : Type*} (x : α) :
  ({x} : set α)ᶜ = ⋃ (y : α) (hy : y ≠ x), {y} :=
by { ext y, simp only [exists_prop, mem_Union, mem_singleton_iff, exists_eq_right', mem_compl_eq]}

/-- to topology.order -/
lemma forall_open_iff_discrete {X : Type*} [topological_space X] :
  (∀ s : set X, is_open s) ↔ discrete_topology X :=
⟨λ h, ⟨by { ext U , show is_open U ↔ true, simp [h U] }⟩,
 λ a, @is_open_discrete _ _ a⟩

/-- to topology.order -/
lemma singletons_open_iff_discrete {X : Type*} [topological_space X] :
  (∀ a : X, is_open ({a} : set X)) ↔ discrete_topology X :=
⟨λ h, ⟨eq_bot_of_singletons_open h⟩, λ a _, @is_open_discrete _ _ a _⟩

/-- to topology.separation -/
lemma discrete_of_t1_of_finite {X : Type*} [topological_space X] [t1_space X] [fintype X] :
  discrete_topology X :=
begin
  apply singletons_open_iff_discrete.mp,
  intros x,
  rw [← is_closed_compl_iff, compl_singleton_eq_bUnion_singleton x],
  exact is_closed_bUnion (finite.of_fintype _) (λ y _, is_closed_singleton)
end

open metric

/-- to topology.metric_space.basic -/
lemma metric.is_open_singleton_iff {X : Type*} [metric_space X] {x : X} :
  is_open ({x} : set X) ↔ ∃ ε > 0, ∀ y, dist y x < ε → y = x :=
by simp [is_open_iff, subset_singleton_iff, mem_ball]

/-- to topology.metric_space.basic -/
lemma metric.discrete_of_fintype {X : Type*} [metric_space X] [fintype X] : discrete_topology X :=
discrete_of_t1_of_finite

/-- to topology.metric_space.basic -/
lemma metric.discrete_of_finite {X : Type*} [metric_space X] {s : finset X} :
  discrete_topology {a : X // a ∈ s} :=
discrete_of_t1_of_finite

/-- to data.polynomial.ring_division -/
lemma polynomial.eval_zero_eq_roots {f : polynomial ℝ} (hf : f ≠ 0) :
  (λ (a : ℝ), polynomial.eval a f = 0) = (λ (a : ℝ), a ∈ f.roots.to_finset) :=
by { ext, simp only [multiset.mem_to_finset, (polynomial.mem_roots hf), polynomial.is_root.def] }

/-- I could not find a good home for these last two results
The following result does not require the assumption that `f` be non-zero, as
`0.roots` is defined to be `∅`.
-/
lemma roots_discrete (f : polynomial ℝ) : discrete_topology {a : ℝ // a ∈ f.roots.to_finset} :=
discrete_of_t1_of_finite

lemma polynomial_eval_zero_discrete {f : polynomial ℝ} (hf : f ≠ 0) :
  discrete_topology {a : ℝ // f.eval a = 0} :=
begin
  rw polynomial.eval_zero_eq_roots hf,
  exact roots_discrete f,
end

[Damiano Testa]

Dear All,

I just created #5298 adding almost all these lemmas in their appropriate places!

Lean is now building it and we'll see what it does not like!

[Yury G. Kudryashov]

I left some comments.

[Damiano Testa]

Thank you very much for your comments! I have implemented all of them, except the very last one. I left a more expanded comment in the PR.

Thanks again!
:pray:

[Johan Commelin]

@Damiano Testa thanks a lot for doing this :thumbs_up:

[Damiano Testa]

Thank you all to those who contributed to cleaning up and polishing the PR: this is now in mathlib!