Zulip Chat Archive

Stream: Is there code for X?

Topic: R^m is finite dimensional over R


view this post on Zulip 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?

view this post on Zulip Yakov Pechersky (Mar 24 2021 at 02:06):

docs#is_noetherian_pi ?

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 24 2021 at 02:16):

Is finite dimensional map even a class?

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 24 2021 at 02:19):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 24 2021 at 02:22):

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

view this post on Zulip Adam Topaz (Mar 24 2021 at 02:23):

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

view this post on Zulip Bhavik Mehta (Mar 24 2021 at 02:24):

Yup it doesn't work

view this post on Zulip Adam Topaz (Mar 24 2021 at 02:28):

Sounds like a missing instance :expressionless:

view this post on Zulip 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...

view this post on Zulip Adam Topaz (Mar 24 2021 at 02:36):

Oooh... The mystery deepens

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Alex J. Best (Mar 24 2021 at 05:34):

Just getting rid of real.ring is enough even

view this post on Zulip Mario Carneiro (Mar 24 2021 at 05:35):

hm, this works:

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Yakov Pechersky (Mar 25 2021 at 04:27):

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

view this post on Zulip Yakov Pechersky (Mar 25 2021 at 04:28):

I think there's probably an issue somewhere with is_R_or_C

view this post on Zulip Yakov Pechersky (Mar 25 2021 at 04:30):

Ah. It might have to do with real.linear_ordered_field

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 25 2021 at 04:57):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 23 2021 at 14:05):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Apr 23 2021 at 14:13):

Then apply_instance can close the original goal

view this post on Zulip Johan Commelin (Apr 23 2021 at 14:14):

Did you check that it closes the original goal?

view this post on Zulip Johan Commelin (Apr 23 2021 at 14:14):

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

view this post on Zulip Eric Wieser (Apr 23 2021 at 14:14):

Huh, I guess I screwed up

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 23 2021 at 14:19):

This doesn't seem to be enough

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Apr 23 2021 at 14:23):

I have a hard time minimizing...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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