# Zulip Chat Archive

## Stream: lean4

### Topic: Reducibility and Classes

#### François G. Dorais (Jan 22 2021 at 15:56):

Type class inference has changed drastically in Lean 4, with better and faster search algorithms. However, I found the following Lean 4 behavior surprising:

```
class P {α : Type} (op : α → α → α) : Prop
def T {α : Type} (op : α → α → α) [P op] := 0
def natAdd := Nat.add
instance : P natAdd := ⟨⟩
#check T natAdd -- works
#check T Nat.add -- fails
attribute [reducible] natAdd
#check T natAdd -- fails!?
#check T Nat.add -- fails!?
```

In Lean 3 (after substituting `Nat`

with `nat`

), marking the definition reducible has the exact opposite effect where the last two checks both work. I would have expected at least the first check to continue working in Lean 4 after marking `natAdd`

reducible. I can live with the last check failing but I prefer the Lean 3 behavior. What is the rationale for Lean 4's behavior?

#### Leonardo de Moura (Jan 22 2021 at 16:07):

The current implementation assumes the reducibility settings do not change after the declaration is created. Note that the two checks succeed if you use

```
@[reducible] def natAdd := Nat.add
```

We should generate an error if the user tries to change the reducibility annotation using

```
attribute [reducible] natAdd
```

We are making this assumption because we don't want to spend time reconstructing all indices when reducibility settings are modified.

We index type class instances, simp lemmas, etc.

#### François G. Dorais (Jan 22 2021 at 16:43):

Thank you Leo! That makes perfect sense!

Is the following a variation on the same?

```
structure A (α) where op : α → α → α
class P {α} (op : α → α → α) : Prop
def T {α} (x : A α) [P x.op] := 0
class Q {α} (x : A α) : Prop
instance instPOfQ {α} (x : A α) [Q x] : P x.op := ⟨⟩
def x₁ : A Nat where op := Nat.add
instance q₁ : Q x₁ := ⟨⟩
@[reducible] def x₂ : A Nat where op := Nat.add
instance q₂ : Q x₂ := ⟨⟩
#synth P (x₁.op) -- works
#synth P (x₂.op) -- fails
#check T x₁ -- works
#check T x₂ -- fails
```

#### Leonardo de Moura (Jan 22 2021 at 16:54):

Yes, it is. Your type class index contains an entry for `P x.op`

. When you mark `x₂`

as reducible, `P (x₂.op)`

becomes `P Nat.add`

. Then, when we ask the index for candidate instances for `P Nat.add`

, we get none.

In Lean 3, the example above works because the index uses just the head symbol, `P`

in this example.

The indexing data-structure for simp lemmas and instances work as follows:

- When adding a "key" to the index, we expand reducible constants.
- When searching the index for "candidates", we also expand "reducible" constants.

#### Leonardo de Moura (Jan 22 2021 at 16:59):

BTW, we added an annotation to disable indexing on subterms. If you write

```
instance instPOfQ {α} (x : A α) [Q x] : P (noindex! x.op) := ⟨⟩
```

Lean 4 will treat `x.op`

as a wildcard, and the example above will succeed. The `noindex!`

is just an annotation.

Of course, if one overuses `noindex!`

, the indexing data structures will not filter potential candidates effectively and will impact performance.

#### François G. Dorais (Jan 22 2021 at 17:17):

Thank you for the detailed explanation. I will need to rethink some of the ways I use classes in Lean 4.

So far, `noindex!`

works for porting Lean 3 code. Thanks for the tip!

#### Jason Gross (Mar 22 2021 at 19:44):

Is it an oversight that `attribute [reducible]`

is supported for structure fields, but `@[reducible]`

is not? (I think I just hit this as https://github.com/leanprover/lean4/issues/365 ?)

#### Daniel Selsam (Mar 22 2021 at 22:48):

(deleted)

Last updated: May 18 2021 at 23:14 UTC