(ModelTheory)Automation for proving first-order definability

Stream: mathlib4

[Zikang Yu]

I am currently working on formalizing some model theory in Lean (specifically o-minimality).

Context: Assume we are working in a structure M that expands a dense linear order. By "definable," I mean definable with parameters from the universe.

The Problem: I frequently need to introduce definitions that are intuitively first-order definable. For instance, given a definable function on an interval $f : I \to M$, I define an "ascending point" essentially as:

$$x \in I \land \exists y (y \in I \land \forall u (y<u<x \to f(u) < f(x))) \land \exists z (z \in I \land \forall v (x<v<z \to f(x)<f(v)))$$

(Note that $f$ and $I$ are also definable.)

And its formal definition is as following:

def IsAscendingAt (I : Set M) (f : M → M) (x : M) : Prop :=
  x ∈ I ∧
  (∃ y, y ∈ I ∧ (∀ u, y < u ∧ u < x → f u < f x)) ∧
  (∃ z, z ∈ I  ∧ (∀ v, x < v ∧ v < z → f x < f v))

Currently, for every such definition (even for simple ones like open intervals Ioo a b), I have to manually prove Set.Definable for them. This involves manually constructing the FirstOrder.Language.Formula term and unfolding definitions, which feels very repetitive and tedious.

My Question: Is there existing a best practice to handle this? Or should we develop a tactic similar to measurability or continuity that can inspect the logical structure of the Prop and infer its definability. We could potentially go even further: similar to how @[to_additive] automatically creates additive versions, could we envision an attribute like @[definable] that automatically generates the proof of definability for a given definition for some Set M? Perhaps some advanced metaprogramming techniques would be useful here?

[Aaron Anderson]

I think there are some possible tactics and refactors that would help with this process, but there's already a better way to prove this sort of thing than writing the whole first-order formula from scratch.

[Aaron Anderson]

Definable sets satisfy certain closure properties, such as definable sets of a particular "dimension" forming a Boolean algebra.

[Aaron Anderson]

You may have to start with a few basic applications of the definition of definability, but you can bootstrap up with these lemmas.

[Aaron Anderson]

For a concrete instance of what I mean, if I was trying to prove definability of your IsAscendingAt, I'd apply docs#Set.Definable.inter to break it down into 3 simpler definability statements (one of which should be the assumption, missing here, that I itself is definable.)

[Aaron Anderson]

To deal with quantifiers, you can use lemmas such as docs#Set.Definable.image_comp

[Aaron Anderson]

This API probably isn't ideal yet, but I think improving this is the first step, and then wrapping it in a tactic is the second step.

[Artie Khovanov]

@Zikang Yu you can use a custom Aesop ruleset as a quick way to get a tactic that works for what you want
Specifically, you register the lemmas that recursively break down the formula as @Aaron Anderson describes as Aesop apply rules.
This approach is already used to automate substructure membership goals - see the SetLike ruleset.

[Dexin Zhang]

It would be nice to have a custom definability tactic like measurability. FFL does the same thing

[Dexin Zhang]

And it's interesting how to automate definability of f x < f v. I guess we need a predicate saying "the graph of this function is definable" and tag lemmas with fun_prop

[Zikang Yu]

Artie Khovanov 說：

recursively break down the formula

So basically I write down a definition with only Exists, And, Or and Neg manually (or automatically maybe, by some simplifier), and use aesop with extra apply rules to deconstruct it into some "atomic" parts, then show these atomic parts are definable, which should be easily and directly. Is that an ideal process?

[Zikang Yu]

Dexin Zhang 說：

automate definability of f x < f v

Yeah that's quite tedious, too. Even considering definable sets in the set algebra, we still need to use preimage_comp and image_comp to handle quantifiers.

[Artie Khovanov]

@Zikang Yu yes, and hopefully you can discharge the atoms by some simp rules or something

[Zikang Yu]

@Artie Khovanov Then how do we deal with parameters?

Consider { x : M | x < a} : Set M where a : M is a parameter. Then we have {x : M | x < a} = {x : M | ∃ y, x < y ∧ y = a}. Now we can use Definable.inter, Definable.preimage_comp and Definable.image_comp to prove that the latter set is definable, where we prove { (x,y) | x < y } and { x | x = a } are definable by constructing the specific formulas.

But the problem arises since we are actually dealing with Fin 1 -> M. Now we have to prove {v | v 0 < a} = (fun g ↦ g ∘ fun (x : Fin 1) ↦ 0) '' S where S = { v : Fin 2 → M | v 0 < v 1 ∧ v 1 = a }. Although the proof is straightforward, one of two directions still can't be completed by simp, aesop or grind since it needs a witness and a manual application of List.ofFn_inj.mp .

Do we or should we have a lemma to automate this? If not, it would be easier to manually construct the constant term and the formula in this particular case.

[Artie Khovanov]

Yeah I don't know, sorry
Aesop is good when your goal is soluble by some sort of structural recursion scheme but you don't want to have to specify the scheme
If you have to supply witnesses, then yeah probably you should do some metaprogramming

[Dexin Zhang]

Zikang Yu said:

But the problem arises since we are actually dealing with Fin 1 -> M. Now we have to prove {v | v 0 < a} = (fun g ↦ g ∘ fun (x : Fin 1) ↦ 0) '' S where S = { v : Fin 2 → M | v 0 < v 1 ∧ v 1 = a }. Although the proof is straightforward, one of two directions still can't be completed by simp, aesop or grind since it needs a witness and a manual application of List.ofFn_inj.mp .

Do we or should we have a lemma to automate this? If not, it would be easier to manually construct the constant term and the formula in this particular case.

We definitely should have lemmas! For proving Definable {v : Fin 1 -> M | v 0 < a}, I could imagine the following steps:

1. Apply lemma Definable.lt so that goal becomes DefinableFun fun v : (Fin 1 -> M) => v 0 and DefinableFun fun v : (Fin 1 -> M) => a where DefinableFun : ((a -> M) -> M) -> Prop says the function has a definable graph
2. Apply lemma DefinableFun.proj and DefinableFun.const to resolve the two goals

Definable.lt should do the tedious things manually, like combine "< is definable" and Definable.image_comp

[Zikang Yu]

Now I've managed to create an auxiliary lemma as follows:

lemma definable_exists {n : ℕ} {p : (Fin (n + 1) → M) → Prop} {A : Set M} (p_def : A.Definable L {v | p v}) :
    A.Definable L { v : Fin n → M | ∃ x, p (Fin.snoc v x)} := by sorry

Surprisingly, aesop can prove equalities about such set quite well, like {v | v 0 < a} = {v | ∃ x, p (Fin.snoc v x)} where p : (Fin 2 → M) → Prop := fun v ↦ v 0 < v 1 ∧ v 1 = a.

My idea is that we can substitute variables with parameters (or more generally, functions that are definable but not in the language since you can regard parameters as constant functions). The strategy is to first permute the variable (or function) we want to replace to the last position using Definable.image_comp, and then apply definable_exists to introduce the existential quantifiers recursively. It still could be handy to prove the equality of the permuted sets, but maybe aesop performs well in these cases too, or we need an another auxiliary lemma.

The only thing left is to manually construct the innermost BoundedFormula (under the nested existential quantifiers)—or, in this context, the predicate p on n+m variables. I suspect we might need some metaprogramming to automatically expand expressions into this form.

[Dexin Zhang]

@Zikang Yu I got a proof of your lemma without constructing a formula explicitly. I guess this can still be golfed

lemma definable_exists {n : ℕ} {p : (Fin (n + 1) → M) → Prop} {A : Set M} (p_def : A.Definable L {v | p v}) :
    A.Definable L { v : Fin n → M | ∃ x, p (Fin.snoc v x)} := by
  convert p_def.image_comp (Fin.castSucc)
  ext v
  simp only [mem_setOf_eq, mem_image]
  constructor
  · intro ⟨x, hx⟩
    refine ⟨_, hx, ?_⟩
    simp
  · rintro ⟨x, h, rfl⟩
    exists x (Fin.last n)
    convert h
    ext i
    cases i using Fin.lastCases with simp

[Zikang Yu]

@Dexin Zhang Yeah I used image_comp (Fin.castSucc) to prove this lemma as well. Now I wonder if we can directly use Fin.insertNth instead of Fin.snoc to insert the variable of an arbitrary index and then use image_comp (i.succAbove) to eliminate it. Then we don't need to permute variables at all.

[Dexin Zhang]

@Zikang Yu Do you mean things like this?

lemma definable_exists {n : ℕ} {p : (Fin (n + 1) → M) → Prop} {A : Set M} (p_def : A.Definable L {v | p v}) {i : Fin (n + 1)} :
    A.Definable L { v : Fin n → M | ∃ x, p (Fin.insertNth i x v)} := by
  convert p_def.image_comp (Fin.succAbove i)
  ext v
  simp only [mem_setOf_eq, mem_image]
  constructor
  · intro ⟨x, hx⟩
    refine ⟨_, hx, ?_⟩
    simp
  · rintro ⟨x, h, rfl⟩
    exists x i
    convert h
    ext j
    cases j using Fin.succAboveCases i with simp

[Zikang Yu]

@Dexin Zhang Right. It would be more general.

[Zikang Yu]

It seems like the only thing left is to get the first-order definition of some predicate p : (Fin n → M) → Prop or function f : (Fin n → M) → M) and prove the definablity recursively. Clearly one can always manunally write down the formula. And I believe there's little chance for someone to directly give a hugely complex definition.

However, it still seems unlikely to automatically unfold some simple definition into a first-order formula. Consider the following "indicator" function:

noncomputable def indicator (p : M → Prop) (x : M) : M :=
  if p x then 1
  else 0

(Suppose that 0 and 1 are aliases of some given elements of M, and p is definable.)
Its graph is essentially defined by the following formula:

def i_formula (p : M → Prop) (x y : M) : Prop :=
  (p x ∧ y = 1) ∨ (¬ p x ∧ y = 0)

Of conrse we can easily prove the equivalence:

lemma indicator_is_defined_by_formula (p : M → Prop) (x y : M) :
  y = indicator p x ↔ i_formula p x y := by sorry

But we can't directly prove that A.Definable L { v | v 1 = indicator p (v 0) } ↔ A.Definable L { v | i_formula p (v 0) (v 1) } without this lemma.

Since working with functions is much more natural than raw formulas in contexts other than proving definability, we can't simply bypass this by only providing first-order definitions.

Such definitions could be common, and the difficulty of proving their equivalence to formulas can vary, so I think this is the best we can do for now.

[Dexin Zhang]

@Zikang Yu Yeah, these if-then-else are pretty common as definable functions.

[Dexin Zhang]

In fact, I would suggest not to operate on raw formulas at all. If we define DefinableFun as above, we can prove things like

theorem DefinableFun.ite {p : (α → M) → Prop} [DecidablePred p] {f g : (α → M) → M}
    (hp : A.Definable L (setOf p)) (hf : A.DefinableFun L f) (hg : A.DefinableFun L g) :
    A.DefinableFun L (fun x => if p x then f x else g x)

and make them aesop rules (or rules for the definability tactic, following FFL).

If we operate on raw formulas, we have to unfold these if-then-else and write the formulas, which is doable but quite tedious.

[Zikang Yu]

@Dexin Zhang Then how do we deal with match expressions? Should they be treated as nested if-then-else statements and unfolded layer by layer? I'm not sure if the equivalence between them could be automatically verified.

[Zikang Yu]

By the way, I tried to use the following definition to bypass the difficulties in proving definability of functions with only finitely many values:

def DefinableFunOfFiniteRange {A : Set M} {S : Type*} [Finite S] (f : (α → M) → S) : Prop :=
  ∀ s : S, A.Definable L (f⁻¹' {s})

It even eliminates the problem that the values are actually not in the structure, given we use integers frequently.

However, such a definition seems quite unrelated to the original definition DefinableFun since it actually is not a function to M at all. So that could be a convenient way, but not a proper way.

[Dexin Zhang]

Zikang Yu said:

Dexin Zhang Then how do we deal with match expressions? Should they be treated as nested if-then-else statements and unfolded layer by layer? I'm not sure if the equivalence between them could be automatically verified.

That sounds quite tricky! Do you have a case where match has to be used instead of if?

[Dexin Zhang]

match are auto-generated functions, so they can't be easily unfolded to if...

[Dexin Zhang]

Zikang Yu said:

By the way, I tried to use the following definition to bypass the difficulties in proving definability of functions with only finitely many values:

def DefinableFunOfFiniteRange {A : Set M} {S : Type*} [Finite S] (f : (α → M) → S) : Prop :=
  ∀ s : S, A.Definable L (f⁻¹' {s})

Is there any other assumption for DefinableFunOfFiniteRange? If I understand correctly, we can define f x := if p x then true else false then any set {x | p x} = f ⁻¹' {true} would be definable...

[Zikang Yu]

DefinableFunOfFiniteRange is actually a defintion but not a lemma. We may prove the equivalence of DefinableFunOfFiniteRange with DefinableFun if the codomain of f is M.

[Zikang Yu]

Dexin Zhang 說：

Do you have a case where match has to be used instead of if?

It seems not. I tried to use match compare to define a "comparator" function and dealing with match expression is actually an issue.

[Dexin Zhang]

Zikang Yu said:

DefinableFunOfFiniteRange is actually a defintion but not a lemma. We may prove the equivalence of DefinableFunOfFiniteRange with DefinableFun if the codomain of f is M.

Oh, that makes sense! Out of curiosity, what kinds of f do you find satisfying DefinableFunOfFiniteRange?

[Zikang Yu]

Dexin Zhang 說：

What kinds of f do you find satisfying DefinableFunOfFiniteRange?

For any definable predicate p, the indicator fun x => if p x then 1 else 0 : (α → M) → Fin 2 would be a DefinableFunOfFiniteRange.

And the following comparator should be as well, I guess.

noncomputable def comparator (a : M) : M → Fin 3 :=
  fun x =>
    match compare x a with
  | Ordering.lt => 0
  | Ordering.eq => 1
  | Ordering.gt => 2