Zulip Chat Archive

Stream: general

Topic: old_structure_cmd


view this post on Zulip Johan Commelin (Apr 05 2019 at 17:50):

I have

structure TopCommRing :=
(α : Type u)
[cr : comm_ring α]
[ts : topological_space α]
[tr : topological_ring α]

and

section uniform
local attribute [instance] topological_add_group.to_uniform_space

structure CmplTopCommRing extends TopCommRing.{u} :=
[cs : complete_space α]
[sp : separated α]

end uniform

view this post on Zulip Johan Commelin (Apr 05 2019 at 17:50):

Should I use the old_structure_cmd or not? What are the pros and cons?

view this post on Zulip Mario Carneiro (Apr 05 2019 at 18:13):

I will say this: old_structure_cmd is not deprecated. The name is really unfortunate, and it should be something more like flat_structure

view this post on Zulip Mario Carneiro (Apr 05 2019 at 18:15):

old_structure_cmd will lay out a structure as a bunch of fields, inlining all fields of the parent(s). It then constructs "parent coercions" (also a bad name, it's an instance not a coercion) so that you can infer parents from the children

view this post on Zulip Mario Carneiro (Apr 05 2019 at 18:15):

This can get expensive, especially for deep hierarchies or structures with many fields

view this post on Zulip Mario Carneiro (Apr 05 2019 at 18:17):

The "new structure cmd" (aka the default) is to use a "nested" layout, where a structure B extends A contains a field to_A that allows access to all the fields of A. Some magic is then done so you can't tell the difference, but the parent coercions are now a lot simpler to define

view this post on Zulip Mario Carneiro (Apr 05 2019 at 18:19):

The major downside of the new structure cmd is that you can't nest two structures with a common field, at least not if you don't want two copies of the field as data (and they can potentially be different, and bad things can happen). To avoid this, diamonds are just plain rejected. So structure foo extends add_comm_group A, ring A is rejected

view this post on Zulip Mario Carneiro (Apr 05 2019 at 18:20):

For a structure without parents, I don't think it makes a difference which you use

view this post on Zulip Johan Commelin (Apr 05 2019 at 18:21):

But my example has a parent (-;

view this post on Zulip Johan Commelin (Apr 05 2019 at 18:23):

In the end, I want to put a category structure on both, get the induced forgetful functor, etc...
This all goes quite smoothly.
Now, what I would like is if I have an type R and it turns out to have instances of complete_space and topological_ring etc... that I can just write
{ \alpha := R } for the object of CmplTopCommRing and that type class inference figures out the other fields of the structure.

view this post on Zulip Johan Commelin (Apr 05 2019 at 18:24):

Does that affect my choice for old/flat vs new/nested structures?

view this post on Zulip Johan Commelin (Apr 05 2019 at 19:20):

@Mario Carneiro Why are flat structures expensive if you have deep hierarchies? As in, why more expensive then nested structures?

view this post on Zulip Johan Commelin (Apr 05 2019 at 19:21):

Are all the "grandparent coercions" also inlined into the flat structure? Is that the issue?

view this post on Zulip Mario Carneiro (Apr 05 2019 at 19:39):

Yes, all transitive parent fields are pulled in. I think leo had examples like decidable_linear_ordered_field or something which were one line to write but just massive under the hood

view this post on Zulip Kenny Lau (May 28 2020 at 22:25):

what exactly does set_option old_structure_cmd true do?

view this post on Zulip Kenny Lau (May 28 2020 at 22:25):

I can't find this in the mathlib docs

view this post on Zulip Kenny Lau (May 28 2020 at 22:27):

one thing I observed is this:

set_option old_structure_cmd true

class A (n : ) :=
(A : )

class B (n : ) extends A n :=
(B : )

#print B.to_A
/-
@[instance]
def B.to_A : Π (n : ℕ) [s : B n], A n :=
λ (n : ℕ) [s : B n], {A := B.A n s}
-/

set_option old_structure_cmd false

class C (n : ) :=
(C : )

class D (n : ) extends C n :=
(D : )

#print D.to_C
/-
@[instance, reducible]
def D.to_C : Π {n : ℕ} [c : D n], C n :=
λ (n : ℕ) [c : D n], [D.to_C c]
-/

view this post on Zulip Kenny Lau (May 28 2020 at 22:28):

the latter one is problematic because it might cause things that should be defeq to not be defeq

view this post on Zulip Kenny Lau (May 28 2020 at 22:28):

e.g. when there are diamonds

view this post on Zulip Jeremy Avigad (May 28 2020 at 22:28):

This is core Lean. The original Lean 3 encoding of structures stored all the fields flat, and a structure could extend and combine as many structures as you want. At some point, Leo determined that the multiple inheritance and diamonds were causing efficiency problems, and changed the representation, making it harder to have inheritance diamonds. (You could still define them by hand, but extends doesn't allow it.) This option restores the old behavior, which is sometimes convenient, though it potentially causes inefficiencies.

view this post on Zulip Kenny Lau (May 28 2020 at 22:29):

thanks

view this post on Zulip Kenny Lau (May 28 2020 at 22:30):

however the old_strcuture_cmd is not a panacea either, as demonstrated by this example:

set_option old_structure_cmd true

class A (n : ) :=
(A : )

class B (n : ) [A n] :=
(B : )

class C (n : ) extends A n, B n. -- failed to add declaration to environment, it contains local constants

view this post on Zulip Mario Carneiro (May 28 2020 at 22:32):

Note that you can replicate the behavior of old_structure_cmd by hand, by inlining all the fields of the parents

view this post on Zulip Mario Carneiro (May 28 2020 at 22:32):

The whole reason the @[ancestor] attribute exists is because these are indistinguishable by later things

view this post on Zulip Mario Carneiro (May 28 2020 at 22:34):

set_option old_structure_cmd true

class A (n : ) :=
(A : )

class B (n : ) [A n] :=
(B : )

class C (n : ) extends A n :=
(B : )

instance C.to_B (n) [A n] [B n] : C n := A.A n, B.B n

view this post on Zulip Jeremy Avigad (May 28 2020 at 22:35):

Leo wrote this before making the switch: https://github.com/leanprover/lean/wiki/Refactoring-structures.

view this post on Zulip Kenny Lau (May 28 2020 at 22:50):

looks like I should just set_option old_structure_cmd true for everything in the algebra hierarchy

view this post on Zulip Kenny Lau (May 28 2020 at 22:50):

at least those without is_

view this post on Zulip Kenny Lau (May 28 2020 at 22:52):

but then they would be very slow

view this post on Zulip Mario Carneiro (May 28 2020 at 22:53):

I hesitate to give any blanket rule here, but it is true that most types in the algebraic hierarchy use old_structure_cmd

view this post on Zulip Mario Carneiro (May 28 2020 at 22:54):

I think that the speed issue that leo was worried about is not the major concern, because it deals with the cost of elaborating a new class declaration, which is relatively rare. Even structure literals are pretty rare in mathlib

view this post on Zulip Mario Carneiro (May 28 2020 at 22:55):

the real killer in mathlib is the constant typeclass inference

view this post on Zulip Mario Carneiro (May 28 2020 at 22:55):

which makes this quote especially terrifying:

Another potential problem is performance: theory_ac.cpp generates many type class resolution problems. It generates at least one for every subterm of the form f a b. I'm not sure how expensive it will be. The simplifier also generates a lot of type class resolution problems.

view this post on Zulip Kenny Lau (May 28 2020 at 22:56):

yeah... but the new approach generates diamond problems

view this post on Zulip Kenny Lau (May 28 2020 at 22:56):

because things are not defeq anymore

view this post on Zulip Mario Carneiro (May 28 2020 at 22:56):

the new approach solves diamond problems by giving an error

view this post on Zulip Mario Carneiro (May 28 2020 at 22:56):

you just can't do it

view this post on Zulip Kenny Lau (May 28 2020 at 22:56):

here's the real use case

view this post on Zulip Mario Carneiro (May 28 2020 at 22:57):

which is a non-solution for all the stuff in the algebraic hierarchy

view this post on Zulip Kenny Lau (May 28 2020 at 22:57):

euclidean_domain extends comm_ring (it used to extend nonzero_comm_ring)

view this post on Zulip Kenny Lau (May 28 2020 at 22:57):

and there is an instance that every euclidean domain is an integral domain

view this post on Zulip Kenny Lau (May 28 2020 at 22:57):

so you get two paths to comm_ring that are not defeq

view this post on Zulip Kenny Lau (May 28 2020 at 22:57):

euclidean_domain uses the new approach

view this post on Zulip Kenny Lau (May 28 2020 at 22:57):

while integral_domain uses the old approach

view this post on Zulip Kenny Lau (May 28 2020 at 22:57):

what should I do?

view this post on Zulip Mario Carneiro (May 28 2020 at 22:57):

make it an old structure

view this post on Zulip Kenny Lau (May 28 2020 at 22:58):

aha

view this post on Zulip Kenny Lau (May 28 2020 at 22:58):

alright

view this post on Zulip Mario Carneiro (May 28 2020 at 22:58):

actually now that I come to think about it I'm not sure that's actually a problem

view this post on Zulip Kenny Lau (May 28 2020 at 22:59):

but now rw cannot find

@has_add.add.{u} α
    (@distrib.to_has_add.{u} α
       (@ring.to_distrib.{u} α (@comm_ring.to_ring.{u} α (@euclidean_domain.to_comm_ring.{u} α _inst_1))))
    (@has_mul.mul.{u} α
       (@mul_zero_class.to_has_mul.{u} α
          (@semiring.to_mul_zero_class.{u} α
             (@ring.to_semiring.{u} α (@comm_ring.to_ring.{u} α (@euclidean_domain.to_comm_ring.{u} α _inst_1)))))
       a
       s)
    (@has_mul.mul.{u} α
       (@mul_zero_class.to_has_mul.{u} α
          (@semiring.to_mul_zero_class.{u} α
             (@ring.to_semiring.{u} α (@comm_ring.to_ring.{u} α (@euclidean_domain.to_comm_ring.{u} α _inst_1)))))
       b
       t)

(which is a * s + b * t)
inside

(@has_add.add.{u} α
             (@distrib.to_has_add.{u} α
                (@ring.to_distrib.{u} α (@comm_ring.to_ring.{u} α (@euclidean_domain.to_comm_ring.{u} α _inst_1))))
             (@has_mul.mul.{u} α (@has_mul.mk.{u} α (@euclidean_domain.mul.{u} α _inst_1)) a s)
             (@has_mul.mul.{u} α (@has_mul.mk.{u} α (@euclidean_domain.mul.{u} α _inst_1)) b t)

view this post on Zulip Kenny Lau (May 28 2020 at 22:59):

Mario Carneiro said:

actually now that I come to think about it I'm not sure that's actually a problem

I get synthesized error

view this post on Zulip Mario Carneiro (May 28 2020 at 22:59):

it's true that the two paths to comm_ring are not defeq, but that doesn't matter, what matters is that all projections out of comm_ring are defeq regardless of the path

view this post on Zulip Kenny Lau (May 28 2020 at 22:59):

but the problem is that ideal uses comm_ring itself

view this post on Zulip Kenny Lau (May 28 2020 at 22:59):

it used to not matter because there is nonzero_comm_ring in between

view this post on Zulip Kenny Lau (May 28 2020 at 23:05):

@Mario Carneiro you can actually see the error itself in vivo in src/ring_theory/principal_ideal_domain.lean in the nonzero branch

view this post on Zulip Kenny Lau (May 28 2020 at 23:05):

(which has oleans ready)

view this post on Zulip Chris Hughes (May 28 2020 at 23:06):

Is the rw using euclidean_domain.mul_comm or something? I remember this causing problems

view this post on Zulip Kenny Lau (May 28 2020 at 23:07):

as in, the error caused by the two paths not being defeq

view this post on Zulip Kenny Lau (May 28 2020 at 23:07):

the rw error arises when I use old structure command

view this post on Zulip Kenny Lau (May 28 2020 at 23:07):

which is currently not enabled

view this post on Zulip Chris Hughes (May 28 2020 at 23:08):

Because. old_structure_cnd will ad euclidean_domain.mul_comm to the environment

view this post on Zulip Kenny Lau (May 28 2020 at 23:08):

right

view this post on Zulip Chris Hughes (May 28 2020 at 23:13):

You can protect lemmas after defying them now, so you can solve that problem if that was the problem.

view this post on Zulip Kenny Lau (May 28 2020 at 23:14):

the current problem is the two paths not being defeq because euclidean domain is using the new approach

view this post on Zulip Kenny Lau (May 28 2020 at 23:15):

and "just use the old approach" creates other problems which might or might not be solvable depending or not depending on lean#282

view this post on Zulip Chris Hughes (May 28 2020 at 23:15):

What are the other problems?

view this post on Zulip Kenny Lau (May 28 2020 at 23:18):

the rw problem not recognizing a * s + b * t

view this post on Zulip Chris Hughes (May 28 2020 at 23:21):

This command after the definition of euclidean domain solves the rw issue

run_cmd do env  tactic.get_env,
  tactic.set_env $ environment.mk_protected env ``euclidean_domain.mul_assoc

view this post on Zulip Kevin Buzzard (May 28 2020 at 23:23):

I am so proud of my undergraduates and their deep understanding of the system I love

view this post on Zulip Mario Carneiro (May 29 2020 at 00:23):

I think the two paths are actually defeq, but not defeq with instance reducibility, because it involves unfolding ideal to note that the definition only uses the various components of a ring and not the ring itself

view this post on Zulip Kenny Lau (May 29 2020 at 05:49):

then what should i do?

view this post on Zulip Chris Hughes (May 29 2020 at 06:00):

Use old_structure_cmd

view this post on Zulip Kenny Lau (May 29 2020 at 06:35):

I don't understand why making mul_assoc protected has anything to do with rw figuring out some patterns

view this post on Zulip Kenny Lau (May 29 2020 at 07:15):

as a result one should not open euclidean_domain now

view this post on Zulip Kenny Lau (May 29 2020 at 07:16):

aha

view this post on Zulip Kenny Lau (May 29 2020 at 07:17):

or I should make everything protected

view this post on Zulip Kenny Lau (May 29 2020 at 07:21):

how does set_env work? I thought it cannot change anything

view this post on Zulip Kenny Lau (May 29 2020 at 07:21):

or is that limited to new declarations

view this post on Zulip Chris Hughes (May 29 2020 at 08:40):

#2855 gives you an attribute to protect the projections

view this post on Zulip Kenny Lau (May 29 2020 at 08:41):

oh thanks!

view this post on Zulip Kenny Lau (May 29 2020 at 08:42):

but some projections might not need to be protected

view this post on Zulip Kenny Lau (May 29 2020 at 08:42):

this is what I do currently for euclidean_domain:

view this post on Zulip Kenny Lau (May 29 2020 at 08:43):

https://github.com/leanprover-community/mathlib/blob/396edbf68a450118a6c880c59943a8bd9c395ba5/src/algebra/euclidean_domain.lean#L36-L54

run_cmd do env  tactic.get_env,
  let env := env.mk_protected ``euclidean_domain.add,
  let env := env.mk_protected ``euclidean_domain.add_assoc,
  let env := env.mk_protected ``euclidean_domain.zero,
  let env := env.mk_protected ``euclidean_domain.zero_add,
  let env := env.mk_protected ``euclidean_domain.add_zero,
  let env := env.mk_protected ``euclidean_domain.neg,
  let env := env.mk_protected ``euclidean_domain.add_left_neg,
  let env := env.mk_protected ``euclidean_domain.add_comm,
  let env := env.mk_protected ``euclidean_domain.mul,
  let env := env.mk_protected ``euclidean_domain.mul_assoc,
  let env := env.mk_protected ``euclidean_domain.one,
  let env := env.mk_protected ``euclidean_domain.one_mul,
  let env := env.mk_protected ``euclidean_domain.mul_one,
  let env := env.mk_protected ``euclidean_domain.left_distrib,
  let env := env.mk_protected ``euclidean_domain.right_distrib,
  let env := env.mk_protected ``euclidean_domain.mul_comm,
  let env := env.mk_protected ``euclidean_domain.zero_ne_one,
  tactic.set_env env

view this post on Zulip Kenny Lau (May 29 2020 at 08:44):

as in, there's no need to make euclidean_domain.quotient protected

view this post on Zulip Kenny Lau (May 29 2020 at 08:44):

oh I guess there's a need

view this post on Zulip Kenny Lau (May 29 2020 at 08:44):

it coincides with the quotient for quotienting a setoid

view this post on Zulip Johan Commelin (May 29 2020 at 08:45):

Can we make fields of a structure/class protected by default?

view this post on Zulip Chris Hughes (May 29 2020 at 08:46):

I'm not sure there's a way to unprotect, that's the only trouble I can think of with that.

view this post on Zulip Johan Commelin (May 29 2020 at 08:50):

I see... we might want to protect at the end of the file that introduced the structure...

view this post on Zulip Mario Carneiro (May 29 2020 at 08:50):

here's hoping protected becomes an attribute at some point...

view this post on Zulip Chris Hughes (May 29 2020 at 10:35):

Mario Carneiro said:

here's hoping protected becomes an attribute at some point...

I added this to #2855

view this post on Zulip Johan Commelin (May 29 2020 at 10:58):

@Chris Hughes Wow, thanks for that PR!


Last updated: May 10 2021 at 18:22 UTC