fun_prop?

Stream: Is there code for X?

[Filippo A. E. Nuccio]

For pedagogical reasons, I'd like to show what term has been created by a call of fun_prop, in the same vein as one could do continuity?, but fun_prop? does not exist (and show_term{fun_prop} does not work). Is there a workaround?

[Kenny Lau]

do you have a mwe for "show_term fun_prop doesn't work"?

[Filippo A. E. Nuccio]

import Mathlib.Topology.Continuous
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

example : Continuous (fun (x : ℝ) ↦ sin (2 * x)) := by
  show_term{fun_prop}

[Filippo A. E. Nuccio]

I get

found a proof, but the corresponding tactic failed:
  (expose_names; exact Continuous.comp' continuous_sin
    (Continuous.comp' (Continuous.mul (Continuous.fst continuous_id') (Continuous.snd continuous_id'))
      (Continuous.prodMk continuous_const continuous_id')))

It may be possible to correct this proof by adding type annotations, explicitly specifying implicit arguments, or eliminating unnecessary function abstractions.

[Filippo A. E. Nuccio]

you might say that the term is somewhat hidden there, but not in a nice, clickable form

[Kenny Lau]

import Mathlib.Topology.Continuous
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

open Real
example : Continuous (fun (x : ℝ) ↦ sin (2 * x)) := by?
  fun_prop

[Filippo A. E. Nuccio]

WOWOW, the by? was totally unknown to me. Thanks!

[Filippo A. E. Nuccio]

Is it documented somewhere?

[Robin Arnez]

... it still doesn't work, it just doesn't tell you beforehand

[Robin Arnez]

Try set_option pp.analyze true

[Robin Arnez]

import Mathlib.Topology.Continuous
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

open Real

example : Continuous (fun (x : ℝ) ↦ sin (2 * x)) := by
  set_option pp.analyze true in
  show_term fun_prop

works

[Kenny Lau]

that sounds like an implementation detail that shouldn't appear...

[Filippo A. E. Nuccio]

Yes, with this it indeed works because it adds the type annotation of the identity function

[Kenny Lau]

can we toggle this option on by default when calling by? or show_term?

[Filippo A. E. Nuccio]

This would be great, yes.

[Filippo A. E. Nuccio]

(for my class, I can just hide the set_option at the very beginning of the file and mumble something about it being " like an import", but it is suboptimal)

[ZhiKai Pong]

set_option trace.Meta.Tactic.fun_prop true

allows you to follow what is used

[Riccardo Brasca]

You can do

import Mathlib.Topology.Continuous
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

open Real
theorem foo : Continuous (fun (x : ℝ) ↦ sin (2 * x)) := by
  fun_prop

#print foo

[Riccardo Brasca]

Hmm, copying/pasting the proof doesn't work, it's probably the same output as by?

[Filippo A. E. Nuccio]

ZhiKai Pong said:

set_option trace.Meta.Tactic.fun_prop true

Yes, this I knew, but it is way less efficient than by? ( with the right option), because you cannot click. Thanks anyway!

[Ruben Van de Velde]

Yeah, I think those are all the same thing