Zulip Chat Archive

Stream: general

Topic: tactic.unfreeze_local_instances


Kenny Lau (Oct 28 2018 at 21:43):

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 (Oct 28 2018 at 21:43):

Why do I need tactic.unfreeze_local_instances there?

Kenny Lau (Oct 28 2018 at 21:44):

(working example, but clearly not minimal)

Mario Carneiro (Oct 28 2018 at 21:50):

because it's a typeclas arg left of the colon

Mario Carneiro (Oct 28 2018 at 21:51):

you can use unfreezeI for short

Kenny Lau (Oct 28 2018 at 21:57):

I don't understand

Kenny Lau (Oct 28 2018 at 21:57):

isn't every typeclass argument left of colon?

Chris Hughes (Oct 28 2018 at 22:26):

You don't usually do cases on type class args

Kenny Lau (Oct 28 2018 at 22:26):

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

Mario Carneiro (Oct 28 2018 at 22:42):

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

Mario Carneiro (Oct 28 2018 at 22:43):

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 (Oct 28 2018 at 22:44):

oh, I get it now

Kenny Lau (Oct 28 2018 at 22:45):

oh and how would you golf the proof?

Mario Carneiro (Oct 28 2018 at 22:45):

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

Mario Carneiro (Oct 28 2018 at 22:45):

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

Kenny Lau (Oct 28 2018 at 22:53):

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

Mario Carneiro (Oct 28 2018 at 22:54):

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 (Oct 28 2018 at 22:54):

it's basically finite zorn's lemma

Kevin Buzzard (Oct 28 2018 at 22:55):

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

Mario Carneiro (Oct 28 2018 at 22:56):

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

Mario Carneiro (Oct 28 2018 at 22:56):

they say y is a specialization of x in that case

Mario Carneiro (Oct 28 2018 at 22:57):

they also say that the orientation is contentious

Kevin Buzzard (Oct 28 2018 at 22:57):

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

Kevin Buzzard (Oct 28 2018 at 22:58):

Including my own

Kevin Buzzard (Oct 28 2018 at 22:59):

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

Mario Carneiro (Oct 28 2018 at 22:59):

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

Kevin Buzzard (Oct 28 2018 at 23:00):

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

Mario Carneiro (Oct 28 2018 at 23:02):

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

Mario Carneiro (Oct 28 2018 at 23:03):

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 (Oct 28 2018 at 23:19):

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 (Oct 28 2018 at 23:23):

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

Mario Carneiro (Oct 28 2018 at 23:36):

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

Mario Carneiro (Oct 28 2018 at 23:36):

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

Kenny Lau (Oct 29 2018 at 02:46):

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

Kevin Buzzard (Oct 29 2018 at 07:56):

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 (Oct 29 2018 at 12:38):

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

Reid Barton (Oct 29 2018 at 14:10):

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

Reid Barton (Oct 29 2018 at 14:11):

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

Reid Barton (Oct 29 2018 at 14:12):

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

Kevin Buzzard (Oct 29 2018 at 15:52):

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 ss the closed point then the sequence η,η,η,\eta,\eta,\eta,\ldots converges to ss (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 (Jan 09 2022 at 21:12):

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 (Jan 09 2022 at 21:24):

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

Kyle Miller (Jan 09 2022 at 21:41):

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 (Jan 10 2022 at 06:46):

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

Mario Carneiro (Jan 10 2022 at 07:50):

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 (Jan 10 2022 at 07:50):

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


Last updated: Dec 20 2023 at 11:08 UTC