From 7c8d5ae8a6026483519e37999054564d269c7776 Mon Sep 17 00:00:00 2001 From: lecopivo Date: Fri, 28 Jul 2023 18:56:40 -0400 Subject: [PATCH] some improvements to ftrans --- SciLean/FTrans/Adjoint/Basic.lean | 136 ++++++++++++------ SciLean/FTrans/Adjoint/Test.lean | 117 +++++++++++++++ SciLean/FTrans/Broadcast/Basic.lean | 67 ++++++++- SciLean/FTrans/Broadcast/Test.lean | 26 ++++ SciLean/FTrans/FDeriv/Basic.lean | 3 +- SciLean/FTrans/FDeriv/Test.lean | 6 + SciLean/FTrans/FwdDeriv/Basic.lean | 115 ++++++--------- SciLean/FTrans/FwdDeriv/Test.lean | 69 ++++++++- SciLean/FTrans/RevDeriv/Basic.lean | 99 ++++++++++++- .../Analysis/InnerProductSpace/Prod.lean | 110 ++++++++++++++ SciLean/Tactic/FTrans/Basic.lean | 14 +- 11 files changed, 626 insertions(+), 136 deletions(-) create mode 100644 SciLean/FTrans/Adjoint/Test.lean create mode 100644 SciLean/FTrans/Broadcast/Test.lean create mode 100644 SciLean/Mathlib/Analysis/InnerProductSpace/Prod.lean diff --git a/SciLean/FTrans/Adjoint/Basic.lean b/SciLean/FTrans/Adjoint/Basic.lean index 1824ab6b..ba5038a4 100644 --- a/SciLean/FTrans/Adjoint/Basic.lean +++ b/SciLean/FTrans/Adjoint/Basic.lean @@ -34,6 +34,7 @@ instance (f : X →L[K] Y) : SciLean.Dagger f (ContinuousLinearMap.adjoint f : Y open SciLean +variable (X) (K) theorem id_rule : (fun (x : X) =>L[K] x)† = fun x =>L[K] x := by @@ -41,27 +42,38 @@ by rw[h]; simp +variable (Y) theorem const_rule : (fun (x : X) =>L[K] (0 : Y))† = fun x =>L[K] 0 := by sorry +variable {Y} + +theorem proj_rule [DecidableEq ι] + (i : ι) + : (fun (f : PiLp 2 (fun _ => X)) =>L[K] f i)† + = + fun x =>L[K] (fun j => if h : i=j then x else (0 : X)) + := sorry +variable {X} + theorem prod_rule - (g : X → Y) (hg : IsContinuousLinearMap K g) - (f : X → Z) (hf : IsContinuousLinearMap K f) - : ((fun x =>L[K] (g x, f x)) : X →L[K] Y×₂Z)† + (f : X → Y) (g : X → Z) + (hf : IsContinuousLinearMap K f) (hg : IsContinuousLinearMap K g) + : ((fun x =>L[K] (f x, g x)) : X →L[K] Y×₂Z)† = fun yz : Y×₂Z =>L[K] - let x₁ := (fun x =>L[K] g x)† yz.1 - let x₂ := (fun x =>L[K] f x)† yz.2 + let x₁ := (fun x =>L[K] f x)† yz.1 + let x₂ := (fun x =>L[K] g x)† yz.2 x₁ + x₂ := by sorry theorem comp_rule - (g : X → Y) (hg : IsContinuousLinearMap K g) - (f : Y → Z) (hf : IsContinuousLinearMap K f) + (f : Y → Z) (g : X → Y) + (hf : IsContinuousLinearMap K f) (hg : IsContinuousLinearMap K g) : (fun x =>L[K] f (g x))† = fun z =>L[K] @@ -79,8 +91,8 @@ by theorem let_rule - (g : X → Y) (hg : IsContinuousLinearMap K g) - (f : X → Y → Z) (hf : IsContinuousLinearMap K (fun xy : X×Y => f xy.1 xy.2)) + (f : X → Y → Z) (g : X → Y) + (hf : IsContinuousLinearMap K (fun xy : X×Y => f xy.1 xy.2)) (hg : IsContinuousLinearMap K g) : (fun x =>L[K] let y := g x; f x y)† = fun z =>L[K] @@ -96,40 +108,19 @@ by have h' : ((fun x =>L[K] (x, g x)) : X →L[K] X×₂Y)† = (fun (xy : X×₂Y) =>L[K] xy.1 + (fun x =>L[K] g x)† xy.2) - := by rw[prod_rule (fun x => x) (by fprop) g hg]; simp[id_rule] + := by rw[prod_rule K (fun x => x) g (by fprop) hg]; simp[id_rule] rw[h']; rfl - -example : CompleteSpace ((i :ι) → E i) := by infer_instance - -open BigOperators - --- set_option trace.Meta.Tactic.fprop.discharge true in --- set_option trace.Meta.Tactic.fprop.step true in +open BigOperators in theorem pi_rule - (f : (i : ι) → X → E i) (hf : ∀ i, IsContinuousLinearMap K (f i)) - : ((fun (x : X) =>L[K] fun (i : ι) => f i x) : X →L[K] PiLp 2 E)† + (f : X → (i : ι) → E i) (hf : ∀ i, IsContinuousLinearMap K (f · i)) + : ((fun (x : X) =>L[K] fun (i : ι) => f x i) : X →L[K] PiLp 2 E)† = - (fun x' =>L[K] ∑ i, (fun x =>L[K] f i x)† (x' i)) + (fun x' =>L[K] ∑ i, (fun x =>L[K] f x i)† (x' i)) := sorry -set_option trace.Meta.Tactic.fprop.discharge true in --- theorem proj_rule [DecidableEq ι] --- (i : ι) --- : (fun (f : PiLp 2 E) =>L[K] f i)† --- = --- fun y =>L[K] ((fun j => if h : i=j then (h ▸ y) else (0 : E j)) : PiLp 2 E) --- := sorry - -theorem proj_rule [DecidableEq ι] - (i : ι) - : (fun (f : PiLp 2 (fun _ => X)) =>L[K] f i)† - = - fun x =>L[K] (fun j => if h : i=j then x else (0 : X)) - := sorry - -- Register `adjoint` as function transformation ------------------------------- -------------------------------------------------------------------------------- @@ -184,13 +175,72 @@ def ftransExt : FTransExt where else return e - identityRule := .some <| .thm ``adjoint.id_rule - constantRule := .some <| .thm ``adjoint.const_rule - compRule := .some <| .thm ``adjoint.comp_rule - lambdaLetRule := .some <| .thm ``adjoint.let_rule - lambdaLambdaRule := .some <| .thm ``adjoint.pi_rule + idRule e X := do + let K := (e.getArg! 1).getArg! 0 + tryTheorems + #[ { proof := ← mkAppM ``id_rule #[K, X], origin := .decl ``id_rule, rfl := false} ] + discharger e + + constRule e X y := do + let K := (e.getArg! 1).getArg! 0 + tryTheorems + #[ { proof := ← mkAppM ``const_rule #[K, X, (← inferType y)], origin := .decl ``const_rule, rfl := false} ] + discharger e + + projRule e X i := do + let K := (e.getArg! 1).getArg! 0 + let X' := X.bindingBody! + if X'.hasLooseBVars then + trace[Meta.Tactic.ftrans.step] "can't handle this bvar app case, projection rule for dependent function of type {← ppExpr X} is not supported" + return none + tryTheorems + #[ { proof := ← mkAppM ``proj_rule #[K, X', i], origin := .decl ``proj_rule, rfl := false} ] + discharger e + + compRule e f g := do + let K := (e.getArg! 1).getArg! 0 + + let XY ← inferType g + let YZ ← inferType f + + let two : Q(ℝ) := q(2) + let fixProduct : Expr → Option Expr := + (fun e => + if let .app (.app (.const name us) A) B := e then + if name == ``Prod then + mkApp3 (mkConst ``ProdLp us) two A B + else + none + else + none) - discharger := adjoint.discharger + let X := XY.bindingDomain!.replace fixProduct + let Y := XY.bindingBody!.replace fixProduct + let Z := YZ.bindingBody!.replace fixProduct + + let args : Array (Option Expr) := + #[K, none, X, none, none, none, + Y, none, none, none, + Z, none, none, none, f, g] + + tryTheorems + #[ { proof := ← withTransparency .all <| + mkAppM ``comp_rule #[K, f, g], origin := .decl ``comp_rule, rfl := false} ] + discharger e + + letRule e f g := do + let K := (e.getArg! 1).getArg! 0 + tryTheorems + #[ { proof := ← mkAppM ``let_rule #[K, f, g], origin := .decl ``let_rule, rfl := false} ] + discharger e + + piRule e f := do + let K := (e.getArg! 1).getArg! 0 + tryTheorems + #[ { proof := ← mkAppM ``pi_rule #[K, f], origin := .decl ``pi_rule, rfl := false} ] + discharger e + + discharger := discharger -- register adjoint @@ -215,7 +265,6 @@ variable open SciLean - -- Prod.mk --------------------------------------------------------------------- -------------------------------------------------------------------------------- @@ -367,7 +416,6 @@ by sorry - -- Finset.sum ------------------------------------------------------------------ -------------------------------------------------------------------------------- @@ -414,11 +462,9 @@ by case isFalse h => ext y; simp[h] - -- Inner ----------------------------------------------------------------------- -------------------------------------------------------------------------------- -set_option trace.Meta.Tactic.fprop.discharge true in open ComplexConjugate in @[ftrans_rule] theorem Inner.inner.arg_a0.adjoint_comp diff --git a/SciLean/FTrans/Adjoint/Test.lean b/SciLean/FTrans/Adjoint/Test.lean new file mode 100644 index 00000000..467a7416 --- /dev/null +++ b/SciLean/FTrans/Adjoint/Test.lean @@ -0,0 +1,117 @@ +import SciLean.FTrans.Adjoint.Basic + +variable + {K : Type _} [IsROrC K] + {X : Type _} [NormedAddCommGroup X] [InnerProductSpace K X] [CompleteSpace X] + {Y : Type _} [NormedAddCommGroup Y] [InnerProductSpace K Y] [CompleteSpace Y] + {Z : Type _} [NormedAddCommGroup Z] [InnerProductSpace K Z] [CompleteSpace Z] + {Y₁ : Type _} [NormedAddCommGroup Y₁] [InnerProductSpace K Y₁] [CompleteSpace Y₁] + {Y₂ : Type _} [NormedAddCommGroup Y₂] [InnerProductSpace K Y₂] [CompleteSpace Y₂] + {ι : Type _} [Fintype ι] + {E : ι → Type _} [∀ i, NormedAddCommGroup (E i)] [∀ i, InnerProductSpace K (E i)] [∀ i, CompleteSpace (E i)] + +open SciLean + +example + : (fun (x : X) =>L[K] x)† = fun x =>L[K] x := by ftrans + +example + : (fun (x : X) =>L[K] (0 : Y))† = fun x =>L[K] 0 := by ftrans + + +set_option trace.Meta.Tactic.ftrans.step true in +example [DecidableEq ι] (i : ι) + : (fun (f : PiLp 2 (fun _ => X)) =>L[K] f i)† + = + fun x =>L[K] (fun j => if h : i=j then x else (0 : X)) + := by ftrans + + +example + (f : X → Y) (g : X → Z) + (hf : IsContinuousLinearMap K f) (hg : IsContinuousLinearMap K g) + : ((fun x =>L[K] (f x, g x)) : X →L[K] Y×₂Z)† + = + fun yz : Y×₂Z =>L[K] + let x₁ := (fun x =>L[K] f x)† yz.1 + let x₂ := (fun x =>L[K] g x)† yz.2 + x₁ + x₂ := by ftrans + + +example + (f : Y → Z) (g : X → Y) + (hf : IsContinuousLinearMap K f) (hg : IsContinuousLinearMap K g) + : (fun x =>L[K] f (g x))† + = + fun z =>L[K] + let y := (fun y =>L[K] f y)† z + let x := (fun x =>L[K] g x)† y + x := by ftrans + + + +example + (f : X → Y → Z) (g : X → Y) + (hf : IsContinuousLinearMap K (fun xy : X×Y => f xy.1 xy.2)) (hg : IsContinuousLinearMap K g) + : (fun x =>L[K] let y := g x; f x y)† + = + fun z =>L[K] + let xy := ((fun xy : X×₂Y =>L[K] f xy.1 xy.2)†) z + let x' := ((fun x =>L[K] g x)†) xy.2 + xy.1 + x' := by ftrans + +open BigOperators in +example + (f : X → (i : ι) → E i) (hf : ∀ i, IsContinuousLinearMap K (f · i)) + : ((fun (x : X) =>L[K] fun (i : ι) => f x i) : X →L[K] PiLp 2 E)† + = + (fun x' =>L[K] ∑ i, (fun x =>L[K] f x i)† (x' i)) + := by ftrans + + +-- instance introducing diamond!!! +@[reducible] +noncomputable +instance instNormedAddCommGroupProdL2 + {K : Type _} [IsROrC K] + {X : Type _} [NormedAddCommGroup X] [InnerProductSpace K X] + {Y : Type _} [NormedAddCommGroup Y] [InnerProductSpace K Y] + : NormedAddCommGroup (X × Y) := by rw[show (X×Y) = (ProdLp 2 X Y) by rfl]; infer_instance + +@[reducible] +noncomputable +instance instInnerProductSpaceProdL2 + {K : Type _} [IsROrC K] + {X : Type _} [NormedAddCommGroup X] [InnerProductSpace K X] + {Y : Type _} [NormedAddCommGroup Y] [InnerProductSpace K Y] + : @InnerProductSpace K (X × Y) _ (@instNormedAddCommGroupProdL2 K _ X _ _ Y _ _) := + show InnerProductSpace K (ProdLp 2 X Y) by infer_instance + + + +-- set_option trace.Meta.Tactic.simp.discharge true in +set_option trace.Meta.Tactic.ftrans.discharge true in +set_option trace.Meta.Tactic.ftrans.step true in +set_option trace.Meta.Tactic.simp.unify true in +example + (f : Y₁ → Y₂ → Z) (g₁ : X → Y₁) (g₂ : X → Y₂) + (hf : IsContinuousLinearMap K (fun yy : Y₁×Y₂ => f yy.1 yy.2)) + (hg₁ : IsContinuousLinearMap K g₁) + (hg₂ : IsContinuousLinearMap K g₂) + : (fun x =>L[K] f (g₁ x) (g₂ x))† + = + 0 + := +by + ftrans only + + + + + +instance + {X : Type _} [NormedAddCommGroup X] [InnerProductSpace K X] [CompleteSpace X] + {Y : Type _} [NormedAddCommGroup Y] [InnerProductSpace K Y] [CompleteSpace Y] + : InnerProductSpace K (X × Y) := by rw[show (X×Y) = (ProdLp 2 X Y) by rfl]; + + diff --git a/SciLean/FTrans/Broadcast/Basic.lean b/SciLean/FTrans/Broadcast/Basic.lean index c2ece8ec..b88e0234 100644 --- a/SciLean/FTrans/Broadcast/Basic.lean +++ b/SciLean/FTrans/Broadcast/Basic.lean @@ -3,6 +3,7 @@ import SciLean.Tactic.FTrans.Basic namespace SciLean + /-- Broadcast vectorizes operations. For example, broadcasting multiplication `fun (x : ℝ) => c * x` will produce scalar multiplication `fun (x₁,...,xₙ) => (c*x₁,...,c*x₂)`. @@ -72,6 +73,14 @@ by simp[broadcast, broadcastIntro] +theorem proj_rule (j : κ) + : broadcast tag R ι (fun (x : (j : κ) → E j) => x j) + = + fun (mx : (j : κ ) → ME j) => mx j := +by + simp[broadcast, broadcastIntro, BroadcastType.equiv] + + theorem comp_rule (g : X → Y) (f : Y → Z) : broadcast tag R ι (fun x => f (g x)) @@ -141,11 +150,59 @@ def broadcast.ftransExt : FTransExt where 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 + idRule := tryNamedTheorem ``id_rule discharger + constRule := tryNamedTheorem ``const_rule discharger + projRule := tryNamedTheorem ``proj_rule discharger + compRule e f g := do + let .some K := e.getArg? 0 + | return none + + let mut thrms : Array SimpTheorem := #[] + + thrms := thrms.push { + proof := ← mkAppM ``comp_rule #[K, f, g] + origin := .decl ``comp_rule + rfl := false + } + + for thm in thrms do + if let some result ← Meta.Simp.tryTheorem? e thm discharger then + return Simp.Step.visit result + return none + + letRule e f g := do + let .some K := e.getArg? 0 + | return none + + let mut thrms : Array SimpTheorem := #[] + + thrms := thrms.push { + proof := ← mkAppM ``let_rule #[K, f, g] + origin := .decl ``comp_rule + rfl := false + } + + for thm in thrms do + if let some result ← Meta.Simp.tryTheorem? e thm discharger then + return Simp.Step.visit result + return none + + piRule e f := do + let .some K := e.getArg? 0 + | return none + + let mut thrms : Array SimpTheorem := #[] + + thrms := thrms.push { + proof := ← mkAppM ``pi_rule #[K, f] + origin := .decl ``comp_rule + rfl := false + } + + for thm in thrms do + if let some result ← Meta.Simp.tryTheorem? e thm discharger then + return Simp.Step.visit result + return none discharger := broadcast.discharger diff --git a/SciLean/FTrans/Broadcast/Test.lean b/SciLean/FTrans/Broadcast/Test.lean new file mode 100644 index 00000000..733c228c --- /dev/null +++ b/SciLean/FTrans/Broadcast/Test.lean @@ -0,0 +1,26 @@ +import SciLean.FTrans.Broadcast.Basic + +open SciLean + +variable + {R : Type _} [Ring R] + {X : Type _} [AddCommGroup X] [Module R X] + {Y : Type _} [AddCommGroup Y] [Module R Y] + + +example (r : R) + : broadcast `Prod R (Fin 3) (fun x : X => r • x) + = + fun ((x,y,z) : X×X×X) => (r•x, r•y, r•z) := +by + ftrans; funext (x,y,z); simp + + +example (r : R) + : broadcast `Prod R (Fin 3) (fun s : R => r * s) + = + fun ((x,y,z) : R×R×R) => (r*x, r*y, r*z) := +by + ftrans; funext (x,y,z); simp + + diff --git a/SciLean/FTrans/FDeriv/Basic.lean b/SciLean/FTrans/FDeriv/Basic.lean index 3393a9fc..036d53c7 100644 --- a/SciLean/FTrans/FDeriv/Basic.lean +++ b/SciLean/FTrans/FDeriv/Basic.lean @@ -44,8 +44,7 @@ theorem fderiv.const_rule (x : X) variable {Y} variable (E) -theorem fderiv.proj_rule - [DecidableEq ι] (i : ι) +theorem fderiv.proj_rule (i : ι) : (fderiv K fun (x : (i : ι) → E i) => x i) = fun x => fun dx =>L[K] dx i := diff --git a/SciLean/FTrans/FDeriv/Test.lean b/SciLean/FTrans/FDeriv/Test.lean index 814fcd72..925c26c2 100644 --- a/SciLean/FTrans/FDeriv/Test.lean +++ b/SciLean/FTrans/FDeriv/Test.lean @@ -9,6 +9,8 @@ variable {K : Type _} [NontriviallyNormedField K] variable {X : Type _} [NormedAddCommGroup X] [NormedSpace K X] variable {Y : Type _} [NormedAddCommGroup Y] [NormedSpace K Y] variable {Z : Type _} [NormedAddCommGroup Z] [NormedSpace K Z] +variable {Y₁ : Type _} [NormedAddCommGroup Y₁] [NormedSpace K Y₁] +variable {Y₂ : Type _} [NormedAddCommGroup Y₂] [NormedSpace K Y₂] variable {ι : Type _} [Fintype ι] variable {E : ι → Type _} [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace K (E i)] @@ -121,3 +123,7 @@ example fun _ => fun dx =>L[K] dx i := by ftrans only + + + + diff --git a/SciLean/FTrans/FwdDeriv/Basic.lean b/SciLean/FTrans/FwdDeriv/Basic.lean index 8ea61af0..cca681ff 100644 --- a/SciLean/FTrans/FwdDeriv/Basic.lean +++ b/SciLean/FTrans/FwdDeriv/Basic.lean @@ -26,26 +26,30 @@ variable -- Basic lambda calculus rules ------------------------------------------------- -------------------------------------------------------------------------------- +variable (K) + +variable (X) theorem id_rule : fwdDeriv K (fun x : X => x) = fun x dx => (x,dx) := by unfold fwdDeriv; ftrans +variable {X} - +variable (Y) theorem const_rule (x : X) : fwdDeriv K (fun _ : Y => x) = fun y dy => (x, 0) := by unfold fwdDeriv; ftrans +variable {Y} - -theorem proj_rule [DecidableEq ι] (i : ι) +variable (E) +theorem proj_rule (i : ι) : fwdDeriv K (fun (x : (i : ι) → E i) => x i) = fun x dx => (x i, dx i) := by unfold fwdDeriv; ftrans +variable {E} -variable (K) - theorem comp_rule (f : Y → Z) (g : X → Y) (hf : Differentiable K f) (hg : Differentiable K g) @@ -160,77 +164,44 @@ def ftransExt : FTransExt where else e - idRule := tryNamedTheorem ``id_rule discharger - constRule := tryNamedTheorem ``const_rule discharger - projRule := tryNamedTheorem ``proj_rule discharger - compRule e f g := do - let .some K := e.getArg? 0 - | return none - - let mut thrms : Array SimpTheorem := #[] - - thrms := thrms.push { - proof := ← mkAppM ``comp_rule #[K, f, g] - origin := .decl ``comp_rule - rfl := false - } - - thrms := thrms.push { - proof := ← mkAppM ``comp_rule_at #[K, f, g] - origin := .decl ``comp_rule - rfl := false - } - - for thm in thrms do - if let some result ← Meta.Simp.tryTheorem? e thm discharger then - return Simp.Step.visit result - return none + idRule e X := do + let .some K := e.getArg? 0 | return none + tryTheorems + #[ { proof := ← mkAppM ``id_rule #[K, X], origin := .decl ``id_rule, rfl := false} ] + discharger e + + constRule e X y := do + let .some K := e.getArg? 0 | return none + tryTheorems + #[ { proof := ← mkAppM ``const_rule #[K, X, y], origin := .decl ``const_rule, rfl := false} ] + discharger e + + projRule e X i := do + let .some K := e.getArg? 0 | return none + tryTheorems + #[ { proof := ← mkAppM ``proj_rule #[K, X, i], origin := .decl ``proj_rule, rfl := false} ] + discharger e + + compRule e f g := do + let .some K := e.getArg? 0 | return none + tryTheorems + #[ { proof := ← mkAppM ``comp_rule #[K, f, g], origin := .decl ``comp_rule, rfl := false}, + { proof := ← mkAppM ``comp_rule_at #[K, f, g], origin := .decl ``comp_rule, rfl := false} ] + discharger e letRule e f g := do - let .some K := e.getArg? 0 - | return none - - let mut thrms : Array SimpTheorem := #[] - - thrms := thrms.push { - proof := ← mkAppM ``let_rule #[K, f, g] - origin := .decl ``comp_rule - rfl := false - } - - thrms := thrms.push { - proof := ← mkAppM ``let_rule_at #[K, f, g] - origin := .decl ``comp_rule - rfl := false - } - - for thm in thrms do - if let some result ← Meta.Simp.tryTheorem? e thm discharger then - return Simp.Step.visit result - return none + let .some K := e.getArg? 0 | return none + tryTheorems + #[ { proof := ← mkAppM ``let_rule #[K, f, g], origin := .decl ``let_rule, rfl := false}, + { proof := ← mkAppM ``let_rule_at #[K, f, g], origin := .decl ``let_rule, rfl := false} ] + discharger e piRule e f := do - let .some K := e.getArg? 0 - | return none - - let mut thrms : Array SimpTheorem := #[] - - thrms := thrms.push { - proof := ← mkAppM ``pi_rule #[K, f] - origin := .decl ``comp_rule - rfl := false - } - - thrms := thrms.push { - proof := ← mkAppM ``pi_rule_at #[K, f] - origin := .decl ``comp_rule - rfl := false - } - - for thm in thrms do - if let some result ← Meta.Simp.tryTheorem? e thm discharger then - return Simp.Step.visit result - return none + let .some K := e.getArg? 0 | return none + tryTheorems + #[ { proof := ← mkAppM ``pi_rule #[K, f], origin := .decl ``pi_rule, rfl := false}, + { proof := ← mkAppM ``pi_rule_at #[K, f], origin := .decl ``pi_rule, rfl := false} ] + discharger e discharger := fderiv.discharger diff --git a/SciLean/FTrans/FwdDeriv/Test.lean b/SciLean/FTrans/FwdDeriv/Test.lean index ea3c015c..6c040c7f 100644 --- a/SciLean/FTrans/FwdDeriv/Test.lean +++ b/SciLean/FTrans/FwdDeriv/Test.lean @@ -3,7 +3,74 @@ import SciLean.FTrans.FwdDeriv.Basic open SciLean variable - {K : Type _} [NontriviallyNormedField K] + {K : Type _} [NontriviallyNormedField K] + {X : Type _} [NormedAddCommGroup X] [NormedSpace K X] + {Y : Type _} [NormedAddCommGroup Y] [NormedSpace K Y] + {Z : Type _} [NormedAddCommGroup Z] [NormedSpace K Z] + {ι : Type _} [Fintype ι] + {E : ι → Type _} [∀ j, NormedAddCommGroup (E j)] [∀ j, NormedSpace K (E j)] + +example : fwdDeriv K (fun x : X => x) = fun x dx => (x,dx) := by ftrans + +example (x : X) + : fwdDeriv K (fun _ : Y => x) = fun y dy => (x, 0) := by ftrans + +example (i : ι) + : fwdDeriv K (fun (x : (i : ι) → E i) => x i) = fun x dx => (x i, dx i) := by ftrans only + +example + (f : Y → Z) (g : X → Y) + (hf : Differentiable K f) (hg : Differentiable K g) + : fwdDeriv K (fun x : X => f (g x)) + = + fun x dx => + let ydy := fwdDeriv K g x dx + let zdz := fwdDeriv K f ydy.1 ydy.2 + zdz := by ftrans + +example + (f : X → Y → Z) (g : X → Y) + (hf : Differentiable K (fun (xy : X×Y) => f xy.1 xy.2)) (hg : Differentiable K g) + : fwdDeriv K (fun x : X => let y := g x; f x y) + = + fun x dx => + let ydy := fwdDeriv K g x dx + let zdz := fwdDeriv K (fun (xy : X×Y) => f xy.1 xy.2) (x,ydy.1) (dx,ydy.2) + zdz := by ftrans + +example + (f : X → (i : ι) → E i) (hf : ∀ i, Differentiable K (f · i)) + : (fwdDeriv K fun (x : X) (i : ι) => f x i) + = + fun x dx => + (fun i => f x i, fun i => (fwdDeriv K (f · i) x dx).2) := by ftrans + +example + (f : Y → Z) (g : X → Y) (x : X) + (hf : DifferentiableAt K f (g x)) (hg : DifferentiableAt K g x) + : fwdDeriv K (fun x : X => f (g x)) x + = + fun dx => + let ydy := fwdDeriv K g x dx + let zdz := fwdDeriv K f ydy.1 ydy.2 + zdz := by ftrans + +example + (f : X → Y → Z) (g : X → Y) (x : X) + (hf : DifferentiableAt K (fun (xy : X×Y) => f xy.1 xy.2) (x, g x)) (hg : DifferentiableAt K g x) + : fwdDeriv K (fun x : X => let y := g x; f x y) x + = + fun dx => + let ydy := fwdDeriv K g x dx + let zdz := fwdDeriv K (fun (xy : X×Y) => f xy.1 xy.2) (x,ydy.1) (dx,ydy.2) + zdz := by ftrans + +example + (f : X → (i : ι) → E i) (x : X) (hf : ∀ i, DifferentiableAt K (f · i) x) + : (fwdDeriv K fun (x : X) (i : ι) => f x i) x + = + fun dx => + (fun i => f x i, fun i => (fwdDeriv K (f · i) x dx).2) := by ftrans example : fwdDeriv K (fun x : K => x + x + x + x + x) diff --git a/SciLean/FTrans/RevDeriv/Basic.lean b/SciLean/FTrans/RevDeriv/Basic.lean index 8662483c..ca7cedda 100644 --- a/SciLean/FTrans/RevDeriv/Basic.lean +++ b/SciLean/FTrans/RevDeriv/Basic.lean @@ -38,7 +38,7 @@ by -theorem const_rule (x :X) +theorem const_rule (x : X) : revDeriv K (fun _ : Y => x) = fun y => (x, fun _ => 0) := by unfold revDeriv @@ -47,6 +47,27 @@ by ext _; simp +theorem proj_rule [DecidableEq ι] (i : ι) + : revDeriv K (fun (x : PiLp 2 (fun (_ : ι) => X)) => x i) + = + fun x => + (x i, fun dxi j => if i=j then dxi else (0 : X)) := +by + unfold revDeriv + funext _ + ftrans; ftrans + set_option trace.Meta.Tactic.ftrans.step true in + set_option trace.Meta.Tactic.ftrans.unify true in + set_option trace.Meta.Tactic.ftrans.discharge true in + set_option trace.Meta.Tactic.simp.unify true in + set_option trace.Meta.Tactic.simp.rewrite true in + set_option trace.Meta.Tactic.simp.discharge true in + set_option pp.funBinderTypes true in + ftrans + ext _; simp + + + theorem comp_rule (g : X → Y) (hg : Differentiable K g) (f : Y → Z) (hf : Differentiable K f) @@ -216,11 +237,77 @@ def revDeriv.ftransExt : FTransExt where 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 + idRule := tryNamedTheorem ``id_rule discharger + constRule := tryNamedTheorem ``const_rule discharger + projRule := tryNamedTheorem ``proj_rule discharger + compRule e f g := do + let .some K := e.getArg? 0 + | return none + + let mut thrms : Array SimpTheorem := #[] + + thrms := thrms.push { + proof := ← mkAppM ``comp_rule #[K, f, g] + origin := .decl ``comp_rule + rfl := false + } + + thrms := thrms.push { + proof := ← mkAppM ``comp_rule_at #[K, f, g] + origin := .decl ``comp_rule + rfl := false + } + + for thm in thrms do + if let some result ← Meta.Simp.tryTheorem? e thm discharger then + return Simp.Step.visit result + return none + + letRule e f g := do + let .some K := e.getArg? 0 + | return none + + let mut thrms : Array SimpTheorem := #[] + + thrms := thrms.push { + proof := ← mkAppM ``let_rule #[K, f, g] + origin := .decl ``comp_rule + rfl := false + } + + thrms := thrms.push { + proof := ← mkAppM ``let_rule_at #[K, f, g] + origin := .decl ``comp_rule + rfl := false + } + + for thm in thrms do + if let some result ← Meta.Simp.tryTheorem? e thm discharger then + return Simp.Step.visit result + return none + + piRule e f := do + let .some K := e.getArg? 0 + | return none + + let mut thrms : Array SimpTheorem := #[] + + thrms := thrms.push { + proof := ← mkAppM ``pi_rule #[K, f] + origin := .decl ``comp_rule + rfl := false + } + + thrms := thrms.push { + proof := ← mkAppM ``pi_rule_at #[K, f] + origin := .decl ``comp_rule + rfl := false + } + + for thm in thrms do + if let some result ← Meta.Simp.tryTheorem? e thm discharger then + return Simp.Step.visit result + return none discharger := revDeriv.discharger diff --git a/SciLean/Mathlib/Analysis/InnerProductSpace/Prod.lean b/SciLean/Mathlib/Analysis/InnerProductSpace/Prod.lean new file mode 100644 index 00000000..a65ce8ff --- /dev/null +++ b/SciLean/Mathlib/Analysis/InnerProductSpace/Prod.lean @@ -0,0 +1,110 @@ +import Mathlib.Data.Real.Basic +import Mathlib.Data.Real.NNReal +import Mathlib.Analysis.SpecialFunctions.Pow.Real + +import Mathlib.Analysis.InnerProductSpace.PiL2 + +import Mathlib.Analysis.InnerProductSpace.Basic + +namespace SciLean + +open NNReal + + +def ProdLp (p : ℝ) (α β : Type _) := α × β + +macro α:term:35 " ×[" p:term "] " β:term:36 : term => `(ProdLp $p $α $β) +macro α:term:35 " ×₂ " β:term:36 : term => `(ProdLp 2 $α $β) + +namespace ProdLp + +variable {α b : Type _} {p : ℝ} + + +instance + [AddGroup α] [AddGroup β] : AddGroup (α ×[p] β) + := by unfold ProdLp; infer_instance + +-- @[reducible] +-- instance [AddCommMonoid α] [AddCommMonoid β] +-- : AddCommMonoid (α ×[p] β) +-- := by unfold ProdLp; infer_instance + +instance + [AddCommGroup α] [AddCommGroup β] : AddCommGroup (α ×[p] β) + := by unfold ProdLp; infer_instance + +instance [Semiring K] [AddCommGroup α] [Module K α] [AddCommGroup β] [Module K β] + : Module K (α ×[p] β) := by unfold ProdLp; infer_instance + +noncomputable +instance instDist [Dist α] [Dist β] : Dist (α ×[p] β) where + dist x y := ((dist x.1 y.1)^p + (dist x.2 y.2)^p)^(1/p) + + +-- Dist +-- PseudoMetricSpace +-- MetricSpace + +-- Norm + + +noncomputable +instance instInner [IsROrC K] + [Inner K α] [Inner K β] : Inner K (α ×₂ β) where + inner x y := Real.sqrt (IsROrC.re (@inner K _ _ x.1 y.1 + @inner K _ _ x.2 y.2)) + +noncomputable +instance instNorm + [Norm α] [Norm β] : Norm (α ×[p] β) where + norm x := sorry + + + +instance + [UniformSpace α] [UniformSpace β] + : UniformSpace (α ×[p] β) := by unfold ProdLp; infer_instance + +instance + [UniformSpace α] [CompleteSpace α] + [UniformSpace β] [CompleteSpace β] + : CompleteSpace (α ×[p] β) := by unfold ProdLp; infer_instance + +noncomputable +instance [MetricSpace α] [MetricSpace β] + : MetricSpace (α ×[p] β) where + dist_self := sorry + dist_comm := sorry + dist_triangle := sorry + edist := sorry + edist_dist := sorry + toUniformSpace := by infer_instance + uniformity_dist := sorry + toBornology := sorry + cobounded_sets := sorry + eq_of_dist_eq_zero := sorry + +noncomputable +instance [NormedAddCommGroup α] [NormedAddCommGroup β] + : NormedAddCommGroup (α ×[p] β) where + dist_eq := sorry + +noncomputable +instance [IsROrC K] + [NormedAddCommGroup α] [InnerProductSpace K α] + [NormedAddCommGroup β] [InnerProductSpace K β] + : InnerProductSpace K (α ×₂ β) where + norm_sq_eq_inner := sorry + conj_symm := sorry + add_left := sorry + smul_left := sorry + norm_smul_le := sorry + + + +-- -- TODO: move to mathlib +-- instance +-- {K : Type _} [IsROrC K] +-- {X : Type _} [NormedAddCommGroup X] [InnerProductSpace K X] [CompleteSpace X] +-- {Y : Type _} [NormedAddCommGroup Y] [InnerProductSpace K Y] [CompleteSpace Y] +-- : CompleteSpace (X × Y) := by infer_instance diff --git a/SciLean/Tactic/FTrans/Basic.lean b/SciLean/Tactic/FTrans/Basic.lean index b634e4f5..587adc89 100644 --- a/SciLean/Tactic/FTrans/Basic.lean +++ b/SciLean/Tactic/FTrans/Basic.lean @@ -65,12 +65,13 @@ def fvarAppStep (e : Expr) (ext : FTransExt) (f : Expr) : SimpM (Option Simp.Ste let (g, h) ← splitLambdaToComp f - -- trivial case? - if (← isDefEq g f ) then + -- we are agresive with transparency here as we want to deal with type synonyms + -- the motivation is to handle `ProdLp` + if (← withTransparency .all <| isDefEq g f) then trace[Meta.Tactic.ftrans.step] "trivial case fvar app, nothing to be done\n{← ppExpr e}" return none else - trace[Meta.Tactic.ftrans.step] "case fvar app\n{← ppExpr e}" + trace[Meta.Tactic.ftrans.step] "case fvar app\n{← ppExpr e}\n=\n{g}\n∘\n{h}" ext.compRule e g h @@ -88,8 +89,11 @@ def bvarAppStep (e : Expr) (ext : FTransExt) (f : Expr) : SimpM (Option Simp.Ste return none if g == (.bvar 0) then - let Lean.Expr.forallE iName iType type bi ← whnf xType - | trace[Meta.Tactic.ftrans.step] "can't handle this bvar app case, unexpected function type {← ppExpr xType}" + -- aggressively reduce to see through any possible type synonyms + -- the motivation is to handle `PiLp` + let xType' ← reduce (skipTypes := false) (← withTransparency TransparencyMode.all <| whnf xType) + let Lean.Expr.forallE iName iType type bi := xType' + | trace[Meta.Tactic.ftrans.step] "can't handle this bvar app case, unexpected function type {← ppExpr xType'}" return none ext.projRule e (.lam iName iType type bi) x else