From cb37e425b8e8f75e1456e663c727efcda8117550 Mon Sep 17 00:00:00 2001 From: lecopivo Date: Tue, 25 Jul 2023 18:48:41 -0400 Subject: [PATCH] fix bug in fprop and started working on fwdDeriv --- SciLean.lean | 1 + SciLean/FTrans/FDeriv/Basic.lean | 60 ++++- SciLean/FTrans/FDeriv/Test.lean | 85 ++++-- SciLean/FTrans/FwdDeriv/Basic.lean | 244 ++++++++++++++++++ SciLean/FTrans/FwdDeriv/Test.lean | 35 +++ .../FunctionSpaces/Differentiable/Tactic.lean | 4 - SciLean/Tactic/FProp/Basic.lean | 27 +- SciLean/Tactic/FProp/Init.lean | 6 +- SciLean/Tactic/FTrans/Init.lean | 2 + 9 files changed, 412 insertions(+), 52 deletions(-) create mode 100644 SciLean/FTrans/FwdDeriv/Basic.lean create mode 100644 SciLean/FTrans/FwdDeriv/Test.lean diff --git a/SciLean.lean b/SciLean.lean index e70ca6e0..bc840585 100644 --- a/SciLean.lean +++ b/SciLean.lean @@ -12,6 +12,7 @@ import SciLean.Tactic.FTrans.Basic import SciLean.Tactic.FProp.Notation import SciLean.FTrans.FDeriv.Basic import SciLean.FunctionSpaces.Differentiable.Basic +import SciLean.FTrans.CDeriv.Basic /-! diff --git a/SciLean/FTrans/FDeriv/Basic.lean b/SciLean/FTrans/FDeriv/Basic.lean index 8e6b8fa6..57839d31 100644 --- a/SciLean/FTrans/FDeriv/Basic.lean +++ b/SciLean/FTrans/FDeriv/Basic.lean @@ -10,7 +10,7 @@ import Mathlib.Analysis.Calculus.Deriv.Basic import Mathlib.Analysis.Calculus.Deriv.Inv -import SciLean.FunctionSpaces.ContinuousLinearMap.Basic +import SciLean.FunctionSpaces.ContinuousLinearMap.Notation import SciLean.FunctionSpaces.Differentiable.Basic import SciLean.Tactic.FTrans.Basic @@ -35,11 +35,43 @@ theorem fderiv.id_rule : (fderiv K fun x : X => x) = fun _ => fun dx =>L[K] dx := by ext x dx; simp - theorem fderiv.const_rule (x : X) : (fderiv K fun _ : Y => x) = fun _ => fun dx =>L[K] 0 := by ext x dx; simp +theorem fderiv.comp_rule_at + (x : X) + (g : X → Y) (hg : DifferentiableAt K g x) + (f : Y → Z) (hf : DifferentiableAt K f (g x)) + : (fderiv K fun x : X => f (g x)) x + = + let y := g x + fun dx =>L[K] + let dy := fderiv K g x dx + let dz := fderiv K f y dy + dz := +by + rw[show (fun x => f (g x)) = f ∘ g by rfl] + rw[fderiv.comp x hf hg] + ext dx; simp + +theorem fderiv.comp_rule + (g : X → Y) (hg : Differentiable K g) + (f : Y → Z) (hf : Differentiable K f) + : (fderiv K fun x : X => f (g x)) + = + fun x => + let y := g x + fun dx =>L[K] + let dy := fderiv K g x dx + let dz := fderiv K f y dy + dz := +by + funext x; + rw[show (fun x => f (g x)) = f ∘ g by rfl] + rw[fderiv.comp x (hf (g x)) (hg x)] + ext dx; simp + theorem fderiv.let_rule_at (x : X) @@ -54,12 +86,14 @@ theorem fderiv.let_rule_at fun dx =>L[K] let dy := fderiv K g x dx let dz := fderiv K (fun xy : X×Y => f xy.1 xy.2) (x,y) (dx, dy) - dz := -by + dz := +by have h : (fun x => f x (g x)) = (fun xy : X×Y => f xy.1 xy.2) ∘ (fun x => (x, g x)) := by rfl - rw[h] - rw[fderiv.comp x hf (DifferentiableAt.prod (by simp) hg)] - rw[DifferentiableAt.fderiv_prod (by simp) hg] + conv => + lhs + rw[h] + rw[fderiv.comp x hf (DifferentiableAt.prod (by simp) hg)] + rw[DifferentiableAt.fderiv_prod (by simp) hg] ext dx; simp[ContinuousLinearMap.comp] rfl @@ -107,12 +141,19 @@ theorem fderiv.pi_rule open Lean Meta Qq -def fderiv.discharger (e : Expr) : SimpM (Option Expr) := - FTrans.tacticToDischarge (Syntax.mkLit ``tacticDifferentiable "differentiable") e +def fderiv.discharger (e : Expr) : SimpM (Option Expr) := do + withTraceNode `fderiv_discharger (fun _ => return s!"discharge {← ppExpr e}") do + let cache := (← get).cache + let config : FProp.Config := {} + let state : FProp.State := { cache := cache } + let (proof?, state) ← FProp.fprop e |>.run config |>.run state + modify (fun simpState => { simpState with cache := state.cache }) + return proof? open Lean Elab Term FTrans def fderiv.ftransExt : FTransExt where ftransName := ``fderiv + getFTransFun? e := if e.isAppOf ``fderiv then @@ -131,6 +172,7 @@ def fderiv.ftransExt : FTransExt where identityRule := .some <| .thm ``fderiv.id_rule constantRule := .some <| .thm ``fderiv.const_rule + compRule := .some <| .thm ``fderiv.comp_rule lambdaLetRule := .some <| .thm ``fderiv.let_rule lambdaLambdaRule := .some <| .thm ``fderiv.pi_rule diff --git a/SciLean/FTrans/FDeriv/Test.lean b/SciLean/FTrans/FDeriv/Test.lean index 11528ea1..a412df5e 100644 --- a/SciLean/FTrans/FDeriv/Test.lean +++ b/SciLean/FTrans/FDeriv/Test.lean @@ -3,6 +3,9 @@ import SciLean.Profile open SciLean +-- #profile_this_file + +set_option profiler true variable {K : Type _} [NontriviallyNormedField K] @@ -14,24 +17,23 @@ variable {ι : Type _} [Fintype ι] variable {E : ι → Type _} [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace K (E i)] -example : NormedCommRing K := by infer_instance -example : NormedAlgebra K K := by infer_instance - -example - : fderiv K (fun (x : K) => x * x * x) - = - fun x => fun dx =>L[K] dx * x + dx * x := -by - ftrans only - set_option trace.Meta.Tactic.simp.rewrite true in - set_option trace.Meta.Tactic.simp.discharge true in - set_option trace.Meta.Tactic.simp.unify true in - set_option trace.Meta.Tactic.lsimp.pre true in - set_option trace.Meta.Tactic.lsimp.step true in - set_option trace.Meta.Tactic.lsimp.post true in - ftrans only - ext x; simp +#exits +-- example +-- : fderiv K (fun (x : K) => x * x * x) +-- = +-- fun x => fun dx =>L[K] dx * x + dx * x := +-- by +-- ftrans only +-- set_option trace.Meta.Tactic.simp.rewrite true in +-- set_option trace.Meta.Tactic.simp.discharge true in +-- set_option trace.Meta.Tactic.simp.unify true in +-- set_option trace.Meta.Tactic.lsimp.pre true in +-- set_option trace.Meta.Tactic.lsimp.step true in +-- set_option trace.Meta.Tactic.lsimp.post true in +-- ftrans only +-- ext x; simp +example : Differentiable K fun x : K => x := by fprop example : fderiv K (fun (x : K) => x + x) @@ -42,30 +44,59 @@ by ftrans only ext x; simp - example : fderiv K (fun (x : K) => x + x + x) = fun x => fun dx =>L[K] dx + dx + dx := by - ftrans only + ftrans only; ext x; simp +example + : fderiv K (fun (x : K) => x * x * x * x) + = + fun x => fun dx =>L[K] 0 := +by + conv => + lhs + ftrans only + sorry + + +set_option trace.Meta.Tactic.simp.rewrite true in example : fderiv K (fun (x : K) => x + x + x + x) = fun x => fun dx =>L[K] dx + dx + dx + dx := by - ftrans only - ext x; simp + ftrans -example - : fderiv K (fun (x : K) => x + x + x + x + x) + +variable {K : Type _} [NontriviallyNormedField K] + +variable {E : Type _} [NormedAddCommGroup E] [NormedSpace K E] + +variable {F : Type _} [NormedAddCommGroup F] [NormedSpace K F] + +variable {G : Type _} [NormedAddCommGroup G] [NormedSpace K G] + +variable {f f₀ f₁ g : E → F} + +theorem fderiv_add' + (hf : Differentiable K f) (hg : Differentiable K g) : + fderiv K (fun y => f y + g y) + = + fun x => + fun dx =>L[K] + fderiv K f x dx + fderiv K g x dx := sorry + +example (x : K) + : fderiv K (fun (x : K) => x + x + x + x + x) x = - fun x => fun dx =>L[K] + fun dx =>L[K] dx + dx + dx + dx + dx := -by - ftrans only - ext x; simp +by + simp (discharger:=fprop) only [fderiv_add', fderiv_id'] + dsimp diff --git a/SciLean/FTrans/FwdDeriv/Basic.lean b/SciLean/FTrans/FwdDeriv/Basic.lean new file mode 100644 index 00000000..e8534d2a --- /dev/null +++ b/SciLean/FTrans/FwdDeriv/Basic.lean @@ -0,0 +1,244 @@ +import SciLean.FTrans.FDeriv.Basic +import SciLean.Profile + +namespace SciLean + +/-- `BroadcastType tag X ι MX` says that `MX` is `ι`-many copies of `X` + + `tag` is used to indicate the class of broadcasting types. For example, dense or sparse matrices are broadcast type for vectors. + -/ +class BroadcastType (tag : Name) (R : Type _) [Ring R] (ι : Type _) (X : Type _) (MX : outParam $ Type _) [AddCommGroup X] [Module R X] [AddCommGroup MX] [Module R MX] where + equiv : MX ≃ₗ[R] (ι → X) + + + + +variable + {R : Type _} [Ring R] + {X : Type _} [AddCommGroup X] [Module R X] + {Y : Type _} [AddCommGroup Y] [Module R Y] + {MX : Type _} [AddCommGroup MX] [Module R MX] + {MY : Type _} [AddCommGroup MY] [Module R MY] + {ι : Type _} -- [Fintype ι] + {κ : Type _} -- [Fintype κ] + {E ME : κ → Type _} + [∀ j, AddCommGroup (E j)] [∀ j, Module R (E j)] + [∀ j, AddCommGroup (ME j)] [∀ j, Module R (ME j)] + + +def broadcast (tag : Name) [BroadcastType tag R ι X MX] [BroadcastType tag R ι Y MY] + (f : X → Y) : MX → MY := fun mx => + (BroadcastType.equiv tag (R:=R)).invFun fun (i : ι) => f ((BroadcastType.equiv tag (R:=R)) mx i) + + +open BroadcastType in +instance [BroadcastType tag R ι X MX] [BroadcastType tag R ι Y MY] : BroadcastType tag R ι (X×Y) (MX×MY) where + equiv := { + toFun := fun (mx,my) i => (equiv tag (R:=R) mx i, + equiv tag (R:=R) my i) + invFun := fun xy => ((equiv tag (R:=R)).invFun fun i => (xy i).1, + (equiv tag (R:=R)).invFun fun i => (xy i).2) + map_add' := by intro x y; funext i; simp + map_smul' := by intro x y; funext i; simp + left_inv := fun _ => by simp + right_inv := fun _ => by simp + } + +open BroadcastType in +instance [∀ j, BroadcastType tag R ι (E j) (ME j)] + : BroadcastType tag R ι (∀ j, E j) (∀ j, ME j) where + equiv := { + toFun := fun mx i j => equiv tag (R:=R) (mx j) i + invFun := fun x j => (equiv tag (R:=R)).invFun (fun i => x i j) + map_add' := by intro x y; funext i j; simp + map_smul' := by intro x y; funext i j; simp + left_inv := fun _ => by simp + right_inv := fun _ => by simp + } + +open BroadcastType in +instance : BroadcastType `normal R Unit X X where + equiv := { + toFun := fun x _ => x + invFun := fun x => x () + map_add' := by intro x y; funext _; simp + map_smul' := by intro x y; funext _; simp + left_inv := fun _ => by simp + right_inv := fun _ => by simp + } + +-- open BroadcastType in +-- instance [BroadcastType `normal R (Fin n) X MX] : BroadcastType `normal R (Fin (n+1)) X (X×MX) where +-- equiv := { +-- toFun := fun (x,mx) i => +-- match i with +-- | ⟨0, _⟩ => x +-- | ⟨i'+1, h⟩ => +-- let i' : Fin n := ⟨i', by aesop⟩ +-- equiv `normal (R:=R) mx i' +-- invFun := fun x => (x 0, (equiv `normal (R:=R)).invFun fun i : Fin n => x ⟨i.1+1, by aesop⟩) +-- map_add' := by intro x y; funext ⟨i,hi⟩; induction i; simp; rfl; simp +-- map_smul' := by intro x y; funext ⟨i,hi⟩; induction i; simp; rfl; simp +-- left_inv := fun (x,mx) => by simp; rfl +-- right_inv := fun _ => by simp; funext ⟨i,hi⟩; induction i; simp; rfl +-- } + + +-- instance : Broadcast `EigenSparse ℝ^m (Eigen.SparseMatrix n m) (Fin n) where +-- instance : Broadcast `EigenDense ℝ^m (Eigen.Matrix n m) (Fin n) where + + +noncomputable +def fwdDeriv + (K : Type _) [NontriviallyNormedField K] + (tag : Name) (ι : Type _) + {X : Type _} [NormedAddCommGroup X] [NormedSpace K X] + {Y : Type _} [NormedAddCommGroup Y] [NormedSpace K Y] + {DX : Type _} [AddCommGroup DX] [Module K DX] + {DY : Type _} [AddCommGroup DY] [Module K DY] + [BroadcastType tag K ι X DX] [BroadcastType tag K ι Y DY] + (f : X → Y) (x : X) (dx : DX) : Y×DY := + (f x, broadcast tag (R:=K) (ι:=ι) (fun dx => fderiv K f x dx) dx) + +namespace fwdDeriv + +variable + {K : Type _} [NontriviallyNormedField K] + {tag : Name} {ι : Type _} + {X : Type _} [NormedAddCommGroup X] [NormedSpace K X] + {Y : Type _} [NormedAddCommGroup Y] [NormedSpace K Y] + {Z : Type _} [NormedAddCommGroup Z] [NormedSpace K Z] + {DX : Type _} [AddCommGroup DX] [Module K DX] [BroadcastType tag K ι X DX] + {DY : Type _} [AddCommGroup DY] [Module K DY] [BroadcastType tag K ι Y DY] + {DZ : Type _} [AddCommGroup DZ] [Module K DZ] [BroadcastType tag K ι Z DZ] + {κ : Type _} [Fintype κ] + {E : κ → Type _} [∀ j, NormedAddCommGroup (E j)] [∀ j, NormedSpace K (E j)] + {DE : κ → Type _} [∀ j, AddCommGroup (DE j)] [∀ j, Module K (DE j)] + [∀ j, BroadcastType tag K ι (E j) (DE j)] + + +theorem id_rule + : fwdDeriv K tag ι (fun x : X => x) = fun x dx => (x,dx) := +by + unfold fwdDeriv; unfold broadcast + simp + +theorem const_rule (x :X) + : fwdDeriv K tag ι (fun y : Y => x) = fun y dy => (x, 0) := +by + unfold fwdDeriv; unfold broadcast + funext y dy + simp; rfl + +theorem comp_rule + (g : X → Y) (hg : Differentiable K g) + (f : Y → Z) (hf : Differentiable K f) + : fwdDeriv K tag ι (fun x : X => f (g x)) + = + fun x dx => + let ydy := fwdDeriv K tag ι g x dx + let zdz := fwdDeriv K tag ι f ydy.1 ydy.2 + zdz := +by + unfold fwdDeriv; unfold broadcast + funext x dx; congr; funext i; + rw[fderiv.comp_rule g hg f hf] + simp + + +theorem let_rule + (g : X → Y) (hg : Differentiable K g) + (f : X → Y → Z) (hf : Differentiable K (fun (xy : X×Y) => f xy.1 xy.2)) + : fwdDeriv K tag ι (fun x : X => let y := g x; f x y) + = + fun x dx => + let ydy := fwdDeriv K tag ι g x dx + let zdz := fwdDeriv K tag ι (fun (xy : X×Y) => f xy.1 xy.2) (x,ydy.1) (dx,ydy.2) + zdz := +by + unfold fwdDeriv; unfold broadcast + funext x dx; congr; funext i + rw[fderiv.let_rule g hg f hf]; + simp; congr; simp + + + +theorem pi_rule + (f : (j : κ) → X → E j) (hf : ∀ j, Differentiable K (f j)) + : (fwdDeriv K tag ι fun (x : X) (j : κ) => f j x) + = + fun x dx => + (fun j => f j x, fun j => (fwdDeriv K tag ι (f j) x dx).2) := +by + unfold fwdDeriv; unfold broadcast + funext x; rw[fderiv_pi (fun i => hf i x)] + simp; funext dx; simp[BroadcastType.equiv] + + +-- Register `fwdDeriv` as function transformation ------------------------------ +-------------------------------------------------------------------------------- + +open Lean Meta Qq + +def fwdDeriv.discharger (e : Expr) : SimpM (Option Expr) := do + withTraceNode `fwdDeriv_discharger (fun _ => return s!"discharge {← ppExpr e}") do + let cache := (← get).cache + let config : FProp.Config := {} + let state : FProp.State := { cache := cache } + let (proof?, state) ← FProp.fprop e |>.run config |>.run state + modify (fun simpState => { simpState with cache := state.cache }) + return proof? + +open Lean Elab Term FTrans +def fwdDeriv.ftransExt : FTransExt where + ftransName := ``fwdDeriv + + getFTransFun? e := + if e.isAppOf ``fwdDeriv then + + if let .some f := e.getArg? 19 then + some f + else + none + else + none + + replaceFTransFun e f := + if e.isAppOf ``fwdDeriv then + e.modifyArg (fun _ => f) 19 + else + e + + identityRule := .some <| .thm ``id_rule + constantRule := .some <| .thm ``const_rule + compRule := .some <| .thm ``comp_rule + lambdaLetRule := .some <| .thm ``let_rule + lambdaLambdaRule := .some <| .thm ``pi_rule + + discharger := fwdDeriv.discharger + + +-- register fderiv +#eval show Lean.CoreM Unit from do + modifyEnv (λ env => FTrans.ftransExt.addEntry env (``fwdDeriv, fwdDeriv.ftransExt)) + + +example : BroadcastType tag K ι X DX := by infer_instance + + +@[ftrans_rule] +theorem HAdd.hAdd.arg_a4a5.fderiv_comp + (f g : X → Y) (hf : Differentiable K f) (hg : Differentiable K g) + : (fwdDeriv K tag ι fun x => f x + g x) + = + fun x dx => + let ydy₁ := fwdDeriv K tag ι f x dx + let ydy₂ := fwdDeriv K tag ι g x dx + ydy₁ + ydy₂ := +by + funext x dx + unfold fwdDeriv; unfold broadcast + ftrans only + simp; rw[← map_add]; rfl + + diff --git a/SciLean/FTrans/FwdDeriv/Test.lean b/SciLean/FTrans/FwdDeriv/Test.lean new file mode 100644 index 00000000..37e18e47 --- /dev/null +++ b/SciLean/FTrans/FwdDeriv/Test.lean @@ -0,0 +1,35 @@ +import SciLean.FTrans.FwdDeriv.Basic + +import SciLean.Tactic.LSimp.Notation +import SciLean.Tactic.LetEnter +import SciLean.Tactic.Basic + + +open SciLean + +variable + {K : Type _} [NontriviallyNormedField K] + +example + : fwdDeriv K `normal Unit (fun x : K => x + x + x + x + x) + = + fun x dx => + (x + x + x + x + x, dx + dx + dx + dx + dx):= +by + conv => + lhs + ftrans only + enter [x,dx] + simp (config := { zeta := false}) only [Prod.add_def] + ftrans only + +#exit + +example + : fwdDeriv K `normal Unit (fun x : K => x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x) + = + fun x dx => + (x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x, + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx):= +by + ftrans diff --git a/SciLean/FunctionSpaces/Differentiable/Tactic.lean b/SciLean/FunctionSpaces/Differentiable/Tactic.lean index b366662c..4a95e5dc 100644 --- a/SciLean/FunctionSpaces/Differentiable/Tactic.lean +++ b/SciLean/FunctionSpaces/Differentiable/Tactic.lean @@ -145,8 +145,4 @@ theorem hoho : Differentiable ℝ (fun x : ℝ => let y := x + x + x + x + x + ( example : Differentiable ℝ (fun x : ℝ => x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x) := by fprop -example : Differentiable ℝ (fun x : ℝ => x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x) := by differentiable - -example : Differentiable ℝ (fun x : ℝ => let y := x + x; let z := x + y; let f := fun x : ℝ => x + x; f y + y + x + z) := by differentiable - diff --git a/SciLean/Tactic/FProp/Basic.lean b/SciLean/Tactic/FProp/Basic.lean index b1db5eb2..d63cdeb8 100644 --- a/SciLean/Tactic/FProp/Basic.lean +++ b/SciLean/Tactic/FProp/Basic.lean @@ -77,7 +77,7 @@ def cache (e : Expr) (proof? : Option Expr) : FPropM (Option Expr) := -- return match proof? with | .none => return none | .some proof => do - modify (fun s => { s with cache := s.cache.insert e proof} ) + modify (fun s => { s with cache := s.cache.insert e { expr := q(True), proof? := proof} }) return proof @@ -90,10 +90,6 @@ def getLocalRules (fpropName : Name) : MetaM (Array SimpTheorem) := do if (type.getForallBody.getAppFn.constName? == .some fpropName) && (var.kind ≠ Lean.LocalDeclKind.auxDecl) then - -- dbg_trace "adding `{← ppExpr var.toExpr} : {←ppExpr type}` to local rules to be applied" - -- dbg_trace "hasExprMVar {var.hasExprMVar}" - -- dbg_trace "hasValue {var.hasValue}" - -- dbg_trace "hasValue {repr var.kind}" arr := arr.push { proof := var.toExpr origin := .fvar var.fvarId @@ -106,7 +102,8 @@ def getLocalRules (fpropName : Name) : MetaM (Array SimpTheorem) := do mutual partial def fprop (e : Expr) : FPropM (Option Expr) := do - if let .some proof := (← get).cache.find? e then + if let .some { expr := _, proof? := .some proof } := (← get).cache.find? e then + trace[Meta.Tactic.fprop.cache] "cached result for {e}" return proof else forallTelescope e fun xs b => do @@ -131,16 +128,22 @@ mutual ext.identityRule e | .lam xName xType (.letE yName yType yValue body _) xBi => + -- We perform reduction because the type is quite often of the form + -- `(fun x => Y) #0` which is just `Y` + let yType := yType.headBeta + if (yType.hasLooseBVar 0) then + throwError "dependent type encountered {← ppExpr (Expr.forallE xName xType yType default)}" + match (body.hasLooseBVar 0), (body.hasLooseBVar 1) with | true, true => trace[Meta.Tactic.fprop.step] "case let\n{← ppExpr e}" - let f := Expr.lam xName xType (.lam yName yType body xBi) default + let f := Expr.lam xName xType (.lam yName yType body default) xBi let g := Expr.lam xName xType yValue default ext.lambdaLetRule e f g | true, false => trace[Meta.Tactic.fprop.step] "case comp\n{← ppExpr e}" - let f := Expr.lam yName yType body xBi + let f := Expr.lam yName yType body default let g := Expr.lam xName xType yValue default ext.compRule e f g @@ -148,6 +151,7 @@ mutual let f := Expr.lam xName xType (body.lowerLooseBVars 1 1) xBi FProp.fprop (ext.replaceFPropFun e f) + | .lam _ _ (.lam ..) _ => trace[Meta.Tactic.fprop.step] "case pi\n{← ppExpr e}" ext.lambdaLambdaRule e f @@ -160,11 +164,14 @@ mutual trace[Meta.Tactic.fprop.step] "case fvar app\n{← ppExpr e}" applyFVarApp e ext.discharger else - trace[Meta.Tactic.fprop.step] "case other\n{← ppExpr e}" + trace[Meta.Tactic.fprop.step] "case other\n{← ppExpr e}\n" applyTheorems e (ext.discharger) + | .mvar _ => do + fprop (← instantiateMVars e) + | _ => do - trace[Meta.Tactic.fprop.step] "case other\n{← ppExpr e}" + trace[Meta.Tactic.fprop.step] "case other\n{← ppExpr e}\n" applyTheorems e (ext.discharger) partial def applyFVarApp (e : Expr) (discharge? : Expr → FPropM (Option Expr)) : FPropM (Option Expr) := do diff --git a/SciLean/Tactic/FProp/Init.lean b/SciLean/Tactic/FProp/Init.lean index 51e92ab8..09e2ee09 100644 --- a/SciLean/Tactic/FProp/Init.lean +++ b/SciLean/Tactic/FProp/Init.lean @@ -18,6 +18,7 @@ namespace SciLean.FProp ------------- initialize registerTraceClass `Meta.Tactic.fprop initialize registerTraceClass `Meta.Tactic.fprop.step +initialize registerTraceClass `Meta.Tactic.fprop.cache initialize registerTraceClass `Meta.Tactic.fprop.missing_rule -- initialize registerTraceClass `Meta.Tactic.fprop.normalize_let initialize registerTraceClass `Meta.Tactic.fprop.rewrite @@ -33,10 +34,11 @@ open Meta structure Config where -- config -abbrev Cache := ExprMap Expr +-- abbrev Cache := ExprMap Expr structure State where - cache : Cache := {} + /-- Simp's cache is used as the `fprop` tactic is designed to be used inside of simp and utilize its cache -/ + cache : Simp.Cache := {} abbrev _root_.SciLean.FPropM := ReaderT FProp.Config $ StateRefT FProp.State MetaM diff --git a/SciLean/Tactic/FTrans/Init.lean b/SciLean/Tactic/FTrans/Init.lean index de7ba2b9..6168bccc 100644 --- a/SciLean/Tactic/FTrans/Init.lean +++ b/SciLean/Tactic/FTrans/Init.lean @@ -73,6 +73,8 @@ structure FTransExt where identityRule : Option RewriteRule /-- Custom rule for transforming `fun x => y -/ constantRule : Option RewriteRule + /-- Custom rule for transforming `fun x => f (g x)` or `fun x => let y := g x; f y -/ + compRule : Option RewriteRule /-- Custom rule for transforming `fun x => let y := g x; f x y -/ lambdaLetRule : Option RewriteRule /-- Custom rule for transforming `fun x y => f x y -/