fail to synthesize

Stream: new members

[Ralf Stephan]

Trying to construct a subtype for power series with nonzero constant coeff., is there a doc about constructing subtypes?
Also, regarding the error failed to synthesize I read that usually an instance is missing but don't understand why I get the error here: adding instance definitions of NZCPowerSeries doesn't seem to matter here, as I'm not making such an object in this part of the code?

import Mathlib
set_option autoImplicit false
set_option diagnostics true

namespace PowerSeries

variable {R : Type*} [CommSemiring R]

def nonzero_constantCoeff (f : R⟦X⟧) : Prop := constantCoeff R f ≠ 0

def NZCPowerSeries (R : Type*) := { f : R⟦X⟧ // nonzero_constantCoeff f }       -- <===============

failed to synthesize
  CommSemiring R

[Ralf Stephan]

Or is it that already the nonzero condition of one coefficient leads to that failure?

[Matthew Ballard]

There are two R's. The one at L7 and the one that is a parameter of NZCPowerSeries

[Damiano Testa]

Following Matt's suggestion, you can write

variable (R)  -- make `R` explicit
def NZCPowerSeries := { f : R⟦X⟧ // nonzero_constantCoeff f }       -- <===============

[Ralf Stephan]

Thanks. Implicit-/explicitness seems to be a recurring theme that I don't grasp.

The motivation for this subtype is to enable the log operator for formal power series.

[Matthew Ballard]

Implicit: Lean should be able to figure this from the context. Eg we have (h : n > 0) so Lean should be able to figure out that n : Nat at the call site.
Explicit: Lean can't figure this out and/or readability degrades significantly omitting this.

[Matthew Ballard]

Implicit-ness is a mechanism to avoid writing giant signatures for functions

[Damiano Testa]

Ralf Stephan said:

Thanks. Implicit-/explicitness seems to be a recurring theme that I don't grasp.

The motivation for this subtype is to enable the log operator for formal power series.

Note that a lot of the times, rather than working with subtypes it is easier to work with the full type and assign junk values to terms that you would otherwise exclude. E.g. you could have the log of a power-series that starts with 0 be 0.

[Damiano Testa]

Then you do not need a subtype, since log is defined on all power series -- it is just not interesting, rather than undefined, where you would normally not compute it.

[Ralf Stephan]

If that is not frowned upon, I'll take easier any time!

[Damiano Testa]

I would say that it is standard practice and often desirable. Kevin may tell you about square-roots of negative reals, if you ask him! :smile:

[Ruben Van de Velde]

Sometimes even if you don't ask :innocent:

[Patrick Massot]

Did anyone ever ask?

[Ralf Stephan]

I didn't need to, as I found his blogpost in another thread.