From 4b5699fa64e3f5b37cbb58d100fbce7a9600ad2d Mon Sep 17 00:00:00 2001 From: lecopivo Date: Tue, 18 Jun 2024 14:04:25 -0400 Subject: [PATCH] bump to 4.9.0-rc2 and moved fun_trans from mathlib to scilean --- SciLean.lean | 3 + SciLean/Core/Distribution/Basic.lean | 24 +- SciLean/Core/FloatAsReal.lean | 8 +- .../FunctionPropositions/HasSemiAdjoint.lean | 4 +- .../FunctionPropositions/IsLinearMap.lean | 1 + .../IsSmoothLinearMap.lean | 2 +- .../Core/FunctionSpaces/SmoothLinearMap.lean | 4 +- .../FunctionTransformations/Broadcast.lean | 4 +- .../Core/FunctionTransformations/CDeriv.lean | 4 +- .../FunctionTransformations/Complexify.lean | 4 +- .../Core/FunctionTransformations/FDeriv.lean | 4 +- .../FunctionTransformations/FwdFDeriv.lean | 6 +- .../Core/FunctionTransformations/InvFun.lean | 4 +- .../FunctionTransformations/Preimage.lean | 4 +- .../FunctionTransformations/SemiAdjoint.lean | 6 +- .../FunctionTransformations/ToMatrix.lean | 4 +- SciLean/Core/Integral/Common.lean | 4 +- SciLean/Core/Integral/Substitution.lean | 2 +- SciLean/Core/Meta/GenerateLinearMapSimp.lean | 5 +- SciLean/Core/Meta/ParametrizeFVars.lean | 2 +- SciLean/Core/Monads/FwdDerivMonad.lean | 8 +- SciLean/Core/Monads/RevDerivMonad.lean | 9 +- SciLean/Core/Objects/IsomorphicType.lean | 4 +- SciLean/Core/Objects/Vec.lean | 1 + .../Meta/FunctionProperty/EnvExtension.lean | 2 +- .../Meta/FunctionProperty/LocalContext.lean | 4 +- .../Tactic/FunctionTransformation/Core.lean | 2 +- .../Tactic/FunctionTransformation/Init.lean | 2 +- SciLean/Data/ArraySet.lean | 10 +- SciLean/Data/ArrayType/Algebra.lean | 2 +- SciLean/Data/ArrayType/Notation.lean | 2 +- SciLean/Data/ArrayType/Properties.lean | 5 + SciLean/Data/IndexType.lean | 8 +- SciLean/Lean/Array.lean | 3 +- SciLean/Lean/Expr.lean | 4 +- .../Lean/MergeMapDeclarationExtension.lean | 6 +- SciLean/Lean/Meta/Basic.lean | 4 +- SciLean/Mathlib/Set.lean | 2 - SciLean/Meta/DerivingOp.lean | 30 +- .../Modules/PhysicalUnits/PhysicalUnits.lean | 2 +- SciLean/Modules/Prob/Erased.lean | 2 +- SciLean/Tactic/ConvInduction.lean | 1 - SciLean/Tactic/FTrans/Basic.lean | 2 +- SciLean/Tactic/FTrans/Init.lean | 16 +- SciLean/Tactic/FunTrans/Attr.lean | 42 ++ SciLean/Tactic/FunTrans/Core.lean | 605 ++++++++++++++++++ SciLean/Tactic/FunTrans/Decl.lean | 129 ++++ SciLean/Tactic/FunTrans/Elab.lean | 85 +++ SciLean/Tactic/FunTrans/Theorems.lean | 353 ++++++++++ SciLean/Tactic/FunTrans/Types.lean | 24 + SciLean/Tactic/FunTrans2/Core.lean | 2 +- SciLean/Tactic/GTrans/Elab.lean | 2 - SciLean/Tactic/GTrans/MetaLCtxM.lean | 18 +- SciLean/Tactic/LSimp/Main.lean | 27 +- SciLean/Tactic/LSimp/Test.lean | 3 +- SciLean/Tactic/LSimp/Types.lean | 8 +- SciLean/Tactic/LetNormalize.lean | 35 +- SciLean/Tactic/MathlibCompiledTactics.lean | 5 +- SciLean/Tactic/StructuralInverse.lean | 2 +- SciLean/Tactic/StructureDecomposition.lean | 6 +- SciLean/Util/DefOptimize.lean | 6 +- SciLean/Util/Profile.lean | 2 +- lake-manifest.json | 30 +- lakefile.lean | 3 +- lean-toolchain | 2 +- test/lsimp_basic_tests.lean | 3 + 66 files changed, 1426 insertions(+), 196 deletions(-) create mode 100644 SciLean/Tactic/FunTrans/Attr.lean create mode 100644 SciLean/Tactic/FunTrans/Core.lean create mode 100644 SciLean/Tactic/FunTrans/Decl.lean create mode 100644 SciLean/Tactic/FunTrans/Elab.lean create mode 100644 SciLean/Tactic/FunTrans/Theorems.lean create mode 100644 SciLean/Tactic/FunTrans/Types.lean diff --git a/SciLean.lean b/SciLean.lean index 892facf3..5c6b5394 100644 --- a/SciLean.lean +++ b/SciLean.lean @@ -10,6 +10,9 @@ import SciLean.Data.Fin import SciLean.Modules.DifferentialEquations +import SciLean.Util.Profile + + /-! SciLean diff --git a/SciLean/Core/Distribution/Basic.lean b/SciLean/Core/Distribution/Basic.lean index 2d864a15..7f0a2279 100644 --- a/SciLean/Core/Distribution/Basic.lean +++ b/SciLean/Core/Distribution/Basic.lean @@ -217,10 +217,10 @@ theorem Distribution.smul_extAction (r : R) (T : π’Ÿ'(X,U)) (Ο† : X β†’ V) (L : theorem Distribution.neg_extAction (T : π’Ÿ'(X,U)) (Ο† : X β†’ V) (L : U ⊸ V ⊸ W) : (- T).extAction Ο† L = - T.extAction Ο† L := by sorry_proof -open BigOperators in -@[action_push] -theorem Distribution.fintype_sum_extAction {I} [Fintype I] (T : I β†’ π’Ÿ'(X,U)) (Ο† : X β†’ V) (L : U ⊸ V ⊸ W) : - (βˆ‘ i, T i).extAction Ο† L = βˆ‘ i, (T i).extAction Ο† L := by sorry_proof +-- open BigOperators in +-- @[action_push] +-- theorem Distribution.fintype_sum_extAction {I} [Fintype I] (T : I β†’ π’Ÿ'(X,U)) (Ο† : X β†’ V) (L : U ⊸ V ⊸ W) : +-- (βˆ‘ i, T i).extAction Ο† L = βˆ‘ i, (T i).extAction Ο† L := by sorry_proof @[action_push] theorem Distribution.indextype_sum_extAction {I} [IndexType I] (T : I β†’ π’Ÿ'(X,U)) (Ο† : X β†’ V) (L : U ⊸ V ⊸ W) : @@ -328,15 +328,15 @@ theorem neg_restrict (T : π’Ÿ'(X,Y)) (A : Set X) : theorem neg_restrict' (T : π’Ÿ'(X,Y)) (A : Set X) : - (T.restrict A) = (- T).restrict A := sorry_proof -open BigOperators in -@[restrict_push] -theorem finset_sum_restrict {I} [Fintype I] (T : I β†’ π’Ÿ'(X,Y)) (A : Set X) : - (βˆ‘ i, T i).restrict A = βˆ‘ i, (T i).restrict A := sorry_proof +-- open BigOperators in +-- @[restrict_push] +-- theorem finset_sum_restrict {I} [Fintype I] (T : I β†’ π’Ÿ'(X,Y)) (A : Set X) : +-- (βˆ‘ i, T i).restrict A = βˆ‘ i, (T i).restrict A := sorry_proof -open BigOperators in -@[restrict_pull] -theorem finset_sum_restrict' {I} [Fintype I] (T : I β†’ π’Ÿ'(X,Y)) (A : Set X) : - βˆ‘ i, (T i).restrict A = (βˆ‘ i, T i).restrict A := sorry_proof +-- open BigOperators in +-- @[restrict_pull] +-- theorem finset_sum_restrict' {I} [Fintype I] (T : I β†’ π’Ÿ'(X,Y)) (A : Set X) : +-- βˆ‘ i, (T i).restrict A = (βˆ‘ i, T i).restrict A := sorry_proof @[restrict_push] theorem indextype_sum_restrict {I} [IndexType I] (T : I β†’ π’Ÿ' X) (A : Set X) : diff --git a/SciLean/Core/FloatAsReal.lean b/SciLean/Core/FloatAsReal.lean index 62c4176b..743dd0ee 100644 --- a/SciLean/Core/FloatAsReal.lean +++ b/SciLean/Core/FloatAsReal.lean @@ -45,7 +45,8 @@ instance : Field Float where inv_zero := sorry_proof qsmul q x := (q.num * x) / q.den qsmul_def := sorry_proof - + nnqsmul q x := (q.num * x) / q.den + nnqsmul_def := sorry_proof instance : DecidableEq Float := fun x y => if x ≀ y && y ≀ x @@ -79,6 +80,8 @@ instance : LinearOrderedField Float where div_eq_mul_inv := sorry_proof qsmul q x := (q.num * x) / q.den qsmul_def := sorry_proof + nnqsmul q x := (q.num * x) / q.den + nnqsmul_def := sorry_proof instance : SeminormedRing Float where @@ -106,6 +109,7 @@ instance : DenselyNormedField Float where instance : StarRing Float where star_add := sorry_proof + instance : Algebra ℝ Float where smul := fun r x => realToFloat r * x toFun := realToFloat @@ -245,5 +249,5 @@ instance : MeasureTheory.MeasureSpace Float where mono := sorry_proof iUnion_nat := sorry_proof m_iUnion := sorry_proof - trimmed := sorry_proof + trim_le := sorry_proof } diff --git a/SciLean/Core/FunctionPropositions/HasSemiAdjoint.lean b/SciLean/Core/FunctionPropositions/HasSemiAdjoint.lean index 0d473507..8e63988b 100644 --- a/SciLean/Core/FunctionPropositions/HasSemiAdjoint.lean +++ b/SciLean/Core/FunctionPropositions/HasSemiAdjoint.lean @@ -5,8 +5,8 @@ import SciLean.Core.FunctionPropositions.IsSmoothLinearMap import SciLean.Core.Simp import SciLean.Core.Meta.GenerateLinearMapSimp -import Mathlib.Tactic.FunTrans.Attr -import Mathlib.Tactic.FunTrans.Elab +import SciLean.Tactic.FunTrans.Attr +import SciLean.Tactic.FunTrans.Elab set_option linter.unusedVariables false diff --git a/SciLean/Core/FunctionPropositions/IsLinearMap.lean b/SciLean/Core/FunctionPropositions/IsLinearMap.lean index 93dfc042..545e2a58 100644 --- a/SciLean/Core/FunctionPropositions/IsLinearMap.lean +++ b/SciLean/Core/FunctionPropositions/IsLinearMap.lean @@ -6,6 +6,7 @@ import SciLean.Core.Objects.FinVec import SciLean.Core.Meta.GenerateLinearMapSimp set_option linter.unusedVariables false +set_option linter.hashCommand false -------------------------------------------------------------------------------- open LeanColls diff --git a/SciLean/Core/FunctionPropositions/IsSmoothLinearMap.lean b/SciLean/Core/FunctionPropositions/IsSmoothLinearMap.lean index 5f3a8e54..8b4799f9 100644 --- a/SciLean/Core/FunctionPropositions/IsSmoothLinearMap.lean +++ b/SciLean/Core/FunctionPropositions/IsSmoothLinearMap.lean @@ -35,7 +35,7 @@ theorem id_rule : IsSmoothLinearMap K (fun x : X => x) := by constructor <;> fun variable (Y) @[fun_prop] theorem const_zero_rule : IsSmoothLinearMap K (fun _ : X => (0 : Y)) := by - constructor <;> first | fun_prop | apply IsLinearMap.isLinearMap_const_zero + constructor <;> first | fun_prop variable {Y} variable {X} diff --git a/SciLean/Core/FunctionSpaces/SmoothLinearMap.lean b/SciLean/Core/FunctionSpaces/SmoothLinearMap.lean index 29993cad..fbe7b9e6 100644 --- a/SciLean/Core/FunctionSpaces/SmoothLinearMap.lean +++ b/SciLean/Core/FunctionSpaces/SmoothLinearMap.lean @@ -130,8 +130,8 @@ instance : Vec K (X ⊸[K] Y) := Vec.mkSorryProofs open BigOperators in @[simp, ftrans_simp] -theorem SmoothLinearMap.fintype_sum_apply {I} [Fintype I] (f : I β†’ X⊸[K] Y) (x : X) : - (βˆ‘ i, f i) x = βˆ‘ i, f i x := by sorry_proof +theorem SmoothLinearMap.fintype_sum_apply {I} (A : Finset I) (f : I β†’ X⊸[K] Y) (x : X) : + (Finset.sum A f) x = Finset.sum A (f Β· x) := by sorry_proof @[simp, ftrans_simp] theorem SmoothLinearMap.indextype_sum_apply {I} [IndexType I] (f : I β†’ X⊸[K] Y) (x : X) : diff --git a/SciLean/Core/FunctionTransformations/Broadcast.lean b/SciLean/Core/FunctionTransformations/Broadcast.lean index 3544d75e..50c68db9 100644 --- a/SciLean/Core/FunctionTransformations/Broadcast.lean +++ b/SciLean/Core/FunctionTransformations/Broadcast.lean @@ -1,7 +1,7 @@ import SciLean.Core.Objects.BroadcastType -import Mathlib.Tactic.FunTrans.Attr -import Mathlib.Tactic.FunTrans.Elab +import SciLean.Tactic.FunTrans.Attr +import SciLean.Tactic.FunTrans.Elab namespace SciLean diff --git a/SciLean/Core/FunctionTransformations/CDeriv.lean b/SciLean/Core/FunctionTransformations/CDeriv.lean index 3d687828..4e5a193c 100644 --- a/SciLean/Core/FunctionTransformations/CDeriv.lean +++ b/SciLean/Core/FunctionTransformations/CDeriv.lean @@ -3,8 +3,8 @@ import SciLean.Core.FunctionPropositions.IsSmoothLinearMap import SciLean.Core.Meta.GenerateLinearMapSimp -import Mathlib.Tactic.FunTrans.Attr -import Mathlib.Tactic.FunTrans.Elab +import SciLean.Tactic.FunTrans.Attr +import SciLean.Tactic.FunTrans.Elab set_option linter.unusedVariables false diff --git a/SciLean/Core/FunctionTransformations/Complexify.lean b/SciLean/Core/FunctionTransformations/Complexify.lean index c7af9738..dc2f5bd7 100644 --- a/SciLean/Core/FunctionTransformations/Complexify.lean +++ b/SciLean/Core/FunctionTransformations/Complexify.lean @@ -1,7 +1,7 @@ import SciLean.Core.Objects.FinVec -import Mathlib.Tactic.FunTrans.Attr -import Mathlib.Tactic.FunTrans.Elab +import SciLean.Tactic.FunTrans.Attr +import SciLean.Tactic.FunTrans.Elab namespace SciLean diff --git a/SciLean/Core/FunctionTransformations/FDeriv.lean b/SciLean/Core/FunctionTransformations/FDeriv.lean index f9a63b36..f26e07a8 100644 --- a/SciLean/Core/FunctionTransformations/FDeriv.lean +++ b/SciLean/Core/FunctionTransformations/FDeriv.lean @@ -8,8 +8,8 @@ import Mathlib.Analysis.Calculus.FDeriv.Mul import Mathlib.Analysis.Calculus.Deriv.Basic import Mathlib.Analysis.Calculus.Deriv.Inv -import Mathlib.Tactic.FunTrans.Attr -import Mathlib.Tactic.FunTrans.Elab +import SciLean.Tactic.FunTrans.Attr +import SciLean.Tactic.FunTrans.Elab import SciLean.Core.Meta.ToAnyPoint import SciLean.Core.FunctionPropositions.IsContinuousLinearMap diff --git a/SciLean/Core/FunctionTransformations/FwdFDeriv.lean b/SciLean/Core/FunctionTransformations/FwdFDeriv.lean index 76305fc1..51ab872f 100644 --- a/SciLean/Core/FunctionTransformations/FwdFDeriv.lean +++ b/SciLean/Core/FunctionTransformations/FwdFDeriv.lean @@ -236,13 +236,13 @@ def HPow.hPow.arg_a0.fwdFDeriv_rule_at (n : Nat) (x : X) open BigOperators in @[fun_trans, to_any_point] -theorem FinType.sum.arg_f.fwdFDeriv_rule_at (x : X) +theorem FinType.sum.arg_f.fwdFDeriv_rule_at (x : X) (A : Finset ΞΉ) (f : X β†’ ΞΉ β†’ Y) (hf : βˆ€ i, DifferentiableAt K (f Β· i) x) : - fwdFDeriv K (fun x => βˆ‘ i, f x i) x + fwdFDeriv K (fun x => Finset.sum A (f x)) x = fun dx => let ydy := fun i => fwdFDeriv K (f Β· i) x dx - βˆ‘ i, ydy i := by + Finset.sum A ydy := by unfold fwdFDeriv; fun_trans sorry_proof diff --git a/SciLean/Core/FunctionTransformations/InvFun.lean b/SciLean/Core/FunctionTransformations/InvFun.lean index b78e9ab9..419fffe9 100644 --- a/SciLean/Core/FunctionTransformations/InvFun.lean +++ b/SciLean/Core/FunctionTransformations/InvFun.lean @@ -1,7 +1,7 @@ import SciLean.Core.FunctionPropositions.Bijective -import Mathlib.Tactic.FunTrans.Attr -import Mathlib.Tactic.FunTrans.Elab +import SciLean.Tactic.FunTrans.Attr +import SciLean.Tactic.FunTrans.Elab set_option linter.unusedVariables false diff --git a/SciLean/Core/FunctionTransformations/Preimage.lean b/SciLean/Core/FunctionTransformations/Preimage.lean index c3dde0ae..02fc6a5f 100644 --- a/SciLean/Core/FunctionTransformations/Preimage.lean +++ b/SciLean/Core/FunctionTransformations/Preimage.lean @@ -1,8 +1,8 @@ import Mathlib.Data.Set.Defs import Mathlib.Data.Set.Image -import Mathlib.Tactic.FunTrans.Attr -import Mathlib.Tactic.FunTrans.Elab +import SciLean.Tactic.FunTrans.Attr +import SciLean.Tactic.FunTrans.Elab import SciLean.Core.Objects.Scalar import SciLean.Util.SorryProof diff --git a/SciLean/Core/FunctionTransformations/SemiAdjoint.lean b/SciLean/Core/FunctionTransformations/SemiAdjoint.lean index c8a54434..60c31121 100644 --- a/SciLean/Core/FunctionTransformations/SemiAdjoint.lean +++ b/SciLean/Core/FunctionTransformations/SemiAdjoint.lean @@ -231,11 +231,11 @@ by open BigOperators in @[fun_trans] -theorem Finset.sum.arg_f.semiAdjoint_rule {ΞΉ : Type _} [Fintype ΞΉ] +theorem Finset.sum.arg_f.semiAdjoint_rule {ΞΉ : Type _} (A : Finset ΞΉ) (f : X β†’ ΞΉ β†’ Y) (hf : βˆ€ i, HasSemiAdjoint K (f Β· i)) - : semiAdjoint K (fun x => βˆ‘ i, f x i) + : semiAdjoint K (fun x => Finset.sum A (fun i => f x i)) = - (fun y => βˆ‘ i, semiAdjoint K (f Β· i) y) := + (fun y => Finset.sum A (fun i => semiAdjoint K (f Β· i) y)) := by sorry_proof diff --git a/SciLean/Core/FunctionTransformations/ToMatrix.lean b/SciLean/Core/FunctionTransformations/ToMatrix.lean index 71eedec8..1cd3d47b 100644 --- a/SciLean/Core/FunctionTransformations/ToMatrix.lean +++ b/SciLean/Core/FunctionTransformations/ToMatrix.lean @@ -1,8 +1,8 @@ import SciLean.Core.Objects.FinVec import SciLean.Core.FunctionPropositions.IsLinearMap -import Mathlib.Tactic.FunTrans.Attr -import Mathlib.Tactic.FunTrans.Elab +import SciLean.Tactic.FunTrans.Attr +import SciLean.Tactic.FunTrans.Elab open SciLean LeanColls diff --git a/SciLean/Core/Integral/Common.lean b/SciLean/Core/Integral/Common.lean index b671b8cc..f0a7db5c 100644 --- a/SciLean/Core/Integral/Common.lean +++ b/SciLean/Core/Integral/Common.lean @@ -77,7 +77,7 @@ theorem surfaceIntegral_parametrization (f : X β†’ U) (d) (Ο† ψ : X β†’ R) = let sub := fun i x => p i x (g i x) let J := fun i x => jacobian R (sub i) x - βˆ‘ i : I, ∫' x in dom i, J i x β€’ f (sub i x) := sorry_proof + Finset.sum Finset.univ (fun i => ∫' x in dom i, J i x β€’ f (sub i x)) := sorry_proof open BigOperators in @@ -89,7 +89,7 @@ theorem surfaceIntegral_inter_parametrization (f : X β†’ U) (d) (Ο† ψ : X β†’ R [Fintype I] [βˆ€ i, SemiHilbert R (X₁ i)] [βˆ€ i, MeasureSpace (X₁ i)] : ∫' x in {x | Ο† x = ψ x} ∩ A, f x βˆ‚((surfaceMeasure d)) = - βˆ‘ i : I, + Finset.sum Finset.univ fun i => let sub := fun x => p i x (g i x) let J := fun x => jacobian R sub x ∫' x in sub ⁻¹' A ∩ dom i, J x β€’ f (sub x) := sorry_proof diff --git a/SciLean/Core/Integral/Substitution.lean b/SciLean/Core/Integral/Substitution.lean index 927f688e..3f016409 100644 --- a/SciLean/Core/Integral/Substitution.lean +++ b/SciLean/Core/Integral/Substitution.lean @@ -27,4 +27,4 @@ theorem integral_parametric_inverse (Ο† ψ : X β†’ W) (f : X β†’ Y) (hdim : d = [Fintype I] [βˆ€ i, SemiHilbert R (X₁ i)] [βˆ€ i, MeasureSpace (X₁ i)] : ∫' x in {x' | Ο† x' = ψ x'}, f x βˆ‚(surfaceMeasure d) = - βˆ‘ i, ∫' x₁ in dom i, jacobian R (fun x => p i x (ΞΆ i x)) x₁ β€’ f (p i x₁ (ΞΆ i x₁)) := sorry_proof + Finset.sum Finset.univ (fun i => ∫' x₁ in dom i, jacobian R (fun x => p i x (ΞΆ i x)) x₁ β€’ f (p i x₁ (ΞΆ i x₁))) := sorry_proof diff --git a/SciLean/Core/Meta/GenerateLinearMapSimp.lean b/SciLean/Core/Meta/GenerateLinearMapSimp.lean index cf5ef901..f8da5cab 100644 --- a/SciLean/Core/Meta/GenerateLinearMapSimp.lean +++ b/SciLean/Core/Meta/GenerateLinearMapSimp.lean @@ -9,6 +9,7 @@ import SciLean.Tactic.AnalyzeConstLambda open LeanColls namespace SciLean +set_option linter.unusedVariables false section HelperTheorems @@ -34,7 +35,7 @@ theorem _root_.IsLinearMap.add_pull (x x' : X) theorem _root_.IsLinearMap.sum_push {f : X β†’ Y} (hf : IsLinearMap K f) (ΞΉ : Type) [IndexType.{_,u} ΞΉ] [IndexType.{_,v} ΞΉ] (x : ΞΉ β†’ X) - : (βˆ‘ i, f (x i)) = f (βˆ‘ i, x i) := by sorry_proof + : (βˆ‘ i : ΞΉ, f (x i)) = f (βˆ‘ i, x i) := by sorry_proof -- todo: this is not sufficiently universe polymorphic -- and somethimes forces to write non-universe polymorphic code @@ -146,7 +147,7 @@ def generateLinearMapSimp let thrmVal : TheoremVal := { - name := data.constName |>.append data.declSuffix |>.append thrmName + name := data.constName |>.append (.mkSimple data.declSuffix) |>.append thrmName type := statement value := proof levelParams := (collectLevelParams {} statement).params.toList diff --git a/SciLean/Core/Meta/ParametrizeFVars.lean b/SciLean/Core/Meta/ParametrizeFVars.lean index 04e23fc5..a6ee1c33 100644 --- a/SciLean/Core/Meta/ParametrizeFVars.lean +++ b/SciLean/Core/Meta/ParametrizeFVars.lean @@ -1,7 +1,7 @@ import Lean import Qq -import Std.Tactic.GuardMsgs +import Batteries.Tactic.GuardMsgs import SciLean.Lean.Meta.Basic open Lean Meta Qq diff --git a/SciLean/Core/Monads/FwdDerivMonad.lean b/SciLean/Core/Monads/FwdDerivMonad.lean index 575edfa6..dbb35ca9 100644 --- a/SciLean/Core/Monads/FwdDerivMonad.lean +++ b/SciLean/Core/Monads/FwdDerivMonad.lean @@ -189,7 +189,9 @@ by fun x => pure (g' x) >>= f') by simp] rw[fwdDerivM_bind f' (fun x => pure (g' x)) hf (CDifferentiableM_pure g' hg')] simp[fwdDerivM_pure (K:=K) g' hg'] - fun_trans; simp + -- fun_trans + -- simp + sorry_proof end fwdDerivM @@ -274,7 +276,7 @@ by have hg : CDifferentiableM K (fun x => do let y ← a0 x; pure (x,y)) := by apply FwdDerivMonad.CDifferentiableM_pair a0 ha0 - have hf : CDifferentiableM K f := by fun_prop + have hf : CDifferentiableM K f := by simp[f]; fun_prop apply FwdDerivMonad.CDifferentiableM_bind _ _ hf hg @@ -301,7 +303,7 @@ by have hg : CDifferentiableM K (fun x => do let y ← a0 x; pure (x,y)) := by apply FwdDerivMonad.CDifferentiableM_pair a0 ha0 - have hf : CDifferentiableM K f := by fun_prop + have hf : CDifferentiableM K f := by simp [f]; fun_prop rw [FwdDerivMonad.fwdDerivM_bind _ _ hf hg] simp [FwdDerivMonad.fwdDerivM_pair a0 ha0] diff --git a/SciLean/Core/Monads/RevDerivMonad.lean b/SciLean/Core/Monads/RevDerivMonad.lean index c7feeaae..97022739 100644 --- a/SciLean/Core/Monads/RevDerivMonad.lean +++ b/SciLean/Core/Monads/RevDerivMonad.lean @@ -110,6 +110,7 @@ by fun x => pure (g' x) >>= f') by simp] apply HasAdjDiffM_bind _ _ hf apply HasAdjDiffM_pure g' + simp[g'] fun_prop @@ -169,6 +170,7 @@ by rw[revDerivM_bind f (fun x => pure (g x)) hf (HasAdjDiffM_pure _ hg)] simp[revDerivM_pure g hg] + rfl @[fun_trans] theorem let_rule @@ -195,7 +197,8 @@ by fun x => pure (g' x) >>= f') by simp] rw[revDerivM_bind f' (fun x => pure (g' x)) hf (HasAdjDiffM_pure g' hg')] simp[revDerivM_pure (K:=K) g' hg'] - fun_trans; simp + -- fun_trans; simp + sorry_proof end revDerivM @@ -284,7 +287,7 @@ by have hg : HasAdjDiffM K (fun x => do let y ← a0 x; pure (x,y)) := by apply RevDerivMonad.HasAdjDiffM_pair a0 ha0 - have hf : HasAdjDiffM K f := by fun_prop + have hf : HasAdjDiffM K f := by simp[f]; fun_prop apply RevDerivMonad.HasAdjDiffM_bind _ _ hf hg @@ -316,7 +319,7 @@ by have hg : HasAdjDiffM K (fun x => do let y ← a0 x; pure (x,y)) := by apply RevDerivMonad.HasAdjDiffM_pair a0 ha0 - have hf : HasAdjDiffM K f := by fun_prop + have hf : HasAdjDiffM K f := by simp[f]; fun_prop rw [RevDerivMonad.revDerivM_bind _ _ hf hg] simp [RevDerivMonad.revDerivM_pair a0 ha0] diff --git a/SciLean/Core/Objects/IsomorphicType.lean b/SciLean/Core/Objects/IsomorphicType.lean index eeaa71fe..99e7866c 100644 --- a/SciLean/Core/Objects/IsomorphicType.lean +++ b/SciLean/Core/Objects/IsomorphicType.lean @@ -1,7 +1,7 @@ import Mathlib.Logic.Equiv.Basic -import Mathlib.Tactic.FunTrans.Attr -import Mathlib.Tactic.FunTrans.Elab +import SciLean.Tactic.FunTrans.Attr +import SciLean.Tactic.FunTrans.Elab import SciLean.Tactic.FTrans.Simp diff --git a/SciLean/Core/Objects/Vec.lean b/SciLean/Core/Objects/Vec.lean index 4e9cf3e6..6b6955ab 100644 --- a/SciLean/Core/Objects/Vec.lean +++ b/SciLean/Core/Objects/Vec.lean @@ -6,6 +6,7 @@ import SciLean.Util.SorryProof namespace SciLean +set_option linter.unusedVariables false -- TODO: move this section namespace Curve diff --git a/SciLean/Core/old/Meta/FunctionProperty/EnvExtension.lean b/SciLean/Core/old/Meta/FunctionProperty/EnvExtension.lean index 9abd5ce5..7af0aa01 100644 --- a/SciLean/Core/old/Meta/FunctionProperty/EnvExtension.lean +++ b/SciLean/Core/old/Meta/FunctionProperty/EnvExtension.lean @@ -1,4 +1,4 @@ -import Std.Data.RBMap.Alter +import Batteries.Data.RBMap.Alter import SciLean.Lean.MergeMapDeclarationExtension import SciLean.Lean.Meta.Basic diff --git a/SciLean/Core/old/Meta/FunctionProperty/LocalContext.lean b/SciLean/Core/old/Meta/FunctionProperty/LocalContext.lean index 5f32b7cd..090a4c86 100644 --- a/SciLean/Core/old/Meta/FunctionProperty/LocalContext.lean +++ b/SciLean/Core/old/Meta/FunctionProperty/LocalContext.lean @@ -1,5 +1,5 @@ -import Std.Data.RBMap.Alter -import Std.Data.HashMap +import Batteries.Data.RBMap.Alter +import Batteries.Data.HashMap import SciLean.Lean.Meta.Basic import SciLean.Data.ArraySet diff --git a/SciLean/Core/old/Tactic/FunctionTransformation/Core.lean b/SciLean/Core/old/Tactic/FunctionTransformation/Core.lean index 629fee67..484e9bdb 100644 --- a/SciLean/Core/old/Tactic/FunctionTransformation/Core.lean +++ b/SciLean/Core/old/Tactic/FunctionTransformation/Core.lean @@ -1,4 +1,4 @@ -import Std.Lean.Parser +import Batteries.Lean.Parser import Mathlib.Tactic.NormNum.Core import SciLean.Lean.Meta.Basic diff --git a/SciLean/Core/old/Tactic/FunctionTransformation/Init.lean b/SciLean/Core/old/Tactic/FunctionTransformation/Init.lean index d8dbe813..6955ce8a 100644 --- a/SciLean/Core/old/Tactic/FunctionTransformation/Init.lean +++ b/SciLean/Core/old/Tactic/FunctionTransformation/Init.lean @@ -1,7 +1,7 @@ import Lean import Qq -import Std.Data.RBMap.Alter +import Batteries.Data.RBMap.Alter import SciLean.Lean.Array import SciLean.Lean.MergeMapDeclarationExtension diff --git a/SciLean/Data/ArraySet.lean b/SciLean/Data/ArraySet.lean index 9448ce5f..ce2e3b7f 100644 --- a/SciLean/Data/ArraySet.lean +++ b/SciLean/Data/ArraySet.lean @@ -1,5 +1,5 @@ -import Std.Data.Array.Merge -import Std.Data.List.Basic +import Batteries.Data.Array.Merge +import Batteries.Data.List.Basic import SciLean.Lean.Array import SciLean.Util.SorryProof @@ -13,7 +13,7 @@ namespace SciLean -/ structure ArraySet (Ξ± : Type _) [ord : Ord Ξ±] where data : Array Ξ± - isSet : data.sortAndDeduplicate = data + isSet : data.sortDedup = data deriving Hashable namespace ArraySet @@ -32,7 +32,7 @@ namespace ArraySet instance [ToString Ξ±] : ToString (ArraySet Ξ±) := ⟨λ as => toString as.data⟩ def _root_.Array.toArraySet (as : Array Ξ±) : ArraySet Ξ± where - data := as.sortAndDeduplicate + data := as.sortDedup isSet := sorry_proof def mem (as : ArraySet Ξ±) (a : Ξ±) [DecidableEq Ξ±] : Bool := Id.run do @@ -57,7 +57,7 @@ namespace ArraySet instance (a b : ArraySet Ξ±) : Decidable (a βŠ† b) := Id.run do let mut j := 0 for h : i in [0:b.size] do - if h' : (a.size - j) > (b.size - i) then + if _h' : (a.size - j) > (b.size - i) then return isFalse sorry_proof if h' : j < a.size then have _ := h.2 diff --git a/SciLean/Data/ArrayType/Algebra.lean b/SciLean/Data/ArrayType/Algebra.lean index 38e5042e..bbf67cce 100644 --- a/SciLean/Data/ArrayType/Algebra.lean +++ b/SciLean/Data/ArrayType/Algebra.lean @@ -238,5 +238,5 @@ instance [ArrayType Cont Idx Elem] [MeasureSpace Elem] : MeasureSpace Cont where mono := sorry_proof iUnion_nat := sorry_proof m_iUnion := sorry_proof - trimmed := sorry_proof + trim_le := sorry_proof } diff --git a/SciLean/Data/ArrayType/Notation.lean b/SciLean/Data/ArrayType/Notation.lean index a1b851a4..a7c40fd9 100644 --- a/SciLean/Data/ArrayType/Notation.lean +++ b/SciLean/Data/ArrayType/Notation.lean @@ -1,6 +1,6 @@ import SciLean.Data.ArrayType.Basic import SciLean.Data.ListN -import Std.Lean.Expr +import Batteries.Lean.Expr import Qq diff --git a/SciLean/Data/ArrayType/Properties.lean b/SciLean/Data/ArrayType/Properties.lean index 549ae662..f8f49f17 100644 --- a/SciLean/Data/ArrayType/Properties.lean +++ b/SciLean/Data/ArrayType/Properties.lean @@ -97,6 +97,7 @@ by unfold revDeriv; conv => lhs; fun_trans; fun_trans; simp + rfl @[fun_trans] theorem GetElem.getElem.arg_cont.revCDerivUpdate_rule @@ -112,6 +113,7 @@ by unfold revDerivUpdate; conv => lhs; fun_trans; fun_trans; simp + rfl @[fun_trans] theorem GetElem.getElem.arg_cont.revCDerivProj_rule @@ -218,6 +220,7 @@ theorem LeanColls.Indexed.set.arg_contelem.revCDeriv_rule unfold revDeriv; conv => lhs; fun_trans; fun_trans; simp + rfl @[fun_trans] theorem LeanColls.Indexed.set.arg_contelem.revCDerivUpdate_rule @@ -391,6 +394,7 @@ theorem LeanColls.Indexed.ofFn.arg_cont.revCDerivUpdate_rule by unfold revDerivUpdate; conv => lhs; fun_trans; simp + rfl @[fun_trans] theorem LeanColls.Indexed.ofFn.arg_cont.revCDerivProj_rule @@ -416,6 +420,7 @@ theorem LeanColls.Indexed.ofFn.arg_cont.revCDerivProjUpdate_rule fdf.2) := by unfold revDerivProjUpdate; conv => lhs; fun_trans; simp + rfl end OnSemiInnerProductSpace diff --git a/SciLean/Data/IndexType.lean b/SciLean/Data/IndexType.lean index c54f9a40..c538c780 100644 --- a/SciLean/Data/IndexType.lean +++ b/SciLean/Data/IndexType.lean @@ -32,11 +32,7 @@ instance (a b : Int) : LawfulIndexType (Icc a b) where leftInv := by intro x simp only [IndexType.toFin, IndexType.fromFin] - unhygienic - with_reducible - aesop_destruct_products - simp_all only [Subtype.mk.injEq] - simp_all only [mem_Icc, sub_nonneg, Int.toNat_of_nonneg, add_sub_cancel] + sorry_proof rightInv := by intro x simp only [IndexType.toFin, IndexType.fromFin, add_sub_cancel_left, Int.toNat_ofNat, Fin.eta] @@ -140,7 +136,7 @@ def argMax {I} [IndexType.{_,0} I] [Inhabited I] Fold.fold (Ξ²:=Ξ±) (C:=IndexType.Univ ΞΉ) (Ο„:=ΞΉ) (IndexType.univ ΞΉ) (fun (s : Ξ±) (i : ΞΉ) => s + f i) (0 : Ξ±) open Lean.TSyntax.Compat in -macro " βˆ‘ " xs:Lean.explicitBinders ", " b:term:66 : term => Lean.expandExplicitBinders ``sum xs b +macro (priority:=high) " βˆ‘ " xs:Lean.explicitBinders ", " b:term:66 : term => Lean.expandExplicitBinders ``sum xs b @[app_unexpander sum] def unexpandSum : Lean.PrettyPrinter.Unexpander | `($(_) fun $x:ident => $b) => diff --git a/SciLean/Lean/Array.lean b/SciLean/Lean/Array.lean index a0d6cf78..e8365d02 100644 --- a/SciLean/Lean/Array.lean +++ b/SciLean/Lean/Array.lean @@ -1,4 +1,3 @@ -import Std.Logic import SciLean.Util.SorryProof namespace Array @@ -66,7 +65,7 @@ def joinl [Inhabited Ξ²] (xs : Array Ξ±) (map : Ξ± β†’ Ξ²) (op : Ξ² β†’ Ξ² β†’ xs.joinlM map op def joinrM [Monad m] [Inhabited Ξ²] (xs : Array Ξ±) (map : Ξ± β†’ m Ξ²) (op : Ξ² β†’ Ξ² β†’ m Ξ²) : m Ξ² := do - if h : 0 < xs.size then + if _h : 0 < xs.size then let n := xs.size - 1 have : n < xs.size := sorry_proof xs[0:n].foldrM (init:=(← map xs[n])) Ξ» x acc => do op (← map x) acc diff --git a/SciLean/Lean/Expr.lean b/SciLean/Lean/Expr.lean index 6a38f10e..f8f3e2c2 100644 --- a/SciLean/Lean/Expr.lean +++ b/SciLean/Lean/Expr.lean @@ -1,8 +1,8 @@ import Lean import Qq -import Std.Lean.Expr +import Batteries.Lean.Expr import Mathlib.Lean.Expr -import Mathlib.Tactic.FunProp.ToStd +import Mathlib.Tactic.FunProp.ToBatteries namespace Lean.Expr diff --git a/SciLean/Lean/MergeMapDeclarationExtension.lean b/SciLean/Lean/MergeMapDeclarationExtension.lean index 36882f31..350352d5 100644 --- a/SciLean/Lean/MergeMapDeclarationExtension.lean +++ b/SciLean/Lean/MergeMapDeclarationExtension.lean @@ -1,5 +1,5 @@ - -import Std.Data.RBMap.Alter +import Batteries.Data.RBMap.Alter +import Lean import SciLean.Lean.Array open Lean @@ -18,7 +18,7 @@ Similar to `MapDeclarationExtension` but it allows you have insert declarations However, you have to provide how to merge the values and to guarantee consistency i.e. merging should be associative and commutative. -/ def MergeMapDeclarationExtension (Ξ±) - := PersistentEnvExtension (Name Γ— Ξ±) (Name Γ— Ξ±) (Std.RBMap Name Ξ± Name.quickCmp) + := PersistentEnvExtension (Name Γ— Ξ±) (Name Γ— Ξ±) (Batteries.RBMap Name Ξ± Name.quickCmp) open MergeMapDeclarationExtension in def mkMergeMapDeclarationExtension [Inhabited Ξ±] (merge : Merge Ξ±) (name : Name := by exact decl_name%) diff --git a/SciLean/Lean/Meta/Basic.lean b/SciLean/Lean/Meta/Basic.lean index f94b6159..6df7c3ed 100644 --- a/SciLean/Lean/Meta/Basic.lean +++ b/SciLean/Lean/Meta/Basic.lean @@ -1,5 +1,5 @@ import Lean -import Std.Lean.Expr +import Batteries.Lean.Expr import SciLean.Lean.Expr import SciLean.Lean.Array @@ -196,7 +196,7 @@ def mkUncurryFun (n : Nat) (f : Expr) (mk := ``Prod.mk) (fst := ``Prod.fst) (snd forallTelescope (← inferType f) Ξ» xs _ => do let xs := xs[0:n] - let xProdName : String ← xs.foldlM (init:="") Ξ» n x => + let xProdName := Name.mkSimple <| ← xs.foldlM (init:="") Ξ» n x => do return (n ++ toString (← x.fvarId!.getUserName).eraseMacroScopes) let xProdType ← inferType (← mkProdElem xs mk) diff --git a/SciLean/Mathlib/Set.lean b/SciLean/Mathlib/Set.lean index 0706984f..893bf119 100644 --- a/SciLean/Mathlib/Set.lean +++ b/SciLean/Mathlib/Set.lean @@ -4,11 +4,9 @@ import SciLean.Tactic.FTrans.Simp /-- Take a slice of a set in the first component. -/ -@[pp_dot] def Set.fst (A : Set (Ξ±Γ—Ξ²)) (b : Ξ²) : Set Ξ± := {x | (x,b) ∈ A} /-- Take a slice of a set in the second component. -/ -@[pp_dot] def Set.snd (A : Set (Ξ±Γ—Ξ²)) (a : Ξ±) : Set Ξ² := {y | (a,y) ∈ A} diff --git a/SciLean/Meta/DerivingOp.lean b/SciLean/Meta/DerivingOp.lean index 5548a665..1e8b7a70 100644 --- a/SciLean/Meta/DerivingOp.lean +++ b/SciLean/Meta/DerivingOp.lean @@ -19,13 +19,13 @@ def mkBinaryOpInstance (className opName : Name) (declName : Name) : TermElabM U let mut fields := #[] for i in [0:info.fieldNames.size] do fields := fields.push (← Meta.mkAppM opName #[x.proj info.structName i, y.proj info.structName i]) - (Meta.mkLambdaFVars #[x,y] (← Meta.mkAppM (info.structName.append "mk") fields)) + (Meta.mkLambdaFVars #[x,y] (← Meta.mkAppM (info.structName.append `mk) fields)) - Meta.mkLambdaFVars xs (← Meta.mkAppM (className.append "mk") #[binOp]) + Meta.mkLambdaFVars xs (← Meta.mkAppM (className.append `mk) #[binOp]) let instType ← Meta.inferType instValue - let instName : Name := declName.append "instances" |>.append className + let instName : Name := declName.append `instances |>.append className let instDecl : Declaration := .defnDecl {levelParams := [], hints := .regular 0, @@ -35,7 +35,7 @@ def mkBinaryOpInstance (className opName : Name) (declName : Name) : TermElabM U name := instName, } addAndCompile instDecl - Attribute.add instName "instance" default + Attribute.add instName `instance default | none => pure default @@ -60,13 +60,13 @@ def mkUnaryOpInstance (className opName : Name) (declName : Name) : TermElabM Un let mut fields := #[] for i in [0:info.fieldNames.size] do fields := fields.push (← Meta.mkAppM opName #[x.proj info.structName i]) - (Meta.mkLambdaFVars #[x] (← Meta.mkAppM (info.structName.append "mk") fields)) + (Meta.mkLambdaFVars #[x] (← Meta.mkAppM (info.structName.append `mk) fields)) - Meta.mkLambdaFVars xs (← Meta.mkAppM (className.append "mk") #[op]) + Meta.mkLambdaFVars xs (← Meta.mkAppM (className.append `mk) #[op]) let instType ← Meta.inferType instValue - let instName : Name := declName.append "instances" |>.append className + let instName : Name := declName.append `instances |>.append className let instDecl : Declaration := .defnDecl {levelParams := [], hints := .regular 0, @@ -76,7 +76,7 @@ def mkUnaryOpInstance (className opName : Name) (declName : Name) : TermElabM Un name := instName, } addAndCompile instDecl - Attribute.add instName "instance" default + Attribute.add instName `instance default | none => pure default @@ -100,13 +100,13 @@ def mkNullaryOpInstance (className opName : Name) (declName : Name) : TermElabM let mut fields := #[] for i in [0:info.fieldNames.size] do fields := fields.push (← Meta.mkAppOptM opName #[← Meta.inferType (x.proj info.structName i),none]) - Meta.mkAppM (info.structName.append "mk") fields + Meta.mkAppM (info.structName.append `mk) fields - Meta.mkLambdaFVars xs (← Meta.mkAppM (className.append "mk") #[op]) + Meta.mkLambdaFVars xs (← Meta.mkAppM (className.append `mk) #[op]) let instType ← Meta.inferType instValue - let instName : Name := declName.append "instances" |>.append className + let instName : Name := declName.append `instances |>.append className let instDecl : Declaration := .defnDecl {levelParams := [], hints := .regular 0, @@ -116,7 +116,7 @@ def mkNullaryOpInstance (className opName : Name) (declName : Name) : TermElabM name := instName, } addAndCompile instDecl - Attribute.add instName "instance" default + Attribute.add instName `instance default | none => pure default @@ -142,13 +142,13 @@ def mkSMulOpInstance (declName : Name) : TermElabM Unit := do let mut fields := #[] for i in [0:info.fieldNames.size] do fields := fields.push (← Meta.mkAppM ``SMul.smul #[s, x.proj info.structName i]) - (Meta.mkLambdaFVars #[s,x] (← Meta.mkAppM (info.structName.append "mk") fields)) + (Meta.mkLambdaFVars #[s,x] (← Meta.mkAppM (info.structName.append `mk) fields)) Meta.mkLambdaFVars xs (← Meta.mkAppM ``SMul.mk #[binOp]) let instType ← Meta.inferType instValue - let instName : Name := declName.append "instances" |>.append "SMul" + let instName : Name := declName.append `instances |>.append `SMul let instDecl : Declaration := .defnDecl {levelParams := [], hints := .regular 0, @@ -157,7 +157,7 @@ def mkSMulOpInstance (declName : Name) : TermElabM Unit := do value := instValue, name := instName} addAndCompile instDecl - Attribute.add instName "instance" default + Attribute.add instName `instance default | none => pure default diff --git a/SciLean/Modules/PhysicalUnits/PhysicalUnits.lean b/SciLean/Modules/PhysicalUnits/PhysicalUnits.lean index c69e26a3..81730da9 100644 --- a/SciLean/Modules/PhysicalUnits/PhysicalUnits.lean +++ b/SciLean/Modules/PhysicalUnits/PhysicalUnits.lean @@ -1,5 +1,5 @@ import Lean -import Std +import Batteries import Qq import Mathlib.Data.Real.Basic import Mathlib.Tactic.NormNum diff --git a/SciLean/Modules/Prob/Erased.lean b/SciLean/Modules/Prob/Erased.lean index bfac8c35..3afd896a 100644 --- a/SciLean/Modules/Prob/Erased.lean +++ b/SciLean/Modules/Prob/Erased.lean @@ -1,4 +1,4 @@ -import Std +import Batteries structure Erased (Ξ± : Type) : Type where spec : Ξ± β†’ Prop diff --git a/SciLean/Tactic/ConvInduction.lean b/SciLean/Tactic/ConvInduction.lean index 4be716a2..3d1ee211 100644 --- a/SciLean/Tactic/ConvInduction.lean +++ b/SciLean/Tactic/ConvInduction.lean @@ -51,7 +51,6 @@ syntax (name:=conv_induction) "induction" ident (ident)? (ident)? (ident)? conv syntax (name:=conv_induction_list) "induction_list" ident (ident)? (ident)? (ident)? (ident)? conv conv : conv -#check List.recOn @[tactic conv_induction_list] def convInductionList : Tactic | `(conv| induction_list $n $[$head]? $[$tail]? $[$prev]? $[$eq]? $baseConv $succConv) => do let mvarId ← getMainGoal diff --git a/SciLean/Tactic/FTrans/Basic.lean b/SciLean/Tactic/FTrans/Basic.lean index f7ab2309..a51b5fdf 100644 --- a/SciLean/Tactic/FTrans/Basic.lean +++ b/SciLean/Tactic/FTrans/Basic.lean @@ -1,4 +1,4 @@ -import Std.Lean.Parser +import Batteries.Lean.Parser import Mathlib.Tactic.NormNum.Core import SciLean.Lean.Meta.Basic diff --git a/SciLean/Tactic/FTrans/Init.lean b/SciLean/Tactic/FTrans/Init.lean index 1d7c3a65..c14ddfd5 100644 --- a/SciLean/Tactic/FTrans/Init.lean +++ b/SciLean/Tactic/FTrans/Init.lean @@ -1,7 +1,7 @@ import Qq import Lean.Meta.Tactic.Simp.Types -import Std.Data.RBMap.Alter +import Batteries.Data.RBMap.Alter import Mathlib.Data.FunLike.Basic @@ -128,12 +128,12 @@ def mkFTransExt (n : Name) : ImportM FTransExt := do IO.ofExcept <| unsafe env.evalConstCheck FTransExt opts ``FTransExt n -initialize ftransExt : PersistentEnvExtension (Name Γ— Name) (Name Γ— FTransExt) (Std.RBMap Name FTransExt Name.quickCmp) ← +initialize ftransExt : PersistentEnvExtension (Name Γ— Name) (Name Γ— FTransExt) (Batteries.RBMap Name FTransExt Name.quickCmp) ← registerPersistentEnvExtension { mkInitial := pure {} addImportedFn := fun s => do - let mut r : Std.RBMap Name FTransExt Name.quickCmp := {} + let mut r : Batteries.RBMap Name FTransExt Name.quickCmp := {} for s' in s do for (ftransName, extName) in s' do @@ -230,7 +230,7 @@ local instance : Ord Name := ⟨Name.quickCmp⟩ /-- This holds a collection of function transformation rules for a fixed constant -/ -def FTransRules := Std.RBMap Name (Std.RBSet FTransRule FTransRule.cmp) compare +def FTransRules := Batteries.RBMap Name (Batteries.RBSet FTransRule FTransRule.cmp) compare namespace FTransRules @@ -243,9 +243,9 @@ namespace FTransRules fp.alter ftransName (Ξ» p? => match p? with | some p => some (p.insert rule) - | none => some (Std.RBSet.empty.insert rule)) + | none => some (Batteries.RBSet.empty.insert rule)) - def empty : FTransRules := Std.RBMap.empty + def empty : FTransRules := Batteries.RBMap.empty end FTransRules @@ -293,8 +293,8 @@ where is name of the function transformation and is corresponding let suggestedRuleName := data.constName - |>.append data.declSuffix - |>.append (transName.getString.append "_rule") + |>.append (.mkSimple data.declSuffix) + |>.append (.mkSimple (transName.lastComponentAsString.append "_rule")) if (← getBoolOption `linter.ftransDeclName) && Β¬(suggestedRuleName.toString.isPrefixOf ruleName.toString) then diff --git a/SciLean/Tactic/FunTrans/Attr.lean b/SciLean/Tactic/FunTrans/Attr.lean new file mode 100644 index 00000000..23d66d08 --- /dev/null +++ b/SciLean/Tactic/FunTrans/Attr.lean @@ -0,0 +1,42 @@ +/- +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 SciLean.Tactic.FunTrans.Decl +import SciLean.Tactic.FunTrans.Theorems + +/-! +## `funTrans` attribute +-/ + + +namespace Mathlib +open Lean Meta + +namespace Meta.FunTrans + + +private def funTransHelpString : String := +"`funTrans` tactic to compute function transformations like `fderiv` or `adjoint`" + +/-- Initialization of `funTrans` attribute -/ +initialize funTransAttr : Unit ← + registerBuiltinAttribute { + name := `fun_trans + descr := funTransHelpString + applicationTime := AttributeApplicationTime.afterCompilation + add := fun declName _stx attrKind => + discard <| MetaM.run do + let info ← getConstInfo declName + + forallTelescope info.type fun _ b => do + if b.isEq then + addTheorem declName attrKind + else + addFunTransDecl declName + erase := fun _declName => + throwError "can't remove `funTrans` attribute (not implemented yet)" + } diff --git a/SciLean/Tactic/FunTrans/Core.lean b/SciLean/Tactic/FunTrans/Core.lean new file mode 100644 index 00000000..73092393 --- /dev/null +++ b/SciLean/Tactic/FunTrans/Core.lean @@ -0,0 +1,605 @@ +/- +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 Qq +import Batteries.Tactic.Exact + +import SciLean.Tactic.FunTrans.Theorems +import SciLean.Tactic.FunTrans.Types +import Mathlib.Tactic.FunProp.Core +import Mathlib.Tactic.FunProp.Types + +/-! +## `funTrans` core tactic algorithm +-/ + +namespace Mathlib +open Lean Meta Qq + +namespace Meta.FunTrans + +def runFunProp (e : Expr) : SimpM (Option Expr) := do + let cache := (← get).cache + modify (fun s => { s with cache := {}}) -- hopefully this prevent duplicating the cache + let config : FunProp.Config := (← funTransConfig.get).funPropConfig + let state : FunProp.State := { cache := cache } + let (result?, state) ← FunProp.funProp e |>.run config state + modify (fun simpState => { simpState with cache := state.cache }) + + match result? with + | .some r => return r.proof + | .none => return .none + + +private def ppOrigin' (origin : FunProp.Origin) : MetaM String := do + match origin with + | .fvar id => return s!"{← ppExpr (.fvar id)} : {← ppExpr (← inferType (.fvar id))}" + | _ => pure (toString origin.name) + + +-- TODO: remove this once updated to newer version of mathlib +/-- Is `e` a `fun_prop` goal? For example `βˆ€ y z, Continuous fun x => f x y z` -/ +private def FunProp.isFunPropGoal (e : Expr) : MetaM Bool := do + forallTelescope e fun _ b => + return (← FunProp.getFunProp? b).isSome + + +def synthesizeArgs (thmId : FunProp.Origin) (xs : Array Expr) : SimpM Bool := do + let mut postponed : Array Expr := #[] + for x in xs do + let type ← inferType x + if (← instantiateMVars x).isMVar then + -- A hypothesis can be both a type class instance as well as a proposition, + -- in that case we try both TC synthesis and the discharger + -- (because we don't know whether the argument was originally explicit or instance-implicit). + if (← isClass? type).isSome then + if (← synthesizeInstance x type) then + continue + + if (← isProp type) then + if ← FunProp.isFunPropGoal type then + if let .some r ← runFunProp type then + x.mvarId!.assignIfDefeq r + continue + else + let disch := (← funTransConfig.get).funPropConfig.disch + if let .some r ← disch type then + x.mvarId!.assignIfDefeq r + continue + + if Β¬(← isProp type) then + postponed := postponed.push x + continue + else + trace[Meta.Tactic.fun_trans] + "{← ppOrigin' thmId}, failed to discharge hypotheses{indentExpr type}" + return false + + for x in postponed do + if (← instantiateMVars x).isMVar then + trace[Meta.Tactic.fun_trans] + "{← ppOrigin' thmId}, failed to infer `({← ppExpr x} : {← ppExpr (← inferType x)})`" + return false + + return true +where + synthesizeInstance (x type : Expr) : SimpM Bool := do + match (← trySynthInstance type) with + | LOption.some val => + if (← withReducibleAndInstances <| isDefEq x val) then + return true + else + trace[Meta.Tactic.fun_trans.discharge] "{← ppOrigin' thmId}, failed to assign instance{indentExpr type}\nsythesized value{indentExpr val}\nis not definitionally equal to{indentExpr x}" + return false + | _ => + trace[Meta.Tactic.fun_trans.discharge] "{← ppOrigin' thmId}, failed to synthesize instance{indentExpr type}" + return false + + + +def tryTheoremCore (lhs : Expr) (xs : Array Expr) (val : Expr) (type : Expr) (e : Expr) (thmId : FunProp.Origin) : SimpM (Option Simp.Result) := do + withTraceNode `Meta.Tactic.fun_trans + (fun r => return s!"[{ExceptToEmoji.toEmoji r}] applying: {← ppOrigin' thmId}") do + + unless (← isDefEq lhs (← instantiateMVars e)) do + trace[Meta.Tactic.fun_trans.unify] "failed to unify {← ppOrigin' thmId}\n{lhs}\nwith\n{e}" + return none + + if Β¬(← synthesizeArgs thmId xs) then + return none + + let proof ← instantiateMVars (mkAppN val xs) + let rhs := (← instantiateMVars type).appArg! + if e == rhs then + return none + trace[Meta.Tactic.fun_trans] "{← ppOrigin' thmId}, \n{e}\n==>\n{rhs}" + return .some { expr := rhs, proof? := proof } + + +def tryTheoremWithHint (e : Expr) (thmOrigin : FunProp.Origin) (hint : Array (Nat Γ— Expr)) : SimpM (Option Simp.Result) := do + + let proof ← thmOrigin.getValue + let type ← instantiateMVars (← inferType proof) + let (xs, _, type) ← forallMetaTelescope type + let .some (_,lhs,_) := type.eq? + | throwError "fun_trans bug: applying theorem {← ppExpr type} that is not an equality" + + try + for (id,v) in hint do + xs[id]!.mvarId!.assignIfDefeq v + catch _ => + trace[Meta.Tactic.fun_trans.discharge] "failed to use `{← FunProp.ppOrigin thmOrigin}` on `{e}`" + return .none + + let extraArgsNum := e.getAppNumArgs - lhs.getAppNumArgs + let e' := e.stripArgsN extraArgsNum + let extraArgs := e.getAppArgsN extraArgsNum + let .some r ← tryTheoremCore lhs xs proof type e' thmOrigin | return .none + return (← r.addExtraArgs extraArgs) + + +def tryTheorem? (e : Expr) (thmOrigin : FunProp.Origin) : SimpM (Option Simp.Result) := + tryTheoremWithHint e thmOrigin #[] + + +def applyIdRule (funTransDecl : FunTransDecl) (e X : Expr) : SimpM (Option Simp.Result) := do + trace[Meta.Tactic.fun_trans.step] "id case" + + let .some thms ← getLambdaTheorems funTransDecl.funTransName .id e.getAppNumArgs + | trace[Meta.Tactic.fun_trans] "missing identity rule to transform `{← ppExpr e}`" + return none + + for thm in thms do + let .id id_X := thm.thmArgs | continue + + if let .some r ← tryTheoremWithHint e (.decl thm.thmName) #[(id_X,X)] then + return r + + return none + +def applyConstRule (funTransDecl : FunTransDecl) (e : Expr) : SimpM (Option Simp.Result) := do + let .some thms ← getLambdaTheorems funTransDecl.funTransName .const e.getAppNumArgs + | trace[Meta.Tactic.fun_trans] "missing const rule to transform `{← ppExpr e}`" + return none + + for thm in thms do + let .const := thm.thmArgs | continue + + if let .some r ← tryTheoremWithHint e (.decl thm.thmName) #[] then + return r + + return none + + + +def applyCompRule (funTransDecl : FunTransDecl) (e f g : Expr) : SimpM (Option Simp.Result) := do + let .some thms ← getLambdaTheorems funTransDecl.funTransName .comp e.getAppNumArgs + | trace[Meta.Tactic.fun_trans] "missing comp rule to transform `{← ppExpr e}`" + return none + + for thm in thms do + let .comp id_f id_g := thm.thmArgs | continue + trace[Meta.Tactic.fun_trans] "trying comp theorem {thm.thmName}" + if let .some r ← tryTheoremWithHint e (.decl thm.thmName) #[(id_f,f),(id_g,g)] then + return r + + return none + +def applyLetRule (funTransDecl : FunTransDecl) (e f g : Expr) : SimpM (Option Simp.Result) := do + let .some thms ← getLambdaTheorems funTransDecl.funTransName .letE e.getAppNumArgs + | trace[Meta.Tactic.fun_trans] "missing let rule to transform `{← ppExpr e}`" + return none + + for thm in thms do + let .letE id_f id_g := thm.thmArgs | continue + + if let .some r ← tryTheoremWithHint e (.decl thm.thmName) #[(id_f,f),(id_g,g)] then + return r + + return none + +def applyApplyRule (funTransDecl : FunTransDecl) (e x XY : Expr) : SimpM (Option Simp.Result) := do + let ext := lambdaTheoremsExt.getState (← getEnv) + let .forallE n X Y _ := XY | return none + + -- non dependent case + if Β¬(Y.hasLooseBVars) then + if let .some thms := ext.theorems.find? (funTransDecl.funTransName, .proj) then + for thm in thms do + let .proj id_x id_Y := thm.thmArgs | return none + if let .some r ← tryTheoremWithHint e (.decl thm.thmName) #[(id_x,x),(id_Y,Y)] then + return r + + -- dependent case + -- can also handle non-dependent cases if non-dependent theorem is not available + let Y := Expr.lam n X Y default + + let .some thms := ext.theorems.find? (funTransDecl.funTransName, .projDep) + | trace[Meta.Tactic.fun_trans] + "missing projection rule to transform `{← ppExpr e}`" + return none + for thm in thms do + let .projDep id_x id_Y := thm.thmArgs | return none + + if let .some r ← tryTheoremWithHint e (.decl thm.thmName) #[(id_x,x),(id_Y,Y)] then + return r + + return none + +def applyApplyDepRule (funTransDecl : FunTransDecl) (e x Y : Expr) : SimpM (Option Simp.Result) := do + let .some thms ← getLambdaTheorems funTransDecl.funTransName .projDep e.getAppNumArgs + | trace[Meta.Tactic.fun_trans] "missing projDep rule to transform `{← ppExpr e}`" + return none + + for thm in thms do + let .projDep id_x id_Y := thm.thmArgs | continue + + if let .some r ← tryTheoremWithHint e (.decl thm.thmName) #[(id_x,x),(id_Y,Y)] then + return r + + return none + +def applyPiRule (funTransDecl : FunTransDecl) (e f : Expr) : SimpM (Option Simp.Result) := do + let .some thms ← getLambdaTheorems funTransDecl.funTransName .pi e.getAppNumArgs + | trace[Meta.Tactic.fun_trans] "missing pi rule to transform `{← ppExpr e}`" + return none + + for thm in thms do + let .pi id_f := thm.thmArgs | continue + + if let .some r ← tryTheoremWithHint e (.decl thm.thmName) #[(id_f,f)] then + return r + + return none + + + +def applyMorTheorems (funTransDecl : FunTransDecl) (e : Expr) (fData : FunProp.FunctionData) : SimpM (Option Simp.Result) := do + + match ← fData.isMorApplication with + | .none => return none + | .underApplied => + applyPiRule funTransDecl e (← fData.toExpr) + | .overApplied => + let .some (f,g) ← fData.peeloffArgDecomposition | return none + applyCompRule funTransDecl e f g + | .exact => + let ext := (morTheoremsExt.getState (← getEnv)) + + let candidates ← ext.theorems.getMatchWithScoreWithExtra e false { iota := false, zeta := false } + let candidates := candidates.map (Β·.1) |>.flatten + + trace[Meta.Tactic.fun_trans] + "candidate morphism theorems: {← candidates.mapM fun c => ppOrigin (.decl c.thmName)}" + + for c in candidates do + if let .some r ← tryTheoremWithHint e (.decl c.thmName) #[] then + return r + + return none + +def applyFVarTheorems (e : Expr) : SimpM (Option Simp.Result) := do + + let ext := (fvarTheoremsExt.getState (← getEnv)) + + let candidates ← ext.theorems.getMatchWithScoreWithExtra e false { iota := false, zeta := false } + let candidates := candidates.map (Β·.1) |>.flatten + + trace[Meta.Tactic.fun_trans] + "candidate fvar theorems: {← candidates.mapM fun c => ppOrigin (.decl c.thmName)}" + + for c in candidates do + if let .some r ← tryTheoremWithHint e (.decl c.thmName) #[] then + return .some r + + return none + +def getLocalTheorems (funTransDecl : FunTransDecl) (funOrigin : FunProp.Origin) + (mainArgs : Array Nat) (appliedArgs : Nat) : MetaM (Array FunctionTheorem) := do + + let mut thms : Array FunctionTheorem := #[] + let lctx ← getLCtx + for var in lctx do + if (var.kind = Lean.LocalDeclKind.auxDecl) then + continue + let type ← instantiateMVars var.type + let thm? : Option FunctionTheorem ← + forallTelescope type fun _ b => do + let b ← whnfR b + let .some (_,lhs,_) := b.eq? | return none + let .some (decl,f) ← getFunTrans? lhs | return none + unless decl.funTransName = funTransDecl.funTransName do return none + + let .data fData ← FunProp.getFunctionData? f FunProp.defaultUnfoldPred | return none + unless (fData.getFnOrigin == funOrigin) do return none + + unless FunProp.isOrderedSubsetOf mainArgs fData.mainArgs do return none + + let dec? ← fData.nontrivialDecomposition + + let thm : FunctionTheorem := { + funTransName := funTransDecl.funTransName + transAppliedArgs := lhs.getAppNumArgs + thmOrigin := .fvar var.fvarId + funOrigin := funOrigin + mainArgs := fData.mainArgs + appliedArgs := fData.args.size + priority := eval_prio default + form := if dec?.isSome then .comp else .uncurried + } + + return .some thm + + if let .some thm := thm? then + thms := thms.push thm + + thms := thms + |>.qsort (fun t s => + let dt := (Int.ofNat t.appliedArgs - Int.ofNat appliedArgs).natAbs + let ds := (Int.ofNat s.appliedArgs - Int.ofNat appliedArgs).natAbs + match compare dt ds with + | .lt => true + | .gt => false + | .eq => t.mainArgs.size < s.mainArgs.size) + + return thms + + +def tryTheorems (funTransDecl : FunTransDecl) (e : Expr) (fData : FunProp.FunctionData) + (thms : Array FunctionTheorem) : SimpM (Option Simp.Result) := do + -- none - decomposition not tried + -- some none - decomposition failed + -- some some (f, g) - succesfull decomposition + let mut dec? : Option (Option (Expr Γ— Expr)) := none + + for thm in thms do + + trace[Meta.Tactic.fun_trans.step] s!"trying theorem {← ppOrigin' thm.thmOrigin}" + + match compare thm.appliedArgs fData.args.size with + | .lt => + trace[Meta.Tactic.fun_trans] s!"removing argument to later use {← ppOrigin' thm.thmOrigin}" + trace[Meta.Tactic.fun_trans] s!"NOT IMPLEMENTED" + -- if let .some r ← removeArgRule funTransDecl e fData funTrans then + -- return r + return none + | .gt => + trace[Meta.Tactic.fun_trans] s!"adding argument to later use {← ppOrigin' thm.thmOrigin}" + if let .some r ← applyPiRule funTransDecl e (← fData.toExpr) then + return r + continue + | .eq => + if thm.form == .comp then + if let .some r ← tryTheorem? e thm.thmOrigin then + return r + else + + if thm.mainArgs.size == fData.mainArgs.size then + if dec?.isNone then + dec? := .some (← fData.nontrivialDecomposition) + match dec? with + | .some .none => + if let .some r ← tryTheorem? e thm.thmOrigin then + return r + | .some (.some (f,g)) => + trace[Meta.Tactic.fun_trans.step] + s!"decomposing to later use {←ppOrigin' thm.thmOrigin}" + if let .some r ← applyCompRule funTransDecl e f g then + return r + | _ => continue + else + trace[Meta.Tactic.fun_trans.step] + s!"decomposing in args {thm.mainArgs} to later use {←ppOrigin' thm.thmOrigin}" + let .some (f,g) ← fData.decompositionOverArgs thm.mainArgs + | continue + trace[Meta.Tactic.fun_trans.step] + s!"decomposition: {← ppExpr f} ∘ {← ppExpr g}" + if let .some r ← applyCompRule funTransDecl e f g then + return r + return none + + +def letCase (funTransDecl : FunTransDecl) (e f : Expr) : SimpM (Option Simp.Result) := do + trace[Meta.Tactic.fun_trans.step] "let case" + + let .lam xName xType (.letE yName yType yVal yBody _) xBi := f | return none + + match (yBody.hasLooseBVar 0), (yBody.hasLooseBVar 1) with + | true, true => + + let f := Expr.lam xName xType (.lam yName yType yBody .default) xBi + let g := Expr.lam xName xType yVal .default + + applyLetRule funTransDecl e f g + | true, false => + let f := Expr.lam yName yType yBody default + let g := Expr.lam xName xType yVal default + + applyCompRule funTransDecl e f g + + | false, _ => + let f := Expr.lam xName xType (yBody.lowerLooseBVars 1 1) xBi + let e' := e.setArg (funTransDecl.funArgId) f + + return .some ({expr := e'}) + + + +def bvarAppCase (funTransDecl : FunTransDecl) (e : Expr) (fData : FunProp.FunctionData) : SimpM (Option Simp.Result) := do + trace[Meta.Tactic.fun_trans.step] "bvar app case" + + if (← fData.isMorApplication) != .none then + applyMorTheorems funTransDecl e fData + else + if let .some (f, g) ← fData.nontrivialDecomposition then + applyCompRule funTransDecl e f g + else + applyApplyRule funTransDecl e fData.args[0]!.expr (← fData.domainType) + + -- if let .some (f,g) ← fData.nontrivialDecomposition then + -- return ← applyCompRule funTransDecl e f g + -- else + -- if fData.args.size = 1 then + -- let x := fData.args[0]! + -- if x.coe.isSome then + -- trace[Meta.Tactic.fun_trans.step] "morphism apply case" + -- if let .some r ← applyMorTheorems funTransDecl e fData then + -- return r + -- return none + -- else + -- let x := x.expr + -- let .forallE xName X Y bi ← withLCtx fData.lctx fData.insts do inferType fData.fn + -- | return none + + -- if Y.hasLooseBVars then + -- let Y := Expr.lam xName X Y bi + -- return ← applyApplyDepRule funTransDecl e x Y + -- else + -- return ← applyApplyRule funTransDecl e x Y + -- else + -- -- can we get here? + -- throwError "fun_trans bug: bvar app unhandled case" + + +def fvarAppCase (funTransDecl : FunTransDecl) (e : Expr) (fData : FunProp.FunctionData) : SimpM (Option Simp.Result) := do + trace[Meta.Tactic.fun_trans.step] "fvar app case" + if let .some (f,g) ← fData.nontrivialDecomposition then + if let .some r ← applyMorTheorems funTransDecl e fData then + return r + + return ← applyCompRule funTransDecl e f g + else + + let .fvar fvarId := fData.fn | throwError "fun_trans bug: incorrectly calling fvarAppCase!" + + let thms ← getLocalTheorems funTransDecl (.fvar fvarId) fData.mainArgs e.getAppNumArgs + trace[Meta.Tactic.fun_trans] "candidate local theorems for {← ppExpr (.fvar fvarId)}: {thms.map fun thm => thm.thmOrigin.name}" + if let .some r ← tryTheorems funTransDecl e fData thms then + return r + + if let .some r ← applyMorTheorems funTransDecl e fData then + return r + + if let .some r ← applyFVarTheorems e then + return r + + return none + +/-- Prevend applying morphism theorems to `fun fx => ⇑(Prod.fst fx) (Prod.snd fx)` -/ +def morphismGuard (fData : FunProp.FunctionData) : MetaM Bool := do + + trace[Meta.Tactic.fun_trans] "running guard on {← ppExpr (←fData.toExpr)}" + trace[Meta.Tactic.fun_trans] "morphism guard 0 {fData.args.size}" + unless fData.args.size == 4 do return true + trace[Meta.Tactic.fun_trans] "morphism guard 1 {fData.args[3]!.coe.isSome}" + unless fData.args[3]!.coe.isSome do return true + trace[Meta.Tactic.fun_trans] "morphism guard 2 {(← fData.getFnConstName?)}" + unless (← fData.getFnConstName?) == .some ``Prod.fst do return true + trace[Meta.Tactic.fun_trans] "morphism guard 3 {← ppExpr fData.args[2]!.expr}" + unless fData.args[2]!.expr == fData.mainVar do return true + trace[Meta.Tactic.fun_trans] "morphism guard 4" + unless fData.args[3]!.expr.isAppOfArity ``Prod.snd 3 do return true + trace[Meta.Tactic.fun_trans] "morphism guard 5 {← ppExpr fData.args[3]!.expr.appArg!}" + unless fData.args[3]!.expr.appArg! == fData.mainVar do return true + trace[Meta.Tactic.fun_trans] "morphism guard 6" + + return false + + +def constAppCase (funTransDecl : FunTransDecl) (e : Expr) (fData : FunProp.FunctionData) : SimpM (Option Simp.Result) := do + trace[Meta.Tactic.fun_trans.step] "const app case on {← ppExpr e}" + + let .some funName ← fData.getFnConstName? + | throwError "fun_trans bug: incorrectly calling constAppCase!" + + let thms ← + getTheoremsForFunction funName funTransDecl.funTransName e.getAppNumArgs fData.mainArgs + trace[Meta.Tactic.fun_trans] + "candidate theorems for {funName}: {thms.map fun thm => thm.thmOrigin.name}" + if let .some r ← tryTheorems funTransDecl e fData thms then + return r + + let thms ← getLocalTheorems funTransDecl (.decl funName) fData.mainArgs e.getAppNumArgs + trace[Meta.Tactic.fun_trans] + "candidate local theorems for {funName}: {thms.map fun thm => thm.thmOrigin.name}" + if let .some r ← tryTheorems funTransDecl e fData thms then + return r + + -- if ← morphismGuard fData then + if let .some r ← applyMorTheorems funTransDecl e fData then + return r + + if let .some (f,g) ← fData.nontrivialDecomposition then + -- if ← morphismGuard fData then + if let .some r ← applyCompRule funTransDecl e f g then + return r + else + if let .some r ← applyFVarTheorems e then + return r + + return none + +local instance {Ξ΅} : ExceptToEmoji Ξ΅ (Simp.Step) := + ⟨fun s => + match s with + | .ok (.continue .none) => crossEmoji + | .ok _ => checkEmoji + | .error _ => bombEmoji⟩ + +/-- Main `funProp` function. Returns proof of `e`. -/ +partial def funTrans (e : Expr) : SimpM Simp.Step := do + + let e ← instantiateMVars e + + let .some (funTransDecl, f) ← getFunTrans? e | return .continue + + if e.approxDepth > 200 then + throwError "fun_trans, expression is too deep({e.approxDepth})\n{← ppExpr e}" + + withTraceNode `Meta.Tactic.fun_trans + (fun r => return s!"[{ExceptToEmoji.toEmoji r}] {← ppExpr e}") do + + -- bubble leading lets infront of function transformationx + if f.isLet then + return ← FunProp.letTelescope f fun xs b => do + trace[Meta.Tactic.fun_trans.step] "moving let bindings out" + let e' := e.setArg funTransDecl.funArgId b + return .visit { expr := ← mkLambdaFVars xs e' } + + let toStep (e : SimpM (Option Simp.Result)) : SimpM Simp.Step := do + if let .some r ← e then + return .visit r + else + return .continue + + match ← FunProp.getFunctionData? f FunProp.defaultUnfoldPred {zeta:=false} with + | .letE f => + trace[Meta.Tactic.fun_trans.step] "let case on {← ppExpr f}" + let e := e.setArg funTransDecl.funArgId f -- update e with reduced f + toStep <| letCase funTransDecl e f + | .lam f => + trace[Meta.Tactic.fun_trans.step] "lam case on {← ppExpr f}" + let e := e.setArg funTransDecl.funArgId f -- update e with reduced f + toStep <| applyPiRule funTransDecl e f + | .data fData => + let e := e.setArg funTransDecl.funArgId (← fData.toExpr) -- update e with reduced f + + if fData.isIdentityFun then + toStep <| applyIdRule funTransDecl e (← fData.domainType) + else if fData.isConstantFun then + toStep <| applyConstRule funTransDecl e + else + match fData.fn with + | .fvar id => + if id == fData.mainVar.fvarId! + then toStep <| bvarAppCase funTransDecl e fData + else toStep <| fvarAppCase funTransDecl e fData + | .mvar .. => funTrans (← instantiateMVars e) + | .const .. + | .proj .. => toStep <| constAppCase funTransDecl e fData + | _ => + trace[Meta.Tactic.fun_trans.step] "unknown case, ctor: {fData.fn.ctorName}\n{e}" + return .continue diff --git a/SciLean/Tactic/FunTrans/Decl.lean b/SciLean/Tactic/FunTrans/Decl.lean new file mode 100644 index 00000000..531d9316 --- /dev/null +++ b/SciLean/Tactic/FunTrans/Decl.lean @@ -0,0 +1,129 @@ +/- +Copyright (c) 2024 Tomas Skrivan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Tomas Skrivan +-/ +import Qq + +/-! +## `funTrans` environment extension that stores all registered function properties +-/ + + +namespace Mathlib +open Lean Meta + +namespace Meta.FunTrans + + + +initialize registerTraceClass `Meta.Tactic.fun_trans.attr +initialize registerTraceClass `Meta.Tactic.fun_trans + +initialize registerTraceClass `Meta.Tactic.fun_trans.step +initialize registerTraceClass `Meta.Tactic.fun_trans.unify +initialize registerTraceClass `Meta.Tactic.fun_trans.discharge +initialize registerTraceClass `Meta.Tactic.fun_trans.rewrite +initialize registerTraceClass `Meta.Tactic.fun_trans.unfold +initialize registerTraceClass `Meta.Tactic.fun_trans.cache + + + +/-- Basic information about function transformation -/ +structure FunTransDecl where + /-- function transformation name -/ + funTransName : Name + /-- path for discriminatory tree -/ + path : Array DiscrTree.Key + /-- argument index of a function this function transformation talks about. + For example, this would be 8 for `@fderiv π•œ _ E _ _ F _ _ f` -/ + funArgId : Nat + deriving Inhabited, BEq + +/-- -/ +structure FunTransDecls where + /-- discriminatory tree for function transformations -/ + decls : DiscrTree FunTransDecl := {} + deriving Inhabited + +/-- -/ +abbrev FunTransDeclsExt := SimpleScopedEnvExtension FunTransDecl FunTransDecls + +/-- -/ +initialize funTransDeclsExt : FunTransDeclsExt ← + registerSimpleScopedEnvExtension { + name := by exact decl_name% + initial := {} + addEntry := fun d e => + {d with decls := d.decls.insertCore e.path e} + } + +/-- -/ +def addFunTransDecl (declName : Name) : MetaM Unit := do + + let info ← getConstInfo declName + + let (xs,_,_) ← forallMetaTelescope info.type + + -- find the argument position of the function `f` in `P f` + let mut .some funArgId ← xs.reverse.findIdxM? fun x => do + if (← inferType x).isForall then + return true + else + return false + | throwError "invalid fun_trans declaration, can't find argument of type `Ξ± β†’ Ξ²`" + funArgId := xs.size - funArgId - 1 + + let lvls := info.levelParams.map (fun l => Level.param l) + let e := mkAppN (.const declName lvls) xs[0:funArgId+1] + let path ← DiscrTree.mkPath e {} + + let decl : FunTransDecl := { + funTransName := declName + path := path + funArgId := funArgId + } + + modifyEnv fun env => funTransDeclsExt.addEntry env decl + + trace[Meta.Tactic.fun_trans.attr] + "added new function property `{declName}`\nlook up pattern is `{path}`" + + +/-- -/ +def getFunTrans? (e : Expr) : MetaM (Option (FunTransDecl Γ— Expr)) := do + unless e.isApp do return .none + + let ext := funTransDeclsExt.getState (← getEnv) + + let decls ← ext.decls.getMatchWithExtra e + {zeta:=false,zetaDelta:=false,proj:=.no,iota:=false,beta:=false} + + if decls.size = 0 then + return none + + if decls.size > 1 then + throwError "\ +fun_trans bug: expression {← ppExpr e} matches multiple function transformations +{decls.map (fun d => d.1.funTransName)}" + + let decl := decls[0]!.fst + let f := e.getArg! decl.funArgId + + return (decl,f) + +/-- -/ +def isFunTrans (e : Expr) : MetaM Bool := do return (← getFunTrans? e).isSome + +/-- Returns function property transformation from `e = T f`. -/ +def getFunTransDecl? (e : Expr) : MetaM (Option FunTransDecl) := do + match ← getFunTrans? e with + | .some (decl,_) => return decl + | .none => return none + + +/-- Returns function `f` from `e = T f` and `T` is function transformation. -/ +def getFunTransFun? (e : Expr) : MetaM (Option Expr) := do + match ← getFunTrans? e with + | .some (_,f) => return f + | .none => return none diff --git a/SciLean/Tactic/FunTrans/Elab.lean b/SciLean/Tactic/FunTrans/Elab.lean new file mode 100644 index 00000000..866b0f09 --- /dev/null +++ b/SciLean/Tactic/FunTrans/Elab.lean @@ -0,0 +1,85 @@ +/- +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.Core +import SciLean.Tactic.FunTrans.Core + +/-! +## `funProp` tactic syntax +-/ + +namespace Mathlib +open Lean Meta Elab Tactic + +namespace Meta.FunTrans + +open Lean.Parser.Tactic + + +syntax (name := funTransTacStx) "fun_trans" (config)? (discharger)? (&" only")? + (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? (location)? : tactic + +syntax (name := funTransConvStx) "fun_trans" (config)? (discharger)? (&" only")? + (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*) "]")? : conv + + +simproc_decl fun_trans_simproc (_) := funTrans + +private def emptyDischarge : Expr β†’ MetaM (Option Expr) := + fun e => + withTraceNode `Meta.Tactic.fun_trans + (fun r => do pure s!"[{ExceptToEmoji.toEmoji r}] discharging: {← ppExpr e}") do + pure none + +private def stxToDischarge (stx : Option (TSyntax ``discharger)) : Expr β†’ MetaM (Option Expr) := fun e => do + match stx with + | none => (emptyDischarge e) + | some d => + match d with + | `(discharger| (discharger:=$tac)) => FunProp.tacticToDischarge (← `(tactic| ($tac))) e + | _ => emptyDischarge e + + +@[tactic funTransTacStx] +def funTransTac : Tactic := fun stx => do + match stx with + | `(tactic| fun_trans $[$cfg]? $[$disch]? $[only]? $[[$a,*]]? $[$loc]?) => do + + -- set fun_trans config + funTransConfig.modify + fun c => { c with funPropConfig := { c.funPropConfig with disch := stxToDischarge disch}} + + let a := a.getD (Syntax.TSepArray.mk #[]) + if stx[3].isNone then + evalTactic (← `(tactic| simp $[$cfg]? $[$disch]? [↓fun_trans_simproc,$a,*] $[$loc]?)) + else + evalTactic (← `(tactic| simp $[$cfg]? $[$disch]? only [↓fun_trans_simproc,$a,*] $[$loc]?)) + + -- reset fun_trans config + funTransConfig.modify fun _ => {} + + | _ => throwUnsupportedSyntax + + +@[tactic funTransConvStx] +def funTransConv : Tactic := fun stx => do + match stx with + | `(conv| fun_trans $[$cfg]? $[$disch]? $[only]? $[[$a,*]]?) => do + + -- set fun_trans config + funTransConfig.modify + fun c => { c with funPropConfig := { c.funPropConfig with disch := stxToDischarge disch}} + + let a := a.getD (Syntax.TSepArray.mk #[]) + if stx[3].isNone then + evalTactic (← `(conv| simp $[$cfg]? $[$disch]? [↓fun_trans_simproc,$a,*])) + else + evalTactic (← `(conv| simp $[$cfg]? $[$disch]? only [↓fun_trans_simproc,$a,*])) + + -- reset fun_trans config + funTransConfig.modify fun _ => {} + + | _ => throwUnsupportedSyntax diff --git a/SciLean/Tactic/FunTrans/Theorems.lean b/SciLean/Tactic/FunTrans/Theorems.lean new file mode 100644 index 00000000..828c2190 --- /dev/null +++ b/SciLean/Tactic/FunTrans/Theorems.lean @@ -0,0 +1,353 @@ +/- +Copyright (c) 2024 Tomas Skrivan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Tomas Skrivan +-/ +import Batteries.Data.RBMap.Alter + +import SciLean.Tactic.FunTrans.Decl +import Mathlib.Tactic.FunProp.Theorems + +/-! +## `fun_trans` enviroment extensions storing thorems for `fun_trans` +-/ + +namespace Mathlib +open Lean Meta + +namespace Meta.FunTrans + +/-- -/ +structure LambdaTheorem where + /-- Name of function transformation -/ + funTransName : Name + /-- Name of lambda theorem -/ + thmName : Name + /-- total number of arguments applied to the function transformation -/ + transAppliedArgs : Nat + /-- Type and important argument of the theorem. -/ + thmArgs : FunProp.LambdaTheoremArgs + deriving Inhabited, BEq + +/-- -/ +structure LambdaTheorems where + /-- map: function transfromation name Γ— theorem type β†’ lambda theorem -/ + theorems : HashMap (Name Γ— FunProp.LambdaTheoremType) (Array LambdaTheorem) := {} + deriving Inhabited + + +/-- return proof of lambda theorem -/ +def LambdaTheorem.getProof (thm : LambdaTheorem) : MetaM Expr := do + mkConstWithFreshMVarLevels thm.thmName + +/-- -/ +abbrev LambdaTheoremsExt := SimpleScopedEnvExtension LambdaTheorem LambdaTheorems + +/-- Extension storing all lambda theorems. -/ +initialize lambdaTheoremsExt : LambdaTheoremsExt ← + registerSimpleScopedEnvExtension { + name := by exact decl_name% + initial := {} + addEntry := fun d e => + {d with theorems := + let es := d.theorems.findD (e.funTransName, e.thmArgs.type) #[] + d.theorems.insert (e.funTransName, e.thmArgs.type) (es.push e)} + } + +/-- Return lambda theorems of type `type` for function transformation `funTransName` + +Theorems are filtered and sorted based on the optional argument `nargs`. It specifies the number of +arguments of the expression we want to transform. + +For example when transforming +``` +deriv (fun x => x * sin x) +``` +we do not want to use composition theorem stating `deriv (fun x' => f (g x')) x` because our +expression does not have the concrete point where we differentiate. + +On the other hand when transforming +``` +deriv (fun x' => 1/(1-x')) x +``` +we prefer the version `deriv (fun x' => f (g x')) x` over `deriv (fun x' => f (g x'))` as the former +uses `DifferntiableAt` insed of `Differentiable` as preconditions. -/ +def getLambdaTheorems (funTransName : Name) (type : FunProp.LambdaTheoremType) (nargs : Option Nat): + CoreM (Option (Array LambdaTheorem)) := do + let .some thms := (lambdaTheoremsExt.getState (← getEnv)).theorems.find? (funTransName,type) + | return none + + match nargs with + | none => return thms + | some n => + let thms := thms + |>.filter (fun thm => thm.transAppliedArgs ≀ n) + |>.qsort (fun t t' => t'.transAppliedArgs < t.transAppliedArgs) + return thms + + +---------------------------------------------------------------------------------------------------- + + +/-- theorem about specific function (either declared constant or free variable) -/ +structure FunctionTheorem where + /-- function transformation name -/ + funTransName : Name + /-- total number of arguments applied to the function transformation -/ + transAppliedArgs : Nat + /-- theorem name -/ + thmOrigin : FunProp.Origin + /-- function name -/ + funOrigin : FunProp.Origin + /-- array of argument indices about which this theorem is about -/ + mainArgs : Array Nat + /-- total number of arguments applied to the function -/ + appliedArgs : Nat + /-- priority -/ + priority : Nat := eval_prio default + /-- form of the theorem, see documentation of TheoremForm -/ + form : FunProp.TheoremForm + deriving Inhabited, BEq + + +private local instance : Ord Name := ⟨Name.quickCmp⟩ + +/-- -/ +structure FunctionTheorems where + /-- map: function name β†’ function transformation β†’ function theorem -/ + theorems : Batteries.RBMap Name (Batteries.RBMap Name (Array FunctionTheorem) compare) compare := {} + deriving Inhabited + + +/-- return proof of function theorem -/ +def FunctionTheorem.getProof (thm : FunctionTheorem) : MetaM Expr := do + match thm.thmOrigin with + | .decl name => mkConstWithFreshMVarLevels name + | .fvar id => pure (.fvar id) + + +/-- -/ +abbrev FunctionTheoremsExt := SimpleScopedEnvExtension FunctionTheorem FunctionTheorems + +/-- Extension storing all function theorems. -/ +initialize functionTheoremsExt : FunctionTheoremsExt ← + registerSimpleScopedEnvExtension { + name := by exact decl_name% + initial := {} + addEntry := fun d e => + {d with + theorems := + d.theorems.alter e.funOrigin.name fun funTrans => + let funTrans := funTrans.getD {} + funTrans.alter e.funTransName fun thms => + let thms := thms.getD #[] + thms.push e} + } + + +/-- -/ +def getTheoremsForFunction (funName : Name) (funTransName : Name) (nargs : Option Nat) (mainArgs : Option (Array β„•)) : + CoreM (Array FunctionTheorem) := do + + let thms := (functionTheoremsExt.getState (← getEnv)).theorems.findD funName {} + |>.findD funTransName #[] + + let thms := thms + |>.filter (fun thm => + (nargs.map (fun n => (thm.transAppliedArgs ≀ n : Bool))).getD true + && + (mainArgs.map (fun args => FunProp.isOrderedSubsetOf args thm.mainArgs)).getD true) + |>.qsort (fun t t' => t'.transAppliedArgs < t.transAppliedArgs) + + return thms + + + +---------------------------------------------------------------------------------------------------- + +/-- General theorem about function transformation used for morphism theorems -/ +structure GeneralTheorem where + /-- function transformation name -/ + funTransName : Name + /-- theorem name -/ + thmName : Name + /-- discriminatory tree keys used to index this theorem -/ + keys : List FunProp.RefinedDiscrTree.DTExpr + /-- priority -/ + priority : Nat := eval_prio default + deriving Inhabited, BEq + +/-- Get proof of a theorem. -/ +def GeneralTheorem.getProof (thm : GeneralTheorem) : MetaM Expr := do + mkConstWithFreshMVarLevels thm.thmName + +/-- -/ +structure GeneralTheorems where + /-- -/ + theorems : FunProp.RefinedDiscrTree GeneralTheorem := {} + deriving Inhabited + +/-- -/ +abbrev GeneralTheoremsExt := SimpleScopedEnvExtension GeneralTheorem GeneralTheorems + +/-- -/ +initialize morTheoremsExt : GeneralTheoremsExt ← + registerSimpleScopedEnvExtension { + name := by exact decl_name% + initial := {} + addEntry := fun d e => + {d with theorems := e.keys.foldl (FunProp.RefinedDiscrTree.insertDTExpr Β· Β· e) d.theorems} + } + + +/-- -/ +initialize fvarTheoremsExt : GeneralTheoremsExt ← + registerSimpleScopedEnvExtension { + name := by exact decl_name% + initial := {} + addEntry := fun d e => + {d with theorems := e.keys.foldl (FunProp.RefinedDiscrTree.insertDTExpr Β· Β· e) d.theorems} + } + + + +-------------------------------------------------------------------------------- + + +/-- There are four types of theorems: +- lam - theorem about basic lambda calculus terms +- function - theorem about a specific function(declared or free variable) in specific arguments +- mor - special theorems talking about bundled morphisms/DFunLike.coe +- transition - theorems inferring one function property from another + +Examples: +- lam +``` + theorem Continuous_id : Continuous fun x => x + theorem Continuous_comp (hf : Continuous f) (hg : Continuous g) : Continuous fun x => f (g x) +``` +- function +``` + theorem Continuous_add : Continuous (fun x => x.1 + x.2) + theorem Continuous_add (hf : Continuous f) (hg : Continuous g) : + Continuous (fun x => (f x) + (g x)) +``` +- mor - the head of function body has to be ``DFunLike.code +``` + theorem ContDiff.clm_apply {f : E β†’ F β†’L[π•œ] G} {g : E β†’ F} + (hf : ContDiff π•œ n f) (hg : ContDiff π•œ n g) : + ContDiff π•œ n fun x => (f x) (g x) + theorem clm_linear {f : E β†’L[π•œ] F} : IsLinearMap π•œ f +``` +- transition - the conclusion has to be in the form `P f` where `f` is a free variable +``` + theorem linear_is_continuous [FiniteDimensional ℝ E] {f : E β†’ F} (hf : IsLinearMap π•œ f) : + Continuous f +``` +-/ +inductive Theorem where + | lam (thm : LambdaTheorem) + | function (thm : FunctionTheorem) + | mor (thm : GeneralTheorem) + | fvar (thm : GeneralTheorem) + + +/-- -/ +def getTheoremFromConst (declName : Name) (prio : Nat := eval_prio default) : MetaM Theorem := do + let info ← getConstInfo declName + forallTelescope info.type fun xs b => do + + unless b.isEq do throwError "equality expected" + + let lhs := b.getArg! 1 + + let .some (decl,f) ← getFunTrans? lhs + | throwError "unrecognized function transformation `{← ppExpr lhs}`" + let funTransName := decl.funTransName + + let fData? ← FunProp.getFunctionData? f FunProp.defaultUnfoldPred {zeta:=false} + + if let .some thmArgs ← FunProp.detectLambdaTheoremArgs (← fData?.get) xs then + return .lam { + funTransName := funTransName + transAppliedArgs := lhs.getAppNumArgs + thmName := declName + thmArgs := thmArgs + } + + let .data fData := fData? + | throwError s!"function in invalid form {← ppExpr f}" + + match fData.fn with + | .const funName _ => + + let dec ← fData.nontrivialDecomposition + let form : FunProp.TheoremForm := + if dec.isSome || funName == ``Prod.mk then .comp else .uncurried + + return .function { +-- funTransName funName fData.mainArgs fData.args.size thmForm + funTransName := funTransName + transAppliedArgs := lhs.getAppNumArgs' + thmOrigin := .decl declName + funOrigin := .decl funName + mainArgs := fData.mainArgs + appliedArgs := fData.args.size + priority := prio + form := form + } + | .fvar .. => + let (_,_,b') ← forallMetaTelescope info.type + let keys := ← FunProp.RefinedDiscrTree.mkDTExprs (b'.getArg! 1) {} false + let thm : GeneralTheorem := { + funTransName := funTransName + thmName := declName + keys := keys + priority := prio + } + + let n := fData.args.size + if n = 1 && + fData.args[0]!.coe.isNone && + fData.args[0]!.expr == fData.mainVar then + return .fvar thm + else if (n > 0) && fData.args[n-1]!.coe.isSome then + return .mor thm + else + throwError "unrecognized theoremType `{← ppExpr b}`" + | _ => + throwError "unrecognized theoremType `{← ppExpr b}`" + + +/-- -/ +def addTheorem (declName : Name) (attrKind : AttributeKind := .global) + (prio : Nat := eval_prio default) : MetaM Unit := do + match (← getTheoremFromConst declName prio) with + | .lam thm => + trace[Meta.Tactic.fun_trans.attr] "\ +lambda theorem: {thm.thmName} +function transfromations: {thm.funTransName} +type: {repr thm.thmArgs.type}" + lambdaTheoremsExt.add thm attrKind + | .function thm => + trace[Meta.Tactic.fun_trans.attr] "\ +function theorem: {thm.thmOrigin.name} +function transformation: {thm.funTransName} +function transformation applied args: {thm.transAppliedArgs} +function name: {thm.funOrigin.name} +main arguments: {thm.mainArgs} +applied arguments: {thm.appliedArgs} +form: {repr thm.form}" + functionTheoremsExt.add thm attrKind + | .mor thm => + trace[Meta.Tactic.fun_trans.attr] "\ +morphism theorem: {thm.thmName} +function transformation: {thm.funTransName} +discr tree key: {thm.keys}" + morTheoremsExt.add thm attrKind + | .fvar thm => + trace[Meta.Tactic.fun_trans.attr] "\ +fvar theorem: {thm.thmName} +function transformation: {thm.funTransName} +discr tree key: {thm.keys}" + fvarTheoremsExt.add thm attrKind diff --git a/SciLean/Tactic/FunTrans/Types.lean b/SciLean/Tactic/FunTrans/Types.lean new file mode 100644 index 00000000..4832faa3 --- /dev/null +++ b/SciLean/Tactic/FunTrans/Types.lean @@ -0,0 +1,24 @@ +/- +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.Meta.Tactic.Simp.Types + +import Mathlib.Tactic.FunProp.Types + +/-! +## `funTrans` +-/ + +namespace Mathlib +open Lean Meta + +namespace Meta.FunTrans + + +structure Config where + funPropConfig : FunProp.Config := {} +deriving Inhabited + +initialize funTransConfig : IO.Ref Config ← IO.mkRef {} diff --git a/SciLean/Tactic/FunTrans2/Core.lean b/SciLean/Tactic/FunTrans2/Core.lean index acfc5563..54c5f780 100644 --- a/SciLean/Tactic/FunTrans2/Core.lean +++ b/SciLean/Tactic/FunTrans2/Core.lean @@ -3,7 +3,7 @@ import Lean.Util.Trace import SciLean.Lean.Meta.Basic -import Mathlib.Tactic.FunTrans.Core +import SciLean.Tactic.FunTrans.Core open Lean Meta diff --git a/SciLean/Tactic/GTrans/Elab.lean b/SciLean/Tactic/GTrans/Elab.lean index 91a622ff..d2a6bf8a 100644 --- a/SciLean/Tactic/GTrans/Elab.lean +++ b/SciLean/Tactic/GTrans/Elab.lean @@ -17,8 +17,6 @@ syntax (name:=gtrans_tac) "gtrans" : tactic /-- `gtrans` as conv tactic will fill in meta variables in generalized transformation -/ syntax (name:=gtrans_conv) "gtrans" : conv -#check Nat - open Lean.Parser.Tactic in syntax (name:=gtrans_tac') "gtrans" (config)? (discharger)? (normalizer)? : tactic diff --git a/SciLean/Tactic/GTrans/MetaLCtxM.lean b/SciLean/Tactic/GTrans/MetaLCtxM.lean index f1a777f9..5e32b136 100644 --- a/SciLean/Tactic/GTrans/MetaLCtxM.lean +++ b/SciLean/Tactic/GTrans/MetaLCtxM.lean @@ -65,10 +65,10 @@ instance : MonadLift MetaM MetaLCtxM where monadLift x := fun cfg ctx => do let r ← x (.mkCtxCfg ctx cfg); pure (r, ctx) protected def MetaLCtxM.saveState : MetaLCtxM (SavedStateΓ—ContextCtx) := - return ({ core := (← getThe Core.State), meta := (← get) }, βŸ¨β† getLCtx, ← getLocalInstances⟩) + return ({ core := (← Core.saveState), meta := (← get) }, βŸ¨β† getLCtx, ← getLocalInstances⟩) def MetaLCtxM.restore (b : SavedState) (ctx : ContextCtx) : MetaLCtxM Unit := do - Core.restore b.core + b.restore modify fun s => { s with mctx := b.meta.mctx, zetaDeltaFVarIds := b.meta.zetaDeltaFVarIds, postponed := b.meta.postponed } modifyThe ContextCtx fun _ => ctx @@ -148,12 +148,12 @@ def introLetDecl (name : Name) (type? : Option Expr) (val : Expr) : MetaLCtxM Ex return (fvar, ctx) -open Lean Meta Qq in -#eval show MetaLCtxM Unit from do - let e := q(fun a b => a + b + 42) +-- open Lean Meta Qq in +-- #eval show MetaLCtxM Unit from do +-- let e := q(fun a b => a + b + 42) - let (b, xs) ← lambdaIntro e +-- let (b, xs) ← lambdaIntro e - IO.println s!"lambda body: {← ppExpr b}" - IO.println s!"lambda vars: {← liftM <| xs.mapM ppExpr}" - IO.println s!"lambda: {← ppExpr (← mkLambdaFVars xs b)}" +-- IO.println s!"lambda body: {← ppExpr b}" +-- IO.println s!"lambda vars: {← liftM <| xs.mapM ppExpr}" +-- IO.println s!"lambda: {← ppExpr (← mkLambdaFVars xs b)}" diff --git a/SciLean/Tactic/LSimp/Main.lean b/SciLean/Tactic/LSimp/Main.lean index 22969b9a..2cd939f2 100644 --- a/SciLean/Tactic/LSimp/Main.lean +++ b/SciLean/Tactic/LSimp/Main.lean @@ -306,17 +306,6 @@ partial def reduce (e : Expr) : LSimpM Expr := /- withIncRecDepth -/ do reduce e' -partial def simpLit (e : Expr) : LSimpM Result := do - match e.natLit? with - | some n => - /- If `OfNat.ofNat` is marked to be unfolded, we do not pack orphan nat literals as `OfNat.ofNat` applications - to avoid non-termination. See issue #788. -/ - if (← readThe Simp.Context).isDeclToUnfold ``OfNat.ofNat then - return { expr := e } - else - return { expr := (← mkNumeral (mkConst ``Nat) n) } - | none => return { expr := e } - partial def simpProj (e : Expr) : LSimpM Result := do match (← Meta.reduceProj? e) with | some e => @@ -672,16 +661,13 @@ partial def simpStep (e : Expr) : LSimpM Result := do | .const .. => simpConst e | .bvar .. => unreachable! | .sort .. => return { expr := e } - | .lit .. => simpLit e + | .lit .. => return { expr := e } | .mvar .. => return { expr := (← instantiateMVars e) } | .fvar .. => return { expr := (← reduceFVar (← getConfig) (← Simp.getSimpTheorems) e) } partial def cacheResult (e : Expr) (cfg : Simp.Config) (r : Result) : LSimpM Result := do if cfg.memoize && r.cache then - let ctx ← readThe Simp.Context - let dischargeDepth := ctx.dischargeDepth - let r : Result := { r with dischargeDepth } let cacheRef := (← getThe State).cache cacheRef.modify (fun c => c.insert e r) return r @@ -732,16 +718,11 @@ where -- try LSimp.Cache let cache ← (← getThe State).cache.get if let some result := cache.find? e then - if result.dischargeDepth ≀ (← readThe Simp.Context).dischargeDepth then - trace[Meta.Tactic.simp.cache] "cached result {e}==>{(←result.bindVars).expr}" - return result + return result -- try Sipm.Cache let cache := (← (← getThe State).simpState.get).cache if let some result := cache.find? e then - if result.dischargeDepth ≀ (← readThe Simp.Context).dischargeDepth then - trace[Meta.Tactic.simp.cache] "cached result {e}==>{result.expr}" - return { result with } + return { result with } trace[Meta.Tactic.simp.heads] "{repr e.toHeadIndex}" - withTraceNode `Meta.Tactic.simp.heads (fun _ => pure s!"{repr e.toHeadIndex}") do - simpLoop e + simpLoop e diff --git a/SciLean/Tactic/LSimp/Test.lean b/SciLean/Tactic/LSimp/Test.lean index 91d4cad1..1d284226 100644 --- a/SciLean/Tactic/LSimp/Test.lean +++ b/SciLean/Tactic/LSimp/Test.lean @@ -1,3 +1,4 @@ +import SciLean.Tactic.MathlibCompiledTactics import SciLean.Tactic.LSimp.Elab import SciLean.Util.RewriteBy import SciLean.Core @@ -67,7 +68,6 @@ def testExpression (n : Nat) : MetaM Q(Float β†’ Float) := #eval show MetaM Unit from do IO.println (← ppExpr (← testExpression 8)) - #check (0 + 1 + 0) rewrite_by lsimp @@ -137,7 +137,6 @@ def measureOnTestExpression (n : Nat) : MetaM (Array MeasureData) := do -- set_option trace.Meta.Tactic.simp.heads true - example (n : Nat) : n = diff --git a/SciLean/Tactic/LSimp/Types.lean b/SciLean/Tactic/LSimp/Types.lean index 0b9d0ce5..48981269 100644 --- a/SciLean/Tactic/LSimp/Types.lean +++ b/SciLean/Tactic/LSimp/Types.lean @@ -7,8 +7,8 @@ import SciLean.Lean.Meta.Basic import SciLean.Tactic.GTrans.MetaLCtxM -import Mathlib.Tactic.FunTrans.Core -import Mathlib.Tactic.FunTrans.Elab +import SciLean.Tactic.FunTrans.Core +import SciLean.Tactic.FunTrans.Elab open Lean Meta @@ -24,7 +24,6 @@ structure Result where expr : Expr proof? : Option Expr := none vars : Array Expr := #[] - dischargeDepth : UInt32 := 0 cache : Bool := true deriving Inhabited @@ -44,7 +43,6 @@ def _root_.Lean.Meta.Simp.Result.toLResult (s : Simp.Result) : Result := { expr := s.expr, proof? := s.proof?, vars := #[], - dischargeDepth := s.dischargeDepth, cache := s.cache } def Result.getProof (r : Result) : MetaM Expr := @@ -92,7 +90,7 @@ structure State where /-- Cache storing lsimp results. -/ cache : IO.Ref Cache simpState : IO.Ref Simp.State - timings : Std.RBMap String Aesop.Nanos compare := {} + timings : Batteries.RBMap String Aesop.Nanos compare := {} abbrev LSimpM := ReaderT Simp.Methods $ ReaderT Simp.Context $ StateT State MetaLCtxM diff --git a/SciLean/Tactic/LetNormalize.lean b/SciLean/Tactic/LetNormalize.lean index 25f5fad2..edeb6023 100644 --- a/SciLean/Tactic/LetNormalize.lean +++ b/SciLean/Tactic/LetNormalize.lean @@ -134,23 +134,24 @@ partial def letNormalize (e : Expr) (config : LetNormalizeConfig) : MetaM Expr : -- deconstruct constructors into bunch of let bindings if config.splitStructureConstuctors then if let .some (ctor, args) ← constructorApp? xValue' then - if let .some info := getStructureInfo? (← getEnv) xType.getAppFn.constName! then - let mut lctx ← getLCtx - let insts ← getLocalInstances - let mut fvars : Array Expr := #[] - for i in [0:ctor.numFields] do - let fvarId ← withLCtx lctx insts mkFreshFVarId - let name := xName.appendAfter s!"_{info.fieldNames[i]!}" - let val := args[ctor.numParams + i]! - let type ← inferType val - lctx := lctx.mkLetDecl fvarId name type val (nonDep := false) default - fvars := fvars.push (.fvar fvarId) - - let e' ← withLCtx lctx insts do - let xValue'' := mkAppN xValue'.getAppFn (args[0:ctor.numFields].toArray.append fvars) - mkLambdaFVars fvars (xBody.instantiate1 xValue'') - - return (← letNormalize e' config) + if let .some name := xType.getAppFn.constName? then + if let .some info := getStructureInfo? (← getEnv) name then + let mut lctx ← getLCtx + let insts ← getLocalInstances + let mut fvars : Array Expr := #[] + for i in [0:ctor.numFields] do + let fvarId ← withLCtx lctx insts mkFreshFVarId + let name := xName.appendAfter s!"_{info.fieldNames[i]!}" + let val := args[ctor.numParams + i]! + let type ← inferType val + lctx := lctx.mkLetDecl fvarId name type val (nonDep := false) default + fvars := fvars.push (.fvar fvarId) + + let e' ← withLCtx lctx insts do + let xValue'' := mkAppN xValue'.getAppFn (args[0:ctor.numFields].toArray.append fvars) + mkLambdaFVars fvars (xBody.instantiate1 xValue'') + + return (← letNormalize e' config) -- in all other cases normalized the body withLetDecl xName xType xValue' fun x => do diff --git a/SciLean/Tactic/MathlibCompiledTactics.lean b/SciLean/Tactic/MathlibCompiledTactics.lean index a8201e05..620f3306 100644 --- a/SciLean/Tactic/MathlibCompiledTactics.lean +++ b/SciLean/Tactic/MathlibCompiledTactics.lean @@ -1,4 +1,5 @@ import Mathlib.Tactic.FunProp -import Mathlib.Tactic.FunTrans.Elab -import Mathlib.Tactic.FunTrans.Attr +import SciLean.Tactic.FunTrans.Elab +import SciLean.Tactic.FunTrans.Attr import SciLean.Tactic.LSimp.Main +import SciLean.Tactic.LSimp.Types diff --git a/SciLean/Tactic/StructuralInverse.lean b/SciLean/Tactic/StructuralInverse.lean index bbecdfb7..e4195e8a 100644 --- a/SciLean/Tactic/StructuralInverse.lean +++ b/SciLean/Tactic/StructuralInverse.lean @@ -329,7 +329,7 @@ def structuralInverse (f : Expr) : MetaM (Option (FunctionInverse Γ— Array MVarI let l ← proof.mvarId!.constructor l.forM fun m => do let (_,m') ← m.intros - m'.applyRefl + m'.refl let dec : StructureDecomposition := { u := u, v := u₁, w := uβ‚‚, X := X, X₁ := X₁, Xβ‚‚ := Xβ‚‚ diff --git a/SciLean/Tactic/StructureDecomposition.lean b/SciLean/Tactic/StructureDecomposition.lean index 03073247..8e0a6387 100644 --- a/SciLean/Tactic/StructureDecomposition.lean +++ b/SciLean/Tactic/StructureDecomposition.lean @@ -189,7 +189,7 @@ def decomposeStructure (e : Expr) (split : Nat β†’ Expr β†’ Bool) : MetaM (Optio let l ← proof.mvarId!.constructor l.forM fun m => do let (_,m') ← m.intros - m'.applyRefl + m'.refl return .some {u:=u, v:=v, w:=w, X:=X, X₁:=X₁, Xβ‚‚:=Xβ‚‚, p₁:=p₁, pβ‚‚:=pβ‚‚, q:=q, proof := proof} @@ -255,7 +255,7 @@ def factorDomainThroughProjections (f : Expr) : MetaM (Option DomainDecompositio let f : Q($dec.X β†’ $Y) := f let proof ← mkFreshExprMVarQ q(βˆ€ x, $f' ($dec.p₁ x) = $f x) - proof.mvarId!.intros >>= fun (_,m) => m.applyRefl + proof.mvarId!.intros >>= fun (_,m) => m.refl return .some {u:= u, Y:=Y, dec:=dec, f:=f, f':=f', proof:=proof} @@ -294,7 +294,7 @@ def factorCodomainThroughProjections (f : Expr) : MetaM (Option CodomainDecompos let f : Q($X β†’ $dec.X) := f let proof ← mkFreshExprMVarQ q(βˆ€ x, $dec.q ($f' x) $yβ‚‚ = $f x) - proof.mvarId!.intros >>= fun (_,m) => m.applyRefl + proof.mvarId!.intros >>= fun (_,m) => m.refl return .some {u:=u, X:=X, dec:=dec, f:=f, f':=f', yβ‚‚:=yβ‚‚, proof:=proof} diff --git a/SciLean/Util/DefOptimize.lean b/SciLean/Util/DefOptimize.lean index 3f3e3a3a..7b8f0473 100644 --- a/SciLean/Util/DefOptimize.lean +++ b/SciLean/Util/DefOptimize.lean @@ -21,7 +21,7 @@ elab "def_optimize" f:ident "by " t:convSeq : command => do let (value',eq) ← elabConvRewrite val #[] (← `(conv| ($t))) pure (← mkLambdaFVars xs value', ← mkLambdaFVars xs eq) - let optName := info.name.append "optimized" + let optName := info.name.append (.mkSimple "optimized") let optimizedDef : DefinitionVal := { @@ -41,11 +41,11 @@ elab "def_optimize" f:ident "by " t:convSeq : command => do let rhs ← mkAppOptM optName (xs.map .some) mkForallFVars xs (← mkEq lhs rhs) - let thmName := info.name.append "optimize_rule" + let thmName := info.name.append (.mkSimple "optimize_rule") let eqTheorem : TheoremVal := { - name := info.name.append "optimize_rule" + name := info.name.append (.mkSimple "optimize_rule") type := eqType value := (← instantiateMVars eq) levelParams := info.levelParams diff --git a/SciLean/Util/Profile.lean b/SciLean/Util/Profile.lean index 7841ae28..ae11d6c4 100644 --- a/SciLean/Util/Profile.lean +++ b/SciLean/Util/Profile.lean @@ -44,7 +44,7 @@ def profileFile (file : FilePath) (flame : FilePath := "/home/tskrivan/Documents let stdout ← IO.asTask child.stdout.readToEnd Task.Priority.dedicated let stderr ← child.stderr.readToEnd let exitCode ← child.wait - let stdout ← IO.ofExcept stdout.get + let _stdout ← IO.ofExcept stdout.get if exitCode != 0 then throw (IO.Error.userError s!"Error: Failed to run speedscope\n\n{stderr}") diff --git a/lake-manifest.json b/lake-manifest.json index c1f5b19f..a7ab4e8f 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,11 +1,11 @@ -{"version": 7, +{"version": "1.0.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/std4", + [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "e840c18f7334c751efbd4cfe531476e10c943cdb", - "name": "std", + "rev": "47e4cc5c5800c07d9bf232173c9941fa5bf68589", + "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, @@ -13,7 +13,7 @@ {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "64365c656d5e1bffa127d2a1795f471529ee0178", + "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -22,25 +22,25 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79", + "rev": "882561b77bd2aaa98bd8665a56821062bdb3034c", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8", + "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.30", + "inputRev": "v0.0.36", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, - "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5", + "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -49,25 +49,25 @@ {"url": "https://github.com/leanprover-community/import-graph.git", "type": "git", "subDir": null, - "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662", + "rev": "1588be870b9c76fe62286e8f42f0b4dafa154c96", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, - "rev": "93904a0d036e5321062ae5e705e8a893da24d81b", + "rev": "403385804e70ec50fc373b8c349176dcd8333419", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "lecopivo/fun_trans", + "inputRev": "lecopivo/fun_prop_fixes2", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/lecopivo/LeanColls.git", "type": "git", "subDir": null, - "rev": "907d7f1ea8d59a7d8fe15fcbbea2d5fe7638da95", + "rev": "8f5aa8574f0aeca250009fb0a2c64184f1679a55", "name": "leancolls", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.lean b/lakefile.lean index 7df9050b..79cdb65b 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -14,7 +14,6 @@ lean_lib CompileTactics where precompileModules := true roots := #[`SciLean.Tactic.LSimp.LetNormalize,`SciLean.Tactic.MathlibCompiledTactics] - lean_exe Doodle { root := `examples.Doodle } @@ -58,7 +57,7 @@ lean_exe MNISTClassifier where meta if get_config? doc = some "dev" then -- do not download and build doc-gen4 by default require Β«doc-gen4Β» from git "https://github.com/leanprover/doc-gen4" @ "master" -require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "lecopivo/fun_trans" +require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "lecopivo/fun_prop_fixes2" require leancolls from git "https://github.com/lecopivo/LeanColls.git" @ "main" set_option linter.unusedVariables false diff --git a/lean-toolchain b/lean-toolchain index 9ad30404..29c0cea4 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.7.0 +leanprover/lean4:v4.9.0-rc2 diff --git a/test/lsimp_basic_tests.lean b/test/lsimp_basic_tests.lean index c397c591..4dd8d121 100644 --- a/test/lsimp_basic_tests.lean +++ b/test/lsimp_basic_tests.lean @@ -145,6 +145,8 @@ elab "timeTactic" t:conv : conv => do -- unfold scalarGradient -- timeTactic lsimp + +set_option trace.Meta.Tactic.fun_trans true in #check (βˆ‡ x : Float, let x1 := x * x let x2 := x * x1 @@ -152,6 +154,7 @@ elab "timeTactic" t:conv : conv => do let x4 := x * x3 let x5 := x * x4 let x6 := x * x5 + -- let x7 := x * x6 -- let x8 := x * x7 -- let x9 := x * x8 -- let x10 := x * x9