Reducibility and Classes

Stream: lean4

[François G. Dorais]

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]

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]

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]

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]

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]

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]

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]

(deleted)