Zulip Chat Archive

Stream: maths

Topic: o-minimality repo


view this post on Zulip Johan Commelin (Aug 28 2020 at 08:16):

Several people have expressed interest in model theory and o-minimality (cc @Aaron Anderson). For quite some time @Reid Barton and I have been working on a project (with and without lean) involving o-minimality. On the Lean side, it took a while to get something that we are happy with. Since others have also started work in this direction, we've decided to open up our repo, so others can take a look: https://github.com/rwbarton/lean-omin
Note that we take a very non-model-theoretic approach to the definitions. We believe that both versions should exist, with an interface between them. The model theoretic approach is suited for reasoning about (o-minimal) structures, whereas our hands-on approach is (we think) better for actually working with specific examples.

Our two "showcases": we've proven the first part of monotonicity and constructed the o-minimal structure of semilinear sets/functions.

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 08:21):

What is the situation regarding the missing tactic which Reid talked about in his Pittsburgh talk?

view this post on Zulip Johan Commelin (Aug 28 2020 at 08:24):

We don't really have a dedicated tactic yet, but it won't be hard to write it now.

view this post on Zulip Johan Commelin (Aug 28 2020 at 08:24):

It can be very similar to continuity. We have the "basic lemmas" that it should try to apply. And then there should maybe be a bit of convenience wrapping around it.

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 09:01):

Isn't it amazing that ideas coming from one area of formalization can be used in another? This push just to "get math done" goes off in many directions but the things we learn all somehow feed back into each other

view this post on Zulip Rob Lewis (Aug 28 2020 at 09:46):

Ooh, a new project repo. Install some Actions, add it to the contrib list, and it will show up on the brand new web page!

view this post on Zulip Reid Barton (Aug 28 2020 at 14:35):

This is on my todo list, though I think the project already doesn't build with the latest mathlib :face_palm:

view this post on Zulip Rob Lewis (Aug 28 2020 at 14:37):

One purpose of the table at the bottom of that page is to shame people into keeping their projects updated

view this post on Zulip Aaron Anderson (Aug 28 2020 at 16:38):

Does van den Dries ever actually define "tame" that way?

view this post on Zulip Reid Barton (Aug 28 2020 at 16:42):

No, I think the book just says "a finite union of intervals and points", and doesn't actually ever use the term "tame" at all, so it seemed like a convenient opportunity to define "tame" to mean something.

view this post on Zulip Reid Barton (Aug 28 2020 at 16:43):

I also made up some words in the construction of the simple / semilinear o-minimal structures like "isolating" that probably have a real name in model theory.

view this post on Zulip Aaron Anderson (Aug 28 2020 at 16:43):

Coloquially model theorists tend to use "tame" to mean a larger class of things, although I don't think we use it as a technical word

view this post on Zulip Aaron Anderson (Aug 28 2020 at 16:44):

It basically refers to any structure where only a small collection of well-behaved sets are definable

view this post on Zulip Reid Barton (Aug 28 2020 at 16:45):

So here I need a word for precisely those "well-behaved" sets

view this post on Zulip Johan Commelin (Aug 28 2020 at 16:45):

Certainly o_minimal.tame can have only one meaning (-;

view this post on Zulip Reid Barton (Aug 28 2020 at 16:45):

at least, once you know what a DUNLO is :upside_down:

view this post on Zulip Reid Barton (Aug 28 2020 at 16:46):

Naming improvement suggestions are more than welcome

view this post on Zulip Aaron Anderson (Aug 28 2020 at 16:46):

Yeah, I don't have a problem with o_minimal.tame for now, I just wanted to point out that we'd also refer to the definable sets of an algebraically closed field or something as tame, even when there's no order involved

view this post on Zulip Reid Barton (Aug 28 2020 at 16:47):

By the way, for those interested in the model theory of real closed fields, Johan and I have no intention of proving that the semialgebraic structure is o-minimal, and we'd be quite happy if such a theorem (or the hard part of such a theorem, maybe formulated differently) were to magically appear.

view this post on Zulip Aaron Anderson (Aug 28 2020 at 16:48):

Yeah, I do have the intention of formalizing Tarski-Seidenberg

view this post on Zulip Aaron Anderson (Aug 28 2020 at 16:49):

I think the first thing I could do really is relate this definability-only definition of a structure to the functions-and-relations one

view this post on Zulip Aaron Anderson (Aug 28 2020 at 16:51):

I find that it's pretty easy to port the flypitch definition of a structure and start defining model theory things with that, but I haven't made any serious attempt to actually port formulas

view this post on Zulip Aaron Anderson (Aug 28 2020 at 16:52):

but there's a surprising amount of model theory you can define without formulas, including the category of definable sets as you've seen, and back-and-forth arguments

view this post on Zulip Adam Topaz (Aug 28 2020 at 17:18):

The word "tame" came from Grothendieck (the esquisse, I think).

view this post on Zulip Johan Commelin (Aug 28 2020 at 17:26):

Yup, but he didn't define it (-;

view this post on Zulip Reid Barton (Aug 28 2020 at 17:35):

Aaron Anderson said:

I think the first thing I could do really is relate this definability-only definition of a structure to the functions-and-relations one

Yes, if you have a (model-theoretic) structure for a language, its definable sets form a struc, and conversely, if you have a struc then you could form the language whose relation symbols are given by all the definable sets.

view this post on Zulip Reid Barton (Aug 28 2020 at 17:35):

It's sort of like eqv_gen and setoid

view this post on Zulip Aaron Anderson (Aug 28 2020 at 17:36):

We can maybe make struc an instance for L-structures, but it depends on the choice of language

view this post on Zulip Aaron Anderson (Aug 29 2020 at 22:43):

I know the naming isn’t so important yet, but here’s a concept: a constructible set of a topological space is a boolean combination of open/closed sets

view this post on Zulip Aaron Anderson (Aug 29 2020 at 22:43):

Then o_minimal.tame is just constructible in the order topology

view this post on Zulip Aaron Anderson (Aug 29 2020 at 22:44):

And of course it works for ACF also

view this post on Zulip Reid Barton (Aug 31 2020 at 01:26):

Kevin Buzzard said:

What is the situation regarding the missing tactic which Reid talked about in his Pittsburgh talk?

We've just gotten to the point where we can state and prove the statements in question by hand in the first place. I wrote this proof and this proof manually; these are two of the examples from the talk. As you can see it's already not that pleasant to write the proofs by hand.

view this post on Zulip Reid Barton (Aug 31 2020 at 01:29):

As Johan says the hope is to use something like the continuity tactic to produce these proofs automatically, although the space of problems we want to handle is more complicated (involving both definable sets and definable functions, and in the future possibly higher-order notions of definability).

view this post on Zulip Aaron Anderson (Aug 31 2020 at 01:32):

While a tactic would be nice for those things, I think a flypitch-ish encoding of formulas should be able to get us most of the way.

view this post on Zulip Aaron Anderson (Aug 31 2020 at 01:34):

At least, I think writing the flypitchishly formal version of the defining formula wouldn't be too bad, although eventually a tactic could do it

view this post on Zulip Aaron Anderson (Aug 31 2020 at 01:36):

And then we'd just need a theorem that says that def_set is equivalent to there existing some formula whose realization is exactly the set in question.

view this post on Zulip Johan Commelin (Aug 31 2020 at 02:54):

Sure, but you still don't want to do this by hand, because when I just wrote down a set that is obviously definable, I simply want the system to notice this.

view this post on Zulip Johan Commelin (Aug 31 2020 at 02:55):

Aaron Anderson said:

Then o_minimal.tame is just constructible in the order topology

I'm confused. Doesn't this mean that the infinite union of open intervals n2Z(n,n+1)\bigcup_{n \in 2 \mathbb{Z}} (n, n+1) is constructible, hence tame? That seems wrong.

view this post on Zulip Aaron Anderson (Aug 31 2020 at 04:40):

Johan Commelin said:

Aaron Anderson said:

Then o_minimal.tame is just constructible in the order topology

I'm confused. Doesn't this mean that the infinite union of open intervals n2Z(n,n+1)\bigcup_{n \in 2 \mathbb{Z}} (n, n+1) is constructible, hence tame? That seems wrong.

Yeah, you're right, constructible and tame are totally different here.

view this post on Zulip Aaron Anderson (Aug 31 2020 at 04:43):

Johan Commelin said:

Sure, but you still don't want to do this by hand, because when I just wrote down a set that is obviously definable, I simply want the system to notice this.

Like I said, I agree that this tactic should exist eventually, but it looks to me that the most annoying part of the job is showing that the set realized by a given formula is actually a def_set

view this post on Zulip Johan Commelin (Aug 31 2020 at 05:00):

But in our current setup, there are no formulas. Showing that a set is definable typically amounts to hitting it with "definable sets are a boolean algebra" several times.

view this post on Zulip Aaron Anderson (Aug 31 2020 at 05:02):

Right, and that's the part that could be eliminated "just" with porting some flypitch and proving our two definitions of definable are equivalent.

view this post on Zulip Johan Commelin (Aug 31 2020 at 05:03):

I don't see how that would make proving that a certain set is definable any easier in practice.

view this post on Zulip Johan Commelin (Aug 31 2020 at 05:05):

Saying STS \cap T is definable, because it is the intersection of two definable sets, seems a lot shorter than saying, oh well, there are formulas f,gf, g that realize to S,TS, T, and hence fgf \land g realizes to STS \cap T, therefore it is definable.

view this post on Zulip Johan Commelin (Aug 31 2020 at 05:05):

I very much agree that what you are suggesting should be in mathlib. It will be important and useful.

view this post on Zulip Johan Commelin (Aug 31 2020 at 05:06):

But I don't think it will help with this particular issue.

view this post on Zulip Johan Commelin (Aug 31 2020 at 05:06):

Rather, I like it because it will allow me to say that a certain set is definable without parameters, things like that. That stuff that simply cannot be expressed in our current framework.

view this post on Zulip Aaron Anderson (Aug 31 2020 at 05:08):

The way that @Reid Barton stuctures one of the proofs goes like this:

  • Take a look at this predicate which is visibly-to-a-human first-order
  • Quickly show with ext that it defines the set I want to show is definable
  • Spend a long time applying boolean algebra and projection axioms

view this post on Zulip Aaron Anderson (Aug 31 2020 at 05:08):

I don't think we can automate the first bullet point without a tactic, and the second one seems inevitable, and not a problem.

view this post on Zulip Aaron Anderson (Aug 31 2020 at 05:08):

It's the 3rd one that I think can be simplified with this proof structure:

view this post on Zulip Johan Commelin (Aug 31 2020 at 05:12):

Ok, fair enough. I agree that there a places where this would significantly shorten the proof.

view this post on Zulip Aaron Anderson (Aug 31 2020 at 05:12):

  • Take a look at this explicit first-order formula that's just as easy to write as the Lean predicate
  • Show the set that it realizes is the set satisfied by set you want, this step should still be easy once we have a simp-set for unfolding the recursive definition of formula realization, and maybe that already exists in flypitch
  • Use a theorem which says def_set S is equivalent to "there exists a formula whose realization is S`

view this post on Zulip Jesse Michael Han (Aug 31 2020 at 05:15):

that will be painful with flypitch-style model theory

it's easier to just do backward chaining with definability lemmas than synthesize a formula and apply a soundness theorem, even if the search for definability lemmas can be phrased in terms of synthesizing a first-order formula

view this post on Zulip Aaron Anderson (Aug 31 2020 at 05:20):

I'm willing to consider that synthesizing a first-order formula with a tactic might be more difficult than I would first guess, but I still think that it'd be more straightforward when you're working manually, because a lot of model theory texts already have the formulas written out

view this post on Zulip Aaron Anderson (Aug 31 2020 at 05:22):

In any case, I don't think it matters much just yet, because we're still a long way from having either theorems about first-order formulas or a tactic

view this post on Zulip Jesse Michael Han (Aug 31 2020 at 05:57):

in the end, the same work must be done, regardless of whether the search tree is reified as a formula or how the work is split between Lean and the user

In any case, I don't think it matters much just yet, because we're still a long way from having either theorems about first-order formulas or a tactic

you might be surprised, as tidy is OP:

import tactic.tidy
import .definable

open o_minimal

namespace tactic

meta def definability_tactics (md : transparency := reducible) : list (tactic string) :=
[
  assumption *> pure "assumption",
  `[apply def_fun_subtype_val] *> pure "apply def_fun_subtype_val",
  `[apply def_fun.id] *> pure "apply def_fun.id",
  `[apply def_fun.fst] *> pure "apply def_fun.fst",
  `[apply def_fun.snd] *> pure "apply def_fun.snd",
  `[apply def_fun.id] *> pure "apply def_fun.id",
  `[apply def_fun_const] *> pure "apply def_fun_const",
  `[apply def_val_const] *> pure "apply def_val_const",
  `[apply def_fun.image] *> pure "apply def_fun.image",
  `[apply def_fun.comp] *> pure "apply def_fun.comp",
  `[apply def_fun.preimage] *> pure "apply def_fun.preimage",
  `[apply def_set.imp] *> pure "apply def_set.imp",
  `[apply def_set_eq] *> pure "apply def_set_eq",
  `[apply definable_le] *> pure "apply definable_le",
  `[apply def_set.forall] *> pure "apply def_set.forall",
  `[apply def_set.prod] *> pure "apply def_set.prod"
]

namespace interactive
setup_tactic_parser

meta def definability (trace : parse $ optional $ tk "?") : tactic unit :=
tactic.tidy { tactics := definability_tactics reducible, trace_result := trace.is_some }

end interactive
end tactic
   have finite_fibers : ∀ z, finite (f ⁻¹' {z}),
   { intro z,
     have : def_set S (subtype.val '' (f ⁻¹' {z})),
-    { apply def_fun.image,
-      exact def_fun_subtype_val,
-      exact def_fun.preimage hf def_val_const },
+    { definability },


-  have : def_set S (subtype.val '' K) := begin
-    apply def_fun.image def_fun_subtype_val,
-    -- TODO: automate this proof
-    apply def_set.forall,
-    apply def_set.imp,
-    apply def_set_eq,
-    exact hf.comp def_fun.fst,
-    exact hf.comp def_fun.snd,
-    -- TODO: definable_le instance for Ioo
-    change def_set S {p : Ioo a b × Ioo a b | p.1.val ≤ p.2.val},
-    apply definable_le,
-    exact def_fun_subtype_val.comp def_fun.fst,
-    exact def_fun_subtype_val.comp def_fun.snd
-  end,
+  have : def_set S (subtype.val '' K) :=
+    by { definability, change def_set S {p : Ioo a b × Ioo a b | p.1.val ≤ p.2.val}, definability },

view this post on Zulip Reid Barton (Aug 31 2020 at 11:23):

Aaron Anderson said:

I'm willing to consider that synthesizing a first-order formula with a tactic might be more difficult than I would first guess, but I still think that it'd be more straightforward when you're working manually, because a lot of model theory texts already have the formulas written out

It is less straightforward than it might appear; for example, in def_interior's

    {x |  (l u : fin _  R), ( i, l i < coords R x i  coords R x i < u i)
           y, ( i, l i < coords R y i  coords R y i < u i)  y  s},
  • The ∃ l u, ∀ y quantifiers bind n R-valued variables, not just one. Furthermore, the ∀ y one implicitly restricts y to the subset X of R^n.
  • On the other hand, the ∀ is aren't actually quantifiers in the first-order language at all, but rather a way to express a conjunction of a variable number of formulas. The formula written out looks something like

l1,,ln,u1,,un,l1<x1<u1ln<xn<un(y1,,yn,l1<y1<u1ln<yn<un    (y1,,yn)S)\exists l_1, \ldots, l_n, u_1, \ldots, u_n, l_1 < x_1 < u_1 \wedge \cdots \wedge l_n < x_n < u_n \wedge \\ (\forall y_1, \ldots, y_n, l_1 < y_1 < u_1 \wedge \cdots \wedge l_n < y_n < u_n \implies (y_1, \ldots, y_n) \in S)

  • We have to find some way to handle the condition "y ∈ s", using the hypothesis that s is definable.

view this post on Zulip Reid Barton (Aug 31 2020 at 11:28):

The nice thing about just applying lemmas rather than writing down some term of an inductive type is that you don't have to decide up front what the rules for building formulas are--you can keep extending your collection of lemmas as needed.


Last updated: May 10 2021 at 07:15 UTC