Compiler IR check failed

Stream: new members

[Gareth Ma]

Hello, I don't understand why Polynomial.C is unknown declaration.

import Mathlib.Algebra.RingQuot
import Mathlib.RingTheory.Ideal.IsPrimary
import Mathlib.RingTheory.Ideal.LocalRing

open Polynomial Ideal

example {R : Type*} [CommRing R] : (R[X] ⧸ (span {X} : Ideal R[X])) ≃+* R where
  toFun := fun f ↦ by sorry
  invFun := fun f ↦ Quotient.mk _ (C f)
  left_inv := by sorry
  right_inv := by sorry
  map_mul' := by sorry
  map_add' := by sorry

[Gareth Ma]

(Also, does this exist already? And is there a better way to writing it? It seems Quot and Quotient is a bit awkward to work with)

[Gareth Ma]

noncomputable example {R : Type*} [CommRing R] : R ≃+* (R[X] ⧸ (span {X} : Ideal R[X])) where
  toFun := fun f ↦ Ideal.Quotient.mk _ (C f)
  invFun := fun f ↦ by
    apply Quot.lift Polynomial.constantCoeff ?_ f
    intro f g h
    rwa [Submodule.quotientRel_r_def, mem_span_singleton, X_dvd_iff, coeff_sub, sub_eq_zero] at h
  left_inv := fun f ↦ by
    change constantCoeff (C f) = f
    simp
  right_inv := fun f ↦ by
    apply Quotient.ind ?_ f
    intro f
    change _ = mk (span {Y}) f
    simp [Ideal.Quotient.eq, mem_span_singleton, X_dvd_iff]
  map_mul' := fun f g ↦ by simp
  map_add' := fun f g ↦ by simp

I finished the proof, plus I still don't understand the issue above. It seems to be related to the fact that I have to add noncomputable now

[Gareth Ma]

(In particular it would be nice for induction to work for Quot types using Quotient.ind - I think mathematically/type-theoretically it's incorrect, but still, it's literally called .ind)

[Riccardo Brasca]

The first one is docs#Polynomial.quotientSpanXSubCAlgEquiv

[Riccardo Brasca]

Or at least very close

[Gareth Ma]

It seems that AlgEquiv extends A ≃ B, A ≃* B, A ≃+ B, A ≃+* B so I should be able to extract the RingEquiv at the end. But

[Gareth Ma]

example {R : Type*} [CommRing R] : R ≃+* (R[X] ⧸ (span {X} : Ideal R[X])) := by
  have := Polynomial.quotientSpanXSubCAlgEquiv (R := R) 0
  rw [C_0, sub_zero] at this
  /-
  ▶ 45:9-45:28: error:
  synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
    NonUnitalNonAssocRing.toMul
  inferred
    Equiv.mul this.toEquiv
  -/
  exact this.ringEquiv.symm

Have I found a type diamond? Or is this a different issue?

[Riccardo Brasca]

What does convert say?

[Gareth Ma]

Actually I don't understand why it extends the earlier 3 classes either

[Gareth Ma]

convert gives two goals, but also throws the same error:

⊢ NonUnitalNonAssocRing.toMul = Equiv.mul this.toEquiv
⊢ Distrib.toAdd = Equiv.add this.toEquiv

[Riccardo Brasca]

Ah sorry, the error is at rw

[Riccardo Brasca]

Right?

[Gareth Ma]

Nono

[Gareth Ma]

The exact

[Gareth Ma]

My bad

[Gareth Ma]

Found something interesting.

have := this.ringEquiv /- this is "ok", but gives
this : let add := Equiv.add this✝.toEquiv;
let mul := Equiv.mul this✝.toEquiv;
R[X] ⧸ span {Y - C 0} ≃+* R
-/
have := this.ringEquiv.symm /- this fails with the same synthesizer error

[Riccardo Brasca]

Well, the problem is probably that rw is modifying the objects you are working on, but not all the instances, and this confuses Lean

[Riccardo Brasca]

I don't think it is a diamond.

[Gareth Ma]

No, the rw is irrelevant, see this:

def asdf {R : Type*} [CommRing R] : false := by
  have := Polynomial.quotientSpanXSubCAlgEquiv (R := R) 37
  have := this.ringEquiv /- works -/
  have := this.ringEquiv.symm /- fails -/

[Gareth Ma]

I've got to go, but thanks for the help. I can dig around a bit more later but I don't know how far I can get :tear:

[Riccardo Brasca]

Can you write a #mwe? Anyway I need a computer to debug this (I will have access to one later today)

[Gareth Ma]

MWE is just this:

import Mathlib.Algebra.RingQuot
import Mathlib.RingTheory.Ideal.IsPrimary
import Mathlib.RingTheory.Ideal.LocalRing

open Polynomial Ideal

def asdf {R : Type*} [CommRing R] : false := by
  have := Polynomial.quotientSpanXSubCAlgEquiv (R := R) 37
  have := this.ringEquiv
  have := this.ringEquiv.symm

[Riccardo Brasca]

There are 2 .ringEquiv

[Yaël Dillies]

The this in the third have refers to the second have, not the first

[Gareth Ma]

My bad, but it's still not fixed :(

def asdf {R : Type*} [CommRing R] : false := by
  have yael := Polynomial.quotientSpanXSubCAlgEquiv (R := R) 37
  have := yael.ringEquiv
  have := yael.ringEquiv.symm

[Gareth Ma]

(I think {line 1}.ringEquiv = {line 2}.ringEquiv = {line 2} anyways)

[Riccardo Brasca]

You are using have instead of let maybe?

[Riccardo Brasca]

Yes, this is the problem.

import Mathlib.Algebra.RingQuot
import Mathlib.RingTheory.Ideal.IsPrimary
import Mathlib.RingTheory.Ideal.LocalRing

open Polynomial Ideal

noncomputable
def asdf {R : Type*} [CommRing R] : R ≃+* (R[X] ⧸ (span {X} : Ideal R[X])) := by
  let f := Polynomial.quotientSpanXSubCAlgEquiv (R := R) 0
  rw [C_0, sub_zero] at f
  exact f.toRingEquiv.symm

works.

[Riccardo Brasca]

It's not really idiomatic since we try to avoid using tactic mode to write definitons, but still.

[Gareth Ma]

Ah but .ringEquiv still fails

[Riccardo Brasca]

It's called toRingEquiv

[Gareth Ma]

Ah .ringEquiv just tries to access one of the underlying inherited typeclasses(?)' ringEquiv, which is just wrong. Okay, makes sense. Thanks!!

[Gareth Ma]

Learned a lot :D

[Bolton Bailey]

I encountered a similar problem recently. I think it should be considered a bug for Lean to be able to say "unknown declaration" immediately after a #check statement that confirms the declaration is present in the context.

[Bolton Bailey]

lean4#1785 deals with this issue. I encourage people to upvote it if they agree it should be fixed.

[Gareth Ma]

IR check failed in presence of noncomputable

Yep I think that's one of the problem originally, upvoted :)