Statement about particular instance of typeclass

Stream: general

[Daniel Weber]

What is the proper way to state this? I want to state that for the particular instance of DifferentialRing returned by derivMem we get a differential algebra.

import Differential

variable {F : Type*} [CommDifferentialRing F]

open Polynomial


noncomputable def derivMem (b : F) : CommDifferentialRing F[X] where
  deriv := sorry
  deriv_mul := sorry

noncomputable def derivMemAlgebra (b : F) :
    @DifferentialAlgebra F F[X] _ (derivMem b).toDifferentialRing where -- failed to synthesize instance DifferentialRing F[X]
  deriv_cast := sorry

This is Differential:

import Mathlib
import Lean

open algebraMap
open Lean PrettyPrinter Delaborator SubExpr

class Differential (R : Type*) [AddZeroClass R] where
  deriv : R →+ R

postfix:75 "′" => Differential.deriv

@[delab app.DFunLike.coe]
def delabDeriv : Delab := do
  let e ← getExpr
  guard <| e.isAppOfArity' `DFunLike.coe 6
  guard <| (e.getArg!' 4).isAppOf' `Differential.deriv
  let arg ← withAppArg delab
  `($arg′)

class DifferentialRing (R : Type*) extends Ring R, Differential R where
  deriv_mul : ∀ a b : R, (a * b)′ = a′ * b + a * b′

class CommDifferentialRing (R : Type*) extends CommRing R, DifferentialRing R

class DifferentialAlgebra (A : Type*) (B : Type*) [CommDifferentialRing A] [DifferentialRing B]
    extends Algebra A B where
  deriv_cast : ∀ a : A, (a′ : A) = (a : B)′

[Kevin Buzzard]

Yeah I can't make head or tail of what's failing here -- nice question! Using let you can add the instance to the context and check that everything's working; the fact that the error is after inferInstance and on the where means (I believe) that typeclass inference is working fine. If you comment out i,j,k you get the expected error on the second inferInstance. Here's a single-file repro to make others' lives easier (I stripped out universes too because they sometimes do weird things, but it's not the answer; I also unsorried data but that wasn't it either):

import Mathlib
import Lean

section differential_file

open algebraMap
open Lean PrettyPrinter Delaborator SubExpr

class Differential (R : Type) [AddZeroClass R] where
  deriv : R →+ R

postfix:75 "′" => Differential.deriv

@[delab app.DFunLike.coe]
def delabDeriv : Delab := do
  let e ← getExpr
  guard <| e.isAppOfArity' `DFunLike.coe 6
  guard <| (e.getArg!' 4).isAppOf' `Differential.deriv
  let arg ← withAppArg delab
  `($arg′)

class DifferentialRing (R : Type) extends Ring R, Differential R where
  deriv_mul : ∀ a b : R, (a * b)′ = a′ * b + a * b′

class CommDifferentialRing (R : Type) extends CommRing R, DifferentialRing R

class DifferentialAlgebra (A : Type) (B : Type) [CommDifferentialRing A] [DifferentialRing B]
    extends Algebra A B where
  deriv_cast : ∀ a : A, (a′ : A) = (a : B)′

end differential_file

variable {F : Type} [CommDifferentialRing F]

open Polynomial

noncomputable def derivMem (b : F) : CommDifferentialRing F[X] where
  deriv := by exact divX_hom -- instead of sorrying data I added some wrong data
  deriv_mul := sorry -- less scared to sorry a proof

noncomputable def derivMemAlgebra (b : F) :
    let i := derivMem b
    let j : CommDifferentialRing F[X] := inferInstance
    let k : DifferentialRing F[X] := inferInstance
    let l : Algebra F F[X] := inferInstance
    @DifferentialAlgebra F F[X] inferInstance inferInstance where -- failed to synthesize instance DifferentialRing F[X]
  deriv_cast := sorry

[Daniel Weber]

I managed to get it to work as

noncomputable def derivMemAlgebra (b : F) :
    letI := derivMem b; DifferentialAlgebra F F[X] :=
  letI := derivMem b
  DifferentialAlgebra.mk sorry

but I'm still curious about the error

[Eric Wieser]

I think this is failing because derivMem is a def, and defs are not reducible to instance search

[Eric Wieser]

Why aren't you using instance?

[Daniel Weber]

Because it depends on b---different values of b produce different CommDifferentialRings

[Eric Wieser]

This works:

suppress_compilation

def derivMem (b : F) : CommDifferentialRing F[X] where
  deriv := by exact divX_hom -- instead of sorrying data I added some wrong data
  deriv_mul := sorry -- less scared to sorry a proof

def derivMemAlgebra (b : F) :
    letI := derivMem b
    DifferentialAlgebra F F[X] :=
  letI := derivMem b
  { deriv_cast := sorry }

[Eric Wieser]

You need the letI in both the type and the value

[Eric Wieser]

Because Lean ignores the expected type and goes searching for the instance again anyway

[Eric Wieser]

The error appears on the where keyword because this is calling DifferentiableAlgebra.mk, and it's here that the instance can't be synthesized

[Eric Wieser]

This also works:

noncomputable def derivMemAlgebra (b : F) :
    @DifferentialAlgebra F F[X] _ (derivMem b).toDifferentialRing :=
  @DifferentialAlgebra.mk _ _ (_) (_) _
    sorry

[Eric Wieser]

Here (_) means "don't look for the instance, work it out from the expected type"