# Zulip Chat Archive

## Stream: new members

### Topic: synthesization order error in class

#### Will Blackmore (Oct 03 2023 at 13:02):

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 (Oct 03 2023 at 13:15):

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

#### Anne Baanen (Oct 03 2023 at 13:15):

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 (Oct 03 2023 at 13:15):

OK, Anne was faster :D

#### Anne Baanen (Oct 03 2023 at 13:19):

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 (Oct 03 2023 at 13:22):

Thanks, the outParam worked for me

#### Anne Baanen (Oct 03 2023 at 13:23):

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 `DeltaRing`

s 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 (Oct 03 2023 at 13:24):

Will Blackmore said:

Thanks, the outParam worked for me

Great! This is the end of my infodump :)

#### Kevin Buzzard (Oct 03 2023 at 16:50):

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?

Last updated: Dec 20 2023 at 11:08 UTC