how to define positive cones in $\mathbb{R}^n$?

Stream: maths

[Apurva Nakade]

I want to define the docs#convex_cone.positive consisting of vectors of a finite size n with all coordinates non-negative. If I try

#check convex_cone.positive ℝ (fin 2 → ℝ)

I get the following error:

failed to synthesize type class instance for
𝕜 : Type u_1,
E : Type u_2,
F : Type u_3,
G : Type u_4,
_inst_1 : add_comm_group E,
_inst_2 : module ℝ E
⊢ ordered_smul ℝ (fin 2 → ℝ)

I'm getting really lost in the various instance hierarchies in trying to define this. Any suggestions on how to do this?

[Yaël Dillies]

That should be obvious.

[Yaël Dillies]

Are you importing docs#pi.ordered_smul?

[Apurva Nakade]

Didn't know about this file. Let me try.

[Apurva Nakade]

Same error even with the import

[Yaël Dillies]

Give me a MWE, I'll fix it.

[Apurva Nakade]

import analysis.cone.basic
import algebra.order.module

#check convex_cone.positive ℝ (fin 2 → ℝ)

[Yaël Dillies]

analysis.cone.basic doesn't exist

[Apurva Nakade]

typo, convex

[Apurva Nakade]

analysis.convex.basic

sorry

[Yaël Dillies]

file#analysis/convex/cone, actually

[Apurva Nakade]

my vscode is stuck, 1 min, will fix the MWE

[Apurva Nakade]

ok here's is the corrected mwe

import analysis.convex.cone
import algebra.order.module

#check convex_cone.positive ℝ (fin 2 → ℝ)

and the error is

failed to synthesize type class instance for
⊢ ordered_smul ℝ (fin 2 → ℝ)

[Yaël Dillies]

Okay, this is really weird.

import algebra.order.module
import data.real.basic

example : ordered_smul ℝ ℝ := infer_instance
noncomputable example : linear_ordered_field ℝ := infer_instance
example : mul_action_with_zero ℝ ℝ := infer_instance
example : ordered_add_comm_group ℝ := infer_instance

example : ordered_smul ℝ (fin 2 → ℝ) := infer_instance -- fails
example : ordered_smul ℝ (fin 2 → ℝ) := @pi.ordered_smul' ℝ _ (fin 2) ℝ _ _ _ -- works

[Yaël Dillies]

TC inference does try unifyingpi.ordered_smul' but then it fails to find linear_ordered_field ℝ, even though it's clearly there.

[Yaël Dillies]

Looking at the trace, it might be because it finds a huge term for ordered_add_comm_monoid (fin 2 → ℝ). Maybe it would also help if docs#ordered_smul only assumed docs#has_smul, not docs#smul_with_zero.

[Apurva Nakade]

Should I try removing it? I don't think my laptop can handle this deep a change though lol. I can only push this change to mathlib and wait for CI.

[Eric Wieser]

Is docs#pi.ordered_smul true more generally without needing linear_ordered_field?

[Apurva Nakade]

But this shouldn't cause problems for ℝ modules, no?

[Yaël Dillies]

Yes it should be. Looks like everything got dumped into the same section by accident.

[Apurva Nakade]

Should I create an Issue for now?

[Yaël Dillies]

Am still trying to fix it, fwiw

[Apurva Nakade]

Oh, oops, thank you so much! I saw your reply one min after I posted #16021

[Yaël Dillies]

I cleaned up algebra.order.smul and algebra.order.module, but that still didn't the error, so in # I am adding yet another redundant instance.

import algebra.order.module
import data.real.basic

variables {ι : Type*}

example : ordered_smul ℝ ℝ := infer_instance
noncomputable example : linear_ordered_field ℝ := infer_instance
example : mul_action_with_zero ℝ ℝ := infer_instance
example : ordered_add_comm_group ℝ := infer_instance

example : ordered_smul ℝ (ι → ℝ) := infer_instance -- fails
example : ordered_smul ℝ (ι → ℝ) := @pi.ordered_smul' ι ℝ ℝ _ _ _ _ -- works

(MWE on #16131 when removing pi.ordered_smul'')
cc @Apurva Nakade

[Apurva Nakade]

Thank you! Do you have a general sense of why this is happening? Are there some diamonds being created which prevents lean from infering the correct instance?

[Yaël Dillies]

No, I don't understand why Lean fails to find linear_ordered_field ℝ within the search for ordered_smul ℝ (ι → ℝ).

[Yaël Dillies]

Maybe @Anne Baanen will have an idea?

[Eric Wieser]

It's the standard pi typeclass issue for dependent type classes

[Yaël Dillies]

Yes, but why is it failing given that we have docs#pi.ordered_smul'?

[Eric Wieser]

Because that's about @module (ring.to_semiring) or similar, but here you need @module (comm_semiring.to_semiring) or similar

[Eric Wieser]

(or more likely, the same problem but for the add_comm_monoid argument since that's about a pi type)

[Yaël Dillies]

But surely that doesn't matter? This kind of mismatch happens all over the place.

[Eric Wieser]

Yeah, and it causes problems all over the place too

[Eric Wieser]

See for instance these lines which provide docs#function.algebra_ring and friends

[Eric Wieser]

It's possible having a function.module_ring shortcut instance would solve the ordered_smul problem being faced here.