Backporting coercions

Stream: general

[Gabriel Ebner]

Yury is currently busy backporting the coercion type classes from Lean 4. I'm wondering if it makes sense to backport the coercion unfolding as well. This will break a lot of stuff in mathlib. Therefore it could make sense to do this refactoring before the port. I am just bringing it up as an option. Making the change in core is not too involved, but I don't think I'll be able to take on the mathlib refactoring.

[Yury G. Kudryashov]

What changed about the coercion unfolding in Lean 4?

[Yury G. Kudryashov]

About coe_fn, could you please fix the pretty printer? I guess the broken function is pp_hide_coercion_fnbut I'm not sure. The broken test is tests/lean/coe4.

[Yury G. Kudryashov]

One more issue: now Lean fails to generate instance names for has_coe_to_fun instances.

[Gabriel Ebner]

I'm not sure if everybody realizes this, but Lean 4 doesn't have ⇑ or ↑. The coercion is immediately eliminated after/during elaboration:

instance : CoeFun Nat (fun _ => Nat → Nat) where
  coe a b := a + b

#check (4 : Nat) 8
-- (fun (b : Nat) => 4 + b) 8 : Nat

[Yury G. Kudryashov]

So, we'll see explicit (e : E →L[R] F).to_linear_map, subtype.val etc?

[Yury G. Kudryashov]

I mean, in the proof state.

[Gabriel Ebner]

Yes.

[Yury G. Kudryashov]

:(

[Yury G. Kudryashov]

But we won't need coe_mk etc. :-)

[Yury G. Kudryashov]

But we'll need a new norm_cast that tracks all functions used as coercions, not only coe/coe_fn.

[Sebastien Gouezel]

One will need some pretty-printer tweaking so that subtype.val shows up as a little arrow, as well as all the other functions we are used to as coercions. Then the situation should not be really different from what we are used to.

[Yury G. Kudryashov]

No way to have @[simp] lemma [is_monoid_hom (coe : M → N)] (x y : M) : ((x * y : M) : N) = x * y := ... (though we want to have it as a rfl simp lemma in many cases anyway)

[Eric Wieser]

How does this unfolding work? Is CoeFun special cased in the elaborator?

[Eric Wieser]

Do subclasses of it get unfolded in the same way?

[Mario Carneiro]

I don't think we should bother backporting this. We can eliminate coercions in mathport, but this is going to need a lot of manual work to make it work well and I'd rather do that work in a context where the rest of lean 4 is available

[Yury G. Kudryashov]

Thanks to @Gabriel Ebner, Lean core builds with the new has_coe_to_fun and has_coe_to_sort. I've started porting mathlib and found out that has_coe_to_sort doesn't work as expected (by me):

universe u

instance {α : Type u} : has_coe_to_sort (set α) (Type u) := ⟨λ s, {x // x ∈ s}⟩

example : ↥({0} : set ℕ) := ⟨0, rfl⟩

now fails with message "5:29: invalid constructor ⟨...⟩, 'has_coe_to_sort.coe' is not an inductive type"

[Yury G. Kudryashov]

branch#coe-fn-backport

[Eric Wieser]

This sounds like something that #6768 might make worse

[Eric Wieser]

Did the elaborator have special support for this before that we forgot to patch?

[Gabriel Ebner]

This works just fine if you remove the ↥.

[Eric Wieser]

So this is like the opposite of the let bug I found recently that required the arrow?

[Gabriel Ebner]

If you will. I'm not completely sure why it worked before, but I've pushed a fix to the branch.

[Yury G. Kudryashov]

I'm trying to adjust simps. Currently it uses this code

        e_inst_type ← to_expr ((expr.const class_nm []).app (pexpr.of_expr e_str)),
        e_inst ← try_for 1000 (mk_instance e_inst_type),

to find an instance of has_coe_to_fun/has_coe_to_sort. This no longer works because these classes now take one more argument. How do I fix this?

[Yury G. Kudryashov]

Ping @Floris van Doorn and @Gabriel Ebner here

[Yury G. Kudryashov]

Fixed simps. The next expression that used to work with the old coe_fn but fails now:

universe u

structure End (α : Sort*) := (to_fun : α → α)

instance {α} : has_coe_to_fun (End α) (λ _, α → α) := ⟨End.to_fun⟩

-- This works fine
example {f g : End ℕ} (h : (f : ℕ → ℕ) = g) : f = g := by cases f; cases g; cases h; refl

-- This fails with error
-- failed to synthesize type class instance for
-- f g : End ℕ
-- ⊢ has_coe_to_fun (End ℕ) (λ {f : End ℕ}, End ℕ)"
example {f g : End ℕ} (h : ⇑f = g) : f = g := by cases f; cases g; cases h; refl

[Yury G. Kudryashov]

One more problem: derive has_coe_to_sort no longer works because has_coe_to_sort new_def is not a Sort*

[Eric Wieser]

Does derive [\lam T, has_coe_to_sort T (A \to B)]?

[Yury G. Kudryashov]

I'll try tonight (or you can try on branch#coe-fn-backport)

[Yury G. Kudryashov]

Also, I can't understand why Lean fails to simplify using swap_apply_left in group_theory/perm/sign, line 439

[Eric Wieser]

Oh, I bet in the context of the derive handler A and B aren't available yet

[Yury G. Kudryashov]

So far I was replacing derive with explicit instances.

[Eric Wieser]

I think that's probably fine

[Yury G. Kudryashov]

I have no idea why it fails in perm/sign.

[Yury G. Kudryashov]

@Scott Morrison Could you please fix elementwise in branch#coe-fn-backport? In this branch we moved F/S in has_coe_to_fun/has_coe_to_sort from output to an out_params argument.

[Scott Morrison]

Certainly I can try, but unfortunately I won't really have time until next Tuesday. I've already exceeded my Lean budget today and should start packing for the weekend! I've starred this message.

[Bhavik Mehta]

I had a go at fixing this in branch#coe-fn-backport-bmehta-test (so as not to mess up anyone else's work), I think it worked? The CI error is in a different file now at least

[Yury G. Kudryashov]

Thank you! Merged back to my branch, fixing other errors.

[Yury G. Kudryashov]

I fixed all compile errors in src/, see #7033, but there are a few regressions that may be related to the changes in C++ code. I'll try to make #mwe's tonight.

• sometimes exact ⟨_, by simp, a + b⟩ fails to deduce the value of _ from a + b before evaluating by simp, see these lines of the diff.
• sometimes Lean needs more type annotations, may be related to the previous item, see here;
• @[derive has_coe_to_fun] no longer works because has_coe_to_fun my_type is not a Sort*. Is it hard to make derive work when myclass mytype is Π (arg : Type . out_param), Sort*?
• simp can't use coe_fn_coe_base, see here and here;
• lemma coe_inj {e₁ e₂ : α ≃ β} : ⇑e₁ = e₂ ↔ e₁ = e₂ := no longer works, now we need lemma coe_inj {e₁ e₂ : α ≃ β} : (e₁ : α → β) = e₂ ↔ e₁ = e₂ :=;
• change ... with ... causes timeout here;
• in one proof simp fails to use swap_apply_left and swap_apply_right

[Yury G. Kudryashov]

And tests still fail. Some of them indicate that we need to fix linters about coe_fn.

[Yury G. Kudryashov]

@Gabriel Ebner Ping here

[Yury G. Kudryashov]

I've updated both Lean branch and mathlib branch.

[Yury G. Kudryashov]

Pushed to #7033, waiting for CI. Probably there will be some new failures.

[Yury G. Kudryashov]

@Eric Wieser @Anne Baanen :up:

[Yury G. Kudryashov]

See also the list of regressions from April. I guess, it's still the same.

[Anne Baanen]

Thanks for the update! I'll take a look in about 1 hour.

[Yury G. Kudryashov]

Pushed some fixes

[Yury G. Kudryashov]

I don't know how to fix the deterministic timeout (see CI).

[Scott Morrison]

@Yury G. Kudryashov I've pushed a fix for this timeout.

[Anne Baanen]

Fixed everything in src/ and some things in test/, now merging master and seeing what broke in the meantime.

[Anne Baanen]

Another bump, fixed src and some more files in test. We're nearly there now...

[Anne Baanen]

src and test now fully build on my machine. Let's hope the CI runner doesn't crash this time.

[Anne Baanen]

Another week, another bump. All tests passed on my machine before the merge, let's see what they do now.

[Johan Commelin]

Should we freeze the queue and prioritize this?

[Gabriel Ebner]

What is the state with mathlib? Can we expect to port mathlib to the change in a timely manner?

[Johan Commelin]

@Gabriel Ebner I think that's what #7033 is doing.

[Gabriel Ebner]

Ah ok, that one only has failures in the tests.

[Gabriel Ebner]

I'm happy with merging lean#557

[Johan Commelin]

Let's go for it.

[Anne Baanen]

Gabriel Ebner said:

Ah ok, that one only has failures in the tests.

It even built completely once on my machine, except mathlib got some new has_coe_to_fun definitions :P

[Johan Commelin]

Seems like bors is having trouble to find time for lean#557

[Johan Commelin]

But I don't think it's waiting for a runner, right?

[Bryan Gin-ge Chen]

The staging build has a job which appears to be stuck: https://github.com/leanprover-community/lean/runs/3941583934?check_suite_focus=true

[Johan Commelin]

lean#557 is now merged. So #7033 should become the corresponding "bump lean" PR, I guess.

[Johan Commelin]

Ooh never mind, I guess we first need a lean release.

[Gabriel Ebner]

Yeah, the previous PR (not even #557) was stuck in the "Build sanitized" steps for an unknown reason. I've put the other one back one queue again as well.

[Daniel Selsam]

Could somebody please adjust the types of the coercion inductives to match Lean4?

Coe.{u_1, u_2} : Sort u_1 → Sort u_2 → Sort (max (max 1 u_1) u_2)
Coeₓ.{u_1, u_2} : Sort u_1 → Sort u_2 → Sort (max 1 (imax u_1 u_2))
CoeFun.{u_1, u_2} : (α : Sort u_1) → outParam.{max u_1 (u_2 + 1)} (α → Sort u_2) → Sort (max (max 1 u_1) u_2)
CoeFunₓ.{u_1, u_2} : (a : Sort u_1) → outParam.{max u_1 (u_2 + 1)} (a → Sort u_2) → Sort (max u_1 (u_2 + 1))
CoeSort.{u_1, u_2} : Sort u_1 → outParam.{u_2 + 1} (Sort u_2) → Sort (max (max 1 u_1) u_2)
CoeSortₓ.{u_1, u_2} : Sort u_1 → outParam.{u_2 + 1} (Sort u_2) → Type (max u_1 (u_2 + 1))

[Scott Morrison]

https://github.com/leanprover-community/lean/pull/632

[Scott Morrison]

I haven't done any testing, just handed it off to CI for now.

[Daniel Selsam]

Thanks! I forgot that the mathlib-propagation happens later.

[Scott Morrison]

It seems plausible that there may not be any changes required in mathlib. Later today I'll make a mathlib branch to test.

[Yury G. Kudryashov]

I suggest that we merge #9824 without waiting for this.

[Yury G. Kudryashov]

Once lean#632 (and its mathlib part) are ready, we can release a new Lean and merge again.

[Yury G. Kudryashov]

@maintainers Should I merge #9824 once CI is happy? It was happy with the previous commit, and the last commit just removes a duplicate import, so I'm pretty sure that CI will be happy.

[Rob Lewis]

Can we edit Scott's post so the commit message says something about the coercion changes?

[Rob Lewis]

Nothing long, but this is a big breaking change, it doesn't hurt to have it in the permanent record

[Rob Lewis]

Otherwise I'm fine with merging

[Yury G. Kudryashov]

I added a short commit message. Did I forget something?

[Yury G. Kudryashov]

I also see a new command setup_tactic_parser. @Rob Lewis could you please add its description to the commit message?

[Rob Lewis]

setup_tactic_parser has been around for ages, looks like it just got a minor update because of the namespacing changes. https://github.com/leanprover-community/mathlib/pull/9824/files#diff-41e4d36d845844e40ede47bd45f062b5f9293b9517112eb65dcfed9f25ce17cfL1886

[Scott Morrison]

We use setup_tactic_parser a lot more now, both because we should, and a lot of the open statements that it can replace needed fixing anyway.