ContMdiffMfderiv

Stream: mathlib4

[Patrick Massot]

I tried to work a bit on #5496. I fixed some issues with Lean 4 being less smart than Lean 3 to understand what univ means. But a big issue is a simp that does not work. The simp line in Lean 3 is this one. This is mathlib's manifold library so it actually uses more than 30 lemmas. The work I did was to expaned the Lean 3 version to

     simp only [ext_chart_at],
     simp only [local_homeomorph.extend],
     simp only [tangent_bundle_model_space_chart_at],
     simp only [model_with_corners_prod_to_local_equiv],
     simp only [model_with_corners_self_local_equiv],
     simp only [local_equiv.coe_trans ],
     simp only [local_equiv.prod_coe],
     simp only [model_with_corners.to_local_equiv_coe],
     simp only [local_equiv.refl_coe],
     simp only [id.def],
     simp only [equiv.to_local_equiv_apply],
     simp only [local_equiv.coe_trans_symm],
     simp only [equiv.to_local_equiv_symm_apply],
     simp only [local_equiv.prod_symm],
     simp only [local_equiv.refl_symm],
     simp only [local_equiv.prod_coe],
     simp only [model_with_corners.to_local_equiv_coe_symm],
     simp only [local_equiv.trans_target],
     simp only [local_equiv.prod_target],
     simp only [model_with_corners.target_eq],
     simp only [local_equiv.refl_target],
     simp only [equiv.to_local_equiv_target],
     simp only [preimage_univ],
     simp only [inter_univ],
     simp only [local_equiv.trans_source],
     simp only [equiv.to_local_equiv_source],
     simp only [local_equiv.prod_source],
     simp only [model_with_corners.source_eq],
     simp only [local_equiv.refl_source],
     simp only [univ_prod_univ],
     simp only [local_equiv.refl_coe],
     simp only [id.def],
     simp only [preimage_univ],
     simp only [inter_univ],
     simp only [preimage_univ],
     simp only [inter_univ],
     simp only [A],

and translate it to Lean 4 here. The next task is to find which simp call isn't doing its job. The first one that does nothing is simp only [LocalEquiv.prod_symm], but I think the issue happens before.

[Patrick Massot]

@Yury G. Kudryashov

[Patrick Massot]

I need to go to bed now, so I don't have time to compare the tactic states between Lean 3 and Lean 4 (which is hard because Lean 3 doesn't have goal diff and the dot notation do not behave the same in info view in both versions).

[Yury G. Kudryashov]

Simps about sigma will become better when I change the definition of total_space but I don't know what to do about simps for ModelProd

[Kevin Buzzard]

When I'm doing this kind of work I introduce unexpanders to make dot notation behave the same in Lean 3 and Lean 4. See for example #3592

[Floris van Doorn]

@Yury G. Kudryashov @Sebastien Gouezel do you think it's feasible to also make ModelProd a separate structure (just like Yuri is doing for Bundle.TotalSpace). That would disallow defeq "abuse" of these type synonyms, and therefore help simp.

[Floris van Doorn]

Together with Patrick I minimized the simp issue to the following MWE.
In Lean 4, simp does nothing in the following examples:

def ModelProd (α β : Type _) := α × β

theorem prod_lemma (x : α × β) : id x = x := rfl
theorem modelProd_lemma (x : ModelProd α β) : id x = x := rfl

example (x y : ModelProd α β)  : id x = y := by
  simp only [prod_lemma] -- doesn't rewrite anything

example (x y : α × β)  : id x = y := by
  simp only [modelProd_lemma] -- doesn't rewrite anything

In Lean 3, simp would rewrite in the following example:

def model_prod (α β : Type*) := α × β

variables {α β : Type*}
lemma prod_lemma (x : α × β) : id x = x := rfl

example {x y : model_prod α β} : id x = y :=
begin
  simp only [prod_lemma], -- rewrites with `prod_lemma`
end

[Sebastien Gouezel]

This looks very reasonable.

[Yury G. Kudryashov]

When do we want/need to abuse defeq for model_prod?

[Yury G. Kudryashov]

(and model_pi)

[Yury G. Kudryashov]

I guess, the only way to find out is to turn it into a separate structure. Then we'll need a version of docs#LocalEquiv.prod for ModelProd on one side.

[Yury G. Kudryashov]

(at least)

[Yury G. Kudryashov]

Should we do this directly in mathlib4, or do it in mathlib3, then forward-port?

[Floris van Doorn]

I'm not necessarily saying that we want to abuse the defeq, but our mathlib3 proofs are doing it

The fact that we need erw [A] instead of simp only [A] in one of the current proofs is partially caused by ModelProd. If you want to do this only with simp, you can replace this tactic by this:

    simp only [ModelProd, TangentBundle, TangentSpace, Bundle.TotalSpace]
    simp_rw [LocalEquiv.prod_symm, LocalEquiv.prod, LocalEquiv.refl_symm, LocalEquiv.refl_coe,
      Function.id_def]
    simp_rw [ModelWithCorners.symm] at A
    simp only [A]

The Equiv.sigmaEquivProd in the type of hypothesis Ais "really" totalSpaceEquivModelProd.

[Floris van Doorn]

For the sake of porting sphere eversion, I see no problem doing this directly in Lean 4.

[Yury G. Kudryashov]

Please wait till I forward-port !3#19221 first.

[Patrick Massot]

Sebastien Gouezel said:

This looks very reasonable.

Could you please clarify what looks very reasonable? Changing ModelProd or Lean failing to simp?

[Sebastien Gouezel]

Changing ModelProd. Sorry for the ambiguity.

[Yury G. Kudryashov]

Possibly this is a stupid idea but let me say it anyway: what do you think about bundling manifolds?

[Yury G. Kudryashov]

I mean using a bundled structure with a coercion to Type _ instead of a Type _ with a typeclass.

[Yury G. Kudryashov]

Ignore: the tangent bundle can't be (reudcibly) both coercion of a Manifold to Type _ and a Bundle.TotalSpace.

[Yury G. Kudryashov]

I rebased on top of #5720

[Yury G. Kudryashov]

Please don't push to this branch for a few hours. I'm working on it locally.

[Yury G. Kudryashov]

BTW, this is in fact a leaf file.

[Yury G. Kudryashov]

All reverse dependencies only needed a section I moved to MFDeriv while porting.

[Yury G. Kudryashov]

I'm going to try removing @[simp, mfld_simps] from docs#extChartAt for two reasons:

• IMHO, we should build API about new definitions, not simp them out;
• if we talk more about extChartAt, not chartAt, then we hide H from Lean, thus don't need to care about simp not dealing with ModelProd and ModelPi.

[Floris van Doorn]

This was also on my to do list, so I'm happy that you're doing this!

[Yury G. Kudryashov]

Another idea (probably, after-port): it looks like many lemmas about docs#ContMDiffWithinAt and docs#MDifferentiableWithinAt can be unified if we define

structure ComposableGermProp (X : Type _) [TopologicalSpace X] where
  prop : (X → X) → Set X → X → Prop
  prop_id : ∀ s x, prop id s x
  congr_fun {f g s x} : prop f s x → EqOn f g s → f x = g x → prop g s x
  congr_set {f s t x} : prop f s x → t ∈ 𝓝[s] x → prop f t x
  prop_comp {f g s t x} : prop f s (g x) → prop g t x → MapsTo g t s → prop (f ∘ g) t x

then add constructors from ComposableGermProp to StructureGroupoid and StructureGroupoid.LocalInvariantProp.

[Yury G. Kudryashov]

In the meantime, I fixed compile in #5496 without refactors. Who wants to review it?