fun_prop issues

Stream: mathlib4

[Jireh Loreaux]

@Tomas Skrivan I have a failing case for fun_prop I'm hoping you have a quick fix for.

import Mathlib

example {X : Type*} [TopologicalSpace X] {f : X → X} {x : X}
    (hf : ContinuousAt f x) (hx : f x = x) (n : ℕ) :
    ContinuousAt f^[n] x :=
  Nat.recOn n continuousAt_id fun n ihn => by
    rw [Function.iterate_succ, Function.comp]
    rw [← hx] at ihn
    apply ContinuousAt.comp'
    sorry -- `fun_prop` fails to find the hypothesis `ihn` in context.
    fun_prop

[Yury G. Kudryashov]

If you're going to add this lemma to the library, then could you please add a more general version?

protected theorem Filter.Tendsto.iterate {α : Type*} {l : Filter α} {f : α → α} (hf : Tendsto f l l) (n : Nat) :
    Tendsto (f^[n]) l l

The ContinuousAt version follows by some simp(a)

[Jireh Loreaux]

This lemma is already in the library as docs#ContinuousAt.iterate, I'm just trying out fun_prop in various places to see what it's capable of.

[Yury G. Kudryashov]

I'm going to add the generic Tendsto version so that we can use it, e.g., for l = atTop.

[Tomas Skrivan]

I see, this should be relatively easy to fix.

When writing the tactic I wasn't thinking about recursively defined functions at all. They might break the tactic in more ways :)

[Tomas Skrivan]

I'm also thinking allowing to specify a custom normalization of the goal. Right now, there is no normalization going on(some unfolding and beta reduction).

What about proving it with induction n <;> (simp[Nat.iterate]; fun_prop (normalization:=rw[hx])) ?

Currently induction n <;> (simp[Nat.iterate]; fun_prop) stops on ContinuousAt (fun x3 => f^[n] x3) (f x). To continue it would need to somehow apply hx to rewrite the f x to x.

[Jireh Loreaux]

I'm not asking for fun_prop to do the whole thing, just for it to see the hypothesis ihn. I thought it might be a missing withMainContext somewhere.

[Tomas Skrivan]

Nope, because the goal is ContinuousAt (Nat.iterate f n) x it is looking for facts about Nat.iterate. Right now, it does not look in the local context for constants.

[Jireh Loreaux]

Oh I see

[llllvvuu]

I found another test case:

import Mathlib

set_option trace.Meta.Tactic.fun_prop true

lemma test_case : DifferentiableOn ℂ (fun (x : ℂ) ↦ 1 * x) ({0}ᶜ : Set ℂ) := by
  try fun_prop
  apply DifferentiableOn.mul
  · apply differentiableOn_const
  · apply differentiableOn_id

[Meta.Tactic.fun_prop] [❌] DifferentiableOn ℂ (fun x ↦ 1 * x) {0}ᶜ ▼
  [] applicable theorems for HMul.hMul: [DifferentiableOn.mul]
  [] [❌] applying: DifferentiableOn.mul ▼
    [] [❌] DifferentiableOn ℂ (fun y ↦ 1) {0}ᶜ ▼
      [] [❌] applying: differentiableOn_const