search

lecopivo / SciLean

Scientific computing in Lean 4
https://lecopivo.github.io/scientific-computing-lean/
Apache License 2.0
327 stars 29 forks source link

unification issue with overly applied constant #22

Closed lecopivo closed 1 year ago

lecopivo commented 1 year ago

Applying ftrans/fprop rules fails when a constant has more applied arguments then its normal number of arguments. For example Prof.fst has only one argument but Prod.fst (f,g) x has two applied arguments.

This issue is effectively a reverse situation of #9 when there are too few applied arguments

This should work

import SciLean

open SciLean

variable 
  {K : Type _} [IsROrC K]
  {α : Type _}

set_option trace.Meta.Tactic.simp.unify true
example (i : α) : IsDifferentiable K (fun (xy : (α → K) × (α → K)) => xy.fst i) := by fprop

set_option trace.Meta.Tactic.simp.unify true
example (i : α) 
  : cderiv K (fun (xy : (α → K) × (α → K)) => xy.fst i)
    =
    fun xy dxy => 
      dxy.1 i := by ftrans only