Zulip Chat Archive

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