transitive coercions

Stream: general

[Reid Barton]

Here's the first thing which broke in a nontrivial way when I made coe_fn_trans and coe_sort_trans no longer instances:

lemma Union_range_eq_sUnion {α β : Type*} (C : set (set α))
  {f : ∀(s : C), β → s} (hf : ∀(s : C), surjective (f s)) :
  (⋃(y : β), range (λ(s : C), (f s y).val)) = ⋃₀ C :=

[Reid Barton]

(By "nontrivial", I mean something not directly related to transitive coercions. Obviously the fix for this example is still simple.)

[Mario Carneiro]

I recommend explicitly putting in multiple type ascriptions whenever we literally want a transitive coercion

[Reid Barton]

I got distracted from this project, but a second class of issues are ones where we define a new type and a has_coe instance for it to another type that has a coercion to function/sort, and expect the new type to also have a coercion to function/sort. A prototypical example is subgroup G which has a coercion to set G. These are easily addressed by adding an explicit has_coe_to_sort instance.

[Gabriel Ebner]

These need to be fixed anyhow. Transitive coercion instances are not in simp-normal form.

[Reid Barton]

If we want to make this change, it might be handy to write a little attribute we can put on has_coe instances to automatically generate has_coe_to_sort/has_coe_to_fun instances--though they're quite easy to write by hand also: I've been using things like

instance : has_coe_to_sort (submodule R M) := @coe_sort_trans _ (set M) _ _

and it seems to be working so far...

[Reid Barton]

In a fancier system, maybe it would be worth thinking of "an R-submodule of M is a set" as a different kind of thing from "a natural number is an integer"

[Reid Barton]

Haha, I briefly panicked when a dsimp in the middle of some random proof stopped working, but I just deleted it and all is well :slight_smile:

[Reid Barton]

Whoa, it builds :tada:
20 files changed, 38 insertions(+), 37 deletions(-)

[Johan Commelin]

That's actually a rather small diff

[Reid Barton]

and a little bit is commenting out things that should just be deleted, so it actually saves a few lines overall

[Johan Commelin]

And speeds up the build, I guess

[Johan Commelin]

But probably not noticable

[Reid Barton]

Here is the commit if anyone is interested; there are some bits like the has_coe_to_fun_linter which I don't understand yet.

[Reid Barton]

I assume it doesn't build with the current version of Lean, but I suppose it might

[Reid Barton]

Ah, the CI build failed immediately because of my change to leanpkg.toml--probably for the best :slight_smile:

[Gabriel Ebner]

The has_coe_to_fun linter is supposed to check for exactly this kind of problem, where a type has a has_coe instance but no has_coe_to_fun. If the transitive instances are gone, then the linter is no longer necessary.

[Reid Barton]

So here's my proposal (https://github.com/leanprover-community/mathlib/compare/rwbarton-no-trans):

1. Remove coe_fn_trans and coe_sort_trans as instances from core, turning them into @[reducible] defs (so that they can be used as the definitions of instances, and will still be transparent to instance search).
2. Remove the related simp lemmas (even though I guess we could keep them, they don't seem to be useful any more), library notes, linter in mathlib.
3. Add back instances instance {α : Sort*} [has_coe_to_fun α] (p : α → Prop) : has_coe_to_fun (subtype p), instance {α : Sort*} [has_coe_to_sort α] (p : α → Prop) : has_coe_to_sort (subtype p) to core. (Currently they are in my mathlib patch rather than core but that is only out of laziness.) These are Haskell 98-style instances so they should not cause any trouble--there's exactly one way to treat x : subtype p as a function/sort, namely by treating x.val as a function/sort.
4. Add back has_coe_to_sort/has_coe_to_fun instances for things like lie_subalgebra, M ≃L[R] M₂ (whatever this is), etc.--there's a fairly small number of these.

[Reid Barton]

Actually I guess in 4, all the has_coe_to_fun instances already existed (thanks to the linter) but I had to reimplement some of them to not rely on the transitive instance.

[Reid Barton]

Or more precisely: not rely on coe_fn_trans being an instance (now they invoke it by name).

[Reid Barton]

Overall, the change seems like a simplification, besides fixing the strange coercion of nat to nat -> real (though I haven't actually tested this).

[Reid Barton]

The alternative as I see it is to be a lot more judicious with the choice between has_coe and has_coe_t--in principle this seems better as it generalizes what I did for subtype specifically, but I'm not sure whether we can be trusted to choose wisely. Maybe @Gabriel Ebner's linter from #2573 will help with that though?

[Gabriel Ebner]

#2573 moves some coercions (ℕ → α, etc.) to has_coe_t. These will hence no longer participate in function coercion. Not sure if this was the problem here.

[Reid Barton]

I think it was int → α that was involved here.

[Gabriel Ebner]

I have mixed feelings about the proposed change here. I detest transitive coercions as much as everyone here, and would remove them today if it helped. But I fear that these instances will just come back in a few months.

[Reid Barton]

By "these instances" do you mean ones like int → α? Or coe_fn_trans as a global instance? Or ones like those I added for subtype?

[Gabriel Ebner]

coe_fn_trans

[Gabriel Ebner]

The others are in mathlib, we can remove or change them as much as we want.

[Reid Barton]

Ohh, you mean in Lean 4.

[Reid Barton]

I thought you meant the feature creep of people adding more and more instances because they look nice, and then it falls apart.

[Reid Barton]

I am also happy with your approach in #2573 as long as we can communicate clearly how to decide whether to use has_coe or has_coe_t and enforce it.

[Reid Barton]

Indeed I already thought when writing those subtype instances that they could be part of a more general system, and then realized the general system already existed but we were not using it correctly.

[Reid Barton]

We can have linters that see all modules at once, to check for things like cycles, right?

[Gabriel Ebner]

The fixes in #2573 are necessary irrespective of whether we remove coe_fn_trans and coe_sort_trans or not. The issues already pop up with regular coercions. My one-size-fits-all solution for enforcement and communication is of course a linter, which the PR includes.

[Patrick Massot]

I think it would be a huge mistake to start refactoring mathlib in a way which is guaranteed to make the Lean 4 migration more painful.

[Reid Barton]

Well, it can't be that huge a mistake because the diff already exists and it is +31 -128 lines of code.

[Patrick Massot]

This is only an abstract comment based on Gabriel's message

[Patrick Massot]

I have no clue about the current discussion

[Reid Barton]

Sure, I just mean that as it happens we are fortunately not discussing any herculean effort.

[Mario Carneiro]

Patrick Massot said:

I think it would be a huge mistake to start refactoring mathlib in a way which is guaranteed to make the Lean 4 migration more painful.

I think it would be a huge mistake to take everything in lean 4 as gospel, because that's what lead to the situation where we worked around lean 3 bugs for a year. I think we should try to make the best lean we can, and when lean 4 comes out we will either forward port our changes to lean 4 or fork if necessary. I'm not about to lose progress made in lean 3 on account of the new version.

[Mario Carneiro]

This might be obvious, but I don't think we should move to lean 4 until it is better than lean 3.10 or whatever the latest version is at that time. Ideally that would be better in every way (pareto-dominant), but for every thing that we have to sacrifice it should be a conscious decision based on a cost-benefit tradeoff. That means in particular that all the little tweaks and additions that are going into later lean 3 versions should be mimicked appropriately, and of course all the theorems should be carried over. If that sounds like a long and difficult process, I agree, I think we will be on lean 3 for a while yet.

[Johan Commelin]

Well... doesn't the CamelCase allready rule out pareto-dominance? :wink:

[Patrick Massot]

Mario, you know this will not happen. If Lean 4 achieves half of what it promises then it will be much better than Lean 3 and we'll switch. And nobody will have the time, skill and energy to maintain a fork while Lean 4 will continue to change.

[Mario Carneiro]

At the very least, I would want roadmaps and open issues for every feature that we leave behind in our anxiety to ride the next wave

[Mario Carneiro]

Whether or not a fork is necessary depends on interaction between Leo & co and mathlib & co. So far it's basically nil, and there is some evidence that this is not merely because lean 4 is an separate project from mathlib, so I am not expecting this to change to another governance structure when it matures

[Kevin Buzzard]

Whether there is interactivity in the future will, I should think, depend a lot on whether our community manages to hold back and let Leo and his team deal with issues which are important to them, or whether we just flood the issues page with complaints that it's not like how it was and could they please fix it.

[Kevin Buzzard]

It will be a delicate balancing act.

[Kevin Buzzard]

But one thing we do need to remember is that there were a hell of a lot of issues with Lean 3 which we managed to deal with on the mathlib side

[Kevin Buzzard]

I wasn't there at the time, but one impression I got was that Leo does not take kindly to being told that what he did was not as good as doing it some other way, especially when he can see subtle problems with the other way which are not apparent to most.

[Sebastien Gouezel]

Since coercions are a hot topic today, let me ask again about the issue of simp and coercions. In the following code

variable (α : Type*)

structure my_equiv :=
(to_fun : α → α)

instance : has_coe_to_fun (my_equiv α) := ⟨_, my_equiv.to_fun⟩

def my_equiv1 : my_equiv α :=
{ to_fun := id }

def my_equiv2 : my_equiv α :=
{ to_fun := id }

@[simp] lemma one_eq_two : my_equiv1 α = my_equiv2 α := rfl

@[simp] lemma two_apply (x : α) : my_equiv2 α x = x := rfl

lemma one_apply (x : α) : my_equiv1 α x = x := by simp -- fails

simp fails in the last lemma, because it should simplify in a coercion and it is unable to do this. This is the reason why, in manifolds, I could not use coercions and I used e.to_fun and e.inv_fun all over the place. Is this something that is so deeply buried in C++ that there is no hope to fix it?

[Gabriel Ebner]

I don't think this is something we can easily fix in mathlib. The core problem is that has_coe_to_fun doesn't necessarily coerce to a function.

[Kevin Buzzard]

Doesn't not?

[Kevin Buzzard]

I am confused either way

[Gabriel Ebner]

It's confusing.

[Reid Barton]

I guess the problem is my_equiv1 α x means coe_fn (my_equiv1 α) x but coe_fn has a dependent type: coe_fn (my_equiv1 α) has type has_coe_to_fun.F (my_equiv1 α). That means rewriting my_equiv1 α to my_equiv2 α might result in a type-incorrect expression.

[Reid Barton]

Of course in this case it does not because has_coe_to_fun.F (my_equiv1 α) and has_coe_to_fun.F (my_equiv2 α) are definitionally equal (they are both α -> α).

[Reid Barton]

I actually never knew about this issue because I would always abandon coercions earlier when α could not be inferred in my_equiv1 α x.

[Gabriel Ebner]

Do we actually use dependent function coercions? That is, 1) where coe_fn a : α a → β a depends on a, or 2) where coe_fn a : ∀ x : α, β x is a dependent function?

[Reid Barton]

I wouldn't be surprised if dfinsupp is an example of 2

[Reid Barton]

But 1 would be more surprising I think...

[Sebastien Gouezel]

I would love having two versions of has_coe_to_fun, a non-dependent one where simp would work, and a dependent one has_coe_to_dep_fun where it wouldn't. Because I guess in 99% of the situations we use a non-dependent version...

[Gabriel Ebner]

lean#209

[Patrick Massot]

Gabriel, do you understand the Lean 4 answer here? I remember Sebastian pointed out a commit "simplifying coercions to functions"

[Gabriel Ebner]

As far as Sébastien's problem is concerned, the coeFun function has essentially the same signature: https://github.com/leanprover/lean4/blob/0c4030137f24f2371db85469de2f627eccbb1703/src/Init/Coe.lean#L59-L60 The only difference is that the function space is now an out param. I don't think there are congruence lemmas yet in Lean 4.

[Sebastien Gouezel]

Gabriel, will your fix for simp in has_coe_to_fun also fix the congr behavior? I mean

import tactic.basic

variable (α : Type*)

structure my_equiv :=
(to_fun : α → α)

instance : has_coe_to_fun (my_equiv α) := ⟨_, my_equiv.to_fun⟩

lemma fail (e f : my_equiv α) (x : α) (h : e = f) : e x = f x :=
begin
  unfold_coes,
  congr,
  exact h
end

Without the unfold_coes, congr does not work. I guess it is because it has to identify has_coe_to_fun.F on the left and on the right, but since it has lost the information on the type it is working with, there is no way it can do this. Even congr' 1 fails here. I have learnt to always unfold coercions before applying congr, but this can be a tricky one the first time you encounter it.

[Gabriel Ebner]

Works for me both with and without unfold_coes.

[Sebastien Gouezel]

You mean, on Lean 3.9 or Lean 3.10?

[Gabriel Ebner]

Lean 3.10.

[Sebastien Gouezel]

Great, thanks again!