Talk: Basic Tactics

Stream: LFTCM 2024

[Jireh Loreaux]

This is a thread for Alex's talk on Basic Tactics

[Jireh Loreaux]

Alex mentioned that you can prove the statement in his talk about continuous functions with the continuity tactic. One can also try the fun_prop tactic for proving simple statements about continuity, which should be faster. Mathlib is currently transitioning from the former to the latter for performance reasons (and other reasons as well). In this particular case, continuity succeeds, but fun_prop fails. This is only because no one has yet told the fun_prop tactic that sin and cos are continuous. Once we tell it that (I've done that using the attribute line below), it succeeds.

import Mathlib

open Real

attribute [fun_prop] continuous_cos continuous_sin

example : Continuous (fun x ↦ sin (x ^ 2) ^ 3 * cos (5 * x)) := by
  fun_prop

[Riccardo Brasca]

@Jireh Loreaux what was your suggestion about numeric types?

[Jireh Loreaux]

set_option pp.numericTypes true will show in the infoview what type a numeral has, so instead of showing 5, it will show 5 : ℕ or 5 : ℝ.

[Jireh Loreaux]

This is very helpful for new users I suspect (and for experienced ones too sometimes!)

[Riccardo Brasca]

A numeral is essentially an expression made of digits, like 3432523534. Lean has a special support to understand that those are natural/real/complex/... numbers

[Filippo A. E. Nuccio]

Jireh Loreaux said:

set_option pp.numericTypes true will show in the infoview what type a numeral has, so instead of showing 5, it will show 5 : ℕ or 5 : ℝ.

Just to complement to @Jireh Loreaux 's comment: if you want to use one of these set_option tools, you should use them outside proofs, not inside them. Just before the lemma/def you are working on, basically, on a new line.

[Vincent Beffara]

Where can we find documentation on fun_prop?