## Stream: Is there code for X?

### Topic: R^m is finite dimensional over R

#### Bhavik Mehta (Mar 24 2021 at 01:59):

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?

#### Bhavik Mehta (Mar 24 2021 at 02:06):

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 (Mar 24 2021 at 02:16):

Is finite dimensional map even a class?

#### Bhavik Mehta (Mar 24 2021 at 02:18):

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 (Mar 24 2021 at 02:19):

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

#### Bhavik Mehta (Mar 24 2021 at 02:20):

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 (Mar 24 2021 at 02:22):

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

#### Adam Topaz (Mar 24 2021 at 02:23):

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

#### Bhavik Mehta (Mar 24 2021 at 02:24):

Yup it doesn't work

#### Adam Topaz (Mar 24 2021 at 02:28):

Sounds like a missing instance :expressionless:

#### Bhavik Mehta (Mar 24 2021 at 02:35):

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 (Mar 24 2021 at 02:36):

Oooh... The mystery deepens

#### Shing Tak Lam (Mar 24 2021 at 05:22):

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 (Mar 24 2021 at 05:30):

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 (Mar 24 2021 at 05:34):

Just getting rid of real.ring is enough even

#### Mario Carneiro (Mar 24 2021 at 05:35):

hm, this works:

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


#### Mario Carneiro (Mar 24 2021 at 05:38):

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 (Mar 25 2021 at 00:03):

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

#### Bhavik Mehta (Mar 25 2021 at 04:25):

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 (Mar 25 2021 at 04:27):

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


#### Yakov Pechersky (Mar 25 2021 at 04:28):

I think there's probably an issue somewhere with is_R_or_C

#### Yakov Pechersky (Mar 25 2021 at 04:30):

Ah. It might have to do with real.linear_ordered_field

#### Bhavik Mehta (Mar 25 2021 at 04:33):

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 (Mar 25 2021 at 04:35):

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 (Mar 25 2021 at 04:51):

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 (Mar 25 2021 at 04:54):

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

#### Mario Carneiro (Mar 25 2021 at 04:57):

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

#### Patrick Massot (Apr 23 2021 at 14:00):

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 (Apr 23 2021 at 14:03):

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

#### Mario Carneiro (Apr 23 2021 at 14:04):

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

#### Johan Commelin (Apr 23 2021 at 14:05):

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

#### Eric Wieser (Apr 23 2021 at 14:13):

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 (Apr 23 2021 at 14:13):

Then apply_instance can close the original goal

#### Johan Commelin (Apr 23 2021 at 14:14):

Did you check that it closes the original goal?

#### Johan Commelin (Apr 23 2021 at 14:14):

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

#### Eric Wieser (Apr 23 2021 at 14:14):

Huh, I guess I screwed up

#### Eric Wieser (Apr 23 2021 at 14:15):

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 (Apr 23 2021 at 14:16):

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 (Apr 23 2021 at 14:19):

This doesn't seem to be enough

#### Eric Wieser (Apr 23 2021 at 14:19):

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

#### Patrick Massot (Apr 23 2021 at 14:23):

I have a hard time minimizing...

#### Patrick Massot (Apr 23 2021 at 17:05):

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 (Apr 23 2021 at 17:24):

The failing lemma can be reduced to

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


#### Eric Wieser (Apr 23 2021 at 17:31):

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


Last updated: May 07 2021 at 23:11 UTC