changes to apply magic in 4.8.0

Stream: lean4

[Patrick Massot]

I just noticed that Lean 4.8.0-rc1 no longer does a rather disturbing magic trick that Lean used to do (even in the Lean 3 days). My example is not minimal at all since it happens in the sphere eversion project. I can work on a minimization if Lean devs want to see it. But I expect that the magic trick was never intended to work and so this minimization work wouldn’t be useful. I’m writing this message to test this assumption, and also potentially help people who could stumble on this without having ever noticed this kind of (evil?) miracle.

In this file, one can read

theorem contDiff_parametric_symm_of_deriv_pos {f : E → ℝ → ℝ} (hf : ContDiff ℝ ⊤ ↿f)
    (hderiv : ∀ x t, 0 < partialDerivSnd f x t) (hsurj : ∀ x, Surjective <| f x) :
    ContDiff ℝ ⊤ fun p : E × ℝ ↦
      (StrictMono.orderIsoOfSurjective (f p.1) (strictMono_of_deriv_pos <| hderiv p.1)
            (hsurj p.1)).symm p.2

where the only relevant thing is the presence of three explicit arguments, the last one being some surjectivity assumption.

The lemma is used in a later file with the following surprising proof:

theorem reparametrize_smooth : 𝒞 ∞ <| uncurry fun (x : E) (t : ℝ) ↦ γ.reparametrize x t := by
  let f : E → ℝ → ℝ := fun x t ↦ ∫ s in (0)..t, γ.centeringDensity x s
  change 𝒞 ⊤ fun p : E × ℝ ↦ (StrictMono.orderIsoOfSurjective (f p.1) _ _).symm p.2
  apply contDiff_parametric_symm_of_deriv_pos
  · exact contDiff_parametric_primitive_of_contDiff'' γ.centeringDensity_smooth 0
  · exact fun x ↦ deriv_integral_centeringDensity_pos γ x

Notice how apply contDiff_parametric_symm_of_deriv_pos generates only two goals. The surjectivity assumption simply does not appear at all. Needless to say, this surjectivity is not rfl or “filled in by unification” or anything like this. So where Lean got it? One can look at the term generated by apply and see: refine contDiff_parametric_symm_of_deriv_pos ?hf ?hderiv (reparametrize.proof_2 γ). So Lean took the initiative to find some auto-generated lemma reparametrize.proof_2 that was floating around. It came from a couple of lines above:

def reparametrize : E → EquivariantEquiv := fun x ↦
  ({ toFun := fun t ↦ ∫ s in (0)..t, γ.centeringDensity x s
     invFun :=
       (StrictMono.orderIsoOfSurjective _ (γ.strictMono_integral_centeringDensity x)
           (γ.surjective_integral_centeringDensity x)).symm
     left_inv := StrictMono.orderIsoOfSurjective_symm_apply_self _ _ _
     right_inv := fun t ↦ StrictMono.orderIsoOfSurjective_self_symm_apply _ (γ.strictMono_integral_centeringDensity x) _ t
     map_zero' := integral_same
     eqv' := γ.integral_add_one_centeringDensity x } : EquivariantEquiv).symm

Note this surjectivity is not even a field of this structure, it appears as part of the proof of one of the fields. Specifically, it is the γ.surjective_integral_centeringDensity that appears in invFun.

Again this whole story worked in Lean 3 and up to Lean 4.7.0, and it no longer works in 4.8.0-rc1 which, very reasonably, asks for a surjectivity proof after the apply line.

The question is: was this ever intended to work? Should we worry that it no longer works? Would a minimization be helpful?

[Oliver Nash]

Wow, I never knew this (and I might even be the author of that apply that surprisingly emits only two subgoals instead of three).

I think I lean in favour of the new world in which this does not work: surely proofs should not be this non-local. I'd be interested to hear from Lean devs if they have remarks.

[Eric Wieser]

I assume the change here is that unification no longer recurses into proofs? Hopefully it still visits top-level proofs.

[Kyle Miller]

Seeing a proof from another proof isn't too surprising, and it doesn't immediately imply a non-local effect. There's a step where proofs are abstracted out of definitions after the definition is constructed, and there's a cache for these abstracted proofs. It's possible that somehow pre-4.8.0 apply was able to come up with a surjectivity proof by some means and then it had the same type as something in the cache, and that cached proof was used.

What does #print reparametrize.proof_2 show?

[Kyle Miller]

I wonder what the change was. This also seems like the thing that could be caused by a cache that wasn't supposed to survive across declarations....

[Patrick Massot]

In 4.7.0 it shows the proof I mentioned:

theorem SmoothSurroundingFamily.reparametrize.proof_2.{u_1, u_2} : ∀ {E : Type u_1} {F : Type u_2}
  [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] [inst_2 : FiniteDimensional ℝ F]
  [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace ℝ E] [inst_5 : FiniteDimensional ℝ E] {g : E → F}
  (γ : SmoothSurroundingFamily g) [inst_6 : DecidablePred fun x ↦ x ∈ affineBases ι ℝ F] (x : E),
  Surjective fun t ↦ ∫ (s : ℝ) in 0 ..t, centeringDensity γ x s :=
fun {E} {F} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] {g} γ [DecidablePred fun x ↦ x ∈ affineBases ι ℝ F] x ↦
  surjective_integral_centeringDensity γ x

[Patrick Massot]

and the same in 4.8.0

[Patrick Massot]

No, I’m wrong. In 4.8.0 it is

theorem SmoothSurroundingFamily.reparametrize.proof_2.{u_1, u_2} : ∀ {E : Type u_2} {F : Type u_1}
  [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] [inst_2 : FiniteDimensional ℝ F]
  [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace ℝ E] [inst_5 : FiniteDimensional ℝ E] {g : E → F}
  (γ : SmoothSurroundingFamily g) [inst_6 : DecidablePred fun x ↦ x ∈ affineBases ι ℝ F] (x : E) (t : ℝ),
  ∫ (s : ℝ) in 0 ..(StrictMono.orderIsoOfSurjective (fun t ↦ ∫ (s : ℝ) in 0 ..t, γ.centeringDensity x s) ⋯ ⋯).symm t,
      γ.centeringDensity x s =
    t :=
fun {E} {F} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] {g} γ [DecidablePred fun x ↦ x ∈ affineBases ι ℝ F] x t ↦
  StrictMono.orderIsoOfSurjective_self_symm_apply (fun t ↦ ∫ (s : ℝ) in 0 ..t, γ.centeringDensity x s)
    (strictMono_integral_centeringDensity γ x) (surjective_integral_centeringDensity γ x) t

[Patrick Massot]

So in the new version it is the full field proof, not the subproof.

[Kyle Miller]

This guess could be totally off-base [edit: yes, this guess was totally off-base] (and I can't point to where in isDefEq this could have happened), but it seems plausible that what happened before was that reparameterize was being unfolded in reparameterize_smooth during a defeq check at apply, which put one of the proofs contained inside it into some cache, and then that was used to fill in a proof metavariable. Maybe with changes to isDefEq, it's not being unfolded anymore, so it doesn't get put into that cache?

In any case, I think the old behavior was total magic and unintended :magic:

[Patrick Massot]

It was certainly unintended by me (and Oliver).

[Patrick Massot]

I’ll let you decide whether this is worth bringing to Leo’s attention.

[Kyle Miller]

The difference turns out to be in the change.

Here are the goals after change (I did set_option pp.proofs true for this):

-- On 4.7.0

⊢ 𝒞 ⊤ fun p ↦
  (OrderIso.symm (StrictMono.orderIsoOfSurjective (f p.1) (reparametrize.proof_1 γ p.1) (reparametrize.proof_2 γ p.1)))
    p.2

-- On 4.8.0-rc1

⊢ 𝒞 ⊤ fun p ↦
  (StrictMono.orderIsoOfSurjective (f p.1) (strictMono_integral_centeringDensity γ p.1)
        (surjective_integral_centeringDensity γ p.1)).symm
    p.2

Notice that reparametrize.proof_2 is in the first one. If you look at the full conclusion for contDiff_parametric_symm_of_deriv_pos

𝒞 ⊤ fun p ↦ (StrictMono.orderIsoOfSurjective (f p.1) (strictMono_of_deriv_pos (hderiv p.1)) (hsurj p.1)).symm p.2

you can see that hsurj p.1 lines up perfectly to unify with reparametrize.proof_2 γ p.1, so it's able to pick up the proof.

In fact, if you change the proof in 4.8.0-rc1 to include a surjectivity proof in the second underscore for the change

theorem reparametrize_smooth : 𝒞 ∞ <| uncurry fun (x : E) (t : ℝ) ↦ γ.reparametrize x t := by
  let f : E → ℝ → ℝ := fun x t ↦ ∫ s in (0)..t, γ.centeringDensity x s
  have hsurj : ∀ (x : E), Surjective (f x) := sorry
  change 𝒞 ⊤ fun p : E × ℝ ↦ (StrictMono.orderIsoOfSurjective (f p.1) _ (hsurj p.1)).symm p.2
  apply contDiff_parametric_symm_of_deriv_pos
  · exact contDiff_parametric_primitive_of_contDiff'' γ.centeringDensity_smooth 0
  · exact fun x ↦ deriv_integral_centeringDensity_pos γ x

then the magic is back.

[Patrick Massot]

Ooooh… It didn’t occur to me at all that the goal could be different before the apply. It makes a lot more sense than a apply change.

[Patrick Massot]

I’m still happier with my three goals, but I guess I’m probably using the same magic elsewhere without noticing it.

[Kyle Miller]

It's odd that isDefEq isn't seeing surjective_integral_centeringDensity γ as being the necessary proof of surjectivity, but I guess it's in different of enough form that Lean doesn't notice.

By beta expanding and inserting an id, I was able to get it back to three goals, so Lean is able to solve for this by unification if the stars align.

theorem reparametrize_smooth : 𝒞 ∞ <| uncurry fun (x : E) (t : ℝ) ↦ γ.reparametrize x t := by
  let f : E → ℝ → ℝ := fun x t ↦ ∫ s in (0)..t, γ.centeringDensity x s
  change 𝒞 ⊤ fun p : E × ℝ ↦ (StrictMono.orderIsoOfSurjective (f p.1) _ (((id fun x => surjective_integral_centeringDensity γ x) : ∀ (x : E), Surjective (f x)) p.1)).symm p.2
  apply contDiff_parametric_symm_of_deriv_pos
  · exact contDiff_parametric_primitive_of_contDiff'' γ.centeringDensity_smooth 0
  · exact fun x ↦ deriv_integral_centeringDensity_pos γ x

[Kyle Miller]

I can't say what the exact change was, but the investigation is pointing toward "this is working as intended, and this proof was previously relying on a higher-order unification of proof terms working out"