## Stream: general

### Topic: Reduction rule when declaring structure

#### Sebastien Gouezel (Jan 27 2020 at 08:50):

I am creating an instance of a structure with lets inside lets inside lets. I vaguely remember that I should declare an option to make sure that my definition will be reasonably flattened, but I don't remember its name.

#### Mario Carneiro (Jan 27 2020 at 08:52):

set_option eqn_compiler.zeta true?

#### Sebastien Gouezel (Jan 27 2020 at 08:55):

Maybe this is it. Except that I am not using the equation compiler, so maybe this is not needed. Here is my definition:

/-- The space of continuous multilinear maps on Ī (i : fin (n+1)), E i is canonically isomorphic to
the space of continuous linear maps from E 0 to the space of continuous multilinear maps on
Ī (i : fin n), E i.succ , by separating the first variable. We register this isomorphism in
linear_to_multilinear_equiv_multilinear_cont š E Eā. We build on the algebraic version (without
topology) given in linear_to_multilinear_equiv_multilinear š E Eā. -/
def linear_to_multilinear_equiv_multilinear_cont :
(E 0 āL[š] (continuous_multilinear_map š (Ī»(i : fin n), E i.succ) Eā)) āL[š]
(continuous_multilinear_map š E Eā) :=
-- first, register a linear equiv aux. Then, to check the continuity, it makes it possible to use
-- linear_map.continuous_of_bound
let aux : (E 0 āL[š] (continuous_multilinear_map š (Ī»(i : fin n), E i.succ) Eā)) āā[š]
(continuous_multilinear_map š E Eā) :=
{ to_fun  := Ī»f, (linear_to_multilinear_equiv_multilinear š E Eā
(continuous_multilinear_map.to_multilinear_map_linear.comp f.to_linear_map)).mk_continuous_of_bound
(ā„fā„) (Ī»m, continuous_multilinear_map.norm_image_tail_le f m),
add     := Ī»fā fā, by { ext m, refl },
smul    := Ī»c f, by { ext m, refl },
inv_fun := Ī»f,
let finv : (E 0 āā[š] (continuous_multilinear_map š (Ī»(i : fin n), E i.succ) Eā)) :=
{ -- define a linear map into n continuous multilinear maps from an n+1 continuous multilinear map
to_fun := Ī»x,
((linear_to_multilinear_equiv_multilinear š E Eā).symm
f.to_multilinear_map x).mk_continuous_of_bound (ā„fā„ * ā„xā„) (f.norm_image_cons_le x),
add    := Ī»x y, by { ext m, exact f.cons_add m x y },
smul   := Ī»c x, by { ext m, exact f.cons_smul m c x } }
in
-- the linear map finv is also continuous
{ cont := begin
refine linear_map.continuous_of_bound _ (ā„fā„) (Ī»x, _),
apply multilinear_map.mk_continuous_norm_le _ (mul_nonneg' (norm_nonneg _) (norm_nonneg _)),
end,
.. finv },
left_inv := Ī»f, begin
ext x m,
change f (cons x m 0) (tail (cons x m)) = f x m,
rw [cons_zero, tail_cons]
end,
right_inv := Ī»f, begin
ext m,
change f (cons (m 0) (tail m)) = f m,
rw cons_self_tail
end } in
-- now, create our continuous linear equiv, by using the fields of aux and adding continuity.
{ continuous_to_fun := begin
refine aux.to_linear_map.continuous_of_bound (1 : ā) (Ī»f, _),
rw one_mul,
apply continuous_multilinear_map.op_norm_le_bound _ (norm_nonneg _) (Ī»m, _),
apply continuous_multilinear_map.norm_image_tail_le f
end,
continuous_inv_fun := begin
refine aux.symm.to_linear_map.continuous_of_bound (1 : ā) (Ī»f, _),
rw one_mul,
apply continuous_linear_map.op_norm_le_bound _ (norm_nonneg _ ) (Ī»x, _),
apply continuous_multilinear_map.op_norm_le_bound _ ((mul_nonneg' (norm_nonneg _) (norm_nonneg _))) (Ī»m, _),
exact f.norm_image_cons_le x m
end,
.. aux }


#### Mario Carneiro (Jan 27 2020 at 08:56):

Have you considered not writing huge definitions with lets upon lets?

#### Mario Carneiro (Jan 27 2020 at 08:56):

there is no tax on auxiliary defs

#### Sebastien Gouezel (Jan 27 2020 at 08:57):

You mean, separating the aux in an auxiliary definition, whose only purpose would be to define linear_to_multilinear_equiv_multilinear_cont? Since it would never be used later on, what would be the interest?

#### Mario Carneiro (Jan 27 2020 at 08:58):

Well, I think you are about to create a new contender for the world's largest term tree again

#### Sebastien Gouezel (Jan 27 2020 at 08:58):

(Of course, when I did my definition, I did it in two steps as you advertise, to keep Lean reasonably reactive).

#### Mario Carneiro (Jan 27 2020 at 08:59):

I don't think inlining like this is actually good for lean

#### Sebastien Gouezel (Jan 27 2020 at 08:59):

OK, I will split it then.

#### Mario Carneiro (Jan 27 2020 at 09:00):

One reason you might want to keep an auxiliary def is if you ever want to inspect this definition later (prove some theorem about it, which is usually the case for defs) all of this stuff will explode on you

#### Sebastien Gouezel (Jan 27 2020 at 09:00):

Still, is there some option to tell Lean to flatten the definition of linear_to_multilinear_equiv_multilinear_cont (or is it a better idea to keep it unflattened?)

#### Mario Carneiro (Jan 27 2020 at 09:00):

with an auxiliary you can unfold stuff one at a time

#### Mario Carneiro (Jan 27 2020 at 09:01):

I don't think there are many options for changing the definition between the elaborator and the kernel

#### Sebastien Gouezel (Jan 27 2020 at 09:02):

Everything in there is Prop, except for the actual definition (when one applies things to objects) which is completely trivial and for which I register a simp lemma right after the definition, of course.

#### Mario Carneiro (Jan 27 2020 at 09:02):

most of it is out of your control, meaning you have to use tactics if you want what you write to not reflect the actual output

#### Mario Carneiro (Jan 27 2020 at 09:02):

lean automatically creates auxiliary defs for props inside defs

#### Mario Carneiro (Jan 27 2020 at 09:03):

eqn_compiler.zeta affects how those auxiliaries are stated

#### Mario Carneiro (Jan 27 2020 at 09:03):

The easiest way to find out if a planned optimization happened is to look at the #print on the result

#### Sebastien Gouezel (Jan 27 2020 at 09:06):

The output of #print ends with nice dots like

ā¦
ā¦
ā¦
ā¦
ā¦
ā¦
ā¦
ā¦
ā¦
ā¦
ā¦
ā¦)
ā¦
ā¦


#### Johan Commelin (Jan 27 2020 at 09:08):

Have you considered not writing huge definitions with lets upon lets?

Aaaaah, you're spoiling all our fun :oops:

#### Mario Carneiro (Jan 27 2020 at 09:11):

if you want, you can see more letters and less dots (well, probably even more dots) by increasing pp.max_steps

#### Mario Carneiro (Jan 27 2020 at 09:11):

but that's probably a bad sign

#### Sebastien Gouezel (Jan 27 2020 at 09:12):

The next lemma is

set_option class.instance_max_depth 352

@[simp] lemma linear_to_multilinear_equiv_multilinear_cont_apply
(f : E 0 āL[š] (continuous_multilinear_map š (Ī»(i : fin n), E i.succ) Eā))
(m : Ī (i : fin n.succ), E i) :
linear_to_multilinear_equiv_multilinear_cont š E Eā f m = f (m 0) (tail m) := rfl


and yes, 351 is not enough :-)

#### Johan Commelin (Jan 27 2020 at 09:12):

I guess my computer would have punched me in my stomach around 253...

#### Sebastien Gouezel (Jan 27 2020 at 09:13):

It's extremely quick though. But there are a lot of coercions in there...

#### Kevin Buzzard (Jan 27 2020 at 11:00):

You mean, separating the aux in an auxiliary definition, whose only purpose would be to define linear_to_multilinear_equiv_multilinear_cont? Since it would never be used later on, what would be the interest?

I think there are several other occasions in the library where auxiliary definitions are made and never used again. Isn't there some module_aux and maybe some metric or topological or uniform space aux def too?

#### Mario Carneiro (Jan 27 2020 at 11:00):

If you search for *_aux you will find lots of examples

Last updated: Dec 20 2023 at 11:08 UTC