o-minimality repo

Stream: maths

[Johan Commelin]

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.

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

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.

[Kevin Buzzard]

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

[Rob Lewis]

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!

[Reid Barton]

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

[Rob Lewis]

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

[Aaron Anderson]

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

[Reid Barton]

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.

[Reid Barton]

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.

[Aaron Anderson]

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

[Aaron Anderson]

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

[Reid Barton]

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

[Johan Commelin]

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

[Reid Barton]

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

[Reid Barton]

Naming improvement suggestions are more than welcome

[Aaron Anderson]

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

[Reid Barton]

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.

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Adam Topaz]

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

[Johan Commelin]

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

[Reid Barton]

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.

[Reid Barton]

It's sort of like eqv_gen and setoid

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

Then o_minimal.tame is just constructible in the order topology

[Aaron Anderson]

And of course it works for ACF also

[Reid Barton]

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.

[Reid Barton]

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).

[Aaron Anderson]

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.

[Aaron Anderson]

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

[Aaron Anderson]

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.

[Johan Commelin]

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.

[Johan Commelin]

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 $\bigcup_{n \in 2 \mathbb{Z}} (n, n+1)$ is constructible, hence tame? That seems wrong.

[Aaron Anderson]

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 $\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.

[Aaron Anderson]

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

[Johan Commelin]

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.

[Aaron Anderson]

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

[Johan Commelin]

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

[Johan Commelin]

Saying $S \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, g$ that realize to $S, T$, and hence $f \land g$ realizes to $S \cap T$, therefore it is definable.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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.

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Johan Commelin]

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

[Aaron Anderson]

• 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`

[Jesse Michael Han]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Jesse Michael Han]

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 },

[Reid Barton]

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

$$\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.

[Reid Barton]

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.