Using `Type 1` types inside the `MetaM` monad

Stream: mathlib4

[Sebastian Zimmer]

I'm trying to revive my very old PR adding a tactic which proves real inequalities by automatically deriving sufficiently good rational bounds. I don't like the original implementation strategy which was more of a proof of concept, I want to do something that looks more like this:

structure Approximator where
  State : Type
  improve : State → State
  bounds : State → ℚ × ℚ
  prove_lb : State → Expr -- : e ≥ ↑{mkRatExpr lb}
  prove_ub : State → Expr -- : e ≤ ↑{mkRatExpr ub}

structure ByApproxExt where
  build_approximator (e : Q(ℝ)) : MetaM Approximator

Basically I want to build a tree of Approximators which each keep state. This type of this state varies depending on the expression being approximated. Then I want to recursively improve the approximation at whichever node in the tree is most important to the overall error.

I think this should all work, the problem is that this leads to Approximator being Type 1, which I can't really use inside a MetaM so it's very unclear to me whether I can do any of this in a tactic.

Any advice?

[Kyle Miller]

If you can make an inductive type that comprises all possible State types, that's one way around this. (Presumably not every type is a possible state.) It's less flexible though, if you want to be able to support adding new approximators for new kinds of expressions from outside the core module.

[Sebastian Zimmer]

I'll try that. I'll make the expression-specific code be stateless and have a fixed state representing the approximations of the children.

[Kyle Miller]

Or, there's an interface like

structure Approximation where
  improve : Unit → Approximation
  bounds : ℚ × ℚ
  prove_lb : Expr
  prove_ub : Expr

where the state is encapsulated in the function improve, so it doesn't cause a universe bump.

You'll have to define partial approximations though I'm pretty sure.

The tradeoff is "make a universal state type, no need for partial" vs "can write flexible approximators more directly, but need partial, so no guarantee the meta code will terminate". It's meta code though, and partial doesn't cause any soundness issues for the generated proofs.

[Sebastian Zimmer]

Ok I'll try both approaches thanks

[Kyle Miller]

One more:

structure Approximation where
  improve : MetaM Approximation
  bounds : ℚ × ℚ
  prove_lb : MetaM Expr
  prove_ub : MetaM Expr

The MetaM is enough to defer computing the next approximation, plus it lets the system use MetaM, if you want. This also lets you defer computing the lb and ub proofs and use MetaM to construct them.

[Sebastian Zimmer]

That last approach looks great but when I try it doesn't compile.

(kernel) arg #1 of 'Mathlib.Tactic.ByApprox.Approximation.mk' contains a non valid occurrence of the datatypes being declaredLean 4

Do I need to tell it somehow not to pass the type to the kernel?

[Sebastian Zimmer]

I guess I can mark everything unsafe, but presumably that is undesirable?

[Eric Wieser]

I'll note that lean4#3011 suggests steps towards making using Type 1 legal inside MetaM, but I don't think there's much appetite for it

[Eric Wieser]

I'd love it if the less controversial lean4#3010 could be merged though

[Kyle Miller]

Oh, sorry Sebastian, with the last example I forgot that this kind of recursion isn't allowed.

It's possible to mark it unsafe. I think the main consequence is that everything that mentions Approximation then has to be marked unsafe too. None of the meta code would be kernel checked.

[Sebastian Zimmer]

i) Would marking this code unsafe be a usability issue for people using the tactic?
ii) Is there any easy way to mark an entire module unsafe?

[Kyle Miller]

i) No
ii) I'm not sure