synthesization order error in class

Stream: new members

[Will Blackmore]

Hey,

I am new to lean and am doing a project of formalizing delta rings. I have began by making a delta ring class but have and error that says
"Cannot find synthesization order for instance"

class DeltaRing (A: Type u) (p : ℕ) (hp : Nat.Prime p) extends CommRing A where
  (δ: A → A)
  (zero_prop: δ 0 = 0)
  (one_prop: δ 1 = 0)
  (add_prop: ∀{x y}, δ (x+y) = δ (x) + δ (y) - ∑ i: Finset.range p, (((1/p) * (Nat.choose p i)): ℕ) * x^(i: ℕ) * (y^(p-i)))
  (mul_prop: ∀{x y}, δ (x*y) = (x^p * δ (y)) + (y^p * δ (x)) + (p * δ (x) * δ (y)))

[Riccardo Brasca]

Lean is telling you that your definition is rather problematic. Let me explain.

[Anne Baanen]

Welcome! This error basically means that your instance has parameters that Lean cannot figure out. Specifically, here the extends keyword creates an instance of the following shape:

instance (A: Type u) (p : ℕ) (hp : Nat.Prime p) [DeltaRing A p hp] : CommRing A

So whenever Lean wants to find a CommRing A instance, it will try this instance, and suddenly need to come up with a prime number p out of nowhere.

One solution is to use "unbundled" inheritance, where you don't use extends but instead add the parent class as a parameter:

class DeltaRing (A: Type u) (p : ℕ) (hp : Nat.Prime p) [CommRing A] where
  (δ: A → A)
  (zero_prop: δ 0 = 0)
  (one_prop: δ 1 = 0)
  (add_prop: ∀{x y}, δ (x+y) = δ (x) + δ (y) - ∑ i: Finset.range p, (((1/p) * (Nat.choose p i)): ℕ) * x^(i: ℕ) * (y^(p-i)))
  (mul_prop: ∀{x y}, δ (x*y) = (x^p * δ (y)) + (y^p * δ (x)) + (p * δ (x) * δ (y)))

(untested)

[Riccardo Brasca]

OK, Anne was faster :D

[Anne Baanen]

Alternatively, if p and hp are uniquely determined by A (and I suppose here they are), you can tell that to Lean using outParam, which means it will try to pick up p and hp from the instances, instead of coming up with them upfront.

class DeltaRing (A: Type u) (p : outParam ℕ) (hp : outParam (Nat.Prime p)) extends CommRing A where
  (δ: A → A)
  (zero_prop: δ 0 = 0)
  (one_prop: δ 1 = 0)
  (add_prop: ∀{x y}, δ (x+y) = δ (x) + δ (y) - ∑ i: Finset.range p, (((1/p) * (Nat.choose p i)): ℕ) * x^(i: ℕ) * (y^(p-i)))
  (mul_prop: ∀{x y}, δ (x*y) = (x^p * δ (y)) + (y^p * δ (x)) + (p * δ (x) * δ (y)))

(untested, again)

[Will Blackmore]

Thanks, the outParam worked for me

[Anne Baanen]

If p and hp are indeed uniquely determined, you can also move them to a field of your class:

class DeltaRing (A: Type u) extends CommRing A where
  (p : ℕ)
  (hp : Nat.Prime p)
  (δ: A → A)
  (zero_prop: δ 0 = 0)
  (one_prop: δ 1 = 0)
  (add_prop: ∀{x y}, δ (x+y) = δ (x) + δ (y) - ∑ i: Finset.range p, (((1/p) * (Nat.choose p i)): ℕ) * x^(i: ℕ) * (y^(p-i)))
  (mul_prop: ∀{x y}, δ (x*y) = (x^p * δ (y)) + (y^p * δ (x)) + (p * δ (x) * δ (y)))

Which one of the three works best depends very much on the kind of uses: do you often talk about DeltaRings where p is equal to one specific number (say 37) (in this case outParam is best), or is it almost always "let p be an arbitrary prime and A be a DeltaRing for p" (in this case I'd go for having p as a field).

[Anne Baanen]

Will Blackmore said:

Thanks, the outParam worked for me

Great! This is the end of my infodump :)

[Kevin Buzzard]

Don't get discouraged -- definitions are the hard part! Once you have the definition written, you will have all the fun of making the API for it (i.e. all the basic lemmas) to come :-). In fact it's good to ask about definitions first, because what's very discouraging is that you make a definition, prove a bunch of theorems about it, PR it to mathlib and then the experts say "the definition is not optimal and you will have to change it, which by the way will break all your proofs"

I would be tempted to call the fields map_zero, map_one, map_add and map_mul. Or maybe \delta_zero etc. I've heard some computer scientists complain when mathematicians call maps unicode characters like \delta (arguing that it should be called delta and then you should make unicode notation for it), but here this is standard notation. I don't really know the disadvantages of unicode names, maybe it has something to do with documentation issues or something?