Modified typeclass resolution

Stream: lean4

[Tomas Skrivan]

In a recent post, I had an issue with a special kind of infinite loop during typeclass synthesis. Concretely, the loop is of the form:

C
α → C
α → α → C
α → α → α → C
...

I believed that it should be fixable and after a weekend of thinking and coding I have a fix.

I have forked lean4 and now the typeclass synthetisis should work much better for synthesizing classes of the form (a : α) → C where a does not appear in C. The modified lean does not break a single unit test, so hopefully the modification is purely an extension.

Why did I do that? I want to work with unbundled morphisms. In mathlib, we work with unbundled objects and any kind of structure is fetch on the fly with the typeclass system. I want to do the same for functions and on the fly fetch a proof that a function is linear, continuous, differentiable, ...

Here is an example of what the modification allows. All of the examples are automatically solver by typeclass resolution and those six instances roughly correspond to rules that hold in cartesian closed category.

def is_smooth {α β} (f : α → β) : Prop := sorry

class IsSmooth {α β} (f : α → β) : Prop where
  (proof : is_smooth f)

instance identity : IsSmooth fun a : α => a := sorry
instance const (b : β) : IsSmooth fun a : α => b := sorry
instance swap (f : α → β → γ) [∀ a, IsSmooth (f a)] : IsSmooth (λ b a => f a b) := sorry
instance parm (f : α → β → γ) [IsSmooth f] (b : β) : IsSmooth (λ a => f a b) := sorry
instance comp (f : β → γ) (g : α → β) [IsSmooth f] [IsSmooth g] : IsSmooth (f ∘ g) := sorry
instance diag (f : β → δ → γ) (g : α → β) (h : α → δ) [IsSmooth f] [∀ b, IsSmooth (f b)] : IsSmooth (λ a => f (g a) (h a)) := sorry

example (f : β → γ) (g : α → β) [IsSmooth f] [IsSmooth g] : IsSmooth (f ∘ g) := by infer_instance
example (f : β → γ) [IsSmooth f] : IsSmooth λ (g : α → β) => (f ∘ g) := by infer_instance
example (f : β → δ → γ) [IsSmooth f] (g : α → β) [IsSmooth g] (d : δ) : IsSmooth (λ a => f (g a) d) := by infer_instance
example (f : β → δ → γ) [IsSmooth f] (g : α → β) [IsSmooth g] : IsSmooth (λ a d => f (g a) d) := by infer_instance
example (f : δ → β → γ) [∀ d, IsSmooth (f d)] (g : α → β) [IsSmooth g] : IsSmooth (λ a d => (f d (g a))) := by infer_instance
example (f : β → δ → γ) [IsSmooth f] (g : α → β) [IsSmooth g] (h : α → α) [IsSmooth h] (d : δ) : IsSmooth (λ a => f (g (h a)) d) := by infer_instance
example (f : α → β → γ) [∀ a, IsSmooth (f a)] : IsSmooth (λ b a => f a b) := by infer_instance
example (f : α → β → γ → δ) [∀ a b, IsSmooth (f a b)] : IsSmooth (λ c b a => f a b c) := by infer_instance
example (f : α → β → γ → δ) [∀ a b, IsSmooth (f a b)] : IsSmooth (λ c a b => f a b c) := by infer_instance
example (f : α → β → γ → δ → ε) [∀ a b c, IsSmooth (f a b c)] : IsSmooth (λ d a b c => f a b c d) := by infer_instance
example (f : α → β → γ) [IsSmooth f] (b : β) : IsSmooth (λ a => f a b) := by infer_instance
example (f : α → β → γ → δ) [IsSmooth f] (b : β) (c : γ) : IsSmooth (λ a => f a b c) := by infer_instance
example (f : α → β → γ → δ) [IsSmooth f] (b : β) : IsSmooth (λ a c => f a b c) := by infer_instance
example (f : α → β → γ → δ) [IsSmooth f] (c : γ) : IsSmooth (λ a b => f a b c) := by infer_instance
example (f : α → β → γ → δ) (b : β) [IsSmooth (λ a => f a b)] : IsSmooth (λ a c => f a b c) := by infer_instance
example (f : α → β → γ) (g : δ → ε → α) (h : δ → ε → β) [IsSmooth f] [∀ a, IsSmooth (f a)] [IsSmooth g] [IsSmooth h] : IsSmooth (λ x y => f (g x y) (h x y)) := by infer_instance
example (f : β → δ → γ) (g : α → β) [IsSmooth f] [∀ b, IsSmooth (f b)] [IsSmooth g] (a : α): IsSmooth (λ (h : α → δ) => f (g a) (h a)) := by infer_instance
example (f : β → δ → γ) (h : α → δ) [IsSmooth f] : IsSmooth (λ (g : α → β) a => f (g a) (h a)) := by infer_instance
example (f : β → δ → γ) [IsSmooth f] (d : δ) : IsSmooth (λ (g : α → β) a => f (g a) d) := by infer_instance
example (f : β → γ) (g : β → β) [IsSmooth f] [IsSmooth g] : IsSmooth (fun x => f (g (g x))) := by infer_instance
example (f : α → β → γ) [∀ a, IsSmooth (f a)] : IsSmooth (λ b a => f a b) := by infer_instance
example (f : α → β → γ → δ) [∀ a b, IsSmooth (f a b)] : IsSmooth (λ c a b => f a b c) := by infer_instance
example (f : α → β → γ → δ → ε) [∀ a b c, IsSmooth (f a b c)] : IsSmooth (λ d a b c => f a b c d) := by infer_instance
example (f : β → δ → γ) [IsSmooth f] (g : α → β) [IsSmooth g] (d : δ) : IsSmooth (λ a => f (g a) d) := by infer_instance
example (f : β → δ → γ) [IsSmooth f] (g : α → β) [IsSmooth g] : IsSmooth (λ a d => f (g a) d) := by infer_instance
example (f : δ → β → γ) [∀ d, IsSmooth (f d)] (g : α → β) [IsSmooth g] : IsSmooth (λ a d => (f d (g a))) := by infer_instance

Any thoughts on this? Is it a good idea to add this to lean?

[Floris van Doorn]

I somehow completely missed this post.
This looks amazing! This would be incredibly useful for a lot of predicates on functions in mathlib.

[Mac]

@Tomas Skrivan seems very cool! Does it pass all the tests? If so, why not PR it to Lean? You have already written the changes so there is little cost and it would likely be more easily noticed by @Sebastian Ullrich or @Leonardo de Moura.

[Tomas Skrivan]

Yes it passes all tests, but I know it is breakable by some intricate classes with dependent types. Should be fairly easy to fix and then I can make a PR, I just didn't have time to do it yet. Also I do not fully understand the whole TC resolution, so I thought I keep testing it before PR.

[Tomas Skrivan]

Yes and I find it very very useful. I'm writing automatic differentiation tool with it where I use the TC system to prove that certain functions are smooth, linear, invertible. I can almost do symbolic calculations in variational calculus like deriving Euler-Lagrange equation by taking gradient of action, not completely there yet but soon.

[Leonardo de Moura]

@Tomas Skrivan This looks very interesting. Thanks for investigating the issue and finding a solution. I am currently busy with boring stuff (slides, proposal writing, etc), but I will try to find time during the weekend to go over your code. Could you please add comments and any other information it may be relevant?

[Sebastian Ullrich]

If you open a PR, we can also check if there are any (significant) performance regressions

[Tomas Skrivan]

I will explain and comment the code, but I'm away from a computer for the next three days so I can't touch the code or make a PR.

[Tomas Skrivan]

@Leonardo de Moura Let me explain how it works.

The main problem is to deal with instances of type a : A -> C where a does not appear in class C. When you look for such an instance it is enough to look for an instance c : C and then return fun _ => c.

My solution makes sure that instance of a type like a : A -> C never gets tabled/cached. More on that later.

At the core is the function removeUnusedArguments, it takes an expression E and does two things:

1. Removes unused arguments producing E', for example
a : A -> C to C
a1 : A1 -> a2 : A2 -> C a1 to a1 : A1 -> C a1
a1 : A1 -> a2 : A2 -> a3 : A3 a1 -> C a3 to a1 : A1 -> a3 : A3 a1 -> C a3 (this does not work and need to be fixed)

2. Creates a function to do the reverse transformation E' -> E, for example:
C -> (a : A -> C)
(a1 : A1 -> C a1) -> (a1 : A1 -> a2 : A2 -> C a1)

The modification to TC resolution works this way: We are looking for an instance of E, if it is tabled just get it as normal, but if not first remove all unused arguments producing E'. Now we look up the table again but for E'. If it exists, use the map E' -> E to create E. If it does not exists, create a new goal E'.

Maybe as an optimization, E can be added to the table too, but I do not know how to setup proper dependency on E', i.e. correct generator, waiter and consumer nodes.

I have also added few comment to the code. Let me know if something is unclear.

[Tomas Skrivan]

I have created a pull request

Unfortunately, I have messed up few things on my github, so my code comments disappeared. I will try to comment the code again at some point.

[Mauricio Collares]

If you ever committed the comments, git reflog probably still lists those commits even if you overwrote them later

[Tomas Skrivan]

Well I have managed to make a mess with few branches and stupid commits. So I thought that the easiest thing to do in order to clean in up and submit a nice pull request would be to delete the github repo and fork it again :)