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: Dec 20 2023 at 11:08 UTC