tactic.unfreeze_local_instances

Stream: general

[Kenny Lau]

import analysis.topology.topological_space
universe u
open set
local attribute [instance] classical.prop_decidable
class t0_space (α : Type u) [topological_space α] : Prop :=
(t0 : ∀ x y, x ≠ y → ∃ U:set α, is_open U ∧ (xor (x ∈ U) (y ∈ U)))

theorem exists_open_singleton_of_fintype
  (α : Type u) [topological_space α] [t0_space α]
  [f : fintype α] [decidable_eq α] [ha : nonempty α] :
  ∃ x:α, is_open ({x}:set α) :=
have H : ∀ (T : finset α), T ≠ ∅ → ∃ x ∈ T, ∃ u, is_open u ∧ {x} = {y | y ∈ T} ∩ u :=
begin
  intro T,
  apply finset.case_strong_induction_on T,
  { intro h, exact (h rfl).elim },
  { intros x S hxS ih h,
    by_cases hs : S = ∅,
    { existsi [x, finset.mem_insert_self x S, univ, is_open_univ],
      rw [hs, inter_univ], refl },
    { rcases ih S (finset.subset.refl S) hs with ⟨y, hy, V, hv1, hv2⟩,
      by_cases hxV : x ∈ V,
      { cases t0_space.t0 x y (λ hxy, hxS $ by rwa hxy) with U hu,
        rcases hu with ⟨hu1, ⟨hu2, hu3⟩ | ⟨hu2, hu3⟩⟩,
        { existsi [x, finset.mem_insert_self x S, U ∩ V, is_open_inter hu1 hv1],
          apply set.ext,
          intro z,
          split,
          { intro hzx,
            rw set.mem_singleton_iff at hzx,
            rw hzx,
            exact ⟨finset.mem_insert_self x S, ⟨hu2, hxV⟩⟩ },
          { intro hz,
            rw set.mem_singleton_iff,
            rcases hz with ⟨hz1, hz2, hz3⟩,
            cases finset.mem_insert.1 hz1 with hz4 hz4,
            { exact hz4 },
            { have h1 : z ∈ {y : α | y ∈ S} ∩ V,
              { exact ⟨hz4, hz3⟩ },
              rw ← hv2 at h1,
              rw set.mem_singleton_iff at h1,
              rw h1 at hz2,
              exact (hu3 hz2).elim } } },
        { existsi [y, finset.mem_insert_of_mem hy, U ∩ V, is_open_inter hu1 hv1],
          apply set.ext,
          intro z,
          split,
          { intro hz,
            rw set.mem_singleton_iff at hz,
            rw hz,
            refine ⟨finset.mem_insert_of_mem hy, hu2, _⟩,
            have h1 : y ∈ {y} := set.mem_singleton y,
            rw hv2 at h1,
            exact h1.2 },
          { intro hz,
            rw set.mem_singleton_iff,
            cases hz with hz1 hz2,
            cases finset.mem_insert.1 hz1 with hz3 hz3,
            { rw hz3 at hz2,
              exact (hu3 hz2.1).elim },
            { have h1 : z ∈ {y : α | y ∈ S} ∩ V := ⟨hz3, hz2.2⟩,
              rw ← hv2 at h1,
              rw set.mem_singleton_iff at h1,
              exact h1 } } } },
      { existsi [y, finset.mem_insert_of_mem hy, V, hv1],
        apply set.ext,
        intro z,
        split,
        { intro hz,
          rw set.mem_singleton_iff at hz,
          rw hz,
          split,
          { exact finset.mem_insert_of_mem hy },
          { have h1 : y ∈ {y} := set.mem_singleton y,
            rw hv2 at h1,
            exact h1.2 } },
        { intro hz,
          rw hv2,
          cases hz with hz1 hz2,
          cases finset.mem_insert.1 hz1 with hz3 hz3,
          { rw hz3 at hz2,
            exact (hxV hz2).elim },
          { exact ⟨hz3, hz2⟩ } } } } }
end,
begin
  tactic.unfreeze_local_instances,
  cases ha with x,
  specialize H finset.univ (finset.ne_empty_of_mem $ finset.mem_univ x),
  rcases H with ⟨y, hyf, U, hu1, hu2⟩,
  existsi y,
  have h1 : {y : α | y ∈ finset.univ} = (univ : set α),
  { exact set.eq_univ_of_forall (λ x : α,
      by rw mem_set_of_eq; exact finset.mem_univ x) },
  rw h1 at hu2,
  rw set.univ_inter at hu2,
  rw hu2,
  exact hu1
end

[Kenny Lau]

Why do I need tactic.unfreeze_local_instances there?

[Kenny Lau]

(working example, but clearly not minimal)

[Mario Carneiro]

because it's a typeclas arg left of the colon

[Mario Carneiro]

you can use unfreezeI for short

[Kenny Lau]

I don't understand

[Kenny Lau]

isn't every typeclass argument left of colon?

[Chris Hughes]

You don't usually do cases on type class args

[Kenny Lau]

yeah even if I don't do cases it still messes up

[Mario Carneiro]

anything that disrupts the context past the position of the colon will require unfreezeI

[Mario Carneiro]

in this case you can do cases id ha with a if you don't want to clear the hypothesis in the context

[Kenny Lau]

oh, I get it now

[Kenny Lau]

oh and how would you golf the proof?

[Mario Carneiro]

I've been thinking about that... that proof is a little scary long

[Mario Carneiro]

Maybe you can find a maximal element in the specialization preorder?

[Kenny Lau]

I don't understand what you mean by the specialization preorder

[Mario Carneiro]

okay, I refreshed my memory on the specialization preorder and indeed this proof should work (although it is a minimal element by wiki's definition)

[Mario Carneiro]

it's basically finite zorn's lemma

[Kevin Buzzard]

A point x specialises to a point y if y is in the closure of x

[Mario Carneiro]

I think that's the reverse of wiki's terminology?

[Mario Carneiro]

they say y is a specialization of x in that case

[Mario Carneiro]

they also say that the orientation is contentious

[Kevin Buzzard]

Darn Zulip app doesn't show me new posts when they arrive

[Kevin Buzzard]

Including my own

[Kevin Buzzard]

Right -- x specialises to y, so y is a specialisation of x.

[Mario Carneiro]

okay, I wasn't sure about the active verb there

[Kevin Buzzard]

This is how the words are used in algebraic geometry at least

[Mario Carneiro]

You should look at the wiki page and decide which order of le makes sense

[Mario Carneiro]

I'm leaning to the first definition, x <= y means x is a specialization of y, because the evidence from algebraic geometry using Spec R smacks of that order-reversing filter thing

[Reid Barton]

The ordering I have seen is the one which is equivalent to x \le y if closure({x}) is a subset of closure({y})

[Reid Barton]

Actually, I'm not sure which way it goes now and my source is at home

[Mario Carneiro]

I'm not sure why this argument doesn't extend to the infinite case by zorn's lemma though

[Mario Carneiro]

Obviously it's not true for R so I'm missing a part of the argument

[Kenny Lau]

https://github.com/leanprover/mathlib/pull/448

[Kevin Buzzard]

Obviously it's not true for R so I'm missing a part of the argument

For sensible spaces like R the preorder is just "x<=y iff x=y". So there are maximal and minimal elements, but these do not correspond to open singletons.

[Reid Barton]

Okay, the paper where I've encountered this actually says "... so that $\le_X$ is the well-known [4] reflexive and transitive relation $y \in \{x\}^-$", so I did have this backwards.

[Reid Barton]

After being confused by this for a while, my conclusion is that the "$x$ specializes to $y$" relation is actually different in algebraic geometry and in domain theory

[Reid Barton]

one of them has to do with closed sets, the other with open sets

[Reid Barton]

Because of the duality between open and closed sets, this appears as a reversal of the order

[Kevin Buzzard]

In algebraic geometry, a "generic point" of an irreducible algebraic variety is a rigorous notion of the intuitive idea of how a general point on the variety behaves. Historically this was done in a vague way -- we had the "actual points" and then "it's true for a generic point" just meant "most points satisfy this" with several, sometimes competing definitions of "most", but with Grothendieck's approach we have the luxury of the generic point actually being a point in the top space, whose topological closure is the entire variety. The idea is that a generic point can specialise to a random "actual point", which is then a specialisation of the generic point. Perhaps the simplest example of this is the two-point topological space with one closed and one open point. A fruitful mental model of this space in geometry is that the whole space is the open unit disc, the closed point is the origin, and the open point is all the other points -- a "general" point in the open disc. If $\eta$ is the generic point and $s$ the closed point then the sequence $\eta,\eta,\eta,\ldots$ converges to $s$ (as well as to $\eta$), which is the specialisation in action. One cna think of it as a bunch of points in the punctured disc tending to the origin.

[Gabriel Ebner]

BTW, since I just grepped for unfreeze in mathlib and was surprised by how often it turns up: please don't use tactic.unfreeze_local_instances. This is a huge performance problem since it disables the local instance cache. Please use tactics like substI, casesI, unfreezingI { ... }, etc. instead. And if all that doesn't work, please use tactic.reset_instance_cache. Please never use tactic.unfreeze_local_instances.

[Arthur Paulino]

I had no idea. Sorry if something I wrote used it and made it to master

[Kyle Miller]

It might help if Lean didn't suggest using it. There are two places in the Lean repository that say "try tactic.unfreeze_local_instances" or "use tactic tactic.unfreeze_local_instances". library/init/meta/tactic.lean and src/library/type_context.cpp

[Johan Commelin]

Can we lint against this? Also, are the suggested alternatives available in core, or are they partly mathlib?

[Mario Carneiro]

The exactI etc tactics are in mathlib, but it wouldn't be the first time lean error messages make reference to things in mathlib

[Mario Carneiro]

But also, they have very few prerequisites so we could just move them to core