linearity of functions

Stream: general

[Eric Wieser]

Can't you prove \lam a f x, L a (f x) is tri-linear by proving it's separately linear in each argument?

• Linear in a; use apply_linear, L.is_linear
• Linear in f; use L.is_linear2, apply_linear
• Linear in x; use L.is_linear2, f.is_linear

[Eric Wieser]

(I moved this to a new thread, feel free to rename it)

[Tomas Skrivan]

I Lean 4 you can abuse type class system to automatically prove linearity/continuity of lambda functions. Here are the core instances that tear each lambda into its atomic function: https://github.com/lecopivo/SciLean/blob/master/SciLean/Core/Mor/IsLin/Core.lean
Those instances vaguely correspond to SKI combinators.

To deal with addition and alike I use the fact that uncurried add is linear:

instance diag_parm.arg_x.isLin (f : Y₁ → Y₂ → Z) [IsLin (λ yy : Y₁ × Y₂ => f yy.1 yy.2)] (g₁ : X → α → Y₁) [IsLin g₁] (g₂ : X → α → Y₂) [IsLin g₂] : IsLin (λ x a => f (g₁ x a) (g₂ x a)) := sorry

However, there are some issues with higher order unification so you need to add certain class instances manually, when f has additional trailing argument, example:

instance (priority := mid-1) subst.arg_x.parm_a.isSmooth (a : α) (f : X → Y → α → Z) [IsSmooth (λ x y => f x y a)] [∀ x, IsSmooth (λ y => f x y a)] (g : X → Y) [IsSmooth g] : IsSmooth (λ x => f x (g x) a) := by try infer_instance apply subst.arg_x.isSmooth (λ x y => f x y a) done

It is trivialy solvable by direct application of a previous instance, but Lean is unable to do it automatically. I'm still unsure what is the general pattern of these "additional instances"

[Tomas Skrivan]

A quick test for something like \la p, matrix.trace (f p.1 + g p.2):

example {X Y Z W} [Vec X] [Vec Y] [Vec Z] [Vec W]
  (f : X → Z) [IsLin f]
  (g : Y → Z) [IsLin g]
  (h : Z → W) [IsLin h]
  : IsLin (λ p : (X × Y) => h (f p.1 + g p.2)) := by infer_instance

A part of the trace that shows the sequence of reasoning:

[Meta.synthInstance] main goal IsLin fun p => h (f p.fst + g p.snd)
[Meta.synthInstance.newAnswer] size: 1, IsLin fun yy => yy.fst + yy.snd
[Meta.synthInstance.newAnswer] size: 0, IsLin f
[Meta.synthInstance.newAnswer] size: 2, IsLin fun p => p.fst
[Meta.synthInstance.newAnswer] size: 7, IsLin fun p => f p.fst
[Meta.synthInstance.newAnswer] size: 0, IsLin g
[Meta.synthInstance.newAnswer] size: 2, IsLin fun p => p.snd
[Meta.synthInstance.newAnswer] size: 7, IsLin fun p => g p.snd
[Meta.synthInstance.newAnswer] size: 22, IsLin fun p => f p.fst + g p.snd
[Meta.synthInstance.newAnswer] size: 27, IsLin fun p => h (f p.fst + g p.snd)

[Tomas Skrivan]

The requirement that a variable appears only once is too harsh, for example this is also a linear function:

example {X Y Z} [Vec X] [Vec Y] [Vec Z]
  (f g : X → Y) [IsLin f] [IsLin g]
  (h : Y → Z) [IsLin h]
  : IsLin (λ p : (X × Y) => h (f p.1 + g p.1)) := by infer_instance

[Eric Wieser]

Note that we actually used to have such a typeclass system in lean3 (docs#is_add_monoid_hom etc), but it didn't behave well with the simplifier or composition

[Tomas Skrivan]

Do you have an example of problematic cases? It works quite well for me in Lean 4, and and main use case is exactly to steer simplifier when applying theorems.

[Tomas Skrivan]

I remember reading Use and abuse of instance parameters in the Lean mathematical library which states that the unbundled approach for morphisms was problematic for mathlib3.

[Eric Wieser]

I don't know what the canonical reference is for that problem, it was discovered quite a while ago. It's entirely possible that the problem is not as bad in Lean 4.

[Tomas Skrivan]

I know that my approach is impossible in lean3 as it is heavily relaying on the new type class system's ability handling cycles.

[Tomas Skrivan]

I can also do the tri-linearity of \lam a f x, L a (f x). The only catch if that for linearity in x you need to set f type to bundled linear map, in my notation W ⊸ Y:

  variable {W X Y Z : Type} [Vec W] [Vec X] [Vec Y] [Vec Z]
  variable (L : X → Y → Z) [IsLin L] [∀ x, IsLin (L x)]

  example : IsLin (λ (x : W) (f : W ⊸ Y) (a : X) => L a (f x)) := by infer_instance
  example : IsLin (λ (a : X) (f : W → Y) (x : W) => L a (f x)) := by infer_instance
  example : IsLin (λ (f : W → Y) (a : X) (x : W) => L a (f x)) := by infer_instance

[Kevin Buzzard]

Yes I thought the whole point of hanging on to the deprecated lean 3 version of this was that people were aware that it might come back into play in lean 4