Reducible

Stream: new members

[Nicolò Cavalleri]

If I introduce a type synonym with @[reducible] def, I know type class instances will lift from the underlying type to the type synonym, but is it true that instances declared on the type synonym will descend on the underlying type? I used to think not but in #7803 it seems instances are descending...

[Johan Commelin]

It wouldn't surprise me if they descend. I thinkthat in practice it's better to write @[derive [add_comm_group, topological_space]] before a semireducible def.

[Eric Wieser]

Usually the whole point of a type synonym is to _not_ be reducible so that you can pick a different instance implementation

[Nicolò Cavalleri]

Eric Wieser said:

Usually the whole point of a type synonym is to _not_ be reducible so that you can pick a different instance implementation

But then I'd need to rewrite a lot of instances: I need all the instances to lift and I whish there were a way to do so automatically

[Eric Wieser]

why do you need a synonym at all then?

[Nicolò Cavalleri]

Johan Commelin said:

It wouldn't surprise me if they descend. I thinkthat in practice it's better to write @[derive [add_comm_group, topological_space]] before a semireducible def.

What is a semireducible def?

[Johan Commelin]

The default.

[Johan Commelin]

And hopefully the derive handler can take care of most of the instances in just 1 line.

[Nicolò Cavalleri]

Johan Commelin said:

And hopefully the derive handler can take care of most of the instances in just 1 line.

Ok thanks do I need to list the ones I need or is there a way to get them all?

[Johan Commelin]

No, you need to list everything you need.

[Nicolò Cavalleri]

Eric Wieser said:

why do you need a synonym at all then?

Because I need to declare instances that I do not want to descend: the type synonym I want is for a Pi type and if the instances descend then mathlib breaks

[Nicolò Cavalleri]

Johan Commelin said:

No, you need to list everything you need.

Ok thanks

[Johan Commelin]

Can you use a regular Pi type with a local instance?

[Johan Commelin]

So instead of instance foobar you write def foobar and then local attribute [instance] foobar below it.

[Nicolò Cavalleri]

Johan Commelin said:

Can you use a regular Pi type with a local instance?

No I need instances to be permanent: all this is for sections of vector bundles implemented with pi types, I need to do things once for all

[Eric Wieser]

Right, I was unclear: type synonym are for when you want some instances to be different

[Eric Wieser]

A good example in the library is docs#finsupp vs docs#monoid_algebra, which have different choices of * but agree on+

[Nicolò Cavalleri]

Eric Wieser said:

Right, I was unclear: type synonym are for when you want some instances to be different

Oh in this case I do not need instances to be different, I just need to add more instances that cannot be declared on generic pi types (and even if they could it would not makes sense to have them on generic pi types)

[Nicolò Cavalleri]

What would you do in such case? I'm persuaded by Johan to use derive

[Eric Wieser]

derive is the best tool for the job when it works

[Eric Wieser]

Sometimes you can't use it though; if your instance is something like "additionally, when the domain is a field provide this other instance" you have to add those instances by hand

[Eric Wieser]

See for instance src#monoid_algebra.is_scalar_tower where the copy is manual

[Eric Wieser]

Can you elaborate on what the instance is, and why it doesn't make sense to put it on generic pi types? (A line link to a PR is fine)

[Nicolò Cavalleri]

Eric Wieser said:

Sometimes you can't use it though; if your instance is something like "additionally, when the domain is a field provide this other instance" you have to add those instances by hand

Oh yes this is totally my case... I feel it will be a pain copying instances by hand

[Nicolò Cavalleri]

This is the link https://github.com/leanprover-community/mathlib/pull/7803/files#r665803546

[Nicolò Cavalleri]

You can see all the problems it creates by checking the linter check on the same PR

[Nicolò Cavalleri]

(since bundle_section is reducible, it changes nothing when the bare pi type is used instead)

[Nicolò Cavalleri]

Let me know if you have ideas to solve the problem

[Eric Wieser]

Do you really need a coercion there? Or would .to_right_inv be acceptable as a spelling instead?

[Eric Wieser]

Ignoring instances for a moment, the statement seems quite weird - you're saying that for any f, λ x, sigma.mk x (f x) is a right inverse to sigma.fst

[Nicolò Cavalleri]

Yes I'd need a coercion. Basically I want sections for vector bundles to be recognized as sections for fiber bundles

[Nicolò Cavalleri]

Why is the statement weird? It seems natural to me

[Eric Wieser]

I've realized that the coercion you're after can be broken down into one that almost already exists (docs#lift_fn_range), and one that doesn't:

import tactic.lint

variables (ι : Type*) (A : ι → Type*) (B : ι → Type*)
/-- Should this be a `lift` instead? Or maybe this should work on a type alias of
`sigma`, which I think you have already. -/
instance has_coe_to_sigma (i : ι) : has_coe (A i) (sigma A) := ⟨sigma.mk i⟩

/-- A dependent version of `lift_fn_range`. It's easy to argue this should exist,
but note it uses `has_lift` not `has_coe`, so the `↑` is required. -/
instance lift_fn_range' [Π i, has_lift_t (A i) (B i)] :
  has_lift (Π i, A i) (Π i, B i) := ⟨λ f i, ↑(f i)⟩


-- the coercion lean finds is the one you're asking for, it seems
example (f : Π i, A i) : (↑f : ι → sigma A) = λ i, ⟨i, f i⟩ := rfl

[Nicolò Cavalleri]

Is the only difference between has_coe and has_lift for has_lift you need to put the arrow yourself whereas for has_coe Lean does automatically?

[Nicolò Cavalleri]

Also I never understood what has_lift_t is, since "theorem proving in Lean" only says transitive closure which I do not know what it is...

[Nicolò Cavalleri]

Eric Wieser said:

I've realized that the coercion you're after can be broken down into one that almost already exists (docs#lift_fn_range), and one that doesn't:

import tactic.lint

variables (ι : Type*) (A : ι → Type*) (B : ι → Type*)
/-- Should this be a `lift` instead? Or maybe this should work on a type alias of
`sigma`, which I think you have already. -/
instance has_coe_to_sigma (i : ι) : has_coe (A i) (sigma A) := ⟨sigma.mk i⟩

/-- A dependent version of `lift_fn_range`. It's easy to argue this should exist,
but note it uses `has_lift` not `has_coe`, so the `↑` is required. -/
instance lift_fn_range' [Π i, has_lift_t (A i) (B i)] :
  has_lift (Π i, A i) (Π i, B i) := ⟨λ f i, ↑(f i)⟩


-- the coercion lean finds is the one you're asking for, it seems
example (f : Π i, A i) : (↑f : ι → sigma A) = λ i, ⟨i, f i⟩ := rfl

The first coercion here already exists (for the type Alias)

[Eric Wieser]

Looking at the instances for docs#has_coe_t may help understand what transitivity means here

[Eric Wieser]

In particular, docs#coe_trans is the key

[Eric Wieser]

Which says "if A is convertible to B and B is transitively convertible to C, then A is transitively convertible to C"

[Eric Wieser]

The other half of this "induction" rule is docs#coe_base, which says "if A is convertible to B then if A is transitively convertible to B"

[Nicolò Cavalleri]

What does transitively means?

[Eric Wieser]

That definition is self-referencing, it means what it defines it to mean

[Nicolò Cavalleri]

Oh I see

[Eric Wieser]

That's not the whole picture, but it's hopefully enough to get an idea

[Nicolò Cavalleri]

So it is something that is just internal to Lean, the user should never declare has_coe_t themselves

[Eric Wieser]

No, you declare has_coe_t instead of has_coe if you don't want your coercion to take place anywhere but at the end of transitive coercions

[Eric Rodriguez]

for example, iirc, the ℕ → arbitrary semiring coe is defined as has_coe_t

[Eric Wieser]

Either because otherwise the search would be too big (the linter will usually catch this), or because it doesn't make sense

[Eric Wieser]

There's a library note about that, right @Eric Rodriguez?

[Nicolò Cavalleri]

Eric Wieser said:

No, you declare has_coe_t instead of has_coe if you don't want your coercion to take place anywhere but at the end of transitive coercions

Oh I see, I guess this is also the reason why is it useful to distinguish between has_coe_t and has_coe and they cannot all be has_coe

[Eric Rodriguez]

yes I think so

[Eric Rodriguez]

https://leanprover-community.github.io/mathlib_docs/notes.html#coercion%20into%20rings here we are!

[Nicolò Cavalleri]

Eric Wieser said:

I've realized that the coercion you're after can be broken down into one that almost already exists (docs#lift_fn_range), and one that doesn't:

import tactic.lint

variables (ι : Type*) (A : ι → Type*) (B : ι → Type*)
/-- Should this be a `lift` instead? Or maybe this should work on a type alias of
`sigma`, which I think you have already. -/
instance has_coe_to_sigma (i : ι) : has_coe (A i) (sigma A) := ⟨sigma.mk i⟩

/-- A dependent version of `lift_fn_range`. It's easy to argue this should exist,
but note it uses `has_lift` not `has_coe`, so the `↑` is required. -/
instance lift_fn_range' [Π i, has_lift_t (A i) (B i)] :
  has_lift (Π i, A i) (Π i, B i) := ⟨λ f i, ↑(f i)⟩


-- the coercion lean finds is the one you're asking for, it seems
example (f : Π i, A i) : (↑f : ι → sigma A) = λ i, ⟨i, f i⟩ := rfl

I wonder why this code would work: is B → E just syntactic sugar for Π x: B, E? Otherwise how does Lean recognize a function as a dependent type?

[Nicolò Cavalleri]

A connected question: should then

instance lift_fn_range' [Π i, has_lift_t (A i) (B i)] :
  has_lift (Π i, A i) (Π i, B i) := ⟨λ f i, ↑(f i)⟩

completely replace lift_fn_range?

[Eric Wieser]

Yes, it is just syntactic sugar

[Eric Wieser]

I think it might still be worth having both; dependent typed instances create more work for the elaborator, and having a non-dependent variant will both provide a possible shortcut, and allow the user to disable the slower instance separately.

[Eric Wieser]

I don't think there's much harm to having both, at any rate

[Nicolò Cavalleri]

Ok isn't there a coe version of lift_fn_range? I was so convinced there was...

[Eric Wieser]

No, and that's a deliberate choice I think

[Nicolò Cavalleri]

Where would you place your lift_fn_range?

[Eric Wieser]

I'd probably make a PR against lean core to add it next to lift_fn_range

[Eric Wieser]

Alternatively, logic.function.basic would be reasonable

[Nicolò Cavalleri]

Eric Wieser said:

I'd probably make a PR against lean core to add it next to lift_fn_range

Yeah I'm not sure I would know how to do this... should I PR to a different repo than that of mathlib?

[Ruben Van de Velde]

https://github.com/leanprover-community/lean/ ?

[Eric Wieser]

src#lift_fn_range should tell you where the file is that needs changing

[Eric Wieser]

If you edit that file, changing a few /- -/s to /-! -/ would make them appear in the web docs

[Nicolò Cavalleri]

Ruben Van de Velde said:

https://github.com/leanprover-community/lean/ ?

Ok thanks

[Nicolò Cavalleri]

Eric Wieser said:

If you edit that file, changing a few /- -/s to /-! -/ would make them appear in the web docs

Do you have specific ones I should change or most of them?

[Eric Wieser]

Mainly the one at the top of the file

[Kyle Miller]

L7: /-!

L101 L118 L140 L150 (maybe L168): /--

[Nicolò Cavalleri]

Should I fork or can I get permission to contribute so to open a new branch?

[Nicolò Cavalleri]

Kyle Miller said:

L7: /-!

L101 L118 L140 L150 (maybe L168): /--

Ok thanks

[Johan Commelin]

Nicolò Cavalleri said:

Should I fork or can I get permission to contribute so to open a new branch?

I'll give you permission, 1 sec.

[Nicolò Cavalleri]

Ok thanks

[Johan Commelin]

https://github.com/leanprover-community/lean/invitations

[Kyle Miller]

Nicolò Cavalleri said:

What does transitively means?

From a certain point of view, the coercion typeclasses define a relation on types/sorts, but rather than being Prop-valued, given types a and b, then there either is or is not an instance for has_coe a b (the relation is determined by the typeclass resolution algorithm rather than something more mathy).

Transitive closure then means what it does for relations: take the smallest transitive relation containing the original relation.

[Kyle Miller]

For normal mathy relations, you can use some inductive type to construct a transitive closure, but because the relation is implemented at the level of typeclasses, it's instead implemented using the coe_trans instance.

You can almost think of this as being one of the constructors of a Prop-valued inductive type has_coe_t:

instance coe_trans {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [has_coe_t b c] [has_coe a b] : has_coe_t a c

[Nicolò Cavalleri]

Is this the correct form to write it?

instance lift_pi_range {α : Sort*} {A : α → Sort*} {B : α → Sort*} [Π i, has_lift_t (A i) (B i)] : has_lift (Π i, A i) (Π i, B i) := ⟨λ f i, ↑(f i)⟩

[Kyle Miller]

Seems fine to me. You might use the universe variables defined in the file, just to clarify they're all different:

instance lift_pi_range {α : Sort u} {A : α → Sort ua} {B : α → Sort ub} [Π i, has_lift_t (A i) (B i)] :
  has_lift (Π i, A i) (Π i, B i) :=
⟨λ f i, ↑(f i)⟩

(also, newlines for line length reasons, though the first line is still over 100 characters)

[Nicolò Cavalleri]

Kyle Miller said:

Seems fine to me. You might use the universe variables defined in the file, just to clarify they're all different:

instance lift_pi_range {α : Sort u} {A : α → Sort ua} {B : α → Sort ub} [Π i, has_lift_t (A i) (B i)] :
  has_lift (Π i, A i) (Π i, B i) :=
⟨λ f i, ↑(f i)⟩

(also, newlines for line length reasons)

Ok for the universes, as for the length I saw that the convention in the file is to write everything on one line and many other lines are much longer than the one I wrote

[Kyle Miller]

I suppose mathlib style guidelines probably don't carry over to lean core, but if I were writing it I would probably use the new guidelines for new code (leaving everything else alone). Of course, it's up to you and the reviewers.

[Nicolò Cavalleri]

Once it will build in the Lean repo, how will we know it does not break anything in Mathlib?

[Eric Wieser]

Mathlib has to be manually bumped to new lean versions

[Eric Wieser]

Anyway, now that you've made the PR, someone more involved in lean releases than me should know what's best.

[Eric Wieser]

Thanks!

[Bryan Gin-ge Chen]

(For the record, the PR is at lean#590.)

[Nicolò Cavalleri]

Ok with this modification of Lean core, there is still a problem in my code, as shown in the following example:

import topology.topological_fiber_bundle

open bundle

variables {B : Type*} {E : B → Type*} [topological_space B] [topological_space (total_space E)]

instance lift_fn_range'' {α : Sort*} {A : α → Sort*} {B : α → Sort*} [Π i, has_lift_t (A i) (B i)] :
  has_lift (Π i, A i) (Π i, B i) := ⟨λ f i, ↑(f i)⟩

@[reducible] def bundle_section' (E : B → Type*) := Π x, E x

structure continuous_bundle_section' (E : B → Type*) [topological_space (total_space E)] :=
(to_fun : bundle_section E)
(continuous_to_fun : continuous (↑to_fun : B → total_space E))

variables (s : continuous_bundle_section' E)

instance : has_coe (continuous_bundle_section' E) (bundle_section' E) :=
⟨continuous_bundle_section'.to_fun⟩

-- works
@[continuity] lemma continuous' : continuous (↑(s : bundle_section' E) : B → total_space E) :=
s.continuous_to_fun

-- does not work... Why!? `has_lift_t` should be transitive!!
@[continuity] lemma continuous'' : continuous (↑s : B → total_space E) := s.continuous_to_fun

[Eric Wieser]

I suspect this is behaving strangely for you because has_coe_to_fun is getting involved here too

[Eric Wieser]

But I haven't tried it out myself so am only guessing.

[Nicolò Cavalleri]

What has_coe_to_fun are you referring to? there's none in the code!

[Kyle Miller]

I haven't taken any time to understand what's going on, but I did find this fix:

instance : has_lift (continuous_bundle_section' E) (bundle_section' E) :=
⟨continuous_bundle_section'.to_fun⟩

-- works
@[continuity] lemma continuous' : continuous (↑(↑s : bundle_section' E) : B → total_space E) :=
s.continuous_to_fun

-- works, too
@[continuity] lemma continuous'' : continuous (↑s : B → total_space E) := s.continuous_to_fun

[Kyle Miller]

Would this be acceptable?

import topology.topological_fiber_bundle

open bundle

variables {B : Type*} {E : B → Type*} [topological_space B] [topological_space (total_space E)]

@[reducible] def bundle_section (E : B → Type*) := Π x, E x

def bundle_section.to_total {E : B → Type*} (s : bundle_section E) : B → total_space E :=
λ b, ⟨b, s b⟩

structure continuous_bundle_section' (E : B → Type*) [topological_space (total_space E)] :=
(to_fun : bundle_section E)
(continuous_to_fun : continuous to_fun.to_total)

instance : has_coe (continuous_bundle_section' E) (bundle_section E) :=
⟨continuous_bundle_section'.to_fun⟩

variables (s : continuous_bundle_section' E)

@[continuity] lemma continuous' : continuous (bundle_section.to_total s : B → total_space E) :=
s.continuous_to_fun

[Kyle Miller]

It seems like basically you want every instance that Π x, E x already has (to give the space of sections structure when the fibers have that structure), so it's worth having bundle_section be reducible. But, it's fraught with peril to add additional instances to this. Dot notation here is used to add this to_total function to the pre-existing type when it's being thought of as a bundle_section.

(Also, I know there are a bunch of coercions that implement to_total, but I found it hard to follow the chain to figure out what it was doing! It only takes 13 characters to write the definition, so it seems clearer to just write it.)

[Kyle Miller]

How did the original lift work? The confusing thing to me is that total_space is semireducible, so I would have thought typeclass resolution wouldn't have found the has_coe_to_sigma instance.

[Nicolò Cavalleri]

Kyle Miller said:

I haven't taken any time to understand what's going on, but I did find this fix:

instance : has_lift (continuous_bundle_section' E) (bundle_section' E) :=
⟨continuous_bundle_section'.to_fun⟩

-- works
@[continuity] lemma continuous' : continuous (↑(↑s : bundle_section' E) : B → total_space E) :=
s.continuous_to_fun

-- works, too
@[continuity] lemma continuous'' : continuous (↑s : B → total_space E) := s.continuous_to_fun

Ok this is weird: why does it work as with has_lift but not with has_coe?

[Nicolò Cavalleri]

I might have found a solution for the coercion to work

[Nicolò Cavalleri]

Btw, lean#590 is ready for review!

[Nicolò Cavalleri]

reducible is behaving weirdly here. Are either simp or rw supposed to see through reducible defs?