phantom declaration

Stream: mathlib4

[Patrick Massot]

The following code contains a phantom theorem. It looks declared (and sorried) but then the #check commands doesn't know about it. Replacing the sorry by the commented "proof" results in this tactic is never executed [linter.unreachableTactic] over the whole proof.

import Mathlib

noncomputable section

open Set Equiv Bundle ContinuousLinearMap

open scoped Manifold Bundle Topology

universe u v

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type*)
  [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {F : Type*}
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type*} [TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type*} [TopologicalSpace N] [ChartedSpace G N]
  [SmoothManifoldWithCorners J N] (V : Type*) [NormedAddCommGroup V] [NormedSpace 𝕜 V]

local notation "FJ¹MV" =>
  Bundle.ContinuousLinearMap (RingHom.id 𝕜) (TangentSpace I : M → Type*) (Bundle.Trivial M V)

local notation "J¹MV" => TotalSpace (E →L[𝕜] V) FJ¹MV

section Smoothness

variable {I M V} {f : N → J¹MV}

theorem smoothAt_one_jet_eucl_bundle' {x₀ : N} :
    SmoothAt J (I.prod 𝓘(𝕜, E →L[𝕜] V)) f x₀ ↔ SmoothAt J I (fun x => (f x).1) x₀ ∧
    SmoothAt J 𝓘(𝕜, E →L[𝕜] V)
      (fun x => show E →L[𝕜] V from (f x).2 ∘L (trivializationAt E (TangentSpace I : M → Type u) (f x₀).1).symmL 𝕜 (f x).1) x₀ := sorry
      /- by
  simp_rw [smoothAt_hom_bundle, in_coordinates, trivial.trivialization_at,
    trivial.trivialization_continuous_linear_map_at]
  dsimp only [Bundle.Trivial]
  simp_rw [ContinuousLinearMap.id_comp] -/

#check smoothAt_one_jet_eucl_bundle'

Any idea?

[Patrick Massot]

@Heather Macbeth, this is mathported from code you wrote.

[Adam Topaz]

Just for the sake of minimization, the first prop in the conjunction can be removed while preserving the issue (with the sorry):

theorem foo {x₀ : N} :
    (SmoothAt J 𝓘(𝕜, E →L[𝕜] V)
      (fun x => show E →L[𝕜] V from (f x).2 ∘L
        (trivializationAt E (TangentSpace I : M → Type u) (f x₀).1).symmL 𝕜 (f x).1) x₀) := sorry

#check foo

[Mario Carneiro]

This sounds related to an old lean4 issue of mine (lean4#2226), where an error would occur during elaboration without reporting any actual info diagnostics

[Mario Carneiro]

Yes, it's an instance of the same issue. There is an issue elaborating the variables line and it produces a synthetic sorry without reporting an error about it, which breaks an invariant of the system (synthetic sorries should only appear if errors have been reported), and if you do it right you can get no further error to be reported (because things see the synthetic sorry and think "I guess I don't need to add insult to injury here, we are already in an error state so no need to report more"

[Patrick Massot]

And lean4#2226 refers to lean4#2257 which seems very relevant here.

[Patrick Massot]

Getting rid of the local notation by copy-paste reveals an error.

[Mario Carneiro]

def foo := f will produce a definition, but notice that it has sorry in it caused by typechecking failures and there are no app mismatch errors or the like

[Patrick Massot]

New mystery is then

import Mathlib

noncomputable section

open Set Equiv Bundle ContinuousLinearMap

open scoped Manifold Bundle Topology

universe u v

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type*)
  [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {F : Type*}
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type*} [TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type*} [TopologicalSpace N] [ChartedSpace G N]
  [SmoothManifoldWithCorners J N] (V : Type*) [NormedAddCommGroup V] [NormedSpace 𝕜 V]

variable {I M V} {f : N → TotalSpace (E →L[𝕜] V) (Bundle.ContinuousLinearMap (RingHom.id 𝕜) (TangentSpace I : M → Type u) (Bundle.Trivial M V))}

[Patrick Massot]

which does features an error message, so this is a great progress.

[Mario Carneiro]

you have to separate the two binder groups there or else {I M V} won't be interpreted as a binder update

[Mario Carneiro]

and

variable {I M V}
variable {f : N → TotalSpace (E →L[𝕜] V) (Bundle.ContinuousLinearMap (RingHom.id 𝕜) (TangentSpace I : M → Type*) (Bundle.Trivial M V))}

has yet another error message

[Patrick Massot]

I know how to fix that one.

[Patrick Massot]

The following works now:

import Mathlib

noncomputable section

open Set Equiv Bundle ContinuousLinearMap

open scoped Manifold Bundle Topology

universe u v

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type*)
  [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {F : Type*}
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type*} [TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type*} [TopologicalSpace N] [ChartedSpace G N]
  [SmoothManifoldWithCorners J N] (V : Type*) [NormedAddCommGroup V] [NormedSpace 𝕜 V]

variable {I M V}

variable {f : N → TotalSpace (E →L[𝕜] V) (Bundle.ContinuousLinearMap (RingHom.id 𝕜) (TangentSpace I : M → Type u) (Bundle.Trivial M V))}

theorem smoothAt_one_jet_eucl_bundle' {x₀ : N} :
    SmoothAt J (I.prod 𝓘(𝕜, E →L[𝕜] V)) f x₀ ↔ SmoothAt J I (fun x => (f x).1) x₀ ∧
    SmoothAt J 𝓘(𝕜, E →L[𝕜] V)
      (fun x => show E →L[𝕜] V from (f x).2 ∘L (trivializationAt E (TangentSpace I : M → Type u) (f x₀).1).symmL 𝕜 (f x).1) x₀ := sorry
      /- by
  simp_rw [smoothAt_hom_bundle, in_coordinates, trivial.trivialization_at,
    trivial.trivialization_continuous_linear_map_at]
  dsimp only [Bundle.Trivial]
  simp_rw [ContinuousLinearMap.id_comp] -/

#check smoothAt_one_jet_eucl_bundle'

[Patrick Massot]

So I'm unstuck now.

[Patrick Massot]

Thanks a lot Mario! You can continue that impressive series by solving the minimization quest at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Another.20simp.20mystery/near/398356577

[Mario Carneiro]

what did you even change? I'm eyeball diffing and I don't see anything

[Mario Carneiro]

oh, Type* -> Type u

[Mario Carneiro]

what a terrible error message

[Patrick Massot]

Do you think there is anyway I could use a notation here? Or should I write TotalSpace (E →L[𝕜] V) (Bundle.ContinuousLinearMap (RingHom.id 𝕜) (TangentSpace I : M → Type u) (Bundle.Trivial M V)) everywhere in this file?

[Mario Carneiro]

there's nothing wrong with using a notation, it was just hiding an error

[Patrick Massot]

Can you fix the above snippet while keeping a notation?

[Patrick Massot]

I think I already met that issue that local notations are no longer really allowed in Lean 4.

[Patrick Massot]

I found it https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Notation.20introduces.20sorry/near/390552023

[Mario Carneiro]

set_option hygiene false
local notation "FJ¹MV" =>
  Bundle.ContinuousLinearMap (RingHom.id 𝕜) (TangentSpace I : M → Type u) (Bundle.Trivial M V)
set_option hygiene true

local notation "J¹MV" => TotalSpace (E →L[𝕜] V) FJ¹MV

section Smoothness

variable {I M V}
variable {f : N → J¹MV}

[Patrick Massot]

Thanks, but this introduces a sorry in the statement.