fprop tactic and modifying simp cache

Stream: lean4

[Tomas Skrivan]

I want to do some symbolic algebra and program transformation. I was running into issues that using typeclasses and/or aesop for proving linearity, continuity, differentiability is too slow. So I wrote my own tactic fprop(function property/proposition). For example proving:

example : Continuous (fun x : ℝ =>
  let x1 := x
  let x2 := x + x1
  let x3 := x + x1 + x2
  let x4 := x + x1 + x2 + x3
  let x5 := x + x1 + x2 + x3 + x4
  let x6 := x + x1 + x2 + x3 + x4 + x5
  let x7 := x + x1 + x2 + x3 + x4 + x5 + x6
  x7) := ...

by aesop it takes around one second and by fprop around 25ms. Would there be interest adding this to mathlib? Here is the file setting up Continuous for fprop.

---

Now the question about the cache. I want to use this tactic as a discharger in simp and I want to cache its results. Can I reuse simp's cache? I'm unable to understand how exactly simp handles propositions. It seems to me that simp somehow rewrites propositions to True.

Should I modify simp's cache like this?

  let mut c : Lean.Meta.Simp.Cache := sorry
  let P : Expr := q(Continuous fun x : ℝ => x)
  c := c.insert P {
    expr := q(True)
    proof? := q(eq_true (continuous_id' (α:=ℝ)))
  }

I'm not sure if the proof should be the proof of Continuous fun x : ℝ => x or of (Continuous fun x : ℝ => x) = True.

Also should I worry about free variables in P and in proof?? If simp goes inside of lambda or let, it introduces free variables and those would end up in the cache. Simp has to deal with this problem somehow but it is not clear to me how.

[James Gallicchio]

(deleted)