# Zulip Chat Archive

## Stream: maths

### Topic: o-minimality repo

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

#### Kevin Buzzard (Aug 28 2020 at 08:21):

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

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

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

#### 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

#### 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!

#### 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:

#### 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

#### Aaron Anderson (Aug 28 2020 at 16:38):

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

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

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

#### 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

#### 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

#### Reid Barton (Aug 28 2020 at 16:45):

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

#### Johan Commelin (Aug 28 2020 at 16:45):

Certainly `o_minimal.tame`

can have only one meaning (-;

#### Reid Barton (Aug 28 2020 at 16:45):

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

#### Reid Barton (Aug 28 2020 at 16:46):

Naming improvement suggestions are more than welcome

#### 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

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

#### Aaron Anderson (Aug 28 2020 at 16:48):

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

#### 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

#### 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

#### 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

#### Adam Topaz (Aug 28 2020 at 17:18):

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

#### Johan Commelin (Aug 28 2020 at 17:26):

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

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

#### Reid Barton (Aug 28 2020 at 17:35):

It's sort of like `eqv_gen`

and `setoid`

#### 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

#### 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

#### Aaron Anderson (Aug 29 2020 at 22:43):

Then `o_minimal.tame`

is just constructible in the order topology

#### Aaron Anderson (Aug 29 2020 at 22:44):

And of course it works for ACF also

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

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

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

#### 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

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

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

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

#### Aaron Anderson (Aug 31 2020 at 04:40):

Johan Commelin said:

Aaron Anderson said:

Then

`o_minimal.tame`

is just constructible in the order topologyI'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 (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`

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

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

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

#### Johan Commelin (Aug 31 2020 at 05:05):

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

#### Johan Commelin (Aug 31 2020 at 05:06):

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

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

#### 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

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

#### Aaron Anderson (Aug 31 2020 at 05:08):

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

#### Johan Commelin (Aug 31 2020 at 05:12):

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

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

#### 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

#### 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

#### 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

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

#### 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
`∀ i`

s 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 (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