distrib_mul_action_with_zero

Stream: general

[Yaël Dillies]

Is there any reason we don't have distrib_mul_action_with_zero? module isn't quite the intersection of distrib_mul_action and mul_action_with_zero as it also assumes add_smul : ∀ (r s : R) (x : M), (r + s) • x = r • x + s • x.

[Yaël Dillies]

cc @Eric Wieser

[Eric Wieser]

Probably due to lack of particular need?

[Yaël Dillies]

It comes up quite a lot with what I'm doing now. These are abstract lemmas, so it's not like I have a concrete example satisfying distrib_mul_action_with_zero. Should we define it then?

[Eric Wieser]

I'm not opposed to adding it. I think I actually have an example of such an action in https://github.com/leanprover-community/mathlib/pull/8945/files#diff-923fd2b8078cd05fe5d03aee47329529e737233260a69f86464faf2602c94ccbR1001

[Eric Wieser]

(docs#submodule.pointwise_distrib_mul_action and docs#submodule.pointwise_mul_action_with_zero for when the PR lands)

[Yaël Dillies]

Ahah! Do you want to do it, as you seem to have done that all your life, or should I take the opportunity to learn about writing scalar actions and get gently pestered?

[Eric Wieser]

Please go ahead!

[Eric Wieser]

docs#mul_action_with_zero was @Damiano Testa's doing anyway, I thought

[Yaël Dillies]

What's happening here?

import algebra.smul_with_zero

variables (R M : Type*) [monoid_with_zero R] [add_monoid M]

/--  An action of a monoid with zero `R` on a Type `M`, also with `0`, extends `distrib_mul_action`
and is compatible with `0` (both in `R` and in `M`), with `1 ∈ R`, and with associativity of
multiplication on the monoid `M`. -/
class distrib_mul_action_with_zero extends distrib_mul_action R M :=
-- this field is copied from `smul_with_zero`, as `extends` behaves poorly
(zero_smul : ∀ m : M, (0 : R) • m = 0)

/-- Converts a `mul` typeclass into the corresponding `smul` one. See also `semiring.to_module` -/
instance monoid_with_zero.to_distrib_mul_action_with_zero : distrib_mul_action_with_zero R R :=
{ ..mul_zero_class.to_smul_with_zero R,
  ..monoid.to_distrib_mul_mul_action R }

/-
type mismatch at field 'zero_smul'
  smul_with_zero.zero_smul
has type
  ∀ (m : R),
    @eq R
      (@has_scalar.smul R R
         (@smul_with_zero.to_has_scalar R R
            (@mul_zero_class.to_has_zero R
               (@mul_zero_one_class.to_mul_zero_class R (@monoid_with_zero.to_mul_zero_one_class R _inst_1)))
            (@mul_zero_class.to_has_zero R
               (@mul_zero_one_class.to_mul_zero_class R (@monoid_with_zero.to_mul_zero_one_class R _inst_1)))
            (@mul_zero_class.to_smul_with_zero R
               (@mul_zero_one_class.to_mul_zero_class R (@monoid_with_zero.to_mul_zero_one_class R _inst_1))))
         0
         m)
      0
but is expected to have type
  ∀ (m : R),
    @eq R
      (@has_scalar.smul R R
         (@mul_action.to_has_scalar R R (@monoid_with_zero.to_monoid R _inst_1)
            (@distrib_mul_action.to_mul_action R R (@monoid_with_zero.to_monoid R _inst_1) ⁇
               (@distrib_mul_action_with_zero.to_distrib_mul_action R R _inst_1 ⁇
                  (@monoid_with_zero.to_distrib_mul_action_with_zero R _inst_1))))
         0
         m)
      0
-/

[Eric Wieser]

Well for one that's highlighted as the wrong language

[Yaël Dillies]

Arf, Discord reflex here

[Eric Wieser]

What is monoid.to_distrib_mul_mul_action?

[Yaël Dillies]

Sorry, that doesn't exist :sweat:

[Yaël Dillies]

But that wasn't the problem:

protected def function.injective.distrib_mul_action_with_zero
  (f : zero_hom M' M) (hf : function.injective f) (smul : ∀ (a : R) b, f (a • b) = a • f b) :
  distrib_mul_action_with_zero R M' :=
{ ..hf.distrib_mul_action f smul, ..hf.smul_with_zero f smul }

Same error... Different error, actually!

[Yaël Dillies]

I think I just don't know what I'm doing.

[Yaël Dillies]

I'll study the typeclasses more thoroughly...

[Eric Wieser]

That's an entirely different code snippet!

[Eric Wieser]

but docs#function.injective.distrib_mul_action require an add_monoid_hom doesn't it?

[Eric Wieser]

And you're passing it a zero_hom (edit: until you just fixed it)

[Yaël Dillies]

Psch :innocent:

[Eric Wieser]

What's the error message?

[Yaël Dillies]

Now that's ok. I left the confusing error messages land.

[Yaël Dillies]

Right now it's

failed to synthesize type class instance for
R : Type u_1,
M' : Type u_4,
_inst_1 : monoid_with_zero R,
_inst_5 : has_zero M',
_inst_6 : has_scalar R M'
⊢ add_zero_class M'

[Yaël Dillies]

which I can just solve by upgrading has_zero M' to add_monoid M'

[Yaël Dillies]

@Eric Wieser, with the same definition as above, this loops (or at least repeats the same search over and over again) on typeclass inference:

variables (R M : Type*) [monoid_with_zero R] [add_monoid M][distrib_mul_action_with_zero R M]

instance : mul_action_with_zero R M := by apply_instance

Have I born a monster?

[Yaël Dillies]

It ends up repeating

[class_instances] (32) ?x_225 : @mul_action_with_zero R M _inst_1 (@add_zero_class.to_has_zero M (@add_monoid.to_add_zero_class M _inst_2)) := @monoid_with_zero.to_mul_action_with_zero ?x_226 ?x_227
failed is_def_eq
[class_instances] (32) ?x_225 : @mul_action_with_zero R M _inst_1 (@add_zero_class.to_has_zero M (@add_monoid.to_add_zero_class M _inst_2)) := @distrib_mul_action_with_zero.to_mul_action_with_zero ?x_228 ?x_229 ?x_230 ?x_231 ?x_232
[class_instances] cached instance for add_monoid M
_inst_2

[Yaël Dillies]

Actually, even #check distrib_mul_action_with_zero.to_mul_action_with_zero R M fails to terminate :fear:

[Eric Wieser]

Mwe?

[Yaël Dillies]

Same as above

[Eric Wieser]

I thought all your snippets above gave errors

[Eric Wieser]

Can you put the whole lot inone code block?

[Yaël Dillies]

import algebra.smul_with_zero

variables (R M : Type*) [monoid_with_zero R] [add_monoid M]

class distrib_mul_action_with_zero extends distrib_mul_action R M :=
(zero_smul : ∀ m : M, (0 : R) • m = 0)

variables [distrib_mul_action_with_zero R M]

@[priority 100] -- see Note [lower instance priority]
instance distrib_mul_action_with_zero.to_mul_action_with_zero [m : mul_action_with_zero R M] :
  mul_action_with_zero R M :=
{..m}

#check distrib_mul_action_with_zero.to_mul_action_with_zero R M

[Eric Wieser]

What the heck is [m : for there?

[Eric Wieser]

It has the same type as the instance you're trying to produce!

[Yaël Dillies]

Oh, yeah. Words. Speaking. Hard. :face_palm:

[Yaël Dillies]

I knew I was being dumb!

[Yaël Dillies]

I just didn't know how.

[Yaël Dillies]

Thanks a lot :smile:

[Kevin Buzzard]

Often talking to other people is a good way to get to the bottom of situations like that! Before chatrooms I used to write long emails to people every time I'd proved 0=1 and during my explanation I'd realise my mistake. What's that technique called? Something to do with ducks or something?

[Mario Carneiro]

https://en.wikipedia.org/wiki/Rubber_duck_debugging

[Yaël Dillies]

Ahah! I actually managed to make all the proofs work.

[Yaël Dillies]

#9123

[Yaël Dillies]

I didn't relax any module to distrib_mul_action_with_zero yet. Should that be part of this PR?

[Eric Wieser]

I think you should probably at least add instances for everything that already has a docs#mul_action_with_zero instance and can be generalized

[Eric Wieser]

Namely, pi, prod, and order_dual.

[Eric Wieser]

Also, there seems to be a duplicate! docs#opposite.monoid_with_zero.to_opposite_mul_action_with_zero vs docs#monoid_with_zero.to_opposite_mul_action_with_zero

[Yaël Dillies]

Oooh, good find!

[Eric Wieser]

docs#opposite.semiring.to_opposite_module is also a duplicate of docs#semiring.to_opposite_module

[Yaël Dillies]

Which ones should I remove?

[Eric Wieser]

It looks like some sinister accidental namespacing has prevented their names clashing

[Eric Wieser]

The opposite. prefix shouldn't be there

[Yaël Dillies]

And mul_zero_class.to_opposite_smul_with_zero vs opposite.mul_zero_class.to_opposite_smul_with_zero

[Yaël Dillies]

I don't understand this build fail: https://github.com/leanprover-community/mathlib/runs/3561609511
but maybe the pi/prod/order_dual instances will solve it?

[Eric Wieser]

My hunch: The build failure is that the has_scalar in that is_scalar_tower is not syntactically equal to the one it used to be (aka the one we have an instance for), and the lean3 typeclass search gets stuck on dependent arguments like that sometimes.

[Yaël Dillies]

Arf, what can I do?

[Eric Wieser]

Well, your PR has some typos that may or may not help

[Eric Wieser]

I'd try finding the instance manually with a haveI, and see if lean thinks their types are equal

[Yaël Dillies]

I could squash all the typos had I a functioning infoview, but I'm in hell so I'm coding blindly.

[Eric Wieser]

Why are you in hell?

[Yaël Dillies]

I have no idea :confused:

[Eric Wieser]

I think the best approach to get out of it is:

• Close all tabs in vs-code
• Close vs-code
• Use get-cache --rev on the last known revision
• Reopen vs-code

[Yaël Dillies]

Didn't do anything but I'm out of hell!

[Yaël Dillies]

All the order_dual instances in algebra.ordered_smul but the last one could be generalized. That's why I had a relaxable semiring :smile:

[Yaël Dillies]

How did you do that slide by the way? https://eric-wieser.github.io/fmm-2021/#/elementary-multiplication-stronger/4
I'm very interested in visualising hierarchies like that. I think we should have such pictures somewhere in the docs.

[Eric Wieser]

I wrote it out by hand as a graphviz file then compiled it to svg.

[Eric Wieser]

https://eric-wieser.github.io/fmm-2021/figures/has_mul.dot

[Eric Wieser]

(If you hit view source on the presentation, every .dot.svg file has a corresponding .dot uploaded)

[Yaël Dillies]

Oh, by hand.

[Yaël Dillies]

I seem to have gotten a random timeout: https://github.com/leanprover-community/mathlib/pull/9123/checks?check_run_id=3567080085
I can't reproduce it locally.

[Yaël Dillies]

The culprit is ideal.module_pi. Is there any speedup available?

[Eric Wieser]

I've got timeouts there before

[Eric Wieser]

Can you spin out a PR to delete all the duplicate instances so that we can at least merge that while you fight the timeouts?

[Yaël Dillies]

Sure

[Yaël Dillies]

Uh. I reran the jobs and I got a different error. https://github.com/leanprover-community/mathlib/pull/9123/checks?check_run_id=3569471500

[Yaël Dillies]

New scalar hierarchy scalar_hierarchy.png

[Yaël Dillies]

Yes, I had fun with Paint

[Eric Wieser]

docs#mul_distrib_mul_action is also new

[Yaël Dillies]

Where does it fit? Between mul_semiring_action and distrib_mul_action?

[Yaël Dillies]

Updated updated scalar hierarchy Scalar-hierarchy.png

[Eric Wieser]

Oh sorry, it's adjacent to distrb_mul_action not a superset of it

[Yaël Dillies]

Ah, and mul_semiring_action goes to both of them?

[Eric Wieser]

Yes!

[Kevin Buzzard]

Yaël Dillies said:

The culprit is ideal.module_pi. Is there any speedup available?

#9148

[Yaël Dillies]

Wow thanks!

[Yaël Dillies]

Sorry to bother you again, but I'm getting yet another error I don't understand. https://github.com/leanprover-community/mathlib/runs/3579349443
The instructions are very detailed, but I don't really get it. How do I "run scripts/mk_all.sh"? sh mk_all.sh doesn't seem to produce anything.

Here's the message

/- The `fails_quickly` linter reports: -/
/- TYPE CLASS SEARCHES TIMED OUT.
The following instances are part of a loop, or an excessively long search.
It is common that the loop occurs in a different class than the one flagged below,
but usually an instance that is part of the loop is also flagged.
To debug:
(1) run `scripts/mk_all.sh` and create a file with `import all` and
`set_option trace.class_instances true`
(2) Recreate the state shown in the error message. You can do this easily by copying the type of
the instance (the output of `#check @my_instance`), turning this into an example and removing the
last argument in square brackets. Prove the example using `by apply_instance`.
For example, if `additive.topological_add_group` raises an error, run

example {G : Type*} [topological_space G] [group G] : topological_add_group (additive G) :=
by apply_instance

(3) What error do you get?
(3a) If the error is "tactic.mk_instance failed to generate instance",
there might be nothing wrong. But it might take unreasonably long for the type-class inference to
fail. Check the trace to see if type-class inference takes any unnecessary long unexpected turns.
If not, feel free to increase the value in the definition of the linter `fails_quickly`.
(3b) If the error is "maximum class-instance resolution depth has been reached" there is almost
certainly a loop in the type-class inference. Find which instance causes the type-class inference to
go astray, and fix that instance. -/
-- algebra/module/pi.lean
#check @pi.has_scalar' /- type-class inference timed out
State:
I : Type u,
f : I → Type v,
g : I → Type u_1
⊢ has_scalar (Π (i : I), f i) (Π (i : I), g i) -/

[Alex J. Best]

Running ./scripts/mk_all.sh creates a file src/all.lean iirc

[Alex J. Best]

Then you should be able to import the whole of mathlib using import all