Chain Rule Times Out (WHNF max exceeded)

Stream: new members

[Dominic Steinitz]

Does anyone know why this times out?

import Mathlib

open Manifold
open SmoothManifoldWithCorners

example
  (m : ℕ) {M : Type*}
  [TopologicalSpace M]
  [ChartedSpace (EuclideanSpace ℝ (Fin m)) M]
  [SmoothManifoldWithCorners (𝓡 m) M]
  (f : M → (EuclideanSpace ℝ (Fin 1)))
  (hs : ContMDiff (𝓡 m) (𝓡 1) ⊤ f)
  (φ_α : PartialHomeomorph M (EuclideanSpace ℝ (Fin m)))
  (hΦ_Α : φ_α ∈ maximalAtlas (𝓡 m) M)
  (φ_β : PartialHomeomorph M (EuclideanSpace ℝ (Fin m)))
  (hΦ_Β : φ_β ∈ maximalAtlas (𝓡 m) M)

  (x : M) (hx : x ∈  φ_α.source ∩ φ_β.source) : true := by

    let αβ : EuclideanSpace ℝ (Fin m) → (EuclideanSpace ℝ (Fin m)) := (φ_α.symm.trans φ_β)

    let Dαβ : M -> (EuclideanSpace ℝ (Fin m) →L[ℝ] EuclideanSpace ℝ (Fin m)) :=
      λ x => mfderiv (𝓡 m) (𝓡 m) αβ (φ_α.toFun x)

    have hst : HasMFDerivAt (𝓡 m) (𝓡 m) (φ_α.symm.trans φ_β) (φ_α x) (Dαβ x) := sorry

    let h : EuclideanSpace ℝ (Fin m) → (EuclideanSpace ℝ (Fin 1)) := f ∘ φ_β.invFun

    let Dh : M -> (EuclideanSpace ℝ (Fin m) →L[ℝ] EuclideanSpace ℝ (Fin 1)) :=
      λ x => mfderiv (𝓡 m) (𝓡 1) h (φ_β.toFun x)

    have hsh : HasMFDerivAt (𝓡 m) (𝓡 1) h ((φ_α.symm.trans φ_β) (φ_α x)) (Dh x) := sorry

    -- The chain rule but no proof
    have baa : HasMFDerivAt (𝓡 m) (𝓡 1) (h ∘ ((φ_α.symm.trans φ_β))) (φ_α x) ((Dh x).comp (Dαβ x)) := sorry

-- A proof but no theorem! Here we obviously get a type mismatch:
/-
type mismatch
  HasMFDerivAt.comp (↑φ_α x) hsh hst
has type
  HasMFDerivAt 𝓘(ℝ, EuclideanSpace ℝ (Fin m)) 𝓘(ℝ, EuclideanSpace ℝ (Fin 1)) (h ∘ ↑(φ_α.symm ≫ₕ φ_β)) (↑φ_α x)
    ((Dh x).comp (Dαβ x)) : Prop
but is expected to have type
  true = true : Prop
-/
    have bab : true := HasMFDerivAt.comp (φ_α x) hsh hst

-- So let's use lean's suggestion
    have bac : HasMFDerivAt 𝓘(ℝ, EuclideanSpace ℝ (Fin m)) 𝓘(ℝ, EuclideanSpace ℝ (Fin 1)) (h ∘ ↑(φ_α.symm ≫ₕ φ_β)) (φ_α x) ((Dh x).comp (Dαβ x)) :=
      HasMFDerivAt.comp (φ_α x) hsh hst

-- But this gives the following
/-
(deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached
Use `set_option maxHeartbeats <num>` to set the limit.
Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
    sorry

[Dominic Steinitz]

Here's a slightly simpler example

import Mathlib

open Manifold
open SmoothManifoldWithCorners

example
  (m : ℕ) {M : Type*}
  [TopologicalSpace M]
  [ChartedSpace (EuclideanSpace ℝ (Fin m)) M]
  [SmoothManifoldWithCorners (𝓡 m) M]
  (φ_α : PartialHomeomorph M (EuclideanSpace ℝ (Fin m)))
  (hΦ_Α : φ_α ∈ maximalAtlas (𝓡 m) M)
  (φ_β : PartialHomeomorph M (EuclideanSpace ℝ (Fin m)))
  (hΦ_Β : φ_β ∈ maximalAtlas (𝓡 m) M)
  (φ_γ : PartialHomeomorph M (EuclideanSpace ℝ (Fin m)))
  (hΦ_Γ : φ_γ ∈ maximalAtlas (𝓡 m) M)

  (x : M) (hx : x ∈  φ_α.source ∩ φ_β.source) : true := by

    let αβ : EuclideanSpace ℝ (Fin m) → (EuclideanSpace ℝ (Fin m)) := φ_α.symm.trans φ_β

    let Dαβ : M -> (EuclideanSpace ℝ (Fin m) →L[ℝ] EuclideanSpace ℝ (Fin m)) :=
      λ x => mfderiv (𝓡 m) (𝓡 m) αβ (φ_α.toFun x)

    let βγ : EuclideanSpace ℝ (Fin m) → (EuclideanSpace ℝ (Fin m)) := φ_β.symm.trans φ_γ

    let Dβγ : M -> (EuclideanSpace ℝ (Fin m) →L[ℝ] EuclideanSpace ℝ (Fin m)) :=
      λ x => mfderiv (𝓡 m) (𝓡 m) βγ (φ_β.toFun x)

    have hst : HasMFDerivAt (𝓡 m) (𝓡 m) (φ_α.symm.trans φ_β) (φ_α x) (Dαβ x) := sorry
    have hsu : HasMFDerivAt (𝓡 m) (𝓡 m) (φ_β.symm.trans φ_γ) (φ_β x) (Dβγ x) := sorry

    have bac : HasMFDerivAt (𝓡 m) (𝓡 m) (↑(φ_β.symm ≫ₕ φ_γ) ∘ ↑(φ_α.symm ≫ₕ φ_β)) (φ_α x) ((Dβγ x).comp (Dαβ x)) :=
      HasMFDerivAt.comp (φ_α x) hsu hst

    sorry

[Michael Rothgang]

Your second example still has a type mismatch. Let's use by apply instead of just given the term --- then we get a better error message.

import Mathlib

open Manifold
open SmoothManifoldWithCorners

example
  (m : ℕ) {M : Type*}
  [TopologicalSpace M]
  [ChartedSpace (EuclideanSpace ℝ (Fin m)) M]
  [SmoothManifoldWithCorners (𝓡 m) M]
  (φ_α : PartialHomeomorph M (EuclideanSpace ℝ (Fin m)))
  (hΦ_Α : φ_α ∈ maximalAtlas (𝓡 m) M)
  (φ_β : PartialHomeomorph M (EuclideanSpace ℝ (Fin m)))
  (hΦ_Β : φ_β ∈ maximalAtlas (𝓡 m) M)
  (φ_γ : PartialHomeomorph M (EuclideanSpace ℝ (Fin m)))
  (hΦ_Γ : φ_γ ∈ maximalAtlas (𝓡 m) M)

  (x : M) (hx : x ∈  φ_α.source ∩ φ_β.source) : true := by

    let αβ : EuclideanSpace ℝ (Fin m) → (EuclideanSpace ℝ (Fin m)) := φ_α.symm.trans φ_β

    let Dαβ : M -> (EuclideanSpace ℝ (Fin m) →L[ℝ] EuclideanSpace ℝ (Fin m)) :=
      λ x => mfderiv (𝓡 m) (𝓡 m) αβ (φ_α.toFun x)

    let βγ : EuclideanSpace ℝ (Fin m) → (EuclideanSpace ℝ (Fin m)) := φ_β.symm.trans φ_γ

    let Dβγ : M -> (EuclideanSpace ℝ (Fin m) →L[ℝ] EuclideanSpace ℝ (Fin m)) :=
      λ x => mfderiv (𝓡 m) (𝓡 m) βγ (φ_β.toFun x)

    have hst : HasMFDerivAt (𝓡 m) (𝓡 m) (φ_α.symm.trans φ_β) (φ_α x) (Dαβ x) := sorry
    have hsu : HasMFDerivAt (𝓡 m) (𝓡 m) (φ_β.symm.trans φ_γ) (φ_β x) (Dβγ x) := sorry

    have bac : HasMFDerivAt (𝓡 m) (𝓡 m) ((φ_β.symm ≫ₕ φ_γ) ∘ (φ_α.symm ≫ₕ φ_β)) (φ_α x) ((Dβγ x).comp (Dαβ x)) := by
      apply HasMFDerivAt.comp (φ_α x) hsu hst

    sorry

[Michael Rothgang]

You'll see that hsu is underlined, as the types don't match up:

application type mismatch
  HasMFDerivAt.comp (↑φ_α x) hsu
argument
  hsu
has type
  HasMFDerivAt (𝓡 m) (𝓡 m) (↑(φ_β.symm ≫ₕ φ_γ)) (↑φ_β x) (Dβγ x) : Prop
but is expected to have type
  HasMFDerivAt (𝓡 m) (𝓡 m) (↑(φ_β.symm ≫ₕ φ_γ)) (↑(φ_α.symm ≫ₕ φ_β) (↑φ_α x)) (Dβγ x) : Prop

[Michael Rothgang]

The reason is an identification that's usually "invisible", but Lean complains about it being implicit: comparing (↑(φ_α.symm ≫ₕ φ_β) (↑φ_α x) with (↑φ_β x). These are, of course, mathematically the same.

[Michael Rothgang]

Here's a fixed proof:

import Mathlib

open Manifold
open SmoothManifoldWithCorners

example
  (m : ℕ) {M : Type*}
  [TopologicalSpace M]
  [ChartedSpace (EuclideanSpace ℝ (Fin m)) M]
  [SmoothManifoldWithCorners (𝓡 m) M]
  (φ_α : PartialHomeomorph M (EuclideanSpace ℝ (Fin m)))
  (hΦ_Α : φ_α ∈ maximalAtlas (𝓡 m) M)
  (φ_β : PartialHomeomorph M (EuclideanSpace ℝ (Fin m)))
  (hΦ_Β : φ_β ∈ maximalAtlas (𝓡 m) M)
  (φ_γ : PartialHomeomorph M (EuclideanSpace ℝ (Fin m)))
  (hΦ_Γ : φ_γ ∈ maximalAtlas (𝓡 m) M)

  (x : M) (hx : x ∈  φ_α.source ∩ φ_β.source) : true := by

    let αβ : EuclideanSpace ℝ (Fin m) → (EuclideanSpace ℝ (Fin m)) := φ_α.symm.trans φ_β

    let Dαβ : M -> (EuclideanSpace ℝ (Fin m) →L[ℝ] EuclideanSpace ℝ (Fin m)) :=
      λ x => mfderiv (𝓡 m) (𝓡 m) αβ (φ_α.toFun x)

    let βγ : EuclideanSpace ℝ (Fin m) → (EuclideanSpace ℝ (Fin m)) := φ_β.symm.trans φ_γ

    let Dβγ : M -> (EuclideanSpace ℝ (Fin m) →L[ℝ] EuclideanSpace ℝ (Fin m)) :=
      λ x => mfderiv (𝓡 m) (𝓡 m) βγ (φ_β.toFun x)

    have hst : HasMFDerivAt (𝓡 m) (𝓡 m) (φ_α.symm.trans φ_β) (φ_α x) (Dαβ x) := sorry
    have hsu : HasMFDerivAt (𝓡 m) (𝓡 m) (φ_β.symm.trans φ_γ) (φ_β x) (Dβγ x) := sorry

    have bac : HasMFDerivAt (𝓡 m) (𝓡 m) ((φ_β.symm ≫ₕ φ_γ) ∘ (φ_α.symm ≫ₕ φ_β)) (φ_α x) ((Dβγ x).comp (Dαβ x)) := by
      have : (φ_α.symm ≫ₕ φ_β) (φ_α x) = (φ_β x) := by
        rw [PartialHomeomorph.trans_apply]
        congr
        exact PartialHomeomorph.left_inv φ_α (Set.mem_of_mem_inter_left hx)
      rw [← this] at hsu
      apply HasMFDerivAt.comp (φ_α x) hsu hst

    sorry

[Michael Rothgang]

Though, I may take a step back and ask why you're proving this. Anything just for your personal learning is totally fine, of course. But if you want to fight to the manifold library, there are many little things still waiting for somebody to do them. :-)

[Dominic Steinitz]

Partly for personal learning and partly to define the cotangent bundle without first defining the tangent bundle (which I will define to be the dual of the cotangent bundle). For what I really want to do, I want differential forms and I got the impression that these were still being thought about.

Thanks very much for your help. A type error would have been great but failing to unify was not so helpful. I am used to terms being proofs. It would never have occurred to me use a tactic(?) like apply.

[Michael Rothgang]

Yes, apply is a tactic (like refine, exact or intro). Have you seen a list of common tactics already? In my experience, writing out proof terms by hand gets tedious pretty quickly.

[Michael Rothgang]

Tactics do proof terms - but using a tactic can hide some of the (imho, usually boring) details from you, so you can focus on higher-level things.

[Michael Rothgang]

Right now, mathlib

• knows about the tangent bundle docs#TangentBundle
• knows about the cotangent bundle implicitly: the dual bundle is a special case of the Hom bundle (docs#SmoothVectorBundle.continuousLinearMap)

[Michael Rothgang]

Perhaps, adding a definition (maybe an abbrev) for the dual bundle could be useful. (I'd need to think: is this worth mentioning explicitly, and separately from the more general construction? Perhaps it is.) Feel free to propose a PR and one can discuss.

[Michael Rothgang]

Differential forms: these are indeed very sorely missing, but there is also work on adding them. See e.g. this old zulip thread, and these recent news: a student in Utrecht is working on this here.

[Dominic Steinitz]

I hoping that Lie-algebra valued forms are supported so we can define connection and curvature forms. This is an area that could really do with some formalisation as many presentations of the subject conflate the abstract with the representation.

[Dominic Steinitz]

Michael Rothgang said:

Perhaps, adding a definition (maybe an abbrev) for the dual bundle could be useful. (I'd need to think: is this worth mentioning explicitly, and separately from the more general construction? Perhaps it is.) Feel free to propose a PR and one can discuss.

I am a long way from raising a PR and I ought to be able to use 1-forms as the dual to the tangent space but maybe an abbreviation would be nice when introducing the subject.