Zulip Chat Archive

Stream: general

Topic: old_structure_cmd

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

Johan Commelin (Apr 05 2019 at 17:50):

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

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

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

Mario Carneiro (Apr 05 2019 at 18:15):

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

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

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

Mario Carneiro (Apr 05 2019 at 18:20):

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

Johan Commelin (Apr 05 2019 at 18:21):

But my example has a parent (-;

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.

Johan Commelin (Apr 05 2019 at 18:24):

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

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?

Johan Commelin (Apr 05 2019 at 19:21):

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

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

Kenny Lau (May 28 2020 at 22:25):

what exactly does set_option old_structure_cmd true do?

Kenny Lau (May 28 2020 at 22:25):

I can't find this in the mathlib docs

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]
-/

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

Kenny Lau (May 28 2020 at 22:28):

e.g. when there are diamonds

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.

Kenny Lau (May 28 2020 at 22:29):

thanks

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

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

Mario Carneiro (May 28 2020 at 22:32):

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

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⟩

Jeremy Avigad (May 28 2020 at 22:35):

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

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

Kenny Lau (May 28 2020 at 22:50):

at least those without is_

Kenny Lau (May 28 2020 at 22:52):

but then they would be very slow

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

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

Mario Carneiro (May 28 2020 at 22:55):

the real killer in mathlib is the constant typeclass inference

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.

Kenny Lau (May 28 2020 at 22:56):

yeah... but the new approach generates diamond problems

Kenny Lau (May 28 2020 at 22:56):

because things are not defeq anymore

Mario Carneiro (May 28 2020 at 22:56):

the new approach solves diamond problems by giving an error

Mario Carneiro (May 28 2020 at 22:56):

you just can't do it

Kenny Lau (May 28 2020 at 22:56):

here's the real use case

Mario Carneiro (May 28 2020 at 22:57):

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

Kenny Lau (May 28 2020 at 22:57):

euclidean_domain extends comm_ring (it used to extend nonzero_comm_ring)

Kenny Lau (May 28 2020 at 22:57):

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

Kenny Lau (May 28 2020 at 22:57):

so you get two paths to comm_ring that are not defeq

Kenny Lau (May 28 2020 at 22:57):

euclidean_domain uses the new approach

Kenny Lau (May 28 2020 at 22:57):

while integral_domain uses the old approach

Kenny Lau (May 28 2020 at 22:57):

what should I do?

Mario Carneiro (May 28 2020 at 22:57):

make it an old structure

Kenny Lau (May 28 2020 at 22:58):

aha

Kenny Lau (May 28 2020 at 22:58):

alright

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

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)

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

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

Kenny Lau (May 28 2020 at 22:59):

but the problem is that ideal uses comm_ring itself

Kenny Lau (May 28 2020 at 22:59):

it used to not matter because there is nonzero_comm_ring in between

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

Kenny Lau (May 28 2020 at 23:05):

(which has oleans ready)

Chris Hughes (May 28 2020 at 23:06):

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

Kenny Lau (May 28 2020 at 23:07):

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

Kenny Lau (May 28 2020 at 23:07):

the rw error arises when I use old structure command

Kenny Lau (May 28 2020 at 23:07):

which is currently not enabled

Chris Hughes (May 28 2020 at 23:08):

Because. old_structure_cnd will ad euclidean_domain.mul_comm to the environment

Kenny Lau (May 28 2020 at 23:08):

right

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.

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

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

Chris Hughes (May 28 2020 at 23:15):

What are the other problems?

Kenny Lau (May 28 2020 at 23:18):

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

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

Kevin Buzzard (May 28 2020 at 23:23):

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

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

Kenny Lau (May 29 2020 at 05:49):

then what should i do?

Chris Hughes (May 29 2020 at 06:00):

Use old_structure_cmd

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

Kenny Lau (May 29 2020 at 07:15):

as a result one should not open euclidean_domain now

Kenny Lau (May 29 2020 at 07:16):

aha

Kenny Lau (May 29 2020 at 07:17):

or I should make everything protected

Kenny Lau (May 29 2020 at 07:21):

how does set_env work? I thought it cannot change anything

Kenny Lau (May 29 2020 at 07:21):

or is that limited to new declarations

Chris Hughes (May 29 2020 at 08:40):

#2855 gives you an attribute to protect the projections

Kenny Lau (May 29 2020 at 08:41):

oh thanks!

Kenny Lau (May 29 2020 at 08:42):

but some projections might not need to be protected

Kenny Lau (May 29 2020 at 08:42):

this is what I do currently for euclidean_domain:

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