search

leanprover-community / aesop

White-box automation for Lean 4
Apache License 2.0
155 stars 24 forks source link

Aesop ruleset runs forever #94

Open adomasbaliuka opened 5 months ago

adomasbaliuka commented 5 months ago

In the following example, aesop does not terminate (for at least 20 minutes). Besides my hope that aesop might actually solve the goal, is "running forever" an intended behavior? This is the first time I've seen where it doesn't quickly run out of "iterations" or heartbeats or something.

The example arose while making a differentiability tactic, like Mathlib's current continuity. For reproducing the issue, cheking out the Mathlib PR may be convenient.

-- Init.lean
import Aesop
declare_aesop_rule_sets [Differentiable]
import Init -- the file above
import Mathlib

attribute [aesop (rule_sets [Differentiable]) unfold norm] Function.comp

attribute [local aesop safe 2 apply (rule_sets [Differentiable])]
    Differentiable.sum  -- Mathlib.Analysis.Calculus.FDeriv.Add
    Differentiable.sub  -- Mathlib.Analysis.Calculus.FDeriv.Add
    Differentiable.add  -- Mathlib.Analysis.Calculus.FDeriv.Add
    Differentiable.mul  -- Mathlib.Analysis.Calculus.FDeriv.Mul
    Differentiable.star  -- Mathlib.Analysis.Calculus.FDeriv.Star
    Differentiable.smul  -- Mathlib.Analysis.Calculus.FDeriv.Mul
    Differentiable.comp

attribute [local aesop safe apply (rule_sets [Differentiable])]
    -- Differentiable.norm  -- Mathlib.Analysis.InnerProductSpace.Calculus
    Differentiable.norm_sq  -- Mathlib.Analysis.InnerProductSpace.Calculus
    -- SchwartzMap.differentiable  -- Mathlib.Analysis.Distribution.SchwartzSpace
    Differentiable.inner  -- Mathlib.Analysis.InnerProductSpace.Calculus
    -- AffineMap.differentiable  -- Mathlib.Analysis.Calculus.Deriv.AffineMap
    Differentiable.clm_comp  -- Mathlib.Analysis.Calculus.FDeriv.Mul
    Differentiable.clm_apply  -- Mathlib.Analysis.Calculus.FDeriv.Mul
    Differentiable.arsinh  -- Mathlib.Analysis.SpecialFunctions.Arsinh
    Differentiable.exp  -- Mathlib.Analysis.SpecialFunctions.ExpDeriv
    Differentiable.cexp  -- Mathlib.Analysis.SpecialFunctions.ExpDeriv
    Differentiable.log  -- Mathlib.Analysis.SpecialFunctions.Log.Deriv
    Real.differentiable_rpow_const  -- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
    Differentiable.rpow_const  -- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
    Differentiable.sin  -- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
    Differentiable.cos  -- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
    Real.differentiable_cos  -- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
    Real.differentiable_cosh  -- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
    Real.differentiable_sin  -- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
    Real.differentiable_sinh  -- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
    Differentiable.ccos  -- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
    Differentiable.ccosh  -- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
    Differentiable.cosh  -- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
    Differentiable.csin  -- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
    Differentiable.csinh  -- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
    Differentiable.sinh  -- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
    Real.differentiable_arsinh  -- Mathlib.Analysis.SpecialFunctions.Arsinh
    Complex.differentiable_cos  -- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
    Complex.differentiable_cosh  -- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
    Complex.differentiable_sin  -- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
    Complex.differentiable_sinh  -- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
    Differentiable.sqrt  -- Mathlib.Analysis.SpecialFunctions.Sqrt
    Polynomial.differentiable  -- Mathlib.Analysis.Calculus.Deriv.Polynomial
    Polynomial.differentiable_aeval  -- Mathlib.Analysis.Calculus.Deriv.Polynomial
    differentiable_id
    differentiable_id'
    differentiable_const  -- Mathlib.Analysis.Calculus.FDeriv.Basic
    Differentiable.dist  -- Mathlib.Analysis.InnerProductSpace.Calculus
    differentiable_fst  -- Mathlib.Analysis.Calculus.FDeriv.Prod
    differentiable_snd  -- Mathlib.Analysis.Calculus.FDeriv.Prod
    Differentiable.fst  -- Mathlib.Analysis.Calculus.FDeriv.Prod
    Differentiable.snd  -- Mathlib.Analysis.Calculus.FDeriv.Prod
    Differentiable.const_mul  -- Mathlib.Analysis.Calculus.FDeriv.Mul
    Differentiable.mul_const  -- Mathlib.Analysis.Calculus.FDeriv.Mul
    Differentiable.pow  -- Mathlib.Analysis.Calculus.FDeriv.Mul
    Differentiable.inverse  -- Mathlib.Analysis.Calculus.FDeriv.Mul
    Differentiable.inv'  -- Mathlib.Analysis.Calculus.FDeriv.Mul
    Differentiable.smul_const  -- Mathlib.Analysis.Calculus.FDeriv.Mul
    Differentiable.neg  -- Mathlib.Analysis.Calculus.FDeriv.Add
    Differentiable.const_sub  -- Mathlib.Analysis.Calculus.FDeriv.Add
    Differentiable.sub_const  -- Mathlib.Analysis.Calculus.FDeriv.Add
    Differentiable.add_const  -- Mathlib.Analysis.Calculus.FDeriv.Add
    Differentiable.const_add  -- Mathlib.Analysis.Calculus.FDeriv.Add
    Differentiable.const_smul  -- Mathlib.Analysis.Calculus.FDeriv.Add
    Differentiable.div_const  -- Mathlib.Analysis.Calculus.Deriv.Mul
    Differentiable.inv  -- Mathlib.Analysis.Calculus.Deriv.Inv
    Differentiable.div  -- Mathlib.Analysis.Calculus.Deriv.Inv
    differentiable_neg  -- Mathlib.Analysis.Calculus.Deriv.Add
    Real.differentiable_exp  -- Mathlib.Analysis.SpecialFunctions.ExpDeriv
    Complex.differentiable_exp  -- Mathlib.Analysis.SpecialFunctions.ExpDeriv
    Differentiable.clog  -- Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
    Differentiable.rpow  -- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
    Real.differentiable_arctan  -- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
    Differentiable.arctan  -- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv

-- This just runs forever
example : Differentiable ℝ (fun (x : ℝ) ↦
(sin x * exp x + 3) * 999 * (cosh (cos x)))
:= by
    aesop (options := { terminal := true }) (rule_sets [Differentiable])
JLimperg commented 5 months ago

Minimised:

import Mathlib.Data.Complex.Exponential

open Real (cos)

axiom MyDifferentiable : (ℝ → ℝ) → Prop
axiom MyDifferentiable.cos {f : ℝ → ℝ} :
  MyDifferentiable f → MyDifferentiable fun x => cos (f x)

example : MyDifferentiable fun y ↦ (Complex.cosh ↑(cos y)).re := by
  aesop (add safe MyDifferentiable.cos) (rule_sets [-builtin,-default])

apply MyDifferentiable.cos in the same place runs out of heartbeats, so that may have something to do with it. But I haven't yet figured out why Aesop doesn't run out of heartbeats as well.