Making fun_prop support ContMDiff

Stream: mathlib4

[Michael Rothgang]

Let me start a new thread about this: see e.g. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Painful.20.60ContMDiff.60.20proof and #mathlib4 > Differential geometry elaborators experiment for previous discussion.

Right now, fun_prop does not support ContMDiff, MDifferentiable and friends: this is because these definitions take a model with corners on the domain and codomain as arguments,
and fun_prop would have to find a model with corners for intermediate domains.

One complication is that there is not always a canonical model: there are two different models with corners on a product of normed spaces spaces (which are propeq, but not defeq).
Sébastien Gouezel tried to make the model with corners an outparam, solving this issue with forgetful inheritance: as he writes
https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Differential.20geometry.20elaborators.20experiment/near/527262536,
the result is arguably worse (and certainly not better) than the current design.

However, we have a third approach now: using a custom elaborator to infer the model with corners from the domain in the "almost all" cases which are not a product of normed spaces. The basic infrastructure (and support for inferring many models) has already been merged into master, #30463 and its dependencies complete the loop by adding support for every instance known to mathlib. In other words, with that in place, we have a way to ask "what's the model with corners on this space". It cannot be 100% reliable, but get pretty close.

Given this gadget, what would it take to make fun_prop support ContMDiff and friends?

[Tomas Skrivan]

I think it is almost supported :)

You need to modify synthesizeArgs . In particular this part

        -- try user provided discharger
        let ctx : Context ← read
        if (← isProp type) then
          if let some proof ← ctx.disch type then
            if (← isDefEq x proof) then
              continue
            else do
              trace[Meta.Tactic.fun_prop]
                "{← ppOrigin thmId}, failed to assign proof{indentExpr type}"
              return false
          else
            logError s!"Failed to prove necessary assumption `{← ppExpr type}` \
                        when applying theorem `{← ppOrigin' thmId}`."

For some reason I thought that custom discharger should be run only on Prop but you want to run it on ?I' : ModelWithCorners 𝕜 E' H' when applying ContMDiff.comp

I think it should really be just removing the if (← isProp type) then line and running fun_prop (disch:=find_model) where find_model is a tactic capable of discharging ModelWithCorners 𝕜 E' H' .

[Tomas Skrivan]

not a product of normed spaces

This is a bit worrisome, fun_prop rewrite function into compositions of functions over product spaces. For example, fun x => sin x + exp x is decomposed as (fun xy => xy.1 + xy.2) ∘ (fun x => (sin x, exp x)). Thus fun_prop creates lots of intermediate product spaces so I'm a bit worried if it will work in practice for ContMDiff.

However, the above decomposition is not done if there is a theorem for addition in compositional form like Continuous.add instead of continuous_add

[Michael Rothgang]

These are great news, I'm very excited to hear this! I've started work on this in branch#funpropM.

[Michael Rothgang]

This is a bit worrisome, fun_prop rewrite function into compositions of functions over product spaces.

Thanks for the warning, that is very good to know. I hope this won't be a big issue here --- taking products of two manifolds is fine, as are products of a manifold and a normed space. Only products of two normed spaces are an issue --- and if I understand correctly, a workaround for now could be to have find_model look in the local context first, and then provide the model I want by hand, as in

have : ModelWithCorners 𝕜 (E × F) (E × F) :=  𝓘(𝕜, E × F)
fun_prop

right?

[Tomas Skrivan]

Yeah, that way you can force it to use a particular model you want.

Btw the link to the branch is broken. Unfortunately, I don't really have the time to help out with it but I'm happy to answer any questions.

[Michael Rothgang]

Thanks! In fact, I already have a first question: when my find_model tactic is run on goals of the form I? : ModelWithCorners k E H, can I assume the ModelWithCorners k E H is type-correct? (For example, that it's not ModelWithCorners Bool Bool Bool, or that E is a k-normed space and H a topological space?) This would avoid the need for some checks in the tactic.

[Michael Rothgang]

The branch is now a WIP PR: #31580

[Tomas Skrivan]

When trying to apply theorem fun_prop does

let (xs,_,statement) <- forallMetaTelescope theoremType

unifies statemetn with the current goal and then runs synthesizeArgs on each xs[i] in order.

It does not error out if it fails to synthesize an argument, for example when having {n : Nat} (hf : ContDiff 𝕜 n f) the n often fails to be synthesized but then it is inferred from hf. Therefore, I think you can safely assume that ModelWithCorners k E H is type correct but I think you might be able to get ModelWithCorners Bool Bool Bool however in that case all the type class instances will be metavariables.

I think you can do the check like this

def syntesizeModelWithCorners (goal : Expr) : MetaM Bool := do
  let X ← inferType goal
  if X.isAppOfArity ``ModelWithCorners 7 then
    let X ← instantiateMVars X
    -- check if all the instances [NontriviallyNormedField 𝕜] [NormedAddCommGroup E]
    --                            [NormedSpace 𝕜 E] [TopologicalSpace H]
    -- has been syntasized
    if ¬X.hasMVar then
      let model := sorry
      goal.mvarId!.assign model
      return true

  return false