ToExpr instance for FirstOrder.Language.Term

Stream: lean4

[Cody Roux]

I've been struggling to build an instance for ToTerm for FirstOrder.Language.Sentence in mathlib which needs a bunch of other instances, notably FirstOrder.Language.BoundedFormula and FirstOrder.Language.Term which I'm finding difficult to write.

The idea is to be able to reflect a Lean.Expr (when amenable) into a syntactic first order term, _including bound variables_ of course!

To do this, I'm writing a Lean.Expr -> FirstOrder.Language.BoundedFormula function, and then calling toExpr (and say, applying the "models" function to it).

The trouble is that, Term, for instance (no pun intended) has a constructor of type ... -> Fin n -> Termwhich is a bit awkward, (though there is an instance for such arrows) and the types are very dependent.

The mathlib ToExpr instance generator fails for all of these, perhaps unsurprisingly.

My questions are therefore:

• Is there an easier way to write these instances or just grit my teeth?
• Is this the right approach, or should I be doing this differently?

[Adam Topaz]

how do you intend to define toExpr for a term?

[Adam Topaz]

In other words, do you really want Term.var to give a bvar, or do you want to also quantify over some type, and have var be a term of said type?

[Adam Topaz]

Also, as far as I know, Mathlib's model theory library currently only supports single-sorted theories. If one were to do the hard work to develop such reflections, then I think we should do it in the correct level of generality, which should include the multi-sorted case as well.

[Adam Topaz]

Maybe I should also mention that I did something like this not for all of first-order logic, but just a small fragment as part of a project on Lawvere theories (which I gave a talk about a few weeks ago, and supposedly the recording of the talk will be posted soon).

[Yaël Dillies]

(it was a very interesting talk!)

[Adam Topaz]

Reading this again, it’s possible I misunderstood the original question. What is ToTerm?

[Cody Roux]

Sorry, was distracted yesterda.

ToTerm was a typo, I meant ToExpr. I think you got my question perfectly right. The advantage of the existing mono-sorted logic is that

1. It exists, and has some non-trivial lemmas
2. It's roughly up to mathlib standards
3. You can do plenty of things in mono-sorted logic, including (if you really want) encode multi-sorted theories.

I also need it right now, to do this non-standard arithmetic stuff.

[Cody Roux]

I want Term.var to give the Expr it should stand for! In this case, I guess a Expr.app (Expr.const ``Term.var []) (toExpr some_argument) or something along those lines.

[Adam Topaz]

Ah ok, so you don’t want to interpret first order logic in terms of lean’s type-theoretic logic. That’s much easier to accomplish :)

[Cody Roux]

Well, I want that too, but that's easy :)

Just use https://leanprover-community.github.io/mathlib4_docs/Mathlib/ModelTheory/Semantics.html#FirstOrder.Language.Sentence.Realize

[Adam Topaz]

Yeah ok, but that takes a structure in the sense of docs#FirstOrder.Language.Structure not in the sense of lean’s structures

[Cody Roux]

Ah I see, yes it'd be nice to generalize this, for sure. But for now, toExpr would be nice, so I can write a little tactic that reifies propositions into theories with "known" properties.

In my specific case, I have "spillover": the non-standard model of R satisfies exactly the same first-order sentences as R.

[Cody Roux]

https://github.com/codyroux/compact-php/blob/main/CompactPhp/NonstandardReal.lean#L330

[Timo Carlin-Burns]

@Cody Roux could you use a typeclass like this for your use case instead of a meta function from Expr? (I heard you explain your problem during office hours)

class ToRealSentence (P : Prop) where
  arithSentence : Sentence Arith
  isAboutReals : Sentence.Realize ℝ arithSentence ↔ P

instance : ToRealSentence False where
  arithSentence := .falsum
  isAboutReals := sorry

instance (x y : ℝ) : ToRealSentence (x = y) where
  arithSentence := .equal sorry sorry
  isAboutReals := sorry

-- and so on for every constructor of FirstOrder.Language.BoundedFormula

[Timo Carlin-Burns]

Hmm after playing with it for a bit I think I see the problem. This is as far as I got

class ToRealSentence (P : Prop) where
  arithSentence : Sentence Arith
  isAboutReals : Sentence.Realize ℝ arithSentence ↔ P

class ToRealTerm (x : ℝ) where
  arithTerm [IsEmpty α] : Term Arith α
  isAboutReals : Term.realize nofun (arithTerm (α := Empty)) = x

instance : ToRealSentence False where
  arithSentence := .falsum
  isAboutReals := sorry

instance (x y : ℝ) [ToRealTerm x] [ToRealTerm y]: ToRealSentence (x = y) where
  arithSentence := .equal (ToRealTerm.arithTerm x) (ToRealTerm.arithTerm y)
  isAboutReals := sorry

instance (P : ℝ → Prop) [f : ∀ x [ToRealTerm x], ToRealSentence (P x)] : ToRealSentence (∀ x, P x) where
  -- we get stuck because we need to recursively synthesize an instance about the quantified formula,
  -- but `P x` can't have a `ToRealSentence` instance for all `x : ℝ` because we don't necessarily know how to encode `x` as a term.
  -- if we try encoding `x` as `.var _`, we have another problem because we've been assuming all terms are ground.
  arithSentence := .all (@f sorry {arithTerm := .var sorry, isAboutReals := sorry}).arithSentence

[Timo Carlin-Burns]

Basically the problem with using typeclass synthesis for this is that typeclasses are always indexed by well-formed expressions, but we want to recurse on expressions with free variables.

[Timo Carlin-Burns]

If there was a function that lifted functions from terms to terms into terms with free variables, I think that would solve the problem, but I don't think it's possible to write such a function.

def liftFun : (Term Arith (Fin n) → Term Arith (Fin n)) → Term Arith (Fin (n + 1)) := sorry

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

liftFun could not work because not all Lean functions of that type are "definable" as FOL terms with a free variable. Logical frameworks can sometimes provide such a property (everything in a meta-level function space is definable), but general type theories don't.

[Cody Roux]

Right, I actually considered a less clever form of this idea but couldn't think of how to make it work. Let me think it through a bit.

What's certainly not true is that there is a mapping from the non-standards NS to R, even less one that preserves all the properties. I don't think there is one in the other direction either, but that's less obvious (I think NS can be countable though).

But I'm not sure that that's needed.