command to generate linear map

[lecopivo]

There should be a command that that generates theorems for linear maps.

For

def foo {X Y} [Vec K X] [Vec K Y] (x : X) : Y := ...

there should be a command

#generate_linear_map foo x by tac

that generates

@[fprop]
theorem foo.IsLinearMap_rule_simple : IsLinearMap K foo := by tac

@[fprop]
theorem foo.IsLinearMap_rule (f : W → X) [hf : IsLinearMap K f] 
  : IsLinearMap K (fun w => foo (f w)) := ...

@[add_pull] 
theorem foo.add_pull (x x' : X) : foo (x + x') = f x + f x' := ...

@[add_pull] 
theorem foo.add_push (x x' : X) : f x + f x' = foo (x + x') := ...

@[smul_pull] 
theorem foo.smul_pull (k : K) (x : X) : foo (k • x) = k • foo x := ...

@[smul_push] 
theorem foo.smul_push (k : K) (x : X) : k • foo x = foo (k • x) := ...

@[simp, ftrans_simp] 
theorem foo.zero : foo 0 = 0 := ...

For smooth linear maps there should be

#generate_smooth_linear_map foo x 
  linear_by tac
  smooth_by tac'

which in addition to the above generates also

@[fprop]
theorem foo.IsSmoothLinearMap_rule_simple : IsSmoothLinearMap K foo := ⟨by tac,by tac'⟩

@[fprop]
theorem foo.IsSmoothLinearMap_rule (f : W → X) (hf : IsSmoothLinearMap K f)
  : IsLinearMap K (fun w => foo (f w)) := ...

@[fprop]
theorem foo.IsDifferentiable_rule (f : W → X) (hf : IsDifferentiable K f)
  : IsDifferentiable K (fun w => foo (f w)) := ...

@[ftrans]
theorem foo.cderiv_rule (f : W → X) (hf : IsDifferentiable K f)
  : cderiv (fun w => foo (f w)) 
    =
    fun w dw =>
      let dx := ceriv f w dw
      foo dx := ...
 
@[ftrans]
theorem foo.fwdCDeriv_rule (f : W → X) (hf : IsDifferentiable K f)
  : fwdCDeriv (fun w => foo (f w)) 
    =
    fun w dw =>
      let (x,dx) := ceriv f w dw
      (foo x, foo dx) := ...

Example for function with multiple arguments

def add {X} [Vec K X] (x y : X) : X := x + y
#generate_linear_map add x y by tac

example of generated theorems

@[fprop]
theorem add.IsLinearMap_rule 
  (f g : W → X) (hf : IsLinearMap K f) (hg : IsLinearMap K g)
  : IsLinearMap K (fun w => add (f w) (g w)) := ...

@[add_pull] 
theorem add.add_pull (x x' y y' : X) : add (x + x') (y + y') = add x y + add x' y' := ...