elaboration issue challenge

Stream: general

[Patrick Massot]

I have a great new elaboration issue for the most experts users of this distinguished place. The only bad point is it's not minimized. In order to play, you need to leanproject get mathlib:sgouezel_multilinear, then code mathlib_sgouezel_multilinear and open analysis/normed_space/multilinear and go to line 247. Have a quick look at the statement of the next lemma, and take the firm decision to fix that ugly string of underscores.

Now, before that lemma, end the multilinear_map namespace, and paste the following section:

section
--set_option pp.implicit true
lemma  multilinear_map.restr_norm_le {k n : ℕ} (f : multilinear_map 𝕜 (λ i : fin n, G) E₂)
  (s : finset (fin n)) (hk : s.card = k) (z : G) {C : ℝ}
  (H : ∀ m, ∥f m∥ ≤ C * finset.univ.prod (λi, ∥m i∥)) (v : fin k → G) :
∥f.restr  s hk z v∥ ≤ C * ∥z∥ ^ (n - k) * finset.univ.prod (λi, ∥v i∥)  :=
begin
sorry
end

variables {k : ℕ} (f : multilinear_map 𝕜 (λ i : fin n, G) E₂)
  (s : finset (fin n)) (hk : s.card = k) (z : G) {C : ℝ}
  (H : ∀ m, ∥f m∥ ≤ C * finset.univ.prod (λi, ∥m i∥)) (v : fin k → G)
include H

lemma multilinear_map.restr_norm_le' : ∥f.restr  s hk z v∥ ≤ C * ∥z∥ ^ (n - k) * finset.univ.prod (λi, ∥v i∥)
 :=
begin
  sorry
end
end

[Patrick Massot]

Note how the first statement is rejected, and the second one is accepted.

[Patrick Massot]

On surface level, the only difference is the second lemma has all arguments passed as variables.

[Patrick Massot]

Now un-comment the set_option line, replace the first statement by sorry and spot the differences in context.

[Patrick Massot]

Did you get it? It's in the [∀i, add_comm_group (M₁ i)] argument to multilinear_map. Here M₁ is the constant function from fin n to Type with value G.

[Patrick Massot]

When it works, the inferred instance features boring naked G. In the failing case you'll see (λ (i : fin n), G) i.

[Patrick Massot]

Now the challenge is to explain the issue, and PR a fix to Lean 3.7.3.

[Patrick Massot]

Let me ping @Sebastien Gouezel since this happens in his PR.

[Kevin Buzzard]

Is it documented that leanproject get mathlib:sgouezel_multilinear works to get a mathlib branch? I hadn't realised this, I've been getting mathlib and then switching branches and getting the oleans. This way is much cooler :-)

[Kevin Buzzard]

So the failure gives the error

type mismatch at application
  multilinear_map.restr f
term
  f
has type
  multilinear_map 𝕜 (λ (i : fin n), G) E₂ : Type (max wG w₂)
but is expected to have type
  multilinear_map ?m_1 (λ (i : fin ?m_2), ?m_3) ?m_4 : Type (max ? ?)

which is the kind of frustrating error which one sees occasionally, because clearly one can solve for the metavariables. Are you saying that you might be able to understand this failure and perhaps the prettyprinter is lying to us?

[Patrick Massot]

Kevin Buzzard said:

Is it documented that leanproject get mathlib:sgouezel_multilinear works to get a mathlib branch? I hadn't realised this, I've been getting mathlib and then switching branches and getting the oleans. This way is much cooler :-)

Yes, last paragraph of "Getting an existing Lean project" at https://github.com/leanprover-community/mathlib-tools/blob/master/README.md#getting-an-existing-lean-project

[Patrick Massot]

Elaboration fails to fill in metavariables presumably because it fails some class instance search, because there is application which is not random.choice(['alpha', 'beta', 'gamma', 'delta', 'zeta'])-reduced.

[Johan Commelin]

Aren't you missing eta?

[Patrick Massot]

Do you think it's eta? Doesn't sound likely to my ear :grinning:

[Johan Commelin]

https://en.wikipedia.org/wiki/Lambda_calculus#Reduction

[Patrick Massot]

Wikipedia says beta

[Patrick Massot]

Johan was looking there too :)

[Johan Commelin]

Ooh, I was just complaining that your Russian roulette was missing out on some options.

[Patrick Massot]

I know.

[Patrick Massot]

We should have a general purpose Zulip shortcut to insert random.choice(['alpha', 'beta', 'gamma', 'delta', 'eta' 'zeta'])

[Patrick Massot]

In the mean time, I hope some expert will have a look, or at least @Sebastian Ullrich will post his standard: "this is fixed in Lean 4" message.

[Patrick Massot]

@Sebastien Gouezel it's a bit sad no expert seems to have anything to say here, but I still recommend you but the multilinear map in a variable (you can leave everything else in the lemma), and have the nice statement.

[Gabriel Ebner]

Since you're calling the experts, I can give you one more workaround:

lemma  multilinear_map.restr_norm_le {k : ℕ} (f : (multilinear_map 𝕜 (λ i : fin n, G) E₂ : _))
  (s : finset (fin n)) (hk : s.card = k) (z : G) {C : ℝ}
  (H : ∀ m, ∥f m∥ ≤ C * finset.univ.prod (λi, ∥m i∥)) (v : fin k → G) :
∥f.restr  s hk z v∥ ≤ C * ∥z∥ ^ (n - k) * finset.univ.prod (λi, ∥v i∥)  :=
begin
sorry
end

[Gabriel Ebner]

I assume that is also the elaboration difference between variables and arguments: types of variables are apparently elaborated without expected type, but arguments are elaborated with expected type Sort*.

[Patrick Massot]

Thanks Gabriel!

[Patrick Massot]

Sébastien, did you see that?

[Kevin Buzzard]

If we went through Lean's library and replaced every (a : A) function input with (a : (A : _)) would anything break?

[Mario Carneiro]

it seems unlikely, but lean works in mysterious ways

[Sebastian Ullrich]

In Lean 4, there will actually be no difference between variables and regular parameters, because the former are simply macros and are re-elaborated inside each declaration that uses them.

[Kevin Buzzard]

Here is a version which uses only mathlib master and uses much less of it:

import analysis.normed_space.basic

variables

{𝕜 : Type}
[nondiscrete_normed_field 𝕜]
{G : Type}
[normed_group G]
[normed_space 𝕜 G]
{I J : Type}

structure mm (R : Type) [ring R] (I : Type) (M₁ : I → Type) [∀ i  : I, add_comm_group (M₁ i)]
[∀ i : I, module R (M₁ i)]
.

-- M' is implicit and we will show that Lean can't guess it below
def mmrest (R : Type) [ring R] {M' : Type} [add_comm_group M'] [module R M'] (I : Type)
  (F : mm R I (λ i : I, M')) : mm R I (λ j : I, M') := F

variables (F : mm 𝕜 I (λ i : I, G))

-- works fine
lemma restr_norm_le : mmrest 𝕜 I F = mmrest 𝕜 I F := rfl

-- also works
lemma restr_norm_le' (F : (mm 𝕜 I (λ i : I, G))) :
@mmrest 𝕜 _ G _ _  I F = mmrest 𝕜 I F := by refl -- removing G makes it fail

-- Lean can't guess G
lemma restr_norm_le'' (F : (mm 𝕜 I (λ i : I, G))) :
mmrest 𝕜 I F = mmrest 𝕜 I F := by refl -- fails

/-
type mismatch at application
  mmrest 𝕜 I F
term
  F
has type
  mm 𝕜 I (λ (i : I), G)
but is expected to have type
  mm 𝕜 I (λ (i : I), ?m_1)
-/

[Kevin Buzzard]

Lean is failing to infer G from (λ i : I, G)

[Kevin Buzzard]

When it succeeds. F has type

F :
  @mm 𝕜
    (@normed_ring.to_ring 𝕜
       (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))
    I
    (λ (i : I), G)
    (λ (i : I), @normed_group.to_add_comm_group G _inst_2)
    (λ (i : I),
       @normed_space.to_module 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1) _inst_2 _inst_3)

and when it fails, it has the defeq type

  @mm 𝕜
    (@normed_ring.to_ring 𝕜
       (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))
    I
    (λ (i : I), G)
    (λ (i : I), @normed_group.to_add_comm_group ((λ (i : I), G) i) _inst_2)
    (λ (i : I),
       @normed_space.to_module 𝕜 ((λ (i : I), G) i) (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1) _inst_2
         _inst_3)

[Gabriel Ebner]

The issue lies in unification: we need to solve ?m1 =?= (fun x, G) i where ?m1 may not contain i.

[Kevin Buzzard]

How about ?m1=G?

[Sebastien Gouezel]

I have fixed the PR following @Gabriel Ebner 's advice. Thanks Gabriel!

[Kevin Buzzard]

Another fix would be to make the implicit variable explicit -- the one which unification can't guess.

[Kevin Buzzard]

You are asking Lean to guess G from (f : multilinear_map 𝕜 (λ i : fin n, G) E₂)` and perhaps we learn here that it is not always capable of such guesses.

[Gabriel Ebner]

Kevin Buzzard said:

How about ?m1=G?

This is exactly the solution that we would like, in this case. So you say, "how about we just beta-reduce the right-hand side whenever we assign a meta-variable"? And in this case, it would work. However changes in the unifier have the unfortunate habit of breaking things elsewhere in unexpected places. Since it is not 100% clear to me that this the right behavior, I'm not too eager to change the unifier unless this problem pops up more often.

[Kevin Buzzard]

I see!

[Patrick Stevens]

Forgive the noob question, but this made me think about a problem I encountered earlier today: is it possible to manually assign a metavariable? If I have m1 in scope in a goal, can I specify m1 somehow without having to track down where exactly the metavariable arose?

[Johan Commelin]

It means that you'll have multiple goals.

[Johan Commelin]

So you can use swap 4 to jump to goal number 4. And use exact foobar close it.

[Johan Commelin]

You will have to figure out manually which goal corresponds to ?m1

[Kevin Buzzard]

I think that in general you might want to try and avoid metavariables in goals. Usually when one appears for me, I instantly stomp on it by changing the line which created it. It is often not hard to do this, it is usually an _ which just needed to be filled in explicitly. Having metavariables around can actually mess you up, some tactics can get confused for example.