feat: fun_prop tactic for proving Continuous, Differentiable, Measurable, ... (#10040)

New tactic `fun_prop` to prove FUNction PROPerties like continuity, differentiability, ...

Author: lecopivo

Mathlib.lean

@@ -3388,6 +3388,23 @@ import Mathlib.Tactic.FailIfNoProgress
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.FinCases
 import Mathlib.Tactic.Find
+import Mathlib.Tactic.FunProp
+import Mathlib.Tactic.FunProp.AEMesurable
+import Mathlib.Tactic.FunProp.Attr
+import Mathlib.Tactic.FunProp.ContDiff
+import Mathlib.Tactic.FunProp.Continuous
+import Mathlib.Tactic.FunProp.Core
+import Mathlib.Tactic.FunProp.Decl
+import Mathlib.Tactic.FunProp.Differentiable
+import Mathlib.Tactic.FunProp.Elab
+import Mathlib.Tactic.FunProp.FunctionData
+import Mathlib.Tactic.FunProp.Measurable
+import Mathlib.Tactic.FunProp.Mor
+import Mathlib.Tactic.FunProp.RefinedDiscrTree
+import Mathlib.Tactic.FunProp.StateList
+import Mathlib.Tactic.FunProp.Theorems
+import Mathlib.Tactic.FunProp.ToStd
+import Mathlib.Tactic.FunProp.Types
 import Mathlib.Tactic.GCongr
 import Mathlib.Tactic.GCongr.Core
 import Mathlib.Tactic.GCongr.ForwardAttr

Mathlib/Lean/Expr/Basic.lean

@@ -324,18 +324,21 @@ def modifyAppArgM [Functor M] [Pure M] (modifier : Expr → M Expr) : Expr → M
   | app f a => mkApp f <$> modifier a
   | e => pure e
 
-def modifyAppArg (modifier : Expr → Expr) : Expr → Expr :=
-  modifyAppArgM (M := Id) modifier
-
 def modifyRevArg (modifier : Expr → Expr) : Nat → Expr → Expr
-  | 0 => modifyAppArg modifier
-  | (i+1) => modifyAppArg (modifyRevArg modifier i)
+  | 0,     (.app f x) => .app f (modifier x)
+  | (i+1), (.app f x) => .app (modifyRevArg modifier i f) x
+  | _, e => e
 
 /-- Given `f a₀ a₁ ... aₙ₋₁`, runs `modifier` on the `i`th argument or
 returns the original expression if out of bounds. -/
 def modifyArg (modifier : Expr → Expr) (e : Expr) (i : Nat) (n := e.getAppNumArgs) : Expr :=
   modifyRevArg modifier (n - i - 1) e
 
+/-- Given `f a₀ a₁ ... aₙ₋₁`, sets the argument on the `i`th argument to `x` or
+returns the original expression if out of bounds. -/
+def setArg (e : Expr) (i : Nat) (x : Expr) (n := e.getAppNumArgs) : Expr :=
+  e.modifyArg (fun _ => x) i n
+
 def getRevArg? : Expr → Nat → Option Expr
   | app _ a, 0   => a
   | app f _, i+1 => getRevArg! f i

Mathlib/Tactic.lean

@@ -51,6 +51,23 @@ import Mathlib.Tactic.FailIfNoProgress
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.FinCases
 import Mathlib.Tactic.Find
+import Mathlib.Tactic.FunProp
+import Mathlib.Tactic.FunProp.AEMesurable
+import Mathlib.Tactic.FunProp.Attr
+import Mathlib.Tactic.FunProp.ContDiff
+import Mathlib.Tactic.FunProp.Continuous
+import Mathlib.Tactic.FunProp.Core
+import Mathlib.Tactic.FunProp.Decl
+import Mathlib.Tactic.FunProp.Differentiable
+import Mathlib.Tactic.FunProp.Elab
+import Mathlib.Tactic.FunProp.FunctionData
+import Mathlib.Tactic.FunProp.Measurable
+import Mathlib.Tactic.FunProp.Mor
+import Mathlib.Tactic.FunProp.RefinedDiscrTree
+import Mathlib.Tactic.FunProp.StateList
+import Mathlib.Tactic.FunProp.Theorems
+import Mathlib.Tactic.FunProp.ToStd
+import Mathlib.Tactic.FunProp.Types
 import Mathlib.Tactic.GCongr
 import Mathlib.Tactic.GCongr.Core
 import Mathlib.Tactic.GCongr.ForwardAttr

Mathlib/Tactic/FunProp.lean

@@ -0,0 +1,11 @@
+import Mathlib.Tactic.FunProp.Attr
+import Mathlib.Tactic.FunProp.Core
+import Mathlib.Tactic.FunProp.Decl
+import Mathlib.Tactic.FunProp.Elab
+import Mathlib.Tactic.FunProp.FunctionData
+import Mathlib.Tactic.FunProp.Mor
+import Mathlib.Tactic.FunProp.RefinedDiscrTree
+import Mathlib.Tactic.FunProp.StateList
+import Mathlib.Tactic.FunProp.Theorems
+import Mathlib.Tactic.FunProp.ToStd
+import Mathlib.Tactic.FunProp.Types

Mathlib/Tactic/FunProp/AEMesurable.lean

@@ -0,0 +1,85 @@
+/-
+Copyright (c) 2024 Tomáš Skřivan All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tomáš Skřivan
+-/
+import Mathlib.MeasureTheory.Measure.AEMeasurable
+import Mathlib.MeasureTheory.Constructions.Prod.Basic
+import Mathlib.MeasureTheory.Constructions.Pi
+import Mathlib.MeasureTheory.Measure.Haar.OfBasis
+
+import Mathlib.Tactic.FunProp
+import Mathlib.Tactic.FunProp.Measurable
+
+/-!
+## `fun_prop` minimal setup for AEMeasurable
+-/
+
+
+section missing
+
+open MeasureTheory
+
+variable {ι α β γ δ R : Type*} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ]
+  [MeasurableSpace δ] {f g : α → β} {μ ν : Measure α}
+
+theorem AEMeasurable.comp_aemeasurable' {f : α → δ} {g : δ → β} (hg : AEMeasurable g (μ.map f))
+    (hf : AEMeasurable f μ) : AEMeasurable (fun x => g (f x)) μ := comp_aemeasurable hg hf
+
+end missing
+
+open Mathlib
+
+-- mark definition
+attribute [fun_prop]
+  AEMeasurable
+
+-- lambda rules
+attribute [fun_prop]
+  aemeasurable_id'
+  aemeasurable_const
+  AEMeasurable.comp_aemeasurable'
+  -- Measurable.comp_aemeasurable'
+  -- AEMeasurable_apply -- is this somewhere?
+  -- AEMeasurable_pi -- is this somewhere?
+
+-- product
+attribute [fun_prop]
+  AEMeasurable.prod_mk
+  AEMeasurable.fst
+  AEMeasurable.snd
+
+-- algebra
+attribute [fun_prop]
+  AEMeasurable.add
+  AEMeasurable.sub
+  AEMeasurable.mul
+  AEMeasurable.neg
+  AEMeasurable.div
+  AEMeasurable.inv
+  AEMeasurable.smul
+
+-- transitions
+attribute [fun_prop]
+  AEMeasurable.mono'
+  Measurable.aemeasurable
+
+
+attribute [fun_prop]
+  AEMeasurable.mono'
+  Measurable.aemeasurable
+
+
+-- Notice that no theorems about measuability of log are used. It is infered from continuity.
+example : AEMeasurable (fun x => x * (Real.log x) ^ 2 - Real.exp x / x) :=
+  by fun_prop
+
+private noncomputable def S (a b c d : ℝ) : ℝ :=
+    a / (a + b + d) + b / (a + b + c) +
+    c / (b + c + d) + d / (a + c + d)
+
+private noncomputable def T (t : ℝ) : ℝ := S 1 (1 - t) t (t * (1 - t))
+
+example : AEMeasurable T := by
+  unfold T S
+  fun_prop

Mathlib/Tactic/FunProp/Attr.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2024 Tomas Skrivan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tomas Skrivan
+-/
+import Lean
+
+import Mathlib.Tactic.FunProp.Decl
+import Mathlib.Tactic.FunProp.Theorems
+
+/-!
+## `funProp` attribute
+-/
+
+
+namespace Mathlib
+open Lean Meta
+
+namespace Meta.FunProp
+
+-- TODO: add support for specifying priority and discharger
+-- open Lean.Parser.Tactic
+-- syntax (name:=Attr.funProp) "funProp" (prio)? (discharger)? : attr
+
+private def funPropHelpString : String :=
+"`funProp` tactic to prove function properties like `Continuous`, `Differentiable`, `IsLinearMap`"
+
+/-- Initialization of `funProp` attribute -/
+initialize funPropAttr : Unit ←
+  registerBuiltinAttribute {
+    name  := `fun_prop
+    descr := funPropHelpString
+    applicationTime := AttributeApplicationTime.afterCompilation
+    add   := fun declName _stx attrKind =>
+       discard <| MetaM.run do
+       let info ← getConstInfo declName
+
+       forallTelescope info.type fun _ b => do
+         if b.isProp then
+           addFunPropDecl declName none
+         else
+           addTheorem declName attrKind
+    erase := fun _declName =>
+      throwError "can't remove `funProp` attribute (not implemented yet)"
+  }