Rules for not fully applied constants

[lecopivo]

There is an issue when writing rules that do not contain fully applied constant.

For example for (f : X → Y → Z) (x dx : X) (z : Z), this expression has fully applied invFun

∂ (x':=x;dx), invFun (f x) z

but this expression does not have fully applied invFun

(∂ (x':=x;dx), invFun (f x)) z

We should be able to pull the argument z in and out when differentiating. Currently this does not work.

---

Potential solution:

1. Require that all rules are written in fully applied form. When applying rules we might have to eta unexpand expressions to introduce new arguments. After eta unexpand, we probably immediately apply pi_rule.
2. Support rules in not fully applied form. When applying rules and there are only rules for less applied for, we apply proj_rule to remove applied argument

---

Make this work:

import SciLean.Core

open SciLean

variable 
  {K} [IsROrC K]
  {X Y Z W} [Vec K X] [Vec K Y] [Vec K Z] [Vec K W]

def inv1 (f : X → Y) (y : Y) : X := sorry
def inv2 (f : X → Y) (y : Y) : X := sorry

variable (f : X → Y → Z) (z : Z)

@[fprop]
theorem inv1.arg_f.IsDifferentiable_rule
  : IsDifferentiable K (fun x => inv1 (f x)) := sorry

@[ftrans]
theorem inv1.arg_f.cderiv_rule
  : cderiv K (fun x => inv1 (f x))
    =
    fun x dx z => 
      let y := inv1 (f x) z
      let dfdx_y := cderiv K f x dx y 
      let df'dy := cderiv K (inv1 (f x)) (f x y) (dfdx_y)
      (-df'dy) := sorry

@[fprop]
theorem inv2.arg_f.IsDifferentiable_rule
  : IsDifferentiable K (fun w => inv2 (f w) y) := sorry

@[ftrans]
theorem inv2.arg_f.cderiv_rule
  : cderiv K (fun x => inv2 (f x) z)
    =
    fun x dx => 
      let y := inv2 (f x) z
      let dfdx_y := cderiv K f x dx y 
      let df'dy := cderiv K (inv2 (f x)) (f x y) (dfdx_y)
      (-df'dy) := sorry


-- works
example : IsDifferentiable K (fun w => inv1 (f w)) := by fprop 
example : IsDifferentiable K (fun w => inv2 (f w) y) := by fprop 

example : cderiv K (fun x => inv1 (f x))
          =
          fun x dx z => 
            let y := inv1 (f x) z
            let dfdx_y := cderiv K f x dx y 
            let df'dy := cderiv K (inv1 (f x)) (f x y) (dfdx_y)
            (-df'dy) := by ftrans

example : cderiv K (fun x => inv2 (f x) z)
          =
          fun x dx => 
            let y := inv2 (f x) z
            let dfdx_y := cderiv K f x dx y 
            let df'dy := cderiv K (inv2 (f x)) (f x y) (dfdx_y)
            (-df'dy) := by ftrans


-- does not work
example : IsDifferentiable K (fun w => inv1 (f w) y) := by fprop
example : IsDifferentiable K (fun w => inv2 (f w)) := by fprop

example : cderiv K (fun x => inv1 (f x) z)
          =
          fun x dx => 
            let y := inv1 (f x) z
            let dfdx_y := cderiv K f x dx y 
            let df'dy := cderiv K (inv1 (f x)) (f x y) (dfdx_y)
            (-df'dy) := by ftrans

example : cderiv K (fun x => inv2 (f x))
          =
          fun x dx z => 
            let y := inv2 (f x) z
            let dfdx_y := cderiv K f x dx y 
            let df'dy := cderiv K (inv2 (f x)) (f x y) (dfdx_y)
            (-df'dy) := by ftrans

[lecopivo]

The next to last problem in the set file is does not work because of missing fun_trans feature.