R^m is finite dimensional over R

Stream: Is there code for X?

[Bhavik Mehta]

import data.real.basic
import linear_algebra.finite_dimensional

example {m : ℕ} : finite_dimensional ℝ (fin m → ℝ) :=
begin
  apply_instance
end

I presume I'm just missing imports, but which ones?

[Yakov Pechersky]

docs#is_noetherian_pi ?

[Bhavik Mehta]

import data.real.basic
import linear_algebra.finite_dimensional
import ring_theory.noetherian

example {m : ℕ} : finite_dimensional ℝ (fin m → ℝ) :=
begin
  apply_instance
end

Doesn't work

[Adam Topaz]

Is finite dimensional map even a class?

[Bhavik Mehta]

Most of the lemmas about it in linear_algebra.finite_dimensional take finite_dimensional K V as a typeclass argument, so I assume that's how it's meant to be used

[Adam Topaz]

Right. I got confused because the API docs just lists it as a def

[Bhavik Mehta]

import data.real.basic
import linear_algebra.finite_dimensional

example {m : ℕ} : finite_dimensional ℝ (fin m → ℝ) :=
@is_noetherian_pi _ _ _ _ _ _ _ (λ i, infer_instance)

This works but it's weird that there's no nicer way - why is it that I need to look at the implemention of finite_dimensional and look through noetherian lemmas to get a linear algebra result

[Adam Topaz]

Does it work if you replace fin n with a type with a Fintype instance?

[Adam Topaz]

I mean, it shouldn't. But might be worth checking anyway

[Bhavik Mehta]

Yup it doesn't work

[Adam Topaz]

Sounds like a missing instance :expressionless:

[Bhavik Mehta]

import data.real.basic
import linear_algebra.finite_dimensional

example {K : Type*} [field K] {i : ℕ} : finite_dimensional K (fin i → K) :=
begin
  apply_instance
end

But this works...

[Adam Topaz]

Oooh... The mystery deepens

[Shing Tak Lam]

Seems like local attribute [-instance] real.semiring real.ring "fixes" it and apply_instance works

import data.real.basic
import linear_algebra.finite_dimensional

local attribute [-instance] real.semiring real.ring

example {m : ℕ} : finite_dimensional ℝ (fin m → ℝ) := by apply_instance

[Shing Tak Lam]

Here's the original failure and the case for field K minimised

import data.real.basic
import linear_algebra.finite_dimensional

-- These both find `finite_dimensional.finite_dimensional_self`
example {K : Type*} [field K] (m : ℕ) : ∀ (i : fin m), is_noetherian K K :=
  by show_term {apply_instance}
example (m : ℕ) : ∀ (i : fin m), finite_dimensional ℝ ℝ :=
  by show_term {apply_instance}

-- But this fails
example (m : ℕ) : ∀ (i : fin m), is_noetherian ℝ ℝ := by apply_instance

If I turn on set_option pp.all, the goal for finite_dimensional ℝ ℝ is like so

@finite_dimensional.{0 0} real real real.field real.add_comm_group
    (@semiring.to_semimodule.{0} real
       (@ring.to_semiring.{0} real (@division_ring.to_ring.{0} real (@field.to_division_ring.{0} real real.field))))

and for is_noetherian ℝ ℝ it's

@is_noetherian.{0 0} real real real.semiring real.add_comm_monoid (@semiring.to_semimodule.{0} real real.semiring)

and as the instance it found for finite_dimensional ℝ ℝ uses a finite_dimensional lemma, and not a is_noetherian lemma, I guessed that maybe the short circuit instances are causing issues, so I added local attribute [-instance] real.semiring real.ring and then the instance search worked.

[Alex J. Best]

Just getting rid of real.ring is enough even

[Mario Carneiro]

hm, this works:

example (m : ℕ) (i : fin m) : is_noetherian ℝ ℝ := by apply_instance

[Mario Carneiro]

The only difference:

[class_instances] (0) ?x_0 i :
  @is_noetherian ℝ ℝ real.semiring real.add_comm_monoid (@semiring.to_semimodule ℝ real.semiring) :=
  @finite_dimensional.finite_dimensional_self (?x_42 i) (?x_43 i)
failed is_def_eq

vs

[class_instances] (0) ?x_0 :
  @is_noetherian ℝ ℝ real.semiring real.add_comm_monoid (@semiring.to_semimodule ℝ real.semiring) :=
  @finite_dimensional.finite_dimensional_self ?x_42 ?x_43
(works)

[Bhavik Mehta]

So what's the fix in mathlib? Or should I be saying local attribute [-instance] real.ring

[Bhavik Mehta]

Alright, now I've additionally used the import analysis.convex.topology and the local attribute fixes no longer work:

import data.real.basic
import linear_algebra.finite_dimensional
import analysis.convex.topology

local attribute [-instance] real.semiring real.ring

example {m : ℕ} : finite_dimensional ℝ (fin m → ℝ) :=
begin
  apply_instance
end

What am I meant to do with this now?

[Yakov Pechersky]

local attribute [-instance] real.nondiscrete_normed_field real.normed_field real.semiring real.ring

[Yakov Pechersky]

I think there's probably an issue somewhere with is_R_or_C

[Yakov Pechersky]

Ah. It might have to do with real.linear_ordered_field

[Bhavik Mehta]

It's so bizarre to me that mathlib is set up so that I can't show R^m is finite dimensional out of the box!

[Yakov Pechersky]

I don't know enough about diamond discovery to figure out what's wrong here, will have to wait for the real sleuths

[Bryan Gin-ge Chen]

Whatever is going on, I doubt the troubles you're having here are intentional. Something needs to be fixed; maybe some instances need to be put in locales?

[Mario Carneiro]

yeah, those local attribute [-instance] lines are definitely not a proper solution. It looks like a lean bug

[Mario Carneiro]

For a mathlib workaround, you can just declare instance {m : ℕ} : finite_dimensional ℝ (fin m → ℝ)

[Patrick Massot]

It seems this issue is still not solved in mathlib master. I think this is a very serious issue. @Mario Carneiro are you suggesting we put

import data.real.basic
import linear_algebra.finite_dimensional

instance {m : ℕ} : finite_dimensional ℝ (fin m → ℝ) :=
@is_noetherian_pi ℝ _ _ _ _ _ _ (λ i, finite_dimensional.finite_dimensional_self _)

somewhere? It feels like the underlying issue will get more opportunities to strike elsewhere if we ignore it.

[Mario Carneiro]

I don't think it's a great solution but it should help for the time being

[Mario Carneiro]

I don't know what's wrong in lean and I'm not especially motivated to try to patch typeclass inference

[Johan Commelin]

If we add the instance, we should probably replace fin m by an arbitrary fintype.

[Eric Wieser]

This works:

/-- non-dependent version of `is_noetherian_pi` -/
instance is_noetherian_pi' {R ι : Type*} {M : Type*} [ring R]
  [add_comm_group M] [semimodule R M] [fintype ι]
  [is_noetherian R M] : is_noetherian R (ι → M) :=
is_noetherian_pi

[Eric Wieser]

Then apply_instance can close the original goal

[Johan Commelin]

Did you check that it closes the original goal?

[Johan Commelin]

Because this thread seems to show that it doesn't always work as expected...

[Eric Wieser]

Huh, I guess I screwed up

[Eric Wieser]

Yes, it does:

import data.real.basic
import linear_algebra.finite_dimensional

/-- non-dependent version of `is_noetherian_pi` -/
instance is_noetherian_pi' {R ι : Type*} {M : Type*} [ring R]
  [add_comm_group M] [semimodule R M] [fintype ι]
  [is_noetherian R M] : is_noetherian R (ι → M) :=
is_noetherian_pi

instance {m : ℕ} : finite_dimensional ℝ (fin m → ℝ) :=
by apply_instance  -- works fine

[Eric Wieser]

I've seen something very similar for all the dfinsupp instances, where it can't seem to work out how to provide M : ι → Type* when it's a constant function

[Patrick Massot]

This doesn't seem to be enough

[Eric Wieser]

As in, that example fails for you, or there's a wider use case that still fails?

[Patrick Massot]

I have a hard time minimizing...

[Patrick Massot]

I returned to this but gave up on true minimization. It seems to be a really subtle elaboration order issue. The next piece of code works only if you uncomment the specialized instance:

import analysis.calculus.times_cont_diff

/-- non-dependent version of `is_noetherian_pi`, because typeclass inference struggles to infer `M` in the non-dependent case. -/
instance is_noetherian_pi' {R ι : Type*} {M : Type*} [ring R]
  [add_comm_group M] [semimodule R M] [fintype ι]
  [is_noetherian R M] : is_noetherian R (ι → M) :=
is_noetherian_pi

--instance {m : ℕ} : finite_dimensional ℝ (fin m → ℝ) :=
--by apply_instance  -- works fine

open_locale topological_space

variables {E : Type*} [normed_group E] [normed_space ℝ E]
          {F : Type*} [normed_group F] [normed_space ℝ F] [finite_dimensional ℝ F]

def smooth_at (f : E → F) (x : E) : Prop := ∃ s ∈ 𝓝 x, times_cont_diff_on ℝ ⊤ f s

lemma smooth_surrounding {x : F} {d} {p : fin d → F} :
  ∃ W : F × (fin d → F) → (fin d → ℝ),
  ∀ᶠ y in 𝓝 x, ∀ᶠ q in 𝓝 p, smooth_at W (y, q)  :=
sorry

[Eric Wieser]

The failing lemma can be reduced to

lemma smooth_fails {d} (W : F → (fin d → ℝ)) (y : F) : smooth_at W y  :=
sorry

[Eric Wieser]

Some more investigation:

import analysis.calculus.times_cont_diff

/-- non-dependent version of `is_noetherian_pi`, because typeclass inference struggles to infer `M` in the non-dependent case. -/
instance is_noetherian_pi' {R ι : Type*} {M : Type*} [ring R]
  [add_comm_group M] [semimodule R M] [fintype ι]
  [is_noetherian R M] : is_noetherian R (ι → M) :=
is_noetherian_pi

-- if this is an instance the original works
def missing (ι : Type*) [fintype ι] : is_noetherian ℝ (ι → ℝ) :=
by apply_instance  -- works fine

open_locale topological_space

variables {E : Type*} [normed_group E] [normed_space ℝ E]
          {F : Type*} [normed_group F] [normed_space ℝ F] [is_noetherian ℝ F]

def smooth_at (f : E → F) (x : E) : Prop := ∃ s ∈ 𝓝 x, times_cont_diff_on ℝ ⊤ f s

set_option pp.implicit true

lemma smooth_fails {d} (W : F → (fin d → ℝ)) (y : F) :
  @smooth_at _ _ _ _ _ _ (missing _) W y  :=
sorry

lemma smooth_ok1 {d} (W : F → (fin d → ℝ)) (y : F) :
  @smooth_at _ _ _ _ _ _ (missing $ fin d) W y  :=
sorry

lemma smooth_ok2 {d} (W : F → (fin d → ℝ)) (y : F) :
  @smooth_at _ _ _ _ _ _ (by exact missing _) W y  :=
sorry